Fixed k-bound not updating, and fixed exception thrown by loadDocumen…

…t in VerifyTAPNTraceParser.java
TAPAAL · Feb 7, 2024 · 8cd8817 · 8cd8817
1 parent f5ebf0b
commit 8cd8817
Show file tree

Hide file tree

Showing 5 changed files with 37 additions and 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
@@ -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
@@ -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
@@ -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
@@ -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<TimedToken> consumedTokens = new ArrayList<TimedToken>(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("<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;
 		}
 	}

diff --git 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);