102 clock values/constraints in trace

.github/workflows/build.yml

@@ -16,8 +16,9 @@ jobs:
           submodules: recursive
 
       - name: Set up JDK 11
-        uses: actions/setup-java@v1
+        uses: actions/setup-java@v2
         with:
+          distribution: 'adopt'
           java-version: 11
           java-package: jdk
       - name: Cache Gradle packages

.gitignore

@@ -13,6 +13,10 @@ lib/*.dll
 .idea/
 /out/
 
+#VsCode
+/bin/
+.vscode/
+
 ### Gradle ###
 .gradle
 /build/

.gitmodules

@@ -1,3 +1,4 @@
 [submodule "src/main/proto"]
 	path = src/main/proto
-	url = https://github.com/Ecdar/Ecdar-ProtoBuf.git
+	url = https://github.com/Ecdar-SW5/Ecdar-ProtoBuf.git
+

build.gradle

@@ -10,6 +10,20 @@ javafx {
     modules = ['javafx.controls', 'javafx.fxml', 'javafx.swing']
 }
 
+run {
+    mainClassName = 'com.jfxbase/com.jfxbase.sample.Main'
+    applicationDefaultJvmArgs += [
+            "--add-opens", "javafx.graphics/javafx.css=ALL-UNNAMED",
+            "--add-opens", "javafx.base/com.sun.javafx.runtime=ALL-UNNAMED",
+            "--add-opens", "javafx.controls/com.sun.javafx.scene.control.behavior=ALL-UNNAMED",
+            "--add-opens", "javafx.controls/com.sun.javafx.scene.control=ALL-UNNAMED",
+            "--add-opens", "javafx.base/com.sun.javafx.binding=ALL-UNNAMED",
+            "--add-opens", "javafx.base/com.sun.javafx.event=ALL-UNNAMED",
+            "--add-opens", "javafx.graphics/com.sun.javafx.stage=ALL-UNNAMED",
+            "--add-opens", "javafx.graphics/com.sun.javafx.scene=ALL-UNNAMED",
+    ]
+}
+
 group 'ecdar'
 if (project.hasProperty('ecdarVersion')) {
     version = project.ecdarVersion
@@ -46,7 +60,6 @@ def protocVersion = protobufVersion
 
 dependencies {
     implementation fileTree(dir: 'lib', include: ['*.jar'])
-
     implementation 'com.jfoenix:jfoenix:9.0.10'
     implementation group: 'de.codecentric.centerdevice', name: 'javafxsvg', version: '1.3.0'
     implementation 'org.kordamp.ikonli:ikonli-core:12.3.1'
@@ -79,6 +92,7 @@ dependencies {
     testRuntimeOnly group: 'org.junit.jupiter', name: 'junit-jupiter-engine', version: '5.8.2'
     testImplementation group: 'org.testfx', name: 'testfx-junit', version: '4.0.15-alpha'
     testImplementation group: 'org.testfx', name: 'openjfx-monocle', version: 'jdk-12.0.1+2'
+    testImplementation group: 'org.junit.jupiter', name: 'junit-jupiter-params', version: '5.8.2'
 }
 
 

src/main/java/ecdar/Ecdar.java

@@ -4,6 +4,8 @@
 import ecdar.abstractions.Project;
 import ecdar.backend.BackendDriver;
 import ecdar.backend.BackendHelper;
+import ecdar.backend.QueryHandler;
+import ecdar.backend.SimulationHandler;
 import ecdar.code_analysis.CodeAnalysis;
 import ecdar.controllers.EcdarController;
 import ecdar.presentations.BackgroundThreadPresentation;
@@ -52,6 +54,8 @@ public class Ecdar extends Application {
     public static BooleanProperty shouldRunBackgroundQueries = new SimpleBooleanProperty(true);
     private static final BooleanProperty isSplit = new SimpleBooleanProperty(true); //Set to true to ensure correct behaviour at first toggle.
     private static BackendDriver backendDriver = new BackendDriver();
+    private static QueryHandler queryHandler = new QueryHandler(backendDriver);
+    private static SimulationHandler simulationHandler;
     private Stage debugStage;
 
     /**
@@ -120,6 +124,20 @@ public static Project getProject() {
         return project;
     }
 
+    /**
+     * Returns the backend driver used to execute queries and handle simulation
+     * @return BackendDriver
+     */
+    public static BackendDriver getBackendDriver() {
+        return backendDriver;
+    }
+
+    public static QueryHandler getQueryExecutor() {
+        return queryHandler;
+    }
+
+    public static SimulationHandler getSimulationHandler() { return simulationHandler; }
+
     public static EcdarPresentation getPresentation() {
         return presentation;
     }
