Ecdar · Brandhoej · Mar 30, 2023 · Mar 30, 2023 · Mar 30, 2023 · Mar 30, 2023
diff --git a/src/logic/Pruning.java b/src/logic/Pruning.java
@@ -142,7 +142,8 @@ public static void addInconsistentPartsToInvariants(List<Location> locations, Li
                     l.setInvariantGuard(new FalseGuard());
                 }
                 else {
-                    CDD invarMinusIncCDD = new CDD(l.getInvariantGuard()).minus(l.getInconsistentPart());
+                    CDD invariantCDD = CDDFactory.create(l.getInvariantGuard());
+                    CDD invarMinusIncCDD = invariantCDD.minus(l.getInconsistentPart());
                     l.setInvariantGuard(invarMinusIncCDD.getGuard(clocks));
                 }
             }
@@ -158,9 +159,10 @@ public static void addInvariantsToGuards(List<Edge> edges, List<Clock> clocks) {
         for (Edge e : edges) {
             if (!(e.getTarget().getInvariantGuard() instanceof TrueGuard)) {
                 if (!(e.getTarget().getInvariantGuard() instanceof FalseGuard)) {
-                    CDD target = new CDD(e.getTarget().getInvariantGuard());
+                    CDD target = CDDFactory.create(e.getTarget().getInvariantGuard());
                     CDD cddBeforeEdge = target.transitionBack(e);
-                    e.setGuard(cddBeforeEdge.conjunction(new CDD(e.getSource().getInvariantGuard())).getGuard(clocks));
+                    CDD sourceInvariantCdd = CDDFactory.create(e.getSource().getInvariantGuard());
+                    e.setGuard(cddBeforeEdge.conjunction(sourceInvariantCdd).getGuard(clocks));
                 }
             }
         }
@@ -225,7 +227,9 @@ public static void handleOutput(Location targetLoc, Edge e, List<Edge>edges, Lis
                         // calculate and backtrack the part that is NOT inconsistent
 
                         CDD incPartOfTransThatSavesUs = new CDD(otherE.getTarget().getInconsistentPart().getPointer());
-                        CDD targetInvariantCDDOfTransThatSavesUs = new CDD(otherE.getTarget().getInvariantGuard());
+                        CDD targetInvariantCDDOfTransThatSavesUs = CDDFactory.create(
+                                otherE.getTarget().getInvariantGuard()
+                        );
                         CDD goodPart = targetInvariantCDDOfTransThatSavesUs.minus(incPartOfTransThatSavesUs);
 
                         CDD doubleCheck = goodPart.transitionBack(otherE);
@@ -237,7 +241,9 @@ public static void handleOutput(Location targetLoc, Edge e, List<Edge>edges, Lis
                         assert(doubleCheck.equiv(goodPart));
 
                         goodPart = goodPart.past(); // TODO 05.02.21: is it okay to do that?
-                        goodPart = goodPart.conjunction(new CDD(otherE.getSource().getInvariantGuard()));
+                        goodPart = goodPart.conjunction(CDDFactory.create(
+                                otherE.getSource().getInvariantGuard()
+                        ));
 
                         if (printComments)
                             Log.debug("Guards done");
@@ -248,7 +254,8 @@ public static void handleOutput(Location targetLoc, Edge e, List<Edge>edges, Lis
                         // simply apply guards
                         CDD cddOfGuard = otherE.getGuardCDD();
                         cddOfGuard = cddOfGuard.past(); // TODO 05.02.21: IMPORTANT!!!! Since invariants are not bound to start at 0 anymore, every time we use down we need to afterwards intersect with invariant
-                        cddOfGuard = cddOfGuard.conjunction(new CDD(otherE.getSource().getInvariantGuard()));
+                        CDD sourceInvariant = CDDFactory.create(otherE.getSource().getInvariantGuard());
+                        cddOfGuard = cddOfGuard.conjunction(sourceInvariant);
                         cddThatSavesUs = cddOfGuard.disjunction(cddThatSavesUs);
 
                     }
@@ -257,7 +264,8 @@ public static void handleOutput(Location targetLoc, Edge e, List<Edge>edges, Lis
             if (printComments)
                 Log.debug("Coming to the subtraction");
 
-            CDD newIncPart = new CDD(e.getSource().getInvariantGuard()).minus(cddThatSavesUs);
+            CDD sourceInvariantCdd = CDDFactory.create(e.getSource().getInvariantGuard());
+            CDD newIncPart = sourceInvariantCdd.minus(cddThatSavesUs);
             processSourceLocation(e,  newIncPart,passedPairs, inconsistentQueue);
 
 
@@ -285,7 +293,7 @@ public static void handleInput(Location targetLoc, Edge e, List<Edge> edges, Map
         CDD incCDD = e.getTarget().getInconsistentPart();
 
         // apply target invariant
-        CDD invarCDD = new CDD(e.getTarget().getInvariantGuard());
+        CDD invarCDD = CDDFactory.create(e.getTarget().getInvariantGuard());
         incCDD = invarCDD.conjunction(incCDD);
 
         incCDD = incCDD.transitionBack(e);
@@ -294,7 +302,7 @@ public static void handleInput(Location targetLoc, Edge e, List<Edge> edges, Map
         // apply updates as guard
         //incCDD = CDD.applyReset(incCDD,e.getUpdates());
 
-        if (incCDD.isFalse()) {
+        if (incCDD.equivFalse()) {
             // Checking for satisfiability after clocks were reset (only a problem because target invariant might now be x>4)
             // if unsatisfiable => keep edge // todo: is return the right thing here?
             if (printComments)
@@ -310,7 +318,7 @@ public static void handleInput(Location targetLoc, Edge e, List<Edge> edges, Map
 
 
         // if the inconsistent part cannot be reached, we can ignore the edge e, and go on
-        if (incCDD.isFalse()) {
+        if (incCDD.equivFalse()) {
             if (printComments)
                 Log.debug("could not reach inconsistent part, fed is empty");
         } else {
@@ -335,7 +343,7 @@ public static void handleInput(Location targetLoc, Edge e, List<Edge> edges, Map
                 if (printComments)
                     Log.debug("Could not be saved by an output");
                 incCDD = incCDD.past(); // TODO: Check if this works
-                incCDD = incCDD.conjunction(new CDD(e.getSource().getInvariantGuard()));
+                incCDD = incCDD.conjunction(CDDFactory.create(e.getSource().getInvariantGuard()));
             }
 
             if (printComments)
@@ -358,13 +366,13 @@ public CDD backExplorationOnTransition(Edge e, CDD incCDD)
         incCDD = incCDD.past();
 
         // apply source invariant
-        CDD invarCDD1 = new CDD(e.getSource().getInvariantGuard());
+        CDD invarCDD1 = CDDFactory.create(e.getSource().getInvariantGuard());
         incCDD = invarCDD1.conjunction(incCDD);
 
         if (printComments)
             Log.debug("Invariants done");
 
-        if (incCDD.isNotFalse()) {
+        if (incCDD.notEquivFalse()) {
             if (printComments)
                 Log.debug("Inconsistent part is reachable with this transition. ");
         } else {
@@ -383,7 +391,9 @@ public static void removeTransitionIfUnsat(Edge e,  CDD incCDD, List<Edge> edges
 
 
         // apply target invariant
-        CDD tartgetInvCDD= new CDD(e.getTarget().getInvariantGuard());
+        CDD tartgetInvCDD= CDDFactory.create(
+                e.getTarget().getInvariantGuard()
+        );
         testForSatEdgeCDD = tartgetInvCDD.conjunction(testForSatEdgeCDD);
 
         testForSatEdgeCDD = testForSatEdgeCDD.minus(e.getTarget().getInconsistentPart());
@@ -395,15 +405,17 @@ public static void removeTransitionIfUnsat(Edge e,  CDD incCDD, List<Edge> edges
         CDD guardCDD1 = e.getGuardCDD();
         testForSatEdgeCDD = guardCDD1.conjunction(testForSatEdgeCDD);
 
-        CDD sourceInvCDD = new CDD(e.getSource().getInvariantGuard());
+        CDD sourceInvCDD = CDDFactory.create(
+                e.getSource().getInvariantGuard()
+        );
         testForSatEdgeCDD = sourceInvCDD.conjunction(testForSatEdgeCDD);
 
         // remove inconsistent part
 
         testForSatEdgeCDD = testForSatEdgeCDD.minus(e.getSource().getInconsistentPart());
 
 
-        if (!testForSatEdgeCDD.isNotFalse()) {
+        if (!testForSatEdgeCDD.notEquivFalse()) {
             edges.remove(e);
         }
         if (printComments)
@@ -416,7 +428,7 @@ public static void processSourceLocation(Edge e, CDD incCDD, Map<Location, CDD>
         // If that federation is unsatisfiable, we can just ignore the transition to inc, and be done,
         // so we check for that, zone by zone. Only one zone needs to be sat.
 
-        if (incCDD.isFalse())
+        if (incCDD.equivFalse())
         {
             if (printComments)
                 Log.debug("Did not add a new inconsistent part");
@@ -463,16 +475,20 @@ public static CDD predtOfAllOutputs(Edge e, CDD incCDD, List<Edge> edges)
                 Log.debug("found an output that might lead us to good");
 
             // Ged invariant Federation
-            CDD goodCDD = new CDD(otherEdge.getTarget().getInvariantGuard());
+            CDD goodCDD = CDDFactory.create(
+                    otherEdge.getTarget().getInvariantGuard()
+            );
             goodCDD = goodCDD.minus(otherEdge.getTarget().getInconsistentPart());
 
             // constrain it by the guards and invariants  of the "good transition". TODO: IMPORTANT: Check if the order of doing the target invariant first, freeing, etc. is the correct one
 
-            if (goodCDD.isNotFalse()) {
+            if (goodCDD.notEquivFalse()) {
                 goodCDD = goodCDD.transitionBack(otherEdge);
                 //goodCDD = CDD.applyReset(goodCDD, otherEdge.getUpdates());
 
-                CDD sourceInvFed = new CDD(otherEdge.getSource().getInvariantGuard());
+                CDD sourceInvFed = CDDFactory.create(
+                        otherEdge.getSource().getInvariantGuard()
+                );
                 goodCDD = sourceInvFed.conjunction(goodCDD);
                 allGoodCDDs = allGoodCDDs.disjunction(goodCDD);
                 //Log.debug(incFederation.getZones().get(0).buildGuardsFromZone(clocks));

diff --git a/src/logic/Refinement.java b/src/logic/Refinement.java
@@ -1,6 +1,5 @@
 package logic;
 
-import lib.CDDLib;
 import log.Log;
 import models.*;
 
@@ -266,7 +265,7 @@ private StatePair buildStatePair(Transition leaderTransition, Transition followe
 
         // check if there is a part of the CDD where both leader and follower are enabled, abort otherwise
         leaderTarget.applyGuards(followerTransition.getGuardCDD());
-        if (leaderTarget.getInvariant().isFalse()) {
+        if (leaderTarget.getInvariant().equivFalse()) {
             return null;
         }
 
@@ -275,11 +274,11 @@ private StatePair buildStatePair(Transition leaderTransition, Transition followe
 
         // check target invariants to see if transitions are actually enabled
         CDD leaderTargetInvariant = leaderTransition.getTarget().getLocationInvariant();
-        if (leaderTarget.getInvariant().conjunction(leaderTargetInvariant).isFalse())
+        if (leaderTarget.getInvariant().conjunction(leaderTargetInvariant).equivFalse())
             return null;
 
         CDD followerTargetInvariant = followerTransition.getTarget().getLocationInvariant();
-        if (leaderTarget.getInvariant().conjunction(followerTargetInvariant).isFalse())
+        if (leaderTarget.getInvariant().conjunction(followerTargetInvariant).equivFalse())
             return null;
 
         // forward explored both transitions, reaching the new target states
@@ -317,7 +316,7 @@ private boolean createNewStatePairs(List<Transition> trans1, List<Transition> tr
             rightCDD = rightCDD.disjunction(c);
 
         // If trans2 does not satisfy all solution of trans1, return empty list which should result in refinement failure
-        if (!isInput && leftCDD.minus(rightCDD).isNotFalse()) {
+        if (!isInput && leftCDD.minus(rightCDD).notEquivFalse()) {
             Log.info("trans 2 does not satisfiy all solutions of trans 1");
             Log.debug("trans 2 does not satisfiy all solutions " + trans2.get(0).getEdges().get(0).getChan());
             Log.debug(leftCDD);
@@ -326,7 +325,7 @@ private boolean createNewStatePairs(List<Transition> trans1, List<Transition> tr
             return false;
         }
 
-        if (isInput && rightCDD.minus(leftCDD).isNotFalse()) {
+        if (isInput && rightCDD.minus(leftCDD).notEquivFalse()) {
             Log.info("trans 2 does not satisfiy all solutions of trans 1");
 //            Log.debug("trans 2 does not satisfiy all solutions " + trans2.get(0).getEdges().get(0).getChan());
             Log.debug(leftCDD);

diff --git a/src/logic/SimpleTransitionSystem.java b/src/logic/SimpleTransitionSystem.java
@@ -123,7 +123,7 @@ public boolean checkMovesOverlap(List<Transition> trans) {
 
 
 
-                if (state1.getInvariant().isNotFalse() && state2.getInvariant().isNotFalse()) {
+                if (state1.getInvariant().notEquivFalse() && state2.getInvariant().notEquivFalse()) {
                     if(state1.getInvariant().intersects(state2.getInvariant())) {
                         Log.debug(trans.get(i).getGuardCDD().getGuard(clocks.getItems()));
                         Log.debug(trans.get(j).getGuardCDD().getGuard(clocks.getItems()));

diff --git a/src/logic/State.java b/src/logic/State.java
@@ -62,7 +62,7 @@ public void applyResets(List<Update> resets) {
     }
 
     public void extrapolateMaxBounds(HashMap<Clock,Integer> maxBounds, List<Clock> relevantClocks){
-        if (invarCDD.isTrue())
+        if (invarCDD.equivTrue())
             return;
         CDD bcddLeftToAnalyse = new CDD(invarCDD.getPointer());
         CDD resCDD = CDD.cddFalse();
@@ -113,7 +113,7 @@ public void extrapolateMaxBounds(HashMap<Clock,Integer> maxBounds, List<Clock> r
     }
 
     public void extrapolateMaxBoundsDiag(HashMap<Clock,Integer> maxBounds, List<Clock> relevantClocks){
-        if (invarCDD.isTrue())
+        if (invarCDD.equivTrue())
             return;
         CDD copy = new CDD(invarCDD.getPointer());
         CDD resCDD = CDD.cddFalse();

diff --git a/src/logic/TransitionSystem.java b/src/logic/TransitionSystem.java
@@ -85,7 +85,7 @@ private Transition createNewTransition(State state, Move move) {
          *   that the edge guard is false and thereby the conjunction
          *   (Applying the edge guard) will result in a contradiction. */
         CDD guardCDD = CDD.cddFalse();
-        if (!edgeGuard.isFalse()) {
+        if (!edgeGuard.equivFalse()) {
             guardCDD = state.getInvariant().conjunction(edgeGuard);
         }
 
@@ -118,7 +118,7 @@ public List<Transition> createNewTransitions(State state, List<Move> moves, List
             Transition transition = createNewTransition(state, move);
 
             // Check if it is unreachable and if so then ignore it
-            if (transition.getTarget().getInvariant().isFalse()) {
+            if (transition.getTarget().getInvariant().equivFalse()) {
                 continue;
             }
 

diff --git a/src/models/Automaton.java b/src/models/Automaton.java
@@ -286,17 +286,17 @@ public void makeInputEnabled() {
                 }
 
                 // If the enabled part is true then the disabled part will be false.
-                if (enabledPart.isTrue()) {
+                if (enabledPart.equivTrue()) {
                     continue;
                 }
 
                 // If there is any solution to the enabled CDD then subtract it from the invariant.
-                if (enabledPart.isNotFalse()) {
+                if (enabledPart.notEquivFalse()) {
                     disabledPart = disabledPart.minus(enabledPart);
                 }
 
                 // If there is any solution to the disabled CDD then create an edge.
-                if (disabledPart.isNotFalse()) {
+                if (disabledPart.notEquivFalse()) {
                     Edge newEdge = new Edge(location, location, input, true, disabledPart.getGuard(), new ArrayList<>());
                     getEdges().add(newEdge);
                 }
@@ -312,7 +312,9 @@ public void addTargetInvariantToEdges() {
         boolean initialisedCdd = CDD.tryInit(clocks, BVs);
 
         for (Edge edge : getEdges()) {
-            CDD targetCDD = new CDD(edge.getTarget().getInvariantGuard());
+            CDD targetCDD = CDDFactory.create(
+                    edge.getTarget().getInvariantGuard()
+            );
             CDD past = targetCDD.transitionBack(edge);
             if (!past.equiv(CDD.cddTrue()))
                 edge.setGuard(past.conjunction(edge.getGuardCDD()).getGuard(getClocks()));