Skip to content
Snippets Groups Projects
Commit cbbcaab5 authored by Ludovic Apvrille's avatar Ludovic Apvrille
Browse files

Revert "Finished the implementation of the model checker validator and of the associated tests"

This reverts commit 4edaea66.
parent 7ecf059d
No related branches found
No related tags found
No related merge requests found
...@@ -92,6 +92,10 @@ public class Action extends Command { ...@@ -92,6 +92,10 @@ public class Action extends Command {
private final static String NAVIGATE_LEFT_PANEL = "navigate-left-panel"; private final static String NAVIGATE_LEFT_PANEL = "navigate-left-panel";
private final static String AVATAR_RG_GENERATION = "avatar-rg"; 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() { public Action() {
...@@ -586,7 +590,20 @@ public class Action extends Command { ...@@ -586,7 +590,20 @@ public class Action extends Command {
return "Generate a Reachability graph from an AVATAR model"; return "Generate a Reachability graph from an AVATAR model";
} }
<<<<<<< HEAD
public String getUsage() { return "arg <Ref to graph file>"; } 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() { public String getExample() {
return "arg /tmp/mylovelyrg?.aut (\"?\" is replaced with current date and time)"; return "arg /tmp/mylovelyrg?.aut (\"?\" is replaced with current date and time)";
...@@ -662,6 +679,57 @@ public class Action extends Command { ...@@ -662,6 +679,57 @@ public class Action extends Command {
return null; 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
......
...@@ -281,7 +281,6 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act ...@@ -281,7 +281,6 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
livenessCheckable.setSelected(livenessSelected == LIVENESS_SELECTED); livenessCheckable.setSelected(livenessSelected == LIVENESS_SELECTED);
livenessAllStates.setSelected(livenessSelected == LIVENESS_ALL); livenessAllStates.setSelected(livenessSelected == LIVENESS_ALL);
// RG // RG
saveGraphAUT = new JCheckBox("Reachability Graph Generation", graphSelected); saveGraphAUT = new JCheckBox("Reachability Graph Generation", graphSelected);
saveGraphAUT.addActionListener(this); saveGraphAUT.addActionListener(this);
......
...@@ -55,6 +55,7 @@ import java.util.List; ...@@ -55,6 +55,7 @@ import java.util.List;
import java.util.Map; import java.util.Map;
import cli.Interpreter; import cli.Interpreter;
import graph.AUTGraph; import graph.AUTGraph;
import org.junit.Before; import org.junit.Before;
import org.junit.Test; import org.junit.Test;
...@@ -87,5 +88,5 @@ public class CLIAvatarModelCheckerTest extends AbstractTest implements Interpret ...@@ -87,5 +88,5 @@ public class CLIAvatarModelCheckerTest extends AbstractTest implements Interpret
} }
} }
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment