diff --git a/src/main/java/avatartranslator/AvatarBlock.java b/src/main/java/avatartranslator/AvatarBlock.java
index 4ff2d674eb4fd398e85e339be42ffd89ede0fd16..511d0ebf1ca40d3fe58a75f48cbe676b00894a11 100644
--- a/src/main/java/avatartranslator/AvatarBlock.java
+++ b/src/main/java/avatartranslator/AvatarBlock.java
@@ -57,6 +57,7 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
private List<AvatarSignal> signals;
private AvatarStateMachine asm;
private AvatarSpecification avspec;
+ private int blockIndex; //Index of block in the Avatar Specification
private String globalCode;
@@ -253,6 +254,14 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
public AvatarAttribute getAttribute(int _index) {
return attributes.get(_index);
}
+
+ public int getBlockIndex() {
+ return blockIndex;
+ }
+
+ public void setBlockIndex(int _blockIndex) {
+ blockIndex = _blockIndex;
+ }
public boolean setAttributeValue(int _index, String _value) {
AvatarAttribute aa = attributes.get(_index);
diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index 5f8ac57c61369cde9dbecf7abdd892efb484d1f1..581a38e379537e22275d971ecf5ea1034a6ebc66 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -342,6 +342,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
stateLimitRG = false;
timeLimitRG = false;
+ ignoreEmptyTransitions = true;
studyR = studyReachability;
studyL = studyLiveness;
studyS = studySafety;
@@ -468,16 +469,15 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
}
- //initialState.id = 0//getStateID();
if (ignoreEmptyTransitions) {
handleNonEmptyUniqueTransition(initialState);
}
-
- prepareTransitionsOfState(initialState);
+//
+// prepareTransitionsOfState(initialState);
blockValues = initialState.getBlockValues();
initialState.distance = 0;
- TraceManager.addDev("initialState=" + initialState.toString() + "\n nbOfTransitions" + initialState.transitions.size());
+ //TraceManager.addDev("initialState=" + initialState.toString() + "\n nbOfTransitions" + initialState.transitions.size());
initialState.computeHash(blockValues);
addState(initialState);
@@ -522,11 +522,8 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
// initialState's transitions and blocks must be already initialized
blockValues = initialState.getBlockValues();
initialState.distance = 0;
-
- // properties are not tested on the initial node. The property is reset
- initialState.property = false;
- TraceManager.addDev("initialState=" + initialState.toString() + "\n nbOfTransitions" + initialState.transitions.size());
+ //TraceManager.addDev("initialState=" + initialState.toString() + "\n nbOfTransitions" + initialState.transitions.size());
initialState.computeHash(blockValues);
addState(initialState);
@@ -536,11 +533,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
//statesByID.put(initialState.id, initialState);
nbOfCurrentComputations = 0;
- if (timeLimitRG) {
- computeAllStatesTime();
- } else {
- computeAllStates();
- }
+ computeAllStates();
// All done
}
@@ -580,6 +573,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
//TraceManager.addDev("Preparing Avatar specification :" + spec.toString());
prepareStates();
prepareTransitions();
+ prepareBlocks();
nbOfThreads = Runtime.getRuntime().availableProcessors();
@@ -813,6 +807,8 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
mustStop();
return;
}
+
+ prepareTransitionsOfState(_ss);
ArrayList<SpecificationTransition> transitions = _ss.transitions;
if (transitions == null) {
@@ -948,11 +944,11 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
newState.property = evaluateSafetyOfProperty(newState, tr, _ss.property);
}
- // Remove empty transitions if applicable
+// // Remove empty transitions if applicable
if (ignoreEmptyTransitions) {
handleNonEmptyUniqueTransition(newState);
}
- prepareTransitionsOfState(newState);
+// prepareTransitionsOfState(newState);
// Compute the hash of the new state, and create the link to the right next state
@@ -1208,7 +1204,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
SpecificationTransition st = new SpecificationTransition();
st.fromStateWithMoreThanOneTransition = _fromStateWithMoreThanOneTransition;
_transitionsToAdd.add(st);
- st.init(1, _at, _block, _sb, _indexOfBlock);
+ st.init(1, _at, _indexOfBlock);
// Must compute the clockmin and clockmax values
String minDelay = _at.getMinDelay().trim();
@@ -1292,6 +1288,13 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
}
}
+
+ private void prepareBlocks() {
+ int i = 0;
+ for (AvatarBlock ab : spec.getListOfBlocks()) {
+ ab.setBlockIndex(i++);
+ }
+ }
public boolean oldEvaluateBoolExpression(String _expr, AvatarBlock _block, SpecificationBlock _sb) {
String act = _expr;
@@ -1428,7 +1431,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
//int index = _st.blocks[i].getStateMachine().getIndexOfState(ase);
int index = _st.transitions[i].getBlock().getStateMachine().getIndexOfState(ase);
if (index > -1) {
- _newState.blocks[_st.blocksInt[i]].values[SpecificationBlock.STATE_INDEX] = index;
+ _newState.blocks[((AvatarBlock) _st.transitions[i].getBlock()).getBlockIndex()].values[SpecificationBlock.STATE_INDEX] = index;
}
}
}
@@ -1485,7 +1488,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
retAction = nameOfVar + "=" + act;
}
- ((AvatarActionAssignment) aAction).executeActionSolver(_newState.blocks[_st.blocksInt[0]]);
+ ((AvatarActionAssignment) aAction).executeActionSolver(_newState.blocks[((AvatarBlock) _st.transitions[0].getBlock()).getBlockIndex()]);
// int indexVar = block.getIndexOfAvatarAttributeWithName(nameOfVar);
// AvatarType type = block.getAttribute(indexVar).getType();
@@ -1562,8 +1565,8 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
// }
for (int i = 0; i < aaoss.getNbOfValues(); i++) {
// try {
- result = aaoss.getExpressionAttribute(i).getValue(_newState.blocks[_st.blocksInt[0]]);
- aaosr.getExpressionAttribute(i).setValue(_newState.blocks[_st.blocksInt[1]], result);
+ result = aaoss.getExpressionAttribute(i).getValue(_newState.blocks[((AvatarBlock) _st.transitions[0].getBlock()).getBlockIndex()]);
+ aaosr.getExpressionAttribute(i).setValue(_newState.blocks[((AvatarBlock) _st.transitions[1].getBlock()).getBlockIndex()], result);
ret += "" + result;
// } catch (Exception e) {
// TraceManager.addDev("EXCEPTION on adding value " + aaoss);
@@ -1746,7 +1749,6 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (similar == null) {
if (newState.property) {
SpecificationState state = newState.advancedClone();
- state.transitions = newState.transitions;
safetyLeadStates.add(state);
newState.property = false;
}
diff --git a/src/main/java/avatartranslator/modelchecker/SpecificationTransition.java b/src/main/java/avatartranslator/modelchecker/SpecificationTransition.java
index a44e68f79b0b5fc57b41bf8414a726f84ad50ee8..f70c8e73ea7cb10ab21d069c8397d375b9bcfd9b 100644
--- a/src/main/java/avatartranslator/modelchecker/SpecificationTransition.java
+++ b/src/main/java/avatartranslator/modelchecker/SpecificationTransition.java
@@ -54,25 +54,17 @@ import avatartranslator.AvatarTransition;
*/
public class SpecificationTransition {
public int clockMin, clockMax;
-
public boolean fromStateWithMoreThanOneTransition;
-
- public int[] blocksInt;
-
public AvatarTransition[] transitions;
-
public String infoForGraph;
public SpecificationTransition() {
}
- public void init(int _nbOfElements, AvatarTransition _at, AvatarBlock _ab, SpecificationBlock _sb, int _blockIndex) {
+ public void init(int _nbOfElements, AvatarTransition _at, int _blockIndex) {
transitions = new AvatarTransition[_nbOfElements];
transitions[0] = _at;
-
- blocksInt = new int[_nbOfElements];
- blocksInt[0] = _blockIndex;
}
public int getType() {
@@ -89,13 +81,8 @@ public class SpecificationTransition {
transitions[0] = _tr1.transitions[0];
transitions[1] = _tr2.transitions[0];
- blocksInt = new int[nbOfElements];
- blocksInt[0] = _tr1.blocksInt[0];
- blocksInt[1] = _tr2.blocksInt[0];
-
clockMin = Math.max(_tr1.clockMin, _tr2.clockMin);
clockMax = Math.max(_tr1.clockMax, _tr2.clockMax);
-
}
public boolean hasBlockOf(SpecificationTransition _tr) {
@@ -120,27 +107,21 @@ public class SpecificationTransition {
public boolean hasBlockIndex(int _index) {
- if (blocksInt == null) {
+ if (transitions == null) {
return false;
}
-
- for(int i=0; i<blocksInt.length; i++) {
- if (blocksInt[i] == _index) {
+
+ for(int i = 0; i<transitions.length; i++) {
+ if (((AvatarBlock) transitions[i].getBlock()).getBlockIndex() == _index) {
return true;
}
}
-
return false;
}
public String toString() {
String ret = "Trans: ";
-// if (blocks != null) {
-// for (int i=0; i<blocks.length; i++) {
-// ret += "/ Block" + i + ": " + blocks[i].getName();
-// }
-// }
if (transitions != null) {
for (int i = 0; i < transitions.length; i++) {
ret += "/ Block" + i + ": " + transitions[i].getBlock().getName() + "/" + transitions[i];
diff --git a/src/main/java/ui/window/JDialogAvatarModelChecker.java b/src/main/java/ui/window/JDialogAvatarModelChecker.java
index 5722554a9a6935bbda956bfdf46a35a429e8ea8d..5f4907a802240911c78c5773415496fe8e5687a0 100644
--- a/src/main/java/ui/window/JDialogAvatarModelChecker.java
+++ b/src/main/java/ui/window/JDialogAvatarModelChecker.java
@@ -560,9 +560,6 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
reinitValues();
jta.append("Starting the model checker\n");
-
-
-
amc = new AvatarModelChecker(spec);
if (generateDesignSelected) {
@@ -891,7 +888,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) || safetySelected|| graphSelected || graphSelectedDot) {
+ if ((reachabilitySelected == REACHABILITY_SELECTED) || (reachabilitySelected == REACHABILITY_ALL) || (livenessSelected == LIVENESS_SELECTED) || (livenessSelected == LIVENESS_ALL) || safetySelected || checkNoDeadSelected || graphSelected || graphSelectedDot) {
start.setEnabled(true);
} else {
start.setEnabled(false);