2.12.2021, 9:00 - 11:00: Due to updates GitLab may be unavailable for some minutes between 09:00 and 11:00.

StateEquation.hs 1.63 KB
 Philipp Meyer committed May 09, 2014 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 ``````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 placeConstraints net m = bAnd \$ map checkPlaceEquation \$ places net 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) nonnegativityConstraints :: PetriNet -> ModelSI -> SBool nonnegativityConstraints net m = bAnd \$ map checkPT \$ places net ++ transitions net where checkPT x = (m M.! x) .>= 0 checkTraps :: [[String]] -> ModelSI -> SBool checkTraps traps m = bAnd \$ map checkTrapDelta traps where checkTrapDelta trap = sum (map (m M.!) trap) .>= 1 checkStateEquation :: PetriNet -> Formula -> [[String]] -> ModelSI -> SBool checkStateEquation net f traps m = placeConstraints net m &&& nonnegativityConstraints net m &&& 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``````