Added model-checker tests for liveness, reachability and state limit

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";

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";
+        
+    }
 
 }

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

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());
+    }
 
 }

ttool/src/test/resources/cli/input/modelchecker_rl_expected

+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

ttool/src/test/resources/cli/input/scriptmodelchecker_rl

+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

ttool/src/test/resources/cli/input/scriptmodelchecker_sl

+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