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