LivenessInvariant.hs 5.47 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 14 ``````import PetriNet `````` Philipp Meyer committed Dec 19, 2014 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 ++ ")" `````` Philipp Meyer committed Dec 15, 2014 28 29 `````` instance Show LivenessInvariant where `````` Philipp Meyer committed Dec 19, 2014 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 = `````` Philipp Meyer committed Dec 15, 2014 49 `````` zipWith nameCut `````` Philipp Meyer committed Dec 19, 2014 50 51 `````` (numPref "@r") (foldl combine [formulaToCut f] (map cutToSimpleCuts cuts)) `````` Philipp Meyer committed Dec 11, 2014 52 `````` where `````` Philipp Meyer committed Dec 15, 2014 53 `````` nameCut n c = (n, numPref "@comp" `zip` c) `````` Philipp Meyer committed Dec 19, 2014 54 `````` combine curCuts compCut = [x : c | x <- compCut, c <- curCuts] `````` Philipp Meyer committed Dec 11, 2014 55 56 57 58 59 60 `````` varNames :: PetriNet -> [NamedCut] -> [String] varNames net = concatMap cutNames where cutNames (n, c) = [n ++ "@comp0"] ++ `````` Philipp Meyer committed Dec 19, 2014 61 `````` map (placeName n) (places net) ++ `````` Philipp Meyer committed Dec 11, 2014 62 63 `````` map (\(n', _) -> n ++ n') c `````` Philipp Meyer committed Dec 19, 2014 64 65 66 67 68 ``````cutToSimpleCuts :: Cut -> [SimpleCut] cutToSimpleCuts (ts,u) = (u, False) : map (\(_, t) -> (t, True)) ts formulaToCut :: Formula Transition -> [SimpleCut] formulaToCut = transformF `````` Philipp Meyer committed Dec 11, 2014 69 `````` where `````` Philipp Meyer committed Dec 19, 2014 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 `````` Philipp Meyer committed Dec 15, 2014 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 `````` Philipp Meyer committed Dec 11, 2014 88 `````` `````` Philipp Meyer committed Dec 19, 2014 89 ``````checkCut :: PetriNet -> SIMap String -> NamedCut -> SBool `````` Philipp Meyer committed Dec 11, 2014 90 91 ``````checkCut net m (n, comps) = bAnd (map checkTransition (transitions net)) &&& `````` Philipp Meyer committed Dec 19, 2014 92 93 `````` val m (n ++ "@comp0") + sum (map addComp2 comps) .> 0 &&& bAnd (map (checkNonNegativity . placeName n) (places net)) &&& `````` Philipp Meyer committed Dec 11, 2014 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 `````` Philipp Meyer committed Dec 19, 2014 99 `````` zeroComp = val m (n ++ "@comp0") `````` Philipp Meyer committed Dec 11, 2014 100 101 `````` addComp1 (n', (ts, xv)) = if t `elem` ts then `````` Philipp Meyer committed Dec 19, 2014 102 `````` (if xv then 1 else (-1)) * val m (n ++ n') `````` Philipp Meyer committed Dec 11, 2014 103 104 105 106 `````` else 0 cutComps = map addComp1 comps in sum outgoing - sum incoming + zeroComp .<= sum cutComps `````` Philipp Meyer committed Dec 19, 2014 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 `````` Philipp Meyer committed Dec 11, 2014 110 `````` `````` Philipp Meyer committed Dec 19, 2014 111 ``````checkLivenessInvariant :: PetriNet -> [NamedCut] -> SIMap String -> SBool `````` Philipp Meyer committed Dec 11, 2014 112 113 114 ``````checkLivenessInvariant net cuts m = bAnd (map (checkCut net m) cuts) `````` Philipp Meyer committed Dec 19, 2014 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) `````` Philipp Meyer committed Dec 15, 2014 125 `````` `````` Philipp Meyer committed Dec 19, 2014 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)) `````` Philipp Meyer committed Dec 15, 2014 135 `````` `````` Philipp Meyer committed Dec 09, 2014 136