Commit 01e1cc92 authored by Philipp J. Meyer's avatar Philipp J. Meyer
Browse files

Added firing vector to satisfying assignment of unique terminal marking

parent 0f385267
......@@ -44,16 +44,16 @@ checkUniqueTerminalMarking net m1 m2 x =
terminalConstraints net m1 &&&
terminalConstraints net m2
checkUniqueTerminalMarkingSat :: PetriNet -> ConstraintProblem Integer (Marking, Marking)
checkUniqueTerminalMarkingSat :: PetriNet -> ConstraintProblem Integer (Marking, Marking, FiringVector)
checkUniqueTerminalMarkingSat net =
let m1 = makeVarMap $ places net
m2 = makeVarMapWith prime $ places net
x = makeVarMap $ transitions net
in ("unique terminal marking", "pair of markings",
in ("unique terminal marking", "pair of markings and firing vector",
getNames m1 ++ getNames m2 ++ getNames x,
\fm -> checkUniqueTerminalMarking net (fmap fm m1) (fmap fm m2) (fmap fm x),
\fm -> markingsFromAssignment (fmap fm m1) (fmap fm m2))
\fm -> markingsFromAssignment (fmap fm m1) (fmap fm m2) (fmap fm x))
markingsFromAssignment :: IMap Place -> IMap Place -> (Marking, Marking)
markingsFromAssignment m1 m2 = (makeVector m1, makeVector m2)
markingsFromAssignment :: IMap Place -> IMap Place -> IMap Transition -> (Marking, Marking, FiringVector)
markingsFromAssignment m1 m2 x = (makeVector m1, makeVector m2, makeVector x)
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