diff --git a/src/main/java/avatartranslator/AvatarPragmaLatency.java b/src/main/java/avatartranslator/AvatarPragmaLatency.java
index 6a23fca0a06af607acb39da8feaf2e4775c83067..19db85bb5ea2a131b2ca659ff004619c837775df 100644
--- a/src/main/java/avatartranslator/AvatarPragmaLatency.java
+++ b/src/main/java/avatartranslator/AvatarPragmaLatency.java
@@ -57,6 +57,7 @@ public class AvatarPragmaLatency extends AvatarPragma {
private int symbolType;
public static final int lessThan =1;
public static final int greaterThan=2;
+ public static final int query=3;
private int time;
private List<String> id1;
private List<String> id2;
diff --git a/src/main/java/avatartranslator/AvatarSpecification.java b/src/main/java/avatartranslator/AvatarSpecification.java
index 0c792f13fe732be166909be5c7d5fe652c982b05..0da19ddeffee3c42a2461c51220262709b84eaa6 100644
--- a/src/main/java/avatartranslator/AvatarSpecification.java
+++ b/src/main/java/avatartranslator/AvatarSpecification.java
@@ -222,7 +222,6 @@ public class AvatarSpecification extends AvatarElement {
}
public void addLatencyPragma(AvatarPragmaLatency _pragma) {
- System.out.println(_pragma);
latency_pragmas.add(_pragma);
}
diff --git a/src/main/java/avatartranslator/AvatarStateMachine.java b/src/main/java/avatartranslator/AvatarStateMachine.java
index ece3482dea29c7f19114bd3b0974a401f211c373..0665d8478ddddafdfc1561fc87305afad1b4045b 100644
--- a/src/main/java/avatartranslator/AvatarStateMachine.java
+++ b/src/main/java/avatartranslator/AvatarStateMachine.java
@@ -1080,17 +1080,17 @@ public class AvatarStateMachine extends AvatarElement {
}
- public AvatarActionOnSignal getAOSWithName(String _name){
+ public List<AvatarActionOnSignal> getAllAOSWithName(String _name){
+ List<AvatarActionOnSignal> list = new ArrayList<AvatarActionOnSignal>();
for(AvatarStateMachineElement element: elements) {
if (element instanceof AvatarActionOnSignal) {
AvatarActionOnSignal aaos = (AvatarActionOnSignal) element;
- System.out.println("element " + aaos.getSignal().getName());
if (aaos.getSignal().getName().compareTo(_name) == 0) {
- return aaos;
+ list.add(aaos);
}
}
}
- return null;
+ return list;
}
// All transitions reaching a state that has an internal start state
diff --git a/src/main/java/tmltranslator/TMLModeling.java b/src/main/java/tmltranslator/TMLModeling.java
index 26fb4ed6695db61e5a773452e6225998acd7ba26..94915b9061828ec0231a9d2812f1d5253482f52b 100755
--- a/src/main/java/tmltranslator/TMLModeling.java
+++ b/src/main/java/tmltranslator/TMLModeling.java
@@ -99,7 +99,7 @@ public class TMLModeling<E> {
}
}
- public void addSec(SecurityPattern sp){
+ public void addSecurityPattern(SecurityPattern sp){
if (!secPatterns.contains(sp)){
secPatterns.add(sp);
}
diff --git a/src/main/java/tmltranslator/toavatar/TML2Avatar.java b/src/main/java/tmltranslator/toavatar/TML2Avatar.java
index 18fcac7d0d54856f2c85bba59785bee97d6b4df7..6485bfd7205f8aba47a15d79be2c8f711b16794c 100644
--- a/src/main/java/tmltranslator/toavatar/TML2Avatar.java
+++ b/src/main/java/tmltranslator/toavatar/TML2Avatar.java
@@ -655,18 +655,18 @@ public class TML2Avatar {
as.addNext(tran);
elementList.add(as);
elementList.add(tran);
- if (security || ae.securityPattern==null){
+ if (security && ae.securityPattern!=null){
if (ae.securityPattern!=null && ae.getName().contains("encrypt")){
secPatterns.add(ae.securityPattern);
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name+"_encrypted", AvatarType.INTEGER, block, null));
if (ae.securityPattern.type.equals("Advanced")){
tran.addAction(ae.securityPattern.formula);
}
else if (ae.securityPattern.type.equals("Symmetric Encryption")){
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block,null));
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name+"_encrypted", AvatarType.INTEGER, block,null));
+ block.addAttribute(new AvatarAttribute("key_"+ae.securityPattern.name, AvatarType.INTEGER, block,null));
if (!ae.securityPattern.nonce.isEmpty()){
block.addAttribute(new AvatarAttribute(ae.securityPattern.nonce, AvatarType.INTEGER, block, null));
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block,null));
AvatarMethod concat2 = new AvatarMethod("concat2",ae);
concat2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
concat2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.nonce));
@@ -694,7 +694,9 @@ public class TML2Avatar {
AvatarMethod sencrypt = new AvatarMethod("sencrypt", ae);
sencrypt.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
sencrypt.addParameter(block.getAvatarAttributeWithName("key_"+ae.securityPattern.name));
+ sencrypt.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name+"_encrypted"));
if (block.getAvatarAttributeWithName(ae.securityPattern.name)!=null && block.getAvatarAttributeWithName("key_"+ae.securityPattern.name)!=null){
+ System.out.println("adding method sencrypt");
block.addMethod(sencrypt);
}
tran.addAction(ae.securityPattern.name+"_encrypted = sencrypt("+ae.securityPattern.name+", key_"+ae.securityPattern.name+")");
@@ -719,6 +721,7 @@ public class TML2Avatar {
block.addAttribute(new AvatarAttribute("encryptedKey_"+ae.securityPattern.key, AvatarType.INTEGER, block,null));
aencrypt.addParameter(block.getAvatarAttributeWithName("key_"+ae.securityPattern.key));
aencrypt.addParameter(block.getAvatarAttributeWithName("pubKey_"+ae.securityPattern.name));
+ aencrypt.addReturnParameter(block.getAvatarAttributeWithName("encryptedKey_"+ae.securityPattern.key));
if (block.getAvatarAttributeWithName("key_"+ae.securityPattern.key)!=null && block.getAvatarAttributeWithName("pubKey_"+ae.securityPattern.name)!=null){
block.addMethod(aencrypt);
}
@@ -726,8 +729,12 @@ public class TML2Avatar {
}
else {
AvatarMethod aencrypt = new AvatarMethod("aencrypt", ae);
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute("pubKey_"+ae.securityPattern.name, AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name+"_encrypted", AvatarType.INTEGER, block, null));
aencrypt.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
aencrypt.addParameter(block.getAvatarAttributeWithName("pubKey_"+ae.securityPattern.name));
+ aencrypt.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name+"_encrypted"));
if (block.getAvatarAttributeWithName("pubKey_"+ae.securityPattern.name)!=null && block.getAvatarAttributeWithName(ae.securityPattern.name)!=null){
block.addMethod(aencrypt);
}
@@ -756,31 +763,40 @@ public class TML2Avatar {
tran.addAction(ae.securityPattern.name+"_encrypted = hash("+ae.securityPattern.name+")");
}
else if (ae.securityPattern.type.equals("MAC")){
+
+ if (!ae.securityPattern.nonce.isEmpty()){
+ AvatarMethod concat = new AvatarMethod("concat2", ae);
+ concat.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ concat.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.nonce));
+ concat.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ block.addMethod(concat);
+ tran.addAction(ae.securityPattern.name+"=concat2("+ae.securityPattern.name+","+ae.securityPattern.nonce+")");
+ }
+
AvatarMethod mac = new AvatarMethod("MAC", ae);
AvatarAttribute macattr = new AvatarAttribute(ae.securityPattern.name +"_mac", AvatarType.INTEGER, block, null);
block.addAttribute(macattr);
+
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute("key_"+ae.securityPattern.name, AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name+"_encrypted", AvatarType.INTEGER, block, null));
+
mac.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
mac.addParameter(block.getAvatarAttributeWithName("key_"+ae.securityPattern.name));
mac.addReturnParameter(macattr);
+
if (block.getAvatarAttributeWithName(ae.securityPattern.name)!=null && block.getAvatarAttributeWithName("key_"+ae.securityPattern.name)!=null){
block.addMethod(mac);
}
- if (!ae.securityPattern.nonce.isEmpty()){
- AvatarMethod concat = new AvatarMethod("concat2", ae);
- concat.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- concat.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.nonce));
- concat.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- block.addMethod(concat);
- tran.addAction(ae.securityPattern.name+"=concat2("+ae.securityPattern.name+","+ae.securityPattern.nonce+")");
- }
+
tran.addAction(ae.securityPattern.name+"_mac = MAC("+ae.securityPattern.name+",key_"+ae.securityPattern.name+")");
AvatarMethod concat = new AvatarMethod("concat2", ae);
concat.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- concat.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ concat.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name+"_mac"));
concat.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name+"_encrypted"));
//concat.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.));
- if (block.getAvatarAttributeWithName(ae.securityPattern.name)!=null){
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name)!=null && block.getAvatarAttributeWithName(ae.securityPattern.name+"_encrypted")!=null){
block.addMethod(concat);
}
tran.addAction(ae.securityPattern.name+"_encrypted = concat2("+ae.securityPattern.name +","+ae.securityPattern.name+"_mac)");
@@ -983,7 +999,7 @@ public class TML2Avatar {
}
}
else {
- //
+ //Translate state without security
}
}
else if (ae instanceof TMLActivityElementWithIntervalAction){
@@ -1363,8 +1379,12 @@ public class TML2Avatar {
//TODO: Make state names readable
//TODO: Put back numeric guards
//TODO: Calcuate for temp variable
- this.avspec = new AvatarSpecification("spec", tmlmap.getTMLModeling().getTGComponent().getTDiagramPanel().tp);
-
+ if (tmlmap.getTMLModeling().getTGComponent()!=null){
+ this.avspec = new AvatarSpecification("spec", tmlmap.getTMLModeling().getTGComponent().getTDiagramPanel().tp);
+ }
+ else {
+ this.avspec = new AvatarSpecification("spec", null);
+ }
attrsToCheck.clear();
//tmlmodel.removeForksAndJoins();
//Only set the loop limit if it's a number
diff --git a/src/main/java/ui/AvatarDesignPanel.java b/src/main/java/ui/AvatarDesignPanel.java
index db4ac08e11083f980d893f530a75269e30931baf..f27b44af6261637c06c8f26caf31251f56186fc9 100644
--- a/src/main/java/ui/AvatarDesignPanel.java
+++ b/src/main/java/ui/AvatarDesignPanel.java
@@ -408,21 +408,25 @@ public class AvatarDesignPanel extends TURTLEPanel {
}
if (pragma.getSymbolType() == AvatarPragmaLatency.lessThan){
if (time<refTime){
- bdpragma.verifMap.put(s, AvatarBDSafetyPragma.PROVED_TRUE);
+ bdpragma.verifMap.put(s, "PROVED_TRUE");
//mark as true
}
else {
- bdpragma.verifMap.put(s, AvatarBDSafetyPragma.PROVED_FALSE);
+ bdpragma.verifMap.put(s, "PROVED_FALSE");
}
}
- else {
+ else if (pragma.getSymbolType() == AvatarPragmaLatency.greaterThan) {
if (time>refTime){
- bdpragma.verifMap.put(s, AvatarBDSafetyPragma.PROVED_TRUE);
+ bdpragma.verifMap.put(s, "PROVED_TRUE");
//mark as true
}
else {
- bdpragma.verifMap.put(s, AvatarBDSafetyPragma.PROVED_FALSE);
+ bdpragma.verifMap.put(s, "PROVED_FALSE");
}
+ }
+ else if (pragma.getSymbolType() == AvatarPragmaLatency.query) {
+ //Draw average time on verif map
+ bdpragma.verifMap.put(s,Float.toString(time));
}
}
}
diff --git a/src/main/java/ui/AvatarDesignPanelTranslator.java b/src/main/java/ui/AvatarDesignPanelTranslator.java
index 43ce5a755a83667967714a178bceb269d4f7c3a6..9429b4f29e4989870b1888407d48ef9193c89ae0 100644
--- a/src/main/java/ui/AvatarDesignPanelTranslator.java
+++ b/src/main/java/ui/AvatarDesignPanelTranslator.java
@@ -220,7 +220,7 @@ public class AvatarDesignPanelTranslator {
tgpp = (AvatarBDPerformancePragma)tgc;
values = tgpp.getValues();
for (String s: values){
- AvatarPragmaLatency pragma = checkLatencyPragma(s, _blocks, _as, tgc);
+ AvatarPragmaLatency pragma = checkPerformancePragma(s, _blocks, _as, tgc);
if (pragma!=null){
_as.addLatencyPragma(pragma);
}
@@ -229,8 +229,8 @@ public class AvatarDesignPanelTranslator {
}
}
- public AvatarPragmaLatency checkLatencyPragma(String _pragma, List<AvatarBDBlock> _blocks, AvatarSpecification as, TGComponent tgc){
- if (_pragma.contains("=") || (!_pragma.contains(">") && !_pragma.contains("<")) || !_pragma.contains("Latency")){
+ public AvatarPragmaLatency checkPerformancePragma(String _pragma, List<AvatarBDBlock> _blocks, AvatarSpecification as, TGComponent tgc){
+ if (_pragma.contains("=") || (!_pragma.contains(">") && !_pragma.contains("<") && !_pragma.contains("?")) || !_pragma.contains("Latency")){
TraceManager.addDev("No latency expression found");
return null;
}
@@ -251,7 +251,7 @@ public class AvatarDesignPanelTranslator {
String block1 = p1.split("\\.")[0];
String state1 = p1.split("\\.")[1];
AvatarBlock bl1;
- AvatarActionOnSignal st1;
+ AvatarActionOnSignal st1=null;
List<String> id1= new ArrayList<String>();
bl1 = as.getBlockWithName(block1);
if (bl1==null){
@@ -259,16 +259,17 @@ public class AvatarDesignPanelTranslator {
return null;
}
AvatarStateMachine asm = bl1.getStateMachine();
- st1 = asm.getAOSWithName(state1);
- if (bl1 ==null || st1 ==null){
- TraceManager.addDev("State " + block1+ "." + state1 + " in pragma does not exist");
- return null;
+ for (AvatarActionOnSignal aaos: asm.getAllAOSWithName(state1)){
+ if (aaos.getCheckLatency()){
+ id1.add((aaos.getSignal().isIn() ? "Receive signal" : "Send signal") +"-"+ aaos.getSignal().getName()+":"+aaos.getID());
+ st1= aaos;
+ }
}
- if (!st1.getCheckLatency()){
- TraceManager.addDev("State " + block1+ "." + state1 + " is not checkable");
+ if (id1.size()==0){
+ TraceManager.addDev("Cannot find checkable state " + block1+ "." + state1 + " in pragma");
return null;
}
- id1.add((st1.getSignal().isIn() ? "Receive signal" : "Send signal") +"-"+ st1.getSignal().getName()+":"+st1.getID());
+
@@ -289,7 +290,7 @@ public class AvatarDesignPanelTranslator {
AvatarBlock bl2;
- AvatarActionOnSignal st2;
+ AvatarActionOnSignal st2=null;
bl2 = as.getBlockWithName(block2);
if (bl2==null){
@@ -297,19 +298,24 @@ public class AvatarDesignPanelTranslator {
return null;
}
asm = bl2.getStateMachine();
- st2 = asm.getAOSWithName(state2);
+
List<String> id2= new ArrayList<String>();
- if (bl2 ==null || st2 ==null){
- TraceManager.addDev("State " + block2+ "." + state2 + " in pragma does not exist");
- return null;
+ for (AvatarActionOnSignal aaos: asm.getAllAOSWithName(state2)){
+
+ if (aaos.getCheckLatency()){
+ id2.add((aaos.getSignal().isIn() ? "Receive signal" : "Send signal")+"-"+ aaos.getSignal().getName()+":"+aaos.getID());
+ st2=aaos;
+ }
}
- if (!st2.getCheckLatency()){
- TraceManager.addDev("State " + block2+ "." + state2 + " is not checkable");
+
+ if (id2.size()==0){
+ TraceManager.addDev("Cannot find checkable state " + block2+ "." + state2 + " in pragma");
return null;
}
+
+
+
- id2.add((st2.getSignal().isIn() ? "Receive signal" : "Send signal")+"-"+ st2.getSignal().getName()+":"+st2.getID());
-
String equation = pragma.split("\\)")[1];
equation = equation.replaceAll(" ","");
@@ -335,6 +341,9 @@ public class AvatarDesignPanelTranslator {
return null;
}
}
+ else if (equation.substring(0,1).equals("?")){
+ symbolType=AvatarPragmaLatency.query;
+ }
else {
TraceManager.addDev("No latency expression found");
diff --git a/src/main/java/ui/GTMLModeling.java b/src/main/java/ui/GTMLModeling.java
index 6ff86a083c4da06b8d59b702c2fce2d2b99d092b..496165968e1c725c81229696bade2750823cfc73 100755
--- a/src/main/java/ui/GTMLModeling.java
+++ b/src/main/java/ui/GTMLModeling.java
@@ -1598,7 +1598,7 @@ public class GTMLModeling {
if (!((TMLADEncrypt)tgc).securityContext.isEmpty()){
SecurityPattern securityPattern = new SecurityPattern(((TMLADEncrypt)tgc).securityContext, ((TMLADEncrypt)tgc).type, ((TMLADEncrypt)tgc).message_overhead, ((TMLADEncrypt)tgc).size, ((TMLADEncrypt)tgc).encTime, ((TMLADEncrypt)tgc).decTime, ((TMLADEncrypt)tgc).nonce, ((TMLADEncrypt)tgc).formula, ((TMLADEncrypt)tgc).key);
securityPatterns.put(securityPattern.name, securityPattern);
- tmlm.addSec(securityPattern);
+ tmlm.addSecurityPattern(securityPattern);
ArrayList<TMLTask> l = new ArrayList<TMLTask>();
tmlm.securityTaskMap.put(securityPattern, l);
TraceManager.addDev("Adding Security Pattern " + securityPattern.name);
diff --git a/src/main/java/ui/MainGUI.java b/src/main/java/ui/MainGUI.java
index d5d6218b602f1cbc20b0f2fb97db5eb67c9fbe1d..def6a1c7e7a76a0b5488444331f1defb23c57bcc 100644
--- a/src/main/java/ui/MainGUI.java
+++ b/src/main/java/ui/MainGUI.java
@@ -519,7 +519,7 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Pe
}
- private void initActions() {
+ public void initActions() {
actions = new TGUIAction[TGUIAction.NB_ACTION];
for(int i=0; i<TGUIAction.NB_ACTION; i++) {
actions[i] = new TGUIAction(i);
@@ -6832,6 +6832,9 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Pe
public void setPanelMode() {
int index;
TURTLEPanel tp = getCurrentTURTLEPanel();
+ if (tp==null){
+ return;
+ }
index = tp.tabbedPane.getSelectedIndex();
if (index < tp.panels.size() -1) {
diff --git a/src/main/java/ui/avatarbd/AvatarBDPerformancePragma.java b/src/main/java/ui/avatarbd/AvatarBDPerformancePragma.java
index c72fefa4265945307b741c06ee2113ef6dd6030f..09a95a53bef5975c3ac694cb930bb76595cf8e9b 100644
--- a/src/main/java/ui/avatarbd/AvatarBDPerformancePragma.java
+++ b/src/main/java/ui/avatarbd/AvatarBDPerformancePragma.java
@@ -68,7 +68,7 @@ public class AvatarBDPerformancePragma extends TGCScalableWithoutInternalCompone
protected String[] values;
protected LinkedList<String> properties;
- protected int textX = 25;
+ protected int textX = 40;
protected int textY = 5;
protected int marginY = 20;
protected int marginX = 20;
@@ -82,12 +82,9 @@ public class AvatarBDPerformancePragma extends TGCScalableWithoutInternalCompone
private Font myFont;//, myFontB;
// private int maxFontSize = 30;
// private int minFontSize = 4;
- public final static int PROVED_TRUE = 1;
- public final static int PROVED_FALSE = 0;
- public final static int PROVED_ERROR=2;
private int currentFontSize = -1;
private final String[] pPragma = {"A[]", "A<>", "E[]", "E<>"};
- public Map<String, Integer> verifMap = new HashMap<String, Integer>();
+ public Map<String, String> verifMap = new HashMap<String, String>();
protected Graphics graphics;
public AvatarBDPerformancePragma(int _x, int _y, int _minX, int _maxX, int _minY, int _maxY, boolean _pos, TGComponent _father, TDiagramPanel _tdp) {
@@ -223,7 +220,7 @@ public class AvatarBDPerformancePragma extends TGCScalableWithoutInternalCompone
if (s.isEmpty() || !s.contains("Latency") ){
//Ignore
}
- else if (s.contains("Latency") && (s.contains("<") || s.contains(">")) ) {
+ else if (s.contains("Latency") && (s.contains("<") || s.contains(">") || s.contains("?")) ) {
properties.add(s);
}
else {
@@ -310,36 +307,41 @@ public class AvatarBDPerformancePragma extends TGCScalableWithoutInternalCompone
private void drawVerification(String s, Graphics g, int _x, int _y){
Color c = g.getColor();
// Color c1;
- int status;
- if (verifMap.containsKey(s)){
- status = verifMap.get(s);
- if (status== PROVED_TRUE){
- g.setColor(Color.green);
- int[] xp1 = new int[]{_x-20, _x-18, _x-12, _x-14};
- int[] yp1 = new int[]{_y-3, _y-5, _y-1, _y+1};
- int[] xp2 = new int[]{_x-14, _x-12, _x-3, _x-5};
- int[] yp2 = new int[]{_y-1, _y+1, _y-8, _y-10};
- g.fillPolygon(xp1, yp1, 4);
- g.fillPolygon(xp2, yp2, 4);
- }
-
- else if (status==PROVED_ERROR){
- Font f= g.getFont();
- g.setFont(new Font("TimesRoman", Font.BOLD, 14));
- g.drawString("?",_x-15,_y);
- g.setFont(f);
+ String status;
+ if (verifMap.containsKey(s)){
+ status = verifMap.get(s);
+ if (status.equals("PROVED_TRUE")){
+ g.setColor(Color.green);
+ int[] xp1 = new int[]{_x-35, _x-33, _x-27, _x-29};
+ int[] yp1 = new int[]{_y-3, _y-5, _y-1, _y+1};
+ int[] xp2 = new int[]{_x-29, _x-27, _x-18, _x-20};
+ int[] yp2 = new int[]{_y-1, _y+1, _y-8, _y-10};
+ g.fillPolygon(xp1, yp1, 4);
+ g.fillPolygon(xp2, yp2, 4);
+ }
+ else if (status.equals("PROVED_ERROR")){
+ Font f= g.getFont();
+ g.setFont(new Font("TimesRoman", Font.BOLD, 14));
+ g.drawString("?",_x-30,_y);
+ g.setFont(f);
+ }
+ else if (status.equals("PROVED_FALSE")){
+ g.setColor(Color.red);
+ int[] xp1 = new int[]{_x-32, _x-30, _x-21, _x-23};
+ int[] yp1 = new int[]{_y-12, _y-10, _y-2, _y};
+ int[] xp2 = new int[]{_x-30, _x-32, _x-23, _x-21};
+ int[] yp2 = new int[]{_y, _y-2, _y-12, _y-10};
+ g.fillPolygon(xp1, yp1, 4);
+ g.fillPolygon(xp2, yp2, 4);
+ }
+ else {
+ Font f= g.getFont();
+ g.setFont(new Font("TimesRoman", Font.BOLD, 10));
+ g.drawString(status,_x-35,_y);
+ g.setFont(f);
+ }
}
- else {
- g.setColor(Color.red);
- int[] xp1 = new int[]{_x-17, _x-15, _x-6, _x-8};
- int[] yp1 = new int[]{_y-12, _y-10, _y-2, _y};
- int[] xp2 = new int[]{_x-15, _x-17, _x-8, _x-6};
- int[] yp2 = new int[]{_y, _y-2, _y-12, _y-10};
- g.fillPolygon(xp1, yp1, 4);
- g.fillPolygon(xp2, yp2, 4);
- }
- }
- g.setColor(c);
+ g.setColor(c);
}
@Override
diff --git a/src/main/java/ui/avatarinteractivesimulation/JFrameAvatarInteractiveSimulation.java b/src/main/java/ui/avatarinteractivesimulation/JFrameAvatarInteractiveSimulation.java
index d3e30c9f3a21e94c6d33355a6aab4978e3f57947..0a7b75d49f1a0917ad807de570576ae703d88635 100755
--- a/src/main/java/ui/avatarinteractivesimulation/JFrameAvatarInteractiveSimulation.java
+++ b/src/main/java/ui/avatarinteractivesimulation/JFrameAvatarInteractiveSimulation.java
@@ -267,18 +267,22 @@ public class JFrameAvatarInteractiveSimulation extends JFrame implements Avatar
transTimes.put(id, new ArrayList<String>());
}
for (AvatarPragmaLatency latencyPragma: _avspec.getLatencyPragmas()){
- if (!nameLatencyMap.containsKey(latencyPragma.getId1().get(0) + "--"+latencyPragma.getId2().get(0))){
- SimulationLatency sl = new SimulationLatency();
- sl.setTransaction1(latencyPragma.getId1().get(0));
- sl.setTransaction2(latencyPragma.getId2().get(0));
- sl.addPragma(latencyPragma);
- nameLatencyMap.put(latencyPragma.getId1().get(0) + "--"+latencyPragma.getId2().get(0), sl);
- latencies.add(sl);
- //toCheck.add(latencyPragma.getId1().get(0) + "--"+latencyPragma.getId2().get(0));
- updateTransactionsTable();
- }
- else {
- nameLatencyMap.get(latencyPragma.getId1().get(0) + "--"+latencyPragma.getId2().get(0)).addPragma(latencyPragma);
+ for (String id1: latencyPragma.getId1()){
+ for (String id2: latencyPragma.getId2()){
+ if (!nameLatencyMap.containsKey(id1 + "--"+id2)){
+ SimulationLatency sl = new SimulationLatency();
+ sl.setTransaction1(id1);
+ sl.setTransaction2(id2);
+ sl.addPragma(latencyPragma);
+ nameLatencyMap.put(id1 + "--"+id2, sl);
+ latencies.add(sl);
+ //toCheck.add(latencyPragma.getId1().get(0) + "--"+latencyPragma.getId2().get(0));
+ updateTransactionsTable();
+ }
+ else {
+ nameLatencyMap.get(id1 + "--"+id2).addPragma(latencyPragma);
+ }
+ }
}
}
makeComponents();
diff --git a/src/main/java/ui/tmldd/TMLArchiArtifact.java b/src/main/java/ui/tmldd/TMLArchiArtifact.java
index cf78c0574d2b76547fa89cc18077a2c721885ece..510f153f27360a9df43c71ef069cb0a4a7ebfff4 100755
--- a/src/main/java/ui/tmldd/TMLArchiArtifact.java
+++ b/src/main/java/ui/tmldd/TMLArchiArtifact.java
@@ -130,7 +130,6 @@ public class TMLArchiArtifact extends TGCWithoutInternalComponent implements Swa
if (oldValue.compareTo(value) != 0) {
setValue(value, g);
}
- g.drawString(value, x + textX , y + textY);
g.drawRect(x, y, width, height);
Color c = g.getColor();
diff --git a/src/main/java/ui/window/JDialogPerformancePragma.java b/src/main/java/ui/window/JDialogPerformancePragma.java
index 214e81780c166f6cb27043d8edb59d920e71c13f..fa053e982d46a1b76b1122c32a8e4d55bc642a30 100644
--- a/src/main/java/ui/window/JDialogPerformancePragma.java
+++ b/src/main/java/ui/window/JDialogPerformancePragma.java
@@ -80,9 +80,8 @@ public class JDialogPerformancePragma extends JDialogBase implements ActionListe
//Suggestion Panel code from: http://stackoverflow.com/questions/10873748/how-to-show-autocomplete-as-i-type-in-jtextarea
public class SuggestionPanel {
- private final String[] pragma = {"A[]", "E<>", "A<>", "E[]", "min(", "max("};
//Form list of all blocks
- //For each block, create a list of all attribute strings and states
+ //For each block, create a list of all states and signals
private JList list;
private JPopupMenu popupMenu;
@@ -113,15 +112,11 @@ public class JDialogPerformancePragma extends JDialogBase implements ActionListe
private JList createSuggestionList(int linePosition, final int position, final String subWord) {
ArrayList<String> matches = new ArrayList<String>();
- if (linePosition<3){
- for (String p: pragma) {
- if (p.startsWith(subWord)){
- matches.add(p);
- }
- }
+ if (linePosition<6){
+ matches.add("Latency(");
}
- if (!subWord.contains(".")){
+ else if (!subWord.contains(".")){
for (String block: blockAttributeMap.keySet()){
if (block.startsWith(subWord)){
matches.add(block);
@@ -220,7 +215,7 @@ public class JDialogPerformancePragma extends JDialogBase implements ActionListe
String text = textarea.getText();
int start = Math.max(0, position - 1);
while (start > 0) {
- if (!Character.isWhitespace(text.charAt(start)) && !text.substring(start,start+1).equals("(") && !text.substring(start,start+1).equals(")") && !text.substring(start,start+1).equals(",") ) {
+ if (!text.substring(start,start+1).equals("(") && !text.substring(start,start+1).equals(")") && !text.substring(start,start+1).equals(",") ) {
start--;
} else {
start++;
diff --git a/ttool/src/test/java/avatartranslator/AvatarSafetyTests.java b/ttool/src/test/java/avatartranslator/AvatarSafetyTests.java
index 8e0c0d695c0ec627f99d2a50759ee2b0758851d5..5d674a8d6149fc27dd44414905f4ce2416964902 100644
--- a/ttool/src/test/java/avatartranslator/AvatarSafetyTests.java
+++ b/ttool/src/test/java/avatartranslator/AvatarSafetyTests.java
@@ -68,6 +68,10 @@ public class AvatarSafetyTests {
AvatarDesignPanelTranslator adpt;
AvatarPragmaLatency pragma;
+ avatartranslator.AvatarSignal sig2;
+ avatartranslator.AvatarSignal sig;
+
+
public AvatarSafetyTests () {
// super ("AvatarSafety", true);
}
@@ -79,7 +83,8 @@ public class AvatarSafetyTests {
blocks = new ArrayList<AvatarBDBlock>();
as = new AvatarSpecification("avspec",null);
AvatarBlock A = new AvatarBlock("A", null, null);
- avatartranslator.AvatarSignal sig = new avatartranslator.AvatarSignal("sig", 0, null);
+
+ sig = new avatartranslator.AvatarSignal("sig", 0, null);
A.addSignal(sig);
AvatarStateMachine Aasm = A.getStateMachine();
AvatarActionOnSignal aaos = new AvatarActionOnSignal("action_on_signal", sig, null);
@@ -92,7 +97,7 @@ public class AvatarSafetyTests {
AvatarBlock B = new AvatarBlock("B", null, null);
AvatarStateMachine Basm = B.getStateMachine();
- avatartranslator.AvatarSignal sig2 = new avatartranslator.AvatarSignal("sig2", 0, null);
+ sig2 = new avatartranslator.AvatarSignal("sig2", 0, null);
AvatarActionOnSignal aaos2= new AvatarActionOnSignal("action_on_signal", sig2, null);
aaos2.setCheckLatency(true);
Basm.addElement(aaos2);
@@ -117,24 +122,24 @@ public class AvatarSafetyTests {
@Test
public void testFailIfLatencyPragmaEmpty(){
- pragma = adpt.checkLatencyPragma("", blocks, as, null);
+ pragma = adpt.checkPerformancePragma("", blocks, as, null);
assertNull(pragma);
}
@Test
public void testFailIfBadFormat(){
//Fail if does not contain 'Latency()'
- pragma = adpt.checkLatencyPragma("Lat(b,s)<1", blocks, as, null);
+ pragma = adpt.checkPerformancePragma("Lat(b,s)<1", blocks, as, null);
assertNull(pragma);
//Fail if unmatched ')'
- pragma = adpt.checkLatencyPragma("Latency(b,s<1", blocks, as, null);
+ pragma = adpt.checkPerformancePragma("Latency(b,s<1", blocks, as, null);
assertNull(pragma);
}
@Test
public void testFormLessThanPragma(){
//Test : Form pragma with less than expression
- pragma = adpt.checkLatencyPragma("Latency(A.sig,B.sig2)<1", blocks, as, null);
+ pragma = adpt.checkPerformancePragma("Latency(A.sig,B.sig2)<1", blocks, as, null);
assertTrue(pragma !=null);
//Check Block names
assertEquals(pragma.getBlock1().getName(),"A");
@@ -155,7 +160,7 @@ public class AvatarSafetyTests {
@Test
public void testFormGreaterThanPragma(){
//Test : Form pragma with greater than expression
- pragma = adpt.checkLatencyPragma("Latency(B.sig2,A.sig)>231", blocks, as, null);
+ pragma = adpt.checkPerformancePragma("Latency(B.sig2,A.sig)>231", blocks, as, null);
assertTrue(pragma !=null);
//Check symbol
assertEquals(pragma.getSymbolType(),AvatarPragmaLatency.greaterThan);
@@ -165,28 +170,49 @@ public class AvatarSafetyTests {
@Test
public void testFailWrongNumberFormat(){
- pragma = adpt.checkLatencyPragma("Latency(B.sig2,A.sig)>a231", blocks, as, null);
+ pragma = adpt.checkPerformancePragma("Latency(B.sig2,A.sig)>a231", blocks, as, null);
assertNull(pragma);
}
@Test
public void testFailMissingBlock(){
- pragma = adpt.checkLatencyPragma("Latency(Bob.sig2,A.sig)>231", blocks, as, null);
+ pragma = adpt.checkPerformancePragma("Latency(Bob.sig2,A.sig)>231", blocks, as, null);
assertNull(pragma);
- pragma = adpt.checkLatencyPragma("Latency(B.sig2,Alice.sig)>231", blocks, as, null);
+ pragma = adpt.checkPerformancePragma("Latency(B.sig2,Alice.sig)>231", blocks, as, null);
assertNull(pragma);
}
@Test
public void testFailMissingState(){
- pragma = adpt.checkLatencyPragma("Latency(B.state,A.sig)>231", blocks, as, null);
+ pragma = adpt.checkPerformancePragma("Latency(B.state,A.sig)>231", blocks, as, null);
assertNull(pragma);
- pragma = adpt.checkLatencyPragma("Latency(B.sig2,A.sig2)>231", blocks, as, null);
+ pragma = adpt.checkPerformancePragma("Latency(B.sig2,A.sig2)>231", blocks, as, null);
assertNull(pragma);
}
+ @Test
+ public void testFormQueryPragma(){
+ pragma = adpt.checkPerformancePragma("Latency(B.sig2,A.sig)?", blocks, as, null);
+ assertTrue(pragma!=null);
+ }
+ @Test
+ public void testMultipleIdsPerSignal(){
+ AvatarBlock A = as.getBlockWithName("A");
+ AvatarStateMachine Aasm = A.getStateMachine();
+ AvatarActionOnSignal aaos = new AvatarActionOnSignal("action_on_signal", sig, null);
+ aaos.setCheckLatency(true);
+ Aasm.addElement(aaos);
+ Aasm.getListOfElements().get(0).addNext(aaos);
+
+ //Form pragma
+ pragma = adpt.checkPerformancePragma("Latency(B.sig2,A.sig)>231", blocks, as, null);
+
+ assertEquals(pragma.getId1().size(),1);
+ assertEquals(pragma.getId2().size(),2);
+
+ }
public static void main(String[] args){
AvatarSafetyTests ast = new AvatarSafetyTests ();
diff --git a/ttool/src/test/java/avatartranslator/AvatarSecurityTranslationTests.java b/ttool/src/test/java/avatartranslator/AvatarSecurityTranslationTests.java
new file mode 100644
index 0000000000000000000000000000000000000000..473f9f163e0e45b87b42c2a524ab82ef8689b3a7
--- /dev/null
+++ b/ttool/src/test/java/avatartranslator/AvatarSecurityTranslationTests.java
@@ -0,0 +1,243 @@
+/**Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
+ *
+ * ludovic.apvrille AT enst.fr
+ *
+ * This software is a computer program whose purpose is to allow the
+ * edition of TURTLE analysis, design and deployment diagrams, to
+ * allow the generation of RT-LOTOS or Java code from this diagram,
+ * and at last to allow the analysis of formal validation traces
+ * obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
+ * from INRIA Rhone-Alpes.
+ *
+ * This software is governed by the CeCILL license under French law and
+ * abiding by the rules of distribution of free software. You can use,
+ * modify and/ or redistribute the software under the terms of the CeCILL
+ * license as circulated by CEA, CNRS and INRIA at the following URL
+ * "http://www.cecill.info".
+ *
+ * As a counterpart to the access to the source code and rights to copy,
+ * modify and redistribute granted by the license, users are provided only
+ * with a limited warranty and the software's author, the holder of the
+ * economic rights, and the successive licensors have only limited
+ * liability.
+ *
+ * In this respect, the user's attention is drawn to the risks associated
+ * with loading, using, modifying and/or developing or reproducing the
+ * software by the user in light of its specific status of free software,
+ * that may mean that it is complicated to manipulate, and that also
+ * therefore means that it is reserved for developers and experienced
+ * professionals having in-depth computer knowledge. Users are therefore
+ * encouraged to load and test the software's suitability as regards their
+ * requirements in conditions enabling the security of their systems and/or
+ * data to be ensured and, more generally, to use and operate it in the
+ * same conditions as regards security.
+ *
+ * The fact that you are presently reading this means that you have had
+ * knowledge of the CeCILL license and that you accept its terms.
+ *
+ * /**
+ * Class AvatarSecurityTranslationTests
+ * Creation: 1/10/2017
+ * @version 1.1 01/10/2017
+ * @author Letitia LI
+ * @see
+ */
+
+package avatartranslator;
+
+import org.junit.Test;
+import org.junit.*;
+
+import static org.junit.Assert.*;
+import static org.junit.Assert.assertFalse;
+import static org.junit.Assert.assertTrue;
+
+import ui.*;
+import ui.tmlcompd.*;
+
+import java.util.LinkedList;
+import java.util.HashMap;
+import java.util.LinkedList;
+import java.util.List;
+import java.util.Vector;
+
+import ui.tree.*;
+
+import javax.swing.*;
+
+import tmltranslator.*;
+import tmltranslator.toavatar.TML2Avatar;
+
+public class AvatarSecurityTranslationTests {
+ TMLMapping<TGComponent> map;
+ TMLTask task1;
+ TMLStartState start;
+ TMLModeling<TGComponent> tmlm;
+ public AvatarSecurityTranslationTests () {
+ //
+ }
+
+ @Before
+ public void setupDiploMapping (){
+ MainGUI mgui = new MainGUI(false, false, false, false, false, false, false, false, false, true, false, false);
+ mgui.initActions();
+ mgui.panelForTab = new JPanel();
+ mgui.frame = new JFrame();
+ mgui.dtree = new JDiagramTree(mgui);
+ mgui.dtree.setCellRenderer(new DiagramTreeRenderer());
+ ToolTipManager.sharedInstance().registerComponent(mgui.dtree);
+ JScrollPane scrollPane = new JScrollPane(mgui.dtree);
+ mgui.newTurtleModeling();
+// mgui.tabs = new Vector<TURTLEPanel>();
+ TMLComponentDesignPanel tmlcdp = new TMLComponentDesignPanel(mgui);
+ tmlcdp.tmlctdp = new TMLComponentTaskDiagramPanel(mgui, null);
+ tmlcdp.tmlctdp.tp = tmlcdp;
+
+ tmlm = new TMLModeling<TGComponent>();
+
+ task1= new TMLTask("DESIGN__task1", null, new TMLCPrimitiveComponent(0, 0, 0, 0, 0, 0, false, null, tmlcdp.tmlctdp));
+
+
+ start = new TMLStartState("start",null);
+ task1.getActivityDiagram().addElement(start);
+
+ tmlm.addTask(task1);
+ TMLArchitecture arch = new TMLArchitecture();
+ map = new TMLMapping<TGComponent>(tmlm, arch, false);
+
+ }
+ //protected void test () {
+
+ @Test
+ public void testBlockTranslation(){
+ TML2Avatar tml2avatar = new TML2Avatar(map,false,true);
+
+ AvatarSpecification avspec =tml2avatar.generateAvatarSpec("1");
+ assertTrue(avspec!=null);
+ assertEquals(avspec.getListOfBlocks().size(),1);
+
+ }
+
+ @Test
+ public void testTranslateStatesSymmetricEncryption(){
+ //setup security pattern
+ SecurityPattern sec = new SecurityPattern("sym", "Symmetric Encryption", "100", "100", "100", "100", "", "", "");
+ tmlm.addSecurityPattern(sec);
+
+ //Setup states
+ TMLExecC tmlexecc = new TMLExecC("encrypt_sym", null);
+ tmlexecc.securityPattern = sec;
+ start.addNext(tmlexecc);
+ task1.getActivityDiagram().addElement(tmlexecc);
+
+
+ TML2Avatar tml2avatar = new TML2Avatar(map,false,true);
+ AvatarSpecification avspec =tml2avatar.generateAvatarSpec("1");
+ assertTrue(avspec!=null);
+ AvatarBlock block1 = avspec.getBlockWithName("task1");
+ AvatarStateMachine sm = block1.getStateMachine();
+ LinkedList<AvatarStateMachineElement> elems= sm.getListOfElements();
+ //First state is start state
+ assertTrue(elems.get(0) instanceof AvatarStartState);
+ //state is avatartransition
+ assertTrue(elems.get(1) instanceof AvatarTransition);
+ //state is avatarstate
+ assertTrue(elems.get(2) instanceof AvatarState);
+ assertEquals(elems.get(2).getName(),"_encrypt_sym");
+ //Next state is avatartransition
+ assertTrue(elems.get(3) instanceof AvatarTransition);
+ assertEquals(elems.get(3).getName(),"__after_encrypt_sym");
+ AvatarTransition at = (AvatarTransition) elems.get(3);
+ //Check that action is encryption
+ assertEquals(at.getActions().get(0).getName().replaceAll(" ",""),"sym_encrypted=sencrypt(sym,key_sym)");
+ }
+
+
+ @Test
+ public void testTranslateStatesAsymmetricEncryption(){
+ //setup security pattern
+ SecurityPattern sec = new SecurityPattern("asym", "Asymmetric Encryption", "100", "100", "100", "100", "", "", "");
+ tmlm.addSecurityPattern(sec);
+
+ //Setup states
+ TMLExecC tmlexecc = new TMLExecC("encrypt_asym", null);
+ tmlexecc.securityPattern = sec;
+ start.addNext(tmlexecc);
+ task1.getActivityDiagram().addElement(tmlexecc);
+
+
+ TML2Avatar tml2avatar = new TML2Avatar(map,false,true);
+ AvatarSpecification avspec =tml2avatar.generateAvatarSpec("1");
+ assertTrue(avspec!=null);
+ AvatarBlock block1 = avspec.getBlockWithName("task1");
+ AvatarStateMachine sm = block1.getStateMachine();
+ LinkedList<AvatarStateMachineElement> elems= sm.getListOfElements();
+
+ AvatarTransition at = (AvatarTransition) elems.get(3);
+ //Check that action is encryption
+ assertEquals(at.getActions().get(0).getName().replaceAll(" ",""),"asym_encrypted=aencrypt(asym,pubKey_asym)");
+ }
+
+
+ @Test
+ public void testTranslateNonce(){
+ //setup security pattern
+ SecurityPattern sec = new SecurityPattern("asym", "Nonce", "100", "100", "100", "100", "", "", "");
+ tmlm.addSecurityPattern(sec);
+
+ //Setup states
+ TMLExecC tmlexecc = new TMLExecC("encrypt_asym", null);
+ tmlexecc.securityPattern = sec;
+ start.addNext(tmlexecc);
+ task1.getActivityDiagram().addElement(tmlexecc);
+
+
+ TML2Avatar tml2avatar = new TML2Avatar(map,false,true);
+ AvatarSpecification avspec =tml2avatar.generateAvatarSpec("1");
+ assertTrue(avspec!=null);
+ AvatarBlock block1 = avspec.getBlockWithName("task1");
+ AvatarStateMachine sm = block1.getStateMachine();
+ LinkedList<AvatarStateMachineElement> elems= sm.getListOfElements();
+
+ AvatarTransition at = (AvatarTransition) elems.get(3);
+ //Check that action is empty
+ assertEquals(at.getActions().size(),0);
+ //Check that next state is random
+ assertTrue(elems.get(4) instanceof AvatarRandom);
+
+ }
+
+
+
+ @Test
+ public void testTranslateMAC(){
+ //setup security pattern
+ SecurityPattern sec = new SecurityPattern("mac", "MAC", "100", "100", "100", "100", "", "", "");
+ tmlm.addSecurityPattern(sec);
+
+ //Setup states
+ TMLExecC tmlexecc = new TMLExecC("encrypt_mac", null);
+ tmlexecc.securityPattern = sec;
+ start.addNext(tmlexecc);
+ task1.getActivityDiagram().addElement(tmlexecc);
+
+
+ TML2Avatar tml2avatar = new TML2Avatar(map,false,true);
+ AvatarSpecification avspec =tml2avatar.generateAvatarSpec("1");
+ assertTrue(avspec!=null);
+ AvatarBlock block1 = avspec.getBlockWithName("task1");
+ AvatarStateMachine sm = block1.getStateMachine();
+ LinkedList<AvatarStateMachineElement> elems= sm.getListOfElements();
+
+ AvatarTransition at = (AvatarTransition) elems.get(3);
+ //Check that action is encryption
+ assertEquals(at.getActions().get(0).getName().replaceAll(" ",""),"mac_mac=MAC(mac,key_mac)");
+ }
+
+
+
+ public static void main(String[] args){
+ AvatarSecurityTranslationTests apt = new AvatarSecurityTranslationTests ();
+ //apt.runTest ();
+ }
+}