LivenessInvariant.hs 6.83 KB
Newer Older
 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 Jan 30, 2015 51 52 `````` let dnfCuts = foldl combine [formulaToCut f] (map cutToSimpleDNFCuts cuts) in zipWith nameCut (numPref "@r") \$ removeWith isMoreGeneralCut dnfCuts `````` Philipp Meyer committed Dec 11, 2014 53 `````` where `````` Philipp Meyer committed Jan 30, 2015 54 55 56 `````` nameCut n (c0, cs) = (n, (c0, numPref "@comp" `zip` cs)) combine cs1 cs2 = concat [ combineCuts c1 c2 | c1 <- cs1, c2 <- cs2 ] `````` Philipp Meyer committed Jan 30, 2015 57 58 59 60 61 62 63 ``````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) `````` Philipp Meyer committed Jan 30, 2015 64 ``````combineCuts :: SimpleCut -> SimpleCut -> [SimpleCut] `````` Philipp Meyer committed Jan 30, 2015 65 66 67 68 69 70 71 72 73 74 75 76 ``````combineCuts (c1c0, c1cs) (c2c0, c2cs) = let remove b a = a `S.difference` b c0 = c1c0 `S.union` c2c0 cs = removeWith S.isSubsetOf \$ map (remove c0) \$ c1cs ++ c2cs in if any S.null cs then [] else [(c0, cs)] isMoreGeneralCut :: SimpleCut -> SimpleCut -> Bool isMoreGeneralCut (c1c0, c1cs) (c2c0, c2cs) = c1c0 `S.isSubsetOf` c2c0 && all (\c1 -> any (`S.isSubsetOf` c1) c2cs) c1cs `````` Philipp Meyer committed Dec 11, 2014 77 78 79 80 `````` varNames :: PetriNet -> [NamedCut] -> [String] varNames net = concatMap cutNames where `````` Philipp Meyer committed Jan 30, 2015 81 82 `````` cutNames (n, (_, c)) = [n ++ "@yone"] ++ [n ++ "@comp0"] ++ `````` Philipp Meyer committed Dec 19, 2014 83 `````` map (placeName n) (places net) ++ `````` Philipp Meyer committed Dec 11, 2014 84 85 `````` map (\(n', _) -> n ++ n') c `````` Philipp Meyer committed Jan 30, 2015 86 87 88 89 90 ``````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 91 `````` `````` Philipp Meyer committed Jan 30, 2015 92 93 94 ``````toSimpleCut :: NamedCut -> SimpleCut toSimpleCut (_, (c0, ncs)) = (c0, map snd ncs) `````` Philipp Meyer committed Jan 30, 2015 95 ``````formulaToCut :: Formula Transition -> SimpleCut `````` Philipp Meyer committed Dec 19, 2014 96 ``````formulaToCut = transformF `````` Philipp Meyer committed Dec 11, 2014 97 `````` where `````` Philipp Meyer committed Jan 30, 2015 98 99 100 101 102 `````` 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 103 `````` transformF (LinearInequation ts Gt (Const 0)) = `````` Philipp Meyer committed Jan 30, 2015 104 `````` (S.empty, [transformTerm ts]) `````` Philipp Meyer committed Dec 19, 2014 105 `````` transformF (LinearInequation ts Ge (Const 1)) = `````` Philipp Meyer committed Jan 30, 2015 106 `````` (S.empty, [transformTerm ts]) `````` Philipp Meyer committed Dec 19, 2014 107 `````` transformF (LinearInequation ts Eq (Const 0)) = `````` Philipp Meyer committed Jan 30, 2015 108 `````` (transformTerm ts, []) `````` Philipp Meyer committed Dec 19, 2014 109 `````` transformF (LinearInequation ts Le (Const 0)) = `````` Philipp Meyer committed Jan 30, 2015 110 `````` (transformTerm ts, []) `````` Philipp Meyer committed Dec 19, 2014 111 `````` transformF (LinearInequation ts Lt (Const 1)) = `````` Philipp Meyer committed Jan 30, 2015 112 `````` (transformTerm ts, []) `````` Philipp Meyer committed Dec 19, 2014 113 114 `````` transformF f = error \$ "formula not supported for invariant: " ++ show f `````` Philipp Meyer committed Jan 30, 2015 115 116 `````` transformTerm (t :+: u) = transformTerm t `S.union` transformTerm u transformTerm (Var x) = S.singleton x `````` Philipp Meyer committed Dec 15, 2014 117 118 `````` transformTerm t = error \$ "term not supported for invariant: " ++ show t `````` Philipp Meyer committed Dec 11, 2014 119 `````` `````` Philipp Meyer committed Dec 19, 2014 120 ``````checkCut :: PetriNet -> SIMap String -> NamedCut -> SBool `````` Philipp Meyer committed Jan 30, 2015 121 ``````checkCut net m (n, (comp0, comps)) = `````` Philipp Meyer committed Dec 11, 2014 122 `````` bAnd (map checkTransition (transitions net)) &&& `````` Philipp Meyer committed Jan 30, 2015 123 `````` val m (n ++ "@yone") + sum (map addComp comps) .> 0 &&& `````` Philipp Meyer committed Dec 19, 2014 124 `````` bAnd (map (checkNonNegativity . placeName n) (places net)) &&& `````` Philipp Meyer committed Jan 30, 2015 125 `````` checkNonNegativity (n ++ "@yone") &&& `````` Philipp Meyer committed Dec 11, 2014 126 127 128 129 130 `````` 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 131 132 133 134 135 `````` 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 136 `````` addPlace (p,w) = literal w * val m (placeName n p) `````` Philipp Meyer committed Jan 30, 2015 137 `````` addComp (n', _) = val m (n ++ n') `````` Philipp Meyer committed Dec 19, 2014 138 `````` checkNonNegativity x = val m x .>= 0 `````` Philipp Meyer committed Dec 11, 2014 139 `````` `````` Philipp Meyer committed Dec 19, 2014 140 ``````checkLivenessInvariant :: PetriNet -> [NamedCut] -> SIMap String -> SBool `````` Philipp Meyer committed Dec 11, 2014 141 142 143 ``````checkLivenessInvariant net cuts m = bAnd (map (checkCut net m) cuts) `````` Philipp Meyer committed Dec 22, 2014 144 ``````-- TODO: split up into many smaller sat problems `````` Philipp Meyer committed Dec 19, 2014 145 146 147 148 149 150 151 152 153 154 ``````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 155 `````` `````` Philipp Meyer committed Dec 19, 2014 156 157 158 159 ``````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 160 161 `````` where rankCut cut@(n, _) = RankingFunction (n, toSimpleCut cut, `````` Philipp Meyer committed Dec 19, 2014 162 163 `````` buildVector (map (\p -> (p, val y (placeName n p))) (places net))) compCut n c = ComponentCut `````` Philipp Meyer committed Jan 30, 2015 164 `````` (n, cutToSimpleCNFCut c, map fst (fst c)) `````` Philipp Meyer committed Dec 15, 2014 165 `````` `````` Philipp Meyer committed Dec 09, 2014 166