UniqueTerminalMarking.hs 5.4 KB
 Philipp J. Meyer committed Dec 19, 2016 1 2 ``````{-# LANGUAGE FlexibleContexts #-} `````` Philipp J. Meyer committed Dec 19, 2016 3 ``````module Solver.UniqueTerminalMarking `````` Philipp J. Meyer committed Dec 19, 2016 4 5 `````` (checkUniqueTerminalMarkingSat, checkUnmarkedTrapSat) `````` Philipp J. Meyer committed Dec 19, 2016 6 7 8 ``````where import Data.SBV `````` Philipp J. Meyer committed Dec 19, 2016 9 ``````import qualified Data.Map as M `````` Philipp J. Meyer committed Dec 19, 2016 10 11 12 13 14 15 `````` import Util import PetriNet import Property import Solver `````` Philipp J. Meyer committed Dec 19, 2016 16 ``````stateEquationConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Transition -> SBool `````` Philipp J. Meyer committed Dec 19, 2016 17 ``````stateEquationConstraints net m0 m x = `````` Philipp J. Meyer committed Dec 19, 2016 18 19 `````` bAnd \$ map checkStateEquation \$ places net where checkStateEquation p = `````` Philipp J. Meyer committed Dec 19, 2016 20 21 `````` let incoming = map addTransition \$ lpre net p outgoing = map addTransition \$ lpost net p `````` Philipp J. Meyer committed Dec 19, 2016 22 `````` in val m0 p + sum incoming - sum outgoing .== val m p `````` Philipp J. Meyer committed Dec 19, 2016 23 24 `````` addTransition (t,w) = literal w * val x t `````` Philipp J. Meyer committed Dec 19, 2016 25 26 27 28 ``````nonNegativityConstraints :: (Ord a, Show a) => SIMap a -> SBool nonNegativityConstraints m = bAnd \$ map checkVal \$ vals m where checkVal x = x .>= 0 `````` Philipp J. Meyer committed Dec 19, 2016 29 30 31 32 `````` terminalConstraints :: PetriNet -> SIMap Place -> SBool terminalConstraints net m = bAnd \$ map checkTransition \$ transitions net `````` Philipp J. Meyer committed Dec 19, 2016 33 `````` where checkTransition t = bOr \$ map checkPlace \$ lpre net t `````` Philipp J. Meyer committed Dec 19, 2016 34 35 `````` checkPlace (p,w) = val m p .< literal w `````` Philipp J. Meyer committed Dec 19, 2016 36 ``````nonEqualityConstraints :: (Ord a, Show a) => PetriNet -> SIMap a -> SIMap a -> SBool `````` Philipp J. Meyer committed Dec 19, 2016 37 ``````nonEqualityConstraints net m1 m2 = `````` Philipp J. Meyer committed Dec 19, 2016 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 `````` if elemsSet m1 /= elemsSet m2 then false else bOr \$ map checkNonEquality \$ elems m1 where checkNonEquality x = val m1 x ./= val m2 x checkTrap :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> Trap -> SBool checkTrap net m0 m1 m2 x1 x2 trap = checkMarkingDelta m0 m1 &&& checkMarkingDelta m0 m2 &&& checkSequenceDelta x1 m1 &&& checkSequenceDelta x2 m2 where checkMarkingDelta m0 m = sum (map (val m0) trap) .>= 1 ==> sum (map (val m) trap) .>= 1 checkSequenceDelta x m = sum (map (val x) (mpre net trap)) .>= 1 ==> sum (map (val m) trap) .>= 1 checkTrapConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> [Trap] -> SBool checkTrapConstraints net m0 m1 m2 x1 x2 traps = bAnd \$ map (checkTrap net m0 m1 m2 x1 x2) traps `````` Philipp J. Meyer committed Dec 19, 2016 58 `````` `````` Philipp J. Meyer committed Dec 19, 2016 59 60 ``````checkUniqueTerminalMarking :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> [Trap] -> SBool checkUniqueTerminalMarking net m0 m1 m2 x1 x2 traps = `````` Philipp J. Meyer committed Dec 19, 2016 61 `````` nonEqualityConstraints net m1 m2 &&& `````` Philipp J. Meyer committed Dec 19, 2016 62 63 64 65 66 67 68 `````` stateEquationConstraints net m0 m1 x1 &&& stateEquationConstraints net m0 m2 x2 &&& nonNegativityConstraints m0 &&& nonNegativityConstraints m1 &&& nonNegativityConstraints m2 &&& nonNegativityConstraints x1 &&& nonNegativityConstraints x2 &&& `````` Philipp J. Meyer committed Dec 19, 2016 69 `````` terminalConstraints net m1 &&& `````` Philipp J. Meyer committed Dec 19, 2016 70 71 72 73 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 102 103 104 105 106 `````` terminalConstraints net m2 &&& checkTrapConstraints net m0 m1 m2 x1 x2 traps checkUniqueTerminalMarkingSat :: PetriNet -> [Trap] -> ConstraintProblem Integer (Marking, Marking, Marking, FiringVector, FiringVector) checkUniqueTerminalMarkingSat net traps = let m0 = makeVarMap \$ places net m1 = makeVarMapWith prime \$ places net m2 = makeVarMapWith (prime . prime) \$ places net x1 = makeVarMap \$ transitions net x2 = makeVarMapWith prime \$ transitions net in ("unique terminal marking", "(m0, m1, m2, x1, x2)", getNames m0 ++ getNames m1 ++ getNames m2 ++ getNames x1 ++ getNames x2, \fm -> checkUniqueTerminalMarking net (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2) traps, \fm -> markingsFromAssignment (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2)) markingsFromAssignment :: IMap Place -> IMap Place -> IMap Place -> IMap Transition -> IMap Transition -> (Marking, Marking, Marking, FiringVector, FiringVector) markingsFromAssignment m0 m1 m2 x1 x2 = (makeVector m0, makeVector m1, makeVector m2, makeVector x1, makeVector x2) -- trap refinement constraints trapConstraints :: PetriNet -> SBMap Place -> SBool trapConstraints net b = bAnd \$ map trapConstraint \$ transitions net where trapConstraint t = bOr (mval b (pre net t)) ==> bOr (mval b (post net t)) trapMarkedByMarking :: PetriNet -> Marking -> SBMap Place -> SBool trapMarkedByMarking net m b = bOr \$ mval b \$ elems m trapMarkedBySequence :: PetriNet -> FiringVector -> SBMap Place -> SBool trapMarkedBySequence net x b = bOr \$ mval b \$ mpost net \$ elems x trapUnassigned :: Marking -> SBMap Place -> SBool trapUnassigned m b = bAnd \$ map (bnot . val b) \$ elems m properTrap :: SBMap Place -> SBool properTrap b = bOr \$ vals b `````` Philipp J. Meyer committed Dec 19, 2016 107 `````` `````` Philipp J. Meyer committed Dec 19, 2016 108 109 110 111 112 113 ``````checkUnmarkedTrap :: PetriNet -> Marking -> Marking -> FiringVector -> SBMap Place -> SBool checkUnmarkedTrap net m0 m x b = trapConstraints net b &&& (trapMarkedByMarking net m0 b ||| trapMarkedBySequence net x b) &&& trapUnassigned m b &&& properTrap b `````` Philipp J. Meyer committed Dec 19, 2016 114 `````` `````` Philipp J. Meyer committed Dec 19, 2016 115 116 117 118 119 120 121 ``````checkUnmarkedTrapSat :: PetriNet -> Marking -> Marking -> FiringVector -> ConstraintProblem Bool Trap checkUnmarkedTrapSat net m0 m x = let b = makeVarMap \$ places net in ("unmarked trap marked by sequence or initial marking", "trap", getNames b, \fm -> checkUnmarkedTrap net m0 m x (fmap fm b), \fm -> trapFromAssignment (fmap fm b)) `````` Philipp J. Meyer committed Dec 19, 2016 122 `````` `````` Philipp J. Meyer committed Dec 19, 2016 123 124 ``````trapFromAssignment :: BMap Place -> Trap trapFromAssignment b = M.keys \$ M.filter id b``````