LivenessInvariant.hs 6.83 KB
Newer Older
1
module Solver.LivenessInvariant (
2
3
    checkLivenessInvariantSat
  , LivenessInvariant
4
5
) where

6
import Data.SBV
7
import Data.List (intercalate)
8
import qualified Data.Map as M
9

10
import Util
11
import Solver
12
import Property
13
import PetriNet
14
import qualified Data.Set as S
15

16
data LivenessInvariant =
17
18
19
20
21
22
23
24
25
26
27
28
            RankingFunction (String, SimpleCut, Vector Place)
          | ComponentCut (String, SimpleCut, [Trap])

showSimpleCuts :: SimpleCut -> Bool -> String
showSimpleCuts cs inv = intercalate " ∧ " (showSimpleCut cs)
        where showSimpleCut (ts0, cs1) =
                if S.null ts0 then
                    map (showTrans inv) cs1
                else
                    showTrans (not inv) ts0 : map (showTrans inv) cs1
              showTrans pos ts =
                  if pos then
29
                       let d = intercalate " ∨ "
30
31
32
33
                                (map (\t -> show t ++ " ∈ σ") (S.toList ts))
                       in  if S.size ts == 1 then d else "(" ++ d ++ ")"
                  else
                       intercalate " ∧ " (map (\t -> show t ++ " ∉ σ") (S.toList ts))
34
35

instance Show LivenessInvariant where
36
37
        show (RankingFunction (n, cs, xs)) = n ++
                    " [" ++ showSimpleCuts cs True ++ "]: " ++
38
                    intercalate " + " (map showWeighted (items xs))
39
40
41
42
        show (ComponentCut (n, cs, ps)) = n ++
                    " [" ++ showSimpleCuts cs False ++ "]: " ++
                    show ps

43
44
type SimpleCut = (S.Set Transition, [S.Set Transition])
type NamedCut = (String, (S.Set Transition, [(String, S.Set Transition)]))
45
46
47
48
49
50

placeName :: String -> Place -> String
placeName n p = n ++ "@p" ++ show p

generateCuts :: Formula Transition -> [Cut] -> [NamedCut]
generateCuts f cuts =
51
52
        let dnfCuts = foldl combine [formulaToCut f] (map cutToSimpleDNFCuts cuts)
        in  zipWith nameCut (numPref "@r") $ removeWith isMoreGeneralCut dnfCuts
53
        where
54
55
56
            nameCut n (c0, cs) = (n, (c0, numPref "@comp" `zip` cs))
            combine cs1 cs2 = concat [ combineCuts c1 c2 | c1 <- cs1, c2 <- cs2 ]

57
58
59
60
61
62
63
removeWith :: (a -> a -> Bool) -> [a] -> [a]
removeWith f = removeCuts' []
        where
            removeCuts' acc [] = reverse acc
            removeCuts' acc (x:xs) = removeCuts' (x : cutFilter x acc) (cutFilter x xs)
            cutFilter cut = filter (not . f cut)

64
combineCuts :: SimpleCut -> SimpleCut -> [SimpleCut]
65
66
67
68
69
70
71
72
73
74
75
76
combineCuts (c1c0, c1cs) (c2c0, c2cs) =
        let remove b a = a `S.difference` b
            c0 = c1c0 `S.union` c2c0
            cs = removeWith S.isSubsetOf $ map (remove c0) $ c1cs ++ c2cs
        in  if any S.null cs then
                []
            else
                [(c0, cs)]

isMoreGeneralCut :: SimpleCut -> SimpleCut -> Bool
isMoreGeneralCut (c1c0, c1cs) (c2c0, c2cs) =
        c1c0 `S.isSubsetOf` c2c0 && all (\c1 -> any (`S.isSubsetOf` c1) c2cs) c1cs
77
78
79
80

varNames :: PetriNet -> [NamedCut] -> [String]
varNames net = concatMap cutNames
        where
81
82
            cutNames (n, (_, c)) =
                [n ++ "@yone"] ++ [n ++ "@comp0"] ++
83
                map (placeName n) (places net) ++
