diff --git a/src/main/java/avatartranslator/modelchecker/SpecificationActionLoop.java b/src/main/java/avatartranslator/modelchecker/SpecificationActionLoop.java
index 128ede76c8156306b1826374c5dbab92c6c0c5c2..d28445494f7d798bee04a54b52d0925ad22a68cf 100644
--- a/src/main/java/avatartranslator/modelchecker/SpecificationActionLoop.java
+++ b/src/main/java/avatartranslator/modelchecker/SpecificationActionLoop.java
@@ -226,7 +226,20 @@ public class SpecificationActionLoop {
if(internalLoops == null) {
return "";
} else if (cover == null) {
- return "In block " + internalLoops.get(0).get(0).getBlock().getName();
+ s.append("In block " + internalLoops.get(0).get(0).getBlock().getName() + " : ");
+ boolean first = true;
+ for (List<AvatarTransition> list : internalLoops) {
+ if (!first) {
+ s.append(", or ");
+ }
+ first = false;
+ s.append(list.get(list.size() - 1).getNext(0).getName());
+ for (AvatarTransition at : list) {
+ s.append(" --> " + at.getNext(0).getName());
+ }
+ }
+ s.append(" lead to a infinite internal loop\n");
+ return s.toString();
}
int i = 0;
diff --git a/src/main/java/cli/Action.java b/src/main/java/cli/Action.java
index e9ba8acdc4bd3caae911b80b8f195d98ed7b04bc..4a3e12db79ad99ba45bc0ab78250b030b7a71a32 100644
--- a/src/main/java/cli/Action.java
+++ b/src/main/java/cli/Action.java
@@ -42,6 +42,7 @@ package cli;
import avatartranslator.AvatarSpecification;
import avatartranslator.modelchecker.AvatarModelChecker;
import avatartranslator.modelchecker.CounterexampleQueryReport;
+import avatartranslator.modelchecker.SpecificationActionLoop;
import avatartranslator.modelcheckervalidator.ModelCheckerValidator;
import common.ConfigurationTTool;
import common.SpecConfigTTool;
@@ -851,12 +852,14 @@ public class Action extends Command {
+ "-la\tliveness of all states\n"
+ "-s\tsafety pragmas verification\n"
+ "-q \"QUERY\"\tquery a safety pragma\n"
- + "-d\tno deadlocks verification\n"
+ + "-d\tno deadlocks check\n"
+ + "-i\ttest model reinitialization\n"
+ + "-a\tno internal actions loops check\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"
+ "-c\tconsider full concurrency between actions\n"
- + "-v FILE\tsave counterexample traces for pragmas in FILE"
- + "-va FILE\tsave counterexample traces and AUT graph for pragmas in FILE";
+ + "-vt FILE\tsave verification traces in FILE"
+ + "-va FILE\tsave verification traces as AUT graph in FILE";
}
public String getExample() {
@@ -878,6 +881,7 @@ public class Action extends Command {
//String graphPath = commands[commands.length - 1];
String graphPath = "";
String counterPath = "";
+ String counterPathAUT = "";
AvatarSpecification avspec = interpreter.mgui.gtm.getAvatarSpecification();
if(avspec == null) {
@@ -896,6 +900,8 @@ public class Action extends Command {
boolean livenessAnalysis = false;
boolean safetyAnalysis = false;
boolean noDeadlocks = false;
+ boolean reinit = false;
+ boolean actionLoop = false;
for (int i = 0; i < commands.length; i++) {
//specification
switch (commands[i]) {
@@ -961,10 +967,20 @@ public class Action extends Command {
safetyAnalysis = true;
break;
case "-d":
- //safety
+ //deadlock
amc.setCheckNoDeadlocks(true);
noDeadlocks = true;
break;
+ case "-i":
+ //reinitialization
+ amc.setReinitAnalysis(true);
+ reinit = true;
+ break;
+ case "-a":
+ //internal action loops
+ amc.setInternalActionLoopAnalysis(true);
+ actionLoop = true;
+ break;
case "-n":
//state limit followed by a number
long states;
@@ -994,7 +1010,6 @@ public class Action extends Command {
case "-v":
if (i != commands.length - 1) {
counterPath = commands[++i];
- amc.setCounterExampleTrace(true, false);
counterTraces = true;
} else {
return Interpreter.BAD;
@@ -1002,9 +1017,7 @@ public class Action extends Command {
break;
case "-va":
if (i != commands.length - 1) {
- counterPath = commands[++i];
- amc.setCounterExampleTrace(true, true);
- counterTraces = true;
+ counterPathAUT = commands[++i];
counterTracesAUT = true;
} else {
return Interpreter.BAD;
@@ -1015,6 +1028,8 @@ public class Action extends Command {
}
}
TraceManager.addDev("Starting model checking");
+ amc.setCounterExampleTrace(counterTraces, counterTracesAUT);
+
if (livenessAnalysis || safetyAnalysis || noDeadlocks) {
amc.startModelCheckingProperties();
} else {
@@ -1026,6 +1041,21 @@ public class Action extends Command {
if (noDeadlocks) {
interpreter.print("No Deadlocks:\n" + amc.deadlockToString());
}
+ if (reinit) {
+ interpreter.print("Reinitialization?:\n" + amc.reinitToString());
+ }
+ if (actionLoop) {
+ boolean result = amc.getInternalActionLoopsResult();
+ interpreter.print("No internal action loops?:\n" + result);
+ if (!result) {
+ ArrayList<SpecificationActionLoop> al = amc.getInternalActionLoops();
+ for (SpecificationActionLoop sal : al) {
+ if (sal.getResult()) {
+ interpreter.print(sal.toString());
+ }
+ }
+ }
+ }
if (reachabilityAnalysis) {
interpreter.print("Reachability Analysis:\n" + amc.reachabilityToStringGeneric());
}
@@ -1059,6 +1089,11 @@ public class Action extends Command {
}
if (counterTracesAUT) {
+ if (counterPathAUT.indexOf("$") != -1) {
+ file = Conversion.replaceAllChar(counterPathAUT, '$', dateAndTime);
+ } else {
+ file = counterPathAUT;
+ }
List<CounterexampleQueryReport> autTraces = amc.getAUTTraces();
if (autTraces != null) {
int i = 0;
diff --git a/src/main/java/ui/window/JDialogAvatarModelChecker.java b/src/main/java/ui/window/JDialogAvatarModelChecker.java
index 89e45b228b761ac37a9ea30d3662660c268cb17f..a94cf11001e86cc85b093bbc756ca35125e6f6f4 100644
--- a/src/main/java/ui/window/JDialogAvatarModelChecker.java
+++ b/src/main/java/ui/window/JDialogAvatarModelChecker.java
@@ -330,7 +330,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
// Internal action loop
cbasic.gridwidth = GridBagConstraints.REMAINDER;
- actionLoop = new JCheckBox("No internal action loops? (test)", checkActionLoopSelected);
+ actionLoop = new JCheckBox("No internal action loops?", checkActionLoopSelected);
actionLoop.addActionListener(this);
jpbasic.add(actionLoop, cbasic);
@@ -888,9 +888,10 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
jta.append("Internal action loops:\n");
for (SpecificationActionLoop sal : al) {
if (sal.getResult()) {
- jta.append(sal.toString() + "\n");
+ jta.append(sal.toString());
}
}
+ jta.append("\n");
}
}