From 6cce3089d8fe03a62dbd4ec901594ad804ff2b96 Mon Sep 17 00:00:00 2001
From: Letitia Li <leli@enst.fr>
Date: Tue, 8 Mar 2016 10:22:53 +0000
Subject: [PATCH] fixed TML2Avatar
---
src/avatartranslator/AvatarTransition.java | 1 -
.../toproverif/AVATAR2ProVerif.java | 13 ++--
src/proverifspec/ProVerifPitypeSyntaxer.java | 6 ++
src/tmltranslator/TMLRequest.java | 18 +++--
src/tmltranslator/toavatar/TML2Avatar.java | 65 +++++++++++--------
src/ui/GTMLModeling.java | 2 +
6 files changed, 69 insertions(+), 36 deletions(-)
diff --git a/src/avatartranslator/AvatarTransition.java b/src/avatartranslator/AvatarTransition.java
index 996152c9d4..eb2ede6d2a 100644
--- a/src/avatartranslator/AvatarTransition.java
+++ b/src/avatartranslator/AvatarTransition.java
@@ -79,7 +79,6 @@ public class AvatarTransition extends AvatarStateMachineElement {
public void addGuard(String _g) {
AvatarGuard guard = AvatarGuard.createFromString (this.block, _g);
- System.out.println("DID I ADD THE GUARD " + guard.toString());
this.guard = AvatarGuard.addGuard (this.guard, guard, "and");
}
diff --git a/src/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
index b4e132c990..ff4c426c2f 100755
--- a/src/avatartranslator/toproverif/AVATAR2ProVerif.java
+++ b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
@@ -1014,7 +1014,9 @@ public class AVATAR2ProVerif implements AvatarTranslator {
String tmp = "out (" + CH_MAINCH + ", ";
if (isPrivate)
tmp += CH_ENCRYPT + name + " (";
-
+ if (_asme.getNbOfValues()>1){
+ tmp +="(";
+ }
if (_asme.getNbOfValues() == 0)
tmp += "data__" + this.dummyDataCounter;
else {
@@ -1042,6 +1044,9 @@ public class AVATAR2ProVerif implements AvatarTranslator {
tmp += ")";
tmp += ")";
+ if (_asme.getNbOfValues()>1){
+ tmp +=")";
+ }
TraceManager.addDev("| | " + tmp);
_lastInstr = _lastInstr.setNextInstr (new ProVerifProcRaw (tmp, true));
@@ -1058,7 +1063,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
if (term == null || ! (term instanceof AvatarAttribute)) {
CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Unknown attribute '" + value + "' (ignored)");
ce.setAvatarBlock(arg.block);
- ce.setTDiagramPanel(((AvatarDesignPanel)(this.avspec.getReferenceObject())).getAvatarSMDPanel(arg.block.getName()));
+ // ce.setTDiagramPanel(((AvatarDesignPanel)(this.avspec.getReferenceObject())).getAvatarSMDPanel(arg.block.getName()));
ce.setTGComponent((TGComponent)(_asme.getReferenceObject()));
this.warnings.add(ce);
continue;
@@ -1105,7 +1110,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
TraceManager.addDev ("!!! Guard: " + _asme.getGuard() + " in block " + arg.block.getName() + " is not supported. Replacing by an empty guard");
CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Guard: " + _asme.getGuard() + " in block " + arg.block.getName() + " is not supported. Replacing by an empty guard");
ce.setAvatarBlock(arg.block);
- ce.setTDiagramPanel(((AvatarDesignPanel)(avspec.getReferenceObject())).getAvatarSMDPanel(arg.block.getName()));
+ //ce.setTDiagramPanel(((AvatarDesignPanel)(avspec.getReferenceObject())).getAvatarSMDPanel(arg.block.getName()));
ce.setTGComponent((TGComponent)(_asme.getReferenceObject()));
warnings.add(ce);
_lastInstr = _lastInstr.setNextInstr (new ProVerifProcRaw ("(* Unsupported guard:" + _asme.getGuard() + " *)"));
@@ -1196,7 +1201,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
TraceManager.addDev ("!!! Assignment: " + action.toString () + " in block " + arg.block.getName() + " is not supported. Removing it.");
CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Assignment: " + action.toString () + " in block " + arg.block.getName() + " is not supported. Removing it.");
ce.setAvatarBlock(arg.block);
- ce.setTDiagramPanel(((AvatarDesignPanel)(avspec.getReferenceObject())).getAvatarSMDPanel(arg.block.getName()));
+ //ce.setTDiagramPanel(((AvatarDesignPanel)(avspec.getReferenceObject())).getAvatarSMDPanel(arg.block.getName()));
ce.setTGComponent((TGComponent)(_asme.getReferenceObject()));
warnings.add(ce);
}
diff --git a/src/proverifspec/ProVerifPitypeSyntaxer.java b/src/proverifspec/ProVerifPitypeSyntaxer.java
index 99395ecf04..be64de5a75 100644
--- a/src/proverifspec/ProVerifPitypeSyntaxer.java
+++ b/src/proverifspec/ProVerifPitypeSyntaxer.java
@@ -217,6 +217,9 @@ public class ProVerifPitypeSyntaxer extends ProVerifSyntaxer {
protected void translateProcIn (ProVerifProcIn _node, int _alinea) {
this.fullSpec += "\n" + this.printAlinea (_alinea);
this.fullSpec += "in (" + _node.channel + ", ";
+ if (_node.vars.length>1){
+ this.fullSpec += "(";
+ }
boolean first = true;
for (ProVerifVar var: _node.vars) {
if (first)
@@ -226,6 +229,9 @@ public class ProVerifPitypeSyntaxer extends ProVerifSyntaxer {
this.fullSpec += var.name + ": " + var.type;
}
this.fullSpec += ")";
+ if (_node.vars.length>1){
+ this.fullSpec += ")";
+ }
if (_node.next != null) {
this.fullSpec += ";";
this.translate (_node.next, _alinea);
diff --git a/src/tmltranslator/TMLRequest.java b/src/tmltranslator/TMLRequest.java
index 3dc3006fe3..7484381d38 100755
--- a/src/tmltranslator/TMLRequest.java
+++ b/src/tmltranslator/TMLRequest.java
@@ -52,11 +52,12 @@ public class TMLRequest extends TMLCommunicationElement {
protected Vector params; // List of various types of parameters
protected ArrayList<TMLTask> originTasks; // list of tasks from which request starts
protected TMLTask destinationTask;
-
+ protected ArrayList<String> paramNames;
public TMLRequest(String name, Object reference) {
super(name, reference);
params = new Vector();
originTasks = new ArrayList<TMLTask>();
+ paramNames = new ArrayList<String>();
}
public int getNbOfParams() {
@@ -66,7 +67,10 @@ public class TMLRequest extends TMLCommunicationElement {
public void addParam(TMLType _type) {
params.add(_type);
}
-
+ public void addParamName(String name){
+ paramNames.add(name);
+ }
+
public TMLType getType(int i) {
if (i<getNbOfParams()) {
return (TMLType)(params.elementAt(i));
@@ -74,7 +78,13 @@ public class TMLRequest extends TMLCommunicationElement {
return null;
}
}
-
+ public String getParam(int i){
+ if (i<getNbOfParams()) {
+ return paramNames.get(i);
+ } else {
+ return null;
+ }
+ }
public void setDestinationTask(TMLTask _task) {
destinationTask = _task;
}
@@ -119,4 +129,4 @@ public class TMLRequest extends TMLCommunicationElement {
return true;
}
-}
\ No newline at end of file
+}
diff --git a/src/tmltranslator/toavatar/TML2Avatar.java b/src/tmltranslator/toavatar/TML2Avatar.java
index 917cb47fe3..ce957b220b 100644
--- a/src/tmltranslator/toavatar/TML2Avatar.java
+++ b/src/tmltranslator/toavatar/TML2Avatar.java
@@ -288,7 +288,7 @@ public class TML2Avatar {
}
else if (ae instanceof TMLStartState){
AvatarStartState ss= new AvatarStartState(ae.getName(), ae.getReferenceObject());
- tran = new AvatarTransition(block, "__after_" + ae.getName(), ss);
+ tran = new AvatarTransition(block, "__after_" + ae.getName(), ss.getReferenceObject());
ss.addNext(tran);
elementList.add(ss);
elementList.add(tran);
@@ -298,7 +298,7 @@ public class TML2Avatar {
TMLRandom tmlr = (TMLRandom) ae;
ar.setVariable(tmlr.getVariable());
ar.setValues(tmlr.getMinValue(), tmlr.getMaxValue());
- tran = new AvatarTransition(block, "__after_"+ae.getName(), ae);
+ tran = new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
ar.addNext(tran);
//Add to list
elementList.add(ar);
@@ -367,7 +367,10 @@ public class TML2Avatar {
AvatarAttribute requestData= new AvatarAttribute(req.getName()+"__reqData", AvatarType.INTEGER, block, null);
as.addValue(req.getName()+"__reqData");
block.addAttribute(requestData);
- tran= new AvatarTransition(block, "__after_"+ae.getName(), ae);
+ for (int i=0; i< req.getNbOfParams(); i++){
+ as.addValue(req.getParam(i));
+ }
+ tran= new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
elementList.add(as);
as.addNext(tran);
elementList.add(tran);
@@ -403,7 +406,7 @@ public class TML2Avatar {
//Build branch 0
- tran = new AvatarTransition(block, "__after_"+ae.getName()+"_0", ae);
+ tran = new AvatarTransition(block, "__after_"+ae.getName()+"_0", ae.getReferenceObject());
choiceState.addNext(tran);
elementList.add(tran);
tran.addNext(set0.get(0));
@@ -438,7 +441,7 @@ public class TML2Avatar {
elementList.add(e);
}
}
- tran = new AvatarTransition(block, "__after_"+ae.getName()+"_1", ae);
+ tran = new AvatarTransition(block, "__after_"+ae.getName()+"_1", ae.getReferenceObject());
elementList.add(tran);
choiceState.addNext(tran);
tran.addNext(set1_1.get(0));
@@ -456,7 +459,7 @@ public class TML2Avatar {
//This gets really complicated in ProVerif
for (int i=0; i< ae.getNbNext(); i++){
//For each of the possible state blocks, translate 1 and recurse on the remaining random sequence
- tran = new AvatarTransition(block, "__after_"+ae.getName()+"_"+i, ae);
+ tran = new AvatarTransition(block, "__after_"+ae.getName()+"_"+i, ae.getReferenceObject());
choiceState.addNext(tran);
List<AvatarStateMachineElement> tmp = translateState(ae.getNextElement(i), block);
tran.addNext(tmp.get(0));
@@ -466,7 +469,7 @@ public class TML2Avatar {
newSeq.addNext(ae.getNextElement(j));
}
}
- tran = new AvatarTransition(block, "__after_"+ae.getNextElement(i).getName(), ae);
+ tran = new AvatarTransition(block, "__after_"+ae.getNextElement(i).getName(), ae.getReferenceObject());
tmp.get(tmp.size()-1).addNext(tran);
elementList.addAll(tmp);
elementList.add(tran);
@@ -495,7 +498,7 @@ public class TML2Avatar {
AvatarAttribute eventData= new AvatarAttribute(ch.getName()+"__eventData", AvatarType.INTEGER, block, null);
as.addValue(ch.getName()+"__eventData");
block.addAttribute(eventData);
- tran= new AvatarTransition(block, "__after_"+ae.getName(), ae);
+ tran= new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
elementList.add(as);
as.addNext(tran);
elementList.add(tran);
@@ -515,7 +518,7 @@ public class TML2Avatar {
AvatarAttribute eventData= new AvatarAttribute(ch.getName()+"__eventData", AvatarType.INTEGER, block, null);
as.addValue(ch.getName()+"__eventData");
block.addAttribute(eventData);
- tran= new AvatarTransition(block, "__after_"+ae.getName(), ae);
+ tran= new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
elementList.add(as);
as.addNext(tran);
elementList.add(tran);
@@ -523,7 +526,7 @@ public class TML2Avatar {
else {
//Notify Event, I don't know how to translate this
AvatarRandom as = new AvatarRandom(ae.getName(), ae.getReferenceObject());
- tran = new AvatarTransition(block, "__after_"+ae.getName(), ae);
+ tran = new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
as.setVariable(aee.getVariable());
as.setValues("0", "1");
as.addNext(tran);
@@ -534,7 +537,7 @@ public class TML2Avatar {
}
else if (ae instanceof TMLActivityElementWithAction){
AvatarState as = new AvatarState(ae.getName(), ae.getReferenceObject());
- tran = new AvatarTransition(block, "__after_"+ae.getName(), ae);
+ tran = new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
tran.addAction(((TMLActivityElementWithAction) ae).getAction());
as.addNext(tran);
elementList.add(as);
@@ -542,7 +545,7 @@ public class TML2Avatar {
}
else if (ae instanceof TMLActivityElementWithIntervalAction){
AvatarState as = new AvatarState(ae.getName(), ae.getReferenceObject());
- tran = new AvatarTransition(block, "__after_"+ae.getName(), ae);
+ tran = new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
as.addNext(tran);
elementList.add(as);
elementList.add(tran);
@@ -579,7 +582,7 @@ public class TML2Avatar {
}
AvatarActionOnSignal as = new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
as.addValue(ch.getName()+"__chData");
- tran= new AvatarTransition(block, "__after_"+ae.getName(), ae);
+ tran= new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
as.addNext(tran);
elementList.add(as);
elementList.add(tran);
@@ -618,7 +621,7 @@ public class TML2Avatar {
AvatarState initState = new AvatarState(ae.getName()+"__init", ae.getReferenceObject(), true);
elementList.add(initState);
//Build transition to choice
- tran = new AvatarTransition(block, "loop_init__"+ae.getName(), ae);
+ tran = new AvatarTransition(block, "loop_init__"+ae.getName(), ae.getReferenceObject());
tran.addAction(AvatarTerm.createActionFromString(block, loop.getInit()));
elementList.add(tran);
initState.addNext(tran);
@@ -627,7 +630,7 @@ public class TML2Avatar {
elementList.add(as);
tran.addNext(as);
//transition to first element of loop
- tran = new AvatarTransition(block, "loop_increment__"+ae.getName(), ae);
+ tran = new AvatarTransition(block, "loop_increment__"+ae.getName(), ae.getReferenceObject());
tran.setGuard(loop.getCondition().replaceAll("<", "!="));
tran.addAction(AvatarTerm.createActionFromString(block, loop.getIncrement()));
tran.addNext(elements.get(0));
@@ -653,7 +656,7 @@ public class TML2Avatar {
}
//Transition if exiting loop
- tran=new AvatarTransition(block, "end_loop__"+ae.getName(), ae);
+ tran=new AvatarTransition(block, "end_loop__"+ae.getName(), ae.getReferenceObject());
tran.setGuard("else");
as.addNext(tran);
if (afterloop.size()==0){
@@ -671,8 +674,8 @@ public class TML2Avatar {
elementList.add(as);
TMLChoice c = (TMLChoice) ae;
for (int i=0; i<c.getNbGuard(); i++){
- tran = new AvatarTransition(block, "__after_"+ae.getName()+"_"+i, ae);
- tran.addGuard(c.getGuard(i));
+ tran = new AvatarTransition(block, "__after_"+ae.getName()+"_"+i, ae.getReferenceObject());
+ tran.setGuard(c.getGuard(i));
as.addNext(tran);
List<AvatarStateMachineElement> nexts = translateState(ae.getNextElement(i), block);
tran.addNext(nexts.get(0));
@@ -688,7 +691,7 @@ public class TML2Avatar {
//Make many choices
TMLSelectEvt c = (TMLSelectEvt) ae;
for (int i=0; i < ae.getNbNext(); i++){
- tran = new AvatarTransition(block, "__after_"+ae.getName()+"_"+i, ae);
+ tran = new AvatarTransition(block, "__after_"+ae.getName()+"_"+i, ae.getReferenceObject());
as.addNext(tran);
List<AvatarStateMachineElement> nexts = translateState(ae.getNextElement(i), block);
tran.addNext(nexts.get(0));
@@ -749,7 +752,7 @@ public class TML2Avatar {
AvatarTransition last;
AvatarStateMachine asm = block.getStateMachine();
- //Create a fork with many requests. This looks terrible
+ //TODO: Create a fork with many requests. This looks terrible
if (tmlmodel.getRequestToMe(task)!=null){
TMLRequest request= tmlmodel.getRequestToMe(task);
//Oh this is fun...let's restructure the state machine
@@ -757,7 +760,7 @@ public class TML2Avatar {
List<AvatarStateMachineElement> elementList= translateState(task.getActivityDiagram().get(0), block);
AvatarStartState ss = new AvatarStartState("start", task.getActivityDiagram().get(0).getReferenceObject());
asm.addElement(ss);
- AvatarTransition at= new AvatarTransition(block, "__after_start", task.getActivityDiagram().get(0));
+ AvatarTransition at= new AvatarTransition(block, "__after_start", task.getActivityDiagram().get(0).getReferenceObject());
ss.addNext(at);
asm.addElement(at);
AvatarSignal sig = new AvatarSignal(block.getName()+"__"+request.getName(), AvatarSignal.IN, request.getReferenceObject());
@@ -766,7 +769,10 @@ public class TML2Avatar {
AvatarActionOnSignal as= new AvatarActionOnSignal("getRequest__"+request.getName(), sig, request.getReferenceObject());
at.addNext(as);
asm.addElement(as);
- AvatarTransition tran = new AvatarTransition(block, "__after_" + request.getName(), task.getActivityDiagram().get(0));
+ for (int i=0; i< request.getNbOfParams(); i++){
+ as.addValue(request.getParam(i)+"__reqData");
+ }
+ AvatarTransition tran = new AvatarTransition(block, "__after_" + request.getName(), task.getActivityDiagram().get(0).getReferenceObject());
as.addNext(tran);
asm.addElement(tran);
@@ -777,10 +783,14 @@ public class TML2Avatar {
tran.addNext(newStart);
elementList.remove(start);
elementList.remove(startTran);
- //Find every stop state, remove them, reroute transitions to them
+ //Find every stop state, remove them, reroute transitions to them
+ //For now, route every transition to stop state to remove the loop on requests
+
for (AvatarStateMachineElement e: elementList){
e.setName(processName(e.getName(), e.getID()));
- if (e instanceof AvatarStopState){
+ asm.addElement(e);
+ }
+ /* if (e instanceof AvatarStopState){
//ignore it
}
else {
@@ -793,7 +803,7 @@ public class TML2Avatar {
}
asm.addElement(e);
}
- }
+ }*/
asm.setStartState((AvatarStartState) ss);
}
else {
@@ -855,6 +865,7 @@ public class TML2Avatar {
System.out.println("Complex channel ");
for (TMLTask t1: channel.getOriginTasks()){
for (TMLTask t2: channel.getDestinationTasks()){
+
AvatarRelation ar= new AvatarRelation(channel.getName(), taskBlockMap.get(t1), taskBlockMap.get(t2), channel.getReferenceObject());
ar.setPrivate(channelMap.get(channel)==1);
//Find in signal
@@ -863,7 +874,7 @@ public class TML2Avatar {
for (AvatarSignal sig: signals){
if (sig.getInOut()==AvatarSignal.IN){
String name = sig.getName();
- if (name.equals(channel.getDestinationTask().getName()+"__"+channel.getName())){
+ if (name.equals(t2.getName()+"__"+channel.getName())){
sig1.add(sig);
}
}
@@ -872,7 +883,7 @@ public class TML2Avatar {
for (AvatarSignal sig: signals){
if (sig.getInOut()==AvatarSignal.OUT){
String name = sig.getName();
- if (name.equals(channel.getOriginTask().getName()+"__"+channel.getName())){
+ if (name.equals(t1.getName()+"__"+channel.getName())){
sig2.add(sig);
}
}
diff --git a/src/ui/GTMLModeling.java b/src/ui/GTMLModeling.java
index d01a0ed64b..0355b20ace 100755
--- a/src/ui/GTMLModeling.java
+++ b/src/ui/GTMLModeling.java
@@ -1661,10 +1661,12 @@ public class GTMLModeling {
for(int k=0; k<allVariables.size(); k++) {
//TraceManager.addDev("Adding record: " + allVariables.get(k));
tmlsendrequest.addParam(allVariables.get(k));
+ request.addParamName(allVariables.get(k));
}
} else {
//TraceManager.addDev("Adding param: " + tmp);
tmlsendrequest.addParam(tmp);
+ request.addParamName(tmp);
}
}
if (request.getNbOfParams() != tmlsendrequest.getNbOfParams()) {
--
GitLab