LivenessInvariant.hs 4.59 KB
 Philipp Meyer committed Dec 09, 2014 1 2 3 ``````module Solver.LivenessInvariant ( checkLivenessInvariant , checkLivenessInvariantSat `````` Philipp Meyer committed Dec 15, 2014 4 `````` , generateCuts `````` Philipp Meyer committed Dec 09, 2014 5 6 `````` , getLivenessInvariant , PlaceVector `````` Philipp Meyer committed Dec 15, 2014 7 `````` , LivenessInvariant(..) `````` Philipp Meyer committed Dec 09, 2014 8 9 ``````) where `````` Philipp Meyer committed Dec 11, 2014 10 ``````import Data.SBV `````` Philipp Meyer committed Dec 15, 2014 11 ``````import Data.List (intercalate) `````` Philipp Meyer committed Dec 11, 2014 12 13 14 `````` import Solver import Solver.SComponent `````` Philipp Meyer committed Dec 15, 2014 15 ``````import Property `````` Philipp Meyer committed Dec 11, 2014 16 17 18 ``````import PetriNet type PlaceVector = [(String, Integer)] `````` Philipp Meyer committed Dec 15, 2014 19 20 21 22 23 24 25 26 27 28 29 30 31 32 ``````newtype LivenessInvariant = LivenessInvariant { getInv :: (String, [Cut], PlaceVector) } instance Show LivenessInvariant where show (LivenessInvariant (n, cs, xs)) = n ++ " [" ++ intercalate " ∧ " (map showTrans cs) ++ "]: " ++ intercalate " + " (map showPlace (filter ((> 0) . snd) xs)) where showPlace (p, w) = show w ++ p showTrans (ts, b) = if b then intercalate " ∧ " (map (++ " ∉ σ") ts) else let d = intercalate " ∨ " (map (++ " ∈ σ") ts) in if length ts == 1 then d else "(" ++ d ++ ")" `````` Philipp Meyer committed Dec 09, 2014 33 `````` `````` Philipp Meyer committed Dec 11, 2014 34 35 36 ``````type Cut = ([String], Bool) type NamedCut = (String, [(String, Cut)]) `````` Philipp Meyer committed Dec 15, 2014 37 38 39 40 41 ``````generateCuts :: Formula -> [SCompCut] -> [NamedCut] generateCuts f comps = zipWith nameCut (numPref "@part") (foldl combine [formulaToCut f] comps) `````` Philipp Meyer committed Dec 11, 2014 42 `````` where `````` Philipp Meyer committed Dec 15, 2014 43 `````` nameCut n c = (n, numPref "@comp" `zip` c) `````` Philipp Meyer committed Dec 11, 2014 44 `````` numPref s = map (\i -> s ++ show i) [(1::Integer)..] `````` Philipp Meyer committed Dec 15, 2014 45 `````` combine cuts compCut = [x : c | x <- compCut, c <- cuts] `````` Philipp Meyer committed Dec 11, 2014 46 47 48 49 50 51 52 53 54 `````` varNames :: PetriNet -> [NamedCut] -> [String] varNames net = concatMap cutNames where cutNames (n, c) = [n ++ "@comp0"] ++ map (\p -> n ++ "@p" ++ p) (places net) ++ map (\(n', _) -> n ++ n') c `````` Philipp Meyer committed Dec 15, 2014 55 56 ``````formulaToCut :: Formula -> SCompCut formulaToCut = transformConj `````` Philipp Meyer committed Dec 11, 2014 57 `````` where `````` Philipp Meyer committed Dec 15, 2014 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 `````` transformConj FTrue = [] transformConj (p :&: q) = transformConj p ++ transformConj q transformConj (Atom lieq) = transformLieq lieq transformConj form = error \$ "formula not supported for invariant: " ++ show form transformLieq (LinIneq ts Gt (Const 0)) = [(transformTerm ts, False)] transformLieq (LinIneq ts Ge (Const 1)) = [(transformTerm ts, False)] transformLieq (LinIneq ts Eq (Const 0)) = [(transformTerm ts, True)] transformLieq (LinIneq ts Le (Const 0)) = [(transformTerm ts, True)] transformLieq (LinIneq ts Lt (Const 1)) = [(transformTerm ts, True)] transformLieq l = error \$ "linear inequation not supported for invariant: " ++ show l 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 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 `````` checkCut :: PetriNet -> ModelSI -> NamedCut -> SBool checkCut net m (n, comps) = bAnd (map checkTransition (transitions net)) &&& mVal m (n ++ "@comp0") + sum (map addComp2 comps) .> 0 &&& bAnd (map (\p -> checkNonNegativity (n ++ "@p" ++ p)) (places net)) &&& 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 zeroComp = mVal m (n ++ "@comp0") addComp1 (n', (ts, xv)) = if t `elem` ts then (if xv then 1 else (-1)) * mVal m (n ++ n') else 0 cutComps = map addComp1 comps in sum outgoing - sum incoming + zeroComp .<= sum cutComps addPlace (p,w) = literal w * mVal m (n ++ "@p" ++ p) addComp2 (n', (_, w)) = if w then 0 else mVal m (n ++ n') checkNonNegativity x = mVal m x .>= 0 checkLivenessInvariant :: PetriNet -> [NamedCut] -> ModelSI -> SBool checkLivenessInvariant net cuts m = bAnd (map (checkCut net m) cuts) `````` Philipp Meyer committed Dec 15, 2014 102 ``````checkLivenessInvariantSat :: PetriNet -> [NamedCut] -> `````` Philipp Meyer committed Dec 09, 2014 103 `````` ([String], ModelSI -> SBool) `````` Philipp Meyer committed Dec 15, 2014 104 105 106 107 108 109 110 111 ``````checkLivenessInvariantSat net cuts = (varNames net cuts, checkLivenessInvariant net cuts) getLivenessInvariant :: PetriNet -> [NamedCut] -> ModelI -> [LivenessInvariant] getLivenessInvariant net cuts as = map lookupCut cuts where lookupCut (n, c) = LivenessInvariant (n, map snd c, map (\p -> (p, mVal as (n ++ "@p" ++ p))) (places net)) `````` Philipp Meyer committed Dec 09, 2014 112