diff --git a/src/avatartranslator/AvatarStateMachine.java b/src/avatartranslator/AvatarStateMachine.java index c82e1e210ed104874ac83ed5b9f2f75ab0a3cac6..af3db6d3b09ca4fcd51e01d8782c0c8a225da125 100644 --- a/src/avatartranslator/AvatarStateMachine.java +++ b/src/avatartranslator/AvatarStateMachine.java @@ -93,6 +93,8 @@ public class AvatarStateMachine extends AvatarElement { } public void removeCompositeStates() { + removeAllInternalStartStates(); + AvatarTransition at; at = getCompositeTransition(); @@ -218,7 +220,7 @@ public class AvatarStateMachine extends AvatarElement { as.addNext(at); } else { // Badly formed machine! - TraceManager.addError("Badly formed sm (removing composite trasnition)"); + TraceManager.addError("Badly formed sm (removing composite transition)"); } } @@ -275,26 +277,35 @@ public class AvatarStateMachine extends AvatarElement { LinkedList<AvatarStartState> ll = new LinkedList<AvatarStartState>(); for(AvatarStateMachineElement element: elements) { if ((element instanceof AvatarStartState) && (element.getState() != null)) { - TraceManager.addDev("found a internal state state"); + TraceManager.addDev("-> -> found an internal state state"); ll.add((AvatarStartState)element); } } - + AvatarState as0; LinkedList<AvatarStateMachineElement> le; for(AvatarStartState as: ll) { AvatarState astate = as.getState(); if (as != null) { le = getPreviousElementsOf(astate); - if (astate.nbOfNexts() > 0) { - for(AvatarStateMachineElement element: elements) { + if (le.size() > 0) { + as0 = new AvatarState(astate.getName() + "__external", astate.getReferenceObject()); + as0.addNext(as.getNext(0)); + for(AvatarStateMachineElement element: le) { if (element instanceof AvatarTransition) { element.removeAllNexts(); - element.addNext(astate.getNext(0)); + element.addNext(as0); + as0.setState(element.getState()); } else { TraceManager.addDev("Badly formed state machine"); } } + // Remove the start state and its next transition + removeElement(as); + addElement(as0); + TraceManager.addDev("-> -> removed an internal state state!"); + } else { + TraceManager.addDev("Badly formed state machine"); } } } diff --git a/src/avatartranslator/AvatarTransition.java b/src/avatartranslator/AvatarTransition.java index e0218bb6f66f9fa6b403610488d7d8c2cae300c0..c5e2dcebb882a8f8d76f897f2b111201cfc1c5f2 100644 --- a/src/avatartranslator/AvatarTransition.java +++ b/src/avatartranslator/AvatarTransition.java @@ -144,6 +144,10 @@ public class AvatarTransition extends AvatarStateMachineElement { at.addAction(getAction(i)); } + for(int i=0; i<nbOfNexts(); i++) { + at.addNext(getNext(i)); + } + return at; } diff --git a/src/avatartranslator/touppaal/AVATAR2UPPAAL.java b/src/avatartranslator/touppaal/AVATAR2UPPAAL.java index a92aae83e5c6120dea7acdfd72390611f3457e4b..ea4555a9175776b0fa0925781aebf31cd2802a15 100755 --- a/src/avatartranslator/touppaal/AVATAR2UPPAAL.java +++ b/src/avatartranslator/touppaal/AVATAR2UPPAAL.java @@ -148,6 +148,8 @@ public class AVATAR2UPPAAL { avspec.removeCompositeStates(); + TraceManager.addDev("Spec:" + avspec.toString()); + UPPAALLocation.reinitID(); gatesNotSynchronized = new LinkedList(); gatesNotSynchronized.add("makeChoice");