diff --git a/src/main/java/avatartranslator/modelcheckercompare/CompareToUppaal.java b/src/main/java/avatartranslator/modelcheckervalidator/ModelCheckerValidator.java
similarity index 78%
rename from src/main/java/avatartranslator/modelcheckercompare/CompareToUppaal.java
rename to src/main/java/avatartranslator/modelcheckervalidator/ModelCheckerValidator.java
index 322f8c760b1aa93c4d1c048ab6bbedb690ce2b15..eb5bd788afc897ba03b2fbe9075b5069fd4a0760 100644
--- a/src/main/java/avatartranslator/modelcheckercompare/CompareToUppaal.java
+++ b/src/main/java/avatartranslator/modelcheckervalidator/ModelCheckerValidator.java
@@ -36,12 +36,14 @@
* knowledge of the CeCILL license and that you accept its terms.
*/
-package avatartranslator.modelcheckercompare;
+package avatartranslator.modelcheckervalidator;
import java.io.File;
import java.util.ArrayList;
import java.util.Collection;
import java.util.HashSet;
+import java.util.Map;
+
import launcher.LauncherException;
import launcher.RshClient;
import rationals.properties.isEmpty;
@@ -50,23 +52,27 @@ import ui.MainGUI;
import ui.TGComponent;
import ui.TGComponentAndUPPAALQuery;
import ui.TURTLEPanel;
+import uppaaldesc.UPPAALSpec;
+import uppaaldesc.UPPAALTemplate;
+import avatartranslator.AvatarBlock;
import avatartranslator.AvatarSpecification;
import avatartranslator.AvatarStateMachineElement;
import avatartranslator.modelchecker.AvatarModelChecker;
import avatartranslator.modelchecker.SafetyProperty;
import avatartranslator.modelchecker.SpecificationPropertyPhase;
import avatartranslator.modelchecker.SpecificationReachability;
+import avatartranslator.touppaal.AVATAR2UPPAAL;
/**
- * Class CompareToUppaal
- * Compare To Uppaal
+ * Class ModelCheckerValidator
+ * Model-checker validator
* Creation: 05/05/2020
*
* @author Alessandro TEMPIA CALVINO
* @version 1.0 05/05/2020
*/
-public class CompareToUppaal {
+public class ModelCheckerValidator {
public final static int STUDY_SELECTED = 1;
public final static int STUDY_ALL = 2;
@@ -105,7 +111,7 @@ public class CompareToUppaal {
* Starts the internal Avatar model-checker and UPPAAL. It verifies that the results are the same.
* Returns true if the results are equal or UPPAAL is not installed. Returns false if the results are different.
*/
- public static boolean compareToUppaal(MainGUI mgui, int rStudy, int lStudy, boolean sStudy, boolean dStudy) {
+ public static boolean validate(MainGUI mgui, int rStudy, int lStudy, boolean sStudy, boolean dStudy) {
GTURTLEModeling gtm = mgui.gtm;
TURTLEPanel tp = mgui.getCurrentTURTLEPanel();
@@ -161,6 +167,7 @@ public class CompareToUppaal {
//run UPPAAL
StringBuilder diff = new StringBuilder();
+ boolean equal = true;
try {
id = rshc.getId();
fn = fileName.substring(0, fileName.length() - 4) + "_" + id;
@@ -174,6 +181,7 @@ public class CompareToUppaal {
uResult = workQuery(gtm, rshc, "A[] not deadlock", fn);
if (!((uResult == 0 && amc.getNbOfDeadlocks() > 0) || (uResult == 1 && amc.getNbOfDeadlocks() == 0))) {
diff.append("No Deadlock: amc = " + (amc.getNbOfDeadlocks() == 0) + "; uppaal = " + (uResult == 1) + "\n");
+ equal = false;
}
}
@@ -199,14 +207,15 @@ public class CompareToUppaal {
if (!(uResult == 1 && sr.result == SpecificationPropertyPhase.SATISFIED ||
uResult == 0 && sr.result == SpecificationPropertyPhase.NONSATISFIED)) {
diff.append("Reachability " + ((AvatarStateMachineElement)sr.ref1).getExtendedName() + ": amc = " + (sr.result == SpecificationPropertyPhase.SATISFIED) + "; uppaal = " + (uResult == 1) + "\n");
- break;
+ equal = false;
}
+ break;
}
}
}
}
if (!match) {
- //diff.append("Reachability query " + s + " not matched\n");
+ diff.append("Reachability query " + s + " not matched\n");
}
}
}
@@ -233,36 +242,49 @@ public class CompareToUppaal {
if (!(uResult == 1 && sp.getPhase() == SpecificationPropertyPhase.SATISFIED ||
uResult == 0 && sp.getPhase() == SpecificationPropertyPhase.NONSATISFIED)) {
diff.append("Liveness " + sp.getState().getExtendedName() + ": amc = " + (sp.getPhase() == SpecificationPropertyPhase.SATISFIED) + "; uppaal = " + (uResult == 1) + "\n");
- break;
+ equal = false;
}
+ break;
}
}
}
if (!match) {
- //diff.append("Liveness query " + s + " not matched\n");
+ diff.append("Liveness query " + s + " not matched\n");
}
}
}
+ }
+
+ if (sStudy) {
+ ArrayList<SafetyProperty> safeties = amc.getSafeties();
+ for (SafetyProperty sp : safeties) {
+ query = translateCustomQuery(gtm, spec, sp.getRawProperty());
+ uResult = workQuery(gtm, rshc, query, fn);
+ if (!(uResult == 1 && sp.getPhase() == SpecificationPropertyPhase.SATISFIED ||
+ uResult == 0 && sp.getPhase() == SpecificationPropertyPhase.NONSATISFIED)) {
+ diff.append("Safety " + sp.getRawProperty() + ": amc = " + (sp.getPhase() == SpecificationPropertyPhase.SATISFIED) + "; uppaal = " + (uResult == 1) + "\n");
+ equal = false;
+ }
+ }
- rshc.deleteFile(fn + ".xml");
- rshc.deleteFile(fn + ".q");
- rshc.deleteFile(fn + ".res");
- rshc.deleteFile(fn + ".xtr");
-
- rshc.freeId(id);
}
+
+ rshc.deleteFile(fn + ".xml");
+ rshc.deleteFile(fn + ".q");
+ rshc.deleteFile(fn + ".res");
+ rshc.deleteFile(fn + ".xtr");
+
+ rshc.freeId(id);
} catch (Exception e) {
System.out.println("Shit: " + e + "\n");
return false;
}
- if (diff.length() == 0) {
- return true;
- } else {
- //report diff
+ if (diff.length() != 0) {
System.out.println("Avatar-UPPAAL Compare diff:\n" + diff);
- return false;
}
+
+ return equal;
}
@@ -338,6 +360,51 @@ public class CompareToUppaal {
}
return false;
}
-
+
+
+ private static String translateCustomQuery(GTURTLEModeling gtm, AvatarSpecification avspec, String query) {
+ UPPAALSpec spec = gtm.getLastUPPAALSpecification();
+ AVATAR2UPPAAL avatar2uppaal = gtm.getAvatar2Uppaal();
+ Map<String, String> hash = avatar2uppaal.getHash();
+ String finQuery = query + " ";
+
+ for (String str : hash.keySet()) {
+ finQuery = finQuery.replaceAll(str + "\\s", hash.get(str));
+ finQuery = finQuery.replaceAll(str + "\\)", hash.get(str) + "\\)");
+ finQuery = finQuery.replaceAll(str + "\\-", hash.get(str) + "\\-");
+ }
+
+ if (avspec == null) {
+ return "";
+ }
+
+ java.util.List<AvatarBlock> blocks = avspec.getListOfBlocks();
+ java.util.List<String> matches = new java.util.ArrayList<String>();
+ for (AvatarBlock block : blocks) {
+ UPPAALTemplate temp = spec.getTemplateByName(block.getName());
+ if (temp != null) {
+ if (finQuery.contains(block.getName() + ".")) {
+ matches.add(block.getName());
+ }
+ }
+ }
+
+
+ for (String match : matches) {
+ boolean ignore = false;
+ for (String posStrings : matches) {
+ if (!posStrings.equals(match) && posStrings.contains(match)) {
+ ignore = true;
+ }
+ }
+ if (!ignore) {
+ UPPAALTemplate temp = spec.getTemplateByName(match);
+ int index = avatar2uppaal.getIndexOfTranslatedTemplate(temp);
+ finQuery = finQuery.replaceAll(match, match + "__" + index);
+ }
+ }
+
+ return finQuery;
+ }
}
diff --git a/src/main/java/cli/Action.java b/src/main/java/cli/Action.java
index c20766186cf2d586f9670521ad25e24f9215926c..9b7ecf52b124593e69729580b83d6d531afb76ac 100644
--- a/src/main/java/cli/Action.java
+++ b/src/main/java/cli/Action.java
@@ -41,7 +41,7 @@ package cli;
import avatartranslator.AvatarSpecification;
import avatartranslator.modelchecker.AvatarModelChecker;
-import avatartranslator.modelcheckercompare.CompareToUppaal;
+import avatartranslator.modelcheckervalidator.ModelCheckerValidator;
import common.ConfigurationTTool;
import common.SpecConfigTTool;
import graph.RG;
@@ -91,7 +91,7 @@ public class Action extends Command {
private final static String NAVIGATE_LEFT_PANEL = "navigate-left-panel";
private final static String AVATAR_RG_GENERATION = "avatar-rg";
- private final static String AVATAR_UPPAAL_COMPARE = "comp-uppaal";
+ private final static String AVATAR_UPPAAL_VALIDATE = "avatar-rg-validate";
public Action() {
@@ -591,10 +591,10 @@ 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 safety pragmas verification\n"
- + "-d no deadlocks verification\n"
- + "-n NUM\t maximum states created\n"
- + "-t NUM\t maximum time (ms)\n";
+ + "-s\tsafety pragmas verification\n"
+ + "-d\tno deadlocks verification\n"
+ + "-n NUM\tmaximum states created\n"
+ + "-t NUM\tmaximum time (ms)\n";
}
public String getExample() {
@@ -758,23 +758,29 @@ public class Action extends Command {
Command compareUppaal = new Command() {
public String getCommand() {
- return AVATAR_UPPAAL_COMPARE;
+ return AVATAR_UPPAAL_VALIDATE;
}
public String getShortCommand() {
- return "cup";
+ return "avg-val";
}
public String getDescription() {
- return "Compare the internal verification tool with uppaal";
+ return "Validate the internal verification tool with uppaal";
}
public String getUsage() {
- return "c-uppaal [UPPAAL PATH]";
+ return "avatar-rg-validate [OPTION]... [UPPAAL PATH]\n" +
+ "-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" +
+ "-d\tno deadlocks verification\n";
}
public String getExample() {
- return "comp-uppaal /packages/uppaal/";
+ return "avatar-rg-validate -ra -la -s -d /packages/uppaal/";
}
public String executeCommand(String command, Interpreter interpreter) {
@@ -783,23 +789,62 @@ public class Action extends Command {
}
String[] commands = command.split(" ");
- if (commands.length != 1) {
+ if (commands.length < 1) {
return Interpreter.BAD;
}
- String uppaalPath = commands[0];
+ //get args
+ String uppaalPath = commands[commands.length - 1];
+
+ int rStudy = 0;
+ int lStudy = 0;
+ boolean sStudy = false;
+ boolean dStudy = false;
+ for (int i = 0; i < commands.length - 1; i++) {
+ //specification
+ switch (commands[i]) {
+ case "-r":
+ case "-rs":
+ //reachability of selected states
+ rStudy = ModelCheckerValidator.STUDY_SELECTED;
+ break;
+ case "-ra":
+ //reachability of all states
+ rStudy = ModelCheckerValidator.STUDY_ALL;
+ break;
+ case "-l":
+ case "-ls":
+ //liveness of selected states
+ lStudy = ModelCheckerValidator.STUDY_SELECTED;
+ break;
+ case "-la":
+ //liveness of all states
+ lStudy = ModelCheckerValidator.STUDY_ALL;
+ break;
+ case "-s":
+ //safety
+ sStudy = true;
+ break;
+ case "-d":
+ //safety
+ dStudy = true;
+ break;
+ default:
+ return Interpreter.BAD;
+ }
+ }
//set configuration paths
ConfigurationTTool.UPPAALVerifierHost = "localhost";
ConfigurationTTool.UPPAALVerifierPath = uppaalPath + "/bin-Linux/verifyta";
ConfigurationTTool.UPPAALCodeDirectory = "../../uppaal/";
SpecConfigTTool.UPPAALCodeDirectory = ConfigurationTTool.UPPAALCodeDirectory;
-
+
interpreter.mgui.gtm.generateUPPAALFromAVATAR(SpecConfigTTool.UPPAALCodeDirectory);
- boolean res = CompareToUppaal.compareToUppaal(interpreter.mgui, 2, 2, false, true);
+ boolean res = ModelCheckerValidator.validate(interpreter.mgui, rStudy, lStudy, sStudy, dStudy);
- interpreter.print("comp-uppaal result: " + res);
+ interpreter.print("avatar-rg-validate result: " + res);
return null;
}
};
diff --git a/src/main/java/ui/window/JDialogAvatarModelChecker.java b/src/main/java/ui/window/JDialogAvatarModelChecker.java
index 5a30a1434db71b5ea33bffc5788e1a068f3a5985..7609c874cdc816e5e95d2a5b84aacf98b679af46 100644
--- a/src/main/java/ui/window/JDialogAvatarModelChecker.java
+++ b/src/main/java/ui/window/JDialogAvatarModelChecker.java
@@ -368,6 +368,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
if (spec.getSafetyPragmas() == null || spec.getSafetyPragmas().isEmpty()) {
safety.setEnabled(false);
+ safety.setSelected(false);
}
jpopt.add(jp01, c01);
diff --git a/ttool/src/test/java/cli/CLIAvatarModelCheckerTest.java b/ttool/src/test/java/cli/CLIAvatarModelCheckerTest.java
index f9222067b551c321fb6a6294d9decfd0ea7c6eaa..16917ccc638ebb6f7418b88308e46b1cf609d03c 100644
--- a/ttool/src/test/java/cli/CLIAvatarModelCheckerTest.java
+++ b/ttool/src/test/java/cli/CLIAvatarModelCheckerTest.java
@@ -47,25 +47,13 @@ package cli;
import static org.junit.Assert.assertEquals;
import static org.junit.Assert.assertTrue;
-
import java.io.File;
-import java.util.HashMap;
-import java.util.LinkedList;
-import java.util.List;
-import java.util.Map;
-
-import cli.Interpreter;
import common.ConfigurationTTool;
import common.SpecConfigTTool;
import graph.AUTGraph;
-import org.junit.Before;
import org.junit.Test;
-
-import avatartranslator.modelcheckercompare.CompareToUppaal;
import test.AbstractTest;
-import ui.TAttribute;
-import ui.avatarbd.AvatarBDPanel;
-import ui.avatarbd.AvatarBDPragma;
+
public class CLIAvatarModelCheckerTest extends AbstractTest implements InterpreterOutputInterface {
@@ -228,8 +216,37 @@ public class CLIAvatarModelCheckerTest extends AbstractTest implements Interpret
}
@Test
- public void testCompareUppaal() {
- String filePath = getBaseResourcesDir() + PATH_TO_TEST_FILE + "scriptmodelchecker_u";
+ public void testValidateCoffeeMachine() {
+ String filePath = getBaseResourcesDir() + PATH_TO_TEST_FILE + "scriptmodelchecker_val1";
+ String script;
+
+ outputResult = new StringBuilder();
+
+ File f = new File(filePath);
+ assertTrue(myutil.FileUtils.checkFileForOpen(f));
+
+ script = myutil.FileUtils.loadFileData(f);
+
+ 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 testValidateAirbusDoor_V2 () {
+ String filePath = getBaseResourcesDir() + PATH_TO_TEST_FILE + "scriptmodelchecker_val2";
String script;
outputResult = new StringBuilder();
diff --git a/ttool/src/test/resources/cli/expected/modelchecker_rl_expected b/ttool/src/test/resources/cli/expected/modelchecker_rl_expected
index bfb96028dfe2aeb48e4b1863020238220532b0ad..a2af6faaaa4a38a84a61367a0d57b9d7af334118 100644
--- a/ttool/src/test/resources/cli/expected/modelchecker_rl_expected
+++ b/ttool/src/test/resources/cli/expected/modelchecker_rl_expected
@@ -1,43 +1,35 @@
No Deadlocks:
property is NOT satisfied
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
+1. Element main of block Wallet -> reachable
+2. Element action_on_signal__clone:getCoin of block Wallet -> reachable
+3. Element WaitingForFirstCoin of block CoffeeMachine -> reachable
+4. Element action_on_signal__clone:getCoin of block CoffeeMachine -> reachable
+5. Element WaitingForSecondCoin of block CoffeeMachine -> reachable
+6. Element ejectState of block CoffeeMachine -> reachable
+7. Element action_on_signal__clone:getCoin of block CoffeeMachine -> reachable
+8. Element Beverage of block CoffeeMachine -> reachable
+9. Element WaitingForSelection of block CoffeeMachine -> reachable
+10. Element action_on_signal__clone:ejectCoin of block CoffeeMachine -> NOT reachable
+11. Element action_on_signal__clone:pushCoffeeButton of block CoffeeMachine -> reachable
+12. Element action_on_signal__clone:pushTeaButton of block CoffeeMachine -> reachable
+13. Element main of block CoffeeButton -> reachable
+14. Element state0 of block CoffeeButton -> reachable
+15. 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
+1. Element main of block Wallet -> liveness is satisfied
+2. Element action_on_signal__clone:getCoin of block Wallet -> liveness is NOT satisfied
+3. Element WaitingForFirstCoin of block CoffeeMachine -> liveness is satisfied
+4. Element action_on_signal__clone:getCoin of block CoffeeMachine -> liveness is satisfied
+5. Element WaitingForSecondCoin of block CoffeeMachine -> liveness is satisfied
+6. Element ejectState of block CoffeeMachine -> liveness is NOT satisfied
+7. Element action_on_signal__clone:getCoin of block CoffeeMachine -> liveness is NOT satisfied
+8. Element Beverage of block CoffeeMachine -> liveness is NOT satisfied
+9. Element WaitingForSelection of block CoffeeMachine -> liveness is NOT satisfied
+10. Element action_on_signal__clone:ejectCoin of block CoffeeMachine -> liveness is NOT satisfied
+11. Element action_on_signal__clone:pushCoffeeButton of block CoffeeMachine -> liveness is NOT satisfied
+12. Element action_on_signal__clone:pushTeaButton of block CoffeeMachine -> liveness is NOT satisfied
+13. Element main of block CoffeeButton -> liveness is satisfied
+14. Element state0 of block CoffeeButton -> liveness is satisfied
+15. 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/expected/modelchecker_s_expected b/ttool/src/test/resources/cli/expected/modelchecker_s_expected
index 332becb8acad0012c1bfb887ee733ba7795095be..f7c838af5a13085e5142dbe89e74575a69b504f7 100644
--- a/ttool/src/test/resources/cli/expected/modelchecker_s_expected
+++ b/ttool/src/test/resources/cli/expected/modelchecker_s_expected
@@ -1,53 +1,33 @@
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
+1. Element CLOSED_AND_LOCKED of block DoorAndLockButton -> reachable
+2. Element action_on_signal__clone:unlock of block DoorAndLockButton -> reachable
+3. Element CLOSED_AND_UNLOCKED of block DoorAndLockButton -> reachable
+4. Element action_on_signal__clone:lock of block DoorAndLockButton -> reachable
+5. Element action_on_signal__clone:open of block DoorAndLockButton -> reachable
+6. Element OPENED of block DoorAndLockButton -> reachable
+7. Element action_on_signal__clone:leaveCockpit of block DoorAndLockButton -> reachable
+8. Element action_on_signal__clone:close of block DoorAndLockButton -> reachable
+9. Element action_on_signal__clone:enterCockpit of block DoorAndLockButton -> reachable
+10. Element LOCKED_EMPTY_COCKPIT of block DoorAndLockButton -> NOT reachable
+11. Element action_on_signal__clone:emergencyCall of block DoorAndLockButton -> reachable
+12. Element IN_EMERGENCY_CALL of block DoorAndLockButton -> reachable
+13. Element action_on_signal__clone:lock of block DoorAndLockButton -> 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
+1. Element CLOSED_AND_LOCKED of block DoorAndLockButton -> liveness is satisfied
+2. Element action_on_signal__clone:unlock of block DoorAndLockButton -> liveness is NOT satisfied
+3. Element CLOSED_AND_UNLOCKED of block DoorAndLockButton -> liveness is NOT satisfied
+4. Element action_on_signal__clone:lock of block DoorAndLockButton -> liveness is NOT satisfied
+5. Element action_on_signal__clone:open of block DoorAndLockButton -> liveness is NOT satisfied
+6. Element OPENED of block DoorAndLockButton -> liveness is NOT satisfied
+7. Element action_on_signal__clone:leaveCockpit of block DoorAndLockButton -> liveness is NOT satisfied
+8. Element action_on_signal__clone:close of block DoorAndLockButton -> liveness is NOT satisfied
+9. Element action_on_signal__clone:enterCockpit of block DoorAndLockButton -> liveness is NOT satisfied
+10. Element LOCKED_EMPTY_COCKPIT of block DoorAndLockButton -> liveness is NOT satisfied
+11. Element action_on_signal__clone:emergencyCall of block DoorAndLockButton -> liveness is NOT satisfied
+12. Element IN_EMERGENCY_CALL of block DoorAndLockButton -> liveness is NOT satisfied
+13. Element action_on_signal__clone:lock of block DoorAndLockButton -> 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
diff --git a/ttool/src/test/resources/cli/input/scriptmodelchecker_u b/ttool/src/test/resources/cli/input/scriptmodelchecker_val1
similarity index 78%
rename from ttool/src/test/resources/cli/input/scriptmodelchecker_u
rename to ttool/src/test/resources/cli/input/scriptmodelchecker_val1
index d3e73fe202b5166fc75941cd651656fa57b50bcf..b47e099dc88e631e779b6b13140b85795e8b1582 100644
--- a/ttool/src/test/resources/cli/input/scriptmodelchecker_u
+++ b/ttool/src/test/resources/cli/input/scriptmodelchecker_val1
@@ -7,5 +7,5 @@ wait 2
action open $model
wait 4
action check-syntax
-action comp-uppaal ../../../uppaal/
+action avatar-rg-validate -ra -la -d ../../../uppaal/
action quit
diff --git a/ttool/src/test/resources/cli/input/scriptmodelchecker_val2 b/ttool/src/test/resources/cli/input/scriptmodelchecker_val2
new file mode 100644
index 0000000000000000000000000000000000000000..26a90cdfdf263051e37e09f9d460ebba6f82ae31
--- /dev/null
+++ b/ttool/src/test/resources/cli/input/scriptmodelchecker_val2
@@ -0,0 +1,11 @@
+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-validate -ra -la -s -d ../../../uppaal/
+action quit