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

10
import Data.SBV
11
import Data.List (intercalate)
12
import qualified Data.Map as M
13
import qualified Data.Set as S
14

15
import Util
16
import Solver
17
import Property
18
19
import PetriNet

20
data LivenessInvariant =
21
22
            RankingFunction (SimpleCut, Vector Place)
          | ComponentCut (SimpleCut, [Trap])
23

24
25
showSimpleCuts :: SimpleCut -> String
showSimpleCuts cs = intercalate " ∧ " (showSimpleCut cs)
26
27
        where showSimpleCut (ts0, cs1) =
                if S.null ts0 then
28
                    map (showTrans True) cs1
29
                else
30
                    showTrans False ts0 : map (showTrans True) cs1
31
32
              showTrans pos ts =
                  if pos then
33
                       let d = intercalate " ∨ "
34
35
36
37
                                (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))
38
39

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

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

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

53
generateCuts :: Formula Transition -> [Cut] -> [SimpleCut]
54
generateCuts f cuts =
55
            foldl combine [formulaToCut f] (map cutToSimpleDNFCuts cuts)
56
        where
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
            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)
74

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

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

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

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

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

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

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