From 23131d44788a9111dc9623e6524e8d197899b93a Mon Sep 17 00:00:00 2001
From: Letitia Li <leli@enst.fr>
Date: Thu, 19 May 2016 12:26:21 +0000
Subject: [PATCH] To AvatarDP translation
---
src/tmltranslator/TMLActivityElement.java | 8 +++++++-
src/tmltranslator/toavatar/TML2Avatar.java | 7 +++----
src/ui/GTMLModeling.java | 4 ++++
src/ui/GTURTLEModeling.java | 3 +++
src/ui/avatarbd/AvatarBDBlock.java | 2 +-
src/ui/avatarbd/AvatarBDPragma.java | 4 ++++
6 files changed, 22 insertions(+), 6 deletions(-)
diff --git a/src/tmltranslator/TMLActivityElement.java b/src/tmltranslator/TMLActivityElement.java
index ff9af0a8d8..8ae3fbdd6d 100755
--- a/src/tmltranslator/TMLActivityElement.java
+++ b/src/tmltranslator/TMLActivityElement.java
@@ -51,6 +51,7 @@ import java.util.*;
public class TMLActivityElement extends TMLElement{
protected Vector<TMLActivityElement> nexts;
public SecurityPattern securityPattern;
+ private String value="";
public TMLActivityElement(String _name, Object _referenceObject) {
super(_name, _referenceObject);
nexts = new Vector();
@@ -60,7 +61,12 @@ public class TMLActivityElement extends TMLElement{
public int getNbNext() {
return nexts.size();
}
-
+ public void setValue(String val){
+ value=val;
+ }
+ public String getValue(){
+ return value;
+ }
public TMLActivityElement getNextElement(int _i) {
if (_i < getNbNext() ) {
return (TMLActivityElement)(nexts.elementAt(_i));
diff --git a/src/tmltranslator/toavatar/TML2Avatar.java b/src/tmltranslator/toavatar/TML2Avatar.java
index 4357c797eb..25be499f94 100644
--- a/src/tmltranslator/toavatar/TML2Avatar.java
+++ b/src/tmltranslator/toavatar/TML2Avatar.java
@@ -647,7 +647,7 @@ public class TML2Avatar {
}
else if (ae instanceof TMLActivityElementWithAction){
//Might be encrypt or decrypt
- AvatarState as = new AvatarState(ae.getName(), ae.getReferenceObject());
+ AvatarState as = new AvatarState(ae.getValue(), ae.getReferenceObject());
tran = new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
//For now, get rid of the action. It won't translate anyway
//tran.addAction(((TMLActivityElementWithAction) ae).getAction());
@@ -1194,14 +1194,13 @@ public class TML2Avatar {
asm.setStartState((AvatarStartState) elementList.get(0));
}
for (SecurityPattern secPattern: secPatterns){
- System.out.println("secpattern "+ secPattern.name);
AvatarAttribute sec = new AvatarAttribute(secPattern.name, AvatarType.INTEGER, block, null);
AvatarAttribute enc = new AvatarAttribute(secPattern.name+"_encrypted", AvatarType.INTEGER, block, null);
LinkedList<AvatarAttribute> attrs = new LinkedList<AvatarAttribute>();
block.addAttribute(sec);
block.addAttribute(enc);
attrs.add(sec);
- avspec.addPragma(new AvatarPragmaSecret("#Confidentiality "+block.getName() + "."+ "securitypattern", null, attrs));
+ avspec.addPragma(new AvatarPragmaSecret("#Confidentiality "+block.getName() + "."+ secPattern.name, null, attrs));
}
avspec.addBlock(block);
}
@@ -1212,7 +1211,7 @@ public class TML2Avatar {
//Add authenticity pragmas
for (String s: signalAuthOriginMap.keySet()){
if (signalAuthDestMap.containsKey(s)){
- AvatarPragmaAuthenticity pragma = new AvatarPragmaAuthenticity(s, signalAuthOriginMap.get(s).getReferenceObject(), signalAuthOriginMap.get(s), signalAuthDestMap.get(s));
+ AvatarPragmaAuthenticity pragma = new AvatarPragmaAuthenticity("#Authenticity ", signalAuthOriginMap.get(s).getReferenceObject(), signalAuthOriginMap.get(s), signalAuthDestMap.get(s));
avspec.addPragma(pragma);
}
}
diff --git a/src/ui/GTMLModeling.java b/src/ui/GTMLModeling.java
index 41d3742abb..b01ffd77b4 100755
--- a/src/ui/GTMLModeling.java
+++ b/src/ui/GTMLModeling.java
@@ -1483,12 +1483,14 @@ public class GTMLModeling {
} else if (tgc instanceof TMLADExecI) {
tmlexeci = new TMLExecI("execi", tgc);
tmlexeci.setAction(modifyString(((TMLADExecI)tgc).getDelayValue()));
+ tmlexeci.setValue(((TMLADExecC)tgc).getDelayValue());
activity.addElement(tmlexeci);
((BasicErrorHighlight)tgc).setStateAction(ErrorHighlight.OK);
listE.addCor(tmlexeci, tgc);
} else if (tgc instanceof TMLADExecIInterval) {
tmlexecii = new TMLExecIInterval("execi", tgc);
+ tmlexecii.setValue(tgc.getValue());
tmlexecii.setMinDelay(modifyString(((TMLADExecIInterval)tgc).getMinDelayValue()));
tmlexecii.setMaxDelay(modifyString(((TMLADExecIInterval)tgc).getMaxDelayValue()));
activity.addElement(tmlexecii);
@@ -1516,6 +1518,8 @@ public class GTMLModeling {
} else if (tgc instanceof TMLADExecC) {
tmlexecc = new TMLExecC("execc", tgc);
+ tmlexecc.setValue(((TMLADExecC)tgc).getDelayValue());
+ System.out.println("val " + tgc.getValue());
tmlexecc.setAction(modifyString(((TMLADExecC)tgc).getDelayValue()));
activity.addElement(tmlexecc);
((BasicErrorHighlight)tgc).setStateAction(ErrorHighlight.OK);
diff --git a/src/ui/GTURTLEModeling.java b/src/ui/GTURTLEModeling.java
index 3459b80094..f963bef878 100755
--- a/src/ui/GTURTLEModeling.java
+++ b/src/ui/GTURTLEModeling.java
@@ -639,6 +639,9 @@ public class GTURTLEModeling {
public boolean generateProVerifFromAVATAR(String _path, int _stateReachability, boolean _typed, String loopLimit) {
if (tmap!=null){
t2a = new TML2Avatar(tmap);
+ TML2AvatarDP tml2avatardp = new TML2AvatarDP(tmap);
+ tml2avatardp.adp = mgui.getFirstAvatarDesignPanelFound();
+ tml2avatardp.translate();
avatarspec = t2a.generateAvatarSpec(loopLimit);
}
else if (tmlm!=null){
diff --git a/src/ui/avatarbd/AvatarBDBlock.java b/src/ui/avatarbd/AvatarBDBlock.java
index 6f677c64a6..0beba05139 100644
--- a/src/ui/avatarbd/AvatarBDBlock.java
+++ b/src/ui/avatarbd/AvatarBDBlock.java
@@ -519,7 +519,7 @@ public class AvatarBDBlock extends TGCScalableWithInternalComponent implements S
return true;
} else {
JOptionPane.showMessageDialog(frame,
- "Could not change the name of the Block: this name is already in use",
+ "Could not change the name of the Block: frame error",
"Error",
JOptionPane.INFORMATION_MESSAGE);
setValue(oldValue);
diff --git a/src/ui/avatarbd/AvatarBDPragma.java b/src/ui/avatarbd/AvatarBDPragma.java
index 6404f815ea..6ec8090bc1 100755
--- a/src/ui/avatarbd/AvatarBDPragma.java
+++ b/src/ui/avatarbd/AvatarBDPragma.java
@@ -130,6 +130,10 @@ public class AvatarBDPragma extends TGCScalableWithoutInternalComponent {
public String[] getValues() {
return values;
}
+ public void setValues(String[] v){
+ values=v;
+ makeValue();
+ }
public LinkedList<String> getProperties() {
return properties;
}
--
GitLab