diff --git a/src/avatartranslator/modelchecker/AvatarModelChecker.java b/src/avatartranslator/modelchecker/AvatarModelChecker.java
index ccfc23c8611ce9ac97cbba8dd10e8df6b7ea6bb1..725da2a4a924a365f08b7fe6fa20397d44158360 100644
--- a/src/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -52,7 +52,7 @@ import java.util.*;
import avatartranslator.*;
import myutil.*;
-public class AvatarModelChecker implements Runnable {
+public class AvatarModelChecker implements Runnable, myutil.Graph {
private final static int DEFAULT_NB_OF_THREADS = 12;
private final static int SLEEP_DURATION = 500;
@@ -67,9 +67,11 @@ public class AvatarModelChecker implements Runnable {
// ReachabilityGraph
private Map<Integer, SpecificationState> states;
private List<SpecificationState> pendingStates;
- private List<SpecificationLink> links;
+ //private List<SpecificationLink> links;
+ private int nbOfLinks;
private long stateID = 0;
private int blockValues;
+ private boolean freeIntermediateStateCoding;
// Options
@@ -78,7 +80,7 @@ public class AvatarModelChecker implements Runnable {
// RG
private boolean computeRG;
-
+
// Reachability
private boolean studyReachability;
private ArrayList<SpecificationReachability> reachabilities;
@@ -87,9 +89,14 @@ public class AvatarModelChecker implements Runnable {
public AvatarModelChecker(AvatarSpecification _spec) {
spec = _spec;
ignoreEmptyTransitions = true;
- ignoreConcurrenceBetweenInternalActions = true;
- studyReachability = false;
- computeRG = false;
+ ignoreConcurrenceBetweenInternalActions = true;
+ studyReachability = false;
+ computeRG = false;
+ freeIntermediateStateCoding = true;
+ }
+
+ public int getWeightOfTransition(int originState, int destinationState) {
+ return 0;
}
public int getNbOfStates() {
@@ -97,7 +104,8 @@ public class AvatarModelChecker implements Runnable {
}
public int getNbOfLinks() {
- return links.size();
+ //return links.size();
+ return nbOfLinks;
}
public int getNbOfPendingStates() {
@@ -110,54 +118,58 @@ public class AvatarModelChecker implements Runnable {
return tmp;
}
+ public void setFreeIntermediateStateCoding(boolean _b) {
+ freeIntermediateStateCoding = _b;
+ }
+
public void setIgnoreEmptyTransitions(boolean _b) {
ignoreEmptyTransitions = _b;
}
public void setIgnoreConcurrenceBetweenInternalActions(boolean _b) {
- ignoreConcurrenceBetweenInternalActions = _b;
+ ignoreConcurrenceBetweenInternalActions = _b;
}
public int setReachabilityOfSelected() {
- reachabilities = new ArrayList<SpecificationReachability>();
- for(AvatarBlock block: spec.getListOfBlocks()) {
- for(AvatarStateMachineElement elt: block.getStateMachine().getListOfElements()) {
- if (elt.isCheckable()) {
- SpecificationReachability reach = new SpecificationReachability(elt);
- reachabilities.add(reach);
- }
- }
- }
- nbOfRemainingReachabilities = reachabilities.size();
- studyReachability = true;
- return nbOfRemainingReachabilities;
+ reachabilities = new ArrayList<SpecificationReachability>();
+ for(AvatarBlock block: spec.getListOfBlocks()) {
+ for(AvatarStateMachineElement elt: block.getStateMachine().getListOfElements()) {
+ if (elt.isCheckable()) {
+ SpecificationReachability reach = new SpecificationReachability(elt);
+ reachabilities.add(reach);
+ }
+ }
+ }
+ nbOfRemainingReachabilities = reachabilities.size();
+ studyReachability = true;
+ return nbOfRemainingReachabilities;
}
public int setReachabilityOfAllStates() {
- reachabilities = new ArrayList<SpecificationReachability>();
- for(AvatarBlock block: spec.getListOfBlocks()) {
- for(AvatarStateMachineElement elt: block.getStateMachine().getListOfElements()) {
- if (elt instanceof AvatarStateElement) {
- SpecificationReachability reach = new SpecificationReachability(elt);
- reachabilities.add(reach);
- }
- }
- }
- nbOfRemainingReachabilities = reachabilities.size();
- studyReachability = true;
- return nbOfRemainingReachabilities;
+ reachabilities = new ArrayList<SpecificationReachability>();
+ for(AvatarBlock block: spec.getListOfBlocks()) {
+ for(AvatarStateMachineElement elt: block.getStateMachine().getListOfElements()) {
+ if (elt instanceof AvatarStateElement) {
+ SpecificationReachability reach = new SpecificationReachability(elt);
+ reachabilities.add(reach);
+ }
+ }
+ }
+ nbOfRemainingReachabilities = reachabilities.size();
+ studyReachability = true;
+ return nbOfRemainingReachabilities;
}
public ArrayList<SpecificationReachability> getReachabilities() {
- return reachabilities;
+ return reachabilities;
}
public int getNbOfRemainingReachabilities() {
- return nbOfRemainingReachabilities;
+ return nbOfRemainingReachabilities;
}
public void setComputeRG(boolean _rg) {
- computeRG = _rg;
+ computeRG = _rg;
}
@@ -171,9 +183,9 @@ public class AvatarModelChecker implements Runnable {
spec.removeCompositeStates();
spec.removeRandoms();
spec.makeFullStates();
- if (ignoreEmptyTransitions) {
- spec.removeEmptyTransitions(nbOfRemainingReachabilities == 0);
- }
+ if (ignoreEmptyTransitions) {
+ spec.removeEmptyTransitions(nbOfRemainingReachabilities == 0);
+ }
TraceManager.addDev("Preparing Avatar specification");
@@ -196,28 +208,29 @@ public class AvatarModelChecker implements Runnable {
// Init data stuctures
states = Collections.synchronizedMap(new HashMap<Integer, SpecificationState>());
pendingStates = Collections.synchronizedList(new LinkedList<SpecificationState>());
- links = Collections.synchronizedList(new ArrayList<SpecificationLink>());
+ //links = Collections.synchronizedList(new ArrayList<SpecificationLink>());
+ nbOfLinks = 0;
+
+ // Check stop conditions
+ if (mustStop()) {
+ return;
+ }
- // Check stop conditions
- if (mustStop()) {
- return;
- }
-
// Compute initial state
SpecificationState initialState = new SpecificationState();
initialState.setInit(spec);
- for(AvatarBlock block: spec.getListOfBlocks()) {
- checkElement(block.getStateMachine().getStartState(), initialState);
- }
+ for(AvatarBlock block: spec.getListOfBlocks()) {
+ checkElement(block.getStateMachine().getStartState(), initialState);
+ }
initialState.id = getStateID();
- if (ignoreEmptyTransitions) {
- handleNonEmptyUniqueTransition(initialState);
- }
- prepareTransitionsOfState(initialState);
- blockValues = initialState.getBlockValues();
-
+ if (ignoreEmptyTransitions) {
+ handleNonEmptyUniqueTransition(initialState);
+ }
+ prepareTransitionsOfState(initialState);
+ blockValues = initialState.getBlockValues();
+
//TraceManager.addDev("initialState=" + initialState.toString());
- initialState.computeHash(blockValues);
+ initialState.computeHash(blockValues);
states.put(initialState.hashValue, initialState);
pendingStates.add(initialState);
@@ -245,15 +258,15 @@ public class AvatarModelChecker implements Runnable {
ts[i].join();} catch (Exception e){}
}
- // Set to non reachable not computed elements
- if ((studyReachability) && (!stoppedBeforeEnd)) {
- for(SpecificationReachability re: reachabilities) {
- if (re.result == SpecificationReachabilityType.NOTCOMPUTED) {
- re.result = SpecificationReachabilityType.NONREACHABLE;
- }
- }
- }
-
+ // Set to non reachable not computed elements
+ if ((studyReachability) && (!stoppedBeforeEnd)) {
+ for(SpecificationReachability re: reachabilities) {
+ if (re.result == SpecificationReachabilityType.NOTCOMPUTED) {
+ re.result = SpecificationReachabilityType.NONREACHABLE;
+ }
+ }
+ }
+
}
// MAIN LOOP
@@ -264,16 +277,16 @@ public class AvatarModelChecker implements Runnable {
boolean go = true;
while(go) {
// Pickup a state
- if ((stoppedBeforeEnd) || (stoppedConditionReached)) {
- return;
- }
-
- // Pickup a state
+ if ((stoppedBeforeEnd) || (stoppedConditionReached)) {
+ return;
+ }
+
+ // Pickup a state
s = pickupState();
- if ((stoppedBeforeEnd) || (stoppedConditionReached)) {
- return;
- }
+ if ((stoppedBeforeEnd) || (stoppedConditionReached)) {
+ return;
+ }
if (s == null) {
// Terminate
@@ -320,8 +333,8 @@ public class AvatarModelChecker implements Runnable {
}
private void prepareTransitionsOfState(SpecificationState _ss) {
- int cpt;
- _ss.transitions = new ArrayList<SpecificationTransition>();
+ int cpt;
+ _ss.transitions = new ArrayList<SpecificationTransition>();
// At first, do not merge synchronous transitions
// Simply get basics transitions
@@ -344,7 +357,7 @@ public class AvatarModelChecker implements Runnable {
private void computeAllStatesFrom(SpecificationState _ss) {
- ArrayList<SpecificationTransition> transitions = _ss.transitions;
+ ArrayList<SpecificationTransition> transitions = _ss.transitions;
//TraceManager.addDev("Possible transitions 1:" + transitions.size());
@@ -365,10 +378,10 @@ public class AvatarModelChecker implements Runnable {
}
}
} else if (AvatarTransition.isActionType(tr.getType())) {
- newTransitions.add(tr);
- } else if (tr.getType() == AvatarTransition.TYPE_EMPTY) {
- newTransitions.add(tr);
- }
+ newTransitions.add(tr);
+ } else if (tr.getType() == AvatarTransition.TYPE_EMPTY) {
+ newTransitions.add(tr);
+ }
}
transitions = newTransitions;
//TraceManager.addDev("Possible transitions 2:" + transitions.size());
@@ -393,45 +406,45 @@ public class AvatarModelChecker implements Runnable {
transitions = newTransitions;
//TraceManager.addDev("Possible transitions 3:" + transitions.size());
- if (ignoreConcurrenceBetweenInternalActions) {
- SpecificationTransition st = null;
- // See whether there is at least one transition with an immediate internal action with no alternative in the same block
- for(SpecificationTransition tr: transitions) {
- if ((AvatarTransition.isActionType(tr.getType()) && (tr.clockMax == clockMin))|| tr.getType() == AvatarTransition.TYPE_EMPTY) {
- // Must look for similar transitions in the the same block
- //TraceManager.addDev("Lookin for same block for " + tr);
- boolean foundSameBlock = false;
- for(SpecificationTransition tro: transitions) {
- if (tro != tr) {
- if (tro.hasBlockOf(tr)) {
- foundSameBlock = true;
- //TraceManager.addDev("Found same block tr=" + tr + " tro=" + tro);
- break;
- }
- }
- }
- if (!foundSameBlock) {
- st = tr;
- break;
- }
- }
- }
- if (st != null) {
- transitions.clear();
- transitions.add(st);
- }
- }
+ if (ignoreConcurrenceBetweenInternalActions) {
+ SpecificationTransition st = null;
+ // See whether there is at least one transition with an immediate internal action with no alternative in the same block
+ for(SpecificationTransition tr: transitions) {
+ if ((AvatarTransition.isActionType(tr.getType()) && (tr.clockMax == clockMin))|| tr.getType() == AvatarTransition.TYPE_EMPTY) {
+ // Must look for similar transitions in the the same block
+ //TraceManager.addDev("Lookin for same block for " + tr);
+ boolean foundSameBlock = false;
+ for(SpecificationTransition tro: transitions) {
+ if (tro != tr) {
+ if (tro.hasBlockOf(tr)) {
+ foundSameBlock = true;
+ //TraceManager.addDev("Found same block tr=" + tr + " tro=" + tro);
+ break;
+ }
+ }
+ }
+ if (!foundSameBlock) {
+ st = tr;
+ break;
+ }
+ }
+ }
+ if (st != null) {
+ transitions.clear();
+ transitions.add(st);
+ }
+ }
- //TraceManager.addDev("Possible transitions 4:" + transitions.size());
+ //TraceManager.addDev("Possible transitions 4:" + transitions.size());
// For each realizable transition
// Make it, reset clock of the involved blocks to 0, increase clockmin/clockhmax of each block
// compute new state, and compare with existing ones
// If not a new state, create the link rom the previous state to the new one
// Otherwise create the new state and its link, and add it to the pending list of states
- int cptt = 0;
+ int cptt = 0;
for(SpecificationTransition tr: transitions) {
- //TraceManager.addDev("Handling transitions #" + cptt + " type =" + tr.getType());
- cptt ++;
+ //TraceManager.addDev("Handling transitions #" + cptt + " type =" + tr.getType());
+ cptt ++;
// Make tr
// to do so, must create a new state
@@ -444,16 +457,16 @@ public class AvatarModelChecker implements Runnable {
// doing the synchronization
String action = executeTransition(_ss, newState, tr);
- // Remove empty transitions if applicable
- if (ignoreEmptyTransitions) {
- handleNonEmptyUniqueTransition(newState);
- }
- prepareTransitionsOfState(newState);
+ // Remove empty transitions if applicable
+ if (ignoreEmptyTransitions) {
+ handleNonEmptyUniqueTransition(newState);
+ }
+ prepareTransitionsOfState(newState);
// Compute the hash of the new state, and create the link to the right next state
SpecificationLink link = new SpecificationLink();
link.originState = _ss;
- action += " [" + tr.clockMin + " ..." + clockMax + "]";
+ action += " [" + tr.clockMin + " ..." + clockMax + "]";
link.action = action;
newState.computeHash(blockValues);
SpecificationState similar = states.get(newState.getHash(blockValues));
@@ -470,17 +483,24 @@ public class AvatarModelChecker implements Runnable {
//TraceManager.addDev("Similar state found State=" + newState.getHash(blockValues) + "\n" + newState + "\nsimilar=" + similar.getHash(blockValues) + "\n" + similar);
link.destinationState = similar;
}
- links.add(link);
+ //links.add(link);
+ nbOfLinks ++;
+ _ss.addNext(link);
}
- _ss.finished();
- mustStop();
+ if (freeIntermediateStateCoding) {
+ freeUselessAllocations();
+ } else {
+ _ss.finished();
+ }
+
+ mustStop();
}
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();
@@ -494,10 +514,10 @@ public class AvatarModelChecker implements Runnable {
}
// Must see whether the guard is ok or not
- boolean guard = guardResult(_at, _block, _sb);
- if (!guard) {
- return;
- }
+ boolean guard = guardResult(_at, _block, _sb);
+ if (!guard) {
+ return;
+ }
SpecificationTransition st = new SpecificationTransition();
_transitionsToAdd.add(st);
@@ -514,8 +534,8 @@ public class AvatarModelChecker implements Runnable {
if ((maxDelay == null) || (maxDelay.length() == 0)) {
st.clockMax = 0 - _sb.values[SpecificationBlock.CLOCKMAX_INDEX];
} else {
- int resMax = evaluateIntExpression(_at.getMaxDelay(), _block, _sb);
- _sb.maxClock = Math.max(_sb.maxClock, resMax);
+ int resMax = evaluateIntExpression(_at.getMaxDelay(), _block, _sb);
+ _sb.maxClock = Math.max(_sb.maxClock, resMax);
st.clockMax = resMax - _sb.values[SpecificationBlock.CLOCKMAX_INDEX];
}
@@ -558,19 +578,19 @@ public class AvatarModelChecker implements Runnable {
}
}
} else {
- 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;
- }
- }
+ 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;
+ }
+ }
}
}
}
@@ -619,7 +639,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()) {
@@ -677,7 +697,7 @@ public class AvatarModelChecker implements Runnable {
for(int i=0; i<_st.transitions.length; i++) {
ase = getNextState(_st.transitions[i], _newState, 10);
if (ase != null) {
- checkElement(ase, _newState);
+ checkElement(ase, _newState);
int index = _st.blocks[i].getStateMachine().getIndexOfState(ase);
if (index > -1) {
_newState.blocks[_st.blocksInt[i]].values[SpecificationBlock.STATE_INDEX] = index;
@@ -697,16 +717,16 @@ public class AvatarModelChecker implements Runnable {
}
private AvatarStateElement getNextState(AvatarStateMachineElement e, SpecificationState _newState, int maxNbOfIterations) {
- checkElement(e, _newState);
- e = e.getNext(0);
- if (e instanceof AvatarStateElement) {
- return (AvatarStateElement)e;
- }
- maxNbOfIterations --;
- if (maxNbOfIterations == 0) {
- return null;
- }
- return getNextState(e, _newState, maxNbOfIterations);
+ checkElement(e, _newState);
+ e = e.getNext(0);
+ if (e instanceof AvatarStateElement) {
+ return (AvatarStateElement)e;
+ }
+ maxNbOfIterations --;
+ if (maxNbOfIterations == 0) {
+ return null;
+ }
+ return getNextState(e, _newState, maxNbOfIterations);
}
// Execute the actions of a transition, and correspondingly impact the variables of the
@@ -814,127 +834,127 @@ public class AvatarModelChecker implements Runnable {
}
public void handleNonEmptyUniqueTransition(SpecificationState _ss) {
- int cpt = 0;
- for(AvatarBlock block: spec.getListOfBlocks()) {
- AvatarStateMachine asm = block.getStateMachine();
- SpecificationBlock sb = _ss.blocks[cpt];
+ 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, _ss);
- if (aseAfter != ase) {
- checkElement(aseAfter, _ss);
- // Must modify the state of the considered block
- sb.values[SpecificationBlock.STATE_INDEX] = asm.getIndexOfState(aseAfter);
- }
- cpt ++;
- }
+
+
+ AvatarStateElement aseAfter = getStateWithNonEmptyUniqueTransition(ase, block, sb, _ss);
+ if (aseAfter != ase) {
+ checkElement(aseAfter, _ss);
+ // 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, SpecificationState _ss) {
- return getStateWithNonEmptyUniqueTransitionArray(_ase, _block, _sb, _ss, null);
+ return getStateWithNonEmptyUniqueTransitionArray(_ase, _block, _sb, _ss, null);
}
private AvatarStateElement getStateWithNonEmptyUniqueTransitionArray(AvatarStateElement _ase, AvatarBlock _block, SpecificationBlock _sb, SpecificationState _ss, ArrayList<AvatarStateElement> listOfStates ) {
- // TraceManager.addDev("Handling Empty transition of previous=" + _ase.getName());
-
- if (_ase.getNexts().size() != 1) {
- return _ase;
- }
+ // TraceManager.addDev("Handling Empty transition of previous=" + _ase.getName());
-
- //TraceManager.addDev("Handling Empty transition of previous= 1 " + _ase.getName());
-
- AvatarTransition at = (AvatarTransition)(_ase.getNext(0));
+ if (_ase.getNexts().size() != 1) {
+ return _ase;
+ }
- //TraceManager.addDev("Handling Empty transition of previous= 2 " + _ase.getName() + " trans=" + at.getName());
- if(!((at.type == AvatarTransition.TYPE_EMPTY) || (at.type == AvatarTransition.TYPE_METHODONLY))) {
- return _ase;
- }
+ //TraceManager.addDev("Handling Empty transition of previous= 1 " + _ase.getName());
- //TraceManager.addDev("Handling Empty transition of previous= 3 " + _ase.getName() + " trans=" + at.getName());
-
- // Check guard;
- boolean guard = guardResult(at, _block, _sb);
+ AvatarTransition at = (AvatarTransition)(_ase.getNext(0));
- if (!guard) {
- return _ase;
- }
+ //TraceManager.addDev("Handling Empty transition of previous= 2 " + _ase.getName() + " trans=" + at.getName());
- //TraceManager.addDev("Handling Empty transition of previous= 4 " + _ase.getName() + " trans=" + at.getName());
+ if(!((at.type == AvatarTransition.TYPE_EMPTY) || (at.type == AvatarTransition.TYPE_METHODONLY))) {
+ return _ase;
+ }
-
- AvatarStateElement ase = (AvatarStateElement)(at.getNext(0));
- checkElement(ase, _ss);
- //TraceManager.addDev("Handling Empty transition of " + _block.getName() + " with nextState = " + ase.getName() + " and previous=" + _ase.getName());
-
- if (listOfStates == null) {
- if (ase == _ase) {
- return _ase;
- }
- //TraceManager.addDev("New list of states " + _block.getName());
- listOfStates = new ArrayList<AvatarStateElement>();
- } else {
- if (listOfStates.contains(ase)) {
- return _ase;
- }
- }
- listOfStates.add(_ase);
+ //TraceManager.addDev("Handling Empty transition of previous= 3 " + _ase.getName() + " trans=" + at.getName());
- return getStateWithNonEmptyUniqueTransitionArray(ase, _block, _sb, _ss, listOfStates);
-
-
- }
+ // Check guard;
+ boolean guard = guardResult(at, _block, _sb);
+
+ if (!guard) {
+ return _ase;
+ }
+
+ //TraceManager.addDev("Handling Empty transition of previous= 4 " + _ase.getName() + " trans=" + at.getName());
+
+
+ AvatarStateElement ase = (AvatarStateElement)(at.getNext(0));
+ checkElement(ase, _ss);
+ //TraceManager.addDev("Handling Empty transition of " + _block.getName() + " with nextState = " + ase.getName() + " and previous=" + _ase.getName());
+
+ if (listOfStates == null) {
+ if (ase == _ase) {
+ return _ase;
+ }
+ //TraceManager.addDev("New list of states " + _block.getName());
+ listOfStates = new ArrayList<AvatarStateElement>();
+ } else {
+ if (listOfStates.contains(ase)) {
+ return _ase;
+ }
+ }
+ listOfStates.add(_ase);
+
+ return getStateWithNonEmptyUniqueTransitionArray(ase, _block, _sb, _ss, listOfStates);
+
+
+ }
// Checking elements
public void checkElement(AvatarStateMachineElement elt, SpecificationState _ss) {
- if (studyReachability) {
- checkElementReachability(elt, _ss);
- }
+ if (studyReachability) {
+ checkElementReachability(elt, _ss);
+ }
}
public void checkElementReachability(AvatarStateMachineElement elt, SpecificationState _ss) {
- for(SpecificationReachability re: reachabilities) {
- if (re.result == SpecificationReachabilityType.NOTCOMPUTED) {
- if (re.ref == elt) {
- re.result = SpecificationReachabilityType.REACHABLE;
- re.state = _ss;
- nbOfRemainingReachabilities --;
- TraceManager.addDev("Remaining reachabilities:" + nbOfRemainingReachabilities);
- }
- }
- }
+ for(SpecificationReachability re: reachabilities) {
+ if (re.result == SpecificationReachabilityType.NOTCOMPUTED) {
+ if (re.ref == elt) {
+ re.result = SpecificationReachabilityType.REACHABLE;
+ re.state = _ss;
+ nbOfRemainingReachabilities --;
+ TraceManager.addDev("Remaining reachabilities:" + nbOfRemainingReachabilities);
+ }
+ }
+ }
}
-
+
// Stop condition
public synchronized boolean mustStop() {
- if (stoppedConditionReached) {
- return true;
- }
+ if (stoppedConditionReached) {
+ return true;
+ }
- stoppedConditionReached = true;
+ stoppedConditionReached = true;
- if (studyReachability && nbOfRemainingReachabilities==0) {
- TraceManager.addDev("***** All reachability found");
- }
-
- if (studyReachability && nbOfRemainingReachabilities>0) {
- stoppedConditionReached = false;
- }
+ if (studyReachability && nbOfRemainingReachabilities==0) {
+ TraceManager.addDev("***** All reachability found");
+ }
- if (computeRG) {
- stoppedConditionReached = false;
- }
+ if (studyReachability && nbOfRemainingReachabilities>0) {
+ stoppedConditionReached = false;
+ }
+
+ if (computeRG) {
+ stoppedConditionReached = false;
+ }
- return stoppedConditionReached;
+ return stoppedConditionReached;
}
-
+
// Generators
@@ -944,8 +964,10 @@ public class AvatarModelChecker implements Runnable {
sb.append(state.toString() + "\n");
}
sb.append("\nLinks:\n");
- for(SpecificationLink link: links) {
- sb.append(link.toString() + "\n");
+ for(SpecificationState state: states.values()) {
+ for(SpecificationLink link: state.nexts) {
+ sb.append(link.toString() + "\n");
+ }
}
return sb.toString();
}
@@ -955,8 +977,10 @@ public class AvatarModelChecker implements Runnable {
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");
+ for(SpecificationState state: states.values()) {
+ for(SpecificationLink link: state.nexts) {
+ sb.append("(" + link.originState.id + ",\"" + link.action + "\"," + link.destinationState.id + ")\n");
+ }
}
return new String(sb);
}
@@ -965,30 +989,40 @@ public class AvatarModelChecker implements Runnable {
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");
+ for(SpecificationState state: states.values()) {
+ for(SpecificationLink link: state.nexts) {
+
+ sb.append(" " + link.originState.id + " -> " + link.destinationState.id + "[label=\"" + link.action + "\"];\n");
+ }
}
sb.append("}");
return new String(sb);
}
public String reachabilityToString() {
- if (!studyReachability) {
- return "Reachability not activated";
- }
+ if (!studyReachability) {
+ return "Reachability not activated";
+ }
- String ret = "";
- if (stoppedBeforeEnd) {
- ret += "Beware: Full study of reacha&bility might not have been fully completed\n";
- }
+ String ret = "";
+ if (stoppedBeforeEnd) {
+ ret += "Beware: Full study of reacha&bility might not have been fully completed\n";
+ }
+
+ int cpt=0;
+ for(SpecificationReachability re: reachabilities) {
+ ret += cpt + ": " + re.toString() + "\n";
+ cpt ++;
+ }
+ return ret;
+ }
- int cpt=0;
- for(SpecificationReachability re: reachabilities) {
- ret += cpt + ": " + re.toString() + "\n";
- cpt ++;
+ // Do not free the RG
+ public void freeUselessAllocations() {
+ for(SpecificationState state: states.values()) {
+ state.freeUselessAllocations();
}
- return ret;
}
diff --git a/src/avatartranslator/modelchecker/SpecificationState.java b/src/avatartranslator/modelchecker/SpecificationState.java
index ddc3ac40e0182bc3aeb7469e7b796cb8c06f369f..3d7eacb370af463439f233a0c4d5a5bb89469342 100644
--- a/src/avatartranslator/modelchecker/SpecificationState.java
+++ b/src/avatartranslator/modelchecker/SpecificationState.java
@@ -60,6 +60,7 @@ public class SpecificationState {
public int hashValue;
public boolean hashComputed;
public long id;
+ public LinkedList<SpecificationLink> nexts;
public ArrayList<SpecificationTransition> transitions;
@@ -105,6 +106,9 @@ public class SpecificationState {
}
public String toString() {
+ if (blocks == null) {
+ return "";
+ }
StringBuffer sb = new StringBuffer("id: " + id);
for(int i=0; i<blocks.length; i++) {
sb.append("\n "+i + ": " + blocks[i].toString());
@@ -149,9 +153,21 @@ public class SpecificationState {
return cpt;
}
+ public void addNext(SpecificationLink sl) {
+ if (nexts == null) {
+ nexts = new LinkedList<SpecificationLink>();
+ }
+ nexts.add(sl);
+ }
+
public void finished() {
//blocks = null;
transitions = null;
}
+ public void freeUselessAllocations() {
+ blocks = null;
+ transitions = null;
+ }
+
}
diff --git a/src/myutil/Graph.java b/src/myutil/Graph.java
index 91d0db80b4a2dde7debee8f958571a0feaf6e74f..72d2933f25b25fa2fa3011e1381631df493e5e1d 100755
--- a/src/myutil/Graph.java
+++ b/src/myutil/Graph.java
@@ -50,7 +50,7 @@ package myutil;
public interface Graph {
- public int getNbState();
+ public int getNbOfStates();
// Returns 0 is no transition, 1 otherwise
public int getWeightOfTransition(int originState, int destinationState);
diff --git a/src/myutil/GraphAlgorithms.java b/src/myutil/GraphAlgorithms.java
index 5dd418b43214daa109b24b7202c47ba85ec64d05..16aa00c67c28e9565f957add7eee867051fe64ca 100755
--- a/src/myutil/GraphAlgorithms.java
+++ b/src/myutil/GraphAlgorithms.java
@@ -56,7 +56,7 @@ public class GraphAlgorithms {
// Assume that states are numbered from 0 to nbState - 1
public static boolean hasCycle(Graph g){
- int nbState = g.getNbState();
+ int nbState = g.getNbOfStates();
int i,j;
if (nbState == 0) {
@@ -133,7 +133,7 @@ public class GraphAlgorithms {
public static DijkstraState[] ShortestPathFrom(Graph g, int startState){
- int nbState = g.getNbState();
+ int nbState = g.getNbOfStates();
if (nbState == 0) {
return null;
}
@@ -227,7 +227,7 @@ public class GraphAlgorithms {
}*/
- int nbState = g.getNbState();
+ int nbState = g.getNbOfStates();
if (nbState == 0) {
return null;
}
diff --git a/src/ui/graph/AUTGraph.java b/src/ui/graph/AUTGraph.java
index 7c61faa932f5fec7d3b4e24ce6d34b19eb81ea75..e6b8b5347fc8fe7f7903e6487636e211c7ad44f6 100755
--- a/src/ui/graph/AUTGraph.java
+++ b/src/ui/graph/AUTGraph.java
@@ -205,11 +205,11 @@ public class AUTGraph implements myutil.Graph {
return array;
}
- public int getNbState() {
+ public int getNbOfStates() {
return nbState;
}
- public int getNbTransition() {
+ public int getNbOfTransitions() {
//return nbTransition;
return transitions.size();
}
diff --git a/src/ui/window/DeadlockTableModel.java b/src/ui/window/DeadlockTableModel.java
index 08446b7646e322e667756d51eaeb896d3475ae5d..05dafb21f9200335576dbc2c9928d462f32bdf91 100755
--- a/src/ui/window/DeadlockTableModel.java
+++ b/src/ui/window/DeadlockTableModel.java
@@ -1,48 +1,48 @@
/**Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
-ludovic.apvrille AT enst.fr
-
-This software is a computer program whose purpose is to allow the
-edition of TURTLE analysis, design and deployment diagrams, to
-allow the generation of RT-LOTOS or Java code from this diagram,
-and at last to allow the analysis of formal validation traces
-obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
-from INRIA Rhone-Alpes.
-
-This software is governed by the CeCILL license under French law and
-abiding by the rules of distribution of free software. You can use,
-modify and/ or redistribute the software under the terms of the CeCILL
-license as circulated by CEA, CNRS and INRIA at the following URL
-"http://www.cecill.info".
-
-As a counterpart to the access to the source code and rights to copy,
-modify and redistribute granted by the license, users are provided only
-with a limited warranty and the software's author, the holder of the
-economic rights, and the successive licensors have only limited
-liability.
-
-In this respect, the user's attention is drawn to the risks associated
-with loading, using, modifying and/or developing or reproducing the
-software by the user in light of its specific status of free software,
-that may mean that it is complicated to manipulate, and that also
-therefore means that it is reserved for developers and experienced
-professionals having in-depth computer knowledge. Users are therefore
-encouraged to load and test the software's suitability as regards their
-requirements in conditions enabling the security of their systems and/or
-data to be ensured and, more generally, to use and operate it in the
-same conditions as regards security.
-
-The fact that you are presently reading this means that you have had
-knowledge of the CeCILL license and that you accept its terms.
-
-/**
- * Class DeadlockTableModel
- * Data of an action on a simulation trace
- * Creation: 15/09/2004
- * @version 1.0 15/09/2004
- * @author Ludovic APVRILLE
- * @see
- */
+ ludovic.apvrille AT enst.fr
+
+ This software is a computer program whose purpose is to allow the
+ edition of TURTLE analysis, design and deployment diagrams, to
+ allow the generation of RT-LOTOS or Java code from this diagram,
+ and at last to allow the analysis of formal validation traces
+ obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
+ from INRIA Rhone-Alpes.
+
+ This software is governed by the CeCILL license under French law and
+ abiding by the rules of distribution of free software. You can use,
+ modify and/ or redistribute the software under the terms of the CeCILL
+ license as circulated by CEA, CNRS and INRIA at the following URL
+ "http://www.cecill.info".
+
+ As a counterpart to the access to the source code and rights to copy,
+ modify and redistribute granted by the license, users are provided only
+ with a limited warranty and the software's author, the holder of the
+ economic rights, and the successive licensors have only limited
+ liability.
+
+ In this respect, the user's attention is drawn to the risks associated
+ with loading, using, modifying and/or developing or reproducing the
+ software by the user in light of its specific status of free software,
+ that may mean that it is complicated to manipulate, and that also
+ therefore means that it is reserved for developers and experienced
+ professionals having in-depth computer knowledge. Users are therefore
+ encouraged to load and test the software's suitability as regards their
+ requirements in conditions enabling the security of their systems and/or
+ data to be ensured and, more generally, to use and operate it in the
+ same conditions as regards security.
+
+ The fact that you are presently reading this means that you have had
+ knowledge of the CeCILL license and that you accept its terms.
+
+ /**
+ * Class DeadlockTableModel
+ * Data of an action on a simulation trace
+ * Creation: 15/09/2004
+ * @version 1.0 15/09/2004
+ * @author Ludovic APVRILLE
+ * @see
+ */
package ui.window;
@@ -53,98 +53,98 @@ import myutil.*;
import ui.graph.*;
public class DeadlockTableModel extends AbstractTableModel {
- Vector deadlockData;
- int maxTransitions;
-
- public DeadlockTableModel(AUTGraph _graph, int _maxTransitions) {
- deadlockData = new Vector();
- maxTransitions = _maxTransitions;
- makeDeadlockData(_graph);
- }
-
- // From AbstractTableModel
- public int getRowCount() {
- return deadlockData.size();
- }
-
- public int getColumnCount() {
- return 3;
- }
-
- public Object getValueAt(int row, int column) {
- DeadlockItem di;
- di = (DeadlockItem)(deadlockData.elementAt(Math.min(row, deadlockData.size())));
- if (column == 0) {
- return di.getName();
- } else if (column == 1) {
- return di.getOriginAction();
- } else {
- return di.getPath();
- }
- }
-
- public String getColumnName(int columnIndex) {
- switch(columnIndex) {
- case 0:
- return "States";
- case 1:
- return "(origin, action)";
- case 2:
- default:
- return "Shortest path to state";
- }
- }
-
-
- // to build internal data structure -> graph in AUT format
- private void makeDeadlockData(AUTGraph graph) {
- DeadlockItem di;
- AUTTransition aut1;
- DijkstraState[] dss = null;
- if (graph.getNbTransition() < maxTransitions) {
- dss = GraphAlgorithms.ShortestPathFrom(graph, 0);
- }
- //System.out.println(dss.toString());
-
- /*for(int k=0; k<dss.length; k++) {
- System.out.println(dss[k]);
- }*/
-
- //System.out.println("Getting vector potential deadlocks");
- int [] states = graph.getVectorPotentialDeadlocks();
- //System.out.println("Got vector potential deadlocks");
- int i, j, size, state;
- String path;
-
- for(i=0; i<states.length; i++) {
- state = states[i];
- di = new DeadlockItem(""+ state);
- deadlockData.add(di);
- if (dss != null) {
- for(j=0; j<graph.getNbTransition(); j++) {
- aut1 = graph.getAUTTransition(j);
- if (aut1.destination == state) {
- di.addOriginAction(""+aut1.origin, aut1.transition);
- }
- }
- }else {
- di.addOriginAction("", "");
- }
- //path = "0 --" + graph.getActionTransition(0, dss[state].path[0]) + "--> ";;
- if (dss != null) {
- size = dss[state].path.length;
- path = "";
- for(j=0; j<dss[state].path.length; j++) {
- path = path + "[" + dss[state].path[j] + "]";
- if (j < size - 1) {
- path = path + " -- " + graph.getActionTransition(dss[state].path[j], dss[state].path[j+1]) + " --> ";
- }
- }
- di.setPath(path);
- } else {
- di.setPath("not calculated");
- }
- }
- Collections.sort(deadlockData);
- }
-}
\ No newline at end of file
+ Vector deadlockData;
+ int maxTransitions;
+
+ public DeadlockTableModel(AUTGraph _graph, int _maxTransitions) {
+ deadlockData = new Vector();
+ maxTransitions = _maxTransitions;
+ makeDeadlockData(_graph);
+ }
+
+ // From AbstractTableModel
+ public int getRowCount() {
+ return deadlockData.size();
+ }
+
+ public int getColumnCount() {
+ return 3;
+ }
+
+ public Object getValueAt(int row, int column) {
+ DeadlockItem di;
+ di = (DeadlockItem)(deadlockData.elementAt(Math.min(row, deadlockData.size())));
+ if (column == 0) {
+ return di.getName();
+ } else if (column == 1) {
+ return di.getOriginAction();
+ } else {
+ return di.getPath();
+ }
+ }
+
+ public String getColumnName(int columnIndex) {
+ switch(columnIndex) {
+ case 0:
+ return "States";
+ case 1:
+ return "(origin, action)";
+ case 2:
+ default:
+ return "Shortest path to state";
+ }
+ }
+
+
+ // to build internal data structure -> graph in AUT format
+ private void makeDeadlockData(AUTGraph graph) {
+ DeadlockItem di;
+ AUTTransition aut1;
+ DijkstraState[] dss = null;
+ if (graph.getNbOfTransitions() < maxTransitions) {
+ dss = GraphAlgorithms.ShortestPathFrom(graph, 0);
+ }
+ //System.out.println(dss.toString());
+
+ /*for(int k=0; k<dss.length; k++) {
+ System.out.println(dss[k]);
+ }*/
+
+ //System.out.println("Getting vector potential deadlocks");
+ int [] states = graph.getVectorPotentialDeadlocks();
+ //System.out.println("Got vector potential deadlocks");
+ int i, j, size, state;
+ String path;
+
+ for(i=0; i<states.length; i++) {
+ state = states[i];
+ di = new DeadlockItem(""+ state);
+ deadlockData.add(di);
+ if (dss != null) {
+ for(j=0; j<graph.getNbOfTransitions(); j++) {
+ aut1 = graph.getAUTTransition(j);
+ if (aut1.destination == state) {
+ di.addOriginAction(""+aut1.origin, aut1.transition);
+ }
+ }
+ }else {
+ di.addOriginAction("", "");
+ }
+ //path = "0 --" + graph.getActionTransition(0, dss[state].path[0]) + "--> ";;
+ if (dss != null) {
+ size = dss[state].path.length;
+ path = "";
+ for(j=0; j<dss[state].path.length; j++) {
+ path = path + "[" + dss[state].path[j] + "]";
+ if (j < size - 1) {
+ path = path + " -- " + graph.getActionTransition(dss[state].path[j], dss[state].path[j+1]) + " --> ";
+ }
+ }
+ di.setPath(path);
+ } else {
+ di.setPath("not calculated");
+ }
+ }
+ Collections.sort(deadlockData);
+ }
+}
diff --git a/src/ui/window/JFrameStatistics.java b/src/ui/window/JFrameStatistics.java
index fbfef1c0bbcf8d78ac454035d3159bd37a7cd0b6..01adedaea22250f626f5da2793e848815c5d9a76 100755
--- a/src/ui/window/JFrameStatistics.java
+++ b/src/ui/window/JFrameStatistics.java
@@ -280,13 +280,13 @@ public class JFrameStatistics extends JFrame implements ActionListener, Stoppab
jp.add(new JLabel("States:"));
state = new JTextField(5);
state.setEditable(false);
- state.setText(String.valueOf(graph.getNbState()));
+ state.setText(String.valueOf(graph.getNbOfStates()));
jp.add(state);
jp.add(new JLabel("Transitions:"));
transition = new JTextField(15);
transition.setEditable(false);
- transition.setText(String.valueOf(graph.getNbTransition()));
+ transition.setText(String.valueOf(graph.getNbOfTransitions()));
jp.add(transition);
if (shouldIStop()) {
@@ -392,7 +392,7 @@ public class JFrameStatistics extends JFrame implements ActionListener, Stoppab
c1.gridwidth = GridBagConstraints.REMAINDER; //end row
//combo2 = new JComboBox(tab2);
- combo2 = new JTextField("" + (graph.getNbState() - 1), 10);
+ combo2 = new JTextField("" + (graph.getNbOfStates() - 1), 10);
jp1.add(combo2, c1);
//jp2.add(jp1, BorderLayout.NORTH);
@@ -432,7 +432,7 @@ public class JFrameStatistics extends JFrame implements ActionListener, Stoppab
cycleDone = true;
//System.out.println("Searching for cycles");
- if (graph.getNbTransition() < MAX_TRANSITIONS) {
+ if (graph.getNbOfTransitions() < MAX_TRANSITIONS) {
hasCycle = GraphAlgorithms.hasCycle(graph);
cycleComputed = true;
} else {
@@ -480,7 +480,7 @@ public class JFrameStatistics extends JFrame implements ActionListener, Stoppab
c2.gridwidth = GridBagConstraints.REMAINDER; //end row
//combo4 = new JComboBox(tab2);
- combo4 = new JTextField("" + (graph.getNbState() - 1), 10);
+ combo4 = new JTextField("" + (graph.getNbOfStates() - 1), 10);
jp3.add(combo4, c2);
//jp2.add(jp1, BorderLayout.NORTH);
@@ -630,13 +630,13 @@ public class JFrameStatistics extends JFrame implements ActionListener, Stoppab
return;
}
- if(from>=graph.getNbState()) {
- text1.setText("Invalid value:" + combo1.getText() + ". Maximum value is: " + (graph.getNbState()-1));
+ if(from>=graph.getNbOfStates()) {
+ text1.setText("Invalid value:" + combo1.getText() + ". Maximum value is: " + (graph.getNbOfStates()-1));
return;
}
- if(to>=graph.getNbState()) {
- text1.setText("Invalid value:" + combo2.getText() + ". Maximum value is: " + (graph.getNbState()-1));
+ if(to>=graph.getNbOfStates()) {
+ text1.setText("Invalid value:" + combo2.getText() + ". Maximum value is: " + (graph.getNbOfStates()-1));
return;
}
@@ -666,13 +666,13 @@ public class JFrameStatistics extends JFrame implements ActionListener, Stoppab
return;
}
- if(from>=graph.getNbState()) {
- text1.setText("Invalid value:" + combo3.getText() + ". Maximum value is: " + (graph.getNbState()-1));
+ if(from>=graph.getNbOfStates()) {
+ text1.setText("Invalid value:" + combo3.getText() + ". Maximum value is: " + (graph.getNbOfStates()-1));
return;
}
- if(to>=graph.getNbState()) {
- text2.setText("Invalid value:" + combo4.getText() + ". Maximum value is: " + (graph.getNbState()-1));
+ if(to>=graph.getNbOfStates()) {
+ text2.setText("Invalid value:" + combo4.getText() + ". Maximum value is: " + (graph.getNbOfStates()-1));
return;
}
diff --git a/src/ui/window/StatisticsTableModel.java b/src/ui/window/StatisticsTableModel.java
index a0e8b5877a312d85fd46699ebbdd86fe6b3b2576..f2e209f63d36b3ef5cce7a3b7bcb4dd00b0e512b 100755
--- a/src/ui/window/StatisticsTableModel.java
+++ b/src/ui/window/StatisticsTableModel.java
@@ -164,7 +164,7 @@ public class StatisticsTableModel extends AbstractTableModel implements SteppedA
StatisticsItem si1 = null;
String array[];
int i;
- int nb = graph.getNbTransition();
+ int nb = graph.getNbOfTransitions();
AUTTransition tr;
percentage = 0;
@@ -172,7 +172,7 @@ public class StatisticsTableModel extends AbstractTableModel implements SteppedA
setGo();
try {
- for(i=0; i<graph.getNbTransition(); i++) {
+ for(i=0; i<graph.getNbOfTransitions(); i++) {
if (!go) {
return;