diff --git a/src/translator/ADChoice.java b/src/translator/ADChoice.java
index 163c46a0e5d467277aa79a80052c31247ab27203..cc52414dda83e3e79754afef5b93fdefef951564 100755
--- a/src/translator/ADChoice.java
+++ b/src/translator/ADChoice.java
@@ -156,7 +156,7 @@ public class ADChoice extends ADComponent implements NonBlockingADComponent {
return s;
}
- public boolean isSpecialChoice() {
+ public boolean isSpecialChoice(boolean variableAsActions) {
// All actions following the choice must either be a action on a gate or a delay - determinitic or not - followed by an action on a gate
ADComponent adc, adc1;
@@ -169,7 +169,13 @@ public class ADChoice extends ADComponent implements NonBlockingADComponent {
} else if ((adc instanceof ADDelay) || (adc instanceof ADLatency) ||(adc instanceof ADTimeInterval)) {
adc1 = adc.getNext(0);
if (!(adc1 instanceof ADActionStateWithGate)) {
- return false;
+ if (variableAsActions) {
+ if (!(adc1 instanceof ADActionStateWithParam)) {
+ return false;
+ }
+ } else {
+ return false;
+ }
}
} else {
return false;
@@ -179,12 +185,12 @@ public class ADChoice extends ADComponent implements NonBlockingADComponent {
return true;
}
- public boolean isSpecialChoiceDelay() {
+ public boolean isSpecialChoiceDelay(boolean variableAsActions) {
ADComponent adc, adc1;
String value;
/*if (isElseChoice()) {
- return true;
+ return true;
}*/
@@ -196,14 +202,26 @@ public class ADChoice extends ADComponent implements NonBlockingADComponent {
} else if (adc instanceof ADDelay) {
adc1 = adc.getNext(0);
if (!(adc1 instanceof ADActionStateWithGate)) {
- return false;
+ if (variableAsActions) {
+ if (!(adc1 instanceof ADActionStateWithParam)) {
+ return false;
+ }
+ } else {
+ return false;
+ }
}
} else if (adc instanceof ADLatency) {
value = ((ADLatency)adc).getValue().trim();
if (value.equals("0")) {
adc1 = adc.getNext(0);
if (!(adc1 instanceof ADActionStateWithGate)) {
- return false;
+ if (variableAsActions) {
+ if (!(adc instanceof ADActionStateWithParam)) {
+ return false;
+ }
+ } else {
+ return false;
+ }
}
}
} else if (adc instanceof ADTimeInterval) {
@@ -211,7 +229,13 @@ public class ADChoice extends ADComponent implements NonBlockingADComponent {
if (adt.getMinValue().equals(adt.getMaxValue())) {
adc1 = adc.getNext(0);
if (!(adc1 instanceof ADActionStateWithGate)) {
- return false;
+ if (variableAsActions) {
+ if (!(adc1 instanceof ADActionStateWithParam)) {
+ return false;
+ }
+ } else {
+ return false;
+ }
}
}
} else {
@@ -222,7 +246,7 @@ public class ADChoice extends ADComponent implements NonBlockingADComponent {
return true;
}
- public boolean isSpecialChoiceAction() {
+ public boolean isSpecialChoiceAction(boolean variableAsActions) {
ADComponent adc, adc1;
String value;
@@ -230,14 +254,22 @@ public class ADChoice extends ADComponent implements NonBlockingADComponent {
adc = getNext(i);
if (!(adc instanceof ADActionStateWithGate)) {
- return false;
+ if (variableAsActions) {
+ if (!(adc instanceof ADActionStateWithParam)) {
+ return false;
+ }
+ } else {
+ return false;
+ }
}
+
+
}
return true;
}
- public boolean isSpecialChoice(int index) {
+ public boolean isSpecialChoice(int index, boolean variableAsActions) {
ADComponent adc, adc1;
adc = getNext(index);
@@ -246,7 +278,13 @@ public class ADChoice extends ADComponent implements NonBlockingADComponent {
} else if ((adc instanceof ADDelay) || (adc instanceof ADLatency) ||(adc instanceof ADTimeInterval)) {
adc1 = adc.getNext(0);
if (!(adc1 instanceof ADActionStateWithGate)) {
- return false;
+ if (variableAsActions) {
+ if (!(adc1 instanceof ADActionStateWithParam)) {
+ return false;
+ }
+ } else {
+ return false;
+ }
}
} else {
return false;
@@ -299,9 +337,9 @@ public class ADChoice extends ADComponent implements NonBlockingADComponent {
g1 = Conversion.replaceAllChar(g1, ']', "").trim();
if (g0.startsWith("not(")) {
- g0 = g0.substring(4, g0.length()-1);
+ g0 = g0.substring(4, g0.length()-1);
} else if (g1.startsWith("not(")) {
- g1 = g1.substring(4, g1.length()-1);
+ g1 = g1.substring(4, g1.length()-1);
}
if (g0.compareTo(g1) == 0) {
diff --git a/src/translator/ADTimeCapture.java b/src/translator/ADTimeCapture.java
new file mode 100755
index 0000000000000000000000000000000000000000..c3cce62faec1664680efd747480d841d7ce496f7
--- /dev/null
+++ b/src/translator/ADTimeCapture.java
@@ -0,0 +1,90 @@
+/**Copyright or 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 ADTimeCapture
+ * Creation: 23/07/2009
+ * @version 1.0 23/07/2009
+ * @author Ludovic APVRILLE
+ * @see
+ */
+
+package translator;
+
+
+
+public class ADTimeCapture extends ADComponent {
+ protected Param p;
+ Process proc;
+
+ public ADTimeCapture(Param _p) {
+ p = _p;
+ }
+
+ public ADTimeCapture() {
+ }
+
+ public void setParam(Param _p) {
+ p = _p;
+ }
+
+ public Param getParam() {
+ return p;
+ }
+
+ public void setProcess(Process _p) {
+ proc = _p;
+ }
+
+ public Process getProcess() {
+ return proc;
+ }
+
+ public String toString() {
+ return "Time capture (" + p.getName() + ")";
+ }
+
+ public String brutToString() {
+ return p.getName();
+ }
+
+ public ADComponent makeSame() {
+ ADTimeCapture adtc = new ADTimeCapture(getParam());
+ return adtc;
+ }
+}
+
diff --git a/src/translator/ActivityDiagram.java b/src/translator/ActivityDiagram.java
index 572f6855bb23cca1b83e9259f2b8fe56bd69b92b..623d9495e47f77be85ce79641bf374e5d7ac01ee 100755
--- a/src/translator/ActivityDiagram.java
+++ b/src/translator/ActivityDiagram.java
@@ -497,7 +497,7 @@ public class ActivityDiagram extends Vector{
add(adag);
}
- public void makeSpecialChoices() {
+ public void makeSpecialChoices(boolean variableAsActions) {
ADComponent adc;
boolean changeMade = true;
while(changeMade) {
@@ -505,8 +505,8 @@ public class ActivityDiagram extends Vector{
for(int i=0; i<size(); i++) {
adc = (ADComponent)(elementAt(i));
if (adc instanceof ADChoice) {
- if (!(((ADChoice)(adc)).isSpecialChoice())) {
- if (makeSpecialChoice((ADChoice)(adc))) {
+ if (!(((ADChoice)(adc)).isSpecialChoice(variableAsActions))) {
+ if (makeSpecialChoice((ADChoice)(adc), variableAsActions)) {
changeMade = true;
}
}
@@ -515,7 +515,7 @@ public class ActivityDiagram extends Vector{
}
}
- public boolean makeSpecialChoice(ADChoice adch) {
+ public boolean makeSpecialChoice(ADChoice adch, boolean variableAsActions) {
ADComponent adc;
ADChoice adch1;
boolean go = true;
@@ -528,7 +528,7 @@ public class ActivityDiagram extends Vector{
for(int i=0; i<adch.getNbGuard(); i++) {
delay = 0;
- if (!adch.isSpecialChoice(i)) {
+ if (!adch.isSpecialChoice(i, variableAsActions)) {
// Go through the elements
adc = adch.getNext(i);
met = new LinkedList();
@@ -551,7 +551,7 @@ public class ActivityDiagram extends Vector{
if ((adc instanceof ADChoice) && (delay <1) && (adc != adch)) {
// Combine choices together
adch1 = (ADChoice)adc;
- if (adch1.isSpecialChoice()) {
+ if (adch1.isSpecialChoice(variableAsActions)) {
//Good!
//adch.removeGuard(i);
//System.out.println("Working on it...");
@@ -579,7 +579,7 @@ public class ActivityDiagram extends Vector{
}
add(adag1);
add(adj);
- if (adch.isSpecialChoice()) {
+ if (adch.isSpecialChoice(variableAsActions)) {
//System.out.println("Now, special choice!");
} else {
//System.out.println("Still not a special choice!");
@@ -611,7 +611,7 @@ public class ActivityDiagram extends Vector{
add(adag1);
add(adj);
- if (adch.isSpecialChoice()) {
+ if (adch.isSpecialChoice(variableAsActions)) {
System.out.println("Now, special choice!");
} else {
System.out.println("Still not a special choice!");
@@ -659,7 +659,7 @@ public class ActivityDiagram extends Vector{
}
- public int getMaximumNbOfGuardsPerSpecialChoice() {
+ public int getMaximumNbOfGuardsPerSpecialChoice(boolean variableAsActions) {
int nb = 0;
ADComponent adc;
ADChoice adch;
@@ -667,7 +667,7 @@ public class ActivityDiagram extends Vector{
adc = (ADComponent)(elementAt(i));
if (adc instanceof ADChoice) {
adch = (ADChoice)adc;
- if (adch.isSpecialChoice() && (!adch.isSpecialChoiceAction())) {
+ if (adch.isSpecialChoice(variableAsActions) && (!adch.isSpecialChoiceAction(variableAsActions))) {
nb = Math.max(nb, ((ADChoice)adc).getNbGuard());
}
}
diff --git a/src/translator/TClass.java b/src/translator/TClass.java
index 86cea236e3a236e886a1bfb6200743de1b33a7f2..463131e53cd4c2b639640afb22ea283ef9b48fe5 100755
--- a/src/translator/TClass.java
+++ b/src/translator/TClass.java
@@ -656,12 +656,12 @@ public class TClass {
return ad.getMaximumNbOfGuardsPerChoice();
}
- public int getMaximumNbOfGuardsPerSpecialChoice() {
+ public int getMaximumNbOfGuardsPerSpecialChoice(boolean variableAsActions) {
if (ad == null) {
return 0;
}
- return ad.getMaximumNbOfGuardsPerSpecialChoice();
+ return ad.getMaximumNbOfGuardsPerSpecialChoice(variableAsActions);
}
diff --git a/src/translator/TURTLEModeling.java b/src/translator/TURTLEModeling.java
index cef58c1e142c1df4aaf680ec0d555ee91e07264c..d9f09c1ad2f531cac9dadb6e301fb7238327f31e 100755
--- a/src/translator/TURTLEModeling.java
+++ b/src/translator/TURTLEModeling.java
@@ -258,15 +258,15 @@ public class TURTLEModeling {
// * No non regular choice (delay choice in fact)
// * No recursivity over parallel operator
public boolean isARegularTIFSpec() {
- return isARegularTIFSpec(false);
+ return isARegularTIFSpec(false, false);
}
- public boolean isARegularTIFSpec(boolean choicesDeterministic) {
+ public boolean isARegularTIFSpec(boolean choicesDeterministic, boolean variableAsActions) {
if (!hasOnlyRegularRelations()) {
return false;
}
- if (!hasOnlyRegularTClasses(choicesDeterministic)) {
+ if (!hasOnlyRegularTClasses(choicesDeterministic, variableAsActions)) {
return false;
}
@@ -285,18 +285,18 @@ public class TURTLEModeling {
return true;
}
- public boolean hasOnlyRegularTClasses(boolean choicesDeterministic) {
+ public boolean hasOnlyRegularTClasses(boolean choicesDeterministic, boolean variableAsActions) {
TClass tmp;
for(int i=0; i<tclass.size(); i++) {
tmp = (TClass)(tclass.elementAt(i));
- if (!isRegularTClass(tmp.getActivityDiagram(), choicesDeterministic)) {
+ if (!isRegularTClass(tmp.getActivityDiagram(), choicesDeterministic, variableAsActions)) {
return false;
}
}
return true;
}
- public boolean isRegularTClass(ActivityDiagram ad, boolean choicesDeterministic) {
+ public boolean isRegularTClass(ActivityDiagram ad, boolean choicesDeterministic, boolean variableAsActions) {
ADComponent adc;
ADChoice adchoice;
@@ -314,7 +314,7 @@ public class TURTLEModeling {
if (adc instanceof ADChoice) {
adchoice = (ADChoice)adc;
if (!choicesDeterministic) {
- if (!adchoice.isSpecialChoiceDelay()) {
+ if (!adchoice.isSpecialChoiceDelay(variableAsActions)) {
if (!adchoice.isElseChoice()) {
System.out.println("Choice is not regular");
for(int j=0; j<adchoice.getNbNext(); j++) {
@@ -1040,7 +1040,7 @@ public class TURTLEModeling {
//System.out.println("Remove All useless components");
if (specialChoices) {
- ad.makeSpecialChoices();
+ ad.makeSpecialChoices(false);
}
while(i<ad.size()) {
@@ -1249,6 +1249,7 @@ public class TURTLEModeling {
ADComponent adc;
ADActionStateWithGate adag;
ADActionStateWithParam adap;
+ ADTimeCapture adtc;
ADChoice adch;
ADTLO adtlo;
int i, j;
@@ -1281,6 +1282,7 @@ public class TURTLEModeling {
usage = analyzeString2WithParam(adag.getLimitOnGate(), name);
}
}
+
} else if (adc instanceof ADActionStateWithParam) {
adap = (ADActionStateWithParam)adc;
if (adap.getParam() == p) {
@@ -1290,6 +1292,13 @@ public class TURTLEModeling {
if (usage == 0) {
usage = analyzeString2WithParam(adap.getActionValue(), name);
}
+
+ } else if (adc instanceof ADTimeCapture) {
+ adtc = (ADTimeCapture)adc;
+ if (adtc.getParam() == p) {
+ return 2;
+ }
+
} else if (adc instanceof ADTLO) {
adtlo = (ADTLO)adc;
s = adtlo.getAction();
@@ -2724,22 +2733,22 @@ public class TURTLEModeling {
}
public void mergeChoices() {
- mergeChoices(false);
+ mergeAllChoices();
}
- public void mergeChoices(boolean nonDeterministic) {
- System.out.println("Merging choices: algorithm / not guarded only: " + nonDeterministic);
+ public void mergeAllChoices() {
+ System.out.println("Merging choices: algorithm");
TClass t;
for(int i=0; i<tclass.size(); i++) {
t = (TClass)(tclass.elementAt(i));
- mergeChoices(t.getActivityDiagram(), nonDeterministic);
+ mergeChoices(t.getActivityDiagram());
}
System.out.println("End merging choices: algorithm");
}
-
- public void mergeChoices(ActivityDiagram ad, boolean nonDeterministic) {
+ // We merge non-else choices
+ public void mergeChoices(ActivityDiagram ad) {
boolean changeMade = true;
int i;
ADComponent adc1;
@@ -2750,17 +2759,12 @@ public class TURTLEModeling {
adc1 = (ADComponent)(ad.get(i));
if (adc1 instanceof ADChoice) {
adch1 = (ADChoice) adc1;
- if ((index = adch1.getNextChoice()) != -1) {
- if ((nonDeterministic) && (!adch1.isGuarded())) {
+ if (!adch1.isElseChoice()) {
+ index = adch1.getNextChoice();
+ if (index != -1) {
mergeChoices(ad, adch1, index);
- mergeChoices(ad, nonDeterministic);
+ mergeChoices(ad);
return;
- } else {
- if (!nonDeterministic) {
- mergeChoices(ad, adch1, index);
- mergeChoices(ad, nonDeterministic);
- return;
- }
}
}
}
@@ -2801,6 +2805,8 @@ public class TURTLEModeling {
adch1.removeNext(adch2);
ad.remove(adch2);
+
+ System.out.println("New choice:" + adch1.toString());
}
public void makeSequenceWithDataSave() {
diff --git a/src/translator/tojava/TURTLE2Java.java b/src/translator/tojava/TURTLE2Java.java
index 9b598c27104959bab932e6595fab565ba242af56..1d504480cb1f3bdb75d742cedff29622247d8857 100755
--- a/src/translator/tojava/TURTLE2Java.java
+++ b/src/translator/tojava/TURTLE2Java.java
@@ -912,7 +912,7 @@ public class TURTLE2Java {
}
- if (adch.isSpecialChoice()) {
+ if (adch.isSpecialChoice(false)) {
/*indent(jo, dec);
jo.addCode("__bchoice__name = new JGate[" + nbG + "];\n");
indent(jo, dec);
diff --git a/src/translator/touppaal/TURTLE2UPPAAL.java b/src/translator/touppaal/TURTLE2UPPAAL.java
index 7f0f88fc0995089e5e235bc20744a6f7a797f072..f59888a0d18ac1958488682bc23ba21cc056c2c8 100755
--- a/src/translator/touppaal/TURTLE2UPPAAL.java
+++ b/src/translator/touppaal/TURTLE2UPPAAL.java
@@ -59,6 +59,7 @@ public class TURTLE2UPPAAL {
private boolean isRegular;
private boolean isRegularTClass;
private boolean choicesDeterministic = false;
+ private boolean variableAsActions = false;
private RelationTIFUPPAAL table;
private Vector warnings;
@@ -131,6 +132,11 @@ public class TURTLE2UPPAAL {
System.out.println("choices are assumed to be deterministic:" + choicesDeterministic);
}
+ public void setVariablesAsActions(boolean _b) {
+ variableAsActions = _b;
+ System.out.println("Branch of choices may be selected according to variable setting: " + variableAsActions);
+ }
+
public UPPAALSpec generateUPPAAL(boolean _debug, int _nb) {
warnings = new Vector();
spec = new UPPAALSpec();
@@ -161,13 +167,13 @@ public class TURTLE2UPPAAL {
// Work with tm modeling
// For example, compact latencies together, etc.
- tm.mergeChoices(true);
+ tm.mergeChoices();
tm.translateWatchdogs();
tm.translateInvocationIntoSynchronization();
tm.translateActionStatesWithMultipleParams();
// Analyze the tm spcification
- isRegular = tm.isARegularTIFSpec(choicesDeterministic);
+ isRegular = tm.isARegularTIFSpec(choicesDeterministic, variableAsActions);
idPar = 0;
System.out.println("Regular spec:" + isRegular);
@@ -326,7 +332,7 @@ public class TURTLE2UPPAAL {
template1 = (UPPAALTemplate)(iterator.next());
t = tm.getTClassWithName(template1.getName());
if (t!= null) {
- if(!(tm.isRegularTClass(t.getActivityDiagram(), choicesDeterministic))) {
+ if(!(tm.isRegularTClass(t.getActivityDiagram(), choicesDeterministic, variableAsActions))) {
spec.addGlobalDeclaration(makeGlobalParamDeclaration(t));
loc2 = addLocation(template);
@@ -492,7 +498,7 @@ public class TURTLE2UPPAAL {
}
public void translateTClass(TClass t) {
- isRegularTClass = tm.isRegularTClass(t.getActivityDiagram(), choicesDeterministic);
+ isRegularTClass = tm.isRegularTClass(t.getActivityDiagram(), choicesDeterministic, variableAsActions);
tmpComponents = new LinkedList();
tmpLocations = new LinkedList();
locations = new LinkedList();
@@ -547,7 +553,7 @@ public class TURTLE2UPPAAL {
template.addDeclaration("int " + t.getName() + "__" + g.getName() + TURTLE2UPPAAL.SYNCID + " = 0;\n");
}
- int nbOfChoice = t.getMaximumNbOfGuardsPerSpecialChoice();
+ int nbOfChoice = t.getMaximumNbOfGuardsPerSpecialChoice(variableAsActions);
for(i=0; i<nbOfChoice; i++) {
template.addDeclaration("int choice__" + i + ";\n");
}
@@ -985,13 +991,14 @@ public class TURTLE2UPPAAL {
makeElementBehavior(t, template, elt.getNext(0), previous, end, null);
}
} else {
- if (adch.isSpecialChoiceDelay()) {
-
+ if (adch.isSpecialChoiceDelay(variableAsActions)) {
+ System.out.println("Special choice found");
// Must check whether some actions are delayed or not
- if (adch.isSpecialChoiceAction()) {
+ if (adch.isSpecialChoiceAction(variableAsActions)) {
for(i=0; i<elt.getNbNext(); i++){
- //System.out.println("Special choice action / Task " + t.getName() + ": Choice is deterministic i=" + i + " with guard =" + adch.getGuard(i));
+ System.out.println("Special choice action / Task " + t.getName() + ": guard i=" + i + " =" + adch.getGuard(i));
+
String gua = null;
if (adch.isGuarded(i)) {
@@ -1002,7 +1009,7 @@ public class TURTLE2UPPAAL {
currentX += 2 * STEP_LOOP_X;
}
} else {
- //System.out.println("Special choice delay");
+ System.out.println("Special choice delay");
int tmpX = currentX;
int next = 0;
@@ -1013,7 +1020,7 @@ public class TURTLE2UPPAAL {
// Initialization
String init = "h__ = 0";
for(i=0; i<elt.getNbNext(); i++){
- //System.out.println("Special choice delay / Task " + t.getName() + ": Choice is deterministic i=" + i + " with guard =" + adch.getGuard(i));
+ System.out.println("Special choice delay / Task " + t.getName() + ": guard i=" + i + " =" + adch.getGuard(i));
elt1 = elt.getNext(i);
diff --git a/src/ui/DesignPanelTranslator.java b/src/ui/DesignPanelTranslator.java
index a003277464c0c0f592bed877fb09ccf112329fc8..239a6e22ff34dd761f958a2acdc4302507deca4d 100755
--- a/src/ui/DesignPanelTranslator.java
+++ b/src/ui/DesignPanelTranslator.java
@@ -356,6 +356,7 @@ public class DesignPanelTranslator {
ADStop adst;
ADTimeInterval adti;
ADTLO adtlo;
+ ADTimeCapture adtc;
String s, s1;
Gate g;
Param p;
@@ -476,6 +477,23 @@ public class DesignPanelTranslator {
//System.out.println("Bad action state found " + s);
}
+ } else if (tgc instanceof TADTimeCapture) {
+ p = t.getParamByName(tgc.getValue().trim());
+ if (p != null){
+ System.out.println("Time capture with param " + p.getName());
+ adtc = new ADTimeCapture(p);
+ ad.addElement(adtc);
+ ((TADTimeCapture)tgc).setStateAction(ErrorHighlight.ATTRIBUTE);
+ } else {
+ CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Unknown variable: " + tgc.getValue());
+ ce.setTClass(t);
+ ce.setTGComponent(tgc);
+ ce.setTDiagramPanel(tdp);
+ addCheckingError(ce);
+ ((TADTimeCapture)tgc).setStateAction(ErrorHighlight.UNKNOWN_AS);
+ }
+
+ // Get element from Array
} else if (tgc instanceof TADArrayGetState) {
TADArrayGetState ags = (TADArrayGetState)tgc;
sTmp = ags.getIndex();
diff --git a/src/ui/GTURTLEModeling.java b/src/ui/GTURTLEModeling.java
index e06d35895aecd5f1c3151c4c4d61dbb007e3f73a..9dcdf8727805343c281f4de61903c0e49b18c9ff 100755
--- a/src/ui/GTURTLEModeling.java
+++ b/src/ui/GTURTLEModeling.java
@@ -254,11 +254,11 @@ public class GTURTLEModeling {
return ret;
}
- public void mergeChoices(boolean nonDeterministic) {
+ /*public void mergeChoices(boolean nonDeterministic) {
if (tm != null) {
tm.mergeChoices(nonDeterministic);
}
- }
+ }*/
public NCStructure getNCS() {
return ncs;
@@ -354,9 +354,10 @@ public class GTURTLEModeling {
uppaalTable = _uppaalTable;
}*/
- public boolean generateUPPAALFromTIF(String path, boolean debug, int nb, boolean choices) {
+ public boolean generateUPPAALFromTIF(String path, boolean debug, int nb, boolean choices, boolean variables) {
TURTLE2UPPAAL turtle2uppaal = new TURTLE2UPPAAL(tm);
turtle2uppaal.setChoiceDeterministic(choices);
+ turtle2uppaal.setVariablesAsActions(variables);
uppaal = turtle2uppaal.generateUPPAAL(debug, nb);
System.out.println("Building relation table");
uppaalTIFTable = turtle2uppaal.getRelationTIFUPPAAL();
diff --git a/src/ui/MainGUI.java b/src/ui/MainGUI.java
index a38cf61004191fc2228b44606e1b04e950de993d..07522aca1b1504dd5a00398dfddc8b00a9660878 100755
--- a/src/ui/MainGUI.java
+++ b/src/ui/MainGUI.java
@@ -5481,6 +5481,8 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener {
actionOnButton(TGComponentManager.COMPONENT, TGComponentManager.TAD_TIME_LIMITED_OFFER);
} else if (command.equals(actions[TGUIAction.AD_TIME_LIMITED_OFFER_WITH_LATENCY].getActionCommand())) {
actionOnButton(TGComponentManager.COMPONENT, TGComponentManager.TAD_TIME_LIMITED_OFFER_WITH_LATENCY);
+ } else if (command.equals(actions[TGUIAction.AD_TIME_CAPTURE].getActionCommand())) {
+ actionOnButton(TGComponentManager.COMPONENT, TGComponentManager.TAD_TIME_CAPTURE);
} else if (command.equals(actions[TGUIAction.IOD_EDIT].getActionCommand())) {
actionOnButton(TGComponentManager.EDIT, -1);
} else if (command.equals(actions[TGUIAction.IOD_CONNECTOR].getActionCommand())) {
diff --git a/src/ui/TGComponentManager.java b/src/ui/TGComponentManager.java
index 7cef5f8d01e697a42fe4656eda1e719d07ccf6e5..7420237400bd2696037dcdfc0e617a1766a6ed41 100755
--- a/src/ui/TGComponentManager.java
+++ b/src/ui/TGComponentManager.java
@@ -86,6 +86,7 @@ public class TGComponentManager {
public static final int TAD_DELAY_NON_DETERMINISTIC_DELAY = 20;
public static final int TAD_CHOICE = 19;
public static final int TAD_TIME_LIMITED_OFFER_WITH_LATENCY = 10;
+ public static final int TAD_TIME_CAPTURE = 27;
public static final int TAD_ARRAY_GET = 25;
public static final int TAD_ARRAY_SET = 26;
@@ -302,6 +303,9 @@ public class TGComponentManager {
break;
case TAD_TIME_LIMITED_OFFER_WITH_LATENCY:
tgc = new TADTimeLimitedOfferWithLatency(x, y, tdp.getMinX(), tdp.getMaxX(), tdp.getMinY(), tdp.getMaxY(), false, null, tdp);
+ break;
+ case TAD_TIME_CAPTURE:
+ tgc = new TADTimeCapture(x, y, tdp.getMinX(), tdp.getMaxX(), tdp.getMinY(), tdp.getMaxY(), false, null, tdp);
break;
case TAD_CHOICE:
tgc = new TADChoice(x, y, tdp.getMinX(), tdp.getMaxX(), tdp.getMinY(), tdp.getMaxY(), false, null, tdp);
@@ -648,6 +652,8 @@ public class TGComponentManager {
return TAD_DELAY_NON_DETERMINISTIC_DELAY;
} else if (tgc instanceof TADTimeLimitedOfferWithLatency) {
return TAD_TIME_LIMITED_OFFER_WITH_LATENCY;
+ } else if (tgc instanceof TADTimeCapture) {
+ return TAD_TIME_CAPTURE;
} else if (tgc instanceof TADChoice) {
return TAD_CHOICE;
} else if (tgc instanceof TCDTClass) {
diff --git a/src/ui/TGUIAction.java b/src/ui/TGUIAction.java
index c1322f53e019dfbf33b0628adc708122147a8411..2a5ab4f3aa441d5552561027587a072ff0c36a69 100755
--- a/src/ui/TGUIAction.java
+++ b/src/ui/TGUIAction.java
@@ -105,6 +105,7 @@ public class TGUIAction extends AbstractAction {
public static final int AD_DELAY_NON_DETERMINISTIC_DELAY = 49;
public static final int AD_TIME_LIMITED_OFFER = 17;
public static final int AD_TIME_LIMITED_OFFER_WITH_LATENCY = 18;
+ public static final int AD_TIME_CAPTURE = 269;
public static final int TCD_PARALLEL_OPERATOR = 19;
public static final int TCD_CONNECTOR_ATTRIBUTE = 20;
public static final int TCD_SEQUENCE_OPERATOR = 21;
@@ -379,7 +380,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 = 269;
+ public static final int NB_ACTION = 270;
private static final TAction [] actions = new TAction[NB_ACTION];
@@ -558,6 +559,7 @@ public class TGUIAction extends AbstractAction {
actions[AD_DELAY_NON_DETERMINISTIC_DELAY] = new TAction("add-time-interval", "Add Time Interval", IconManager.imgic224, IconManager.imgic224, "Time interval", "Add a time interval to the currently opened activity diagram", 0);
actions[AD_TIME_LIMITED_OFFER] = new TAction("add-time-limited-offer", "Add Time-Limited offer", IconManager.imgic218, IconManager.imgic218, "Time-Limited Offer", "Add a time-limited offer to the currently opened activity diagram", 0);
actions[AD_TIME_LIMITED_OFFER_WITH_LATENCY] = new TAction("add-time-limited-offer-with-latency", "Add Time-Limited offer with a non-deterministic delay", IconManager.imgic220, IconManager.imgic220, "Time-Limited Offer with non-deterministic delay", "Adds a time-limited offer, beginning with a non-deterministic delay, to the currently opened activity diagram", 0);
+ actions[AD_TIME_CAPTURE] = new TAction("add-time-capture", "Time capture", IconManager.imgic204, IconManager.imgic204, "Action time capture", "Add a time capture operator to the currently opened activity diagram", 0);
actions[AD_ARRAY_GET] = new TAction("add-array-get", "Add array get element", IconManager.imgic230, IconManager.imgic230, "Array get element", "Add an array get element action to the currently opened activity diagram", 0);
actions[AD_ARRAY_SET] = new TAction("add-array-set", "Add array set element", IconManager.imgic232, IconManager.imgic232, "Array set element", "Add an array set element action to the currently opened activity diagram", 0);
diff --git a/src/ui/ad/TADTimeCapture.java b/src/ui/ad/TADTimeCapture.java
new file mode 100755
index 0000000000000000000000000000000000000000..ba80e25bdf9170b2e2dad3bfcacac96d5a1ba09b
--- /dev/null
+++ b/src/ui/ad/TADTimeCapture.java
@@ -0,0 +1,145 @@
+/**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 TADTimeCapture
+ * Capturing the time in an activity diagram
+ * Creation: 23/07/2009
+ * @version 1.0 23/07/2009
+ * @author Ludovic APVRILLE
+ * @see
+ */
+
+package ui.ad;
+
+import java.awt.*;
+import java.awt.geom.*;
+
+import myutil.*;
+import ui.*;
+
+public class TADTimeCapture extends TGCOneLineText implements ActionStateErrorHighlight {
+ protected int lineLength = 5;
+ protected int textX = 5;
+ protected int textY = 15;
+ protected int arc = 5;
+
+ protected int stateAction = 0; // 0: unchecked 1: attribute; 3:unknown
+
+
+ public TADTimeCapture(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 TGConnectingPointAD(this, 0, -lineLength, true, false, 0.5, 0.0);
+ connectingPoint[1] = new TGConnectingPointAD(this, 0, lineLength, false, true, 0.5, 1.0);
+ addTGConnectingPointsComment();
+
+ moveable = true;
+ editable = true;
+ removable = true;
+
+ value = "x";
+ name = "Capture time in variable:";
+
+ myImageIcon = IconManager.imgic204;
+ }
+
+ public void internalDrawing(Graphics g) {
+ String myVal = "time -> " + value;
+ int w = g.getFontMetrics().stringWidth(myVal);
+ int w1 = Math.max(minWidth, w + 2 * textX);
+ if ((w1 != width) & (!tdp.isScaled())) {
+ setCd(x + width/2 - w1/2, y);
+ width = w1;
+ //updateConnectingPoints();
+ }
+
+
+ if (stateAction > 0) {
+ Color c = g.getColor();
+ switch(stateAction) {
+ case ErrorHighlight.ATTRIBUTE:
+ g.setColor(ColorManager.ATTRIBUTE_BOX_ACTION);
+ 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.drawString(myVal, x + (width - w) / 2 , y + textY);
+
+ }
+
+ 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;
+ }
+
+
+ return null;
+ }
+
+
+ public int getType() {
+ return TGComponentManager.TAD_TIME_CAPTURE;
+ }
+
+ public int getDefaultConnector() {
+ return TGComponentManager.CONNECTOR_AD_DIAGRAM;
+ }
+
+ public void setStateAction(int _stateAction) {
+ stateAction = _stateAction;
+ }
+
+}
diff --git a/src/ui/ad/TActivityDiagramToolBar.java b/src/ui/ad/TActivityDiagramToolBar.java
index 0bf7d79476c5dbe00d545f1bb4cbabc62f119f09..051f76aae3d75970b4db14fc74f46dc42c4e1a33 100755
--- a/src/ui/ad/TActivityDiagramToolBar.java
+++ b/src/ui/ad/TActivityDiagramToolBar.java
@@ -77,6 +77,7 @@ public class TActivityDiagramToolBar extends TToolBar {
mgui.actions[TGUIAction.AD_DELAY_NON_DETERMINISTIC_DELAY].setEnabled(b);
mgui.actions[TGUIAction.AD_TIME_LIMITED_OFFER].setEnabled(b);
mgui.actions[TGUIAction.AD_TIME_LIMITED_OFFER_WITH_LATENCY].setEnabled(b);
+ mgui.actions[TGUIAction.AD_TIME_CAPTURE].setEnabled(b);
mgui.actions[TGUIAction.AD_ARRAY_GET].setEnabled(b);
mgui.actions[TGUIAction.AD_ARRAY_SET].setEnabled(b);
mgui.actions[TGUIAction.ACT_TOGGLE_JAVA].setEnabled(b);
@@ -152,6 +153,9 @@ public class TActivityDiagramToolBar extends TToolBar {
button = this.add(mgui.actions[TGUIAction.AD_TIME_LIMITED_OFFER_WITH_LATENCY]);
button.addMouseListener(mgui.mouseHandler);
+ /*button = this.add(mgui.actions[TGUIAction.AD_TIME_CAPTURE]);
+ button.addMouseListener(mgui.mouseHandler);*/
+
this.addSeparator();
button = this.add(mgui.actions[TGUIAction.AD_ARRAY_GET]);
diff --git a/src/ui/window/JDialogUPPAALGeneration.java b/src/ui/window/JDialogUPPAALGeneration.java
index 5f2b4a99a5a3ecccbb1eaf968ddd26326ec06a10..44461aa7036af2648a531211732ff2e69dde2430 100755
--- a/src/ui/window/JDialogUPPAALGeneration.java
+++ b/src/ui/window/JDialogUPPAALGeneration.java
@@ -67,6 +67,7 @@ public class JDialogUPPAALGeneration extends javax.swing.JDialog implements Acti
protected static String sizeInfiniteFIFO = "1024";
protected static boolean debugGen = false;
protected static boolean choicesDeterministicStatic = false;
+ protected static boolean variablesAsActionsStatic = true;
protected final static int NOT_STARTED = 1;
@@ -86,7 +87,7 @@ public class JDialogUPPAALGeneration extends javax.swing.JDialog implements Acti
protected JTextField sizeOfInfiniteFIFO;
protected JTabbedPane jp1;
protected JScrollPane jsp;
- protected JCheckBox debugmode, choicesDeterministic;
+ protected JCheckBox debugmode, choicesDeterministic, variablesAsActions;
private Thread t;
private boolean go = false;
@@ -174,7 +175,16 @@ public class JDialogUPPAALGeneration extends javax.swing.JDialog implements Acti
choicesDeterministic = new JCheckBox("Assume all choices as deterministic");
choicesDeterministic.setSelected(choicesDeterministicStatic);
jp01.add(choicesDeterministic, c01);
+
+ variablesAsActions = new JCheckBox("Assume variable setting as actions for branch selection");
+ variablesAsActions.setSelected(variablesAsActionsStatic);
+ jp01.add(variablesAsActions, c01);
+ TURTLEPanel tp = mgui.getCurrentTURTLEPanel();
+ if (tp instanceof TMLDesignPanel) {
+ variablesAsActions.setEnabled(false);
+ }
+
jp01.add(new JLabel(" "), c01);
jp1.add("Generate code", jp01);
@@ -264,7 +274,7 @@ public class JDialogUPPAALGeneration extends javax.swing.JDialog implements Acti
String cmd;
String list;
- boolean debug, choices;
+ boolean debug, choices, variables;
int nb = 0;
int nb1;
@@ -278,6 +288,7 @@ public class JDialogUPPAALGeneration extends javax.swing.JDialog implements Acti
//Manage debug
debug = debugmode.isSelected();
choices = choicesDeterministic.isSelected();
+ variables = variablesAsActions.isSelected();
// Manage nb of processes
try {
@@ -314,7 +325,7 @@ public class JDialogUPPAALGeneration extends javax.swing.JDialog implements Acti
if (tp instanceof TMLDesignPanel) {
result = mgui.gtm.generateUPPAALFromTML(pathCode, debug, size1, choices);
} else {
- result = mgui.gtm.generateUPPAALFromTIF(pathCode, debug, nb1, choices);
+ result = mgui.gtm.generateUPPAALFromTIF(pathCode, debug, nb1, choices, variables);
jta.append("UPPAAL specification generated\n");
jta.append("Checking the regularity of the TIF specification\n");
System.out.println("Regularity?");