diff --git a/src/main/java/avatartranslator/AvatarExpressionSolver.java b/src/main/java/avatartranslator/AvatarExpressionSolver.java
index 5f192339466d4a728f4123e8b746b0da66e71660..b9773bf0fa8281cf7eadfb1effe195b71d4aa6fd 100644
--- a/src/main/java/avatartranslator/AvatarExpressionSolver.java
+++ b/src/main/java/avatartranslator/AvatarExpressionSolver.java
@@ -760,6 +760,17 @@ public class AvatarExpressionSolver {
}
}
+ public void setBlockIndex(AvatarSpecification spec) {
+ if (isLeaf) {
+ if (isImmediateValue == IMMEDIATE_NO) {
+ leaf.setBlockIndex(spec);
+ }
+ } else {
+ left.setBlockIndex(spec);
+ right.setBlockIndex(spec);
+ }
+ }
+
public static boolean containsElementAttribute(AvatarElement ae) {
if (attributesMap != null) {
diff --git a/src/main/java/avatartranslator/AvatarSpecification.java b/src/main/java/avatartranslator/AvatarSpecification.java
index 44b5770b6cce5659b93ede234bed61997af1e2d1..d6b46e511c0b9d5916750367125358a3212057db 100644
--- a/src/main/java/avatartranslator/AvatarSpecification.java
+++ b/src/main/java/avatartranslator/AvatarSpecification.java
@@ -452,6 +452,28 @@ public class AvatarSpecification extends AvatarElement {
block.setAttributeOptRatio(attributeOptRatio);
}
}
+
+ public List<ArrayList<AvatarTransition>> checkStaticInternalLoops() {
+ List<ArrayList<AvatarTransition>> loops = new ArrayList<ArrayList<AvatarTransition>>();
+
+ //collect all the possible loops which do not contain signal communication
+ for(AvatarBlock block: blocks) {
+ block.getStateMachine().checkStaticInternalLoops(loops);
+ }
+
+ return loops;
+
+// //check presence of unguarded loops
+// for (ArrayList<AvatarTransition> trace : loops) {
+// boolean guarded = false;
+// for (AvatarTransition at : trace) {
+// guarded |= at.isGuarded();
+// }
+// if (!guarded) {
+// //no transition has a guard check --> reachability of first state
+// }
+// }
+ }
//
// private void renameTimers() {
// // Check whether timers have the same name in different blocks
diff --git a/src/main/java/avatartranslator/AvatarStateMachine.java b/src/main/java/avatartranslator/AvatarStateMachine.java
index 55b610d6e49fe13db9305fdcbcd1855fc30dccae..4c8b6310f3511e865600638e70356387295d779e 100644
--- a/src/main/java/avatartranslator/AvatarStateMachine.java
+++ b/src/main/java/avatartranslator/AvatarStateMachine.java
@@ -43,6 +43,7 @@ import myutil.TraceManager;
import java.util.*;
+
/**
* Class AvatarStateMachine
* State machine, with composite states
@@ -1866,5 +1867,54 @@ public class AvatarStateMachine extends AvatarElement {
return invalids;
}
+
+
+ public boolean checkStaticInternalLoops(List<ArrayList<AvatarTransition>> loops) {
+ if (allStates == null) {
+ return false;
+ }
+
+ List<AvatarTransition> trace = new ArrayList<AvatarTransition>();
+ Set<AvatarStateMachineElement> visited= new HashSet<AvatarStateMachineElement>();
+
+ for (AvatarStateElement state : allStates) {
+ checkStaticInternalLoopsRec(state, state, trace, visited, loops, 0);
+ visited.add(state); //avoid cycles permutations
+ }
+ return true;
+ }
+
+
+ public void checkStaticInternalLoopsRec(AvatarStateMachineElement node, AvatarStateMachineElement arrival, List<AvatarTransition> trace, Set<AvatarStateMachineElement> visited, List<ArrayList<AvatarTransition>> loops, int depth) {
+ if (visited.contains(node)) {
+ if (node == arrival) {
+ //valid loop, copy trace to loops
+ loops.add(new ArrayList<AvatarTransition>(trace));
+ return;
+ } else {
+ //not valid loop
+ return;
+ }
+ } else if (node.nexts == null){
+ return;
+ }
+
+ visited.add(node);
+ for (AvatarStateMachineElement next : node.nexts) {
+ if (next instanceof AvatarTransition) {
+ AvatarTransition at = (AvatarTransition) next;
+ //the state machine should alternate states and transitions
+ if (!(at.getNext(0) instanceof AvatarActionOnSignal)) {
+ //Choose internal action paths
+ trace.add(depth, at);
+ checkStaticInternalLoopsRec(at.getNext(0), arrival, trace, visited, loops, depth + 1);
+ trace.remove(depth);
+ }
+ }
+ }
+ visited.remove(node);
+
+ return;
+ }
}
diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index f34898efe4aed9c0853b9f6aeb9276eae78302ff..1d79f836e48ece499e2fde613a8593407e923bc1 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -112,6 +112,10 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
private boolean studyReinit;
private SpecificationReinit initState;
+ // Internal-action loop
+ private boolean studyActionLoop;
+ private ArrayList<SpecificationActionLoop> actionLoops;
+
//Debug counterexample
private boolean counterexample;
private boolean counterTraceText;
@@ -376,6 +380,29 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
return false;
}
+ public void setInternalActionLoopAnalysis(boolean studyActionLoop) {
+ this.studyActionLoop = studyActionLoop;
+ }
+
+
+ public ArrayList<SpecificationActionLoop> getInternalActionLoops() {
+ if (studyActionLoop) {
+ return actionLoops;
+ }
+ return null;
+ }
+
+ public boolean getInternalActionLoopsResult() {
+ if (studyActionLoop && actionLoops != null) {
+ for (SpecificationActionLoop sal : actionLoops) {
+ if (sal.getResult()) {
+ return false;
+ }
+ }
+ }
+ return true;
+ }
+
public void setCounterExampleTrace(boolean counterTraceText, boolean counterTraceAUT) {
this.counterexample = counterTraceText || counterTraceAUT;
this.counterTraceText = counterTraceText;
@@ -424,7 +451,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}*/
public boolean startModelCheckingProperties() {
- boolean studyS, studyL, studyR, studyRI, genRG, genTrace;
+ boolean studyS, studyL, studyR, studyRI, studyAL, genRG, genTrace;
boolean emptyTr, ignoreConcurrence;
long deadlocks = 0;
@@ -449,6 +476,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
studyL = studyLiveness;
studyS = studySafety;
studyRI = studyReinit;
+ studyAL = studyActionLoop;
genRG = computeRG;
genTrace = counterexample;
verboseInfo = false;
@@ -460,6 +488,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
studyLiveness = false;
studyReachability = false;
studyReinit = false;
+ studyActionLoop = false;
counterexample = false;
@@ -538,6 +567,32 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
studyReinit = false;
}
+ if (studyAL) {
+ studySafety = true;
+ ignoreConcurrenceBetweenInternalActions = true;
+ List<ArrayList<AvatarTransition>> internalLoops = spec.checkStaticInternalLoops();
+ if (!internalLoops.isEmpty()) {
+ actionLoops = new ArrayList<SpecificationActionLoop>();
+ for (ArrayList<AvatarTransition> loop : internalLoops) {
+ SpecificationActionLoop sap = new SpecificationActionLoop(loop, spec);
+ if (!sap.hasError()) {
+ actionLoops.add(sap);
+ safety = sap.getReachability();
+ startModelChecking(nbOfThreads);
+ resetModelChecking();
+ if (sap.hasProperty()) {
+ safety = sap.getProperty();
+ startModelChecking(nbOfThreads);
+ resetModelChecking();
+ }
+ sap.setResult();
+ }
+ }
+ }
+ ignoreConcurrenceBetweenInternalActions = ignoreConcurrence;
+ studySafety = false;
+ }
+
if (checkNoDeadlocks) {
//If a complete study with reachability graph generation has been executed,
//there is no need to study deadlocks again
@@ -581,6 +636,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
studySafety = studyS;
studyReachability = studyR;
studyReinit = studyRI;
+ studyActionLoop = studyAL;
TraceManager.addDev("Model checking done");
return true;
@@ -773,10 +829,12 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
spec.sortAttributes();
spec.setAttributeOptRatio(compressionFactor);
spec.generateAllExpressionSolvers();
+
prepareTransitions();
prepareBlocks();
-
+
+ spec.checkStaticInternalLoops();
nbOfThreads = Runtime.getRuntime().availableProcessors();
TraceManager.addDev("Starting the model checking with " + nbOfThreads + " threads");
diff --git a/src/main/java/avatartranslator/modelchecker/SafetyProperty.java b/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
index 4f39eff0791002e37370ef2ef27c8ef52a5a3751..1c35663399c1879aadbe4c1266c7a6bcb79f6ece 100644
--- a/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
+++ b/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
@@ -103,27 +103,8 @@ public class SafetyProperty {
String tmpP = rawProperty.trim();
String p;
- errorOnProperty = NO_ERROR;
-
- if (tmpP.startsWith("A[]")) {
- safetyType = ALLTRACES_ALLSTATES;
- result = true;
- } else if (tmpP.startsWith("A<>")) {
- safetyType = ALLTRACES_ONESTATE;
- result = true;
- } else if (tmpP.startsWith("E[]")) {
- safetyType = ONETRACE_ALLSTATES;
- result = false;
- } else if (tmpP.startsWith("E<>")) {
- safetyType = ONETRACE_ONESTATE;
- result = false;
- } else if (tmpP.contains("-->")){
- safetyType = LEADS_TO;
- result = true;
- } else {
- errorOnProperty = BAD_SAFETY_TYPE;
- result = false;
- return false;
+ if (!initType(tmpP)) {
+ return false;
}
if (safetyType != LEADS_TO) {
@@ -138,6 +119,28 @@ public class SafetyProperty {
return (errorOnProperty == NO_ERROR);
}
+ //for local variables inside a block
+ public boolean analyzeProperty(AvatarBlock block, AvatarSpecification _spec) {
+ String tmpP = rawProperty.trim();
+ String p;
+
+ if (!initType(tmpP)) {
+ return false;
+ }
+
+ if (safetyType != LEADS_TO) {
+ p = tmpP.substring(3, tmpP.length()).trim();
+ initSafetyTrace(block, _spec, p);
+ } else {
+ p = tmpP;
+ initSafetyLeads(block, _spec, p);
+ }
+
+
+ return (errorOnProperty == NO_ERROR);
+ }
+
+
public void initLead() {
safetySolver = safetySolverLead;
safetyType = ALLTRACES_ONESTATE;
@@ -238,6 +241,32 @@ public class SafetyProperty {
return name;
}
+ private boolean initType(String tmpP) {
+ errorOnProperty = NO_ERROR;
+
+ if (tmpP.startsWith("A[]")) {
+ safetyType = ALLTRACES_ALLSTATES;
+ result = true;
+ } else if (tmpP.startsWith("A<>")) {
+ safetyType = ALLTRACES_ONESTATE;
+ result = true;
+ } else if (tmpP.startsWith("E[]")) {
+ safetyType = ONETRACE_ALLSTATES;
+ result = false;
+ } else if (tmpP.startsWith("E<>")) {
+ safetyType = ONETRACE_ONESTATE;
+ result = false;
+ } else if (tmpP.contains("-->")){
+ safetyType = LEADS_TO;
+ result = true;
+ } else {
+ errorOnProperty = BAD_SAFETY_TYPE;
+ result = false;
+ return false;
+ }
+ return true;
+ }
+
private boolean initSafetyTrace(AvatarSpecification _spec, String p) {
safetySolver = new AvatarExpressionSolver(p);
@@ -256,6 +285,25 @@ public class SafetyProperty {
return exprRet;
}
+ private boolean initSafetyTrace(AvatarBlock block, AvatarSpecification _spec, String p) {
+ safetySolver = new AvatarExpressionSolver(p);
+ boolean exprRet = safetySolver.buildExpression(block);
+
+ if (exprRet == false) {
+ errorOnProperty = BAD_PROPERTY_STRUCTURE;
+ }
+
+ safetySolver.setBlockIndex(_spec);
+
+ if (safetySolver.hasState()) {
+ propertyType = BLOCK_STATE;
+ } else {
+ propertyType = BOOL_EXPR;
+ }
+
+ return exprRet;
+ }
+
private boolean initSafetyLeads(AvatarSpecification _spec, String p) {
String[] pFields;
@@ -301,5 +349,54 @@ public class SafetyProperty {
return true;
}
+
+ private boolean initSafetyLeads(AvatarBlock block, AvatarSpecification _spec, String p) {
+ String[] pFields;
+ String pp, pq;
+ boolean exprRet;
+
+ pFields = p.split("-->");
+ if (pFields.length != 2) {
+ errorOnProperty = BAD_PROPERTY_STRUCTURE;
+ return false;
+ }
+
+ pp = pFields[0].trim();
+ pq = pFields[1].trim();
+
+ safetySolver = new AvatarExpressionSolver(pp);
+ exprRet = safetySolver.buildExpression(block);
+
+ if (exprRet == false) {
+ errorOnProperty = BAD_PROPERTY_STRUCTURE;
+ return false;
+ }
+
+ safetySolver.setBlockIndex(_spec);
+
+ safetySolverLead = new AvatarExpressionSolver(pq);
+ exprRet = safetySolverLead.buildExpression(block);
+
+ if (exprRet == false) {
+ errorOnProperty = BAD_PROPERTY_STRUCTURE;
+ return false;
+ }
+
+ safetySolverLead.setBlockIndex(_spec);
+
+ if (safetySolver.hasState()) {
+ propertyType = BLOCK_STATE;
+ } else {
+ propertyType = BOOL_EXPR;
+ }
+
+ if (safetySolverLead.hasState()) {
+ leadType = BLOCK_STATE;
+ } else {
+ leadType = BOOL_EXPR;
+ }
+
+ return true;
+ }
}
diff --git a/src/main/java/avatartranslator/modelchecker/SpecificationActionLoop.java b/src/main/java/avatartranslator/modelchecker/SpecificationActionLoop.java
new file mode 100644
index 0000000000000000000000000000000000000000..c5da755352834877a81411d50a4551fb75c5f9ed
--- /dev/null
+++ b/src/main/java/avatartranslator/modelchecker/SpecificationActionLoop.java
@@ -0,0 +1,90 @@
+package avatartranslator.modelchecker;
+
+import java.util.List;
+
+import avatartranslator.AvatarBlock;
+import avatartranslator.AvatarSpecification;
+import avatartranslator.AvatarTransition;
+
+public class SpecificationActionLoop {
+ private List<AvatarTransition> path;
+ private SafetyProperty reachability;
+ private SafetyProperty property;
+ private boolean hasProperty;
+ private boolean result;
+ private boolean error;
+
+ public SpecificationActionLoop(List<AvatarTransition> path, AvatarSpecification spec) {
+ this.path = path;
+ this.error = false;
+ init(spec);
+ }
+
+ private void init(AvatarSpecification spec) {
+ //check presence of unguarded loops
+ boolean guarded = false;
+ StringBuilder condition = new StringBuilder("!(");
+ for (AvatarTransition at : path) {
+ if (at.isGuarded()) {
+ String guard = at.getGuard().toString().replaceAll("\\[", "").trim().replaceAll("\\]", "");
+ if (guarded) {
+ condition.append(" && " + guard);
+ } else {
+ condition.append(guard);
+ }
+ guarded = true;
+ }
+ }
+ condition.append(")");
+ AvatarTransition at = path.get(path.size() - 1);
+ //no transition has a guard check --> reachability of first state
+ reachability = new SafetyProperty("E<> " + at.getBlock().getName() + "." + at.getNext(0).getName());
+ reachability.analyzeProperty(spec);
+ error = reachability.hasError();
+ hasProperty = false;
+ if (guarded) {
+ hasProperty = true;
+ property = new SafetyProperty("E<> " + at.getNext(0).getName() + " && " + condition.toString());
+ property.analyzeProperty((AvatarBlock) at.getBlock(), spec);
+ error |= property.hasError();
+ }
+ }
+
+ public boolean hasError() {
+ return error;
+ }
+
+ public boolean hasProperty() {
+ return hasProperty;
+ }
+
+ public SafetyProperty getReachability() {
+ return reachability;
+ }
+
+ public SafetyProperty getProperty() {
+ return property;
+ }
+
+ public void setResult() {
+ result = reachability.result;
+ if (hasProperty) {
+ result &= !property.result;
+ }
+ }
+
+ public boolean getResult() {
+ return result;
+ }
+
+ public String toString() {
+ StringBuilder s = new StringBuilder();
+
+ s.append("In block " + path.get(path.size() - 1).getBlock().getName() + " : " + path.get(path.size() - 1).getNext(0).getName());
+ for (AvatarTransition at : path) {
+ s.append(" --> " + at.getNext(0).getName());
+ }
+
+ return s.toString();
+ }
+}
diff --git a/src/main/java/ui/window/JDialogAvatarModelChecker.java b/src/main/java/ui/window/JDialogAvatarModelChecker.java
index 1592e9e3178a095b2308ee53895d5d3d482a9124..44de8fdafa01b846598cefa6fe00677c3c8b2c7e 100644
--- a/src/main/java/ui/window/JDialogAvatarModelChecker.java
+++ b/src/main/java/ui/window/JDialogAvatarModelChecker.java
@@ -44,6 +44,7 @@ import avatartranslator.AvatarStateMachineElement;
import avatartranslator.modelchecker.AvatarModelChecker;
import avatartranslator.modelchecker.CounterexampleQueryReport;
import avatartranslator.modelchecker.SafetyProperty;
+import avatartranslator.modelchecker.SpecificationActionLoop;
import avatartranslator.modelchecker.SpecificationReachability;
import avatartranslator.modelchecker.SpecificationPropertyPhase;
import myutil.*;
@@ -105,6 +106,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
protected static boolean safetySelected = false;
protected static boolean checkNoDeadSelected = false;
protected static boolean checkReinitSelected = false;
+ protected static boolean checkActionLoopSelected = false;
protected static boolean limitStatesSelected = false;
protected static boolean generateCountertraceSelected = false;
protected static boolean generateCountertraceAUTSelected = false;
@@ -159,6 +161,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
protected JTextField timeLimitField;
protected JCheckBox noDeadlocks;
protected JCheckBox reinit;
+ protected JCheckBox actionLoop;
protected JCheckBox safety;
protected JCheckBox countertrace;
protected JCheckBox countertraceAUT;
@@ -321,10 +324,15 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
// Reinit
- cbasic.gridwidth = GridBagConstraints.REMAINDER;
reinit = new JCheckBox("Reinitialization?", checkReinitSelected);
reinit.addActionListener(this);
jpbasic.add(reinit, cbasic);
+
+ // Internal action loop
+ cbasic.gridwidth = GridBagConstraints.REMAINDER;
+ actionLoop = new JCheckBox("No internal action loops? (test)", checkActionLoopSelected);
+ actionLoop.addActionListener(this);
+ jpbasic.add(actionLoop, cbasic);
// Reachability
@@ -735,6 +743,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
amc.setIgnoreInternalStates(ignoreInternalStatesSelected);
amc.setCheckNoDeadlocks(checkNoDeadSelected);
amc.setReinitAnalysis(checkReinitSelected);
+ amc.setInternalActionLoopAnalysis(checkActionLoopSelected);
amc.setCounterExampleTrace(generateCountertraceSelected, generateCountertraceAUTSelected);
// Reachability
@@ -838,7 +847,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
// Starting model checking
testGo();
- if (livenessSelected == LIVENESS_NONE && safetySelected == false && checkNoDeadSelected == false) {
+ if (livenessSelected == LIVENESS_NONE && safetySelected == false && checkNoDeadSelected == false && checkActionLoopSelected == false) {
amc.startModelChecking();
} else {
amc.startModelCheckingProperties();
@@ -869,6 +878,21 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
if (checkReinitSelected) {
jta.append("\nReinitialization?\n" + "-> " + amc.reinitToString() + "\n");
}
+
+ if (checkActionLoopSelected) {
+ boolean result = amc.getInternalActionLoopsResult();
+ jta.append("\nNo internal action loops?\n" + "-> " + result + "\n");
+
+ if (!result) {
+ ArrayList<SpecificationActionLoop> al = amc.getInternalActionLoops();
+ jta.append("Internal action loops:\n");
+ for (SpecificationActionLoop sal : al) {
+ if (sal.getResult()) {
+ jta.append(sal.toString() + "\n");
+ }
+ }
+ }
+ }
if ((reachabilitySelected == REACHABILITY_SELECTED) || (reachabilitySelected == REACHABILITY_ALL)) {
jta.append("\nReachabilities found:\n");
@@ -1090,6 +1114,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
ignoreInternalStatesSelected = ignoreInternalStates.isSelected();
checkNoDeadSelected = noDeadlocks.isSelected();
checkReinitSelected = reinit.isSelected();
+ checkActionLoopSelected = actionLoop.isSelected();
if (noReachability.isSelected()) {
reachabilitySelected = REACHABILITY_NONE;
@@ -1129,7 +1154,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
switch (mode) {
case NOT_STARTED:
- if ((reachabilitySelected == REACHABILITY_SELECTED) || (reachabilitySelected == REACHABILITY_ALL) || (livenessSelected == LIVENESS_SELECTED) || (livenessSelected == LIVENESS_ALL) || checkNoDeadSelected || checkReinitSelected || graphSelected || graphSelectedDot) {
+ if ((reachabilitySelected == REACHABILITY_SELECTED) || (reachabilitySelected == REACHABILITY_ALL) || (livenessSelected == LIVENESS_SELECTED) || (livenessSelected == LIVENESS_ALL) || checkNoDeadSelected || checkReinitSelected || checkActionLoopSelected || graphSelected || graphSelectedDot) {
start.setEnabled(true);
} else {
if (safetySelected) {