diff --git a/src/main/java/avatartranslator/AvatarStateMachine.java b/src/main/java/avatartranslator/AvatarStateMachine.java
index b109596a7eb33b88f5f68ef2260323353fc6563e..9b98266ba98a6b2f409af81daffa90026f485cd9 100644
--- a/src/main/java/avatartranslator/AvatarStateMachine.java
+++ b/src/main/java/avatartranslator/AvatarStateMachine.java
@@ -440,7 +440,9 @@ public class AvatarStateMachine extends AvatarElement {
public void removeCompositeStates(AvatarBlock _block) {
TraceManager.addDev("\n-------------- Remove composite states ---------------\n");
- /*LinkedList<AvatarState> lists =*/ removeAllInternalStartStates();
+ /*LinkedList<AvatarState> lists =*/
+ List<AvatarStartState> compositeStateToBeRemoved = removeAllInternalStartStates();
+ removeAllInternalStopStatesByRegularStates();
AvatarTransition at = getAvatarCompositeTransition();
@@ -456,23 +458,28 @@ public class AvatarStateMachine extends AvatarElement {
}
}
- // For each composite transition: We link it to all the substates of the current state
+ // For each composite transition: We link it to all the subStates of the current state
AvatarState src;
- while (((at = getAvatarCompositeTransition()) != null)) {
+
+ Vector<AvatarTransition>transitions = getAvatarCompositeTransitions();
+
+ for (AvatarTransition atc: transitions) {
+ src = (AvatarState) (getPreviousElementOf(atc));
+ atc.setAsVerifiable(false);
+ for (int j = 0; j < elements.size(); j++) {
+ AvatarStateMachineElement elt = elements.get(j);
+ if ((elt instanceof AvatarState) && (elt.hasInUpperState(src))) {
+ AvatarTransition att = cloneCompositeTransition(atc);
+ elt.addNext(att);
+ att.setAsVerifiable(false);
+ }
+ }
+ }
+
+ /*while (((at = getAvatarCompositeTransition()) != null)) {
src = (AvatarState) (getPreviousElementOf(at));
elements.remove(at);
- // Add a new state after the transition
- /*String tmp = findUniqueStateName("forCompositeTransition_state");
- AvatarState as = new AvatarState(tmp, at.getReferenceObject());
- elements.add(as);
- AvatarTransition ats = new AvatarTransition("forCompositeTransition_trans", at.getReferenceObject());
- elements.add(ats);
- ats.addNext(at.getNext(0));
- at.removeAllNexts();
- at.addNext(as);
- as.addNext(ats);*/
-
// Link a clone of the transition to all internal states
for (int j = 0; j < elements.size(); j++) {
@@ -485,11 +492,47 @@ public class AvatarStateMachine extends AvatarElement {
}
}
- }
+ }*/
+
+ // Removing composite states
+ /*for(AvatarStateMachineElement elt: compositeStateToBeRemoved) {
+ elements.remove(elt);
+ }*/
}
+ private void removeAllInternalStopStatesByRegularStates() {
+ Vector<AvatarStopState> v = new Vector<>();
+ Vector<AvatarState> toAdd = new Vector<>();
+
+ for (AvatarStateMachineElement element : elements) {
+ if (element instanceof AvatarTransition) {
+ AvatarTransition at = (AvatarTransition) element;
+ //TraceManager.addDev("at? element=" + element);
+ // Transition fully in the internal state?
+ if (element.getNext(0) instanceof AvatarStopState) {
+ AvatarStopState stop = (AvatarStopState)(element.getNext(0));
+ if (stop.getState() != null) {
+ AvatarState newState = new AvatarState(stop.getName(), stop.getReferenceObject());
+ element.removeNext(0);
+ element.addNext(newState);
+ toAdd.add(newState);
+ v.add(stop);
+ }
+
+ }
+ }
+ }
+ for(AvatarStopState s: v) {
+ elements.remove(s);
+ }
+ for(AvatarState st: toAdd) {
+ elements.add(st);
+ }
+ }
+
+
private void modifyStateForCompositeSupport(AvatarState _state) {
// Each time there is a transition with an after or more than one action, we must rework the transition
@@ -625,6 +668,24 @@ public class AvatarStateMachine extends AvatarElement {
return null;
}
+ private Vector<AvatarTransition> getAvatarCompositeTransitions() {
+
+ Vector<AvatarTransition> transitions = new Vector<>();
+
+ for (AvatarStateMachineElement element : elements) {
+ if (element instanceof AvatarTransition) {
+ if ((isACompositeTransition((AvatarTransition) element))) {
+ transitions.add((AvatarTransition) element);
+ }
+ }
+ }
+
+ return transitions;
+ }
+
+
+
+
// Checks whether the previous element is a state with an internal state machine
public boolean isACompositeTransition(AvatarTransition _at) {
AvatarStateMachineElement element = getPreviousElementOf(_at);
@@ -637,7 +698,17 @@ public class AvatarStateMachine extends AvatarElement {
}
AvatarState state = (AvatarState) element;
- return hasInternalComponents(state);
+
+ if (!hasInternalComponents(state)) {
+ return false;
+ }
+
+ AvatarStateMachineElement next = _at.getNext(0);
+ if (next.hasInUpperState(state)) {
+ return false;
+ }
+
+ return true;
}
private boolean hasInternalComponents(AvatarState _state) {
@@ -970,11 +1041,11 @@ public class AvatarStateMachine extends AvatarElement {
// All transitions reaching a state that has an internal start state
// shall in fact go directly to the nexts of the start state
- public List<AvatarState> removeAllInternalStartStates() {
+ public List<AvatarStartState> removeAllInternalStartStates() {
// identify allstart state
List<AvatarStartState> ll = new LinkedList<AvatarStartState>();
- List<AvatarState> removedinfos = new LinkedList<AvatarState>();
+ List<AvatarStartState> removedinfos = new LinkedList<>();
for (AvatarStateMachineElement element : elements) {
if ((element instanceof AvatarStartState) && (element.getState() != null)) {
@@ -988,7 +1059,11 @@ public class AvatarStateMachine extends AvatarElement {
for (AvatarStartState as : ll) {
AvatarState astate = as.getState();
if (as != null) {
- le = getPreviousElementsOf(astate);
+ elements.remove(as);
+ AvatarStateMachineElement elt = as.getNext(0);
+ astate.addNext(elt);
+ removedinfos.add(as);
+ /*le = getPreviousElementsOf(astate);
if (le.size() > 0) {
as0 = new AvatarState("entrance__" + astate.getName(), astate.getReferenceObject());
as0.addNext(as.getNext(0));
@@ -1013,7 +1088,7 @@ public class AvatarStateMachine extends AvatarElement {
//TraceManager.addDev("-> -> removed an internal state state!");
} else {
TraceManager.addDev("Badly formed state machine");
- }
+ }*/
}
}
diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index 9fd7708873eb9f3bc0574b201c5a4be569401314..c3390bb71166a755305b2ea06967f0ebfed7355a 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -103,6 +103,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
//TraceManager.addDev("Before clone:\n" + spec);
initialSpec.removeLibraryFunctionCalls();
initialSpec.removeCompositeStates();
+ TraceManager.addDev("Before clone:\n" + initialSpec);
spec = initialSpec.advancedClone();
//TraceManager.addDev("After clone:\n" + spec);
}
diff --git a/src/main/java/ui/AvatarDesignPanelTranslator.java b/src/main/java/ui/AvatarDesignPanelTranslator.java
index 85eb6fbcbb517c8a8f8d37e4bda5af1a6fab7e78..2ce1bb4c7d9056391303038c5051615f57286e42 100644
--- a/src/main/java/ui/AvatarDesignPanelTranslator.java
+++ b/src/main/java/ui/AvatarDesignPanelTranslator.java
@@ -1742,7 +1742,7 @@ public class AvatarDesignPanelTranslator {
//TDiagramPanel tdp = asmdp;
// Search for composite AvatarStates: they cannot be checked for reachability and liveness
- for (TGComponent tgc : asmdp.getComponentList()) {
+ /*for (TGComponent tgc : asmdp.getComponentList()) {
if (tgc instanceof AvatarSMDState) {
AvatarSMDState sta = (AvatarSMDState)tgc;
if (sta.isACompositeState()) {
@@ -1758,7 +1758,7 @@ public class AvatarDesignPanelTranslator {
}
}
- }
+ }*/