diff --git a/src/avatartranslator/AvatarBlockTemplate.java b/src/avatartranslator/AvatarBlockTemplate.java
new file mode 100644
index 0000000000000000000000000000000000000000..9a80fc0462074b4c901fc5e314b2aa422a1c0fda
--- /dev/null
+++ b/src/avatartranslator/AvatarBlockTemplate.java
@@ -0,0 +1,136 @@
+/**Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
+
+ludovic.apvrille AT enst.fr
+
+This software is a computer program whose purpose is to allow the
+edition of TURTLE analysis, design and deployment diagrams, to
+allow the generation of RT-LOTOS or Java code from this diagram,
+and at last to allow the analysis of formal validation traces
+obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
+from INRIA Rhone-Alpes.
+
+This software is governed by the CeCILL license under French law and
+abiding by the rules of distribution of free software. You can use,
+modify and/ or redistribute the software under the terms of the CeCILL
+license as circulated by CEA, CNRS and INRIA at the following URL
+"http://www.cecill.info".
+
+As a counterpart to the access to the source code and rights to copy,
+modify and redistribute granted by the license, users are provided only
+with a limited warranty and the software's author, the holder of the
+economic rights, and the successive licensors have only limited
+liability.
+
+In this respect, the user's attention is drawn to the risks associated
+with loading, using, modifying and/or developing or reproducing the
+software by the user in light of its specific status of free software,
+that may mean that it is complicated to manipulate, and that also
+therefore means that it is reserved for developers and experienced
+professionals having in-depth computer knowledge. Users are therefore
+encouraged to load and test the software's suitability as regards their
+requirements in conditions enabling the security of their systems and/or
+data to be ensured and, more generally, to use and operate it in the
+same conditions as regards security.
+
+The fact that you are presently reading this means that you have had
+knowledge of the CeCILL license and that you accept its terms.
+
+/**
+ * Class AvatarBlockTemplate
+ * Templates of AVATAR blocks (Timers, etc.)
+ * Creation: 09/07/2010
+ * @version 1.0 09/07/2010
+ * @author Ludovic APVRILLE
+ * @see
+ */
+
+
+package avatartranslator;
+
+import java.util.*;
+
+import myutil.*;
+
+public class AvatarBlockTemplate {
+
+ public AvatarBlockTemplate() {
+ }
+
+ public static AvatarBlock getTimerBlock(String _name, Object _reference) {
+ AvatarBlock ab = new AvatarBlock(_name, _reference);
+
+ AvatarAttribute aa = new avatarAttribute("value", AvatarType.NATURAL, _reference);
+ ab.addAttribute(aa);
+
+ AvatarSignal set = new AvatarSignal("set", AvatarSignal.IN, _reference);
+ AvatarSignal reset = new AvatarSignal("reset", AvatarSignal.IN, _reference);
+ AvatarSignal expire = new AvatarSignal("expire", AvatarSignal.OUT, _reference);
+ ab.addSignal(set);
+ ab.addSignal(reset);
+ ab.addSignal(expire);
+
+ AvatarStateMachine asm = ab.getStateMachine();
+ AvatarStartState ass = new AvatarStartState("start", _reference);
+
+ asm.setStartState(ass);
+ asm.addElement(asm);
+
+ AvatarState as1 = new AvatarState("wait4set", _reference);
+ asm.addElement(as1);
+
+ AvatarState as2 = new AvatarState("wait4expire", _reference);
+ asm.addElement(as2);
+
+ AvatarActionOnSignal aaos1 = new AvatarActionOnSignal("set1", set, _reference);
+ aaos1.addValue("value");
+ asm.addElement(aaos1);
+
+ AvatarActionOnSignal aaos2 = new AvatarActionOnSignal("set2", set, _reference);
+ aaos1.addValue("value");
+ asm.addElement(aaos2);
+
+ AvatarActionOnSignal aaos3 = new AvatarActionOnSignal("reset1", set, _reference);
+ asm.addElement(aaos3);
+
+ AvatarActionOnSignal aaos4 = new AvatarActionOnSignal("reset2", set, _reference);
+ asm.addElement(aaos4);
+
+ AvatarActionOnSignal aaos5 = new AvatarActionOnSignal("expire", set, _reference);
+ asm.addElement(aaos5);
+
+ AvatarTransition at;
+
+ // set
+ at = makeAvatarEmptyTransitionBetween(asm, ass, as1, _reference);
+ at = makeAvatarEmptyTransitionBetween(asm, as1, aaos1, _reference);
+ at = makeAvatarEmptyTransitionBetween(asm, aaos1, as2, _reference);
+
+ at = makeAvatarEmptyTransitionBetween(asm, as2, aaos2, _reference);
+ at = makeAvatarEmptyTransitionBetween(asm, aaos2, as2, _reference);
+
+ // expire
+ at = makeAvatarEmptyTransitionBetween(asm, aaos5, as1, _reference);
+ at = makeAvatarEmptyTransitionBetween(asm, as2, aaos5, _reference);
+ at.setDelays("value", "value");
+
+ // reset
+ at = makeAvatarEmptyTransitionBetween(asm, aaos3, as1, _reference);
+ at = makeAvatarEmptyTransitionBetween(asm, as1, aaos3, _reference);
+ at = makeAvatarEmptyTransitionBetween(asm, aaos4, as1, _reference);
+ at = makeAvatarEmptyTransitionBetween(asm, as2, aaos4, _reference);
+
+ return ab;
+
+ }
+
+ public static AvatarTransition makeAvatarEmptyTransitionBetween(AvatarStateMachine _asm, AvatarStateMachineElement _elt1, AvatarStateMachineElement _elt2, Object _reference) {
+ AvatarTransition at = new AvatarTransition("tr", _reference);
+
+ asm.addElement(at);
+
+ _elt1.addNext(at);
+ at.addNext(_elt2);
+
+ return at;
+ }
+}
\ No newline at end of file
diff --git a/src/avatartranslator/AvatarRandom.java b/src/avatartranslator/AvatarRandom.java
new file mode 100644
index 0000000000000000000000000000000000000000..8f51f74e788849046ecbf3857fd813915bf573de
--- /dev/null
+++ b/src/avatartranslator/AvatarRandom.java
@@ -0,0 +1,90 @@
+/**Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
+ *
+ * ludovic.apvrille AT enst.fr
+ *
+ * This software is a computer program whose purpose is to allow the
+ * edition of TURTLE analysis, design and deployment diagrams, to
+ * allow the generation of RT-LOTOS or Java code from this diagram,
+ * and at last to allow the analysis of formal validation traces
+ * obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
+ * from INRIA Rhone-Alpes.
+ *
+ * This software is governed by the CeCILL license under French law and
+ * abiding by the rules of distribution of free software. You can use,
+ * modify and/ or redistribute the software under the terms of the CeCILL
+ * license as circulated by CEA, CNRS and INRIA at the following URL
+ * "http://www.cecill.info".
+ *
+ * As a counterpart to the access to the source code and rights to copy,
+ * modify and redistribute granted by the license, users are provided only
+ * with a limited warranty and the software's author, the holder of the
+ * economic rights, and the successive licensors have only limited
+ * liability.
+ *
+ * In this respect, the user's attention is drawn to the risks associated
+ * with loading, using, modifying and/or developing or reproducing the
+ * software by the user in light of its specific status of free software,
+ * that may mean that it is complicated to manipulate, and that also
+ * therefore means that it is reserved for developers and experienced
+ * professionals having in-depth computer knowledge. Users are therefore
+ * encouraged to load and test the software's suitability as regards their
+ * requirements in conditions enabling the security of their systems and/or
+ * data to be ensured and, more generally, to use and operate it in the
+ * same conditions as regards security.
+ *
+ * The fact that you are presently reading this means that you have had
+ * knowledge of the CeCILL license and that you accept its terms.
+ *
+ * /**
+ * Class AvatarRandom
+ * Creation: 12/07/2010
+ * @version 1.0 12/07/2010
+ * @author Ludovic APVRILLE
+ * @see
+ */
+
+package avatartranslator;
+
+import java.util.*;
+
+
+public class AvatarRandom extends AvatarStateMachineElement {
+ protected String variable;
+ protected String minValue;
+ protected String maxValue;
+ protected int functionId;
+
+ public AvatarRandom(String _name, Object _referenceObject) {
+ super(_name, _referenceObject);
+ }
+
+ public String getVariable() {
+ return variable;
+ }
+
+ public String getMinValue() {
+ return minValue;
+ }
+
+ public String getMaxValue() {
+ return maxValue;
+ }
+
+ public int getFunctionId() {
+ return functionId;
+ }
+
+ public void setVariable(String _variable) {
+ variable = _variable;
+ }
+
+ public void setValues(String _minValue, String _maxValue) {
+ minValue = _minValue;
+ maxValue = _maxValue;
+ }
+
+ public void setFunctionId(int _functionId) {
+ functionId = _functionId;
+ }
+
+}
\ No newline at end of file
diff --git a/src/avatartranslator/AvatarSpecification.java b/src/avatartranslator/AvatarSpecification.java
index 9350c9a25d065f98f001699d1f7ee5a2ca547b8a..afece0248cebe12d31d2beef278a0f218667f3ec 100644
--- a/src/avatartranslator/AvatarSpecification.java
+++ b/src/avatartranslator/AvatarSpecification.java
@@ -122,7 +122,7 @@ public class AvatarSpecification extends AvatarElement {
public void removeCompositeStates() {
for(AvatarBlock block: blocks) {
- block.getStateMachine().removeCompositeStates();
+ block.getStateMachine().removeCompositeStates(block);
}
}
diff --git a/src/avatartranslator/AvatarStateMachine.java b/src/avatartranslator/AvatarStateMachine.java
index 6bdfd12e0535bc418048414cbd00764ec6b6b104..47f37ffdce8c87add04f627a2a301ac10b17b53c 100644
--- a/src/avatartranslator/AvatarStateMachine.java
+++ b/src/avatartranslator/AvatarStateMachine.java
@@ -92,8 +92,12 @@ public class AvatarStateMachine extends AvatarElement {
return sb.toString();
}
- public void removeCompositeStates() {
- removeAllInternalStartStates();
+ public void removeCompositeStates(AvatarBlock _block) {
+ // Contains in odd index: composite state
+ // even index: new state replacing the start state
+
+ LinkedList <AvatarState> lists = removeAllInternalStartStates();
+
AvatarTransition at;
@@ -109,11 +113,7 @@ public class AvatarStateMachine extends AvatarElement {
removeAllSuperStates();
}
- private void removeallSuperStates() {
- for(AvatarStateMachineElement element: elements) {
- element.setState(null);
- }
- }
+
private AvatarTransition getCompositeTransition() {
for(AvatarStateMachineElement element: elements) {
@@ -174,7 +174,7 @@ public class AvatarStateMachine extends AvatarElement {
}
for(AvatarStateMachineElement element: v) {
- adaptCompositeTransition(_at, element);
+ adaptCompositeTransition(_at, element, 0);
}
removeElement(_at);
@@ -182,6 +182,22 @@ public class AvatarStateMachine extends AvatarElement {
}
private void splitAvatarTransition(AvatarTransition _at) {
+ /*if (_at.hasCompute()) {
+ AvatarState as0 = new AvatarState("splitstate0", null);
+ AvatarState as1 = new AvatarState("splitstate1", null);
+
+
+
+ AvatarTransition at = _at.basicCloneMe();
+ _at.removeAllActions();
+ _at.removeAllNexts();
+ _at.addNext(as);
+ as.addNext(at);
+ addElement(as);
+ addElement(at);
+ splitAvatarTransition(at);
+ }*/
+
if (_at.getNbOfAction() > 1) {
AvatarState as = new AvatarState("splitstate", null);
AvatarTransition at = _at.basicCloneMe();
@@ -197,7 +213,7 @@ public class AvatarStateMachine extends AvatarElement {
}
}
- private void adaptCompositeTransition(AvatarTransition _at, AvatarStateMachineElement _element) {
+ private void adaptCompositeTransition(AvatarTransition _at, AvatarStateMachineElement _element, int _transitionID) {
AvatarState as;
AvatarTransition at;
LinkedList<AvatarStateMachineElement> ll;
@@ -215,9 +231,11 @@ public class AvatarStateMachine extends AvatarElement {
at.addNext(_element);
as.addNext(at);
addElement(as);
+
at = _at.cloneMe();
addElement(at);
as.addNext(at);
+
} else {
// Badly formed machine!
TraceManager.addError("Badly formed sm (removing composite transition)");
@@ -272,9 +290,12 @@ public class AvatarStateMachine extends AvatarElement {
// All transitions reaching a state that has an internal start state
// shall in fact go directly to the nexts of the start state
- public void removeAllInternalStartStates() {
+ public LinkedList<AvatarState> removeAllInternalStartStates() {
// identify allstart state
LinkedList<AvatarStartState> ll = new LinkedList<AvatarStartState>();
+
+ LinkedList<AvatarState> removedinfos = new LinkedList<AvatarState>();
+
for(AvatarStateMachineElement element: elements) {
if ((element instanceof AvatarStartState) && (element.getState() != null)) {
TraceManager.addDev("-> -> found an internal state state");
@@ -300,9 +321,14 @@ public class AvatarStateMachine extends AvatarElement {
TraceManager.addDev("Badly formed state machine");
}
}
+
+ removedinfos.add(as.getState());
+ removedinfos.add(as0);
+
// 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");
@@ -310,6 +336,8 @@ public class AvatarStateMachine extends AvatarElement {
}
}
+ return removedinfos;
+
}
public void removeAllSuperStates() {
diff --git a/src/avatartranslator/AvatarTransition.java b/src/avatartranslator/AvatarTransition.java
index 94897c57e694533b0c93f8b199b857999c460c12..91af544eedd7bf615ad150b2dc1f657ff6ab55de 100644
--- a/src/avatartranslator/AvatarTransition.java
+++ b/src/avatartranslator/AvatarTransition.java
@@ -70,6 +70,10 @@ public class AvatarTransition extends AvatarStateMachineElement {
guard = _guard;
}
+ public void addGuard(String _g) {
+ guard = "(" + guard + ") and (" + _g + ")";
+ }
+
public int getNbOfAction() {
return actions.size();
}
@@ -97,6 +101,9 @@ public class AvatarTransition extends AvatarStateMachineElement {
}
public String getMaxDelay() {
+ if (maxDelay.trim().length() ==0) {
+ return getMinDelay();
+ }
return maxDelay;
}
@@ -105,34 +112,12 @@ public class AvatarTransition extends AvatarStateMachineElement {
}
public String getMaxCompute() {
- return maxCompute;
- }
-
- public String getTotalMinDelay() {
- if (minDelay.trim().length() ==0) {
- return minCompute;
- }
- if (minCompute.trim().length() ==0) {
- return minDelay;
- }
- return "(" + minDelay + ")+(" + minCompute + ")";
- }
-
- public String getTotalMaxDelay() {
- if (maxDelay.trim().length() ==0) {
- if (maxCompute.trim().length() ==0) {
- return getTotalMinDelay();
- }
- return maxCompute;
- }
if (maxCompute.trim().length() ==0) {
- if (maxDelay.trim().length() ==0) {
- return getTotalMinDelay();
- }
- return maxDelay;
+ return getMinCompute();
}
- return "(" + maxDelay + ")+(" + maxCompute + ")";
+ return maxCompute;
}
+
public AvatarTransition cloneMe() {
AvatarTransition at = new AvatarTransition(getName(), getReferenceObject());
@@ -174,6 +159,10 @@ public class AvatarTransition extends AvatarStateMachineElement {
actions.remove(0);
}
+ public void removeAllActions() {
+ actions.clear();
+ }
+
// No actions
//public boolean isAGuardTransition() {
//}
@@ -196,13 +185,20 @@ public class AvatarTransition extends AvatarStateMachineElement {
}
public boolean hasDelay() {
- if ((minDelay.trim().length() == 0) && (minCompute.trim().length() ==0)) {
+ if (minDelay.trim().length() == 0) {
return false;
}
return true;
}
+ public boolean hasCompute() {
+ if (minCompute.trim().length() ==0) {
+ return false;
+ }
+ return true;
+ }
+
public boolean hasActions() {
if (actions.size() == 0) {
return false;
diff --git a/src/avatartranslator/touppaal/AVATAR2UPPAAL.java b/src/avatartranslator/touppaal/AVATAR2UPPAAL.java
index 86314eef58554e66c17b8f7a50d6175fc9fb5bd2..3e730c37aad5857d1bf56d48a3dd207f794d90c9 100755
--- a/src/avatartranslator/touppaal/AVATAR2UPPAAL.java
+++ b/src/avatartranslator/touppaal/AVATAR2UPPAAL.java
@@ -74,8 +74,8 @@ public class AVATAR2UPPAAL {
private Hashtable <AvatarStateMachineElement, UPPAALLocation> hash;
- public final static int STEP_X = 0;
- public final static int STEP_Y = 80;
+ public final static int STEP_X = 5;
+ public final static int STEP_Y = 70;
public final static int STEP_LOOP_X = 150;
public final static int NAME_X = 10;
public final static int NAME_Y = 5;
@@ -141,7 +141,7 @@ public class AVATAR2UPPAAL {
}
/*public RelationTIFUPPAAL getRelationTIFUPPAAL () {
- return table;
+ return table;
}*/
public UPPAALSpec generateUPPAAL(boolean _debug, boolean _optimize) {
@@ -495,6 +495,7 @@ public class AVATAR2UPPAAL {
String tmps, tmps0;
AvatarAttribute aa;
AvatarState state;
+ AvatarRandom arand;
if (_elt == null) {
return;
@@ -510,32 +511,40 @@ public class AVATAR2UPPAAL {
if (_elt instanceof AvatarStartState) {
hash.put(_elt, _previous);
//if (_elt.getNext(0) != null) {
- makeElementBehavior(_block, _template, _elt.getNext(0), _previous, _end, null, false);
+ makeElementBehavior(_block, _template, _elt.getNext(0), _previous, _end, null, false);
//}
return;
-
- // Stop state
+
+ // Stop state
} else if (_elt instanceof AvatarStopState) {
//tr = addRTransition(template, previous, end);
hash.put(_elt, _previous);
return;
+ // Random
+ } else if (_elt instanceof AvatarRandom) {
+ arand = (AvatarRandom)_elt;
+ //tr = addRTransition(template, previous, end);
+ loc = addLocation(_template);
+ tr = addTransition(_template, _previous, loc);
+ setAssignment(tr, arand.getVariable() + "=" + arand.getMinValue());
+ tr = addTransition(_template, loc, loc);
+ setAssignment(tr, arand.getVariable() + "=" + arand.getVariable() + "+1");
+ setGuard(tr, arand.getVariable() + "<" + arand.getMaxValue());
+ _previous.setCommitted();
+ loc.setCommitted();
+ hash.put(_elt, loc);
+ hash.put(_elt, _previous);
+ makeElementBehavior(_block, _template, _elt.getNext(0), loc, _end, null, false);
+ return;
+
- // Avatar Action on Signal
+ // Avatar Action on Signal
} else if (_elt instanceof AvatarActionOnSignal) {
- aaos = (AvatarActionOnSignal)_elt;
- String [] ss = manageSynchro(_block, aaos);
- loc = addLocation(_template);
- hash.put(_elt, loc);
- tr = addTransition(_template, _previous, loc);
- if (_guard != null) {
- addGuard(tr, _guard);
- }
- setSynchronization(tr, ss[0]);
- addAssignment(tr, ss[1]);
+ loc = translateAvatarActionOnSignal((AvatarActionOnSignal)_elt, _block, _template, _previous, _guard);
makeElementBehavior(_block, _template, _elt.getNext(0), loc, _end, null, false);
-
- // Avatar State
+
+ // Avatar State
} else if (_elt instanceof AvatarState) {
if (_elt.nbOfNexts() == 0) {
return;
@@ -546,182 +555,260 @@ public class AVATAR2UPPAAL {
// We translate at the same time the state and its next transitions (guard and time + first method call)
// We assume all nexts are transitions
- // At first, we set variables choice__i to the min delay
- tmps = "h__ = 0";
- j = 0;
+
+ LinkedList<AvatarTransition> transitions = new LinkedList<AvatarTransition>();
for(i=0; i<state.nbOfNexts(); i++) {
at = (AvatarTransition)(state.getNext(i));
if (at.hasDelay()) {
- tmps += ", " + CHOICE_VAR + j + " = max(0 , " + at.getTotalMinDelay() + ")";
- _block.addIntAttributeIfApplicable(CHOICE_VAR + j);
- j ++;
+ transitions.add(at);
}
}
- if (j == 0) {
- tmps = "";
+ if (transitions.size() == 0) {
+ // No transition with a delay
+ for(i=0; i<state.nbOfNexts(); i++) {
+ at = (AvatarTransition)(state.getNext(i));
+ makeElementBehavior(_block, _template, at, _previous, _end, null, false);
+ }
+ } else {
+ // At least one transition with a delay
+ // Reset the clock
+ tmps = "h__ = 0";
+ loc = addLocation(_template);
+ hash.put(_elt, loc);
+ tr = addTransition(_template, _previous, loc);
+ setAssignment(tr, tmps);
+ _previous.setCommitted();
+
+ LinkedList<UPPAALLocation> locs = new LinkedList<UPPAALLocation>();
+ for(i=0; i<state.nbOfNexts(); i++) {
+ at = (AvatarTransition)(state.getNext(i));
+ locs.add(addLocation(_template));
+ }
+
+ LinkedList<UPPAALLocation> builtlocs = new LinkedList<UPPAALLocation>();
+ LinkedList<AvatarStateMachineElement> elements = new LinkedList<AvatarStateMachineElement>();
+
+ makeStateTransitions(state, locs, transitions, loc, _end, _block, _template, builtlocs, elements);
+
+ for(int k=0; k<builtlocs.size(); k++) {
+ makeElementBehavior(_block, _template, elements.get(k), builtlocs.get(k), _end, null, false);
+ }
}
- loc = addLocation(_template);
- loc.setCommitted();
- hash.put(_elt, loc);
- tr = addTransition(_template, _previous, loc);
- setAssignment(tr, tmps);
- _previous.setCommitted();
+ } else if (_elt instanceof AvatarTransition) {
+ at = (AvatarTransition) _elt;
+ loc = translateAvatarTransition(at, _block, _template, _previous, _guard, _previousState);
+ makeElementBehavior(_block, _template, _elt.getNext(0), loc, _end, null, false);
- // Then, random value between min and max delays
- j = 0;
- for(i=0; i<state.nbOfNexts(); i++) {
- at = (AvatarTransition)(state.getNext(i));
- if (at.hasDelay()) {
- tr = addTransition(_template, loc, loc);
- tmps = CHOICE_VAR + j + " = " + CHOICE_VAR + j + " + 1";
- setAssignment(tr, tmps);
- tmps = CHOICE_VAR + j + " < (" + at.getTotalMaxDelay() + ")";
- setGuard(tr, tmps);
- j++;
- }
+ } else {
+ TraceManager.addDev("Reached end of elseif in block behaviour...");
+ return;
+ }
+ }
+
+
+ public UPPAALLocation translateAvatarActionOnSignal(AvatarActionOnSignal _aaos, AvatarBlock _block, UPPAALTemplate _template, UPPAALLocation _previous, String _guard) {
+ String [] ss = manageSynchro(_block, _aaos);
+ UPPAALLocation loc = addLocation(_template);
+ hash.put(_aaos, loc);
+ UPPAALTransition tr = addTransition(_template, _previous, loc);
+ if (_guard != null) {
+ addGuard(tr, _guard);
+ }
+ setSynchronization(tr, ss[0]);
+ addAssignment(tr, ss[1]);
+ return loc;
+ }
+
+ public UPPAALLocation translateAvatarTransition(AvatarTransition _at, AvatarBlock _block, UPPAALTemplate _template, UPPAALLocation _previous, String _guard, boolean _previousState) {
+ UPPAALLocation loc = _previous;
+ UPPAALLocation loc1;
+ UPPAALTransition tr;
+ String tmps;
+ int i;
+
+ if (!_previousState) {
+ if (_at.isGuarded()) {
+ loc1 = addLocation(_template);
+ tr = addTransition(_template, _previous, loc1);
+ tmps = convertGuard(_at.getGuard());
+ setGuard(tr, tmps);
+ loc = loc1;
}
- // Then, wait for delays to elapse ...
- loc1 = addLocation(_template);
- tr = addTransition(_template, loc, loc1);
- j = 0;
- for(i=0; i<state.nbOfNexts(); i++) {
- at = (AvatarTransition)(state.getNext(i));
- if (at.hasDelay()) {
- tr = addTransition(_template, loc1, loc1);
- tmps = CHOICE_VAR + j + " = 0";
+ if (_at.hasDelay()) {
+ loc = makeTimeInterval(_template, loc, _at.getMinDelay(), _at.getMaxDelay());
+ }
+ }
+
+ if (_at.hasCompute()) {
+ loc = makeTimeInterval(_template, loc, _at.getMinCompute(), _at.getMaxCompute());
+ _previousState = false;
+ }
+
+ if (_at.hasActions()) {
+ for(i=0; i<_at.getNbOfAction(); i++) {
+ tmps = _at.getAction(i);
+
+ // Setting a variable
+ if (AvatarSpecification.isAVariableSettingString(tmps)) {
+ loc1 = addLocation(_template);
+ loc.setCommitted();
+ tr = addTransition(_template, loc, loc1);
setAssignment(tr, tmps);
- tmps = "(" + CHOICE_VAR + j + " > 0) && (h__ >" + CHOICE_VAR + j + ")";
- setGuard(tr, tmps);
- j ++;
+ loc = loc1;
+ // Method call
+ } else {
+ TraceManager.addDev("Found method call:" + tmps);
+ loc1 = addLocation(_template);
+ tr = addTransition(_template, loc, loc1);
+
+ if ((i ==0) && (_previousState)) {
+ setGuard(tr, _guard);
+ } else {
+ loc.setUrgent();
+ }
+ setSynchronization(tr, AvatarSpecification.getMethodCallFromAction(tmps) + "!");
+ makeMethodCall(_block, tr, tmps);
+ loc = loc1;
}
}
+ }
+ hash.put(_at, loc);
+ return loc;
+ }
+
+ // Start from a given state / loc, and derive progressively all locations
+ // _transitions contains timing transitions
+ public void makeStateTransitions(AvatarState _state, LinkedList<UPPAALLocation> _locs, LinkedList<AvatarTransition> _transitions, UPPAALLocation _loc, UPPAALLocation _end, AvatarBlock _block, UPPAALTemplate _template, LinkedList<UPPAALLocation> _builtlocs, LinkedList<AvatarStateMachineElement> _elements) {
+ // Make the current state
+ // Invariant
+ String inv = "";
+ int cpt = 0;
+ int i;
+ UPPAALLocation loc1;
+ String tmps, tmps0;
+ AvatarTransition at;
+ UPPAALLocation loc;
+ UPPAALTransition tr;
+
+
+ for(AvatarTransition att: _transitions) {
+ if (cpt == 0) {
+ inv += "h__ <= " + att.getMaxDelay();
+ } else {
+ inv = "(" + inv + ") && (h__ <= " +att.getMaxDelay() + ")";
+ }
+ cpt ++;
+ }
+
+ _loc.setInvariant(inv);
+
+ // Put all logical transitions
+ // Choice between transitions
+ // If the first action is a method call, or not action but the next one is an action on a signal:
+ // Usual translation way i.e. use the action as the UPPAAL transition trigger
+ // Otherwise introduce a fake choice action
+ //j = 0;
+ UPPAALLocation locend;
+ for(i=0; i<_state.nbOfNexts(); i++) {
+ at = (AvatarTransition)(_state.getNext(i));
+ locend = _locs.get(i);
- // Choice between transitions
- // If the first action is a method call, or not action but the next one is an action on a signal:
- // Usual translation way i.e. use the action as the UPPAAL transition trigger
- // Otherwise introduce a fake choice action
- j = 0;
- for(i=0; i<state.nbOfNexts(); i++) {
- at = (AvatarTransition)(state.getNext(i));
+ if (!(_transitions.contains(at))) {
// Computing guard
if (at.isGuarded()) {
tmps = convertGuard(at.getGuard());
- if (at.hasDelay()) {
- tmps = "(" + tmps + ") && (" + CHOICE_VAR + j + " == 0)";
- j ++;
- }
} else {
- if (at.hasDelay()) {
- tmps = CHOICE_VAR + j + " == 0";
- j ++;
- } else {
- tmps = "";
- }
+ tmps = "";
}
- if (at.hasActions()) {
+ if (at.hasCompute()) {
+ tr = addTransition(_template, _loc, locend);
+ setGuard(tr, tmps);
+ setSynchronization(tr, CHOICE_ACTION + "!");
+ if (_template.nbOfTransitionsExitingFrom(locend) == 0) {
+ loc1 = translateAvatarTransition(at, _block, _template, locend, "", true);
+ _builtlocs.add(loc1);
+ _elements.add(at.getNext(0));
+ }
+
+ } else if (at.hasActions()) {
tmps0 = at.getAction(0);
if (AvatarSpecification.isAVariableSettingString(tmps0)) {
// We must introduce a fake action
- loc = addLocation(_template);
- tr = addTransition(_template, loc1, loc);
- setGuard(tr, tmps);
+ tr = addTransition(_template, _loc, locend);
+ if (tmps != null) {
+ setGuard(tr, tmps);
+ }
setSynchronization(tr, CHOICE_ACTION + "!");
- makeElementBehavior(_block, _template, _elt.getNext(i), loc, _end, null, true);
+ if (_template.nbOfTransitionsExitingFrom(locend) == 0) {
+ loc1 = translateAvatarTransition(at, _block, _template, locend, "", true);
+ _builtlocs.add(loc1);
+ _elements.add(at.getNext(0));
+ }
+
} else {
// We make the translation in the next transition
- makeElementBehavior(_block, _template, _elt.getNext(i), loc1, _end, tmps, true);
+ loc1 = translateAvatarTransition(at, _block, _template, _loc, "", true);
+ tr = addTransition(_template, loc1, locend);
+ loc1.setCommitted();
+ if (!(_elements.contains(at.getNext(0)))) {
+ _builtlocs.add(locend);
+ _elements.add(at.getNext(0));
+ }
}
} else {
// Must consider whether the transition leads to an action on a signal
if (at.followedWithAnActionOnASignal()) {
- makeElementBehavior(_block, _template, at.getNext(0), loc1, _end, tmps, true);
+ loc1 = translateAvatarActionOnSignal((AvatarActionOnSignal)(at.getNext(0)), _block, _template, _loc, "");
+ tr = addTransition(_template, loc1, locend);
+ loc1.setCommitted();
+ if (!(_elements.contains(at.getNext(0).getNext(0)))) {
+ _builtlocs.add(locend);
+ _elements.add(at.getNext(0).getNext(0));
+ }
} else {
// If this is not the only transition
// We must introduce a fake action
- if (state.nbOfNexts() > 1) {
- loc = addLocation(_template);
- tr = addTransition(_template, loc1, loc);
- setGuard(tr, tmps);
- setSynchronization(tr, CHOICE_ACTION + "!");
- // Useless to translate the next transition, we directly jump to after the transition
- makeElementBehavior(_block, _template, at.getNext(0), loc, _end, null, true);
- } else {
- // Only one transition
- if (tmps.length() > 0) {
- loc = addLocation(_template);
- tr = addTransition(_template, loc1, loc);
- setGuard(tr, tmps);
- makeElementBehavior(_block, _template, at.getNext(0), loc, _end, null, true);
- } else {
- makeElementBehavior(_block, _template, at.getNext(0), loc1, _end, null, true);
- }
- }
- }
- }
- }
-
-
- // Avatar Transition not following a state -> only the next one one transitions:
- // So, translated at it is
- } else if (_elt instanceof AvatarTransition) {
- at = (AvatarTransition) _elt;
- loc = _previous;
- if (!_previousState) {
- if (at.isGuarded()) {
- loc1 = addLocation(_template);
- tr = addTransition(_template, _previous, loc1);
- tmps = convertGuard(at.getGuard());
- setGuard(tr, tmps);
- loc = loc1;
- }
-
- if (at.hasDelay()) {
- loc = makeTimeInterval(_template, loc, at.getTotalMinDelay(), at.getTotalMaxDelay());
- }
- }
-
- if (at.hasActions()) {
- for(i=0; i<at.getNbOfAction(); i++) {
- tmps = at.getAction(i);
-
- // Setting a variable
- if (AvatarSpecification.isAVariableSettingString(tmps)) {
- loc1 = addLocation(_template);
- loc.setCommitted();
- tr = addTransition(_template, loc, loc1);
- setAssignment(tr, tmps);
- loc = loc1;
- // Method call
- } else {
-
- loc1 = addLocation(_template);
- tr = addTransition(_template, loc, loc1);
-
- if ((i ==0) && (_previousState)) {
- setGuard(tr, _guard);
- } else {
- loc.setUrgent();
+ tr = addTransition(_template, _loc, locend);
+ setGuard(tr, tmps);
+ setSynchronization(tr, CHOICE_ACTION + "!");
+ // Useless to translate the next transition, we directly jump to after the transition
+ if (!(_elements.contains(at.getNext(0)))) {
+ _builtlocs.add(locend);
+ _elements.add(at.getNext(0));
}
- setSynchronization(tr, AvatarSpecification.getMethodCallFromAction(tmps) + "!");
- makeMethodCall(_block, tr, tmps);
- loc = loc1;
}
}
}
- hash.put(_elt, loc);
- makeElementBehavior(_block, _template, _elt.getNext(0), loc, _end, null, false);
+ }
- } else {
- TraceManager.addDev("Reached end of elseif in block behaviour...");
+
+ // Make the nexts transitions / put all timing transitions
+ // Consider all possibilities
+
+ if (_transitions.size() == 0) {
return;
}
+ LinkedList<AvatarTransition> cloneList;
+
+ for(i=0; i<_transitions.size(); i++) {
+ cloneList = new LinkedList<AvatarTransition>();
+ cloneList.addAll(_transitions);
+ cloneList.remove(i);
+ currentX = currentX + STEP_LOOP_X;
+ loc1 = addLocation(_template);
+ tr = addTransition(_template, _loc, loc1);
+ addGuard(tr, "h__ >= " + _transitions.get(i).getMinDelay());
+ makeStateTransitions(_state, _locs, cloneList, loc1, _end, _block, _template, _builtlocs, _elements);
+ currentX = currentX - STEP_LOOP_X;
+ }
+
}
@@ -804,9 +891,9 @@ public class AVATAR2UPPAAL {
/*if (avspec.isASynchronousSignal(as)) {
-
+
} else {
- return manageSynchroAsynchronous(_block, _aaos);
+ return manageSynchroAsynchronous(_block, _aaos);
}*/
}
@@ -865,7 +952,7 @@ public class AVATAR2UPPAAL {
TraceManager.addDev("Null param:" + _aaos.getValue(i));
}
}
-
+
nbOfIntParameters = Math.max(nbOfIntParameters, nbOfInt);
nbOfBooleanParameters = Math.max(nbOfBooleanParameters, nbOfBool);
@@ -922,7 +1009,7 @@ public class AVATAR2UPPAAL {
}
}
}
-
+
nbOfIntParameters = Math.max(nbOfIntParameters, nbOfInt);
nbOfBooleanParameters = Math.max(nbOfBooleanParameters, nbOfBool);
@@ -1098,4 +1185,131 @@ public class AVATAR2UPPAAL {
}
+ // At first, we set variables choice__i to the min delay
+ /*tmps = "h__ = 0";
+ j = 0;
+ for(i=0; i<state.nbOfNexts(); i++) {
+ at = (AvatarTransition)(state.getNext(i));
+ if (at.hasDelay()) {
+ tmps += ", " + CHOICE_VAR + j + " = max(0 , " + at.getMinDelay() + ")";
+ _block.addIntAttributeIfApplicable(CHOICE_VAR + j);
+ j ++;
+ }
+ }
+
+ if (j == 0) {
+ tmps = "";
+ }
+
+
+ loc = addLocation(_template);
+ loc.setCommitted();
+ hash.put(_elt, loc);
+ tr = addTransition(_template, _previous, loc);
+ setAssignment(tr, tmps);
+ _previous.setCommitted();
+
+ // Then, random value between min and max delays
+ j = 0;
+ for(i=0; i<state.nbOfNexts(); i++) {
+ at = (AvatarTransition)(state.getNext(i));
+ if (at.hasDelay()) {
+ tr = addTransition(_template, loc, loc);
+ tmps = CHOICE_VAR + j + " = " + CHOICE_VAR + j + " + 1";
+ setAssignment(tr, tmps);
+ tmps = CHOICE_VAR + j + " < (" + at.getMaxDelay() + ")";
+ setGuard(tr, tmps);
+ j++;
+ }
+ }
+
+ // Then, wait for delays to elapse ...
+ loc1 = addLocation(_template);
+ tr = addTransition(_template, loc, loc1);
+ j = 0;
+ for(i=0; i<state.nbOfNexts(); i++) {
+ at = (AvatarTransition)(state.getNext(i));
+ if (at.hasDelay()) {
+ tr = addTransition(_template, loc1, loc1);
+ tmps = CHOICE_VAR + j + " = 0";
+ setAssignment(tr, tmps);
+ tmps = "(" + CHOICE_VAR + j + " > 0) && (h__ >" + CHOICE_VAR + j + ")";
+ setGuard(tr, tmps);
+ j ++;
+ }
+ }
+
+ // Choice between transitions
+ // If the first action is a method call, or not action but the next one is an action on a signal:
+ // Usual translation way i.e. use the action as the UPPAAL transition trigger
+ // Otherwise introduce a fake choice action
+ j = 0;
+ for(i=0; i<state.nbOfNexts(); i++) {
+ at = (AvatarTransition)(state.getNext(i));
+
+ // Computing guard
+ if (at.isGuarded()) {
+ tmps = convertGuard(at.getGuard());
+ if (at.hasDelay()) {
+ tmps = "(" + tmps + ") && (" + CHOICE_VAR + j + " == 0)";
+ j ++;
+ }
+ } else {
+ if (at.hasDelay()) {
+ tmps = CHOICE_VAR + j + " == 0";
+ j ++;
+ } else {
+ tmps = "";
+ }
+ }
+
+ if (at.hasCompute()) {
+ loc = addLocation(_template);
+ tr = addTransition(_template, loc1, loc);
+ setSynchronization(tr, CHOICE_ACTION + "!");
+ makeElementBehavior(_block, _template, _elt.getNext(i), loc, _end, null, true);
+ } else if (at.hasActions()) {
+ tmps0 = at.getAction(0);
+ if (AvatarSpecification.isAVariableSettingString(tmps0)) {
+ // We must introduce a fake action
+ loc = addLocation(_template);
+ tr = addTransition(_template, loc1, loc);
+ if (tmps != null) {
+ setGuard(tr, tmps);
+ }
+ setSynchronization(tr, CHOICE_ACTION + "!");
+ makeElementBehavior(_block, _template, _elt.getNext(i), loc, _end, null, true);
+ } else {
+ // We make the translation in the next transition
+ makeElementBehavior(_block, _template, _elt.getNext(i), loc1, _end, tmps, true);
+ }
+ } else {
+ // Must consider whether the transition leads to an action on a signal
+ if (at.followedWithAnActionOnASignal()) {
+ makeElementBehavior(_block, _template, at.getNext(0), loc1, _end, tmps, true);
+ } else {
+ // If this is not the only transition
+ // We must introduce a fake action
+ if (state.nbOfNexts() > 1) {
+ loc = addLocation(_template);
+ tr = addTransition(_template, loc1, loc);
+ setGuard(tr, tmps);
+ setSynchronization(tr, CHOICE_ACTION + "!");
+ // Useless to translate the next transition, we directly jump to after the transition
+ makeElementBehavior(_block, _template, at.getNext(0), loc, _end, null, true);
+ } else {
+ // Only one transition
+ if (tmps.length() > 0) {
+ loc = addLocation(_template);
+ tr = addTransition(_template, loc1, loc);
+ setGuard(tr, tmps);
+ makeElementBehavior(_block, _template, at.getNext(0), loc, _end, null, true);
+ } else {
+ makeElementBehavior(_block, _template, at.getNext(0), loc1, _end, null, true);
+ }
+ }
+ }
+ }
+ }*/
+
}
\ No newline at end of file
diff --git a/src/ui/AvatarDesignPanelTranslator.java b/src/ui/AvatarDesignPanelTranslator.java
index 06adb3b3a065bf9fcfe2bd179acde784ac29d376..fafcc7f0281cb32471bf8c08b06209937832a0d4 100644
--- a/src/ui/AvatarDesignPanelTranslator.java
+++ b/src/ui/AvatarDesignPanelTranslator.java
@@ -346,6 +346,7 @@ public class AvatarDesignPanelTranslator {
iterator = asmdp.getAllComponentList().listIterator();
AvatarSMDReceiveSignal asmdrs;
AvatarSMDSendSignal asmdss;
+ AvatarSMDRandom asmdrand;
AvatarStateMachine asm = _ab.getStateMachine();
avatartranslator.AvatarSignal atas;
@@ -354,11 +355,14 @@ public class AvatarDesignPanelTranslator {
AvatarStopState astop;
AvatarStartState astart;
AvatarState astate;
+ AvatarRandom arandom;
int i;
String tmp;
TAttribute ta;
int choiceID = 0;
+ int error;
+ String tmp1, tmp2;
while(iterator.hasNext()) {
tgc = (TGComponent)(iterator.next());
@@ -493,6 +497,34 @@ public class AvatarDesignPanelTranslator {
choiceID ++;
asm.addElement(astate);
listE.addCor(astate, tgc);
+
+ // Random
+ } else if (tgc instanceof AvatarSMDRandom) {
+ asmdrand = (AvatarSMDRandom)tgc;
+ arandom = new AvatarRandom("random", tgc);
+ tmp1 = modifyString(asmdrand.getMinValue());
+ error = AvatarSyntaxChecker.isAValidIntExpr(_as, _ab, tmp1);
+ if (error < 0) {
+ makeError(error, tdp, _ab, tgc, "min value of random", tmp1);
+ }
+ tmp2 = modifyString(asmdrand.getMaxValue());
+ error = AvatarSyntaxChecker.isAValidIntExpr(_as, _ab, tmp1);
+ if (error < 0) {
+ makeError(error, tdp, _ab, tgc, "max value of random", tmp2);
+ }
+ arandom.setValues(tmp1, tmp2);
+ arandom.setFunctionId(asmdrand.getFunctionId());
+
+ tmp1 = modifyString(asmdrand.getVariable());
+ aa = _ab.getAvatarAttributeWithName(tmp1);
+
+ if (aa == null) {
+ makeError(error, tdp, _ab, tgc, "variable of random", tmp2);
+ }
+ arandom.setVariable(tmp1);
+
+ asm.addElement(arandom);
+ listE.addCor(arandom, tgc);
// Start state
} else if (tgc instanceof AvatarSMDStartState) {
@@ -537,8 +569,6 @@ public class AvatarDesignPanelTranslator {
AvatarSMDConnector asmdco;
AvatarTransition at;
TGComponent tgc1, tgc2;
- int error;
- String tmp1, tmp2;
Vector <String> vs;
while(iterator.hasNext()) {
diff --git a/src/ui/MainGUI.java b/src/ui/MainGUI.java
index a01602949782c525af70fb23d12ae90d75d060ec..47283b059cf24efd51c678c9d6f3fbb16f782ba7 100755
--- a/src/ui/MainGUI.java
+++ b/src/ui/MainGUI.java
@@ -6083,6 +6083,8 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener {
actionOnButton(TGComponentManager.COMPONENT, TGComponentManager.AVATARSMD_STATE);
} else if (command.equals(actions[TGUIAction.ASMD_CHOICE].getActionCommand())) {
actionOnButton(TGComponentManager.COMPONENT, TGComponentManager.AVATARSMD_CHOICE);
+ } else if (command.equals(actions[TGUIAction.ASMD_RANDOM].getActionCommand())) {
+ actionOnButton(TGComponentManager.COMPONENT, TGComponentManager.AVATARSMD_RANDOM);
// AVATAR RD
} else if (command.equals(actions[TGUIAction.ARD_EDIT].getActionCommand())) {
diff --git a/src/ui/TGComponentManager.java b/src/ui/TGComponentManager.java
index 9f285a45972b8972361cb932770ba9d3676cd2c2..603963bdad6c04c2bafd85b508989a0f5d9edb86 100755
--- a/src/ui/TGComponentManager.java
+++ b/src/ui/TGComponentManager.java
@@ -302,6 +302,7 @@ public class TGComponentManager {
public static final int AVATARSMD_PARALLEL = 5105;
public static final int AVATARSMD_STATE = 5106;
public static final int AVATARSMD_CHOICE = 5107;
+ public static final int AVATARSMD_RANDOM = 5108;
// AVATAR RD -> starts at 5200
public static final int AVATARRD_REQUIREMENT = 5200;
@@ -362,6 +363,9 @@ public class TGComponentManager {
break;
case AVATARSMD_CHOICE:
tgc = new AvatarSMDChoice(x, y, tdp.getMinX(), tdp.getMaxX(), tdp.getMinY(), tdp.getMaxY(), false, null, tdp);
+ break;
+ case AVATARSMD_RANDOM:
+ tgc = new AvatarSMDRandom(x, y, tdp.getMinX(), tdp.getMaxX(), tdp.getMinY(), tdp.getMaxY(), false, null, tdp);
break;
case AVATARRD_REQUIREMENT:
tgc = new AvatarRDRequirement(x, y, tdp.getMinX(), tdp.getMaxX(), tdp.getMinY(), tdp.getMaxY(), false, null, tdp);
@@ -841,7 +845,9 @@ public class TGComponentManager {
} else if (tgc instanceof AvatarSMDState) {
return AVATARSMD_STATE;
} else if (tgc instanceof AvatarSMDChoice) {
- return AVATARSMD_CHOICE;
+ return AVATARSMD_CHOICE;
+ } else if (tgc instanceof AvatarSMDRandom) {
+ return AVATARSMD_RANDOM;
// AVATAR RD
} else if (tgc instanceof AvatarRDRequirement) {
diff --git a/src/ui/TGUIAction.java b/src/ui/TGUIAction.java
index 70edeaed4aa04508f52974141bdc0cacb1d839cc..17e3c788e90d7455329913c0462ad86ac00127e2 100755
--- a/src/ui/TGUIAction.java
+++ b/src/ui/TGUIAction.java
@@ -311,6 +311,7 @@ public class TGUIAction extends AbstractAction {
public static final int ASMD_PARALLEL = 298;
public static final int ASMD_STATE = 299;
public static final int ASMD_CHOICE = 325;
+ public static final int ASMD_RANDOM = 326;
// AVATAR Requirement
public static final int ARD_EDIT = 300;
@@ -445,7 +446,7 @@ public class TGUIAction extends AbstractAction {
//Action for the help button created by Solange
public static final int PRUEBA_1 = 205;
- public static final int NB_ACTION = 326;
+ public static final int NB_ACTION = 327;
private static final TAction [] actions = new TAction[NB_ACTION];
@@ -842,6 +843,8 @@ public class TGUIAction extends AbstractAction {
actions[ASMD_PARALLEL] = new TAction("add-asmd-parallel", "Parallel", IconManager.imgic206, IconManager.imgic206, "Parallel", "Add a parallel operator to the currently opened AVATAR state machine diagram", 0);
actions[ASMD_STATE] = new TAction("add-asmd-state", "State", IconManager.imgic5036, IconManager.imgic5036, "State", "Add a new state to the currently opened AVATAR state machine diagram", 0);
actions[ASMD_CHOICE] = new TAction("add-asmd-choice", "Add Choice", IconManager.imgic208, IconManager.imgic208, "Choice", "Add a choice - non-deterministic or guarded - to the currently opened AVATAR state machine diagram", 0);
+ actions[ASMD_RANDOM] = new TAction("add-asmd-random", "Add random", IconManager.imgic924, IconManager.imgic924, "Select random", "Add a random operator to the currently opened AVATAR State Machine diagram", 0);
+
// AVATAR Requirement Diagrams
actions[ARD_EDIT] = new TAction("edit-ard-diagram", "Edit AVATAR Requirement Diagram", IconManager.imgic100, IconManager.imgic101, "Edit AVATAR Requirement Diagram", "Make it possible to edit the currently opened AVATAR requirement diagram", 0);
diff --git a/src/ui/avatarsmd/AvatarSMDRandom.java b/src/ui/avatarsmd/AvatarSMDRandom.java
new file mode 100755
index 0000000000000000000000000000000000000000..d1a9c799debe0ddc99c1a880ccc1e9211d3e825f
--- /dev/null
+++ b/src/ui/avatarsmd/AvatarSMDRandom.java
@@ -0,0 +1,294 @@
+/**Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
+ *
+ * ludovic.apvrille AT enst.fr
+ *
+ * This software is a computer program whose purpose is to allow the
+ * edition of TURTLE analysis, design and deployment diagrams, to
+ * allow the generation of RT-LOTOS or Java code from this diagram,
+ * and at last to allow the analysis of formal validation traces
+ * obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
+ * from INRIA Rhone-Alpes.
+ *
+ * This software is governed by the CeCILL license under French law and
+ * abiding by the rules of distribution of free software. You can use,
+ * modify and/ or redistribute the software under the terms of the CeCILL
+ * license as circulated by CEA, CNRS and INRIA at the following URL
+ * "http://www.cecill.info".
+ *
+ * As a counterpart to the access to the source code and rights to copy,
+ * modify and redistribute granted by the license, users are provided only
+ * with a limited warranty and the software's author, the holder of the
+ * economic rights, and the successive licensors have only limited
+ * liability.
+ *
+ * In this respect, the user's attention is drawn to the risks associated
+ * with loading, using, modifying and/or developing or reproducing the
+ * software by the user in light of its specific status of free software,
+ * that may mean that it is complicated to manipulate, and that also
+ * therefore means that it is reserved for developers and experienced
+ * professionals having in-depth computer knowledge. Users are therefore
+ * encouraged to load and test the software's suitability as regards their
+ * requirements in conditions enabling the security of their systems and/or
+ * data to be ensured and, more generally, to use and operate it in the
+ * same conditions as regards security.
+ *
+ * The fact that you are presently reading this means that you have had
+ * knowledge of the CeCILL license and that you accept its terms.
+ *
+ * /**
+ * Class AvatarSMDRandom
+ * Random operator of an AVATAR State Machine diagram
+ * Creation: 12/07/2010
+ * @version 1.0 12/07/2010
+ * @author Ludovic APVRILLE
+ * @see
+ */
+
+package ui.avatarsmd;
+
+import java.awt.*;
+import java.awt.geom.*;
+import javax.swing.*;
+
+import org.w3c.dom.*;
+
+import myutil.*;
+import ui.*;
+import ui.window.*;
+
+public class AvatarSMDRandom extends AvatarSMDBasicComponent implements EmbeddedComment, BasicErrorHighlight {
+ protected int lineLength = 5;
+ protected int textX = 5;
+ protected int textY = 15;
+ protected int arc = 5;
+ protected String valueRandom = "";
+ protected String variable;
+ protected String minValue;
+ protected String maxValue;
+ protected int functionId;
+
+ protected int stateOfError = 0; // Not yet checked
+
+ public AvatarSMDRandom(int _x, int _y, int _minX, int _maxX, int _minY, int _maxY, boolean _pos, TGComponent _father, TDiagramPanel _tdp) {
+ super(_x, _y, _minX, _maxX, _minY, _maxY, _pos, _father, _tdp);
+
+ width = 30;
+ height = 20;
+ minWidth = 30;
+
+ nbConnectingPoint = 2;
+ connectingPoint = new TGConnectingPoint[2];
+ connectingPoint[0] = new AvatarSMDConnectingPoint(this, 0, -lineLength, true, false, 0.5, 0.0);
+ connectingPoint[1] = new AvatarSMDConnectingPoint(this, 0, lineLength, false, true, 0.5, 1.0);
+
+ moveable = true;
+ editable = true;
+ removable = true;
+
+ variable = "x";
+ minValue = "0";
+ maxValue = "10";
+ functionId = 0;
+
+ myImageIcon = IconManager.imgic912;
+ }
+
+ public void makeValue() {
+ valueRandom = variable + " = RANDOM" + functionId + "[" + minValue + ", " + maxValue + "]";
+ }
+
+ public void internalDrawing(Graphics g) {
+
+ if (valueRandom.length() == 0) {
+ makeValue();
+ }
+
+ int w = g.getFontMetrics().stringWidth(valueRandom);
+ int w1 = Math.max(minWidth, w + 2 * textX);
+ if ((w1 != width) & (!tdp.isScaled())) {
+ setCd(x + width/2 - w1/2, y);
+ width = w1;
+ //updateConnectingPoints();
+ }
+
+ if (stateOfError > 0) {
+ Color c = g.getColor();
+ switch(stateOfError) {
+ case ErrorHighlight.OK:
+ g.setColor(ColorManager.RANDOM);
+ break;
+ default:
+ g.setColor(ColorManager.UNKNOWN_BOX_ACTION);
+ }
+ g.fillRoundRect(x, y, width, height, arc, arc);
+ g.setColor(c);
+ }
+
+ g.drawRoundRect(x, y, width, height, arc, arc);
+ g.drawLine(x+(width/2), y, x+(width/2), y - lineLength);
+ g.drawLine(x+(width/2), y+height, x+(width/2), y + lineLength + height);
+ //g.drawLine(x+width, y+height/2, x+width +lineLength, y+height/2);
+
+ g.drawString(valueRandom, x + (width - w) / 2 , y + textY);
+ }
+
+ public boolean editOndoubleClick(JFrame frame) {
+ boolean error = false;
+ String errors = "";
+ int tmp;
+ String tmpName;
+
+ JDialogTMLADRandom dialog = new JDialogTMLADRandom(frame, "Setting RANDOM attributes", getVariable(), getMinValue(), getMaxValue(), getFunctionId());
+ dialog.setSize(500, 450);
+ GraphicLib.centerOnParent(dialog);
+ dialog.show(); // blocked until dialog has been closed
+
+ if (!dialog.isRegularClose()) {
+ return false;
+ }
+
+ if (dialog.getVariable().length() != 0) {
+ tmpName = dialog.getVariable();
+ tmpName = tmpName.trim();
+ if (!TAttribute.isAValidId(tmpName, false, false)) {
+ error = true;
+ errors += "Variable ";
+ } else {
+ variable = tmpName;
+ }
+ }
+
+ if (dialog.getMinValue().length() != 0) {
+ minValue = dialog.getMinValue();
+ } else {
+ error = true;
+ errors += "Min value ";
+ }
+
+ if (dialog.getMaxValue().length() != 0) {
+ maxValue = dialog.getMaxValue();
+ } else {
+ error = true;
+ errors += "Max value ";
+ }
+
+ functionId = dialog.getFunctionId();
+
+ if (error) {
+ JOptionPane.showMessageDialog(frame,
+ "Invalid value for the following attributes: " + errors,
+ "Error",
+ JOptionPane.INFORMATION_MESSAGE);
+ return false;
+ }
+
+ makeValue();
+
+ return true;
+ }
+
+ public TGComponent isOnMe(int _x, int _y) {
+ if (GraphicLib.isInRectangle(_x, _y, x, y, width, height)) {
+ return this;
+ }
+
+ if ((int)(Line2D.ptSegDistSq(x+(width/2), y-lineLength, x+(width/2), y + lineLength + height, _x, _y)) < distanceSelected) {
+ return this;
+ }
+
+ if ((int)(Line2D.ptSegDistSq(x+width, y+height/2, x+width +lineLength, y+height/2, _x, _y)) < distanceSelected) {
+ return this;
+ }
+
+ return null;
+ }
+
+ public String getVariable() {
+ return variable;
+ }
+
+ public String getMinValue() {
+ return minValue;
+ }
+
+ public String getMaxValue() {
+ return maxValue;
+ }
+
+ public int getFunctionId() {
+ return functionId;
+ }
+
+ protected String translateExtraParam() {
+ StringBuffer sb = new StringBuffer("<extraparam>\n");
+ sb.append("<Data variable=\"");
+ sb.append(getVariable());
+ sb.append("\" minValue=\"");
+ sb.append(getMinValue());
+ sb.append("\" maxValue=\"");
+ sb.append(getMaxValue());
+ sb.append("\" functionId=\"");
+ sb.append(getFunctionId());
+ sb.append("\" />\n");
+ sb.append("</extraparam>\n");
+ return new String(sb);
+ }
+
+ public void loadExtraParam(NodeList nl, int decX, int decY, int decId) throws MalformedModelingException{
+ //System.out.println("*** load extra synchro *** " + getId());
+ try {
+
+ NodeList nli;
+ Node n1, n2;
+ Element elt;
+ int k;
+ String s;
+
+ //System.out.println("Loading Synchronization gates");
+ //System.out.println(nl.toString());
+
+ for(int i=0; i<nl.getLength(); i++) {
+ n1 = nl.item(i);
+ //System.out.println(n1);
+ if (n1.getNodeType() == Node.ELEMENT_NODE) {
+ nli = n1.getChildNodes();
+ for(int j=0; i<nli.getLength(); i++) {
+ n2 = nli.item(i);
+ //System.out.println(n2);
+ if (n2.getNodeType() == Node.ELEMENT_NODE) {
+ elt = (Element) n2;
+ if (elt.getTagName().equals("Data")) {
+ variable = elt.getAttribute("variable");
+ minValue = elt.getAttribute("minValue");
+ maxValue = elt.getAttribute("maxValue");
+ s = elt.getAttribute("functionId");
+ if (s != null) {
+ try {
+ functionId = new Integer(s).intValue();
+ } catch (Exception e){
+ }
+ }
+ //System.out.println("eventName=" +eventName + " variable=" + result);
+ }
+ }
+ }
+ }
+ }
+
+ } catch (Exception e) {
+ throw new MalformedModelingException();
+ }
+ makeValue();
+ }
+
+
+ public int getType() {
+ return TGComponentManager.AVATARSMD_RANDOM;
+ }
+
+ public void setStateAction(int _stateAction) {
+ stateOfError = _stateAction;
+ }
+
+
+}
diff --git a/src/ui/avatarsmd/AvatarSMDToolBar.java b/src/ui/avatarsmd/AvatarSMDToolBar.java
index a5700d13f29437d5bb5452a09be2e5b942bbb6de..6ba6d840b5d0381adbaba0c0823794fbd3f3048e 100755
--- a/src/ui/avatarsmd/AvatarSMDToolBar.java
+++ b/src/ui/avatarsmd/AvatarSMDToolBar.java
@@ -72,6 +72,7 @@ public class AvatarSMDToolBar extends TToolBar {
mgui.actions[TGUIAction.ASMD_PARALLEL].setEnabled(b);
mgui.actions[TGUIAction.ASMD_STATE].setEnabled(b);
mgui.actions[TGUIAction.ASMD_CHOICE].setEnabled(b);
+ mgui.actions[TGUIAction.ASMD_RANDOM].setEnabled(b);
mgui.actions[TGUIAction.ACT_ENHANCE].setEnabled(b);
@@ -120,6 +121,11 @@ public class AvatarSMDToolBar extends TToolBar {
button = this.add(mgui.actions[TGUIAction.ASMD_CHOICE]);
button.addMouseListener(mgui.mouseHandler);
+ this.addSeparator();
+
+ button = this.add(mgui.actions[TGUIAction.ASMD_RANDOM]);
+ button.addMouseListener(mgui.mouseHandler);
+
/*this.addSeparator();
button = this.add(mgui.actions[TGUIAction.ASMD_PARALLEL]);
diff --git a/src/ui/tmlad/TMLADRandom.java b/src/ui/tmlad/TMLADRandom.java
index 50180d00b2fd78fd99acd7c23fafa44bf1d21b57..7357257bc0bd14a0978725bc410b5f2cc2481509 100755
--- a/src/ui/tmlad/TMLADRandom.java
+++ b/src/ui/tmlad/TMLADRandom.java
@@ -138,7 +138,7 @@ public class TMLADRandom extends TGCWithoutInternalComponent implements Embedded
int tmp;
String tmpName;
- JDialogTMLADRandom dialog = new JDialogTMLADRandom(frame, "Setting RANDOM attributes", this);
+ JDialogTMLADRandom dialog = new JDialogTMLADRandom(frame, "Setting RANDOM attributes", getVariable(), getMinValue(), getMaxValue(), getFunctionId());
dialog.setSize(500, 450);
GraphicLib.centerOnParent(dialog);
dialog.show(); // blocked until dialog has been closed
diff --git a/src/ui/window/JDialogTMLADRandom.java b/src/ui/window/JDialogTMLADRandom.java
index 9ee8f46ab54f805ff5a1ada5b5db719c8fdee21b..c44ef2d3c88862beac6ade3467c4c3afde9ceb8f 100755
--- a/src/ui/window/JDialogTMLADRandom.java
+++ b/src/ui/window/JDialogTMLADRandom.java
@@ -63,11 +63,12 @@ public class JDialogTMLADRandom extends javax.swing.JDialog implements ActionLis
private JPanel panel2;
private Frame frame;
- private TMLADRandom random;
+ private String variable, minValue, maxValue;
+ private int functionId;
// Panel2
- protected JTextField variable, minValue, maxValue;
+ protected JTextField jvariable, jminValue, jmaxValue;
protected JComboBox randomFunction;
// Main Panel
@@ -75,10 +76,13 @@ public class JDialogTMLADRandom extends javax.swing.JDialog implements ActionLis
private JButton cancelButton;
/** Creates new form */
- public JDialogTMLADRandom(Frame _frame, String _title, TMLADRandom _random) {
+ public JDialogTMLADRandom(Frame _frame, String _title, String _variable, String _minValue, String _maxValue, int _functionId) {
super(_frame, _title, true);
frame = _frame;
- random = _random;
+ variable = _variable;
+ minValue = _minValue;
+ maxValue = _maxValue;
+ functionId = _functionId;
initComponents();
myInitComponents();
@@ -115,33 +119,33 @@ public class JDialogTMLADRandom extends javax.swing.JDialog implements ActionLis
c2.fill = GridBagConstraints.HORIZONTAL;
panel2.add(new JLabel("Variable name:"), c2);
c2.gridwidth = GridBagConstraints.REMAINDER; //end row
- variable = new JTextField(random.getVariable(), 30);
- variable.setEditable(true);
- variable.setFont(new Font("times", Font.PLAIN, 12));
- panel2.add(variable, c2);
+ jvariable = new JTextField(variable, 30);
+ jvariable.setEditable(true);
+ jvariable.setFont(new Font("times", Font.PLAIN, 12));
+ panel2.add(jvariable, c2);
c2.gridwidth = 1;
panel2.add(new JLabel("Minimum value:"), c2);
c2.gridwidth = GridBagConstraints.REMAINDER; //end row
- minValue = new JTextField(random.getMinValue(), 30);
- minValue.setEditable(true);
- minValue.setFont(new Font("times", Font.PLAIN, 12));
- panel2.add(minValue, c2);
+ jminValue = new JTextField(minValue, 30);
+ jminValue.setEditable(true);
+ jminValue.setFont(new Font("times", Font.PLAIN, 12));
+ panel2.add(jminValue, c2);
c2.gridwidth = 1;
panel2.add(new JLabel("Maximum value:"), c2);
c2.gridwidth = GridBagConstraints.REMAINDER; //end row
- maxValue = new JTextField(random.getMaxValue(), 30);
- maxValue.setEditable(true);
- maxValue.setFont(new Font("times", Font.PLAIN, 12));
- panel2.add(maxValue, c2);
+ jmaxValue = new JTextField(maxValue, 30);
+ jmaxValue.setEditable(true);
+ jmaxValue.setFont(new Font("times", Font.PLAIN, 12));
+ panel2.add(jmaxValue, c2);
c2.gridwidth = 1;
panel2.add(new JLabel("Probability function:"), c2);
c2.gridwidth = GridBagConstraints.REMAINDER; //end row
randomFunction = new JComboBox();
randomFunction.addItem("Uniform");
- randomFunction.setSelectedIndex(random.getFunctionId());
+ randomFunction.setSelectedIndex(functionId);
panel2.add(randomFunction, c2);
// main panel;
@@ -196,15 +200,15 @@ public class JDialogTMLADRandom extends javax.swing.JDialog implements ActionLis
}
public String getVariable() {
- return variable.getText();
+ return jvariable.getText();
}
public String getMinValue() {
- return minValue.getText();
+ return jminValue.getText();
}
public String getMaxValue() {
- return maxValue.getText();
+ return jmaxValue.getText();
}
public int getFunctionId() {
diff --git a/src/uppaaldesc/UPPAALTransition.java b/src/uppaaldesc/UPPAALTransition.java
index 36a44268d889204291ab637da3c39f445500baff..c8fa4eb07e8ebc6e241bb4a61476fdbbf1596478 100755
--- a/src/uppaaldesc/UPPAALTransition.java
+++ b/src/uppaaldesc/UPPAALTransition.java
@@ -99,6 +99,10 @@ public class UPPAALTransition {
public boolean isAnEmptyTransition() {
+ if (guard == null) {
+ return true;
+ }
+
if (guard.length() > 0) {
return false;
}