From bb7f24f6d0cd61b0d8def14cd70c66a1511fcd56 Mon Sep 17 00:00:00 2001
From: Ludovic Apvrille <ludovic.apvrille@telecom-paristech.fr>
Date: Fri, 28 May 2010 14:20:05 +0000
Subject: [PATCH] Update on AVATAR to UPPAAL Translation: support of composite
states
---
src/avatartranslator/AvatarStateMachine.java | 23 ++++++++++++++-----
src/avatartranslator/AvatarTransition.java | 4 ++++
.../touppaal/AVATAR2UPPAAL.java | 2 ++
3 files changed, 23 insertions(+), 6 deletions(-)
diff --git a/src/avatartranslator/AvatarStateMachine.java b/src/avatartranslator/AvatarStateMachine.java
index c82e1e210e..af3db6d3b0 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 e0218bb6f6..c5e2dcebb8 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 a92aae83e5..ea4555a917 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");
--
GitLab