Wrong k-bound passed when using approximation with raw verification - fix 2052379

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());

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) {

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;
+	}
 }

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<TimedToken> consumedTokens = new ArrayList<TimedToken>(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("<trace>");
+			int startTraceList = xml.indexOf("<trace-list>");
+			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;
 		}
 	}

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<TimedArcPetriNet, NameMapping> 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

src/main/java/net/tapaal/gui/petrinet/verification/RunVerification.java

@@ -103,8 +103,10 @@ protected boolean showResult(VerificationResult<TAPNNetworkTrace> 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