StateEquation.hs 1.63 KB
 Philipp Meyer committed May 09, 2014 1 2 3 4 5 6 7 8 9 10 11 12 13 ``````module Solver.StateEquation (checkStateEquation,checkStateEquationSat, markedPlacesFromAssignment) where import Data.SBV import PetriNet import Property import Solver import Solver.Formula placeConstraints :: PetriNet -> ModelSI -> SBool `````` Philipp Meyer committed May 13, 2014 14 ``````placeConstraints net m = bAnd \$ map checkPlaceEquation \$ places net `````` Philipp Meyer committed May 09, 2014 15 16 17 18 `````` where checkPlaceEquation p = let incoming = map addTransition \$ lpre net p outgoing = map addTransition \$ lpost net p pinit = literal \$ initial net p `````` Philipp Meyer committed May 16, 2014 19 20 `````` in pinit + sum incoming - sum outgoing .== mVal m p addTransition (t,w) = literal w * mVal m t `````` Philipp Meyer committed May 09, 2014 21 `````` `````` Philipp Meyer committed Dec 02, 2014 22 23 24 25 26 ``````nonNegativityConstraints :: PetriNet -> ModelSI -> SBool nonNegativityConstraints net m = bAnd (map checkNonNegativity (places net)) &&& bAnd (map checkNonNegativity (transitions net)) where checkNonNegativity x = mVal m x .>= 0 `````` Philipp Meyer committed May 09, 2014 27 28 `````` checkTraps :: [[String]] -> ModelSI -> SBool `````` Philipp Meyer committed May 13, 2014 29 ``````checkTraps traps m = bAnd \$ map checkTrapDelta traps `````` Philipp Meyer committed May 16, 2014 30 `````` where checkTrapDelta trap = sum (map (mVal m) trap) .>= 1 `````` Philipp Meyer committed May 09, 2014 31 32 33 34 `````` checkStateEquation :: PetriNet -> Formula -> [[String]] -> ModelSI -> SBool checkStateEquation net f traps m = placeConstraints net m &&& `````` Philipp Meyer committed Dec 02, 2014 35 `````` nonNegativityConstraints net m &&& `````` Philipp Meyer committed May 09, 2014 36 37 38 39 40 41 42 43 44 `````` checkTraps traps m &&& evaluateFormula f m checkStateEquationSat :: PetriNet -> Formula -> [[String]] -> ([String], ModelSI -> SBool) checkStateEquationSat net f traps = (places net ++ transitions net, checkStateEquation net f traps) markedPlacesFromAssignment :: PetriNet -> ModelI -> [String] `````` Philipp Meyer committed May 16, 2014 45 ``markedPlacesFromAssignment net a = filter (cElem a) \$ places net``