diff --git a/bin/config.xml b/bin/config.xml
index 56ec830d9bab6ea48903eb68e2a86b511dd0cc23..40386028d8e75b37bb924beeb30c0b7decb03446 100755
--- a/bin/config.xml
+++ b/bin/config.xml
@@ -42,18 +42,14 @@
<SystemCCodeInteractiveExecuteCommand data="/homes/apvrille/TechTTool/SystemCCode/generated/run.x -server" />
<TMLCodeDirectory data="/Users/ludovicapvrille/TTool/tmlcode" />
<GTKWavePath data="/opt/local/bin/gtkwave" />
-<<<<<<< .mine
<VCDPath data="/Users/ludovicapvrille/TTool/vcd/" />
-=======
-<VCDPath data="/Users/ludovicapvrille/TTool/vcd" />
->>>>>>> .r2431
<UPPAALCodeDirectory data="/Users/ludovicapvrille/TTool/uppaal/" />
-<UPPAALVerifierPath data="/Applications/uppaal-4.0.7-aca/verifyta" />
+<UPPAALVerifierPath data="/Applications/uppaal-4.0.11/verifyta" />
<UPPAALVerifierHost data="localhost" />
<ExternalCommand1Host data="localhost"/>
<ExternalCommand1 data="/opt/local/bin/gtkwave /Users/ludovicapvrille/simulators/c++2/vcddump.vcd"/>
<ExternalCommand2Host data="localhost"/>
-<ExternalCommand2 data="/Applications/uppaal-4.0.7-aca/uppaal /Users/ludovicapvrille/TTool/uppaal/spec.xml"/>
+<ExternalCommand2 data="open /Applications/uppaal-4.0.11/UPPAAL.app /Users/ludovicapvrille/TTool/uppaal/spec.xml"/>
<LastWindowAttributes x="367" y="47" width="1094" height="924" max="false" />
diff --git a/src/avatartranslator/AvatarRelation.java b/src/avatartranslator/AvatarRelation.java
index e16b376e28d4ebd174db166dd0d8acd8179ad2c1..8439253f1cbe56422add9e79e97620d7874280d9 100644
--- a/src/avatartranslator/AvatarRelation.java
+++ b/src/avatartranslator/AvatarRelation.java
@@ -56,6 +56,8 @@ public class AvatarRelation extends AvatarElement {
public AvatarBlock block1, block2;
private LinkedList<AvatarSignal> signals1, signals2;
+ private boolean blocking, asynchronous;
+ private int sizeOfFIFO;
public AvatarRelation(String _name, AvatarBlock _block1, AvatarBlock _block2, Object _referenceObject) {
@@ -64,8 +66,28 @@ public class AvatarRelation extends AvatarElement {
signals2 = new LinkedList<AvatarSignal>();
block1 = _block1;
block2 = _block2;
+ blocking = false;
+ sizeOfFIFO = 1024;
+ asynchronous = false;
+
}
+ public void setAsynchronous(boolean _b) {
+ asynchronous = _b;
+ }
+
+ public void setBlocking(boolean _b) {
+ blocking = _b;
+ }
+
+ public void setSizeOfFIFO(int _sizeOfFIFO) {
+ sizeOfFIFO = _sizeOfFIFO;
+ }
+
+ public boolean isAsynchronous() {
+ return asynchronous;
+ }
+
public void addSignals(AvatarSignal _sig1, AvatarSignal _sig2) {
diff --git a/src/avatartranslator/touppaal/AVATAR2UPPAAL.java b/src/avatartranslator/touppaal/AVATAR2UPPAAL.java
index 09030f831a858c6c6672b646a303396342173d39..8ee0b97d048caee79888f5d5d60f6a58b2791be1 100755
--- a/src/avatartranslator/touppaal/AVATAR2UPPAAL.java
+++ b/src/avatartranslator/touppaal/AVATAR2UPPAAL.java
@@ -68,6 +68,8 @@ public class AVATAR2UPPAAL {
private LinkedList gatesNotSynchronized; // String
private LinkedList gatesSynchronized;
+ private LinkedList gatesAsynchronized;
+
private int nbOfIntParameters, nbOfBooleanParameters;
private Hashtable <AvatarStateMachineElement, UPPAALLocation> hash;
@@ -154,6 +156,7 @@ public class AVATAR2UPPAAL {
gatesNotSynchronized = new LinkedList();
gatesNotSynchronized.add("makeChoice");
gatesSynchronized = new LinkedList();
+ gatesAsynchronized = new LinkedList();
// Deal with blocks
translateBlocks();
@@ -234,16 +237,46 @@ public class AVATAR2UPPAAL {
public void translationRelations() {
AvatarSignal si1, sig2;
for(AvatarRelation ar: avspec.getRelations()) {
- for(int i=0; i<ar.nbOfSignals(); i++) {
- gatesSynchronized.add(relationToString(ar, i));
+ if (ar.isAsynchronous()) {
+ for(int i=0; i<ar.nbOfSignals(); i++) {
+ gatesAsynchronized.add(relationToString(ar, i, 0));
+ gatesAsynchronized.add(relationToString(ar, i, 1));
+ }
+ } else {
+ for(int i=0; i<ar.nbOfSignals(); i++) {
+ gatesSynchronized.add(relationToString(ar, i));
+ }
}
}
}
+
+ // For synchronous relations
public String relationToString(AvatarRelation _ar, int _index) {
return _ar.block1.getName() + "_" + _ar.getSignal1(_index).getName() + "__" + _ar.block2.getName() + "_" + _ar.getSignal2(_index).getName();
}
+ // For asynchronous relations
+ public String relationToString(AvatarRelation _ar, int _index, int _indexOfBlock) {
+ String signalName;
+ AvatarSignal sig;
+ if (_indexOfBlock == 0) {
+ sig = _ar.getSignal1(_index);
+ signalName = _ar.block1.getName() + "_" + sig.getName() + "__";
+ } else {
+ sig = _ar.getSignal2(_index);
+ signalName = _ar.block2.getName() + "_" + sig.getName() + "__";
+ }
+
+ if (sig.isIn()) {
+ signalName += "rd";
+ } else {
+ signalName += "wr";
+ }
+
+ return signalName;
+ }
+
public String signalToUPPAALString(AvatarSignal _as) {
AvatarRelation ar = avspec.getAvatarRelationWithSignal(_as);
if (ar == null) {
@@ -319,6 +352,8 @@ public class AVATAR2UPPAAL {
spec.addGlobalDeclaration("urgent chan " + action + ";\n");
//spec.addGlobalDeclaration("int " + action + TURTLE2UPPAAL.SYNCID + " = 0;\n");
}
+
+
}
public void makeSynchronized() {
@@ -326,7 +361,7 @@ public class AVATAR2UPPAAL {
return;
}
- spec.addGlobalDeclaration("\n//Declarations used for synchronized gates\n");
+ spec.addGlobalDeclaration("\n//Declarations for synchronous channels\n");
String action;
ListIterator iterator = gatesSynchronized.listIterator();
@@ -334,6 +369,13 @@ public class AVATAR2UPPAAL {
action = (String)(iterator.next());
spec.addGlobalDeclaration("urgent chan " + action + ";\n");
}
+
+ spec.addGlobalDeclaration("\n//Declarations for asynchronous channels\n");
+ iterator = gatesAsynchronized.listIterator();
+ while(iterator.hasNext()) {
+ action = (String)(iterator.next());
+ spec.addGlobalDeclaration("urgent chan " + action + ";\n");
+ }
}
public void makeBehaviour(AvatarBlock _block, UPPAALTemplate _template) {
diff --git a/src/ui/AvatarDesignPanelTranslator.java b/src/ui/AvatarDesignPanelTranslator.java
index 46f8d0b7532eb66db6da5f03ed8638b445e61e66..a93ac0a63039355806bdec9cfeae9a638f77a1a4 100644
--- a/src/ui/AvatarDesignPanelTranslator.java
+++ b/src/ui/AvatarDesignPanelTranslator.java
@@ -712,6 +712,12 @@ public class AvatarDesignPanelTranslator {
TraceManager.addDev("null gates in AVATAR relation: " + name1 + " " + name2);
}
}
+
+ // Attribute of the relation
+ r.setBlocking(port.isBlocking());
+ r.setAsynchronous(port.isAsynchronous());
+ r.setSizeOfFIFO(port.getSizeOfFIFO());
+
_as.addRelation(r);
}
}
diff --git a/src/ui/avatarbd/AvatarBDPortConnector.java b/src/ui/avatarbd/AvatarBDPortConnector.java
index d768997e97cf0b425293753e0aebbb521ac5f351..a59984c05eb3bfaa15e4e545537eeff147c797ae 100644
--- a/src/ui/avatarbd/AvatarBDPortConnector.java
+++ b/src/ui/avatarbd/AvatarBDPortConnector.java
@@ -73,6 +73,10 @@ public class AvatarBDPortConnector extends TGConnector implements ScalableTGCom
protected LinkedList<String> inSignalsAtDestination;
protected LinkedList<String> outSignalsAtOrigin;
+ protected boolean asynchronous;
+ protected int sizeOfFIFO;
+ protected boolean blockingFIFO;
+
public AvatarBDPortConnector(int _x, int _y, int _minX, int _minY, int _maxX, int _maxY, boolean _pos, TGComponent _father, TDiagramPanel _tdp, TGConnectingPoint _p1, TGConnectingPoint _p2, Vector _listPoint) {
@@ -80,6 +84,7 @@ public class AvatarBDPortConnector extends TGConnector implements ScalableTGCom
myImageIcon = IconManager.imgic202;
value = "";
editable = true;
+
oldScaleFactor = tdp.getZoom();
inSignalsAtOrigin = new LinkedList<String>();
inSignalsAtDestination = new LinkedList<String>();
@@ -95,17 +100,38 @@ public class AvatarBDPortConnector extends TGConnector implements ScalableTGCom
}*/
//g.drawLine(x1, y1, x2, y2);
+ Color col = g.getColor();
int cz = (int)(tdp.getZoom() * c);
+ if (isAsynchronous()) {
+ g.setColor(Color.WHITE);
+ }
g.fillRect(x2-(cz/2), y2-(cz/2), cz, cz);
g.fillRect(p1.getX()-(cz/2), p1.getY()-(cz/2), cz, cz);
+ g.setColor(col);
+ if (isAsynchronous()) {
+ g.drawRect(x2-(cz/2), y2-(cz/2), cz, cz);
+ g.drawRect(p1.getX()-(cz/2), p1.getY()-(cz/2), cz, cz);
+ if (isBlocking()) {
+ g.drawLine(x2-(cz/2), y2-(cz/2), x2-(cz/2)+cz, y2-(cz/2)+cz);
+ g.drawLine(x2-(cz/2), y2-(cz/2)+cz, x2-(cz/2)+cz, y2-(cz/2));
+ g.drawLine(p1.getX()-(cz/2), p1.getY()+(cz/2), p1.getX()+(cz/2), p1.getY()-(cz/2));
+ g.drawLine(p1.getX()-(cz/2), p1.getY()-(cz/2), p1.getX()+(cz/2), p1.getY()+(cz/2));
+ }
+ }
- Point p = GraphicLib.intersectionRectangleSegment(x2-(cz/2), y2-(cz/2), cz, cz, x1, y1, x2, y2);
- if (p == null) {
+ Point p11 = GraphicLib.intersectionRectangleSegment(p1.getX()-(cz/2), p1.getY()-(cz/2), cz, cz, x1, y1, x2, y2);
+ if (p11 == null) {
+ p11 = new Point(p1.getX(), p1.getY());
+ //System.out.println("null point");
+ }
+ Point p22 = GraphicLib.intersectionRectangleSegment(x2-(cz/2), y2-(cz/2), cz, cz, x1, y1, x2, y2);
+ if (p22 == null) {
+ p22 = new Point(p2.getX(), p2.getY());
//System.out.println("null point");
- } else {
- g.drawLine(x1, y1, p.x, p.y);
}
+ g.drawLine(p11.x, p11.y, p22.x, p22.y);
+
Font f = g.getFont();
Font fold = f;
f = f.deriveFont((float)fontSize);
@@ -205,7 +231,7 @@ public class AvatarBDPortConnector extends TGConnector implements ScalableTGCom
Vector v = getAssociationSignals();
JDialogSignalAssociation jdas = new JDialogSignalAssociation(frame, block1, block2, v, this, "Setting signal association");
- jdas.setSize(750, 400);
+ jdas.setSize(750, 500);
GraphicLib.centerOnParent(jdas);
jdas.show(); // blocked until dialog has been closed
@@ -237,6 +263,21 @@ public class AvatarBDPortConnector extends TGConnector implements ScalableTGCom
}
}
}
+
+ asynchronous = jdas.isAsynchronous();
+ blockingFIFO = jdas.isBlocking();
+
+ try {
+ sizeOfFIFO = Integer.decode(jdas.getSizeOfFIFO()).intValue();
+ sizeOfFIFO = Math.max(1, sizeOfFIFO);
+ } catch (Exception e) {
+ JOptionPane.showMessageDialog(frame,
+ "Unvalid FIFO size: " + jdas.getSizeOfFIFO(),
+ "Error",
+ JOptionPane.INFORMATION_MESSAGE);
+ return false;
+ }
+
return true;
}
@@ -262,6 +303,11 @@ public class AvatarBDPortConnector extends TGConnector implements ScalableTGCom
sb.append(oso);
sb.append("\" />\n");
}
+ sb.append("<FIFOType asynchronous=\"");
+ sb.append(asynchronous);
+ sb.append("\" size=\"" + sizeOfFIFO);
+ sb.append("\" blocking=\"" + blockingFIFO);
+ sb.append("\" />\n");
sb.append("</extraparam>\n");
return new String(sb);
@@ -272,7 +318,11 @@ public class AvatarBDPortConnector extends TGConnector implements ScalableTGCom
NodeList nli;
Node n1, n2;
Element elt;
- String val;
+ String val, val1, val2;
+ sizeOfFIFO = 1024;
+ blockingFIFO = false;
+ asynchronous = false;
+
//System.out.println("Loading attributes");
//System.out.println(nl.toString());
@@ -313,6 +363,38 @@ public class AvatarBDPortConnector extends TGConnector implements ScalableTGCom
if ((val != null) && (!(val.equals("null")))) {
outSignalsAtOrigin.add(val);
+ }
+ }
+ if (elt.getTagName().equals("FIFOType")) {
+ val = elt.getAttribute("asynchronous");
+ val1 = elt.getAttribute("size");
+ val2 = elt.getAttribute("blocking");
+
+ if ((val != null) && (!(val.equals("null")))) {
+ if (val.trim().toLowerCase().compareTo("true") == 0) {
+ asynchronous = true;
+ } else {
+ asynchronous = false;
+ }
+
+ }
+
+ if ((val1 != null) && (!(val1.equals("null")))) {
+ try {
+ sizeOfFIFO = Integer.decode(val1).intValue();
+ } catch(Exception e) {
+ sizeOfFIFO = 1024;
+ }
+ }
+
+
+ if ((val2 != null) && (!(val2.equals("null")))) {
+ if (val2.trim().toLowerCase().compareTo("true") == 0) {
+ blockingFIFO = true;
+ } else {
+ blockingFIFO = false;
+ }
+
}
}
}
@@ -498,5 +580,17 @@ public class AvatarBDPortConnector extends TGConnector implements ScalableTGCom
return _s.substring(0, index).trim();
}
+ public boolean isAsynchronous() {
+ return asynchronous;
+ }
+
+ public int getSizeOfFIFO() {
+ return sizeOfFIFO;
+ }
+
+ public boolean isBlocking() {
+ return blockingFIFO;
+ }
+
}
diff --git a/src/ui/window/JDialogSignalAssociation.java b/src/ui/window/JDialogSignalAssociation.java
index d1a49e70e8129d3e2b383a44d8628d4317f01398..7729d85c8eea01047cc94768fb8eee756e490246 100644
--- a/src/ui/window/JDialogSignalAssociation.java
+++ b/src/ui/window/JDialogSignalAssociation.java
@@ -63,7 +63,11 @@ public class JDialogSignalAssociation extends javax.swing.JDialog implements Act
private Vector available1, available2;
private AvatarBDPortConnector connector;
- private JPanel panel1, panel2;
+ private JRadioButton synchronous, asynchronous;
+ private JLabel labelFIFO;
+ private JTextField sizeOfFIFO;
+ private JCheckBox blocking;
+ private JPanel panel1, panel2, panel3;
private boolean cancelled = false;
@@ -112,9 +116,11 @@ public class JDialogSignalAssociation extends javax.swing.JDialog implements Act
GridBagLayout gridbag0 = new GridBagLayout();
GridBagLayout gridbag1 = new GridBagLayout();
GridBagLayout gridbag2 = new GridBagLayout();
+ GridBagLayout gridbag3 = new GridBagLayout();
GridBagConstraints c0 = new GridBagConstraints();
GridBagConstraints c1 = new GridBagConstraints();
GridBagConstraints c2 = new GridBagConstraints();
+ GridBagConstraints c3 = new GridBagConstraints();
setFont(new Font("Helvetica", Font.PLAIN, 14));
c.setLayout(gridbag0);
@@ -130,6 +136,11 @@ public class JDialogSignalAssociation extends javax.swing.JDialog implements Act
panel2.setLayout(gridbag2);
panel2.setBorder(new javax.swing.border.TitledBorder("Managing Signals"));
panel2.setPreferredSize(new Dimension(300, 250));
+
+ panel3 = new JPanel();
+ panel3.setLayout(gridbag3);
+ panel3.setBorder(new javax.swing.border.TitledBorder("Connector type"));
+ panel3.setPreferredSize(new Dimension(600, 100));
// first line panel1
c1.weighty = 1.0;
@@ -206,7 +217,39 @@ public class JDialogSignalAssociation extends javax.swing.JDialog implements Act
removeButton = new JButton("Remove signals");
removeButton.addActionListener(this);
panel2.add(removeButton, c2);
-
+
+ // panel3
+ c3.gridwidth = GridBagConstraints.REMAINDER; //end row
+ c3.fill = GridBagConstraints.BOTH;
+ c3.gridheight = 1;
+ c3.weighty = 1;
+ c3.weightx = 10.0;
+ synchronous = new JRadioButton("synchronous");
+ synchronous.addActionListener(this);
+ panel3.add(synchronous, c3);
+ asynchronous = new JRadioButton("asynchronous");
+ asynchronous.addActionListener(this);
+ panel3.add(asynchronous, c3);
+ ButtonGroup bt = new ButtonGroup();
+ bt.add(synchronous);
+ bt.add(asynchronous);
+ asynchronous.setSelected(connector.isAsynchronous());
+ synchronous.setSelected(!connector.isAsynchronous());
+
+ c3.gridwidth = 3;
+ labelFIFO = new JLabel("Size of FIFO:");
+ panel3.add(labelFIFO, c3);
+ c3.gridwidth = GridBagConstraints.REMAINDER; //end row
+ sizeOfFIFO = new JTextField(""+connector.getSizeOfFIFO());
+ panel3.add(sizeOfFIFO, c3);
+
+ blocking = new JCheckBox("Blocking on write when FIFO is full");
+ blocking.setSelected(connector.isBlocking());
+ panel3.add(blocking, c3);
+
+ updateSynchronousElements();
+
+
// main panel;
c0.gridwidth = 1;
c0.gridheight = 10;
@@ -216,6 +259,7 @@ public class JDialogSignalAssociation extends javax.swing.JDialog implements Act
c.add(panel1, c0);
c0.gridwidth = GridBagConstraints.REMAINDER; //end row
c.add(panel2, c0);
+ c.add(panel3, c0);
c0.gridwidth = 1;
c0.gridheight = 1;
@@ -250,9 +294,20 @@ public class JDialogSignalAssociation extends javax.swing.JDialog implements Act
updateAddButton();
} else if (evt.getSource() == signalsBlock2) {
updateAddButton();
- }
+ } else if (evt.getSource() == synchronous) {
+ updateSynchronousElements();
+ } else if (evt.getSource() == asynchronous) {
+ updateSynchronousElements();
+ }
}
+ private void updateSynchronousElements() {
+ boolean b = asynchronous.isSelected();
+ labelFIFO.setEnabled(b);
+ sizeOfFIFO.setEnabled(b);
+ blocking.setEnabled(b);
+ }
+
private void updateAddButton() {
TraceManager.addDev("updateAddButton");
int i1 = signalsBlock1.getSelectedIndex();
@@ -382,5 +437,17 @@ public class JDialogSignalAssociation extends javax.swing.JDialog implements Act
}
}
}
+
+ public boolean isAsynchronous() {
+ return asynchronous.isSelected();
+ }
+
+ public String getSizeOfFIFO() {
+ return sizeOfFIFO.getText();
+ }
+
+ public boolean isBlocking() {
+ return blocking.isSelected();
+ }
}