From 120674122cef548e767da1176c18b6de317d8cf6 Mon Sep 17 00:00:00 2001
From: Ludovic Apvrille <ludovic.apvrille@telecom-paristech.fr>
Date: Fri, 10 Apr 2009 15:48:36 +0000
Subject: [PATCH] Many bugs resolved!
---
src/translator/ADChoice.java | 19 +-
src/translator/ActivityDiagram.java | 30 +
src/translator/TClass.java | 16 +
src/translator/TURTLEModeling.java | 11 +
src/translator/TURTLETranslator.java | 23 +-
.../touppaal/RelationTIFUPPAAL.java | 11 +
src/translator/touppaal/TURTLE2UPPAAL.java | 532 ++++++++++--------
src/ui/CorrespondanceTGElement.java | 33 +-
src/ui/DesignPanelTranslator.java | 3 +-
src/ui/GTURTLEModeling.java | 64 +--
src/ui/MainGUI.java | 8 +
src/ui/TDiagramPanel.java | 7 -
src/ui/ad/TActivityDiagramToolBar.java | 5 +
src/ui/cd/TClassDiagramToolBar.java | 5 +
src/ui/dd/TDeploymentDiagramToolBar.java | 5 +
.../InteractionOverviewDiagramToolBar.java | 5 +
src/ui/ncdd/NCDiagramToolBar.java | 5 +
.../osad/TURTLEOSActivityDiagramToolBar.java | 5 +
src/ui/oscd/TURTLEOSClassDiagramToolBar.java | 5 +
src/ui/procsd/ProactiveCSDToolBar.java | 6 +
src/ui/prosmd/ProactiveSMDToolBar.java | 5 +
src/ui/sd/SequenceDiagramToolBar.java | 5 +
src/ui/tmlad/TMLActivityDiagramToolBar.java | 5 +
src/ui/tmlcd/TMLTaskDiagramToolBar.java | 5 +
src/ui/tmldd/TMLArchiDiagramToolBar.java | 3 +
src/ui/ucd/UseCaseDiagramToolBar.java | 5 +
src/ui/window/JDialogUPPAALGeneration.java | 4 +
src/ui/window/JDialogUPPAALValidation.java | 4 +-
src/uppaaldesc/UPPAALSpec.java | 4 +-
src/uppaaldesc/UPPAALTemplate.java | 28 +-
30 files changed, 546 insertions(+), 320 deletions(-)
diff --git a/src/translator/ADChoice.java b/src/translator/ADChoice.java
index 435d4f988b..163c46a0e5 100755
--- a/src/translator/ADChoice.java
+++ b/src/translator/ADChoice.java
@@ -183,9 +183,9 @@ public class ADChoice extends ADComponent implements NonBlockingADComponent {
ADComponent adc, adc1;
String value;
- if (isElseChoice()) {
+ /*if (isElseChoice()) {
return true;
- }
+ }*/
for(int i=0; i<next.size(); i++) {
@@ -219,6 +219,21 @@ public class ADChoice extends ADComponent implements NonBlockingADComponent {
}
}
+ return true;
+ }
+
+ public boolean isSpecialChoiceAction() {
+ ADComponent adc, adc1;
+ String value;
+
+ for(int i=0; i<next.size(); i++) {
+ adc = getNext(i);
+
+ if (!(adc instanceof ADActionStateWithGate)) {
+ return false;
+ }
+ }
+
return true;
}
diff --git a/src/translator/ActivityDiagram.java b/src/translator/ActivityDiagram.java
index c26d1a0fc1..761de66585 100755
--- a/src/translator/ActivityDiagram.java
+++ b/src/translator/ActivityDiagram.java
@@ -645,4 +645,34 @@ public class ActivityDiagram extends Vector{
}
return nb;
}
+
+ public int getMaximumNbOfGuardsPerChoice() {
+ int nb = 0;
+ ADComponent adc;
+ for(int i=0; i<size(); i++) {
+ adc = (ADComponent)(elementAt(i));
+ if (adc instanceof ADChoice) {
+ nb = Math.max(nb, ((ADChoice)adc).getNbGuard());
+ }
+ }
+ return nb;
+
+ }
+
+ public int getMaximumNbOfGuardsPerSpecialChoice() {
+ int nb = 0;
+ ADComponent adc;
+ ADChoice adch;
+ for(int i=0; i<size(); i++) {
+ adc = (ADComponent)(elementAt(i));
+ if (adc instanceof ADChoice) {
+ adch = (ADChoice)adc;
+ if (adch.isSpecialChoice() && (!adch.isSpecialChoiceAction())) {
+ nb = Math.max(nb, ((ADChoice)adc).getNbGuard());
+ }
+ }
+ }
+ return nb;
+
+ }
}
diff --git a/src/translator/TClass.java b/src/translator/TClass.java
index 3bde60338a..86cea236e3 100755
--- a/src/translator/TClass.java
+++ b/src/translator/TClass.java
@@ -648,6 +648,22 @@ public class TClass {
return ad.getNbOfJunctions();
}
+ public int getMaximumNbOfGuardsPerChoice() {
+ if (ad == null) {
+ return 0;
+ }
+
+ return ad.getMaximumNbOfGuardsPerChoice();
+ }
+
+ public int getMaximumNbOfGuardsPerSpecialChoice() {
+ if (ad == null) {
+ return 0;
+ }
+
+ return ad.getMaximumNbOfGuardsPerSpecialChoice();
+ }
+
/*public void setIgnoredJava(boolean b) {
ignoredJava = b;
diff --git a/src/translator/TURTLEModeling.java b/src/translator/TURTLEModeling.java
index 4ed3cb9739..f23d68c433 100755
--- a/src/translator/TURTLEModeling.java
+++ b/src/translator/TURTLEModeling.java
@@ -152,6 +152,17 @@ public class TURTLEModeling {
}
return null;
}
+
+ public void addAllTClassesEndingWith(ArrayList<TClass> tclasses, String end) {
+ TClass tmp;
+ for(int i=0; i<tclass.size(); i++) {
+ tmp = (TClass)(tclass.elementAt(i));
+ if (tmp.getName().endsWith(end)) {
+ tclasses.add(tmp);
+ System.out.println("Adding tclass:" + tmp.getName());
+ }
+ }
+ }
public int getIndexOf(TClass t) {
return tclass.indexOf(t);
diff --git a/src/translator/TURTLETranslator.java b/src/translator/TURTLETranslator.java
index eb904023fb..146943cec8 100755
--- a/src/translator/TURTLETranslator.java
+++ b/src/translator/TURTLETranslator.java
@@ -1280,9 +1280,9 @@ public class TURTLETranslator {
// End added May 2008
}
/*if (p.getName().indexOf("67") > -1)
- System.out.println(p.getName() + " -> " + s);
+ System.out.println(p.getName() + " -> " + s);
if (s == null) {
- System.out.println("*** NULL S (PROCESS) ***");
+ System.out.println("*** NULL S (PROCESS) ***");
}
if (s.startsWith("null")) {
System.out.println("*** NULL S1 (PROCESS) ***");
@@ -1298,7 +1298,7 @@ public class TURTLETranslator {
params.add(ad.getParam());
actions.add(modifyAction(ad.getActionValue(), languageID));
return translateADActionStateWithParam((ADActionStateWithParam)(ad.getNext(0)));
- // end added May 2008
+ // end added May 2008
} else {
System.out.println("*** NULL PROCESS ***");
return "";
@@ -1530,9 +1530,24 @@ public class TURTLETranslator {
adsnext = (ADActionStateWithParam)(adc.getNext(0));
par = ads.getParam();
if (adsnext.getParam() != par) {
- // One must verify that the second does not use the Param declared in the first one
+ // One must verify that the second does not use the Param declared in the first one!
+ //System.out.println("Param " + par.getName()+ " in use in " + adsnext.getActionValue() + "?");
if (!paramIsUsedIn(par, adsnext.getActionValue())) {
makeProcess = false;
+ //System.out.println("no");
+ } else {
+ //System.out.println("yes");
+ }
+
+ // Must check also in the next ones of the next.
+ if (makeProcess == false) {
+ while(adsnext.getNext(0) instanceof ADActionStateWithParam) {
+ adsnext = (ADActionStateWithParam)(adsnext.getNext(0));
+ //System.out.println("Param " + par.getName()+ " in use in " + adsnext.getActionValue() + "?");
+ if (paramIsUsedIn(par, adsnext.getActionValue())) {
+ makeProcess = true;
+ }
+ }
}
}
}
diff --git a/src/translator/touppaal/RelationTIFUPPAAL.java b/src/translator/touppaal/RelationTIFUPPAAL.java
index 80a67b10f8..de7bcac207 100755
--- a/src/translator/touppaal/RelationTIFUPPAAL.java
+++ b/src/translator/touppaal/RelationTIFUPPAAL.java
@@ -109,8 +109,19 @@ public class RelationTIFUPPAAL {
}
public String getRQuery(TClass _t, ADComponent _adc) {
+ //System.out.println("get RQuery for " + _t.getName());
+
ADComponentLocation adcl = getFirstADComponentLocation(_adc);
TClassTemplate tt = getFirstTClassTemplate(_t);
+
+ if (tt == null) {
+ System.out.println("null tt");
+ }
+
+ if (adcl == null) {
+ System.out.println("null adc1");
+ }
+
if ((tt == null) || (adcl == null)) {
return null;
}
diff --git a/src/translator/touppaal/TURTLE2UPPAAL.java b/src/translator/touppaal/TURTLE2UPPAAL.java
index 19fbe38e7c..d8437a408d 100755
--- a/src/translator/touppaal/TURTLE2UPPAAL.java
+++ b/src/translator/touppaal/TURTLE2UPPAAL.java
@@ -190,7 +190,9 @@ public class TURTLE2UPPAAL {
//makeParallel(nb);
makeSystem(effectiveNb);
+ System.out.println("Enhancing graphical representation ...");
spec.enhanceGraphics();
+ System.out.println("Enhancing graphical representation done");
//System.out.println("relations:" + table.toString());
@@ -218,7 +220,7 @@ public class TURTLE2UPPAAL {
spec.addGlobalDeclaration("int groups__[maxGroups__];\n");
spec.addGlobalDeclaration("urgent broadcast chan endGroup__;\n");
spec.addGlobalDeclaration("urgent broadcast chan goAllTasks__;\n");
-
+
// Has to manage
s = "\nint hasToManage(int tab[maxTasks__]) {\nint i;\nfor(i=0; i<maxTasks__; i++) {\n";
s += "if (tab[i] != -1) {\nreturn 1;\n}\n}\nreturn 0;\n}\n\n";
@@ -242,13 +244,13 @@ public class TURTLE2UPPAAL {
// End task
s = "int endTask(int id) {\nint i, j;\nint taskid;\nint ids[maxTasks__];\nint tmpids[maxTasks__];\n";
- s += "int cpt = 0;\nint currentid;\n\nif (tasks__[id][id] == -3) {\n// I have been preempted\n";
+ s += "int cpt = 0;\nint currentid;\n\nif (tasks__[id][id] == -3) {\n// I have been preempted\n";
s += "tasks__[id][id] = 0;\nreturn -1;\n} else {\n// Normal termination\npreempt(id);\n}\n";
s += "\nfor(i=0; i<maxTasks__; i++) {\nids[i] = -1;\n}\n";
s += "ids[0] = id;\n\nwhile(hasToManage(ids) == 1) {\ncpt = 0;\nfor(i=0; i<maxTasks__; i++) {\n";
- s += "tmpids[i] = ids[i];\nids[i] = -1;\n}\nfor(j=0; j<maxTasks__; j++) {\nif (tmpids[j] != -1) {\n";
- s += "taskid = (tmpids[j] / totalTasks__)*totalTasks__;\ncurrentid = tmpids[j];\ntasks__[currentid][currentid] = 0;\n";
- s += "for(i=taskid; i<(taskid + totalTasks__); i++) {\nif ((i != id) && (tasks__[i][currentid] == preempt__)) {\ntasks__[i][currentid] = 0;\n";
+ s += "tmpids[i] = ids[i];\nids[i] = -1;\n}\nfor(j=0; j<maxTasks__; j++) {\nif (tmpids[j] != -1) {\n";
+ s += "taskid = (tmpids[j] / totalTasks__)*totalTasks__;\ncurrentid = tmpids[j];\ntasks__[currentid][currentid] = 0;\n";
+ s += "for(i=taskid; i<(taskid + totalTasks__); i++) {\nif ((i != id) && (tasks__[i][currentid] == preempt__)) {\ntasks__[i][currentid] = 0;\n";
s += "ids[cpt] = i;\ncpt ++;\n}\n}\n}\n}\n}\nreturn -1;\n}\n\n";
spec.addGlobalDeclaration(Conversion.indentString(s, 2));
@@ -507,7 +509,7 @@ public class TURTLE2UPPAAL {
public UPPAALTemplate newTClassTemplate(TClass t, int id) {
UPPAALTemplate template = new UPPAALTemplate();
if (id != 0) {
- template.setName(t.getName() + "__" + id);
+ template.setName(t.getName() + "___" + id);
} else {
template.setName(t.getName());
}
@@ -520,7 +522,9 @@ public class TURTLE2UPPAAL {
public void makeAttributes(TClass t, UPPAALTemplate template) {
Param p;
Vector params = t.getParamList();
- for(int i=0; i<params.size(); i++) {
+ int i;
+
+ for(i=0; i<params.size(); i++) {
p = (Param)(params.get(i));
if (p.getType() == Param.NAT) {
template.addDeclaration("int ");
@@ -536,6 +540,12 @@ public class TURTLE2UPPAAL {
for(Gate g:gatesWithInternalSynchro) {
template.addDeclaration("int " + t.getName() + "__" + g.getName() + TURTLE2UPPAAL.SYNCID + " = 0;\n");
}
+
+ int nbOfChoice = t.getMaximumNbOfGuardsPerSpecialChoice();
+ for(i=0; i<nbOfChoice; i++) {
+ template.addDeclaration("int choice__" + i + ";\n");
+ }
+
}
public void makeAttributeChoice(TClass t, int id1, int id2) {
@@ -768,7 +778,7 @@ public class TURTLE2UPPAAL {
buildAssignment(tr, action);
table.addADComponentLocation(elt, previous, loc);
-
+
makeElementBehavior(t, template, elt.getNext(0), loc, end, null);
} else {
@@ -835,7 +845,7 @@ public class TURTLE2UPPAAL {
//setSynchronization(tr2, "timeLimitedOfferExpired!");
//addNotSync("timeLimitedOfferExpired");
-
+
makeElementBehavior(t, template, elt.getNext(1), loc2, end, null);
currentX -= STEP_LOOP_X;
@@ -943,15 +953,17 @@ public class TURTLE2UPPAAL {
// Choice
} else if (elt instanceof ADChoice) {
- System.out.println("ADChoice");
+ //System.out.println("ADChoice");
adch = (ADChoice)elt;
if (adch.getNbGuard() == 1) {
if (adch.isGuarded(0)){
- loc = makeTimeInterval(template, previous, "0", ((ADLatency)(elt)).getValue());
+ //loc = makeTimeInterval(template, previous, "0", ((ADLatency)(elt)).getValue());
//table.addADComponentLocation(elt, previous, loc);
- previous = loc;
+ //previous = loc;
+
+ previous.setUrgent();
loc = addLocation(template);
loc.setUrgent();
@@ -967,44 +979,14 @@ public class TURTLE2UPPAAL {
makeElementBehavior(t, template, elt.getNext(0), previous, end, null);
}
} else {
- //System.out.println("ADChoice: testing");
- if (choicesDeterministic) {
- //System.out.println("Choice is deterministic");
- int tmpX = currentX;
- for(i=0; i<elt.getNbNext(); i++){
- //System.out.println("Choice is deterministic i=" + i);
- String gua = null;
- if (adch.isGuarded(i)) {
- gua = convertGuard(adch.getGuard(i));
- }
-
- if (gua == null) {
- gua = "";
- }
-
- gua = gua.trim();
-
- if (gua.length() == 0) {
- System.out.println("New choice system");
- table.addADComponentLocation(elt, previous, previous);
- makeElementBehavior(t, template, elt.getNext(i), previous, end, null);
- currentX += 2 * STEP_LOOP_X;
- } else {
-
- loc = addLocation(template);
- tr = addTransition(template, previous, loc);
- setGuard(tr, gua);
+ if (adch.isSpecialChoiceDelay()) {
+
+ // Must check whether some actions are delayed or not
+ if (adch.isSpecialChoiceAction()) {
- table.addADComponentLocation(elt, previous, loc);
-
- makeElementBehavior(t, template, elt.getNext(i), loc, end, null);
- currentX += 2 * STEP_LOOP_X;
- }
- }
- } else {
- /*if (adch.choiceFollowedWithADActionStateWithGates()) {
- int tmpX = currentX;
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));
+
String gua = null;
if (adch.isGuarded(i)) {
gua = convertGuard(adch.getGuard(i));
@@ -1012,187 +994,239 @@ public class TURTLE2UPPAAL {
table.addADComponentLocation(elt, previous, previous);
makeElementBehavior(t, template, elt.getNext(i), previous, end, gua);
currentX += 2 * STEP_LOOP_X;
- }*/
- if (adch.isSpecialChoiceDelay()) {
+ }
+ } else {
+ //System.out.println("Special choice delay");
+
int tmpX = currentX;
+ int next = 0;
+ ADComponent elt1;
+ boolean delayed;
+ String gua = null;
+
+ // Initialization
+ String init = "h__ = 0";
for(i=0; i<elt.getNbNext(); i++){
- String gua = null;
- String guadelay = null;
- if (adch.isGuarded(i)) {
- gua = convertGuard(adch.getGuard(i));
- }
+ //System.out.println("Special choice delay / Task " + t.getName() + ": Choice is deterministic i=" + i + " with guard =" + adch.getGuard(i));
+
+ elt1 = elt.getNext(i);
- if (elt.getNext(i) instanceof ADDelay) {
- guadelay = ((ADDelay)(elt.getNext(i))).getValue();
- guadelay = "(h__ >= (" + guadelay + "))";
+ if (elt1 instanceof ADDelay) {
+ init = init + ", choice__" + i + " = max(0, " + ((ADDelay)(elt1)).getValue() + ")";
}
- if (elt.getNext(i) instanceof ADLatency) {
- guadelay = ((ADLatency)(elt.getNext(i))).getValue();
- guadelay = "(h__ >= (" + guadelay + "))";
+ if (elt1 instanceof ADLatency) {
+ init = init + ", choice__" + i + " = 0";
}
- if (elt.getNext(i) instanceof ADTimeInterval) {
- guadelay = ((ADTimeInterval)(elt.getNext(i))).getMinValue();
- guadelay = "(h__ >= (" + guadelay + "))";
+ if (elt1 instanceof ADTimeInterval) {
+ init = init + ", choice__" + i + " = max(0, " + ((ADTimeInterval)(elt1)).getMinValue() + ")";
}
-
- if (gua == null) {
- gua = guadelay;
- } else {
- if (guadelay != null) {
- gua = "((" + gua + " && " + guadelay + ")";
- }
+ }
+ loc = addRLocation(template);
+ previous.setCommitted();
+ tr = addRTransition(template, previous, loc);
+ setAssignment(tr, init);
+
+
+ // Setting randomnly the value of non-deterministic time
+ for(i=0; i<elt.getNbNext(); i++){
+ elt1 = elt.getNext(i);
+ if (elt1 instanceof ADLatency) {
+ tr = addRTransition(template, loc, loc);
+ setGuard(tr, "choice__" + i + " <" + ((ADLatency)(elt1)).getValue());
+ setAssignment(tr, "choice__" + i + " = choice__" + i + " + 1");
}
- table.addADComponentLocation(elt, previous, previous);
-
- makeElementBehavior(t, template, elt.getNext(i), previous, end, gua);
- currentX += 2 * STEP_LOOP_X;
+ if (elt1 instanceof ADTimeInterval) {
+ tr = addRTransition(template, loc, loc);
+ setGuard(tr, "choice__" + i + " <" + ((ADTimeInterval)(elt1)).getMaxValue());
+ setAssignment(tr, "choice__" + i + " = choice__" + i + " + 1");
+ }
}
- } /*else if (adch.isElseChoice()) {
- System.out.println("Else choice detected");
- int tmpX = currentX;
- previous.setUrgent();
+
+ loc1 = addRLocation(template);
+ loc.setCommitted();
+ tr = addRTransition(template, loc, loc1);
+
+ table.addADComponentLocation(elt, previous, loc1);
+
for(i=0; i<elt.getNbNext(); i++){
- loc = addLocation(template);
- tr = addTransition(template, previous, loc);
- action = convertGuard(adch.getGuard(i));
- setGuard(tr, action);
+ delayed = false;
+ elt1 = elt.getNext(i);
- table.addADComponentLocation(elt, previous, loc);
+ gua = null;
+ // An action follows the guard #i
+ if (adch.isGuarded(i)) {
+ gua = convertGuard(adch.getGuard(i));
+ }
- makeElementBehavior(t, template, elt.getNext(i), loc, end, null);
- currentX += 2 * STEP_LOOP_X;
+ if ((elt1 instanceof ADDelay) || (elt1 instanceof ADLatency) || (elt1 instanceof ADTimeInterval)){
+ delayed = true;
+ }
+
+ if (!delayed) {
+ makeElementBehavior(t, template, elt.getNext(i), loc1, end, gua);
+ currentX += 2 * STEP_LOOP_X;
+ } else {
+ String guadelay = "(choice__" + i + " >0) && ( h__>= choice__" + i + ")";
+ if (gua != null) {
+ guadelay = "(" + gua + ") && (" + guadelay + ")";
+ }
+ tr = addRTransition(template, loc1, loc1);
+ setGuard(tr, guadelay);
+ setAssignment(tr, "choice__" + i + " = 0");
+
+ guadelay = "choice__" + i + " == 0";
+ if (gua == null) {
+ gua = guadelay;
+ } else {
+ gua = "(" + gua + ") && (" + guadelay + ")";
+ }
+ makeElementBehavior(t, template, elt1.getNext(0), loc1, end, gua);
+ currentX += 2 * STEP_LOOP_X;
+ }
+ }
+ }
+ //System.out.println("ADChoice: testing");
+ } else if ((choicesDeterministic) || (adch.isElseChoice())) {
+ //System.out.println("Choice is deterministic");
+ int tmpX = currentX;
+ previous.setCommitted();
+ for(i=0; i<elt.getNbNext(); i++){
+ //System.out.println("Task " + t.getName() + ": Choice is deterministic i=" + i + " with guard =" + adch.getGuard(i));
+ String gua = null;
+ if (adch.isGuarded(i)) {
+ gua = convertGuard(adch.getGuard(i));
}
- }*/ else {
- System.out.println("Irregular choice");
- setMultiProcess(template);
- addParallel(t, template);
-
- //start other tasks
- loc = previous;
+ if (gua == null) {
+ gua = "";
+ }
- loc.setUrgent();
- loc3 = addLocation(template);
- loc3.setCommitted();
- tr1 = addRTransition(template, loc, loc3);
- setSynchronization(tr1, "lockmutextask__!");
- //addAssignment(tr1, "gotasks__ = 0, \nstartingid__ = myid__,\npreemptid__ = myid__,\ngroupid__= firstGroupId(),\n waitgroupid__ = groupid__");
- addAssignment(tr1, "gotasks__ = 0, \nstartingid__ = myid__,\npreemptid__ = myid__,\ngroupid__= mygroupid__");
- loc = loc3;
+ gua = gua.trim();
- //System.out.println("Managing preempt");
- index = currentX;
- for(i=1; i<elt.getNbNext(); i++){
- loc2 = makePreemptFromInit(t, template);
- loc1 = addLocation(template);
- loc1.setUrgent();
- tr1 = addTransition(template, loc, loc1);
- if (i!=0) {
- setAssignment(tr1, "locid__ = " + loc2.int_id + ",\ntaskid__ = firstFree(myid__),\nmygroupid__ = groupid__");
+ if (gua.length() == 0) {
+ //System.out.println("New choice system");
+ if (elt.getNext(i) instanceof ADChoice) {
+ makeElementBehavior(t, template, elt.getNext(i), previous, end, null);
} else {
- setAssignment(tr1, "locid__ = " + loc2.int_id + ",\ntaskid__ = firstFree(myid__)");
- }
- loc3 = addLocation(template);
- loc3.setCommitted();
- tr1 = addTransition(template, loc1, loc3);
- setSynchronization(tr1, "begintask__!");
- setAssignment(tr1, makeSetParam(t));
- loc = loc3;
- currentX += 2 * STEP_LOOP_X;
- // Manage guard if applicable
- //System.out.println("Guard #" + i);
- if (adch.isGuarded(i)) {
- loc4 = addRLocation(template);
- tr1 = addTransition(template, loc2, loc4);
- action = convertGuard(adch.getGuard(i));
- //System.out.println("action=" + action);
- setGuard(tr1, action);
- loc2.setUrgent();
- //System.out.println("guard set");
- loc5 = addRLocation(template);
- tr1 = addTransition(template, loc2, loc5);
- action = convertGuard("!(" + adch.getGuard(i) + ")");
- setGuard(tr1, action);
+ loc = addLocation(template);
+ tr = addTransition(template, previous, loc);
-
- loc2 = loc4;
+ table.addADComponentLocation(elt, previous, previous);
+ makeElementBehavior(t, template, elt.getNext(i), loc, end, null);
+ currentX += 2 * STEP_LOOP_X;
}
+ } else {
+
+ loc = addLocation(template);
+ tr = addTransition(template, previous, loc);
+ setGuard(tr, gua);
- table.addADComponentLocation(elt, previous, loc2);
+ table.addADComponentLocation(elt, previous, loc);
- makeElementBehavior(t, template, elt.getNext(i), loc2, end, null);
+ makeElementBehavior(t, template, elt.getNext(i), loc, end, null);
+ currentX += 2 * STEP_LOOP_X;
+ }
+ }
+ } else {
+
+ System.out.println("Irregular choice");
+ setMultiProcess(template);
+ addParallel(t, template);
+
+ //start other tasks
+ loc = previous;
+
+ loc.setUrgent();
+ loc3 = addLocation(template);
+ loc3.setCommitted();
+ tr1 = addRTransition(template, loc, loc3);
+ setSynchronization(tr1, "lockmutextask__!");
+ //addAssignment(tr1, "gotasks__ = 0, \nstartingid__ = myid__,\npreemptid__ = myid__,\ngroupid__= firstGroupId(),\n waitgroupid__ = groupid__");
+ addAssignment(tr1, "gotasks__ = 0, \nstartingid__ = myid__,\npreemptid__ = myid__,\ngroupid__= mygroupid__");
+ loc = loc3;
+
+ //System.out.println("Managing preempt");
+ index = currentX;
+ for(i=1; i<elt.getNbNext(); i++){
+ loc2 = makePreemptFromInit(t, template);
+ loc1 = addLocation(template);
+ loc1.setUrgent();
+ tr1 = addTransition(template, loc, loc1);
+ if (i!=0) {
+ setAssignment(tr1, "locid__ = " + loc2.int_id + ",\ntaskid__ = firstFree(myid__),\nmygroupid__ = groupid__");
+ } else {
+ setAssignment(tr1, "locid__ = " + loc2.int_id + ",\ntaskid__ = firstFree(myid__)");
}
-
- /*loc3 = addLocation(template);
- tr1 = addTransition(template, loc, loc3);
- setAssignment(tr1, "gotasks__ = " + (elt.getNbNext() - 1));
- loc2 = addLocation(template);
- tr1 = addTransition(template, loc3, loc2);
- setSynchronization(tr1, "unlockmutextask__!");
- setGuard(tr1, "gotasks__ == 0");
- //setAssignment(tr1, "makeParallel(myid__, startingid__)");
-
loc3 = addLocation(template);
- tr1 = addTransition(template, loc2, loc3);
- setSynchronization(tr1, "endGroup__[waitgroupid__]?");
-
- makeEnd(template, loc3);*/
-
- loc3 = addRLocation(template);
- //loc3.setUrgent();
loc3.setCommitted();
- tr1 = addTransition(template, loc, loc3);
- //setAssignment(tr1, "gotasks__ = " + (elt.getNbNext() - 1));
- setSynchronization(tr1, "goAllTasks__!");
-
- loc2 = addRLocation(template);
- tr1 = addTransition(template, loc3, loc2);
- setSynchronization(tr1, "unlockmutextask__!");
- setGuard(tr1, "gotasks__ == 0");
- setAssignment(tr1, "makeParallel(myid__, startingid__),\nmakePreempt(myid__, preemptid__, startingid__)");
-
- if (adch.isGuarded(0)) {
+ tr1 = addTransition(template, loc1, loc3);
+ setSynchronization(tr1, "begintask__!");
+ setAssignment(tr1, makeSetParam(t));
+ loc = loc3;
+ currentX += 2 * STEP_LOOP_X;
+ // Manage guard if applicable
+ //System.out.println("Guard #" + i);
+ if (adch.isGuarded(i)) {
loc4 = addRLocation(template);
tr1 = addTransition(template, loc2, loc4);
- loc2.setUrgent();
- action = convertGuard(adch.getGuard(0));
+ action = convertGuard(adch.getGuard(i));
+ //System.out.println("action=" + action);
setGuard(tr1, action);
-
+ loc2.setUrgent();
+ //System.out.println("guard set");
loc5 = addRLocation(template);
tr1 = addTransition(template, loc2, loc5);
- action = convertGuard("!(" + adch.getGuard(0) + ")");
+ action = convertGuard("!(" + adch.getGuard(i) + ")");
setGuard(tr1, action);
+
+
loc2 = loc4;
}
- loc = loc2;
- currentX += 2 * STEP_LOOP_X;
+ table.addADComponentLocation(elt, previous, loc2);
- table.addADComponentLocation(elt, previous, loc);
+ makeElementBehavior(t, template, elt.getNext(i), loc2, end, null);
+ }
+
+ loc3 = addRLocation(template);
+ //loc3.setUrgent();
+ loc3.setCommitted();
+ tr1 = addTransition(template, loc, loc3);
+ //setAssignment(tr1, "gotasks__ = " + (elt.getNbNext() - 1));
+ setSynchronization(tr1, "goAllTasks__!");
+
+ loc2 = addRLocation(template);
+ tr1 = addTransition(template, loc3, loc2);
+ setSynchronization(tr1, "unlockmutextask__!");
+ setGuard(tr1, "gotasks__ == 0");
+ setAssignment(tr1, "makeParallel(myid__, startingid__),\nmakePreempt(myid__, preemptid__, startingid__)");
+
+ if (adch.isGuarded(0)) {
+ loc4 = addRLocation(template);
+ tr1 = addTransition(template, loc2, loc4);
+ loc2.setUrgent();
+ action = convertGuard(adch.getGuard(0));
+ setGuard(tr1, action);
- makeElementBehavior(t, template, elt.getNext(0), loc, end, null);
- currentX = index;
+ loc5 = addRLocation(template);
+ tr1 = addTransition(template, loc2, loc5);
+ action = convertGuard("!(" + adch.getGuard(0) + ")");
+ setGuard(tr1, action);
+ loc2 = loc4;
}
+
+ loc = loc2;
+ currentX += 2 * STEP_LOOP_X;
+
+ table.addADComponentLocation(elt, previous, loc);
+
+ makeElementBehavior(t, template, elt.getNext(0), loc, end, null);
+ currentX = index;
}
}
- return;
- // Start activities in parallel -> all of them may preempt the others
-
-
-
- // Quite complex -> use other functions to continue
- /*if (adch.isSpecialChoice()) {
- makeSpecialChoice(t, template, elt, previous, end, adch);
- System.out.println("Special choice encountered");
- return;
- } else {
- // Choice is considered as a "regular" choice and not a LOTOS choice
- System.out.println("Warning: elt = " + elt + " is not a special choice");
- makeChoice(t, template, elt, previous, end, adch);
- }*/
// Sequence
} else if (elt instanceof ADSequence) {
@@ -1378,7 +1412,7 @@ public class TURTLE2UPPAAL {
}
return;
- } else if (elt instanceof ADPreempt) {
+ } else if (elt instanceof ADPreempt) {
if (elt.getNbNext() == 0) {
table.addADComponentLocation(elt, previous, previous);
makeElementBehavior(t, template, elt.getNext(0), previous, end, null);
@@ -1486,7 +1520,7 @@ public class TURTLE2UPPAAL {
UPPAALLocation loc, loc1;
UPPAALTransition tr, tr1;
loc1 = addRLocation(template);
- previous.setUrgent();
+ previous.setCommitted();
tr1 = addRTransition(template, previous, loc1);
setAssignment(tr1, "h__ = 0");
loc = addRLocation(template);
@@ -1599,7 +1633,7 @@ public class TURTLE2UPPAAL {
return loc2;
}
- // Assumes adch is a not special choice
+ // Assumes adch is a not special choice
public void makeChoice(TClass t, UPPAALTemplate template, ADComponent elt, UPPAALLocation previous, UPPAALLocation end, ADChoice adch) {
int nbG = adch.getNbGuard();
UPPAALLocation loc1, loc2;
@@ -2075,8 +2109,8 @@ public class TURTLE2UPPAAL {
}
}
-
- public UPPAALLocation addLocation(UPPAALTemplate template) {
+
+ public UPPAALLocation addLocation(UPPAALTemplate template) {
UPPAALLocation loc = new UPPAALLocation();
loc.idPoint.x = currentX;
loc.idPoint.y = currentY;
@@ -2086,9 +2120,9 @@ public class TURTLE2UPPAAL {
currentX += STEP_X;
currentY += STEP_Y;
return loc;
- }
-
- public UPPAALLocation addRLocation(UPPAALTemplate template) {
+ }
+
+ public UPPAALLocation addRLocation(UPPAALTemplate template) {
UPPAALLocation loc = new UPPAALLocation();
loc.idPoint.x = currentX;
loc.idPoint.y = currentY;
@@ -2104,7 +2138,7 @@ public class TURTLE2UPPAAL {
}
return loc;
- }
+ }
public UPPAALLocation addRUnlockLocation(UPPAALTemplate template) {
UPPAALLocation loc = new UPPAALLocation();
@@ -2123,9 +2157,9 @@ public class TURTLE2UPPAAL {
}
return loc;
- }
-
- public UPPAALLocation addRUnlockTaskLocation(UPPAALTemplate template) {
+ }
+
+ public UPPAALLocation addRUnlockTaskLocation(UPPAALTemplate template) {
UPPAALLocation loc = new UPPAALLocation();
loc.idPoint.x = currentX;
loc.idPoint.y = currentY;
@@ -2142,7 +2176,7 @@ public class TURTLE2UPPAAL {
}
return loc;
- }
+ }
public void addRandomNailPoint(UPPAALTransition tr) {
int x = 0, y = 0;
@@ -2152,8 +2186,8 @@ public class TURTLE2UPPAAL {
tr.points.add(new Point(x, y));
}
}
-
- public UPPAALTransition addTransition(UPPAALTemplate template, UPPAALLocation loc1, UPPAALLocation loc2) {
+
+ public UPPAALTransition addTransition(UPPAALTemplate template, UPPAALLocation loc1, UPPAALLocation loc2) {
UPPAALTransition tr = new UPPAALTransition();
tr.sourceLoc = loc1;
tr.destinationLoc = loc2;
@@ -2168,17 +2202,17 @@ public class TURTLE2UPPAAL {
tr.points.add(new Point(x, y));
}*/
return tr;
- }
+ }
- public UPPAALTransition addEndTransition(UPPAALTemplate template, UPPAALLocation loc1) {
+ public UPPAALTransition addEndTransition(UPPAALTemplate template, UPPAALLocation loc1) {
UPPAALTransition tr = addTransition(template, loc1, template.getInitLocation());
//template.addTransition(tr);
setEndAssignment(tr);
addRandomNailPoint(tr);
return tr;
- }
-
- public UPPAALTransition addRTransition(UPPAALTemplate template, UPPAALLocation loc1, UPPAALLocation loc2) {
+ }
+
+ public UPPAALTransition addRTransition(UPPAALTemplate template, UPPAALLocation loc1, UPPAALLocation loc2) {
UPPAALTransition tr = new UPPAALTransition();
tr.sourceLoc = loc1;
tr.destinationLoc = loc2;
@@ -2191,24 +2225,24 @@ public class TURTLE2UPPAAL {
addRandomNailPoint(tr);
// Nails?
return tr;
- }
-
- public UPPAALTransition addActionTransition(UPPAALTemplate template, UPPAALLocation loc1, UPPAALLocation loc2) {
+ }
+
+ public UPPAALTransition addActionTransition(UPPAALTemplate template, UPPAALLocation loc1, UPPAALLocation loc2) {
UPPAALTransition tr = addRTransition(template, loc1, loc2);
if (!isRegularTClass) {
addAssignment(tr, "preempt(myid__),\nh__ = 0");
}
addRandomNailPoint(tr);
return tr;
- }
-
- public void setSynchronization(UPPAALTransition tr, String s) {
+ }
+
+ public void setSynchronization(UPPAALTransition tr, String s) {
tr.synchronization = modifyString(s);
tr.synchronizationPoint.x = (tr.sourceLoc.idPoint.x + tr.destinationLoc.idPoint.x)/2 + SYNCHRO_X;
tr.synchronizationPoint.y = (tr.sourceLoc.idPoint.y + tr.destinationLoc.idPoint.y)/2 + SYNCHRO_Y;
- }
-
- public void addGuard(UPPAALTransition tr, String s) {
+ }
+
+ public void addGuard(UPPAALTransition tr, String s) {
if ((tr.guard == null) || (tr.guard.length() < 2)){
tr.guard = modifyString(s);
} else {
@@ -2216,25 +2250,25 @@ public class TURTLE2UPPAAL {
}
tr.guardPoint.x = (tr.sourceLoc.idPoint.x + tr.destinationLoc.idPoint.x)/2 + GUARD_X;
tr.guardPoint.y = (tr.sourceLoc.idPoint.y + tr.destinationLoc.idPoint.y)/2 + GUARD_Y;
- }
-
- public void setInvariant(UPPAALLocation loc, String s) {
- loc.setInvariant(modifyString(s));
- }
-
- public void setGuard(UPPAALTransition tr, String s) {
+ }
+
+ public void setInvariant(UPPAALLocation loc, String s) {
+ loc.setInvariant(modifyString(s));
+ }
+
+ public void setGuard(UPPAALTransition tr, String s) {
tr.guard = modifyString(s);
tr.guardPoint.x = (tr.sourceLoc.idPoint.x + tr.destinationLoc.idPoint.x)/2 + GUARD_X;
tr.guardPoint.y = (tr.sourceLoc.idPoint.y + tr.destinationLoc.idPoint.y)/2 + GUARD_Y;
- }
-
- public void setAssignment(UPPAALTransition tr, String s) {
+ }
+
+ public void setAssignment(UPPAALTransition tr, String s) {
tr.assignment = modifyString(s);
tr.assignmentPoint.x = (tr.sourceLoc.idPoint.x + tr.destinationLoc.idPoint.x)/2 + ASSIGN_X;
tr.assignmentPoint.y = (tr.sourceLoc.idPoint.y + tr.destinationLoc.idPoint.y)/2 + ASSIGN_Y;
- }
-
- public void addAssignment(UPPAALTransition tr, String s) {
+ }
+
+ public void addAssignment(UPPAALTransition tr, String s) {
if (s.length() <1) {
return;
}
@@ -2246,17 +2280,17 @@ public class TURTLE2UPPAAL {
tr.assignmentPoint.x = (tr.sourceLoc.idPoint.x + tr.destinationLoc.idPoint.x)/2 + ASSIGN_X;
tr.assignmentPoint.y = (tr.sourceLoc.idPoint.y + tr.destinationLoc.idPoint.y)/2 + ASSIGN_Y;
- }
-
- public void setEndAssignment(UPPAALTransition tr) {
+ }
+
+ public void setEndAssignment(UPPAALTransition tr) {
if (!isRegularTClass) {
tr.assignment = "endTask(myid__)";
}
tr.assignmentPoint.x = (tr.sourceLoc.idPoint.x + tr.destinationLoc.idPoint.x)/2 + ASSIGN_X;
tr.assignmentPoint.y = (tr.sourceLoc.idPoint.y + tr.destinationLoc.idPoint.y)/2 + ASSIGN_Y;
- }
-
- public void makeSystem(int nb) {
+ }
+
+ public void makeSystem(int nb) {
ListIterator iterator = spec.getTemplates().listIterator();
UPPAALTemplate template;
String system = "system ";
@@ -2308,7 +2342,7 @@ public class TURTLE2UPPAAL {
}
spec.addInstanciation(dec+system);
- }
+ }
public void setMultiProcess(UPPAALTemplate t) {
System.out.println("Setting multiprocess: " + t.getName());
@@ -2317,24 +2351,24 @@ public class TURTLE2UPPAAL {
}
multiprocess = true;
}
-
- public String modifyString(String _input) {
- try {
+
+ public String modifyString(String _input) {
+ try {
//_input = Conversion.replaceAllString(_input, "&&", "&&");
//_input = Conversion.changeBinaryOperatorWithUnary(_input, "div", "/");
//_input = Conversion.changeBinaryOperatorWithUnary(_input, "mod", "%");
//_input = Conversion.replaceAllChar(_input, '<', "<");
//_input = Conversion.replaceAllChar(_input, '>', ">");
_input = Conversion.replaceAllStringNonAlphanumerical(_input, "mod", "%");
- } catch (Exception e) {
+ } catch (Exception e) {
e.printStackTrace();
System.out.println("Exception when changing binary operator in " + _input);
- }
+ }
//System.out.println("Modified string=" + _input);
- return _input;
- }
-
- public String convertGuard(String g) {
+ return _input;
+ }
+
+ public String convertGuard(String g) {
if (g == null) {
return "";
}
@@ -2345,7 +2379,7 @@ public class TURTLE2UPPAAL {
String action = Conversion.replaceAllChar(g, '[', "");
action = Conversion.replaceAllChar(action, ']', "");
return modifyString(action.trim());
- }
+ }
+
-
}
\ No newline at end of file
diff --git a/src/ui/CorrespondanceTGElement.java b/src/ui/CorrespondanceTGElement.java
index a9110bee86..c30cdf36f2 100755
--- a/src/ui/CorrespondanceTGElement.java
+++ b/src/ui/CorrespondanceTGElement.java
@@ -189,15 +189,17 @@ public class CorrespondanceTGElement {
}
ArrayList<ADComponent> listAD = new ArrayList<ADComponent>();
- ADComponent adc;
+ ArrayList<ADComponent> listADs;
+
for(TGComponent tgc:_list) {
- adc = getADComponent(tgc);
- if (adc != null) {
- listAD.add(adc);
- //System.out.println("Adding adc=" + adc + " from tgc=" + tgc);
+ listADs = getADComponents(tgc);
+ //System.out.println("List size:" + listADs.size());
+ if (listADs.size() > 0) {
+ listAD.addAll(listADs);
}
}
+ //System.out.println("Final List size:" + listAD.size());
return listAD;
}
@@ -231,6 +233,27 @@ public class CorrespondanceTGElement {
return null;
}
+ public ArrayList<ADComponent> getADComponents(TGComponent tgc) {
+ ArrayList<ADComponent> list = new ArrayList<ADComponent>();
+ TGComponent tmptgc;
+ Object o;
+
+ int index = tg.indexOf(tgc);
+ if (index == -1) {
+ return list;
+ }
+
+ for(int i=0; i<tg.size(); i++) {
+ tmptgc = (TGComponent)(tg.elementAt(i));
+ if (tmptgc == tgc) {
+ o = data.elementAt(i);
+ list.add((ADComponent)o);
+ }
+ }
+
+ return list;
+ }
+
public HwNode getHwNode(TGComponent tgc) {
int index = tg.indexOf(tgc);
if ((index != -1) && (data.size() > index)) {
diff --git a/src/ui/DesignPanelTranslator.java b/src/ui/DesignPanelTranslator.java
index 5d9068ee5f..a30dd99786 100755
--- a/src/ui/DesignPanelTranslator.java
+++ b/src/ui/DesignPanelTranslator.java
@@ -405,8 +405,9 @@ public class DesignPanelTranslator {
return;
}
s1 = TURTLEModeling.addTypeToDataReceiving(t, s1);
- //System.out.println("Adding type done s1=" + s1);
+
adag.setActionValue(s1);
+ //System.out.println("Adding correspondance tgc=" + tgc + "adag=" + adag);
listE.addCor(adag, tgc);
} else if ((p != null) && (nbActions == 1)){
//System.out.println("Action state with param found " + p.getName() + " value:" + t.getExprValueFromActionState(s));
diff --git a/src/ui/GTURTLEModeling.java b/src/ui/GTURTLEModeling.java
index 4015bb16ab..f8a1374f07 100755
--- a/src/ui/GTURTLEModeling.java
+++ b/src/ui/GTURTLEModeling.java
@@ -5,7 +5,7 @@
* 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
+ * and at last to almalow the analysis of formal validation traces
* obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
* from INRIA Rhone-Alpes.
*
@@ -336,15 +336,18 @@ public class GTURTLEModeling {
TURTLE2UPPAAL turtle2uppaal = new TURTLE2UPPAAL(tm);
turtle2uppaal.setChoiceDeterministic(choices);
uppaal = turtle2uppaal.generateUPPAAL(debug, nb);
+ System.out.println("Building relation table");
uppaalTIFTable = turtle2uppaal.getRelationTIFUPPAAL();
+ System.out.println("Building relation table done");
uppaalTMLTable = null;
languageID = UPPAAL;
mgui.setMode(MainGUI.UPPAAL_OK);
try {
+ System.out.println("Saving specification in " + path + "\n");
turtle2uppaal.saveInFile(path);
- System.out.println("UPPAAL specification has been generated in " + path);
+ System.out.println("UPPAAL specification has been generated in " + path + "\n");
return true;
} catch (FileException fe) {
System.out.println("Exception: " + fe.getMessage());
@@ -375,6 +378,7 @@ public class GTURTLEModeling {
//System.out.println("Searching for queries");
TURTLEPanel tp = mgui.getCurrentTURTLEPanel();
ArrayList<TGComponent> list = new ArrayList<TGComponent>();
+ ArrayList<TClass> tclasses;
tp.getAllCheckableTGComponent(list);
ArrayList<String> listQ = new ArrayList<String>();
@@ -382,6 +386,8 @@ public class GTURTLEModeling {
if (uppaalTIFTable != null) {
ArrayList<ADComponent> listAD = listE.getADComponentCorrespondance(list);
+ //System.out.println("List size:" + listAD.size());
+
if (listAD == null) {
return null;
}
@@ -391,11 +397,19 @@ public class GTURTLEModeling {
for(ADComponent adc:listAD) {
if (adc != null) {
t = tm.findTClass(adc);
+ //System.out.println("Found class:" + t.getName());
if (t!= null) {
- s = uppaalTIFTable.getRQuery(t, adc);
- if (s != null) {
- //System.out.println("Adding query:" + s);
- listQ.add(s + "$" + adc);
+ tclasses = new ArrayList<TClass>();
+ tclasses.add(t);
+ // For handling tobjects
+ tm.addAllTClassesEndingWith(tclasses, "_" + t.getName());
+ for(TClass tc: tclasses) {
+ //System.out.println("Analyzing class:" + tc.getName());
+ s = uppaalTIFTable.getRQuery(tc, adc);
+ if (s != null) {
+ //System.out.println("Adding query:" + s);
+ listQ.add(s + "$" + adc);
+ }
}
}
}
@@ -2324,32 +2338,8 @@ public class GTURTLEModeling {
}
}
- //Method added by Solange
-// public int countPrimitives(TGComponent comp)
-// {
-// int cuenta=0, nb=0;
-// if (comp.getType()==TGComponentManager.PROCSD_COMPONENT)
-// {
-// nb=comp.getNbInternalTGComponent();
-// if(nb==0) // does not have ports, inner components, etc
-// {
-// cuenta++;
-// }
-// else
-// {
-// for (int j=0;j<nb;j++)
-// {
-// TGComponent tmp=comp.getInternalTGComponent(j);
-// cuenta= cuenta + countPrimitives(tmp);
-// }
-// }
-// }
-// return(cuenta);
-// }
- //until here
-
public void copyModelingFromXML(TDiagramPanel tdp, String s, int X, int Y) throws MalformedModelingException {
- //System.out.println("copyModelingFromXML");
+ System.out.println("copyModelingFromXML");
//System.out.println(s);
//System.out.println("copyModelingFromXML:");
//LinkedList ComponentsList=tdp.getComponentList();
@@ -2359,6 +2349,9 @@ public class GTURTLEModeling {
int cuenta=1;
s = decodeString(s);
+
+ //System.out.println("copy=" + s);
+
ByteArrayInputStream bais = new ByteArrayInputStream(s.getBytes());
if ((dbf == null) || (db == null)) {
throw new MalformedModelingException();
@@ -2396,6 +2389,8 @@ public class GTURTLEModeling {
// Managing diagrams
if (tdp instanceof TClassDiagramPanel) {
+ System.out.println("TClassDiagramPanel copy");
+
nl = doc.getElementsByTagName("TClassDiagramPanelCopy");
docCopy = doc;
@@ -2444,6 +2439,7 @@ public class GTURTLEModeling {
docCopy = null;
} else if (tdp instanceof TActivityDiagramPanel) {
+ System.out.println("TActivityDiagramPanel copy");
nl = doc.getElementsByTagName("TActivityDiagramPanelCopy");
if (nl == null) {
@@ -3183,8 +3179,8 @@ public class GTURTLEModeling {
return sb.toString();
}
- // Assumes a class diagram is already created
public void loadModelingFromXML(String s) throws MalformedModelingException {
+
if (s == null) {
return;
}
@@ -3952,8 +3948,8 @@ public class GTURTLEModeling {
try {
NodeList activityDiagramNl = docCopy.getElementsByTagName("TActivityDiagramPanel");
- //System.out.println("Loading activity diagram of " + newValue + "Before : " + oldValue);
- //System.out.println(docCopy);
+ System.out.println("Loading activity diagram of " + newValue + "Before : " + oldValue);
+ System.out.println(docCopy);
if (activityDiagramNl == null) {
throw new MalformedModelingException();
diff --git a/src/ui/MainGUI.java b/src/ui/MainGUI.java
index 4e3d709e40..be35b22a5e 100755
--- a/src/ui/MainGUI.java
+++ b/src/ui/MainGUI.java
@@ -2230,6 +2230,14 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener {
boolean b = false;
boolean ret = false;
+ if (file == null) {
+ JOptionPane.showMessageDialog(frame,
+ "The project must be saved before any simulation or formal verification can be performed",
+ "Syntax analysis failed",
+ JOptionPane.INFORMATION_MESSAGE);
+ return false;
+ }
+
TURTLEPanel tp = getCurrentTURTLEPanel();
if (tp instanceof AnalysisPanel) {
try {
diff --git a/src/ui/TDiagramPanel.java b/src/ui/TDiagramPanel.java
index 60472c428e..340906b8d8 100755
--- a/src/ui/TDiagramPanel.java
+++ b/src/ui/TDiagramPanel.java
@@ -505,18 +505,11 @@ public abstract class TDiagramPanel extends JPanel implements GenericTree {
if (s == null) {
return null;
}
- //Added by Solange
- //StringBuffer s2 =SMDInXML(false);
StringBuffer sb = new StringBuffer(getXMLHead());
sb.append("\n");
sb.append(s);
sb.append("\n");
- //Added by Solange
- //sb.append(s2);
- //sb.append("\n");
- //
- //System.out.println("Tail of " + toString());
sb.append(getXMLTail());
return sb;
}
diff --git a/src/ui/ad/TActivityDiagramToolBar.java b/src/ui/ad/TActivityDiagramToolBar.java
index f93f0292db..0bf7d79476 100755
--- a/src/ui/ad/TActivityDiagramToolBar.java
+++ b/src/ui/ad/TActivityDiagramToolBar.java
@@ -81,6 +81,11 @@ public class TActivityDiagramToolBar extends TToolBar {
mgui.actions[TGUIAction.AD_ARRAY_SET].setEnabled(b);
mgui.actions[TGUIAction.ACT_TOGGLE_JAVA].setEnabled(b);
mgui.actions[TGUIAction.ACT_ENHANCE].setEnabled(b);
+
+ mgui.actions[TGUIAction.ACT_ZOOM_MORE].setEnabled(false);
+ mgui.actions[TGUIAction.ACT_ZOOM_LESS].setEnabled(false);
+ mgui.actions[TGUIAction.ACT_SHOW_ZOOM].setEnabled(false);
+ mgui.updateZoomInfo();
}
protected void setButtons() {
diff --git a/src/ui/cd/TClassDiagramToolBar.java b/src/ui/cd/TClassDiagramToolBar.java
index 452292ffe1..05a9a2611f 100755
--- a/src/ui/cd/TClassDiagramToolBar.java
+++ b/src/ui/cd/TClassDiagramToolBar.java
@@ -76,6 +76,11 @@ public class TClassDiagramToolBar extends TToolBar {
mgui.actions[TGUIAction.ACT_TOGGLE_ATTRIBUTES].setEnabled(b);
mgui.actions[TGUIAction.ACT_TOGGLE_GATES].setEnabled(b);
mgui.actions[TGUIAction.ACT_TOGGLE_SYNCHRO].setEnabled(b);
+
+ mgui.actions[TGUIAction.ACT_ZOOM_MORE].setEnabled(false);
+ mgui.actions[TGUIAction.ACT_ZOOM_LESS].setEnabled(false);
+ mgui.actions[TGUIAction.ACT_SHOW_ZOOM].setEnabled(false);
+ mgui.updateZoomInfo();
}
protected void setButtons() {
diff --git a/src/ui/dd/TDeploymentDiagramToolBar.java b/src/ui/dd/TDeploymentDiagramToolBar.java
index e940e0c1f4..193c27c97e 100755
--- a/src/ui/dd/TDeploymentDiagramToolBar.java
+++ b/src/ui/dd/TDeploymentDiagramToolBar.java
@@ -66,6 +66,11 @@ public class TDeploymentDiagramToolBar extends TToolBar {
mgui.actions[TGUIAction.TDD_LINK].setEnabled(b);
mgui.actions[TGUIAction.TDD_NODE].setEnabled(b);
mgui.actions[TGUIAction.TDD_ARTIFACT].setEnabled(b);
+
+ mgui.actions[TGUIAction.ACT_ZOOM_MORE].setEnabled(false);
+ mgui.actions[TGUIAction.ACT_ZOOM_LESS].setEnabled(false);
+ mgui.actions[TGUIAction.ACT_SHOW_ZOOM].setEnabled(false);
+ mgui.updateZoomInfo();
}
protected void setButtons() {
diff --git a/src/ui/iod/InteractionOverviewDiagramToolBar.java b/src/ui/iod/InteractionOverviewDiagramToolBar.java
index 0fa7472b06..484b2ee823 100755
--- a/src/ui/iod/InteractionOverviewDiagramToolBar.java
+++ b/src/ui/iod/InteractionOverviewDiagramToolBar.java
@@ -74,6 +74,11 @@ public class InteractionOverviewDiagramToolBar extends TToolBar {
mgui.actions[TGUIAction.IOD_STOP].setEnabled(b);
mgui.actions[TGUIAction.IOD_JUNCTION].setEnabled(b);
mgui.actions[TGUIAction.ACT_ENHANCE].setEnabled(b);
+
+ mgui.actions[TGUIAction.ACT_ZOOM_MORE].setEnabled(false);
+ mgui.actions[TGUIAction.ACT_ZOOM_LESS].setEnabled(false);
+ mgui.actions[TGUIAction.ACT_SHOW_ZOOM].setEnabled(false);
+ mgui.updateZoomInfo();
}
diff --git a/src/ui/ncdd/NCDiagramToolBar.java b/src/ui/ncdd/NCDiagramToolBar.java
index 9980941292..644f6b8051 100755
--- a/src/ui/ncdd/NCDiagramToolBar.java
+++ b/src/ui/ncdd/NCDiagramToolBar.java
@@ -69,6 +69,11 @@ public class NCDiagramToolBar extends TToolBar {
mgui.actions[TGUIAction.NCDD_TRAFFIC_ARTIFACT].setEnabled(b);
mgui.actions[TGUIAction.NCDD_ROUTE_ARTIFACT].setEnabled(b);
mgui.actions[TGUIAction.ACT_TOGGLE_ATTR].setEnabled(b);
+
+ mgui.actions[TGUIAction.ACT_ZOOM_MORE].setEnabled(false);
+ mgui.actions[TGUIAction.ACT_ZOOM_LESS].setEnabled(false);
+ mgui.actions[TGUIAction.ACT_SHOW_ZOOM].setEnabled(false);
+ mgui.updateZoomInfo();
}
protected void setButtons() {
diff --git a/src/ui/osad/TURTLEOSActivityDiagramToolBar.java b/src/ui/osad/TURTLEOSActivityDiagramToolBar.java
index d039647414..d09d7d2056 100755
--- a/src/ui/osad/TURTLEOSActivityDiagramToolBar.java
+++ b/src/ui/osad/TURTLEOSActivityDiagramToolBar.java
@@ -69,6 +69,11 @@ public class TURTLEOSActivityDiagramToolBar extends TToolBar {
mgui.actions[TGUIAction.TOSAD_CHOICE].setEnabled(b);
mgui.actions[TGUIAction.TOSAD_TIME_INTERVAL].setEnabled(b);
mgui.actions[TGUIAction.TOSAD_INT_TIME_INTERVAL].setEnabled(b);
+
+ mgui.actions[TGUIAction.ACT_ZOOM_MORE].setEnabled(false);
+ mgui.actions[TGUIAction.ACT_ZOOM_LESS].setEnabled(false);
+ mgui.actions[TGUIAction.ACT_SHOW_ZOOM].setEnabled(false);
+ mgui.updateZoomInfo();
}
protected void setButtons() {
diff --git a/src/ui/oscd/TURTLEOSClassDiagramToolBar.java b/src/ui/oscd/TURTLEOSClassDiagramToolBar.java
index e1cd8c778f..898b5889a1 100755
--- a/src/ui/oscd/TURTLEOSClassDiagramToolBar.java
+++ b/src/ui/oscd/TURTLEOSClassDiagramToolBar.java
@@ -78,6 +78,11 @@ public class TURTLEOSClassDiagramToolBar extends TToolBar {
mgui.actions[TGUIAction.ACT_TOGGLE_ATTRIBUTES].setEnabled(b);
mgui.actions[TGUIAction.ACT_TOGGLE_GATES].setEnabled(b);
mgui.actions[TGUIAction.ACT_TOGGLE_SYNCHRO].setEnabled(b);*/
+
+ mgui.actions[TGUIAction.ACT_ZOOM_MORE].setEnabled(false);
+ mgui.actions[TGUIAction.ACT_ZOOM_LESS].setEnabled(false);
+ mgui.actions[TGUIAction.ACT_SHOW_ZOOM].setEnabled(false);
+ mgui.updateZoomInfo();
}
protected void setButtons() {
diff --git a/src/ui/procsd/ProactiveCSDToolBar.java b/src/ui/procsd/ProactiveCSDToolBar.java
index 0f7dcb6cc3..ead61149b3 100755
--- a/src/ui/procsd/ProactiveCSDToolBar.java
+++ b/src/ui/procsd/ProactiveCSDToolBar.java
@@ -77,6 +77,12 @@ public class ProactiveCSDToolBar extends TToolBar {
mgui.actions[TGUIAction.CONNECTOR_COMMENT].setEnabled(b);
//Enable the new action created by Solange
//mgui.actions[TGUIAction.PRUEBA_1].setEnabled(b);
+
+ mgui.actions[TGUIAction.ACT_ZOOM_MORE].setEnabled(false);
+ mgui.actions[TGUIAction.ACT_ZOOM_LESS].setEnabled(false);
+ mgui.actions[TGUIAction.ACT_SHOW_ZOOM].setEnabled(false);
+ mgui.updateZoomInfo();
+
}
protected void setButtons() {
diff --git a/src/ui/prosmd/ProactiveSMDToolBar.java b/src/ui/prosmd/ProactiveSMDToolBar.java
index 809b5636b6..cc4d40d949 100755
--- a/src/ui/prosmd/ProactiveSMDToolBar.java
+++ b/src/ui/prosmd/ProactiveSMDToolBar.java
@@ -85,6 +85,11 @@ public class ProactiveSMDToolBar extends TToolBar {
mgui.actions[TGUIAction.AD_TIME_LIMITED_OFFER_WITH_LATENCY].setEnabled(b);
mgui.actions[TGUIAction.ACT_TOGGLE_JAVA].setEnabled(b);
mgui.actions[TGUIAction.ACT_ENHANCE].setEnabled(b);*/
+
+ mgui.actions[TGUIAction.ACT_ZOOM_MORE].setEnabled(false);
+ mgui.actions[TGUIAction.ACT_ZOOM_LESS].setEnabled(false);
+ mgui.actions[TGUIAction.ACT_SHOW_ZOOM].setEnabled(false);
+ mgui.updateZoomInfo();
}
protected void setButtons() {
diff --git a/src/ui/sd/SequenceDiagramToolBar.java b/src/ui/sd/SequenceDiagramToolBar.java
index 7da5154fc0..0c05a8376b 100755
--- a/src/ui/sd/SequenceDiagramToolBar.java
+++ b/src/ui/sd/SequenceDiagramToolBar.java
@@ -77,6 +77,11 @@ public class SequenceDiagramToolBar extends TToolBar {
mgui.actions[TGUIAction.SD_RELATIVE_TIME_CONSTRAINT].setEnabled(b);
mgui.actions[TGUIAction.SD_RELATIVE_TIME_CONSTRAINT_CONNECTOR].setEnabled(b);
mgui.actions[TGUIAction.SD_ALIGN_INSTANCES].setEnabled(b);
+
+ mgui.actions[TGUIAction.ACT_ZOOM_MORE].setEnabled(false);
+ mgui.actions[TGUIAction.ACT_ZOOM_LESS].setEnabled(false);
+ mgui.actions[TGUIAction.ACT_SHOW_ZOOM].setEnabled(false);
+ mgui.updateZoomInfo();
}
protected void setButtons() {
diff --git a/src/ui/tmlad/TMLActivityDiagramToolBar.java b/src/ui/tmlad/TMLActivityDiagramToolBar.java
index 832ad85320..3f3aecc75f 100755
--- a/src/ui/tmlad/TMLActivityDiagramToolBar.java
+++ b/src/ui/tmlad/TMLActivityDiagramToolBar.java
@@ -88,6 +88,11 @@ public class TMLActivityDiagramToolBar extends TToolBar {
mgui.actions[TGUIAction.TMLAD_SEQUENCE].setEnabled(b);
mgui.actions[TGUIAction.ACT_ENHANCE].setEnabled(b);
mgui.actions[TGUIAction.ACT_TOGGLE_INTERNAL_COMMENT].setEnabled(b);
+
+ mgui.actions[TGUIAction.ACT_ZOOM_MORE].setEnabled(false);
+ mgui.actions[TGUIAction.ACT_ZOOM_LESS].setEnabled(false);
+ mgui.actions[TGUIAction.ACT_SHOW_ZOOM].setEnabled(false);
+ mgui.updateZoomInfo();
}
protected void setButtons() {
diff --git a/src/ui/tmlcd/TMLTaskDiagramToolBar.java b/src/ui/tmlcd/TMLTaskDiagramToolBar.java
index 16657af518..c9080fc0e3 100755
--- a/src/ui/tmlcd/TMLTaskDiagramToolBar.java
+++ b/src/ui/tmlcd/TMLTaskDiagramToolBar.java
@@ -70,6 +70,11 @@ public class TMLTaskDiagramToolBar extends TToolBar {
mgui.actions[TGUIAction.ACT_TOGGLE_CHANNELS].setEnabled(b);
mgui.actions[TGUIAction.ACT_TOGGLE_EVENTS].setEnabled(b);
mgui.actions[TGUIAction.ACT_TOGGLE_REQUESTS].setEnabled(b);
+
+ mgui.actions[TGUIAction.ACT_ZOOM_MORE].setEnabled(false);
+ mgui.actions[TGUIAction.ACT_ZOOM_LESS].setEnabled(false);
+ mgui.actions[TGUIAction.ACT_SHOW_ZOOM].setEnabled(false);
+ mgui.updateZoomInfo();
}
protected void setButtons() {
diff --git a/src/ui/tmldd/TMLArchiDiagramToolBar.java b/src/ui/tmldd/TMLArchiDiagramToolBar.java
index 44ffd67edb..33f388c242 100755
--- a/src/ui/tmldd/TMLArchiDiagramToolBar.java
+++ b/src/ui/tmldd/TMLArchiDiagramToolBar.java
@@ -72,6 +72,9 @@ public class TMLArchiDiagramToolBar extends TToolBar {
mgui.actions[TGUIAction.TMLARCHI_COMMUNICATION_ARTIFACT].setEnabled(b);
mgui.actions[TGUIAction.TMLARCHI_MEMORYNODE].setEnabled(b);
mgui.actions[TGUIAction.ACT_TOGGLE_ATTR].setEnabled(b);
+
+ mgui.actions[TGUIAction.ACT_SHOW_ZOOM].setEnabled(false);
+ mgui.updateZoomInfo();
}
protected void setButtons() {
diff --git a/src/ui/ucd/UseCaseDiagramToolBar.java b/src/ui/ucd/UseCaseDiagramToolBar.java
index 89897243d1..bc15b5e8dd 100755
--- a/src/ui/ucd/UseCaseDiagramToolBar.java
+++ b/src/ui/ucd/UseCaseDiagramToolBar.java
@@ -69,6 +69,11 @@ public class UseCaseDiagramToolBar extends TToolBar {
mgui.actions[TGUIAction.UCD_CONNECTOR_INCLUDE].setEnabled(b);
mgui.actions[TGUIAction.UCD_CONNECTOR_EXTEND].setEnabled(b);
mgui.actions[TGUIAction.UCD_CONNECTOR_SPECIA].setEnabled(b);
+
+ mgui.actions[TGUIAction.ACT_ZOOM_MORE].setEnabled(false);
+ mgui.actions[TGUIAction.ACT_ZOOM_LESS].setEnabled(false);
+ mgui.actions[TGUIAction.ACT_SHOW_ZOOM].setEnabled(false);
+ mgui.updateZoomInfo();
}
protected void setButtons() {
diff --git a/src/ui/window/JDialogUPPAALGeneration.java b/src/ui/window/JDialogUPPAALGeneration.java
index 8cc2748179..5f2b4a99a5 100755
--- a/src/ui/window/JDialogUPPAALGeneration.java
+++ b/src/ui/window/JDialogUPPAALGeneration.java
@@ -315,12 +315,16 @@ public class JDialogUPPAALGeneration extends javax.swing.JDialog implements Acti
result = mgui.gtm.generateUPPAALFromTML(pathCode, debug, size1, choices);
} else {
result = mgui.gtm.generateUPPAALFromTIF(pathCode, debug, nb1, choices);
+ jta.append("UPPAAL specification generated\n");
+ jta.append("Checking the regularity of the TIF specification\n");
+ System.out.println("Regularity?");
boolean b = mgui.gtm.isRegularTM();
if (b) {
jta.append("UPPAAL code was optimized since the TIF specification is regular\n");
} else {
jta.append("UPPAAL code was NOT optimized since the TIF specification is NOT regular\n");
}
+ System.out.println("Regularity done");
}
if (result) {
jta.append("UPPAAL code generated in " + pathCode);
diff --git a/src/ui/window/JDialogUPPAALValidation.java b/src/ui/window/JDialogUPPAALValidation.java
index 58767414a7..6553e1e5b4 100755
--- a/src/ui/window/JDialogUPPAALValidation.java
+++ b/src/ui/window/JDialogUPPAALValidation.java
@@ -325,7 +325,7 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
}
}
} else {
- jta.append("No component to analyze found on diagrams\n");
+ jta.append("No component to analyze accessibility found on diagrams\n");
}
}
@@ -347,7 +347,7 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
}
}
} else {
- jta.append("No component found\n");
+ jta.append("No component to analyze liveness found on diagrams\n");
}
}
diff --git a/src/uppaaldesc/UPPAALSpec.java b/src/uppaaldesc/UPPAALSpec.java
index 0f91408197..9553dcbd40 100755
--- a/src/uppaaldesc/UPPAALSpec.java
+++ b/src/uppaaldesc/UPPAALSpec.java
@@ -71,12 +71,12 @@ public class UPPAALSpec {
UPPAALTemplate template;
globalDeclaration = "<declaration>\n//Global declarations\n" + Conversion.transformToXMLString(globalDeclaration) + "</declaration>\n";
- String templatesString = "";
+ StringBuffer templatesString = new StringBuffer("");
while(iterator.hasNext()) {
//System.out.println("Template!");
template = (UPPAALTemplate)(iterator.next());
- templatesString += template.makeTemplate();
+ templatesString.append(template.makeTemplate());
}
instanciations = "<system>\n//Instanciation \n" + Conversion.transformToXMLString(instanciations) + "</system>\n";
diff --git a/src/uppaaldesc/UPPAALTemplate.java b/src/uppaaldesc/UPPAALTemplate.java
index a7bef78701..14647b1c6b 100755
--- a/src/uppaaldesc/UPPAALTemplate.java
+++ b/src/uppaaldesc/UPPAALTemplate.java
@@ -119,35 +119,35 @@ public class UPPAALTemplate {
}
- public String makeStringAutomata() {
+ public StringBuffer makeStringAutomata() {
+ StringBuffer ret = new StringBuffer("");
+
if (initLocation == null) {
- return "";
+ return ret;
}
- String ret = "";
-
ListIterator iterator = locations.listIterator();
while(iterator.hasNext()) {
- ret += ((UPPAALLocation)(iterator.next())).getXML();
+ ret.append(((UPPAALLocation)(iterator.next())).getXML());
}
- ret += "<init ref=\"" +initLocation.id + "\" />\n";
+ ret.append("<init ref=\"" +initLocation.id + "\" />\n");
iterator = transitions.listIterator();
while(iterator.hasNext()) {
- ret += ((UPPAALTransition)(iterator.next())).getXML();
+ ret.append(((UPPAALTransition)(iterator.next())).getXML());
}
return ret;
}
- public String makeTemplate() {
- String fullString = "<template>\n";
- fullString += "<name>" + name + "</name>\n";
- fullString += "<parameter>" + Conversion.transformToXMLString(parameter) + "</parameter>\n";
- fullString += "<declaration>" + Conversion.transformToXMLString(declaration) + "</declaration>\n";
- fullString += makeStringAutomata();
- fullString += "</template>\n";
+ public StringBuffer makeTemplate() {
+ StringBuffer fullString = new StringBuffer("<template>\n");
+ fullString.append("<name>" + name + "</name>\n");
+ fullString.append("<parameter>" + Conversion.transformToXMLString(parameter) + "</parameter>\n");
+ fullString.append("<declaration>" + Conversion.transformToXMLString(declaration) + "</declaration>\n");
+ fullString.append(makeStringAutomata());
+ fullString.append("</template>\n");
return fullString;
}
--
GitLab