Commit 8e67fda6 authored by Ludovic Apvrille's avatar Ludovic Apvrille

Revert "First version model-checker validator which validates internal...

Revert "First version model-checker validator which validates internal verification results with UPPAAL"

This reverts commit 9b20334e.
parent cbbcaab5
......@@ -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;
}
......
......@@ -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();
......
......@@ -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");
......
......@@ -87,6 +87,5 @@ public class CLIAvatarModelCheckerTest extends AbstractTest implements Interpret
System.out.println("info from interpreter:" + s);
}
}
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment