From 8bd6d0cf3bd9ea2231183212358c16e9ad3e30ac Mon Sep 17 00:00:00 2001 From: mtygesen Date: Thu, 1 Feb 2024 18:28:56 +0100 Subject: [PATCH 1/3] Added color bindings to simulation --- .../VerifyTAPN/ColorBindingParser.java | 106 ++++++++++++++++++ .../VerifyTAPN/VerifyDTAPNOptions.java | 1 + .../VerifyTAPN/VerifyDTAPNUnfoldOptions.java | 1 + .../VerifyTAPN/VerifyPNOptions.java | 1 + .../VerifyTAPN/VerifyPNUnfoldOptions.java | 3 +- .../VerifyTAPN/VerifyTAPNOptions.java | 4 + .../verification/RunVerification.java | 6 +- .../gui/petrinet/verification/UnfoldNet.java | 43 ++++--- .../gui/petrinet/dataLayer/DataLayer.java | 7 +- 9 files changed, 141 insertions(+), 31 deletions(-) create mode 100644 src/main/java/dk/aau/cs/verification/VerifyTAPN/ColorBindingParser.java diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/ColorBindingParser.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/ColorBindingParser.java new file mode 100644 index 000000000..e60ac7561 --- /dev/null +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/ColorBindingParser.java @@ -0,0 +1,106 @@ +package dk.aau.cs.verification.VerifyTAPN; + +import java.io.ByteArrayInputStream; +import java.io.InputStream; +import java.io.InputStreamReader; +import java.nio.charset.StandardCharsets; +import java.util.HashMap; +import java.util.Map; + +import javax.xml.parsers.SAXParser; +import javax.xml.parsers.SAXParserFactory; + +import org.xml.sax.SAXException; +import org.xml.sax.helpers.DefaultHandler; + +import dk.aau.cs.io.LoadedModel; +import net.tapaal.gui.petrinet.Template; +import pipe.gui.petrinet.dataLayer.DataLayer; +import pipe.gui.petrinet.graphicElements.Transition; + +import org.xml.sax.Attributes; +import org.xml.sax.InputSource; + +public class ColorBindingParser extends DefaultHandler { + private String currentElement = ""; + private String transitionId = ""; + private String variableId = ""; + private String color = ""; + private Map bindings = new HashMap<>(); + + public static void addBindings(LoadedModel loadedModel, String output) { + ColorBindingParser parser = new ColorBindingParser(); + Map bindings = parser.parseBindings(output); + + for (Template net : loadedModel.templates()) { + for (Transition transition : net.guiModel().getTransitions()) { + transition.setToolTipText(bindings.get(transition.getName())); + } + } + } + + public static void addBindings(DataLayer guiModel, String output) { + ColorBindingParser parser = new ColorBindingParser(); + Map bindings = parser.parseBindings(output); + + for (Transition transition : guiModel.getTransitions()) { + transition.setToolTipText(bindings.get(transition.getName())); + } + } + + private Map parseBindings(String output) { + try { + SAXParserFactory factory = SAXParserFactory.newInstance(); + SAXParser parser = factory.newSAXParser(); + + int start = output.indexOf(""); + int end = output.indexOf("") + "".length(); + + String xml = output.substring(start, end); + + InputStream stream = new ByteArrayInputStream(xml.getBytes(StandardCharsets.UTF_8)); + parser.parse(new InputSource(new InputStreamReader(stream, StandardCharsets.UTF_8)), this); + } catch (Exception e) { + e.printStackTrace(); + } + + return bindings; + } + + @Override + public void startElement(String uri, String localName, String qName, Attributes atts) throws SAXException { + currentElement = qName; + + switch (currentElement) { + case "transition": + transitionId = atts.getValue("id"); + break; + + case "variable": + variableId = atts.getValue("id"); + break; + } + } + + @Override + public void endElement(String uri, String localName, String qName) throws SAXException { + if (qName.equalsIgnoreCase("transition")) { + if (!variableId.isEmpty() && !color.isEmpty()) { + bindings.put(transitionId, variableId + " -> " + color); + } + + transitionId = ""; + variableId = ""; + color = ""; + } + + currentElement = ""; + } + + @Override + public void characters(char[] ch, int start, int length) throws SAXException { + if ("color".equals(currentElement)) { + color = new String(ch, start, length); + } + } +} \ No newline at end of file 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..4ab588a55 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNOptions.java @@ -116,6 +116,7 @@ public String toString() { result.append(" --write-unfolded-queries "); result.append(unfoldedQueriesPath); result.append(" "); + result.append("--bindings "); } result.append(searchArg(searchOption)); result.append("--verification-method "); diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNUnfoldOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNUnfoldOptions.java index 2c33ff5b6..b0364d52e 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNUnfoldOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPNUnfoldOptions.java @@ -58,6 +58,7 @@ public String toString() { result.append(" --write-unfolded-net "); result.append(modelOut); result.append(" --search-strategy OverApprox --xml-queries "); + result.append("--bindings "); for(int i = 0; i < numQueries; ++i){ if(i != 0) result.append(","); result.append(i + 1); 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..fe15ea041 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java @@ -225,6 +225,7 @@ public String toString() { if(unfold){ String writeUnfoldedCMD = " --write-unfolded-net " +unfoldedModelPath + " --write-unfolded-queries " + unfoldedQueriesPath; result.append(writeUnfoldedCMD); + result.append(" --bindings "); } if (this.queryCategory == QueryCategory.CTL){ diff --git a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNUnfoldOptions.java b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNUnfoldOptions.java index 2e3163c29..2930e685d 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNUnfoldOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyPNUnfoldOptions.java @@ -80,7 +80,8 @@ public String toString() { if(!symmetricVars){ result.append(" --disable-symmetry-vars"); } - result.append(" --col-reduction 0"); + result.append(" --col-reduction 0 "); + result.append("--bindings "); return result.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 85b0b507e..367529d98 100644 --- a/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java +++ b/src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java @@ -20,6 +20,7 @@ public class VerifyTAPNOptions extends VerificationOptions{ private final boolean symmetry; private final boolean discreteInclusion; private final boolean tarOption; + private boolean isColor; private InclusionPlaces inclusionPlaces; private boolean useRawVerification; private String rawVerificationOptions; @@ -45,6 +46,7 @@ public VerifyTAPNOptions(int extraTokens, TraceOption traceOption, SearchOption this.useRawVerification = useRawVerification; this.rawVerificationOptions = rawVerificationOptions; + this.isColor = isColor; if(isColor && trace() != TraceOption.NONE && !useRawVerification) // we only force unfolding when traces are involved { @@ -110,6 +112,7 @@ public String toString() { result.append(" --write-unfolded-queries "); result.append(unfoldedQueriesPath); result.append(" "); + result.append("--bindings "); } result.append(kBoundArg()); @@ -122,6 +125,7 @@ public String toString() { result.append(' '); result.append(discreteInclusion ? " --inclusion-check 1" : ""); result.append(discreteInclusion ? " --inclusion-places " + generateDiscretePlacesList() : ""); + return result.toString(); } 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 5d481741d..19fc05ccb 100644 --- a/src/main/java/net/tapaal/gui/petrinet/verification/RunVerification.java +++ b/src/main/java/net/tapaal/gui/petrinet/verification/RunVerification.java @@ -18,6 +18,7 @@ import dk.aau.cs.util.Tuple; import dk.aau.cs.util.VerificationCallback; import dk.aau.cs.verification.*; +import dk.aau.cs.verification.VerifyTAPN.ColorBindingParser; import net.tapaal.gui.petrinet.TAPNLens; import net.tapaal.swinghelpers.GridBagHelper; import pipe.gui.MessengerImpl; @@ -87,7 +88,8 @@ protected boolean showResult(VerificationResult result) { if ((lens != null && lens.isColored()) || model.isColored()) { int dialogResult = JOptionPane.showConfirmDialog(null, "There is a trace that will be displayed in a new tab on the unfolded net/query.", "Open trace", JOptionPane.OK_CANCEL_OPTION); if (dialogResult == JOptionPane.OK_OPTION) { - TAPAALGUI.openNewTabFromStream(result.getUnfoldedTab()); + PetriNetTab tab = result.getUnfoldedTab(); + TAPAALGUI.openNewTabFromStream(tab); } else return false; } if (result.getTraceMap() == null) { @@ -101,6 +103,8 @@ protected boolean showResult(VerificationResult result) { } TAPAALGUI.getAnimator().setTrace(result.getTrace(), traceMap); } + + ColorBindingParser.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 diff --git a/src/main/java/net/tapaal/gui/petrinet/verification/UnfoldNet.java b/src/main/java/net/tapaal/gui/petrinet/verification/UnfoldNet.java index ed86c0b7c..f2f012348 100644 --- a/src/main/java/net/tapaal/gui/petrinet/verification/UnfoldNet.java +++ b/src/main/java/net/tapaal/gui/petrinet/verification/UnfoldNet.java @@ -15,6 +15,7 @@ import dk.aau.cs.util.Tuple; import dk.aau.cs.util.UnsupportedModelException; import dk.aau.cs.verification.*; +import dk.aau.cs.verification.VerifyTAPN.ColorBindingParser; import dk.aau.cs.verification.VerifyTAPN.VerifyDTAPNUnfoldOptions; import dk.aau.cs.verification.VerifyTAPN.VerifyPNUnfoldOptions; import pipe.gui.petrinet.dataLayer.DataLayer; @@ -97,7 +98,6 @@ protected String doInBackground() throws Exception { ArrayList