Skip to content

Commit

Permalink
Wrong k-bound passed when using approximation with raw verification -…
Browse files Browse the repository at this point in the history 
… fix 2052379 (#135)

Fixes:
https://bugs.launchpad.net/tapaal/+bug/2052379

Also fixes:
- Issue where gui in some cases would be unable to display trace event
though the xml received from the engine was perfectly fine.
- NPE with color switches when trying to add bindings to a net that is
not unfolded
  • Loading branch information
@srba
srba authored Feb 12, 2024
2 parents b33e6ef + d34bd38 commit bdba796
Show file tree
Hide file tree
Showing 6 changed files with 115 additions and 54 deletions.
6 changes: 3 additions & 3 deletions src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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());
Expand Down
9 changes: 4 additions & 5 deletions src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down
55 changes: 49 additions & 6 deletions src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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)
{
Expand Down Expand Up @@ -172,4 +208,11 @@ public void setInclusionPlaces(InclusionPlaces inclusionPlaces) {
this.inclusionPlaces = inclusionPlaces;
}

public boolean kBoundPresentInRawVerification() {
return kBoundPresentInRawVerificationOptions;
}

public boolean tracePresentInRawVerification() {
return tracePresentInRawVerificationOptions;
}
}
67 changes: 31 additions & 36 deletions src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNTraceParser.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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;
Expand All @@ -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;

Expand Down Expand Up @@ -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++){
Expand All @@ -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;
}
}
Expand Down
26 changes: 24 additions & 2 deletions src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down Expand Up @@ -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);
Expand All @@ -4611,6 +4615,7 @@ public void itemStateChanged(ItemEvent e) {
setVerificationOptionsEnabled(!rawVerificationOptionsEnabled.isSelected());
rawVerificationOptionsTextArea.setEnabled(rawVerificationOptionsEnabled.isSelected());
rawVerificationOptionsHelpButton.setEnabled(rawVerificationOptionsEnabled.isSelected());
updateRawVerificationOptions();
}
});

Expand Down Expand Up @@ -4687,7 +4692,6 @@ private void setVerificationOptionsEnabled(boolean isEnabled) {
setAllEnabled(traceOptionsPanel, isEnabled);
setAllEnabled(boundednessCheckPanel, isEnabled);
setAllEnabled(searchOptionsPanel, isEnabled);
setAllEnabled(overApproximationOptionsPanel, isEnabled);

setEnabledOptionsAccordingToCurrentReduction();
}
Expand Down Expand Up @@ -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() {
Expand Down Expand Up @@ -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
Expand Down
6 changes: 4 additions & 2 deletions src/main/java/net/tapaal/gui/petrinet/verification/RunVerification.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit bdba796

Please sign in to comment.