From c934fdebd5fffcd00f50fdc1df05f1ada4bf91d3 Mon Sep 17 00:00:00 2001
From: Ludovic Apvrille <ludovic.apvrille@telecom-paristech.fr>
Date: Fri, 16 Jul 2010 15:56:52 +0000
Subject: [PATCH] AVATAR: Update on composite state management
---
src/avatartranslator/AvatarBlock.java | 17 +++
src/avatartranslator/AvatarStateMachine.java | 137 +++++++++++++++---
.../AvatarStateMachineElement.java | 20 ++-
.../touppaal/AVATAR2UPPAAL.java | 2 +-
src/uppaaldesc/UPPAALLocation.java | 2 +
5 files changed, 155 insertions(+), 23 deletions(-)
diff --git a/src/avatartranslator/AvatarBlock.java b/src/avatartranslator/AvatarBlock.java
index f54ade5844..1c8a89045b 100644
--- a/src/avatartranslator/AvatarBlock.java
+++ b/src/avatartranslator/AvatarBlock.java
@@ -302,6 +302,23 @@ public class AvatarBlock extends AvatarElement {
return aa;
}
+ public AvatarAttribute addIntegerAttribute(String _name) {
+ AvatarAttribute aa;
+ int cpt;
+
+ for(cpt=0; cpt<50000; cpt++) {
+ aa = getAvatarAttributeWithName(_name + cpt);
+ if (aa == null) {
+ break;
+ }
+ }
+
+ aa = new AvatarAttribute(_name+cpt, AvatarType.INTEGER, getReferenceObject());
+ addAttribute(aa);
+
+ return aa;
+ }
+
}
\ No newline at end of file
diff --git a/src/avatartranslator/AvatarStateMachine.java b/src/avatartranslator/AvatarStateMachine.java
index 01e284f098..ea6daa004d 100644
--- a/src/avatartranslator/AvatarStateMachine.java
+++ b/src/avatartranslator/AvatarStateMachine.java
@@ -101,14 +101,17 @@ public class AvatarStateMachine extends AvatarElement {
AvatarTransition at;
- at = getCompositeTransition();
+ /*at = getCompositeTransition();
if (at != null) {
TraceManager.addDev("*** Found composite transition: " + at.toString());
- }
+ }*/
while((at = getCompositeTransition()) != null) {
+ TraceManager.addDev("*** Found composite transition: " + at.toString());
+ TraceManager.addDev(_block.toString());
removeCompositeTransition(at, _block);
}
+ TraceManager.addDev(_block.toString());
removeAllSuperStates();
}
@@ -155,10 +158,21 @@ public class AvatarStateMachine extends AvatarElement {
private void removeCompositeTransition(AvatarTransition _at, AvatarBlock _block) {
AvatarState state = (AvatarState)(getPreviousElementOf(_at));
+ // Remove "after" and replace them with timers
+ AvatarTransition at = removeAfter(_at, _block);
+
Vector <AvatarStateMachineElement> v = new Vector<AvatarStateMachineElement>();
for(AvatarStateMachineElement element: elements) {
- if (element.hasInUpperState(state) == true) {
+ //TraceManager.addDev("\nIs in composite state " + state + ": >" + element + "< ???");
+ if (element instanceof AvatarTransition) {
+ TraceManager.addDev("at? element=" + element);
+ if (element.getNext(0).hasInUpperState(state) == true) {
+ if (getPreviousElementOf(element).hasInUpperState(state) == true) {
+ v.add(element);
+ }
+ }
+ } else if (element.hasInUpperState(state) == true) {
// We found a candidate!
if (element != _at) {
v.add(element);
@@ -166,29 +180,39 @@ public class AvatarStateMachine extends AvatarElement {
}
}
- // Remove "after" and replace them with timers
+
+
+ TraceManager.addDev("*** Analyzing components in state " + state);
+ // Split avatar transitions
for(AvatarStateMachineElement element: v) {
+ TraceManager.addDev(">" + element + "<");
if (element instanceof AvatarTransition) {
- removeAfter((AvatarTransition)element, _block);
+ splitAvatarTransition((AvatarTransition)element, state);
}
}
- // Split avatar transitions
- for(AvatarStateMachineElement element: v) {
- if (element instanceof AvatarTransition) {
- splitAvatarTransition((AvatarTransition)element);
+ 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) {
+ v.add(element);
+ }
}
}
+
for(AvatarStateMachineElement element: v) {
- adaptCompositeTransition(_at, element, 0);
+ adaptCompositeTransition(at, element, 0);
}
- removeElement(_at);
+ removeElement(at);
}
- private void splitAvatarTransition(AvatarTransition _at) {
+ private void splitAvatarTransition(AvatarTransition _at, AvatarState _currentState) {
/*if (_at.hasCompute()) {
AvatarState as0 = new AvatarState("splitstate0", null);
AvatarState as1 = new AvatarState("splitstate1", null);
@@ -205,18 +229,22 @@ public class AvatarStateMachine extends AvatarElement {
splitAvatarTransition(at);
}*/
+ TraceManager.addDev(" - - - - - - - - - - Split transition nbofactions=" + _at.getNbOfAction());
if (_at.getNbOfAction() > 1) {
+ TraceManager.addDev("New split state");
AvatarState as = new AvatarState("splitstate", null);
+ as.setState(_currentState);
AvatarTransition at = _at.basicCloneMe();
_at.removeAllActionsButTheFirstOne();
at.removeFirstAction();
+ at.addNext(_at.getNext(0));
_at.removeAllNexts();
_at.addNext(as);
as.addNext(at);
addElement(as);
addElement(at);
- splitAvatarTransition(at);
+ splitAvatarTransition(at, _currentState);
}
}
@@ -317,13 +345,13 @@ public class AvatarStateMachine extends AvatarElement {
if (as != null) {
le = getPreviousElementsOf(astate);
if (le.size() > 0) {
- as0 = new AvatarState(astate.getName() + "__external", astate.getReferenceObject());
+ as0 = new AvatarState(astate.getName() + "__entrance", astate.getReferenceObject());
as0.addNext(as.getNext(0));
for(AvatarStateMachineElement element: le) {
if (element instanceof AvatarTransition) {
element.removeAllNexts();
element.addNext(as0);
- as0.setState(element.getState());
+ as0.setState(astate);
} else {
TraceManager.addDev("Badly formed state machine");
}
@@ -424,18 +452,70 @@ public class AvatarStateMachine extends AvatarElement {
}
}
- public void removeAfter(AvatarTransition at, AvatarBlock _block) {
- String delay = at.getMinDelay();
+ public AvatarTransition removeAfter(AvatarTransition _at, AvatarBlock _block) {
+ String delay = _at.getMinDelay();
if ((delay == null) || (delay.trim().length() == 0)) {
- return;
+ return _at;
}
+
+
// 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());
// Timer is set at the entrance in the composite state
- LinkedList<AvatarTransition> ll = findEntranceTransitionElements(at.getState());
+ LinkedList<AvatarTransition> ll = findEntranceTransitionElements(_at.getState());
+
+ AvatarTransition newat0, newat1;
+ AvatarSetTimer ast;
+ AvatarRandom ar;
+ for(AvatarTransition att: ll) {
+ ar = new AvatarRandom("randomfortimer", _block.getReferenceObject());
+ ar.setVariable(val.getName());
+ ar.setValues(_at.getMinDelay(), _at.getMaxDelay());
+
+ ast = new AvatarSetTimer("settimer_" + aa.getName(), _block.getReferenceObject());
+ ast.setTimerValue(val.getName());
+ ast.setTimer(aa);
+
+ newat0 = new AvatarTransition("transition_settimer_" + aa.getName(), _block.getReferenceObject());
+ newat1 = new AvatarTransition("transition_settimer_" + aa.getName(), _block.getReferenceObject());
+
+ elements.add(ar);
+ elements.add(ast);
+ elements.add(newat0);
+ elements.add(newat1);
+
+ newat1.addNext(att.getNext(0));
+ att.removeAllNexts();
+ att.addNext(ar);
+ ar.addNext(newat0);
+ newat0.addNext(ast);
+ ast.addNext(newat1);
+
+ }
+
+ // 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());
+
+ addElement(aet);
+ addElement(newat0);
+ newat0.addNext(aet);
+ aet.addNext(_at);
+ LinkedList<AvatarStateMachineElement> elts = getElementsLeadingTo(_at);
+
+ for(AvatarStateMachineElement elt: elts) {
+ elt.removeNext(_at);
+ elt.addNext(newat0);
+ }
+
+ return newat0;
}
@@ -445,12 +525,29 @@ public class AvatarStateMachine extends AvatarElement {
for(AvatarStateMachineElement elt: elements) {
if (elt instanceof AvatarTransition) {
- if (elt.inAnUpperStateThan(_state)) {
+
+ if (elt.getNext(0) == _state) {
+ ll.add((AvatarTransition)elt);
+ } else if (elt.inAnUpperStateOf(_state)) {
+ ll.add((AvatarTransition)elt);
}
}
}
return ll;
}
+
+ public LinkedList<AvatarStateMachineElement> getElementsLeadingTo(AvatarStateMachineElement _elt) {
+ LinkedList<AvatarStateMachineElement> elts = new LinkedList<AvatarStateMachineElement>();
+
+ for(AvatarStateMachineElement elt: elements) {
+ if (elt.hasNext(_elt)) {
+ elts.add(elt);
+ }
+ }
+
+ return elts;
+
+ }
}
\ No newline at end of file
diff --git a/src/avatartranslator/AvatarStateMachineElement.java b/src/avatartranslator/AvatarStateMachineElement.java
index d6d225c236..ba5f926610 100644
--- a/src/avatartranslator/AvatarStateMachineElement.java
+++ b/src/avatartranslator/AvatarStateMachineElement.java
@@ -97,8 +97,24 @@ public class AvatarStateMachineElement extends AvatarElement {
return false;
}
- public boolean inAnUpperStateThan(AvatarState _state) {
- return true;
+ public boolean inAnUpperStateOf(AvatarState _state) {
+ if (_state == null) {
+ return false;
+ }
+
+ AvatarState as = getState();
+ if (as == null) {
+ return true;
+ }
+
+ while((_state = _state.getState()) != null) {
+ if (_state == as) {
+ return true;
+ }
+ }
+
+ return false;
+
}
public String toString() {
diff --git a/src/avatartranslator/touppaal/AVATAR2UPPAAL.java b/src/avatartranslator/touppaal/AVATAR2UPPAAL.java
index f2399b5529..4a930b5585 100755
--- a/src/avatartranslator/touppaal/AVATAR2UPPAAL.java
+++ b/src/avatartranslator/touppaal/AVATAR2UPPAAL.java
@@ -927,7 +927,7 @@ public class AVATAR2UPPAAL {
result[0] = signal;
- TraceManager.addDev("Nb of params on signal " + signal + ":" + _aaos.getNbOfValues());
+ //TraceManager.addDev("Nb of params on signal " + signal + ":" + _aaos.getNbOfValues());
for(int i=0; i<_aaos.getNbOfValues(); i++) {
val = _aaos.getValue(i);
diff --git a/src/uppaaldesc/UPPAALLocation.java b/src/uppaaldesc/UPPAALLocation.java
index 04e4286153..3fa6480d6d 100755
--- a/src/uppaaldesc/UPPAALLocation.java
+++ b/src/uppaaldesc/UPPAALLocation.java
@@ -78,6 +78,7 @@ public class UPPAALLocation {
public void setUrgent() {
urgent = true;
+ committed = false;
}
public void unsetUrgent() {
@@ -86,6 +87,7 @@ public class UPPAALLocation {
public void setCommitted() {
committed = true;
+ urgent = false;
}
public void unsetCommitted() {
--
GitLab