diff --git a/src/main/java/avatartranslator/AvatarExpressionAttribute.java b/src/main/java/avatartranslator/AvatarExpressionAttribute.java
index 5fb16200dc1d823acdb393184d270d7f1bfde9fa..0ca60b084df1368030ff3bcd047b6b5467ef5ac4 100644
--- a/src/main/java/avatartranslator/AvatarExpressionAttribute.java
+++ b/src/main/java/avatartranslator/AvatarExpressionAttribute.java
@@ -101,7 +101,7 @@ public class AvatarExpressionAttribute {
block = spec.getBlockWithName(blockString);
- if (blockIndex == -1) {
+ if (block == null) {
return false;
}
diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index 802d4170f3504f4116b793bfa2c2248c64c254d1..f1b8e5cf6b3c52d1a3e1209fe2ddaeeb349e01c4 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -194,7 +194,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
public void setIgnoreInternalStates(boolean _b) {
- TraceManager.addDev("ignore niternal state?" + ignoreInternalStates);
+ TraceManager.addDev("ignore internal state?" + ignoreInternalStates);
ignoreInternalStates = _b;
}
@@ -346,7 +346,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}*/
public boolean startModelCheckingProperties() {
- boolean studyS, studyL, studyR;
+ boolean studyS, studyL, studyR, genRG;
long deadlocks = 0;
if (spec == null) {
@@ -365,6 +365,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
studyR = studyReachability;
studyL = studyLiveness;
studyS = studySafety;
+ genRG = computeRG;
//then compute livenesses
computeRG = false;
@@ -414,16 +415,24 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
studySafety = false;
}
- if (studyR) {
- studyReachability = true;
- //computeRG = true;
+ if (studyR || genRG) {
+ if (genRG) {
+ deadlocks = 0;
+ }
+ studyReachability = studyR;
+ computeRG = genRG;
startModelChecking(nbOfThreads);
deadlocks += nbOfDeadlocks;
resetModelChecking();
studyReachability = false;
+ computeRG = false;
}
- if (checkNoDeadlocks) {
+ if (genRG) {
+ nbOfDeadlocks = (int) deadlocks;
+ } else if (checkNoDeadlocks) {
+ //If a complete study with reachability graph generation has been executed,
+ //there is no need to study deadlocks again
if (deadlocks == 0) {
deadlockStop = true;
startModelChecking(nbOfThreads);
@@ -432,9 +441,11 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
}
+ computeRG = genRG;
studyLiveness = studyL;
studySafety = studyS;
studyReachability = studyR;
+
TraceManager.addDev("Model checking done");
return true;
}
diff --git a/src/main/java/cli/Action.java b/src/main/java/cli/Action.java
index 9b7ecf52b124593e69729580b83d6d531afb76ac..2448561495d0c40f3c3822b3ae21cadb1a89e9ae 100644
--- a/src/main/java/cli/Action.java
+++ b/src/main/java/cli/Action.java
@@ -587,14 +587,16 @@ public class Action extends Command {
}
public String getUsage() { return "[OPTION]... [FILE]\n"
+ + "-g FILE\tcompute and save in FILE the reachability graph"
+ "-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\tsafety pragmas verification\n"
+ + "-q \"QUERY\"\tquery a safety pragma\n"
+ "-d\tno deadlocks verification\n"
- + "-n NUM\tmaximum states created\n"
- + "-t NUM\tmaximum time (ms)\n";
+ + "-n NUM\tmaximum states created (Only for a non verification study)\n"
+ + "-t NUM\tmaximum time (ms) (Only for a non verification study)\n";
}
public String getExample() {
@@ -602,7 +604,7 @@ public class Action extends Command {
}
public String executeCommand(String command, Interpreter interpreter) {
- //format: flags(-rl -la -t 100) graph_path
+ //format: -rl -la -t 100 -g graph_path
if (!interpreter.isTToolStarted()) {
return Interpreter.TTOOL_NOT_STARTED;
@@ -613,7 +615,8 @@ public class Action extends Command {
return Interpreter.BAD;
}
- String graphPath = commands[commands.length - 1];
+ //String graphPath = commands[commands.length - 1];
+ String graphPath = "";
AvatarSpecification avspec = interpreter.mgui.gtm.getAvatarSpecification();
if(avspec == null) {
@@ -624,14 +627,24 @@ public class Action extends Command {
amc.setIgnoreEmptyTransitions(true);
amc.setIgnoreConcurrenceBetweenInternalActions(true);
amc.setIgnoreInternalStates(true);
- amc.setComputeRG(true);
+ amc.setComputeRG(false);
+ boolean rgGraph = false;
boolean reachabilityAnalysis = false;
boolean livenessAnalysis = false;
boolean safetyAnalysis = false;
boolean noDeadlocks = false;
- for (int i = 0; i < commands.length - 1; i++) {
+ for (int i = 0; i < commands.length; i++) {
//specification
switch (commands[i]) {
+ case "-g":
+ if (i != commands.length - 1) {
+ graphPath = commands[++i];
+ amc.setComputeRG(true);
+ rgGraph = true;
+ } else {
+ return Interpreter.BAD;
+ }
+ break;
case "-r":
case "-rs":
//reachability of selected states
@@ -659,6 +672,31 @@ public class Action extends Command {
amc.setSafetyAnalysis();
safetyAnalysis = true;
break;
+ case "-q":
+ //query
+ StringBuilder query;
+ if (!commands[++i].startsWith("\"")) {
+ return Interpreter.BAD;
+ }
+ query = new StringBuilder(commands[i].substring(1));
+ while (!commands[++i].endsWith("\"") && i < commands.length) {
+ query.append(" ");
+ query.append(commands[i]);
+ }
+ query.append(" ");
+ query.append(commands[i].substring(0, commands[i].length() - 1));
+ //Supports multiple queries separated by a comma
+ String[] queries = query.toString().split("\\s*,\\s*");
+ for (String q : queries) {
+ if (q != "") {
+ if (amc.addSafety(q) == false) {
+ System.out.println("Query " + q + " is badly written");
+ return Interpreter.BAD;
+ }
+ }
+ }
+ safetyAnalysis = true;
+ break;
case "-d":
//safety
amc.setCheckNoDeadlocks(true);
@@ -669,7 +707,7 @@ public class Action extends Command {
long states;
try {
states = Long.parseLong(commands[++i]);
- } catch (NumberFormatException e){
+ } catch (Exception e){
return Interpreter.BAD;
}
amc.setStateLimitValue(states);
@@ -680,7 +718,7 @@ public class Action extends Command {
long time;
try {
time = Long.parseLong(commands[++i]);
- } catch (NumberFormatException e){
+ } catch (Exception e){
return Interpreter.BAD;
}
amc.setTimeLimitValue(time);
@@ -691,7 +729,7 @@ public class Action extends Command {
}
}
TraceManager.addDev("Starting model checking");
- if (livenessAnalysis || safetyAnalysis) {
+ if (livenessAnalysis || safetyAnalysis || noDeadlocks) {
amc.startModelCheckingProperties();
} else {
amc.startModelChecking();
@@ -713,43 +751,45 @@ public class Action extends Command {
}
// Saving graph
- String graphAUT = amc.toAUT();
- String autfile;
-
- if (graphPath.length() == 0) {
- graphPath = System.getProperty("user.dir") + "/" + "rg$.aut";
- }
-
-
-
- if (graphPath.indexOf("?") != -1) {
- //System.out.println("Question mark found");
- DateFormat dateFormat = new SimpleDateFormat("_yyyyMMdd_HHmmss");
- Date date = new Date();
- String dateAndTime = dateFormat.format(date);
- autfile = Conversion.replaceAllChar(graphPath, '?', dateAndTime);
- //System.out.println("graphpath=" + graphPath);
- } else {
- autfile = graphPath;
- }
- System.out.println("graphpath=" + graphPath);
-
- System.out.println("autfile=" + autfile);
-
- try {
- RG rg = new RG(autfile);
- rg.data = graphAUT;
- rg.fileName = autfile;
- rg.nbOfStates = amc.getNbOfStates();
- rg.nbOfTransitions = amc.getNbOfLinks();
- System.out.println("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");
- } catch (Exception e) {
- System.out.println("Graph could not be saved in " + autfile + "\n");
+ if (rgGraph) {
+ String graphAUT = amc.toAUT();
+ String autfile;
+
+ if (graphPath.length() == 0) {
+ graphPath = System.getProperty("user.dir") + "/" + "rg$.aut";
+ }
+
+
+
+ if (graphPath.indexOf("?") != -1) {
+ //System.out.println("Question mark found");
+ DateFormat dateFormat = new SimpleDateFormat("_yyyyMMdd_HHmmss");
+ Date date = new Date();
+ String dateAndTime = dateFormat.format(date);
+ autfile = Conversion.replaceAllChar(graphPath, '?', dateAndTime);
+ //System.out.println("graphpath=" + graphPath);
+ } else {
+ autfile = graphPath;
+ }
+ System.out.println("graphpath=" + graphPath);
+
+ System.out.println("autfile=" + autfile);
+
+ try {
+ RG rg = new RG(autfile);
+ rg.data = graphAUT;
+ rg.fileName = autfile;
+ rg.nbOfStates = amc.getNbOfStates();
+ rg.nbOfTransitions = amc.getNbOfLinks();
+ System.out.println("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");
+ } catch (Exception e) {
+ System.out.println("Graph could not be saved in " + autfile + "\n");
+ }
}
return null;
diff --git a/src/main/java/cli/Interpreter.java b/src/main/java/cli/Interpreter.java
index e138246a96b73c396c94ccb17421bcea0fff44c6..5592462488e2f4c7a49a6006f8380ca30ed223d2 100644
--- a/src/main/java/cli/Interpreter.java
+++ b/src/main/java/cli/Interpreter.java
@@ -251,7 +251,7 @@ public class Interpreter implements Runnable, TerminalProviderInterface {
input = "";
} else {
varName = input.substring(0, indexSpace);
- input = input.substring(indexSpace + 1, input.length());
+ input = input.substring(indexSpace, input.length());
}
// Identifying variable
diff --git a/ttool/src/test/java/cli/CLIAvatarModelCheckerTest.java b/ttool/src/test/java/cli/CLIAvatarModelCheckerTest.java
index a26853fedc9aa10829571c8c6fef66192190aa24..3ce5bb50adf1559cacdcdc3e69d87d927ff4d18a 100644
--- a/ttool/src/test/java/cli/CLIAvatarModelCheckerTest.java
+++ b/ttool/src/test/java/cli/CLIAvatarModelCheckerTest.java
@@ -207,11 +207,28 @@ public class CLIAvatarModelCheckerTest extends AbstractTest implements Interpret
Interpreter interpret = new Interpreter(script, (InterpreterOutputInterface)this, show);
interpret.interpret();
+ // Must now load the graph
+ filePath = "rgmodelchecker.aut";
+ f = new File(filePath);
+ assertTrue(myutil.FileUtils.checkFileForOpen(f));
+ String data = myutil.FileUtils.loadFileData(f);
+
+ assertTrue(data.length() > 0);
+ AUTGraph graph = new AUTGraph();
+ graph.buildGraph(data);
+ graph.computeStates();
+
filePath = getBaseResourcesDir() + PATH_TO_EXPECTED_FILE + "modelchecker_s_expected";
f = new File(filePath);
assertTrue(myutil.FileUtils.checkFileForOpen(f));
String expectedOutput = myutil.FileUtils.loadFileData(f);
+ System.out.println("states=" + graph.getNbOfStates() + " transitions=" + graph.getNbOfTransitions());
+ assertTrue(graph.getNbOfStates() == 251);
+ assertTrue(graph.getNbOfTransitions() > 750);
+ assertTrue(graph.getNbOfTransitions() < 770);
+
+
assertEquals(expectedOutput, outputResult.toString());
}
@@ -229,15 +246,6 @@ public class CLIAvatarModelCheckerTest extends AbstractTest implements Interpret
assertTrue(script.length() > 0);
- //Load configuration for UPPAAL paths
- String config = "../../bin/config.xml";
- try {
- ConfigurationTTool.loadConfiguration(config, true);
- SpecConfigTTool.setBasicConfigFile(config);
- } catch (Exception e) {
- System.out.println("Error loading configuration from file: " + config);
- }
-
Interpreter interpret = new Interpreter(script, (InterpreterOutputInterface)this, false);
interpret.interpret();
@@ -245,7 +253,7 @@ public class CLIAvatarModelCheckerTest extends AbstractTest implements Interpret
}
@Test
- public void testValidateAirbusDoor_V2 () {
+ public void testValidateAirbusDoor_V2() {
String filePath = getBaseResourcesDir() + PATH_TO_TEST_FILE + "scriptmodelchecker_val2";
String script;
@@ -258,15 +266,6 @@ public class CLIAvatarModelCheckerTest extends AbstractTest implements Interpret
assertTrue(script.length() > 0);
- //Load configuration for UPPAAL paths
- String config = "../../bin/config.xml";
- try {
- ConfigurationTTool.loadConfiguration(config, true);
- SpecConfigTTool.setBasicConfigFile(config);
- } catch (Exception e) {
- System.out.println("Error loading configuration from file: " + config);
- }
-
Interpreter interpret = new Interpreter(script, (InterpreterOutputInterface)this, false);
interpret.interpret();
@@ -274,7 +273,7 @@ public class CLIAvatarModelCheckerTest extends AbstractTest implements Interpret
}
@Test
- public void testValidatePressureController_V2 () {
+ public void testValidatePressureController_V2() {
String filePath = getBaseResourcesDir() + PATH_TO_TEST_FILE + "scriptmodelchecker_val3";
String script;
@@ -287,19 +286,35 @@ public class CLIAvatarModelCheckerTest extends AbstractTest implements Interpret
assertTrue(script.length() > 0);
- //Load configuration for UPPAAL paths
- String config = "../../bin/config.xml";
- try {
- ConfigurationTTool.loadConfiguration(config, true);
- SpecConfigTTool.setBasicConfigFile(config);
- } catch (Exception e) {
- System.out.println("Error loading configuration from file: " + config);
- }
-
Interpreter interpret = new Interpreter(script, (InterpreterOutputInterface)this, false);
interpret.interpret();
assertTrue(outputResult.toString().contains("true"));
}
+
+ @Test
+ public void testCliCustomQuery () {
+ String filePath = getBaseResourcesDir() + PATH_TO_TEST_FILE + "scriptmodelchecker_q";
+ String script;
+
+ outputResult = new StringBuilder();
+
+ File f = new File(filePath);
+ assertTrue(myutil.FileUtils.checkFileForOpen(f));
+
+ script = myutil.FileUtils.loadFileData(f);
+
+ assertTrue(script.length() > 0);
+
+ Interpreter interpret = new Interpreter(script, (InterpreterOutputInterface)this, false);
+ interpret.interpret();
+
+ filePath = getBaseResourcesDir() + PATH_TO_EXPECTED_FILE + "modelchecker_q_expected";
+ f = new File(filePath);
+ assertTrue(myutil.FileUtils.checkFileForOpen(f));
+ String expectedOutput = myutil.FileUtils.loadFileData(f);
+
+ assertEquals(expectedOutput, outputResult.toString()+"\n");
+ }
}
diff --git a/ttool/src/test/resources/cli/expected/modelchecker_q_expected b/ttool/src/test/resources/cli/expected/modelchecker_q_expected
new file mode 100644
index 0000000000000000000000000000000000000000..16e0f75a1065479e4ce7e7fc479e681766ac5418
--- /dev/null
+++ b/ttool/src/test/resources/cli/expected/modelchecker_q_expected
@@ -0,0 +1,4 @@
+Safety Analysis:
+DoorAndLockButton.inside == 0 --> DoorAndLockButton.inside>0 -> property is NOT satisfied
+E<> Passenger.isInCockpit ==true&&DoorAndLockButton.inside==1 -> property is satisfied
+All done. See you soon.
diff --git a/ttool/src/test/resources/cli/input/scriptmodelchecker b/ttool/src/test/resources/cli/input/scriptmodelchecker
index 143766fcf45e962d280ec103ff8e5ee3e1f98eb7..56d193955eddf5cd15494475cd1f06ed5fb1cb25 100644
--- a/ttool/src/test/resources/cli/input/scriptmodelchecker
+++ b/ttool/src/test/resources/cli/input/scriptmodelchecker
@@ -7,5 +7,5 @@ wait 2
action open $model
wait 4
action check-syntax
-action avatar-rg rgmodelchecker.aut
+action avatar-rg -g rgmodelchecker.aut
action quit
diff --git a/ttool/src/test/resources/cli/input/scriptmodelchecker_n b/ttool/src/test/resources/cli/input/scriptmodelchecker_n
index 04e36bc95fde62569d22b3ea6c5a88675683ce61..71c70fdae15b78bf045e5313871ecadee89cf530 100644
--- a/ttool/src/test/resources/cli/input/scriptmodelchecker_n
+++ b/ttool/src/test/resources/cli/input/scriptmodelchecker_n
@@ -7,5 +7,5 @@ wait 2
action open $model
wait 4
action check-syntax
-action avatar-rg -n 12 rgmodelchecker.aut
+action avatar-rg -n 12 -g rgmodelchecker.aut
action quit
diff --git a/ttool/src/test/resources/cli/input/scriptmodelchecker_q b/ttool/src/test/resources/cli/input/scriptmodelchecker_q
new file mode 100644
index 0000000000000000000000000000000000000000..ceb06cc27cb56dcb69e054ea38f12b47aa598433
--- /dev/null
+++ b/ttool/src/test/resources/cli/input/scriptmodelchecker_q
@@ -0,0 +1,12 @@
+print dir
+set model resources/test/cli/models/AirbusDoor_V2.xml
+set query "DoorAndLockButton.inside == 0 --> DoorAndLockButton.inside>0, E<> Passenger.isInCockpit ==true&&DoorAndLockButton.inside==1"
+#print The model to be opened is: $model
+action start
+wait 2
+#toto
+action open $model
+wait 4
+action check-syntax
+action avatar-rg -q $query
+action quit
diff --git a/ttool/src/test/resources/cli/input/scriptmodelchecker_rl b/ttool/src/test/resources/cli/input/scriptmodelchecker_rl
index 86e99ddff2163e203f142433414e7b20202eb475..1fb6735fb188e93b4d34e8f4e58abb85bfcc4570 100644
--- a/ttool/src/test/resources/cli/input/scriptmodelchecker_rl
+++ b/ttool/src/test/resources/cli/input/scriptmodelchecker_rl
@@ -7,5 +7,5 @@ wait 2
action open $model
wait 4
action check-syntax
-action avatar-rg -ra -la -d rgmodelchecker.aut
+action avatar-rg -ra -la -d -g rgmodelchecker.aut
action quit
diff --git a/ttool/src/test/resources/cli/input/scriptmodelchecker_s b/ttool/src/test/resources/cli/input/scriptmodelchecker_s
index b55abc668c8f575c1d807be1070acfb7111c551a..ac0993faa5b64d367c6f0d0e72454a2d62062664 100644
--- a/ttool/src/test/resources/cli/input/scriptmodelchecker_s
+++ b/ttool/src/test/resources/cli/input/scriptmodelchecker_s
@@ -7,5 +7,5 @@ wait 2
action open $model
wait 4
action check-syntax
-action avatar-rg -d -ra -la -s rgmodelchecker.aut
+action avatar-rg -d -ra -la -s -g rgmodelchecker.aut
action quit