diff --git a/src/main/java/avatartranslator/AvatarLibraryFunction.java b/src/main/java/avatartranslator/AvatarLibraryFunction.java index 72eb4f59d14b19fac93d23256459e9593dfd5a82..86d5495ff26f75804719715d826ad319f14a451d 100644 --- a/src/main/java/avatartranslator/AvatarLibraryFunction.java +++ b/src/main/java/avatartranslator/AvatarLibraryFunction.java @@ -451,9 +451,11 @@ public class AvatarLibraryFunction extends AvatarElement implements AvatarTransl * * @return The last element of the state machine created. */ - public AvatarState translateASMWithMapping( Map<AvatarAttribute, AvatarAttribute> placeholdersMapping, Map<AvatarSignal, AvatarSignal> signalsMapping, AvatarStateMachineElement firstElement, AvatarBlock block, Object referenceObject, int counter) { + public AvatarState translateASMWithMapping( Map<AvatarAttribute, AvatarAttribute> placeholdersMapping, Map<AvatarSignal, AvatarSignal> signalsMapping, + AvatarStateMachineElement firstElement, AvatarBlock block, Object referenceObject, int counter) { /* Create the last state */ AvatarState lastState = new AvatarState ("exit_" + this.name + "_" + counter, referenceObject); + block.getStateMachine().addElement(lastState); /* Create the argument object that will be passed to translation functions */ Object arg = new TranslatorArgument ( @@ -490,7 +492,7 @@ public class AvatarLibraryFunction extends AvatarElement implements AvatarTransl arg.elementsMapping.put (placeholder, asme); // Must be added to the state machine as well? - //asm.addElement(asme); + arg.block.getStateMachine().addElement(asme); /* If there is no next element, consider this as an end state */ if (placeholder.nbOfNexts () == 0) { diff --git a/src/main/java/avatartranslator/AvatarSpecification.java b/src/main/java/avatartranslator/AvatarSpecification.java index c9e38d61264b8db806f03a396e382dbc14d01442..cbb51f59091a64374e8f49d1091f6ca1cb82f24c 100644 --- a/src/main/java/avatartranslator/AvatarSpecification.java +++ b/src/main/java/avatartranslator/AvatarSpecification.java @@ -498,6 +498,9 @@ public class AvatarSpecification extends AvatarElement { asm.removeLibraryFunctionCalls (block); } + + + //TraceManager.addDev("\n\nNew spec:" + this.toString() + "\n"); } public boolean hasLossyChannel() { diff --git a/src/main/java/avatartranslator/AvatarStateMachine.java b/src/main/java/avatartranslator/AvatarStateMachine.java index d6bb4b6d9639b12c17f122e70e6956e44a7bcd25..dfe82a9756995265ff4f986c119584bdb627c086 100644 --- a/src/main/java/avatartranslator/AvatarStateMachine.java +++ b/src/main/java/avatartranslator/AvatarStateMachine.java @@ -1501,21 +1501,30 @@ public class AvatarStateMachine extends AvatarElement { if (curAsme instanceof AvatarLibraryFunctionCall) { AvatarLibraryFunctionCall alfc = (AvatarLibraryFunctionCall) curAsme; + /* Create a state that will be used as an entry point for the sub-state machine */ AvatarState firstState = new AvatarState("entry_" + alfc.getLibraryFunction().getName() + "_" + alfc.getCounter(), curAsme.getReferenceObject()); + elements.add(firstState); /* Add this state to the mapping so that future state can use it to replace their next element */ callsTranslated.put(alfc, firstState); /* inline the function call */ AvatarStateMachineElement lastState = alfc.inlineFunctionCall(block, firstState); + TraceManager.addDev("LAST STATE IS " + lastState + " class=" + lastState.getClass().getCanonicalName()); /* Add the next elements to the newly created last state */ for (AvatarStateMachineElement asme : curAsme.getNexts()) lastState.addNext(asme); + /* Remove the call in the list of elements */ + elements.remove(curAsme); + + /* Use the translated function call's first element as current element */ curAsme = firstState; + + } /* Add current element to the visited set */ diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java index 3c51a8809ddb34c7a2ad6854fea380eff2ad4e94..e597096279d5e9e9534d721b7fddc1cd270e2315 100644 --- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java +++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java @@ -1110,8 +1110,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph { return _ase; } - //TraceManager.addDev("Handling Empty transition of previous= 4 " + _ase.getName() + " trans=" + at.getName() + " delay=" + at.getMinDelay()); - + //TraceManager.addDev("Handling Empty transition of previous= 4 " + _ase.getName() + " trans=" + at.getName() + " delay=" + at.getMinDelay() + " guard=" + at.getGuard() + " next=" + at.getNext(0)); AvatarStateElement ase = (AvatarStateElement) (at.getNext(0)); checkElement(ase, _ss);