Backend to engine

README.md

@@ -17,7 +17,7 @@ This project is a hard fork of https://github.com/ulriknyman/H-Uppaal.
 This section covers what dependencies are currently needed by the GUI.
 
 ### JVM
-As with all Java applications, a working JVM is required to run the project. 
+As with all Java applications, a working JVM is required to run the project.
 
 You will need Java version 11 containing JavaFX. We suggest downloading Azul's Java 11 from https://www.azul.com/downloads/?version=java-11-lts&package=jdk-fx, as this is the version used by the main development team.
 
@@ -53,15 +53,15 @@ After having retrieved the code and acquired all the dependencies mentioned in [
 
 <a id="engine_configuration"></a>
 ## Engine Configuration
-In order to utilize the model-checking capabilities of the system, at least one engine must be configured. 
+In order to utilize the model-checking capabilities of the system, at least one engine must be configured.
 The distributions available at [ECDAR](https://github.com/Ecdar/ECDAR) will automatically load the default engines on startup, but this is currently not working when running the GUI through Gradle.
 For the same reason, the `Reset Engines` button will clear the engines but will not be able to load the packaged once.
 
 An engine can be added through the configurator found under `Options > Engines Options` in the menubar, which opens the pop-up shown below.
 
 <img src="presentation/EngineConfiguration.png" alt="Engine Configuration Pop-up">
 
-> :information_source: If you accidentally removed or changed an engine, these changes can be reverted be pressing `Cancel` or by clicking outside the pop-up. Consequently, if any changes should be saved, **MAKE SURE TO PRESS `Save`** 
+> :information_source: If you accidentally removed or changed an engine, these changes can be reverted be pressing `Cancel` or by clicking outside the pop-up. Consequently, if any changes should be saved, **MAKE SURE TO PRESS `Save`**
 
 ### Address
 The _Address_ is either the address of a server running the engine (for remote execution) or a path to a local engine binary (for this, the _Local_ checkbox must be checked).
@@ -75,7 +75,7 @@ If an engine is marked with _Default_, all added queries will be assigned that e
 
 
 ## Exemplary Projects
-To get started and get an idea of what the system can be used for, multiple examples can be found in the `examples` directory. 
+To get started and get an idea of what the system can be used for, multiple examples can be found in the `examples` directory.
 These projects include preconfigured models and queries to execute against them.
 
 For the theoretical background and what the tool can be used for, please check out the latest research links at [here](https://ulrik.blog.aau.dk/ecdar/).
@@ -93,7 +93,7 @@ Pull requests are continuously being reviewed and merged. In order to ease this
 
 Additionally, please add `Closes #{ISSUE_ID}` if the pull request is linked to a specific issue. If a PR addresses multiple pull requests, please add `Closes #{ISSUE_ID}` for each one.
 
-A CI workflow is executed against all pull requests and must succeed before the pull request can be merged, so please make sure that you check the workflow status and potential error messages. 
+A CI workflow is executed against all pull requests and must succeed before the pull request can be merged, so please make sure that you check the workflow status and potential error messages.
 
 ### Tests
 All non-UI tests are executed as part of the CI workflow and hence must succeed before merging. The tests are written with JUnit and relevant tests should be added when new code is added. If you are new to JUnit, you can check out syntax and structure [here](https://junit.org/junit5/docs/current/user-guide/).
@@ -103,7 +103,7 @@ The test suite can be executed locally by running:
 ./gradlew test
 ```
 
-> :information_source: Currently, the codebase has high coupling, which has made testing difficult and the test suite very small. 
+> :information_source: Currently, the codebase has high coupling, which has made testing difficult and the test suite very small.
 
 #### UI Tests
 For features that are highly coupled with the interface, a second test suite has been added under `src/test/java/ecdar/ui`. These tests are excluded from the `test` task are can be executed by running:
@@ -154,4 +154,4 @@ Besides the packages mentioned above, some larger functionalities are located in
 - `code_analysis`: Responsible for analysing the elements of the current project and construct messages if errors or warnings are encountered.
 - `issues`: Classes for representing `Errors`, `Issues`, and `Warnings`.
 - `model_canvas.arrow_heads`: Arrowheads used in the UI to visualize the direction of edges.
-
+- `mutation [Deprecrated]`: Functionality for supporting mutation testing of components. **This feature is currently not implemented in the engines and is therefor currently not supported**.  

examples/AGTest/Queries.json

@@ -5,22 +5,22 @@
     "isPeriodic": false,
     "ignoredInputs": {},
     "ignoredOutputs": {},
-    "backend": "Reveaal"
+    "engine": "Reveaal"
   },
   {
     "query": "refinement: ((A1 || G2) \\ A2) \u003c\u003d G1",
     "comment": "",
     "isPeriodic": false,
     "ignoredInputs": {},
     "ignoredOutputs": {},
-    "backend": "Reveaal"
+    "engine": "Reveaal"
   },
   {
     "query": "refinement:  ((A1 || G1) \\ A2) \u003c\u003d Imp",
     "comment": "",
     "isPeriodic": false,
     "ignoredInputs": {},
     "ignoredOutputs": {},
-    "backend": "Reveaal"
+    "engine": "Reveaal"
   }
 ]

examples/CarAlarm/Model/Queries.json

@@ -5,46 +5,46 @@
     "isPeriodic": false,
     "ignoredInputs": {},
     "ignoredOutputs": {},
-    "backend": "Reveaal"
+    "engine": "Reveaal"
   },
   {
     "query": "specification: Alarm",
     "comment": "",
     "isPeriodic": false,
     "ignoredInputs": {},
     "ignoredOutputs": {},
-    "backend": "Reveaal"
+    "engine": "Reveaal"
   },
   {
     "query": "reachability: Alarm.L11",
     "comment": "",
     "isPeriodic": false,
     "ignoredInputs": {},
     "ignoredOutputs": {},
-    "backend": "Reveaal"
+    "engine": "Reveaal"
   },
   {
     "query": "reachability: Alarm.L12",
     "comment": "",
     "isPeriodic": false,
     "ignoredInputs": {},
     "ignoredOutputs": {},
-    "backend": "Reveaal"
+    "engine": "Reveaal"
   },
   {
     "query": "reachability: Alarm.L9",
     "comment": "",
     "isPeriodic": false,
     "ignoredInputs": {},
     "ignoredOutputs": {},
-    "backend": "Reveaal"
+    "engine": "Reveaal"
   },
   {
     "query": "specification: (Alarm: A[] not Alarm.L7 || Alarm.x\u003c\u003d30)",
     "comment": "",
     "isPeriodic": false,
     "ignoredInputs": {},
     "ignoredOutputs": {},
-    "backend": "Reveaal"
+    "engine": "Reveaal"
   }
 ]

examples/EcdarUniversity/Queries.json

@@ -5,38 +5,38 @@
     "isPeriodic": false,
     "ignoredInputs": {},
     "ignoredOutputs": {},
-    "backend": "Reveaal"
+    "engine": "Reveaal"
   },
   {
     "query": "specification: Spec",
     "comment": "",
     "isPeriodic": false,
     "ignoredInputs": {},
     "ignoredOutputs": {},
-    "backend": "Reveaal"
+    "engine": "Reveaal"
   },
   {
     "query": "consistency: (Administration || Machine || Researcher)",
     "comment": "",
     "isPeriodic": false,
     "ignoredInputs": {},
     "ignoredOutputs": {},
-    "backend": "Reveaal"
+    "engine": "Reveaal"
   },
   {
     "query": "consistency: (Administration || Machine || Researcher)",
     "comment": "",
     "isPeriodic": false,
     "ignoredInputs": {},
     "ignoredOutputs": {},
-    "backend": "Reveaal"
+    "engine": "Reveaal"
   },
   {
     "query": "refinement: (Administration || Machine || Researcher) \u003c\u003d Spec",
     "comment": "",
     "isPeriodic": false,
     "ignoredInputs": {},
     "ignoredOutputs": {},
-    "backend": "Reveaal"
+    "engine": "Reveaal"
   }
 ]

examples/FishRetailer/Model/Queries.json

@@ -5,6 +5,6 @@
     "isPeriodic": false,
     "ignoredInputs": {},
     "ignoredOutputs": {},
-    "backend": "Reveaal"
+    "engine": "Reveaal"
   }
 ]

examples/SenderReceiver/Queries.json

@@ -5,22 +5,22 @@
     "isPeriodic": false,
     "ignoredInputs": {},
     "ignoredOutputs": {},
-    "backend": "Reveaal"
+    "engine": "Reveaal"
   },
   {
     "query": "specification: Sender",
     "comment": "",
     "isPeriodic": false,
     "ignoredInputs": {},
     "ignoredOutputs": {},
-    "backend": "Reveaal"
+    "engine": "Reveaal"
   },
   {
     "query": "implementation: Sender",
     "comment": "",
     "isPeriodic": false,
     "ignoredInputs": {},
     "ignoredOutputs": {},
-    "backend": "Reveaal"
+    "engine": "Reveaal"
   }
 ]

src/main/java/ecdar/Ecdar.java

@@ -301,7 +301,7 @@ public void start(final Stage stage) {
             BackendHelper.stopQueries();
 
             try {
-                backendDriver.closeAllBackendConnections();
+                backendDriver.closeAllEngineConnections();
             } catch (IOException e) {
                 e.printStackTrace();
             }
@@ -310,11 +310,11 @@ public void start(final Stage stage) {
             System.exit(0);
         });
 
-        BackendHelper.addBackendInstanceListener(() -> {
-            // When the backend instances change, re-instantiate the backendDriver
+        BackendHelper.addEngineInstanceListener(() -> {
+            // When the engines change, re-instantiate the backendDriver
             // to prevent dangling connections and queries
             try {
-                backendDriver.closeAllBackendConnections();
+                backendDriver.closeAllEngineConnections();
             } catch (IOException e) {
                 throw new RuntimeException(e);
             }

src/main/java/ecdar/abstractions/BackendInstance.java → src/main/java/ecdar/abstractions/Engine.java

@@ -4,7 +4,7 @@
 import ecdar.utility.serialize.Serializable;
 import javafx.beans.property.SimpleBooleanProperty;
 
-public class BackendInstance implements Serializable {
+public class Engine implements Serializable {
     private static final String NAME = "name";
     private static final String IS_LOCAL = "isLocal";
     private static final String IS_DEFAULT = "isDefault";
@@ -16,14 +16,14 @@ public class BackendInstance implements Serializable {
     private String name;
     private boolean isLocal;
     private boolean isDefault;
-    private String backendLocation;
+    private String engineLocation;
     private int portStart;
     private int portEnd;
     private SimpleBooleanProperty locked = new SimpleBooleanProperty(false);
 
-    public BackendInstance() {};
+    public Engine() {};
 
-    public BackendInstance(final JsonObject jsonObject) {
+    public Engine(final JsonObject jsonObject) {
         deserialize(jsonObject);
     };
 
@@ -51,12 +51,12 @@ public void setDefault(boolean aDefault) {
         isDefault = aDefault;
     }
 
-    public String getBackendLocation() {
-        return backendLocation;
+    public String getEngineLocation() {
+        return engineLocation;
     }
 
-    public void setBackendLocation(String backendLocation) {
-        this.backendLocation = backendLocation;
+    public void setEngineLocation(String engineLocation) {
+        this.engineLocation = engineLocation;
     }
 
     public int getPortStart() {
@@ -76,7 +76,7 @@ public void setPortEnd(int portEnd) {
     }
 
     public int getNumberOfInstances() {
-        return this.portEnd - this.portStart;
+        return this.portEnd - this.portStart + 1;
     }
 
     public void lockInstance() {
@@ -93,7 +93,7 @@ public JsonObject serialize() {
         result.addProperty(NAME, getName());
         result.addProperty(IS_LOCAL, isLocal());
         result.addProperty(IS_DEFAULT, isDefault());
-        result.addProperty(LOCATION, getBackendLocation());
+        result.addProperty(LOCATION, getEngineLocation());
         result.addProperty(PORT_RANGE_START, getPortStart());
         result.addProperty(PORT_RANGE_END, getPortEnd());
         result.addProperty(LOCKED, getLockedProperty().get());
@@ -106,7 +106,7 @@ public void deserialize(final JsonObject json) {
         setName(json.getAsJsonPrimitive(NAME).getAsString());
         setLocal(json.getAsJsonPrimitive(IS_LOCAL).getAsBoolean());
         setDefault(json.getAsJsonPrimitive(IS_DEFAULT).getAsBoolean());
-        setBackendLocation(json.getAsJsonPrimitive(LOCATION).getAsString());
+        setEngineLocation(json.getAsJsonPrimitive(LOCATION).getAsString());
         setPortStart(json.getAsJsonPrimitive(PORT_RANGE_START).getAsInt());
         setPortEnd(json.getAsJsonPrimitive(PORT_RANGE_END).getAsInt());
         if (json.getAsJsonPrimitive(LOCKED).getAsBoolean()) lockInstance();

src/main/java/ecdar/abstractions/Query.java

@@ -3,7 +3,6 @@
 import ecdar.Ecdar;
 import ecdar.backend.*;
 import ecdar.controllers.EcdarController;
-import ecdar.utility.helpers.StringValidator;
 import ecdar.utility.serialize.Serializable;
 import com.google.gson.JsonObject;
 import javafx.application.Platform;
@@ -15,15 +14,15 @@ public class Query implements Serializable {
     private static final String QUERY = "query";
     private static final String COMMENT = "comment";
     private static final String IS_PERIODIC = "isPeriodic";
-    private static final String BACKEND = "backend";
+    private static final String ENGINE = "engine";
 
     private final StringProperty query = new SimpleStringProperty("");
     private final StringProperty comment = new SimpleStringProperty("");
     private final StringProperty errors = new SimpleStringProperty("");
     private final SimpleBooleanProperty isPeriodic = new SimpleBooleanProperty(false);
     private final ObjectProperty<QueryState> queryState = new SimpleObjectProperty<>(QueryState.UNKNOWN);
     private final ObjectProperty<QueryType> type = new SimpleObjectProperty<>();
-    private BackendInstance backend;
+    private Engine engine;
 
 
     private final Consumer<Boolean> successConsumer = (aBoolean) -> {
@@ -61,7 +60,7 @@ public Query(final String query, final String comment, final QueryState querySta
         this.query.set(query);
         this.comment.set(comment);
         this.queryState.set(queryState);
-        setBackend(BackendHelper.getDefaultBackendInstance());
+        setEngine(BackendHelper.getDefaultEngine());
     }
 
     public Query(final JsonObject jsonElement) {
@@ -118,12 +117,12 @@ public void setIsPeriodic(final boolean isPeriodic) {
         this.isPeriodic.set(isPeriodic);
     }
 
-    public BackendInstance getBackend() {
-        return backend;
+    public Engine getEngine() {
+        return engine;
     }
 
-    public void setBackend(BackendInstance backend) {
-        this.backend = backend;
+    public void setEngine(Engine engine) {
+        this.engine = engine;
     }
 
     public void setType(QueryType type) {
@@ -153,7 +152,7 @@ public JsonObject serialize() {
         result.addProperty(QUERY, getType().getQueryName() + ": " + getQuery());
         result.addProperty(COMMENT, getComment());
         result.addProperty(IS_PERIODIC, isPeriodic());
-        result.addProperty(BACKEND, backend.getName());
+        result.addProperty(ENGINE, engine.getName());
 
         return result;
     }
@@ -176,10 +175,10 @@ public void deserialize(final JsonObject json) {
             setIsPeriodic(json.getAsJsonPrimitive(IS_PERIODIC).getAsBoolean());
         }
 
-        if(json.has(BACKEND)) {
-            setBackend(BackendHelper.getBackendInstanceByName(json.getAsJsonPrimitive(BACKEND).getAsString()));
+        if(json.has(ENGINE)) {
+            setEngine(BackendHelper.getEngineByName(json.getAsJsonPrimitive(ENGINE).getAsString()));
         } else {
-            setBackend(BackendHelper.getDefaultBackendInstance());
+            setEngine(BackendHelper.getDefaultEngine());
         }
     }