Added tests for model-checker

src/main/java/avatartranslator/modelchecker/SafetyProperty.java

@@ -227,13 +227,13 @@ public class SafetyProperty  {
         String name = "Element " + state.getExtendedName() + " of block " + block.getName();
         switch(phase) {
         case NOTCOMPUTED:
-            name += rawProperty + " -> liveness not computed";
+            name += " -> liveness not computed";
             break;
         case SATISFIED:
-            name += rawProperty + " -> liveness is satisfied";
+            name += " -> liveness is satisfied";
             break;
         case NONSATISFIED:
-            name += rawProperty + " -> liveness is NOT satisfied"; 
+            name += " -> liveness is NOT satisfied"; 
             break;
         }
         return name;

src/main/java/cli/Action.java

@@ -591,7 +591,9 @@ public class Action extends Command {
                     + "-ra\treachability of all states\n"
                     + "-l, ls\tliveness of all states\n"
                     + "-la\tliveness of all states\n"
-                    + "-s NUM\t maximum states created\n"
+                    + "-s safety pragmas verification\n"
+                    + "-d no deadlocks verification\n"
+                    + "-n NUM\t maximum states created\n"
                     + "-t NUM\t maximum time (ms)\n";
             }
 
@@ -625,6 +627,8 @@ public class Action extends Command {
                 amc.setComputeRG(true);
                 boolean reachabilityAnalysis = false;
                 boolean livenessAnalysis = false;
+                boolean safetyAnalysis = false;
+                boolean noDeadlocks = false;
                 for (int i = 0; i < commands.length - 1; i++) {
                     //specification
                     switch (commands[i]) {
@@ -651,6 +655,16 @@ public class Action extends Command {
                             livenessAnalysis = true;
                             break;
                         case "-s":
+                            //safety
+                            amc.setSafetyAnalysis();
+                            safetyAnalysis = true;
+                            break;
+                        case "-d":
+                            //safety
+                            amc.setCheckNoDeadlocks(true);
+                            noDeadlocks = true;
+                            break;
+                        case "-n":
                             //state limit followed by a number
                             long states;
                             try {
@@ -677,7 +691,7 @@ public class Action extends Command {
                     }
                 }
                 TraceManager.addDev("Starting model checking");
-                if (livenessAnalysis) {
+                if (livenessAnalysis || safetyAnalysis) {
                     amc.startModelCheckingProperties();
                 } else {
                     amc.startModelChecking();
@@ -685,12 +699,18 @@ public class Action extends Command {
                 
                 System.out.println("Model checking done\nGraph: states:" + amc.getNbOfStates() +
                         " links:" + amc.getNbOfLinks() + "\n");
+                if (noDeadlocks) {
+                    interpreter.print("No Deadlocks:\n" + amc.deadlockToString());
+                }
                 if (reachabilityAnalysis) {
                     interpreter.print("Reachability Analysis:\n" + amc.reachabilityToStringGeneric());
                 }
                 if (livenessAnalysis) {
                     interpreter.print("Liveness Analysis:\n" + amc.livenessToString());
                 }
+                if (safetyAnalysis) {
+                    interpreter.print("Safety Analysis:\n" + amc.safetyToString());
+                }
 
                 // Saving graph
                 String graphAUT = amc.toAUT();

ttool/src/test/java/cli/CLIAvatarModelCheckerTest.java

@@ -126,7 +126,7 @@ public class CLIAvatarModelCheckerTest extends AbstractTest implements Interpret
 	
 	@Test
     public void testStateLimitCoffeeMachine() {
-        String filePath = getBaseResourcesDir() + PATH_TO_TEST_FILE + "scriptmodelchecker_sl";
+        String filePath = getBaseResourcesDir() + PATH_TO_TEST_FILE + "scriptmodelchecker_n";
         String script;
         
         outputResult = new StringBuilder();
@@ -196,5 +196,31 @@ public class CLIAvatarModelCheckerTest extends AbstractTest implements Interpret
         assertTrue(graph.getNbOfTransitions() == 16);
         assertEquals(expectedOutput, outputResult.toString());
     }
+	
+	@Test
+    public void testReachabilityLivenessSafetyAirbusDoor_V2() {
+        String filePath = getBaseResourcesDir() + PATH_TO_TEST_FILE + "scriptmodelchecker_s";
+        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();
+        
+        filePath = getBaseResourcesDir() + PATH_TO_TEST_FILE + "modelchecker_s_expected";
+        f = new File(filePath);
+        assertTrue(myutil.FileUtils.checkFileForOpen(f));
+        String expectedOutput = myutil.FileUtils.loadFileData(f);
+
+        assertEquals(expectedOutput, outputResult.toString());
+    }
 
 }

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

+No Deadlocks:
+property is not satisfied
 Reachability Analysis:
 1. Element start of block Wallet -> reachable
 2. Element main of block Wallet -> reachable

ttool/src/test/resources/cli/input/modelchecker_s_expected

+No Deadlocks:
+property is satisfied
+Reachability Analysis:
+1. Element start of block DoorAndLockButton -> reachable
+2. Element CLOSED_AND_LOCKED of block DoorAndLockButton -> reachable
+3. Element action_on_signal__clone:unlock of block DoorAndLockButton -> reachable
+4. Element CLOSED_AND_UNLOCKED of block DoorAndLockButton -> reachable
+5. Element action_on_signal__clone:lock of block DoorAndLockButton -> reachable
+6. Element action_on_signal__clone:open of block DoorAndLockButton -> reachable
+7. Element OPENED of block DoorAndLockButton -> reachable
+8. Element action_on_signal__clone:leaveCockpit of block DoorAndLockButton -> reachable
+9. Element action_on_signal__clone:close of block DoorAndLockButton -> reachable
+10. Element action_on_signal__clone:enterCockpit of block DoorAndLockButton -> reachable
+11. Element LOCKED_EMPTY_COCKPIT of block DoorAndLockButton -> NOT reachable
+12. Element action_on_signal__clone:emergencyCall of block DoorAndLockButton -> reachable
+13. Element IN_EMERGENCY_CALL of block DoorAndLockButton -> reachable
+14. Element action_on_signal__clone:lock of block DoorAndLockButton -> reachable
+15. Element start of block OnboardPersons -> reachable
+16. Element start of block Captain -> reachable
+17. Element stop of block Captain -> NOT reachable
+18. Element start of block Crew -> reachable
+19. Element stop of block Crew -> NOT reachable
+20. Element start of block Passenger -> reachable
+21. Element stop of block Passenger -> NOT reachable
+22. Element start of block FirstOfficer -> reachable
+23. Element stop of block FirstOfficer -> NOT reachable
+Liveness Analysis:
+1. Element start of block DoorAndLockButton -> liveness is satisfied
+2. Element CLOSED_AND_LOCKED of block DoorAndLockButton -> liveness is satisfied
+3. Element action_on_signal__clone:unlock of block DoorAndLockButton -> liveness is NOT satisfied
+4. Element CLOSED_AND_UNLOCKED of block DoorAndLockButton -> liveness is NOT satisfied
+5. Element action_on_signal__clone:lock of block DoorAndLockButton -> liveness is NOT satisfied
+6. Element action_on_signal__clone:open of block DoorAndLockButton -> liveness is NOT satisfied
+7. Element OPENED of block DoorAndLockButton -> liveness is NOT satisfied
+8. Element action_on_signal__clone:leaveCockpit of block DoorAndLockButton -> liveness is NOT satisfied
+9. Element action_on_signal__clone:close of block DoorAndLockButton -> liveness is NOT satisfied
+10. Element action_on_signal__clone:enterCockpit of block DoorAndLockButton -> liveness is NOT satisfied
+11. Element LOCKED_EMPTY_COCKPIT of block DoorAndLockButton -> liveness is NOT satisfied
+12. Element action_on_signal__clone:emergencyCall of block DoorAndLockButton -> liveness is NOT satisfied
+13. Element IN_EMERGENCY_CALL of block DoorAndLockButton -> liveness is NOT satisfied
+14. Element action_on_signal__clone:lock of block DoorAndLockButton -> liveness is NOT satisfied
+15. Element start of block OnboardPersons -> liveness is satisfied
+16. Element start of block Captain -> liveness is satisfied
+17. Element stop of block Captain -> liveness is NOT satisfied
+18. Element start of block Crew -> liveness is satisfied
+19. Element stop of block Crew -> liveness is NOT satisfied
+20. Element start of block Passenger -> liveness is satisfied
+21. Element stop of block Passenger -> liveness is NOT satisfied
+22. Element start of block FirstOfficer -> liveness is satisfied
+23. Element stop of block FirstOfficer -> liveness is NOT satisfied
+Safety Analysis:
+E<> Passenger.isInCockpit ==true&&DoorAndLockButton.inside==1 -> property is satisfied
+E<> DoorAndLockButton.LOCKED_EMPTY_COCKPIT -> property is NOT satisfied
+DoorAndLockButton.CLOSED_AND_LOCKED --> DoorAndLockButton.CLOSED_AND_UNLOCKED -> property is NOT satisfied
+DoorAndLockButton.inside == 0 --> DoorAndLockButton.inside>0 -> property is NOT satisfied
+DoorAndLockButton.IN_EMERGENCY_CALL --> DoorAndLockButton.CLOSED_AND_UNLOCKED -> property is NOT satisfied
+DoorAndLockButton.IN_EMERGENCY_CALL --> DoorAndLockButton.CLOSED_AND_UNLOCKED -> property is NOT satisfied
+DoorAndLockButton.IN_EMERGENCY_CALL --> DoorAndLockButton.CLOSED_AND_LOCKED || DoorAndLockButton.CLOSED_AND_UNLOCKED -> property is satisfied
+All done. See you soon.
\ No newline at end of file

ttool/src/test/resources/cli/input/scriptmodelchecker_sl → 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 -s 12 rgmodelchecker.aut
+action avatar-rg -n 12 rgmodelchecker.aut
 action quit

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 rgmodelchecker.aut
+action avatar-rg -ra -la -d rgmodelchecker.aut
 action quit

ttool/src/test/resources/cli/input/scriptmodelchecker_s

+print dir
+set model resources/test/cli/input/AirbusDoor_V2.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 -d -ra -la -s rgmodelchecker.aut
+action quit