LivenessInvariant.hs 6.34 KB
Newer Older
1
module Solver.LivenessInvariant (
2
3
    checkLivenessInvariantSat
  , LivenessInvariant
4
5
6
  , generateCuts
  , simplifyCuts
  , cutToLivenessInvariant
7
8
) where

9
import Data.SBV
10
import Data.List (intercalate)
11
import qualified Data.Map as M
12

13
import Util
14
import Solver
15
import Property
16
import PetriNet
17
import qualified Data.Set as S
18

19
data LivenessInvariant =
20
21
            RankingFunction (SimpleCut, Vector Place)
          | ComponentCut (SimpleCut, [Trap])
22
23
24
25
26
27
28
29
30
31

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
32
                       let d = intercalate " ∨ "
33
34
35
36
                                (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))
37
38

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

46
type SimpleCut = (S.Set Transition, [S.Set Transition])
47
type NamedCut = (S.Set Transition, [(String, S.Set Transition)])
48

49
50
placeName :: Place -> String
placeName p = "@p" ++ show p
51

52
generateCuts :: Formula Transition -> [Cut] -> [SimpleCut]
53
generateCuts f cuts =
54
            foldl combine [formulaToCut f] (map cutToSimpleDNFCuts cuts)
55
        where
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
            combine cs1 cs2 = [ (c1c0 `S.union` c2c0, c1cs ++ c2cs)
                              | (c1c0, c1cs) <- cs1, (c2c0, c2cs) <- cs2 ]

simplifyCuts :: [SimpleCut] -> [SimpleCut]
simplifyCuts = removeWith isMoreGeneralCut . concatMap simplifyCut

simplifyCut :: SimpleCut -> [SimpleCut]
simplifyCut (c0, cs) =
        let remove b a = a `S.difference` b
            cs' = removeWith S.isSubsetOf $ map (remove c0) cs
        in  if any S.null cs' then
                []
            else
                [(c0, cs')]

nameCut :: SimpleCut -> NamedCut
nameCut (c0, cs) = (c0, numPref "@comp" `zip` cs)
73

74
75
76
77
78
79
80
81
82
83
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)

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

85
86
87
88
89
cutNames :: PetriNet -> NamedCut -> [String]
cutNames net (_, c) =
        ["@yone", "@comp0"] ++
        map placeName (places net) ++
        map fst c
90

91
92
93
94
95
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)
96

97
toSimpleCut :: NamedCut -> SimpleCut
98
toSimpleCut (c0, ncs) = (c0, map snd ncs)
99

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

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

145
146
147
148
checkLivenessInvariantSat :: PetriNet -> SimpleCut -> ConstraintProblem Integer LivenessInvariant
checkLivenessInvariantSat net cut =
        let namedCut = nameCut cut
            names = cutNames net namedCut
149
150
151
            myVarMap fvm = M.fromList $ names `zip` fmap fvm names
        in  ("liveness invariant constraints", "liveness invariant",
             names,
152
153
154
155
156
157
158
159
160
161
162
             checkLivenessInvariant net namedCut . myVarMap,
             getLivenessInvariant net namedCut . myVarMap)

cutToLivenessInvariant :: Cut -> LivenessInvariant
cutToLivenessInvariant c = ComponentCut (cutToSimpleCNFCut c, map fst (fst c))

getLivenessInvariant :: PetriNet -> NamedCut -> IMap String -> LivenessInvariant
getLivenessInvariant net cut y =
        RankingFunction
                (toSimpleCut cut,
                 buildVector (map (\p -> (p, val y (placeName p))) (places net)))
163

164