Fix/inconsistent location invariant

src/logic/AggregatedTransitionSystem.java

@@ -185,7 +185,7 @@ private Automaton aggregate(Automaton[] automata) {
                     String targetName = targetState.getLocation().getName();
                     locationMap.computeIfAbsent(
                             targetName, key -> {
-                                Location newLocation = Location.createFromState(targetState, clocks.getItems());
+                                Location newLocation = Location.createFromState(targetState);
                                 locations.add(newLocation);
                                 return newLocation;
                             }

src/logic/Quotient.java

@@ -18,7 +18,7 @@ public Quotient(TransitionSystem t, TransitionSystem s) {
         this.s = s;
 
         // Clocks should contain the clocks of t, s, and the new clock.
-        Optional<Clock> existingClock = clocks.findFirstWithOriginalName("quo_new");
+        Optional<Clock> existingClock = clocks.findAnyWithOriginalName("quo_new");
         if (existingClock.isPresent()) {
             newClock = existingClock.get();
         } else {
@@ -58,7 +58,7 @@ public String getName() {
     @Override
     public List<Move> getNextMoves(Location location, Channel a) {
         Location univ = Location.createUniversalLocation("universal", 0, 0);
-        Location inc = Location.createInconsistentLocation("inconsistent", 0, 0);
+        Location inc = Location.createInconsistentLocation("inconsistent", 0, 0, newClock);
 
         List<Move> resultMoves = new ArrayList<>();
 
@@ -94,7 +94,7 @@ public List<Move> getNextMoves(Location location, Channel a) {
             // 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);
+                List<Move> moveProduct = moveProduct(t_moves, s_moves, true, true);
                 for (Move move : moveProduct) {
                     move.conjunctCDD(move.getEnabledPart());
                 }
@@ -105,7 +105,7 @@ public List<Move> getNextMoves(Location location, Channel a) {
             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<>()));
+                movesLeft.add(new Move(lt, lt, new ArrayList<>()));
 
                 List<Move> moveProduct = moveProduct(movesLeft, s_moves, true, true);
                 for (Move move : moveProduct) {
@@ -176,8 +176,8 @@ public List<Move> getNextMoves(Location location, Channel a) {
             if (in(a, difference(t.getActions(), s.getActions()))) {
                 Log.debug("Rule 8");
                 List<Move> movesRight = new ArrayList<>();
-                movesRight.add(new Move(ls,ls,new ArrayList<>()));
-                List<Move> moveProduct = moveProduct(t_moves, movesRight, true,true);
+                movesRight.add(new Move(ls, ls, new ArrayList<>()));
+                List<Move> moveProduct = moveProduct(t_moves, movesRight, true, true);
                 for (Move move : moveProduct) {
                     move.conjunctCDD(move.getEnabledPart());
                 }

src/logic/Refinement.java

@@ -432,8 +432,9 @@ private boolean checkActions(State state1, State state2, boolean isInput) {
                     Log.debug("create pairs failed");
                     if (RET_REF)
                     {
-                        Location ll = Location.createInconsistentLocation("inconsistent", 0, 0);
-                        Location rl = Location.createInconsistentLocation("inconsistent", 0, 0);
+                        Clock inconsistentClock = new Clock("inconsistent clock", "refinement");
+                        Location ll = Location.createInconsistentLocation("inconsistent", 0, 0, inconsistentClock);
+                        Location rl = Location.createInconsistentLocation("inconsistent", 0, 0, inconsistentClock);
                         StatePair refViolationStates = new StatePair(new State(ll,CDD.cddTrue()), new State(rl, CDD.cddTrue()));
                         currNode.constructSuccessor(refViolationStates, leaderEdges, followerEdges);
                     }

src/models/Automaton.java

@@ -268,30 +268,36 @@ public int hashCode() {
     public void makeInputEnabled() {
         boolean initialisedCdd = CDD.tryInit(clocks, BVs);
 
-        for (Location loc : getLocations()) {
-            CDD sourceInvariantCDD = loc.getInvariantCdd();
-            // loop through all inputs
+        for (Location location : getLocations()) {
+            CDD invariant = location.getInvariantCdd();
+
             for (Channel input : getInputAct()) {
+                // The part which is already handled by existing edges.
+                CDD enabledPart = CDD.cddFalse();
+                // The part which requires an edge to be input enabled.
+                CDD disabledPart = invariant;
+
+                // Calculate the enabled CDD.
+                List<Edge> edges = getEdgesFromLocationAndSignal(location, input);
+                for (Edge edge : edges) {
+                    CDD targetInvariant = edge.getTarget().getInvariantCdd();
+                    CDD preGuard = targetInvariant.transitionBack(edge);
+                    enabledPart = enabledPart.disjunction(preGuard);
+                }
+
+                // If the enabled part is true then the disabled part will be false.
+                if (enabledPart.isTrue()) {
+                    continue;
+                }
 
-                // build CDD of zones from edges
-                List<Edge> inputEdges = getEdgesFromLocationAndSignal(loc, input);
-                CDD resCDD;
-                CDD cddOfAllEdgesWithCurrentInput = CDD.cddFalse();
-                if (!inputEdges.isEmpty()) {
-                    for (Edge edge : inputEdges) {
-                        CDD target = edge.getTarget().getInvariantCdd();
-                        CDD preGuard1 = target.transitionBack(edge);
-                        cddOfAllEdgesWithCurrentInput = cddOfAllEdgesWithCurrentInput.disjunction(preGuard1);
-                    }
-                    cddOfAllEdgesWithCurrentInput = cddOfAllEdgesWithCurrentInput.removeNegative().reduce();
-                    // subtract the federation of zones from the original fed
-                    resCDD = sourceInvariantCDD.minus(cddOfAllEdgesWithCurrentInput);
-                } else {
-                    resCDD = sourceInvariantCDD;
+                // If there is any solution to the enabled CDD then subtract it from the invariant.
+                if (enabledPart.isNotFalse()) {
+                    disabledPart = disabledPart.minus(enabledPart);
                 }
 
-                if (resCDD.isNotFalse()) {
-                    Edge newEdge = new Edge(loc, loc, input, true, resCDD.getGuard(getClocks()), new ArrayList<>());
+                // If there is any solution to the disabled CDD then create an edge.
+                if (disabledPart.isNotFalse()) {
+                    Edge newEdge = new Edge(location, location, input, true, disabledPart.getGuard(), new ArrayList<>());
                     getEdges().add(newEdge);
                 }
             }