From bd746a58ed069680497518184dbafb8e7a5f5539 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Tue, 9 Apr 2024 16:41:30 +0200 Subject: [PATCH] tweak logic to drop one enumeration case --- .../application/solver/ExclusiveImplicantsComputer.java | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/solver/ExclusiveImplicantsComputer.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/solver/ExclusiveImplicantsComputer.java index 04a8ab3692..cb5b44c08f 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/solver/ExclusiveImplicantsComputer.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/solver/ExclusiveImplicantsComputer.java @@ -27,7 +27,7 @@ public class ExclusiveImplicantsComputer { private static final int DEBUG = 0; public enum ProblemType { - B_IMPLIES_A, A_IMPLIES_B, A_EXCLUSIVE_B + A_IMPLIES_B, A_EXCLUSIVE_B } /** @@ -64,9 +64,6 @@ public String printConstraint(SparsePetriNet spn) { case A_IMPLIES_B: sb.append(" => "); break; - case B_IMPLIES_A: - sb.append(" <= "); - break; case A_EXCLUSIVE_B: sb.append(" <> "); break; @@ -400,10 +397,10 @@ private static void testInvariants(SparseIntArray a, SparseIntArray b, MccTransl SparseIntArray consNotFeedA = SparseIntArray.removeAll(consA, feedA); if (consNotFeedA.size() > 0) { // must be drain transitions of B - problems.add(new DrainProblem(b, consNotFeedA, ProblemType.B_IMPLIES_A, a, b)); + problems.add(new DrainProblem(b, consNotFeedA, ProblemType.A_IMPLIES_B, b, a)); } else { // Ok, we proved it without SMT. - constraints.add(new Constraint(ProblemType.B_IMPLIES_A, a, b)); + constraints.add(new Constraint(ProblemType.A_IMPLIES_B, b, a)); } } }