diff --git a/src/main/java/ui/interactivesimulation/JFrameSimulationSDPanel.java b/src/main/java/ui/interactivesimulation/JFrameSimulationSDPanel.java index 1be213a37400e3c16dc6dbdc2f398012a064ad53..51ca1b7a12aa05f05c0e2abe34aa9612d92fd02f 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 012201621f1969b499b94fc6082faf2ad6e4f65f..0ad67a66fba35b78d615f98f45f942f0ab353842 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 6171a17bebb71de1b8219d00595eccb347a0f75f..4b7510aa3f62e64bf31e421f99d6daf96310b45a 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 ---");