From 4e841ce3248b0a344920d91a113041b446b40937 Mon Sep 17 00:00:00 2001 From: Mikkel Tygesen Date: Wed, 13 Nov 2024 19:25:02 +0100 Subject: [PATCH 1/7] started work on building observation expressions --- .../aau/cs/TCTL/visitors/SMCQueryVisitor.java | 32 +- .../dk/aau/cs/io/queries/TAPNQueryLoader.java | 19 + .../dk/aau/cs/verification/SMCSettings.java | 16 + .../observations/Observation.java | 48 +++ .../observations/expressions/ObsAdd.java | 16 + .../observations/expressions/ObsConstant.java | 19 + .../expressions/ObsExprPosition.java | 29 ++ .../expressions/ObsExpression.java | 8 + .../observations/expressions/ObsLeaf.java | 18 + .../observations/expressions/ObsMultiply.java | 16 + .../observations/expressions/ObsOperator.java | 108 ++++++ .../observations/expressions/ObsPlace.java | 21 + .../expressions/ObsPlaceHolder.java | 13 + .../observations/expressions/ObsSubtract.java | 16 + .../petrinet/dialog/ObservationDialog.java | 367 ++++++++++++++++++ .../dialog/ObservationListDialog.java | 162 ++++++++ .../gui/petrinet/dialog/QueryDialog.java | 45 ++- src/main/java/net/tapaal/helpers/Enabler.java | 22 ++ 18 files changed, 954 insertions(+), 21 deletions(-) create mode 100644 src/main/java/dk/aau/cs/verification/observations/Observation.java create mode 100644 src/main/java/dk/aau/cs/verification/observations/expressions/ObsAdd.java create mode 100644 src/main/java/dk/aau/cs/verification/observations/expressions/ObsConstant.java create mode 100644 src/main/java/dk/aau/cs/verification/observations/expressions/ObsExprPosition.java create mode 100644 src/main/java/dk/aau/cs/verification/observations/expressions/ObsExpression.java create mode 100644 src/main/java/dk/aau/cs/verification/observations/expressions/ObsLeaf.java create mode 100644 src/main/java/dk/aau/cs/verification/observations/expressions/ObsMultiply.java create mode 100644 src/main/java/dk/aau/cs/verification/observations/expressions/ObsOperator.java create mode 100644 src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlace.java create mode 100644 src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlaceHolder.java create mode 100644 src/main/java/dk/aau/cs/verification/observations/expressions/ObsSubtract.java create mode 100644 src/main/java/net/tapaal/gui/petrinet/dialog/ObservationDialog.java create mode 100644 src/main/java/net/tapaal/gui/petrinet/dialog/ObservationListDialog.java create mode 100644 src/main/java/net/tapaal/helpers/Enabler.java diff --git a/src/main/java/dk/aau/cs/TCTL/visitors/SMCQueryVisitor.java b/src/main/java/dk/aau/cs/TCTL/visitors/SMCQueryVisitor.java index 7d9d406a5..f1365de95 100644 --- a/src/main/java/dk/aau/cs/TCTL/visitors/SMCQueryVisitor.java +++ b/src/main/java/dk/aau/cs/TCTL/visitors/SMCQueryVisitor.java @@ -1,7 +1,10 @@ package dk.aau.cs.TCTL.visitors; +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 { @@ -14,6 +17,10 @@ public class SMCQueryVisitor extends LTLQueryVisitor { private static final String XML_CONFIDENCE_TAG = "confidence"; 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); @@ -21,7 +28,13 @@ public String getXMLQueryFor(TCTLAbstractProperty property, String queryName, SM } public void buildXMLQuery(TCTLAbstractProperty property, String queryName, SMCSettings settings) { - xmlQuery.append(startTag(XML_PROP) + queryInfo(queryName) + smcTag(settings) + startTag(XML_FORMULA)); + xmlQuery.append(startTag(XML_PROP) + queryInfo(queryName) + smcTag(settings)); + + if (!settings.getObservations().isEmpty()) { + xmlQuery.append(observationTag(settings.getObservations())); + } + + xmlQuery.append(startTag(XML_FORMULA)); property.accept(this, null); xmlQuery.append(endTag(XML_FORMULA) + endTag(XML_PROP)); } @@ -44,6 +57,23 @@ private String smcTag(SMCSettings settings) { return emptyElement(tagContent); } + private String observationTag(List observations) { + String observationXml = startTag(XML_OBSERVATIONS); + + for (Observation observation : observations) { + String tagContent = XML_WATCH; + tagContent += tagAttribute(XML_WATCH_ID, observation.getId()); + tagContent += tagAttribute(XML_WATCH_NAME, observation.getName()); + + observationXml += startTag(tagContent); + observationXml += endTag(XML_WATCH); + } + + observationXml += endTag(XML_OBSERVATIONS); + + return observationXml; + } + private String tagAttribute(String name, String value) { return " " + name + "=\"" + 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 index 855a1ec5e..21ba7a861 100644 --- a/src/main/java/dk/aau/cs/io/queries/TAPNQueryLoader.java +++ b/src/main/java/dk/aau/cs/io/queries/TAPNQueryLoader.java @@ -8,6 +8,7 @@ import dk.aau.cs.TCTL.XMLParsing.XMLLTLQueryParser; import dk.aau.cs.verification.SMCSettings; import dk.aau.cs.verification.SMCTraceType; +import dk.aau.cs.verification.observations.Observation; import org.w3c.dom.Document; import org.w3c.dom.Element; @@ -113,9 +114,27 @@ private TAPNQuery parseTAPNQuery(Element queryElement, TimedArcPetriNetNetwork n if(smcTagList.getLength() > 0) { Element settingsNode = (Element) smcTagList.item(0); smcSettings = parseSmcSettings(settingsNode); + NodeList observationsList = queryElement.getElementsByTagName("observations"); + if (observationsList.getLength() > 0) { + Element observationsNode = (Element)observationsList.item(0); + NodeList watchList = observationsNode.getElementsByTagName("watch"); + + List observations = new ArrayList<>(); + for (int i = 0; i < watchList.getLength(); ++i) { + Element watch = (Element)watchList.item(i); + String id = watch.getAttribute("id"); + String name = watch.getAttribute("name"); + + Observation observation = new Observation(name, id); + observations.add(observation); + } + + smcSettings.setObservations(observations); + } } else { smcSettings = SMCSettings.Default(); } + query = parseLTLQueryProperty(queryElement); } else if (queryElement.hasAttribute("type") && queryElement.getAttribute("type").equals("LTL")) { query = parseLTLQueryProperty(queryElement); diff --git a/src/main/java/dk/aau/cs/verification/SMCSettings.java b/src/main/java/dk/aau/cs/verification/SMCSettings.java index d64910c27..f40063d16 100644 --- a/src/main/java/dk/aau/cs/verification/SMCSettings.java +++ b/src/main/java/dk/aau/cs/verification/SMCSettings.java @@ -1,5 +1,10 @@ package dk.aau.cs.verification; +import java.util.ArrayList; +import java.util.List; + +import dk.aau.cs.verification.observations.Observation; + public class SMCSettings { public int timeBound; @@ -12,6 +17,8 @@ public class SMCSettings { public boolean compareToFloat; public float geqThan; + private List observations; + public static SMCSettings Default() { SMCSettings settings = new SMCSettings(); settings.timeBound = 1000; @@ -23,6 +30,7 @@ public static SMCSettings Default() { settings.estimationIntervalWidth = 0.05f; settings.compareToFloat = false; settings.geqThan = 0.5f; + settings.setObservations(new ArrayList<>()); return settings; } @@ -56,4 +64,12 @@ public int getTimeBound() { public int getStepBound() { return stepBound; } + + public void setObservations(List observations) { + this.observations = observations; + } + + public List getObservations() { + return observations; + } } diff --git a/src/main/java/dk/aau/cs/verification/observations/Observation.java b/src/main/java/dk/aau/cs/verification/observations/Observation.java new file mode 100644 index 000000000..bd12698ed --- /dev/null +++ b/src/main/java/dk/aau/cs/verification/observations/Observation.java @@ -0,0 +1,48 @@ +package dk.aau.cs.verification.observations; + +import java.util.UUID; + +import dk.aau.cs.verification.observations.expressions.ObsExpression; +import dk.aau.cs.verification.observations.expressions.ObsPlaceHolder; + +public class Observation { + private final String id; + + private String name; + + private ObsExpression expression = new ObsPlaceHolder(); + + public Observation(String name, String id) { + this.name = name; + this.id = id; + } + + public Observation(String name) { + this(name, UUID.randomUUID().toString()); + } + + public String getName() { + return name; + } + + public String getId() { + return id; + } + + public ObsExpression getExpression() { + return expression; + } + + public void setName(String name) { + this.name = name; + } + + public void setExpression(ObsExpression expression) { + this.expression = expression; + } + + @Override + public String toString() { + return name; + } +} diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsAdd.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsAdd.java new file mode 100644 index 000000000..d9843ce89 --- /dev/null +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsAdd.java @@ -0,0 +1,16 @@ +package dk.aau.cs.verification.observations.expressions; + +public class ObsAdd extends ObsOperator { + public ObsAdd(ObsExpression left, ObsExpression right) { + super(left, right); + } + + public ObsAdd() { + super(); + } + + @Override + protected String getOperator() { + return "+"; + } +} diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsConstant.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsConstant.java new file mode 100644 index 000000000..760926cd6 --- /dev/null +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsConstant.java @@ -0,0 +1,19 @@ +package dk.aau.cs.verification.observations.expressions; + +public class ObsConstant extends ObsLeaf { + private final int tokens; + + public ObsConstant(int tokens) { + this.tokens = tokens; + } + + @Override + public String toString() { + return Integer.toString(tokens); + } + + @Override + public ObsExpression copy() { + return new ObsConstant(tokens); + } +} diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsExprPosition.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsExprPosition.java new file mode 100644 index 000000000..8d2fdc404 --- /dev/null +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsExprPosition.java @@ -0,0 +1,29 @@ +package dk.aau.cs.verification.observations.expressions; + +public class ObsExprPosition { + private final int start; + private final int end; + private final ObsExpression object; + + public ObsExprPosition(int start, int end, ObsExpression object) { + this.start = start; + this.end = end; + this.object = object; + } + + public int getStart() { + return start; + } + + public int getEnd() { + return end; + } + + public ObsExpression getObject() { + return object; + } + + public ObsExprPosition addOffset(int offset) { + return new ObsExprPosition(start + offset, end + offset, object); + } +} \ No newline at end of file diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsExpression.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsExpression.java new file mode 100644 index 000000000..539b0f8bb --- /dev/null +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsExpression.java @@ -0,0 +1,8 @@ +package dk.aau.cs.verification.observations.expressions; + +public interface ObsExpression { + ObsExpression copy(); + ObsExprPosition getObjectPosition(int index); + boolean isOperator(); + boolean isLeaf(); +} diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsLeaf.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsLeaf.java new file mode 100644 index 000000000..4f2ed956d --- /dev/null +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsLeaf.java @@ -0,0 +1,18 @@ +package dk.aau.cs.verification.observations.expressions; + +public abstract class ObsLeaf implements ObsExpression { + @Override + public ObsExprPosition getObjectPosition(int index) { + return new ObsExprPosition(0, toString().length(), this); + } + + @Override + public boolean isOperator() { + return false; + } + + @Override + public boolean isLeaf() { + return true; + } +} diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsMultiply.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsMultiply.java new file mode 100644 index 000000000..caae17b32 --- /dev/null +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsMultiply.java @@ -0,0 +1,16 @@ +package dk.aau.cs.verification.observations.expressions; + +public class ObsMultiply extends ObsOperator { + public ObsMultiply(ObsExpression left, ObsExpression right) { + super(left, right); + } + + public ObsMultiply() { + super(); + } + + @Override + protected String getOperator() { + return "*"; + } +} diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsOperator.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsOperator.java new file mode 100644 index 000000000..ca9e4e57d --- /dev/null +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsOperator.java @@ -0,0 +1,108 @@ +package dk.aau.cs.verification.observations.expressions; + +public abstract class ObsOperator implements ObsExpression { + protected ObsExpression left; + protected ObsExpression right; + protected ObsExpression parent; + + protected ObsOperator(ObsExpression left, ObsExpression right) { + this.left = left; + this.right = right; + } + + protected ObsOperator() { + this(new ObsPlaceHolder(), new ObsPlaceHolder()); + } + + public void insertLeftMost(ObsExpression expr) { + if (expr.isOperator()) { + ((ObsOperator)expr).parent = this; + } + + if (left.isOperator()) { + ((ObsOperator)left).insertLeftMost(expr); + } else { + left = expr; + } + } + + public void replace(ObsExpression selectedExpr, ObsExpression newExpr) { + if (left.equals(selectedExpr) || right.equals(selectedExpr)) { + if (newExpr.isOperator()) { + ((ObsOperator)newExpr).parent = this; + if (selectedExpr.isOperator()) { + ((ObsOperator)newExpr).left = ((ObsOperator)selectedExpr).left; + ((ObsOperator)newExpr).right = ((ObsOperator)selectedExpr).right; + } + } + + if (left.equals(selectedExpr)) { + left = newExpr; + } else if (right.equals(selectedExpr)) { + right = newExpr; + } + } + + if (left.isOperator()) { + ((ObsOperator)left).replace(selectedExpr, newExpr); + } + + if (right.isOperator()) { + ((ObsOperator)right).replace(selectedExpr, newExpr); + } + } + + @Override + public ObsExpression copy() { + try { + return getClass() + .getConstructor(ObsExpression.class, ObsExpression.class) + .newInstance(left.copy(), right.copy()); + } catch (Exception e) { + throw new RuntimeException("Failed to copy ObsOperator", e); + } + } + + protected boolean addParenthesis() { + return parent != null && parent.getClass() != getClass(); + } + + @Override + public ObsExprPosition getObjectPosition(int index) { + int leftLen = left.toString().length(); + int rightLen = right.toString().length(); + int totalLen = toString().length(); + int thisLen = totalLen - leftLen - rightLen; + + int parenOffset = addParenthesis() ? 1 : 0; + if (index < leftLen + parenOffset) { + return left.getObjectPosition(index - parenOffset).addOffset(parenOffset); + } else if (index >= leftLen + thisLen - parenOffset) { + return right.getObjectPosition(index - leftLen - thisLen).addOffset(leftLen + thisLen - parenOffset); + } + + return new ObsExprPosition(0, totalLen, this); + } + + @Override + public boolean isOperator() { + return true; + } + + @Override + public boolean isLeaf() { + return false; + } + + @Override + public String toString() { + String operator = getOperator(); + if (addParenthesis()) { + return "(" + left + " " + operator + " " + right + ")"; + } + + return left + " " + operator + " " + right; + } + + protected abstract String getOperator(); +} \ No newline at end of file diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlace.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlace.java new file mode 100644 index 000000000..1990f89e6 --- /dev/null +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlace.java @@ -0,0 +1,21 @@ +package dk.aau.cs.verification.observations.expressions; + +import dk.aau.cs.model.tapn.TimedPlace; + +public class ObsPlace extends ObsLeaf { + private final TimedPlace place; + + public ObsPlace(TimedPlace place) { + this.place = place; + } + + @Override + public String toString() { + return place.name(); + } + + @Override + public ObsExpression copy() { + return new ObsPlace(place); + } +} diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlaceHolder.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlaceHolder.java new file mode 100644 index 000000000..47a7e93a4 --- /dev/null +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlaceHolder.java @@ -0,0 +1,13 @@ +package dk.aau.cs.verification.observations.expressions; + +public class ObsPlaceHolder extends ObsLeaf { + @Override + public String toString() { + return "<*>"; + } + + @Override + public ObsExpression copy() { + return new ObsPlaceHolder(); + } +} \ No newline at end of file diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsSubtract.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsSubtract.java new file mode 100644 index 000000000..e8aac0e21 --- /dev/null +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsSubtract.java @@ -0,0 +1,16 @@ +package dk.aau.cs.verification.observations.expressions; + +public class ObsSubtract extends ObsOperator { + public ObsSubtract(ObsExpression left, ObsExpression right) { + super(left, right); + } + + public ObsSubtract() { + super(); + } + + @Override + protected String getOperator() { + return "-"; + } +} diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/ObservationDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/ObservationDialog.java new file mode 100644 index 000000000..88b649ea9 --- /dev/null +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/ObservationDialog.java @@ -0,0 +1,367 @@ +package net.tapaal.gui.petrinet.dialog; + +import javax.swing.BorderFactory; +import javax.swing.DefaultListModel; +import javax.swing.JButton; +import javax.swing.JComboBox; +import javax.swing.JLabel; +import javax.swing.JPanel; +import javax.swing.JScrollPane; +import javax.swing.JTextField; +import javax.swing.JTextPane; +import javax.swing.ScrollPaneConstants; +import javax.swing.text.MutableAttributeSet; +import javax.swing.text.SimpleAttributeSet; +import javax.swing.text.StyleConstants; +import javax.swing.text.StyledDocument; + +import dk.aau.cs.model.tapn.TimedArcPetriNet; +import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork; +import dk.aau.cs.verification.observations.Observation; +import dk.aau.cs.verification.observations.expressions.ObsExprPosition; +import dk.aau.cs.verification.observations.expressions.ObsAdd; +import dk.aau.cs.verification.observations.expressions.ObsExpression; +import dk.aau.cs.verification.observations.expressions.ObsMultiply; +import dk.aau.cs.verification.observations.expressions.ObsOperator; +import dk.aau.cs.verification.observations.expressions.ObsPlaceHolder; +import dk.aau.cs.verification.observations.expressions.ObsSubtract; +import net.tapaal.helpers.Enabler; +import net.tapaal.swinghelpers.CustomJSpinner; +import pipe.gui.TAPAALGUI; +import pipe.gui.swingcomponents.EscapableDialog; +import java.awt.GridBagLayout; +import java.awt.Insets; +import java.awt.event.MouseAdapter; +import java.awt.event.MouseEvent; +import java.awt.Dimension; +import java.awt.GridBagConstraints; + +public class ObservationDialog extends EscapableDialog { + private static final String SHARED = "Shared"; + + private final DefaultListModel observationModel; + private final Observation observation; + + private JPanel placesPanel; + private JPanel constantsPanel; + + private ObsExpression currentExpr; + private ObsExpression selectedExpr; + + private boolean isNewObservation; + private boolean isEditing; + + private JButton saveButton; + + private final TimedArcPetriNetNetwork tapnNetwork; + private final JTextPane expressionField = new JTextPane(); + + public ObservationDialog(TimedArcPetriNetNetwork tapnNetwork, DefaultListModel observationModel, Observation observation) { + super(TAPAALGUI.getApp(), observation.getName(), true); + this.tapnNetwork = tapnNetwork; + this.observationModel = observationModel; + this.observation = observation; + this.currentExpr = observation.getExpression().copy(); + + init(); + } + + public ObservationDialog(TimedArcPetriNetNetwork tapnNetwork, DefaultListModel observationModel) { + this(tapnNetwork, observationModel, new Observation("New Observation")); + isNewObservation = true; + } + + private void init() { + setSize(1200, 425); + setResizable(false); + + setLayout(new GridBagLayout()); + GridBagConstraints gbc = new GridBagConstraints(); + gbc.gridx = 0; + gbc.gridy = 0; + gbc.insets = new Insets(10, 10, 10, 10); + gbc.anchor = GridBagConstraints.WEST; + + JPanel namePanel = new JPanel(); + namePanel.setLayout(new GridBagLayout()); + + JLabel nameLabel = new JLabel("Observation name:"); + JTextField nameField = new JTextField(observation.getName(), 25); + + GridBagConstraints nameGbc = new GridBagConstraints(); + nameGbc.gridx = 0; + nameGbc.gridy = 0; + nameGbc.anchor = GridBagConstraints.WEST; + nameGbc.insets = new Insets(0, 0, 0, 5); + namePanel.add(nameLabel, nameGbc); + + ++nameGbc.gridx; + nameGbc.insets = new Insets(0, 0, 0, 0); + namePanel.add(nameField, nameGbc); + + add(namePanel, gbc); + + StyledDocument doc = expressionField.getStyledDocument(); + MutableAttributeSet standard = new SimpleAttributeSet(); + StyleConstants.setAlignment(standard, StyleConstants.ALIGN_CENTER); + StyleConstants.setFontSize(standard, 14); + doc.setParagraphAttributes(0, 0, standard, true); + expressionField.setText(currentExpr.toString()); + expressionField.setEditable(false); + + expressionField.addMouseListener(new MouseAdapter() { + @Override + public void mouseClicked(MouseEvent e) { + int pos = expressionField.viewToModel2D(e.getPoint()); + ObsExprPosition exprPos = currentExpr.getObjectPosition(pos - 1); + expressionField.select(exprPos.getStart(), exprPos.getEnd()); + selectedExpr = exprPos.getObject(); + } + }); + + JScrollPane expressionScrollPane = new JScrollPane(expressionField); + expressionScrollPane.setVerticalScrollBarPolicy(ScrollPaneConstants.VERTICAL_SCROLLBAR_AS_NEEDED); + Dimension d = new Dimension(900, 80); + expressionScrollPane.setPreferredSize(d); + expressionScrollPane.setMinimumSize(d); + + JPanel operationsPanel = new JPanel(); + operationsPanel.setLayout(new GridBagLayout()); + operationsPanel.setBorder(BorderFactory.createTitledBorder("Operations")); + JButton plusButton = new JButton("+"); + JButton minusButton = new JButton("-"); + JButton multiplyButton = new JButton("*"); + JButton divideButton = new JButton("/"); + divideButton.setVisible(false); // Division is not supported yet + + plusButton.addActionListener(e -> updateExpression(new ObsAdd())); + minusButton.addActionListener(e -> updateExpression(new ObsSubtract())); + multiplyButton.addActionListener(e -> updateExpression(new ObsMultiply())); + + GridBagConstraints operationsGbc = new GridBagConstraints(); + operationsGbc.gridx = 0; + operationsGbc.gridy = 0; + operationsGbc.weightx = 1; + operationsGbc.fill = GridBagConstraints.HORIZONTAL; + operationsGbc.insets = new Insets(0, 10, 0, 10); + operationsPanel.add(plusButton, operationsGbc); + ++operationsGbc.gridy; + operationsGbc.insets = new Insets(5, 10, 0, 10); + operationsPanel.add(minusButton, operationsGbc); + ++operationsGbc.gridy; + operationsPanel.add(multiplyButton, operationsGbc); + ++operationsGbc.gridy; + operationsPanel.add(divideButton, operationsGbc); + + placesPanel = new JPanel(); + placesPanel.setLayout(new GridBagLayout()); + placesPanel.setBorder(BorderFactory.createTitledBorder("Places")); + + JComboBox templateComboBox = new JComboBox<>(); + tapnNetwork.activeTemplates().forEach(templateComboBox::addItem); + if (tapnNetwork.sharedPlaces().size() > 0) { + templateComboBox.addItem(SHARED); + } + + JComboBox placeComboBox = new JComboBox<>(); + templateComboBox.addActionListener(e -> { + placeComboBox.removeAllItems(); + if (templateComboBox.getSelectedItem().equals(SHARED)) { + tapnNetwork.sharedPlaces().forEach(place -> placeComboBox.addItem(place.name())); + } else { + TimedArcPetriNet template = (TimedArcPetriNet) templateComboBox.getSelectedItem(); + template.places().forEach(place -> placeComboBox.addItem(place.name())); + } + }); + + // Initialize the placeComboBox with the first template + if (templateComboBox.getItemCount() > 0) { + templateComboBox.setSelectedIndex(0); + } + + JButton addPlaceButton = new JButton("Add place"); + + GridBagConstraints placesGbc = new GridBagConstraints(); + placesGbc.gridx = 0; + placesGbc.gridy = 0; + placesGbc.weightx = 1; + placesGbc.fill = GridBagConstraints.HORIZONTAL; + placesGbc.insets = new Insets(0, 10, 0, 10); + placesPanel.add(templateComboBox, placesGbc); + ++placesGbc.gridy; + placesGbc.insets = new Insets(5, 10, 0, 10); + placesPanel.add(placeComboBox, placesGbc); + ++placesGbc.gridy; + placesPanel.add(addPlaceButton, placesGbc); + + Enabler.setAllEnabled(placesPanel, false); + + constantsPanel = new JPanel(); + constantsPanel.setLayout(new GridBagLayout()); + constantsPanel.setBorder(BorderFactory.createTitledBorder("Constants")); + + CustomJSpinner constantSpinner = new CustomJSpinner(0, 0, Integer.MAX_VALUE); + JButton addConstantButton = new JButton("Add constant"); + + GridBagConstraints constantsGbc = new GridBagConstraints(); + constantsGbc.gridx = 0; + constantsGbc.gridy = 0; + constantsGbc.weightx = 1; + constantsGbc.fill = GridBagConstraints.HORIZONTAL; + constantsGbc.insets = new Insets(0, 10, 0, 10); + constantsPanel.add(constantSpinner, constantsGbc); + ++constantsGbc.gridy; + constantsGbc.insets = new Insets(5, 10, 0, 10); + constantsPanel.add(addConstantButton, constantsGbc); + + Enabler.setAllEnabled(constantsPanel, false); + + JPanel editingPanel = new JPanel(); + editingPanel.setLayout(new GridBagLayout()); + editingPanel.setBorder(BorderFactory.createTitledBorder("Editing")); + + JButton undoButton = new JButton("Undo"); + undoButton.setEnabled(false); + + JButton redoButton = new JButton("Redo"); + redoButton.setEnabled(false); + + JButton deleteSelection = new JButton("Delete Selection"); + deleteSelection.setEnabled(false); + JButton resetExpression = new JButton("Reset Expression"); + + resetExpression.addActionListener(e -> { + currentExpr = new ObsPlaceHolder(); + expressionField.setText(currentExpr.toString()); + }); + + JButton editExpression = new JButton("Edit Expression"); + + editExpression.addActionListener(e -> { + isEditing = !isEditing; + + Enabler.setAllEnabled(operationsPanel, !isEditing); + Enabler.setAllEnabled(placesPanel, !isEditing); + Enabler.setAllEnabled(constantsPanel, !isEditing); + saveButton.setEnabled(!isEditing); + expressionField.setEditable(isEditing); + + if (isEditing) { + resetExpression.setText("Parse Expression"); + editExpression.setText("Cancel"); + } else { + resetExpression.setText("Reset Expression"); + editExpression.setText("Edit Expression"); + } + }); + + GridBagConstraints editingGbc = new GridBagConstraints(); + editingGbc.gridx = 0; + editingGbc.gridy = 0; + editingGbc.weightx = 1; + editingGbc.fill = GridBagConstraints.HORIZONTAL; + editingGbc.insets = new Insets(0, 10, 0, 5); + editingPanel.add(undoButton, editingGbc); + ++editingGbc.gridx; + editingGbc.insets = new Insets(0, 0, 0, 10); + editingPanel.add(redoButton, editingGbc); + editingGbc.gridx = 0; + ++editingGbc.gridy; + editingGbc.gridwidth = 2; + editingGbc.insets = new Insets(5, 10, 0, 10); + editingPanel.add(deleteSelection, editingGbc); + ++editingGbc.gridy; + editingPanel.add(resetExpression, editingGbc); + ++editingGbc.gridy; + editingPanel.add(editExpression, editingGbc); + + JPanel expressionPanel = new JPanel(); + expressionPanel.setLayout(new GridBagLayout()); + expressionPanel.setBorder(BorderFactory.createTitledBorder("Observation Expression")); + + GridBagConstraints expressionGbc = new GridBagConstraints(); + expressionGbc.gridx = 0; + expressionGbc.gridy = 0; + expressionGbc.weightx = 1; + expressionGbc.weighty = 1; + expressionGbc.fill = GridBagConstraints.BOTH; + expressionGbc.insets = new Insets(0, 30, 0, 30); + expressionGbc.gridwidth = 4; + expressionPanel.add(expressionScrollPane, expressionGbc); + expressionGbc.gridwidth = 1; + ++expressionGbc.gridy; + expressionGbc.insets = new Insets(0, 30, 0, 0); + expressionPanel.add(operationsPanel, expressionGbc); + ++expressionGbc.gridx; + expressionGbc.insets = new Insets(0, 0, 0, 0); + expressionPanel.add(placesPanel, expressionGbc); + ++expressionGbc.gridx; + expressionPanel.add(constantsPanel, expressionGbc); + ++expressionGbc.gridx; + expressionGbc.insets = new Insets(0, 0, 0, 30); + expressionPanel.add(editingPanel, expressionGbc); + + ++gbc.gridy; + gbc.weightx = 1; + gbc.weighty = 1; + gbc.fill = GridBagConstraints.HORIZONTAL; + add(expressionPanel, gbc); + + JPanel buttonPanel = new JPanel(); + buttonPanel.setLayout(new GridBagLayout()); + JButton cancelButton = new JButton("Cancel"); + saveButton = new JButton("Save"); + + cancelButton.addActionListener(e -> { + dispose(); + }); + + saveButton.addActionListener(e -> { + observation.setName(nameField.getText()); + + if (isNewObservation) { + observationModel.addElement(observation); + } else { + observationModel.setElementAt(observation, observationModel.indexOf(observation)); + } + + dispose(); + }); + + GridBagConstraints buttonGbc = new GridBagConstraints(); + buttonGbc.gridx = 0; + buttonGbc.gridy = 0; + buttonGbc.weightx = 1; + buttonGbc.anchor = GridBagConstraints.EAST; + buttonGbc.insets = new Insets(0, 0, 0, 5); + buttonPanel.add(cancelButton, buttonGbc); + buttonGbc.insets = new Insets(0, 0, 0, 0); + ++buttonGbc.gridx; + buttonPanel.add(saveButton, buttonGbc); + + ++gbc.gridy; + gbc.anchor = GridBagConstraints.EAST; + gbc.fill = GridBagConstraints.NONE; + gbc.weightx = 0; + gbc.weighty = 0; + add(buttonPanel, gbc); + + pack(); + } + + private void updateExpression(ObsExpression newExpr) { + String selectedText = expressionField.getSelectedText(); + String fullText = expressionField.getText(); + if (selectedText != null && + !selectedText.equals(fullText) && + currentExpr.isOperator()) { + ((ObsOperator)currentExpr).replace(selectedExpr, newExpr); + } else if (currentExpr.isOperator() && selectedText == null) { + ((ObsOperator)currentExpr).insertLeftMost(newExpr); + } else { + currentExpr = newExpr; + } + + expressionField.setText(currentExpr.toString()); + } +} diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/ObservationListDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/ObservationListDialog.java new file mode 100644 index 000000000..4612f5527 --- /dev/null +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/ObservationListDialog.java @@ -0,0 +1,162 @@ +package net.tapaal.gui.petrinet.dialog; + +import javax.swing.DefaultListModel; +import javax.swing.JButton; +import javax.swing.JList; +import javax.swing.JPanel; +import javax.swing.JScrollPane; +import javax.swing.event.ListDataListener; +import javax.swing.event.ListDataEvent; + +import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork; +import dk.aau.cs.verification.observations.Observation; +import pipe.gui.TAPAALGUI; +import pipe.gui.swingcomponents.EscapableDialog; + +import java.awt.Dimension; +import java.awt.GridBagLayout; +import java.awt.Insets; +import java.awt.GridBagConstraints; +import java.util.List; + +public class ObservationListDialog extends EscapableDialog { + private final TimedArcPetriNetNetwork tapnNetwork; + + private final List observations; + + public ObservationListDialog(TimedArcPetriNetNetwork tapnNetwork, List observations) { + super(TAPAALGUI.getApp(), "Observations", true); + this.tapnNetwork = tapnNetwork; + this.observations = observations; + + init(); + } + + private void init() { + setSize(500, 350); + setResizable(false); + + setLayout(new GridBagLayout()); + + JPanel observationPanel = new JPanel(); + observationPanel.setLayout(new GridBagLayout()); + DefaultListModel listModel = new DefaultListModel<>(); + for (Observation observation : observations) { + listModel.addElement(observation); + } + + listModel.addListDataListener(new ListDataListener() { + @Override + public void intervalAdded(ListDataEvent e) { + for (int i = e.getIndex0(); i <= e.getIndex1(); ++i) { + observations.add(i, listModel.getElementAt(i)); + } + } + + @Override + public void intervalRemoved(ListDataEvent e) { + for (int i = e.getIndex0(); i <= e.getIndex1(); ++i) { + observations.remove(i); + } + } + + @Override + public void contentsChanged(ListDataEvent e) { + for (int i = e.getIndex0(); i <= e.getIndex1(); ++i) { + observations.set(i, listModel.getElementAt(i)); + } + } + }); + + JList observationList = new JList<>(listModel); + + JScrollPane observationScrollPane = new JScrollPane(observationList); + observationScrollPane.setPreferredSize(new Dimension(500, observationScrollPane.getPreferredSize().height)); + + JButton editButton = new JButton("Edit"); + editButton.setEnabled(false); + editButton.addActionListener(e -> { + int selectedIndex = observationList.getSelectedIndex(); + if (selectedIndex != -1) { + ObservationDialog observationDialog = new ObservationDialog(tapnNetwork, listModel, listModel.get(selectedIndex)); + + observationDialog.setLocationRelativeTo(this); + observationDialog.setVisible(true); + } + }); + + JButton removeButton = new JButton("Remove"); + removeButton.setEnabled(false); + removeButton.addActionListener(e -> { + for (Observation observation : observationList.getSelectedValuesList()) { + listModel.removeElement(observation); + } + }); + + JButton newButton = new JButton("New"); + newButton.addActionListener(e -> { + ObservationDialog observationDialog = new ObservationDialog(tapnNetwork, listModel); + observationDialog.setLocationRelativeTo(this); + observationDialog.setVisible(true); + }); + + observationList.addListSelectionListener(e -> { + if (!e.getValueIsAdjusting()) { + boolean elemIsSelected = observationList.getSelectedIndex() != -1; + editButton.setEnabled(elemIsSelected); + removeButton.setEnabled(elemIsSelected); + } + }); + + GridBagConstraints observationGbc = new GridBagConstraints(); + observationGbc.gridx = 0; + observationGbc.gridy = 0; + observationGbc.weightx = 1; + observationGbc.weighty = 1; + observationGbc.fill = GridBagConstraints.BOTH; + observationGbc.gridwidth = 3; + observationPanel.add(observationScrollPane, observationGbc); + ++observationGbc.gridy; + observationGbc.gridwidth = 1; + observationGbc.fill = GridBagConstraints.HORIZONTAL; + observationPanel.add(editButton, observationGbc); + ++observationGbc.gridx; + observationPanel.add(removeButton, observationGbc); + ++observationGbc.gridx; + observationPanel.add(newButton, observationGbc); + + GridBagConstraints gbc = new GridBagConstraints(); + gbc.gridx = 0; + gbc.gridy = 0; + gbc.weightx = 1; + gbc.weighty = 1; + gbc.fill = GridBagConstraints.BOTH; + gbc.insets = new Insets(10, 10, 10, 10); + + add(observationPanel, gbc); + + JPanel buttonPanel = new JPanel(); + buttonPanel.setLayout(new GridBagLayout()); + + JButton okButton = new JButton("OK"); + + okButton.addActionListener(e -> { + dispose(); + }); + + GridBagConstraints buttonGbc = new GridBagConstraints(); + + buttonGbc.gridx = 0; + buttonGbc.gridy = 0; + buttonGbc.anchor = GridBagConstraints.EAST; + buttonPanel.add(okButton, buttonGbc); + + ++gbc.gridy; + gbc.anchor = GridBagConstraints.EAST; + gbc.fill = GridBagConstraints.NONE; + gbc.weightx = 0; + add(buttonPanel, gbc); + + pack(); + } +} diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 75f210b54..45764522e 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -43,6 +43,7 @@ import dk.aau.cs.model.CPN.Variable; import dk.aau.cs.model.tapn.*; import dk.aau.cs.verification.VerifyTAPN.*; +import dk.aau.cs.verification.observations.Observation; import net.tapaal.gui.petrinet.verification.*; import net.tapaal.swinghelpers.CustomJSpinner; import pipe.gui.petrinet.dataLayer.DataLayer; @@ -52,6 +53,7 @@ import net.tapaal.gui.petrinet.verification.TAPNQuery.SearchOption; import net.tapaal.gui.petrinet.verification.TAPNQuery.TraceOption; import net.tapaal.gui.petrinet.verification.TAPNQuery.VerificationType; +import net.tapaal.helpers.Enabler; import pipe.gui.*; import dk.aau.cs.TCTL.Parsing.TAPAALQueryParser; import dk.aau.cs.approximation.OverApproximation; @@ -256,6 +258,7 @@ public enum QueryDialogueOption { private boolean smcMustUpdateTime = true; private boolean doingBenchmark = false; private RunVerificationBase benchmarkThread = null; + private java.util.List smcObservations; // Buttons in the bottom of the dialogue private JPanel buttonPanel; @@ -854,6 +857,8 @@ private void setSMCSettings(SMCSettings settings) { smcTimeBoundInfinite.setEnabled(!smcStepBoundInfinite.isSelected()); smcStepBoundInfinite.setEnabled(!smcTimeBoundInfinite.isSelected()); + smcObservations = settings.getObservations(); + smcConfidence.setText(String.valueOf(settings.confidence)); if(!doingBenchmark) smcEstimationIntervalWidth.setText(precisionFormat.format(settings.estimationIntervalWidth)); @@ -1620,8 +1625,9 @@ private void disableEditingButtons() { private void enableEditingButtons() { refreshUndoRedo(); - if (currentSelection != null) - deleteButton.setEnabled(true); + if (currentSelection != null) { + deleteButton.setEnabled(currentSelection != null); + } } private void returnFromManualEdit(TCTLAbstractProperty newQuery) { @@ -3076,6 +3082,17 @@ public void focusLost(FocusEvent focusEvent) { guiDialog.pack(); }); + JButton smcObservationsButton = new JButton("Edit observations"); + smcObservationsButton.addActionListener(evt -> { + ObservationListDialog dialog = new ObservationListDialog(tapnNetwork, smcObservations); + dialog.setLocationRelativeTo(guiDialog); + dialog.setVisible(true); + }); + + gbc.gridx = 0; + gbc.gridy = 1; + smcSettingsPanel.add(smcObservationsButton, gbc); + GridBagConstraints gridBagConstraints = new GridBagConstraints(); gridBagConstraints.gridx = 0; gridBagConstraints.gridy = 3; @@ -5343,16 +5360,16 @@ private void showEngineHelp() { } private void setVerificationOptionsEnabled(boolean isEnabled) { - setAllEnabled(reductionOptionsPanel, isEnabled); + Enabler.setAllEnabled(reductionOptionsPanel, isEnabled); if (unfoldingOptionsPanel != null) { - setAllEnabled(unfoldingOptionsPanel, isEnabled); + Enabler.setAllEnabled(unfoldingOptionsPanel, isEnabled); } - setAllEnabled(traceOptionsPanel, isEnabled); - setAllEnabled(boundednessCheckPanel, isEnabled); - setAllEnabled(searchOptionsPanel, isEnabled); - setAllEnabled(smcTracePanel, isEnabled); + Enabler.setAllEnabled(traceOptionsPanel, isEnabled); + Enabler.setAllEnabled(boundednessCheckPanel, isEnabled); + Enabler.setAllEnabled(searchOptionsPanel, isEnabled); + Enabler.setAllEnabled(smcTracePanel, isEnabled); smcVerificationTypeLabel.setEnabled(isEnabled); smcVerificationType.setEnabled(isEnabled); @@ -5362,18 +5379,6 @@ private void setVerificationOptionsEnabled(boolean isEnabled) { setEnabledOptionsAccordingToCurrentReduction(); } - // Enables or disables the container + all children recursively - private void setAllEnabled(Container container, boolean isEnabled) { - for (Component component : container.getComponents()) { - component.setEnabled(isEnabled); - if (component instanceof Container) { - setAllEnabled((Container) component, isEnabled); - } - } - - container.setEnabled(isEnabled); - } - protected void setEnabledOptionsAccordingToCurrentReduction() { refreshQueryEditingButtons(); diff --git a/src/main/java/net/tapaal/helpers/Enabler.java b/src/main/java/net/tapaal/helpers/Enabler.java new file mode 100644 index 000000000..483bad7c8 --- /dev/null +++ b/src/main/java/net/tapaal/helpers/Enabler.java @@ -0,0 +1,22 @@ +package net.tapaal.helpers; + +import java.awt.Component; +import java.awt.Container; + +public class Enabler { + /** + * Set all components in a container to be enabled or disabled. + * @param container The container to set the components of. + * @param isEnabled Whether the components should be enabled or disabled. + */ + public static void setAllEnabled(Container container, boolean isEnabled) { + for (Component component : container.getComponents()) { + component.setEnabled(isEnabled); + if (component instanceof Container) { + setAllEnabled((Container) component, isEnabled); + } + } + + container.setEnabled(isEnabled); + } +} From add0901164c34b16fb87de89ca35febd246f1529 Mon Sep 17 00:00:00 2001 From: Mikkel Tygesen Date: Fri, 15 Nov 2024 19:37:39 +0100 Subject: [PATCH 2/7] everything besides manual edit and xml working --- .../aau/cs/TCTL/visitors/SMCQueryVisitor.java | 2 - .../dk/aau/cs/io/queries/TAPNQueryLoader.java | 3 +- .../observations/Observation.java | 15 +- .../observations/expressions/ObsConstant.java | 10 +- .../expressions/ObsExpression.java | 1 + .../observations/expressions/ObsLeaf.java | 5 + .../observations/expressions/ObsOperator.java | 5 + .../observations/expressions/ObsPlace.java | 8 +- .../expressions/ObsPlaceHolder.java | 5 + .../petrinet/dialog/ObservationDialog.java | 145 +++++++++++++++--- 10 files changed, 151 insertions(+), 48 deletions(-) diff --git a/src/main/java/dk/aau/cs/TCTL/visitors/SMCQueryVisitor.java b/src/main/java/dk/aau/cs/TCTL/visitors/SMCQueryVisitor.java index f1365de95..f36d59658 100644 --- a/src/main/java/dk/aau/cs/TCTL/visitors/SMCQueryVisitor.java +++ b/src/main/java/dk/aau/cs/TCTL/visitors/SMCQueryVisitor.java @@ -62,9 +62,7 @@ private String observationTag(List observations) { for (Observation observation : observations) { String tagContent = XML_WATCH; - tagContent += tagAttribute(XML_WATCH_ID, observation.getId()); tagContent += tagAttribute(XML_WATCH_NAME, observation.getName()); - observationXml += startTag(tagContent); observationXml += endTag(XML_WATCH); } diff --git a/src/main/java/dk/aau/cs/io/queries/TAPNQueryLoader.java b/src/main/java/dk/aau/cs/io/queries/TAPNQueryLoader.java index 21ba7a861..06d58fad0 100644 --- a/src/main/java/dk/aau/cs/io/queries/TAPNQueryLoader.java +++ b/src/main/java/dk/aau/cs/io/queries/TAPNQueryLoader.java @@ -122,10 +122,9 @@ private TAPNQuery parseTAPNQuery(Element queryElement, TimedArcPetriNetNetwork n List observations = new ArrayList<>(); for (int i = 0; i < watchList.getLength(); ++i) { Element watch = (Element)watchList.item(i); - String id = watch.getAttribute("id"); String name = watch.getAttribute("name"); - Observation observation = new Observation(name, id); + Observation observation = new Observation(name); 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 index bd12698ed..e1adab795 100644 --- a/src/main/java/dk/aau/cs/verification/observations/Observation.java +++ b/src/main/java/dk/aau/cs/verification/observations/Observation.java @@ -1,34 +1,21 @@ package dk.aau.cs.verification.observations; -import java.util.UUID; - import dk.aau.cs.verification.observations.expressions.ObsExpression; import dk.aau.cs.verification.observations.expressions.ObsPlaceHolder; public class Observation { - private final String id; - private String name; private ObsExpression expression = new ObsPlaceHolder(); - public Observation(String name, String id) { - this.name = name; - this.id = id; - } - public Observation(String name) { - this(name, UUID.randomUUID().toString()); + this.name = name; } public String getName() { return name; } - public String getId() { - return id; - } - public ObsExpression getExpression() { return expression; } diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsConstant.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsConstant.java index 760926cd6..d5a5ed3cf 100644 --- a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsConstant.java +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsConstant.java @@ -1,19 +1,19 @@ package dk.aau.cs.verification.observations.expressions; public class ObsConstant extends ObsLeaf { - private final int tokens; + private final int value; - public ObsConstant(int tokens) { - this.tokens = tokens; + public ObsConstant(int value) { + this.value = value; } @Override public String toString() { - return Integer.toString(tokens); + return Integer.toString(value); } @Override public ObsExpression copy() { - return new ObsConstant(tokens); + return new ObsConstant(value); } } diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsExpression.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsExpression.java index 539b0f8bb..585ae1c1c 100644 --- a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsExpression.java +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsExpression.java @@ -5,4 +5,5 @@ public interface ObsExpression { ObsExprPosition getObjectPosition(int index); boolean isOperator(); boolean isLeaf(); + boolean isPlaceHolder(); } diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsLeaf.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsLeaf.java index 4f2ed956d..38bb2250b 100644 --- a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsLeaf.java +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsLeaf.java @@ -15,4 +15,9 @@ public boolean isOperator() { public boolean isLeaf() { return true; } + + @Override + public boolean isPlaceHolder() { + return false; + } } diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsOperator.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsOperator.java index ca9e4e57d..c9615d74a 100644 --- a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsOperator.java +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsOperator.java @@ -94,6 +94,11 @@ public boolean isLeaf() { return false; } + @Override + public boolean isPlaceHolder() { + return false; + } + @Override public String toString() { String operator = getOperator(); diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlace.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlace.java index 1990f89e6..087aa799d 100644 --- a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlace.java +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlace.java @@ -3,19 +3,21 @@ import dk.aau.cs.model.tapn.TimedPlace; public class ObsPlace extends ObsLeaf { + private final Object template; private final TimedPlace place; - public ObsPlace(TimedPlace place) { + public ObsPlace(Object template, TimedPlace place) { + this.template = template; this.place = place; } @Override public String toString() { - return place.name(); + return template + "." + place.name(); } @Override public ObsExpression copy() { - return new ObsPlace(place); + return new ObsPlace(template, place); } } diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlaceHolder.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlaceHolder.java index 47a7e93a4..3616242d4 100644 --- a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlaceHolder.java +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlaceHolder.java @@ -10,4 +10,9 @@ public String toString() { public ObsExpression copy() { return new ObsPlaceHolder(); } + + @Override + public boolean isPlaceHolder() { + return true; + } } \ No newline at end of file diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/ObservationDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/ObservationDialog.java index 88b649ea9..bb9dcbf77 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/ObservationDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/ObservationDialog.java @@ -5,6 +5,7 @@ import javax.swing.JButton; import javax.swing.JComboBox; import javax.swing.JLabel; +import javax.swing.JOptionPane; import javax.swing.JPanel; import javax.swing.JScrollPane; import javax.swing.JTextField; @@ -14,15 +15,20 @@ import javax.swing.text.SimpleAttributeSet; import javax.swing.text.StyleConstants; import javax.swing.text.StyledDocument; +import javax.swing.undo.AbstractUndoableEdit; +import javax.swing.undo.UndoManager; import dk.aau.cs.model.tapn.TimedArcPetriNet; import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork; +import dk.aau.cs.model.tapn.TimedPlace; import dk.aau.cs.verification.observations.Observation; import dk.aau.cs.verification.observations.expressions.ObsExprPosition; import dk.aau.cs.verification.observations.expressions.ObsAdd; +import dk.aau.cs.verification.observations.expressions.ObsConstant; import dk.aau.cs.verification.observations.expressions.ObsExpression; import dk.aau.cs.verification.observations.expressions.ObsMultiply; import dk.aau.cs.verification.observations.expressions.ObsOperator; +import dk.aau.cs.verification.observations.expressions.ObsPlace; import dk.aau.cs.verification.observations.expressions.ObsPlaceHolder; import dk.aau.cs.verification.observations.expressions.ObsSubtract; import net.tapaal.helpers.Enabler; @@ -42,8 +48,15 @@ public class ObservationDialog extends EscapableDialog { private final DefaultListModel observationModel; private final Observation observation; + private final TimedArcPetriNetNetwork tapnNetwork; + private final JTextPane expressionField = new JTextPane(); + private final UndoManager undoManager = new UndoManager(); + private JPanel placesPanel; private JPanel constantsPanel; + private JButton saveButton; + private JButton undoButton; + private JButton redoButton; private ObsExpression currentExpr; private ObsExpression selectedExpr; @@ -51,11 +64,6 @@ public class ObservationDialog extends EscapableDialog { private boolean isNewObservation; private boolean isEditing; - private JButton saveButton; - - private final TimedArcPetriNetNetwork tapnNetwork; - private final JTextPane expressionField = new JTextPane(); - public ObservationDialog(TimedArcPetriNetNetwork tapnNetwork, DefaultListModel observationModel, Observation observation) { super(TAPAALGUI.getApp(), observation.getName(), true); this.tapnNetwork = tapnNetwork; @@ -116,6 +124,9 @@ public void mouseClicked(MouseEvent e) { ObsExprPosition exprPos = currentExpr.getObjectPosition(pos - 1); expressionField.select(exprPos.getStart(), exprPos.getEnd()); selectedExpr = exprPos.getObject(); + + Enabler.setAllEnabled(placesPanel, selectedExpr.isLeaf()); + Enabler.setAllEnabled(constantsPanel, selectedExpr.isLeaf()); } }); @@ -163,14 +174,14 @@ public void mouseClicked(MouseEvent e) { templateComboBox.addItem(SHARED); } - JComboBox placeComboBox = new JComboBox<>(); + JComboBox placeComboBox = new JComboBox<>(); templateComboBox.addActionListener(e -> { placeComboBox.removeAllItems(); if (templateComboBox.getSelectedItem().equals(SHARED)) { - tapnNetwork.sharedPlaces().forEach(place -> placeComboBox.addItem(place.name())); + tapnNetwork.sharedPlaces().forEach(place -> placeComboBox.addItem(place)); } else { TimedArcPetriNet template = (TimedArcPetriNet) templateComboBox.getSelectedItem(); - template.places().forEach(place -> placeComboBox.addItem(place.name())); + template.places().forEach(place -> placeComboBox.addItem(place)); } }); @@ -180,6 +191,14 @@ public void mouseClicked(MouseEvent e) { } JButton addPlaceButton = new JButton("Add place"); + addPlaceButton.addActionListener(e -> { + Object template = templateComboBox.getSelectedItem(); + TimedPlace place = (TimedPlace)placeComboBox.getSelectedItem(); + ObsExpression placeExpr = new ObsPlace(template, place); + updateExpression(placeExpr); + Enabler.setAllEnabled(placesPanel, false); + Enabler.setAllEnabled(constantsPanel, false); + }); GridBagConstraints placesGbc = new GridBagConstraints(); placesGbc.gridx = 0; @@ -200,8 +219,15 @@ public void mouseClicked(MouseEvent e) { constantsPanel.setLayout(new GridBagLayout()); constantsPanel.setBorder(BorderFactory.createTitledBorder("Constants")); - CustomJSpinner constantSpinner = new CustomJSpinner(0, 0, Integer.MAX_VALUE); + CustomJSpinner constantSpinner = new CustomJSpinner(1, 1, Integer.MAX_VALUE); JButton addConstantButton = new JButton("Add constant"); + addConstantButton.addActionListener(e -> { + int value = (int)constantSpinner.getValue(); + ObsExpression constantExpr = new ObsConstant(value); + updateExpression(constantExpr); + Enabler.setAllEnabled(placesPanel, false); + Enabler.setAllEnabled(constantsPanel, false); + }); GridBagConstraints constantsGbc = new GridBagConstraints(); constantsGbc.gridx = 0; @@ -220,19 +246,36 @@ public void mouseClicked(MouseEvent e) { editingPanel.setLayout(new GridBagLayout()); editingPanel.setBorder(BorderFactory.createTitledBorder("Editing")); - JButton undoButton = new JButton("Undo"); + undoButton = new JButton("Undo"); + redoButton = new JButton("Redo"); undoButton.setEnabled(false); - - JButton redoButton = new JButton("Redo"); redoButton.setEnabled(false); + undoButton.addActionListener(e -> { + if (undoManager.canUndo()) { + undoManager.undo(); + } + }); + + redoButton.addActionListener(e -> { + if (undoManager.canRedo()) { + undoManager.redo(); + } + }); + JButton deleteSelection = new JButton("Delete Selection"); deleteSelection.setEnabled(false); JButton resetExpression = new JButton("Reset Expression"); resetExpression.addActionListener(e -> { + ObsExpression oldExpr = currentExpr.copy(); currentExpr = new ObsPlaceHolder(); expressionField.setText(currentExpr.toString()); + + if (!oldExpr.isPlaceHolder()) { + undoManager.addEdit(new ExpressionEdit(oldExpr, currentExpr)); + refreshUndoRedoButtons(); + } }); JButton editExpression = new JButton("Edit Expression"); @@ -243,7 +286,13 @@ public void mouseClicked(MouseEvent e) { Enabler.setAllEnabled(operationsPanel, !isEditing); Enabler.setAllEnabled(placesPanel, !isEditing); Enabler.setAllEnabled(constantsPanel, !isEditing); - saveButton.setEnabled(!isEditing); + + if (isEditing) { + saveButton.setEnabled(false); + } else { + saveButton.setEnabled(!includesPlaceHolder()); + } + expressionField.setEditable(isEditing); if (isEditing) { @@ -311,21 +360,33 @@ public void mouseClicked(MouseEvent e) { buttonPanel.setLayout(new GridBagLayout()); JButton cancelButton = new JButton("Cancel"); saveButton = new JButton("Save"); + saveButton.setEnabled(!includesPlaceHolder()); - cancelButton.addActionListener(e -> { - dispose(); - }); - + cancelButton.addActionListener(e -> dispose()); saveButton.addActionListener(e -> { observation.setName(nameField.getText()); + observation.setExpression(currentExpr); + + boolean nameExists = false; + for (int i = 0; i < observationModel.getSize(); i++) { + Observation obs = observationModel.getElementAt(i); + if (obs.getName().equals(observation.getName())) { + nameExists = true; + break; + } + } - if (isNewObservation) { - observationModel.addElement(observation); + if (nameExists) { + JOptionPane.showMessageDialog(TAPAALGUI.getApp(), "An observation with the name \"" + observation.getName() + "\" already exists.", "Error", JOptionPane.ERROR_MESSAGE); } else { - observationModel.setElementAt(observation, observationModel.indexOf(observation)); + if (isNewObservation) { + observationModel.addElement(observation); + } else { + observationModel.setElementAt(observation, observationModel.indexOf(observation)); + } + + dispose(); } - - dispose(); }); GridBagConstraints buttonGbc = new GridBagConstraints(); @@ -352,6 +413,7 @@ public void mouseClicked(MouseEvent e) { private void updateExpression(ObsExpression newExpr) { String selectedText = expressionField.getSelectedText(); String fullText = expressionField.getText(); + ObsExpression oldExpr = currentExpr.copy(); if (selectedText != null && !selectedText.equals(fullText) && currentExpr.isOperator()) { @@ -363,5 +425,44 @@ private void updateExpression(ObsExpression newExpr) { } expressionField.setText(currentExpr.toString()); + undoManager.addEdit(new ExpressionEdit(oldExpr, newExpr)); + refreshUndoRedoButtons(); + + saveButton.setEnabled(!includesPlaceHolder()); + } + + private void refreshUndoRedoButtons() { + undoButton.setEnabled(undoManager.canUndo()); + redoButton.setEnabled(undoManager.canRedo()); + } + + private boolean includesPlaceHolder() { + return currentExpr.toString().contains(new ObsPlaceHolder().toString()); + } + + private class ExpressionEdit extends AbstractUndoableEdit { + private final ObsExpression oldExpr; + private final ObsExpression newExpr; + + public ExpressionEdit(ObsExpression oldExpr, ObsExpression newExpr) { + this.oldExpr = oldExpr; + this.newExpr = newExpr; + } + + @Override + public void undo() { + super.undo(); + currentExpr = oldExpr; + expressionField.setText(currentExpr.toString()); + refreshUndoRedoButtons(); + } + + @Override + public void redo() { + super.redo(); + currentExpr = newExpr; + expressionField.setText(currentExpr.toString()); + refreshUndoRedoButtons(); + } } } From ec5e967e4adbfabb79121c86a122525c54e83198 Mon Sep 17 00:00:00 2001 From: Mikkel Tygesen Date: Mon, 18 Nov 2024 15:46:38 +0100 Subject: [PATCH 3/7] finished xml export and parsing of observations --- .../aau/cs/TCTL/visitors/SMCQueryVisitor.java | 5 +- .../cs/io/TimedArcPetriNetNetworkWriter.java | 2 + .../dk/aau/cs/io/queries/TAPNQueryLoader.java | 98 ++++++++++++++++++- .../observations/Observation.java | 9 ++ .../observations/expressions/ObsAdd.java | 5 + .../observations/expressions/ObsConstant.java | 7 +- .../expressions/ObsExpression.java | 3 +- .../observations/expressions/ObsMultiply.java | 5 + .../observations/expressions/ObsOperator.java | 12 ++- .../observations/expressions/ObsPlace.java | 9 +- .../expressions/ObsPlaceHolder.java | 7 +- .../observations/expressions/ObsSubtract.java | 5 + .../petrinet/dialog/ObservationDialog.java | 28 +++--- 13 files changed, 169 insertions(+), 26 deletions(-) diff --git a/src/main/java/dk/aau/cs/TCTL/visitors/SMCQueryVisitor.java b/src/main/java/dk/aau/cs/TCTL/visitors/SMCQueryVisitor.java index f36d59658..12447cad2 100644 --- a/src/main/java/dk/aau/cs/TCTL/visitors/SMCQueryVisitor.java +++ b/src/main/java/dk/aau/cs/TCTL/visitors/SMCQueryVisitor.java @@ -61,10 +61,7 @@ private String observationTag(List observations) { String observationXml = startTag(XML_OBSERVATIONS); for (Observation observation : observations) { - String tagContent = XML_WATCH; - tagContent += tagAttribute(XML_WATCH_NAME, observation.getName()); - observationXml += startTag(tagContent); - observationXml += endTag(XML_WATCH); + observationXml += observation.toXml(); } observationXml += endTag(XML_OBSERVATIONS); diff --git a/src/main/java/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java b/src/main/java/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java index cf8affc78..263a9ef24 100644 --- a/src/main/java/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java +++ b/src/main/java/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java @@ -505,7 +505,9 @@ private Element createSMCQueryElement(TAPNQuery query, Document document) { .getDocumentElement(); Node smcTag = doc.getElementsByTagName("smc").item(0); Node formula = doc.getElementsByTagName("formula").item(0); + Node observations = doc.getElementsByTagName("observations").item(0); queryElement.appendChild(document.importNode(smcTag, true)); + queryElement.appendChild(document.importNode(observations, true)); queryElement.appendChild(document.importNode(formula, true)); } catch (SAXException | ParserConfigurationException | IOException e) { System.out.println(e + " thrown in savePNML() " diff --git a/src/main/java/dk/aau/cs/io/queries/TAPNQueryLoader.java b/src/main/java/dk/aau/cs/io/queries/TAPNQueryLoader.java index 06d58fad0..768a2b462 100644 --- a/src/main/java/dk/aau/cs/io/queries/TAPNQueryLoader.java +++ b/src/main/java/dk/aau/cs/io/queries/TAPNQueryLoader.java @@ -3,12 +3,21 @@ import java.util.ArrayList; import java.util.Arrays; import java.util.List; +import java.util.function.BiFunction; + import dk.aau.cs.TCTL.*; import dk.aau.cs.TCTL.XMLParsing.XMLHyperLTLQueryParser; import dk.aau.cs.TCTL.XMLParsing.XMLLTLQueryParser; import dk.aau.cs.verification.SMCSettings; import dk.aau.cs.verification.SMCTraceType; import dk.aau.cs.verification.observations.Observation; +import dk.aau.cs.verification.observations.expressions.ObsAdd; +import dk.aau.cs.verification.observations.expressions.ObsConstant; +import dk.aau.cs.verification.observations.expressions.ObsExpression; +import dk.aau.cs.verification.observations.expressions.ObsMultiply; +import dk.aau.cs.verification.observations.expressions.ObsOperator; +import dk.aau.cs.verification.observations.expressions.ObsPlace; +import dk.aau.cs.verification.observations.expressions.ObsSubtract; import org.w3c.dom.Document; import org.w3c.dom.Element; @@ -28,6 +37,7 @@ import dk.aau.cs.TCTL.Parsing.TAPAALQueryParser; import dk.aau.cs.TCTL.XMLParsing.XMLCTLQueryParser; import dk.aau.cs.TCTL.XMLParsing.XMLQueryParseException; +import dk.aau.cs.model.tapn.TimedArcPetriNet; import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork; import dk.aau.cs.model.tapn.TimedPlace; import dk.aau.cs.translations.ReductionOption; @@ -122,9 +132,10 @@ private TAPNQuery parseTAPNQuery(Element queryElement, TimedArcPetriNetNetwork n List observations = new ArrayList<>(); for (int i = 0; i < watchList.getLength(); ++i) { Element watch = (Element)watchList.item(i); - String name = watch.getAttribute("name"); + String name = watch.getAttribute("name"); - Observation observation = new Observation(name); + Element root = getFirstElementChild(watch); + Observation observation = new Observation(name, parseObsExpression(root)); observations.add(observation); } @@ -183,6 +194,89 @@ public static boolean hasSmcTag(Node queryElement) { return false; } + private Element getFirstElementChild(Element parent) { + NodeList children = parent.getChildNodes(); + for (int i = 0; i < children.getLength(); i++) { + Node child = children.item(i); + if (child.getNodeType() == Node.ELEMENT_NODE) { + return (Element)child; + } + } + + return null; + } + + private Element getSecondElementChild(Element parent) { + NodeList children = parent.getChildNodes(); + int elementCount = 0; + for (int i = 0; i < children.getLength(); i++) { + Node child = children.item(i); + if (child.getNodeType() == Node.ELEMENT_NODE) { + ++elementCount; + if (elementCount == 2) { + return (Element)child; + } + } + } + + return null; + } + + private ObsExpression parseObsExpression(Element element) { + String tagName = element.getTagName(); + + switch (tagName) { + case "obs-add": + return createOperatorExpression(element, ObsAdd::new); + case "obs-subtract": + return createOperatorExpression(element, ObsSubtract::new); + case "obs-multiply": + return createOperatorExpression(element, ObsMultiply::new); + case "obs-constant": + return new ObsConstant(Integer.parseInt(element.getAttribute("value"))); + case "obs-place": + return createPlaceExpression(element); + default: + throw new IllegalArgumentException("Unknown expression type: " + tagName); + } + } + + private ObsExpression createOperatorExpression(Element element, BiFunction constructor) { + ObsExpression left = parseObsExpression(getFirstElementChild(element)); + ObsExpression right = parseObsExpression(getSecondElementChild(element)); + ObsOperator operator = constructor.apply(left, right); + + if (left.isOperator()) { + ((ObsOperator)left).setParent(operator); + } + + if (right.isOperator()) { + ((ObsOperator)right).setParent(operator); + } + + return operator; + } + + private ObsExpression createPlaceExpression(Element element) { + String name = element.getAttribute("name"); + String[] parts = name.split("_"); + String templateName = parts[0]; + String placeName = parts[1]; + + Object template; + TimedPlace place; + if (templateName.equals("Shared")) { + template = templateName; + place = network.getSharedPlaceByName(placeName); + } else { + TimedArcPetriNet net = network.getTAPNByName(templateName); + template = net; + place = net.getPlaceByName(placeName); + } + + return new ObsPlace(template, place); + } + public static SMCSettings parseSmcSettings(Element smcTag) { SMCSettings settings = SMCSettings.Default(); if(smcTag.hasAttribute("time-bound")) diff --git a/src/main/java/dk/aau/cs/verification/observations/Observation.java b/src/main/java/dk/aau/cs/verification/observations/Observation.java index e1adab795..35c64395b 100644 --- a/src/main/java/dk/aau/cs/verification/observations/Observation.java +++ b/src/main/java/dk/aau/cs/verification/observations/Observation.java @@ -12,6 +12,11 @@ public Observation(String name) { this.name = name; } + public Observation(String name, ObsExpression expression) { + this.name = name; + this.expression = expression; + } + public String getName() { return name; } @@ -32,4 +37,8 @@ public void setExpression(ObsExpression expression) { public String toString() { return name; } + + public String toXml() { + return "" + expression.toXml() + ""; + } } diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsAdd.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsAdd.java index d9843ce89..f59e29235 100644 --- a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsAdd.java +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsAdd.java @@ -13,4 +13,9 @@ public ObsAdd() { protected String getOperator() { return "+"; } + + @Override + public String toXml() { + return "" + left.toXml() + right.toXml() + ""; + } } diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsConstant.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsConstant.java index d5a5ed3cf..e0e942c6a 100644 --- a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsConstant.java +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsConstant.java @@ -13,7 +13,12 @@ public String toString() { } @Override - public ObsExpression copy() { + public String toXml() { + return ""; + } + + @Override + public ObsExpression deepCopy() { return new ObsConstant(value); } } diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsExpression.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsExpression.java index 585ae1c1c..8233cf73c 100644 --- a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsExpression.java +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsExpression.java @@ -1,9 +1,10 @@ package dk.aau.cs.verification.observations.expressions; public interface ObsExpression { - ObsExpression copy(); + ObsExpression deepCopy(); ObsExprPosition getObjectPosition(int index); boolean isOperator(); boolean isLeaf(); boolean isPlaceHolder(); + String toXml(); } diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsMultiply.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsMultiply.java index caae17b32..7d8512b19 100644 --- a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsMultiply.java +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsMultiply.java @@ -13,4 +13,9 @@ public ObsMultiply() { protected String getOperator() { return "*"; } + + @Override + public String toXml() { + return "" + left.toXml() + right.toXml() + ""; + } } diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsOperator.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsOperator.java index c9615d74a..509124137 100644 --- a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsOperator.java +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsOperator.java @@ -53,16 +53,22 @@ public void replace(ObsExpression selectedExpr, ObsExpression newExpr) { } @Override - public ObsExpression copy() { + public ObsExpression deepCopy() { try { - return getClass() + ObsOperator copy = getClass() .getConstructor(ObsExpression.class, ObsExpression.class) - .newInstance(left.copy(), right.copy()); + .newInstance(left.deepCopy(), right.deepCopy()); + copy.setParent(this.parent); + return copy; } catch (Exception e) { throw new RuntimeException("Failed to copy ObsOperator", e); } } + public void setParent(ObsExpression parent) { + this.parent = parent; + } + protected boolean addParenthesis() { return parent != null && parent.getClass() != getClass(); } diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlace.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlace.java index 087aa799d..bad44e493 100644 --- a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlace.java +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlace.java @@ -1,5 +1,7 @@ package dk.aau.cs.verification.observations.expressions; +import dk.aau.cs.model.tapn.TimedArcPetriNet; +import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork; import dk.aau.cs.model.tapn.TimedPlace; public class ObsPlace extends ObsLeaf { @@ -17,7 +19,12 @@ public String toString() { } @Override - public ObsExpression copy() { + public String toXml() { + return ""; + } + + @Override + public ObsExpression deepCopy() { return new ObsPlace(template, place); } } diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlaceHolder.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlaceHolder.java index 3616242d4..53e02a2f8 100644 --- a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlaceHolder.java +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlaceHolder.java @@ -7,7 +7,12 @@ public String toString() { } @Override - public ObsExpression copy() { + public String toXml() { + throw new UnsupportedOperationException("Cannot convert a placeholder to XML"); + } + + @Override + public ObsExpression deepCopy() { return new ObsPlaceHolder(); } diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsSubtract.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsSubtract.java index e8aac0e21..d93ee43da 100644 --- a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsSubtract.java +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsSubtract.java @@ -13,4 +13,9 @@ public ObsSubtract() { protected String getOperator() { return "-"; } + + @Override + public String toXml() { + return "" + left.toXml() + right.toXml() + ""; + } } diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/ObservationDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/ObservationDialog.java index bb9dcbf77..04ad2a960 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/ObservationDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/ObservationDialog.java @@ -69,7 +69,7 @@ public ObservationDialog(TimedArcPetriNetNetwork tapnNetwork, DefaultListModel { - ObsExpression oldExpr = currentExpr.copy(); + ObsExpression oldExpr = currentExpr.deepCopy(); currentExpr = new ObsPlaceHolder(); expressionField.setText(currentExpr.toString()); if (!oldExpr.isPlaceHolder()) { - undoManager.addEdit(new ExpressionEdit(oldExpr, currentExpr)); + undoManager.addEdit(new ExpressionEdit(oldExpr, currentExpr.deepCopy())); refreshUndoRedoButtons(); } }); @@ -364,13 +364,11 @@ public void mouseClicked(MouseEvent e) { cancelButton.addActionListener(e -> dispose()); saveButton.addActionListener(e -> { - observation.setName(nameField.getText()); - observation.setExpression(currentExpr); - boolean nameExists = false; for (int i = 0; i < observationModel.getSize(); i++) { Observation obs = observationModel.getElementAt(i); - if (obs.getName().equals(observation.getName())) { + if (obs.getName().equals(nameField.getText()) && + !obs.equals(observation)) { nameExists = true; break; } @@ -379,6 +377,9 @@ public void mouseClicked(MouseEvent e) { if (nameExists) { JOptionPane.showMessageDialog(TAPAALGUI.getApp(), "An observation with the name \"" + observation.getName() + "\" already exists.", "Error", JOptionPane.ERROR_MESSAGE); } else { + observation.setName(nameField.getText()); + observation.setExpression(currentExpr); + if (isNewObservation) { observationModel.addElement(observation); } else { @@ -413,7 +414,7 @@ public void mouseClicked(MouseEvent e) { private void updateExpression(ObsExpression newExpr) { String selectedText = expressionField.getSelectedText(); String fullText = expressionField.getText(); - ObsExpression oldExpr = currentExpr.copy(); + ObsExpression oldExpr = currentExpr.deepCopy(); if (selectedText != null && !selectedText.equals(fullText) && currentExpr.isOperator()) { @@ -424,11 +425,12 @@ private void updateExpression(ObsExpression newExpr) { currentExpr = newExpr; } - expressionField.setText(currentExpr.toString()); - undoManager.addEdit(new ExpressionEdit(oldExpr, newExpr)); - refreshUndoRedoButtons(); - - saveButton.setEnabled(!includesPlaceHolder()); + if (!currentExpr.toString().equals(oldExpr.toString())) { + expressionField.setText(currentExpr.toString()); + undoManager.addEdit(new ExpressionEdit(oldExpr, currentExpr.deepCopy())); + refreshUndoRedoButtons(); + saveButton.setEnabled(!includesPlaceHolder()); + } } private void refreshUndoRedoButtons() { From f89d0320fab7edf704678da69f2b7e2d16ef7726 Mon Sep 17 00:00:00 2001 From: Mikkel Tygesen Date: Mon, 18 Nov 2024 15:50:48 +0100 Subject: [PATCH 4/7] removed unused imports --- .../aau/cs/verification/observations/expressions/ObsPlace.java | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlace.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlace.java index bad44e493..80a289540 100644 --- a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlace.java +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlace.java @@ -1,7 +1,5 @@ package dk.aau.cs.verification.observations.expressions; -import dk.aau.cs.model.tapn.TimedArcPetriNet; -import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork; import dk.aau.cs.model.tapn.TimedPlace; public class ObsPlace extends ObsLeaf { From 97024679a0f6a006e0a74b1f8f3f7ff676c6afb8 Mon Sep 17 00:00:00 2001 From: Mikkel Tygesen Date: Mon, 18 Nov 2024 16:25:15 +0100 Subject: [PATCH 5/7] removed prefix --- src/main/java/dk/aau/cs/io/LoadTACPN.java | 2 +- .../dk/aau/cs/io/TapnEngineXmlLoader.java | 7 ++++++- .../dk/aau/cs/io/TapnLegacyXmlLoader.java | 3 +++ src/main/java/dk/aau/cs/io/TapnXmlLoader.java | 3 +++ src/main/java/dk/aau/cs/io/XmlUtil.java | 19 +++++++++++++++++++ .../dk/aau/cs/io/queries/TAPNQueryLoader.java | 10 +++++----- .../observations/expressions/ObsAdd.java | 2 +- .../observations/expressions/ObsConstant.java | 2 +- .../observations/expressions/ObsMultiply.java | 2 +- .../observations/expressions/ObsPlace.java | 2 +- .../observations/expressions/ObsSubtract.java | 2 +- 11 files changed, 42 insertions(+), 12 deletions(-) create mode 100644 src/main/java/dk/aau/cs/io/XmlUtil.java diff --git a/src/main/java/dk/aau/cs/io/LoadTACPN.java b/src/main/java/dk/aau/cs/io/LoadTACPN.java index 11c9b3e83..f69c4bcbf 100644 --- a/src/main/java/dk/aau/cs/io/LoadTACPN.java +++ b/src/main/java/dk/aau/cs/io/LoadTACPN.java @@ -251,7 +251,7 @@ public ArcExpression parseArcExpression(Node node) throws FormatException { ArcExpression childexp = parseArcExpression(child); return new ScalarProductExpression(scalarval, childexp); - }else if (name.equals("all")){ + } else if (name.equals("all")){ ColorType ct = parseUserSort(node); Vector ceVector = new Vector<>(); ceVector.add(new AllExpression(ct)); diff --git a/src/main/java/dk/aau/cs/io/TapnEngineXmlLoader.java b/src/main/java/dk/aau/cs/io/TapnEngineXmlLoader.java index f82129bf9..d02d973da 100644 --- a/src/main/java/dk/aau/cs/io/TapnEngineXmlLoader.java +++ b/src/main/java/dk/aau/cs/io/TapnEngineXmlLoader.java @@ -277,16 +277,21 @@ private List parseConstants(Document doc) { List constants = new ArrayList(); NodeList constantNodes = doc.getElementsByTagName("constant"); for (int i = 0; i < constantNodes.getLength(); i++) { - Node c = constantNodes.item(i); + Node c = constantNodes.item(i); + if (XmlUtil.isDescendantOfTag(c, "watch")) { + continue; + } if (c instanceof Element) { Constant constant = parseConstant((Element) c); constants.add(constant); } } + return constants; } + private Template parseTimedArcPetriNet(Node tapnNode, TimedArcPetriNetNetwork network, ConstantStore constants) throws FormatException { String name = getTAPNName(tapnNode); diff --git a/src/main/java/dk/aau/cs/io/TapnLegacyXmlLoader.java b/src/main/java/dk/aau/cs/io/TapnLegacyXmlLoader.java index 0bc8472dd..816c01dbd 100644 --- a/src/main/java/dk/aau/cs/io/TapnLegacyXmlLoader.java +++ b/src/main/java/dk/aau/cs/io/TapnLegacyXmlLoader.java @@ -128,6 +128,9 @@ private LoadedModel parse(Document tapnDoc) throws FormatException { NodeList constantNodes = tapnDoc.getElementsByTagName("constant"); for (int i = 0; i < constantNodes.getLength(); i++) { Node c = constantNodes.item(i); + if (XmlUtil.isDescendantOfTag(c, "watch")) { + continue; + } if (c instanceof Element) { parseAndAddConstant((Element) c); diff --git a/src/main/java/dk/aau/cs/io/TapnXmlLoader.java b/src/main/java/dk/aau/cs/io/TapnXmlLoader.java index b1ee3f143..31574fe8d 100644 --- a/src/main/java/dk/aau/cs/io/TapnXmlLoader.java +++ b/src/main/java/dk/aau/cs/io/TapnXmlLoader.java @@ -318,6 +318,9 @@ private List parseConstants(Document doc) { NodeList constantNodes = doc.getElementsByTagName("constant"); for (int i = 0; i < constantNodes.getLength(); i++) { Node c = constantNodes.item(i); + if (XmlUtil.isDescendantOfTag(c, "watch")) { + continue; + } if (c instanceof Element) { Constant constant = parseConstant((Element) c); diff --git a/src/main/java/dk/aau/cs/io/XmlUtil.java b/src/main/java/dk/aau/cs/io/XmlUtil.java new file mode 100644 index 000000000..c5a1ef90a --- /dev/null +++ b/src/main/java/dk/aau/cs/io/XmlUtil.java @@ -0,0 +1,19 @@ +package dk.aau.cs.io; + +import org.w3c.dom.Element; +import org.w3c.dom.Node; + +public class XmlUtil { + public static boolean isDescendantOfTag(Node node, String tagName) { + Node parent = node.getParentNode(); + while (parent != null) { + if (parent.getNodeType() == Node.ELEMENT_NODE &&((Element) parent).getTagName().equals(tagName)) { + return true; + } + + parent = parent.getParentNode(); + } + + return false; + } +} diff --git a/src/main/java/dk/aau/cs/io/queries/TAPNQueryLoader.java b/src/main/java/dk/aau/cs/io/queries/TAPNQueryLoader.java index 768a2b462..7d320cb6d 100644 --- a/src/main/java/dk/aau/cs/io/queries/TAPNQueryLoader.java +++ b/src/main/java/dk/aau/cs/io/queries/TAPNQueryLoader.java @@ -226,15 +226,15 @@ private ObsExpression parseObsExpression(Element element) { String tagName = element.getTagName(); switch (tagName) { - case "obs-add": + case "add": return createOperatorExpression(element, ObsAdd::new); - case "obs-subtract": + case "subtract": return createOperatorExpression(element, ObsSubtract::new); - case "obs-multiply": + case "multiply": return createOperatorExpression(element, ObsMultiply::new); - case "obs-constant": + case "constant": return new ObsConstant(Integer.parseInt(element.getAttribute("value"))); - case "obs-place": + case "place": return createPlaceExpression(element); default: throw new IllegalArgumentException("Unknown expression type: " + tagName); diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsAdd.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsAdd.java index f59e29235..d0d9eea3e 100644 --- a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsAdd.java +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsAdd.java @@ -16,6 +16,6 @@ protected String getOperator() { @Override public String toXml() { - return "" + left.toXml() + right.toXml() + ""; + return "" + left.toXml() + right.toXml() + ""; } } diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsConstant.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsConstant.java index e0e942c6a..df962a917 100644 --- a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsConstant.java +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsConstant.java @@ -14,7 +14,7 @@ public String toString() { @Override public String toXml() { - return ""; + return ""; } @Override diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsMultiply.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsMultiply.java index 7d8512b19..d186e9995 100644 --- a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsMultiply.java +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsMultiply.java @@ -16,6 +16,6 @@ protected String getOperator() { @Override public String toXml() { - return "" + left.toXml() + right.toXml() + ""; + return "" + left.toXml() + right.toXml() + ""; } } diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlace.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlace.java index 80a289540..ad0fc9e01 100644 --- a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlace.java +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlace.java @@ -18,7 +18,7 @@ public String toString() { @Override public String toXml() { - return ""; + return ""; } @Override diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsSubtract.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsSubtract.java index d93ee43da..efa4cf0f5 100644 --- a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsSubtract.java +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsSubtract.java @@ -16,6 +16,6 @@ protected String getOperator() { @Override public String toXml() { - return "" + left.toXml() + right.toXml() + ""; + return "" + left.toXml() + right.toXml() + ""; } } From 918d5712d874efa6470868dd4b6066c0433d6245 Mon Sep 17 00:00:00 2001 From: Mikkel Tygesen Date: Mon, 18 Nov 2024 17:09:45 +0100 Subject: [PATCH 6/7] cleanup --- src/main/java/dk/aau/cs/io/XmlUtil.java | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/main/java/dk/aau/cs/io/XmlUtil.java b/src/main/java/dk/aau/cs/io/XmlUtil.java index c5a1ef90a..5c687e57e 100644 --- a/src/main/java/dk/aau/cs/io/XmlUtil.java +++ b/src/main/java/dk/aau/cs/io/XmlUtil.java @@ -4,16 +4,20 @@ import org.w3c.dom.Node; public class XmlUtil { + /** + * Returns true if the given node is a descendant of a node with the given tag name. + */ public static boolean isDescendantOfTag(Node node, String tagName) { Node parent = node.getParentNode(); while (parent != null) { - if (parent.getNodeType() == Node.ELEMENT_NODE &&((Element) parent).getTagName().equals(tagName)) { + if (parent.getNodeType() == Node.ELEMENT_NODE && + ((Element)parent).getTagName().equals(tagName)) { return true; } parent = parent.getParentNode(); } - + return false; } } From 7217a3be72d049de40bbd362468b8d129d360c9e Mon Sep 17 00:00:00 2001 From: Mikkel Tygesen Date: Mon, 18 Nov 2024 22:29:12 +0100 Subject: [PATCH 7/7] added manual editing of observations --- .../dk/aau/cs/io/queries/TAPNQueryLoader.java | 13 +- .../observations/expressions/ObsOperator.java | 19 ++- .../observations/expressions/ObsPlace.java | 13 ++ .../petrinet/dialog/ObservationDialog.java | 88 +++++++---- .../dk/aau/cs/model/SMC/ObservationParser.jj | 148 ++++++++++++++++++ 5 files changed, 234 insertions(+), 47 deletions(-) create mode 100644 src/main/javacc/dk/aau/cs/model/SMC/ObservationParser.jj diff --git a/src/main/java/dk/aau/cs/io/queries/TAPNQueryLoader.java b/src/main/java/dk/aau/cs/io/queries/TAPNQueryLoader.java index 7d320cb6d..fc9bf54fe 100644 --- a/src/main/java/dk/aau/cs/io/queries/TAPNQueryLoader.java +++ b/src/main/java/dk/aau/cs/io/queries/TAPNQueryLoader.java @@ -263,18 +263,7 @@ private ObsExpression createPlaceExpression(Element element) { String templateName = parts[0]; String placeName = parts[1]; - Object template; - TimedPlace place; - if (templateName.equals("Shared")) { - template = templateName; - place = network.getSharedPlaceByName(placeName); - } else { - TimedArcPetriNet net = network.getTAPNByName(templateName); - template = net; - place = net.getPlaceByName(placeName); - } - - return new ObsPlace(template, place); + return new ObsPlace(templateName, placeName, network); } public static SMCSettings parseSmcSettings(Element smcTag) { diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsOperator.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsOperator.java index 509124137..51ee8d30f 100644 --- a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsOperator.java +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsOperator.java @@ -3,7 +3,8 @@ public abstract class ObsOperator implements ObsExpression { protected ObsExpression left; protected ObsExpression right; - protected ObsExpression parent; + private ObsExpression parent; + private boolean hadParentheses = false; protected ObsOperator(ObsExpression left, ObsExpression right) { this.left = left; @@ -26,6 +27,14 @@ public void insertLeftMost(ObsExpression expr) { } } + public void setLeft(ObsExpression left) { + this.left = left; + } + + public void setRight(ObsExpression right) { + this.right = right; + } + public void replace(ObsExpression selectedExpr, ObsExpression newExpr) { if (left.equals(selectedExpr) || right.equals(selectedExpr)) { if (newExpr.isOperator()) { @@ -69,8 +78,12 @@ public void setParent(ObsExpression parent) { this.parent = parent; } - protected boolean addParenthesis() { - return parent != null && parent.getClass() != getClass(); + public void hadParentheses(boolean hadParentheses) { + this.hadParentheses = hadParentheses; + } + + private boolean addParenthesis() { + return (parent != null && parent.getClass() != getClass()) || hadParentheses; } @Override diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlace.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlace.java index ad0fc9e01..c025b8bdf 100644 --- a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlace.java +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlace.java @@ -1,5 +1,7 @@ package dk.aau.cs.verification.observations.expressions; +import dk.aau.cs.model.tapn.TimedArcPetriNet; +import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork; import dk.aau.cs.model.tapn.TimedPlace; public class ObsPlace extends ObsLeaf { @@ -11,6 +13,17 @@ public ObsPlace(Object template, TimedPlace place) { this.place = place; } + public ObsPlace(String templateName, String placeName, TimedArcPetriNetNetwork network) { + if (templateName.equals("Shared")) { + template = templateName; + place = network.getSharedPlaceByName(placeName); + } else { + TimedArcPetriNet net = network.getTAPNByName(templateName); + template = net; + place = net.getPlaceByName(placeName); + } + } + @Override public String toString() { return template + "." + place.name(); diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/ObservationDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/ObservationDialog.java index 04ad2a960..b12472126 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/ObservationDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/ObservationDialog.java @@ -18,6 +18,9 @@ import javax.swing.undo.AbstractUndoableEdit; import javax.swing.undo.UndoManager; +import dk.aau.cs.model.SMC.TokenMgrError; +import dk.aau.cs.model.SMC.ParseException; +import dk.aau.cs.model.SMC.ObservationParser; import dk.aau.cs.model.tapn.TimedArcPetriNet; import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork; import dk.aau.cs.model.tapn.TimedPlace; @@ -54,9 +57,12 @@ public class ObservationDialog extends EscapableDialog { private JPanel placesPanel; private JPanel constantsPanel; + private JPanel operationsPanel; private JButton saveButton; private JButton undoButton; private JButton redoButton; + private JButton resetExpression; + private JButton editExpression; private ObsExpression currentExpr; private ObsExpression selectedExpr; @@ -120,6 +126,8 @@ private void init() { expressionField.addMouseListener(new MouseAdapter() { @Override public void mouseClicked(MouseEvent e) { + if (isEditing) return; + int pos = expressionField.viewToModel2D(e.getPoint()); ObsExprPosition exprPos = currentExpr.getObjectPosition(pos - 1); expressionField.select(exprPos.getStart(), exprPos.getEnd()); @@ -136,7 +144,7 @@ public void mouseClicked(MouseEvent e) { expressionScrollPane.setPreferredSize(d); expressionScrollPane.setMinimumSize(d); - JPanel operationsPanel = new JPanel(); + operationsPanel = new JPanel(); operationsPanel.setLayout(new GridBagLayout()); operationsPanel.setBorder(BorderFactory.createTitledBorder("Operations")); JButton plusButton = new JButton("+"); @@ -265,45 +273,37 @@ public void mouseClicked(MouseEvent e) { JButton deleteSelection = new JButton("Delete Selection"); deleteSelection.setEnabled(false); - JButton resetExpression = new JButton("Reset Expression"); + resetExpression = new JButton("Reset Expression"); resetExpression.addActionListener(e -> { - ObsExpression oldExpr = currentExpr.deepCopy(); - currentExpr = new ObsPlaceHolder(); - expressionField.setText(currentExpr.toString()); - - if (!oldExpr.isPlaceHolder()) { - undoManager.addEdit(new ExpressionEdit(oldExpr, currentExpr.deepCopy())); - refreshUndoRedoButtons(); - } - }); - - JButton editExpression = new JButton("Edit Expression"); - - editExpression.addActionListener(e -> { - isEditing = !isEditing; - - Enabler.setAllEnabled(operationsPanel, !isEditing); - Enabler.setAllEnabled(placesPanel, !isEditing); - Enabler.setAllEnabled(constantsPanel, !isEditing); - if (isEditing) { - saveButton.setEnabled(false); + try { + System.out.println("Parsing expression: " + expressionField.getText()); + ObsExpression parsedExpr = ObservationParser.parse(expressionField.getText(), tapnNetwork); + toggleManualEditing(); + currentExpr = parsedExpr; + expressionField.setText(currentExpr.toString()); + undoManager.addEdit(new ExpressionEdit(new ObsPlaceHolder(), currentExpr.deepCopy())); + refreshUndoRedoButtons(); + saveButton.setEnabled(!includesPlaceHolder()); + } catch (ParseException | TokenMgrError ex) { + JOptionPane.showMessageDialog(TAPAALGUI.getApp(), ex.getMessage(), "Error during parsing", JOptionPane.ERROR_MESSAGE); + } } else { - saveButton.setEnabled(!includesPlaceHolder()); - } + ObsExpression oldExpr = currentExpr.deepCopy(); + currentExpr = new ObsPlaceHolder(); + expressionField.setText(currentExpr.toString()); - expressionField.setEditable(isEditing); - - if (isEditing) { - resetExpression.setText("Parse Expression"); - editExpression.setText("Cancel"); - } else { - resetExpression.setText("Reset Expression"); - editExpression.setText("Edit Expression"); + if (!oldExpr.isPlaceHolder()) { + undoManager.addEdit(new ExpressionEdit(oldExpr, currentExpr.deepCopy())); + refreshUndoRedoButtons(); + } } }); + editExpression = new JButton("Edit Expression"); + editExpression.addActionListener(e -> toggleManualEditing()); + GridBagConstraints editingGbc = new GridBagConstraints(); editingGbc.gridx = 0; editingGbc.gridy = 0; @@ -411,6 +411,30 @@ public void mouseClicked(MouseEvent e) { pack(); } + private void toggleManualEditing() { + isEditing = !isEditing; + + Enabler.setAllEnabled(operationsPanel, !isEditing); + Enabler.setAllEnabled(placesPanel, !isEditing); + Enabler.setAllEnabled(constantsPanel, !isEditing); + + if (isEditing) { + saveButton.setEnabled(false); + } else { + saveButton.setEnabled(!includesPlaceHolder()); + } + + expressionField.setEditable(isEditing); + + if (isEditing) { + resetExpression.setText("Parse Expression"); + editExpression.setText("Cancel"); + } else { + resetExpression.setText("Reset Expression"); + editExpression.setText("Edit Expression"); + } + } + private void updateExpression(ObsExpression newExpr) { String selectedText = expressionField.getSelectedText(); String fullText = expressionField.getText(); diff --git a/src/main/javacc/dk/aau/cs/model/SMC/ObservationParser.jj b/src/main/javacc/dk/aau/cs/model/SMC/ObservationParser.jj new file mode 100644 index 000000000..3b508d3c3 --- /dev/null +++ b/src/main/javacc/dk/aau/cs/model/SMC/ObservationParser.jj @@ -0,0 +1,148 @@ +options { + STATIC = false; +} + +PARSER_BEGIN(ObservationParser) + +package dk.aau.cs.model.SMC; + +import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork; +import dk.aau.cs.verification.observations.expressions.ObsConstant; +import dk.aau.cs.verification.observations.expressions.ObsPlace; +import dk.aau.cs.verification.observations.expressions.ObsExpression; +import dk.aau.cs.verification.observations.expressions.ObsAdd; +import dk.aau.cs.verification.observations.expressions.ObsSubtract; +import dk.aau.cs.verification.observations.expressions.ObsMultiply; +import dk.aau.cs.verification.observations.expressions.ObsOperator; +import java.io.StringReader; + +public class ObservationParser { + private static TimedArcPetriNetNetwork network; + + public static ObsExpression parse(String observationExpressionStr, TimedArcPetriNetNetwork network) throws ParseException, TokenMgrError { + ObservationParser.network = network; + ObservationParser parser = new ObservationParser(new StringReader(observationExpressionStr)); + + return parser.startParsing(); + } +} + +PARSER_END(ObservationParser) + +TOKEN: +{ + + | + + | + + | + + | + + | + + | + + | + <#ALPHA: ["a"-"z","A"-"Z"]> + | + <#ALPHANUM: (["a"-"z","A"-"Z","0"-"9"])> + | + ("_" | )*> +} + +SKIP : +{ + " " + | "\t" + | "\n" + | "\r" +} + +ObsExpression startParsing(): { + ObsExpression expr; +} { + expr = expression() { return expr; } +} + +ObsExpression expression(): { + ObsExpression left, right; + ObsOperator root; + Token op; +} { + left = term() + ( + (op = | op = ) + { + root = op.kind == PLUS ? + new ObsAdd(left, null) : + new ObsSubtract(left, null); + + if (left.isOperator()) { + ((ObsOperator)left).setParent(root); + } + } + + right = term() + { + root.setRight(right); + if (right.isOperator()) { + ((ObsOperator)right).setParent(root); + } + left = root; + } + )* + { return left; } +} + +ObsExpression term(): { + ObsExpression left, right; + ObsOperator root; +} { + left = factor() + ( + + { + root = new ObsMultiply(left, null); + if (left.isOperator()) { + ((ObsOperator)left).setParent(root); + } + } + + right = factor() + { + root.setRight(right); + if (right.isOperator()) { + ((ObsOperator)right).setParent(root); + } + left = root; + } + )* + { return left; } +} + +ObsExpression factor(): { + ObsExpression expr; +} { + ( + expr = atom() | + expr = expression() + { + if (expr.isOperator()) { + ((ObsOperator)expr).hadParentheses(true); + } + } + ) + { return expr; } +} + +ObsExpression atom(): { + Token value, templateName, placeName; +} { + value = + { return new ObsConstant(Integer.parseInt(value.image)); } + | + templateName = placeName = + { return new ObsPlace(templateName.image, placeName.image, network); } +}