diff --git a/src/main/java/ecdar/Ecdar.java b/src/main/java/ecdar/Ecdar.java index 8e0c7c66..ea170b62 100644 --- a/src/main/java/ecdar/Ecdar.java +++ b/src/main/java/ecdar/Ecdar.java @@ -47,7 +47,7 @@ public class Ecdar extends Application { public static SimpleStringProperty projectDirectory = new SimpleStringProperty(); private static BooleanProperty isUICached = new SimpleBooleanProperty(); private static final BooleanProperty isSplit = new SimpleBooleanProperty(true); //Set to true to ensure correct behaviour at first toggle. - private static BackendDriver backendDriver; + private static final BackendDriver backendDriver = new BackendDriver(); private Stage debugStage; /** @@ -190,7 +190,6 @@ public void start(final Stage stage) { // Load the fonts required for the project IconFontFX.register(GoogleMaterialDesignIcons.getIconFont()); loadFonts(); - loadPreferences(); // Remove the classic decoration // kyrke - 2020-04-17: Disabled due to bug https://bugs.openjdk.java.net/browse/JDK-8154847 @@ -212,6 +211,8 @@ public void start(final Stage stage) { scene.getStylesheets().add("ecdar/main.css"); scene.getStylesheets().add("ecdar/colors.css"); scene.getStylesheets().add("ecdar/model_canvas.css"); + scene.getStylesheets().add("ecdar/query_pane.css"); + scene.getStylesheets().add("ecdar/scroll_pane.css"); // Handle a mouse click as a deselection of all elements scene.setOnMousePressed(event -> { @@ -289,16 +290,6 @@ public void start(final Stage stage) { }); } - private void loadPreferences() { - BackendHelper.defaultBackend = preferences.getInt("default_backend", BackendHelper.BackendNames.jEcdar.ordinal()) - == BackendHelper.BackendNames.jEcdar.ordinal() - ? BackendHelper.BackendNames.jEcdar - : BackendHelper.BackendNames.Reveaal; - - backendDriver = new BackendDriver(preferences.get("backend_host_address", "127.0.0.1")); - getBackendDriver().setMaxNumberOfConnections(preferences.getInt("number_of_backend_sockets", 5)); - } - /** * Initializes and resets the project. * This can be used as a test setup. @@ -381,6 +372,5 @@ private void loadFonts() { Font.loadFont(getClass().getResourceAsStream("fonts/roboto_mono/RobotoMono-Regular.ttf"), 14); Font.loadFont(getClass().getResourceAsStream("fonts/roboto_mono/RobotoMono-Thin.ttf"), 14); Font.loadFont(getClass().getResourceAsStream("fonts/roboto_mono/RobotoMono-ThinItalic.ttf"), 14); - } } diff --git a/src/main/java/ecdar/abstractions/BackendInstance.java b/src/main/java/ecdar/abstractions/BackendInstance.java new file mode 100644 index 00000000..3b0eba76 --- /dev/null +++ b/src/main/java/ecdar/abstractions/BackendInstance.java @@ -0,0 +1,119 @@ +package ecdar.abstractions; + +import com.google.gson.JsonObject; +import ecdar.utility.serialize.Serializable; +import javafx.beans.property.SimpleBooleanProperty; + +public class BackendInstance implements Serializable { + private static final String NAME = "name"; + private static final String IS_LOCAL = "isLocal"; + private static final String IS_DEFAULT = "isDefault"; + private static final String LOCATION = "location"; + private static final String PORT_RANGE_START = "portRangeStart"; + private static final String PORT_RANGE_END = "portRangeEnd"; + private static final String LOCKED = "locked"; + + private String name; + private boolean isLocal; + private boolean isDefault; + private String backendLocation; + private int portStart; + private int portEnd; + private SimpleBooleanProperty locked = new SimpleBooleanProperty(false); + + public BackendInstance() {}; + + public BackendInstance(final JsonObject jsonObject) { + deserialize(jsonObject); + }; + + public String getName() { + return name; + } + + public void setName(String name) { + this.name = name; + } + + public boolean isLocal() { + return isLocal; + } + + public void setLocal(boolean local) { + isLocal = local; + } + + public boolean isDefault() { + return isDefault; + } + + public void setDefault(boolean aDefault) { + isDefault = aDefault; + } + + public String getBackendLocation() { + return backendLocation; + } + + public void setBackendLocation(String backendLocation) { + this.backendLocation = backendLocation; + } + + public int getPortStart() { + return portStart; + } + + public void setPortStart(int portStart) { + this.portStart = portStart; + } + + public int getPortEnd() { + return portEnd; + } + + public void setPortEnd(int portEnd) { + this.portEnd = portEnd; + } + + public int getNumberOfInstances() { + return this.portEnd - this.portStart; + } + + public void lockInstance() { + locked.set(true); + } + + public SimpleBooleanProperty getLockedProperty() { + return locked; + } + + @Override + public JsonObject serialize() { + final JsonObject result = new JsonObject(); + result.addProperty(NAME, getName()); + result.addProperty(IS_LOCAL, isLocal()); + result.addProperty(IS_DEFAULT, isDefault()); + result.addProperty(LOCATION, getBackendLocation()); + result.addProperty(PORT_RANGE_START, getPortStart()); + result.addProperty(PORT_RANGE_END, getPortEnd()); + result.addProperty(LOCKED, getLockedProperty().get()); + + return result; + } + + @Override + 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()); + setPortStart(json.getAsJsonPrimitive(PORT_RANGE_START).getAsInt()); + setPortEnd(json.getAsJsonPrimitive(PORT_RANGE_END).getAsInt()); + if (json.getAsJsonPrimitive(LOCKED).getAsBoolean()) lockInstance(); + } + + @Override + public String toString() { + return name; + } +} diff --git a/src/main/java/ecdar/abstractions/Project.java b/src/main/java/ecdar/abstractions/Project.java index 0a0e0be2..5aa2662a 100644 --- a/src/main/java/ecdar/abstractions/Project.java +++ b/src/main/java/ecdar/abstractions/Project.java @@ -169,7 +169,7 @@ public void deserialize(final File projectFolder) throws IOException { deserializeFileHelper(file); } } - // Now we have gone though all the files in the directory we can now deserialize folders + // Now we have gone through all the files in the directory we can now deserialize folders if(componentFolder != null || systemFolder != null) { deserializeComponents(componentFolder); deserializeSystems(systemFolder); diff --git a/src/main/java/ecdar/abstractions/Query.java b/src/main/java/ecdar/abstractions/Query.java index 1c2f60bd..fcfbe392 100644 --- a/src/main/java/ecdar/abstractions/Query.java +++ b/src/main/java/ecdar/abstractions/Query.java @@ -30,14 +30,14 @@ public class Query implements Serializable { private final SimpleBooleanProperty isPeriodic = new SimpleBooleanProperty(false); private final StringProperty errors = new SimpleStringProperty(""); private final ObjectProperty type = new SimpleObjectProperty<>(); - private BackendHelper.BackendNames backend; + private BackendInstance backend; private Consumer runQuery; public Query(final String query, final String comment, final QueryState queryState) { this.query.set(query); this.comment.set(comment); this.queryState.set(queryState); - setBackend(BackendHelper.defaultBackend); + setBackend(BackendHelper.getDefaultBackendInstance()); initializeRunQuery(); } @@ -98,11 +98,11 @@ public void setIsPeriodic(final boolean isPeriodic) { this.isPeriodic.set(isPeriodic); } - public BackendHelper.BackendNames getBackend() { + public BackendInstance getBackend() { return backend; } - public void setBackend(BackendHelper.BackendNames backend) { + public void setBackend(BackendInstance backend) { this.backend = backend; } @@ -179,7 +179,7 @@ public JsonObject serialize() { result.add(IGNORED_INPUTS, getHashMapAsJsonObject(ignoredInputs)); result.add(IGNORED_OUTPUTS, getHashMapAsJsonObject(ignoredOutputs)); - result.addProperty(BACKEND, backend.ordinal()); + result.addProperty(BACKEND, backend.getName()); return result; } @@ -219,11 +219,9 @@ public void deserialize(final JsonObject json) { } if(json.has(BACKEND)) { - setBackend(json.getAsJsonPrimitive(BACKEND).getAsInt() == BackendHelper.BackendNames.jEcdar.ordinal() - ? BackendHelper.BackendNames.jEcdar - : BackendHelper.BackendNames.Reveaal); + setBackend(BackendHelper.getBackendInstanceByName(json.getAsJsonPrimitive(BACKEND).getAsString())); } else { - setBackend(BackendHelper.defaultBackend); + setBackend(BackendHelper.getDefaultBackendInstance()); } } diff --git a/src/main/java/ecdar/abstractions/QueryType.java b/src/main/java/ecdar/abstractions/QueryType.java index 4c399601..3864ecaa 100644 --- a/src/main/java/ecdar/abstractions/QueryType.java +++ b/src/main/java/ecdar/abstractions/QueryType.java @@ -5,7 +5,7 @@ public enum QueryType { QUOTIENT("quotient", "\\"), SPECIFICATION("specification", "Spec"), IMPLEMENTATION("implementation", "Imp"), - LOCAL_CONSISTENCY("local-consistency", "lCon"), + LOCAL_CONSISTENCY("consistency", "lCon"), // ToDo NIELS: Will become local-consistency GLOBAL_CONSISTENCY("global-consistency", "gCon"), BISIM_MIN("bisim", "bsim"), GET_COMPONENT("get-component", "get"), diff --git a/src/main/java/ecdar/backend/BackendDriver.java b/src/main/java/ecdar/backend/BackendDriver.java index 7ea20558..3d561cc8 100644 --- a/src/main/java/ecdar/backend/BackendDriver.java +++ b/src/main/java/ecdar/backend/BackendDriver.java @@ -5,6 +5,7 @@ import EcdarProtoBuf.QueryProtos; import com.google.protobuf.Empty; import ecdar.Ecdar; +import ecdar.abstractions.BackendInstance; import ecdar.abstractions.Component; import ecdar.abstractions.QueryState; import io.grpc.*; @@ -18,33 +19,28 @@ import java.util.function.Consumer; public class BackendDriver { - private int maxNumberOfBackendConnections = 5; - private final List reveaalConnections = new CopyOnWriteArrayList<>(); - private final List jEcdarConnections = new CopyOnWriteArrayList<>(); - - private final String hostAddress; - + private final List openBackendConnections = new CopyOnWriteArrayList<>(); private final int deadlineForResponses = 20000; private final int rerunQueryDelay = 200; + private final int numberOfRetriesPerQuery = 5; - public BackendDriver(String hostAddress) { - this.hostAddress = hostAddress; + public BackendDriver() { } /** * Add the query to execution queue with consumers for success and failure, executed when response received from backends * - * @param query the query to be executed - * @param backend the backend to execute the query on - * @param success consumer for a successful response - * @param failure consumer for a failure response - * @param queryListener query listener for referencing the query for GUI purposes + * @param query the query to be executed + * @param backendInstance name of the backend to execute the query with + * @param success consumer for a successful response + * @param failure consumer for a failure response + * @param queryListener query listener for referencing the query for GUI purposes */ - public void addQueryToExecutionQueue(String query, BackendHelper.BackendNames backend, Consumer success, Consumer failure, QueryListener queryListener) { + public void addQueryToExecutionQueue(String query, BackendInstance backendInstance, Consumer success, Consumer failure, QueryListener queryListener) { new Timer().schedule(new TimerTask() { @Override public void run() { - new ExecutableQuery(query, backend, success, failure, queryListener).execute(); + new ExecutableQuery(query, backendInstance, success, failure, queryListener).execute(); } }, rerunQueryDelay); } @@ -55,8 +51,8 @@ public void run() { * * @param query the ignored input output query containing the query and related GUI elements */ - public void getInputOutputs(IgnoredInputOutputQuery query) { - ExecutableQuery executableQuery = new ExecutableQuery(query.getQuery().getQuery(), BackendHelper.BackendNames.Reveaal, + public void getInputOutputs(IgnoredInputOutputQuery query, BackendInstance backendInstance) { + ExecutableQuery executableQuery = new ExecutableQuery(query.getQuery().getQuery(), backendInstance, a -> { }, @@ -67,16 +63,16 @@ public void getInputOutputs(IgnoredInputOutputQuery query) { // Get available connection or start new (only Reveaal supports ignored inputs/outputs) final Optional connection; - connection = reveaalConnections.stream().filter((element) -> !element.isRunningQuery()).findFirst(); + connection = openBackendConnections.stream().filter((element) -> !element.isRunningQuery() && element.getBackendInstance().equals(backendInstance)).findFirst(); final BackendConnection backendConnection = connection.orElseGet(() -> - (startNewBackendConnection(BackendHelper.BackendNames.Reveaal))); + (startNewBackendConnection(backendInstance))); // If the query connection is null, there are no available sockets // and the maximum number of sockets has already been reached if (backendConnection == null) { new Timer().schedule(new TimerTask() { @Override public void run() { - getInputOutputs(query); + getInputOutputs(query, backendInstance); } }, rerunQueryDelay); return; @@ -93,7 +89,8 @@ public void run() { private boolean error = false; @Override - public void onNext(Empty value) {} + public void onNext(Empty value) { + } @Override public void onError(Throwable t) { @@ -131,65 +128,27 @@ public void onCompleted() { } /** - * Close every open connection for all backends + * Close all open backend connection and kill all locally running processes * - * @throws IOException originally thrown by related process when it is destroyed + * @throws IOException if any of the sockets do not respond */ public void closeAllBackendConnections() throws IOException { - for (BackendConnection s : reveaalConnections) s.close(); - for (BackendConnection s : jEcdarConnections) s.close(); - } - - public int getMaxNumberOfSockets() { - return maxNumberOfBackendConnections; - } - - /** - * Change the number of backend connection currently running for each backend. - * - * This will close connections if there are currently more connection open than the desired number - * @param i the new maximum for open connections - */ - public void setMaxNumberOfConnections(int i) { - maxNumberOfBackendConnections = i; - - closeAdditionalConnections(reveaalConnections); - closeAdditionalConnections(jEcdarConnections); - } - - private void closeAdditionalConnections(List connections) { - while (connections.size() > maxNumberOfBackendConnections) { - BackendConnection unoccupiedConnection = connections.stream().filter(backendConnection -> backendConnection.executableQuery == null).findFirst().orElse(null); - if (unoccupiedConnection != null) { - try { - unoccupiedConnection.close(); - } catch (IOException e) { - e.printStackTrace(); - } finally { - connections.remove(unoccupiedConnection); - } - } - } + for (BackendConnection s : openBackendConnections) s.close(); } private void executeQuery(ExecutableQuery executableQuery) { if (executableQuery.queryListener.getQuery().getQueryState() == QueryState.UNKNOWN) return; // Get available connection or start new - final Optional connection; - if (executableQuery.backend.equals(BackendHelper.BackendNames.jEcdar)) { - connection = jEcdarConnections.stream().filter((element) -> !element.isRunningQuery()).findFirst(); - } else { - connection = reveaalConnections.stream().filter((element) -> !element.isRunningQuery()).findFirst(); - } - - final BackendConnection backendConnection = connection.orElseGet(() -> executableQuery.backend.equals(BackendHelper.BackendNames.Reveaal) ? - (startNewBackendConnection(BackendHelper.BackendNames.Reveaal)) : startNewBackendConnection(BackendHelper.BackendNames.jEcdar)); + final BackendConnection backendConnection = openBackendConnections.stream() + .filter((connection) -> connection.getBackendInstance() == null || connection.getBackendInstance().equals(executableQuery.backend)) + .findFirst() + .orElseGet(() -> startNewBackendConnection(executableQuery.backend)); - // If the query connection is null, there are no available sockets - // and the maximum number of sockets has already been reached + // If the connection is null, there are no available connections, + // and it was not possible to start a new one if (backendConnection == null) { - if (executableQuery.tries < 5) { + if (executableQuery.tries < numberOfRetriesPerQuery) { new Timer().schedule(new TimerTask() { @Override public void run() { @@ -219,11 +178,9 @@ public void onNext(Empty value) { @Override public void onError(Throwable t) { - // Check if query has been canceled if (executableQuery.queryListener.getQuery().getQueryState() != QueryState.UNKNOWN) { - handleBackendError(t, backendConnection); + handleBackendError(t, executableQuery); error = true; - backendConnection.setExecutableQuery(null); } } @@ -234,24 +191,26 @@ public void onCompleted() { @Override public void onNext(QueryProtos.QueryResponse value) { if (executableQuery.queryListener.getQuery().getQueryState() != QueryState.UNKNOWN) { - handleResponse(backendConnection.getExecutableQuery(), value); + handleResponse(executableQuery, value); } - backendConnection.setExecutableQuery(null); } @Override public void onError(Throwable t) { if (executableQuery.queryListener.getQuery().getQueryState() != QueryState.UNKNOWN) { - handleBackendError(t, backendConnection); + handleBackendError(t, executableQuery); } - backendConnection.setExecutableQuery(null); } @Override public void onCompleted() { + backendConnection.setExecutableQuery(null); } }; - backendConnection.getStub().withDeadlineAfter(deadlineForResponses, TimeUnit.MILLISECONDS).sendQuery(QueryProtos.Query.newBuilder().setId(0).setQuery(backendConnection.getExecutableQuery().query).build(), responseObserver); + + backendConnection.getStub().withDeadlineAfter(deadlineForResponses, TimeUnit.MILLISECONDS).sendQuery(QueryProtos.Query.newBuilder().setId(0).setQuery(executableQuery.query).build(), responseObserver); + } else { + backendConnection.setExecutableQuery(null); } } }; @@ -259,54 +218,62 @@ public void onCompleted() { backendConnection.getStub().withDeadlineAfter(deadlineForResponses, TimeUnit.MILLISECONDS).updateComponents(componentsBuilder.build(), observer); } - private void handleBackendError(Throwable t, BackendConnection backendConnection) { - // Each error starts with a capitalized description of the error equal to the gRPC error type encountered - String errorType = t.getMessage().split(":\\s+", 2)[0]; - final ExecutableQuery query = backendConnection.getExecutableQuery(); - - switch (errorType) { - case "CANCELLED": - backendConnection.getExecutableQuery().queryListener.getQuery().setQueryState(QueryState.ERROR); - backendConnection.getExecutableQuery().failure.accept(new BackendException.QueryErrorException("The query was cancelled")); - break; - case "DEADLINE_EXCEEDED": - backendConnection.getExecutableQuery().queryListener.getQuery().setQueryState(QueryState.ERROR); - backendConnection.getExecutableQuery().failure.accept(new BackendException.QueryErrorException("The backend did not answer the request in time")); + private BackendConnection startNewBackendConnection(BackendInstance backend) { + Process p = null; + String hostAddress = (backend.isLocal() ? "127.0.0.1" : backend.getBackendLocation()); + long portNumber = 0; - new Timer().schedule(new TimerTask() { - @Override - public void run() { - query.execute(); - } - }, rerunQueryDelay); + if (backend.isLocal()) { + try { + portNumber = SocketUtils.findAvailableTcpPort(backend.getPortStart(), backend.getPortEnd()); + } catch (IllegalStateException e) { + Ecdar.showToast("No available port for " + backend.getName() + " with port range " + backend.getPortStart() + " - " + backend.getPortEnd()); + } - break; - case "UNIMPLEMENTED": - backendConnection.getExecutableQuery().queryListener.getQuery().setQueryState(QueryState.SYNTAX_ERROR); - backendConnection.getExecutableQuery().failure.accept(new BackendException.QueryErrorException("The query type is not supported by the backend")); - break; - case "INTERNAL": - backendConnection.getExecutableQuery().queryListener.getQuery().setQueryState(QueryState.ERROR); - backendConnection.getExecutableQuery().failure.accept(new BackendException.QueryErrorException("Reveaal was unable to execute this query:\n" + t.getMessage().split(": ", 2)[1])); - break; - case "UNKNOWN": - backendConnection.getExecutableQuery().queryListener.getQuery().setQueryState(QueryState.ERROR); - backendConnection.getExecutableQuery().failure.accept(new BackendException.QueryErrorException("The backend encountered an unknown error")); - break; - default: - backendConnection.getExecutableQuery().queryListener.getQuery().setQueryState(QueryState.ERROR); - backendConnection.getExecutableQuery().failure.accept(new BackendException.QueryErrorException("The query failed and gave the following error: " + errorType)); + do { + ProcessBuilder pb = new ProcessBuilder(backend.getBackendLocation(), "-p", hostAddress + ":" + portNumber); -// try { -// backendConnection.close(); -// } catch (IOException e) { -// e.printStackTrace(); -// } + try { + p = pb.start(); + } catch (IOException ioException) { + Ecdar.showToast("Unable to start backend instance"); + ioException.printStackTrace(); + return null; + } + // If the process is not alive, it failed while starting up, try again + } while (!p.isAlive()); + } else { + // Filter active instances of this engine and map their used ports to an int stream + var activeEnginePorts = openBackendConnections.stream() + .filter((bi) -> bi.backendInstance.equals(backend)) + .mapToInt((bi) -> Integer.parseInt(bi.getStub().getChannel().authority().split(":", 2)[1])); + + int currentPort = backend.getPortStart(); + do { + // Find port not already connected to + int tempPortNumber = currentPort; + if (activeEnginePorts.noneMatch((i) -> i == tempPortNumber)) { + portNumber = tempPortNumber; + } else { + currentPort++; + } + } while (portNumber == 0 && currentPort <= backend.getPortEnd()); - break; + if (currentPort > backend.getPortEnd()) { + Ecdar.showToast("Unable to connect to remote engine: " + backend.getName() + " with port range " + backend.getPortStart() + " - " + backend.getPortEnd()); + return null; + } } - backendConnection.setExecutableQuery(null); + ManagedChannel channel = ManagedChannelBuilder.forTarget(hostAddress + ":" + portNumber) + .usePlaintext() + .keepAliveTime(1000, TimeUnit.MILLISECONDS) + .build(); + + EcdarBackendGrpc.EcdarBackendStub stub = EcdarBackendGrpc.newStub(channel); + BackendConnection newConnection = new BackendConnection(backend, p, stub); + this.openBackendConnections.add(newConnection); + return newConnection; } private void handleResponse(ExecutableQuery executableQuery, QueryProtos.QueryResponse value) { @@ -314,100 +281,79 @@ private void handleResponse(ExecutableQuery executableQuery, QueryProtos.QueryRe executableQuery.queryListener.getQuery().setQueryState(QueryState.SUCCESSFUL); executableQuery.success.accept(true); } else if (value.hasConsistency() && value.getConsistency().getSuccess()) { - System.out.println("Consistency"); executableQuery.queryListener.getQuery().setQueryState(QueryState.SUCCESSFUL); executableQuery.success.accept(true); } else if (value.hasDeterminism() && value.getDeterminism().getSuccess()) { - System.out.println("Determinism"); executableQuery.queryListener.getQuery().setQueryState(QueryState.SUCCESSFUL); executableQuery.success.accept(true); } else if (value.hasComponent()) { - System.out.println("Component"); executableQuery.queryListener.getQuery().setQueryState(QueryState.SUCCESSFUL); executableQuery.success.accept(true); } else { - System.out.println(value.getError()); executableQuery.queryListener.getQuery().setQueryState(QueryState.ERROR); executableQuery.success.accept(false); } } - private BackendConnection startNewBackendConnection(BackendHelper.BackendNames backend) { - boolean isReveaal = backend.equals(BackendHelper.BackendNames.Reveaal); + private void handleBackendError(Throwable t, ExecutableQuery query) { + // Each error starts with a capitalized description of the error equal to the gRPC error type encountered + String errorType = t.getMessage().split(":\\s+", 2)[0]; - if ((isReveaal ? reveaalConnections.size() < maxNumberOfBackendConnections - : jEcdarConnections.size() < maxNumberOfBackendConnections)) { - try { - Process p; - int portNumber = SocketUtils.findAvailableTcpPort(); - - do { - ProcessBuilder pb; - - File engine = null; - if (isReveaal) { - List searchPath = List.of ( - new File("lib/Reveaal.exe"), new File("lib/Reveaal") - ); - for (var f: searchPath){ - if (f.exists()) { - engine = f; - break; - } - } - if (engine == null) { - throw new RuntimeException("Could not locate Reveaal engine"); - } + switch (errorType) { + case "CANCELLED": + query.queryListener.getQuery().setQueryState(QueryState.ERROR); + query.failure.accept(new BackendException.QueryErrorException("The query was cancelled")); + break; + case "DEADLINE_EXCEEDED": + query.queryListener.getQuery().setQueryState(QueryState.ERROR); + query.failure.accept(new BackendException.QueryErrorException("The backend did not answer the request in time")); - pb = new ProcessBuilder(engine.getAbsolutePath(), "-p", this.hostAddress + ":" + portNumber); - } else { - pb = new ProcessBuilder("java", "-jar", "lib/j-Ecdar.jar", "-p" + portNumber ); + new Timer().schedule(new TimerTask() { + @Override + public void run() { + query.execute(); } + }, rerunQueryDelay); - //DEBUG: Write process output to std out - //pb.redirectOutput(ProcessBuilder.Redirect.INHERIT); - //pb.redirectError(ProcessBuilder.Redirect.INHERIT); - - p = pb.start(); - // If the process is not alive, it failed while starting up, try again - } while (!p.isAlive()); - - - - ManagedChannel channel = ManagedChannelBuilder.forTarget(this.hostAddress + ":" + portNumber) - .usePlaintext() - .keepAliveTime(1000, TimeUnit.MILLISECONDS) - .build(); - - EcdarBackendGrpc.EcdarBackendStub stub = EcdarBackendGrpc.newStub(channel); - BackendConnection newConnection = new BackendConnection(p, stub); - - if (isReveaal) { - reveaalConnections.add(newConnection); - } else { - jEcdarConnections.add(newConnection); + break; + case "UNIMPLEMENTED": + query.queryListener.getQuery().setQueryState(QueryState.SYNTAX_ERROR); + query.failure.accept(new BackendException.QueryErrorException("The query type is not supported by the backend")); + break; + case "INTERNAL": + query.queryListener.getQuery().setQueryState(QueryState.ERROR); + query.failure.accept(new BackendException.QueryErrorException("The backend was unable to execute this query:\n" + t.getMessage().split(": ", 2)[1])); + break; + case "UNKNOWN": + query.queryListener.getQuery().setQueryState(QueryState.ERROR); + query.failure.accept(new BackendException.QueryErrorException("The backend encountered an unknown error")); + break; + case "UNAVAILABLE": + query.queryListener.getQuery().setQueryState(QueryState.SYNTAX_ERROR); + query.failure.accept(new BackendException.QueryErrorException("The backend could not be reached")); + break; + default: + try { + query.queryListener.getQuery().setQueryState(QueryState.ERROR); + query.failure.accept(new BackendException.QueryErrorException("The query failed and gave the following error: " + errorType)); + } catch (Exception e) { + e.printStackTrace(); } - - return newConnection; - } catch (IOException e) { - e.printStackTrace(); - } + break; } - - return null; } private class ExecutableQuery { private final String query; - private final BackendHelper.BackendNames backend; + private final BackendInstance backend; private final Consumer success; private final Consumer failure; private final QueryListener queryListener; public int tries = 0; - ExecutableQuery(String query, BackendHelper.BackendNames backend, Consumer success, Consumer failure, QueryListener queryListener) { + ExecutableQuery(String query, BackendInstance backendInstance, Consumer success, Consumer failure, QueryListener queryListener) { this.query = query; - this.backend = backend; + this.backend = backendInstance; this.success = success; this.failure = failure; this.queryListener = queryListener; @@ -417,19 +363,21 @@ private class ExecutableQuery { * Execute the query using the backend driver */ public void execute() { - executeQuery(this); tries++; + executeQuery(this); } } private class BackendConnection { private final Process process; private final EcdarBackendGrpc.EcdarBackendStub stub; + private final BackendInstance backendInstance; private ExecutableQuery executableQuery = null; - BackendConnection(Process process, EcdarBackendGrpc.EcdarBackendStub stub) throws IOException { + BackendConnection(BackendInstance backendInstance, Process process, EcdarBackendGrpc.EcdarBackendStub stub) { this.process = process; this.stub = stub; + this.backendInstance = backendInstance; } /** @@ -450,6 +398,17 @@ public ExecutableQuery getExecutableQuery() { return executableQuery; } + /** + * Get the backend instance that should be used to execute + * the query currently associated with this backend connection + * + * @return the instance of the associated executable query object, + * or null, if no executable query is currently associated + */ + public BackendInstance getBackendInstance() { + return backendInstance; + } + /** * Set the executable query to execute with the connection * @@ -475,13 +434,12 @@ public boolean isRunningQuery() { */ public void close() throws IOException { // Remove the connection from the connection list - if (jEcdarConnections.remove(this) || reveaalConnections.remove(this)) { - System.out.println("Successfully closed connection to backend"); - } else { - System.out.println("Tried to remove a connection not present in either connection list"); - } + openBackendConnections.remove(this); - process.destroy(); + // If the backend-instance is remote, there will not be a process + if (process != null) { + process.destroy(); + } } } diff --git a/src/main/java/ecdar/backend/BackendHelper.java b/src/main/java/ecdar/backend/BackendHelper.java index d64ddf25..b34e098d 100644 --- a/src/main/java/ecdar/backend/BackendHelper.java +++ b/src/main/java/ecdar/backend/BackendHelper.java @@ -2,10 +2,10 @@ import com.uppaal.model.core2.Document; import ecdar.Ecdar; -import ecdar.abstractions.Component; -import ecdar.abstractions.Location; -import ecdar.abstractions.Project; -import ecdar.abstractions.Query; +import ecdar.abstractions.*; +import javafx.beans.property.SimpleListProperty; +import javafx.collections.FXCollections; +import javafx.collections.ObservableList; import org.apache.commons.io.FileUtils; import java.io.File; @@ -17,11 +17,14 @@ import java.util.ArrayList; import java.util.Collections; import java.util.List; +import java.util.Optional; public final class BackendHelper { final static String TEMP_DIRECTORY = "temporary"; private static EcdarDocument ecdarDocument; - public static BackendHelper.BackendNames defaultBackend = BackendHelper.BackendNames.jEcdar; + private static BackendInstance defaultBackend = null; + private static ObservableList backendInstances = new SimpleListProperty<>(); + private static List backendInstancesUpdatedListeners = new ArrayList<>(); public static String storeBackendModel(Project project, String fileName) throws BackendException, IOException, URISyntaxException { return storeBackendModel(project, TEMP_DIRECTORY, fileName); @@ -44,7 +47,7 @@ public static String storeBackendModel(Project project, String relativeDirectory FileUtils.forceMkdir(new File(directoryPath)); final String path = directoryPath + File.separator + fileName + ".xml"; - storeEcdarFile(new EcdarDocument(project).toXmlDocument(), path); + storeEcdarFile(new EcdarDocument(project).toXmlDocument(), path); return path; } @@ -81,8 +84,8 @@ public static String storeQuery(String query, String fileName) throws URISyntaxE * @param backend the name of the backend to check * @return true if the backend supports ignored inputs and outputs, else false */ - public static Boolean backendSupportsInputOutputs(BackendHelper.BackendNames backend) { - return backend == BackendHelper.BackendNames.Reveaal; + public static Boolean backendSupportsInputOutputs(BackendInstance backend) { + return true; } /** @@ -101,7 +104,7 @@ public static String getTempDirectoryAbsolutePath() throws URISyntaxException { * @throws BackendException if the document could not be built */ public static void buildEcdarDocument() throws BackendException { - ecdarDocument = new EcdarDocument(); + BackendHelper.ecdarDocument = new EcdarDocument(); } /** @@ -141,14 +144,57 @@ public static String getExistDeadlockQuery(final Component component) { } /** - * Enum for the available backends. Used for saving and loading the queries. + * Returns the BackendInstance with the specified name, or null, if no such BackendInstance exists + * + * @param backendInstanceName Name of the BackendInstance to return + * @return The BackendInstance with matching name + * or the default backend instance, if no matching backendInstance exists */ - public enum BackendNames { - jEcdar, Reveaal; + public static BackendInstance getBackendInstanceByName(String backendInstanceName) { + Optional backendInstance = BackendHelper.backendInstances.stream().filter(bi -> bi.getName().equals(backendInstanceName)).findFirst(); + return backendInstance.orElse(BackendHelper.getDefaultBackendInstance()); + } - @Override - public String toString() { - return this.ordinal() == 0 ? "jEcdar" : "Reveaal"; + /** + * Returns the default BackendInstance + * + * @return The default BackendInstance + */ + public static BackendInstance getDefaultBackendInstance() { + return defaultBackend; + } + + /** + * Sets the list of BackendInstances to match the provided list + * + * @param updatedBackendInstances The list of BackendInstances that should be stored + */ + public static void updateBackendInstances(ArrayList updatedBackendInstances) { + BackendHelper.backendInstances = FXCollections.observableList(updatedBackendInstances); + for (Runnable runnable : BackendHelper.backendInstancesUpdatedListeners) { + runnable.run(); } } + + /** + * Returns the ObservableList of BackendInstances + * + * @return The ObservableList of BackendInstances + */ + public static ObservableList getBackendInstances() { + return BackendHelper.backendInstances; + } + + /** + * Sets the default BackendInstance to the provided object + * + * @param newDefaultBackend The new defaultBackend + */ + public static void setDefaultBackendInstance(BackendInstance newDefaultBackend) { + BackendHelper.defaultBackend = newDefaultBackend; + } + + public static void addBackendInstanceListener(Runnable runnable) { + BackendHelper.backendInstancesUpdatedListeners.add(runnable); + } } diff --git a/src/main/java/ecdar/backend/BackendThread.java b/src/main/java/ecdar/backend/BackendThread.java deleted file mode 100644 index c39eb776..00000000 --- a/src/main/java/ecdar/backend/BackendThread.java +++ /dev/null @@ -1,36 +0,0 @@ -package ecdar.backend; - -import ecdar.abstractions.QueryState; - -import java.util.concurrent.atomic.AtomicBoolean; -import java.util.function.Consumer; - -public abstract class BackendThread extends Thread { - public AtomicBoolean hasBeenCanceled = new AtomicBoolean(); - final String query; - final Consumer success; - final Consumer failure; - final QueryListener queryListener; - - public BackendThread(final String query, - final Consumer success, - final Consumer failure, - final QueryListener queryListener) { - this.query = query; - this.success = success; - this.failure = failure; - this.queryListener = queryListener; - } - - void handleResult(QueryState result, String line) { - if (result.getStatusCode() == QueryState.SUCCESSFUL.getStatusCode()) { - success.accept(true); - } else if (result.getStatusCode() == QueryState.ERROR.getStatusCode()){ - success.accept(false); - } else if (result.getStatusCode() == QueryState.SYNTAX_ERROR.getStatusCode()) { - failure.accept(new BackendException.QueryErrorException(line)); - } else { - failure.accept(new BackendException.BadBackendQueryException(line)); - } - } -} diff --git a/src/main/java/ecdar/backend/jEcdarThread.java b/src/main/java/ecdar/backend/jEcdarThread.java deleted file mode 100644 index e064ffe6..00000000 --- a/src/main/java/ecdar/backend/jEcdarThread.java +++ /dev/null @@ -1,63 +0,0 @@ -package ecdar.backend; - -import ecdar.Ecdar; -import ecdar.abstractions.QueryState; - -import java.io.*; -import java.util.function.Consumer; - -public class jEcdarThread extends BackendThread { - public jEcdarThread(final String query, - final Consumer success, - final Consumer failure, - final QueryListener queryListener) { - super(query, success, failure, queryListener); - } - - public void run() { - ProcessBuilder pb = new ProcessBuilder("java", "-jar", "src/libs/j-Ecdar.jar"); - pb.redirectErrorStream(true); - try { - //Start the j-Ecdar process - Process jEcdarEngineInstance = pb.start(); - - //Communicate with the j-Ecdar process - try ( - var jEcdarReader = new BufferedReader(new InputStreamReader(jEcdarEngineInstance.getInputStream())); - var jEcdarWriter = new BufferedWriter(new OutputStreamWriter(jEcdarEngineInstance.getOutputStream())); - ) { - //Run the query with the j-Ecdar process - jEcdarWriter.write("-rq -json " + Ecdar.projectDirectory.get() + " " + query.replaceAll("\\s", "") + "\n"); // Newline added to signal EOI - jEcdarWriter.flush(); - - //Read the result of the query from the j-Ecdar process - String line; - QueryState result = QueryState.RUNNING; - while ((line = jEcdarReader.readLine()) != null) { - if (hasBeenCanceled.get()) { - cancel(jEcdarEngineInstance); - return; - } - - // Process the query result - if ((line.equals("true") || line.equals("")) && (result.getStatusCode() <= QueryState.SUCCESSFUL.getStatusCode())) { - result = QueryState.SUCCESSFUL; - } else if (line.equals("false") && (result.getStatusCode() <= QueryState.ERROR.getStatusCode())){ - result = QueryState.ERROR; - } else if (result.getStatusCode() <= QueryState.SYNTAX_ERROR.getStatusCode()) { - result = QueryState.SYNTAX_ERROR; - } - - handleResult(result, line); - } - } - } catch (IOException e) { - e.printStackTrace(); - } - } - - private void cancel(Process jEcdarEngineInstance) { - jEcdarEngineInstance.destroy(); - failure.accept(new BackendException.QueryErrorException("Canceled")); - } -} diff --git a/src/main/java/ecdar/controllers/BackendInstanceController.java b/src/main/java/ecdar/controllers/BackendInstanceController.java new file mode 100644 index 00000000..7ff90b3d --- /dev/null +++ b/src/main/java/ecdar/controllers/BackendInstanceController.java @@ -0,0 +1,172 @@ +package ecdar.controllers; + +import com.jfoenix.controls.JFXCheckBox; +import com.jfoenix.controls.JFXRippler; +import com.jfoenix.controls.JFXTextField; +import ecdar.abstractions.BackendInstance; +import javafx.application.Platform; +import javafx.beans.property.SimpleBooleanProperty; +import javafx.fxml.FXML; +import javafx.fxml.Initializable; +import javafx.scene.Cursor; +import javafx.scene.control.Label; +import javafx.scene.control.RadioButton; +import javafx.scene.layout.HBox; +import javafx.scene.layout.Priority; +import javafx.scene.layout.StackPane; +import javafx.scene.paint.Color; +import javafx.stage.DirectoryChooser; +import javafx.stage.FileChooser; +import org.kordamp.ikonli.javafx.FontIcon; + +import java.io.File; +import java.net.URL; +import java.util.ResourceBundle; + +public class BackendInstanceController implements Initializable { + private BackendInstance backendInstance = new BackendInstance(); + + public JFXTextField backendName; + public Label backendNameIssue; + public FontIcon expansionIcon; + public JFXRippler removeBackendRippler; + public FontIcon removeBackendIcon; + public StackPane content; + public JFXCheckBox isLocal; + public HBox addressSection; + public JFXTextField address; + public HBox pathToBackendSection; + public JFXRippler pickPathToBackend; + public JFXTextField pathToBackend; + public Label locationIssue; + public JFXTextField portRangeStart; + public Label portRangeStartIssue; + public JFXTextField portRangeEnd; + public Label portRangeEndIssue; + public Label portRangeIssue; + public StackPane moveBackendInstanceUpRippler; + public StackPane moveBackendInstanceDownRippler; + public RadioButton defaultBackendRadioButton; + + @Override + public void initialize(URL location, ResourceBundle resources) { + Platform.runLater(() -> { + this.handleLocalPropertyChanged(); + moveBackendInstanceUpRippler.setCursor(Cursor.HAND); + moveBackendInstanceDownRippler.setCursor(Cursor.HAND); + setHGrow(); + + // Prevent deletion of default backend instance + defaultBackendRadioButton.selectedProperty().addListener((observable, oldValue, newValue) -> { + if (newValue) { + removeBackendIcon.setFill(Color.GREY); + } else { + removeBackendIcon.setFill(Color.BLACK); + } + }); + + if (defaultBackendRadioButton.isSelected()) removeBackendIcon.setFill(Color.GREY); + }); + } + + /*** + * Sets the BackendInstance object and overrides the current settings shown in the GUI + * @param instance the new BackendInstance + */ + public void setBackendInstance(BackendInstance instance) { + this.backendInstance = instance; + + this.backendName.setText(instance.getName()); + this.isLocal.setSelected(instance.isLocal()); + this.defaultBackendRadioButton.setSelected(instance.isDefault()); + + // Check if the path or the address should be used + if (isLocal.isSelected()) { + this.pathToBackend.setText(instance.getBackendLocation()); + } else { + this.address.setText(instance.getBackendLocation()); + } + + this.portRangeStart.setText(String.valueOf(instance.getPortStart())); + this.portRangeEnd.setText(String.valueOf(instance.getPortEnd())); + } + + public BackendInstance updateBackendInstance() { + backendInstance.setName(backendName.getText()); + backendInstance.setLocal(isLocal.isSelected()); + backendInstance.setDefault(defaultBackendRadioButton.isSelected()); + backendInstance.setBackendLocation(isLocal.isSelected() ? pathToBackend.getText() : address.getText()); + backendInstance.setPortStart(Integer.parseInt(portRangeStart.getText())); + backendInstance.setPortEnd(Integer.parseInt(portRangeEnd.getText())); + + return backendInstance; + } + + private void setHGrow() { + HBox.setHgrow(backendName.getParent().getParent().getParent(), Priority.ALWAYS); + HBox.setHgrow(backendName.getParent(), Priority.ALWAYS); + HBox.setHgrow(backendName, Priority.ALWAYS); + HBox.setHgrow(content, Priority.ALWAYS); + HBox.setHgrow(addressSection, Priority.ALWAYS); + HBox.setHgrow(address, Priority.ALWAYS); + HBox.setHgrow(pathToBackendSection, Priority.ALWAYS); + HBox.setHgrow(pathToBackend, Priority.ALWAYS); + HBox.setHgrow(portRangeStart, Priority.ALWAYS); + HBox.setHgrow(portRangeEnd, Priority.ALWAYS); + } + + private void handleLocalPropertyChanged() { + if (isLocal.isSelected()) { + address.setDisable(true); + addressSection.setVisible(false); + addressSection.setManaged(false); + pathToBackendSection.setVisible(true); + pathToBackendSection.setManaged(true); + } else { + address.setDisable(false); + addressSection.setVisible(true); + addressSection.setManaged(true); + pathToBackendSection.setVisible(false); + pathToBackendSection.setManaged(false); + } + } + + @FXML + private void addressLocalClicked(){ + handleLocalPropertyChanged(); + } + + @FXML + private void expansionClicked() { + if (expansionIcon.getIconLiteral().equals("gmi-expand-less")) { + expansionIcon.setIconLiteral("gmi-expand-more"); + content.setVisible(false); + content.setManaged(false); + } else { + expansionIcon.setIconLiteral("gmi-expand-less"); + content.setVisible(true); + content.setManaged(true); + } + } + + @FXML + private void openPathToBackendDialog() { + // Dialog title + final FileChooser backendPicker = new FileChooser(); + backendPicker.setTitle("Choose backend"); + + // The initial location for the file choosing dialog + final File jarDir = new File(pathToBackend.getText()).getAbsoluteFile().getParentFile(); + + // If the file does not exist, we must be running it from a development environment, use a default location + if(jarDir.exists()) { + backendPicker.setInitialDirectory(jarDir); + } + + // Prompt the user to find a file (will halt the UI thread) + final File file = backendPicker.showOpenDialog(null); + if(file != null) { + pathToBackend.setText(file.getAbsolutePath()); + } + } +} diff --git a/src/main/java/ecdar/controllers/BackendOptionsDialogController.java b/src/main/java/ecdar/controllers/BackendOptionsDialogController.java new file mode 100644 index 00000000..128ab632 --- /dev/null +++ b/src/main/java/ecdar/controllers/BackendOptionsDialogController.java @@ -0,0 +1,417 @@ +package ecdar.controllers; + +import com.google.gson.JsonArray; +import com.google.gson.JsonParser; +import com.jfoenix.controls.JFXButton; +import com.jfoenix.controls.JFXRippler; +import ecdar.Ecdar; +import ecdar.abstractions.BackendInstance; +import ecdar.backend.BackendHelper; +import ecdar.presentations.BackendInstancePresentation; +import javafx.fxml.Initializable; +import javafx.scene.Node; +import javafx.scene.control.ToggleGroup; +import javafx.scene.layout.HBox; +import javafx.scene.layout.Priority; +import javafx.scene.layout.VBox; +import org.apache.commons.lang3.Range; + +import java.io.File; +import java.io.IOException; +import java.net.InetAddress; +import java.net.URL; +import java.net.UnknownHostException; +import java.nio.file.Files; +import java.nio.file.Path; +import java.nio.file.Paths; +import java.util.ArrayList; +import java.util.List; +import java.util.ResourceBundle; +import java.util.stream.Collectors; + +public class BackendOptionsDialogController implements Initializable { + public VBox backendInstanceList; + public JFXRippler addBackendButton; + public JFXButton closeButton; + public ToggleGroup defaultBackendToggleGroup = new ToggleGroup(); + public JFXButton saveButton; + public JFXButton resetBackendsButton; + + @Override + public void initialize(URL location, ResourceBundle resources) { + initializeBackendInstanceList(); + } + + /** + * Reverts any changes made to the backend options by reloading the options specified in the preference file, + * or to the default, if no backends are present in the preferences file + */ + public void cancelBackendOptionsChanges() { + initializeBackendInstanceList(); + } + + /** + * Saves the changes made to the backend options to the preferences file and returns true + * if no errors where found in the backend instance definitions, otherwise false + * + * @return whether the changes could be saved, + * meaning that no errors where found in the changes made to the backend options + */ + public boolean saveChangesToBackendOptions() { + if (this.backendInstanceListIsErrorFree()) { + ArrayList backendInstances = new ArrayList<>(); + for (Node backendInstance : backendInstanceList.getChildren()) { + if (backendInstance instanceof BackendInstancePresentation) { + backendInstances.add(((BackendInstancePresentation) backendInstance).getController().updateBackendInstance()); + } + } + + BackendHelper.updateBackendInstances(backendInstances); + + JsonArray jsonArray = new JsonArray(); + for (BackendInstance bi : backendInstances) { + jsonArray.add(bi.serialize()); + } + + Ecdar.preferences.put("backend_instances", jsonArray.toString()); + + BackendInstance defaultBackend = backendInstances.stream().filter(BackendInstance::isDefault).findFirst().orElse(backendInstances.get(0)); + BackendHelper.setDefaultBackendInstance(defaultBackend); + + String defaultBackendName = (defaultBackend.getName()); + Ecdar.preferences.put("default_backend", defaultBackendName); + + return true; + } else { + return false; + } + } + + /** + * Resets the backends to the default backends present in the 'default_backends.json' file + */ + public void resetBackendsToDefault() { + updateBackendsInGUI(getDefaultBackends()); + } + + private void initializeBackendInstanceList() { + ArrayList backends; + + // Load backends from preferences or get default + var savedBackends = Ecdar.preferences.get("backend_instances", null); + if (savedBackends != null) { + backends = getBackendsFromJsonArray( + JsonParser.parseString(savedBackends).getAsJsonArray()); + } else { + backends = getDefaultBackends(); + } + + // Style add backend button and handle click event + HBox.setHgrow(addBackendButton, Priority.ALWAYS); + addBackendButton.setMaxWidth(Double.MAX_VALUE); + addBackendButton.setOnMouseClicked((event) -> { + BackendInstancePresentation newBackendInstancePresentation = new BackendInstancePresentation(); + addBackendInstancePresentationToList(newBackendInstancePresentation); + }); + + updateBackendsInGUI(backends); + } + + private void updateBackendsInGUI(ArrayList backends) { + backendInstanceList.getChildren().clear(); + + backends.forEach((bi) -> { + BackendInstancePresentation newBackendInstancePresentation = new BackendInstancePresentation(bi); + newBackendInstancePresentation.getController().backendName.disableProperty().bind(bi.getLockedProperty()); + newBackendInstancePresentation.getController().pathToBackend.disableProperty().bind(bi.getLockedProperty()); + addBackendInstancePresentationToList(newBackendInstancePresentation); + }); + + BackendHelper.updateBackendInstances(backends); + } + + private ArrayList getBackendsFromJsonArray(JsonArray backends) { + ArrayList backendInstances = new ArrayList<>(); + backendInstanceList.getChildren().clear(); + backends.forEach((backend) -> { + BackendInstance newBackendInstance = new BackendInstance(backend.getAsJsonObject()); + backendInstances.add(newBackendInstance); + }); + + return backendInstances; + } + + private ArrayList getDefaultBackends() { + ArrayList defaultBackends = new ArrayList<>(); + + // Add Reveaal engine + var reveaal = new BackendInstance(); + reveaal.setName("Reveaal"); + reveaal.setLocal(true); + reveaal.setDefault(true); + reveaal.setPortStart(5032); + reveaal.setPortEnd(5040); + reveaal.lockInstance(); + + List searchPathForReveaal = List.of( + new File("lib/Reveaal.exe"), new File("lib/Reveaal") + ); + getBackendPathIfFileExists(reveaal, searchPathForReveaal); + defaultBackends.add(reveaal); + + // Add jECDAR engine + var jEcdar = new BackendInstance(); + jEcdar.setName("jECDAR"); + jEcdar.setLocal(true); + jEcdar.setDefault(false); + jEcdar.setPortStart(5042); + jEcdar.setPortEnd(5050); + jEcdar.lockInstance(); + + List searchPathForJEcdar = List.of( + new File("lib/j-Ecdar.exe"), new File("lib/j-Ecdar.bat") + ); + getBackendPathIfFileExists(jEcdar, searchPathForJEcdar); + defaultBackends.add(jEcdar); + + return defaultBackends; + } + + private void getBackendPathIfFileExists(BackendInstance engine, List searchPathForFile) { + engine.setBackendLocation(""); + + for (var f : searchPathForFile) { + if (f.exists()) { + engine.setBackendLocation(f.getAbsolutePath()); + break; + } + } + + if (engine.getBackendLocation().equals("")) { + throw new RuntimeException("Could not locate file for default engine, checked: " + searchPathForFile.stream().map(File::getPath).collect(Collectors.joining(", "))); + } + } + + private void addBackendInstancePresentationToList(BackendInstancePresentation newBackendInstancePresentation) { + backendInstanceList.getChildren().add(newBackendInstancePresentation); + newBackendInstancePresentation.getController().moveBackendInstanceUpRippler.setOnMouseClicked((mouseEvent) -> moveBackendInstance(newBackendInstancePresentation, -1)); + newBackendInstancePresentation.getController().moveBackendInstanceDownRippler.setOnMouseClicked((mouseEvent) -> moveBackendInstance(newBackendInstancePresentation, +1)); + newBackendInstancePresentation.getController().removeBackendRippler.setOnMouseClicked((mouseEvent) -> { + if (!newBackendInstancePresentation.getController().defaultBackendRadioButton.isSelected()) { + backendInstanceList.getChildren().remove(newBackendInstancePresentation); + } + }); + newBackendInstancePresentation.getController().defaultBackendRadioButton.setToggleGroup(defaultBackendToggleGroup); + } + + private void moveBackendInstance(BackendInstancePresentation newBackendInstance, int i) { + int currentIndex = backendInstanceList.getChildren().indexOf(newBackendInstance); + int newIndex = (currentIndex + i) % backendInstanceList.getChildren().size(); + if (newIndex < 0) { + newIndex = backendInstanceList.getChildren().size() - 1; + } + + backendInstanceList.getChildren().remove(newBackendInstance); + backendInstanceList.getChildren().add(newIndex, newBackendInstance); + } + + /** + * Marks input fields in the backendInstanceList that contains errors and returns whether any errors were found + * + * @return whether any errors were found + */ + private boolean backendInstanceListIsErrorFree() { + boolean error = true; + + for (Node child : backendInstanceList.getChildren()) { + if (child instanceof BackendInstancePresentation) { + BackendInstanceController backendInstanceController = ((BackendInstancePresentation) child).getController(); + error = backendNameIsErrorFree(backendInstanceController) && error; + error = portRangeIsErrorFree(backendInstanceController) && error; + error = backendInstanceLocationIsErrorFree(backendInstanceController) && error; + } + } + + return error; + } + + private boolean backendNameIsErrorFree(BackendInstanceController backendInstanceController) { + String backendName = backendInstanceController.backendName.getText(); + + if (backendName.isBlank()) { + backendInstanceController.backendNameIssue.setText(ValidationErrorMessages.BACKEND_NAME_EMPTY.toString()); + backendInstanceController.backendNameIssue.setVisible(true); + return false; + } + + backendInstanceController.backendNameIssue.setVisible(false); + return true; + } + + private boolean portRangeIsErrorFree(BackendInstanceController backendInstanceController) { + boolean errorFree = true; + int portRangeStart = 0, portRangeEnd = 0; + backendInstanceController.portRangeStartIssue.setText(""); + backendInstanceController.portRangeStartIssue.setVisible(false); + backendInstanceController.portRangeEndIssue.setText(""); + backendInstanceController.portRangeEndIssue.setVisible(false); + backendInstanceController.portRangeIssue.setVisible(false); + + try { + portRangeStart = Integer.parseInt(backendInstanceController.portRangeStart.getText()); + } catch (NumberFormatException numberFormatException) { + backendInstanceController.portRangeStartIssue.setText(ValidationErrorMessages.VALUE_NOT_INTEGER.toString()); + errorFree = false; + } + + try { + portRangeEnd = Integer.parseInt(backendInstanceController.portRangeEnd.getText()); + } catch (NumberFormatException numberFormatException) { + backendInstanceController.portRangeEndIssue.setText(ValidationErrorMessages.VALUE_NOT_INTEGER.toString()); + errorFree = false; + } + + Range portRange = Range.between(0, 65535); + + if (!portRange.contains(portRangeStart)) { + if (backendInstanceController.portRangeStartIssue.getText().isBlank()) { + backendInstanceController.portRangeStartIssue.setText(ValidationErrorMessages.PORT_VALUE_NOT_WITHIN_ACCEPTABLE_RANGE.toString()); + } else { + backendInstanceController.portRangeStartIssue.setText(ValidationErrorMessages.PORT_VALUE_NOT_WITHIN_ACCEPTABLE_RANGE_CONCATINATION.toString()); + } + errorFree = false; + } + if (!portRange.contains(portRangeEnd)) { + if (backendInstanceController.portRangeEndIssue.getText().isBlank()) { + backendInstanceController.portRangeEndIssue.setText(ValidationErrorMessages.PORT_VALUE_NOT_WITHIN_ACCEPTABLE_RANGE.toString()); + } else { + backendInstanceController.portRangeEndIssue.setText(ValidationErrorMessages.PORT_VALUE_NOT_WITHIN_ACCEPTABLE_RANGE_CONCATINATION.toString()); + } + errorFree = false; + } + + if (portRangeEnd - portRangeStart < 0) { + backendInstanceController.portRangeIssue.setText(ValidationErrorMessages.PORT_RANGE_MUST_BE_INCREMENTAL.toString()); + errorFree = false; + } + + backendInstanceController.portRangeStartIssue.setVisible(!errorFree); + backendInstanceController.portRangeEndIssue.setVisible(!errorFree); + backendInstanceController.portRangeIssue.setVisible(!errorFree); + + return errorFree; + } + + private boolean backendInstanceLocationIsErrorFree(BackendInstanceController backendInstanceController) { + boolean errorFree = true; + + if (backendInstanceController.isLocal.isSelected()) { + if (backendInstanceController.pathToBackend.getText().isBlank()) { + backendInstanceController.locationIssue.setText(ValidationErrorMessages.FILE_LOCATION_IS_BLANK.toString()); + errorFree = false; + } else { + Path localBackendPath = Paths.get(backendInstanceController.pathToBackend.getText()); + + if (!Files.isExecutable(localBackendPath)) { + backendInstanceController.locationIssue.setText(ValidationErrorMessages.FILE_DOES_NOT_EXIST_OR_NOT_EXECUTABLE.toString()); + errorFree = false; + } + } + } else { + if (backendInstanceController.address.getText().isBlank()) { + backendInstanceController.locationIssue.setText(ValidationErrorMessages.HOST_ADDRESS_IS_BLANK.toString()); + errorFree = false; + } else { + try { + InetAddress address = InetAddress.getByName(backendInstanceController.address.getText()); + boolean reachable = address.isReachable(200); + + if (!reachable) { + backendInstanceController.locationIssue.setText(ValidationErrorMessages.HOST_NOT_REACHABLE.toString()); + errorFree = false; + } + + } catch (UnknownHostException unknownHostException) { + backendInstanceController.locationIssue.setText(ValidationErrorMessages.UNACCEPTABLE_HOST_NAME.toString()); + errorFree = false; + } catch (IOException ioException) { + backendInstanceController.locationIssue.setText(ValidationErrorMessages.IO_EXCEPTION_WITH_HOST.toString()); + errorFree = false; + } + } + } + + backendInstanceController.locationIssue.setVisible(!errorFree); + + return errorFree; + } + + private enum ValidationErrorMessages { + BACKEND_NAME_EMPTY { + @Override + public String toString() { + return "The backend name cannot be empty"; + } + }, + VALUE_NOT_INTEGER { + @Override + public String toString() { + return "Value must be integer"; + } + }, + PORT_RANGE_MUST_BE_INCREMENTAL { + @Override + public String toString() { + return "Start of port range must be greater than end"; + } + }, + PORT_VALUE_NOT_WITHIN_ACCEPTABLE_RANGE { + @Override + public String toString() { + return "Value must be within range 0 - 65535"; + } + }, + PORT_VALUE_NOT_WITHIN_ACCEPTABLE_RANGE_CONCATINATION { + @Override + public String toString() { + return " and within range 0 - 65535"; + } + }, + FILE_LOCATION_IS_BLANK { + @Override + public String toString() { + return "Please specify a file for this backend"; + } + }, + FILE_DOES_NOT_EXIST_OR_NOT_EXECUTABLE { + @Override + public String toString() { + return "The above file does not exists or ECDAR does not have the privileges to execute it"; + } + }, + HOST_ADDRESS_IS_BLANK { + @Override + public String toString() { + return "Please specify an address for the external host"; + } + }, + HOST_NOT_REACHABLE { + @Override + public String toString() { + return "The above address is not reachable. Make sure that the host is correct"; + } + }, + UNACCEPTABLE_HOST_NAME { + @Override + public String toString() { + return "The above address is not an acceptable host name"; + } + }, + IO_EXCEPTION_WITH_HOST { + @Override + public String toString() { + return "An I/O exception was encountered while trying to reach the host"; + } + } + } +} diff --git a/src/main/java/ecdar/controllers/EcdarController.java b/src/main/java/ecdar/controllers/EcdarController.java index 6c350df4..ce529955 100644 --- a/src/main/java/ecdar/controllers/EcdarController.java +++ b/src/main/java/ecdar/controllers/EcdarController.java @@ -155,10 +155,7 @@ protected void interpolate(final double frac) { public MenuItem menuBarFileExportAsPng; public MenuItem menuBarFileExportAsPngNoBorder; public MenuItem menuBarOptionsCache; - public MenuItem menuBarOptionsDefaultBackend; - public HBox menuBarOptionsDefaultBackendContent; - public Tooltip menuBarOptionsDefaultBackendTooltip; - public JFXSlider menuBarOptionsNumberOfSocketsSlider; + public MenuItem menuBarOptionsBackendOptions; public MenuItem menuBarHelpHelp; public MenuItem menuBarHelpAbout; public MenuItem menuBarHelpTest; @@ -174,6 +171,9 @@ protected void interpolate(final double frac) { public Text queryTextResult; public Text queryTextQuery; + public StackPane backendOptionsDialogContainer; + public BackendOptionsDialogPresentation backendOptionsDialog; + private static JFXDialog _queryDialog; private static Text _queryTextResult; private static Text _queryTextQuery; @@ -195,6 +195,18 @@ public static EdgeStatus getGlobalEdgeStatus() { @Override public void initialize(final URL location, final ResourceBundle resources) { + initilizeDialogs(); + initializeCanvasPane(); + initializeEdgeStatusHandling(); + initializeKeybindings(); + initializeTabPane(); + initializeStatusBar(); + initializeMessages(); + initializeMenuBar(); + initializeReachabilityAnalysisThread(); + } + + private void initilizeDialogs() { dialog.setDialogContainer(dialogContainer); dialogContainer.opacityProperty().bind(dialog.getChildren().get(0).scaleXProperty()); dialog.setOnDialogClosed(event -> dialogContainer.setVisible(false)); @@ -202,15 +214,43 @@ public void initialize(final URL location, final ResourceBundle resources) { _queryDialog = queryDialog; _queryTextResult = queryTextResult; _queryTextQuery = queryTextQuery; - queryDialog.setDialogContainer(queryDialogContainer); - queryDialogContainer.opacityProperty().bind(queryDialog.getChildren().get(0).scaleXProperty()); - queryDialog.setOnDialogClosed(event -> { - queryDialogContainer.setVisible(false); - queryDialogContainer.setMouseTransparent(true); + + initializeDialog(queryDialog, queryDialogContainer); + initializeDialog(backendOptionsDialog, backendOptionsDialogContainer); + + backendOptionsDialog.getController().resetBackendsButton.setOnMouseClicked(event -> { + backendOptionsDialog.getController().resetBackendsToDefault(); }); - queryDialog.setOnDialogOpened(event -> { - queryDialogContainer.setVisible(true); - queryDialogContainer.setMouseTransparent(false); + + backendOptionsDialog.getController().closeButton.setOnMouseClicked(event -> { + backendOptionsDialog.getController().cancelBackendOptionsChanges(); + dialog.close(); + backendOptionsDialog.close(); + }); + + backendOptionsDialog.getController().saveButton.setOnMouseClicked(event -> { + if (backendOptionsDialog.getController().saveChangesToBackendOptions()) { + dialog.close(); + backendOptionsDialog.close(); + } + }); + + // Set default backend instance + BackendInstance defaultBackend = BackendHelper.getBackendInstances().stream().filter(BackendInstance::isDefault).findFirst().orElse(BackendHelper.getBackendInstances().get(0)); + BackendHelper.setDefaultBackendInstance(defaultBackend); + } + + private void initializeDialog(JFXDialog dialog, StackPane dialogContainer) { + dialog.setDialogContainer(dialogContainer); + dialogContainer.opacityProperty().bind(dialog.getChildren().get(0).scaleXProperty()); + dialogContainer.opacityProperty().bind(dialog.getChildren().get(0).scaleXProperty()); + dialog.setOnDialogClosed(event -> { + dialogContainer.setVisible(false); + dialogContainer.setMouseTransparent(true); + }); + dialog.setOnDialogOpened(event -> { + dialogContainer.setVisible(true); + dialogContainer.setMouseTransparent(false); }); initializeCanvasPane(); @@ -394,7 +434,7 @@ private void initializeReachabilityAnalysisThread() { reachabilityQuery.setType(QueryType.REACHABILITY); Ecdar.getBackendDriver().addQueryToExecutionQueue(locationReachableQuery, - BackendHelper.BackendNames.Reveaal, + BackendHelper.getDefaultBackendInstance(), (result -> { if (result) { location.setReachability(Location.Reachability.REACHABLE); @@ -410,7 +450,7 @@ private void initializeReachabilityAnalysisThread() { new QueryListener(reachabilityQuery)); final Thread verifyThread = new Thread(() -> Ecdar.getBackendDriver().addQueryToExecutionQueue(locationReachableQuery, - BackendHelper.BackendNames.Reveaal, + BackendHelper.getDefaultBackendInstance(), (result -> { if (result) { location.setReachability(Location.Reachability.REACHABLE); @@ -529,37 +569,11 @@ private void initializeOptionsMenu() { menuBarOptionsCache.getGraphic().opacityProperty().bind(new When(isCached).then(1).otherwise(0)); }); - menuBarOptionsDefaultBackendTooltip = new Tooltip("Change default backend to " + - (BackendHelper.defaultBackend.equals(BackendHelper.BackendNames.jEcdar) - ? BackendHelper.BackendNames.Reveaal.name() - : BackendHelper.BackendNames.jEcdar.name())); - - Tooltip.install(menuBarOptionsDefaultBackendContent, menuBarOptionsDefaultBackendTooltip); - - menuBarOptionsDefaultBackend.setOnAction(event -> { - menuBarOptionsDefaultBackendTooltip.setText("Change default backend to " + BackendHelper.defaultBackend.name()); - BackendHelper.defaultBackend = (BackendHelper.defaultBackend.equals(BackendHelper.BackendNames.jEcdar) - ? BackendHelper.BackendNames.Reveaal - : BackendHelper.BackendNames.jEcdar); - - Ecdar.showToast("The default backend was changed to " + BackendHelper.defaultBackend.name()); - ((Text) menuBarOptionsDefaultBackendContent.getChildrenUnmodifiable().get(1)).setText("Default backend: " + BackendHelper.defaultBackend.name()); - - Ecdar.preferences.put("default_backend", Integer.toString(BackendHelper.defaultBackend.ordinal())); - - }); - - ((Text) menuBarOptionsDefaultBackendContent.getChildrenUnmodifiable().get(1)).setText("Default backend: " + BackendHelper.defaultBackend.name()); - - menuBarOptionsNumberOfSocketsSlider.valueChangingProperty().addListener((observable, oldValue, newValue) -> { - if (oldValue && !newValue) { - int newIntValue = (int) Math.round(menuBarOptionsNumberOfSocketsSlider.getValue()); - Ecdar.getBackendDriver().setMaxNumberOfConnections(newIntValue); - Ecdar.preferences.put("number_of_backend_sockets", Integer.toString(newIntValue)); - } + menuBarOptionsBackendOptions.setOnAction(event -> { + backendOptionsDialogContainer.setVisible(true); + backendOptionsDialog.show(backendOptionsDialogContainer); + backendOptionsDialog.setMouseTransparent(false); }); - - menuBarOptionsNumberOfSocketsSlider.setValue(Ecdar.getBackendDriver().getMaxNumberOfSockets()); } private void initializeEditMenu() { @@ -672,7 +686,7 @@ private void initializeOpenProjectMenuItem() { // The initial location for the file choosing dialog final File jarDir = new File(System.getProperty("java.class.path")).getAbsoluteFile().getParentFile(); - // If the file does not exist, we must be running it from a development environment, use an default location + // If the file does not exist, we must be running it from a development environment, use default location if (jarDir.exists()) { projectPicker.setInitialDirectory(jarDir); } @@ -1451,7 +1465,7 @@ private void setGlobalEdgeStatus(EdgeStatus status) { } @FXML - private void closeDialog() { + private void closeQueryDialog() { dialog.close(); queryDialog.close(); } diff --git a/src/main/java/ecdar/controllers/QueryController.java b/src/main/java/ecdar/controllers/QueryController.java index c357bbd1..114f867a 100644 --- a/src/main/java/ecdar/controllers/QueryController.java +++ b/src/main/java/ecdar/controllers/QueryController.java @@ -1,8 +1,11 @@ package ecdar.controllers; +import com.jfoenix.controls.JFXComboBox; import com.jfoenix.controls.JFXRippler; +import ecdar.abstractions.BackendInstance; import ecdar.abstractions.Query; import ecdar.abstractions.QueryType; +import ecdar.backend.BackendHelper; import ecdar.utility.colors.Color; import javafx.application.Platform; import javafx.beans.property.SimpleBooleanProperty; @@ -20,9 +23,10 @@ public class QueryController implements Initializable { public JFXRippler actionButton; public JFXRippler queryTypeExpand; public Text queryTypeSymbol; + public JFXComboBox backendsDropdown; private Query query; private final Map queryTypeListElementsSelectedState = new HashMap<>(); - private final Tooltip noQueryTypeSatTooltip = new Tooltip("Please select a query type beneath the status icon"); + private final Tooltip noQueryTypeSetTooltip = new Tooltip("Please select a query type beneath the status icon"); @Override public void initialize(URL location, ResourceBundle resources) { @@ -36,16 +40,25 @@ public void setQuery(Query query) { actionButton.setDisable(false); ((FontIcon) actionButton.lookup("#actionButtonIcon")).setIconColor(Color.GREY.getColor(Color.Intensity.I900)); Platform.runLater(() -> { - Tooltip.uninstall(actionButton.getParent(), noQueryTypeSatTooltip); + Tooltip.uninstall(actionButton.getParent(), noQueryTypeSetTooltip); }); } else { actionButton.setDisable(true); ((FontIcon) actionButton.lookup("#actionButtonIcon")).setIconColor(Color.GREY.getColor(Color.Intensity.I500)); Platform.runLater(() -> { - Tooltip.install(actionButton.getParent(), noQueryTypeSatTooltip); + Tooltip.install(actionButton.getParent(), noQueryTypeSetTooltip); }); } })); + + backendsDropdown.setValue(query.getBackend()); + backendsDropdown.valueProperty().addListener((observable, oldValue, newValue) -> { + if (newValue != null) { + query.setBackend(newValue); + } else { + backendsDropdown.setValue(BackendHelper.getDefaultBackendInstance()); + } + }); } public Query getQuery() { @@ -57,7 +70,7 @@ private void initializeActionButton() { if (query.getType() == null) { actionButton.setDisable(true); ((FontIcon) actionButton.lookup("#actionButtonIcon")).setIconColor(Color.GREY.getColor(Color.Intensity.I500)); - Tooltip.install(actionButton.getParent(), noQueryTypeSatTooltip); + Tooltip.install(actionButton.getParent(), noQueryTypeSetTooltip); } }); } diff --git a/src/main/java/ecdar/mutation/MutationTestPlanController.java b/src/main/java/ecdar/mutation/MutationTestPlanController.java index 485f5a84..b98a5b82 100644 --- a/src/main/java/ecdar/mutation/MutationTestPlanController.java +++ b/src/main/java/ecdar/mutation/MutationTestPlanController.java @@ -211,7 +211,7 @@ public void onSelectSutButtonPressed() { jarDir = new File(Ecdar.projectDirectory.get()); - // If the file does not exist, we must be running it from a development environment, use an default location + // If the file does not exist, we must be running it from a development environment, use a default location if (jarDir.exists()) { fileChooser.setInitialDirectory(jarDir); } diff --git a/src/main/java/ecdar/presentations/BackendInstancePresentation.java b/src/main/java/ecdar/presentations/BackendInstancePresentation.java new file mode 100644 index 00000000..52d9029b --- /dev/null +++ b/src/main/java/ecdar/presentations/BackendInstancePresentation.java @@ -0,0 +1,29 @@ +package ecdar.presentations; + +import com.jfoenix.controls.JFXRippler; +import ecdar.abstractions.BackendInstance; +import ecdar.controllers.BackendInstanceController; +import ecdar.utility.colors.Color; +import javafx.scene.Cursor; +import javafx.scene.layout.StackPane; + +public class BackendInstancePresentation extends StackPane { + private final BackendInstanceController controller; + + public BackendInstancePresentation(BackendInstance backendInstance) { + this(); + controller.setBackendInstance(backendInstance); + } + + public BackendInstancePresentation() { + controller = new EcdarFXMLLoader().loadAndGetController("BackendInstancePresentation.fxml", this); + + controller.pickPathToBackend.setCursor(Cursor.HAND); + controller.pickPathToBackend.setRipplerFill(Color.GREY.getColor(Color.Intensity.I500)); + controller.pickPathToBackend.setMaskType(JFXRippler.RipplerMask.CIRCLE); + } + + public BackendInstanceController getController() { + return controller; + } +} diff --git a/src/main/java/ecdar/presentations/BackendOptionsDialogPresentation.java b/src/main/java/ecdar/presentations/BackendOptionsDialogPresentation.java new file mode 100644 index 00000000..c3949083 --- /dev/null +++ b/src/main/java/ecdar/presentations/BackendOptionsDialogPresentation.java @@ -0,0 +1,16 @@ +package ecdar.presentations; + +import com.jfoenix.controls.JFXDialog; +import ecdar.controllers.BackendOptionsDialogController; + +public class BackendOptionsDialogPresentation extends JFXDialog { + private final BackendOptionsDialogController controller; + + public BackendOptionsDialogPresentation() { + controller = new EcdarFXMLLoader().loadAndGetController("BackendOptionsDialogPresentation.fxml", this); + } + + public BackendOptionsDialogController getController() { + return controller; + } +} diff --git a/src/main/java/ecdar/presentations/QueryPresentation.java b/src/main/java/ecdar/presentations/QueryPresentation.java index 17d9f593..464f5d57 100644 --- a/src/main/java/ecdar/presentations/QueryPresentation.java +++ b/src/main/java/ecdar/presentations/QueryPresentation.java @@ -20,19 +20,14 @@ import javafx.scene.layout.*; import javafx.scene.text.TextAlignment; import org.kordamp.ikonli.javafx.FontIcon; - import java.util.Map; import java.util.Set; import java.util.function.Consumer; - import static javafx.scene.paint.Color.*; public class QueryPresentation extends AnchorPane { - private final Tooltip tooltip = new Tooltip(); - private Tooltip swapBackendButtonTooltip; - private Label currentBackendLabel; - + private Tooltip backendDropdownTooltip; private final QueryController controller; public QueryPresentation(final Query query) { @@ -45,8 +40,19 @@ public QueryPresentation(final Query query) { initializeDetailsButton(); initializeTextFields(); initializeInputOutputPaneAndAddIgnoredInputOutputs(); - initializeSwapBackendButton(); initializeMoreInformationButtonAndQueryTypeSymbol(); + initializeBackendsDropdown(); + } + + private void initializeBackendsDropdown() { + controller.backendsDropdown.setItems(BackendHelper.getBackendInstances()); + BackendHelper.addBackendInstanceListener(() -> controller.backendsDropdown.setItems(BackendHelper.getBackendInstances())); + + backendDropdownTooltip = new Tooltip(); + backendDropdownTooltip.setText("Current backend used for the query"); + JFXTooltip.install(controller.backendsDropdown, backendDropdownTooltip); + + controller.backendsDropdown.setValue(BackendHelper.getDefaultBackendInstance()); } private void initializeTextFields() { @@ -271,9 +277,8 @@ private void initializeInputOutputPaneAndAddIgnoredInputOutputs() { } }); - // Change visibility of input/output Pane when backend is changed for the query - lookup("#swapBackendButton").setOnMousePressed(event -> changeTitledPaneVisibility.run()); - + // Change visibility of input/output Pane when backend is changed for the query ToDo NIELS + // lookup("#swapBackendButton").setOnMousePressed(event -> changeTitledPaneVisibility.accept(controller.getQuery().getQuery())); Platform.runLater(() -> addIgnoredInputOutputsFromQuery(inputOutputPane)); }); } @@ -327,35 +332,9 @@ private void initializeResetInputOutputPaneButton(TitledPane inputOutputPane, }); } - private void initializeSwapBackendButton() { - Platform.runLater(() -> { - final JFXRippler swapBackendButton = (JFXRippler) lookup("#swapBackendButton"); - final TitledPane inputOutputPane = (TitledPane) lookup("#inputOutputPane"); - this.currentBackendLabel = (Label) lookup("#currentBackendLabel"); - - swapBackendButton.setCursor(Cursor.HAND); - swapBackendButton.setRipplerFill(Color.GREY.getColor(Color.Intensity.I500)); - swapBackendButton.setMaskType(JFXRippler.RipplerMask.CIRCLE); - swapBackendButton.setOnMousePressed(event -> { - // Set the backend to the one not currently used and update GUI - final BackendHelper.BackendNames newBackend = (this.controller.getQuery().getBackend().equals(BackendHelper.BackendNames.jEcdar) - ? BackendHelper.BackendNames.Reveaal - : BackendHelper.BackendNames.jEcdar); - - this.controller.getQuery().setBackend(newBackend); - setSwapBackendTooltipAndLabel(newBackend); - updateTitlePaneVisibility(inputOutputPane); - }); - - swapBackendButtonTooltip = new Tooltip(); - setSwapBackendTooltipAndLabel(this.controller.getQuery().getBackend()); - JFXTooltip.install(swapBackendButton, swapBackendButtonTooltip); - }); - } - private void updateTitlePaneVisibility(TitledPane inputOutputPane) { - // Check if the query is a refinement and that the backend supports ignored inputs and outputs - if (BackendHelper.backendSupportsInputOutputs(controller.getQuery().getBackend()) && controller.getQuery().getType().equals(QueryType.REFINEMENT)) { + // Check if the query is a refinement and that the engine is set to Reveaal + if (controller.getQuery().getQuery().startsWith("refinement") && BackendHelper.backendSupportsInputOutputs(controller.getQuery().getBackend())) { initiateResetInputOutputButton(inputOutputPane); // Make the input/output pane visible @@ -377,7 +356,7 @@ private void updateInputOutputs(TitledPane inputOutputPane, Boolean shouldResetS clearIgnoredInputsAndOutputs(inputBox, outputBox); } - Ecdar.getBackendDriver().getInputOutputs(query); + Ecdar.getBackendDriver().getInputOutputs(query, controller.getQuery().getBackend()); } private void clearIgnoredInputsAndOutputs(VBox inputBox, VBox outputBox) { @@ -463,17 +442,10 @@ private void addIgnoredInputOutputsFromQuery(TitledPane inputOutputPane) { } } - private void setSwapBackendTooltipAndLabel(BackendHelper.BackendNames backend) { - boolean isReveaal; - if (backend == null) { - isReveaal = false; - } else { - isReveaal = backend.equals(BackendHelper.BackendNames.Reveaal); - } - - swapBackendButtonTooltip.setText("Switch to the " + (isReveaal ? "jEcdar" : "Reveaal") + " backend"); - currentBackendLabel.setText((isReveaal ? "Reveaal" : "jEcdar")); - } +// private void setSwapBackendTooltipAndLabel(BackendInstance backend) { +// swapBackendButtonTooltip.setText("Switch to the " + (isReveaal ? "jEcdar" : "Reveaal") + " backend"); +// currentBackendLabel.setText((isReveaal ? "Reveaal" : "jEcdar")); +// } private void initializeMoreInformationButtonAndQueryTypeSymbol() { Platform.runLater(() -> { diff --git a/src/main/resources/ecdar/main.css b/src/main/resources/ecdar/main.css index 2ad365db..2e2256ab 100644 --- a/src/main/resources/ecdar/main.css +++ b/src/main/resources/ecdar/main.css @@ -1,106 +1,126 @@ -.display4{ - -fx-font-family: "Roboto Light"; - -fx-font-size: 8.6em; +.display4 { + -fx-font-family: "Roboto Light"; + -fx-font-size: 8.6em; } -.display3{ - -fx-font-family: "Roboto"; - -fx-font-size: 4.3em; + +.display3 { + -fx-font-family: "Roboto"; + -fx-font-size: 4.3em; } -.display2{ - -fx-font-family: "Roboto"; - -fx-font-size: 3.5em; + +.display2 { + -fx-font-family: "Roboto"; + -fx-font-size: 3.5em; } -.display1{ - -fx-font-family: "Roboto"; - -fx-font-size: 2.6em; + +.display1 { + -fx-font-family: "Roboto"; + -fx-font-size: 2.6em; } -.headline{ - -fx-font-family: "Roboto"; - -fx-font-size: 1.8em; + +.headline { + -fx-font-family: "Roboto"; + -fx-font-size: 1.8em; } -.title{ - -fx-font-family: "Roboto Medium"; - -fx-font-size: 1.5em; + +.title { + -fx-font-family: "Roboto Medium"; + -fx-font-size: 1.5em; } -.subhead{ - -fx-font-family: "Roboto"; - -fx-font-size: 1.2em; + +.subhead { + -fx-font-family: "Roboto"; + -fx-font-size: 1.2em; } -.body2{ - -fx-font-family: "Roboto Medium"; - -fx-font-size: 1.0em; + +.body2 { + -fx-font-family: "Roboto Medium"; + -fx-font-size: 1.0em; } -.body1{ - -fx-font-family: "Roboto"; - -fx-font-size: 1.0em; + +.body1 { + -fx-font-family: "Roboto"; + -fx-font-size: 1.0em; } -.caption{ - -fx-font-family: "Roboto"; - -fx-font-size: 0.9em; + +.caption { + -fx-font-family: "Roboto"; + -fx-font-size: 0.9em; } -.sub-caption{ - -fx-font-family: "Roboto"; - -fx-font-size: 0.8em; + +.sub-caption { + -fx-font-family: "Roboto"; + -fx-font-size: 0.8em; } -.sub-caption-mono{ - -fx-font-family: "Roboto Mono"; - -fx-font-size: 0.7em; +.sub-caption-mono { + -fx-font-family: "Roboto Mono"; + -fx-font-size: 0.7em; } -.edge-property{ - -fx-font-family: "Roboto Mono Medium"; - -fx-font-size: 0.9em; +.edge-property { + -fx-font-family: "Roboto Mono Medium"; + -fx-font-size: 0.9em; } -.button{ - -fx-font-family: "Roboto Medium"; - -fx-font-size: 1.1em; +.button { + -fx-font-family: "Roboto Medium"; + -fx-font-size: 1.1em; } -.display4-mono{ - -fx-font-family: "Roboto Mono Light"; - -fx-font-size: 8.6em; +.display4-mono { + -fx-font-family: "Roboto Mono Light"; + -fx-font-size: 8.6em; } -.display3-mono{ - -fx-font-family: "Roboto Mono"; - -fx-font-size: 4.3em; + +.display3-mono { + -fx-font-family: "Roboto Mono"; + -fx-font-size: 4.3em; } -.display2-mono{ - -fx-font-family: "Roboto Mono"; - -fx-font-size: 3.5em; + +.display2-mono { + -fx-font-family: "Roboto Mono"; + -fx-font-size: 3.5em; } -.display1-mono{ - -fx-font-family: "Roboto Mono"; - -fx-font-size: 2.6em; + +.display1-mono { + -fx-font-family: "Roboto Mono"; + -fx-font-size: 2.6em; } -.headline-mono{ - -fx-font-family: "Roboto Mono"; - -fx-font-size: 1.8em; + +.headline-mono { + -fx-font-family: "Roboto Mono"; + -fx-font-size: 1.8em; } -.title-mono{ - -fx-font-family: "Roboto Mono Medium"; - -fx-font-size: 1.2em; ; + +.title-mono { + -fx-font-family: "Roboto Mono Medium"; + -fx-font-size: 1.2em;; } -.subhead-mono{ - -fx-font-family: "Roboto Mono"; - -fx-font-size: 1.2em; + +.subhead-mono { + -fx-font-family: "Roboto Mono"; + -fx-font-size: 1.2em; } -.body2-mono{ - -fx-font-family: "Roboto Mono Medium"; - -fx-font-size: 1.0em; + +.body2-mono { + -fx-font-family: "Roboto Mono Medium"; + -fx-font-size: 1.0em; } -.body1-mono{ - -fx-font-family: "Roboto Mono"; - -fx-font-size: 1.0em; + +.body1-mono { + -fx-font-family: "Roboto Mono"; + -fx-font-size: 1.0em; } -.caption-mono{ - -fx-font-family: "Roboto Mono"; - -fx-font-size: 0.9em; + +.caption-mono { + -fx-font-family: "Roboto Mono"; + -fx-font-size: 0.9em; } -.button-mono{ - -fx-font-family: "Roboto Mono Medium"; - -fx-font-size: 1.1em; + +.button-mono { + -fx-font-family: "Roboto Mono Medium"; + -fx-font-size: 1.1em; } .white-text { @@ -112,13 +132,13 @@ } .window-title { - -fx-label-padding: 0em 0em 0em 0.8em; + -fx-label-padding: 0em 0em 0em 0.8em; } .floating-action-button { - -fx-pref-width: 4.3em; - -fx-pref-height: 4.3em; - -fx-text-fill: white; + -fx-pref-width: 4.3em; + -fx-pref-height: 4.3em; + -fx-text-fill: white; } .titled-pane > .content { @@ -180,146 +200,77 @@ } .jfx-tab-pane .scroll-pane { - -fx-background: #ffffff00; /** Transparent **/ + -fx-background: #ffffff00; /** Transparent **/ } .comment { - -fx-fill: -grey-500; + -fx-fill: -grey-500; } .uppaal-keyword { - -fx-fill: -blue-700; + -fx-fill: -blue-700; } .c-keyword { - -fx-fill: -green-700; - -fx-font-weight: bold; + -fx-fill: -green-700; + -fx-font-weight: bold; } .jfx-snackbar-content { - -fx-background-color: #323232; - -fx-font-family: "Roboto Medium"; - -fx-font-size: 1.0em; + -fx-background-color: #323232; + -fx-font-family: "Roboto Medium"; + -fx-font-size: 1.0em; } .jfx-snackbar-toast { - -fx-text-fill: WHITE; - -fx-padding-left: 1.8em; - -fx-padding-right: 1.8em; + -fx-text-fill: WHITE; + -fx-padding-left: 1.8em; + -fx-padding-right: 1.8em; } .jfx-snackbar-action { - -fx-text-fill: WHITE; + -fx-text-fill: WHITE; } .titled-pane > .title { - -fx-background-color: TRANSPARENT; - -fx-border-style: HIDDEN HIDDEN SOLID HIDDEN; - -fx-border-color: -divider-color; - -fx-pref-height: 2.3em; + -fx-background-color: TRANSPARENT; + -fx-border-style: HIDDEN HIDDEN SOLID HIDDEN; + -fx-border-color: -divider-color; + -fx-pref-height: 2.3em; } -.titled-pane > .title > .arrow-button .arrow{ - -fx-background-color: TRANSPARENT; - -fx-border-color: TRANSPARENT; - -fx-padding: 0em 0em 0em -0.7em; /* -10 */ +.titled-pane > .title > .arrow-button .arrow { + -fx-background-color: TRANSPARENT; + -fx-border-color: TRANSPARENT; + -fx-padding: 0em 0em 0em -0.7em; /* -10 */ } .titled-pane > .content { - -fx-background-color: TRANSPARENT; - -fx-padding: 0em -0.1em -0.1em -0.1em; /* -1 */ - -fx-background-insets: 0em 0em 0em 0em; -} - -/* Scroll pane related styling */ -.scroll-bar:horizontal .track, -.scroll-bar:vertical .track{ - -fx-opacity: 0; - -fx-border-color: transparent; - -fx-focus-color: transparent; -} - -.scroll-bar:horizontal .increment-button , -.scroll-bar:horizontal .decrement-button { - visibility: hidden; - -fx-background-radius : 0.0em; - -fx-padding : 0.0em 0.0em 0.3em 0.0em; -} - -.scroll-bar:vertical .increment-button , -.scroll-bar:vertical .decrement-button { - visibility: hidden; - -fx-background-radius : 0.0em; - -fx-padding : 0.0em 0.3em 0.0em 0.0em; -} - -.scroll-bar .increment-arrow, -.scroll-bar .decrement-arrow{ - -fx-shape : " "; - -fx-padding : 0.15em 0.0em; -} - -.scroll-bar:vertical .increment-arrow, -.scroll-bar:vertical .decrement-arrow{ - -fx-shape : " "; - -fx-padding : 0.0em 0.15em; -} - -.scroll-bar:horizontal .thumb, -.scroll-bar:vertical .thumb { - -fx-background-color : derive(-divider-color, 40.0%); - -fx-background-insets : 0.15em, 0.0em, 0.0em; - -fx-background-radius : 1.8em; + -fx-background-color: TRANSPARENT; + -fx-padding: 0em -0.1em -0.1em -0.1em; /* -1 */ + -fx-background-insets: 0em 0em 0em 0em; } -.scroll-bar:horizontal .thumb:hover, -.scroll-bar:vertical .thumb:hover { - -fx-background-color : derive(-divider-color, 10.0%); - -fx-background-insets : 0.15em 0.0em, 0.0em; - -fx-background-radius : 1.8em; +.backend-instances-list { + -fx-padding: 5; + -fx-border-style: SOLID HIDDEN SOLID HIDDEN; + -fx-border-color: -divider-color; + -fx-border-width: 2px; } -.scroll-bar{ - -fx-background-color: transparent; - -fx-background-radius: 2.6em; - -fx-focus-color: transparent; - -fx-faint-focus-color: transparent; -} - -.scroll-bar:vertical:focused { - -fx-background-color: transparent; -} - -.jfx-slider { - -fx-pref-width: 4.6em; -} - -.jfx-slider > .track { - -fx-background-color: -divider-color; -} - -.jfx-slider > .thumb, .jfx-slider > .animated-thumb, .jfx-slider > .colored-track{ - -fx-background-color: -primary-color; -} - -.jfx-slider > .thumb { - -fx-pref-width: 0.7em; - -fx-background-radius: 0.2em; -} - -.jfx-slider > .slider-value { - -fx-fill: -primary-color-darker; - -fx-stroke: -primary-color-darker; -} - -.menu-item-embedded-control { - +.backend-instance { + -fx-border-style: SOLID SOLID SOLID SOLID; + -fx-border-color: -divider-color; + -fx-border-width: 1px; } -.menu-item-embedded-control:hover { - -fx-background-color: none; +.input-violation { + -fx-text-fill: red; } -.menu-item-embedded-control:selected { - -fx-background-color: none; +.button-danger { + -fx-border-style: SOLID SOLID SOLID SOLID; + -fx-border-color: -red-900; + -fx-border-radius: 0.25em; + -fx-border-width: 0.1em; } \ No newline at end of file diff --git a/src/main/resources/ecdar/presentations/BackendInstancePresentation.fxml b/src/main/resources/ecdar/presentations/BackendInstancePresentation.fxml new file mode 100644 index 00000000..391f1664 --- /dev/null +++ b/src/main/resources/ecdar/presentations/BackendInstancePresentation.fxml @@ -0,0 +1,100 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Address: + + + + Path: + + + + + + + + Local + + + + Port range: + + + + - + + + + + + + Default + + + \ No newline at end of file diff --git a/src/main/resources/ecdar/presentations/BackendOptionsDialogPresentation.fxml b/src/main/resources/ecdar/presentations/BackendOptionsDialogPresentation.fxml new file mode 100644 index 00000000..3a29787b --- /dev/null +++ b/src/main/resources/ecdar/presentations/BackendOptionsDialogPresentation.fxml @@ -0,0 +1,44 @@ + + + + + + + + + + + + + + + + + Backends + + + + + + + + + + + + + + + + + + + + diff --git a/src/main/resources/ecdar/presentations/EcdarPresentation.fxml b/src/main/resources/ecdar/presentations/EcdarPresentation.fxml index 58aaca5e..6255356d 100644 --- a/src/main/resources/ecdar/presentations/EcdarPresentation.fxml +++ b/src/main/resources/ecdar/presentations/EcdarPresentation.fxml @@ -11,6 +11,7 @@ + - - - - - Backend - - - - - - - - - - - - Backend Sockets: - - - - + + + + + @@ -396,7 +380,7 @@ - + @@ -499,7 +483,7 @@ - + @@ -586,4 +570,9 @@ + + + + + diff --git a/src/main/resources/ecdar/presentations/QueryPanePresentation.fxml b/src/main/resources/ecdar/presentations/QueryPanePresentation.fxml index 68ef1af6..7aae6d95 100644 --- a/src/main/resources/ecdar/presentations/QueryPanePresentation.fxml +++ b/src/main/resources/ecdar/presentations/QueryPanePresentation.fxml @@ -11,9 +11,7 @@ fx:id="root" fx:controller="ecdar.controllers.QueryPaneController" minWidth="400"> - - @@ -50,7 +48,6 @@ - - - - \ No newline at end of file diff --git a/src/main/resources/ecdar/presentations/QueryPresentation.fxml b/src/main/resources/ecdar/presentations/QueryPresentation.fxml index 950c4bdc..ae5712d0 100644 --- a/src/main/resources/ecdar/presentations/QueryPresentation.fxml +++ b/src/main/resources/ecdar/presentations/QueryPresentation.fxml @@ -78,12 +78,7 @@ - - - - - + diff --git a/src/main/resources/ecdar/scroll_pane.css b/src/main/resources/ecdar/scroll_pane.css new file mode 100644 index 00000000..7029b480 --- /dev/null +++ b/src/main/resources/ecdar/scroll_pane.css @@ -0,0 +1,57 @@ +.scroll-bar:horizontal .track, +.scroll-bar:vertical .track{ + -fx-opacity: 0; + -fx-border-color: transparent; + -fx-focus-color: transparent; +} + +.scroll-bar:horizontal .increment-button , +.scroll-bar:horizontal .decrement-button { + visibility: hidden; + -fx-background-radius : 0.0em; + -fx-padding :0.0 0.0 4.0 0.0; +} + +.scroll-bar:vertical .increment-button , +.scroll-bar:vertical .decrement-button { + visibility: hidden; + -fx-background-radius : 0.0em; + -fx-padding :0.0 4.0 0.0 0.0; +} + +.scroll-bar .increment-arrow, +.scroll-bar .decrement-arrow{ + -fx-shape : " "; + -fx-padding :0.15em 0.0; +} + +.scroll-bar:vertical .increment-arrow, +.scroll-bar:vertical .decrement-arrow{ + -fx-shape : " "; + -fx-padding :0.0 0.15em; +} + +.scroll-bar:horizontal .thumb, +.scroll-bar:vertical .thumb { + -fx-background-color : derive(-divider-color, 40.0%); + -fx-background-insets : 2.0, 0.0, 0.0; + -fx-background-radius : 2.0em; +} + +.scroll-bar:horizontal .thumb:hover, +.scroll-bar:vertical .thumb:hover { + -fx-background-color : derive(-divider-color, 10.0%); + -fx-background-insets : 2.0, 0.0, 0.0; + -fx-background-radius : 2.0em; +} + +.scroll-bar{ + -fx-background-color: transparent; + -fx-background-radius: 2em; + -fx-focus-color: transparent; + -fx-faint-focus-color: transparent; +} + +.scroll-bar:vertical:focused { + -fx-background-color: transparent; +} \ No newline at end of file