Fix/quotient

src/connection/GrpcServer.java

@@ -2,7 +2,6 @@
 
 import io.grpc.Server;
 import io.grpc.netty.shaded.io.grpc.netty.NettyServerBuilder;
-import log.Log;
 
 import java.io.IOException;
 import java.net.InetSocketAddress;

src/logic/Bisimilarity.java

@@ -126,7 +126,7 @@ public static Automaton checkBisimilarity(Automaton aut1) {
                             List<Update> updates = edgeList.get(0).getUpdates();
                             CDD allCDDs = CDD.cddFalse();
                             for (Edge e : edgeList) {
-                                CDD targetFedAfterReset = e.getTarget().getInvariantCdd();
+                                CDD targetFedAfterReset = e.getTarget().getInvariantCddEager();
                                 targetFedAfterReset = targetFedAfterReset.applyReset(e.getUpdates());
                                 allCDDs = allCDDs.disjunction(e.getGuardCDD().conjunction(targetFedAfterReset));
 
@@ -157,7 +157,7 @@ private static int getIndexOfClock(Clock clock, List<Clock> clocks) {
 
     public static boolean hasDifferentZone(Location l1, Location l2, List<Clock> clocks)
     {
-        if (l1.getInvariantCdd().equiv(l2.getInvariantCdd())) {
+        if (l1.getInvariantCddEager().equiv(l2.getInvariantCddEager())) {
             return false;
         }
         return true;
@@ -176,8 +176,8 @@ public static boolean hasDifferentOutgoings(Location l1, Location l2, List<Clock
                 edgesL2.add(e);
         }
 
-        CDD s1 = l1.getInvariantCdd();
-        CDD s2 = l2.getInvariantCdd();
+        CDD s1 = l1.getInvariantCddEager();
+        CDD s2 = l2.getInvariantCddEager();
 
         for (Edge e1 : edgesL1)
         {

src/logic/Pruning.java

@@ -142,7 +142,7 @@ public static void addInconsistentPartsToInvariants(List<Location> locations, Li
                     l.setInvariantGuard(new FalseGuard());
                 }
                 else {
-                    CDD invarMinusIncCDD = l.getInvariantCdd().minus(l.getInconsistentPart());
+                    CDD invarMinusIncCDD = l.getInvariantCddEager().minus(l.getInconsistentPart());
                     l.setInvariantGuard(invarMinusIncCDD.getGuard(clocks));
                 }
             }
@@ -158,9 +158,9 @@ 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 = e.getTarget().getInvariantCdd();
+                    CDD target = e.getTarget().getInvariantCddEager();
                     CDD cddBeforeEdge = target.transitionBack(e);
-                    e.setGuard(cddBeforeEdge.conjunction(e.getSource().getInvariantCdd()).getGuard(clocks));
+                    e.setGuard(cddBeforeEdge.conjunction(e.getSource().getInvariantCddEager()).getGuard(clocks));
                 }
             }
         }
@@ -225,7 +225,7 @@ 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 = otherE.getTarget().getInvariantCdd();
+                        CDD targetInvariantCDDOfTransThatSavesUs = otherE.getTarget().getInvariantCddEager();
                         CDD goodPart = targetInvariantCDDOfTransThatSavesUs.minus(incPartOfTransThatSavesUs);
 
                         CDD doubleCheck = goodPart.transitionBack(otherE);
@@ -237,7 +237,7 @@ 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(otherE.getSource().getInvariantCdd());
+                        goodPart = goodPart.conjunction(otherE.getSource().getInvariantCddEager());
 
                         if (printComments)
                             Log.debug("Guards done");
@@ -248,7 +248,7 @@ 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(otherE.getSource().getInvariantCdd());
+                        cddOfGuard = cddOfGuard.conjunction(otherE.getSource().getInvariantCddEager());
                         cddThatSavesUs = cddOfGuard.disjunction(cddThatSavesUs);
 
                     }
@@ -257,7 +257,7 @@ public static void handleOutput(Location targetLoc, Edge e, List<Edge>edges, Lis
             if (printComments)
                 Log.debug("Coming to the subtraction");
 
-            CDD newIncPart = e.getSource().getInvariantCdd().minus(cddThatSavesUs);
+            CDD newIncPart = e.getSource().getInvariantCddEager().minus(cddThatSavesUs);
             processSourceLocation(e,  newIncPart,passedPairs, inconsistentQueue);
 
 
@@ -285,7 +285,7 @@ public static void handleInput(Location targetLoc, Edge e, List<Edge> edges, Map
         CDD incCDD = e.getTarget().getInconsistentPart();
 
         // apply target invariant
-        CDD invarCDD = e.getTarget().getInvariantCdd();
+        CDD invarCDD = e.getTarget().getInvariantCddEager();
         incCDD = invarCDD.conjunction(incCDD);
 
         incCDD = incCDD.transitionBack(e);
@@ -335,7 +335,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(e.getSource().getInvariantCdd());
+                incCDD = incCDD.conjunction(e.getSource().getInvariantCddEager());
             }
 
             if (printComments)
@@ -358,7 +358,7 @@ public CDD backExplorationOnTransition(Edge e, CDD incCDD)
         incCDD = incCDD.past();
 
         // apply source invariant
-        CDD invarCDD1 = e.getSource().getInvariantCdd();
+        CDD invarCDD1 = e.getSource().getInvariantCddEager();
         incCDD = invarCDD1.conjunction(incCDD);
 
         if (printComments)
@@ -383,7 +383,7 @@ public static void removeTransitionIfUnsat(Edge e,  CDD incCDD, List<Edge> edges
 
 
         // apply target invariant
-        CDD tartgetInvCDD= e.getTarget().getInvariantCdd();
+        CDD tartgetInvCDD= e.getTarget().getInvariantCddEager();
         testForSatEdgeCDD = tartgetInvCDD.conjunction(testForSatEdgeCDD);
 
         testForSatEdgeCDD = testForSatEdgeCDD.minus(e.getTarget().getInconsistentPart());
@@ -395,7 +395,7 @@ public static void removeTransitionIfUnsat(Edge e,  CDD incCDD, List<Edge> edges
         CDD guardCDD1 = e.getGuardCDD();
         testForSatEdgeCDD = guardCDD1.conjunction(testForSatEdgeCDD);
 
-        CDD sourceInvCDD = e.getSource().getInvariantCdd();
+        CDD sourceInvCDD = e.getSource().getInvariantCddEager();
         testForSatEdgeCDD = sourceInvCDD.conjunction(testForSatEdgeCDD);
 
         // remove inconsistent part
@@ -463,7 +463,7 @@ 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 = otherEdge.getTarget().getInvariantCdd();
+            CDD goodCDD = otherEdge.getTarget().getInvariantCddEager();
             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
@@ -472,7 +472,7 @@ public static CDD predtOfAllOutputs(Edge e, CDD incCDD, List<Edge> edges)
                 goodCDD = goodCDD.transitionBack(otherEdge);
                 //goodCDD = CDD.applyReset(goodCDD, otherEdge.getUpdates());
 
-                CDD sourceInvFed = otherEdge.getSource().getInvariantCdd();
+                CDD sourceInvFed = otherEdge.getSource().getInvariantCddEager();
                 goodCDD = sourceInvFed.conjunction(goodCDD);
                 allGoodCDDs = allGoodCDDs.disjunction(goodCDD);
                 //Log.debug(incFederation.getZones().get(0).buildGuardsFromZone(clocks));

src/logic/Quotient.java

@@ -17,7 +17,7 @@ public Quotient(TransitionSystem t, TransitionSystem s) {
         this.t = t;
         this.s = s;
 
-        //clocks should contain the clocks of ts1, ts2 and a new clock
+        // Clocks should contain the clocks of t, s, and the new clock.
         newClock = new Clock("quo_new", "quo"); //TODO: get ownerName in a better way
         clocks.add(newClock);
 
@@ -53,7 +53,7 @@ public Set<Channel> getOutputs() {
 
     @Override
     public String getName() {
-        return t.getName() + "//" + s.getName();
+        return t.getName() + "\\\\" + s.getName();
     }
 
     @Override
@@ -67,7 +67,7 @@ public List<Move> getNextMoves(Location location, Channel a) {
         if (location.isInconsistent()) {
             if (getInputs().contains(a)) {
                 Log.debug("Rule 10");
-                Move newMove = new Move(location, inc, new ArrayList<>());
+                Move newMove = new Move(location, location, new ArrayList<>());
                 newMove.setUpdates(new ArrayList<>(Collections.singletonList(new ClockUpdate(newClock, 0))));
                 resultMoves.add(newMove);
             }
@@ -77,22 +77,22 @@ public List<Move> getNextMoves(Location location, Channel a) {
         if (location.isUniversal()) {
             if (getActions().contains(a)) {
                 Log.debug("Rule 9");
-                Move newMove = new Move(location, univ, new ArrayList<>());
+                Move newMove = new Move(location, location, new ArrayList<>());
                 resultMoves.add(newMove);
             }
         }
 
         if (location.isProduct()) {
             List<Location> locations = location.getProductOf();
 
-            // symbolic locations corresponding to each TS
+            // Symbolic locations corresponding to each TS.
             Location lt = locations.get(0);
             Location ls = locations.get(1);
 
             List<Move> t_moves = t.getNextMoves(lt, a);
             List<Move> s_moves = s.getNextMoves(ls, a);
 
-            // rule 1 (cartesian product)
+            // Rule 1 (cartesian product)
             if (in(a, intersect(s.getActions(), t.getActions()))) {
                 Log.debug("Rule 1");
                 List<Move> moveProduct = moveProduct(t_moves, s_moves, true,true);
@@ -102,22 +102,22 @@ public List<Move> getNextMoves(Location location, Channel a) {
                 resultMoves.addAll(moveProduct);
             }
 
-            // rule 2
+            // Rule 2
             if (in(a, difference(s.getActions(), t.getActions()))) {
                 Log.debug("Rule 2");
                 List<Move> movesLeft = new ArrayList<>();
                 movesLeft.add(new Move(lt,lt, new ArrayList<>()));
 
-                List<Move> moveProduct = moveProduct(movesLeft, s_moves, true,true);
+                List<Move> moveProduct = moveProduct(movesLeft, s_moves, true, true);
                 for (Move move : moveProduct) {
                     move.conjunctCDD(move.getEnabledPart());
                 }
                 resultMoves.addAll(moveProduct);
             }
 
-            // rule 3
-            // rule 4
-            // rule 5
+            // Rule 3
+            // Rule 4
+            // Rule 5
             if (in(a, s.getOutputs())) {
                 Log.debug("Rule 345 1");
                 CDD guard_s = CDD.cddFalse();
@@ -126,7 +126,7 @@ public List<Move> getNextMoves(Location location, Channel a) {
                 }
                 guard_s = guard_s.negation().removeNegative().reduce();
 
-                CDD inv_neg_inv_loc_s = ls.getInvariantCddNew().negation().removeNegative().reduce();
+                CDD inv_neg_inv_loc_s = ls.getInvariantCddLazy().negation().removeNegative().reduce();
 
                 CDD combined = guard_s.disjunction(inv_neg_inv_loc_s);
 
@@ -135,46 +135,45 @@ public List<Move> getNextMoves(Location location, Channel a) {
                 resultMoves.add(move);
             } else {
                 Log.debug("Rule 345 2");
-                CDD inv_neg_inv_loc_s = ls.getInvariantCddNew().negation().removeNegative().reduce();
+                CDD inv_neg_inv_loc_s = ls.getInvariantCddLazy().negation().removeNegative().reduce();
 
                 Move move = new Move(location, univ);
                 move.conjunctCDD(inv_neg_inv_loc_s);
                 resultMoves.add(move);
             }
 
-            // rule 6
+            // Rule 6
             if (in(a, intersect(t.getOutputs(), s.getOutputs()))) {
                 Log.debug("Rule 6");
-                // take all moves from left in order to gather the guards and negate them
-                CDD CDDFromMovesFromLeft = CDD.cddFalse();
-                for (Move moveLeft : t_moves) {
-                    CDDFromMovesFromLeft = CDDFromMovesFromLeft.disjunction(moveLeft.getEnabledPart());
+                // Take all moves from t in order to gather the guards and negate them.
+                CDD CDDFromMovesFromT = CDD.cddFalse();
+                for (Move t_move : t_moves) {
+                    CDDFromMovesFromT = CDDFromMovesFromT.disjunction(t_move.getEnabledPart());
                 }
-                CDD negated = CDDFromMovesFromLeft.negation().removeNegative().reduce();
+                CDD negated = CDDFromMovesFromT.negation().removeNegative().reduce();
 
-
-                for (Move move : s_moves) {
+                for (Move s_move : s_moves) {
                     Move newMoveRule6 = new Move(location, inc, new ArrayList<>());
-                    newMoveRule6.setGuards(move.getEnabledPart().conjunction(negated));
+                    newMoveRule6.setGuards(s_move.getEnabledPart().conjunction(negated));
                     newMoveRule6.setUpdates(new ArrayList<>(Collections.singletonList(new ClockUpdate(newClock, 0))));
                     resultMoves.add(newMoveRule6);
                 }
             }
 
-            // rule 7
+            // Rule 7
             if (Objects.equals(a.getName(), this.newChan.getName())) {
                 Log.debug("Rule 7");
                 Move newMoveRule7 = new Move(location, inc, new ArrayList<>());
-                // invariant is negation of invariant of left conjuncted with invariant of right
-                CDD negatedInvar = lt.getInvariantCddNew().negation();
-                CDD combined = negatedInvar.conjunction(ls.getInvariantCddNew());
+                // Invariant is negation of invariant of t conjoined with invariant of s
+                CDD negatedInvar = lt.getInvariantCddLazy().negation();
+                CDD combined = negatedInvar.conjunction(ls.getInvariantCddLazy());
 
                 newMoveRule7.setGuards(combined);
                 newMoveRule7.setUpdates(new ArrayList<>(Collections.singletonList(new ClockUpdate(newClock, 0))));
                 resultMoves.add(newMoveRule7);
             }
 
-            // rule 8
+            // Rule 8
             if (in(a, difference(t.getActions(), s.getActions()))) {
                 Log.debug("Rule 8");
                 List<Move> movesRight = new ArrayList<>();

src/logic/Refinement.java

@@ -182,7 +182,7 @@ public boolean checkRef() {
             // check that for every delay in TS 1 there is a corresponding delay in TS
             boolean holds0 = checkDelay(left, right);
             if (!holds0) {
-                Log.debug("Delay violation");
+                Log.info("Delay violation");
                 if (initialisedCdd) {
                     CDD.done();
                 }
@@ -193,7 +193,7 @@ public boolean checkRef() {
             boolean holds1 = checkOutputs(left, right);
             if (!holds1) {
 
-                Log.debug("Output violation");
+                Log.info("Output violation");
                 if (initialisedCdd) {
                     CDD.done();
                 }
@@ -204,7 +204,7 @@ public boolean checkRef() {
             boolean holds2 = checkInputs(left, right);
             if (!holds2) {
                 //assert(false); // assuming everything is input enabled
-                Log.debug("Input violation");
+                Log.info("Input violation");
                 if (initialisedCdd) {
                     CDD.done();
                 }
@@ -317,16 +317,16 @@ private boolean createNewStatePairs(List<Transition> trans1, List<Transition> tr
 
         // If trans2 does not satisfy all solution of trans1, return empty list which should result in refinement failure
         if (!isInput && leftCDD.minus(rightCDD).isNotFalse()) {
-            Log.debug("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.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);
             Log.debug(rightCDD);
             Log.debug(leftCDD.minus(rightCDD));
             return false;
         }
 
         if (isInput && rightCDD.minus(leftCDD).isNotFalse()) {
-            Log.debug("trans 2 does not satisfiy all solutions of trans 1");
+            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);
             Log.debug(rightCDD);
@@ -493,8 +493,8 @@ private boolean listContainsStatePair(StatePair pair, Iterable<StatePair> pairs)
     }
 
     public StatePair getInitialStatePair() {
-        State left = ts1.getInitialState( ts2.getInitialLocation().getInvariantCddNew());
-        State right = ts2.getInitialState(ts1.getInitialLocation().getInvariantCddNew());
+        State left = ts1.getInitialState( ts2.getInitialLocation().getInvariantCddLazy());
+        State right = ts2.getInitialState(ts1.getInitialLocation().getInvariantCddLazy());
         return new StatePair(left, right);
     }