From 22d540d42b0f65a367706161ee9f65c113808867 Mon Sep 17 00:00:00 2001 From: Mikkel Tygesen Date: Sat, 28 Dec 2024 15:32:20 +0100 Subject: [PATCH 1/3] fixed all hyperltl traces not showing in simulator --- .../cs/verification/VerifyTAPN/VerifyPN.java | 13 +- .../gui/petrinet/dialog/QueryDialog.java | 212 +++++++++++++++--- 2 files changed, 178 insertions(+), 47 deletions(-) diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java index 2c86711bb..d999e0efb 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java @@ -481,17 +481,10 @@ private Map parseMultipleTraces(String output, Ve } VerifyTAPNTraceParser traceParser = new VerifyTAPNTraceParser(model.value1()); - Map parsedTracesMap = new LinkedHashMap<>(); - - if(query.getCategory() == QueryCategory.HyperLTL) { - for(int i = 0; i < query.getTraceList().size(); i++) { - traceParser.setTraceToParse(query.getTraceList().get(i)); - TimedArcPetriNetTrace result = traceParser.parseTrace(new BufferedReader(new StringReader(output))); - parsedTracesMap.put(query.getTraceList().get(i), result); - - } - return parsedTracesMap; + if (query.getCategory() == QueryCategory.HyperLTL) { + return traceParser.parseTraces(new BufferedReader(new StringReader(output))); } + return null; } 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..cc0b4707a 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -1,21 +1,83 @@ package net.tapaal.gui.petrinet.dialog; -import java.awt.*; +import java.awt.BorderLayout; +import java.awt.Color; +import java.awt.Component; +import java.awt.ComponentOrientation; +import java.awt.Container; import java.awt.Dialog.ModalityType; -import java.awt.event.*; +import java.awt.Dimension; +import java.awt.FlowLayout; +import java.awt.GridBagConstraints; +import java.awt.GridBagLayout; +import java.awt.GridLayout; +import java.awt.Insets; +import java.awt.Point; +import java.awt.Toolkit; +import java.awt.Window; +import java.awt.event.ActionEvent; +import java.awt.event.ActionListener; +import java.awt.event.FocusEvent; +import java.awt.event.FocusListener; +import java.awt.event.ItemEvent; +import java.awt.event.ItemListener; +import java.awt.event.KeyAdapter; +import java.awt.event.KeyEvent; +import java.awt.event.MouseAdapter; +import java.awt.event.MouseEvent; +import java.awt.event.MouseListener; import java.io.ByteArrayInputStream; import java.io.ByteArrayOutputStream; import java.io.File; import java.io.IOException; import java.text.DecimalFormat; import java.text.DecimalFormatSymbols; -import java.util.*; +import java.util.ArrayList; +import java.util.Enumeration; +import java.util.HashMap; +import java.util.HashSet; +import java.util.Objects; +import java.util.Set; +import java.util.Vector; import java.util.regex.Matcher; import java.util.regex.Pattern; -import javax.swing.*; +import javax.swing.AbstractAction; +import javax.swing.AbstractButton; +import javax.swing.ActionMap; +import javax.swing.BorderFactory; +import javax.swing.Box; +import javax.swing.BoxLayout; +import javax.swing.ButtonGroup; +import javax.swing.DefaultComboBoxModel; +import javax.swing.DefaultListModel; +import javax.swing.ImageIcon; +import javax.swing.InputMap; +import javax.swing.JButton; +import javax.swing.JCheckBox; +import javax.swing.JComboBox; +import javax.swing.JDialog; +import javax.swing.JLabel; +import javax.swing.JList; +import javax.swing.JOptionPane; +import javax.swing.JPanel; +import javax.swing.JRadioButton; +import javax.swing.JRootPane; +import javax.swing.JScrollPane; +import javax.swing.JSeparator; +import javax.swing.JSpinner; +import javax.swing.JTextArea; +import javax.swing.JTextField; +import javax.swing.JTextPane; +import javax.swing.KeyStroke; +import javax.swing.ScrollPaneConstants; +import javax.swing.SwingConstants; +import javax.swing.SwingUtilities; import javax.swing.border.LineBorder; -import javax.swing.event.*; +import javax.swing.event.DocumentEvent; +import javax.swing.event.DocumentListener; +import javax.swing.event.UndoableEditEvent; +import javax.swing.event.UndoableEditListener; import javax.swing.text.MutableAttributeSet; import javax.swing.text.SimpleAttributeSet; import javax.swing.text.StyleConstants; @@ -29,40 +91,111 @@ import javax.xml.parsers.ParserConfigurationException; import javax.xml.transform.TransformerException; -import dk.aau.cs.TCTL.*; +import dk.aau.cs.TCTL.HyperLTLPathScopeNode; +import dk.aau.cs.TCTL.LTLANode; +import dk.aau.cs.TCTL.LTLENode; +import dk.aau.cs.TCTL.LTLFNode; +import dk.aau.cs.TCTL.LTLGNode; +import dk.aau.cs.TCTL.LTLUNode; +import dk.aau.cs.TCTL.LTLXNode; +import dk.aau.cs.TCTL.StringPosition; +import dk.aau.cs.TCTL.TCTLAFNode; +import dk.aau.cs.TCTL.TCTLAGNode; +import dk.aau.cs.TCTL.TCTLAUNode; +import dk.aau.cs.TCTL.TCTLAXNode; +import dk.aau.cs.TCTL.TCTLAbstractPathProperty; +import dk.aau.cs.TCTL.TCTLAbstractProperty; +import dk.aau.cs.TCTL.TCTLAbstractStateProperty; +import dk.aau.cs.TCTL.TCTLAndListNode; +import dk.aau.cs.TCTL.TCTLAtomicPropositionNode; +import dk.aau.cs.TCTL.TCTLConstNode; +import dk.aau.cs.TCTL.TCTLDeadlockNode; +import dk.aau.cs.TCTL.TCTLEFNode; +import dk.aau.cs.TCTL.TCTLEGNode; +import dk.aau.cs.TCTL.TCTLEUNode; +import dk.aau.cs.TCTL.TCTLEXNode; +import dk.aau.cs.TCTL.TCTLFalseNode; +import dk.aau.cs.TCTL.TCTLNotNode; +import dk.aau.cs.TCTL.TCTLOrListNode; +import dk.aau.cs.TCTL.TCTLPathPlaceHolder; +import dk.aau.cs.TCTL.TCTLPathToStateConverter; +import dk.aau.cs.TCTL.TCTLPlaceNode; +import dk.aau.cs.TCTL.TCTLStatePlaceHolder; +import dk.aau.cs.TCTL.TCTLStateToPathConverter; +import dk.aau.cs.TCTL.TCTLTransitionNode; +import dk.aau.cs.TCTL.TCTLTrueNode; import dk.aau.cs.TCTL.CTLParsing.TAPAALCTLQueryParser; import dk.aau.cs.TCTL.HyperLTLParsing.TAPAALHyperLTLQueryParser; import dk.aau.cs.TCTL.LTLParsing.TAPAALLTLQueryParser; -import dk.aau.cs.TCTL.SMCParsing.TAPAALSMCQueryParser; -import dk.aau.cs.TCTL.visitors.*; -import dk.aau.cs.util.VerificationCallback; -import dk.aau.cs.verification.*; -import net.tapaal.gui.petrinet.TAPNLens; -import pipe.gui.petrinet.PetriNetTab; -import dk.aau.cs.model.CPN.ColorType; -import dk.aau.cs.model.CPN.Variable; -import dk.aau.cs.model.tapn.*; -import dk.aau.cs.verification.VerifyTAPN.*; -import net.tapaal.gui.petrinet.verification.*; -import net.tapaal.swinghelpers.CustomJSpinner; -import pipe.gui.petrinet.dataLayer.DataLayer; -import dk.aau.cs.io.NetWriter; -import net.tapaal.gui.petrinet.verification.TAPNQuery; -import net.tapaal.gui.petrinet.Template; -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 pipe.gui.*; import dk.aau.cs.TCTL.Parsing.TAPAALQueryParser; +import dk.aau.cs.TCTL.SMCParsing.TAPAALSMCQueryParser; +import dk.aau.cs.TCTL.visitors.FixAbbrivPlaceNames; +import dk.aau.cs.TCTL.visitors.FixAbbrivTransitionNames; +import dk.aau.cs.TCTL.visitors.HasDeadlockVisitor; +import dk.aau.cs.TCTL.visitors.HyperLTLTraceNameVisitor; +import dk.aau.cs.TCTL.visitors.IsReachabilityVisitor; +import dk.aau.cs.TCTL.visitors.RenameAllPlacesVisitor; +import dk.aau.cs.TCTL.visitors.RenameAllTransitionsVisitor; +import dk.aau.cs.TCTL.visitors.VerifyPlaceNamesVisitor; +import dk.aau.cs.TCTL.visitors.VerifyTransitionNamesVisitor; import dk.aau.cs.approximation.OverApproximation; import dk.aau.cs.approximation.UnderApproximation; +import dk.aau.cs.io.NetWriter; import dk.aau.cs.io.TimedArcPetriNetNetworkWriter; +import dk.aau.cs.model.CPN.ColorType; +import dk.aau.cs.model.CPN.Variable; +import dk.aau.cs.model.tapn.Constant; +import dk.aau.cs.model.tapn.SharedPlace; +import dk.aau.cs.model.tapn.SharedTransition; +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.model.tapn.TimedTransition; import dk.aau.cs.translations.ReductionOption; import dk.aau.cs.util.Tuple; import dk.aau.cs.util.UnsupportedModelException; import dk.aau.cs.util.UnsupportedQueryException; +import dk.aau.cs.util.VerificationCallback; +import dk.aau.cs.verification.ITAPNComposer; +import dk.aau.cs.verification.ModelChecker; +import dk.aau.cs.verification.NameMapping; +import dk.aau.cs.verification.SMCSettings; +import dk.aau.cs.verification.SMCStats; +import dk.aau.cs.verification.SMCTraceType; +import dk.aau.cs.verification.TAPNComposer; import dk.aau.cs.verification.UPPAAL.UppaalExporter; +import dk.aau.cs.verification.VerifyTAPN.VerifyCPNExporter; +import dk.aau.cs.verification.VerifyTAPN.VerifyDTAPN; +import dk.aau.cs.verification.VerifyTAPN.VerifyPN; +import dk.aau.cs.verification.VerifyTAPN.VerifyPNExporter; +import dk.aau.cs.verification.VerifyTAPN.VerifyTAPN; +import dk.aau.cs.verification.VerifyTAPN.VerifyTAPNExporter; +import dk.aau.cs.verification.VerifyTAPN.VerifyTAPNOptions; +import net.tapaal.gui.petrinet.TAPNLens; +import net.tapaal.gui.petrinet.Template; +import net.tapaal.gui.petrinet.verification.ChooseInclusionPlacesDialog; +import net.tapaal.gui.petrinet.verification.EngineSupportOptions; +import net.tapaal.gui.petrinet.verification.InclusionPlaces; +import net.tapaal.gui.petrinet.verification.RunVerificationBase; +import net.tapaal.gui.petrinet.verification.TAPNQuery; +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.gui.petrinet.verification.UPPAALBroadcastDegree2Options; +import net.tapaal.gui.petrinet.verification.UPPAALBroadcastOptions; +import net.tapaal.gui.petrinet.verification.UPPAALCombiOptions; +import net.tapaal.gui.petrinet.verification.UPPAALOptimizedStandardOptions; +import net.tapaal.gui.petrinet.verification.UPPAALStandardOptions; +import net.tapaal.gui.petrinet.verification.Verifier; +import net.tapaal.gui.petrinet.verification.VerifyDTAPNEngineOptions; +import net.tapaal.gui.petrinet.verification.VerifyPNEngineOptions; +import net.tapaal.gui.petrinet.verification.VerifyTAPNEngineOptions; +import net.tapaal.swinghelpers.CustomJSpinner; +import pipe.gui.MessengerImpl; +import pipe.gui.TAPAALGUI; import pipe.gui.canvas.Zoomer; +import pipe.gui.petrinet.PetriNetTab; +import pipe.gui.petrinet.dataLayer.DataLayer; import pipe.gui.swingcomponents.EscapableDialog; import pipe.gui.swingcomponents.filebrowser.FileBrowser; @@ -1915,9 +2048,17 @@ private void setupTraceListFromQuery(TAPNQuery queryToCreateFrom) { // First remove all elements (removes the default trace that was added) traceModel.removeAllElements(); - for(int i = 0; i < queryToCreateFrom.getTraceList().size(); i++) { - traceModel.addElement(queryToCreateFrom.getTraceList().get(i)); + Set traces = new HashSet<>(queryToCreateFrom.getTraceList()); + Pattern pattern = Pattern.compile("\\s([a-zA-Z]\\w+)\\."); + Matcher matcher = pattern.matcher(queryToCreateFrom.getProperty().toString()); + while (matcher.find()) { + traces.add(matcher.group(1)); } + + for (String trace : traces) { + traceModel.addElement(trace); + } + traceList.setModel(traceModel); updateTraceBox(); } @@ -3853,18 +3994,15 @@ private void checkUntimedOrNode() { private void updateTraceBox() { // Updates the trace box drop down menu - ArrayList traceList = getUsedTraces(newProperty); - Vector traceBoxVector = new Vector<>(); - Vector traceBoxQuantificationVector = new Vector<>(); + Set traceBoxSet = new HashSet<>(); + Set traceBoxQuantificationSet = new HashSet<>(); for (int i = 0; i < traceModel.getSize(); i++) { - if (traceList.contains(traceModel.get(i).toString())) - traceBoxVector.add(traceModel.get(i)); - else - traceBoxQuantificationVector.add(traceModel.get(i)); + traceBoxSet.add(traceModel.getElementAt(i)); + traceBoxQuantificationSet.add(traceModel.getElementAt(i)); } - traceBox.setModel(new DefaultComboBoxModel<>(traceBoxVector)); - traceBoxQuantification.setModel(new DefaultComboBoxModel<>(traceBoxQuantificationVector)); + traceBox.setModel(new DefaultComboBoxModel<>(traceBoxSet.toArray(new Object[0]))); + traceBoxQuantification.setModel(new DefaultComboBoxModel<>(traceBoxQuantificationSet.toArray(new Object[0]))); updateHyperLTLButtons(); } From 70e1e3217233e40022a2e981eae370c6f1938573 Mon Sep 17 00:00:00 2001 From: Mikkel Tygesen Date: Sat, 28 Dec 2024 15:37:47 +0100 Subject: [PATCH 2/3] regex fix --- .../java/net/tapaal/gui/petrinet/dialog/QueryDialog.java | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) 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 cc0b4707a..ad8c84c0a 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -2049,11 +2049,11 @@ private void setupTraceListFromQuery(TAPNQuery queryToCreateFrom) { traceModel.removeAllElements(); Set traces = new HashSet<>(queryToCreateFrom.getTraceList()); - Pattern pattern = Pattern.compile("\\s([a-zA-Z]\\w+)\\."); + + // Extracts trace names from the field + Pattern pattern = Pattern.compile("\\s([a-zA-Z]\\w*)\\."); Matcher matcher = pattern.matcher(queryToCreateFrom.getProperty().toString()); - while (matcher.find()) { - traces.add(matcher.group(1)); - } + while (matcher.find()) traces.add(matcher.group(1)); for (String trace : traces) { traceModel.addElement(trace); From 83d8494fff6a734f04514580647c289984fbff15 Mon Sep 17 00:00:00 2001 From: Mikkel Tygesen Date: Sun, 29 Dec 2024 22:54:21 +0100 Subject: [PATCH 3/3] reverted updateTraceBox() --- .../tapaal/gui/petrinet/dialog/QueryDialog.java | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) 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 ad8c84c0a..14727a97e 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -36,6 +36,7 @@ import java.util.Enumeration; import java.util.HashMap; import java.util.HashSet; +import java.util.List; import java.util.Objects; import java.util.Set; import java.util.Vector; @@ -3994,15 +3995,19 @@ private void checkUntimedOrNode() { private void updateTraceBox() { // Updates the trace box drop down menu - Set traceBoxSet = new HashSet<>(); - Set traceBoxQuantificationSet = new HashSet<>(); + List traceList = getUsedTraces(newProperty); + Vector traceBoxVector = new Vector<>(); + Vector traceBoxQuantificationVector = new Vector<>(); for (int i = 0; i < traceModel.getSize(); i++) { - traceBoxSet.add(traceModel.getElementAt(i)); - traceBoxQuantificationSet.add(traceModel.getElementAt(i)); + if (traceList.contains(traceModel.get(i).toString())) { + traceBoxVector.add(traceModel.get(i)); + } else { + traceBoxQuantificationVector.add(traceModel.get(i)); + } } - traceBox.setModel(new DefaultComboBoxModel<>(traceBoxSet.toArray(new Object[0]))); - traceBoxQuantification.setModel(new DefaultComboBoxModel<>(traceBoxQuantificationSet.toArray(new Object[0]))); + traceBox.setModel(new DefaultComboBoxModel<>(traceBoxVector)); + traceBoxQuantification.setModel(new DefaultComboBoxModel<>(traceBoxQuantificationVector)); updateHyperLTLButtons(); }