From 0c00c454ea5736306f5fcc8cdb866acbc55c1d10 Mon Sep 17 00:00:00 2001
From: Ludovic Apvrille <ludovic.apvrille@telecom-paristech.fr>
Date: Tue, 19 Feb 2013 17:15:24 +0000
Subject: [PATCH] Resolving bugs in avatar interal simulator, avatr to uppaal
generator and avatar-to-tpn generator
---
executablecode/Makefile.src | 2 +-
.../AvatarSimulationBlock.java | 8 +-
src/avatartranslator/totpn/AVATAR2TPN.java | 27 ++++--
.../touppaal/AVATAR2UPPAAL.java | 5 +-
src/myutil/IntMatrix.java | 12 +++
src/tpndescription/Place.java | 5 ++
src/tpndescription/TPN.java | 79 +++++++++++++++++
src/tpndescription/Transition.java | 46 ++++++++++
src/ui/AvatarDesignPanel.java | 4 +
src/ui/GTURTLEModeling.java | 20 +++++
src/ui/MainGUI.java | 12 +++
src/ui/window/JDialogInvariantAnalysis.java | 84 +++++++++++--------
12 files changed, 261 insertions(+), 43 deletions(-)
diff --git a/executablecode/Makefile.src b/executablecode/Makefile.src
index 28b9acb23f..c3bde51c3e 100755
--- a/executablecode/Makefile.src
+++ b/executablecode/Makefile.src
@@ -1 +1 @@
-SRCS = generated_src/main.c generated_src/ObserverProp1.c generated_src/RemotelyControlledMicrowave.c generated_src/RemoteControl.c generated_src/MicroWaveOven.c generated_src/Bell.c generated_src/ControlPanel.c generated_src/Controller.c generated_src/Magnetron.c generated_src/Door.c generated_src/WirelessInterface.c
\ No newline at end of file
+SRCS = generated_src/main.c generated_src/Block0.c
\ No newline at end of file
diff --git a/src/avatartranslator/directsimulation/AvatarSimulationBlock.java b/src/avatartranslator/directsimulation/AvatarSimulationBlock.java
index 4e8fd78a39..866b5d9538 100644
--- a/src/avatartranslator/directsimulation/AvatarSimulationBlock.java
+++ b/src/avatartranslator/directsimulation/AvatarSimulationBlock.java
@@ -385,12 +385,13 @@ public class AvatarSimulationBlock {
avat = aaos.getSignal().getListOfAttributes().get(i);
result = "";
if (avat.getType() == AvatarType.INTEGER) {
+ //TraceManager.addDev("Evaluating expression, value=" + value);
result += evaluateIntExpression(value, lastTransaction.attributeValues);
} else if (avat.getType() == AvatarType.BOOLEAN) {
result += evaluateBoolExpression(value, lastTransaction.attributeValues);
}
- //TraceManager.addDev("Adding value:" + result);
+ TraceManager.addDev("Adding value:" + result);
parameters.add(result);
} catch (Exception e) {
TraceManager.addDev("EXCEPTION on adding value " + aaos);
@@ -635,10 +636,15 @@ public class AvatarSimulationBlock {
String act = _expr;
int cpt = 0;
for(String attrValue: _attributeValues) {
+ if (attrValue.trim().startsWith("-")) {
+ attrValue = "(0" + attrValue + ")";
+ }
act = Conversion.putVariableValueInString(AvatarSpecification.ops, act, getAttributeName(cpt), attrValue);
cpt ++;
}
+ TraceManager.addDev("Evaluating expression: " + act);
+
return (int)(new IntExpressionEvaluator().getResultOf(act));
}
diff --git a/src/avatartranslator/totpn/AVATAR2TPN.java b/src/avatartranslator/totpn/AVATAR2TPN.java
index 149aabb7d6..99ba997151 100755
--- a/src/avatartranslator/totpn/AVATAR2TPN.java
+++ b/src/avatartranslator/totpn/AVATAR2TPN.java
@@ -116,6 +116,7 @@ public class AVATAR2TPN {
for(AvatarBlock block: blocks) {
makeBlock(block);
}
+ interconnectSynchro();
}
public void makeBlock(AvatarBlock ab) {
@@ -124,7 +125,7 @@ public class AVATAR2TPN {
makeBlockTPN(ab, asm, ass,null);
- interconnectSynchro();
+
}
public void makeBlockTPN(AvatarBlock _block, AvatarStateMachine _asm, AvatarStateMachineElement _asme, AvatarStateMachineElement _previous) {
@@ -146,7 +147,7 @@ public class AVATAR2TPN {
if (p0 != null) {
// Link the exit place of the previous element to the one of the current element
if (p1 != null){
- t0 = new Transition(getTPNName(_block, _previous) + " to " + getTPNName(_block, _asme));
+ t0 = new Transition(getTPNName(_block, _previous) + "_to_" + getTPNName(_block, _asme));
t0.addDestinationPlace(p0);
t0.addOriginPlace(p1);
tpn.addTransition(t0);
@@ -175,6 +176,7 @@ public class AVATAR2TPN {
}
} else if (_asme instanceof AvatarActionOnSignal){
+ TraceManager.addDev("??????? Analyzing actions on signals: " + _asme);
aaos = (AvatarActionOnSignal)_asme;
if (aaos.getSignal().isOut()) {
@@ -202,7 +204,7 @@ public class AVATAR2TPN {
// Must link the new element to the previous one
if ((p1 != null) && (link)){
- t0 = new Transition(getTPNName(_block, _previous) + " to " + getTPNName(_block, _asme));
+ t0 = new Transition(getTPNName(_block, _previous) + "_to_" + getTPNName(_block, _asme));
t0.addDestinationPlace(pentry);
t0.addOriginPlace(p1);
tpn.addTransition(t0);
@@ -227,6 +229,7 @@ public class AVATAR2TPN {
// Interconnect sender and receivers together!
for(AvatarActionOnSignal destination: receiveActions) {
+ TraceManager.addDev("Dealing with receive actions : " + destination);
// Find the related relation
for(AvatarRelation ar: avspec.getRelations()) {
if (ar.containsSignal(destination.getSignal()) && !ar.isAsynchronous()) {
@@ -235,11 +238,11 @@ public class AVATAR2TPN {
for(AvatarActionOnSignal origin:sendActions) {
if (origin.getSignal() == sig) {
// combination found!
- //TraceManager.addDev("Combination found");
- t0 = new Transition("beginning Synchro from " + getTPNName(ar.getOutBlock(index), origin) + " to " + getTPNName(ar.getInBlock(index), destination));
- pSynchro = new Place("Synchro from " + getTPNName(ar.getOutBlock(index), origin) + " to " + getTPNName(ar.getInBlock(index), destination));
+ TraceManager.addDev("Combination found for: " + sig);
+ t0 = new Transition("beginning_Synchro_from_" + getTPNName(ar.getOutBlock(index), origin) + "_to_" + getTPNName(ar.getInBlock(index), destination));
+ pSynchro = new Place("Synchro_from_" + getTPNName(ar.getOutBlock(index), origin) + "_to_" + getTPNName(ar.getInBlock(index), destination));
tpn.addPlace(pSynchro);
- t1 = new Transition("end Synchro from " + getTPNName(ar.getOutBlock(index), origin) + " to " + getTPNName(ar.getInBlock(index), destination));
+ t1 = new Transition("end_Synchro_from_" + getTPNName(ar.getOutBlock(index), origin) + "_to_" + getTPNName(ar.getInBlock(index), destination));
t0.addOriginPlace(entryPlaces.get(destination));
t0.addOriginPlace(entryPlaces.get(origin));
@@ -293,6 +296,16 @@ public class AVATAR2TPN {
}*/
public String getTPNName(AvatarBlock _block, AvatarStateMachineElement _asme) {
+ if (_asme instanceof AvatarActionOnSignal) {
+ AvatarActionOnSignal aaos = (AvatarActionOnSignal)_asme;
+ if (aaos.isSending()) {
+ return _block.getName() + "__Send__" + aaos.getSignal().getName() + "__" + _asme.getID();
+ } else {
+ return _block.getName() + "__Receive__" + aaos.getSignal().getName() + "__" + _asme.getID();
+ }
+
+ }
+
return _block.getName() + "__" + _asme.getName() + "__" + _asme.getID();
}
diff --git a/src/avatartranslator/touppaal/AVATAR2UPPAAL.java b/src/avatartranslator/touppaal/AVATAR2UPPAAL.java
index f641b7ec5b..d6dac199c8 100755
--- a/src/avatartranslator/touppaal/AVATAR2UPPAAL.java
+++ b/src/avatartranslator/touppaal/AVATAR2UPPAAL.java
@@ -919,7 +919,10 @@ public class AVATAR2UPPAAL {
// Must consider whether the transition leads to an action on a signal
if (at.followedWithAnActionOnASignal()) {
aaos = (AvatarActionOnSignal)(at.getNext(0));
- loc1 = translateAvatarActionOnSignal(aaos, _block, _template, _loc, "");
+ if (tmps == null) {
+ tmps = "";
+ }
+ loc1 = translateAvatarActionOnSignal(aaos, _block, _template, _loc, tmps);
loc2 = hash.get(aaos);
if (loc2 == null) {
diff --git a/src/myutil/IntMatrix.java b/src/myutil/IntMatrix.java
index 534981cc30..e20c23b778 100755
--- a/src/myutil/IntMatrix.java
+++ b/src/myutil/IntMatrix.java
@@ -96,6 +96,14 @@ public class IntMatrix {
return cpt;
}
+ public int getValueOfLineFromColumn(int columnIndex, int i) {
+ int cpt = 0;
+ for(int j=columnIndex;j<sizeColumn; j++) {
+ cpt += matrice[i][j];
+ }
+ return cpt;
+ }
+
public void setNameOfLine(int line, String name) {
try {
nameOfRows[line] = name;
@@ -367,6 +375,10 @@ public class IntMatrix {
}
+ // Remove m first columns
+
+
+
}
diff --git a/src/tpndescription/Place.java b/src/tpndescription/Place.java
index 642b84be80..d6507fb321 100755
--- a/src/tpndescription/Place.java
+++ b/src/tpndescription/Place.java
@@ -50,6 +50,7 @@ public class Place {
public int nbOfToken;
public String name;
+ public int x, y;
public Place() {
name = generateName();
@@ -81,5 +82,9 @@ public class Place {
return "pl " + name + " (" + nbOfToken + ")";
}
+ public String toNDRFormat() {
+ return "p " + x + " " + y + " " + name + " " + nbOfToken + " n\n";
+ }
+
}
\ No newline at end of file
diff --git a/src/tpndescription/TPN.java b/src/tpndescription/TPN.java
index 3415b10c47..e2ee180e47 100755
--- a/src/tpndescription/TPN.java
+++ b/src/tpndescription/TPN.java
@@ -69,6 +69,85 @@ public class TPN {
transitions.add(tr);
}
+ public String toNDRFormat() {
+ Place p;
+ String tpn = "";
+ int cpt = 0;
+ int cpty;
+ int nbOfPlaces;
+ ListIterator iterator;
+ String beg;
+ int index;
+
+ int stepx = 250;
+ int stepy = 125;
+
+ // Compute the x and y position of each element
+ // First init all to 0, and then, compute the position
+ for(Place p0: places) {
+ p0.x = 0; p0.y=0;
+ }
+ for(Transition t0: transitions) {
+ t0.x=0; t0.y=0;
+ }
+
+ // Determine an x for each task, with a step of 400 between each, starting at 100
+ // Vertical placement for the same task name.
+ cpt = 100;
+ nbOfPlaces = 0;
+ for(Place p1: places) {
+ //Place already met?
+ if (p1.x == 0) {
+ // Not met!
+ index = p1.name.indexOf("_");
+ if (index == -1) {
+ beg = p1.name;
+ } else {
+ beg = p1.name.substring(0, index);
+ }
+ cpty = 100;
+ p1.x = cpt;
+ p1.y = cpty;
+ cpty += stepy;
+ iterator = places.listIterator();
+ while(iterator.hasNext()) {
+ p = (Place)(iterator.next());
+ if (p.x == 0) {
+ if (p.name.startsWith(beg)) {
+ p.x = cpt;
+ p.y= cpty;
+ cpty+= stepy;
+ }
+ }
+ }
+ cpt += stepx + (nbOfPlaces * 100);
+ nbOfPlaces ++;
+ }
+ }
+
+ // For transitions, we use the barycenter of all connected places
+ for(Transition t: transitions) {
+ t.x = t.getXBarycenterOfPlaces() + 100;
+ t.y = t.getYBarycenterOfPlaces() - 50;
+ }
+
+
+
+ // Generate text of places and transitions
+ iterator = places.listIterator();
+ while(iterator.hasNext()) {
+ p = (Place)(iterator.next());
+ tpn += p.toNDRFormat();
+ }
+ iterator = transitions.listIterator();
+ while(iterator.hasNext()) {
+ tpn += ((Transition)(iterator.next())).toNDRFormat() + "\n";
+
+ }
+
+ return tpn;
+ }
+
public String toTINAString() {
Place p;
String tpn = "net generatedWithTTool\n\n";
diff --git a/src/tpndescription/Transition.java b/src/tpndescription/Transition.java
index 8cc211fa04..fabf215c68 100755
--- a/src/tpndescription/Transition.java
+++ b/src/tpndescription/Transition.java
@@ -51,6 +51,7 @@ public class Transition {
public static int INDEX = 0;
public String name;
+ public int x, y;
public String label; /* name of the synchro gate, name of the delay, etc.) */
public String predicat; /* action to be executed before the transition is fired */
public int intervalMin = 0;
@@ -155,5 +156,50 @@ public class Transition {
return s;
}
+ public String toNDRFormat() {
+ String tr = "";
+ tr += "t " + x + " " + y + " " + name + " 0 w n\n";
+ for(int i=0; i<originPlaces.size(); i++) {
+ tr += "e " + originPlaces.get(i).name + " " + name + " 1 n\n";
+ }
+ for(int j=0; j<destinationPlaces.size(); j++) {
+ tr += "e " + name + " " + destinationPlaces.get(j).name + " 1 n\n";
+ }
+ return tr;
+
+ }
+
+ public int getXBarycenterOfPlaces() {
+ int totalX = 0;
+ int nbMet = 0;
+ for(Place p1: originPlaces) {
+ totalX += p1.x;
+ nbMet ++;
+ }
+ for(Place p2: destinationPlaces) {
+ totalX += p2.x;
+ nbMet ++;
+ }
+
+ return (int)(totalX/nbMet);
+
+ }
+
+ public int getYBarycenterOfPlaces() {
+ int totalY = 0;
+ int nbMet = 0;
+ for(Place p1: originPlaces) {
+ totalY += p1.y;
+ nbMet ++;
+ }
+ for(Place p2: destinationPlaces) {
+ totalY += p2.y;
+ nbMet ++;
+ }
+
+ return (int)(totalY/nbMet);
+
+ }
+
}
\ No newline at end of file
diff --git a/src/ui/AvatarDesignPanel.java b/src/ui/AvatarDesignPanel.java
index 5c201e76ac..f98013e427 100644
--- a/src/ui/AvatarDesignPanel.java
+++ b/src/ui/AvatarDesignPanel.java
@@ -251,6 +251,10 @@ public class AvatarDesignPanel extends TURTLEPanel {
}
}
+ public void clearGraphicalInfoOnInvariants() {
+
+ }
+
}
\ No newline at end of file
diff --git a/src/ui/GTURTLEModeling.java b/src/ui/GTURTLEModeling.java
index 70d66a8d5d..baa23d9378 100755
--- a/src/ui/GTURTLEModeling.java
+++ b/src/ui/GTURTLEModeling.java
@@ -1803,6 +1803,26 @@ public class GTURTLEModeling {
return -3;
+ }
+
+ public void clearGraphicalInfoOnInvariants() {
+ if (avatarspec == null) {
+ return;
+ }
+
+ AvatarDesignPanel adp = null;
+
+ try {
+ adp = (AvatarDesignPanel)(avatarspec.getInformationSource());
+ } catch (Exception e) {
+ TraceManager.addDev("Exception gtm: " + e.getMessage());
+ return;
+ }
+
+ adp.removeAllMutualExclusionWithMasterMutex();
+
+
+
}
diff --git a/src/ui/MainGUI.java b/src/ui/MainGUI.java
index 3a34b32eb9..9c817b9513 100755
--- a/src/ui/MainGUI.java
+++ b/src/ui/MainGUI.java
@@ -1731,6 +1731,18 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener {
saveFile(dtafile, gdata, "Graphical DTA saved under");
}
+ public String saveTPNNDRFormat(String tpn) {
+ String s = file.getAbsolutePath();
+ int l = s.length();
+ String myFile = s.substring(0, l-4) + ".ndr";
+ try {
+ FileUtils.saveFile(myFile, tpn);
+ } catch (Exception e) {
+ return "TPN could not be saved in myFile: " +e.getMessage();
+ }
+ return "TPN saved in " +myFile;
+ }
+
public void saveRG(String tdata, String gdata) {
File rgfile;
diff --git a/src/ui/window/JDialogInvariantAnalysis.java b/src/ui/window/JDialogInvariantAnalysis.java
index b6a9be9f8a..a838e616f2 100644
--- a/src/ui/window/JDialogInvariantAnalysis.java
+++ b/src/ui/window/JDialogInvariantAnalysis.java
@@ -248,13 +248,18 @@ public class JDialogInvariantAnalysis extends javax.swing.JDialog implements Act
try {
jta.append("\n*** WARNING: Invariants do NOT take into account variables nor time constraints ***\n");
+ jta.append("Clearing invariants on diagrams\n");
+ mgui.gtm.clearGraphicalInfoOnInvariants();
jta.append("Generating Petri Net\n");
tpn = mgui.gtm.generateTPNFromAvatar();
jtatpn.append("Petri Net:\n" + tpn.toString() + "\n\n");
+ String ret = mgui.saveTPNNDRFormat(tpn.toNDRFormat());
+ jta.append(ret + "\n");
testGo();
jta.append("Computing incidence matrix\n");
IntMatrix im = tpn.getIncidenceMatrix();
+ int nbOfColumn = im.sizeColumn;
jtamatrix.append("Incidence matrix:\n" + im.toString() + "\n\n");
jta.append("Incidence matrix computed\n");
testGo();
@@ -293,7 +298,7 @@ public class JDialogInvariantAnalysis extends javax.swing.JDialog implements Act
name = im.getNameOfLine(i);
inv = new Invariant("#" + ((i+1)-ignored) + " " + name);
- inv.setValue(im.getValueOfLine(i));
+ inv.setValue(im.getValueOfLineFromColumn(nbOfColumn, i));
// Putting components
name = Conversion.replaceAllString(name, " + ", "&");
@@ -325,7 +330,11 @@ public class JDialogInvariantAnalysis extends javax.swing.JDialog implements Act
try {
myid = Integer.decode(tmps[tmps.length-1]).intValue();
o = ab.getStateMachine().getReferenceObjectFromID(myid);
- tgc1 = (TGComponent)o;
+ if (o != null) {
+ tgc1 = (TGComponent)o;
+ } else {
+ tgc1 = null;
+ }
} catch (Exception e) {
tgc1 = null;
@@ -344,7 +353,11 @@ public class JDialogInvariantAnalysis extends javax.swing.JDialog implements Act
try {
myid = Integer.decode(tmps[tmps.length-1]).intValue();
o = ab.getStateMachine().getReferenceObjectFromID(myid);
- tgc2 = (TGComponent)o;
+ if (o != null) {
+ tgc2 = (TGComponent)o;
+ } else {
+ tgc2 = null;
+ }
} catch (Exception e) {
tgc2 = null;
@@ -378,37 +391,42 @@ public class JDialogInvariantAnalysis extends javax.swing.JDialog implements Act
tmp = Conversion.replaceAllString(tmp, "__", "&");
tmps = tmp.split("&");
if (tmps.length > 2) {
+ //TraceManager.addDev("Getting block with name=" + tmps[0]);
ab = avspec.getBlockWithName(tmps[0]);
- if (prevBlock == null) {
- prevBlock = ab;
- } else {
- if (prevBlock != ab) {
- if (prevBlock1 != null) {
- if (prevBlock1 != ab) {
- sameBlock = false;
- }
- } else {
- sameBlock = false;
- }
- }
- }
- prevBlock = ab;
- prevBlock1 = null;
-
- try {
- myid = Integer.decode(tmps[tmps.length-1]).intValue();
- o = ab.getStateMachine().getReferenceObjectFromID(myid);
- //TraceManager.addDev("Adding component to inv block=" + ab.getName() + " id=" + myid + " object=" + o);
- if (!((o instanceof AvatarSMDReceiveSignal) || (o instanceof AvatarSMDSendSignal))) {
- //TraceManager.addDev("Adding component to inv block=" + ab.getName() + " id=" + myid + " object=" + o);
- inv.addComponent((TGComponent)o);
- }
- //TraceManager.addDev("Component added:" + o);
- if (o instanceof AvatarSMDStartState) {
- valToken ++;
- }
- } catch (Exception e) {
- TraceManager.addDev("Exception invariants:" + e.getMessage() + "tmps[end]=" + tmps[tmps.length-1] + " inv=" + name);
+ if (ab != null) {
+ if (prevBlock == null) {
+ prevBlock = ab;
+ } else {
+ if (prevBlock != ab) {
+ if (prevBlock1 != null) {
+ if (prevBlock1 != ab) {
+ sameBlock = false;
+ }
+ } else {
+ sameBlock = false;
+ }
+ }
+ }
+ prevBlock = ab;
+ prevBlock1 = null;
+
+ try {
+ //TraceManager.addDev("trying ... tmps=" + tmps[tmps.length-1] + "ab=" + ab);
+ myid = Integer.decode(tmps[tmps.length-1]).intValue();
+ //TraceManager.addDev("Adding component to inv block=" + ab.getName() + " id=" + myid);
+ o = ab.getStateMachine().getReferenceObjectFromID(myid);
+ //TraceManager.addDev("Adding component to inv block=" + ab.getName());
+ if (!((o instanceof AvatarSMDReceiveSignal) || (o instanceof AvatarSMDSendSignal))) {
+ //TraceManager.addDev("Adding component to inv block=" + ab.getName() + " id=" + myid + " object=" + o);
+ inv.addComponent((TGComponent)o);
+ }
+ //TraceManager.addDev("Component added:" + o);
+ if (o instanceof AvatarSMDStartState) {
+ valToken ++;
+ }
+ } catch (Exception e) {
+ TraceManager.addDev("Exception invariants:" + e.getMessage() + "tmps[end]=" + tmps[tmps.length-1] + " inv=" + name);
+ }
}
}
}
--
GitLab