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

Adding avatar syntax checker in command line

parent 9b429283
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/main/java/cli/Action.java
+ 103
− 56
View file @ 285fab91
......@@ -148,7 +148,8 @@ public class Action extends Command implements ProVerifOutputListener {
private final static String AVATAR_SIMULATION_SELECT_TRACE = "avatar-simulation-select-trace";
private final static String AVATAR_SIMULATION_OPEN_WINDOW = "avatar-simulation-open-window";
private final static String AVATAR_SIMULATION_GENERIC = "avatar-simulation-generic";
private final static String AVATAR_LOAD_FROM_SYSMLV2= "avatar-load-sysmlv2";
private final static String AVATAR_LOAD_FROM_SYSMLV2 = "avatar-load-sysmlv2";
private final static String AVATAR_SYNTAX_CHECKER = "avatar-syntax-checker";
private final static String AVATAR_COMPLEXITY = "avatar-complexity";
......@@ -229,7 +230,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Starting the graphical interface of TTool";
return "Starts the graphical interface of TTool";
}
public String executeCommand(String command, Interpreter interpreter) {
......@@ -272,7 +273,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Resize TTool main window";
return "Resizes TTool main window";
}
public String executeCommand(String command, Interpreter interpreter) {
......@@ -307,7 +308,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Opening a model in TTool";
return "Opens a model in TTool";
}
public String executeCommand(String command, Interpreter interpreter) {
......@@ -332,7 +333,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Creating a new model in TTool";
return "Creates a new model in TTool";
}
public String executeCommand(String command, Interpreter interpreter) {
......@@ -357,7 +358,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Setting the save file of TTool";
return "Sets the save file of TTool";
}
public String executeCommand(String command, Interpreter interpreter) {
......@@ -388,7 +389,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Get the name of the model under edition TTool";
return "Gets the name of the model under edition TTool";
}
public String getUsage() {
......@@ -409,7 +410,7 @@ public class Action extends Command implements ProVerifOutputListener {
interpreter.addVariable(commands[0], fileName);
}
System.out.println(fileName);
TraceManager.addUser(fileName);
return null;
}
......@@ -426,7 +427,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Saving a model in TTool";
return "Saves a model in TTool";
}
public String executeCommand(String command, Interpreter interpreter) {
......@@ -451,7 +452,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Closing the graphical interface of TTool";
return "Closes the graphical interface of TTool";
}
public String executeCommand(String command, Interpreter interpreter) {
......@@ -474,7 +475,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Create a new design view";
return "Creates a new design view";
}
public String executeCommand(String command, Interpreter interpreter) {
......@@ -499,7 +500,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Remove the current tab";
return "Removes the current tab";
}
public String executeCommand(String command, Interpreter interpreter) {
......@@ -524,7 +525,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Checking the syntax of an opened model";
return "Checks the syntax of an opened graphical model";
}
public String executeCommand(String command, Interpreter interpreter) {
......@@ -569,7 +570,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Removing time operators from an avatar specification";
return "Removes time operators from an avatar specification";
}
public String executeCommand(String command, Interpreter interpreter) {
......@@ -714,7 +715,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Perform a series of mutations on a DIPLODOCUS (TML, TMAP or TARCHI) model";
return "Performs a series of mutations on a DIPLODOCUS (TML, TMAP or TARCHI) model";
}
public String getUsage() {
......@@ -887,7 +888,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Generate the TML code of a diplodocus model";
return "Generates the TML code of a diplodocus model";
}
public String executeCommand(String command, Interpreter interpreter) {
......@@ -929,7 +930,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Generate the XML of a diplodocus model";
return "Generates the XML of a diplodocus model";
}
public String getUsage() {
......@@ -979,7 +980,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Use UPPAAL for formal verification of a DIPLO app";
return "Uses UPPAAL for formal verification of a DIPLO app";
}
public String executeCommand(String command, Interpreter interpreter) {
......@@ -1023,7 +1024,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Remove the NoCs of a diplodocus mapping";
return "Removes the NoCs of a diplodocus mapping";
}
public String executeCommand(String command, Interpreter interpreter) {
......@@ -1058,7 +1059,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Load a textual TML specification";
return "Loads a textual TML specification";
}
public String executeCommand(String command, Interpreter interpreter) {
......@@ -1099,7 +1100,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Load a textual TMAP specification";
return "Loads a textual TMAP specification";
}
public String executeCommand(String command, Interpreter interpreter) {
......@@ -1141,7 +1142,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Draw a TML specification";
return "Draws a TML specification";
}
public String executeCommand(String command, Interpreter interpreter) {
......@@ -1180,7 +1181,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Draw a TMAP specification";
return "Draws a TMAP specification";
}
public String executeCommand(String command, Interpreter interpreter) {
......@@ -1230,7 +1231,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Perform security verification over a TMAP specification";
return "Performs security verification over a TMAP specification";
}
public String executeCommand(String command, Interpreter interpreter) {
......@@ -1308,7 +1309,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Select the edition panel with a name";
return "Selects the edition panel with a name provided as argument";
}
public String executeCommand(String command, Interpreter interpreter) {
......@@ -1338,7 +1339,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Move current panel to the left";
return "Moves current panel to the left";
}
public String executeCommand(String command, Interpreter interpreter) {
......@@ -1362,7 +1363,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Move current panel to the right";
return "Moves current panel to the right";
}
public String executeCommand(String command, Interpreter interpreter) {
......@@ -1484,7 +1485,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Perform a series of mutations on an AVATAR spec";
return "Performs a series of mutations on an AVATAR spec";
}
public String getUsage() {
......@@ -1553,7 +1554,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Print in text format an Avatar Specification";
return "Prints an Avatar Specification in text format";
}
public String getUsage() {
......@@ -1574,7 +1575,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
}
System.out.println(spec);
TraceManager.addUser(spec.toString());
return null;
}
......@@ -1590,7 +1591,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Draw the current avatar specification";
return "Draws the current avatar specification";
}
public String getUsage() {
......@@ -1608,7 +1609,7 @@ public class Action extends Command implements ProVerifOutputListener {
return Interpreter.TTOOL_NO_MODEL;
}
AvatarSpecification spec = as;
if (spec == null) {
spec = interpreter.mgui.gtm.getAvatarSpecification();
......@@ -1633,7 +1634,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Generate the dependency graph of an Avatar model";
return "Generates the dependency graph of an Avatar model";
}
public String getUsage() {
......@@ -1690,7 +1691,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Generate a Reachability graph from an AVATAR model";
return "Generates a Reachability graph from an AVATAR model";
}
public String getUsage() { return "[OPTION]... [FILE]\n"
......@@ -1825,7 +1826,7 @@ public class Action extends Command implements ProVerifOutputListener {
for (String q : queries) {
if (q != "") {
if (amc.addSafety(q, q) == false) {
System.out.println("Query " + q + " is badly written");
TraceManager.addUser("Query " + q + " is badly written");
return Interpreter.BAD;
}
}
......@@ -1921,8 +1922,8 @@ public class Action extends Command implements ProVerifOutputListener {
}
System.out.println("Model checking done\nGraph: states:" + amc.getNbOfStates() +
TraceManager.addUser("Model checking done\nGraph: states:" + amc.getNbOfStates() +
" links:" + amc.getNbOfLinks() + "\n");
if (noDeadlocks) {
......@@ -1973,9 +1974,9 @@ public class Action extends Command implements ProVerifOutputListener {
try {
File f = new File(file);
FileUtils.saveFile(file, trace);
System.out.println("\nCounterexample trace saved in " + file + "\n");
TraceManager.addUser("\nCounterexample trace saved in " + file + "\n");
} catch (Exception e) {
System.out.println("\nCounterexample trace could not be saved in " + file + "\n");
TraceManager.addUser("\nCounterexample trace could not be saved in " + file + "\n");
}
if (counterTracesAUT) {
......@@ -1998,9 +1999,9 @@ public class Action extends Command implements ProVerifOutputListener {
interpreter.mgui.addRG(rg);
File f = new File(filename);
FileUtils.saveFile(filename, tr.getReport());
System.out.println("Counterexample graph trace " + tr.getQuery() + " saved in " + filename + "\n");
TraceManager.addUser("Counterexample graph trace " + tr.getQuery() + " saved in " + filename + "\n");
} catch (Exception e) {
System.out.println("Counterexample graph trace "+ tr.getQuery() + " could not be saved in " + filename + "\n");
TraceManager.addUser("Counterexample graph trace "+ tr.getQuery() + " could not be saved in " + filename + "\n");
}
i++;
}
......@@ -2018,15 +2019,15 @@ public class Action extends Command implements ProVerifOutputListener {
}
if (graphPath.indexOf("?") != -1) {
//System.out.println("Question mark found");
// TraceManager.addUser("Question mark found");
autfile = Conversion.replaceAllChar(graphPath, '?', dateAndTime);
//System.out.println("graphpath=" + graphPath);
// TraceManager.addUser("graphpath=" + graphPath);
} else {
autfile = graphPath;
}
System.out.println("graphpath=" + graphPath);
System.out.println("autfile=" + autfile);
TraceManager.addUser("graphpath=" + graphPath);
TraceManager.addUser("autfile=" + autfile);
try {
RG rg = new RG(autfile);
......@@ -2034,14 +2035,14 @@ public class Action extends Command implements ProVerifOutputListener {
rg.fileName = autfile;
rg.nbOfStates = amc.getNbOfStates();
rg.nbOfTransitions = amc.getNbOfLinks();
System.out.println("Saving graph in " + autfile + "\n");
TraceManager.addUser("Saving graph in " + autfile + "\n");
File f = new File(autfile);
rg.name = f.getName();
interpreter.mgui.addRG(rg);
FileUtils.saveFile(autfile, graphAUT);
System.out.println("Graph saved in " + autfile + "\n");
TraceManager.addUser("Graph saved in " + autfile + "\n");
} catch (Exception e) {
System.out.println("Graph could not be saved in " + autfile + "\n");
TraceManager.addUser("Graph could not be saved in " + autfile + "\n");
}
}
......@@ -2079,7 +2080,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Validate the internal verification tool with uppaal";
return "Validates the internal verification tool with uppaal";
}
public String getUsage() {
......@@ -2173,7 +2174,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Simulate an avatar design until a breakpoint or the end";
return "Simulates an avatar design until a breakpoint is met or the simulation terminates";
}
public String executeCommand(String command, Interpreter interpreter) {
......@@ -2209,7 +2210,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Simulate a trace to be simulated";
return "Selects an execution trace to be simulated";
}
public String getUsage() {
......@@ -2252,7 +2253,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Show / hide Avatar simulation window";
return "Shows / hides Avatar simulation window";
}
public String getUsage() {
......@@ -2284,7 +2285,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Execute a generic action in the Avatar simulation";
return "Executes a generic action in the Avatar simulation";
}
public String getUsage() {
......@@ -2339,7 +2340,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
public String getDescription() {
return "Load an Avatar specification from a SysML v2 textual description";
return "Loads an Avatar specification from a SysML v2 textual description";
}
public String getUsage() {
......@@ -2366,6 +2367,51 @@ public class Action extends Command implements ProVerifOutputListener {
}
};
Command avatarSyntaxChecker = new Command() {
public String getCommand() {
return AVATAR_SYNTAX_CHECKER;
}
public String getShortCommand() {
return "asc";
}
public String getDescription() {
return "Checks the syntax of an avatar specification";
}
public String getUsage() {
String usage = "avatar-syntax-checker\n";
return usage;
}
public String executeCommand(String command, Interpreter interpreter) {
AvatarSpecification spec = as;
if (spec == null) {
if (interpreter.hasAModel()) {
spec = interpreter.mgui.gtm.getAvatarSpecification();
}
if (spec == null) {
return "No AVATAR specification";
}
}
List<AvatarError> errors = AvatarSyntaxChecker.checkSyntaxErrors(spec);
TraceManager.addUser("Syntax checking done, " + errors.size() + " errors found");
for(int i=0; i<errors.size(); i++) {
AvatarError err = errors.get(i);
String res = i + ".\t" + err.toString();
TraceManager.addUser(res);
}
return null;
}
};
Command graphtToAvatar = new Command() {
public String getCommand() {
......@@ -2477,6 +2523,7 @@ public class Action extends Command implements ProVerifOutputListener {
addAndSortSubcommand(avatarSimulationOpenWindow);
addAndSortSubcommand(avatarSimulationGeneric);
addAndSortSubcommand(avatarLoadFromSysMLV2);
addAndSortSubcommand(avatarSyntaxChecker);
addAndSortSubcommand(generic);
......@@ -2593,7 +2640,7 @@ public class Action extends Command implements ProVerifOutputListener {
}
}
System.out.println(buffer);
TraceManager.addUser(buffer.toString());
}
}
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