diff --git a/src/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
index ec32623c2acf44f5012299cc4e7dd9f873dfd649..8f48c8111981d97275fc827dd04f852ee66c357b 100755
--- a/src/avatartranslator/toproverif/AVATAR2ProVerif.java
+++ b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
@@ -91,8 +91,8 @@ public class AVATAR2ProVerif implements AvatarTranslator {
private final static String HASH_HASH = "hash";
private final static String CH_MAINCH = "ch";
- private final static String CH_ENCRYPT = "privChEnc" + ATTR_DELIM;
- private final static String CH_DECRYPT = "privChDec" + ATTR_DELIM;
+ public final static String CH_ENCRYPT = "privChEnc__";
+ private final static String CH_DECRYPT = "privChDec__";
private final static String CHCTRL_CH = "chControl";
private final static String CHCTRL_ENCRYPT = "chControlEnc";
@@ -472,7 +472,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
int nbOfSignals = ar.nbOfSignals ();
int i;
for (i=0; i<nbOfSignals; i++) {
- String name = ar.getBlock1().getName() + ar.getSignal1 (i).getName () + ar.getBlock2().getName() + ar.getSignal2 (i).getName ();
+ String name = ar.getBlock1().getName() + ar.getSignal1 (i).getName () + "__" + ar.getBlock2().getName() + ar.getSignal2 (i).getName ();
this.spec.addDeclaration (new ProVerifFunc (CH_ENCRYPT + name, new String[] {"bitstring"}, "bitstring", true));
this.spec.addDeclaration (new ProVerifReduc (new ProVerifVar[] {new ProVerifVar ("x", "bitstring")}, CH_DECRYPT + name + " (" + CH_ENCRYPT + name + " (x)) = x", true));
}
@@ -1028,7 +1028,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
boolean isPrivate = false;
AvatarRelation ar = this.avspec.getAvatarRelationWithSignal(as);
int index = ar.getIndexOfSignal (as);
- String name = ar.getBlock1().getName() + ar.getSignal1 (index).getName () + ar.getBlock2().getName() + ar.getSignal2 (index).getName ();
+ String name = ar.getBlock1().getName() + ar.getSignal1 (index).getName () + "__" + ar.getBlock2().getName() + ar.getSignal2 (index).getName ();
if (ar != null)
isPrivate = ar.isPrivate();
diff --git a/src/proverifspec/ProVerifResultTrace.java b/src/proverifspec/ProVerifResultTrace.java
index 95cf8c4038047e9f32034780de883097a7c978d1..2070f08e040d4c4f34bef2f14667c529129319da 100644
--- a/src/proverifspec/ProVerifResultTrace.java
+++ b/src/proverifspec/ProVerifResultTrace.java
@@ -50,6 +50,9 @@ import java.util.HashMap;
import java.util.regex.Pattern;
import java.util.regex.Matcher;
+import java.io.BufferedWriter;
+import java.io.IOException;
+
import myutil.TraceManager;
import ui.AvatarDesignPanel;
@@ -80,11 +83,13 @@ public class ProVerifResultTrace {
private String from;
private String to;
private String message;
+ private String channel;
- public OutStep(String from, String to, String message) {
+ public OutStep(String from, String to, String message, String channel) {
this.from = from;
this.to = to;
this.message = message;
+ this.channel = channel;
}
public boolean messageEquals(String message)
@@ -99,14 +104,21 @@ public class ProVerifResultTrace {
public boolean isToAttacker()
{
- return this.to.equals("ATTACKER");
+ return this.to.equals("Attacker");
}
@Override
public String describeAsString(AvatarDesignPanel adp)
{
- // TraceManager.addDev("[DEBUG] !!! " + this.message);
- return "MSG " + this.from + " -> " + this.to + " : " + ProVerifResultTrace.this.replaceAllAttributeNames(adp, this.message).replaceAll(",", ", ");
+ return "MSG " + this.from + " -- " + this.channel + " --> " + this.to + " : " + ProVerifResultTrace.this.replaceAllAttributeNames(adp, this.message).replaceAll(",", ", ");
+ }
+
+ @Override
+ public void describeAsSDTransaction(AvatarDesignPanel adp, BufferedWriter writer, int step) throws IOException
+ {
+ writer.write("#" + step + " time=0.000000000 block=" + this.from + " blockdestination=" + this.to + " type=synchro channel=" + this.channel + " params=\"" + ProVerifResultTrace.this.replaceAllAttributeNames(adp, this.message).replaceAll(",", ", ") + "\"");
+ writer.newLine();
+ writer.flush();
}
}
@@ -125,6 +137,14 @@ public class ProVerifResultTrace {
{
return "EV " + this.block + "." + this.name;
}
+
+ @Override
+ public void describeAsSDTransaction(AvatarDesignPanel adp, BufferedWriter writer, int step) throws IOException
+ {
+ writer.write("#" + step + " time=0.000000000 block=" + this.block + " type=state_entering state="+ this.name);
+ writer.newLine();
+ writer.flush();
+ }
}
private class NewStep implements ProVerifResultTraceStep {
@@ -140,6 +160,14 @@ public class ProVerifResultTrace {
{
return "NEW " + ProVerifResultTrace.this.replaceAttributeName(adp, this.name);
}
+
+ @Override
+ public void describeAsSDTransaction(AvatarDesignPanel adp, BufferedWriter writer, int step) throws IOException
+ {
+ writer.write("#" + step + " time=0.000000000 block=Attacker type=function_call func=new parameters=" + ProVerifResultTrace.this.replaceAttributeName(adp, this.name));
+ writer.newLine();
+ writer.flush();
+ }
}
public ProVerifResultTrace(LinkedList<String> proverifProcess)
@@ -314,6 +342,14 @@ public class ProVerifResultTrace {
|| msgName.startsWith("choice" + AVATAR2ProVerif.ATTR_DELIM))
return m.group(4);
+ String channelName = "";
+ Matcher m2 = Pattern.compile(AVATAR2ProVerif.CH_ENCRYPT + ".+?__(.+?)\\((.*)\\)").matcher(msgName);
+ if (m2.matches())
+ {
+ channelName = m2.group(1);
+ msgName = m2.group(2);
+ }
+
boolean foundAStep = false;
for (ProVerifResultTraceStep step: this.trace)
{
@@ -334,7 +370,7 @@ public class ProVerifResultTrace {
if (!foundAStep)
{
- this.trace.add(new OutStep("ATTACKER", this.getBlockNameFromLine(Integer.parseInt(m.group(3))), msgName));
+ this.trace.add(new OutStep("Attacker", this.getBlockNameFromLine(Integer.parseInt(m.group(3))), msgName, channelName));
}
return m.group(4);
@@ -376,7 +412,6 @@ public class ProVerifResultTrace {
if (str.startsWith("By "))
{
- // TraceManager.addDev("[DEBUG] BY: " + str);
return;
}
@@ -393,10 +428,18 @@ public class ProVerifResultTrace {
|| msgName.startsWith("chControlEnc"))
return;
- // TraceManager.addDev("[DEBUG] OUT: " + str);
String blockName = this.getBlockNameFromLine(Integer.parseInt(m.group(4)));
+
+ String channelName = "";
+ m = Pattern.compile(AVATAR2ProVerif.CH_ENCRYPT + ".+?__(.+?)\\((.*)\\)").matcher(msgName);
+ if (m.matches())
+ {
+ channelName = m.group(1);
+ msgName = m.group(2);
+ }
+
if (blockName != null)
- this.trace.add(new OutStep(blockName, "ATTACKER", msgName));
+ this.trace.add(new OutStep(blockName, "Attacker", msgName, channelName));
return;
}
@@ -406,7 +449,6 @@ public class ProVerifResultTrace {
if (m.matches())
{
String line = m.group(2);
- // TraceManager.addDev("[DEBUG] EVENT: " + str);
p = Pattern.compile("enteringState" + AVATAR2ProVerif.ATTR_DELIM + "[a-zA-Z0-9_]+" + AVATAR2ProVerif.ATTR_DELIM + "([a-zA-Z0-9_]+)");
m = p.matcher(m.group(1));
diff --git a/src/proverifspec/ProVerifResultTraceStep.java b/src/proverifspec/ProVerifResultTraceStep.java
index af843ebe0209f7fe127f663ab92a9740d34f531b..fd14e6663c5bc009e3262a7c2a9a43aef1867d6d 100644
--- a/src/proverifspec/ProVerifResultTraceStep.java
+++ b/src/proverifspec/ProVerifResultTraceStep.java
@@ -45,8 +45,12 @@
package proverifspec;
+import java.io.BufferedWriter;
+import java.io.IOException;
+
import ui.AvatarDesignPanel;
public interface ProVerifResultTraceStep {
public String describeAsString(AvatarDesignPanel adp);
+ public void describeAsSDTransaction(AvatarDesignPanel adp, BufferedWriter writer, int step) throws IOException;
}
diff --git a/src/ui/interactivesimulation/JFrameSimulationSDPanel.java b/src/ui/interactivesimulation/JFrameSimulationSDPanel.java
index fb7b63a4b18b841513067243af4967f8a392b900..42a0dc7e335dff65a5f1ae2042d72a2ec9865d67 100755
--- a/src/ui/interactivesimulation/JFrameSimulationSDPanel.java
+++ b/src/ui/interactivesimulation/JFrameSimulationSDPanel.java
@@ -89,7 +89,6 @@ public class JFrameSimulationSDPanel extends JFrame implements ActionListener {
public InteractiveSimulationActions [] actions;
- private Frame f;
private MainGUI mgui;
private String title;
//private String hostSystemC;
@@ -109,7 +108,6 @@ public class JFrameSimulationSDPanel extends JFrame implements ActionListener {
public JFrameSimulationSDPanel(Frame _f, MainGUI _mgui, String _title) {
super(_title);
- f = _f;
mgui = _mgui;
title = _title;
@@ -224,6 +222,12 @@ public class JFrameSimulationSDPanel extends JFrame implements ActionListener {
sdpanel.setFileReference(_fileReference);
}
}
+
+ public void setFileReference(BufferedReader inputStream) {
+ if (sdpanel != null) {
+ sdpanel.setFileReference(inputStream);
+ }
+ }
public void setCurrentTime(long timeValue) {
status.setText("time = " + timeValue);
diff --git a/src/ui/interactivesimulation/JSimulationSDPanel.java b/src/ui/interactivesimulation/JSimulationSDPanel.java
index 419bc3238cae4c75988d32cbe96d33bc2163273d..f069c8142cbc61451389c5c084b4ea7defd9e6dc 100644
--- a/src/ui/interactivesimulation/JSimulationSDPanel.java
+++ b/src/ui/interactivesimulation/JSimulationSDPanel.java
@@ -84,12 +84,13 @@ public class JSimulationSDPanel extends JPanel implements MouseMotionListener, R
private int spaceVerticalText = 2;
private int spaceHorizontalText = 2;
private int spaceStop = 20;
- private int verticalLink = 7;
+ private int verticalLink = 10;
private int lengthAsync = 50;
private int spaceBroadcast = 25;
// Transactions
- protected String fileReference;
+ private BufferedReader inputStream;
+ private String fileReference;
private int maxNbOfTransactions = 10000;
private int drawnTransactions = 10000;
@@ -113,6 +114,7 @@ public class JSimulationSDPanel extends JPanel implements MouseMotionListener, R
private final int NO_MODE = 0;
private final int FILE_MODE = 1;
+ private final int STREAM_MODE = 2;
private int mode;
private boolean go;
private Thread t;
@@ -249,7 +251,19 @@ public class JSimulationSDPanel extends JPanel implements MouseMotionListener, R
spaceBetweenLifeLines = w+minSpaceBetweenLifeLines;
}
}
-
+
+ for (GenericTransaction gt: this.transactions) {
+ if (gt.type == gt.SYNCHRO) {
+ String messageName = gt.name + "(" + gt.params + ")";
+ w = g.getFontMetrics().stringWidth(messageName);
+ if (w+this.minSpaceBetweenLifeLines > this.spaceBetweenLifeLines)
+ this.spaceBetweenLifeLines = w+this.minSpaceBetweenLifeLines;
+ }
+ }
+
+ int m = this.getSize().width / (this.entityNames.size()+1);
+ if (this.spaceBetweenLifeLines > m)
+ this.spaceBetweenLifeLines = m;
}
public void setNewSize() {
@@ -434,7 +448,7 @@ public class JSimulationSDPanel extends JPanel implements MouseMotionListener, R
// Putting the message name
w = g.getFontMetrics().stringWidth(messageName);
int xtmp = (xOf2ndBlock + currentX)/2 - w/2;
- g.drawString(messageName, xtmp, currentY-2);
+ g.drawString(messageName, xtmp, currentY-4);
currentY += 10;
@@ -917,25 +931,45 @@ public class JSimulationSDPanel extends JPanel implements MouseMotionListener, R
}
public void setFileReference(String _fileReference) {
- fileReference = _fileReference;
-
- mode = FILE_MODE;
-
- Thread t = new Thread(this);
- t.start();
+ try {
+ // Open the file that is the first
+ // command line parameter
+ this.fileReference = _fileReference;
+ this.mode = FILE_MODE;
+ FileInputStream fstream = new FileInputStream(_fileReference);
+ BufferedReader br = new BufferedReader(new InputStreamReader(new DataInputStream(fstream)));
+ // Get the object of DataInputStream
+ this.setFileReference(br, _fileReference);
+ } catch(FileNotFoundException e) {
+ TraceManager.addDev("File " + _fileReference + " not found.");
+ } catch(SecurityException e) {
+ TraceManager.addDev("Reading file Error: " + e.getMessage());
+ }
}
+
+ public void setFileReference(BufferedReader inputStream) {
+ this.mode = STREAM_MODE;
+ this.setFileReference(inputStream, "from unnamed input stream");
+ }
+
+ private void setFileReference(BufferedReader inputStream, String fileReference) {
+ getExclu();
+ jfssdp.setStatus("Reading " + fileReference);
+ this.inputStream = inputStream;
+ this.entityNames.clear();
+ this.transactions.clear();
+ this.transactionsOfPoints.clear();
+ this.points.clear();
+ removeExclu();
+
+ Thread t = new Thread(this);
+ t.start();
+ }
public synchronized void refresh() {
- if (mode == FILE_MODE) {
- entityNames.clear();
- transactions.clear();
- transactionsOfPoints.clear();
- points.clear();
- if (t == null) {
- Thread t = new Thread(this);
- t.start();
- }
- }
+ if (mode == FILE_MODE) {
+ this.setFileReference(this.fileReference);
+ }
}
public void run() {
@@ -950,31 +984,22 @@ public class JSimulationSDPanel extends JPanel implements MouseMotionListener, R
return;
}
- if (mode == FILE_MODE) {
- // Open the file
+ if ((this.mode == FILE_MODE || this.mode == STREAM_MODE) && this.inputStream != null) {
// Read the content of the file
// Read line by line
// Upate the graphic regularly
getExclu();
- jfssdp.setStatus("Reading " + fileReference);
+
try{
- // Open the file that is the first
- // command line parameter
- FileInputStream fstream = new FileInputStream(fileReference);
- // Get the object of DataInputStream
- DataInputStream in = new DataInputStream(fstream);
- BufferedReader br = new BufferedReader(new InputStreamReader(in));
- String strLine;
- //Read File Line By Line
- while ((strLine = br.readLine()) != null) {
- // Print the content on the console
- //TraceManager.addDev("Computing transaction:" + strLine);
- addGenericTransaction(strLine);
- }
+ String strLine;
+ //Read File Line By Line
+ while ((strLine = this.inputStream.readLine()) != null) {
+ addGenericTransaction(strLine);
+ }
//Close the input stream
- in.close();
+ this.inputStream.close();
} catch (Exception e){//Catch exception if any
- TraceManager.addDev("Reading file Error: " + e.getMessage());
+ TraceManager.addDev("Closing file Error: " + e.getMessage());
}
if (jfssdp != null) {
@@ -986,6 +1011,7 @@ public class JSimulationSDPanel extends JPanel implements MouseMotionListener, R
}
t = null;
+ this.inputStream = null;
}
private void updateInfoOnTransactions() {
@@ -1158,9 +1184,13 @@ public class JSimulationSDPanel extends JPanel implements MouseMotionListener, R
}
String ret = main.substring(index+sel.length(), main.length());
- index = ret.indexOf(' ');
+ if (ret.charAt(0) == '"') {
+ ret = ret.substring(1);
+ index = ret.indexOf('"');
+ } else
+ index = ret.indexOf(' ');
- if (index != -1) {
+ if (index >= 0) {
ret = ret.substring(0, index);
}
@@ -1195,4 +1225,4 @@ public class JSimulationSDPanel extends JPanel implements MouseMotionListener, R
clockDiviser = _clockDiviser;
updateInfoOnTransactions();
}
-}
\ No newline at end of file
+}
diff --git a/src/ui/window/JDialogProverifVerification.java b/src/ui/window/JDialogProverifVerification.java
index f8305ee67daaf3dd2459ca7d10a1739060c69d87..4cdfe6d0318966f0017720d885c355cbfdab990a 100644
--- a/src/ui/window/JDialogProverifVerification.java
+++ b/src/ui/window/JDialogProverifVerification.java
@@ -59,6 +59,8 @@ import avatartranslator.*;
import proverifspec.*;
import ui.*;
+import ui.interactivesimulation.JFrameSimulationSDPanel;
+
import launcher.*;
@@ -153,7 +155,7 @@ public class JDialogProverifVerification extends javax.swing.JDialog implements
/** Creates new form */
public JDialogProverifVerification(Frame f, MainGUI _mgui, String title, String _hostProVerif, String _pathCode, String _pathExecute, AvatarDesignPanel adp) {
- super(f, title, true);
+ super(f, title, Dialog.ModalityType.DOCUMENT_MODAL);
mgui = _mgui;
this.adp = adp;
@@ -307,11 +309,35 @@ public class JDialogProverifVerification extends javax.swing.JDialog implements
} else if (command.equals("Show trace")) {
if (evt.getSource() == this.menuItem)
{
- TraceManager.addDev("\n--- Trace ---");
- for (ProVerifResultTraceStep step: this.menuItem.result.getTrace().getTrace())
- TraceManager.addDev(step.describeAsString(this.adp));
- TraceManager.addDev("");
- // TODO
+ PipedOutputStream pos = new PipedOutputStream();
+ try {
+ PipedInputStream pis = new PipedInputStream(pos, 4096);
+ BufferedWriter bw = new BufferedWriter(new OutputStreamWriter(pos));
+
+ JFrameSimulationSDPanel jfssdp = new JFrameSimulationSDPanel(null, this.mgui, this.menuItem.pragma.toString());
+ jfssdp.setIconImage(IconManager.img8);
+ GraphicLib.centerOnParent(jfssdp, 600, 600);
+ jfssdp.setFileReference(new BufferedReader(new InputStreamReader(pis)));
+ jfssdp.setVisible(true);
+ jfssdp.setModalExclusionType(Dialog.ModalExclusionType.APPLICATION_EXCLUDE);
+ jfssdp.toFront();
+
+ // TraceManager.addDev("\n--- Trace ---");
+ int i=0;
+ for (ProVerifResultTraceStep step: this.menuItem.result.getTrace().getTrace()) {
+ step.describeAsSDTransaction(this.adp, bw, i);
+ i++;
+ // TraceManager.addDev(step.describeAsString(this.adp));
+ }
+ bw.close();
+ } catch(IOException e) {
+ TraceManager.addDev("Error when writing trace step SD transaction");
+ } finally {
+ try {
+ pos.close();
+ } catch(IOException e) {}
+ }
+ // TraceManager.addDev("");
}
}
}