TransitionInvariant.hs 1.8 KB
 Philipp Meyer committed May 09, 2014 1 ``````module Solver.TransitionInvariant `````` Philipp Meyer committed May 13, 2014 2 3 `````` (checkTransitionInvariant,checkTransitionInvariantSat, firedTransitionsFromAssignment) `````` Philipp Meyer committed May 09, 2014 4 5 6 7 8 9 10 11 12 13 14 15 16 17 ``````where import Data.SBV import qualified Data.Map as M import PetriNet import Property import Solver import Solver.Formula tInvariantConstraints :: PetriNet -> ModelSI -> SBool tInvariantConstraints net m = bAnd \$ map checkTransitionEquation \$ places net where checkTransitionEquation p = `````` Philipp Meyer committed May 13, 2014 18 19 `````` let incoming = map addTransition \$ lpre net p outgoing = map addTransition \$ lpost net p `````` Philipp Meyer committed May 15, 2014 20 `````` in sum incoming - sum outgoing .>= 0 `````` Philipp Meyer committed May 13, 2014 21 `````` addTransition (t,w) = literal w * (m M.! t) `````` Philipp Meyer committed May 09, 2014 22 `````` `````` Philipp Meyer committed May 13, 2014 23 24 25 26 27 ``````finalInvariantConstraints :: ModelSI -> SBool finalInvariantConstraints m = sum (M.elems m) .> 0 nonnegativityConstraints :: ModelSI -> SBool nonnegativityConstraints m = bAnd \$ map (.>= 0) \$ M.elems m `````` Philipp Meyer committed May 09, 2014 28 `````` `````` Philipp Meyer committed May 16, 2014 29 30 31 32 33 34 35 36 37 ``````checkSComponentTransitions :: [([String],[String])] -> ModelSI -> SBool checkSComponentTransitions strans m = bAnd \$ map checkInOut strans where checkInOut (sOut,sIn) = bAnd (map (\t -> m M.! t .> 0) sOut) ==> bOr (map (\t -> m M.! t .> 0) sIn) checkTransitionInvariant :: PetriNet -> Formula -> [([String],[String])] -> ModelSI -> SBool checkTransitionInvariant net f strans m = `````` Philipp Meyer committed May 09, 2014 38 `````` tInvariantConstraints net m &&& `````` Philipp Meyer committed May 13, 2014 39 40 `````` nonnegativityConstraints m &&& finalInvariantConstraints m &&& `````` Philipp Meyer committed May 16, 2014 41 `````` checkSComponentTransitions strans m &&& `````` Philipp Meyer committed May 09, 2014 42 43 `````` evaluateFormula f m `````` Philipp Meyer committed May 16, 2014 44 45 46 47 ``````checkTransitionInvariantSat :: PetriNet -> Formula -> [([String],[String])] -> ([String], ModelSI -> SBool) checkTransitionInvariantSat net f strans = (transitions net, checkTransitionInvariant net f strans) `````` Philipp Meyer committed May 13, 2014 48 49 50 `````` firedTransitionsFromAssignment :: ModelI -> [String] firedTransitionsFromAssignment a = M.keys \$ M.filter ( > 0) a``````