Color bindings to simulation

src/main/java/dk/aau/cs/verification/VerifyTAPN/ColorBindingParser.java

@@ -0,0 +1,117 @@
+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 Map<String, String> bindings = new HashMap<>();
+
+    private String currentElement = "";
+    private String transitionId = "";
+    private String variableId = "";
+    private String color = "";
+
+    /**
+     * Parses output from the verifier and adds the color bindings to the transitions in the loaded model.
+     * @param loadedModel The loaded model to add the bindings to.
+     * @param output The output from the verifier.
+     */
+    public static void addBindings(LoadedModel loadedModel, String output) {
+        ColorBindingParser parser = new ColorBindingParser();
+        Map<String, String> bindings = parser.parseBindings(output);
+
+        for (Template net : loadedModel.templates()) {
+            for (Transition transition : net.guiModel().getTransitions()) {
+                transition.setToolTipText(bindings.get(transition.getName()));
+            }
+        }
+    }
+
+    /**
+     * Parses output from the verifier and adds the color bindings to the transitions in the GUI model.
+     * @param guiModel The GUI model to add the bindings to.
+     * @param output The output from the verifier.
+     */
+    public static void addBindings(DataLayer guiModel, String output) {
+        ColorBindingParser parser = new ColorBindingParser();
+        Map<String, String> bindings = parser.parseBindings(output);
+
+        for (Transition transition : guiModel.getTransitions()) {
+            transition.setToolTipText(bindings.get(transition.getName()));
+        }
+    }
+
+    private Map<String, String> parseBindings(String output) {
+        try {
+            SAXParserFactory factory = SAXParserFactory.newInstance();
+            SAXParser parser = factory.newSAXParser();
+
+            int start = output.indexOf("<bindings>");
+            int end = output.indexOf("</bindings>") + "</bindings>".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);
+        }
+    }
+}

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

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

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

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

src/main/java/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java

@@ -110,6 +110,7 @@ public String toString() {
             result.append(" --write-unfolded-queries ");
             result.append(unfoldedQueriesPath);
             result.append(" ");
+			result.append("--bindings ");
         }
 
 		result.append(kBoundArg());
@@ -122,6 +123,7 @@ public String toString() {
 		result.append(' ');
 		result.append(discreteInclusion ? " --inclusion-check 1" : "");
 		result.append(discreteInclusion ? " --inclusion-places " + generateDiscretePlacesList() : "");
+
 		return result.toString();
 	}
 

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;
@@ -101,6 +102,8 @@ protected boolean showResult(VerificationResult<TAPNNetworkTrace> 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

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<Template> templates = new ArrayList<>(1);
             ArrayList<TAPNQuery> queries = new ArrayList<>(1);
 
-
             network.add(transformedModel.value1());
             for (ColorType ct : model.colorTypes()) {
                 network.add(ct);
@@ -115,9 +115,6 @@ protected String doInBackground() throws Exception {
                 PNMLWriter writerTACPN = new PNMLWriter(network,guiModels, lens);
                 writerTACPN.savePNML(modelFile);
             }
-
-
-
         } catch (IOException | ParserConfigurationException | TransformerException e) {
             e.printStackTrace();
             error.append(e.getMessage());
@@ -158,8 +155,16 @@ protected String doInBackground() throws Exception {
         runner = new ProcessRunner(modelChecker.getPath(), createUnfoldArgumentString(modelFile.getAbsolutePath(), queryFile.getAbsolutePath(), unfoldTACPNOptions));
         runner.run();
 
+        List<String> outputLines = new ArrayList<>();
+        BufferedReader reader = runner.standardOutput();
+        String line;
+
+        while ((line = reader.readLine()) != null) {
+            outputLines.add(line);
+        }
+
         //String errorOutput = readOutput(runner.errorOutput());
-        int netSize = readUnfoldedSize(runner.standardOutput());
+        int netSize = readUnfoldedSize(outputLines);
 
         if(netSize > maxNetSize){
             //We make a thread so the workers doesn't cancel itself before showing the dialog
@@ -188,6 +193,8 @@ protected String doInBackground() throws Exception {
                     thread.stop();
                 }
             }
+
+            ColorBindingParser.addBindings(loadedModel, String.join(System.lineSeparator(), outputLines));
         } catch (FormatException e) {
             e.printStackTrace();
             error.append(e.getMessage());
@@ -266,27 +273,17 @@ private int calculateShift(Template net, boolean calculatingX) {
         return max - min + Constants.PLACE_TRANSITION_HEIGHT + 10;
     }
 
-    private int readUnfoldedSize(BufferedReader reader){
-        try {
-            if (!reader.ready())
-                return 0;
-        } catch (IOException e1) {
-            return 0;
-        }
+    private int readUnfoldedSize(List<String> lines){
         int numElements = 0;
-        String line;
-        try {
-            while ((line = reader.readLine()) != null) {
-                if(line.startsWith("Size of unfolded net: ")){
-                    Pattern p = Pattern.compile("\\d+");
-                    Matcher m = p.matcher(line);
-                    while (m.find()) {
-                        numElements += Integer.parseInt(m.group());
-                    }
+
+        for (String line : lines) {
+            if (line.startsWith("Size of unfolded net: ")){
+                Pattern p = Pattern.compile("\\d+");
+                Matcher m = p.matcher(line);
+                while (m.find()) {
+                    numElements += Integer.parseInt(m.group());
                 }
             }
-        } catch (IOException e) {
-            System.out.println("Got exception: " + e.getMessage());
         }
 
         return numElements;

src/main/java/pipe/gui/petrinet/dataLayer/DataLayer.java

@@ -609,12 +609,7 @@ public Iterable<PetriNetObject> getPetriNetObjectsWithArcPathPoint() {
 	 * @return A List of all the Place objects
 	 */
 	public Place[] getPlaces() {
-		Place[] returnArray = new Place[placesArray.size()];
-
-		for (int i = 0; i < placesArray.size(); i++) {
-			returnArray[i] = placesArray.get(i);
-		}
-		return returnArray;
+		return placesArray.toArray(new Place[0]);
 	}
 
 	/**
@@ -624,12 +619,7 @@ public Place[] getPlaces() {
 	 *         label objects
 	 */
 	public AnnotationNote[] getLabels() {
-		AnnotationNote[] returnArray = new AnnotationNote[labelsArray.size()];
-
-		for (int i = 0; i < labelsArray.size(); i++) {
-			returnArray[i] = labelsArray.get(i);
-		}
-		return returnArray;
+		return labelsArray.toArray(new AnnotationNote[0]);
 	}
 
 	/**
@@ -638,12 +628,7 @@ public AnnotationNote[] getLabels() {
 	 * @return An List of all the Transition objects
 	 */
 	public Transition[] getTransitions() {
-		Transition[] returnArray = new Transition[transitionsArray.size()];
-
-		for (int i = 0; i < transitionsArray.size(); i++) {
-			returnArray[i] = transitionsArray.get(i);
-		}
-		return returnArray;
+		return transitionsArray.toArray(new Transition[0]);
 	}
 
 	/**
@@ -652,12 +637,7 @@ public Transition[] getTransitions() {
 	 * @return An List of all the Arc objects
 	 */
 	public Arc[] getArcs() {
-		Arc[] returnArray = new Arc[arcsArray.size()];
-
-		for (int i = 0; i < arcsArray.size(); i++) {
-			returnArray[i] = arcsArray.get(i);
-		}
-		return returnArray;
+		return arcsArray.toArray(new Arc[0]);
 	}
 
 	public Arc getArcByEndpoints(PlaceTransitionObject source, PlaceTransitionObject target) {