LivenessInvariant.hs 5.47 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
14
import PetriNet

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

showSimpleCuts :: [SimpleCut] -> Bool -> String
showSimpleCuts cs inv = intercalate " ∧ " (map showTrans cs)
        where showTrans (ts, b) =
                  if b && inv || not b && not inv then
                       intercalate " ∧ " (map (\t -> show t ++ " ∉ σ") ts)
                  else
                       let d = intercalate " ∨ "
                                (map (\t -> show t ++ " ∈ σ") ts)
                       in  if length ts == 1 then d else "(" ++ d ++ ")"
28
29

instance Show LivenessInvariant where
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
        show (RankingFunction (n, cs, xs)) = n ++
                    " [" ++ showSimpleCuts cs True ++ "]: " ++
                    intercalate " + " (map showPlace (items xs))
                where showPlace (p, w) = show w ++ show p
        show (ComponentCut (n, cs, ps)) = n ++
                    " [" ++ showSimpleCuts cs False ++ "]: " ++
                    show ps

type SimpleCut = ([Transition], Bool)
type NamedCut = (String, [(String, SimpleCut)])

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

numPref :: String -> [String]
numPref s = map (\i -> s ++ show i) [(1::Integer)..]

generateCuts :: Formula Transition -> [Cut] -> [NamedCut]
generateCuts f cuts =
49
            zipWith nameCut
50
51
                (numPref "@r")
                (foldl combine [formulaToCut f] (map cutToSimpleCuts cuts))
52
        where
53
            nameCut n c = (n, numPref "@comp" `zip` c)
54
            combine curCuts compCut = [x : c | x <- compCut, c <- curCuts]
55
56
57
58
59
60

varNames :: PetriNet -> [NamedCut] -> [String]
varNames net = concatMap cutNames
        where
            cutNames (n, c) =
                [n ++ "@comp0"] ++
61
                map (placeName n) (places net) ++
62
63
                map (\(n', _) -> n ++ n') c

64
65
66
67
68
cutToSimpleCuts :: Cut -> [SimpleCut]
cutToSimpleCuts (ts,u) = (u, False) : map (\(_, t) -> (t, True)) ts

formulaToCut :: Formula Transition -> [SimpleCut]
formulaToCut = transformF
69
        where
70
71
72
73
74
75
76
77
78
79
80
81
82
83
            transformF FTrue = []
            transformF (p :&: q) = transformF p ++ transformF q
            transformF (LinearInequation ts Gt (Const 0)) =
                [(transformTerm ts, False)]
            transformF (LinearInequation ts Ge (Const 1)) =
                [(transformTerm ts, False)]
            transformF (LinearInequation ts Eq (Const 0)) =
                [(transformTerm ts, True)]
            transformF (LinearInequation ts Le (Const 0)) =
                [(transformTerm ts, True)]
            transformF (LinearInequation ts Lt (Const 1)) =
                [(transformTerm ts, True)]
            transformF f =
                error $ "formula not supported for invariant: " ++ show f
84
85
86
87
            transformTerm (t :+: u) = transformTerm t ++ transformTerm u
            transformTerm (Var x) = [x]
            transformTerm t =
                error $ "term not supported for invariant: " ++ show t
88

89
checkCut :: PetriNet -> SIMap String -> NamedCut -> SBool
90
91
checkCut net m (n, comps) =
            bAnd (map checkTransition (transitions net)) &&&
92
93
            val m (n ++ "@comp0") + sum (map addComp2 comps) .> 0 &&&
            bAnd (map (checkNonNegativity . placeName n) (places net)) &&&
94
95
96
97
98
            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
99
                    zeroComp = val m (n ++ "@comp0")
100
101
                    addComp1 (n', (ts, xv)) =
                        if t `elem` ts then
102
                            (if xv then 1 else (-1)) * val m (n ++ n')
103
104
105
106
                        else
                            0
                    cutComps = map addComp1 comps
                in  sum outgoing - sum incoming + zeroComp .<= sum cutComps
107
108
109
              addPlace (p,w) = literal w * val m (placeName n p)
              addComp2 (n', (_, w)) = if w then 0 else val m (n ++ n')
              checkNonNegativity x = val m x .>= 0
110

111
checkLivenessInvariant :: PetriNet -> [NamedCut] -> SIMap String -> SBool
112
113
114
checkLivenessInvariant net cuts m =
        bAnd (map (checkCut net m) cuts)

115
116
117
118
119
120
121
122
123
124
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)
125

126
127
128
129
130
131
132
133
134
getLivenessInvariant :: PetriNet -> [Cut] -> [NamedCut] -> IMap String ->
        [LivenessInvariant]
getLivenessInvariant net cuts namedCuts y =
            map rankCut namedCuts ++ zipWith compCut (numPref "@cut") cuts
        where rankCut (n, c) = RankingFunction
                (n, map snd c,
                 buildVector (map (\p -> (p, val y (placeName n p))) (places net)))
              compCut n c = ComponentCut
                (n, cutToSimpleCuts c, map fst (fst c))
135

136