LivenessInvariant.hs 6.07 KB
 Philipp Meyer committed Dec 09, 2014 1 ``````module Solver.LivenessInvariant ( `````` Philipp Meyer committed Dec 19, 2014 2 3 `````` checkLivenessInvariantSat , LivenessInvariant `````` Philipp Meyer committed Dec 09, 2014 4 5 ``````) where `````` Philipp Meyer committed Dec 11, 2014 6 ``````import Data.SBV `````` Philipp Meyer committed Dec 15, 2014 7 ``````import Data.List (intercalate) `````` Philipp Meyer committed Dec 19, 2014 8 ``````import qualified Data.Map as M `````` Philipp Meyer committed Dec 11, 2014 9 `````` `````` Philipp Meyer committed Dec 19, 2014 10 ``````import Util `````` Philipp Meyer committed Dec 11, 2014 11 ``````import Solver `````` Philipp Meyer committed Dec 15, 2014 12 ``````import Property `````` Philipp Meyer committed Dec 11, 2014 13 ``````import PetriNet `````` Philipp Meyer committed Jan 30, 2015 14 ``````import qualified Data.Set as S `````` Philipp Meyer committed Dec 11, 2014 15 `````` `````` Philipp Meyer committed Dec 19, 2014 16 ``````data LivenessInvariant = `````` Philipp Meyer committed Jan 30, 2015 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 `````` Philipp Meyer committed Dec 19, 2014 29 `````` let d = intercalate " ∨ " `````` Philipp Meyer committed Jan 30, 2015 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)) `````` Philipp Meyer committed Dec 15, 2014 34 35 `````` instance Show LivenessInvariant where `````` Philipp Meyer committed Dec 19, 2014 36 37 `````` show (RankingFunction (n, cs, xs)) = n ++ " [" ++ showSimpleCuts cs True ++ "]: " ++ `````` Philipp Meyer committed Dec 22, 2014 38 `````` intercalate " + " (map showWeighted (items xs)) `````` Philipp Meyer committed Dec 19, 2014 39 40 41 42 `````` show (ComponentCut (n, cs, ps)) = n ++ " [" ++ showSimpleCuts cs False ++ "]: " ++ show ps `````` Philipp Meyer committed Jan 30, 2015 43 44 ``````type SimpleCut = (S.Set Transition, [S.Set Transition]) type NamedCut = (String, (S.Set Transition, [(String, S.Set Transition)])) `````` Philipp Meyer committed Dec 19, 2014 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 = `````` Philipp Meyer committed Dec 15, 2014 51 `````` zipWith nameCut `````` Philipp Meyer committed Dec 19, 2014 52 `````` (numPref "@r") `````` Philipp Meyer committed Jan 30, 2015 53 `````` (foldl combine [formulaToCut f] (map cutToSimpleDNFCuts cuts)) `````` Philipp Meyer committed Dec 11, 2014 54 `````` where `````` Philipp Meyer committed Jan 30, 2015 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)] `````` Philipp Meyer committed Dec 11, 2014 60 61 62 63 `````` varNames :: PetriNet -> [NamedCut] -> [String] varNames net = concatMap cutNames where `````` Philipp Meyer committed Jan 30, 2015 64 65 `````` cutNames (n, (_, c)) = [n ++ "@yone"] ++ [n ++ "@comp0"] ++ `````` Philipp Meyer committed Dec 19, 2014 66 `````` map (placeName n) (places net) ++ `````` Philipp Meyer committed Dec 11, 2014 67 68 `````` map (\(n', _) -> n ++ n') c `````` Philipp Meyer committed Jan 30, 2015 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) `````` Philipp Meyer committed Dec 19, 2014 74 `````` `````` Philipp Meyer committed Jan 30, 2015 75 ``````formulaToCut :: Formula Transition -> SimpleCut `````` Philipp Meyer committed Dec 19, 2014 76 ``````formulaToCut = transformF `````` Philipp Meyer committed Dec 11, 2014 77 `````` where `````` Philipp Meyer committed Jan 30, 2015 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) `````` Philipp Meyer committed Dec 19, 2014 83 `````` transformF (LinearInequation ts Gt (Const 0)) = `````` Philipp Meyer committed Jan 30, 2015 84 `````` (S.empty, [transformTerm ts]) `````` Philipp Meyer committed Dec 19, 2014 85 `````` transformF (LinearInequation ts Ge (Const 1)) = `````` Philipp Meyer committed Jan 30, 2015 86 `````` (S.empty, [transformTerm ts]) `````` Philipp Meyer committed Dec 19, 2014 87 `````` transformF (LinearInequation ts Eq (Const 0)) = `````` Philipp Meyer committed Jan 30, 2015 88 `````` (transformTerm ts, []) `````` Philipp Meyer committed Dec 19, 2014 89 `````` transformF (LinearInequation ts Le (Const 0)) = `````` Philipp Meyer committed Jan 30, 2015 90 `````` (transformTerm ts, []) `````` Philipp Meyer committed Dec 19, 2014 91 `````` transformF (LinearInequation ts Lt (Const 1)) = `````` Philipp Meyer committed Jan 30, 2015 92 `````` (transformTerm ts, []) `````` Philipp Meyer committed Dec 19, 2014 93 94 `````` transformF f = error \$ "formula not supported for invariant: " ++ show f `````` Philipp Meyer committed Jan 30, 2015 95 96 `````` transformTerm (t :+: u) = transformTerm t `S.union` transformTerm u transformTerm (Var x) = S.singleton x `````` Philipp Meyer committed Dec 15, 2014 97 98 `````` transformTerm t = error \$ "term not supported for invariant: " ++ show t `````` Philipp Meyer committed Dec 11, 2014 99 `````` `````` Philipp Meyer committed Dec 19, 2014 100 ``````checkCut :: PetriNet -> SIMap String -> NamedCut -> SBool `````` Philipp Meyer committed Jan 30, 2015 101 ``````checkCut net m (n, (comp0, comps)) = `````` Philipp Meyer committed Dec 11, 2014 102 `````` bAnd (map checkTransition (transitions net)) &&& `````` Philipp Meyer committed Jan 30, 2015 103 `````` val m (n ++ "@yone") + sum (map addComp comps) .> 0 &&& `````` Philipp Meyer committed Dec 19, 2014 104 `````` bAnd (map (checkNonNegativity . placeName n) (places net)) &&& `````` Philipp Meyer committed Jan 30, 2015 105 `````` checkNonNegativity (n ++ "@yone") &&& `````` Philipp Meyer committed Dec 11, 2014 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 `````` Philipp Meyer committed Jan 30, 2015 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 `````` Philipp Meyer committed Dec 19, 2014 116 `````` addPlace (p,w) = literal w * val m (placeName n p) `````` Philipp Meyer committed Jan 30, 2015 117 `````` addComp (n', _) = val m (n ++ n') `````` Philipp Meyer committed Dec 19, 2014 118 `````` checkNonNegativity x = val m x .>= 0 `````` Philipp Meyer committed Dec 11, 2014 119 `````` `````` Philipp Meyer committed Dec 19, 2014 120 ``````checkLivenessInvariant :: PetriNet -> [NamedCut] -> SIMap String -> SBool `````` Philipp Meyer committed Dec 11, 2014 121 122 123 ``````checkLivenessInvariant net cuts m = bAnd (map (checkCut net m) cuts) `````` Philipp Meyer committed Dec 22, 2014 124 ``````-- TODO: split up into many smaller sat problems `````` Philipp Meyer committed Dec 19, 2014 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) `````` Philipp Meyer committed Dec 15, 2014 135 `````` `````` Philipp Meyer committed Dec 19, 2014 136 137 138 139 ``````getLivenessInvariant :: PetriNet -> [Cut] -> [NamedCut] -> IMap String -> [LivenessInvariant] getLivenessInvariant net cuts namedCuts y = map rankCut namedCuts ++ zipWith compCut (numPref "@cut") cuts `````` Philipp Meyer committed Jan 30, 2015 140 141 `````` where rankCut (n, (c0, cs)) = RankingFunction (n, (c0, map snd cs), `````` Philipp Meyer committed Dec 19, 2014 142 143 `````` buildVector (map (\p -> (p, val y (placeName n p))) (places net))) compCut n c = ComponentCut `````` Philipp Meyer committed Jan 30, 2015 144 `````` (n, cutToSimpleCNFCut c, map fst (fst c)) `````` Philipp Meyer committed Dec 15, 2014 145 `````` `````` Philipp Meyer committed Dec 09, 2014 146