Fix/inconsistent location invariant

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 {

src/models/Automaton.java

@@ -279,19 +279,13 @@ public void makeInputEnabled() {
 
                 // Calculate the enabled CDD.
                 List<Edge> edges = getEdgesFromLocationAndSignal(location, input);
-                if (!edges.isEmpty()) {
-                    for (Edge edge : edges) {
-                        CDD targetInvariant = edge.getTarget().getInvariantCdd();
-                        CDD preGuard = targetInvariant.transitionBack(edge);
-                        enabledPart = enabledPart.disjunction(preGuard);
-                    }
-
-                    if (enabledPart.isTerminal()) {
-                        continue;
-                    }
+                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 the enabled part is true then the disabled part will be false.
                 if (enabledPart.isTrue()) {
                     continue;
                 }

src/models/CDD.java

@@ -11,25 +11,78 @@
 import java.util.stream.Collectors;
 
 public class CDD {
+    /**
+     * The pointer used in the {@link CDDLib} to represent this {@link CDD}.
+     */
     private long pointer;
 
+    /**
+     * This {@link CDD} converted to a {@link Guard}.
+     */
     private Guard guard;
+
+    /**
+     * If this boolean is <code>true</code> then this {@link CDD} has changed, and we should recompute the {@link Guard}.
+     * Otherwise, if this boolean is false, then the already computed {@link CDD#guard} will be returned from {@link CDD#getGuard()}.
+     * Since re-computation of the {@link CDD#guard} is only performed when this {@link CDD has changed, then the guard returned is
+     * a reference mutable from other places, and thereby it should be viewed as readonly or copied.
+     */
     private boolean isGuardDirty;
 
+    /**
+     * If this boolean is <code>true</code> then this {@link CDD} has changed, and {@link CDD#delay()} will call {@link CDDLib#delay(long)} with this {@link CDD#pointer}.
+     * Otherwise, {@link CDD#delayInvar(CDD)} will just return <code>this</code>.
+     */
     private boolean isDelayedDirty;
+
+    /**
+     * If this boolean is <code>true</code> then this {@link CDD} has changed, and {@link CDD#delayInvar(CDD)}} will call {@link CDDLib#delayInvar(long, long)} with this {@link CDD#pointer} and the argument.
+     * Otherwise, {@link CDD#delayInvar(CDD)} will just return <code>this</code>.
+     */
     private boolean isDelayedInvariantDirty;
+
+    /**
+     * If this boolean is <code>true</code> then this {@link CDD} has changed, and {@link CDD#past()}} will call {@link CDDLib#past(long)} with this {@link CDD#pointer}.
+     * Otherwise, {@link CDD#past()} will just return <code>this</code>.
+     */
     private boolean isPastDirty;
 
+    /**
+     * The bottom part of a {@link CDD} are BDD nodes. If this boolean is true then we are within that part of the {@link CDD}.
+     */
     private boolean isBdd;
+
+    /**
+     * The bottom most nodes labeled either <code>true</code> or <code>false</code> are called terminal nodes.
+     * These nodes have only ingoing edges and no outgoing.
+     * If this boolean is true, then the {@link CDD#pointer} points at one of these terminal nodes.
+     * If this is the case, then this {@link CDD} is a BDD ({@link CDD#isBdd} is <code>true</code>).
+     */
     private boolean isTerminal;
+
+    /**
+     * If {@link CDD#isGuardDirty} is true then this {@link CDD} has changed, and {@link CDD#isUrgent()} will be recompute.
+     * Otherwise, {@link CDD#isUrgent()} will just return {@link CDD#isUrgent}.
+     */
     private boolean isUrgent;
+
+    /**
+     *
+     */
     private boolean isUnrestrained;
+
     private boolean isTrue;
     private boolean isFalse;
+
     private boolean canDelayIndefinitely;
     private boolean hasRemovedNegatives;
 
     private CddExtractionResult extraction;
+
+    /**
+     * If this boolean is <code>true</code> then this {@link CDD} has changed, and {@link CDD#extract()} will call {@link CDDLib#extractBddAndDbm(long)} with this {@link CDD#pointer}.
+     * Otherwise, {@link CDD#extract()} will just return the stored {@link CDD#extraction}.
+     */
     private boolean isExtractionDirty;
 
     private static boolean cddIsRunning;
@@ -352,9 +405,7 @@ public boolean canDelayIndefinitely() {
             }
         }
 
-        canDelayIndefinitely = result;
-
-        return result;
+        return canDelayIndefinitely = result;
     }
 
     public boolean isUrgent() {
@@ -381,17 +432,15 @@ public boolean isUrgent() {
             }
         }
 
-        isUrgent = result;
-
-        return result;
+        return isUrgent = result;
     }
 
     /**
      * Returns a new instance of this CDD but with the same pointer.
      * In contrast to {@link #copy()} this does not create a completely
      * new CDD instance by invoking the {@link CDDLib#copy(long)}. The usefulness
      * of {@link #hardCopy()} is its lightweight nature and as the pointer
-     * is a pass-by-value then immediate not oeprator invocations won't alter the pointer
+     * is a pass-by-value the immediate not operator invocations won't alter the pointer
      * value of the original (this.pointer) retrieved through {@link #getPointer()}.
      *
      * @return Returns a new CDD which is not created through {@link CDDLib#copy(long)} but with a pointer copy.
@@ -1004,4 +1053,4 @@ private static void checkIfNotRunning() {
             throw new CddNotRunningException("CDD.init() has not been called");
         }
     }
-}
+}

src/models/UniqueNamedContainer.java

@@ -50,7 +50,7 @@ public UniqueNamedContainer() {
      *
      * @param item item to be added to the end of this container.
      */
-    public void add(T item) {
+    public boolean add(T item) {
         T newItem = (T) item.getCopy();
 
         if (!item.isGlobal()) {
@@ -59,9 +59,11 @@ public void add(T item) {
                     .collect(Collectors.toList());
             if (sameName.size() != 0) {
                 List<T> sameOwner = sameName.stream().filter(c -> c.getOwnerName().equals(item.getOwnerName())).collect(Collectors.toList());
-                if (sameOwner.size() != 0) { // Same name, same owner
-                    for (int i = 0; i < sameOwner.size(); i++) {
-                        sameOwner.get(i).setUniqueName(i + 1);
+                if (sameOwner.size() > 0) { // Same name, same owner
+                    // The first element would always have a unique name without an index.
+                    // Because of this, we have to set its unique name with index 1.
+                    if (sameOwner.size() == 1) {
+                        sameOwner.get(0).setUniqueName(1);
                     }
                     newItem.setUniqueName(sameOwner.size() + 1);
                 } else { //  Same name, different owner
@@ -73,11 +75,13 @@ public void add(T item) {
             }
         }
 
-        // If the unique name is not present in the set of items then add it
+        // If the unique name is not present in the set of items then add it.
         Optional<T> existing = findFirstByUniqueName(newItem.getUniqueName());
         if (existing.isEmpty()) {
             items.add(newItem);
+            return true;
         }
+        return false;
     }
 
     private boolean sameName(UniquelyNamed item1, UniquelyNamed item2) {
@@ -105,7 +109,9 @@ public Optional<T> findAnyWithOriginalName(String originalName) {
     }
 
     /**
-     * @return the internal list representation of this container.
+     * A getter for the backing field {@link UniqueNamedContainer#items}.
+     *
+     * @return The internal list representation of this container.
      */
     public List<T> getItems() {
         return items;

test/features/UniversityTest.java

@@ -192,11 +192,7 @@ public void quotientEqual() {
         SimpleTransitionSystem lhs = new SimpleTransitionSystem(new Quotient(getSpec(), getResearcher()).getAutomaton());
         Quotient rhs = new Quotient(getSpec(), getResearcher());
         Refinement refinement = new Refinement(lhs, rhs);
-
-        XMLFileWriter.toXML("testOutput/quotient.xml", lhs);
-        boolean refines = refinement.check();
-
-        assertTrue(refines);
+        assertTrue(refinement.check());
     }
 
     @Test
@@ -219,13 +215,6 @@ public void testFromTestFramework() {
         TransitionSystem rightAut = new Conjunction(new SimpleTransitionSystem(right1.getAutomaton()), new SimpleTransitionSystem(right2.getAutomaton()));
         Log.trace(rightAut.getOutputs());
 
-        XMLFileWriter.toXML("testOutput/right.xml",right.getAutomaton());
-        XMLFileWriter.toXML("testOutput/right1.xml",right1.getAutomaton());
-        XMLFileWriter.toXML("testOutput/right2.xml",right2.getAutomaton());
-        XMLFileWriter.toXML("testOutput/rightAut.xml",rightAut.getAutomaton());
-
-        XMLFileWriter.toXML("testOutput/left.xml",left.getAutomaton());
-
         Refinement refinement1 = new Refinement(left,rightAut);
         boolean refines1 = refinement1.check(true);
         //Log.trace(refinement1.getTree().toDot());
@@ -290,6 +279,7 @@ public void doubleQuotientTest() {
 
         assertFalse(refines);
     }
+
     @Test
     public void doubleQuotientTest1() {
         // refinement: res <= spec \ adm2 \ machine
@@ -357,12 +347,7 @@ public void newQuotientTest4A() {
         Composition lhs = new Composition(getMachine(), getResearcher());
         Quotient rhs = new Quotient(getSpec(), getAdm());
         Refinement refinement = new Refinement(lhs, rhs);
-
-        XMLFileWriter.toXML("./testOutput/specDIVadm.xml", lhs.getAutomaton());
-        XMLFileWriter.toXML("./testOutput/comp.xml", rhs.getAutomaton());
-        boolean refines = refinement.check();
-
-        assertTrue(refines);
+        assertTrue(refinement.check());
     }
 
     @Test
@@ -418,8 +403,6 @@ public void simpliversityTest2() {
         TransitionSystem lhs = getSimpleResearcher();
 
         TransitionSystem rhs = new SimpleTransitionSystem(new Quotient(getSimpleSpec(), getSimpleAdm()).getAutomaton());
-        // TransitionSystem rhs = new Quotient(getSimpleSpec(), getSimpleAdm());
-        XMLFileWriter.toXML("testOutput/simpleversityQuotient.xml",rhs.getAutomaton());
         Refinement refinement = new Refinement(lhs, rhs);
         assertTrue(new Refinement(new Composition(getSimpleAdm(),getSimpleResearcher()),getSimpleSpec()).check());
         boolean refines = refinement.check();

test/logic/QuotientTest.java

@@ -1,7 +1,5 @@
 package logic;
 
-import log.Log;
-import log.Urgency;
 import models.*;
 import org.junit.Test;
 
@@ -36,7 +34,7 @@ public void quotientConstructorShouldAddANewClockWithNameQuo_new() {
         assertEquals(quotient.getClocks().size(), 1);
         assertTrue(contains_clock_quo_new);
     }
-    
+
     @Test
     public void quotientConstructorShouldAddANewChannel() {
         // Arrange
@@ -61,7 +59,7 @@ public void quotientConstructorShouldAddANewChannel() {
         assertEquals(quotient.getInputs().size(), 1);
         assertTrue(contains_channel_i_new);
     }
-    
+
     @Test
     public void quotientShouldHaveInputsAsUnionOfLhsAndRhs() {
         // Arrange