diff --git a/src/avatartranslator/AvatarStateMachine.java b/src/avatartranslator/AvatarStateMachine.java
index 5bd43c334e275f586c471a93697a778c2e32c172..120cecd9c0f7938476403eed810519bfac560f4d 100644
--- a/src/avatartranslator/AvatarStateMachine.java
+++ b/src/avatartranslator/AvatarStateMachine.java
@@ -238,6 +238,9 @@ public class AvatarStateMachine extends AvatarElement {
// Hanlding transitions with actions which have a non state
// after
+
+ // Then, handling transitions with actions which have a non state
+ // before
private void addStatesToTransitionsWithActions(AvatarBlock _block) {
AvatarStateMachineElement next;
AvatarStateMachineElement previous;
@@ -268,13 +271,47 @@ public class AvatarStateMachine extends AvatarElement {
}
}
}
+
}
for(AvatarStateMachineElement add: toAdd) {
elements.add(add);
}
+ toAdd.clear();
+
+ for(AvatarStateMachineElement elt: elements) {
+ if (elt instanceof AvatarTransition) {
+ AvatarTransition tr = (AvatarTransition)elt;
+
+ // tr with actions?
+ if (tr.getNbOfAction() > 0) {
+ previous = getPreviousElementOf(elt);
+ next = elt.getNext(0);
+ if (!(previous instanceof AvatarState)) {
+ // We create an intermediate state
+ AvatarState state = new AvatarState("IntermediateState__" + id, elt.getReferenceObject());
+ toAdd.add(state);
+ AvatarTransition at1 = new AvatarTransition(_block, "TransitionForIntermediateState__" + id, elt.getReferenceObject());
+ toAdd.add(at1);
+
+ previous.removeAllNexts();
+ previous.addNext(at1);
+ at1.addNext(state);
+ state.addNext(tr);
+ id ++;
+ }
+ }
+ }
+ }
+
+ for(AvatarStateMachineElement add: toAdd) {
+ elements.add(add);
+ }
+
}
+
+
public void removeRandoms(AvatarBlock _block) {
int id = 0;
diff --git a/src/avatartranslator/modelchecker/AvatarModelChecker.java b/src/avatartranslator/modelchecker/AvatarModelChecker.java
index f696d45057d444407f876c49ce1a4b319bfbc00c..dbb7ff977307b9820dcd9eb6262988ac8db937b0 100644
--- a/src/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -147,6 +147,7 @@ public class AvatarModelChecker implements Runnable {
// Compute initial state
SpecificationState initialState = new SpecificationState();
initialState.setInit(spec);
+ prepareTransitionsOfState(initialState);
blockValues = initialState.getBlockValues();
initialState.id = getStateID();
if (ignoreEmptyTransitions) {
@@ -235,12 +236,9 @@ public class AvatarModelChecker implements Runnable {
nbOfCurrentComputations = 0;
}
-
- private void computeAllStatesFrom(SpecificationState _ss) {
- int cpt;
-
- // For each block, get the list of possible transactions
- ArrayList<SpecificationTransition> transitions = new ArrayList<SpecificationTransition>();
+ private void prepareTransitionsOfState(SpecificationState _ss) {
+ int cpt;
+ _ss.transitions = new ArrayList<SpecificationTransition>();
// At first, do not merge synchronous transitions
// Simply get basics transitions
@@ -253,12 +251,17 @@ public class AvatarModelChecker implements Runnable {
for(AvatarStateMachineElement elt: ase.getNexts()) {
if (elt instanceof AvatarTransition) {
- handleAvatarTransition((AvatarTransition)elt, block, sb, cpt, transitions);
+ handleAvatarTransition((AvatarTransition)elt, block, sb, cpt, _ss.transitions);
}
}
cpt ++;
}
+ }
+
+
+ private void computeAllStatesFrom(SpecificationState _ss) {
+ ArrayList<SpecificationTransition> transitions = _ss.transitions;
TraceManager.addDev("Possible transitions 1:" + transitions.size());
@@ -355,6 +358,7 @@ public class AvatarModelChecker implements Runnable {
// Impact the variable of the state, either by executing actions, or by
// doing the synchronization
String action = executeTransition(_ss, newState, tr);
+ prepareTransitionsOfState(newState);
// Remove empty transitions if applicable
if (ignoreEmptyTransitions) {
@@ -382,6 +386,7 @@ public class AvatarModelChecker implements Runnable {
}
links.add(link);
}
+ _ss.finished();
}
private boolean guardResult(AvatarTransition _at, AvatarBlock _block, SpecificationBlock _sb) {
@@ -422,7 +427,9 @@ public class AvatarModelChecker implements Runnable {
if ((maxDelay == null) || (maxDelay.length() == 0)) {
st.clockMax = 0 - _sb.values[SpecificationBlock.CLOCKMAX_INDEX];
} else {
- st.clockMax = evaluateIntExpression(_at.getMaxDelay(), _block, _sb) - _sb.values[SpecificationBlock.CLOCKMAX_INDEX];
+ int resMax = evaluateIntExpression(_at.getMaxDelay(), _block, _sb);
+ _sb.maxClock = Math.max(_sb.maxClock, resMax);
+ st.clockMax = resMax - _sb.values[SpecificationBlock.CLOCKMAX_INDEX];
}
}
@@ -525,7 +532,7 @@ public class AvatarModelChecker implements Runnable {
}
public int evaluateIntExpression(String _expr, AvatarBlock _block, SpecificationBlock _sb) {
- TraceManager.addDev("Evaluating Int expression 1: " + _expr);
+ //TraceManager.addDev("Evaluating Int expression 1: " + _expr);
String act = _expr;
int cpt = 0;
for(AvatarAttribute at: _block.getAttributes()) {
@@ -546,7 +553,7 @@ public class AvatarModelChecker implements Runnable {
cpt ++;
}
- TraceManager.addDev("Evaluating Int expression S: " + act);
+ //TraceManager.addDev("Evaluating Int expression S: " + act);
//Thread.currentThread().dumpStack();
return (int)(new IntExpressionEvaluator().getResultOf(act));
}
@@ -622,7 +629,7 @@ public class AvatarModelChecker implements Runnable {
String nameOfVar = ((AvatarActionAssignment)aAction).getLeftHand().getName();
String act = ((AvatarActionAssignment)aAction).getRightHand().getName();
- TraceManager.addDev("*** act=" + act);
+ //TraceManager.addDev("*** act=" + act);
if (retAction == null) {
retAction = nameOfVar + "=" + act;
diff --git a/src/avatartranslator/modelchecker/SpecificationBlock.java b/src/avatartranslator/modelchecker/SpecificationBlock.java
index 5f6b8e4974e44c52216a601c7dde8dfe1a0b380d..b1a2518d245251a8ab260ae4e5823f9b389ffedf 100644
--- a/src/avatartranslator/modelchecker/SpecificationBlock.java
+++ b/src/avatartranslator/modelchecker/SpecificationBlock.java
@@ -62,8 +62,7 @@ public class SpecificationBlock {
public static final int ATTR_INDEX = 3;
public int [] values; // state in block, clockmin, clockmax, variables
- public boolean hasTimedTransition;
- public boolean timeElapsed;
+ public int maxClock;
public SpecificationBlock() {
}
@@ -106,6 +105,7 @@ public class SpecificationBlock {
public SpecificationBlock advancedClone() {
SpecificationBlock sb = new SpecificationBlock();
sb.values = values.clone();
+ sb.maxClock = maxClock;
return sb;
}
diff --git a/src/avatartranslator/modelchecker/SpecificationState.java b/src/avatartranslator/modelchecker/SpecificationState.java
index 1425e6e986db76e015afb987220526ead50e6504..ddc3ac40e0182bc3aeb7469e7b796cb8c06f369f 100644
--- a/src/avatartranslator/modelchecker/SpecificationState.java
+++ b/src/avatartranslator/modelchecker/SpecificationState.java
@@ -61,94 +61,97 @@ public class SpecificationState {
public boolean hashComputed;
public long id;
+ public ArrayList<SpecificationTransition> transitions;
+
public SpecificationState() {
- hashComputed = false;
+ hashComputed = false;
}
// blocks must not be null
public void computeHash(int blockValues) {
- int[] hash = new int[blockValues];
- int cpt = 0;
- for(int i=0; i<blocks.length; i++) {
- for(int j=0; j<blocks[i].values.length; j++) {
- hash[cpt] = blocks[i].values[j];
- cpt++;
- }
- //TraceManager.addDev("hash[" + i + "]=" + hash[i]);
- }
- hashValue = Arrays.hashCode(hash);
- hashComputed = true;
+ int[] hash = new int[blockValues];
+ int cpt = 0;
+ for(int i=0; i<blocks.length; i++) {
+ for(int j=0; j<blocks[i].values.length; j++) {
+ hash[cpt] = blocks[i].values[j];
+ cpt++;
+ }
+ //TraceManager.addDev("hash[" + i + "]=" + hash[i]);
+ }
+ hashValue = Arrays.hashCode(hash);
+ hashComputed = true;
}
public int getHash(int blockValues) {
- if (!hashComputed) {
- computeHash(blockValues);
- }
- return hashValue;
+ if (!hashComputed) {
+ computeHash(blockValues);
+ }
+ return hashValue;
}
public void setInit(AvatarSpecification _spec) {
- int cpt = 0;
- // Initialize blocks
- // Blocks : h to 0, variables to their starting values, state to starting state.
- blocks = new SpecificationBlock[_spec.getListOfBlocks().size()];
-
- for(AvatarBlock block: _spec.getListOfBlocks()) {
- blocks[cpt] = new SpecificationBlock();
- blocks[cpt].init(block);
- cpt ++;
- }
-
- //computeHash(getBlockValues());
+ int cpt = 0;
+ // Initialize blocks
+ // Blocks : h to 0, variables to their starting values, state to starting state.
+ blocks = new SpecificationBlock[_spec.getListOfBlocks().size()];
+
+ for(AvatarBlock block: _spec.getListOfBlocks()) {
+ blocks[cpt] = new SpecificationBlock();
+ blocks[cpt].init(block);
+ cpt ++;
+ }
+
+ //computeHash(getBlockValues());
}
public String toString() {
- StringBuffer sb = new StringBuffer("id: " + id);
- for(int i=0; i<blocks.length; i++) {
- sb.append("\n "+i + ": " + blocks[i].toString());
- }
- return sb.toString();
+ StringBuffer sb = new StringBuffer("id: " + id);
+ for(int i=0; i<blocks.length; i++) {
+ sb.append("\n "+i + ": " + blocks[i].toString());
+ }
+ return sb.toString();
}
public SpecificationState advancedClone() {
- SpecificationState st = new SpecificationState();
- st.blocks = new SpecificationBlock[blocks.length];
- for(int i=0; i<blocks.length; i++) {
- st.blocks[i] = blocks[i].advancedClone();
- }
- return st;
+ SpecificationState st = new SpecificationState();
+ st.blocks = new SpecificationBlock[blocks.length];
+ for(int i=0; i<blocks.length; i++) {
+ st.blocks[i] = blocks[i].advancedClone();
+ }
+ return st;
}
// Increase the clock of the blocks not in the transition
// and having a timed transition.
// Otherwise, puts the one of others to 0
public void increaseClockOfBlocksExcept(SpecificationTransition _st) {
- SpecificationBlock sb;
- for(int i=0; i<blocks.length; i++) {
- sb = blocks[i];
- if (!(_st.hasBlockIndex(i))) {
- if (sb.hasTimedTransition()) {
- sb.values[SpecificationBlock.CLOCKMIN_INDEX] += _st.clockMin;
- sb.values[SpecificationBlock.CLOCKMAX_INDEX] += _st.clockMax;
- }
- /*else {
- sb.values[SpecificationBlock.CLOCKMIN_INDEX] = 0;
- sb.values[SpecificationBlock.CLOCKMAX_INDEX] = 0;
- }*/
- } else {
- sb.values[SpecificationBlock.CLOCKMIN_INDEX] = 0;
- sb.values[SpecificationBlock.CLOCKMAX_INDEX] = 0;
- }
- }
+ SpecificationBlock sb;
+ for(int i=0; i<blocks.length; i++) {
+ sb = blocks[i];
+ if (!(_st.hasBlockIndex(i))) {
+ sb.values[SpecificationBlock.CLOCKMIN_INDEX] += _st.clockMin;
+ sb.values[SpecificationBlock.CLOCKMAX_INDEX] += _st.clockMax;
+ sb.values[SpecificationBlock.CLOCKMIN_INDEX] = Math.min(sb.values[SpecificationBlock.CLOCKMIN_INDEX], sb.maxClock);
+ sb.values[SpecificationBlock.CLOCKMAX_INDEX] = Math.min(sb.values[SpecificationBlock.CLOCKMAX_INDEX], sb.maxClock);
+ } else {
+ sb.values[SpecificationBlock.CLOCKMIN_INDEX] = 0;
+ sb.values[SpecificationBlock.CLOCKMAX_INDEX] = 0;
+ }
+ }
}
public int getBlockValues() {
- int cpt = 0;
- for(int i=0; i<blocks.length; i++) {
- cpt += blocks[i].values.length;
- //TraceManager.addDev("hash[" + i + "]=" + hash[i]);
- }
- return cpt;
+ int cpt = 0;
+ for(int i=0; i<blocks.length; i++) {
+ cpt += blocks[i].values.length;
+ //TraceManager.addDev("hash[" + i + "]=" + hash[i]);
+ }
+ return cpt;
+ }
+
+ public void finished() {
+ //blocks = null;
+ transitions = null;
}
}