From 8e67fda69b4fe42646f8c6122ffeb5ed7ee5d962 Mon Sep 17 00:00:00 2001
From: Ludovic Apvrille <ludovic.apvrille@telecom-paristech.fr>
Date: Wed, 13 May 2020 15:59:32 +0200
Subject: [PATCH] Revert "First version model-checker validator which validates
internal verification results with UPPAAL"
This reverts commit 9b20334e7fad4ced85917596e7266690f2502710.
---
.../modelchecker/AvatarModelChecker.java | 5 ++
src/main/java/cli/Action.java | 70 -------------------
.../ui/window/JDialogAvatarModelChecker.java | 1 +
.../java/cli/CLIAvatarModelCheckerTest.java | 1 -
4 files changed, 6 insertions(+), 71 deletions(-)
diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index 63644f70c1..deb548acab 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -179,6 +179,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
public void setLivenessofState(AvatarStateElement _ase, AvatarBlock _ab) {
livenessInfo = new SpecificationLiveness(_ase, _ab);
studyLiveness = true;
+
}
public int setReachabilityOfSelected() {
@@ -247,6 +248,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
return false;
}
+
if (livenessInfo == null) {
return false;
}
@@ -257,7 +259,9 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
computeRG = false;
+
startModelChecking();
+
return true;
}
@@ -1414,6 +1418,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
ret += (cpt + 1) + ". " + re.toString() + "\n";
cpt++;
}
+
return ret;
}
diff --git a/src/main/java/cli/Action.java b/src/main/java/cli/Action.java
index 1bb531aef5..9e55e9cbc7 100644
--- a/src/main/java/cli/Action.java
+++ b/src/main/java/cli/Action.java
@@ -92,10 +92,6 @@ 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() {
@@ -590,20 +586,7 @@ 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)";
@@ -679,59 +662,6 @@ 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
-
-
Command generic = new Generic();
diff --git a/src/main/java/ui/window/JDialogAvatarModelChecker.java b/src/main/java/ui/window/JDialogAvatarModelChecker.java
index fb329344e4..f108ea2847 100644
--- a/src/main/java/ui/window/JDialogAvatarModelChecker.java
+++ b/src/main/java/ui/window/JDialogAvatarModelChecker.java
@@ -578,6 +578,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
testGo();
amc.startModelChecking();
+
TraceManager.addDev("Model checking done");
//TraceManager.addDev("RG:" + amc.statesToString() + "\n\n");
diff --git a/ttool/src/test/java/cli/CLIAvatarModelCheckerTest.java b/ttool/src/test/java/cli/CLIAvatarModelCheckerTest.java
index 37daf75fa1..1a03709d9d 100644
--- a/ttool/src/test/java/cli/CLIAvatarModelCheckerTest.java
+++ b/ttool/src/test/java/cli/CLIAvatarModelCheckerTest.java
@@ -87,6 +87,5 @@ public class CLIAvatarModelCheckerTest extends AbstractTest implements Interpret
System.out.println("info from interpreter:" + s);
}
-
}
--
GitLab