diff --git a/src/tepe/TEPEPropertyComponent.java b/src/tepe/TEPEPropertyComponent.java
index efd2e440dc9a263794d8c07b0e5b6fe37eb4d82c..dc06b3904ce08c17360631965ecaf8d1a04ad81f 100644
--- a/src/tepe/TEPEPropertyComponent.java
+++ b/src/tepe/TEPEPropertyComponent.java
@@ -55,6 +55,8 @@ public class TEPEPropertyComponent extends TEPEComponent {
public static final int NON_LIVENESS = 1;
public static final int REACHABILITY = 2;
public static final int NON_REACHABILITY = 3;
+ public static final int SAFETY = 4;
+ public static final int NON_SAFETY = 5;
protected int type;
@@ -83,8 +85,13 @@ public class TEPEPropertyComponent extends TEPEComponent {
ret += "reachability";
break;
case 3:
- default:
ret += "non reachability";
+ break;
+ case 4:
+ ret += "safety";
+ break;
+ default:
+ ret += "non safety";
}
return ret;
diff --git a/src/tmltranslator/toturtle/TML2TURTLE.java b/src/tmltranslator/toturtle/TML2TURTLE.java
index 7bb4e1261fffa2cab40c931bf214db3b344f4343..124d59c953e6b5da73a8383436e115819882d3d1 100755
--- a/src/tmltranslator/toturtle/TML2TURTLE.java
+++ b/src/tmltranslator/toturtle/TML2TURTLE.java
@@ -172,7 +172,9 @@ public class TML2TURTLE {
while(iterator.hasNext()) {
event = (TMLEvent)(iterator.next());
+ TraceManager.addDev("Making event");
if (event.isInfinite()) {
+ TraceManager.addDev("Making event infinite");
tce = new TClassEventInfinite(nameEvent + event.getName(), event.getName(), event.getNbOfParams());
tce.addWriteGate();
tce.addReadGate();
diff --git a/src/translator/TClassEventInfinite.java b/src/translator/TClassEventInfinite.java
index f81d65886961e0397441c94aff7804fbf86a5d27..7f9aa5344d36bcc1ba6a8e6f986f0419d29bf900 100755
--- a/src/translator/TClassEventInfinite.java
+++ b/src/translator/TClassEventInfinite.java
@@ -47,6 +47,8 @@ package translator;
import java.util.*;
+import myutil.*;
+
public class TClassEventInfinite extends TClass implements FIFOInfiniteAndGetSizeTClass, TClassEventCommon {
private int nbPara;
private LinkedList sendReqGates;
@@ -133,11 +135,14 @@ public class TClassEventInfinite extends TClass implements FIFOInfiniteAndGetSiz
return g;
}
- public void makeTClass(boolean _isLossy, int _maxNbOfLoss) {
+ public void makeTClass(boolean _lossy, int _maxNbOfLoss) {
Gate forward_0, forward_1, g;
ADActionStateWithGate adag;
+ Gate loss = null, notloss = null;
+ ADActionStateWithGate aclost, acnotlost;
//ADActionStateWithGate adagsize1, adagsize2, adagsize3;
ADActionStateWithParam adac1, adac2, adac3;
+ Param pmax, currentLoss;
ADParallel adpar0, adpar1;
ADStop adstop;
ADJunction adj1, adj2, adj3, adj4, adj5, adj6, adj7;
@@ -147,6 +152,8 @@ public class TClassEventInfinite extends TClass implements FIFOInfiniteAndGetSiz
int i;
ListIterator iterator;
String action;
+
+ ADComponent comp;
ActivityDiagram ad = new ActivityDiagram();
setActivityDiagram(ad);
@@ -171,6 +178,13 @@ public class TClassEventInfinite extends TClass implements FIFOInfiniteAndGetSiz
nb = new Param("nb", Param.NAT, "0");
addParameter(nb);
+
+ if ((_lossy) && (_maxNbOfLoss > -1)) {
+ pmax = new Param("maxLoss", Param.NAT, ""+_maxNbOfLoss);
+ addParameter(pmax);
+ currentLoss = new Param("currentLoss", Param.NAT, "0");
+ addParameter(currentLoss);
+ }
/*maxs = new Param("maxs", Param.NAT, ""+maxSamples);
addParameter(maxs);*/
@@ -183,6 +197,11 @@ public class TClassEventInfinite extends TClass implements FIFOInfiniteAndGetSiz
forward_0 = addNewGateIfApplicable("forward_0");
forward_1 = addNewGateIfApplicable("forward_1");
+
+ if (_lossy) {
+ loss = addNewGateIfApplicable("msglost__" + eventName);
+ notloss = addNewGateIfApplicable("msgNotLost__" + eventName);
+ }
adpar0 = new ADParallel();
adpar0.setValueGate("[forward_0, forward_1]");
@@ -289,59 +308,89 @@ public class TClassEventInfinite extends TClass implements FIFOInfiniteAndGetSiz
// If there is a loss -> no forward
- adag = new ADActionStateWithGate(forward_0);
- ad.add(adag);
- action = "";
- for(i=0; i<nbPara; i++) {
- action += "!pb" + i + "";
- }
- action+="!index";
- adag.setActionValue(action);
- adj4.addNext(adag);
-
- adac1 = new ADActionStateWithParam(index);
- ad.add(adac1);
- adac1.setActionValue("index+1");
- adag.addNext(adac1);
-
- adj5 = new ADJunction();
- ad.add(adj5);
- adj5.addNext(adj2);
-
- adj6 = new ADJunction();
- ad.add(adj6);
- //adch4.addNext(adj6);
- //adch4.addGuard("[nb==maxs]");
-
- adag = new ADActionStateWithGate(forward_1);
- ad.add(adag);
- action = "";
- for(i=0; i<nbPara; i++) {
- action += "?pa" + i + ":nat";
- }
- action += "!index_r";
- adag.setActionValue(action);
- adj6.addNext(adag);
-
- adac3 = new ADActionStateWithParam(index_r);
- ad.add(adac3);
- adac3.setActionValue("index_r+1");
- adag.addNext(adac3);
- adac3.addNext(adj5);
-
- adac2 = new ADActionStateWithParam(nb);
- ad.add(adac2);
- adac2.setActionValue("nb+1");
- adac1.addNext(adac2);
-
- adch6 = new ADChoice();
- ad.add(adch6);
- adac2.addNext(adch6);
-
- adch6.addNext(adj5);
- adch6.addGuard("[not(nb==1)]");
- adch6.addNext(adj6);
- adch6.addGuard("[nb==1]");
+ if (_lossy) {
+ TraceManager.addDev("Lossy");
+ ADChoice adchloss = new ADChoice();
+ ad.add(adchloss);
+ adj4.addNext(adchloss);
+
+
+
+ adchloss.addGuard("[]");
+ adchloss.addGuard("[]");
+
+ // loss ...
+ adag = new ADActionStateWithGate(loss);
+ ad.add(adag);
+ adag.setActionValue("");
+ adag.addNext(adj2);
+ adchloss.addNext(adag);
+
+ // no loss
+ adag = new ADActionStateWithGate(notloss);
+ ad.add(adag);
+ adag.setActionValue("");
+ adag.addNext(adj2);
+ adchloss.addNext(adag);
+ comp = adag;
+
+ } else {
+ TraceManager.addDev("Not lossy");
+ comp = adj4;
+ }
+ adag = new ADActionStateWithGate(forward_0);
+ ad.add(adag);
+ action = "";
+ for(i=0; i<nbPara; i++) {
+ action += "!pb" + i + "";
+ }
+ action+="!index";
+ adag.setActionValue(action);
+ comp.addNext(adag);
+
+ adac1 = new ADActionStateWithParam(index);
+ ad.add(adac1);
+ adac1.setActionValue("index+1");
+ adag.addNext(adac1);
+
+ adj5 = new ADJunction();
+ ad.add(adj5);
+ adj5.addNext(adj2);
+
+ adj6 = new ADJunction();
+ ad.add(adj6);
+ //adch4.addNext(adj6);
+ //adch4.addGuard("[nb==maxs]");
+
+ adag = new ADActionStateWithGate(forward_1);
+ ad.add(adag);
+ action = "";
+ for(i=0; i<nbPara; i++) {
+ action += "?pa" + i + ":nat";
+ }
+ action += "!index_r";
+ adag.setActionValue(action);
+ adj6.addNext(adag);
+
+ adac3 = new ADActionStateWithParam(index_r);
+ ad.add(adac3);
+ adac3.setActionValue("index_r+1");
+ adag.addNext(adac3);
+ adac3.addNext(adj5);
+
+ adac2 = new ADActionStateWithParam(nb);
+ ad.add(adac2);
+ adac2.setActionValue("nb+1");
+ adac1.addNext(adac2);
+
+ adch6 = new ADChoice();
+ ad.add(adch6);
+ adac2.addNext(adch6);
+
+ adch6.addNext(adj5);
+ adch6.addGuard("[not(nb==1)]");
+ adch6.addNext(adj6);
+ adch6.addGuard("[nb==1]");
// Wait event branch
adj7 = new ADJunction();
diff --git a/src/ui/AvatarRequirementPanelTranslator.java b/src/ui/AvatarRequirementPanelTranslator.java
index 0f9b7cc440e4922daf930250f150cf535a6129dd..4065111e0eeaa59318ec5696641421d801f90699 100644
--- a/src/ui/AvatarRequirementPanelTranslator.java
+++ b/src/ui/AvatarRequirementPanelTranslator.java
@@ -176,6 +176,10 @@ public class AvatarRequirementPanelTranslator {
type = TEPEPropertyComponent.REACHABILITY;
} else if (apdp.isNotRechability()) {
type = TEPEPropertyComponent.NON_REACHABILITY;
+ } else if (apdp.isSafety()) {
+ type = TEPEPropertyComponent.SAFETY;
+ } else if (apdp.isNotSafety()) {
+ type = TEPEPropertyComponent.NON_SAFETY;
}
TEPEPropertyComponent tepepropertyc = new TEPEPropertyComponent("Property", tgc, type);
diff --git a/src/ui/avatarpd/AvatarPDProperty.java b/src/ui/avatarpd/AvatarPDProperty.java
index de13616b1f44fce21588837330c916ddbc6340b0..2e742287459fdf069f795c0398e358284bb6198d 100644
--- a/src/ui/avatarpd/AvatarPDProperty.java
+++ b/src/ui/avatarpd/AvatarPDProperty.java
@@ -64,8 +64,8 @@ public class AvatarPDProperty extends TGCScalableWithInternalComponent implement
protected String oldValue = "";
protected String description = "";
private String stereotype = "property";
- private boolean liveness = true;
- private boolean not = false;
+ private int kind = 0; //0: liveness, 1 reachability, 2 safety
+ private boolean not = false; // Negation of property
private int maxFontSize = 12;
private int minFontSize = 4;
@@ -201,10 +201,12 @@ public class AvatarPDProperty extends TGCScalableWithInternalComponent implement
// Liveness
h+= currentFontSize + sizeBetweenNameAndLiveness;
String state;
- if (liveness) {
+ if (kind == 0) {
state = "liveness";
- } else {
+ } else if (kind == 1) {
state = "reachability";
+ } else {
+ state = "safety";
}
if (not) {
state = "not " + state;
@@ -237,8 +239,8 @@ public class AvatarPDProperty extends TGCScalableWithInternalComponent implement
public boolean editOndoubleClick(JFrame frame) {
String oldValue = value;
- JDialogAvatarProperty jdap = new JDialogAvatarProperty(frame, value, liveness, not);
- jdap.setSize(300, 230);
+ JDialogAvatarProperty jdap = new JDialogAvatarProperty(frame, value, kind, not);
+ jdap.setSize(300, 280);
GraphicLib.centerOnParent(jdap);
jdap.setVisible(true); // blocked until dialog has been closed
@@ -246,8 +248,17 @@ public class AvatarPDProperty extends TGCScalableWithInternalComponent implement
return false;
}
- liveness = jdap.isLivenessSelected() || jdap.isNotLivenessSelected();
- not = jdap.isNotLivenessSelected() || jdap.isNotReachabilitySelected();
+ if (jdap.isLivenessSelected()) {
+ kind = 0;
+ }
+ if (jdap.isReachabilitySelected()) {
+ kind = 1;
+ }
+ if (jdap.isSafetySelected()) {
+ kind = 2;
+ }
+
+ not = jdap.isNotLivenessSelected() || jdap.isNotReachabilitySelected() || jdap.isNotSafetySelected();
String s = jdap.getName();
if ((s != null) && (s.length() > 0) && (!s.equals(oldValue))) {
@@ -269,7 +280,7 @@ public class AvatarPDProperty extends TGCScalableWithInternalComponent implement
protected String translateExtraParam() {
StringBuffer sb = new StringBuffer("<extraparam>\n");
sb.append("<liveness data=\"");
- sb.append(liveness);
+ sb.append(""+kind);
sb.append("\" />\n");
sb.append("<not data=\"");
sb.append(not);
@@ -300,11 +311,25 @@ public class AvatarPDProperty extends TGCScalableWithInternalComponent implement
if (elt.getTagName().equals("liveness")) {
//System.out.println("Analyzing line1");
s = elt.getAttribute("data");
+
+ //TraceManager.addDev("s=" + s);
if (s.equals("true")) {
- liveness = true;
- } else {
- liveness = false;
- }
+ kind = 0;
+ }
+ if (s.equals("false")) {
+ kind = 1;
+ }
+ if (s.equals("0")) {
+ kind = 0;
+ }
+ if (s.equals("1")) {
+ kind = 1;
+ }
+ if (s.equals("2")) {
+ kind = 2;
+ }
+
+ //TraceManager.addDev("Loaded kind=" + kind);
}
if (elt.getTagName().equals("not")) {
//System.out.println("Analyzing line1");
@@ -354,18 +379,26 @@ public class AvatarPDProperty extends TGCScalableWithInternalComponent implement
}
public boolean isLiveness() {
- return (liveness && !not);
+ return ((kind == 0) && !not);
}
public boolean isNotLiveness() {
- return (liveness && not);
+ return ((kind == 0) && not);
}
public boolean isRechability() {
- return (!liveness && !not);
+ return ((kind == 1) && !not);
}
public boolean isNotRechability() {
- return (!liveness && not);
+ return ((kind == 1) && not);
+ }
+
+ public boolean isSafety() {
+ return ((kind == 2) && !not);
+ }
+
+ public boolean isNotSafety() {
+ return ((kind == 2) && not);
}
}
diff --git a/src/ui/window/JDialogAvatarProperty.java b/src/ui/window/JDialogAvatarProperty.java
index 31d69fa80fe00cbecadbd4aeeab84d3bbf687a2e..5a6ee2d9a310c760b293b6501529890799c26452 100755
--- a/src/ui/window/JDialogAvatarProperty.java
+++ b/src/ui/window/JDialogAvatarProperty.java
@@ -56,10 +56,11 @@ public class JDialogAvatarProperty extends javax.swing.JDialog implements Action
private JPanel panel1;
private String name;
- private boolean livenessSelected, notSelected;
+ private int kind;
+ boolean notSelected;
private boolean hasBeenCancelled = false;
private JTextField myName;
- private JRadioButton reachability, liveness, notReachability, notLiveness;
+ private JRadioButton safety, notSafety, reachability, liveness, notReachability, notLiveness;
// Main Panel
private JButton closeButton;
@@ -68,12 +69,12 @@ public class JDialogAvatarProperty extends javax.swing.JDialog implements Action
//private String id1, id2;
/** Creates new form */
- public JDialogAvatarProperty(Frame f, String _name, boolean _livenessSelected, boolean _notSelected) {
+ public JDialogAvatarProperty(Frame f, String _name, int _kind, boolean _notSelected) {
super(f, "Setting property attributes", true);
name = _name;
- livenessSelected = _livenessSelected;
+ kind = _kind;
notSelected = _notSelected;
initComponents();
@@ -102,7 +103,7 @@ public class JDialogAvatarProperty extends javax.swing.JDialog implements Action
panel1.setBorder(new javax.swing.border.TitledBorder("Property"));
- panel1.setPreferredSize(new Dimension(200, 150));
+ //panel1.setPreferredSize(new Dimension(200, 150));
// first line panel1
c1.weighty = 1.0;
@@ -120,29 +121,41 @@ public class JDialogAvatarProperty extends javax.swing.JDialog implements Action
c1.gridwidth = GridBagConstraints.REMAINDER; //end row
reachability = new JRadioButton("Reachable");
- reachability.setSelected(!livenessSelected && !notSelected);
+ reachability.setSelected((kind == 1) && !notSelected);
panel1.add(reachability, c1);
c1.gridwidth = GridBagConstraints.REMAINDER; //end row
notReachability = new JRadioButton("Not reachable");
- notReachability.setSelected(!livenessSelected && notSelected);
+ notReachability.setSelected((kind == 1) && notSelected);
panel1.add(notReachability, c1);
c1.gridwidth = GridBagConstraints.REMAINDER; //end row
liveness = new JRadioButton("Liveness");
- liveness.setSelected(livenessSelected && !notSelected);
+ liveness.setSelected((kind == 0) && !notSelected);
panel1.add(liveness, c1);
c1.gridwidth = GridBagConstraints.REMAINDER; //end row
notLiveness = new JRadioButton("Not Liveness");
- notLiveness.setSelected(livenessSelected && notSelected);
+ notLiveness.setSelected((kind == 0) && notSelected);
panel1.add(notLiveness, c1);
+ c1.gridwidth = GridBagConstraints.REMAINDER; //end row
+ safety = new JRadioButton("Safety");
+ safety.setSelected((kind == 2) && !notSelected);
+ panel1.add(safety, c1);
+
+ c1.gridwidth = GridBagConstraints.REMAINDER; //end row
+ notSafety = new JRadioButton("Not Safety");
+ notSafety.setSelected((kind == 2) && notSelected);
+ panel1.add(notSafety, c1);
+
ButtonGroup bg = new ButtonGroup();
bg.add(reachability);
bg.add(liveness);
bg.add(notReachability);
bg.add(notLiveness);
+ bg.add(safety);
+ bg.add(notSafety);
// main panel;
c0.gridwidth = 1;
@@ -202,6 +215,14 @@ public class JDialogAvatarProperty extends javax.swing.JDialog implements Action
return notLiveness.isSelected();
}
+ public boolean isSafetySelected() {
+ return safety.isSelected();
+ }
+
+ public boolean isNotSafetySelected() {
+ return notSafety.isSelected();
+ }
+
public String getName() {
return myName.getText();
}