diff --git a/src/main/java/avatartranslator/AvatarExpressionAttribute.java b/src/main/java/avatartranslator/AvatarExpressionAttribute.java
index d4559085174036dbddb44876cd5294f481c1fc66..a3e7a4696e3fe7cbea38246ad45251a3d470bb85 100644
--- a/src/main/java/avatartranslator/AvatarExpressionAttribute.java
+++ b/src/main/java/avatartranslator/AvatarExpressionAttribute.java
@@ -38,8 +38,6 @@
package avatartranslator;
-import java.util.List;
-
import avatartranslator.modelchecker.SpecificationBlock;
import avatartranslator.modelchecker.SpecificationState;
diff --git a/src/main/java/avatartranslator/AvatarExpressionSolver.java b/src/main/java/avatartranslator/AvatarExpressionSolver.java
index bacb6d4639fefafb34f660936046a6548c70d10b..a38cf52683824e2714ecb70f931a0c4bf784cd6a 100644
--- a/src/main/java/avatartranslator/AvatarExpressionSolver.java
+++ b/src/main/java/avatartranslator/AvatarExpressionSolver.java
@@ -343,6 +343,17 @@ public class AvatarExpressionSolver {
isNot = true;
expression = expression.substring(4, expression.length() - 1).trim();
}
+ } else if (expression.startsWith("!(")) {
+ int closingIndex = getClosingBracket(2);
+
+ if (closingIndex == -1) {
+ return false;
+ }
+ if (closingIndex == expression.length() - 1) {
+ //not(expression)
+ isNot = true;
+ expression = expression.substring(2, expression.length() - 1).trim();
+ }
}
return true;
}
@@ -709,7 +720,7 @@ public class AvatarExpressionSolver {
right.linkStates();
}
}
-
+
private boolean checkIntegrity() {
int optype, optypel, optyper;
boolean returnVal;
diff --git a/src/main/java/avatartranslator/AvatarSpecification.java b/src/main/java/avatartranslator/AvatarSpecification.java
index 3c0d34b11455419625845251b7863cdbbe5f169a..f5de87261bfdc81597dfa3bab9d16f1ef34ca1bf 100644
--- a/src/main/java/avatartranslator/AvatarSpecification.java
+++ b/src/main/java/avatartranslator/AvatarSpecification.java
@@ -346,6 +346,46 @@ public class AvatarSpecification extends AvatarElement {
public static String putRealAttributeValueInString(String _source, AvatarAttribute _at) {
return Conversion.putVariableValueInString(ops, _source, _at.getName(), _at.getInitialValue());
}
+
+
+ /* Generates the Expression Solvers, returns the AvatarStateMachineElement
+ * containing the errors */
+ public List<AvatarStateMachineElement> generateAllExpressionSolvers() {
+ List<AvatarStateMachineElement> errors = new ArrayList<>();
+ AvatarTransition at;
+ boolean returnVal;
+
+ for (AvatarBlock block : getListOfBlocks()) {
+ AvatarStateMachine asm = block.getStateMachine();
+
+ for (AvatarStateMachineElement elt : asm.getListOfElements()) {
+ if (elt instanceof AvatarTransition) {
+ at = (AvatarTransition) elt;
+ if (at.isGuarded()) {
+ returnVal = at.buildGuardSolver();
+ if (returnVal == false) {
+ errors.add(at);
+ }
+ }
+ for (AvatarAction aa : at.getActions()) {
+ if (aa instanceof AvatarActionAssignment) {
+ returnVal = ((AvatarActionAssignment) aa).buildActionSolver(block);
+ if (returnVal == false) {
+ errors.add(elt);
+ }
+ }
+ }
+ } else if (elt instanceof AvatarActionOnSignal) {
+ returnVal = ((AvatarActionOnSignal) elt).buildActionSolver(block);
+ if (returnVal == false) {
+ errors.add(elt);
+ }
+ }
+ }
+ }
+
+ return errors;
+ }
public void removeCompositeStates() {
for(AvatarBlock block: blocks) {
diff --git a/src/main/java/avatartranslator/AvatarStateMachine.java b/src/main/java/avatartranslator/AvatarStateMachine.java
index 222c90d1f3f4c729bc3555a29cf64ac8c710f019..6dba84aeabbf78b9e610d3f9c1d8c684f63cdbed 100644
--- a/src/main/java/avatartranslator/AvatarStateMachine.java
+++ b/src/main/java/avatartranslator/AvatarStateMachine.java
@@ -427,29 +427,65 @@ public class AvatarStateMachine extends AvatarElement {
previous = getPreviousElementOf(elt);
next = elt.getNext(0);
toRemove.add(elt);
+//
+// // Creating elements
+// AvatarState beforeRandom = new AvatarState("StateBeforeRandom__" + elt.getName() + "__" + id, elt.getReferenceObject());
+// AvatarState randomState = new AvatarState("StateForRandom__" + elt.getName() + "__" + id, elt.getReferenceObject());
+//
+// for (int i = Integer.parseInt(random.getMinValue()); i <= Integer.parseInt(random.getMaxValue()); i++) {
+// AvatarTransition at1 = new AvatarTransition(_block, "TransitionForRandom__" + random.getVariable() + "=" + i + "__" + elt.getName() + "__" + id, elt.getReferenceObject());
+// at1.addAction(random.getVariable() + "=" + i);
+// toAdd.add(at1);
+// beforeRandom.addNext(at1);
+// at1.addNext(randomState);
+// }
+//
+// // Adding elements
+// toAdd.add(beforeRandom);
+// toAdd.add(randomState);
+//
+// // Linking elements
+// if (previous != null) {
+// previous.removeAllNexts();
+// previous.addNext(beforeRandom);
+// }
+// randomState.addNext(next);
+//
+// id++;
+//
+// }
// Creating elements
- AvatarState beforeRandom = new AvatarState("StateBeforeRandom__" + elt.getName() + "__" + id, elt.getReferenceObject());
+ AvatarTransition at1 = new AvatarTransition(_block, "Transition1ForRandom__ " + elt.getName() + "__" + id, elt.getReferenceObject());
+ at1.addAction(random.getVariable() + "=" + random.getMinValue());
AvatarState randomState = new AvatarState("StateForRandom__" + elt.getName() + "__" + id, elt.getReferenceObject());
-
- for (int i = Integer.parseInt(random.getMinValue()); i <= Integer.parseInt(random.getMaxValue()); i++) {
- AvatarTransition at1 = new AvatarTransition(_block, "TransitionForRandom__" + random.getVariable() + "=" + i + "__" + elt.getName() + "__" + id, elt.getReferenceObject());
- at1.addAction(random.getVariable() + "=" + i);
- toAdd.add(at1);
- beforeRandom.addNext(at1);
- at1.addNext(randomState);
- }
-
+ AvatarState beforeRandom = new AvatarState("StateBeforeRandom__" + elt.getName() + "__" + id, elt.getReferenceObject());
+ AvatarTransition at2 = new AvatarTransition(_block, "Transition2ForRandom__" + elt.getName() + "__" + id, elt.getReferenceObject());
+ at2.setGuard("[" + random.getVariable() + " < " + random.getMaxValue() + "]");
+ at2.addAction(random.getVariable() + "=" + random.getVariable() + " + 1");
+ AvatarTransition at3 = new AvatarTransition(_block, "Transition3ForRandom__ " + elt.getName() + "__" + id, elt.getReferenceObject());
+ AvatarState afterRandom = new AvatarState("StateAfterRandom__" + elt.getName() + "__" + id, elt.getReferenceObject());
+
// Adding elements
- toAdd.add(beforeRandom);
+ toAdd.add(at1);
toAdd.add(randomState);
+ toAdd.add(beforeRandom);
+ toAdd.add(at2);
+ toAdd.add(at3);
+ toAdd.add(afterRandom);
// Linking elements
if (previous != null) {
previous.removeAllNexts();
previous.addNext(beforeRandom);
}
- randomState.addNext(next);
+ beforeRandom.addNext(at1);
+ at1.addNext(randomState);
+ randomState.addNext(at2);
+ randomState.addNext(at3);
+ at2.addNext(randomState);
+ at3.addNext(afterRandom);
+ afterRandom.addNext(next);
id++;
diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index 76af8022964d816583229c0b5a7b78608b8086f1..1110313997794262fb42b2721234f131b824cac9 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -112,6 +112,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
//Debug counterexample
private boolean counterexample;
+ private boolean counterTraceAUT;
private CounterexampleTrace counterTrace;
public Map<Integer, CounterexampleTraceState> traceStates;
private StringBuilder counterTraceReport;
@@ -346,10 +347,11 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
return false;
}
- public void setCounterExampleTrace(boolean counterexample) {
+ public void setCounterExampleTrace(boolean counterexample, boolean counterTraceAUT) {
this.counterexample = counterexample;
if (counterexample) {
counterTraceReport = new StringBuilder();
+ this.counterTraceAUT = counterTraceAUT;
}
}
@@ -359,6 +361,13 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
return counterTraceReport.toString();
}
+
+ public List<String> getAUTTraces() {
+ if (counterTrace == null) {
+ return null;
+ }
+ return counterTrace.getAUTTrace();
+ }
public void setComputeRG(boolean _rg) {
computeRG = _rg;
@@ -385,7 +394,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}*/
public boolean startModelCheckingProperties() {
- boolean studyS, studyL, studyR, studyRI, genRG;
+ boolean studyS, studyL, studyR, studyRI, genRG, genTrace;
boolean emptyTr, ignoreConcurrence;
long deadlocks = 0;
@@ -398,6 +407,8 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
initModelChecking();
+
+ initCounterexample();
stateLimitRG = false;
timeLimitRG = false;
@@ -408,6 +419,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
studyS = studySafety;
studyRI = studyReinit;
genRG = computeRG;
+ genTrace = counterexample;
//then compute livenesses
computeRG = false;
@@ -416,6 +428,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
studyLiveness = false;
studyReachability = false;
studyReinit = false;
+ counterexample = false;
if (studyL) {
@@ -424,9 +437,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
ignoreEmptyTransitions = true;
for (SafetyProperty sp : livenesses) {
safety = sp;
-// initCounterexample();
startModelChecking(nbOfThreads);
-// generateCounterexample();
deadlocks += nbOfDeadlocks;
resetModelChecking();
if (!stoppedBeforeEnd) {
@@ -440,6 +451,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (studyS) {
studySafety = true;
+ counterexample = genTrace;
for (SafetyProperty sp : safeties) {
safety = sp;
ignoreConcurrenceBetweenInternalActions = true;
@@ -449,7 +461,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
ignoreEmptyTransitions = false;
ignoreConcurrenceBetweenInternalActions = ignoreConcurrence;
}
- initCounterexample();
+ resetCounterexample();
startModelChecking(nbOfThreads);
generateCounterexample();
if (safety.safetyType == SafetyProperty.LEADS_TO) {
@@ -460,7 +472,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
for (SpecificationState state : safetyLeadStates.values()) {
deadlocks += nbOfDeadlocks;
resetModelChecking();
- initCounterexample();
+ resetCounterexample();
startModelChecking(state, nbOfThreads);
if (safety.result == false) {
generateCounterexample();
@@ -478,6 +490,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
resetModelChecking();
}
studySafety = false;
+ counterexample = false;
}
if (studyRI) {
@@ -488,6 +501,24 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
studyReinit = false;
}
+ if (checkNoDeadlocks) {
+ //If a complete study with reachability graph generation has been executed,
+ //there is no need to study deadlocks again
+ if (deadlocks == 0 || genTrace) {
+ deadlockStop = true;
+ counterexample = genTrace;
+ ignoreConcurrenceBetweenInternalActions = true;
+ resetCounterexample();
+ startModelChecking(nbOfThreads);
+ generateCounterexample();
+ deadlocks = nbOfDeadlocks;
+ resetModelChecking();
+ ignoreConcurrenceBetweenInternalActions = ignoreConcurrence;
+ counterexample = false;
+ deadlockStop = false;
+ }
+ }
+
if (studyR || genRG) {
if (genRG) {
deadlocks = 0;
@@ -503,17 +534,8 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (genRG) {
nbOfDeadlocks = (int) deadlocks;
- } else if (checkNoDeadlocks) {
- //If a complete study with reachability graph generation has been executed,
- //there is no need to study deadlocks again
- if (deadlocks == 0) {
- deadlockStop = true;
- ignoreConcurrenceBetweenInternalActions = true;
- startModelChecking(nbOfThreads);
- ignoreConcurrenceBetweenInternalActions = ignoreConcurrence;
- } else {
- nbOfDeadlocks = 1;
- }
+ } else if (checkNoDeadlocks && deadlocks > 0) {
+ nbOfDeadlocks = 1;
}
computeRG = genRG;
@@ -583,7 +605,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
//
// prepareTransitionsOfState(initialState);
blockValues = initialState.getBlockValues();
- initialState.distance = 0;
+// initialState.distance = 0;
//TraceManager.addDev("initialState=" + initialState.toString() + "\n nbOfTransitions" + initialState.transitions.size());
initialState.computeHash(blockValues);
@@ -596,6 +618,10 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
actionOnProperty(initialState, 0, null, null);
} else {
pendingStates.add(initialState);
+ if (counterexample && deadlockStop) {
+ //Register counterexample trace
+ actionOnProperty(initialState, 0, null, null);
+ }
}
if (studyReinit) {
@@ -646,7 +672,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
// initialState's transitions and blocks must be already initialized
blockValues = initialState.getBlockValues();
- initialState.distance = 0;
+// initialState.distance = 0;
//TraceManager.addDev("initialState=" + initialState.toString() + "\n nbOfTransitions" + initialState.transitions.size());
initialState.computeHash(blockValues);
@@ -659,6 +685,10 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
actionOnProperty(initialState, 0, null, null);
} else {
pendingStates.add(initialState);
+ if (counterexample && deadlockStop) {
+ //Register counterexample trace
+ actionOnProperty(initialState, 0, null, null);
+ }
}
//pendingStates.add(initialState);
@@ -880,30 +910,10 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
nbOfCurrentComputations = 0;
}
- private void initExpressionSolvers() {
- AvatarTransition at;
+ private void initExpressionSolvers() {
+ spec.generateAllExpressionSolvers();
- for (AvatarBlock block : spec.getListOfBlocks()) {
- AvatarStateMachine asm = block.getStateMachine();
-
- for (AvatarStateMachineElement elt : asm.getListOfElements()) {
- if (elt instanceof AvatarTransition) {
- at = (AvatarTransition) elt;
- if (at.isGuarded()) {
- at.buildGuardSolver();
- }
- for (AvatarAction aa : at.getActions()) {
- if (aa instanceof AvatarActionAssignment) {
- ((AvatarActionAssignment) aa).buildActionSolver(block);
- }
- }
- } else if (elt instanceof AvatarActionOnSignal) {
- ((AvatarActionOnSignal) elt).buildActionSolver(block);
- }
- }
- }
-
- //To have all the leadsTo functionalities allStates in stateMachines must be filled with states
+ //To have all the safety functionalities allStates in stateMachines must be filled with states
if (studySafety && safeties != null) {
for (SafetyProperty sp : safeties) {
sp.linkSolverStates();
@@ -919,13 +929,30 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
}
+ private void resetCounterexample() {
+ if (counterexample) {
+ counterTrace.reset();
+ traceStates = Collections.synchronizedMap(new HashMap<Integer, CounterexampleTraceState>());
+ }
+ }
+
private void generateCounterexample() {
if (counterexample && counterTrace.hasCounterexample()) {
counterTrace.buildTrace();
if (studySafety) {
counterTraceReport.append("Trace for " + safety.getRawProperty() + "\n");
- counterTraceReport.append(counterTrace.generateSimpleTrace(states) + "\n");
+ counterTraceReport.append(counterTrace.generateSimpleTrace(states) + "\n\n");
+ } else if (deadlockStop) {
+ counterTraceReport.append("Trace for NO Deadlocks\n");
+ counterTraceReport.append(counterTrace.generateSimpleTrace(states) + "\n\n");
+ }
+ if (counterTraceAUT) {
+ if (studySafety) {
+ counterTrace.generateTraceAUT(safety.getRawProperty(), states);
+ } else if (deadlockStop) {
+ counterTrace.generateTraceAUT("No Deadlocks", states);
+ }
}
}
}
@@ -1097,12 +1124,16 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
//statesByID.put(newState.id, newState);
link.destinationState = newState;
- newState.distance = _ss.distance + 1;
+// newState.distance = _ss.distance + 1;
- if (!studySafety) {
- pendingStates.add(newState);
- } else {
+ if (studySafety) {
actionOnProperty(newState, i, similar, _ss);
+ } else {
+ pendingStates.add(newState);
+ if (counterexample && deadlockStop) {
+ //Register counterexample trace
+ actionOnProperty(newState, i, similar, _ss);
+ }
}
i++;
//newState.id = getStateID();
@@ -1146,6 +1177,8 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
private void computeAllInternalStatesFrom(SpecificationState _ss, SpecificationTransition st) {
SpecificationState newState = _ss.advancedClone();
SpecificationState previousState = _ss;
+
+ ArrayList<Integer> stackStates = new ArrayList<>(); //keeps track of the block hashes
while (st != null) {
//TraceManager.addDev("cpt=" + cpt + " Working on transition:" + st);
@@ -1160,7 +1193,6 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
handleNonEmptyUniqueTransition(newState);
}
-
newState.computeHash(blockValues);
SpecificationState similar = findSimilarState(newState);
@@ -1174,6 +1206,44 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
_ss.addNext(link);
actionOnProperty(newState, 0, similar, _ss);
break;
+ } else if (stackStates.contains(newState.hashValue)) {
+ //already elaborated, add that state
+ SpecificationLink link = new SpecificationLink();
+ link.originState = _ss;
+ action += " [" + "0...0" + "]";
+ link.action = action;
+ link.destinationState = newState;
+ synchronized (this) {
+ similar = states.get(newState.getHash(blockValues));
+ if (similar == null) {
+ if (!(stateLimitRG && stateID >= stateLimit)/* || timeLimitReached*/) {
+ addState(newState);
+ } else {
+ limitReached = true; //can be removed
+ break;
+ }
+ }
+ }
+ if (similar != null) {
+ // check if it has been created by another thread in the meanwhile
+ link.destinationState = similar;
+ actionOnProperty(newState, 0, similar, _ss);
+ } else {
+ link.destinationState = newState;
+// newState.distance = _ss.distance + 1;
+ if (studySafety) {
+ actionOnProperty(newState, 0, similar, _ss);
+ } else {
+ pendingStates.add(newState);
+ if (counterexample && deadlockStop) {
+ //Register counterexample trace
+ actionOnProperty(newState, 0, similar, _ss);
+ }
+ }
+ }
+ nbOfLinks++;
+ _ss.addNext(link);
+ break;
} else if (studySafety && safety.safetyType == SafetyProperty.LEADS_TO && newState.property) {
newState = reduceCombinatorialExplosionProperty(newState);
@@ -1193,7 +1263,8 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
_ss.addNext(link);
break;
}
-
+
+ stackStates.add(newState.hashValue);
// Compute next transition
//prepareTransitionsOfState(previousState);
@@ -1248,11 +1319,15 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
actionOnProperty(newState, 0, similar, _ss);
} else {
link.destinationState = newState;
- newState.distance = _ss.distance + 1;
- if (!studySafety) {
- pendingStates.add(newState);
- } else {
+// newState.distance = _ss.distance + 1;
+ if (studySafety) {
actionOnProperty(newState, 0, similar, _ss);
+ } else {
+ pendingStates.add(newState);
+ if (counterexample && deadlockStop) {
+ //Register counterexample trace
+ actionOnProperty(newState, 0, similar, _ss);
+ }
}
}
nbOfLinks++;
@@ -1286,6 +1361,8 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
SpecificationState prevState = ss;
boolean found;
+ ArrayList<Integer> stackStates = new ArrayList<>(); //keeps track of the block hashes
+
do {
prepareTransitionsOfState(prevState);
@@ -1294,6 +1371,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
ArrayList<SpecificationTransition> transitions = computeValidTransitions(prevState.transitions);
+ stackStates.add(prevState.hashValue);
found = false;
for (SpecificationTransition tr : transitions) {
@@ -1307,7 +1385,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (newState.property) {
newState.computeHash(blockValues);
SpecificationState similar = findSimilarState(newState);
- if (similar != null) {
+ if (similar != null || stackStates.contains(newState.hashValue)) {
return newState;
}
found = true;
@@ -2338,9 +2416,9 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
private boolean stateIsReachableFromState(SpecificationState start, SpecificationState arrival) {
Set<Long> visited= new HashSet<Long>();
- if (start.distance > arrival.distance) {
- return false;
- }
+// if (start.distance > arrival.distance) {
+// return false;
+// }
return stateIsReachableFromStateRec(start, arrival, visited);
}
diff --git a/src/main/java/avatartranslator/modelchecker/CounterexampleTrace.java b/src/main/java/avatartranslator/modelchecker/CounterexampleTrace.java
index aad9fadbd34068c75a2611824b690c9ad86f00e5..028eeab1292e1525c2e9ea1452d8101d1327fd8f 100644
--- a/src/main/java/avatartranslator/modelchecker/CounterexampleTrace.java
+++ b/src/main/java/avatartranslator/modelchecker/CounterexampleTrace.java
@@ -1,5 +1,7 @@
package avatartranslator.modelchecker;
+import java.util.ArrayList;
+import java.util.HashMap;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
@@ -12,12 +14,14 @@ public class CounterexampleTrace {
private LinkedList<CounterexampleTraceState> trace;
private CounterexampleTraceState counterexampleState;
private AvatarSpecification spec;
+ private List<String> autTraces;
public CounterexampleTrace(AvatarSpecification spec) {
this.trace = null;
this.counterexampleState = null;
this.spec = spec;
+ this.autTraces = null;
}
@@ -31,6 +35,24 @@ public class CounterexampleTrace {
}
+ public void reset() {
+ this.trace = null;
+ this.counterexampleState = null;
+ }
+
+
+ public List<String> getAUTTrace() {
+ return autTraces;
+ }
+
+
+ public void resetAUTTrace() {
+ if (autTraces != null) {
+ autTraces.clear();
+ }
+ }
+
+
public boolean buildTrace(CounterexampleTraceState cs) {
counterexampleState = cs;
return buildTrace();
@@ -135,5 +157,51 @@ public class CounterexampleTrace {
}
return s.toString();
}
+
+ public void generateTraceAUT(String name, Map<Integer, SpecificationState> states) {
+ if (trace == null) {
+ return;
+ }
+
+ if (autTraces == null) {
+ autTraces = new ArrayList<String>();
+ }
+
+ List<AvatarBlock> blocks = spec.getListOfBlocks();
+ Map<Long, Integer> statesID = new HashMap<>();
+
+ for (AvatarBlock block : blocks) {
+ if (block.getStateMachine().allStates == null) {
+ return;
+ }
+ }
+
+ SpecificationState state = null;
+
+ StringBuilder s = new StringBuilder();
+
+ int id = 0;
+
+ for (CounterexampleTraceState cs : trace) {
+ if (!statesID.containsKey(states.get(cs.hash).id)) {
+ statesID.put(states.get(cs.hash).id, id++);
+ }
+ if (state != null) {
+ for (SpecificationLink sl : state.nexts) {
+ if (sl.destinationState.hashValue == cs.hash) {
+ s.append("(" + statesID.get(sl.originState.id) + ",\"" + sl.action + "\"," + statesID.get(sl.destinationState.id) + ")\n");
+ break;
+ }
+ }
+ }
+ state = states.get(cs.hash);
+ }
+
+
+ s.insert(0 ,"des(0," + (trace.size() - 1) + "," + statesID.size() + ")\n");
+
+
+ autTraces.add(s.toString());
+ }
}
diff --git a/src/main/java/avatartranslator/modelchecker/SpecificationState.java b/src/main/java/avatartranslator/modelchecker/SpecificationState.java
index 2daca5375773d7ab5e8ed08096edcabfa8993772..6e72e75e54e5a9323cf7a32eccc59e80ed5e3f4b 100644
--- a/src/main/java/avatartranslator/modelchecker/SpecificationState.java
+++ b/src/main/java/avatartranslator/modelchecker/SpecificationState.java
@@ -66,13 +66,13 @@ public class SpecificationState implements Comparable<SpecificationState> {
public boolean property; //trace the property check at this state
public boolean elaborated; //true only if the elaboration has been completed
public ArrayList<SpecificationTransition> transitions;
- public long distance; //max #steps to be reached from S0
+// public long distance; //max #steps to be reached from S0
public SpecificationState() {
hashComputed = false;
property = false;
elaborated = false;
- distance = 0;
+// distance = 0;
}
// blocks must not be null
diff --git a/src/main/java/cli/Action.java b/src/main/java/cli/Action.java
index 3146842521e268401da58db6034b6e599b2e547b..9517a5e392ecb278aee3ac92909a47444e9cf6d1 100644
--- a/src/main/java/cli/Action.java
+++ b/src/main/java/cli/Action.java
@@ -853,7 +853,8 @@ public class Action extends Command {
+ "-d\tno deadlocks verification\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";
+ + "-c\tconsider full concurrency between actions\n"
+ + "-v FILE\tsave counterexample traces for pragmas in FILE";
}
public String getExample() {
@@ -874,6 +875,7 @@ public class Action extends Command {
//String graphPath = commands[commands.length - 1];
String graphPath = "";
+ String counterPath = "";
AvatarSpecification avspec = interpreter.mgui.gtm.getAvatarSpecification();
if(avspec == null) {
@@ -886,6 +888,7 @@ public class Action extends Command {
amc.setIgnoreInternalStates(true);
amc.setComputeRG(false);
boolean rgGraph = false;
+ boolean counterTraces = false;
boolean reachabilityAnalysis = false;
boolean livenessAnalysis = false;
boolean safetyAnalysis = false;
@@ -985,6 +988,15 @@ public class Action extends Command {
//concurrency
amc.setIgnoreConcurrenceBetweenInternalActions(false);
break;
+ case "-v":
+ if (i != commands.length - 1) {
+ counterPath = commands[++i];
+ amc.setCounterExampleTrace(true, false);
+ counterTraces = true;
+ } else {
+ return Interpreter.BAD;
+ }
+ break;
default:
return Interpreter.BAD;
}
@@ -1010,6 +1022,28 @@ public class Action extends Command {
if (safetyAnalysis) {
interpreter.print("Safety Analysis:\n" + amc.safetyToString());
}
+
+
+ DateFormat dateFormat = new SimpleDateFormat("_yyyyMMdd_HHmmss");
+ Date date = new Date();
+ String dateAndTime = dateFormat.format(date);
+
+ if (counterTraces) {
+ String trace = amc.getCounterTrace();
+
+ String autfile;
+ if (counterPath.indexOf("$") != -1) {
+ autfile = Conversion.replaceAllChar(counterPath, '$', dateAndTime);
+ } else {
+ autfile = counterPath;
+ }
+ try {
+ FileUtils.saveFile(autfile, trace);
+ System.out.println("\nCounterexample trace saved in " + autfile + "\n");
+ } catch (Exception e) {
+ System.out.println("\nCounterexample trace could not be saved in " + autfile + "\n");
+ }
+ }
// Saving graph
if (rgGraph) {
@@ -1024,9 +1058,6 @@ public class Action extends Command {
if (graphPath.indexOf("?") != -1) {
//System.out.println("Question mark found");
- DateFormat dateFormat = new SimpleDateFormat("_yyyyMMdd_HHmmss");
- Date date = new Date();
- String dateAndTime = dateFormat.format(date);
autfile = Conversion.replaceAllChar(graphPath, '?', dateAndTime);
//System.out.println("graphpath=" + graphPath);
} else {
diff --git a/src/main/java/ui/window/JDialogAvatarModelChecker.java b/src/main/java/ui/window/JDialogAvatarModelChecker.java
index b3ccbac29ac0767789a92bb8ee4b8f6790432e52..9a97fb1ce519444f3bf2154afb7f1068f991e855 100644
--- a/src/main/java/ui/window/JDialogAvatarModelChecker.java
+++ b/src/main/java/ui/window/JDialogAvatarModelChecker.java
@@ -63,6 +63,7 @@ import java.text.SimpleDateFormat;
import java.util.ArrayList;
import java.util.Date;
import java.util.HashMap;
+import java.util.List;
import java.util.LinkedList;
import java.util.Map;
import java.util.TimerTask;
@@ -727,7 +728,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
amc.setIgnoreInternalStates(ignoreInternalStatesSelected);
amc.setCheckNoDeadlocks(checkNoDeadSelected);
amc.setReinitAnalysis(checkReinitSelected);
- amc.setCounterExampleTrace(generateCountertraceSelected);
+ amc.setCounterExampleTrace(generateCountertraceSelected, false);
// Reachability
int res;
@@ -912,6 +913,14 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
} catch (Exception e) {
jta.append("\nCounterexample trace could not be saved in " + autfile + "\n");
}
+
+ List<String> autTraces = amc.getAUTTraces();
+ if (autTraces != null) {
+ for (String tr : autTraces) {
+ System.out.println(tr + "\n");
+ mgui.showAUTFromString("Last RG", tr);
+ }
+ }
}
if (saveGraphAUT.isSelected()) {
@@ -1081,7 +1090,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
}
}
- countertrace.setEnabled(safety.isSelected());
+ countertrace.setEnabled(safety.isSelected() || noDeadlocks.isSelected());
countertraceField.setEnabled(countertrace.isSelected());
generateCountertraceSelected = countertrace.isSelected();
diff --git a/ttool/src/test/java/avatartranslator/AvatarExpressionTest.java b/ttool/src/test/java/avatartranslator/AvatarExpressionTest.java
index 96318fb4bcb1b693fc76f949b32f1e07511d709b..a76a076d8afabc8af08b6e490bee157baad5a5a6 100644
--- a/ttool/src/test/java/avatartranslator/AvatarExpressionTest.java
+++ b/ttool/src/test/java/avatartranslator/AvatarExpressionTest.java
@@ -111,7 +111,7 @@ public class AvatarExpressionTest {
assertTrue(e3.buildExpression());
AvatarExpressionSolver e4 = new AvatarExpressionSolver("1 && 0 >= 1 || 0");
assertFalse(e4.buildExpression());
- AvatarExpressionSolver e5 = new AvatarExpressionSolver("true and not(false) == not(false or false)");
+ AvatarExpressionSolver e5 = new AvatarExpressionSolver("true and not(false) == !(false or false)");
assertTrue(e5.buildExpression());
AvatarExpressionSolver e6 = new AvatarExpressionSolver("10 -Cabin.match");
assertFalse(e6.buildExpression());