From 65b1e6a12341cf56c8612cda5bd73f71ce3e4e3f Mon Sep 17 00:00:00 2001
From: jerray <jawher.jerray@eurecom.fr>
Date: Tue, 27 Feb 2024 19:13:25 +0100
Subject: [PATCH] Minor update in handling confidentiality in AD
---
.../tmltranslator/SecurityBacktracer.java | 8 +
.../java/tmltranslator/SecurityDecryptor.java | 6 +
src/main/java/tmltranslator/TMLModeling.java | 176 ++++++++++++++---
.../TMLPortWithSecurityInformation.java | 8 +-
.../tmltranslator/toavatarsec/TML2Avatar.java | 185 ++++++++----------
src/main/java/ui/MainGUI.java | 2 -
src/main/java/ui/TDiagramPanel.java | 31 ++-
src/main/java/ui/avatarbd/AvatarBDBlock.java | 2 +-
.../java/ui/avatarbd/AvatarBDInterface.java | 2 +-
src/main/java/ui/avatarbd/AvatarBDPragma.java | 2 +-
.../JFrameSimulationSDPanel.java | 129 ++++++++----
.../JSimulationSDPanel.java | 10 +-
src/main/java/ui/tmlad/TMLADDecrypt.java | 98 ++++++++--
src/main/java/ui/tmlad/TMLADReadChannel.java | 119 +++++++++--
src/main/java/ui/tmlad/TMLADWriteChannel.java | 100 ++++++++--
.../java/ui/tmlcompd/TMLCChannelOutPort.java | 3 +-
.../java/ui/tmlcompd/TMLCPrimitivePort.java | 167 ++++++++--------
...JDialogAvatarExecutableCodeGeneration.java | 2 +-
...ialogAvatarddExecutableCodeGeneration.java | 2 +-
.../java/ui/window/JDialogMultiString.java | 4 +
.../ui/window/JDialogMultiStringAndTabs.java | 6 +
.../window/JDialogProverifVerification.java | 5 +-
22 files changed, 759 insertions(+), 308 deletions(-)
diff --git a/src/main/java/tmltranslator/SecurityBacktracer.java b/src/main/java/tmltranslator/SecurityBacktracer.java
index 8dfc4185cf..ca899ef721 100644
--- a/src/main/java/tmltranslator/SecurityBacktracer.java
+++ b/src/main/java/tmltranslator/SecurityBacktracer.java
@@ -50,6 +50,10 @@
package tmltranslator;
+import proverifspec.ProVerifResultTrace;
+
+import java.util.List;
+
public interface SecurityBacktracer {
@@ -73,4 +77,8 @@ public interface SecurityBacktracer {
public int getConfStatus();
void setConfStatus(int _confStatus);
+ public void setResultTraces(List<ProVerifResultTrace> traces) ;
+
+ public void setPragmasString(List<String> _pragmas);
+
}
diff --git a/src/main/java/tmltranslator/SecurityDecryptor.java b/src/main/java/tmltranslator/SecurityDecryptor.java
index 00c6edffd0..1f1e00ef75 100644
--- a/src/main/java/tmltranslator/SecurityDecryptor.java
+++ b/src/main/java/tmltranslator/SecurityDecryptor.java
@@ -50,6 +50,10 @@
package tmltranslator;
+import proverifspec.ProVerifResultTrace;
+
+import java.util.List;
+
public interface SecurityDecryptor {
public boolean getAuthCheck();
@@ -65,5 +69,7 @@ public interface SecurityDecryptor {
public String getSecurityContext();
+ public void setResultTraces(List<ProVerifResultTrace> traces);
+ public void setPragmasString(List<String> _pragmas);
}
diff --git a/src/main/java/tmltranslator/TMLModeling.java b/src/main/java/tmltranslator/TMLModeling.java
index ce5f3d4155..cbb3ca667f 100755
--- a/src/main/java/tmltranslator/TMLModeling.java
+++ b/src/main/java/tmltranslator/TMLModeling.java
@@ -64,7 +64,8 @@ public class TMLModeling<E> {
// Security
private List<SecurityPattern> secPatterns;
private Map<TMLChannel, Set<AvatarPragma>> secChannelMap;
- private Map<TMLWriteChannel, Set<AvatarPragma>> wrPragmaMap;
+ private Map<TMLWriteChannel, Set<AvatarPragma>> confPragmaMap;
+ private Map<TMLActivityElement, Set<AvatarPragma>> authPragmaMap;
private Map<SecurityPattern, List<TMLTask>> securityTaskMap;
// Tasks and communication
@@ -133,12 +134,12 @@ public class TMLModeling<E> {
this.secChannelMap = secChannelMap;
}
- public Map<TMLWriteChannel, Set<AvatarPragma>> getWrPragmaMap() {
- return wrPragmaMap;
+ public void setConfPragmaMap(Map<TMLWriteChannel, Set<AvatarPragma>> confPragmaMap) {
+ this.confPragmaMap = confPragmaMap;
}
- public void setWrPragmaMap(Map<TMLWriteChannel, Set<AvatarPragma>> wrPragmaMap) {
- this.wrPragmaMap = wrPragmaMap;
+ public void setAuthPragmaMap(Map<TMLActivityElement, Set<AvatarPragma>> authPragmaMap) {
+ this.authPragmaMap = authPragmaMap;
}
public TMLMapping<E> getDefaultMapping() {
@@ -803,9 +804,11 @@ public class TMLModeling<E> {
for (TMLActivityElement actElem : task.getActivityDiagram().getElements()) {
if (actElem instanceof TMLWriteChannel) {
TMLWriteChannel wc = (TMLWriteChannel) actElem;
- if (wrPragmaMap.containsKey(wc)) {
+ if (confPragmaMap.containsKey(wc)) {
List<Integer> confStatus = new ArrayList<Integer>();
- for (AvatarPragma pragma : wrPragmaMap.get(wc)) {
+ List<ProVerifResultTrace> traces = new ArrayList<ProVerifResultTrace>();
+ List<String> pragmasString = new ArrayList<String>();
+ for (AvatarPragma pragma : confPragmaMap.get(wc)) {
if (pragma instanceof AvatarPragmaSecret) {
AvatarPragmaSecret pragmaSecret = (AvatarPragmaSecret) pragma;
ProVerifQueryResult result = confResults.get(pragmaSecret);
@@ -816,6 +819,11 @@ public class TMLModeling<E> {
int r = result.isSatisfied() ? 2 : 3;
confStatus.add(r);
}
+ ProVerifResultTrace trace = confResults.get(pragmaSecret).getTrace();
+ if (trace != null) {
+ traces.add(trace);
+ pragmasString.add(pragma.toString());
+ }
}
}
}
@@ -833,6 +841,104 @@ public class TMLModeling<E> {
SecurityBacktracer sec = (SecurityBacktracer) wc.getReferenceObject();
sec.setConfCheck(ch.checkConf);
sec.setConfStatus(generalConfResult);
+ if (!traces.isEmpty()) {
+ sec.setResultTraces(traces);
+ sec.setPragmasString(pragmasString);
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+
+ public void backtraceAuthenticityADReadChannels(Map<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> authResults, TMLChannel ch) {
+ if (ch.isCheckConfChannel()) {
+ List<TMLTask> tasks = new ArrayList<TMLTask>();
+ if (!ch.getDestinationTasks().isEmpty()) {
+ tasks.addAll(ch.getDestinationTasks());
+ } else {
+ tasks.add(ch.getDestinationTask());
+ }
+ for (TMLTask task : tasks) {
+ for (TMLActivityElement actElem : task.getActivityDiagram().getElements()) {
+ if (authPragmaMap.containsKey(actElem)) {
+ List<Integer> weakAuthStatus = new ArrayList<Integer>();
+ List<Integer> strongAuthStatus = new ArrayList<Integer>();
+ List<ProVerifResultTrace> traces = new ArrayList<ProVerifResultTrace>();
+ List<String> pragmasString = new ArrayList<String>();
+ for (AvatarPragma pragma : authPragmaMap.get(actElem)) {
+ if (pragma instanceof AvatarPragmaAuthenticity) {
+ AvatarPragmaAuthenticity pragmaAuth = (AvatarPragmaAuthenticity) pragma;
+ ProVerifQueryAuthResult result = authResults.get(pragmaAuth);
+ if (result != null) {
+ if (!result.isProved()) {
+ strongAuthStatus.add(1);
+ } else if (result.isProved() && result.isSatisfied()) {
+ strongAuthStatus.add(2);
+ } else if (result.isProved() && !result.isSatisfied()) {
+ strongAuthStatus.add(3);
+ }
+
+ if (!result.isWeakProved()) {
+ weakAuthStatus.add(1);
+ } else if (result.isWeakProved() && result.isWeakSatisfied()) {
+ weakAuthStatus.add(2);
+ } else if (result.isWeakProved() && !result.isWeakSatisfied()) {
+ weakAuthStatus.add(3);
+ }
+ ProVerifResultTrace trace = authResults.get(pragmaAuth).getTrace();
+ if (trace != null) {
+ traces.add(trace);
+ pragmasString.add(pragma.toString());
+ }
+ }
+ }
+ }
+ int generalStrongAuthResult = 1;
+ int generalWeakAuthResult = 1;
+ if (!weakAuthStatus.isEmpty()) {
+ if (weakAuthStatus.contains(3)) {
+ generalWeakAuthResult = 3;
+ } else if (weakAuthStatus.contains(1)) {
+ generalWeakAuthResult = 1;
+ } else {
+ generalWeakAuthResult = 2;
+ }
+ }
+ if (!strongAuthStatus.isEmpty()) {
+ if (strongAuthStatus.contains(3)) {
+ generalStrongAuthResult = 3;
+ } else if (strongAuthStatus.contains(1)) {
+ generalStrongAuthResult = 1;
+ } else {
+ generalStrongAuthResult = 2;
+ }
+ }
+ if (actElem instanceof TMLReadChannel) {
+ TMLReadChannel rc = (TMLReadChannel) actElem;
+ if (rc.getReferenceObject() instanceof SecurityBacktracer) {
+ SecurityBacktracer sec = (SecurityBacktracer) rc.getReferenceObject();
+ sec.setAuthCheck(ch.checkAuth);
+ sec.setWeakAuthStatus(generalWeakAuthResult);
+ sec.setStrongAuthStatus(generalStrongAuthResult);
+ if (!traces.isEmpty()) {
+ sec.setResultTraces(traces);
+ sec.setPragmasString(pragmasString);
+ }
+ }
+ } else if (actElem instanceof TMLExecC) {
+ TMLExecC dec = (TMLExecC) actElem;
+ if (dec.getReferenceObject() instanceof SecurityDecryptor) {
+ SecurityDecryptor sec = (SecurityDecryptor) dec.getReferenceObject();
+ sec.setAuthCheck(ch.checkAuth);
+ sec.setWeakAuthStatus(generalWeakAuthResult);
+ sec.setStrongAuthStatus(generalStrongAuthResult);
+ if (!traces.isEmpty()) {
+ sec.setResultTraces(traces);
+ sec.setPragmasString(pragmasString);
+ }
}
}
}
@@ -848,8 +954,8 @@ public class TMLModeling<E> {
if (ch.isCheckConfChannel()) {
List<Integer> confStatus = new ArrayList<Integer>();
Set<String> secNames = new HashSet<String>();
- ProVerifResultTrace trace = null;
- String pragmaString = "";
+ List<ProVerifResultTrace> traces = new ArrayList<ProVerifResultTrace>();
+ List<String> pragmasString = new ArrayList<String>();
for (AvatarPragma pragma : secChannelMap.get(ch)) {
if (pragma instanceof AvatarPragmaSecret) {
AvatarPragmaSecret pragmaSecret = (AvatarPragmaSecret) pragma;
@@ -863,8 +969,11 @@ public class TMLModeling<E> {
confStatus.add(r);
}
//backtraceConfidentialityInAD(pragmaSecret, ch, confStatus.get(confStatus.size() - 1));
- trace = pvoa.getResults().get(pragma).getTrace();
- pragmaString = pragma.toString();
+ ProVerifResultTrace trace = pvoa.getResults().get(pragma).getTrace();
+ if (trace != null) {
+ traces.add(trace);
+ pragmasString.add(pragma.toString());
+ }
}
}
}
@@ -880,13 +989,13 @@ public class TMLModeling<E> {
}
}
for (TMLPortWithSecurityInformation port : ch.ports) {
- if (port.getCheckConf()) {
+ if (port.getCheckConf() && port.isOrigin()) {
port.setConfStatus(generalConfResult);
port.setSecName(String.join(" ", secNames));
port.setMappingName(mappingName);
- port.setPragmaString(pragmaString);
- if (trace != null) {
- port.setResultTrace(trace);
+ if (!traces.isEmpty()) {
+ port.setResultTraces(traces);
+ port.setPragmasString(pragmasString);
}
}
}
@@ -916,8 +1025,8 @@ public class TMLModeling<E> {
List<Integer> weakAuthStatus = new ArrayList<Integer>();
List<Integer> strongAuthStatus = new ArrayList<Integer>();
String secName = "";
- ProVerifResultTrace trace = null;
- String pragmaString = "";
+ List<ProVerifResultTrace> traces = new ArrayList<ProVerifResultTrace>();
+ List<String> pragmasString = new ArrayList<String>();
for (AvatarPragma pragma : secChannelMap.get(ch)) {
if (pragma instanceof AvatarPragmaAuthenticity) {
AvatarPragmaAuthenticity pragmaAuth = (AvatarPragmaAuthenticity) pragma;
@@ -944,8 +1053,11 @@ public class TMLModeling<E> {
TraceManager.addDev("Backtracing Authenticity weak proved and not weak satisfied");
weakAuthStatus.add(3);
}
- trace = pvoa.getResults().get(pragma).getTrace();
- pragmaString = pragma.toString();
+ ProVerifResultTrace trace = pvoa.getResults().get(pragma).getTrace();
+ if (trace != null) {
+ traces.add(trace);
+ pragmasString.add(pragma.toString());
+ }
}
}
}
@@ -970,17 +1082,18 @@ public class TMLModeling<E> {
}
}
for (TMLPortWithSecurityInformation port : ch.ports) {
- if (port.getCheckAuth()) {
+ if (port.getCheckAuth() && !port.isOrigin()) {
port.setStrongAuthStatus(generalStrongAuthResult);
port.setWeakAuthStatus(generalWeakAuthResult);
port.setSecName(secName);
port.setMappingName(mappingName);
- if (trace != null && !port.isOrigin()) {
- port.setResultTrace(trace);
- port.setPragmaString(pragmaString);
+ if (!traces.isEmpty()) {
+ port.setResultTraces(traces);
+ port.setPragmasString(pragmasString);
}
}
}
+ backtraceAuthenticityADReadChannels(authenticityResults, ch);
}
}
}
@@ -998,8 +1111,8 @@ public class TMLModeling<E> {
port.setStrongAuthStatus(1);
port.setWeakAuthStatus(1);
}
- port.setResultTrace(null);
- port.setPragmaString("");
+ port.setResultTraces(new ArrayList<ProVerifResultTrace>());
+ port.setPragmasString(new ArrayList<String>());
}
}
@@ -1036,6 +1149,19 @@ public class TMLModeling<E> {
}
}
}
+ for (TMLTask task : tasks) {
+ for (TMLActivityElement actElem : task.getActivityDiagram().getElements()) {
+ if (actElem instanceof TMLWriteChannel) {
+ TMLWriteChannel wc = (TMLWriteChannel) actElem;
+ if (wc.getReferenceObject() instanceof SecurityBacktracer) {
+ SecurityBacktracer sec = (SecurityBacktracer) wc.getReferenceObject();
+ sec.setConfStatus(1);
+ sec.setResultTraces(new ArrayList<ProVerifResultTrace>());
+ sec.setPragmasString(new ArrayList<String>());
+ }
+ }
+ }
+ }
return;
}
diff --git a/src/main/java/tmltranslator/TMLPortWithSecurityInformation.java b/src/main/java/tmltranslator/TMLPortWithSecurityInformation.java
index d659e9fb1c..35f0fee20e 100644
--- a/src/main/java/tmltranslator/TMLPortWithSecurityInformation.java
+++ b/src/main/java/tmltranslator/TMLPortWithSecurityInformation.java
@@ -52,6 +52,8 @@ package tmltranslator;
import proverifspec.ProVerifResultTrace;
+import java.util.List;
+
public interface TMLPortWithSecurityInformation {
@@ -66,8 +68,10 @@ public interface TMLPortWithSecurityInformation {
public void setMappingName(String _mappingName);
public void setSecName(String _secName);
- public void setResultTrace(ProVerifResultTrace _trace);
- public void setPragmaString(String _info);
+ public void setResultTraces(List<ProVerifResultTrace> _traces);
+ public void addResultTrace(ProVerifResultTrace _trace);
+ public void setPragmasString(List<String> _infos);
+ public void addPragmaString(String _info);
public void setStrongAuthStatus(int _status);
public void setWeakAuthStatus(int _status);
diff --git a/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java b/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
index 36a905a06c..ab8eb376ce 100644
--- a/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
+++ b/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
@@ -68,7 +68,8 @@ public class TML2Avatar {
private int loopLimit = 1;
private HashMap<TMLChannel, Set<String>> channelsSecAttributes = new HashMap<TMLChannel, Set<String>>();
private HashMap<TMLChannel, Set<AvatarPragma>> secChannelMap = new HashMap<TMLChannel, Set<AvatarPragma>>();
- private Map<TMLWriteChannel, Set<AvatarPragma>> wrPragmaMap = new HashMap<TMLWriteChannel, Set<AvatarPragma>>();;
+ private Map<TMLWriteChannel, Set<AvatarPragma>> confPragmaMap = new HashMap<TMLWriteChannel, Set<AvatarPragma>>();;
+ private Map<TMLActivityElement, Set<AvatarPragma>> authPragmaMap = new HashMap<TMLActivityElement, Set<AvatarPragma>>();;
private HashMap<String, List<AvatarAttributeState>> signalAuthOriginMap = new HashMap<String, List<AvatarAttributeState>>();
private HashMap<String, List<AvatarAttributeState>> signalAuthDestMap = new HashMap<String, List<AvatarAttributeState>>();
private List<AvatarSignal> signals = new ArrayList<AvatarSignal>();
@@ -1304,40 +1305,38 @@ public class TML2Avatar {
if (ae.getSecurityPattern() != null) {
//If nonce
if (ae.getSecurityPattern().getType().equals(SecurityPattern.NONCE_PATTERN)) {
- channelData = new AvatarAttribute(ae.getSecurityPattern().getName(), AvatarType.INTEGER, block, null);
+ String attributeName = setNewAttributeName(ae.getSecurityPattern().getName(), block);
+ channelData = new AvatarAttribute(attributeName, AvatarType.INTEGER, block, null);
block.addAttribute(channelData);
- as.addValue(channelData.getName());
}
//Send the encrypted key
else if (!ae.getSecurityPattern().getKey().isEmpty()) {
- channelData = new AvatarAttribute("encryptedKey_" + ae.getSecurityPattern().getKey(), AvatarType.INTEGER, block, null);
- as.addValue(channelData.getName());
+ String attributeName = setNewAttributeName("encryptedKey_" + ae.getSecurityPattern().getKey(), block);
+ channelData = new AvatarAttribute(attributeName, AvatarType.INTEGER, block, null);
block.addAttribute(channelData);
} else {
//Send the encrypted data
- channelData = new AvatarAttribute(ae.getSecurityPattern().getName() + "_encrypted", AvatarType.INTEGER, block, null);
+ String attributeName = setNewAttributeName(ae.getSecurityPattern().getName() + "_encrypted", block);
+ channelData = new AvatarAttribute(attributeName, AvatarType.INTEGER, block, null);
if (!channelsSecAttributes.containsKey(ch)) {
Set<String> tmp = new HashSet<String>();
channelsSecAttributes.put(ch, tmp);
}
channelsSecAttributes.get(ch).add(channelData.getName());
channelsSecAttributes.get(ch).add(ae.getSecurityPattern().getName());
- as.addValue(channelData.getName());
block.addAttribute(channelData);
}
} else {
- channelData = new AvatarAttribute(getName(ch.getName()) + "_chData", AvatarType.INTEGER, block, null);
+ String attributeName = setNewAttributeName(getName(ch.getName()) + "_chData", block);
+ channelData = new AvatarAttribute(attributeName, AvatarType.INTEGER, block, null);
if (!channelsSecAttributes.containsKey(ch)) {
Set<String> tmp = new HashSet<String>();
channelsSecAttributes.put(ch, tmp);
}
channelsSecAttributes.get(ch).add(channelData.getName());
- if (block.getAvatarAttributeWithName(channelData.getName()) == null) {
- block.addAttribute(channelData);
- }
- as.addValue(channelData.getName());
+ block.addAttribute(channelData);
}
-
+ as.addValue(channelData.getName());
tran = new AvatarTransition(block, "__after_" + ae.getName(), ae.getReferenceObject());
elementList.add(signalState);
signalState.addNext(signalTran);
@@ -1414,32 +1413,29 @@ public class TML2Avatar {
if (ae.getSecurityPattern() != null) {
//send nonce
if (ae.getSecurityPattern().getType().equals(SecurityPattern.NONCE_PATTERN)) {
- channelData = new AvatarAttribute(ae.getSecurityPattern().getName(), AvatarType.INTEGER, block, null);
+ String attributeName = setNewAttributeName(ae.getSecurityPattern().getName(), block);
+ channelData = new AvatarAttribute(attributeName, AvatarType.INTEGER, block, null);
block.addAttribute(channelData);
- as.addValue(channelData.getName());
}
//send encrypted key
else if (!ae.getSecurityPattern().getKey().isEmpty()) {
- channelData = new AvatarAttribute("encryptedKey_" + ae.getSecurityPattern().getKey(), AvatarType.INTEGER, block, null);
- as.addValue(channelData.getName());
+ String attributeName = setNewAttributeName("encryptedKey_" + ae.getSecurityPattern().getKey(), block);
+ channelData = new AvatarAttribute(attributeName, AvatarType.INTEGER, block, null);
block.addAttribute(channelData);
} else {
//send encrypted data
- //
- channelData = new AvatarAttribute(ae.getSecurityPattern().getName() + "_encrypted", AvatarType.INTEGER, block, null);
- as.addValue(channelData.getName());
+ String attributeName = setNewAttributeName(ae.getSecurityPattern().getName() + "_encrypted", block);
+ channelData = new AvatarAttribute(attributeName, AvatarType.INTEGER, block, null);
block.addAttribute(channelData);
}
} else {
//No security pattern
// TraceManager.addDev("no security pattern for " + ch.getName());
- channelData = new AvatarAttribute(getName(ch.getName()) + "_chData", AvatarType.INTEGER, block, null);
-
- if (block.getAvatarAttributeWithName(channelData.getName()) == null) {
- block.addAttribute(channelData);
- }
- as.addValue(channelData.getName());
+ String attributeName = setNewAttributeName(getName(ch.getName()) + "_chData", block);
+ channelData = new AvatarAttribute(attributeName, AvatarType.INTEGER, block, null);
+ block.addAttribute(channelData);
}
+ as.addValue(channelData.getName());
//Add the confidentiality pragma for this channel data
if (ch.checkConf) {
if (ch.originalOriginTasks.size() != 0 && ch.getOriginPort().getName().contains("PORTORIGIN")) {
@@ -1456,22 +1452,22 @@ public class TML2Avatar {
Set<AvatarPragma> tmp = new HashSet<AvatarPragma>();
secChannelMap.put(ch, tmp);
}
+ if (!confPragmaMap.containsKey((TMLWriteChannel) ae)) {
+ Set<AvatarPragma> tmp = new HashSet<AvatarPragma>();
+ confPragmaMap.put((TMLWriteChannel) ae, tmp);
+ }
boolean isAvSecretInSet = false;
for (AvatarPragma av : secChannelMap.get(ch)) {
if (av.getName().equals(avPragmaSecret.getName())) {
isAvSecretInSet = true;
+ confPragmaMap.get((TMLWriteChannel) ae).add(av);
break;
}
}
if (!isAvSecretInSet) {
secChannelMap.get(ch).add(avPragmaSecret);
+ confPragmaMap.get((TMLWriteChannel) ae).add(avPragmaSecret);
}
-
- if (!wrPragmaMap.containsKey((TMLWriteChannel) ae)) {
- Set<AvatarPragma> tmp = new HashSet<AvatarPragma>();
- wrPragmaMap.put((TMLWriteChannel) ae, tmp);
- }
- wrPragmaMap.get((TMLWriteChannel) ae).add(avPragmaSecret);
}
}
}
@@ -1485,22 +1481,22 @@ public class TML2Avatar {
Set<AvatarPragma> tmp = new HashSet<AvatarPragma>();
secChannelMap.put(ch, tmp);
}
+ if (!confPragmaMap.containsKey((TMLWriteChannel) ae)) {
+ Set<AvatarPragma> tmp = new HashSet<AvatarPragma>();
+ confPragmaMap.put((TMLWriteChannel) ae, tmp);
+ }
boolean isAvSecretInSet = false;
for (AvatarPragma av : secChannelMap.get(ch)) {
if (av.getName().equals(avPragmaSecret.getName())) {
isAvSecretInSet = true;
+ confPragmaMap.get((TMLWriteChannel) ae).add(av);
break;
}
}
if (!isAvSecretInSet) {
secChannelMap.get(ch).add(avPragmaSecret);
+ confPragmaMap.get((TMLWriteChannel) ae).add(avPragmaSecret);
}
-
- if (!wrPragmaMap.containsKey((TMLWriteChannel) ae)) {
- Set<AvatarPragma> tmp = new HashSet<AvatarPragma>();
- wrPragmaMap.put((TMLWriteChannel) ae, tmp);
- }
- wrPragmaMap.get((TMLWriteChannel) ae).add(avPragmaSecret);
}
}
}
@@ -2146,11 +2142,11 @@ public class TML2Avatar {
secChannelMap.get(ch).add(secPatternPragmaMap.get(secPattern));
}
- if (!wrPragmaMap.containsKey(wc)) {
+ if (!confPragmaMap.containsKey(wc)) {
Set<AvatarPragma> tmp = new HashSet<AvatarPragma>();
- wrPragmaMap.put(wc, tmp);
+ confPragmaMap.put(wc, tmp);
}
- wrPragmaMap.get(wc).add(secPatternPragmaMap.get(secPattern));
+ confPragmaMap.get(wc).add(secPatternPragmaMap.get(secPattern));
}
}
}
@@ -2184,6 +2180,23 @@ public class TML2Avatar {
if (!isAvSecretInSet) {
secChannelMap.get(ch).add(pragma);
}
+ for (TMLTask task : tmlmodel.getTasks()) {
+ if (ch.hasDestinationTask(task) && ch.isCheckAuthChannel()) {
+ for (TMLActivityElement actElem : task.getActivityDiagram().getElements()) {
+ if (actElem instanceof TMLReadChannel) {
+ TMLReadChannel rd = (TMLReadChannel) actElem;
+ if (rd.hasChannel(ch) && actElem.getSecurityPattern() == null
+ && channelsSecAttributes.get(ch).contains(attributeStateOrigin.getAttribute().getName())) {
+ if (!authPragmaMap.containsKey(rd)) {
+ Set<AvatarPragma> tmp = new HashSet<AvatarPragma>();
+ authPragmaMap.put(rd, tmp);
+ }
+ authPragmaMap.get(rd).add(pragma);
+ }
+ }
+ }
+ }
+ }
}
}
for (SecurityPattern sec : secPatterns) {
@@ -2205,6 +2218,23 @@ public class TML2Avatar {
if (!isAvSecretInSet) {
secChannelMap.get(chSec).add(pragma);
}
+ for (TMLTask task : tmlmodel.getTasks()) {
+ if (chSec.hasDestinationTask(task)) {
+ for (TMLActivityElement actElem : task.getActivityDiagram().getElements()) {
+ if (actElem instanceof TMLExecC) {
+ TMLExecC dec = (TMLExecC) actElem;
+ if (dec.getSecurityPattern() != null && dec.isDecryptionProcess()
+ && channelsSecAttributes.get(chSec).contains(sec.getName())) {
+ if (!authPragmaMap.containsKey(dec)) {
+ Set<AvatarPragma> tmp = new HashSet<AvatarPragma>();
+ authPragmaMap.put(dec, tmp);
+ }
+ authPragmaMap.get(dec).add(pragma);
+ }
+ }
+ }
+ }
+ }
}
}
}
@@ -2644,7 +2674,8 @@ public class TML2Avatar {
}
tmlmap.getTMLModeling().setSecChannelMap(secChannelMap);
- tmlmap.getTMLModeling().setWrPragmaMap(wrPragmaMap);
+ tmlmap.getTMLModeling().setConfPragmaMap(confPragmaMap);
+ tmlmap.getTMLModeling().setAuthPragmaMap(authPragmaMap);
// System.out.println("avatar spec\n" +avspec);
return avspec;
@@ -2674,67 +2705,6 @@ public class TML2Avatar {
}
}
- public void backtraceAuthenticityADReadChannels(ProVerifOutputAnalyzer pvoa, String mappingName) {
- Map<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> authenticityResults = pvoa.getAuthenticityResults();
- for (AvatarPragmaAuthenticity pragma : authenticityResults.keySet()) {
- ProVerifQueryAuthResult result = authenticityResults.get(pragma);
- if (!result.isProved() || !result.isWeakProved())
- continue;
- int resWeakAuthStatus = 1;
- int resStrongAuthStatus = 1;
- if (result.isWeakProved()) {
- resWeakAuthStatus = result.isWeakSatisfied() ? 2 : 3;
- }
-
- if (result.isProved()) {
- resStrongAuthStatus = result.isSatisfied() ? 2 : 3;
- }
-
- if (pragma.getAttrB().getReferenceObject()!= null && pragma.getAttrB().getReferenceObject() instanceof SecurityBacktracer) {
- SecurityBacktracer rc = (SecurityBacktracer) pragma.getAttrB().getReferenceObject();
- TMLChannel channel = tmlmodel.getChannelByShortName(rc.getCommunicationName());
- if (channel != null) {
- rc.setAuthCheck(channel.checkAuth);
- }
- if (rc.getWeakAuthStatus() < 3) {
- rc.setWeakAuthStatus(resWeakAuthStatus);
- if (rc.getStrongAuthStatus() < 3) {
- rc.setStrongAuthStatus(resStrongAuthStatus);
- }
- }
- }
-
- if (pragma.getAttrB().getReferenceObject()!= null && pragma.getAttrB().getReferenceObject() instanceof SecurityDecryptor) {
- SecurityDecryptor dec = (SecurityDecryptor) pragma.getAttrB().getReferenceObject();
- for (TMLTask t : taskBlockMap.keySet()) {
- if (taskBlockMap.get(t).equals(pragma.getAttrB().getAttribute().getBlock())) {
- chDestinationTask:
- for (TMLChannel ch : tmlmodel.getChannels(t)) {
- if (ch.hasDestinationTask(t)) {
- for (TMLActivityElement actElem : t.getActivityDiagram().getElements()) {
- if (actElem instanceof TMLReadChannel) {
- TMLReadChannel rc = (TMLReadChannel) actElem;
- if (rc.hasChannel(ch) && actElem.getSecurityPattern() != null
- && actElem.getSecurityPattern().getName().equals(dec.getSecurityContext())) {
- dec.setAuthCheck(ch.checkAuth);
- break chDestinationTask;
- }
- }
- }
- }
- }
- }
- }
- if (dec.getWeakAuthStatus() < 3) {
- dec.setWeakAuthStatus(resWeakAuthStatus);
- if (dec.getStrongAuthStatus() < 3) {
- dec.setStrongAuthStatus(resStrongAuthStatus);
- }
- }
- }
- }
- }
-
public void distributeKeys() {
List<TMLTask> tasks = tmlmap.getTMLModeling().getTasks();
for (TMLTask t : accessKeys.keySet()) {
@@ -2856,6 +2826,15 @@ public class TML2Avatar {
ret = ret.replaceAll("-", "");
return ret;
}
+ private String setNewAttributeName(String _attributeName, AvatarBlock _block) {
+ String newAttributeName = _attributeName;
+ int indexAttribute = 0;
+ while (_block.getAvatarAttributeWithName(newAttributeName) != null) {
+ newAttributeName = _attributeName + indexAttribute;
+ indexAttribute += 1;
+ }
+ return newAttributeName;
+ }
/* public static boolean isInteger(String string) {
if(string == null || string.equals("")) {
diff --git a/src/main/java/ui/MainGUI.java b/src/main/java/ui/MainGUI.java
index babada70ea..e7e43c8b74 100644
--- a/src/main/java/ui/MainGUI.java
+++ b/src/main/java/ui/MainGUI.java
@@ -4878,7 +4878,6 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Per
getCurrentTDiagramPanel().clearAuthenticityBacktracing();
gtm.getTMLMapping().getTMLModeling().backtraceConfidentiality(pvoa, getTabName(tp));
gtm.getTML2Avatar().backtraceReachability(pvoa.getReachabilityResults());
- gtm.getTML2Avatar().backtraceAuthenticityADReadChannels(pvoa, getTabName(tp));
gtm.getTMLMapping().getTMLModeling().backtraceAuthenticity(pvoa, getTabName(tp));
}
@@ -4889,7 +4888,6 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Per
getCurrentTDiagramPanel().clearAuthenticityBacktracing();
gtm.getTMLMapping().getTMLModeling().backtraceConfidentiality(pvoa, "Default Mapping");
gtm.getTML2Avatar().backtraceReachability(pvoa.getReachabilityResults());
- gtm.getTML2Avatar().backtraceAuthenticityADReadChannels(pvoa, "Default Mapping");
gtm.getTMLMapping().getTMLModeling().backtraceAuthenticity(pvoa, "Default Mapping");
}
}
diff --git a/src/main/java/ui/TDiagramPanel.java b/src/main/java/ui/TDiagramPanel.java
index 6a97c456eb..8f38d869b0 100644
--- a/src/main/java/ui/TDiagramPanel.java
+++ b/src/main/java/ui/TDiagramPanel.java
@@ -80,6 +80,7 @@ import ui.syscams.SysCAMSClock;
import ui.syscams.SysCAMSCompositeComponent;
import ui.tmlad.TMLADDecrypt;
import ui.tmlad.TMLADReadChannel;
+import ui.tmlad.TMLADWriteChannel;
import ui.tmlcd.TMLTaskOperator;
import ui.tmlcompd.*;
import ui.window.JDialogCode;
@@ -2042,6 +2043,12 @@ public abstract class TDiagramPanel extends JPanel implements GenericTree {
((AvatarBDBlock) componentPopup).showTrace(currentY);
} else if (componentPopup instanceof AvatarBDPragma) {
((AvatarBDPragma) componentPopup).showTrace(currentY);
+ } else if (componentPopup instanceof TMLADReadChannel) {
+ ((TMLADReadChannel) componentPopup).showTrace();
+ } else if (componentPopup instanceof TMLADWriteChannel) {
+ ((TMLADWriteChannel) componentPopup).showTrace();
+ } else if (componentPopup instanceof TMLADDecrypt) {
+ ((TMLADDecrypt) componentPopup).showTrace();
}
}
@@ -2325,8 +2332,30 @@ public abstract class TDiagramPanel extends JPanel implements GenericTree {
gotoReference.setEnabled(false);
}
+ boolean enableShowProVerifTrace = false;
+ if (componentPointed instanceof TMLCPrimitivePort) {
+ if (((TMLCPrimitivePort) componentPointed).getCheckWeakAuthStatus() == 3 ||
+ ((TMLCPrimitivePort) componentPointed).getCheckStrongAuthStatus() == 3 ||
+ ((TMLCPrimitivePort) componentPointed).getConfStatus() == 3 ) {
+ enableShowProVerifTrace = true;
+ }
+ } else if (componentPointed instanceof TMLADDecrypt) {
+ if (((TMLADDecrypt) componentPointed).getWeakAuthStatus() == 3 ||
+ ((TMLADDecrypt) componentPointed).getStrongAuthStatus() == 3) {
+ enableShowProVerifTrace = true;
+ }
+ } else if (componentPointed instanceof TMLADReadChannel) {
+ if (((TMLADReadChannel) componentPointed).getWeakAuthStatus() == 3 ||
+ ((TMLADReadChannel) componentPointed).getStrongAuthStatus() == 3) {
+ enableShowProVerifTrace = true;
+ }
+ } else if (componentPointed instanceof TMLADWriteChannel) {
+ if (((TMLADWriteChannel) componentPointed).getConfStatus() == 3) {
+ enableShowProVerifTrace = true;
+ }
+ }
- if (componentPointed instanceof TMLCPrimitivePort || componentPointed instanceof AvatarBDBlock || componentPointed instanceof AvatarBDPragma) {
+ if (enableShowProVerifTrace || componentPointed instanceof AvatarBDBlock || componentPointed instanceof AvatarBDPragma) {
showProVerifTrace.setEnabled(true);
} else {
showProVerifTrace.setEnabled(false);
diff --git a/src/main/java/ui/avatarbd/AvatarBDBlock.java b/src/main/java/ui/avatarbd/AvatarBDBlock.java
index e48df683b3..2681098a15 100644
--- a/src/main/java/ui/avatarbd/AvatarBDBlock.java
+++ b/src/main/java/ui/avatarbd/AvatarBDBlock.java
@@ -436,7 +436,7 @@ public class AvatarBDBlock extends TGCScalableWithInternalComponent implements S
PipedInputStream pis = new PipedInputStream(pos, 4096);
BufferedWriter bw = new BufferedWriter(new OutputStreamWriter(pos));
- JFrameSimulationSDPanel jfssdp = new JFrameSimulationSDPanel(null, tdp.getMGUI(), "Confidentiality " + attr.toString());
+ JFrameSimulationSDPanel jfssdp = new JFrameSimulationSDPanel("Confidentiality " + attr.toString());
jfssdp.setIconImage(IconManager.img8);
GraphicLib.centerOnParent(jfssdp, 600, 600);
jfssdp.setFileReference(new BufferedReader(new InputStreamReader(pis)));
diff --git a/src/main/java/ui/avatarbd/AvatarBDInterface.java b/src/main/java/ui/avatarbd/AvatarBDInterface.java
index 0521ef9db9..5f4562716b 100644
--- a/src/main/java/ui/avatarbd/AvatarBDInterface.java
+++ b/src/main/java/ui/avatarbd/AvatarBDInterface.java
@@ -746,7 +746,7 @@ public class AvatarBDInterface extends TGCScalableWithInternalComponent implemen
PipedInputStream pis = new PipedInputStream(pos, 4096);
BufferedWriter bw = new BufferedWriter(new OutputStreamWriter(pos));
- JFrameSimulationSDPanel jfssdp = new JFrameSimulationSDPanel(null, tdp.getMGUI(), "Confidentiality " + attr.toString());
+ JFrameSimulationSDPanel jfssdp = new JFrameSimulationSDPanel("Confidentiality " + attr.toString());
jfssdp.setIconImage(IconManager.img8);
GraphicLib.centerOnParent(jfssdp, 600, 600);
jfssdp.setFileReference(new BufferedReader(new InputStreamReader(pis)));
diff --git a/src/main/java/ui/avatarbd/AvatarBDPragma.java b/src/main/java/ui/avatarbd/AvatarBDPragma.java
index 32eed053b6..a0973a4c56 100755
--- a/src/main/java/ui/avatarbd/AvatarBDPragma.java
+++ b/src/main/java/ui/avatarbd/AvatarBDPragma.java
@@ -494,7 +494,7 @@ public class AvatarBDPragma extends TGCScalableWithoutInternalComponent {
PipedInputStream pis = new PipedInputStream(pos, 4096);
BufferedWriter bw = new BufferedWriter(new OutputStreamWriter(pos));
- JFrameSimulationSDPanel jfssdp = new JFrameSimulationSDPanel(null, tdp.getMGUI(), pragma);
+ JFrameSimulationSDPanel jfssdp = new JFrameSimulationSDPanel(pragma);
jfssdp.setIconImage(IconManager.img8);
GraphicLib.centerOnParent(jfssdp, 600, 600);
jfssdp.setFileReference(new BufferedReader(new InputStreamReader(pis)));
diff --git a/src/main/java/ui/interactivesimulation/JFrameSimulationSDPanel.java b/src/main/java/ui/interactivesimulation/JFrameSimulationSDPanel.java
index fbff37e734..10d49887ad 100755
--- a/src/main/java/ui/interactivesimulation/JFrameSimulationSDPanel.java
+++ b/src/main/java/ui/interactivesimulation/JFrameSimulationSDPanel.java
@@ -41,6 +41,7 @@
package ui.interactivesimulation;
+import myutil.GraphicLib;
import myutil.TraceManager;
import ui.ColorManager;
import ui.MainGUI;
@@ -52,8 +53,10 @@ import java.awt.event.ActionListener;
import java.awt.event.ComponentAdapter;
import java.awt.event.ComponentEvent;
import java.io.BufferedReader;
+import java.util.ArrayList;
+import java.util.List;
+
-
/**
* Class JFrameSimulationSDPanel
* Creation: 26/05/2011
@@ -68,15 +71,18 @@ public class JFrameSimulationSDPanel extends JFrame implements ActionListener {
private static int[] clockDivisers = {1000000000, 1000000, 1000, 1};
protected JComboBox<String> units;
- private JSimulationSDPanel sdpanel;
+ private List<JSimulationSDPanel> sdpanels = new ArrayList<JSimulationSDPanel>();
protected JLabel status;
+ private int nbTraces;
+ private List<String> pragmas = new ArrayList<String>();
//, buttonStart, buttonStopAndClose;
//protected JTextArea jta;
//protected JScrollPane jsp;
- public JFrameSimulationSDPanel(Frame _f, MainGUI _mgui, String _title) {
+ public JFrameSimulationSDPanel(String _title, int _nbTraces, List<String> _pragmas) {
super(_title);
-
+ nbTraces = _nbTraces;
+ pragmas = _pragmas;
initActions();
makeComponents();
//setComponents();
@@ -84,11 +90,31 @@ public class JFrameSimulationSDPanel extends JFrame implements ActionListener {
@Override
public void componentResized(ComponentEvent e)
{
- if (JFrameSimulationSDPanel.this.sdpanel != null)
- JFrameSimulationSDPanel.this.sdpanel.resized();
+ for (JSimulationSDPanel sdpanel : sdpanels) {
+ if (sdpanel != null)
+ sdpanel.resized();
+ }
}
});
}
+
+ public JFrameSimulationSDPanel(String _title) {
+ super(_title);
+ nbTraces = 1;
+ initActions();
+ makeComponents();
+ //setComponents();
+ this.addComponentListener(new ComponentAdapter() {
+ @Override
+ public void componentResized(ComponentEvent e)
+ {
+ for (JSimulationSDPanel sdpanel : sdpanels) {
+ if (sdpanel != null)
+ sdpanel.resized();
+ }
+ }
+ });
+ }
private JLabel createStatusBar() {
status = new JLabel("Ready...");
@@ -114,14 +140,45 @@ public class JFrameSimulationSDPanel extends JFrame implements ActionListener {
JButton buttonRefresh = new JButton(actions[InteractiveSimulationActions.ACT_REFRESH]);
topPanel.add(buttonRefresh);
framePanel.add(topPanel, BorderLayout.NORTH);
-
// Simulation panel
- sdpanel = new JSimulationSDPanel(this);
- JScrollPane jsp = new JScrollPane(sdpanel, JScrollPane.VERTICAL_SCROLLBAR_ALWAYS, JScrollPane.HORIZONTAL_SCROLLBAR_ALWAYS);
- sdpanel.setMyScrollPanel(jsp);
- jsp.setWheelScrollingEnabled(true);
- jsp.getVerticalScrollBar().setUnitIncrement(MainGUI.INCREMENT);
- framePanel.add(jsp, BorderLayout.CENTER);
+ if (nbTraces == 1) {
+ JSimulationSDPanel sdpanel = new JSimulationSDPanel(this);
+ sdpanels.add(sdpanel);
+ JScrollPane jsp = new JScrollPane(sdpanel, JScrollPane.VERTICAL_SCROLLBAR_ALWAYS, JScrollPane.HORIZONTAL_SCROLLBAR_ALWAYS);
+ sdpanel.setMyScrollPanel(jsp);
+ jsp.setWheelScrollingEnabled(true);
+ jsp.getVerticalScrollBar().setUnitIncrement(MainGUI.INCREMENT);
+ framePanel.add(jsp, BorderLayout.CENTER);
+ } else {
+ JTabbedPane sdpanelsPane = GraphicLib.createTabbedPane();
+ for (int i = 0; i < nbTraces; i++) {
+ JSimulationSDPanel sdpanel = new JSimulationSDPanel(this);
+ sdpanels.add(sdpanel);
+ JPanel jp01 = new JPanel();
+ //GridBagLayout gridbag01 = new GridBagLayout();
+ //GridBagConstraints c01 = new GridBagConstraints();
+ //jp01.setLayout(gridbag01);
+ jp01.setBorder(new javax.swing.border.TitledBorder("Trace " + (i+1)));
+ /*c01.weighty = 1.0;
+ c01.weightx = 1.0;
+ c01.fill = GridBagConstraints.HORIZONTAL;
+ c01.gridheight = 1;
+ c01.gridwidth = 1;*/
+ JLabel labelPragmaName = new JLabel("Pragma: " + pragmas.get(i));
+ jp01.add(labelPragmaName, BorderLayout.NORTH);
+ //c01.gridwidth = GridBagConstraints.REMAINDER;
+
+ JScrollPane jsp = new JScrollPane(sdpanel, JScrollPane.VERTICAL_SCROLLBAR_ALWAYS, JScrollPane.HORIZONTAL_SCROLLBAR_ALWAYS);
+ sdpanel.setMyScrollPanel(jsp);
+ jsp.setWheelScrollingEnabled(true);
+ jsp.getVerticalScrollBar().setUnitIncrement(MainGUI.INCREMENT);
+ jp01.add(jsp, BorderLayout.CENTER);
+ sdpanelsPane.add("Trace " + (i+1), jp01);
+ }
+ framePanel.add(sdpanelsPane, BorderLayout.CENTER);
+ }
+
+
// statusBar
status = createStatusBar();
@@ -154,9 +211,11 @@ public class JFrameSimulationSDPanel extends JFrame implements ActionListener {
}
private void refresh() {
- if (sdpanel != null ){
- sdpanel.refresh();
- }
+ for (JSimulationSDPanel sdpanel : sdpanels) {
+ if (sdpanel != null ) {
+ sdpanel.refresh();
+ }
+ }
}
@@ -169,33 +228,35 @@ public class JFrameSimulationSDPanel extends JFrame implements ActionListener {
} else if (command.equals(actions[InteractiveSimulationActions.ACT_REFRESH].getActionCommand())) {
refresh();
} else if (evt.getSource() == units) {
- if (sdpanel != null) {
- switch(units.getSelectedIndex()) {
- case 0:
-
+ for (JSimulationSDPanel sdpanel : sdpanels) {
+ if (sdpanel != null) {
+ sdpanel.setClockDiviser(clockDivisers[units.getSelectedIndex()]);
}
- sdpanel.setClockDiviser(clockDivisers[units.getSelectedIndex()]);
}
}
}
-
- public void setFileReference(String _fileReference) {
- if (sdpanel != null) {
+
+ public void setFileReference(int index, String _fileReference) {
+ if (sdpanels.size() > index) {
//TraceManager.addDev("Setting file:" + _fileReference);
- sdpanel.setFileReference(_fileReference);
- } else {
- //TraceManager.addDev("Null SD Panel");
+ sdpanels.get(index).setFileReference(_fileReference);
}
}
- public void setFileReference(BufferedReader inputStream) {
- if (sdpanel != null) {
+ public void setFileReference(String _fileReference) {
+ setFileReference(0, _fileReference);
+ }
+
+ public void setFileReference(int index, BufferedReader inputStream) {
+ if (sdpanels.size() > index) {
//TraceManager.addDev("Setting input stream");
- sdpanel.setFileReference(inputStream);
- } else {
- //TraceManager.addDev("Null SD Panel");
+ sdpanels.get(index).setFileReference(inputStream);
}
}
+
+ public void setFileReference(BufferedReader inputStream) {
+ setFileReference(0, inputStream);
+ }
public void setCurrentTime(long timeValue) {
status.setText("time = " + timeValue);
@@ -209,7 +270,9 @@ public class JFrameSimulationSDPanel extends JFrame implements ActionListener {
status.setText("" + x + " transactions, min time=" + minTime + ", max time=" + maxTime);
}
public void setLimitEntity(boolean limit){
- sdpanel.setLimitEntity(limit);
+ for (JSimulationSDPanel sdpanel : sdpanels) {
+ sdpanel.setLimitEntity(limit);
+ }
}
diff --git a/src/main/java/ui/interactivesimulation/JSimulationSDPanel.java b/src/main/java/ui/interactivesimulation/JSimulationSDPanel.java
index bb4fc1f015..94c09d3f57 100644
--- a/src/main/java/ui/interactivesimulation/JSimulationSDPanel.java
+++ b/src/main/java/ui/interactivesimulation/JSimulationSDPanel.java
@@ -1022,10 +1022,12 @@ public class JSimulationSDPanel extends JPanel implements MouseMotionListener, R
}
private void updateInfoOnTransactions() {
- if (transactions.size() == 0) {
- jfssdp.setNbOfTransactions(transactions.size(), 0, 0);
- } else {
- jfssdp.setNbOfTransactions(transactions.size(), transactions.get(0).startingTime/clockDiviser, transactions.get(transactions.size()-1).finishTime/clockDiviser);
+ if (jfssdp != null) {
+ if (transactions.isEmpty()) {
+ jfssdp.setNbOfTransactions(0, 0, 0);
+ } else {
+ jfssdp.setNbOfTransactions(transactions.size(), transactions.get(0).startingTime/clockDiviser, transactions.get(transactions.size()-1).finishTime/clockDiviser);
+ }
}
}
diff --git a/src/main/java/ui/tmlad/TMLADDecrypt.java b/src/main/java/ui/tmlad/TMLADDecrypt.java
index 5cb393d12a..5388cdc62a 100755
--- a/src/main/java/ui/tmlad/TMLADDecrypt.java
+++ b/src/main/java/ui/tmlad/TMLADDecrypt.java
@@ -41,6 +41,7 @@ package ui.tmlad;
import java.awt.Color;
import java.awt.Graphics;
import java.awt.geom.Line2D;
+import java.io.*;
import java.util.ArrayList;
import java.util.List;
@@ -52,6 +53,8 @@ import org.w3c.dom.Node;
import org.w3c.dom.NodeList;
import myutil.GraphicLib;
+import proverifspec.ProVerifResultTrace;
+import proverifspec.ProVerifResultTraceStep;
import tmltranslator.SecurityDecryptor;
import ui.AllowedBreakpoint;
import ui.BasicErrorHighlight;
@@ -64,6 +67,7 @@ import ui.TGComponent;
import ui.TGComponentManager;
import ui.TGConnectingPoint;
import ui.ad.TADComponentWithoutSubcomponents;
+import ui.interactivesimulation.JFrameSimulationSDPanel;
import ui.util.IconManager;
import ui.window.JDialogMultiString;
@@ -96,6 +100,14 @@ public class TMLADDecrypt extends TADComponentWithoutSubcomponents/* Issue #69 T
protected int weakAuthStatus = 0;
protected int strongAuthStatus = 0;
+ private double authLockWidth;
+ private double authLockHeight;
+ private double xAuthLock;
+ private double yAuthLock;
+
+ private List<String> pragmas = new ArrayList<String>();
+ private List<ProVerifResultTrace> resTraces = new ArrayList<ProVerifResultTrace>();
+
public TMLADDecrypt(int _x, int _y, int _minX, int _maxX, int _minY, int _maxY, boolean _pos, TGComponent _father, TDiagramPanel _tdp) {
super(_x, _y, _minX, _maxX, _minY, _maxY, _pos, _father, _tdp);
@@ -208,6 +220,11 @@ public class TMLADDecrypt extends TADComponentWithoutSubcomponents/* Issue #69 T
return this;
}
+ if (authCheck && GraphicLib.isInRectangle(_x, _y, (int) xAuthLock, (int) (yAuthLock - authLockHeight), (int) authLockWidth,
+ (int) authLockHeight)) {
+ return this;
+ }
+
if ((int) (Line2D.ptSegDistSq(x + (width / 2), y - lineLength, x + (width / 2), y + lineLength + height, _x, _y)) < distanceSelected) {
return this;
}
@@ -269,15 +286,15 @@ public class TMLADDecrypt extends TADComponentWithoutSubcomponents/* Issue #69 T
double spacePortAuthLock = width * coeffSpacePortAuthLock;
double authOvalWidth = height * coeffAuthOval;
double authOvalHeight = height * coeffAuthOval;
- double authLockWidth = height * coeffAuthLock;
- double authLockHeight = height * coeffAuthLock;
- double xCoordinateAuthLockLeft = securityMaxX + spacePortAuthLock;
+ authLockWidth = height * coeffAuthLock;
+ authLockHeight = height * coeffAuthLock;
+ xAuthLock = securityMaxX + spacePortAuthLock;
double xCoordinateAuthLockRight = securityMaxX + authLockWidth + spacePortAuthLock;
double yCoordinateAuthLockTop = y + height - authLockHeight;
- double yCoordinateAuthLockBottom = y + height;
- double xCoordinateAuthLockCenter = xCoordinateAuthLockLeft + authLockWidth/2;
- double yCoordinateAuthLockCenter = yCoordinateAuthLockBottom - authLockHeight/2;
- double xCoordinateAuthOvalLeft = xCoordinateAuthLockLeft + (authLockWidth - authOvalWidth)/2;
+ yAuthLock = y + height;
+ double xCoordinateAuthLockCenter = xAuthLock + authLockWidth/2;
+ double yCoordinateAuthLockCenter = yAuthLock - authLockHeight/2;
+ double xCoordinateAuthOvalLeft = xAuthLock + (authLockWidth - authOvalWidth)/2;
double yCoordinateAuthOvalTop = yCoordinateAuthLockTop - authOvalHeight/2;
Color c = g.getColor();
Color c1;
@@ -306,10 +323,10 @@ public class TMLADDecrypt extends TADComponentWithoutSubcomponents/* Issue #69 T
g.drawOval((int) (xCoordinateAuthOvalLeft), (int) (yCoordinateAuthOvalTop), (int) (authOvalWidth), (int) (authOvalHeight));
g.setColor(c1);
- int[] xps = new int[]{(int) (xCoordinateAuthLockLeft), (int) (xCoordinateAuthLockLeft), (int) (xCoordinateAuthLockRight)};
- int[] yps = new int[]{(int) (yCoordinateAuthLockTop), (int) (yCoordinateAuthLockBottom), (int) (yCoordinateAuthLockBottom)};
- int[] xpw = new int[]{(int) (xCoordinateAuthLockRight), (int) (xCoordinateAuthLockRight), (int) (xCoordinateAuthLockLeft)};
- int[] ypw = new int[]{(int) (yCoordinateAuthLockBottom), (int) (yCoordinateAuthLockTop), (int) (yCoordinateAuthLockTop)};
+ int[] xps = new int[]{(int) (xAuthLock), (int) (xAuthLock), (int) (xCoordinateAuthLockRight)};
+ int[] yps = new int[]{(int) (yCoordinateAuthLockTop), (int) (yAuthLock), (int) (yAuthLock)};
+ int[] xpw = new int[]{(int) (xCoordinateAuthLockRight), (int) (xCoordinateAuthLockRight), (int) (xAuthLock)};
+ int[] ypw = new int[]{(int) (yAuthLock), (int) (yCoordinateAuthLockTop), (int) (yCoordinateAuthLockTop)};
g.fillPolygon(xps, yps, 3);
g.setColor(c2);
@@ -319,13 +336,14 @@ public class TMLADDecrypt extends TADComponentWithoutSubcomponents/* Issue #69 T
g.drawPolygon(xpw, ypw, 3);
drawSingleString(g, "S", (int) (securityMaxX + coeffXCoordinateOffsetDrawAuth * spacePortAuthLock),
(int) (y + coeffYCoordinateOffsetDrawAuth * height));
- drawSingleString(g, "W", (int) (xCoordinateAuthLockLeft + coeffYCoordinateOffsetDrawAuth * authLockWidth / 2),
- (int) (yCoordinateAuthLockBottom - coeffYCoordinateOffsetDrawAuth * authLockHeight / 2));
+ drawSingleString(g, "W", (int) (xAuthLock + coeffYCoordinateOffsetDrawAuth * authLockWidth / 2),
+ (int) (yAuthLock - coeffYCoordinateOffsetDrawAuth * authLockHeight / 2));
if (strongAuthStatus == 3) {
- g.drawLine((int) (xCoordinateAuthLockLeft), (int) (yCoordinateAuthLockBottom),
- (int) (xCoordinateAuthLockCenter), (int) (yCoordinateAuthLockCenter));
- g.drawLine((int) (xCoordinateAuthLockLeft), (int) (yCoordinateAuthLockCenter),
- (int) (xCoordinateAuthLockCenter), (int) (yCoordinateAuthLockBottom));
+ g.drawLine((int) (xAuthLock), (int) (yAuthLock),
+ (int) (xAuthLock + g.getFontMetrics().stringWidth("S")),
+ (int) (yAuthLock - g.getFontMetrics().getHeight() * 0.8));
+ g.drawLine((int) (xAuthLock), (int) (yAuthLock - g.getFontMetrics().getHeight() * 0.8),
+ (int) (xAuthLock + g.getFontMetrics().stringWidth("S")), (int) (yAuthLock));
}
if (weakAuthStatus == 3 || strongAuthStatus == 3 && weakAuthStatus < 2) {
g.drawLine((int) (xCoordinateAuthLockCenter), (int) (yCoordinateAuthLockCenter),
@@ -335,6 +353,42 @@ public class TMLADDecrypt extends TADComponentWithoutSubcomponents/* Issue #69 T
}
}
+ public void showTrace() {
+ //Show Result trace
+ if (resTraces.isEmpty()) {
+ return;
+ }
+ try {
+ String title = "Trace for authenticity property";
+ JFrameSimulationSDPanel jfssdp = new JFrameSimulationSDPanel(title, resTraces.size(), pragmas);
+ jfssdp.setIconImage(IconManager.img8);
+ GraphicLib.centerOnParent(jfssdp, 600, 600);
+ jfssdp.setVisible(true);
+ jfssdp.setLimitEntity(false);
+ jfssdp.toFront();
+
+ TraceManager.addDev("\n--- Trace ---");
+ int iTrace = 0;
+ for (ProVerifResultTrace resTrace : resTraces) {
+ PipedOutputStream pos = new PipedOutputStream();
+ int i = 0;
+ PipedInputStream pis = new PipedInputStream(pos, 4096);
+ BufferedWriter bw = new BufferedWriter(new OutputStreamWriter(pos));
+ jfssdp.setFileReference(iTrace, new BufferedReader(new InputStreamReader(pis)));
+ for (ProVerifResultTraceStep step : resTrace.getTrace()) {
+ TraceManager.addDev("\n--- Trace #" + i + ": " + step.toString());
+ step.describeAsTMLSDTransaction(bw, i);
+ i++;
+ }
+ bw.close();
+ iTrace++;
+ pos.close();
+ }
+ } catch (IOException e) {
+ TraceManager.addDev("Error when writing trace step SD transaction");
+ }
+ }
+
@Override
public int getType() {
return TGComponentManager.TMLAD_DECRYPT;
@@ -377,4 +431,14 @@ public class TMLADDecrypt extends TADComponentWithoutSubcomponents/* Issue #69 T
public String getSecurityContext() {
return securityContext;
}
+
+ @Override
+ public void setResultTraces(List<ProVerifResultTrace> traces) {
+ resTraces = traces;
+ }
+
+ @Override
+ public void setPragmasString(List<String> _pragmas) {
+ pragmas = _pragmas;
+ }
}
diff --git a/src/main/java/ui/tmlad/TMLADReadChannel.java b/src/main/java/ui/tmlad/TMLADReadChannel.java
index df74b53c7d..fe82dbcb34 100755
--- a/src/main/java/ui/tmlad/TMLADReadChannel.java
+++ b/src/main/java/ui/tmlad/TMLADReadChannel.java
@@ -41,6 +41,7 @@ package ui.tmlad;
import java.awt.Color;
import java.awt.Graphics;
import java.awt.geom.Line2D;
+import java.io.*;
import java.util.ArrayList;
import java.util.List;
import java.util.Map;
@@ -54,6 +55,8 @@ import org.w3c.dom.Node;
import org.w3c.dom.NodeList;
import myutil.GraphicLib;
+import proverifspec.ProVerifResultTrace;
+import proverifspec.ProVerifResultTraceStep;
import tmltranslator.SecurityBacktracer;
import tmltranslator.SecurityCheckable;
import ui.AllowedBreakpoint;
@@ -70,6 +73,7 @@ import ui.TGComponent;
import ui.TGComponentManager;
import ui.TGConnectingPoint;
import ui.ad.TADComponentWithoutSubcomponents;
+import ui.interactivesimulation.JFrameSimulationSDPanel;
import ui.util.IconManager;
import ui.window.JDialogMultiStringAndTabs;
import ui.window.TabInfo;
@@ -122,6 +126,14 @@ public class TMLADReadChannel extends TADComponentWithoutSubcomponents/* Issue #
protected int weakAuthStatus = 0;
protected int strongAuthStatus = 0;
+ private double authLockWidth;
+ private double authLockHeight;
+ private double xAuthLock;
+ private double yAuthLock;
+
+ private List<String> pragmas = new ArrayList<String>();
+ private List<ProVerifResultTrace> resTraces = new ArrayList<ProVerifResultTrace>();
+
public TMLADReadChannel(int _x, int _y, int _minX, int _maxX, int _minY, int _maxY, boolean _pos, TGComponent _father, TDiagramPanel _tdp) {
super(_x, _y, _minX, _maxX, _minY, _maxY, _pos, _father, _tdp);
@@ -225,7 +237,7 @@ public class TMLADReadChannel extends TADComponentWithoutSubcomponents/* Issue #
if (!tdp.isScaled()) {
//TraceManager.addDev("Size of \"" + ("sec:" + securityContext) +"\": " + g.getFontMetrics().stringWidth("sec:" +
// securityContext));
- securityMaxX = (int) (x + 3 * width / 4 + g.getFontMetrics().stringWidth("sec:" + securityContext) * 1.05);
+ securityMaxX = (int) (x + 3 * width / 4 + g.getFontMetrics().stringWidth("sec:" + securityContext) * 1.2);
}
g.setColor(c);
}
@@ -306,15 +318,15 @@ public class TMLADReadChannel extends TADComponentWithoutSubcomponents/* Issue #
double spacePortAuthLock = width * coeffSpacePortAuthLock;
double authOvalWidth = height * coeffAuthOval;
double authOvalHeight = height * coeffAuthOval;
- double authLockWidth = height * coeffAuthLock;
- double authLockHeight = height * coeffAuthLock;
- double xCoordinateAuthLockLeft = x + width + spacePortAuthLock;
+ authLockWidth = height * coeffAuthLock;
+ authLockHeight = height * coeffAuthLock;
+ xAuthLock = x + width + spacePortAuthLock;
double xCoordinateAuthLockRight = x + width + authLockWidth + spacePortAuthLock;
double yCoordinateAuthLockTop = y + height - authLockHeight;
- double yCoordinateAuthLockBottom = y + height;
- double xCoordinateAuthLockCenter = xCoordinateAuthLockLeft + authLockWidth/2;
- double yCoordinateAuthLockCenter = yCoordinateAuthLockBottom - authLockHeight/2;
- double xCoordinateAuthOvalLeft = xCoordinateAuthLockLeft + (authLockWidth - authOvalWidth)/2;
+ yAuthLock = y + height;
+ double xCoordinateAuthLockCenter = xAuthLock + authLockWidth/2;
+ double yCoordinateAuthLockCenter = yAuthLock - authLockHeight/2;
+ double xCoordinateAuthOvalLeft = xAuthLock + (authLockWidth - authOvalWidth)/2;
double yCoordinateAuthOvalTop = yCoordinateAuthLockTop - authOvalHeight/2;
Color c = g.getColor();
@@ -343,10 +355,10 @@ public class TMLADReadChannel extends TADComponentWithoutSubcomponents/* Issue #
g.drawOval((int) (xCoordinateAuthOvalLeft), (int) (yCoordinateAuthOvalTop), (int) (authOvalWidth), (int) (authOvalHeight));
g.setColor(c1);
- int[] xps = new int[]{(int) (xCoordinateAuthLockLeft), (int) (xCoordinateAuthLockLeft), (int) (xCoordinateAuthLockRight)};
- int[] yps = new int[]{(int) (yCoordinateAuthLockTop), (int) (yCoordinateAuthLockBottom), (int) (yCoordinateAuthLockBottom)};
- int[] xpw = new int[]{(int) (xCoordinateAuthLockRight), (int) (xCoordinateAuthLockRight), (int) (xCoordinateAuthLockLeft)};
- int[] ypw = new int[]{(int) (yCoordinateAuthLockBottom), (int) (yCoordinateAuthLockTop), (int) (yCoordinateAuthLockTop)};
+ int[] xps = new int[]{(int) (xAuthLock), (int) (xAuthLock), (int) (xCoordinateAuthLockRight)};
+ int[] yps = new int[]{(int) (yCoordinateAuthLockTop), (int) (yAuthLock), (int) (yAuthLock)};
+ int[] xpw = new int[]{(int) (xCoordinateAuthLockRight), (int) (xCoordinateAuthLockRight), (int) (xAuthLock)};
+ int[] ypw = new int[]{(int) (yAuthLock), (int) (yCoordinateAuthLockTop), (int) (yCoordinateAuthLockTop)};
g.fillPolygon(xps, yps, 3);
g.setColor(c2);
@@ -354,14 +366,15 @@ public class TMLADReadChannel extends TADComponentWithoutSubcomponents/* Issue #
g.setColor(c);
g.drawPolygon(xps, yps, 3);
g.drawPolygon(xpw, ypw, 3);
- drawSingleString(g, "S", (int) (xCoordinateAuthLockLeft), (int) (y + coeffYCoordinateOffsetDrawAuth*height));
- drawSingleString(g, "W", (int) (xCoordinateAuthLockLeft + coeffXCoordinateOffsetDrawAuth * authLockWidth / 2),
- (int) (yCoordinateAuthLockBottom - coeffYCoordinateOffsetDrawAuth * authLockHeight / 2));
+ drawSingleString(g, "S", (int) (xAuthLock), (int) (y + coeffYCoordinateOffsetDrawAuth*height));
+ drawSingleString(g, "W", (int) (xAuthLock + coeffXCoordinateOffsetDrawAuth * authLockWidth / 2),
+ (int) (yAuthLock - coeffYCoordinateOffsetDrawAuth * authLockHeight / 2));
if (strongAuthStatus == 3) {
- g.drawLine((int) (xCoordinateAuthLockLeft), (int) (yCoordinateAuthLockBottom),
- (int) (xCoordinateAuthLockCenter), (int) (yCoordinateAuthLockCenter));
- g.drawLine((int) (xCoordinateAuthLockLeft), (int) (yCoordinateAuthLockCenter),
- (int) (xCoordinateAuthLockCenter), (int) (yCoordinateAuthLockBottom));
+ g.drawLine((int) (xAuthLock), (int) (yAuthLock),
+ (int) (xAuthLock + g.getFontMetrics().stringWidth("S")),
+ (int) (yAuthLock - g.getFontMetrics().getHeight() * 0.8));
+ g.drawLine((int) (xAuthLock), (int) (yAuthLock - g.getFontMetrics().getHeight() * 0.8),
+ (int) (xAuthLock + g.getFontMetrics().stringWidth("S")), (int) (yAuthLock));
}
if (weakAuthStatus == 3 || strongAuthStatus == 3 && weakAuthStatus < 2) {
g.drawLine((int) (xCoordinateAuthLockCenter), (int) (yCoordinateAuthLockCenter),
@@ -371,12 +384,53 @@ public class TMLADReadChannel extends TADComponentWithoutSubcomponents/* Issue #
}
}
+ public void showTrace() {
+ //Show Result trace
+ if (resTraces.isEmpty()) {
+ return;
+ }
+ try {
+ String title = "Trace for authenticity property";
+ JFrameSimulationSDPanel jfssdp = new JFrameSimulationSDPanel(title, resTraces.size(), pragmas);
+ jfssdp.setIconImage(IconManager.img8);
+ GraphicLib.centerOnParent(jfssdp, 600, 600);
+ jfssdp.setVisible(true);
+ jfssdp.setLimitEntity(false);
+ jfssdp.toFront();
+
+ TraceManager.addDev("\n--- Trace ---");
+ int iTrace = 0;
+ for (ProVerifResultTrace resTrace : resTraces) {
+ PipedOutputStream pos = new PipedOutputStream();
+ int i = 0;
+ PipedInputStream pis = new PipedInputStream(pos, 4096);
+ BufferedWriter bw = new BufferedWriter(new OutputStreamWriter(pos));
+ jfssdp.setFileReference(iTrace, new BufferedReader(new InputStreamReader(pis)));
+ for (ProVerifResultTraceStep step : resTrace.getTrace()) {
+ TraceManager.addDev("\n--- Trace #" + i + ": " + step.toString());
+ step.describeAsTMLSDTransaction(bw, i);
+ i++;
+ }
+ bw.close();
+ iTrace++;
+ pos.close();
+ }
+ } catch (IOException e) {
+ TraceManager.addDev("Error when writing trace step SD transaction");
+ }
+ }
+
@Override
public TGComponent isOnMe(int _x, int _y) {
if (GraphicLib.isInRectangle(_x, _y, x, y, width, height)) {
return this;
}
+ if (authCheck && GraphicLib.isInRectangle(_x, _y, (int) xAuthLock, (int) (yAuthLock - authLockHeight), (int) authLockWidth,
+ (int) authLockHeight)) {
+ return this;
+ }
+
if ((int) (Line2D.ptSegDistSq(x + (width / 2), y - lineLength, x + (width / 2), y + lineLength + height, _x, _y)) < distanceSelected) {
return this;
}
@@ -431,7 +485,14 @@ public class TMLADReadChannel extends TADComponentWithoutSubcomponents/* Issue #
// values[2] = isEncForm ? "Yes" : "No";
help = new ArrayList<String[]>();
String[] choice = new String[]{"Yes", "No"};
- help.add(tdp.getMGUI().getCurrentCryptoConfig());
+ String[] secContext = new String[tdp.getMGUI().getCurrentCryptoConfig().length + 1];
+ secContext[0] = "None";
+ int indexSecContext = 1;
+ for (String sp : tdp.getMGUI().getCurrentCryptoConfig()) {
+ secContext[indexSecContext] = sp;
+ indexSecContext += 1;
+ }
+ help.add(secContext);
help.add(choice);
help.add(choice);
tab2.labels=labels;
@@ -452,7 +513,12 @@ public class TMLADReadChannel extends TADComponentWithoutSubcomponents/* Issue #
if (jdmsat.hasBeenSet() && (jdmsat.hasValidString(0))) {
channelName = jdmsat.getString(0, 0);
nbOfSamples = jdmsat.getString(0, 1);
- securityContext = jdmsat.getString(1, 0);
+ int indexSecurityContextText = jdmsat.getIndexSelectedItem(1, 0);
+ if (indexSecurityContextText == 0) {
+ securityContext = "";
+ } else {
+ securityContext = jdmsat.getString(1, 0);
+ }
isAttacker = jdmsat.getString(1, 1).equals("Yes");
// isEncForm = jdmsat.getString(1, 2).equals("Yes");
makeValue();
@@ -614,7 +680,18 @@ public class TMLADReadChannel extends TADComponentWithoutSubcomponents/* Issue #
}
+ @Override
+ public void setResultTraces(List<ProVerifResultTrace> traces) {
+ resTraces = traces;
+ }
+
+ @Override
+ public void setPragmasString(List<String> _pragmas) {
+ pragmas = _pragmas;
+ }
+
public String getCommunicationName() {
return channelName;
}
+
}
diff --git a/src/main/java/ui/tmlad/TMLADWriteChannel.java b/src/main/java/ui/tmlad/TMLADWriteChannel.java
index d2785468ef..f4dbe2dcb8 100755
--- a/src/main/java/ui/tmlad/TMLADWriteChannel.java
+++ b/src/main/java/ui/tmlad/TMLADWriteChannel.java
@@ -41,6 +41,7 @@ package ui.tmlad;
import java.awt.Color;
import java.awt.Graphics;
import java.awt.geom.Line2D;
+import java.io.*;
import java.util.ArrayList;
import java.util.List;
import java.util.Map;
@@ -55,6 +56,8 @@ import org.w3c.dom.NodeList;
import myutil.Conversion;
import myutil.GraphicLib;
+import proverifspec.ProVerifResultTrace;
+import proverifspec.ProVerifResultTraceStep;
import tmltranslator.SecurityBacktracer;
import tmltranslator.SecurityCheckable;
import ui.AllowedBreakpoint;
@@ -71,6 +74,7 @@ import ui.TGComponent;
import ui.TGComponentManager;
import ui.TGConnectingPoint;
import ui.ad.TADComponentWithoutSubcomponents;
+import ui.interactivesimulation.JFrameSimulationSDPanel;
import ui.util.IconManager;
import ui.window.JDialogMultiStringAndTabs;
import ui.window.TabInfo;
@@ -119,6 +123,15 @@ public class TMLADWriteChannel extends TADComponentWithoutSubcomponents/* Issue
private boolean confCheck;
private int confStatus;
+ //Confidentiality lock parameters
+ private double confLockWidth;
+ private double confLockHeight;
+ private double xConfLock;
+ private double yConfLock;
+
+ private List<String> pragmas = new ArrayList<String>();
+ private List<ProVerifResultTrace> resTraces = new ArrayList<ProVerifResultTrace>();
+
public TMLADWriteChannel(int _x, int _y, int _minX, int _maxX, int _minY, int _maxY, boolean _pos, TGComponent _father, TDiagramPanel _tdp) {
super(_x, _y, _minX, _maxX, _minY, _maxY, _pos, _father, _tdp);
@@ -291,15 +304,15 @@ public class TMLADWriteChannel extends TADComponentWithoutSubcomponents/* Issue
final double coeffConfOval = 0.8;
//final double coeffYCoordinateOffsetDrawConf = 1.01;
double spacePortConfLock = width * coeffSpacePortConfLock;
- double confLockWidth = height * coeffConfLock;
- double confLockHeight = height * coeffConfLock;
+ confLockWidth = height * coeffConfLock;
+ confLockHeight = height * coeffConfLock;
double confOvalWidth = height * coeffConfOval;
double confOvalHeight = height * coeffConfOval;
- double xCoordinateConfLockLeft = x + width + spacePortConfLock;
+ xConfLock = x + width + spacePortConfLock;
double xCoordinateConfLockRight = x + width + confLockWidth + spacePortConfLock;
double yCoordinateConfLockTop = y + height - confLockHeight;
- double yCoordinateConfLockBottom = y + height;
- double xCoordinateConfOvalLeft = xCoordinateConfLockLeft + (confLockWidth - confOvalWidth)/2;
+ yConfLock = y + height;
+ double xCoordinateConfOvalLeft = xConfLock + (confLockWidth - confOvalWidth)/2;
double yCoordinateConfOvalTop = yCoordinateConfLockTop - confOvalHeight/2;
Color c = g.getColor();
@@ -319,14 +332,14 @@ public class TMLADWriteChannel extends TADComponentWithoutSubcomponents/* Issue
}
g.drawOval((int) (xCoordinateConfOvalLeft), (int) (yCoordinateConfOvalTop), (int)confOvalWidth, (int)confOvalHeight);
g.setColor(c1);
- g.fillRect((int) (xCoordinateConfLockLeft), (int) (yCoordinateConfLockTop), (int)confLockWidth, (int)confLockHeight);
+ g.fillRect((int) (xConfLock), (int) (yCoordinateConfLockTop), (int)confLockWidth, (int)confLockHeight);
g.setColor(c);
- g.drawRect((int) (xCoordinateConfLockLeft), (int) (yCoordinateConfLockTop), (int)confLockWidth, (int)confLockHeight);
+ g.drawRect((int) (xConfLock), (int) (yCoordinateConfLockTop), (int)confLockWidth, (int)confLockHeight);
if (confStatus == 3) {
- g.drawLine((int) (xCoordinateConfLockLeft), (int) (yCoordinateConfLockTop),
- (int) (xCoordinateConfLockRight), (int) (yCoordinateConfLockBottom));
+ g.drawLine((int) (xConfLock), (int) (yCoordinateConfLockTop),
+ (int) (xCoordinateConfLockRight), (int) (yConfLock));
g.drawLine((int) (xCoordinateConfLockRight), (int) (yCoordinateConfLockTop),
- (int) (xCoordinateConfLockLeft), (int) (yCoordinateConfLockBottom));
+ (int) (xConfLock), (int) (yConfLock));
}
}
@@ -336,6 +349,10 @@ public class TMLADWriteChannel extends TADComponentWithoutSubcomponents/* Issue
return this;
}
+ if (confCheck && GraphicLib.isInRectangle(_x, _y, (int) xConfLock, (int) (yConfLock - confLockHeight), (int) confLockWidth,
+ (int) confLockHeight)) {
+ return this;
+ }
if ((int) (Line2D.ptSegDistSq(x + (width / 2), y - lineLength, x + (width / 2), y + lineLength + height, _x, _y)) < distanceSelected) {
return this;
}
@@ -370,6 +387,42 @@ public class TMLADWriteChannel extends TADComponentWithoutSubcomponents/* Issue
return value;
}
+ public void showTrace() {
+ //Show Result trace
+ if (resTraces.isEmpty()) {
+ return;
+ }
+ try {
+ String title = "Trace for confidentiality property";
+ JFrameSimulationSDPanel jfssdp = new JFrameSimulationSDPanel(title, resTraces.size(), pragmas);
+ jfssdp.setIconImage(IconManager.img8);
+ GraphicLib.centerOnParent(jfssdp, 600, 600);
+ jfssdp.setVisible(true);
+ jfssdp.setLimitEntity(false);
+ jfssdp.toFront();
+
+ TraceManager.addDev("\n--- Trace ---");
+ int iTrace = 0;
+ for (ProVerifResultTrace resTrace : resTraces) {
+ PipedOutputStream pos = new PipedOutputStream();
+ int i = 0;
+ PipedInputStream pis = new PipedInputStream(pos, 4096);
+ BufferedWriter bw = new BufferedWriter(new OutputStreamWriter(pos));
+ jfssdp.setFileReference(iTrace, new BufferedReader(new InputStreamReader(pis)));
+ for (ProVerifResultTraceStep step : resTrace.getTrace()) {
+ TraceManager.addDev("\n--- Trace #" + i + ": " + step.toString());
+ step.describeAsTMLSDTransaction(bw, i);
+ i++;
+ }
+ bw.close();
+ iTrace++;
+ pos.close();
+ }
+ } catch (IOException e) {
+ TraceManager.addDev("Error when writing trace step SD transaction");
+ }
+ }
+
@Override
public boolean editOnDoubleClick(JFrame frame) {
TabInfo tab1 = new TabInfo("Name and samples");
@@ -409,8 +462,14 @@ public class TMLADWriteChannel extends TADComponentWithoutSubcomponents/* Issue
// labels[2] = "Encrypted Form?";
// values[2] = isEncForm ? "Yes" : "No";
help = new ArrayList<String[]>();
-
- help.add(tdp.getMGUI().getCurrentCryptoConfig());
+ String[] secContext = new String[tdp.getMGUI().getCurrentCryptoConfig().length + 1];
+ secContext[0] = "None";
+ int indexSecContext = 1;
+ for (String sp : tdp.getMGUI().getCurrentCryptoConfig()) {
+ secContext[indexSecContext] = sp;
+ indexSecContext += 1;
+ }
+ help.add(secContext);
help.add(choice);
help.add(choice);
tab2.labels=labels;
@@ -432,7 +491,12 @@ public class TMLADWriteChannel extends TADComponentWithoutSubcomponents/* Issue
if (jdmsat.hasBeenSet() && (jdmsat.hasValidString(0))) {
channelName = jdmsat.getString(0, 0);
nbOfSamples = jdmsat.getString(0, 1);
- securityContext = jdmsat.getString(1, 0);
+ int indexSecurityContextText = jdmsat.getIndexSelectedItem(1, 0);
+ if (indexSecurityContextText == 0) {
+ securityContext = "";
+ } else {
+ securityContext = jdmsat.getString(1, 0);
+ }
isAttacker = jdmsat.getString(1, 1).equals("Yes");
// isEncForm = jdmsat.getString(1, 2).equals("Yes");
makeValue();
@@ -609,4 +673,14 @@ public class TMLADWriteChannel extends TADComponentWithoutSubcomponents/* Issue
public void setStrongAuthStatus(int _strongAuthStatus) {
}
+
+ @Override
+ public void setResultTraces(List<ProVerifResultTrace> traces) {
+ resTraces = traces;
+ }
+
+ @Override
+ public void setPragmasString(List<String> _pragmas) {
+ pragmas = _pragmas;
+ }
}
diff --git a/src/main/java/ui/tmlcompd/TMLCChannelOutPort.java b/src/main/java/ui/tmlcompd/TMLCChannelOutPort.java
index be40949c5d..c5a1b9f126 100755
--- a/src/main/java/ui/tmlcompd/TMLCChannelOutPort.java
+++ b/src/main/java/ui/tmlcompd/TMLCChannelOutPort.java
@@ -41,6 +41,7 @@
package ui.tmlcompd;
+import proverifspec.ProVerifResultTrace;
import ui.TDiagramPanel;
import ui.TGComponent;
import ui.TGComponentManager;
@@ -73,5 +74,5 @@ public class TMLCChannelOutPort extends TMLCPrimitivePort {
public int getType() {
return TGComponentManager.TMLCTD_COPORT;
}
-
+
}
diff --git a/src/main/java/ui/tmlcompd/TMLCPrimitivePort.java b/src/main/java/ui/tmlcompd/TMLCPrimitivePort.java
index 2daa623388..7396879050 100755
--- a/src/main/java/ui/tmlcompd/TMLCPrimitivePort.java
+++ b/src/main/java/ui/tmlcompd/TMLCPrimitivePort.java
@@ -59,6 +59,8 @@
import javax.swing.*;
import java.awt.*;
import java.io.*;
+ import java.util.ArrayList;
+ import java.util.List;
import java.util.Vector;
/**
@@ -116,21 +118,16 @@
protected boolean isBlocking = true;
protected int oldTypep = typep;
- //Authenticity lock parameters
- protected int authlockwidth = (int) (16 * tdp.getZoom());
- protected int authlockheight = (int) (16 * tdp.getZoom());
- protected int xc = (int) (18 * tdp.getZoom());
- protected int yc = (int) (12 * tdp.getZoom());
- protected int authxoffset = (int) (20 * tdp.getZoom());
- protected int authyoffset = (int) (18 * tdp.getZoom());
- protected int authovalwidth = (int) (10 * tdp.getZoom());
- protected int authovalheight = (int) (15 * tdp.getZoom());
- //Confidentiality lock parameters
- protected int conflockwidth = (int) (9 * tdp.getZoom());
- protected int conflockheight = (int) (7 * tdp.getZoom());
- protected int confyoffset = 3 * conflockheight;
- protected int confovalwidth = (int) (6 * tdp.getZoom());
- protected int confovalheight = (int) (9 * tdp.getZoom());
+ //Authenticity and Confidentiality lock parameters
+ private double authLockWidth;
+ private double authLockHeight;
+ private double confLockWidth;
+ private double confLockHeight;
+ private double xConfLock;
+ private double yConfLock;
+ private double xAuthLock;
+ private double yAuthLock;
+
protected boolean isLossy;
protected boolean isPostex = false;
protected boolean isPrex = false;
@@ -147,9 +144,8 @@
// Network
protected int vc = 0;
//ProVerifTrace
- String pragma;
- ProVerifResultTrace resTrace;
-
+ private List<String> pragmas = new ArrayList<String>();
+ private List<ProVerifResultTrace> resTraces = new ArrayList<ProVerifResultTrace>();
public TMLCPrimitivePort(int _x, int _y, int _minX, int _maxX, int _minY, int _maxY, boolean _pos, TGComponent _father, TDiagramPanel _tdp) {
super(_x, _y, _minX, _maxX, _minY, _maxY, _pos, _father, _tdp);
@@ -374,20 +370,20 @@
final double coeffAuthOval = 0.6;
final double coeffAuthLock = 0.7;
final double coeffOffsetSecName = 0.7;
- final double coeffXCoordinateOffsetDrawAuth = 0.8;
+ final double coeffXCoordinateOffsetDrawAuth = 0.775;
final double coeffYCoordinateOffsetDrawAuth = 0.95;
double spacePortAuthLock = width * coeffSpacePortAuthLock;
double authOvalWidth = width * coeffAuthOval;
double authOvalHeight = height * coeffAuthOval;
- double authLockWidth = width * coeffAuthLock;
- double authLockHeight = height * coeffAuthLock;
- double xCoordinateAuthLockLeft = x + width + spacePortAuthLock;
+ authLockWidth = width * coeffAuthLock;
+ authLockHeight = height * coeffAuthLock;
+ xAuthLock = x + width + spacePortAuthLock;
double xCoordinateAuthLockRight = x + width + authLockWidth + spacePortAuthLock;
double yCoordinateAuthLockTop = y + height - authLockHeight;
- double yCoordinateAuthLockBottom = y + height;
- double xCoordinateAuthLockCenter = xCoordinateAuthLockLeft + authLockWidth/2;
- double yCoordinateAuthLockCenter = yCoordinateAuthLockBottom - authLockHeight/2;
- double xCoordinateAuthOvalLeft = xCoordinateAuthLockLeft + (authLockWidth - authOvalWidth)/2;
+ yAuthLock = y + height;
+ double xCoordinateAuthLockCenter = xAuthLock + authLockWidth/2;
+ double yCoordinateAuthLockCenter = yAuthLock - authLockHeight/2;
+ double xCoordinateAuthOvalLeft = xAuthLock + (authLockWidth - authOvalWidth)/2;
double yCoordinateAuthOvalTop = yCoordinateAuthLockTop - authOvalHeight/2;
Color c = g.getColor();
Color c1;
@@ -412,14 +408,14 @@
default:
c2 = c1;
}
- drawSingleString(g, secName, (int) (xCoordinateAuthLockLeft), (int) (yCoordinateAuthLockBottom + coeffOffsetSecName*authLockHeight));
+ drawSingleString(g, secName, (int) (xAuthLock), (int) (yAuthLock + coeffOffsetSecName*authLockHeight));
g.drawOval((int) (xCoordinateAuthOvalLeft), (int) (yCoordinateAuthOvalTop), (int) (authOvalWidth), (int) (authOvalHeight));
g.setColor(c1);
- int[] xps = new int[]{(int) (xCoordinateAuthLockLeft), (int) (xCoordinateAuthLockLeft), (int) (xCoordinateAuthLockRight)};
- int[] yps = new int[]{(int) (yCoordinateAuthLockTop), (int) (yCoordinateAuthLockBottom), (int) (yCoordinateAuthLockBottom)};
- int[] xpw = new int[]{(int) (xCoordinateAuthLockRight), (int) (xCoordinateAuthLockRight), (int) (xCoordinateAuthLockLeft)};
- int[] ypw = new int[]{(int) (yCoordinateAuthLockBottom), (int) (yCoordinateAuthLockTop), (int) (yCoordinateAuthLockTop)};
+ int[] xps = new int[]{(int) (xAuthLock), (int) (xAuthLock), (int) (xCoordinateAuthLockRight)};
+ int[] yps = new int[]{(int) (yCoordinateAuthLockTop), (int) (yAuthLock), (int) (yAuthLock)};
+ int[] xpw = new int[]{(int) (xCoordinateAuthLockRight), (int) (xCoordinateAuthLockRight), (int) (xAuthLock)};
+ int[] ypw = new int[]{(int) (yAuthLock), (int) (yCoordinateAuthLockTop), (int) (yCoordinateAuthLockTop)};
g.fillPolygon(xps, yps, 3);
g.setColor(c2);
@@ -427,14 +423,15 @@
g.setColor(c);
g.drawPolygon(xps, yps, 3);
g.drawPolygon(xpw, ypw, 3);
- drawSingleString(g, "S", (int) (xCoordinateAuthLockLeft), (int) (y + coeffYCoordinateOffsetDrawAuth * height));
- drawSingleString(g, "W", (int) (xCoordinateAuthLockLeft + coeffXCoordinateOffsetDrawAuth * authLockWidth / 2),
- (int) (yCoordinateAuthLockBottom - coeffYCoordinateOffsetDrawAuth * authLockHeight / 2));
+ drawSingleString(g, "S", (int) (xAuthLock), (int) (y + coeffYCoordinateOffsetDrawAuth * height));
+ drawSingleString(g, "W", (int) (xAuthLock + coeffXCoordinateOffsetDrawAuth * authLockWidth / 2),
+ (int) (yAuthLock - coeffYCoordinateOffsetDrawAuth * authLockHeight / 2));
if (checkStrongAuthStatus == 3) {
- g.drawLine((int) (xCoordinateAuthLockLeft), (int) (yCoordinateAuthLockBottom),
- (int) (xCoordinateAuthLockCenter), (int) (yCoordinateAuthLockCenter));
- g.drawLine((int) (xCoordinateAuthLockLeft), (int) (yCoordinateAuthLockCenter),
- (int) (xCoordinateAuthLockCenter), (int) (yCoordinateAuthLockBottom));
+ g.drawLine((int) (xAuthLock), (int) (yAuthLock),
+ (int) (xAuthLock + g.getFontMetrics().stringWidth("S")),
+ (int) (yAuthLock - g.getFontMetrics().getHeight() * 0.8));
+ g.drawLine((int) (xAuthLock), (int) (yAuthLock - g.getFontMetrics().getHeight() * 0.8),
+ (int) (xAuthLock + g.getFontMetrics().stringWidth("S")), (int) (yAuthLock));
}
if (checkWeakAuthStatus == 3 || checkStrongAuthStatus == 3 && checkWeakAuthStatus < 2) {
g.drawLine((int) (xCoordinateAuthLockCenter), (int) (yCoordinateAuthLockCenter),
@@ -451,14 +448,14 @@
final double coeffConfOval = 0.4;
final double coeffYCoordinateOffsetDrawConf = 1.01;
double spacePortConfLock = width * coeffSpacePortConfLock;
- double confLockWidth = width * coeffConfLock;
- double confLockHeight = height * coeffConfLock;
+ confLockWidth = width * coeffConfLock;
+ confLockHeight = height * coeffConfLock;
double confOvalWidth = width * coeffConfOval;
double confOvalHeight = height * coeffConfOval;
- double xCoordinateConfLockLeft = x - confLockWidth - spacePortConfLock;
+ xConfLock = x - confLockWidth - spacePortConfLock;
double xCoordinateConfLockRight = x - spacePortConfLock;
double yCoordinateConfLockTop = y + height - confLockHeight;
- double yCoordinateConfLockBottom = y + height;
+ yConfLock = y + height;
double xCoordinateConfOvalLeft = xCoordinateConfLockRight - (confOvalWidth/2) - (confLockWidth/2);
double yCoordinateConfOvalTop = yCoordinateConfLockTop - confOvalHeight/2;
@@ -478,18 +475,18 @@
return;
}
- drawSingleString(g, mappingName, (int) (xCoordinateConfLockLeft),
- (int) (yCoordinateConfLockBottom + coeffYCoordinateOffsetDrawConf * confLockHeight));
+ drawSingleString(g, mappingName, (int) (xConfLock),
+ (int) (yConfLock + coeffYCoordinateOffsetDrawConf * confLockHeight));
g.drawOval((int) (xCoordinateConfOvalLeft), (int) (yCoordinateConfOvalTop), (int)confOvalWidth, (int)confOvalHeight);
g.setColor(c1);
- g.fillRect((int) (xCoordinateConfLockLeft), (int) (yCoordinateConfLockTop), (int)confLockWidth, (int)confLockHeight);
+ g.fillRect((int) (xConfLock), (int) (yCoordinateConfLockTop), (int)confLockWidth, (int)confLockHeight);
g.setColor(c);
- g.drawRect((int) (xCoordinateConfLockLeft), (int) (yCoordinateConfLockTop), (int)confLockWidth, (int)confLockHeight);
+ g.drawRect((int) (xConfLock), (int) (yCoordinateConfLockTop), (int)confLockWidth, (int)confLockHeight);
if (checkConfStatus == 3) {
- g.drawLine((int) (xCoordinateConfLockLeft), (int) (yCoordinateConfLockTop),
- (int) (xCoordinateConfLockRight), (int) (yCoordinateConfLockBottom));
+ g.drawLine((int) (xConfLock), (int) (yCoordinateConfLockTop),
+ (int) (xCoordinateConfLockRight), (int) (yConfLock));
g.drawLine((int) (xCoordinateConfLockRight), (int) (yCoordinateConfLockTop),
- (int) (xCoordinateConfLockLeft), (int) (yCoordinateConfLockBottom));
+ (int) (xConfLock), (int) (yConfLock));
}
if (!secName.equals("")) {
@@ -506,13 +503,13 @@
default:
return;
}
- drawSingleString(g, mappingName, (int) (xCoordinateConfLockLeft),
- (int) (yCoordinateConfLockBottom + coeffYCoordinateOffsetDrawConf * confLockHeight));
+ drawSingleString(g, mappingName, (int) (xConfLock),
+ (int) (yConfLock + coeffYCoordinateOffsetDrawConf * confLockHeight));
g.drawOval((int) (xCoordinateConfOvalLeft), (int) (yCoordinateConfOvalTop), (int)confOvalWidth, (int)confOvalHeight);
g.setColor(c1);
- g.fillRect((int) (xCoordinateConfLockLeft), (int) (yCoordinateConfLockTop), (int)confLockWidth, (int)confLockHeight);
+ g.fillRect((int) (xConfLock), (int) (yCoordinateConfLockTop), (int)confLockWidth, (int)confLockHeight);
g.setColor(c);
- g.drawRect((int) (xCoordinateConfLockLeft), (int) (yCoordinateConfLockTop), (int)confLockWidth, (int)confLockHeight);
+ g.drawRect((int) (xConfLock), (int) (yCoordinateConfLockTop), (int)confLockWidth, (int)confLockHeight);
}
}
@@ -569,9 +566,13 @@
public TGComponent isOnOnlyMe(int _x, int _y) {
if (GraphicLib.isInRectangle(_x, _y, x, y, width, height)) {
return this;
- } else if (checkAuth && !isOrigin && GraphicLib.isInRectangle(_x, _y, x - authxoffset, y, authxoffset, authlockheight)) {
+ } else if (checkAuth && !isOrigin && GraphicLib.isInRectangle(_x, _y, (int) xAuthLock, (int) (yAuthLock - authLockHeight),
+ (int) authLockWidth,
+ (int) authLockHeight)) {
return this;
- } else if (checkConf && isOrigin && GraphicLib.isInRectangle(_x, _y, x - conflockwidth * 3 / 2, y, conflockwidth * 3 / 2, height)) {
+ } else if (checkConf && isOrigin && GraphicLib.isInRectangle(_x, _y, (int) xConfLock, (int) (yConfLock - confLockHeight),
+ (int) confLockWidth,
+ (int) confLockHeight)) {
return this;
}
return null;
@@ -735,23 +736,21 @@
public void showTrace() {
//Show Result trace
- if (resTrace == null) {
+ if (resTraces.isEmpty()) {
return;
}
- PipedOutputStream pos = new PipedOutputStream();
try {
- PipedInputStream pis = new PipedInputStream(pos, 4096);
- BufferedWriter bw = new BufferedWriter(new OutputStreamWriter(pos));
+
String title = "";
if (isOrigin) {
- title = "Trace for confidentiality property of ";
+ title = "Trace for confidentiality property";
} else {
- title = "Trace for authenticity property of ";
+ title = "Trace for authenticity property";
}
- JFrameSimulationSDPanel jfssdp = new JFrameSimulationSDPanel(null, tdp.getMGUI(), title + pragma);
+ JFrameSimulationSDPanel jfssdp = new JFrameSimulationSDPanel(title, resTraces.size(), pragmas);
jfssdp.setIconImage(IconManager.img8);
GraphicLib.centerOnParent(jfssdp, 600, 600);
- jfssdp.setFileReference(new BufferedReader(new InputStreamReader(pis)));
+
jfssdp.setVisible(true);
jfssdp.setLimitEntity(false);
//jfssdp.setModalExclusionType(ModalExclusionType
@@ -759,20 +758,24 @@
jfssdp.toFront();
TraceManager.addDev("\n--- Trace ---");
- int i = 0;
- for (ProVerifResultTraceStep step : resTrace.getTrace()) {
- TraceManager.addDev("\n--- Trace #" + i + ": " + step.toString());
- step.describeAsTMLSDTransaction(bw, i);
- i++;
+ int iTrace = 0;
+ for (ProVerifResultTrace resTrace : resTraces) {
+ PipedOutputStream pos = new PipedOutputStream();
+ int i = 0;
+ PipedInputStream pis = new PipedInputStream(pos, 4096);
+ BufferedWriter bw = new BufferedWriter(new OutputStreamWriter(pos));
+ jfssdp.setFileReference(iTrace, new BufferedReader(new InputStreamReader(pis)));
+ for (ProVerifResultTraceStep step : resTrace.getTrace()) {
+ TraceManager.addDev("\n--- Trace #" + i + ": " + step.toString());
+ step.describeAsTMLSDTransaction(bw, i);
+ i++;
+ }
+ bw.close();
+ iTrace++;
+ pos.close();
}
- bw.close();
} catch (IOException e) {
TraceManager.addDev("Error when writing trace step SD transaction");
- } finally {
- try {
- pos.close();
- } catch (IOException ignored) {
- }
}
}
@@ -1246,12 +1249,20 @@
return true;
}
- public void setResultTrace(ProVerifResultTrace trace) {
- resTrace = trace;
+ public void setResultTraces(List<ProVerifResultTrace> traces) {
+ resTraces = traces;
+ }
+
+ public void addResultTrace(ProVerifResultTrace trace) {
+ resTraces.add(trace);
+ }
+
+ public void setPragmasString(List<String> _pragmas) {
+ pragmas = _pragmas;
}
- public void setPragmaString(String str) {
- pragma = str;
+ public void addPragmaString(String pragma) {
+ pragmas.add(pragma);
}
//#issue 82
diff --git a/src/main/java/ui/window/JDialogAvatarExecutableCodeGeneration.java b/src/main/java/ui/window/JDialogAvatarExecutableCodeGeneration.java
index 7a5ce78827..4787e25602 100644
--- a/src/main/java/ui/window/JDialogAvatarExecutableCodeGeneration.java
+++ b/src/main/java/ui/window/JDialogAvatarExecutableCodeGeneration.java
@@ -1086,7 +1086,7 @@ public class JDialogAvatarExecutableCodeGeneration extends javax.swing.JFrame im
}
public void showSimulationTrace() {
- JFrameSimulationSDPanel jfssdp = new JFrameSimulationSDPanel(f, mgui, "Simulation trace of " + simulationTraceFile.getText());
+ JFrameSimulationSDPanel jfssdp = new JFrameSimulationSDPanel("Simulation trace of " + simulationTraceFile.getText());
jfssdp.setLimitEntity(false);
jfssdp.setIconImage(IconManager.img8);
// jfssdp.setSize(600, 600);
diff --git a/src/main/java/ui/window/JDialogAvatarddExecutableCodeGeneration.java b/src/main/java/ui/window/JDialogAvatarddExecutableCodeGeneration.java
index 5a43bcdd4c..4e96b04f21 100644
--- a/src/main/java/ui/window/JDialogAvatarddExecutableCodeGeneration.java
+++ b/src/main/java/ui/window/JDialogAvatarddExecutableCodeGeneration.java
@@ -786,7 +786,7 @@ topCellGenerator.saveFile(pathCode,listsyscamspanel); // DG 13.12.2019
}
public void showSimulationTrace() {
- JFrameSimulationSDPanel jfssdp = new JFrameSimulationSDPanel(f, mgui, "Simulation trace of " + simulationTraceFile.getText());
+ JFrameSimulationSDPanel jfssdp = new JFrameSimulationSDPanel("Simulation trace of " + simulationTraceFile.getText());
jfssdp.setIconImage(IconManager.img8);
// jfssdp.setSize(600, 600);
GraphicLib.centerOnParent(jfssdp, 600, 600);
diff --git a/src/main/java/ui/window/JDialogMultiString.java b/src/main/java/ui/window/JDialogMultiString.java
index 2cd5041ade..0c306b9b7d 100644
--- a/src/main/java/ui/window/JDialogMultiString.java
+++ b/src/main/java/ui/window/JDialogMultiString.java
@@ -262,6 +262,10 @@ public class JDialogMultiString extends JDialogBase implements ActionListener {
return texts[i].getText();
}
+ public int getIndexSelectedItem(int i) {
+ return helps.get(i).getSelectedIndex();
+ }
+
public boolean hasValidString(int i) {
return texts[i].getText().length() > 0;
}
diff --git a/src/main/java/ui/window/JDialogMultiStringAndTabs.java b/src/main/java/ui/window/JDialogMultiStringAndTabs.java
index fccb43545f..277c28aa6d 100644
--- a/src/main/java/ui/window/JDialogMultiStringAndTabs.java
+++ b/src/main/java/ui/window/JDialogMultiStringAndTabs.java
@@ -266,6 +266,12 @@ public class JDialogMultiStringAndTabs extends JDialogBase implements ActionList
return texts[index].getText();
}
+ public int getIndexSelectedItem(int tabIndex, int indexInTab) {
+ // Compute index of box
+ int index = getIndex(tabIndex, indexInTab);
+ return helps.get(index).getSelectedIndex();
+ }
+
public boolean hasValidString(int i) {
return texts[i].getText().length() > 0;
}
diff --git a/src/main/java/ui/window/JDialogProverifVerification.java b/src/main/java/ui/window/JDialogProverifVerification.java
index af4f9a1ced..5e930430eb 100644
--- a/src/main/java/ui/window/JDialogProverifVerification.java
+++ b/src/main/java/ui/window/JDialogProverifVerification.java
@@ -1273,11 +1273,10 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
OutputStreamWriter(pos));
JFrameSimulationSDPanel jfssdp = new
- JFrameSimulationSDPanel(null, this.mgui, this
- .menuItem.pragma.toString());
+ JFrameSimulationSDPanel(this.menuItem.pragma.toString());
jfssdp.setIconImage(IconManager.img8);
GraphicLib.centerOnParent(jfssdp, 600, 600);
- jfssdp.setFileReference(new BufferedReader(new
+ jfssdp.setFileReference(0, new BufferedReader(new
InputStreamReader(pis)));
jfssdp.setVisible(true);
jfssdp.setModalExclusionType(ModalExclusionType
--
GitLab