diff --git a/src/main/java/tmltranslator/toavatar/TML2Avatar.java b/src/main/java/tmltranslator/toavatar/TML2Avatar.java
index f32e1404f4aee4910b653fba19620e7bcfa57580..cac9761a2308ad90b69ee9b3e26dbca7ed6c6143 100644
--- a/src/main/java/tmltranslator/toavatar/TML2Avatar.java
+++ b/src/main/java/tmltranslator/toavatar/TML2Avatar.java
@@ -94,7 +94,7 @@ public class TML2Avatar {
this.tmlmap = tmlmap;
this.tmlmodel = tmlmap.getTMLModeling();
-
+
allStates = new ArrayList<String>();
attrsToCheck = new ArrayList<String>();
@@ -1482,6 +1482,30 @@ public class TML2Avatar {
}
attrsToCheck.clear();
tmlmodel.removeForksAndJoins();
+
+ System.out.println("MODIFIED model " + tmlmodel);
+
+ for (TMLChannel chan: tmlmodel.getChannels()){
+ System.out.println("chan " + chan);
+ TMLTask task = chan.getOriginTask();
+
+ TMLTask task2 = chan.getDestinationTask();
+ HwExecutionNode node = (HwExecutionNode) tmlmap.getHwNodeOf(task);
+ HwExecutionNode node2 = (HwExecutionNode) tmlmap.getHwNodeOf(task2);
+ if (node==null){
+ tmlmap.addTaskToHwExecutionNode(task, node2);
+ }
+
+ if (node2==null){
+ tmlmap.addTaskToHwExecutionNode(task2, node);
+ }
+
+ if (chan.getName().contains("fork__") || chan.getName().contains("FORKCHANNEL")){
+ chan.setName(chan.getName().replaceAll("__",""));
+ }
+
+ }
+
//Only set the loop limit if it's a number
String pattern = "^[0-9]{1,2}$";
Pattern r = Pattern.compile(pattern);
diff --git a/src/main/java/ui/AvatarDesignPanel.java b/src/main/java/ui/AvatarDesignPanel.java
index f2e923013b2011e39438aee7aba9cbe4b8aa05d1..bda2bf683f547caa26274c4c42f347de70859238 100644
--- a/src/main/java/ui/AvatarDesignPanel.java
+++ b/src/main/java/ui/AvatarDesignPanel.java
@@ -45,11 +45,14 @@ import avatartranslator.AvatarAttribute;
import avatartranslator.AvatarPragmaAuthenticity;
import avatartranslator.AvatarPragmaReachability;
import avatartranslator.AvatarPragmaSecret;
+import avatartranslator.AvatarPragma;
import avatartranslator.AvatarPragmaLatency;
import myutil.GraphicLib;
import proverifspec.ProVerifOutputAnalyzer;
import proverifspec.ProVerifQueryAuthResult;
import proverifspec.ProVerifQueryResult;
+import proverifspec.ProVerifResultTrace;
+
import ui.avatarbd.*;
import ui.avatardd.ADDDiagramPanel;
import ui.avatarsmd.AvatarSMDPanel;
@@ -453,17 +456,17 @@ public class AvatarDesignPanel extends TURTLEPanel {
// Confidential attributes
Map<AvatarPragmaSecret, ProVerifQueryResult> confResults = pvoa.getConfidentialityResults();
- List<AvatarAttribute> secretAttributes = new LinkedList<AvatarAttribute> ();
- List<AvatarAttribute> nonSecretAttributes = new LinkedList<AvatarAttribute> ();
+ HashMap<AvatarAttribute, AvatarPragma> secretAttributes = new HashMap<AvatarAttribute, AvatarPragma> ();
+ HashMap<AvatarAttribute, AvatarPragma> nonSecretAttributes = new HashMap<AvatarAttribute, AvatarPragma> ();
for (AvatarPragmaSecret pragma: confResults.keySet())
{
ProVerifQueryResult result = confResults.get(pragma);
if (result.isProved())
{
if (result.isSatisfied())
- secretAttributes.add(pragma.getArg());
+ secretAttributes.put(pragma.getArg(), pragma);
else
- nonSecretAttributes.add(pragma.getArg());
+ nonSecretAttributes.put(pragma.getArg(),pragma);
}
}
@@ -474,15 +477,23 @@ public class AvatarDesignPanel extends TURTLEPanel {
int toBeFound = types.size ();
boolean ko = false;
for (TAttribute type: types) {
- for(AvatarAttribute attribute: secretAttributes)
+ for(AvatarAttribute attribute: secretAttributes.keySet())
if (attribute.getBlock ().getName ().equals (bdBlock.getBlockName ()) && attribute.getName ().equals (tattr.getId () + "__" + type.getId ())) {
toBeFound --;
+ ProVerifResultTrace trace = confResults.get(secretAttributes.get(attribute)).getTrace();
+ if (trace!=null){
+ bdBlock.addProVerifTrace(tattr, trace);
+ }
break;
}
- for(AvatarAttribute attribute: nonSecretAttributes)
+ for(AvatarAttribute attribute: nonSecretAttributes.keySet())
if (attribute.getBlock ().getName ().equals (bdBlock.getBlockName ()) && attribute.getName ().equals (tattr.getId () + "__" + type.getId ())) {
ko = true;
+ ProVerifResultTrace trace = confResults.get(nonSecretAttributes.get(attribute)).getTrace();
+ if (trace!=null){
+ bdBlock.addProVerifTrace(tattr, trace);
+ }
break;
}
@@ -490,17 +501,31 @@ public class AvatarDesignPanel extends TURTLEPanel {
break;
}
- if (ko)
+ if (ko){
tattr.setConfidentialityVerification(TAttribute.CONFIDENTIALITY_KO);
- else if (toBeFound == 0)
+
+ }
+ else if (toBeFound == 0) {
tattr.setConfidentialityVerification(TAttribute.CONFIDENTIALITY_OK);
+
+ }
} else {
- for(AvatarAttribute attribute: secretAttributes)
- if (attribute.getBlock ().getName ().equals (bdBlock.getBlockName ()) && attribute.getName ().equals (tattr.getId ()))
+ for(AvatarAttribute attribute: secretAttributes.keySet())
+ if (attribute.getBlock ().getName ().equals (bdBlock.getBlockName ()) && attribute.getName ().equals (tattr.getId ())){
tattr.setConfidentialityVerification(TAttribute.CONFIDENTIALITY_OK);
- for(AvatarAttribute attribute: nonSecretAttributes)
- if (attribute.getBlock ().getName ().equals (bdBlock.getBlockName ()) && attribute.getName ().equals (tattr.getId ()))
+ ProVerifResultTrace trace = confResults.get(secretAttributes.get(attribute)).getTrace();
+ if (trace!=null){
+ bdBlock.addProVerifTrace(tattr, trace);
+ }
+ }
+ for(AvatarAttribute attribute: nonSecretAttributes.keySet())
+ if (attribute.getBlock ().getName ().equals (bdBlock.getBlockName ()) && attribute.getName ().equals (tattr.getId ())){
tattr.setConfidentialityVerification(TAttribute.CONFIDENTIALITY_KO);
+ ProVerifResultTrace trace = confResults.get(nonSecretAttributes.get(attribute)).getTrace();
+ if (trace!=null){
+ bdBlock.addProVerifTrace(tattr, trace);
+ }
+ }
}
}
@@ -565,7 +590,7 @@ public class AvatarDesignPanel extends TURTLEPanel {
boolean weakKo = false;
boolean isNotProved = false;
boolean weakIsNotProved = false;
-
+ ProVerifQueryAuthResult result= new ProVerifQueryAuthResult(false, false);
for (TAttribute type: types) {
for (AvatarPragmaAuthenticity pragmaAuth: authResults.keySet())
{
@@ -577,7 +602,7 @@ public class AvatarDesignPanel extends TURTLEPanel {
|| !pragmaAuth.getAttrB().getState().getName().equals(argB[1].replaceAll("\\.", "__")))
continue;
- ProVerifQueryAuthResult result = authResults.get(pragmaAuth);
+ result = authResults.get(pragmaAuth);
toBeFound --;
if (result.isProved())
@@ -625,7 +650,10 @@ public class AvatarDesignPanel extends TURTLEPanel {
else
pragma.authWeakMap.put(prop, 1);
}
-
+ ProVerifResultTrace trace = result.getTrace();
+ if (trace!=null){
+ pragma.pragmaTraceMap.put(prop, trace);
+ }
} else {
for (AvatarPragmaAuthenticity pragmaAuth: authResults.keySet())
{
@@ -670,7 +698,11 @@ public class AvatarDesignPanel extends TURTLEPanel {
{
pragma.authWeakMap.put(prop, 3);
}
-
+ //Add ProVerif Result Trace to pragma
+ ProVerifResultTrace trace = pvoa.getResults().get(pragmaAuth).getTrace();
+ if (trace!=null){
+ pragma.pragmaTraceMap.put(prop, trace);
+ }
break;
}
}
diff --git a/src/main/java/ui/TDiagramPanel.java b/src/main/java/ui/TDiagramPanel.java
index 832e888d50e956156512b804a51da518c11c4968..28e5a9e262515122baa22f8cc3651a5f5c60b4c7 100755
--- a/src/main/java/ui/TDiagramPanel.java
+++ b/src/main/java/ui/TDiagramPanel.java
@@ -44,6 +44,7 @@ import ui.atd.ATDAttack;
import ui.atd.ATDBlock;
import ui.avatarad.AvatarADActivity;
import ui.avatarbd.AvatarBDBlock;
+import ui.avatarbd.AvatarBDPragma;
import ui.avatarbd.AvatarBDDataType;
import ui.avatarbd.AvatarBDLibraryFunction;
import ui.avatarcd.AvatarCDBlock;
@@ -1859,6 +1860,12 @@ public abstract class TDiagramPanel extends JPanel implements GenericTree {
if (componentPopup instanceof TMLCPrimitivePort){
((TMLCPrimitivePort) componentPopup).showTrace();
}
+ else if (componentPopup instanceof AvatarBDBlock){
+ ((AvatarBDBlock) componentPopup).showTrace(currentY);
+ }
+ else if (componentPopup instanceof AvatarBDPragma){
+ ((AvatarBDPragma) componentPopup).showTrace(currentY);
+ }
}
if (e.getSource() == checkMasterMutex) {
@@ -2114,11 +2121,12 @@ public abstract class TDiagramPanel extends JPanel implements GenericTree {
}
- if (componentPointed instanceof TMLCPrimitivePort){
+ if (componentPointed instanceof TMLCPrimitivePort || componentPointed instanceof AvatarBDBlock || componentPointed instanceof AvatarBDPragma){
showProVerifTrace.setEnabled(true);
} else {
showProVerifTrace.setEnabled(false);
}
+
if (componentPointed instanceof CheckableInvariant) {
diff --git a/src/main/java/ui/avatarbd/AvatarBDBlock.java b/src/main/java/ui/avatarbd/AvatarBDBlock.java
index 53d55718ebd963376ae567bfd322f5252ba80946..0cc3a230edd5af6f24c7f1090019c4680590bd83 100644
--- a/src/main/java/ui/avatarbd/AvatarBDBlock.java
+++ b/src/main/java/ui/avatarbd/AvatarBDBlock.java
@@ -51,11 +51,23 @@ import ui.avatarsmd.AvatarSMDPanel;
import ui.util.IconManager;
import ui.window.JDialogAvatarBlock;
+import java.io.IOException;
+import java.io.InputStreamReader;
+import java.io.OutputStreamWriter;
+import java.io.PipedInputStream;
+import java.io.PipedOutputStream;
+import java.io.BufferedReader;
+import java.io.BufferedWriter;
+
+
import javax.swing.*;
import java.awt.*;
import java.util.Iterator;
import java.util.LinkedList;
-
+import java.util.HashMap;
+import proverifspec.ProVerifResultTrace;
+import proverifspec.ProVerifResultTraceStep;
+import ui.interactivesimulation.JFrameSimulationSDPanel;
/**
* Class AvatarBDBlock
@@ -96,7 +108,9 @@ public class AvatarBDBlock extends TGCScalableWithInternalComponent implements S
protected LinkedList<AvatarSignal> mySignals;
protected String[] globalCode;
-
+ protected HashMap<TAttribute, ProVerifResultTrace> attrTraceMap = new HashMap<TAttribute, ProVerifResultTrace>();
+ protected HashMap<TAttribute, Integer> attrLocMap = new HashMap<TAttribute, Integer>();
+
public String oldValue;
public AvatarBDBlock(int _x, int _y, int _minX, int _maxX, int _minY, int _maxY, boolean _pos, TGComponent _father, TDiagramPanel _tdp) {
@@ -160,6 +174,10 @@ public class AvatarBDBlock extends TGCScalableWithInternalComponent implements S
this.internalDrawingAux(graph);
graph.setFont(font);
}
+
+ public void addProVerifTrace(TAttribute attr, ProVerifResultTrace trace){
+ attrTraceMap.put(attr,trace);
+ }
public void setSignalsAsNonAttached() {
for (AvatarSignal mySig : mySignals) mySig.attachedToARelation = false;
@@ -332,6 +350,8 @@ public class AvatarBDBlock extends TGCScalableWithInternalComponent implements S
// Try to draw it
w = graph.getFontMetrics().stringWidth(attrString);
+
+ attrLocMap.put(attr,this.y+h);
if (w + 2 * textX < this.width) {
graph.drawString(attrString, this.x + textX, this.y + h);
this.drawConfidentialityVerification(attr.getConfidentialityVerification(), graph, this.x, this.y + h);
@@ -498,6 +518,45 @@ public class AvatarBDBlock extends TGCScalableWithInternalComponent implements S
g.setColor(c);
}
+ public void showTrace(int y){
+
+ if (y< limitAttr){
+ for (TAttribute attr: attrLocMap.keySet()){
+ if (attrLocMap.get(attr) < y && y < attrLocMap.get(attr) +currentFontSize && attrTraceMap.get(attr)!=null){
+ PipedOutputStream pos = new PipedOutputStream();
+ try {
+ PipedInputStream pis = new PipedInputStream(pos, 4096);
+ BufferedWriter bw = new BufferedWriter(new OutputStreamWriter(pos));
+
+ JFrameSimulationSDPanel jfssdp = new JFrameSimulationSDPanel(null, tdp.getMGUI(), "Confidentiality " + attr.toString());
+ jfssdp.setIconImage(IconManager.img8);
+ GraphicLib.centerOnParent(jfssdp, 600, 600);
+ jfssdp.setFileReference(new BufferedReader(new InputStreamReader(pis)));
+ jfssdp.setVisible(true);
+ //jfssdp.setModalExclusionType(ModalExclusionType
+ // .APPLICATION_EXCLUDE);
+ jfssdp.toFront();
+
+ // TraceManager.addDev("\n--- Trace ---");
+ int i = 0;
+ for (ProVerifResultTraceStep step : attrTraceMap.get(attr).getTrace()) {
+ step.describeAsTMLSDTransaction(bw, i);
+ i++;
+ }
+ bw.close();
+ } catch (IOException e) {
+ TraceManager.addDev("Error when writing trace step SD transaction");
+ } finally {
+ try {
+ pos.close();
+ } catch (IOException ignored) {
+ }
+ }
+
+ }
+ }
+ }
+ }
private void drawConfidentialityVerification(int confidentialityVerification, Graphics g, int _x, int _y) {
Color c = g.getColor();
diff --git a/src/main/java/ui/avatarbd/AvatarBDPragma.java b/src/main/java/ui/avatarbd/AvatarBDPragma.java
index 65fe6e83b48bf43107216edef2bf8ab8001f77da..7dd4d58ffcd5f8878fcc683c6cc9c7b1d1a121a1 100755
--- a/src/main/java/ui/avatarbd/AvatarBDPragma.java
+++ b/src/main/java/ui/avatarbd/AvatarBDPragma.java
@@ -41,13 +41,31 @@ package ui.avatarbd;
import myutil.Conversion;
import myutil.GraphicLib;
+import myutil.TraceManager;
+
import org.w3c.dom.Element;
import org.w3c.dom.Node;
import org.w3c.dom.NodeList;
+
+
import ui.*;
+
+import java.io.IOException;
+import java.io.InputStreamReader;
+import java.io.OutputStreamWriter;
+import java.io.PipedInputStream;
+import java.io.PipedOutputStream;
+import java.io.BufferedReader;
+import java.io.BufferedWriter;
+
import ui.util.IconManager;
import ui.window.JDialogPragma;
+import proverifspec.ProVerifResultTrace;
+import proverifspec.ProVerifResultTraceStep;
+
+import ui.interactivesimulation.JFrameSimulationSDPanel;
+
import javax.swing.*;
import java.awt.*;
import java.util.ArrayList;
@@ -93,6 +111,10 @@ public class AvatarBDPragma extends TGCScalableWithoutInternalComponent {
public final static int NOT_PROVED = 3;
public HashMap<String, Integer> authStrongMap = new HashMap<String, Integer>();
public HashMap<String, Integer> authWeakMap = new HashMap<String, Integer>();
+
+ protected HashMap<String, Integer> pragmaLocMap = new HashMap<String, Integer>();
+
+ public HashMap<String, ProVerifResultTrace> pragmaTraceMap = new HashMap<String, ProVerifResultTrace>();
public AvatarBDPragma(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);
@@ -232,6 +254,7 @@ public class AvatarBDPragma extends TGCScalableWithoutInternalComponent {
g.drawString("Security features", x + textX, y + textY + currentFontSize);
g.setFont(fold);
for (String s : models) {
+ pragmaLocMap.put(s,y + textY + (i + 1) * currentFontSize);
g.drawString(s, x + textX, y + textY + (i + 1) * currentFontSize);
if (syntaxErrors.contains(s)) {
Color ctmp = g.getColor();
@@ -259,7 +282,7 @@ public class AvatarBDPragma extends TGCScalableWithoutInternalComponent {
g.setFont(fold);
}
g.drawString(s, x + textX, y + textY + (i + 1) * currentFontSize);
-
+ pragmaLocMap.put(s,y + textY + i * currentFontSize);
if (syntaxErrors.contains(s)) {
Color ctmp = g.getColor();
g.setColor(Color.red);
@@ -481,4 +504,46 @@ public class AvatarBDPragma extends TGCScalableWithoutInternalComponent {
throw new MalformedModelingException();
}
}
+
+ public void showTrace(int y){
+
+ //TraceManager.addDev(pragmaTraceMap + " " + pragmaLocMap + " " + y);
+ //On right click, display verification trace
+ for (String pragma: pragmaLocMap.keySet()){
+ if (pragmaLocMap.get(pragma) < y && y <pragmaLocMap.get(pragma) +currentFontSize && pragmaTraceMap.get(pragma)!=null){
+ PipedOutputStream pos = new PipedOutputStream();
+ try {
+ PipedInputStream pis = new PipedInputStream(pos, 4096);
+ BufferedWriter bw = new BufferedWriter(new OutputStreamWriter(pos));
+
+ JFrameSimulationSDPanel jfssdp = new JFrameSimulationSDPanel(null, tdp.getMGUI(), pragma);
+ jfssdp.setIconImage(IconManager.img8);
+ GraphicLib.centerOnParent(jfssdp, 600, 600);
+ jfssdp.setFileReference(new BufferedReader(new InputStreamReader(pis)));
+ jfssdp.setVisible(true);
+ //jfssdp.setModalExclusionType(ModalExclusionType
+ // .APPLICATION_EXCLUDE);
+ jfssdp.toFront();
+
+ // TraceManager.addDev("\n--- Trace ---");
+ int i = 0;
+ for (ProVerifResultTraceStep step : pragmaTraceMap.get(pragma).getTrace()) {
+ step.describeAsTMLSDTransaction(bw, i);
+ i++;
+ }
+ bw.close();
+ } catch (IOException e) {
+ TraceManager.addDev("Error when writing trace step SD transaction");
+ } finally {
+ try {
+ pos.close();
+ } catch (IOException ignored) {
+ }
+ }
+ break;
+
+ }
+ }
+ //
+ }
}
diff --git a/src/main/java/ui/interactivesimulation/JFrameInteractiveSimulation.java b/src/main/java/ui/interactivesimulation/JFrameInteractiveSimulation.java
index 0280a3ee7ffbcf9ebf29e42a6f36a760814e7190..ec11c83c40cd2a3873e75760254448a477274438 100755
--- a/src/main/java/ui/interactivesimulation/JFrameInteractiveSimulation.java
+++ b/src/main/java/ui/interactivesimulation/JFrameInteractiveSimulation.java
@@ -146,10 +146,17 @@ public class JFrameInteractiveSimulation extends JFrame implements ActionListene
protected JTextField stateFileName;
protected JTextField benchmarkFileName;
protected JComboBox<String> cpus, busses, mems, tasks, chans;
- private Map<String, List<Integer>> channelIDMap= new HashMap<String, List<Integer>>();
+ private Map<String, List<Integer>> origChannelIDMap= new HashMap<String, List<Integer>>();
+ private Map<String, List<Integer>> destChannelIDMap= new HashMap<String, List<Integer>>();
private String[] cpuIDs, busIDs, memIDs, taskIDs, chanIDs;
private List<String> simtraces= new ArrayList<String>();
+
+ //Find matching channels
+ public Map<String, List<Integer>> channelMsgIdMap = new HashMap<String, List<Integer>>();
+ public Map<Integer, String> msgIdStartTimeMap = new HashMap<Integer, String>();
+ public Map<Integer, String> msgIdEndTimeMap = new HashMap<Integer, String>();
+
// Status elements
private JLabel status, time, info;
@@ -1383,7 +1390,11 @@ public class JFrameInteractiveSimulation extends JFrame implements ActionListene
public void resetSimTrace(){
msgTimes.clear();
chanId=0;
- channelIDMap.clear();
+ channelMsgIdMap.clear();
+ msgIdStartTimeMap.clear();
+ msgIdEndTimeMap.clear();
+ origChannelIDMap.clear();
+ destChannelIDMap.clear();
simtraces.clear();
simIndex=0;
}
@@ -1563,21 +1574,31 @@ public class JFrameInteractiveSimulation extends JFrame implements ActionListene
msgTimes.put(tran.channelName, new ArrayList<String>());
}
if (!msgTimes.get(tran.channelName).contains(tran.endTime)){
- if (channelIDMap.containsKey(tran.channelName) && channelIDMap.get(tran.channelName).size()>0){
- msgId=channelIDMap.get(tran.channelName).remove(0);
- }
- else {
- if (!channelIDMap.containsKey(tran.channelName)){
- channelIDMap.put(tran.channelName, new ArrayList<Integer>());
- }
- channelIDMap.get(tran.channelName).add(msgId);
- chanId++;
- }
String trace="";
if (command.equals("Write")){
+ if (destChannelIDMap.containsKey(tran.channelName) && destChannelIDMap.get(tran.channelName).size()>0){
+ msgId=destChannelIDMap.get(tran.channelName).remove(0);
+ }
+ else {
+ if (!origChannelIDMap.containsKey(tran.channelName)){
+ origChannelIDMap.put(tran.channelName, new ArrayList<Integer>());
+ }
+ origChannelIDMap.get(tran.channelName).add(msgId);
+ chanId++;
+ }
trace = "time=" + tran.endTime+ " block="+ originTask.getName() + " type="+asynchType+ " blockdestination="+ destTask.getName() + " channel="+tran.channelName+" msgid="+ msgId + " params=\"" +chan.getSize()+"\"";
}
else {
+ if (origChannelIDMap.containsKey(tran.channelName) && origChannelIDMap.get(tran.channelName).size()>0){
+ msgId=origChannelIDMap.get(tran.channelName).remove(0);
+ }
+ else {
+ if (!destChannelIDMap.containsKey(tran.channelName)){
+ destChannelIDMap.put(tran.channelName, new ArrayList<Integer>());
+ }
+ destChannelIDMap.get(tran.channelName).add(msgId);
+ chanId++;
+ }
trace = "time=" + tran.endTime+ " block="+ destTask.getName() + " type="+asynchType+ " blockdestination="+ destTask.getName() + " channel="+tran.channelName+" msgid="+ msgId + " params=\"" +chan.getSize()+"\"";
}
//
@@ -1611,21 +1632,31 @@ public class JFrameInteractiveSimulation extends JFrame implements ActionListene
msgTimes.put(tran.channelName, new ArrayList<String>());
}
if (!msgTimes.get(tran.channelName).contains(tran.endTime)){
- if (channelIDMap.containsKey(tran.channelName) && channelIDMap.get(tran.channelName).size()>0){
- msgId=channelIDMap.get(tran.channelName).remove(0);
- }
- else {
- if (!channelIDMap.containsKey(tran.channelName)){
- channelIDMap.put(tran.channelName, new ArrayList<Integer>());
- }
- channelIDMap.get(tran.channelName).add(msgId);
- chanId++;
- }
String trace="";
if (command.equals("Send")){
+ if (destChannelIDMap.containsKey(tran.channelName) && destChannelIDMap.get(tran.channelName).size()>0){
+ msgId=destChannelIDMap.get(tran.channelName).remove(0);
+ }
+ else {
+ if (!origChannelIDMap.containsKey(tran.channelName)){
+ origChannelIDMap.put(tran.channelName, new ArrayList<Integer>());
+ }
+ origChannelIDMap.get(tran.channelName).add(msgId);
+ chanId++;
+ }
trace = "time=" + tran.endTime+ " block="+ originTask.getName() + " type="+asynchType+ " blockdestination="+ destTask.getName() + " channel="+tran.channelName+" msgid="+ msgId + " params=\"";
}
else {
+ if (origChannelIDMap.containsKey(tran.channelName) && origChannelIDMap.get(tran.channelName).size()>0){
+ msgId=origChannelIDMap.get(tran.channelName).remove(0);
+ }
+ else {
+ if (!destChannelIDMap.containsKey(tran.channelName)){
+ destChannelIDMap.put(tran.channelName, new ArrayList<Integer>());
+ }
+ destChannelIDMap.get(tran.channelName).add(msgId);
+ chanId++;
+ }
trace = "time=" + tran.endTime+ " block="+ destTask.getName() + " type="+asynchType+ " blockdestination="+ destTask.getName() + " channel="+tran.channelName+" msgid="+ msgId + " params=\"";
}
//
@@ -1666,25 +1697,47 @@ public class JFrameInteractiveSimulation extends JFrame implements ActionListene
int msgId=chanId;
if (!msgTimes.containsKey(tran.channelName)){
msgTimes.put(tran.channelName, new ArrayList<String>());
+ }
+ if (!channelMsgIdMap.containsKey(tran.channelName)){
+ channelMsgIdMap.put(tran.channelName, new ArrayList<Integer>());
}
+
+
+
if (!msgTimes.get(tran.channelName).contains(tran.endTime)){
- if (channelIDMap.containsKey(tran.channelName) && channelIDMap.get(tran.channelName).size()>0){
- msgId=channelIDMap.get(tran.channelName).remove(0);
- }
- else {
- if (!channelIDMap.containsKey(tran.channelName)){
- channelIDMap.put(tran.channelName, new ArrayList<Integer>());
- }
- channelIDMap.get(tran.channelName).add(msgId);
- chanId++;
- }
+
+
String trace="";
if (command.equals("Request")){
+ if (destChannelIDMap.containsKey(tran.channelName) && destChannelIDMap.get(tran.channelName).size()>0){
+ msgId=destChannelIDMap.get(tran.channelName).remove(0);
+ }
+ else {
+ if (!origChannelIDMap.containsKey(tran.channelName)){
+ origChannelIDMap.put(tran.channelName, new ArrayList<Integer>());
+ }
+ origChannelIDMap.get(tran.channelName).add(msgId);
+ chanId++;
+ }
trace = "time=" + tran.endTime+ " block="+ tran.taskName + " type="+asynchType+ " blockdestination="+ destTask.getName() + " channel="+tran.channelName+" msgid="+ msgId + " params=\"";
+ msgIdStartTimeMap.put(msgId, tran.endTime);
}
else {
+ if (origChannelIDMap.containsKey(tran.channelName) && origChannelIDMap.get(tran.channelName).size()>0){
+ msgId=origChannelIDMap.get(tran.channelName).remove(0);
+ }
+ else {
+ if (!destChannelIDMap.containsKey(tran.channelName)){
+ destChannelIDMap.put(tran.channelName, new ArrayList<Integer>());
+ }
+ destChannelIDMap.get(tran.channelName).add(msgId);
+ chanId++;
+ }
trace = "time=" + tran.endTime+ " block="+ destTask.getName() + " type="+asynchType+ " blockdestination="+ destTask.getName() + " channel="+tran.channelName+" msgid="+ msgId + " params=\"";
+ msgIdEndTimeMap.put(msgId, tran.endTime);
}
+
+ channelMsgIdMap.get(tran.channelName).add(msgId);
//
if (!simtraces.contains(trace)){
simtraces.add(trace);
@@ -1727,6 +1780,73 @@ public class JFrameInteractiveSimulation extends JFrame implements ActionListene
}
}
+ public void calculateCorrespondingTimes(){
+ for (String channel: channelMsgIdMap.keySet()){
+ List<Integer> minTimes = new ArrayList<Integer>();
+ for (int msgId: channelMsgIdMap.get(channel)){
+ String startTime = msgIdStartTimeMap.get(msgId);
+ String endTime = msgIdEndTimeMap.get(msgId);
+ if (startTime!=null && endTime !=null){
+ int diff = Integer.valueOf(endTime) - Integer.valueOf(startTime);
+ minTimes.add(diff);
+ }
+ }
+ SimulationLatency sl = new SimulationLatency();
+ sl.setTransaction1("Send Req: " + channel);
+ sl.setTransaction2("Corresponding Wait Req " + channel);
+
+
+
+
+ sl.setMinTime("??");
+ sl.setMaxTime("??");
+ sl.setAverageTime("??");
+ sl.setStDev("??");
+ boolean found=false;
+ for (Object o:latencies){
+ SimulationLatency s = (SimulationLatency) o;
+ if (s.getTransaction1().equals(sl.getTransaction1()) && s.getTransaction2().equals(sl.getTransaction2())){
+ sl = s;
+ found=true;
+ }
+ }
+ if (!found){
+ latencies.add(sl);
+ }
+ if (minTimes.size()>0){
+ int sum=0;
+ sl.setMinTime(Integer.toString(Collections.min(minTimes)));
+ sl.setMaxTime(Integer.toString(Collections.max(minTimes)));
+ for (int time: minTimes){
+ sum+=time;
+ }
+ double average = (double) sum/ (double) minTimes.size();
+ double stdev =0.0;
+ for (int time:minTimes){
+ stdev +=(time - average)*(time-average);
+ }
+ stdev= stdev/minTimes.size();
+ stdev = Math.sqrt(stdev);
+ sl.setAverageTime(String.format("%.1f",average));
+ sl.setStDev(String.format("%.1f",stdev));
+ }
+
+
+ //updateLatency();
+ // if (latm !=null && latencies.size()>0){
+ // latm.setData(latencies);
+ // }
+
+
+ }
+
+
+
+ //System.out.println(channelMsgIdMap);
+ //System.out.println(msgIdStartTimeMap);
+ //System.out.println(msgIdEndTimeMap);
+ }
+
protected void addStatusToNode(String status, String task){
mgui.addStatus(task,status);
}
@@ -2681,10 +2801,12 @@ public class JFrameInteractiveSimulation extends JFrame implements ActionListene
//calcuate response + checkpoint 1 id + checkpoint 2 id
List<String> id1List = nameIdMap.get(sl.getTransaction1());
List<String> id2List = nameIdMap.get(sl.getTransaction2());
- for (String id1: id1List){
- for (String id2: id2List){
- sendCommand("cl " + id1 + " " + id2);
- }
+ if (id1List!=null && id2List!=null){
+ for (String id1: id1List){
+ for (String id2: id2List){
+ sendCommand("cl " + id1 + " " + id2);
+ }
+ }
}
}
}
@@ -2704,21 +2826,23 @@ public class JFrameInteractiveSimulation extends JFrame implements ActionListene
List<String> ids2 = nameIdMap.get(sl.getTransaction2());
List<Integer> times1 = new ArrayList<Integer>();
List<Integer> times2 = new ArrayList<Integer>();
- for (String id1: ids1){
- if (transTimes.containsKey(id1)){
- for(String time1: transTimes.get(id1)){
- times1.add(Integer.valueOf(time1));
- }
+ if (ids1!=null && ids2!=null){
+ for (String id1: ids1){
+ if (transTimes.containsKey(id1)){
+ for(String time1: transTimes.get(id1)){
+ times1.add(Integer.valueOf(time1));
+ }
+ }
}
- }
- for (String id2: ids2){
- if (transTimes.containsKey(id2)){
- ArrayList<Integer> minTimes = new ArrayList<Integer>();
- for (String time2: transTimes.get(id2)){
- times2.add(Integer.valueOf(time2));
- }
- }
- }
+ for (String id2: ids2){
+ if (transTimes.containsKey(id2)){
+ ArrayList<Integer> minTimes = new ArrayList<Integer>();
+ for (String time2: transTimes.get(id2)){
+ times2.add(Integer.valueOf(time2));
+ }
+ }
+ }
+ }
//
//
List<Integer> minTimes = new ArrayList<Integer>();
@@ -2756,6 +2880,7 @@ public class JFrameInteractiveSimulation extends JFrame implements ActionListene
}
}
}
+ calculateCorrespondingTimes();
if (latm!=null && latencies.size()>0){
latm.setData(latencies);
}
@@ -3449,7 +3574,7 @@ public class JFrameInteractiveSimulation extends JFrame implements ActionListene
checkedTransactions.add(compName+" (ID: " + tgc.getDIPLOID() + ")");
if (!nameIdMap.containsKey(compName)){
nameIdMap.put(compName,new ArrayList<String>());
- checkedTransactions.add(compName);
+ checkedTransactions.add(compName + " (all instances)");
}
nameIdMap.get(compName).add(Integer.toString(tgc.getDIPLOID()));
nameIdMap.put(compName+" (ID: " + tgc.getDIPLOID() + ")",new ArrayList<String>());