From be7fe1aec88374b762226c92b09373fe65b5f549 Mon Sep 17 00:00:00 2001 From: Mark Kattenbelt Date: Mon, 6 Nov 2006 14:03:59 +0000 Subject: [PATCH] Made small change to the simulator. Now you can double click the table with updates (i.e. enabled transitions) with the result of that the transition is taken. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@121 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/userinterface/simulator/GUISimulator.java | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java index ad462941..09b30118 100644 --- a/prism/src/userinterface/simulator/GUISimulator.java +++ b/prism/src/userinterface/simulator/GUISimulator.java @@ -139,7 +139,18 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect //verifyAllPropertiesAtOnce = true; //options = new GUISimulatorOptions(this); - currentUpdatesTable.setModel(updateTableModel); + currentUpdatesTable.setModel(updateTableModel); + currentUpdatesTable.addMouseListener(new MouseAdapter() + { + public void mouseClicked(MouseEvent e) + { + if (e.getClickCount() == 2 && currentUpdatesTable.isEnabled()) + { + a_manualUpdate(); + } + } + }); + pathTable.setModel(pathTableModel); lastConstants = null;