LivenessInvariant.hs 6.07 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
            zipWith nameCut
52
                (numPref "@r")
53
                (foldl combine [formulaToCut f] (map cutToSimpleDNFCuts cuts))
54
        where
55
56
57
58
59
            nameCut n (c0, cs) = (n, (c0, numPref "@comp" `zip` cs))
            combine cs1 cs2 = concat [ combineCuts c1 c2 | c1 <- cs1, c2 <- cs2 ]

combineCuts :: SimpleCut -> SimpleCut -> [SimpleCut]
combineCuts (c1c0, c1cs) (c2c0, c2cs) = [(c1c0 `S.union` c2c0, c1cs ++ c2cs)]
60
61
62
63

varNames :: PetriNet -> [NamedCut] -> [String]
varNames net = concatMap cutNames
        where
64
65
            cutNames (n, (_, c)) =
                [n ++ "@yone"] ++ [n ++ "@comp0"] ++
66
                map (placeName n) (places net) ++
67
68
                map (\(n', _) -> n ++ n') c

69
70
71
72
73
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)
74

75
formulaToCut :: Formula Transition -> SimpleCut
76
formulaToCut = transformF
77
        where
78
79
80
81
82
            transformF FTrue = (S.empty, [])
            transformF (p :&: q) =
                let (p0, ps) = transformF p
                    (q0, qs) = transformF q
                in  (p0 `S.union` q0, ps ++ qs)
83
            transformF (LinearInequation ts Gt (Const 0)) =
84
                (S.empty, [transformTerm ts])
85
            transformF (LinearInequation ts Ge (Const 1)) =
86
                (S.empty, [transformTerm ts])
87
            transformF (LinearInequation ts Eq (Const 0)) =
88
                (transformTerm ts, [])
89
            transformF (LinearInequation ts Le (Const 0)) =
90
                (transformTerm ts, [])
91
            transformF (LinearInequation ts Lt (Const 1)) =
92
                (transformTerm ts, [])
93
94
            transformF f =
                error $ "formula not supported for invariant: " ++ show f
95
96
            transformTerm (t :+: u) = transformTerm t `S.union` transformTerm u
            transformTerm (Var x) = S.singleton x
97
98
            transformTerm t =
                error $ "term not supported for invariant: " ++ show t
99

100
checkCut :: PetriNet -> SIMap String -> NamedCut -> SBool
101
checkCut net m (n, (comp0, comps)) =
102
            bAnd (map checkTransition (transitions net)) &&&
103
            val m (n ++ "@yone") + sum (map addComp comps) .> 0 &&&
104
            bAnd (map (checkNonNegativity . placeName n) (places net)) &&&
105
            checkNonNegativity (n ++ "@yone") &&&
106
107
108
109
110
            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
111
112
113
114
115
                    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
116
              addPlace (p,w) = literal w * val m (placeName n p)
117
              addComp (n', _) = val m (n ++ n')
118
              checkNonNegativity x = val m x .>= 0
119

120
checkLivenessInvariant :: PetriNet -> [NamedCut] -> SIMap String -> SBool
121
122
123
checkLivenessInvariant net cuts m =
        bAnd (map (checkCut net m) cuts)

124
-- TODO: split up into many smaller sat problems
125
126
127
128
129
130
131
132
133
134
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)
135

136
137
138
139
getLivenessInvariant :: PetriNet -> [Cut] -> [NamedCut] -> IMap String ->
        [LivenessInvariant]
getLivenessInvariant net cuts namedCuts y =
            map rankCut namedCuts ++ zipWith compCut (numPref "@cut") cuts
140
141
        where rankCut (n, (c0, cs)) = RankingFunction
                (n, (c0, map snd cs),
142
143
                 buildVector (map (\p -> (p, val y (placeName n p))) (places net)))
              compCut n c = ComponentCut
144
                (n, cutToSimpleCNFCut c, map fst (fst c))
145

146