From 5a686f808f910a97c1de934f23c9c58c4e4ed4ca Mon Sep 17 00:00:00 2001
From: Ludovic Apvrille <ludovic.apvrille@telecom-paristech.fr>
Date: Tue, 20 Jul 2010 11:42:50 +0000
Subject: [PATCH] AVATAR: Improvement on avatar-to-uppaal code generator
---
.../AvatarActionOnSignal.java | 9 +
src/avatartranslator/AvatarExpireTimer.java | 6 +
src/avatartranslator/AvatarRandom.java | 5 +
src/avatartranslator/AvatarResetTimer.java | 6 +
src/avatartranslator/AvatarSetTimer.java | 7 +
src/avatartranslator/AvatarStartState.java | 4 +
src/avatartranslator/AvatarState.java | 6 +-
src/avatartranslator/AvatarStateMachine.java | 225 +++++++++++++++---
.../AvatarStateMachineElement.java | 11 +-
src/avatartranslator/AvatarStopState.java | 4 +
src/avatartranslator/AvatarTimerOperator.java | 10 +-
src/avatartranslator/AvatarTransition.java | 29 ++-
.../touppaal/AVATAR2UPPAAL.java | 2 +-
13 files changed, 286 insertions(+), 38 deletions(-)
diff --git a/src/avatartranslator/AvatarActionOnSignal.java b/src/avatartranslator/AvatarActionOnSignal.java
index d91b8d5651..d26a79a6b8 100644
--- a/src/avatartranslator/AvatarActionOnSignal.java
+++ b/src/avatartranslator/AvatarActionOnSignal.java
@@ -81,5 +81,14 @@ public class AvatarActionOnSignal extends AvatarStateMachineElement {
public boolean isReceiving() {
return signal.isIn();
}
+
+ public AvatarActionOnSignal basicCloneMe() {
+ AvatarActionOnSignal aaos = new AvatarActionOnSignal(getName() + "_clone", getSignal(), getReferenceObject());
+ for(int i=0; i<getNbOfValues(); i++) {
+ aaos.addValue(getValue(i));
+ }
+
+ return aaos;
+ }
}
\ No newline at end of file
diff --git a/src/avatartranslator/AvatarExpireTimer.java b/src/avatartranslator/AvatarExpireTimer.java
index 11899bd62f..7b72977ea0 100644
--- a/src/avatartranslator/AvatarExpireTimer.java
+++ b/src/avatartranslator/AvatarExpireTimer.java
@@ -54,4 +54,10 @@ public class AvatarExpireTimer extends AvatarTimerOperator {
super(_name, _referenceObject);
}
+ public AvatarStateMachineElement basicCloneMe() {
+ AvatarExpireTimer aet = new AvatarExpireTimer(getName(), getReferenceObject());
+ aet.setTimer(getTimer());
+ return aet;
+ }
+
}
\ No newline at end of file
diff --git a/src/avatartranslator/AvatarRandom.java b/src/avatartranslator/AvatarRandom.java
index 8f51f74e78..3ecf00b0d7 100644
--- a/src/avatartranslator/AvatarRandom.java
+++ b/src/avatartranslator/AvatarRandom.java
@@ -87,4 +87,9 @@ public class AvatarRandom extends AvatarStateMachineElement {
functionId = _functionId;
}
+ public AvatarStateMachineElement basicCloneMe() {
+ AvatarRandom ar = new AvatarRandom(getName(), getReferenceObject());
+ return ar;
+ }
+
}
\ No newline at end of file
diff --git a/src/avatartranslator/AvatarResetTimer.java b/src/avatartranslator/AvatarResetTimer.java
index adb0e512a7..c0f9aeddf5 100644
--- a/src/avatartranslator/AvatarResetTimer.java
+++ b/src/avatartranslator/AvatarResetTimer.java
@@ -54,4 +54,10 @@ public class AvatarResetTimer extends AvatarTimerOperator {
super(_name, _referenceObject);
}
+ public AvatarStateMachineElement basicCloneMe() {
+ AvatarResetTimer art = new AvatarResetTimer(getName(), getReferenceObject());
+ art.setTimer(getTimer());
+ return art;
+ }
+
}
\ No newline at end of file
diff --git a/src/avatartranslator/AvatarSetTimer.java b/src/avatartranslator/AvatarSetTimer.java
index 356c40e8aa..c783d64937 100644
--- a/src/avatartranslator/AvatarSetTimer.java
+++ b/src/avatartranslator/AvatarSetTimer.java
@@ -63,4 +63,11 @@ public class AvatarSetTimer extends AvatarTimerOperator {
return setValue;
}
+ public AvatarStateMachineElement basicCloneMe() {
+ AvatarSetTimer ast = new AvatarSetTimer(getName(), getReferenceObject());
+ ast.setTimer(getTimer());
+ ast.setTimerValue(getTimerValue());
+ return ast;
+ }
+
}
\ No newline at end of file
diff --git a/src/avatartranslator/AvatarStartState.java b/src/avatartranslator/AvatarStartState.java
index 5f0d2f1c70..df11e2995c 100644
--- a/src/avatartranslator/AvatarStartState.java
+++ b/src/avatartranslator/AvatarStartState.java
@@ -54,5 +54,9 @@ public class AvatarStartState extends AvatarStateMachineElement {
public AvatarStartState(String _name, Object _referenceObject) {
super(_name, _referenceObject);
}
+
+ public AvatarStateMachineElement basicCloneMe() {
+ return new AvatarStartState(getName(), getReferenceObject());
+ }
}
\ No newline at end of file
diff --git a/src/avatartranslator/AvatarState.java b/src/avatartranslator/AvatarState.java
index d33f5cf8a4..34609086f3 100644
--- a/src/avatartranslator/AvatarState.java
+++ b/src/avatartranslator/AvatarState.java
@@ -52,6 +52,10 @@ public class AvatarState extends AvatarStateMachineElement {
public AvatarState(String _name, Object _referenceObject) {
super(_name, _referenceObject);
-
}
+
+ public AvatarStateMachineElement basicCloneMe() {
+ AvatarState as = new AvatarState(getName(), getReferenceObject());
+ return as;
+ }
}
\ No newline at end of file
diff --git a/src/avatartranslator/AvatarStateMachine.java b/src/avatartranslator/AvatarStateMachine.java
index ea6daa004d..dafc59a77c 100644
--- a/src/avatartranslator/AvatarStateMachine.java
+++ b/src/avatartranslator/AvatarStateMachine.java
@@ -106,11 +106,22 @@ public class AvatarStateMachine extends AvatarElement {
TraceManager.addDev("*** Found composite transition: " + at.toString());
}*/
+ LinkedList<AvatarStateMachineElement> toRemove = new LinkedList<AvatarStateMachineElement>();
+
while((at = getCompositeTransition()) != null) {
- TraceManager.addDev("*** Found composite transition: " + at.toString());
- TraceManager.addDev(_block.toString());
+ //TraceManager.addDev("*** Found composite transition: " + at.toString());
+ //TraceManager.addDev(_block.toString());
+ if (!(toRemove.contains(getPreviousElementOf(at)))) {
+ toRemove.add(getPreviousElementOf(at));
+ }
removeCompositeTransition(at, _block);
+
+ }
+
+ for(AvatarStateMachineElement asme: toRemove) {
+ removeElement(asme);
}
+
TraceManager.addDev(_block.toString());
removeAllSuperStates();
@@ -158,15 +169,20 @@ public class AvatarStateMachine extends AvatarElement {
private void removeCompositeTransition(AvatarTransition _at, AvatarBlock _block) {
AvatarState state = (AvatarState)(getPreviousElementOf(_at));
+ removeStopStatesOf(state);
+
// Remove "after" and replace them with timers
AvatarTransition at = removeAfter(_at, _block);
+ // Put state after transition
+ modifyAvatarTransition(at);
+
Vector <AvatarStateMachineElement> v = new Vector<AvatarStateMachineElement>();
for(AvatarStateMachineElement element: elements) {
//TraceManager.addDev("\nIs in composite state " + state + ": >" + element + "< ???");
if (element instanceof AvatarTransition) {
- TraceManager.addDev("at? element=" + element);
+ //TraceManager.addDev("at? element=" + element);
if (element.getNext(0).hasInUpperState(state) == true) {
if (getPreviousElementOf(element).hasInUpperState(state) == true) {
v.add(element);
@@ -180,9 +196,7 @@ public class AvatarStateMachine extends AvatarElement {
}
}
-
-
- TraceManager.addDev("*** Analyzing components in state " + state);
+ //TraceManager.addDev("*** Analyzing components in state " + state);
// Split avatar transitions
for(AvatarStateMachineElement element: v) {
TraceManager.addDev(">" + element + "<");
@@ -191,13 +205,13 @@ public class AvatarStateMachine extends AvatarElement {
}
}
- TraceManager.addDev("\nAdding new elements in state");
+ //TraceManager.addDev("\nAdding new elements in state");
v.clear();
for(AvatarStateMachineElement element: elements) {
//TraceManager.addDev("\nIs in composite state " + state + ": >" + element + "< ???");
if (element.hasInUpperState(state) == true) {
// We found a candidate!
- if (element != _at) {
+ if ((element != _at) && (element != at)) {
v.add(element);
}
}
@@ -234,7 +248,7 @@ public class AvatarStateMachine extends AvatarElement {
TraceManager.addDev("New split state");
AvatarState as = new AvatarState("splitstate", null);
as.setState(_currentState);
- AvatarTransition at = _at.basicCloneMe();
+ AvatarTransition at = (AvatarTransition)(_at.basicCloneMe());
_at.removeAllActionsButTheFirstOne();
at.removeFirstAction();
at.addNext(_at.getNext(0));
@@ -253,8 +267,8 @@ public class AvatarStateMachine extends AvatarElement {
AvatarTransition at;
LinkedList<AvatarStateMachineElement> ll;
- // It cannot be a start state since they have been previously removed ..
- if ((_element instanceof AvatarActionOnSignal) || (_element instanceof AvatarStopState)){
+ // It cannot be a start / stop state since they have been previously removed ..
+ if (_element instanceof AvatarActionOnSignal) {
ll = getPreviousElementsOf(_element);
for(AvatarStateMachineElement element: ll) {
if (element instanceof AvatarTransition) {
@@ -267,7 +281,7 @@ public class AvatarStateMachine extends AvatarElement {
as.addNext(at);
addElement(as);
- at = _at.cloneMe();
+ at = cloneCompositeTransition(_at);
addElement(at);
as.addNext(at);
@@ -278,8 +292,8 @@ public class AvatarStateMachine extends AvatarElement {
}
} else if (_element instanceof AvatarState) {
- at = _at.cloneMe();
- addElement(at);
+ at = cloneCompositeTransition(_at);
+ //addElement(at);
_element.addNext(at);
} else if (_element instanceof AvatarTransition) {
// Nothing to do since they shall have been split before
@@ -333,7 +347,7 @@ public class AvatarStateMachine extends AvatarElement {
for(AvatarStateMachineElement element: elements) {
if ((element instanceof AvatarStartState) && (element.getState() != null)) {
- TraceManager.addDev("-> -> found an internal state state");
+ //TraceManager.addDev("-> -> found an internal state state");
ll.add((AvatarStartState)element);
}
}
@@ -345,13 +359,13 @@ public class AvatarStateMachine extends AvatarElement {
if (as != null) {
le = getPreviousElementsOf(astate);
if (le.size() > 0) {
- as0 = new AvatarState(astate.getName() + "__entrance", astate.getReferenceObject());
+ as0 = new AvatarState("entrance__" + astate.getName(), astate.getReferenceObject());
as0.addNext(as.getNext(0));
+ as0.setState(astate);
for(AvatarStateMachineElement element: le) {
if (element instanceof AvatarTransition) {
element.removeAllNexts();
element.addNext(as0);
- as0.setState(astate);
} else {
TraceManager.addDev("Badly formed state machine");
}
@@ -364,7 +378,7 @@ public class AvatarStateMachine extends AvatarElement {
removeElement(as);
addElement(as0);
- TraceManager.addDev("-> -> removed an internal state state!");
+ //TraceManager.addDev("-> -> removed an internal state state!");
} else {
TraceManager.addDev("Badly formed state machine");
}
@@ -436,8 +450,8 @@ public class AvatarStateMachine extends AvatarElement {
TraceManager.addDev("Replacing " + oldone + " with " + newone);
- addElement(oldone);
- removeElement(newone);
+ addElement(newone);
+ removeElement(oldone);
// Previous elements
LinkedList<AvatarStateMachineElement> previous = getPreviousElementsOf(oldone);
@@ -459,20 +473,21 @@ public class AvatarStateMachine extends AvatarElement {
}
-
// We have to use a timer for this transition
AvatarAttribute aa = _block.addTimerAttribute("timer__");
AvatarAttribute val = _block.addIntegerAttribute(aa.getName() + "_val");
- TraceManager.addDev("ADDING TIMER: " + aa.getName());
+ //TraceManager.addDev("ADDING TIMER: " + aa.getName());
// Timer is set at the entrance in the composite state
- LinkedList<AvatarTransition> ll = findEntranceTransitionElements(_at.getState());
+ LinkedList<AvatarTransition> ll = findEntranceTransitionElements((AvatarState)(getPreviousElementOf(_at)));
AvatarTransition newat0, newat1;
AvatarSetTimer ast;
AvatarRandom ar;
+ AvatarState as;
for(AvatarTransition att: ll) {
+ //TraceManager.addDev(" ------------------ Dealing with an entrance transition");
ar = new AvatarRandom("randomfortimer", _block.getReferenceObject());
ar.setVariable(val.getName());
ar.setValues(_at.getMinDelay(), _at.getMaxDelay());
@@ -501,12 +516,18 @@ public class AvatarStateMachine extends AvatarElement {
// Wait for timer expiration on the transition
AvatarExpireTimer aet = new AvatarExpireTimer("expiretimer_" + aa.getName(), _block.getReferenceObject());
aet.setTimer(aa);
- newat0 = new AvatarTransition("transition_expiretimer_" + aa.getName(), _block.getReferenceObject());
-
+ newat0 = new AvatarTransition("transition0_expiretimer_" + aa.getName(), _block.getReferenceObject());
+ newat1 = new AvatarTransition("transition1_expiretimer_" + aa.getName(), _block.getReferenceObject());
+ as = new AvatarState("state1_expiretimer_" + aa.getName(), _block.getReferenceObject());
addElement(aet);
addElement(newat0);
+ addElement(newat1);
+ addElement(as);
+
newat0.addNext(aet);
- aet.addNext(_at);
+ aet.addNext(newat1);
+ newat1.addNext(as);
+ _at.setDelays("", "");
LinkedList<AvatarStateMachineElement> elts = getElementsLeadingTo(_at);
@@ -515,25 +536,26 @@ public class AvatarStateMachine extends AvatarElement {
elt.addNext(newat0);
}
- return newat0;
-
+ as.addNext(_at);
+ return newat0;
}
public LinkedList<AvatarTransition> findEntranceTransitionElements(AvatarState _state) {
+ //TraceManager.addDev("Searching for transitions entering:" + _state.getName());
LinkedList<AvatarTransition> ll = new LinkedList<AvatarTransition>();
for(AvatarStateMachineElement elt: elements) {
if (elt instanceof AvatarTransition) {
-
+ AvatarStateMachineElement element = getPreviousElementOf(elt);
if (elt.getNext(0) == _state) {
ll.add((AvatarTransition)elt);
- } else if (elt.inAnUpperStateOf(_state)) {
+ } else if (element.inAnUpperStateOf(_state) && (elt.getNext(0).getState() == _state)) {
ll.add((AvatarTransition)elt);
}
}
}
-
+ //TraceManager.addDev("Nb of elements found:" + ll.size());
return ll;
}
@@ -549,5 +571,146 @@ public class AvatarStateMachine extends AvatarElement {
return elts;
}
+
+
+ public void modifyAvatarTransition(AvatarTransition _at) {
+ /*if ((_at.getNbOfAction() > 0) || (_at.hasCompute())) {
+ return;
+ }*/
+
+ AvatarStateMachineElement next = _at.getNext(0);
+
+ if (next instanceof AvatarState) {
+ return;
+ } else if ((next instanceof AvatarTimerOperator) || (next instanceof AvatarActionOnSignal)) {
+
+ TraceManager.addDev("-> Timer modification");
+
+ AvatarState myState = new AvatarState("statefortransition", _at.getReferenceObject());
+ AvatarTransition at2 = new AvatarTransition("transitionfortransition", _at.getReferenceObject());
+ AvatarTransition at1 = (AvatarTransition)(next.getNext(0));
+
+ next.removeAllNexts();
+ next.addNext(at2);
+ at2.addNext(myState);
+ myState.addNext(at1);
+
+ addElement(myState);
+ addElement(at2);
+
+ return;
+ } else {
+ AvatarState myState = new AvatarState("statefortransition", _at.getReferenceObject());
+ AvatarTransition at = new AvatarTransition("transitionfortransition", _at.getReferenceObject());
+ at.addNext(_at.getNext(0));
+ _at.removeAllNexts();
+ _at.addNext(myState);
+ myState.addNext(at);
+ addElement(myState);
+ addElement(at);
+ return ;
+ }
+ }
+
+ public AvatarTransition cloneCompositeTransition(AvatarTransition _at) {
+ TraceManager.addDev("Must clone: " + _at);
+ // We clone elements until we find a state!
+ AvatarStateMachineElement tomake, current;
+ AvatarStateMachineElement tmp;
+ AvatarTransition at = (AvatarTransition)(_at.basicCloneMe());
+ addElement(at);
+
+ current = _at.getNext(0);
+ tomake = at;
+
+ while((current != null) && !(current instanceof AvatarState)) {
+ TraceManager.addDev("Cloning: " + current);
+ tmp = current.basicCloneMe();
+ addElement(tmp);
+ tomake.addNext(tmp);
+ tomake = tmp;
+ current = current.getNext(0);
+ if (current == null) {
+ break;
+ }
+ }
+
+ if (current == null) {
+ TraceManager.addDev("NULL CURRENT !!! NULL CURRENT");
+ }
+
+ tomake.addNext(current);
+
+ return at;
+
+ /*if ((_at.getNbOfAction() > 0) || (_at.hasCompute())) {
+ return _at.basicCloneMe();
+ }
+
+ AvatarStateMachineElement next = _at.getNext(0);
+
+ if (next instanceof AvatarActionOnSignal) {
+ AvatarTransition at = _at.
+ AvatarActionOnSignal aaos = ((AvatarActionOnSignal)next).basicCloneMe();
+ addElement(at);
+ addElement(aaos);
+ at.addNext(aaos);
+ aaos.addNext(next.getNext(0)); // Shall be a state!
+ return at;
+ }
+
+ if (next instanceof AvatarExpireTimer) {
+ AvatarTransition at = _at.basicCloneMe();
+ AvatarExpireTimer aet = ((AvatarExpireTimer)next).basicCloneMe();
+ AvatarTransition
+ addElement(at);
+ addElement(aet);
+ at.addNext(aet);
+ aet.addNext(next.getNext(0)); // Shall be a state!
+ return at;
+ }
+
+ if (next instanceof AvatarResetTimer) {
+ AvatarTransition at = _at.basicCloneMe();
+ AvatarResetTimer art = ((AvatarResetTimer)next).basicCloneMe();
+ addElement(at);
+ addElement(art);
+ at.addNext(art);
+ art.addNext(next.getNext(0)); // Shall be a state!
+ return at;
+ }
+
+ if (next instanceof AvatarSetTimer) {
+ AvatarTransition at = _at.basicCloneMe();
+ AvatarSetTimer ast = ((AvatarSetTimer)next).basicCloneMe();
+ addElement(at);
+ addElement(ast);
+ at.addNext(ast);
+ ast.addNext(next.getNext(0)); // Shall be a state!
+ return at;
+ }
+
+ return _at.basicCloneMe();*/
+
+ }
+
+ public void removeStopStatesOf(AvatarState _as) {
+ LinkedList<AvatarStopState> ll = new LinkedList<AvatarStopState>();
+
+ for(AvatarStateMachineElement elt: elements) {
+ if (elt instanceof AvatarStopState) {
+ if (elt.getState() == _as) {
+ ll.add((AvatarStopState)elt);
+ }
+ }
+ }
+
+ for(AvatarStopState ass: ll) {
+ TraceManager.addDev("Removed a stop state");
+ AvatarState astate = new AvatarState("OldStopState", ass.getReferenceObject());
+ astate.setState(ass.getState());
+ replace(ass, astate);
+ }
+ }
}
\ No newline at end of file
diff --git a/src/avatartranslator/AvatarStateMachineElement.java b/src/avatartranslator/AvatarStateMachineElement.java
index ba5f926610..0facd74778 100644
--- a/src/avatartranslator/AvatarStateMachineElement.java
+++ b/src/avatartranslator/AvatarStateMachineElement.java
@@ -48,7 +48,7 @@ package avatartranslator;
import java.util.*;
-public class AvatarStateMachineElement extends AvatarElement {
+public abstract class AvatarStateMachineElement extends AvatarElement {
private LinkedList<AvatarStateMachineElement> nexts;
private AvatarState myState;
@@ -131,9 +131,16 @@ public class AvatarStateMachineElement extends AvatarElement {
ret += cpt + ":" + element.getName() + "/ ID=" + element.getID() + " ";
cpt ++;
}
+
+ ret += specificToString();
+
return ret;
}
+ public String specificToString() {
+ return "";
+ }
+
public int nbOfNexts() {
return nexts.size();
}
@@ -173,5 +180,7 @@ public class AvatarStateMachineElement extends AvatarElement {
return (element instanceof AvatarActionOnSignal);
}
+ public abstract AvatarStateMachineElement basicCloneMe();
+
}
\ No newline at end of file
diff --git a/src/avatartranslator/AvatarStopState.java b/src/avatartranslator/AvatarStopState.java
index cfd7ead258..6af8ea1274 100644
--- a/src/avatartranslator/AvatarStopState.java
+++ b/src/avatartranslator/AvatarStopState.java
@@ -54,5 +54,9 @@ public class AvatarStopState extends AvatarStateMachineElement {
public AvatarStopState(String _name, Object _referenceObject) {
super(_name, _referenceObject);
}
+
+ public AvatarStateMachineElement basicCloneMe() {
+ return new AvatarStartState(getName(), getReferenceObject());
+ }
}
\ No newline at end of file
diff --git a/src/avatartranslator/AvatarTimerOperator.java b/src/avatartranslator/AvatarTimerOperator.java
index 475170e138..eb7d16d262 100644
--- a/src/avatartranslator/AvatarTimerOperator.java
+++ b/src/avatartranslator/AvatarTimerOperator.java
@@ -48,7 +48,7 @@ package avatartranslator;
import java.util.*;
-public class AvatarTimerOperator extends AvatarStateMachineElement {
+public abstract class AvatarTimerOperator extends AvatarStateMachineElement {
protected AvatarAttribute timer;
public AvatarTimerOperator(String _name, Object _referenceObject) {
@@ -63,4 +63,12 @@ public class AvatarTimerOperator extends AvatarStateMachineElement {
return timer;
}
+ public String specificToString() {
+ if (timer != null) {
+ return "\n timer: " + timer.getName();
+ }
+
+ return "";
+ }
+
}
\ No newline at end of file
diff --git a/src/avatartranslator/AvatarTransition.java b/src/avatartranslator/AvatarTransition.java
index 91af544eed..64ed2e5801 100644
--- a/src/avatartranslator/AvatarTransition.java
+++ b/src/avatartranslator/AvatarTransition.java
@@ -136,13 +136,15 @@ public class AvatarTransition extends AvatarStateMachineElement {
return at;
}
- public AvatarTransition basicCloneMe() {
- AvatarTransition at = new AvatarTransition(getName(), getReferenceObject());
+ public AvatarStateMachineElement basicCloneMe() {
+ AvatarTransition at = new AvatarTransition(getName() + "_clone", getReferenceObject());
for(int i=0; i<getNbOfAction(); i++) {
at.addAction(getAction(i));
}
+ at.setComputes(getMinCompute(), getMaxCompute());
+
return at;
}
@@ -213,7 +215,28 @@ public class AvatarTransition extends AvatarStateMachineElement {
return false;
}
-
+ public String specificToString() {
+ String ret = "";
+ if (hasDelay()) {
+ ret += "minDelay=" + getMinDelay() + " maxDelay=" + getMaxDelay() + "\n";
+ }
+
+ if (hasCompute()) {
+ ret += "minCompute=" + getMinCompute() + " maxcompute=" + getMaxCompute() + "\n";
+ }
+
+ for(String s: actions) {
+ if (s.trim().length() > 0) {
+ ret += s.trim() + " / ";
+ }
+ }
+
+ if (ret.length() > 0) {
+ ret = "\n" + ret;
+ }
+
+ return ret;
+ }
diff --git a/src/avatartranslator/touppaal/AVATAR2UPPAAL.java b/src/avatartranslator/touppaal/AVATAR2UPPAAL.java
index 4a930b5585..66890a43a1 100755
--- a/src/avatartranslator/touppaal/AVATAR2UPPAAL.java
+++ b/src/avatartranslator/touppaal/AVATAR2UPPAAL.java
@@ -152,7 +152,7 @@ public class AVATAR2UPPAAL {
avspec.removeCompositeStates();
avspec.removeTimers();
- //TraceManager.addDev("-> Spec:" + avspec.toString());
+ TraceManager.addDev("-> Spec:" + avspec.toString());
UPPAALLocation.reinitID();
gatesNotSynchronized = new LinkedList();
--
GitLab