From cbbcaab55699fd6781832d0e90dcf01a019d8c76 Mon Sep 17 00:00:00 2001
From: Ludovic Apvrille <ludovic.apvrille@telecom-paristech.fr>
Date: Wed, 13 May 2020 15:53:48 +0200
Subject: [PATCH] Revert "Finished the implementation of the model checker
validator and of the associated tests"
This reverts commit 4edaea660539e7760e983be1326d8d175cc132c1.
---
src/main/java/cli/Action.java | 68 +++++++++++++++++++
.../ui/window/JDialogAvatarModelChecker.java | 1 -
.../java/cli/CLIAvatarModelCheckerTest.java | 3 +-
3 files changed, 70 insertions(+), 2 deletions(-)
diff --git a/src/main/java/cli/Action.java b/src/main/java/cli/Action.java
index 700e765481..1bb531aef5 100644
--- a/src/main/java/cli/Action.java
+++ b/src/main/java/cli/Action.java
@@ -92,6 +92,10 @@ public class Action extends Command {
private final static String NAVIGATE_LEFT_PANEL = "navigate-left-panel";
private final static String AVATAR_RG_GENERATION = "avatar-rg";
+<<<<<<< HEAD
+=======
+ private final static String AVATAR_UPPAAL_COMPARE = "comp-uppaal";
+>>>>>>> parent of 4edaea660... Finished the implementation of the model checker validator and of the associated tests
public Action() {
@@ -586,7 +590,20 @@ public class Action extends Command {
return "Generate a Reachability graph from an AVATAR model";
}
+<<<<<<< HEAD
public String getUsage() { return "arg <Ref to graph file>"; }
+=======
+ public String getUsage() { return "[OPTION]... [FILE]\n"
+ + "-r, -rs\treachability of selected states\n"
+ + "-ra\treachability of all states\n"
+ + "-l, ls\tliveness of all states\n"
+ + "-la\tliveness of all states\n"
+ + "-s safety pragmas verification\n"
+ + "-d no deadlocks verification\n"
+ + "-n NUM\t maximum states created\n"
+ + "-t NUM\t maximum time (ms)\n";
+ }
+>>>>>>> parent of 4edaea660... Finished the implementation of the model checker validator and of the associated tests
public String getExample() {
return "arg /tmp/mylovelyrg?.aut (\"?\" is replaced with current date and time)";
@@ -662,6 +679,57 @@ public class Action extends Command {
return null;
}
};
+<<<<<<< HEAD
+=======
+
+ Command compareUppaal = new Command() {
+ public String getCommand() {
+ return AVATAR_UPPAAL_COMPARE;
+ }
+
+ public String getShortCommand() {
+ return "cup";
+ }
+
+ public String getDescription() {
+ return "Compare the internal verification tool with uppaal";
+ }
+
+ public String getUsage() {
+ return "c-uppaal [UPPAAL PATH]";
+ }
+
+ public String getExample() {
+ return "comp-uppaal /packages/uppaal/";
+ }
+
+ public String executeCommand(String command, Interpreter interpreter) {
+ if (!interpreter.isTToolStarted()) {
+ return Interpreter.TTOOL_NOT_STARTED;
+ }
+
+ String[] commands = command.split(" ");
+ if (commands.length != 1) {
+ return Interpreter.BAD;
+ }
+
+ String uppaalPath = commands[0];
+
+ //set configuration paths
+ ConfigurationTTool.UPPAALVerifierHost = "localhost";
+ ConfigurationTTool.UPPAALVerifierPath = uppaalPath + "/bin-Linux/verifyta";
+ ConfigurationTTool.UPPAALCodeDirectory = "../../uppaal/";
+ SpecConfigTTool.UPPAALCodeDirectory = ConfigurationTTool.UPPAALCodeDirectory;
+
+ interpreter.mgui.gtm.generateUPPAALFromAVATAR(SpecConfigTTool.UPPAALCodeDirectory);
+
+ boolean res = CompareToUppaal.compareToUppaal(interpreter.mgui, 2, 2, false, true);
+
+ interpreter.print("comp-uppaal result: " + res);
+ return null;
+ }
+ };
+>>>>>>> parent of 4edaea660... Finished the implementation of the model checker validator and of the associated tests
diff --git a/src/main/java/ui/window/JDialogAvatarModelChecker.java b/src/main/java/ui/window/JDialogAvatarModelChecker.java
index 51ddb00ca1..fb329344e4 100644
--- a/src/main/java/ui/window/JDialogAvatarModelChecker.java
+++ b/src/main/java/ui/window/JDialogAvatarModelChecker.java
@@ -281,7 +281,6 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
livenessCheckable.setSelected(livenessSelected == LIVENESS_SELECTED);
livenessAllStates.setSelected(livenessSelected == LIVENESS_ALL);
-
// RG
saveGraphAUT = new JCheckBox("Reachability Graph Generation", graphSelected);
saveGraphAUT.addActionListener(this);
diff --git a/ttool/src/test/java/cli/CLIAvatarModelCheckerTest.java b/ttool/src/test/java/cli/CLIAvatarModelCheckerTest.java
index edecb4fb47..37daf75fa1 100644
--- a/ttool/src/test/java/cli/CLIAvatarModelCheckerTest.java
+++ b/ttool/src/test/java/cli/CLIAvatarModelCheckerTest.java
@@ -55,6 +55,7 @@ import java.util.List;
import java.util.Map;
import cli.Interpreter;
+
import graph.AUTGraph;
import org.junit.Before;
import org.junit.Test;
@@ -87,5 +88,5 @@ public class CLIAvatarModelCheckerTest extends AbstractTest implements Interpret
}
-
+
}
--
GitLab