LivenessInvariant.hs 3.88 KB
Newer Older
1
module Solver.LivenessInvariant (
2
3
    checkLivenessInvariantSat
  , LivenessInvariant
4
  , cutToLivenessInvariant
5
  , SimpleCut
6
7
) where

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

13
import Util
14
import Solver
15
import Solver.Simplifier
16
17
import PetriNet

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

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

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

45
type NamedCut = (S.Set Transition, [(String, S.Set Transition)])
46

47
48
placeName :: Place -> String
placeName p = "@p" ++ show p
49

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

53
54
55
56
57
cutNames :: PetriNet -> NamedCut -> [String]
cutNames net (_, c) =
        ["@yone", "@comp0"] ++
        map placeName (places net) ++
        map fst c
58

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

62
toSimpleCut :: NamedCut -> SimpleCut
63
toSimpleCut (c0, ncs) = (c0, map snd ncs)
64

65
66
checkLivenessInvariant :: PetriNet -> NamedCut -> SIMap String -> SBool
checkLivenessInvariant net (comp0, comps) m =
67
            bAnd (map checkTransition (transitions net)) &&&
68
69
70
71
72
            val m "@yone" + sum (map addComp comps) .> 0 &&&
            bAnd (map (checkNonNegativity . placeName) (places net)) &&&
            checkNonNegativity "@yone" &&&
            checkNonNegativity "@comp0" &&&
            bAnd (map (\(n, _) -> checkNonNegativity n) comps)
73
74
75
        where checkTransition t =
                let incoming = map addPlace $ lpre net t
                    outgoing = map addPlace $ lpost net t
76
77
                    yone = val m "@yone"
                    addCompT (n, ts) = if t `S.member` ts then val m n else 0
78
79
80
                    comp0Val = addCompT ("@comp0", comp0)
                    compsVal = sum $ map addCompT comps
                in  sum outgoing - sum incoming + yone + compsVal .<= comp0Val
81
82
              addPlace (p,w) = literal w * val m (placeName p)
              addComp (n, _) = val m n
83
              checkNonNegativity x = val m x .>= 0
84

85
86
87
88
checkLivenessInvariantSat :: PetriNet -> SimpleCut -> ConstraintProblem Integer LivenessInvariant
checkLivenessInvariantSat net cut =
        let namedCut = nameCut cut
            names = cutNames net namedCut
89
90
91
            myVarMap fvm = M.fromList $ names `zip` fmap fvm names
        in  ("liveness invariant constraints", "liveness invariant",
             names,
92
93
94
95
96
97
98
99
100
101
102
             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)))