diff --git a/src/avatartranslator/AvatarElement.java b/src/avatartranslator/AvatarElement.java
index c4ee96209ada7ac7056b8f640b07c328af7f128f..a31c151be6798f3b9558c879c6e6ea789744e7e8 100644
--- a/src/avatartranslator/AvatarElement.java
+++ b/src/avatartranslator/AvatarElement.java
@@ -64,6 +64,17 @@ public class AvatarElement {
referenceObject = _referenceObject;
}
+ public void addReferenceObjectFrom(AvatarElement _elt) {
+ addReferenceObject(_elt.getReferenceObject());
+ Vector<Object> others = _elt.getReferenceObjects();
+ if (others != null) {
+ for(Object o: others) {
+ addReferenceObject(o);
+ }
+ }
+
+ }
+
public void addReferenceObject(Object _ref) {
if (otherReferenceObjects == null) {
otherReferenceObjects = new Vector<Object>();
@@ -99,6 +110,10 @@ public class AvatarElement {
return referenceObject;
}
+ public Vector<Object> getReferenceObjects() {
+ return otherReferenceObjects;
+ }
+
public int getID(){
return myID;
}
diff --git a/src/avatartranslator/AvatarSpecification.java b/src/avatartranslator/AvatarSpecification.java
index a18ea6b387fd6296a4653091555d8cfe4eb618a6..01fa3a3dd3e2ba293fa69f0389da8f0e9ee114c9 100644
--- a/src/avatartranslator/AvatarSpecification.java
+++ b/src/avatartranslator/AvatarSpecification.java
@@ -416,6 +416,15 @@ public class AvatarSpecification extends AvatarElement {
return false;
}
+
+ public void removeEmptyTransitions() {
+ for (AvatarBlock block: this.blocks) {
+ AvatarStateMachine asm = block.getStateMachine ();
+ if (asm != null)
+ asm.removeEmptyTransitions (block);
+ }
+ }
+
public void makeRobustness() {
TraceManager.addDev("Make robustness");
if (robustnessMade) {
diff --git a/src/avatartranslator/AvatarStateMachine.java b/src/avatartranslator/AvatarStateMachine.java
index a0b3a941887cadcabfabb801415661686e8f6b11..5bd43c334e275f586c471a93697a778c2e32c172 100644
--- a/src/avatartranslator/AvatarStateMachine.java
+++ b/src/avatartranslator/AvatarStateMachine.java
@@ -56,7 +56,7 @@ public class AvatarStateMachine extends AvatarElement {
public AvatarStateElement [] allStates;
-
+
protected LinkedList<AvatarStateMachineElement> elements;
protected AvatarStartState startState;
@@ -79,13 +79,13 @@ public class AvatarStateMachine extends AvatarElement {
}
public int getNbOfStatesElement() {
- int cpt = 0;
- for(AvatarStateMachineElement asme: elements) {
+ int cpt = 0;
+ for(AvatarStateMachineElement asme: elements) {
if (asme instanceof AvatarStateElement) {
cpt ++;
}
}
- return cpt;
+ return cpt;
}
public void addElement(AvatarStateMachineElement _element) {
@@ -112,12 +112,12 @@ public class AvatarStateMachine extends AvatarElement {
}
public void makeAllStates() {
- int cpt = 0;
- allStates = new AvatarStateElement[getNbOfStatesElement()];
+ int cpt = 0;
+ allStates = new AvatarStateElement[getNbOfStatesElement()];
for(AvatarStateMachineElement asme: elements) {
if (asme instanceof AvatarStateElement) {
allStates[cpt] = (AvatarStateElement)asme;
- cpt ++;
+ cpt ++;
}
}
}
@@ -252,25 +252,25 @@ public class AvatarStateMachine extends AvatarElement {
previous = getPreviousElementOf(elt);
next = elt.getNext(0);
- if (!(next instanceof AvatarState)) {
- // We create an intermediate state
+ if (!(next 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);
- tr.removeAllNexts();
+ tr.removeAllNexts();
tr.addNext(state);
state.addNext(at1);
at1.addNext(next);
id ++;
- }
+ }
}
}
}
- for(AvatarStateMachineElement add: toAdd) {
+ for(AvatarStateMachineElement add: toAdd) {
elements.add(add);
}
}
@@ -1457,33 +1457,83 @@ public class AvatarStateMachine extends AvatarElement {
}
}
- // allstates must be computed first i.e. non null.
- // Otherwise, returns -1
- public int getIndexOfStartState() {
- if (allStates == null) {
- return -1;
- }
+ /**
+ * Removes all empty transitions between two states.
+ * This concerns also the start state, and a end state
+ * DO NOT take into account code of states, and start states
+ *
+ * @param block
+ * The block containing the state machine
+ */
+ public void removeEmptyTransitions (AvatarBlock _block) {
- for(int i=0; i<allStates.length; i++) {
- if (allStates[i] instanceof AvatarStartState) {
- return i;
+ // Look for such a transition
+ // states -> tr -> state with tr is empty
+ // a tr is empty when it has no action or guard
+ AvatarStateElement foundState1 = null, foundState2=null;
+ AvatarTransition foundAt=null;
+
+
+ for(AvatarStateMachineElement elt: elements) {
+ if ((elt instanceof AvatarStateElement) && (!(elt instanceof AvatarStartState))) {
+ if (elt.getNexts().size() == 1) {
+ AvatarTransition at = (AvatarTransition)(elt.getNext(0));
+ if (at.getNext(0) instanceof AvatarStateElement) {
+ if (at.isEmpty() && at.hasNonDeterministicGuard()) {
+ foundState1 = (AvatarStateElement) elt;
+ foundAt = at;
+ foundState2 = (AvatarStateElement)(at.getNext(0));
+ break;
+ }
+ }
+ }
+ }
+ }
+
+ // Found?
+ if (foundState1 != null) {
+ if( foundState1 == foundState2) {
+ // We simply remove the transition
+ removeElement(foundAt);
+ } else {
+ // Must remove state1 and at, and link all previous of state 1 to state2
+ for(AvatarStateMachineElement elt: getPreviousElementsOf(foundState1)) {
+ elt.replaceAllNext(foundState1, foundState2);
+ }
+ removeElement(foundAt);
+ removeElement(foundState1);
+ foundState2.addReferenceObjectFrom(foundState1);
+
}
- }
+ removeEmptyTransitions(_block);
+ }
+ }
- return -1;
+ public int getIndexOfStartState() {
+ if (allStates == null) {
+ return -1;
+ }
+
+ for(int i=0; i<allStates.length; i++) {
+ if (allStates[i] instanceof AvatarStartState) {
+ return i;
+ }
+ }
+
+ return -1;
}
public int getIndexOfState(AvatarStateElement _ase) {
- if (allStates == null) {
- return -1;
- }
+ if (allStates == null) {
+ return -1;
+ }
- for(int i=0; i<allStates.length; i++) {
- if (allStates[i] == _ase) {
- return i;
- }
- }
+ for(int i=0; i<allStates.length; i++) {
+ if (allStates[i] == _ase) {
+ return i;
+ }
+ }
- return -1;
+ return -1;
}
}
diff --git a/src/avatartranslator/AvatarTransition.java b/src/avatartranslator/AvatarTransition.java
index 1826767284634f38a77bc16a4ff306eb0208d419..0fa9c628b9c4553dbf47ae8aa690429eb8d8c316 100644
--- a/src/avatartranslator/AvatarTransition.java
+++ b/src/avatartranslator/AvatarTransition.java
@@ -54,9 +54,14 @@ public class AvatarTransition extends AvatarStateMachineElement {
// Type management: to be used by code generators
public static final int UNDEFINED = -1;
- public static final int TYPE_ACTION = 0;
- public static final int TYPE_SEND_SYNC = 1;
- public static final int TYPE_RECV_SYNC = 2;
+
+ public static final int TYPE_SEND_SYNC = 0;
+ public static final int TYPE_RECV_SYNC = 1;
+
+ public static final int TYPE_ACTIONONLY = 2;
+ public static final int TYPE_EMPTY = 3;
+ public static final int TYPE_METHODONLY = 4;
+ public static final int TYPE_ACTION_AND_METHOD = 5;
public int type = UNDEFINED;
@@ -96,6 +101,31 @@ public class AvatarTransition extends AvatarStateMachineElement {
return actions.size();
}
+ public static boolean isActionType(int _type) {
+ return ((_type == TYPE_ACTIONONLY) || (_type == TYPE_METHODONLY) || (_type == TYPE_ACTION_AND_METHOD));
+ }
+
+ public boolean hasMethod() {
+ for(AvatarAction aa: actions) {
+ if (aa.isAMethodCall()) {
+ return true;
+ }
+ }
+ return false;
+ }
+
+ public boolean hasAction() {
+ for(AvatarAction aa: actions) {
+ if (aa.isABasicVariableSetting()) {
+ return true;
+ }
+ if (aa.isAVariableSetting()) {
+ return true;
+ }
+ }
+ return false;
+ }
+
public LinkedList<AvatarAction> getActions () {
return this.actions;
}
@@ -231,6 +261,7 @@ public class AvatarTransition extends AvatarStateMachineElement {
}
+
public AvatarTransition cloneMe() {
AvatarTransition at = new AvatarTransition(block, getName(), getReferenceObject());
at.setGuard(getGuard());
diff --git a/src/avatartranslator/modelchecker/AvatarModelChecker.java b/src/avatartranslator/modelchecker/AvatarModelChecker.java
index d23e9816324c27951641338baa36706b783a6695..0410c233b49c1f1e3192d3c6b9df334c0daa0906 100644
--- a/src/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -53,7 +53,7 @@ import avatartranslator.*;
import myutil.*;
public class AvatarModelChecker implements Runnable {
- private final static int DEFAULT_NB_OF_THREADS = 4;
+ private final static int DEFAULT_NB_OF_THREADS = 8;
private final static int SLEEP_DURATION = 500;
private AvatarSpecification spec;
@@ -70,31 +70,41 @@ public class AvatarModelChecker implements Runnable {
private long stateID = 0;
private int blockValues;
+
+ // Otions
+ private boolean ignoreEmptyTransitions;
+
public AvatarModelChecker(AvatarSpecification _spec) {
spec = _spec;
+ ignoreEmptyTransitions = true;
}
public int getNbOfStates() {
- return states.size();
+ return states.size();
}
public int getNbOfLinks() {
- return links.size();
+ return links.size();
}
public int getNbOfPendingStates() {
- return pendingStates.size();
+ return pendingStates.size();
}
public synchronized long getStateID() {
- long tmp = stateID;
- stateID ++;
- return tmp;
+ long tmp = stateID;
+ stateID ++;
+ return tmp;
}
+ public void setIgnoreEmptyTransitions(boolean _b) {
+ ignoreEmptyTransitions = _b;
+ }
+
+
public void startModelChecking() {
stoppedBeforeEnd = false;
- stateID = 0;
+ stateID = 0;
// Remove timers, composite states, randoms
TraceManager.addDev("Reworking Avatar specification");
@@ -102,6 +112,9 @@ public class AvatarModelChecker implements Runnable {
spec.removeCompositeStates();
spec.removeRandoms();
spec.makeFullStates();
+ if (ignoreEmptyTransitions) {
+ spec.removeEmptyTransitions();
+ }
TraceManager.addDev("Preparing Avatar specification");
@@ -118,8 +131,6 @@ public class AvatarModelChecker implements Runnable {
}
-
-
public void startModelChecking(int _nbOfThreads) {
nbOfThreads = _nbOfThreads;
@@ -131,10 +142,14 @@ public class AvatarModelChecker implements Runnable {
// Compute initial state
SpecificationState initialState = new SpecificationState();
initialState.setInit(spec);
- blockValues = initialState.getBlockValues();
- initialState.id = getStateID();
- TraceManager.addDev("initialState=" + initialState.toString());
-
+ blockValues = initialState.getBlockValues();
+ initialState.id = getStateID();
+ if (ignoreEmptyTransitions) {
+ handleNonEmptyUniqueTransition(initialState);
+ }
+
+ //TraceManager.addDev("initialState=" + initialState.toString());
+ initialState.computeHash(blockValues);
states.put(initialState.hashValue, initialState);
pendingStates.add(initialState);
@@ -225,11 +240,18 @@ public class AvatarModelChecker implements Runnable {
// At first, do not merge synchronous transitions
// Simply get basics transitions
cpt = 0;
+
for(AvatarBlock block: spec.getListOfBlocks()) {
AvatarStateMachine asm = block.getStateMachine();
SpecificationBlock sb = _ss.blocks[cpt];
AvatarStateElement ase = asm.allStates[sb.values[SpecificationBlock.STATE_INDEX]];
+
+ // Handle empty transitions
+ //if (ignoreEmptyTransitions) {
+ // ase = getStateWithNonEmptyUniqueTransition(ase, block, sb);
+ //}
+
for(AvatarStateMachineElement elt: ase.getNexts()) {
if (elt instanceof AvatarTransition) {
handleAvatarTransition((AvatarTransition)elt, block, sb, cpt, transitions);
@@ -239,8 +261,8 @@ public class AvatarModelChecker implements Runnable {
cpt ++;
}
- //TraceManager.addDev("Possible transitions 1:" + transitions.size());
-
+ //TraceManager.addDev("Possible transitions 1:" + transitions.size());
+
// All locally executable transitions are now gathered.
// We simply need to select the one that are executable
// Two constraints: synchronous transactions must have a counter part
@@ -257,21 +279,23 @@ public class AvatarModelChecker implements Runnable {
if (newT != null) newTransitions.add(newT);
}
}
- } else if (tr.getType() == AvatarTransition.TYPE_ACTION) {
- newTransitions.add(tr);
- }
+ } else if (AvatarTransition.isActionType(tr.getType())) {
+ newTransitions.add(tr);
+ } else if (tr.getType() == AvatarTransition.TYPE_EMPTY) {
+ newTransitions.add(tr);
+ }
}
transitions = newTransitions;
- //TraceManager.addDev("Possible transitions 2:" + transitions.size());
+ //TraceManager.addDev("Possible transitions 2:" + transitions.size());
+
-
// Selecting only the transactions within the smallest clock interval
int clockMin=Integer.MAX_VALUE, clockMax=Integer.MAX_VALUE;
for(SpecificationTransition tr: transitions) {
clockMin = Math.min(clockMin, tr.clockMin);
clockMax = Math.min(clockMax, tr.clockMax);
}
-
+
//TraceManager.addDev("Selected clock interval:" + clockMin + "," + clockMax);
newTransitions = new ArrayList<SpecificationTransition>();
@@ -282,7 +306,7 @@ public class AvatarModelChecker implements Runnable {
}
}
transitions = newTransitions;
- //TraceManager.addDev("Possible transitions 3:" + transitions.size());
+ //TraceManager.addDev("Possible transitions 3:" + transitions.size());
// For each realizable transition
// Make it, reset clock of the involved blocks to 0, increase clockmin/clockhmax of each block
@@ -301,6 +325,11 @@ public class AvatarModelChecker implements Runnable {
// doing the synchronization
String action = executeTransition(_ss, newState, tr);
+ // Remove empty transitions if applicable
+ if (ignoreEmptyTransitions) {
+ handleNonEmptyUniqueTransition(newState);
+ }
+
// Compute the hash of the new state, and create the link to the right next state
SpecificationLink link = new SpecificationLink();
link.originState = _ss;
@@ -312,53 +341,58 @@ public class AvatarModelChecker implements Runnable {
states.put(newState.getHash(blockValues), newState);
pendingStates.add(newState);
link.destinationState = newState;
- newState.id = getStateID();
- //TraceManager.addDev("Creating new state for newState=" + newState);
+ newState.id = getStateID();
+ //TraceManager.addDev("Creating new state for newState=" + newState);
} else {
// Create a link from former state to the existing one
- //TraceManager.addDev("Similar state found State=" + newState.getHash(blockValues) + "\n" + newState + "\nsimilar=" + similar.getHash(blockValues) + "\n" + similar);
+ //TraceManager.addDev("Similar state found State=" + newState.getHash(blockValues) + "\n" + newState + "\nsimilar=" + similar.getHash(blockValues) + "\n" + similar);
link.destinationState = similar;
}
links.add(link);
}
}
+ private boolean guardResult(AvatarTransition _at, AvatarBlock _block, SpecificationBlock _sb) {
+ if (!_at.isGuarded()) {
+ return true;
+ }
+
+ // Must evaluate the guard
+ String guard = _at.getGuard().toString ();
+ String s = Conversion.replaceAllString(guard, "[", "").trim();
+ s = Conversion.replaceAllString(s, "]", "").trim();
+ return evaluateBoolExpression(s, _block, _sb);
+ }
+
private void handleAvatarTransition(AvatarTransition _at, AvatarBlock _block, SpecificationBlock _sb, int _indexOfBlock, ArrayList<SpecificationTransition> _transitionsToAdd) {
if (_at.type == AvatarTransition.UNDEFINED) {
return;
}
// Must see whether the guard is ok or not
- if (_at.isGuarded()) {
- // Must evaluate the guard
- String guard = _at.getGuard().toString ();
- String s = Conversion.replaceAllString(guard, "[", "").trim();
- s = Conversion.replaceAllString(s, "]", "").trim();
- boolean guardOk = evaluateBoolExpression(s, _block, _sb);
- //TraceManager.addDev("guard ok=" + guardOk);
- if (!guardOk) {
- return;
- }
- }
+ boolean guard = guardResult(_at, _block, _sb);
+ if (!guard) {
+ return;
+ }
SpecificationTransition st = new SpecificationTransition();
- _transitionsToAdd.add(st);
+ _transitionsToAdd.add(st);
st.init(1, _at, _block, _sb, _indexOfBlock);
// Must compute the clockmin and clockmax values
- String minDelay = _at.getMinDelay().trim();
- if ((minDelay == null) || (minDelay.length() == 0)) {
- st.clockMin = 0 - _sb.values[SpecificationBlock.CLOCKMIN_INDEX];
- } else {
- st.clockMin = evaluateIntExpression(_at.getMinDelay(), _block, _sb) - _sb.values[SpecificationBlock.CLOCKMIN_INDEX];
- }
- String maxDelay = _at.getMaxDelay().trim();
- 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];
- }
+ String minDelay = _at.getMinDelay().trim();
+ if ((minDelay == null) || (minDelay.length() == 0)) {
+ st.clockMin = 0 - _sb.values[SpecificationBlock.CLOCKMIN_INDEX];
+ } else {
+ st.clockMin = evaluateIntExpression(_at.getMinDelay(), _block, _sb) - _sb.values[SpecificationBlock.CLOCKMIN_INDEX];
+ }
+ String maxDelay = _at.getMaxDelay().trim();
+ 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];
+ }
}
@@ -399,7 +433,19 @@ public class AvatarModelChecker implements Runnable {
}
}
} else {
- at.type = AvatarTransition.TYPE_ACTION;
+ if (at.hasAction()) {
+ if (at.hasMethod()) {
+ at.type = AvatarTransition.TYPE_ACTION_AND_METHOD;
+ } else {
+ at.type = AvatarTransition.TYPE_ACTIONONLY;
+ }
+ } else {
+ if (at.hasMethod()) {
+ at.type = AvatarTransition.TYPE_METHODONLY;
+ } else {
+ at.type = AvatarTransition.TYPE_EMPTY;
+ }
+ }
}
}
}
@@ -469,7 +515,7 @@ public class AvatarModelChecker implements Runnable {
}
//TraceManager.addDev("Evaluating Int expression: " + act);
- //Thread.currentThread().dumpStack();
+ //Thread.currentThread().dumpStack();
return (int)(new IntExpressionEvaluator().getResultOf(act));
}
@@ -514,7 +560,7 @@ public class AvatarModelChecker implements Runnable {
- if (type == AvatarTransition.TYPE_ACTION) {
+ if ((AvatarTransition.isActionType(type)) || (type == AvatarTransition.TYPE_EMPTY)) {
return executeActionTransition(_previousState, _newState, _st);
} else if (type == AvatarTransition.TYPE_SEND_SYNC) {
return executeSyncTransition(_previousState, _newState, _st);
@@ -530,7 +576,7 @@ public class AvatarModelChecker implements Runnable {
// Get the attributes value list
AvatarBlock block = _st.blocks[0];
- String retAction = null;
+ String retAction = null;
for(AvatarAction aAction: _st.transitions[0].getActions()) {
// Variable affectation
@@ -544,17 +590,17 @@ public class AvatarModelChecker implements Runnable {
String nameOfVar = ((AvatarActionAssignment)aAction).getLeftHand().getName();
String act = ((AvatarActionAssignment)aAction).getRightHand().toString();
- //TraceManager.addDev("act=" + act);
-
- if (retAction == null) {
- retAction = nameOfVar + "=" + act;
- }
-
+ //TraceManager.addDev("act=" + act);
+
+ if (retAction == null) {
+ retAction = nameOfVar + "=" + act;
+ }
+
int indexVar = block.getIndexOfAvatarAttributeWithName(nameOfVar);
AvatarType type = block.getAttribute(indexVar).getType();
if (indexVar != -1) {
if (type == AvatarType.INTEGER) {
- //TraceManager.addDev("Evaluating int expr=" + act);
+ //TraceManager.addDev("Evaluating int expr=" + act);
int result = evaluateIntExpression(act, _st.blocks[0], _newState.blocks[_st.blocksInt[0]]);
_newState.blocks[_st.blocksInt[0]].values[SpecificationBlock.ATTR_INDEX+indexVar] = result;
} else if (type == AvatarType.BOOLEAN) {
@@ -569,10 +615,10 @@ public class AvatarModelChecker implements Runnable {
}
}
- if (retAction == null) {
- retAction = "";
- }
-
+ if (retAction == null) {
+ retAction = "";
+ }
+
return "i(" + _st.blocks[0].getName() + "/" + retAction + ")";
}
@@ -580,14 +626,14 @@ public class AvatarModelChecker implements Runnable {
AvatarBlock block0 = _st.blocks[0];
AvatarBlock block1 = _st.blocks[1];
AvatarActionOnSignal aaoss, aaosr;
- AvatarAttribute avat;
+ AvatarAttribute avat;
String value;
- int result;
- boolean resultB;
- int indexVar;
- String nameOfVar;
- String ret = "";
-
+ int result;
+ boolean resultB;
+ int indexVar;
+ String nameOfVar;
+ String ret = "";
+
try {
aaoss = (AvatarActionOnSignal)(_st.transitions[0].getNext(0));
@@ -603,49 +649,106 @@ public class AvatarModelChecker implements Runnable {
avat = aaoss.getSignal().getListOfAttributes().get(i);
if (avat.getType() == AvatarType.INTEGER) {
//TraceManager.addDev("Evaluating expression, value=" + value);
- //TraceManager.addDev("Evaluating int expr=" + value);
+ //TraceManager.addDev("Evaluating int expr=" + value);
result = evaluateIntExpression(value, block0, _newState.blocks[_st.blocksInt[0]]);
} else if (avat.getType() == AvatarType.BOOLEAN) {
resultB = evaluateBoolExpression(value, block0, _newState.blocks[_st.blocksInt[0]]);
- result = resultB? 1 : 0;
+ result = resultB? 1 : 0;
} else {
- result = 0;
- }
-
- // Putting the result to the destination var
- nameOfVar = aaosr.getValue(i);
- indexVar = block1.getIndexOfAvatarAttributeWithName(nameOfVar);
- _newState.blocks[_st.blocksInt[1]].values[SpecificationBlock.ATTR_INDEX+indexVar] = result;
- ret += "" + result;
+ result = 0;
+ }
+
+ // Putting the result to the destination var
+ nameOfVar = aaosr.getValue(i);
+ indexVar = block1.getIndexOfAvatarAttributeWithName(nameOfVar);
+ _newState.blocks[_st.blocksInt[1]].values[SpecificationBlock.ATTR_INDEX+indexVar] = result;
+ ret += "" + result;
} catch (Exception e) {
TraceManager.addDev("EXCEPTION on adding value " + aaoss);
}
}
- return "!" + aaoss.getSignal().getName() + "_?" + aaosr.getSignal().getName() + "("+ ret + ")";
-
+ return "!" + aaoss.getSignal().getName() + "_?" + aaosr.getSignal().getName() + "("+ ret + ")";
+
}
- public String toString() {
- StringBuffer sb = new StringBuffer("States:\n");
- for(SpecificationState state: states.values()) {
- sb.append(state.toString() + "\n");
+ public void handleNonEmptyUniqueTransition(SpecificationState _ss) {
+ int cpt = 0;
+ for(AvatarBlock block: spec.getListOfBlocks()) {
+ AvatarStateMachine asm = block.getStateMachine();
+ SpecificationBlock sb = _ss.blocks[cpt];
+ AvatarStateElement ase = asm.allStates[sb.values[SpecificationBlock.STATE_INDEX]];
+
+
+ AvatarStateElement aseAfter = getStateWithNonEmptyUniqueTransition(ase, block, sb);
+ if (aseAfter != ase) {
+ // Must modify the state of the considered block
+ sb.values[SpecificationBlock.STATE_INDEX] = asm.getIndexOfState(aseAfter);
+ }
+ cpt ++;
+ }
+ }
+
+ private AvatarStateElement getStateWithNonEmptyUniqueTransition(AvatarStateElement _ase, AvatarBlock _block, SpecificationBlock _sb) {
+ return getStateWithNonEmptyUniqueTransitionArray(_ase, _block, _sb, null);
+ }
+
+ private AvatarStateElement getStateWithNonEmptyUniqueTransitionArray(AvatarStateElement _ase, AvatarBlock _block, SpecificationBlock _sb, ArrayList<AvatarStateElement> listOfStates ) {
+ if (_ase.getNexts().size() != 1) {
+ return _ase;
}
- sb.append("\nLinks:\n");
- for(SpecificationLink link: links) {
- sb.append(link.toString() + "\n");
+
+ AvatarTransition at = (AvatarTransition)(_ase.getNext(0));
+
+ if(!((at.type == AvatarTransition.TYPE_EMPTY) || (at.type == AvatarTransition.TYPE_METHODONLY))) {
+ return _ase;
+ }
+
+ // Check guard;
+ boolean guard = guardResult(at, _block, _sb);
+
+ if (!guard) {
+ return _ase;
+ }
+
+ AvatarStateElement ase = (AvatarStateElement)(at.getNext(0));
+ if (listOfStates == null) {
+ if (ase == _ase) {
+ return _ase;
+ }
+ listOfStates = new ArrayList<AvatarStateElement>();
+ } else {
+ if (listOfStates.contains(ase)) {
+ return _ase;
+ }
+ }
+ listOfStates.add(_ase);
+
+ return getStateWithNonEmptyUniqueTransitionArray(ase, _block, _sb, listOfStates);
+
+
}
- return sb.toString();
+
+ public String toString() {
+ StringBuffer sb = new StringBuffer("States:\n");
+ for(SpecificationState state: states.values()) {
+ sb.append(state.toString() + "\n");
+ }
+ sb.append("\nLinks:\n");
+ for(SpecificationLink link: links) {
+ sb.append(link.toString() + "\n");
+ }
+ return sb.toString();
}
public String toAUT() {
StringBuffer sb = new StringBuffer();
sb.append("des(0," + getNbOfLinks() + "," + getNbOfStates() + ")\n");
-
+
for(SpecificationLink link: links){
- sb.append("(" + link.originState.id + ",\"" + link.action + "\"," + link.destinationState.id + ")\n");
+ sb.append("(" + link.originState.id + ",\"" + link.action + "\"," + link.destinationState.id + ")\n");
}
return new String(sb);
}
@@ -653,13 +756,13 @@ public class AvatarModelChecker implements Runnable {
public String toDOT() {
StringBuffer sb = new StringBuffer();
sb.append("digraph TToolAvatarGraph {\n");
-
+
for(SpecificationLink link: links){
- sb.append(" " + link.originState.id + " -> " + link.destinationState.id + "[label=\"" + link.action + "\"];\n");
+ sb.append(" " + link.originState.id + " -> " + link.destinationState.id + "[label=\"" + link.action + "\"];\n");
}
- sb.append("}");
+ sb.append("}");
return new String(sb);
}
-
+
}
diff --git a/src/avatartranslator/modelchecker/SpecificationState.java b/src/avatartranslator/modelchecker/SpecificationState.java
index 1072d63e5e86d26df96512b861773c3fb2c3a6cd..daa93cb327f68d266bd81f39c24594a69f2907b6 100644
--- a/src/avatartranslator/modelchecker/SpecificationState.java
+++ b/src/avatartranslator/modelchecker/SpecificationState.java
@@ -99,7 +99,7 @@ public class SpecificationState {
cpt ++;
}
- computeHash(getBlockValues());
+ //computeHash(getBlockValues());
}
public String toString() {
diff --git a/src/ui/window/JDialogAvatarModelChecker.java b/src/ui/window/JDialogAvatarModelChecker.java
index 4e1cc82b36db5d8c5fb819c63f2eeaba69562e60..165d5a84fe355186e6d9a526f59917db73b49d8a 100644
--- a/src/ui/window/JDialogAvatarModelChecker.java
+++ b/src/ui/window/JDialogAvatarModelChecker.java
@@ -66,6 +66,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JDialog implements Ac
protected static boolean graphSelected = false;
protected static String graphDirDot;
protected static boolean graphSelectedDot = false;
+ protected static boolean ignoreEmptyTransitionsSelected = true;
protected MainGUI mgui;
@@ -94,7 +95,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JDialog implements Ac
//protected JLabel gen, comp;
//protected JTextField code1, code2, unitcycle, compiler1, exe1, exe2, exe3, exe2int, loopLimit;
- protected JCheckBox saveGraphAUT, saveGraphDot;
+ protected JCheckBox saveGraphAUT, saveGraphDot, ignoreEmptyTransitions;
protected JTextField graphPath, graphPathDot;
protected JTabbedPane jp1;
protected JScrollPane jsp;
@@ -156,6 +157,9 @@ public class JDialogAvatarModelChecker extends javax.swing.JDialog implements Ac
c01.weightx = 1.0;
c01.fill = GridBagConstraints.HORIZONTAL;
c01.gridwidth = GridBagConstraints.REMAINDER; //end row
+ ignoreEmptyTransitions = new JCheckBox("IgnoreEmptyTransitions", ignoreEmptyTransitionsSelected);
+ ignoreEmptyTransitions.addActionListener(this);
+ jp01.add(ignoreEmptyTransitions, c01);
saveGraphAUT = new JCheckBox("Save RG (AUT format) in:", graphSelected);
saveGraphAUT.addActionListener(this);
jp01.add(saveGraphAUT, c01);
@@ -215,6 +219,8 @@ public class JDialogAvatarModelChecker extends javax.swing.JDialog implements Ac
setButtons();
} else if (evt.getSource() == saveGraphDot) {
setButtons();
+ } else if (evt.getSource() == ignoreEmptyTransitions) {
+ setButtons();
}
}
@@ -261,8 +267,11 @@ public class JDialogAvatarModelChecker extends javax.swing.JDialog implements Ac
try {
jta.append("Starting the model checker\n");
amc = new AvatarModelChecker(spec);
-
-
+
+ // Setting options
+ amc.setIgnoreEmptyTransitions(ignoreEmptyTransitionsSelected);
+
+ // Starting model checking
testGo();
amc.startModelChecking();
@@ -313,6 +322,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JDialog implements Ac
graphPath.setEnabled(saveGraphAUT.isSelected());
graphSelectedDot = saveGraphDot.isSelected();
graphPathDot.setEnabled(saveGraphDot.isSelected());
+ ignoreEmptyTransitionsSelected = ignoreEmptyTransitions.isSelected();
switch(mode) {
case NOT_STARTED:
start.setEnabled(true);