diff --git a/src/avatartranslator/AvatarBlock.java b/src/avatartranslator/AvatarBlock.java
index 4c7005c9d2491877eb34cc4c3991f7c7986335c4..6cc1f7b2a877b9f1973d6498b8218c7e48fd5742 100644
--- a/src/avatartranslator/AvatarBlock.java
+++ b/src/avatartranslator/AvatarBlock.java
@@ -542,78 +542,4 @@ public class AvatarBlock extends AvatarElement {
}
return cpt;
}
-
- public AvatarState removeElseGuards() {
- if (asm == null) {
- return null;
- }
-
- AvatarStateMachineElement asme0;
- AvatarTransition at = null, at0;
- int nbOfElse;
- String guard, g;
- int i;
-
- for(AvatarStateMachineElement asme :asm.getListOfElements()) {
- if (asme instanceof AvatarState) {
- // Has only one "else" transition?
- if (asme.nbOfNexts() > 0) {
- // Search for several "else"
- nbOfElse = 0;
- for(i=0; i<asme.nbOfNexts(); i++) {
- asme0 = asme.getNext(i);
- if (asme0 instanceof AvatarTransition) {
- if (((AvatarTransition)asme0).hasElseGuard()) {
- nbOfElse ++;
- at = (AvatarTransition)asme0;
- }
- }
- }
-
- if ((asme.nbOfNexts() == 1) && (nbOfElse == 1)) {
- return (AvatarState)asme;
- }
-
- if (nbOfElse > 2) {
- return (AvatarState)asme;
- }
-
- if (nbOfElse == 1) {
- // Must compute the new guard
- guard = "";
- for(i=0; i<asme.nbOfNexts(); i++) {
- asme0 = asme.getNext(i);
- if ((asme0 instanceof AvatarTransition) && (asme0 != at)) {
- at0 = (AvatarTransition)asme0;
- g = at0.getGuard().toString ();
- if (g != null) {
- if (at0.hasNonDeterministicGuard()) {
- guard = "false";
- break;
- } else {
- if (guard.length() == 0) {
- guard = "not(" + at0.getGuard() + ")";
- } else {
- guard = guard + " and (not(" + at0.getGuard() + "))";
- }
- }
- }
- }
- }
- guard = Conversion.replaceAllChar(guard, '[', "(");
- guard = Conversion.replaceAllChar(guard, ']', ")");
- guard = "[" + guard + "]";
- at.setGuard(AvatarGuard.createFromString (this, guard));
- TraceManager.addDev("[ else ] replaced with :" + guard);
- }
- }
- }
- }
-
- return null;
-
- }
-
-
-
}
diff --git a/src/avatartranslator/AvatarSpecification.java b/src/avatartranslator/AvatarSpecification.java
index 631391738574be5143157a26e127ebc77e60561d..a418c3b31f24d4c67ed771f09edc25ad4a2f50de 100644
--- a/src/avatartranslator/AvatarSpecification.java
+++ b/src/avatartranslator/AvatarSpecification.java
@@ -302,17 +302,28 @@ public class AvatarSpecification extends AvatarElement {
return null;
}
- public AvatarState removeElseGuards() {
- AvatarState state;
-
- for(AvatarBlock block: blocks) {
- state = block.removeElseGuards();
- if (state != null) {
- return state;
+ public void removeElseGuards() {
+ for (AvatarBlock block: blocks) {
+ AvatarStateMachine asm = block.getStateMachine ();
+ if (asm == null)
+ continue;
+ for (AvatarStateMachineElement asme: asm.getListOfElements ()) {
+ if (! (asme instanceof AvatarState))
+ continue;
+
+ for (AvatarStateMachineElement next: asme.getNexts ()) {
+ if (! (next instanceof AvatarTransition))
+ continue;
+ AvatarTransition at = (AvatarTransition) next;
+ AvatarGuard ancientGuard = at.getGuard ();
+
+ if (ancientGuard == null)
+ continue;
+
+ at.setGuard (ancientGuard.getRealGuard (asme));
+ }
}
}
-
- return null;
}
public boolean hasLossyChannel() {
diff --git a/src/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
index 949f8b9b2302d91b6c042d860637a72c267f592f..be69b896b06682fc320de20e9b891bb76ea88393 100755
--- a/src/avatartranslator/toproverif/AVATAR2ProVerif.java
+++ b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
@@ -817,99 +817,100 @@ public class AVATAR2ProVerif implements AvatarTranslator {
TraceManager.addDev("| | Actions");
// Loop over all assigment functions
- for(AvatarActionAssignment action: _asme.getAssignments ()) {
- TraceManager.addDev("| | | assignment found: " + action);
- AvatarLeftHand leftHand = action.getLeftHand ();
-
- // Compute right part of assignment
- AvatarTerm rightHand = action.getRightHand ();
- String proVerifRightHand = null;
- if (rightHand instanceof AvatarTermFunction) {
- // If it's a function call
- String name = ((AvatarTermFunction) rightHand).getMethod ().getName ();
- LinkedList<AvatarTerm> args = ((AvatarTermFunction) rightHand).getArgs ().getComponents ();
-
- if (name.equals ("concat2") || name.equals ("concat3") || name.equals ("concat4")) {
- // If it's a concat function, just use tuples
- boolean first = true;
- proVerifRightHand = "(";
- for (AvatarTerm argTerm: args) {
- if (first)
- first = false;
- else
- proVerifRightHand += ", ";
- proVerifRightHand += AVATAR2ProVerif.translateTerm (argTerm, arg.attributeCmp);
- }
- proVerifRightHand += ")";
+ for(AvatarAction aaction: _asme.getActions ()) {
+ if (aaction instanceof AvatarActionAssignment) {
+ AvatarActionAssignment action = (AvatarActionAssignment) aaction;
+ TraceManager.addDev("| | | assignment found: " + action);
+ AvatarLeftHand leftHand = action.getLeftHand ();
+
+ // Compute right part of assignment
+ AvatarTerm rightHand = action.getRightHand ();
+ String proVerifRightHand = null;
+ if (rightHand instanceof AvatarTermFunction) {
+ // If it's a function call
+ String name = ((AvatarTermFunction) rightHand).getMethod ().getName ();
+ LinkedList<AvatarTerm> args = ((AvatarTermFunction) rightHand).getArgs ().getComponents ();
+
+ if (name.equals ("concat2") || name.equals ("concat3") || name.equals ("concat4")) {
+ // If it's a concat function, just use tuples
+ boolean first = true;
+ proVerifRightHand = "(";
+ for (AvatarTerm argTerm: args) {
+ if (first)
+ first = false;
+ else
+ proVerifRightHand += ", ";
+ proVerifRightHand += AVATAR2ProVerif.translateTerm (argTerm, arg.attributeCmp);
+ }
+ proVerifRightHand += ")";
+ } else
+ // Else use the function as is
+ proVerifRightHand = AVATAR2ProVerif.translateTerm (rightHand, arg.attributeCmp);
} else
- // Else use the function as is
+ // If it's not a function, use it as is
proVerifRightHand = AVATAR2ProVerif.translateTerm (rightHand, arg.attributeCmp);
- } else
- // If it's not a function, use it as is
- proVerifRightHand = AVATAR2ProVerif.translateTerm (rightHand, arg.attributeCmp);
-
- // Compute left hand part of the assignment
- LinkedList<ProVerifVar> proVerifLeftHand = new LinkedList<ProVerifVar> ();
- if (leftHand instanceof AvatarTuple)
- for (AvatarTerm term: ((AvatarTuple) leftHand).getComponents ()) {
- if (! (term instanceof AvatarAttribute)) {
- CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "'" + term.getName () + "' should be an attribute (ignored)");
- ce.setAvatarBlock(arg.block);
- ce.setTDiagramPanel(((AvatarDesignPanel)(this.avspec.getReferenceObject())).getAvatarSMDPanel(arg.block.getName()));
- ce.setTGComponent((TGComponent)(_asme.getReferenceObject()));
- this.warnings.add(ce);
- continue;
- }
- AvatarAttribute attr = (AvatarAttribute) term;
+ // Compute left hand part of the assignment
+ LinkedList<ProVerifVar> proVerifLeftHand = new LinkedList<ProVerifVar> ();
+ if (leftHand instanceof AvatarTuple)
+ for (AvatarTerm term: ((AvatarTuple) leftHand).getComponents ()) {
+ if (! (term instanceof AvatarAttribute)) {
+ CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "'" + term.getName () + "' should be an attribute (ignored)");
+ ce.setAvatarBlock(arg.block);
+ ce.setTDiagramPanel(((AvatarDesignPanel)(this.avspec.getReferenceObject())).getAvatarSMDPanel(arg.block.getName()));
+ ce.setTGComponent((TGComponent)(_asme.getReferenceObject()));
+ this.warnings.add(ce);
+ continue;
+ }
+
+ AvatarAttribute attr = (AvatarAttribute) term;
+ Integer c = arg.attributeCmp.get (attr) + 1;
+ arg.attributeCmp.put (attr, c);
+ proVerifLeftHand.add (new ProVerifVar (AVATAR2ProVerif.translateTerm (attr, arg.attributeCmp), "bitstring"));
+ }
+ else if (leftHand instanceof AvatarAttribute) {
+ AvatarAttribute attr = (AvatarAttribute) leftHand;
Integer c = arg.attributeCmp.get (attr) + 1;
arg.attributeCmp.put (attr, c);
proVerifLeftHand.add (new ProVerifVar (AVATAR2ProVerif.translateTerm (attr, arg.attributeCmp), "bitstring"));
}
- else if (leftHand instanceof AvatarAttribute) {
- AvatarAttribute attr = (AvatarAttribute) leftHand;
- Integer c = arg.attributeCmp.get (attr) + 1;
- arg.attributeCmp.put (attr, c);
- proVerifLeftHand.add (new ProVerifVar (AVATAR2ProVerif.translateTerm (attr, arg.attributeCmp), "bitstring"));
- }
-
- if (proVerifRightHand != null && proVerifLeftHand.size () > 0)
- _lastInstr = _lastInstr.setNextInstr (new ProVerifProcLet (proVerifLeftHand.toArray (new ProVerifVar[proVerifLeftHand.size ()]), proVerifRightHand));
- }
-
- // Loop over all function calls
- for(AvatarTermFunction action: _asme.getFunctionCalls ()) {
- String name = action.getMethod ().getName ();
- if (name.equals ("get2") || name.equals ("get3") || name.equals ("get4")) {
- // If the function called is get[234]
- LinkedList<AvatarTerm> args = action.getArgs ().getComponents ();
- int index = (int) name.charAt (3) - 48;
+ if (proVerifRightHand != null && proVerifLeftHand.size () > 0)
+ _lastInstr = _lastInstr.setNextInstr (new ProVerifProcLet (proVerifLeftHand.toArray (new ProVerifVar[proVerifLeftHand.size ()]), proVerifRightHand));
+ } else if (aaction instanceof AvatarTermFunction) {
+ AvatarTermFunction action = (AvatarTermFunction) aaction;
+ String name = action.getMethod ().getName ();
+
+ if (name.equals ("get2") || name.equals ("get3") || name.equals ("get4")) {
+ // If the function called is get[234]
+ LinkedList<AvatarTerm> args = action.getArgs ().getComponents ();
+ int index = (int) name.charAt (3) - 48;
+
+ boolean ok = true;
+ for (int i = 1; i <= index; i++)
+ if (! (args.get(i) instanceof AvatarAttribute)) {
+ CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "'" + args.get(i).getName () + "' should be an attribute (ignored)");
+ ce.setAvatarBlock(arg.block);
+ ce.setTDiagramPanel(((AvatarDesignPanel)(this.avspec.getReferenceObject())).getAvatarSMDPanel(arg.block.getName()));
+ ce.setTGComponent((TGComponent)(_asme.getReferenceObject()));
+ this.warnings.add(ce);
+ ok = false;
+ }
- boolean ok = true;
- for (int i = 1; i <= index; i++)
- if (! (args.get(i) instanceof AvatarAttribute)) {
- CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "'" + args.get(i).getName () + "' should be an attribute (ignored)");
- ce.setAvatarBlock(arg.block);
- ce.setTDiagramPanel(((AvatarDesignPanel)(this.avspec.getReferenceObject())).getAvatarSMDPanel(arg.block.getName()));
- ce.setTGComponent((TGComponent)(_asme.getReferenceObject()));
- this.warnings.add(ce);
- ok = false;
- }
+ if (ok) {
+ // Create the corresponding assignment
+ String rightHand = AVATAR2ProVerif.translateTerm (args.get (0), arg.attributeCmp);
- if (ok) {
- // Create the corresponding assignment
- String rightHand = AVATAR2ProVerif.translateTerm (args.get (0), arg.attributeCmp);
+ LinkedList<ProVerifVar> tup = new LinkedList<ProVerifVar> ();
+ for (int i = 1; i <= index; i++) {
+ AvatarAttribute attr = (AvatarAttribute) args.get (i);
+ Integer c = arg.attributeCmp.get (attr) + 1;
+ arg.attributeCmp.put (attr, c);
+ tup.add (new ProVerifVar (AVATAR2ProVerif.translateTerm (attr, arg.attributeCmp), "bitstring"));
+ }
- LinkedList<ProVerifVar> tup = new LinkedList<ProVerifVar> ();
- for (int i = 1; i <= index; i++) {
- AvatarAttribute attr = (AvatarAttribute) args.get (i);
- Integer c = arg.attributeCmp.get (attr) + 1;
- arg.attributeCmp.put (attr, c);
- tup.add (new ProVerifVar (AVATAR2ProVerif.translateTerm (attr, arg.attributeCmp), "bitstring"));
+ _lastInstr = _lastInstr.setNextInstr (new ProVerifProcLet (tup.toArray (new ProVerifVar[tup.size ()]), rightHand));
}
-
- _lastInstr = _lastInstr.setNextInstr (new ProVerifProcLet (tup.toArray (new ProVerifVar[tup.size ()]), rightHand));
}
}
}
diff --git a/src/ui/AvatarDesignPanelTranslator.java b/src/ui/AvatarDesignPanelTranslator.java
index f13100a01db375b07320387d5018c4d6bbbd16c9..9a8c2548b404af1c3bfbab3a3d254ea3380303d1 100644
--- a/src/ui/AvatarDesignPanelTranslator.java
+++ b/src/ui/AvatarDesignPanelTranslator.java
@@ -116,10 +116,9 @@ public class AvatarDesignPanelTranslator {
} */
createPragmas(as, blocks);
- // FIXME: is it ok to let else guards ?
- // TraceManager.addDev("Removing else guards");
- // as.removeElseGuards();
- // TraceManager.addDev("Removing else guards ... done");
+ TraceManager.addDev("Removing else guards");
+ as.removeElseGuards();
+ TraceManager.addDev("Removing else guards ... done");
return as;
}