Fix/quotient

samples/xml/selfloopNonZeno.xml

@@ -0,0 +1,25 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<nta>
+  <declaration>chan o;</declaration>
+  <template>
+    <name>SelfloopNonZenoCopy</name>
+    <declaration>clock xCopy; clock yCopy;</declaration>
+    <location id="id6" x="-85" y="51" color="#A66C0F">
+      <name>id6</name>
+      <label kind="invariant">(xCopy&lt;3 &amp;&amp; xCopy-yCopy&lt;3)</label>
+    </location>
+    <location id="id7" x="119" y="51" color="#A66C0F">
+      <name>id7</name>
+      <label kind="invariant">false</label>
+    </location>
+    <init ref="id6" />
+    <transition controllable="false">
+      <source ref="id6" />
+      <target ref="id6" />
+      <label kind="synchronisation">o!</label>
+      <label kind="guard">(xCopy&lt;3 &amp;&amp; xCopy-yCopy&lt;3)</label>
+      <label kind="assignment">xCopy = 0</label>
+    </transition>
+  </template>
+  <system>system SelfloopNonZenoCopy;</system>
+</nta>

src/connection/GrpcServer.java

@@ -20,7 +20,7 @@ public GrpcServer(String address) {
     }
 
     private SocketAddress getSocketAddressFromString(String address) {
-        int port = 80;
+        int port = 9000;
         String host = null;
         if (address.indexOf(':') != -1) {
             String[] arr = address.split(":");

src/connection/Main.java

@@ -1,5 +1,7 @@
 package connection;
 
+import log.Log;
+import log.Urgency;
 import logic.*;
 import logic.query.Query;
 import models.Automaton;
@@ -45,6 +47,8 @@ public class Main {
 
 
     public static void main(String[] args) {
+        Log.setUrgency(Urgency.Info);
+
         options.addOption(proto);
         options.addOption(outputFolder);
         options.addOption(inputFolder);
@@ -93,12 +97,12 @@ public static void main(String[] args) {
                     queries = Controller.handleRequest("-json " + inputFolderPath, queryString, false);
                 }
                 for (Query query: queries) {
-                    System.out.println(query.getResult());
-                    System.out.println(query.getResultStrings());
+                    Log.info(query.getResult());
+                    Log.info(query.getResultStrings());
                 }
 
             } catch (Exception e) {
-                System.out.println(e.getMessage());
+                Log.error(e.getMessage());
                 throw new RuntimeException(e);
             }
 
@@ -108,7 +112,7 @@ public static void main(String[] args) {
             }
 
         } catch (ParseException e) {
-            System.out.println(e.getMessage());
+            Log.fatal(e.getMessage());
             printHelp(formatter,options);
         }
 

src/logic/AggregatedTransitionSystem.java

@@ -44,7 +44,7 @@ public List<SimpleTransitionSystem> getSystems() {
     }
 
     @Override
-    public SymbolicLocation getInitialLocation() {
+    public Location getInitialLocation() {
         return getInitialLocation(systems);
     }
 
@@ -84,20 +84,19 @@ currentState, getNextMoves(currentState.getLocation(), channel), allClocks
     }
 
     @Override
-    public List<Move> getNextMoves(SymbolicLocation location, Channel channel) {
+    public List<Move> getNextMoves(Location location, Channel channel) {
         // Check if action belongs to this transition system at all before proceeding
         if (!getOutputs().contains(channel) && !getInputs().contains(channel)) {
             return new ArrayList<>();
         }
 
         // Check that the location is ComplexLocation
-        if (!(location instanceof ComplexLocation)) {
+        if (!location.isProduct()) {
             throw new IllegalArgumentException(
                     "The location type must be ComplexLocation as aggregated transition systems requires multiple locations"
             );
         }
-        ComplexLocation complexLocation = (ComplexLocation) location;
-        List<SymbolicLocation> locations = complexLocation.getLocations();
+        List<Location> locations = location.getProductOf();
 
         /* Check that the complex locations size is the same as the systems
          * This is because the index of the system,
@@ -112,12 +111,18 @@ public List<Move> getNextMoves(SymbolicLocation location, Channel channel) {
         return computeResultMoves(locations, channel);
     }
 
-    protected abstract List<Move> computeResultMoves(List<SymbolicLocation> locations, Channel channel);
+    protected List<Move> computeResultMoves(List<Location> locations, Channel channel) {
+        return new ArrayList<>();
+    }
 
     protected List<TransitionSystem> getRootSystems() {
         return Arrays.asList(systems);
     }
 
+    protected boolean in(Channel element, Set<Channel> set) {
+        return set.contains(element);
+    }
+
     protected Set<Channel> intersect(Set<Channel> set1, Set<Channel> set2) {
         Set<Channel> intersection = new HashSet<>(set1);
         intersection.retainAll(set2);
@@ -145,11 +150,8 @@ private Automaton aggregate(Automaton[] automata) {
         Set<Location> locations = new HashSet<>();
         Map<String, Location> locationMap = new HashMap<>();
 
-        List<Location> initials = new ArrayList<>();
-        for (Automaton aut : automata) {
-            initials.add(aut.getInitial());
-        }
-        Location initial = new Location(initials);
+        State initialState = getInitialState();
+        Location initial = initialState.getLocation();
         locations.add(initial);
         locationMap.put(initial.getName(), initial);
 
@@ -183,7 +185,7 @@ private Automaton aggregate(Automaton[] automata) {
                     String targetName = targetState.getLocation().getName();
                     locationMap.computeIfAbsent(
                             targetName, key -> {
-                                Location newLocation = new Location(targetState, clocks.getItems());
+                                Location newLocation = Location.createFromState(targetState, clocks.getItems());
                                 locations.add(newLocation);
                                 return newLocation;
                             }

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/Composition.java

@@ -80,7 +80,7 @@ public String getName() {
     }
 
     @Override
-    protected List<Move> computeResultMoves(List<SymbolicLocation> locations, Channel channel) {
+    protected List<Move> computeResultMoves(List<Location> locations, Channel channel) {
         if (locations.size() != getRootSystems().size()) {
             throw new IllegalArgumentException("There must be exactly the same amount of locations as systems");
         }
@@ -93,7 +93,7 @@ protected List<Move> computeResultMoves(List<SymbolicLocation> locations, Channe
              *   the one of the composition meaning that the i'th
              *   location is also for the i'th system. */
             TransitionSystem system = getRootSystems().get(i);
-            SymbolicLocation location = locations.get(i);
+            Location location = locations.get(i);
 
             /* By iterating through all systems and then getting the next moves
              *   for each system we get a set of all next moves for all systems. */

src/logic/Conjunction.java

@@ -39,7 +39,7 @@ public String getName() {
     }
 
     @Override
-    protected List<Move> computeResultMoves(List<SymbolicLocation> locations, Channel channel) {
+    protected List<Move> computeResultMoves(List<Location> locations, Channel channel) {
         if (locations.size() != getRootSystems().size()) {
             throw new IllegalArgumentException("There must be exactly the same amount of locations as systems");
         }
@@ -52,7 +52,7 @@ protected List<Move> computeResultMoves(List<SymbolicLocation> locations, Channe
              *   the one of the composition meaning that the i'th
              *   location is also for the i'th system. */
             TransitionSystem system = getRootSystems().get(i);
-            SymbolicLocation location = locations.get(i);
+            Location location = locations.get(i);
 
             List<Move> moves = system.getNextMoves(location, channel);
 

src/logic/JsonAutomatonEncoder.java

@@ -81,7 +81,7 @@ private static JSONObject automatonToJson(Automaton aut){
             locationJson.put("y", l.getY());
 
 
-            String guardString =l.getInvariant().toString();
+            String guardString =l.getInvariantGuard().toString();
             /*int i= 0; int j=0;
             for (List<Guard> disjunction: l.getInvariant())
             {