From ec05d41e20cf2a4f3c42f6e9069033e7bf2614d3 Mon Sep 17 00:00:00 2001
From: apvrille <ludovic.apvrille@eurecom.fr>
Date: Fri, 30 Aug 2019 16:22:07 +0200
Subject: [PATCH] Update on RG generation when having function calls
---
.../java/avatartranslator/AvatarLibraryFunction.java | 6 ++++--
src/main/java/avatartranslator/AvatarSpecification.java | 3 +++
src/main/java/avatartranslator/AvatarStateMachine.java | 9 +++++++++
.../modelchecker/AvatarModelChecker.java | 3 +--
4 files changed, 17 insertions(+), 4 deletions(-)
diff --git a/src/main/java/avatartranslator/AvatarLibraryFunction.java b/src/main/java/avatartranslator/AvatarLibraryFunction.java
index 72eb4f59d1..86d5495ff2 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 c9e38d6126..cbb51f5909 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 d6bb4b6d96..dfe82a9756 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 3c51a8809d..e597096279 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);
--
GitLab