From 2914d85547d7a9c1774e90d8f2b3756033c710ed Mon Sep 17 00:00:00 2001 From: L <letitia.li@telecom-paristech.fr> Date: Wed, 26 Sep 2018 10:22:17 -0400 Subject: [PATCH] Fixed proverif trace missing --- .../JFrameSimulationSDPanel.java | 4 ++- .../JSimulationSDPanel.java | 28 ++++++++++++++++--- .../window/JDialogProverifVerification.java | 1 + 3 files changed, 28 insertions(+), 5 deletions(-) diff --git a/src/main/java/ui/interactivesimulation/JFrameSimulationSDPanel.java b/src/main/java/ui/interactivesimulation/JFrameSimulationSDPanel.java index 1be213a374..51ca1b7a12 100755 --- a/src/main/java/ui/interactivesimulation/JFrameSimulationSDPanel.java +++ b/src/main/java/ui/interactivesimulation/JFrameSimulationSDPanel.java @@ -208,7 +208,9 @@ public class JFrameSimulationSDPanel extends JFrame implements ActionListener { public void setNbOfTransactions(int x, long minTime, long maxTime) { status.setText("" + x + " transactions, min time=" + minTime + ", max time=" + maxTime); } - + public void setLimitEntity(boolean limit){ + sdpanel.setLimitEntity(limit); + } diff --git a/src/main/java/ui/interactivesimulation/JSimulationSDPanel.java b/src/main/java/ui/interactivesimulation/JSimulationSDPanel.java index 012201621f..0ad67a66fb 100644 --- a/src/main/java/ui/interactivesimulation/JSimulationSDPanel.java +++ b/src/main/java/ui/interactivesimulation/JSimulationSDPanel.java @@ -117,6 +117,7 @@ public class JSimulationSDPanel extends JPanel implements MouseMotionListener, R private Vector<GenericTransaction> transactions; private JFrameSimulationSDPanel jfssdp; + private boolean limitEntity = true; //For simulation, we want to select the entities to display, but for proverif traces, we display all of them JSimulationSDPanel(JFrameSimulationSDPanel _jfssdp) { @@ -139,6 +140,7 @@ public class JSimulationSDPanel extends JPanel implements MouseMotionListener, R } + //Return true iff exclu was obtained private synchronized boolean tryToGetExclu() { if (excluOnList == 1) { @@ -453,6 +455,10 @@ public class JSimulationSDPanel extends JPanel implements MouseMotionListener, R return currentY; } + public void setLimitEntity(boolean limit){ + limitEntity = limit; + } + private int drawSendAsynchro(Graphics g, GenericTransaction _gt, int currentX, int currentY) { int w; int x; @@ -1080,10 +1086,17 @@ public class JSimulationSDPanel extends JPanel implements MouseMotionListener, R //TraceManager.addDev("4"); // addEntityNameIfApplicable(tmp); - gt.entityName = tmp; + if (!entityNames.contains(tmp)){ - return; + if (limitEntity){ + return; + } + else { + addEntityNameIfApplicable(tmp); + } } + + gt.entityName = tmp; // Type of the transaction tmp = extract(trans, "type"); @@ -1143,12 +1156,19 @@ public class JSimulationSDPanel extends JPanel implements MouseMotionListener, R tmp = extract(trans, "blockdestination"); if (tmp != null) { gt.otherEntityName = tmp; - // addEntityNameIfApplicable(tmp); +// addEntityNameIfApplicable(tmp); } if (!entityNames.contains(tmp)){ - return; + if (limitEntity){ + return; + } + else { + if (tmp!=null){ + addEntityNameIfApplicable(tmp); + } + } } // Channel of the transaction? diff --git a/src/main/java/ui/window/JDialogProverifVerification.java b/src/main/java/ui/window/JDialogProverifVerification.java index 6171a17beb..4b7510aa3f 100644 --- a/src/main/java/ui/window/JDialogProverifVerification.java +++ b/src/main/java/ui/window/JDialogProverifVerification.java @@ -681,6 +681,7 @@ public class JDialogProverifVerification extends JDialog implements ActionListen jfssdp.setVisible(true); jfssdp.setModalExclusionType(ModalExclusionType .APPLICATION_EXCLUDE); + jfssdp.setLimitEntity(false); jfssdp.toFront(); // TraceManager.addDev("\n--- Trace ---"); -- GitLab