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 4ab588a55..f0c9d0795 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java @@ -102,9 +102,9 @@ public VerifyDTAPNOptions( public String toString() { StringBuilder result = new StringBuilder(); - if (useRawVerification) { - return result.append(rawVerificationOptions).toString(); - } + if (useRawVerification && rawVerificationOptions != null) { + 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 fe15ea041..1804c92a6 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java @@ -183,12 +183,11 @@ public VerifyPNOptions( public String toString() { StringBuilder result = new StringBuilder(); - if (useRawVerification) { - return result.append(rawVerificationOptions).toString(); - } + if (useRawVerification && rawVerificationOptions != null) { + return rawVerificationString(rawVerificationOptions, traceMap.get(traceOption)); + } - 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 c74ba3413..32bacf44b 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,8 @@ 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; @@ -88,20 +90,54 @@ 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 " : ""; + 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(); - if (useRawVerification) { - return result.append(rawVerificationOptions).toString(); - } + if (useRawVerification && rawVerificationOptions != null) { + return rawVerificationString(rawVerificationOptions, traceMap.get(traceOption)); + } if(unfoldedModelPath != null && unfoldedQueriesPath != null) { @@ -172,4 +208,11 @@ public void setInclusionPlaces(InclusionPlaces inclusionPlaces) { this.inclusionPlaces = inclusionPlaces; } + public boolean kBoundPresentInRawVerification() { + return kBoundPresentInRawVerificationOptions; + } + + public boolean tracePresentInRawVerification() { + return tracePresentInRawVerificationOptions; + } } 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..825747b2e 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,29 @@ 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(); + String line; + + while ((line = reader.readLine()) != null) { + if (line.contains("Trace")) continue; + sb.append(line); + sb.append(System.lineSeparator()); + } + + 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 +127,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 +147,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 6551f225e..edd69dad3 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -4373,14 +4373,17 @@ 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); 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 +4596,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 +4615,7 @@ public void itemStateChanged(ItemEvent e) { setVerificationOptionsEnabled(!rawVerificationOptionsEnabled.isSelected()); rawVerificationOptionsTextArea.setEnabled(rawVerificationOptionsEnabled.isSelected()); rawVerificationOptionsHelpButton.setEnabled(rawVerificationOptionsEnabled.isSelected()); + updateRawVerificationOptions(); } }); @@ -4687,7 +4692,6 @@ private void setVerificationOptionsEnabled(boolean isEnabled) { setAllEnabled(traceOptionsPanel, isEnabled); setAllEnabled(boundednessCheckPanel, isEnabled); setAllEnabled(searchOptionsPanel, isEnabled); - setAllEnabled(overApproximationOptionsPanel, isEnabled); setEnabledOptionsAccordingToCurrentReduction(); } @@ -4775,7 +4779,24 @@ 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.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|--trace|-t) +\\d*", ""); + } + rawVerificationOptionsTextArea.setText(rawVerificationOptions.trim()); } private void refreshTraceRefinement() { @@ -5136,6 +5157,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 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