diff --git a/src/main/java/cli/Action.java b/src/main/java/cli/Action.java
index d37db6524fd0a70c7f6ccd526e9f443666bfc9b8..e6a6fe171f3b16e011fc58c5cb5e7e01a72b49db 100644
--- a/src/main/java/cli/Action.java
+++ b/src/main/java/cli/Action.java
@@ -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());
}
}