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

Commit f8ce8a20 authored by Philipp J. Meyer's avatar Philipp J. Meyer

changed order of constraints for terminal markings with unique consensus

parent 2c4fc15f
......@@ -84,10 +84,9 @@ checkInequalityConstraints net m0 m1 m2 inequalities =
checkTerminalMarkingsUniqueConsensus :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition ->
[Trap] -> [Siphon] -> [StableInequality] -> SBool
checkTerminalMarkingsUniqueConsensus net m0 m1 m2 x1 x2 traps siphons inequalities =
initialMarkingConstraints net m0 &&&
differentConsensusConstraints net m1 m2 &&&
stateEquationConstraints net m0 m1 x1 &&&
stateEquationConstraints net m0 m2 x2 &&&
initialMarkingConstraints net m0 &&&
nonNegativityConstraints m0 &&&
nonNegativityConstraints m1 &&&
nonNegativityConstraints m2 &&&
......@@ -95,8 +94,10 @@ checkTerminalMarkingsUniqueConsensus net m0 m1 m2 x1 x2 traps siphons inequaliti
nonNegativityConstraints x2 &&&
terminalConstraints net m1 &&&
terminalConstraints net m2 &&&
differentConsensusConstraints net m1 m2 &&&
checkTrapConstraints net m0 m1 m2 x1 x2 traps &&&
checkSiphonConstraints net m0 m1 m2 x1 x2 siphons &&&
checkSubnetSiphonConstraints net m0 m1 m2 x1 x2 siphons &&&
checkInequalityConstraints net m0 m1 m2 inequalities
checkTerminalMarkingsUniqueConsensusSat :: PetriNet -> [Trap] -> [Siphon] -> [StableInequality] -> ConstraintProblem Integer TerminalMarkingsUniqueConsensusCounterExample
......
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