diff --git a/src/avatartranslator/AvatarAttribute.java b/src/avatartranslator/AvatarAttribute.java
index f1bf8ba92d40cc02caf41e00b0ce01bd67f00f95..e3648c00d6632c29a4a4f65e98bbb9e4731462be 100644
--- a/src/avatartranslator/AvatarAttribute.java
+++ b/src/avatartranslator/AvatarAttribute.java
@@ -192,6 +192,7 @@ public class AvatarAttribute extends AvatarLeftHand {
@Override
public void replaceAttributes (HashMap<AvatarAttribute, AvatarAttribute> attributesMapping) {
+ TraceManager.addDev("!!! ERROR !!! (replaceAttributes in AvatarAttribute)");
/* !!! We should never arrive here !!! */
}
diff --git a/src/avatartranslator/AvatarLibraryFunction.java b/src/avatartranslator/AvatarLibraryFunction.java
index f6ee0d2ac0c409a708290a82f76393af88317a01..8b5c8e72a18c98492d86b656b6aef88f2802e06c 100644
--- a/src/avatartranslator/AvatarLibraryFunction.java
+++ b/src/avatartranslator/AvatarLibraryFunction.java
@@ -107,6 +107,11 @@ public class AvatarLibraryFunction extends AvatarElement implements AvatarTransl
*/
private AvatarSpecification avspec;
+ /**
+ * Counter of invocations of this library function.
+ */
+ private int counter;
+
/**
* Basic constructor of the function function.
@@ -130,6 +135,23 @@ public class AvatarLibraryFunction extends AvatarElement implements AvatarTransl
this.methods = new LinkedList<AvatarMethod> ();
this.asm = new AvatarStateMachine (this, "statemachineoffunction__" + name, referenceObject);
+ this.counter = 0;
+ }
+
+ /**
+ * Return a unique counter for library function call.
+ */
+ public int getCounter()
+ {
+ return this.counter++;
+ }
+
+ /**
+ * Set counter for this library function.
+ */
+ public void setCounter(int counter)
+ {
+ this.counter = counter;
}
@Override
@@ -288,6 +310,7 @@ public class AvatarLibraryFunction extends AvatarElement implements AvatarTransl
*/
public void addAttributesToBlock (AvatarBlock block, HashMap<AvatarAttribute, AvatarAttribute> mapping) {
for (AvatarAttribute attribute: this.attributes) {
+ // TODO: We should use different attributes for different library function call
String name = this.name + "__" + attribute.getName ();
AvatarAttribute attr = block.getAvatarAttributeWithName (name);
if (attr == null) {
@@ -373,6 +396,11 @@ public class AvatarLibraryFunction extends AvatarElement implements AvatarTransl
*/
public Object referenceObject;
+ /**
+ * The counter for the library function call.
+ */
+ public int counter;
+
/**
* Basic constructor.
*
@@ -390,8 +418,10 @@ public class AvatarLibraryFunction extends AvatarElement implements AvatarTransl
* The block the function call belongs to.
* @param referenceObject
* The reference object associated to the function call being translated.
+ * @param counter
+ * The counter for the library function call.
*/
- public TranslatorArgument (HashMap<AvatarAttribute, AvatarAttribute> placeholdersMapping, HashMap<AvatarSignal, AvatarSignal> signalsMapping, AvatarStateMachineElement previousElement, AvatarStateMachineElement lastElement, HashMap<AvatarStateMachineElement, AvatarStateMachineElement> elementsMapping, AvatarBlock block, Object referenceObject) {
+ public TranslatorArgument (HashMap<AvatarAttribute, AvatarAttribute> placeholdersMapping, HashMap<AvatarSignal, AvatarSignal> signalsMapping, AvatarStateMachineElement previousElement, AvatarStateMachineElement lastElement, HashMap<AvatarStateMachineElement, AvatarStateMachineElement> elementsMapping, AvatarBlock block, Object referenceObject, int counter) {
this.placeholdersMapping = placeholdersMapping;
this.signalsMapping = signalsMapping;
this.previousElement = previousElement;
@@ -399,6 +429,7 @@ public class AvatarLibraryFunction extends AvatarElement implements AvatarTransl
this.elementsMapping = elementsMapping;
this.block = block;
this.referenceObject = referenceObject;
+ this.counter = counter;
}
}
@@ -418,9 +449,9 @@ public class AvatarLibraryFunction extends AvatarElement implements AvatarTransl
*
* @return The last element of the state machine created.
*/
- public AvatarState translateASMWithMapping (HashMap<AvatarAttribute, AvatarAttribute> placeholdersMapping, HashMap<AvatarSignal, AvatarSignal> signalsMapping, AvatarStateMachineElement firstElement, AvatarBlock block, Object referenceObject) {
+ public AvatarState translateASMWithMapping (HashMap<AvatarAttribute, AvatarAttribute> placeholdersMapping, HashMap<AvatarSignal, AvatarSignal> signalsMapping, AvatarStateMachineElement firstElement, AvatarBlock block, Object referenceObject, int counter) {
/* Create the last state */
- AvatarState lastState = new AvatarState ("exit_" + this.name, referenceObject);
+ AvatarState lastState = new AvatarState ("exit_" + this.name + "_" + counter, referenceObject);
/* Create the argument object that will be passed to translation functions */
Object arg = new TranslatorArgument (
@@ -430,7 +461,8 @@ public class AvatarLibraryFunction extends AvatarElement implements AvatarTransl
lastState,
new HashMap<AvatarStateMachineElement, AvatarStateMachineElement> (),
block,
- referenceObject);
+ referenceObject,
+ counter);
/* Translate the state machine, starting from the first state */
this.asm.getStartState ().translate (this, arg);
@@ -479,14 +511,14 @@ public class AvatarLibraryFunction extends AvatarElement implements AvatarTransl
if (_asme instanceof AvatarSetTimer) {
// TODO: isn't the name used for the timer ?
- asme = new AvatarSetTimer (this.name + "__" + _asme.getName (), arg.referenceObject);
+ asme = new AvatarSetTimer (this.name + "_" + arg.counter + "__" + _asme.getName (), arg.referenceObject);
// TODO: should probably replace attributes too, right ?
((AvatarSetTimer) asme).setTimerValue (((AvatarSetTimer) _asme).getTimerValue ());
} else if (_asme instanceof AvatarResetTimer)
- asme = new AvatarResetTimer (this.name + "__" + _asme.getName (), arg.referenceObject);
+ asme = new AvatarResetTimer (this.name + "_" + arg.counter + "__" + _asme.getName (), arg.referenceObject);
else if (_asme instanceof AvatarExpireTimer)
- asme = new AvatarExpireTimer (this.name + "__" + _asme.getName (), arg.referenceObject);
+ asme = new AvatarExpireTimer (this.name + "_" + arg.counter + "__" + _asme.getName (), arg.referenceObject);
else
/* !!! should not happen */
return;
@@ -500,7 +532,7 @@ public class AvatarLibraryFunction extends AvatarElement implements AvatarTransl
public void translateActionOnSignal (AvatarActionOnSignal _asme, Object _arg) {
TranslatorArgument arg = (TranslatorArgument) _arg;
- AvatarActionOnSignal asme = new AvatarActionOnSignal (this.name + "__" + _asme.getName (), arg.signalsMapping.get (_asme.getSignal ()), arg.referenceObject);
+ AvatarActionOnSignal asme = new AvatarActionOnSignal (this.name + "_" + arg.counter + "__" + _asme.getName (), arg.signalsMapping.get (_asme.getSignal ()), arg.referenceObject);
for (String s: _asme.getValues ()) {
AvatarAttribute attr = this.getAvatarAttributeWithName (s);
if (attr == null)
@@ -516,7 +548,7 @@ public class AvatarLibraryFunction extends AvatarElement implements AvatarTransl
public void translateTransition (AvatarTransition _asme, Object _arg) {
TranslatorArgument arg = (TranslatorArgument) _arg;
- AvatarTransition asme = new AvatarTransition (arg.block, this.name + "__" + _asme.getName (), arg.referenceObject);
+ AvatarTransition asme = new AvatarTransition (arg.block, this.name + "_" + arg.counter + "__" + _asme.getName (), arg.referenceObject);
AvatarGuard guard = _asme.getGuard ().clone ();
guard.replaceAttributes (arg.placeholdersMapping);
@@ -549,7 +581,7 @@ public class AvatarLibraryFunction extends AvatarElement implements AvatarTransl
* reachability of state in a function for a particular invocation of this
* function.
*/
- AvatarState asme = new AvatarState (this.name + "__" + _asme.getName (), arg.referenceObject, false);
+ AvatarState asme = new AvatarState (this.name + "_" + arg.counter + "__" + _asme.getName (), arg.referenceObject, false);
asme.setHidden (true);
asme.addEntryCode (_asme.getEntryCode ());
@@ -560,7 +592,7 @@ public class AvatarLibraryFunction extends AvatarElement implements AvatarTransl
public void translateRandom (AvatarRandom _asme, Object _arg) {
TranslatorArgument arg = (TranslatorArgument) _arg;
- AvatarRandom asme = new AvatarRandom (this.name + "__" + _asme.getName (), arg.referenceObject);
+ AvatarRandom asme = new AvatarRandom (this.name + "_" + arg.counter + "__" + _asme.getName (), arg.referenceObject);
asme.setValues (_asme.getMinValue (), _asme.getMaxValue ());
asme.setFunctionId (_asme.getFunctionId ());
asme.setVariable (arg.placeholdersMapping.get (this.getAvatarAttributeWithName (_asme.getVariable ())).getName ());
@@ -579,7 +611,7 @@ public class AvatarLibraryFunction extends AvatarElement implements AvatarTransl
public void translateLibraryFunctionCall (AvatarLibraryFunctionCall _asme, Object _arg) {
TranslatorArgument arg = (TranslatorArgument) _arg;
- AvatarLibraryFunctionCall asme = new AvatarLibraryFunctionCall (this.name + "__" + _asme.getName (), _asme.getLibraryFunction (), arg.referenceObject);
+ AvatarLibraryFunctionCall asme = new AvatarLibraryFunctionCall (this.name + "_" + arg.counter + "__" + _asme.getName (), _asme.getLibraryFunction (), arg.referenceObject);
for (AvatarAttribute attr: _asme.getParameters ())
asme.addParameter (arg.placeholdersMapping.get (attr));
for (AvatarSignal signal: _asme.getSignals ())
@@ -595,6 +627,7 @@ public class AvatarLibraryFunction extends AvatarElement implements AvatarTransl
AvatarLibraryFunction result = new AvatarLibraryFunction(this.name, avspec, this.referenceObject);
this.cloneLinkToReferenceObjects (result);
+ result.setCounter(this.counter);
for (AvatarAttribute aa: this.parameters)
result.addParameter(aa.advancedClone(result));
for (AvatarSignal sig: this.signals)
diff --git a/src/avatartranslator/AvatarLibraryFunctionCall.java b/src/avatartranslator/AvatarLibraryFunctionCall.java
index 785001f7f42bfd7fbef95abe176b935426aa4da5..e6299dad822b1cb6ab5707edc778e7b887e915a5 100644
--- a/src/avatartranslator/AvatarLibraryFunctionCall.java
+++ b/src/avatartranslator/AvatarLibraryFunctionCall.java
@@ -73,6 +73,11 @@ public class AvatarLibraryFunctionCall extends AvatarStateMachineElement {
*/
private AvatarLibraryFunction libraryFunction;
+ /**
+ * Counter for library function call.
+ */
+ private int counter;
+
/**
* Basic constructor of the function function.
*
@@ -85,11 +90,20 @@ public class AvatarLibraryFunctionCall extends AvatarStateMachineElement {
super(_name, _referenceObject);
this.libraryFunction = libraryFunction;
+ this.counter = this.libraryFunction.getCounter();
this.parameters = new LinkedList<AvatarAttribute> ();
this.signals = new LinkedList<AvatarSignal> ();
this.returnAttributes = new LinkedList <AvatarAttribute> ();
}
+ /**
+ * @return The counter for this library function call
+ */
+ public int getCounter()
+ {
+ return this.counter;
+ }
+
/**
* Get the list of parameters passed to the function.
*
@@ -196,7 +210,7 @@ public class AvatarLibraryFunctionCall extends AvatarStateMachineElement {
this.libraryFunction.addSignalsToMapping (signalsMapping, this.signals);
/* Translate the state machine */
- return this.libraryFunction.translateASMWithMapping (placeholdersMapping, signalsMapping, firstElement, block, this.referenceObject);
+ return this.libraryFunction.translateASMWithMapping (placeholdersMapping, signalsMapping, firstElement, block, this.referenceObject, this.counter);
}
@Override
diff --git a/src/avatartranslator/AvatarSimpleGuardDuo.java b/src/avatartranslator/AvatarSimpleGuardDuo.java
index 4a90f05719513afb2473097cc05d08a64ef91508..3b855b6f14ef0832d9832b8270f445e38a2aa5d5 100644
--- a/src/avatartranslator/AvatarSimpleGuardDuo.java
+++ b/src/avatartranslator/AvatarSimpleGuardDuo.java
@@ -88,7 +88,21 @@ public class AvatarSimpleGuardDuo extends AvatarSimpleGuard {
@Override
public void replaceAttributes (HashMap<AvatarAttribute, AvatarAttribute> attributesMapping) {
- this.termA.replaceAttributes (attributesMapping);
- this.termB.replaceAttributes (attributesMapping);
+ if (this.termA instanceof AvatarAttribute)
+ {
+ this.termA = attributesMapping.get((AvatarAttribute) this.termA);
+ }
+ else
+ {
+ this.termA.replaceAttributes (attributesMapping);
+ }
+ if (this.termB instanceof AvatarAttribute)
+ {
+ this.termB = attributesMapping.get((AvatarAttribute) this.termB);
+ }
+ else
+ {
+ this.termB.replaceAttributes (attributesMapping);
+ }
}
}
diff --git a/src/avatartranslator/AvatarSimpleGuardMono.java b/src/avatartranslator/AvatarSimpleGuardMono.java
index 3761e9309650eebec53aab194c0815573306df8c..dc9afdb9bb33f6c16e71864e0464f4e948ce1d4d 100644
--- a/src/avatartranslator/AvatarSimpleGuardMono.java
+++ b/src/avatartranslator/AvatarSimpleGuardMono.java
@@ -47,6 +47,7 @@
package avatartranslator;
import java.util.HashMap;
+import myutil.TraceManager;
import myutil.Conversion;
@@ -76,6 +77,16 @@ public class AvatarSimpleGuardMono extends AvatarSimpleGuard {
@Override
public void replaceAttributes (HashMap<AvatarAttribute, AvatarAttribute> attributesMapping) {
- this.term.replaceAttributes (attributesMapping);
+ for (AvatarAttribute attr: attributesMapping.keySet())
+ {
+ }
+ if (this.term instanceof AvatarAttribute)
+ {
+ this.term = attributesMapping.get(((AvatarAttribute) this.term));
+ }
+ else
+ {
+ this.term.replaceAttributes (attributesMapping);
+ }
}
}
diff --git a/src/avatartranslator/AvatarStateMachine.java b/src/avatartranslator/AvatarStateMachine.java
index fdff5e572e924d5204de93963049960c41f88035..a959845bad6b2f90cc765d1fb79c9951ec742f1a 100644
--- a/src/avatartranslator/AvatarStateMachine.java
+++ b/src/avatartranslator/AvatarStateMachine.java
@@ -1535,14 +1535,15 @@ public class AvatarStateMachine extends AvatarElement {
continue;
if (curAsme instanceof AvatarLibraryFunctionCall) {
+ AvatarLibraryFunctionCall alfc = (AvatarLibraryFunctionCall) curAsme;
/* Create a state that will be used as an entry point for the sub-state machine */
- AvatarState firstState = new AvatarState ("entry_" + curAsme.getName (), curAsme.getReferenceObject ());
+ AvatarState firstState = new AvatarState ("entry_" + alfc.getLibraryFunction().getName () + "_" + alfc.getCounter(), curAsme.getReferenceObject ());
/* Add this state to the mapping so that future state can use it to replace their next element */
- callsTranslated.put ((AvatarLibraryFunctionCall) curAsme, firstState);
+ callsTranslated.put (alfc, firstState);
/* inline the function call */
- AvatarStateMachineElement lastState = ((AvatarLibraryFunctionCall) curAsme).inlineFunctionCall (block, firstState);
+ AvatarStateMachineElement lastState = alfc.inlineFunctionCall (block, firstState);
/* Add the next elements to the newly created last state */
for (AvatarStateMachineElement asme: curAsme.getNexts ())
diff --git a/src/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
index 66b6e24713c2876a2017e2e8dca901432d0affa4..ed4cb9ff0b1a833f366673d07bf3a761e90d9e0e 100755
--- a/src/avatartranslator/toproverif/AVATAR2ProVerif.java
+++ b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
@@ -222,9 +222,9 @@ public class AVATAR2ProVerif implements AvatarTranslator {
protected static String translateTerm (AvatarTerm term, HashMap<AvatarAttribute, Integer> attributeCmp) {
if (term instanceof AvatarAttribute) {
AvatarAttribute attr = (AvatarAttribute) term;
- if (attributeCmp != null)
+ if (attributeCmp != null) {
return AVATAR2ProVerif.makeAttrName (attr.getBlock ().getName (), attr.getName (), attributeCmp.get (attr).toString ());
- else
+ } else
return AVATAR2ProVerif.makeAttrName (attr.getBlock ().getName (), attr.getName ());
}
@@ -939,7 +939,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
if (asme != null) {
HashMap<AvatarAttribute, Integer> attributeCmp = new HashMap<AvatarAttribute, Integer> ();
for (AvatarAttribute attr: ab.getAttributes ()) {
- TraceManager.addDev ("=== " + attr);
+ TraceManager.addDev ("=== " + attr.getName());
attributeCmp.put (attr, 0);
}