@@ -134,8 +152,8 @@ public static void showHelp() {
         presentation.showHelp();
     }
 
-    public static BooleanProperty toggleFilePane() {
-        return presentation.toggleFilePane();
+    public static BooleanProperty toggleLeftPane() {
+        return presentation.toggleLeftPane();
     }
 
     /**
@@ -160,7 +178,7 @@ public static BooleanProperty toggleRunBackgroundQueries() {
     }
 
     public static BooleanProperty toggleQueryPane() {
-        return presentation.toggleQueryPane();
+        return presentation.toggleRightPane();
     }
 
     /**
@@ -181,14 +199,6 @@ public static BooleanProperty toggleCanvasSplit() {
         return isSplit;
     }
 
-    /**
-     * Returns the backend driver used to execute queries and handle simulation
-     * @return BackendDriver
-     */
-    public static BackendDriver getBackendDriver() {
-        return backendDriver;
-    }
-
     public static double getDpiScale() {
         if (!autoScalingEnabled.getValue())
             return 1;
@@ -207,6 +217,7 @@ public void start(final Stage stage) {
 
         // Load or create new project
         project = new Project();
+        simulationHandler = new SimulationHandler(getBackendDriver());
 
         // Set the title for the application
         stage.setTitle("Ecdar " + VERSION);
@@ -306,6 +317,8 @@ public void start(final Stage stage) {
 
             try {
                 backendDriver.closeAllBackendConnections();
+                queryHandler.closeAllBackendConnections();
+                simulationHandler.closeAllBackendConnections();
             } catch (IOException e) {
                 e.printStackTrace();
             }
@@ -319,6 +332,8 @@ public void start(final Stage stage) {
             // to prevent dangling connections and queries
             try {
                 backendDriver.closeAllBackendConnections();
+                queryHandler.closeAllBackendConnections();
+                simulationHandler.closeAllBackendConnections();
             } catch (IOException e) {
                 throw new RuntimeException(e);
             }

src/main/java/ecdar/abstractions/Component.java

@@ -38,7 +38,9 @@ public class Component extends HighLevelModelObject implements Boxed {
 
     // Verification properties
     private final ObservableList<Location> locations = FXCollections.observableArrayList();
+    private final ObservableList<Location> failingLocations = FXCollections.observableArrayList();
     private final ObservableList<DisplayableEdge> edges = FXCollections.observableArrayList();
+    private final ObservableList<DisplayableEdge> failingEdges = FXCollections.observableArrayList();
     private final ObservableList<String> inputStrings = FXCollections.observableArrayList();
     private final ObservableList<String> outputStrings = FXCollections.observableArrayList();
     private final StringProperty description = new SimpleStringProperty("");
@@ -486,6 +488,67 @@ public boolean removeLocation(final Location location) {
         return locations.remove(location);
     }
 
+    /**
+     * Add a failing Edge to the list of failing edges
+     * and set the edge's failing property to true.
+     * @param edge the Edge that is failing.
+     * @return whether adding the Edge to the list was a success
+     */
+    public boolean addFailingEdge(final Edge edge) {
+        edge.setFailing(true);
+        return failingEdges.add(edge);
+    }
+
+    /**
+     * Sets all previous failing edges to not failing
+     * and removes all previous failing edges from list.
+     */
+    public void removeFailingEdges() {
+        for (DisplayableEdge edge : failingEdges) {
+            edge.setFailing(false);
+        }
+        failingEdges.removeAll();
+    }
+
+    /**
+     * Observable list of all failing locations.
+     * @return Observable list of all failing locations.
+     */
+    public ObservableList<Location> getFailingLocations() {
+        return failingLocations;
+    }
+
+    /**
+     * Adds a failing location to the list of failing locations.
+     * @param locationId the id of the location that is failing.
+     * @return whether adding the location to the list was a success
+     */
+    public boolean addFailingLocation(final String locationId) {
+        Location failingLocation = findLocation(locationId);
+        failingLocation.setFailing(true);
+        return failingLocations.add(failingLocation);
+    }
+
+    /**
+     * Sets all previous failing locations to not failing
+     * and removes all previous failing locations from list.
+     */
+    public void removeFailingLocations() {
+        for (Location location : failingLocations) {
+            location.setFailing(false);
+        }
+        failingLocations.removeAll();
+    }
+
+    /**
+     * Observable list of all failing edges.
+     * @return Observable list of all failing edges.
+     */
+    public ObservableList<DisplayableEdge> getFailingEdges() {
+        return failingEdges;
+    }
+
+
     /**
      * Returns all DisplayableEdges of the component (returning a list potentially containing GroupEdges and Edges)
      * @return All visual edges of the component

src/main/java/ecdar/abstractions/ComponentInstance.java

@@ -2,7 +2,6 @@
 
 import ecdar.Ecdar;
 import ecdar.presentations.Grid;
-import ecdar.utility.colors.Color;
 import com.google.gson.JsonObject;
 import javafx.beans.property.*;
 import javafx.beans.value.ObservableValue;

src/main/java/ecdar/abstractions/Declarations.java

@@ -1,15 +1,12 @@
 package ecdar.abstractions;
 
 import ecdar.utility.colors.Color;
-import ecdar.utility.colors.EnabledColor;
-import com.google.gson.JsonArray;
 import com.google.gson.JsonObject;
 import javafx.beans.property.SimpleStringProperty;
 import javafx.beans.property.StringProperty;
 import org.apache.commons.lang3.tuple.Triple;
 
 import java.util.ArrayList;
-import java.util.Arrays;
 import java.util.List;
 import java.util.regex.Matcher;
 import java.util.regex.Pattern;

src/main/java/ecdar/abstractions/DisplayableEdge.java

@@ -1,16 +1,17 @@
 package ecdar.abstractions;
 
-import ecdar.Ecdar;
 import ecdar.code_analysis.Nearable;
 import ecdar.presentations.Grid;
 import ecdar.utility.colors.Color;
 import ecdar.utility.helpers.Circular;
 import ecdar.utility.helpers.MouseCircular;
+import ecdar.utility.helpers.StringHelper;
 import javafx.beans.property.*;
 import javafx.collections.FXCollections;
 import javafx.collections.ObservableList;
 
 import java.util.List;
+import java.util.UUID;
 
 public abstract class DisplayableEdge implements Nearable {
     private final StringProperty id = new SimpleStringProperty("");
@@ -39,6 +40,8 @@ public abstract class DisplayableEdge implements Nearable {
 
     private final BooleanProperty isHighlighted = new SimpleBooleanProperty(false);
 
+    protected final BooleanProperty failing = new SimpleBooleanProperty(false);
+
     public Location getSourceLocation() {
         return sourceLocation.get();
     }
@@ -82,7 +85,7 @@ public StringProperty selectProperty() {
     }
 
     public String getGuard() {
-        return guard.get();
+        return StringHelper.ConvertUnicodeToSymbols(guard.get());
     }
 
     public void setGuard(final String guard) {
@@ -279,12 +282,7 @@ public String getId() {
      * Generate and sets a unique id for this location
      */
     protected void setId() {
-        for(int counter = 0; ; counter++) {
-            if(!Ecdar.getProject().getEdgeIds().contains(String.valueOf(counter))){
-                id.set(Edge.EDGE + counter);
-                return;
-            }
-        }
+        id.set(UUID.randomUUID().toString());
     }
 
     /**
@@ -302,4 +300,22 @@ public StringProperty idProperty() {
     public abstract List<String> getProperty(final PropertyType propertyType);
 
     public abstract void setProperty(final PropertyType propertyType, final List<String> newProperty);
+
+    /**
+     * Sets the 'failing' property
+     * @param bool true if the edge is failing.
+     */
+    public abstract void setFailing(final boolean bool);
+
+    /**
+     * Getter for the 'failing' boolean
+     * @return Whether edge is failing in last query response.
+     */
+    public abstract boolean getFailing();
+
+    /**
+     * The observable boolean property for 'failing' of this.
+     * @return The observable boolean property for 'failing' of this.
+     */
+    public abstract BooleanProperty failingProperty();
 }

src/main/java/ecdar/abstractions/EcdarSystemEdge.java

@@ -2,7 +2,6 @@
 
 import ecdar.Ecdar;
 import ecdar.controllers.SystemRootController;
-import com.google.gson.JsonElement;
 import com.google.gson.JsonObject;
 import javafx.beans.property.ObjectProperty;
 import javafx.beans.property.SimpleObjectProperty;