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

Commit 1e1bcf37 authored by Philipp J. Meyer's avatar Philipp J. Meyer
Browse files

Added remaining constraints for unique terminal marking

parent da341783
...@@ -9,26 +9,40 @@ import PetriNet ...@@ -9,26 +9,40 @@ import PetriNet
import Property import Property
import Solver import Solver
placeConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Transition -> SBool stateEquationConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Transition -> SBool
placeConstraints net m1 m2 x = stateEquationConstraints net m1 m2 x =
bAnd $ map checkPlaceEquation $ places net bAnd $ map checkStateEquation $ places net
where checkPlaceEquation p = where checkStateEquation p =
let incoming = map addTransition $ lpre net p let incoming = map addTransition $ lpre net p
outgoing = map addTransition $ lpost net p outgoing = map addTransition $ lpost net p
in val m1 p + sum incoming - sum outgoing .== val m2 p in val m1 p + sum incoming - sum outgoing .== val m2 p
addTransition (t,w) = literal w * val x t addTransition (t,w) = literal w * val x t
nonNegativityConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SBool nonNegativityConstraints :: PetriNet -> SIMap Place -> SBool
nonNegativityConstraints net m1 m2 = nonNegativityConstraints net m =
let m1nn = map (checkVal m1) $ places net bAnd $ map checkVal $ places net
m2nn = map (checkVal m1) $ places net where checkVal p = val m p .>= 0
in bAnd m1nn &&& bAnd m2nn
where checkVal mapping n = val mapping n .>= 0 terminalConstraints :: PetriNet -> SIMap Place -> SBool
terminalConstraints net m =
bAnd $ map checkTransition $ transitions net
where checkTransition :: Transition -> SBool
checkTransition t = bOr $ map checkPlace $ lpre net t
checkPlace (p,w) = val m p .< literal w
nonEqualityConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SBool
nonEqualityConstraints net m1 m2 =
bOr $ map checkNonEquality $ places net
where checkNonEquality p = val m1 p ./= val m2 p
checkUniqueTerminalMarking :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Transition -> SBool checkUniqueTerminalMarking :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Transition -> SBool
checkUniqueTerminalMarking net m1 m2 x = checkUniqueTerminalMarking net m1 m2 x =
placeConstraints net m1 m2 x &&& nonEqualityConstraints net m1 m2 &&&
nonNegativityConstraints net m1 m2 stateEquationConstraints net m1 m2 x &&&
nonNegativityConstraints net m1 &&&
nonNegativityConstraints net m2 &&&
terminalConstraints net m1 &&&
terminalConstraints net m2
checkUniqueTerminalMarkingSat :: PetriNet -> ConstraintProblem Integer (Marking, Marking) checkUniqueTerminalMarkingSat :: PetriNet -> ConstraintProblem Integer (Marking, Marking)
checkUniqueTerminalMarkingSat net = checkUniqueTerminalMarkingSat net =
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment