From d3eb8ac84d860b9b14d9d0a95eba445e5477448e Mon Sep 17 00:00:00 2001 From: mtygesen Date: Sun, 4 Feb 2024 14:31:53 +0100 Subject: [PATCH 01/10] Fixed wrong k-bound passed when using approximation with raw verification --- .../cs/verification/VerifyTAPN/VerifyDTAPNOptions.java | 3 +++ .../aau/cs/verification/VerifyTAPN/VerifyPNOptions.java | 6 ++++-- .../cs/verification/VerifyTAPN/VerifyTAPNOptions.java | 9 ++++++++- 3 files changed, 15 insertions(+), 3 deletions(-) diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java index db38d98b9..f9463c446 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java @@ -103,6 +103,9 @@ public String toString() { StringBuilder result = new StringBuilder(); if (useRawVerification) { + if (rawVerificationOptions != null) { + rawVerificationOptions = rawVerificationOptions.replaceAll("(--k-bound|-k) +\\d+", "$1 " + kBound()); + } return result.append(rawVerificationOptions).toString(); } diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java index 677dc19da..d39ff1e55 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java @@ -184,11 +184,13 @@ public String toString() { StringBuilder result = new StringBuilder(); if (useRawVerification) { + if (rawVerificationOptions != null) { + rawVerificationOptions = rawVerificationOptions.replaceAll("(--k-bound|-k) +\\d+", "$1 " + kBound()); + } return result.append(rawVerificationOptions).toString(); } - result.append("--k-bound "); - result.append(extraTokens+tokensInModel); + result.append(kBoundArg()); var traceSwitch =traceMap.get(traceOption) ; if (traceSwitch != null) { diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java index 85b0b507e..5dd691c77 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java @@ -88,9 +88,13 @@ public void setTokensInModel(int tokens){ // TODO: Get rid of this method when v } public String kBoundArg() { - return " --k-bound " + (extraTokens+tokensInModel) + " "; + return "--k-bound " + kBound() + " "; } + public int kBound() { + return (extraTokens + tokensInModel); + } + public String deadTokenArg() { return dontUseDeadPlaces ? " --keep-dead-tokens " : ""; } @@ -100,6 +104,9 @@ public String toString() { StringBuilder result = new StringBuilder(); if (useRawVerification) { + if (rawVerificationOptions != null) { + rawVerificationOptions = rawVerificationOptions.replaceAll("(--k-bound|-k) +\\d+", "$1 " + kBound()); + } return result.append(rawVerificationOptions).toString(); } From fc7528df8d5f7bd33db4eaa40f1c299aad66832c Mon Sep 17 00:00:00 2001 From: Mikkel Date: Mon, 5 Feb 2024 17:25:32 +0100 Subject: [PATCH 02/10] If using approximation with raw verification it will now ignore the --k-bound set in the raw verification box --- .../dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java | 3 ++- .../dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java | 3 ++- .../dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java | 3 ++- 3 files changed, 6 insertions(+), 3 deletions(-) diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java index f9463c446..9f1a16efd 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java @@ -103,7 +103,8 @@ public String toString() { StringBuilder result = new StringBuilder(); if (useRawVerification) { - if (rawVerificationOptions != null) { + // TODO: temporary fix overriding k-bound if using approximation with raw verification + if (rawVerificationOptions != null && (enabledOverApproximation || enabledUnderApproximation)) { rawVerificationOptions = rawVerificationOptions.replaceAll("(--k-bound|-k) +\\d+", "$1 " + kBound()); } return result.append(rawVerificationOptions).toString(); diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java index d39ff1e55..f2d2bf85a 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java @@ -184,7 +184,8 @@ public String toString() { StringBuilder result = new StringBuilder(); if (useRawVerification) { - if (rawVerificationOptions != null) { + // TODO: temporary fix overriding k-bound if using approximation with raw verification + if (rawVerificationOptions != null && (enabledOverApproximation || enabledUnderApproximation)) { rawVerificationOptions = rawVerificationOptions.replaceAll("(--k-bound|-k) +\\d+", "$1 " + kBound()); } return result.append(rawVerificationOptions).toString(); diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java index 5dd691c77..b580c0cb2 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java @@ -104,7 +104,8 @@ public String toString() { StringBuilder result = new StringBuilder(); if (useRawVerification) { - if (rawVerificationOptions != null) { + // TODO: temporary fix overriding k-bound if using approximation with raw verification + if (rawVerificationOptions != null && (enabledOverApproximation || enabledUnderApproximation)) { rawVerificationOptions = rawVerificationOptions.replaceAll("(--k-bound|-k) +\\d+", "$1 " + kBound()); } return result.append(rawVerificationOptions).toString(); From 47b1e198295be2974c617b5edfa3d195e82493b0 Mon Sep 17 00:00:00 2001 From: Mikkel Date: Tue, 6 Feb 2024 18:55:56 +0100 Subject: [PATCH 03/10] Added warning that k-bound will be overwritten --- .../VerifyTAPN/VerifyDTAPNOptions.java | 13 ++++++++++--- .../VerifyTAPN/VerifyPNOptions.java | 11 ++++++++++- .../VerifyTAPN/VerifyTAPNOptions.java | 17 ++++++++++++++--- .../gui/petrinet/dialog/QueryDialog.java | 18 ++++++++++++++++-- 4 files changed, 50 insertions(+), 9 deletions(-) diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java index 9f1a16efd..84a5a82c4 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java @@ -103,10 +103,17 @@ public String toString() { StringBuilder result = new StringBuilder(); if (useRawVerification) { - // TODO: temporary fix overriding k-bound if using approximation with raw verification - if (rawVerificationOptions != null && (enabledOverApproximation || enabledUnderApproximation)) { - rawVerificationOptions = rawVerificationOptions.replaceAll("(--k-bound|-k) +\\d+", "$1 " + kBound()); + // TODO: temporary fix overriding k-bound if using approximation with raw verification + if (rawVerificationOptions != null && (enabledOverApproximation || enabledUnderApproximation)) { + kBoundPresentInRawVerificationOptions = rawVerificationOptions.contains("--k-bound") || + rawVerificationOptions.contains("-k"); + if (kBoundPresentInRawVerificationOptions) { + rawVerificationOptions = rawVerificationOptions.replaceAll("(--k-bound|-k) +\\d+", "$1 " + kBound()); + } else { + result.append(kBoundArg()); + } } + return result.append(rawVerificationOptions).toString(); } diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java index f2d2bf85a..0090a25bb 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java @@ -4,6 +4,8 @@ import java.io.IOException; import java.util.Map; +import javax.swing.JOptionPane; + import net.tapaal.gui.petrinet.verification.TAPNQuery.SearchOption; import net.tapaal.gui.petrinet.verification.TAPNQuery.QueryReductionTime; import net.tapaal.gui.petrinet.verification.TAPNQuery.TraceOption; @@ -186,8 +188,15 @@ public String toString() { if (useRawVerification) { // TODO: temporary fix overriding k-bound if using approximation with raw verification if (rawVerificationOptions != null && (enabledOverApproximation || enabledUnderApproximation)) { - rawVerificationOptions = rawVerificationOptions.replaceAll("(--k-bound|-k) +\\d+", "$1 " + kBound()); + kBoundPresentInRawVerificationOptions = rawVerificationOptions.contains("--k-bound") || + rawVerificationOptions.contains("-k"); + if (kBoundPresentInRawVerificationOptions) { + rawVerificationOptions = rawVerificationOptions.replaceAll("(--k-bound|-k) +\\d+", "$1 " + kBound()); + } else { + result.append(kBoundArg()); + } } + return result.append(rawVerificationOptions).toString(); } diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java index b580c0cb2..3032b643a 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java @@ -17,6 +17,7 @@ public class VerifyTAPNOptions extends VerificationOptions{ protected int tokensInModel; + protected boolean kBoundPresentInRawVerificationOptions; private final boolean symmetry; private final boolean discreteInclusion; private final boolean tarOption; @@ -104,10 +105,17 @@ public String toString() { StringBuilder result = new StringBuilder(); if (useRawVerification) { - // TODO: temporary fix overriding k-bound if using approximation with raw verification - if (rawVerificationOptions != null && (enabledOverApproximation || enabledUnderApproximation)) { - rawVerificationOptions = rawVerificationOptions.replaceAll("(--k-bound|-k) +\\d+", "$1 " + kBound()); + // TODO: temporary fix overriding k-bound if using approximation with raw verification + if (rawVerificationOptions != null && (enabledOverApproximation || enabledUnderApproximation)) { + kBoundPresentInRawVerificationOptions = rawVerificationOptions.contains("--k-bound") || + rawVerificationOptions.contains("-k"); + if (kBoundPresentInRawVerificationOptions) { + rawVerificationOptions = rawVerificationOptions.replaceAll("(--k-bound|-k) +\\d+", "$1 " + kBound()); + } else { + result.append(kBoundArg()); + } } + return result.append(rawVerificationOptions).toString(); } @@ -178,4 +186,7 @@ public void setInclusionPlaces(InclusionPlaces inclusionPlaces) { this.inclusionPlaces = inclusionPlaces; } + public boolean kBoundPresentInRawVerificationOptions() { + return kBoundPresentInRawVerificationOptions; + } } 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 08819f2de..31fd2a820 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -4377,10 +4377,12 @@ private void initOverApproximationPanel() { overApproximationEnable = new JRadioButton("Over-approximation"); overApproximationEnable.setVisible(true); overApproximationEnable.setToolTipText(TOOL_TIP_APPROXIMATION_METHOD_OVER); + overApproximationEnable.addActionListener(e -> updateRawVerificationOptions()); underApproximationEnable = new JRadioButton("Under-approximation"); underApproximationEnable.setVisible(true); underApproximationEnable.setToolTipText(TOOL_TIP_APPROXIMATION_METHOD_UNDER); + underApproximationEnable.addActionListener(e -> updateRawVerificationOptions()); approximationRadioButtonGroup.add(noApproximationEnable); approximationRadioButtonGroup.add(overApproximationEnable); @@ -4593,6 +4595,7 @@ private void initRawVerificationOptionsPanel() { rawVerificationOptionsEnabled.setToolTipText(TOOL_TIP_RAW_VERIFICATION_ENABLED_CHECKBOX); rawVerificationOptionsTextArea = new JTextArea(); + rawVerificationOptionsTextArea.setEnabled(false); rawVerificationOptionsTextArea.setToolTipText(TOOL_TIP_RAW_VERIFICATION_TEXT_FIELD); rawVerificationOptionsTextArea.setLineWrap(true); @@ -4611,6 +4614,7 @@ public void itemStateChanged(ItemEvent e) { setVerificationOptionsEnabled(!rawVerificationOptionsEnabled.isSelected()); rawVerificationOptionsTextArea.setEnabled(rawVerificationOptionsEnabled.isSelected()); rawVerificationOptionsHelpButton.setEnabled(rawVerificationOptionsEnabled.isSelected()); + updateRawVerificationOptions(); } }); @@ -4687,7 +4691,6 @@ private void setVerificationOptionsEnabled(boolean isEnabled) { setAllEnabled(traceOptionsPanel, isEnabled); setAllEnabled(boundednessCheckPanel, isEnabled); setAllEnabled(searchOptionsPanel, isEnabled); - setAllEnabled(overApproximationOptionsPanel, isEnabled); setEnabledOptionsAccordingToCurrentReduction(); } @@ -4775,7 +4778,17 @@ private void updateRawVerificationOptions() { Tuple transformedModel = composer.transformModel(QueryDialog.this.tapnNetwork); verifytapnOptions.setTokensInModel(transformedModel.value1().getNumberOfTokensInNet()); - rawVerificationOptionsTextArea.setText(verifytapnOptions.toString()); + String rawVerificationOptions = verifytapnOptions.toString(); + + if (verifytapnOptions.enabledOverApproximation() || verifytapnOptions.enabledUnderApproximation()) { + if (verifytapnOptions.kBoundPresentInRawVerificationOptions()) { + JOptionPane.showMessageDialog(QueryDialog.this, + "Because over/under-approximation is active, the specified k-bound in the custom verification options will be overwritten.", "Warning", + JOptionPane.WARNING_MESSAGE); + } + rawVerificationOptions = rawVerificationOptions.replaceAll("(--k-bound|-k) +\\d+", ""); + } + rawVerificationOptionsTextArea.setText(rawVerificationOptions.trim()); } private void refreshTraceRefinement() { @@ -5136,6 +5149,7 @@ public void actionPerformed(ActionEvent evt) { } }); saveAndVerifyButton.addActionListener(evt -> { + updateRawVerificationOptions(); if (checkIfSomeReductionOption()) { querySaved = true; // Now if a query is saved and verified, the net is marked as modified From f5ebf0b8ca8a71a3f341b2baf7242e280412cd48 Mon Sep 17 00:00:00 2001 From: Mikkel Date: Tue, 6 Feb 2024 18:57:57 +0100 Subject: [PATCH 04/10] Remove unused import --- .../java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java index 0090a25bb..9e9176204 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java @@ -4,8 +4,6 @@ import java.io.IOException; import java.util.Map; -import javax.swing.JOptionPane; - import net.tapaal.gui.petrinet.verification.TAPNQuery.SearchOption; import net.tapaal.gui.petrinet.verification.TAPNQuery.QueryReductionTime; import net.tapaal.gui.petrinet.verification.TAPNQuery.TraceOption; From 8cd881722206a12268e9722c7feed0e98b77c0c6 Mon Sep 17 00:00:00 2001 From: Mikkel Date: Wed, 7 Feb 2024 23:58:13 +0100 Subject: [PATCH 05/10] Fixed k-bound not updating, and fixed exception thrown by loadDocument in VerifyTAPNTraceParser.java --- .../VerifyTAPN/VerifyDTAPNOptions.java | 4 +- .../VerifyTAPN/VerifyPNOptions.java | 2 + .../VerifyTAPN/VerifyTAPNOptions.java | 4 +- .../VerifyTAPN/VerifyTAPNTraceParser.java | 64 ++++++++----------- .../gui/petrinet/dialog/QueryDialog.java | 1 + 5 files changed, 37 insertions(+), 38 deletions(-) diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java index 84a5a82c4..85fd011a6 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java @@ -112,7 +112,9 @@ public String toString() { } else { result.append(kBoundArg()); } - } + } else { + result.append(kBoundArg()); + } return result.append(rawVerificationOptions).toString(); } diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java index 9e9176204..d66d7b1a5 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java @@ -193,6 +193,8 @@ public String toString() { } else { result.append(kBoundArg()); } + } else { + result.append(kBoundArg()); } return result.append(rawVerificationOptions).toString(); diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java index 3032b643a..aefa23ff7 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java @@ -114,7 +114,9 @@ public String toString() { } else { result.append(kBoundArg()); } - } + } else { + result.append(kBoundArg()); + } return result.append(rawVerificationOptions).toString(); } diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNTraceParser.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNTraceParser.java index 1aa1632a4..8eb11e210 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNTraceParser.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNTraceParser.java @@ -2,6 +2,7 @@ import java.io.BufferedReader; import java.io.IOException; +import java.io.StringReader; import java.math.BigDecimal; import java.util.ArrayList; import java.util.List; @@ -13,10 +14,8 @@ import dk.aau.cs.model.CPN.ColorType; import org.w3c.dom.*; -import org.xml.sax.ErrorHandler; import org.xml.sax.InputSource; import org.xml.sax.SAXException; -import org.xml.sax.SAXParseException; import dk.aau.cs.model.NTA.trace.TraceToken; import dk.aau.cs.model.tapn.TimedArcPetriNet; @@ -40,7 +39,26 @@ public VerifyTAPNTraceParser(TimedArcPetriNet tapn) { public TimedArcPetriNetTrace parseTrace(BufferedReader reader) { TimedArcPetriNetTrace trace = new TimedArcPetriNetTrace(true); - Document document = loadDocument(reader); + Document document = null; + + try { + StringBuilder sb = new StringBuilder(); + int c; + while ((c = reader.read()) != -1) { + sb.append((char) c); + } + + String xml = sb.toString(); + document = loadDocument(xml); + } catch (IOException e) { + e.printStackTrace(); + } finally { + try { + reader.close(); + } catch (IOException e) { + e.printStackTrace(); + } + } if(document == null) return null; @@ -106,7 +124,6 @@ public String getTraceNameToParse() { private TimedTransitionStep parseTransitionStep(Element element) { TimedTransition transition = tapn.getTransitionByName(element.getAttribute("id")); - NodeList tokenNodes = element.getChildNodes(); List consumedTokens = new ArrayList(tokenNodes.getLength()); for(int i = 0; i < tokenNodes.getLength(); i++){ @@ -127,42 +144,17 @@ private TimeDelayStep parseTimeDelay(Element element) { return new TimeDelayStep(new BigDecimal(element.getTextContent())); } - private Document loadDocument(BufferedReader reader) { + private Document loadDocument(String xml) { try { - boolean shouldSkip = false; - // We need to reset the buffer if we a trace-list: - reader.mark(10000); - String line = reader.readLine(); - try { - if(line.equals("Trace")) shouldSkip = true; - reader.reset(); - } catch (NullPointerException e) { - return null; - } - - if(shouldSkip) reader.readLine(); // first line is "Trace:" + // Check if valid xml + int startTrace = xml.indexOf(""); + int startTraceList = xml.indexOf(""); + if (startTrace == -1 && startTraceList == -1) return null; DocumentBuilder builder = DocumentBuilderFactory.newInstance().newDocumentBuilder(); - builder.setErrorHandler(new ErrorHandler() { - - @Override - public void warning(SAXParseException exception) throws SAXException { - throw exception; - } - - @Override - public void fatalError(SAXParseException exception) throws SAXException { - throw exception; - } - - @Override - public void error(SAXParseException exception) throws SAXException { - throw exception; - } - }); - return builder.parse(new InputSource(reader)); + return builder.parse(new InputSource(new StringReader(xml))); } catch (ParserConfigurationException | IOException | SAXException e) { - e.printStackTrace(); + e.printStackTrace(); 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 31fd2a820..28ee09253 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -4373,6 +4373,7 @@ private void initOverApproximationPanel() { noApproximationEnable.setVisible(true); noApproximationEnable.setSelected(true); noApproximationEnable.setToolTipText(TOOL_TIP_APPROXIMATION_METHOD_NONE); + noApproximationEnable.addActionListener(e -> updateRawVerificationOptions()); overApproximationEnable = new JRadioButton("Over-approximation"); overApproximationEnable.setVisible(true); From e7006073a0c67850b22522f92edb52be3515cfed Mon Sep 17 00:00:00 2001 From: Mikkel Date: Thu, 8 Feb 2024 19:31:04 +0100 Subject: [PATCH 06/10] Fixed issue with --k-bound duplicating --- .../VerifyTAPN/VerifyDTAPNOptions.java | 18 ++++++--------- .../VerifyTAPN/VerifyPNOptions.java | 22 ++++++++----------- .../VerifyTAPN/VerifyTAPNOptions.java | 18 ++++++--------- 3 files changed, 23 insertions(+), 35 deletions(-) diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java index 85fd011a6..45e7f6fc7 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java @@ -102,17 +102,13 @@ public VerifyDTAPNOptions( public String toString() { StringBuilder result = new StringBuilder(); - if (useRawVerification) { - // TODO: temporary fix overriding k-bound if using approximation with raw verification - if (rawVerificationOptions != null && (enabledOverApproximation || enabledUnderApproximation)) { - kBoundPresentInRawVerificationOptions = rawVerificationOptions.contains("--k-bound") || - rawVerificationOptions.contains("-k"); - if (kBoundPresentInRawVerificationOptions) { - rawVerificationOptions = rawVerificationOptions.replaceAll("(--k-bound|-k) +\\d+", "$1 " + kBound()); - } else { - result.append(kBoundArg()); - } - } else { + // TODO: temporary fix overriding k-bound if using approximation with raw verification + if (useRawVerification && rawVerificationOptions != null) { + kBoundPresentInRawVerificationOptions = rawVerificationOptions.contains("--k-bound") || + rawVerificationOptions.contains("-k"); + if ((enabledOverApproximation || enabledUnderApproximation) && kBoundPresentInRawVerificationOptions) { + rawVerificationOptions = rawVerificationOptions.replaceAll("(--k-bound|-k) +\\d+", "$1 " + kBound()); + } else if (!kBoundPresentInRawVerificationOptions) { result.append(kBoundArg()); } diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java index d66d7b1a5..4b579b58c 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java @@ -183,19 +183,15 @@ public VerifyPNOptions( public String toString() { StringBuilder result = new StringBuilder(); - if (useRawVerification) { - // TODO: temporary fix overriding k-bound if using approximation with raw verification - if (rawVerificationOptions != null && (enabledOverApproximation || enabledUnderApproximation)) { - kBoundPresentInRawVerificationOptions = rawVerificationOptions.contains("--k-bound") || - rawVerificationOptions.contains("-k"); - if (kBoundPresentInRawVerificationOptions) { - rawVerificationOptions = rawVerificationOptions.replaceAll("(--k-bound|-k) +\\d+", "$1 " + kBound()); - } else { - result.append(kBoundArg()); - } - } else { - result.append(kBoundArg()); - } + // TODO: temporary fix overriding k-bound if using approximation with raw verification + if (useRawVerification && rawVerificationOptions != null) { + kBoundPresentInRawVerificationOptions = rawVerificationOptions.contains("--k-bound") || + rawVerificationOptions.contains("-k"); + if ((enabledOverApproximation || enabledUnderApproximation) && kBoundPresentInRawVerificationOptions) { + rawVerificationOptions = rawVerificationOptions.replaceAll("(--k-bound|-k) +\\d+", "$1 " + kBound()); + } else if (!kBoundPresentInRawVerificationOptions) { + result.append(kBoundArg()); + } return result.append(rawVerificationOptions).toString(); } diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java index aefa23ff7..2f8c83760 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java @@ -104,17 +104,13 @@ public String deadTokenArg() { public String toString() { StringBuilder result = new StringBuilder(); - if (useRawVerification) { - // TODO: temporary fix overriding k-bound if using approximation with raw verification - if (rawVerificationOptions != null && (enabledOverApproximation || enabledUnderApproximation)) { - kBoundPresentInRawVerificationOptions = rawVerificationOptions.contains("--k-bound") || - rawVerificationOptions.contains("-k"); - if (kBoundPresentInRawVerificationOptions) { - rawVerificationOptions = rawVerificationOptions.replaceAll("(--k-bound|-k) +\\d+", "$1 " + kBound()); - } else { - result.append(kBoundArg()); - } - } else { + // TODO: temporary fix overriding k-bound if using approximation with raw verification + if (useRawVerification && rawVerificationOptions != null) { + kBoundPresentInRawVerificationOptions = rawVerificationOptions.contains("--k-bound") || + rawVerificationOptions.contains("-k"); + if ((enabledOverApproximation || enabledUnderApproximation) && kBoundPresentInRawVerificationOptions) { + rawVerificationOptions = rawVerificationOptions.replaceAll("(--k-bound|-k) +\\d+", "$1 " + kBound()); + } else if (!kBoundPresentInRawVerificationOptions) { result.append(kBoundArg()); } From 9dc720256255a7b32ca59cf3780ecb21ab453f8e Mon Sep 17 00:00:00 2001 From: Mikkel Date: Sun, 11 Feb 2024 21:40:25 +0100 Subject: [PATCH 07/10] Raw verification options now overwrite --trace as well --- .../VerifyTAPN/VerifyDTAPNOptions.java | 13 +---- .../VerifyTAPN/VerifyPNOptions.java | 15 +---- .../VerifyTAPN/VerifyTAPNOptions.java | 56 ++++++++++++++----- .../gui/petrinet/dialog/QueryDialog.java | 11 +++- 4 files changed, 55 insertions(+), 40 deletions(-) diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java index 45e7f6fc7..7c794df2b 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java @@ -102,18 +102,9 @@ public VerifyDTAPNOptions( public String toString() { StringBuilder result = new StringBuilder(); - // TODO: temporary fix overriding k-bound if using approximation with raw verification if (useRawVerification && rawVerificationOptions != null) { - kBoundPresentInRawVerificationOptions = rawVerificationOptions.contains("--k-bound") || - rawVerificationOptions.contains("-k"); - if ((enabledOverApproximation || enabledUnderApproximation) && kBoundPresentInRawVerificationOptions) { - rawVerificationOptions = rawVerificationOptions.replaceAll("(--k-bound|-k) +\\d+", "$1 " + kBound()); - } else if (!kBoundPresentInRawVerificationOptions) { - result.append(kBoundArg()); - } - - return result.append(rawVerificationOptions).toString(); - } + return rawVerificationString(rawVerificationOptions, traceArg(traceOption)); + } result.append(kBoundArg()); result.append(deadTokenArg()); diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java index 4b579b58c..10f5b3b48 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java @@ -183,18 +183,9 @@ public VerifyPNOptions( public String toString() { StringBuilder result = new StringBuilder(); - // TODO: temporary fix overriding k-bound if using approximation with raw verification - if (useRawVerification && rawVerificationOptions != null) { - kBoundPresentInRawVerificationOptions = rawVerificationOptions.contains("--k-bound") || - rawVerificationOptions.contains("-k"); - if ((enabledOverApproximation || enabledUnderApproximation) && kBoundPresentInRawVerificationOptions) { - rawVerificationOptions = rawVerificationOptions.replaceAll("(--k-bound|-k) +\\d+", "$1 " + kBound()); - } else if (!kBoundPresentInRawVerificationOptions) { - result.append(kBoundArg()); - } - - return result.append(rawVerificationOptions).toString(); - } + if (useRawVerification && rawVerificationOptions != null) { + return rawVerificationString(rawVerificationOptions, traceMap.get(traceOption)); + } result.append(kBoundArg()); diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java index 2f8c83760..78f39457d 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java @@ -18,6 +18,7 @@ public class VerifyTAPNOptions extends VerificationOptions{ protected int tokensInModel; protected boolean kBoundPresentInRawVerificationOptions; + protected boolean tracePresentInRawVerificationOptions; private final boolean symmetry; private final boolean discreteInclusion; private final boolean tarOption; @@ -91,31 +92,52 @@ public void setTokensInModel(int tokens){ // TODO: Get rid of this method when v public String kBoundArg() { return "--k-bound " + kBound() + " "; } - + public int kBound() { return (extraTokens + tokensInModel); } - + public String deadTokenArg() { - return dontUseDeadPlaces ? " --keep-dead-tokens " : ""; + return dontUseDeadPlaces ? " --keep-dead-tokens " : ""; } + + protected String rawVerificationString(String rawVerificationOptions, String traceArg) { + StringBuilder sb = new StringBuilder(); + + // TODO: temporary fix overriding k-bound and trace if using approximation with raw verification + kBoundPresentInRawVerificationOptions = rawVerificationOptions.contains("--k-bound") || + rawVerificationOptions.contains("-k"); + tracePresentInRawVerificationOptions = rawVerificationOptions.contains("--trace") || + rawVerificationOptions.contains("-t"); + + if (enabledOverApproximation || enabledUnderApproximation) { + if (kBoundPresentInRawVerificationOptions) { + rawVerificationOptions = rawVerificationOptions.replaceAll("(--k-bound|-k) +\\d+", "$1 " + kBound()); + } + + if (tracePresentInRawVerificationOptions) { + rawVerificationOptions = rawVerificationOptions.replaceAll("(--trace|-t) +\\d+", "$1 " + traceArg); + } + } + + if (!kBoundPresentInRawVerificationOptions) { + sb.append(kBoundArg()); + } + + if (!tracePresentInRawVerificationOptions) { + sb.append(traceArg); + } + return sb.append(rawVerificationOptions).toString(); + } + @Override public String toString() { StringBuilder result = new StringBuilder(); - // TODO: temporary fix overriding k-bound if using approximation with raw verification if (useRawVerification && rawVerificationOptions != null) { - kBoundPresentInRawVerificationOptions = rawVerificationOptions.contains("--k-bound") || - rawVerificationOptions.contains("-k"); - if ((enabledOverApproximation || enabledUnderApproximation) && kBoundPresentInRawVerificationOptions) { - rawVerificationOptions = rawVerificationOptions.replaceAll("(--k-bound|-k) +\\d+", "$1 " + kBound()); - } else if (!kBoundPresentInRawVerificationOptions) { - result.append(kBoundArg()); - } - - return result.append(rawVerificationOptions).toString(); - } + return rawVerificationString(rawVerificationOptions, traceMap.get(traceOption)); + } if(unfoldedModelPath != null && unfoldedQueriesPath != null) { @@ -184,7 +206,11 @@ public void setInclusionPlaces(InclusionPlaces inclusionPlaces) { this.inclusionPlaces = inclusionPlaces; } - public boolean kBoundPresentInRawVerificationOptions() { + public boolean kBoundPresentInRawVerification() { return kBoundPresentInRawVerificationOptions; } + + public boolean tracePresentInRawVerification() { + return tracePresentInRawVerificationOptions; + } } 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 28ee09253..e55c2fb77 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -4782,12 +4782,19 @@ private void updateRawVerificationOptions() { String rawVerificationOptions = verifytapnOptions.toString(); if (verifytapnOptions.enabledOverApproximation() || verifytapnOptions.enabledUnderApproximation()) { - if (verifytapnOptions.kBoundPresentInRawVerificationOptions()) { + if (verifytapnOptions.kBoundPresentInRawVerification() && verifytapnOptions.tracePresentInRawVerification()) { + JOptionPane.showMessageDialog(QueryDialog.this, "Because over/under-approximation is active, the specified k-bound and trace in the custom verification options will be overwritten.", "Warning", JOptionPane.WARNING_MESSAGE); + } else if (verifytapnOptions.kBoundPresentInRawVerification()) { JOptionPane.showMessageDialog(QueryDialog.this, "Because over/under-approximation is active, the specified k-bound in the custom verification options will be overwritten.", "Warning", JOptionPane.WARNING_MESSAGE); + } else if (verifytapnOptions.tracePresentInRawVerification()) { + JOptionPane.showMessageDialog(QueryDialog.this, + "Because over/under-approximation is active, the specified trace in the custom verification options will be overwritten.", "Warning", + JOptionPane.WARNING_MESSAGE); } - rawVerificationOptions = rawVerificationOptions.replaceAll("(--k-bound|-k) +\\d+", ""); + + rawVerificationOptions = rawVerificationOptions.replaceAll("(--k-bound|-k|--trace|-t) +\\d*", ""); } rawVerificationOptionsTextArea.setText(rawVerificationOptions.trim()); } From dc12018e374d326bf6f47f98812d6b082e372337 Mon Sep 17 00:00:00 2001 From: Mikkel Date: Sun, 11 Feb 2024 22:06:48 +0100 Subject: [PATCH 08/10] Fixed issue that would cause problems showing traces in certain cases --- .../verification/VerifyTAPN/VerifyTAPNTraceParser.java | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNTraceParser.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNTraceParser.java index 8eb11e210..e1b09e4c5 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNTraceParser.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNTraceParser.java @@ -43,9 +43,12 @@ public TimedArcPetriNetTrace parseTrace(BufferedReader reader) { try { StringBuilder sb = new StringBuilder(); - int c; - while ((c = reader.read()) != -1) { - sb.append((char) c); + String line; + + while ((line = reader.readLine()) != null) { + if (line.contains("Trace")) continue; + sb.append(line); + sb.append(System.lineSeparator()); } String xml = sb.toString(); @@ -151,6 +154,7 @@ private Document loadDocument(String xml) { int startTraceList = xml.indexOf(""); if (startTrace == -1 && startTraceList == -1) return null; + System.out.println(xml); DocumentBuilder builder = DocumentBuilderFactory.newInstance().newDocumentBuilder(); return builder.parse(new InputSource(new StringReader(xml))); } catch (ParserConfigurationException | IOException | SAXException e) { From ca523460ba00a414ec109fb97ebaaf4a6e5dbd05 Mon Sep 17 00:00:00 2001 From: Mikkel Date: Sun, 11 Feb 2024 22:08:03 +0100 Subject: [PATCH 09/10] Removed debug logging --- .../aau/cs/verification/VerifyTAPN/VerifyTAPNTraceParser.java | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNTraceParser.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNTraceParser.java index e1b09e4c5..825747b2e 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNTraceParser.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNTraceParser.java @@ -44,7 +44,7 @@ public TimedArcPetriNetTrace parseTrace(BufferedReader reader) { try { StringBuilder sb = new StringBuilder(); String line; - + while ((line = reader.readLine()) != null) { if (line.contains("Trace")) continue; sb.append(line); @@ -154,7 +154,6 @@ private Document loadDocument(String xml) { int startTraceList = xml.indexOf(""); if (startTrace == -1 && startTraceList == -1) return null; - System.out.println(xml); DocumentBuilder builder = DocumentBuilderFactory.newInstance().newDocumentBuilder(); return builder.parse(new InputSource(new StringReader(xml))); } catch (ParserConfigurationException | IOException | SAXException e) { From d34bd385c780d048f5d8d3a8e7e8ae547f2449c7 Mon Sep 17 00:00:00 2001 From: Mikkel Date: Mon, 12 Feb 2024 15:12:53 +0100 Subject: [PATCH 10/10] Fixed NPE when trying to add bindings to net that should not be unfolded --- .../tapaal/gui/petrinet/verification/RunVerification.java | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/main/java/net/tapaal/gui/petrinet/verification/RunVerification.java b/src/main/java/net/tapaal/gui/petrinet/verification/RunVerification.java index 044179b92..00be347d4 100644 --- a/src/main/java/net/tapaal/gui/petrinet/verification/RunVerification.java +++ b/src/main/java/net/tapaal/gui/petrinet/verification/RunVerification.java @@ -103,8 +103,10 @@ protected boolean showResult(VerificationResult result) { TAPAALGUI.getAnimator().setTrace(result.getTrace(), traceMap); } - ColorBindingParser parser = new ColorBindingParser(); - parser.addBindings(result.getUnfoldedTab().getModel(), result.getRawOutput()); + if (result.getUnfoldedTab() != null) { + ColorBindingParser parser = new ColorBindingParser(); + parser.addBindings(result.getUnfoldedTab().getModel(), result.getRawOutput()); + } } else { if (( //XXX: this is not complete, we need a better way to signal the engine could not create a trace