84
85
                map (\(n', _) -> n ++ n') c

86
87
88
89
90
cutToSimpleDNFCuts :: Cut -> [SimpleCut]
cutToSimpleDNFCuts (ts, u) = (S.empty, [S.fromList u]) : map (\(_, t) -> (S.fromList t, [])) ts

cutToSimpleCNFCut :: Cut -> SimpleCut
cutToSimpleCNFCut (ts, u) = (S.fromList u, map (\(_, t) -> S.fromList t) ts)
91

92
93
94
toSimpleCut :: NamedCut -> SimpleCut
toSimpleCut (_, (c0, ncs)) = (c0, map snd ncs)

95
formulaToCut :: Formula Transition -> SimpleCut
96
formulaToCut = transformF
97
        where
98
99
100
101
102
            transformF FTrue = (S.empty, [])
            transformF (p :&: q) =
                let (p0, ps) = transformF p
                    (q0, qs) = transformF q
                in  (p0 `S.union` q0, ps ++ qs)
103
            transformF (LinearInequation ts Gt (Const 0)) =
104
                (S.empty, [transformTerm ts])
105
            transformF (LinearInequation ts Ge (Const 1)) =
106
                (S.empty, [transformTerm ts])
107
            transformF (LinearInequation ts Eq (Const 0)) =
108
                (transformTerm ts, [])
109
            transformF (LinearInequation ts Le (Const 0)) =
110
                (transformTerm ts, [])
111
            transformF (LinearInequation ts Lt (Const 1)) =
112
                (transformTerm ts, [])
113
114
            transformF f =
                error $ "formula not supported for invariant: " ++ show f
115
116
            transformTerm (t :+: u) = transformTerm t `S.union` transformTerm u
            transformTerm (Var x) = S.singleton x
117
118
            transformTerm t =
                error $ "term not supported for invariant: " ++ show t
119

120
checkCut :: PetriNet -> SIMap String -> NamedCut -> SBool
121
checkCut net m (n, (comp0, comps)) =
122
            bAnd (map checkTransition (transitions net)) &&&
123
            val m (n ++ "@yone") + sum (map addComp comps) .> 0 &&&
124
            bAnd (map (checkNonNegativity . placeName n) (places net)) &&&
125
            checkNonNegativity (n ++ "@yone") &&&
126
127
128
129
130
            checkNonNegativity (n ++ "@comp0") &&&
            bAnd (map (\(n', _) -> checkNonNegativity (n ++ n')) comps)
        where checkTransition t =
                let incoming = map addPlace $ lpre net t
                    outgoing = map addPlace $ lpost net t
131
132
133
134
135
                    yone = val m (n ++ "@yone")
                    addCompT (n', ts) = if t `S.member` ts then val m (n ++ n') else 0
                    comp0Val = addCompT ("@comp0", comp0)
                    compsVal = sum $ map addCompT comps
                in  sum outgoing - sum incoming + yone + compsVal .<= comp0Val
136
              addPlace (p,w) = literal w * val m (placeName n p)
137
              addComp (n', _) = val m (n ++ n')
138
              checkNonNegativity x = val m x .>= 0
139

140
checkLivenessInvariant :: PetriNet -> [NamedCut] -> SIMap String -> SBool
141
142
143
checkLivenessInvariant net cuts m =
        bAnd (map (checkCut net m) cuts)

144
-- TODO: split up into many smaller sat problems
145
146
147
148
149
150
151
152
153
154
checkLivenessInvariantSat :: PetriNet -> Formula Transition -> [Cut] ->
        ConstraintProblem Integer [LivenessInvariant]
checkLivenessInvariantSat net f cuts =
        let namedCuts = generateCuts f cuts
            names = varNames net namedCuts
            myVarMap fvm = M.fromList $ names `zip` fmap fvm names
        in  ("liveness invariant constraints", "liveness invariant",
             names,
             checkLivenessInvariant net namedCuts . myVarMap,
             getLivenessInvariant net cuts namedCuts . myVarMap)
155

156
157
158
159
getLivenessInvariant :: PetriNet -> [Cut] -> [NamedCut] -> IMap String ->
        [LivenessInvariant]
getLivenessInvariant net cuts namedCuts y =
            map rankCut namedCuts ++ zipWith compCut (numPref "@cut") cuts
160
161
        where rankCut cut@(n, _) = RankingFunction
                (n, toSimpleCut cut,
162
163
                 buildVector (map (\p -> (p, val y (placeName n p))) (places net)))
              compCut n c = ComponentCut
164
                (n, cutToSimpleCNFCut c, map fst (fst c))
165

166