Skip to content

Commit

Permalink
tweak logic to drop one enumeration case
Browse files Browse the repository at this point in the history
  • Loading branch information
yanntm committed Apr 9, 2024
1 parent 1a10ad3 commit bd746a5
Showing 1 changed file with 3 additions and 6 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -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
}

/**
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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));
}
}
}
Expand Down

0 comments on commit bd746a5

Please sign in to comment.