diff --git a/src/tmltranslator/TMLChannel.java b/src/tmltranslator/TMLChannel.java
index 917896b39122ad6696faad01ac5cb8a765b7160d..c15367b2d0d9a650e4b8333b3ae484c80087a8c1 100755
--- a/src/tmltranslator/TMLChannel.java
+++ b/src/tmltranslator/TMLChannel.java
@@ -55,8 +55,8 @@ public class TMLChannel extends TMLCommunicationElement {
public static final int BRBW = 0;
public static final int BRNBW = 1;
public static final int NBRNBW = 2;
- public static int confStatus;
- public static boolean checkConf;
+ public int confStatus;
+ public boolean checkConf;
private int size;
private int type;
private int max;
@@ -85,6 +85,7 @@ public class TMLChannel extends TMLCommunicationElement {
originPorts = new ArrayList<TMLPort>();
destinationPorts = new ArrayList<TMLPort>();
ports = new ArrayList<TMLCPrimitivePort>();
+ checkConf=false;
}
diff --git a/src/tmltranslator/TMLEvent.java b/src/tmltranslator/TMLEvent.java
index 85aa4d49baf8ecf781d1e5c1a56c13e156ef393e..6df4a0e0fd0973b7c99f0b2824631ca471fdcc0c 100755
--- a/src/tmltranslator/TMLEvent.java
+++ b/src/tmltranslator/TMLEvent.java
@@ -54,8 +54,8 @@ public class TMLEvent extends TMLCommunicationElement {
protected boolean isBlocking = false; // By default, latest events is removed when the FIFO is full
protected boolean canBeNotified = false;
protected TMLTask origin, destination;
- public static int confStatus;
- public static boolean checkConf;
+ public int confStatus;
+ public boolean checkConf;
public TMLCPrimitivePort port;
public TMLCPrimitivePort port2;
/*public TMLEvent(String name, Object reference) {
@@ -69,7 +69,7 @@ public class TMLEvent extends TMLCommunicationElement {
maxEvt = _maxEvt;
isBlocking = _isBlocking;
checkMaxEvt();
-
+ checkConf=false;
//System.out.println("New event: " + name + " max=" + _maxEvt + " blocking=" + isBlocking);
}
diff --git a/src/tmltranslator/TMLModeling.java b/src/tmltranslator/TMLModeling.java
index 8b25648f94bf6d7c7972be7fa7dde22748f33892..fc979e811ebeaa7ac8e7446a9bc56c6b25bea438 100755
--- a/src/tmltranslator/TMLModeling.java
+++ b/src/tmltranslator/TMLModeling.java
@@ -48,6 +48,7 @@ package tmltranslator;
import java.util.*;
import myutil.*;
import ui.tmlcompd.*;
+import ui.TAttribute;
import avatartranslator.*;
import proverifspec.*;
//import compiler.expression.*;
@@ -603,61 +604,106 @@ public class TMLModeling {
LinkedList<AvatarAttribute> secretAttributes = pvoa.getSecretTerms ();
LinkedList<AvatarAttribute> nonSecretAttributes = pvoa.getNonSecretTerms ();
for (AvatarAttribute attr: secretAttributes){
- System.out.println("Attribute " + attr.getName());
TMLChannel channel = getChannelByName(attr.getName().replaceAll("__chData",""));
if (channel!=null){
- System.out.println("write to chan " + channel.getName());
for (TMLCPrimitivePort port:channel.ports){
- port.checkStatus = 2;
- port.mappingName= mappingName;
+ if (port.checkConf){
+ port.checkStatus = 2;
+ port.mappingName= mappingName;
+ }
}
}
TMLRequest req = getRequestByName(attr.getName().replaceAll("__reqData",""));
if (req !=null){
- System.out.println("write to req " + req.getName());
for (TMLCPrimitivePort port: req.ports){
- port.checkStatus=2;
- port.mappingName= mappingName;
+ if (port.checkConf){
+ port.checkStatus = 2;
+
+ port.mappingName= mappingName;
+ }
}
}
TMLEvent ev = getEventByName(attr.getName().replaceAll("__eventData",""));
if (ev !=null){
- System.out.println("write to event " + ev.getName());
- ev.port.checkStatus=2;
- ev.port.mappingName= mappingName;
+ if (ev.port.checkConf){
+ ev.port.checkStatus=2;
+ ev.port.mappingName= mappingName;
+ }
+ if (ev.port2.checkConf){
+ ev.port2.checkStatus=2;
+ ev.port2.mappingName=mappingName;
+ }
+ }
+ for (TMLTask t:getTasks()){
+ if (t.getReferenceObject()==null){
+ continue;
+ }
+ if (t.getReferenceObject() instanceof TMLCPrimitiveComponent && t.getName().equals(attr.getBlock().getName())){
+ TMLCPrimitiveComponent comp = (TMLCPrimitiveComponent) t.getReferenceObject();
+ comp.mappingName=mappingName;
+ Vector attrs = comp.getAttributes();
+ int i=0;
+ while(i < attrs.size() ) {
+ TAttribute a = (TAttribute)(attrs.elementAt(i));
+ if (a.getId().equals(attr.getName()) ){
+ a.setConfidentialityVerification(TAttribute.CONFIDENTIALITY_OK);
+ }
+ i++;
+ }
+ }
}
}
for (AvatarAttribute attr: nonSecretAttributes){
TMLChannel channel = getChannelByName(attr.getName().replaceAll("__chData",""));
if (channel!=null){
- System.out.println("write to ch " + channel.getName());
for (TMLCPrimitivePort port:channel.ports){
- port.checkStatus = 3;
- port.mappingName= mappingName;
+ if (port.checkConf){
+ port.checkStatus = 3;
+ port.mappingName= mappingName;
+ }
}
}
TMLRequest req = getRequestByName(attr.getName().replaceAll("__reqData",""));
if (req !=null){
- System.out.println("write to req " + req.getName());
for (TMLCPrimitivePort port: req.ports){
- port.checkStatus=3;
- port.mappingName= mappingName;
+ if (port.checkConf){
+ port.checkStatus = 3;
+ port.mappingName= mappingName;
+ }
}
}
TMLEvent ev = getEventByName(attr.getName().replaceAll("__eventData",""));
if (ev !=null){
- System.out.println("write to event " + ev.getName());
- ev.port.checkStatus=3;
- ev.port2.checkStatus=3;
- ev.port.mappingName= mappingName;
+ if (ev.port.checkConf){
+ ev.port.checkStatus=3;
+ }
+ if (ev.port2.checkConf){
+ ev.port2.checkStatus=3;
+ ev.port2.mappingName= mappingName;
+ }
+ }
+ for (TMLTask t:getTasks()){
+ if (t.getReferenceObject() instanceof TMLCPrimitiveComponent){
+ TMLCPrimitiveComponent comp = (TMLCPrimitiveComponent) t.getReferenceObject();
+ comp.mappingName=mappingName;
+ Vector attrs = comp.getAttributes();
+ int i=0;
+ while(i < attrs.size()) {
+ TAttribute a = (TAttribute)(attrs.elementAt(i));
+ if (a.getId().equals(attr.getName()) &&t.getName().equals(attr.getBlock().getName())){
+ a.setConfidentialityVerification(TAttribute.CONFIDENTIALITY_KO);
+ }
+ i++;
+ }
+ }
}
}
+
System.out.println("backtracing finished");
return;
}
public void clearBacktracing(){
for (TMLChannel channel: getChannels()){
- System.out.println("Channel " + channel.getName());
for (TMLCPrimitivePort port:channel.ports){
if (port.checkStatus>1){
port.checkStatus=1;
diff --git a/src/tmltranslator/TMLRequest.java b/src/tmltranslator/TMLRequest.java
index d36524359dbb68b7e7eebc4c85e99a8c5f8db0c0..51ac20f00247af9967d0af2e4e10b67bcc73185b 100755
--- a/src/tmltranslator/TMLRequest.java
+++ b/src/tmltranslator/TMLRequest.java
@@ -53,8 +53,8 @@ public class TMLRequest extends TMLCommunicationElement {
protected ArrayList<TMLTask> originTasks; // list of tasks from which request starts
protected TMLTask destinationTask;
protected ArrayList<String> paramNames;
- public static int confStatus;
- public static boolean checkConf;
+ public int confStatus;
+ public boolean checkConf;
public ArrayList<TMLCPrimitivePort> ports;
public TMLRequest(String name, Object reference) {
super(name, reference);
@@ -62,6 +62,7 @@ public class TMLRequest extends TMLCommunicationElement {
originTasks = new ArrayList<TMLTask>();
paramNames = new ArrayList<String>();
ports = new ArrayList<TMLCPrimitivePort>();
+ checkConf=false;
}
public int getNbOfParams() {
diff --git a/src/tmltranslator/toavatar/TML2Avatar.java b/src/tmltranslator/toavatar/TML2Avatar.java
index 3b5c76b76e95bf4eae423d4e6d28867a8c391bef..5ed4a6e996bd320b8df59d9b6e5c6294515201f2 100644
--- a/src/tmltranslator/toavatar/TML2Avatar.java
+++ b/src/tmltranslator/toavatar/TML2Avatar.java
@@ -59,6 +59,7 @@ import javax.xml.parsers.*;
import ui.ConfigurationTTool;
import ui.CheckingError;
import ui.AvatarDesignPanel;
+import ui.tmlcompd.*;
import ui.TGComponent;
import proverifspec.*;
import myutil.*;
@@ -225,7 +226,7 @@ public class TML2Avatar {
done.add(curr);
}
if (path.size() ==0){
- System.out.println("Path does not exist for channel " + channel.getName() + " between Task " + a.getTaskName() + " and Task " + t.getTaskName());
+ // System.out.println("Path does not exist for channel " + channel.getName() + " between Task " + a.getTaskName() + " and Task " + t.getTaskName());
channelMap.put(channel, channelUnreachable);
}
else {
@@ -242,7 +243,7 @@ public class TML2Avatar {
}
}
channelMap.put(channel, priv);
- System.out.println("Channel "+channel.getName() + " between Task "+ a.getTaskName() + " and Task " + t.getTaskName() + " is " + (priv==1 ? "confidential" : "not confidential"));
+ //System.out.println("Channel "+channel.getName() + " between Task "+ a.getTaskName() + " and Task " + t.getTaskName() + " is " + (priv==1 ? "confidential" : "not confidential"));
}
}
}
@@ -517,6 +518,7 @@ public class TML2Avatar {
for (int i=0; i< aee.getNbOfParams(); i++){
if (block.getAvatarAttributeWithName(aee.getParam(i))==null){
//Throw Error
+ as.addValue("tmp");
System.out.println("Missing Attribute " + aee.getParam(i));
}
else {
@@ -818,7 +820,6 @@ public class TML2Avatar {
public AvatarSpecification generateAvatarSpec(){
//TODO: Add pragmas
- //TODO: Fix Avatar2Proverif warning references to panel
//TODO: Make state names readable
//TODO: Put back numeric guards
//TODO: Calcuate for temp variable
@@ -829,6 +830,21 @@ public class TML2Avatar {
return avspec;
}
attrsToCheck.clear();
+
+ for (TMLChannel channel: tmlmodel.getChannels()){
+ for (TMLCPrimitivePort p: channel.ports){
+ channel.checkConf = channel.checkConf || p.checkConf;
+ }
+ }
+ for (TMLEvent event: tmlmodel.getEvents()){
+ event.checkConf = event.port.checkConf || event.port2.checkConf;
+ }
+ for (TMLRequest request: tmlmodel.getRequests()){
+ for (TMLCPrimitivePort p: request.ports){
+ request.checkConf = p.checkConf || request.checkConf;
+ }
+ }
+
ArrayList<TMLTask> tasks = tmlmap.getTMLModeling().getTasks();
for (TMLTask task:tasks){
AvatarBlock block = new AvatarBlock(task.getName(), avspec, task.getReferenceObject());
@@ -856,7 +872,6 @@ public class TML2Avatar {
//TODO: Create a fork with many requests. This looks terrible
if (tmlmodel.getRequestToMe(task)!=null){
TMLRequest request= tmlmodel.getRequestToMe(task);
- System.out.println("request to me " + request.getName());
//Oh this is fun...let's restructure the state machine
//Create own start state, and ignore the returned one
List<AvatarStateMachineElement> elementList= translateState(task.getActivityDiagram().get(0), block);
@@ -878,7 +893,6 @@ public class TML2Avatar {
if (block.getAvatarAttributeWithName(request.getParam(i))==null){
//Throw Error
as.addValue("tmp");
- System.out.println("Missing Attribute " + request.getParam(i));
}
else {
as.addValue(request.getParam(i));
@@ -959,11 +973,9 @@ public class TML2Avatar {
}
}
if (sig1.size()==0){
- System.out.println("Failure at " + channel.getDestinationTask().getName()+"__IN__"+channel.getName());
sig1.add(new AvatarSignal(channel.getDestinationTask().getName()+"__IN__"+channel.getName(), AvatarSignal.IN, null));
}
if (sig2.size()==0){
- System.out.println("Fail " + channel.getOriginTask().getName()+"__OUT__"+channel.getName());
sig2.add(new AvatarSignal(channel.getOriginTask().getName()+"__OUT__"+channel.getName(), AvatarSignal.OUT, null));
}
if (sig1.size()==1 && sig2.size()==1){
@@ -975,7 +987,6 @@ public class TML2Avatar {
avspec.addRelation(ar);
}
else {
- 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());
@@ -1057,6 +1068,7 @@ public class TML2Avatar {
}
}
for (TMLEvent event: tmlmodel.getEvents()){
+
AvatarRelation ar = new AvatarRelation(event.getName(), taskBlockMap.get(event.getOriginTask()), taskBlockMap.get(event.getDestinationTask()), event.getReferenceObject());
ar.setPrivate(originDestMap.get(event.getOriginTask().getName()+"__"+event.getDestinationTask().getName())==1);
List<AvatarSignal> sig1 = new ArrayList<AvatarSignal>();
diff --git a/src/ui/GTMLModeling.java b/src/ui/GTMLModeling.java
index f8e660831eea60e5bc285e1718aa2c0b0c853971..249ea14cccdec7bd58031712590d3dfa19c09210 100755
--- a/src/ui/GTMLModeling.java
+++ b/src/ui/GTMLModeling.java
@@ -717,7 +717,6 @@ public class GTMLModeling {
addToTable(makeName(port2, port2.getFather().getValue()) + "/" + name2, name);
channel = new TMLChannel(name, port1);
- channel.checkConf= port1.checkConf || port2.checkConf;
channel.setSize(port1.getSize());
channel.setMax(port1.getMax());
channel.ports.add(port1);
@@ -816,10 +815,8 @@ public class GTMLModeling {
port = (TMLCPrimitivePort)(portstome.get(0));
channel = new TMLChannel(name, port1);
channel.ports.add(port1);
- channel.checkConf= port1.checkConf;
for(j=0; j<portstome.size(); j++) {
TMLCPrimitivePort p = (TMLCPrimitivePort)(portstome.get(j));
- channel.checkConf= p.checkConf || channel.checkConf;
channel.ports.add(p);
}
channel.setSize(port1.getSize());
@@ -961,7 +958,8 @@ public class GTMLModeling {
} else {
event = new TMLEvent(name, port1, -1, port1.isBlocking());
}
- event.checkConf= port1.checkConf;
+ event.port=port1;
+ event.port2= port2;
for(i=0; i<port1.getNbMaxAttribute(); i++) {
tt = port1.getParamAt(i);
if ((tt != null) && (tt.getType() != TType.NONE)) {
@@ -1096,15 +1094,16 @@ public class GTMLModeling {
name = makeName(port1, name1);
addToTable(makeName(port1, port1.getFather().getValue()) + "/" + name1, name);
+ request = new TMLRequest(name, port1);
+ request.ports.add(port1);
for(i=0; i<portstome.size(); i++) {
port2 = (TMLCPrimitivePort)(portstome.get(i));
+ request.ports.add(port2);
TraceManager.addDev("Add add add to table request : " + makeName(port2, port2.getFather().getValue()) + "/" + port2.getName() + " name =" + name);
addToTable(makeName(port2, port2.getFather().getValue()) + "/" + port2.getPortName(), name);
}
- request = new TMLRequest(name, port1);
- request.checkConf = port1.checkConf;
- request.ports.add(port1);
+
for(i=0; i<port1.getNbMaxAttribute(); i++) {
tt = port1.getParamAt(i);
if ((tt != null) && (tt.getType() != TType.NONE)) {
diff --git a/src/ui/tmlcompd/TMLCPrimitiveComponent.java b/src/ui/tmlcompd/TMLCPrimitiveComponent.java
index c572e701467db6d33d184bf605b2adce15502586..69a5b5c9f2cfcc54fc86fd72d5d82ead44a3e9be 100755
--- a/src/ui/tmlcompd/TMLCPrimitiveComponent.java
+++ b/src/ui/tmlcompd/TMLCPrimitiveComponent.java
@@ -72,6 +72,8 @@ public class TMLCPrimitiveComponent extends TGCScalableWithInternalComponent imp
// Attributes
private boolean attributesAreDrawn = false;
+ public HashMap<String, Integer> attrMap = new HashMap<String, Integer>();
+ public String mappingName;
protected Vector myAttributes;
private int textX = 15; // border for ports
private double dtextX = 0.0;
@@ -218,6 +220,7 @@ public class TMLCPrimitiveComponent extends TGCScalableWithInternalComponent imp
w = g.getFontMetrics().stringWidth(attr);
if ((w + (2 * textX) + 1) < width) {
g.drawString(attr, x + textX, y + cpt);
+ drawVerification(g, x + textX, y+ cpt, a.getConfidentialityVerification());
} else {
attr = "...";
w = g.getFontMetrics().stringWidth(attr);
@@ -234,6 +237,28 @@ public class TMLCPrimitiveComponent extends TGCScalableWithInternalComponent imp
g.setFont(fold);
+ }
+ public void drawVerification(Graphics g, int x, int y, int checkStatus){
+ Color c = g.getColor();
+ Color c1;
+ switch(checkStatus) {
+ case TAttribute.CONFIDENTIALITY_OK:
+ c1 = Color.green;
+ break;
+ case TAttribute.CONFIDENTIALITY_KO:
+ c1 = Color.red;
+ break;
+ default:
+ return;
+ }
+ g.drawOval(x-10, y-10, 6, 9);
+ g.setColor(c1);
+ g.fillRect(x-12, y-5, 9, 7);
+ g.setColor(c);
+ g.drawRect(x-12, y-5, 9, 7);
+
+
+
}
public void rescale(double scaleFactor){
diff --git a/src/ui/tmlcompd/TMLCPrimitivePort.java b/src/ui/tmlcompd/TMLCPrimitivePort.java
index c76c6e351f0da86556c5870b2cfcfb4aa2e83068..12d11333ce920e4732c8ecd0b1062fb7cae711ac 100755
--- a/src/ui/tmlcompd/TMLCPrimitivePort.java
+++ b/src/ui/tmlcompd/TMLCPrimitivePort.java
@@ -112,7 +112,7 @@ public abstract class TMLCPrimitivePort extends TGCScalableWithInternalComponent
editable = true;
removable = true;
userResizable = false;
- checkConf=true;
+ checkConf=false;
commName = "comm";
//value = "MyName";
makeValue();
@@ -318,9 +318,9 @@ public abstract class TMLCPrimitivePort extends TGCScalableWithInternalComponent
g.drawString(lname, x+width - w - 1, y+(int)(si)-2);
}
}*/
-
+ if (checkConf){
drawVerification(g);
-
+ }
g.setFont(fold);
drawParticularity(g);