diff --git a/src/avatartranslator/AvatarRelation.java b/src/avatartranslator/AvatarRelation.java
index 94e9c506288b789144038e16aa113883e8ae2f68..9a48fb265bee4267f714b6d33bd480107c682694 100644
--- a/src/avatartranslator/AvatarRelation.java
+++ b/src/avatartranslator/AvatarRelation.java
@@ -206,5 +206,35 @@ public class AvatarRelation extends AvatarElement {
return signals2.indexOf(sig);
}
+ /*public void makeRobustness() {
+ LinkedList<AvatarSignal> signals1_tmp = new LinkedList<AvatarSignal>();
+ LinkedList<AvatarSignal> signals2_tmp = new LinkedList<AvatarSignal>();
+ AvatarSignal as1, as2, astmp;
+ for(int i=0; i<signals1.size(); i++) {
+ as1 = signals1.get(i);
+ as2 = signals2.get(i);
+
+ if (as1.isOut()) {
+ astmp = as2;
+ as2 = as1;
+ as1 = astmp;
+ }
+
+ signals1_tmp.add(as1);
+ astmp = new AvatarSignal(as1.getName() + "__in", AvatarSignal.IN, as1.getReferenceObject());
+ astmp.setInOut(AvatarSignal.IN);
+ signals2_tmp.add(astmp);
+
+
+ astmp = new AvatarSignal(as2.getName() + "__out", AvatarSignal.OUT, as2.getReferenceObject());
+ astmp.setInOut(AvatarSignal.OUT);
+ signals1_tmp.add(astmp);
+ signals2_tmp.add(as2);
+ }
+
+ signals1 = signals1_tmp;
+ signals2 = signals2_tmp;
+ }*/
+
}
\ No newline at end of file
diff --git a/src/avatartranslator/AvatarSpecification.java b/src/avatartranslator/AvatarSpecification.java
index 0f3dca3249ef867183a20e295ab8687892617015..373068eb7d5a752294aedfcd0772182d6809ec71 100644
--- a/src/avatartranslator/AvatarSpecification.java
+++ b/src/avatartranslator/AvatarSpecification.java
@@ -60,6 +60,8 @@ public class AvatarSpecification extends AvatarElement {
//private AvatarBroadcast broadcast;
private LinkedList<String> pragmas;
+
+ private boolean robustnessMade = false;
public AvatarSpecification(String _name, Object _referenceObject) {
@@ -368,4 +370,96 @@ public class AvatarSpecification extends AvatarElement {
return guard.compareTo("[else]") == 0;
}
+ public boolean hasLossyChannel() {
+ for(AvatarRelation relation: relations) {
+ if (relation.isLossy()) {
+ return true;
+ }
+ }
+
+ return false;
+ }
+
+
+ public void makeRobustness() {
+ TraceManager.addDev("Make robustness");
+ if (robustnessMade) {
+ return;
+ }
+
+ /*robustnessMade = true;
+
+ TraceManager.addDev("Testing lossy channels");
+
+ if (hasLossyChannel()) {
+ TraceManager.addDev("Making robustness");
+ int idstate = 0;
+ for(AvatarBlock block: blocks) {
+ idstate = block.getStateMachine().makeMessageLostRobustness(idstate);
+ }
+
+ /*AvatarBlock ab = new AvatarBlock("Robustness__", this.getReferenceObject());
+ addBlock(ab);
+ AvatarMethod am = new AvatarMethod("messageLost", null);
+ ab.addMethod(am);
+ AvatarStateMachine asm = ab.getStateMachine();
+ AvatarStartState ass = new AvatarStartState("StartState", null);
+ asm.addElement(ass);
+ asm.setStartState(ass);
+ AvatarTransition at = new AvatarTransition("Transition", null);
+ asm.addElement(at);
+ ass.addNext(at);
+ AvatarState state = new AvatarState("MainState", null);
+ asm.addElement(state);
+ at.addNext(state);
+
+ // Parsing all state machines to add robustness
+ AvatarStateMachine sm;
+ AvatarActionOnSignal aaos;
+ AvatarSignal as;
+ AvatarState state0;
+ int i;
+
+ for(AvatarRelation ar: relations) {
+ if (ar.isAsynchronous() && ar.isLossy()) {
+ // Modify the relation
+ ar.makeRobustness();
+ for(i=0; i<ar.nbOfSignals(); i = i+2) {
+ as = ar.getInSignal(i);
+ at = new AvatarTransition("TransitionToReceiving", null);
+ asm.addElement(at);
+ state.addNext(at);
+ aaos = new AvatarActionOnSignal("Receiving__" + as.getName(), as, null);
+ asm.addElement(aaos);
+ at.addNext(aaos);
+ at = new AvatarTransition("TransitionToIntermediateState", null);
+ asm.addElement(at);
+ state0 = new AvatarState("Choice__" + as.getName(), null);
+ asm.addElement(state0);
+ aaos.addNext(at);
+ at.addNext(state0);
+ at = new AvatarTransition("TransitionToMainState", null);
+ at.addAction("messageLost()");
+ asm.addElement(at);
+ state0.addNext(at);
+ at.addNext(state);
+
+ as = ar.getOutSignal(i+1);
+ at = new AvatarTransition("TransitionToSending", null);
+ asm.addElement(at);
+ aaos = new AvatarActionOnSignal("Sending__" + as.getName(), as, null);
+ asm.addElement(aaos);
+ state0.addNext(at);
+ at.addNext(aaos);
+ at = new AvatarTransition("TransitionAfterSending", null);
+ asm.addElement(at);
+ aaos.addNext(at);
+ at.addNext(state);
+ }
+
+ }
+ }
+ }*/
+ }
+
}
\ No newline at end of file
diff --git a/src/avatartranslator/directsimulation/AvatarSimulationBlock.java b/src/avatartranslator/directsimulation/AvatarSimulationBlock.java
index e0952117c79725142afe4684b6c061f8d7c310d1..d62d5c8a3488bdba5cfdb23aaa7beef7f1c7d760 100644
--- a/src/avatartranslator/directsimulation/AvatarSimulationBlock.java
+++ b/src/avatartranslator/directsimulation/AvatarSimulationBlock.java
@@ -466,6 +466,8 @@ public class AvatarSimulationBlock {
ast.actions.add(myAction);
}
+ ast.isLost = _aspt.isLost;
+
} else if ((!(_aspt.isSending)) && (_aspt.linkedAsynchronousMessage != null)) {
// Asynchronous Receiving
String myAction = "";
diff --git a/src/avatartranslator/directsimulation/AvatarSimulationPendingTransaction.java b/src/avatartranslator/directsimulation/AvatarSimulationPendingTransaction.java
index c2ed35a166135ebb29f08061062d1f50382d041c..7b499f01e69835e2efa541f5df14a4f2de0d6ddd 100644
--- a/src/avatartranslator/directsimulation/AvatarSimulationPendingTransaction.java
+++ b/src/avatartranslator/directsimulation/AvatarSimulationPendingTransaction.java
@@ -95,6 +95,9 @@ public class AvatarSimulationPendingTransaction {
// broadcast
public boolean isBroadcast;
+ // Lost
+ public boolean isLost;
+
public AvatarSimulationPendingTransaction() {
diff --git a/src/avatartranslator/directsimulation/AvatarSimulationTransaction.java b/src/avatartranslator/directsimulation/AvatarSimulationTransaction.java
index ad7cd55635b421b1a997db52b412e44984cdde10..dee6cdcc8aee671bcbd483f12032c77a144e1830 100644
--- a/src/avatartranslator/directsimulation/AvatarSimulationTransaction.java
+++ b/src/avatartranslator/directsimulation/AvatarSimulationTransaction.java
@@ -85,6 +85,7 @@ public class AvatarSimulationTransaction {
public boolean isBroadcast;
public boolean isSolo; // Used in broadcast transactions to know whether the signal was forwarded to other elements, or not
+ public boolean isLost; // Used in lossy channel to know whether the message was lost or not
public AvatarSimulationTransaction(AvatarStateMachineElement _executeElement) {
executedElement = _executeElement;
diff --git a/src/avatartranslator/directsimulation/AvatarSpecificationSimulation.java b/src/avatartranslator/directsimulation/AvatarSpecificationSimulation.java
index cf45311fbea79a5ab48fa87bfa0a4c09685c462f..4a90c8d850a83e690a1bd5c3f5966c9fb718cfbe 100644
--- a/src/avatartranslator/directsimulation/AvatarSpecificationSimulation.java
+++ b/src/avatartranslator/directsimulation/AvatarSpecificationSimulation.java
@@ -132,6 +132,11 @@ public class AvatarSpecificationSimulation {
// Remove timers
avspec.removeTimers();
+
+ // Robustness
+ avspec.makeRobustness();
+
+ TraceManager.addDev("Spec:" + avspec.toString());
}
public void reset() {
@@ -925,7 +930,18 @@ public class AvatarSpecificationSimulation {
// Get the index of the signal in the relation
AvatarSimulationAsynchronousTransaction asat = new AvatarSimulationAsynchronousTransaction(rel, rel.getIndexOfSignal(sig));
_aspt.linkedAsynchronousMessage = asat;
- asynchronousMessages.add(asat);
+ // Testing whether the message can be lost or not
+ if (rel.isLossy()) {
+ int ra = ((int)(Math.random()*100))%2;
+ if (ra == 0) {
+ _aspt.isLost = true;
+ } else {
+ _aspt.isLost = false;
+ asynchronousMessages.add(asat);
+ }
+ } else {
+ asynchronousMessages.add(asat);
+ }
} else {
// Must remove the asynchronous operation, and give the parameters
AvatarSimulationAsynchronousTransaction asat = getAsynchronousMessage(rel, sig);
diff --git a/src/avatartranslator/touppaal/AVATAR2UPPAAL.java b/src/avatartranslator/touppaal/AVATAR2UPPAAL.java
index 1d674b476e3dbb00093cc99883040741825e6aff..05f9343c68e86325ed89bdecdf2df2503c949097 100755
--- a/src/avatartranslator/touppaal/AVATAR2UPPAAL.java
+++ b/src/avatartranslator/touppaal/AVATAR2UPPAAL.java
@@ -155,6 +155,8 @@ public class AVATAR2UPPAAL {
avspec.removeCompositeStates();
avspec.removeTimers();
+ avspec.makeRobustness();
+
TraceManager.addDev("-> Spec:" + avspec.toString());
@@ -375,6 +377,12 @@ public class AVATAR2UPPAAL {
//spec.addGlobalDeclaration("int " + action + TURTLE2UPPAAL.SYNCID + " = 0;\n");
}
+ if (avspec.hasLossyChannel()) {
+ tr = addTransition(templateNotSynchronized, loc, loc);
+ setSynchronization(tr, "messageLost__?");
+ //addGuard(tr, action + TURTLE2UPPAAL.SYNCID + " == 0");
+ spec.addGlobalDeclaration("urgent chan messageLost__;\n");
+ }
}
@@ -390,7 +398,7 @@ public class AVATAR2UPPAAL {
spec.addTemplate(templateAsynchronous);
UPPAALLocation loc = addLocation(templateAsynchronous);
templateAsynchronous.setInitLocation(loc);
- UPPAALTransition tr;
+ UPPAALTransition tr, tr1;
spec.addGlobalDeclaration("\n//Declarations for asynchronous channels\n");
String action;
@@ -451,16 +459,22 @@ public class AVATAR2UPPAAL {
templateAsynchronous.addDeclaration(enqueue);
templateAsynchronous.addDeclaration(dequeue);
- tr = addTransition(templateAsynchronous, loc, loc);
- setSynchronization(tr, signalToUPPAALString(sig1)+"?");
- setGuard(tr, "size__" + name0 + " <" + ar.getSizeOfFIFO());
- setAssignment(tr, "enqueue__" + name0 + "()");
-
- // If lossy ...
if (ar.isLossy()) {
+ UPPAALLocation loc1 = addLocation(templateAsynchronous);
+ loc1.setCommitted();
+ tr = addTransition(templateAsynchronous, loc, loc1);
+ setSynchronization(tr, signalToUPPAALString(sig1)+"?");
+ setGuard(tr, "size__" + name0 + " <" + ar.getSizeOfFIFO());
+ tr = addTransition(templateAsynchronous, loc1, loc);
+ setSynchronization(tr, "messageLost!");
+ tr = addTransition(templateAsynchronous, loc1, loc);
+ setAssignment(tr, "enqueue__" + name0 + "()");
+
+ } else {
tr = addTransition(templateAsynchronous, loc, loc);
setSynchronization(tr, signalToUPPAALString(sig1)+"?");
setGuard(tr, "size__" + name0 + " <" + ar.getSizeOfFIFO());
+ setAssignment(tr, "enqueue__" + name0 + "()");
}
tr = addTransition(templateAsynchronous, loc, loc);
diff --git a/src/ui/avatarinteractivesimulation/AvatarSpecificationSimulationSDPanel.java b/src/ui/avatarinteractivesimulation/AvatarSpecificationSimulationSDPanel.java
index f00836fe8e59603ff415fdf14dc86080315bc592..936b5b2247c0975c6ede305280383c29f799e634 100644
--- a/src/ui/avatarinteractivesimulation/AvatarSpecificationSimulationSDPanel.java
+++ b/src/ui/avatarinteractivesimulation/AvatarSpecificationSimulationSDPanel.java
@@ -531,6 +531,10 @@ public class AvatarSpecificationSimulationSDPanel extends JPanel implements Mous
GraphicLib.arrowWithLine(g, 1, 2, 10, currentX, currentY, currentX+lengthAsync, currentY, false);
points.add(new Point(currentX, currentY));
transactionsOfPoints.add(ast);
+
+ if (ast.isLost) {
+ g.fillOval(currentX+lengthAsync, currentY-5, 10,10);
+ }
// Putting the message name
w = g.getFontMetrics().stringWidth(messageName);