diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index ec7747e11cddf5751959b380f4982c97873b760e..a3b9ea5c6c8ee581f5a4959002d1fe6c5d91bb3c 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -1696,6 +1696,25 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
return ret.toString();
}
+ public String reachabilityToStringGeneric() {
+ if (!studyReachability) {
+ return "Reachability not activated";
+ }
+
+
+ StringBuilder ret = new StringBuilder();
+ if (stoppedBeforeEnd) {
+ ret.append("Beware: Full study of reachability might not have been fully completed\n");
+ }
+
+ int cpt = 0;
+ for (SpecificationReachability re : reachabilities) {
+ ret.append((cpt + 1) + ". " + re.toStringGeneric() + "\n");
+ cpt++;
+ }
+ return ret.toString();
+ }
+
public String livenessToString() {
if (!studyLiveness) {
return "Liveness not activated";
diff --git a/src/main/java/avatartranslator/modelchecker/SpecificationReachability.java b/src/main/java/avatartranslator/modelchecker/SpecificationReachability.java
index 438c948bf242ed1b6cf62490d9e7c58c3c005f93..c10ed9a43c097a6e1f3cdacf3ddb8e41222fd179 100644
--- a/src/main/java/avatartranslator/modelchecker/SpecificationReachability.java
+++ b/src/main/java/avatartranslator/modelchecker/SpecificationReachability.java
@@ -92,5 +92,34 @@ public class SpecificationReachability {
return name + " -> NOT reachable";
}
+
+ public String toStringGeneric() {
+ String name;
+ if (ref1 instanceof AvatarStateMachineElement) {
+ name = "Element " + ((AvatarStateMachineElement)ref1).getExtendedName();
+ } else {
+ name = ref1.toString();
+ }
+
+ if (ref2 != null) {
+ if (ref2 instanceof AvatarBlock) {
+ name += " of block " + ((AvatarBlock)ref2).getName();
+ } else {
+ name += ref2.toString();
+ }
+ }
+
+
+ if (result == SpecificationReachabilityType.NOTCOMPUTED) {
+ return name + " -> not computed";
+ }
+
+ if (result == SpecificationReachabilityType.REACHABLE) {
+ return name + " -> reachable";
+ }
+
+ return name + " -> NOT reachable";
+
+ }
}
diff --git a/src/main/java/cli/Action.java b/src/main/java/cli/Action.java
index d12eb477225315068bedac2cf16defe1c76613b1..c93d6e5bba05a836d0357fffaae764d3e2c4f9b0 100644
--- a/src/main/java/cli/Action.java
+++ b/src/main/java/cli/Action.java
@@ -686,10 +686,10 @@ public class Action extends Command {
System.out.println("Model checking done\nGraph: states:" + amc.getNbOfStates() +
" links:" + amc.getNbOfLinks() + "\n");
if (reachabilityAnalysis) {
- System.out.println("\nReachability Analysis:" + amc.reachabilityToString());
+ interpreter.print("Reachability Analysis:\n" + amc.reachabilityToStringGeneric());
}
if (livenessAnalysis) {
- System.out.println("\nLiveness Analysis:" + amc.livenessToString());
+ interpreter.print("Liveness Analysis:\n" + amc.livenessToString());
}
// Saving graph
diff --git a/ttool/src/test/java/cli/CLIAvatarModelCheckerTest.java b/ttool/src/test/java/cli/CLIAvatarModelCheckerTest.java
index 82e83254c4415fc4efd0a17fc68a9eb1f8902283..dde48015fc4ef4bc444dc608034816a173596c0c 100644
--- a/ttool/src/test/java/cli/CLIAvatarModelCheckerTest.java
+++ b/ttool/src/test/java/cli/CLIAvatarModelCheckerTest.java
@@ -66,10 +66,11 @@ import ui.avatarbd.AvatarBDPragma;
public class CLIAvatarModelCheckerTest extends AbstractTest implements InterpreterOutputInterface {
- final static String PATH_TO_TEST_FILE = "/cli/input/";
+ final static String PATH_TO_TEST_FILE = "cli/input/";
+ private StringBuilder outputResult;
public CLIAvatarModelCheckerTest() {
- //
+ //
}
@@ -84,12 +85,15 @@ public class CLIAvatarModelCheckerTest extends AbstractTest implements Interpret
public void print(String s) {
System.out.println("info from interpreter:" + s);
+ outputResult.append(s);
}
@Test
public void testCoffeeMachine() {
String filePath = getBaseResourcesDir() + PATH_TO_TEST_FILE + "scriptmodelchecker";
String script;
+
+ outputResult = new StringBuilder();
File f = new File(filePath);
assertTrue(myutil.FileUtils.checkFileForOpen(f));
@@ -120,5 +124,77 @@ public class CLIAvatarModelCheckerTest extends AbstractTest implements Interpret
}
+ @Test
+ public void testStateLimitCoffeeMachine() {
+ String filePath = getBaseResourcesDir() + PATH_TO_TEST_FILE + "scriptmodelchecker_sl";
+ String script;
+
+ outputResult = new StringBuilder();
+
+ File f = new File(filePath);
+ assertTrue(myutil.FileUtils.checkFileForOpen(f));
+
+ script = myutil.FileUtils.loadFileData(f);
+
+ assertTrue(script.length() > 0);
+
+ boolean show = false;
+ 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();
+
+ System.out.println("states=" + graph.getNbOfStates() + " transitions=" + graph.getNbOfTransitions());
+ assertTrue(graph.getNbOfStates() == 12);
+ }
+
+ @Test
+ public void testReachabilityLivenessCoffeeMachine() {
+ String filePath = getBaseResourcesDir() + PATH_TO_TEST_FILE + "scriptmodelchecker_rl";
+ String script;
+
+ outputResult = new StringBuilder();
+
+ File f = new File(filePath);
+ assertTrue(myutil.FileUtils.checkFileForOpen(f));
+
+ script = myutil.FileUtils.loadFileData(f);
+
+ assertTrue(script.length() > 0);
+
+ boolean show = false;
+ 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_TEST_FILE + "modelchecker_rl_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() == 14);
+ assertTrue(graph.getNbOfTransitions() == 16);
+ assertEquals(expectedOutput, outputResult.toString());
+ }
}
diff --git a/ttool/src/test/resources/cli/input/modelchecker_rl_expected b/ttool/src/test/resources/cli/input/modelchecker_rl_expected
new file mode 100644
index 0000000000000000000000000000000000000000..400fd63f64b8a9a313db82567e11dad435029920
--- /dev/null
+++ b/ttool/src/test/resources/cli/input/modelchecker_rl_expected
@@ -0,0 +1,41 @@
+Reachability Analysis:
+1. Element start of block Wallet -> reachable
+2. Element main of block Wallet -> reachable
+3. Element action_on_signal__clone:getCoin of block Wallet -> reachable
+4. Element start of block CoffeeMachine -> reachable
+5. Element WaitingForFirstCoin of block CoffeeMachine -> reachable
+6. Element action_on_signal__clone:getCoin of block CoffeeMachine -> reachable
+7. Element WaitingForSecondCoin of block CoffeeMachine -> reachable
+8. Element ejectState of block CoffeeMachine -> reachable
+9. Element action_on_signal__clone:getCoin of block CoffeeMachine -> reachable
+10. Element Beverage of block CoffeeMachine -> reachable
+11. Element WaitingForSelection of block CoffeeMachine -> reachable
+12. Element action_on_signal__clone:ejectCoin of block CoffeeMachine -> NOT reachable
+13. Element action_on_signal__clone:pushCoffeeButton of block CoffeeMachine -> reachable
+14. Element action_on_signal__clone:pushTeaButton of block CoffeeMachine -> reachable
+15. Element start of block CoffeeButton -> reachable
+16. Element main of block CoffeeButton -> reachable
+17. Element state0 of block CoffeeButton -> reachable
+18. Element start of block TeaButton -> reachable
+19. Element main of block TeaButton -> reachable
+Liveness Analysis:
+1. Element start of block Wallet -> liveness is satisfied
+2. Element main of block Wallet -> liveness is satisfied
+3. Element action_on_signal__clone:getCoin of block Wallet -> liveness is NOT satisfied
+4. Element start of block CoffeeMachine -> liveness is satisfied
+5. Element WaitingForFirstCoin of block CoffeeMachine -> liveness is satisfied
+6. Element action_on_signal__clone:getCoin of block CoffeeMachine -> liveness is satisfied
+7. Element WaitingForSecondCoin of block CoffeeMachine -> liveness is satisfied
+8. Element ejectState of block CoffeeMachine -> liveness is NOT satisfied
+9. Element action_on_signal__clone:getCoin of block CoffeeMachine -> liveness is NOT satisfied
+10. Element Beverage of block CoffeeMachine -> liveness is NOT satisfied
+11. Element WaitingForSelection of block CoffeeMachine -> liveness is NOT satisfied
+12. Element action_on_signal__clone:ejectCoin of block CoffeeMachine -> liveness is NOT satisfied
+13. Element action_on_signal__clone:pushCoffeeButton of block CoffeeMachine -> liveness is NOT satisfied
+14. Element action_on_signal__clone:pushTeaButton of block CoffeeMachine -> liveness is NOT satisfied
+15. Element start of block CoffeeButton -> liveness is satisfied
+16. Element main of block CoffeeButton -> liveness is satisfied
+17. Element state0 of block CoffeeButton -> liveness is satisfied
+18. Element start of block TeaButton -> liveness is satisfied
+19. Element main of block TeaButton -> liveness is satisfied
+All done. See you soon.
\ No newline at end of file
diff --git a/ttool/src/test/resources/cli/input/scriptmodelchecker_rl b/ttool/src/test/resources/cli/input/scriptmodelchecker_rl
new file mode 100644
index 0000000000000000000000000000000000000000..5685cfbb355ab5a7f74a583d025b1235974fde96
--- /dev/null
+++ b/ttool/src/test/resources/cli/input/scriptmodelchecker_rl
@@ -0,0 +1,11 @@
+print dir
+set model resources/test/cli/input/CoffeeMachine_Avatar.xml
+#print The model to be opened is: $model
+action start
+wait 2
+#toto
+action open $model
+wait 4
+action check-syntax
+action avatar-rg -ra -la rgmodelchecker.aut
+action quit
diff --git a/ttool/src/test/resources/cli/input/scriptmodelchecker_sl b/ttool/src/test/resources/cli/input/scriptmodelchecker_sl
new file mode 100644
index 0000000000000000000000000000000000000000..7ebea001869fe3b0291227ca3330227483e30c7f
--- /dev/null
+++ b/ttool/src/test/resources/cli/input/scriptmodelchecker_sl
@@ -0,0 +1,11 @@
+print dir
+set model resources/test/cli/input/CoffeeMachine_Avatar.xml
+#print The model to be opened is: $model
+action start
+wait 2
+#toto
+action open $model
+wait 4
+action check-syntax
+action avatar-rg -s 12 rgmodelchecker.aut
+action quit