Skip to content
Snippets Groups Projects
Commit 168104bc authored by Ludovic Apvrille's avatar Ludovic Apvrille
Browse files

Update on graoh interface

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