Adds checkboxes to observation list (#196)

srba · web-flow · commit 0e70f89fefa3 · 2025-03-11T07:57:32.000+01:00
+ Adds ability do disable and enable observations to observe during SMC
execution
diff --git a/src/main/java/dk/aau/cs/TCTL/visitors/SMCQueryVisitor.java b/src/main/java/dk/aau/cs/TCTL/visitors/SMCQueryVisitor.java
@@ -1,13 +1,13 @@
 package dk.aau.cs.TCTL.visitors;
 
+import java.util.ArrayList;
 import java.util.List;
 
 import dk.aau.cs.TCTL.*;
 import dk.aau.cs.verification.SMCSettings;
 import dk.aau.cs.verification.observations.Observation;
 
 public class SMCQueryVisitor extends LTLQueryVisitor {
-
     private static final String XML_SMC		    	        = "smc";
     private static final String XML_TIME_BOUND_TAG          = "time-bound";
     private static final String XML_STEP_BOUND_TAG          = "step-bound";
@@ -18,20 +18,22 @@ public class SMCQueryVisitor extends LTLQueryVisitor {
     private static final String XML_INTERVAL_WIDTH_TAG      = "interval-width";
     private static final String XML_COMPARE_TO_FLOAT_TAG    = "compare-to";
     private static final String XML_OBSERVATIONS            = "observations";
-    private static final String XML_WATCH                   = "watch";
-    private static final String XML_WATCH_ID                = "id";
-    private static final String XML_WATCH_NAME              = "name";
 
     public String getXMLQueryFor(TCTLAbstractProperty property, String queryName, SMCSettings settings) {
-        buildXMLQuery(property, queryName, settings);
+        buildXMLQuery(property, queryName, settings, true);
         return getFormatted();
     }
 
     public void buildXMLQuery(TCTLAbstractProperty property, String queryName, SMCSettings settings) {
+        buildXMLQuery(property, queryName, settings, false);
+    }
+
+    public void buildXMLQuery(TCTLAbstractProperty property, String queryName, SMCSettings settings, boolean discardDisabled) {
         xmlQuery.append(startTag(XML_PROP) + queryInfo(queryName) + smcTag(settings));
 
-        if (!settings.getObservations().isEmpty()) {
-            xmlQuery.append(observationTag(settings.getObservations()));
+        List<Observation> observations = settings.getObservations();
+        if (!observations.isEmpty()) {
+            xmlQuery.append(observationTag(observations, discardDisabled));
         }
             
         xmlQuery.append(startTag(XML_FORMULA));
@@ -57,10 +59,14 @@ private String smcTag(SMCSettings settings) {
         return emptyElement(tagContent);
     }
 
-    private String observationTag(List<Observation> observations) {
+    private String observationTag(List<Observation> observations, boolean discardDisabled) {
         String observationXml = startTag(XML_OBSERVATIONS); 
-        
-        for (Observation observation : observations) {
+        List<Observation> observationsCopy = new ArrayList<>(observations);
+        if (discardDisabled) {
+            observationsCopy.removeIf(observation -> !observation.isEnabled());
+        }
+
+        for (Observation observation : observationsCopy) {
             observationXml += observation.toXml();
         }
 
@@ -69,10 +75,6 @@ private String observationTag(List<Observation> observations) {
         return observationXml;
     }
 
-    private String tagAttribute(String name, String value) {
-        return " " + name + "=\"" + value + "\"";
-    }
-
     private String tagAttribute(String name, float value) {
         return " " + name + "=\"" + String.valueOf(value) + "\"";
     }
diff --git a/src/main/java/dk/aau/cs/io/queries/TAPNQueryLoader.java b/src/main/java/dk/aau/cs/io/queries/TAPNQueryLoader.java
@@ -135,6 +135,11 @@ private TAPNQuery parseTAPNQuery(Element queryElement, TimedArcPetriNetNetwork n
 
                         Element root = getFirstElementChild(watch);
                         Observation observation = new Observation(name, parseObsExpression(root));
+                        
+                        if (watch.hasAttribute("isEnabled")) {
+                            observation.setEnabled(watch.getAttribute("isEnabled").equals("true"));
+                        }
+
                         observations.add(observation);
                     }
 
diff --git a/src/main/java/dk/aau/cs/verification/observations/Observation.java b/src/main/java/dk/aau/cs/verification/observations/Observation.java
@@ -5,6 +5,7 @@
 
 public class Observation {
     private String name;
+    private boolean isEnabled = true;
 
     private ObsExpression expression = new ObsPlaceHolder();
 
@@ -25,6 +26,10 @@ public ObsExpression getExpression() {
         return expression;
     }
 
+    public boolean isEnabled() {
+        return isEnabled;
+    }
+
     public void setName(String name) {
         this.name = name;
     }
@@ -33,12 +38,16 @@ public void setExpression(ObsExpression expression) {
         this.expression = expression;
     }
 
+    public void setEnabled(boolean isEnabled) {
+        this.isEnabled = isEnabled;
+    }
+
     @Override
     public String toString() {
         return name + ": " + expression.toString();
     }
 
     public String toXml() {
-        return "<watch name=\"" + name + "\">" + expression.toXml() + "</watch>";
+        return "<watch name=\"" + name + "\" isEnabled=\"" + isEnabled + "\">" + expression.toXml() + "</watch>";
     }
 }
diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/ObservationListDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/ObservationListDialog.java
@@ -3,11 +3,13 @@
 import javax.swing.DefaultListCellRenderer;
 import javax.swing.DefaultListModel;
 import javax.swing.JButton;
+import javax.swing.JCheckBox;
+import javax.swing.JLabel;
 import javax.swing.JList;
 import javax.swing.JPanel;
 import javax.swing.JScrollPane;
 import javax.swing.JViewport;
-import javax.swing.SwingUtilities;
+import javax.swing.ListCellRenderer;
 import javax.swing.event.ListDataListener;
 import javax.swing.event.ListDataEvent;
 
@@ -16,15 +18,19 @@
 import pipe.gui.TAPAALGUI;
 import pipe.gui.swingcomponents.EscapableDialog;
 
+import java.awt.BorderLayout;
 import java.awt.Component;
 import java.awt.Dimension;
 import java.awt.FontMetrics;
 import java.awt.GridBagLayout;
 import java.awt.Insets;
+import java.awt.Rectangle;
 import java.awt.event.MouseAdapter;
 import java.awt.event.MouseEvent;
 import java.awt.GridBagConstraints;
+import java.util.HashMap;
 import java.util.List;
+import java.util.Map;
 
 public class ObservationListDialog extends EscapableDialog {
     private final TimedArcPetriNetNetwork tapnNetwork;
@@ -73,6 +79,74 @@ public Component getListCellRendererComponent(JList<?> list, Object value, int i
         }
     }    
 
+    private static class CheckboxListRenderer extends JPanel implements ListCellRenderer<Observation> {
+        private final JCheckBox checkBox;
+        private final JLabel label;
+        private final EllipsisListCellRenderer ellipsisRenderer;
+
+        public CheckboxListRenderer() {
+            setLayout(new BorderLayout());
+            checkBox = new JCheckBox();
+            label = new JLabel();
+            ellipsisRenderer = new EllipsisListCellRenderer();
+            add(checkBox, BorderLayout.WEST);
+            add(label, BorderLayout.CENTER);
+        }
+
+        @Override
+        public Component getListCellRendererComponent(JList<? extends Observation> list, Observation value, int index, boolean isSelected, boolean cellHasFocus) {       
+            ellipsisRenderer.getListCellRendererComponent(list, value, index, isSelected, cellHasFocus);
+            
+            boolean checked = ((CheckboxListModel)list.getModel()).isChecked(value);
+            checkBox.setSelected(checked);
+
+            setToolTipText("Select the observation to be monitored during SMC execution");
+
+            label.setText(value.toString());
+            label.setToolTipText(ellipsisRenderer.getToolTipText());
+            label.setEnabled(checked);
+            
+            setBackground(isSelected ? list.getSelectionBackground() : list.getBackground());
+            setForeground(isSelected ? list.getSelectionForeground() : list.getForeground());
+            checkBox.setBackground(getBackground());
+            label.setBackground(getBackground());
+            
+            return this;
+        }
+    }
+
+    private static class CheckboxListModel extends DefaultListModel<Observation> {
+        private final Map<Observation, Boolean> checkMap = new HashMap<>();
+        
+        public boolean isChecked(Observation observation) {
+            return checkMap.getOrDefault(observation, observation.isEnabled());
+        }
+        
+        public void toggleChecked(Observation observation) {
+            boolean currentState = isChecked(observation);
+            boolean newState = !currentState;
+            checkMap.put(observation, newState);
+            observation.setEnabled(newState);
+            int index = indexOf(observation);
+            if (index >= 0) {
+                fireContentsChanged(this, index, index);
+            }
+        }
+        
+        @Override
+        public void addElement(Observation observation) {
+            super.addElement(observation);
+            checkMap.put(observation, observation.isEnabled());
+        }
+        
+        @Override
+        public boolean removeElement(Object observation) {
+            boolean removed = super.removeElement(observation);
+            checkMap.remove(observation);
+            return removed;
+        }
+    }
+
     private void init() {
         setSize(500, 350);
         setResizable(false);
@@ -81,7 +155,8 @@ private void init() {
        
         JPanel observationPanel = new JPanel();
         observationPanel.setLayout(new GridBagLayout());
-        DefaultListModel<Observation> listModel = new DefaultListModel<>();
+        
+        CheckboxListModel listModel = new CheckboxListModel();
         for (Observation observation : observations) {
             listModel.addElement(observation);
         }
@@ -110,7 +185,7 @@ public void contentsChanged(ListDataEvent e) {
         });
 
         JList<Observation> observationList = new JList<>(listModel);
-        observationList.setCellRenderer(new EllipsisListCellRenderer());
+        observationList.setCellRenderer(new CheckboxListRenderer());
 
         JScrollPane observationScrollPane = new JScrollPane(observationList);
         observationScrollPane.setHorizontalScrollBarPolicy(JScrollPane.HORIZONTAL_SCROLLBAR_NEVER);
@@ -125,8 +200,16 @@ public void contentsChanged(ListDataEvent e) {
         observationList.addMouseListener(new MouseAdapter() {
             @Override
             public void mouseClicked(MouseEvent e) {
-                if (e.getClickCount() == 2) {
-                    showEditObservationDialog(observationList.getSelectedIndex(), listModel);
+                int index = observationList.locationToIndex(e.getPoint());
+                if (index >= 0) {
+                    Rectangle bounds = observationList.getCellBounds(index, index);
+                    if (bounds != null && e.getX() < bounds.x + 20) {
+                        Observation observation = listModel.getElementAt(index);
+                        listModel.toggleChecked(observation);
+                        observationList.repaint();
+                    } else if (e.getClickCount() == 2) {
+                        showEditObservationDialog(observationList.getSelectedIndex(), listModel);
+                    }
                 }
             }
         });

Original file line number	Diff line number	Diff line change
`@@ -5,6 +5,7 @@`
`5`	`5`
`6`	`6`	`public class Observation {`
`7`	`7`	`private String name;`
	`8`	`+ private boolean isEnabled = true;`
`8`	`9`
`9`	`10`	`private ObsExpression expression = new ObsPlaceHolder();`
`10`	`11`
`@@ -25,6 +26,10 @@ public ObsExpression getExpression() {`
`25`	`26`	`return expression;`
`26`	`27`	`}`
`27`	`28`
	`29`	`+ public boolean isEnabled() {`
	`30`	`+ return isEnabled;`
	`31`	`+ }`
	`32`	`+`
`28`	`33`	`public void setName(String name) {`
`29`	`34`	`this.name = name;`
`30`	`35`	`}`
`@@ -33,12 +38,16 @@ public void setExpression(ObsExpression expression) {`
`33`	`38`	`this.expression = expression;`
`34`	`39`	`}`
`35`	`40`
	`41`	`+ public void setEnabled(boolean isEnabled) {`
	`42`	`+ this.isEnabled = isEnabled;`
	`43`	`+ }`
	`44`	`+`
`36`	`45`	`@Override`
`37`	`46`	`public String toString() {`
`38`	`47`	`return name + ": " + expression.toString();`
`39`	`48`	`}`
`40`	`49`
`41`	`50`	`public String toXml() {`
`42`		`- return "<watch name=\"" + name + "\">" + expression.toXml() + "</watch>";`
	`51`	`+ return "<watch name=\"" + name + "\" isEnabled=\"" + isEnabled + "\">" + expression.toXml() + "</watch>";`
`43`	`52`	`}`
`44`	`53`	`}`