SMC observations

src/main/java/dk/aau/cs/TCTL/visitors/SMCQueryVisitor.java

@@ -1,7 +1,10 @@
 package dk.aau.cs.TCTL.visitors;
 
+import java.util.List;
+
 import dk.aau.cs.TCTL.*;
 import dk.aau.cs.verification.SMCSettings;
+import dk.aau.cs.verification.observations.Observation;
 
 public class SMCQueryVisitor extends LTLQueryVisitor {
 
@@ -14,14 +17,24 @@ public class SMCQueryVisitor extends LTLQueryVisitor {
     private static final String XML_CONFIDENCE_TAG          = "confidence";
     private static final String XML_INTERVAL_WIDTH_TAG      = "interval-width";
     private static final String XML_COMPARE_TO_FLOAT_TAG    = "compare-to";
+    private static final String XML_OBSERVATIONS            = "observations";
+    private static final String XML_WATCH                   = "watch";
+    private static final String XML_WATCH_ID                = "id";
+    private static final String XML_WATCH_NAME              = "name";
 
     public String getXMLQueryFor(TCTLAbstractProperty property, String queryName, SMCSettings settings) {
         buildXMLQuery(property, queryName, settings);
         return getFormatted();
     }
 
     public void buildXMLQuery(TCTLAbstractProperty property, String queryName, SMCSettings settings) {
-        xmlQuery.append(startTag(XML_PROP) + queryInfo(queryName) + smcTag(settings) + startTag(XML_FORMULA));
+        xmlQuery.append(startTag(XML_PROP) + queryInfo(queryName) + smcTag(settings));
+
+        if (!settings.getObservations().isEmpty()) {
+            xmlQuery.append(observationTag(settings.getObservations()));
+        }
+
+        xmlQuery.append(startTag(XML_FORMULA));
         property.accept(this, null);
         xmlQuery.append(endTag(XML_FORMULA) + endTag(XML_PROP));
     }
@@ -44,6 +57,18 @@ private String smcTag(SMCSettings settings) {
         return emptyElement(tagContent);
     }
 
+    private String observationTag(List<Observation> observations) {
+        String observationXml = startTag(XML_OBSERVATIONS); 
+
+        for (Observation observation : observations) {
+            observationXml += observation.toXml();
+        }
+
+        observationXml += endTag(XML_OBSERVATIONS);
+
+        return observationXml;
+    }
+
     private String tagAttribute(String name, String value) {
         return " " + name + "=\"" + value + "\"";
     }

src/main/java/dk/aau/cs/io/LoadTACPN.java

@@ -251,7 +251,7 @@ public ArcExpression parseArcExpression(Node node) throws FormatException {
             ArcExpression childexp = parseArcExpression(child);
 
             return new ScalarProductExpression(scalarval, childexp);
-        }else if (name.equals("all")){
+        } else if (name.equals("all")){
             ColorType ct = parseUserSort(node);
             Vector<ColorExpression> ceVector = new Vector<>();
             ceVector.add(new AllExpression(ct));

src/main/java/dk/aau/cs/io/TapnEngineXmlLoader.java

@@ -277,16 +277,21 @@ private List<Constant> parseConstants(Document doc) {
 		List<Constant> constants = new ArrayList<Constant>();
 		NodeList constantNodes = doc.getElementsByTagName("constant");
 		for (int i = 0; i < constantNodes.getLength(); i++) {
-			Node c = constantNodes.item(i);
+            Node c = constantNodes.item(i);
+            if (XmlUtil.isDescendantOfTag(c, "watch")) {
+                continue;
+            }
 
 			if (c instanceof Element) {
 				Constant constant = parseConstant((Element) c);
 				constants.add(constant);
 			}
 		}
+
 		return constants;
 	}
 
+
 	private Template parseTimedArcPetriNet(Node tapnNode, TimedArcPetriNetNetwork network, ConstantStore constants) throws FormatException {
         String name = getTAPNName(tapnNode);
 

src/main/java/dk/aau/cs/io/TapnLegacyXmlLoader.java

@@ -128,6 +128,9 @@ private LoadedModel parse(Document tapnDoc) throws FormatException {
 		NodeList constantNodes = tapnDoc.getElementsByTagName("constant");
 		for (int i = 0; i < constantNodes.getLength(); i++) {
 			Node c = constantNodes.item(i);
+            if (XmlUtil.isDescendantOfTag(c, "watch")) {
+                continue;
+            }
 
 			if (c instanceof Element) {
 				parseAndAddConstant((Element) c);

src/main/java/dk/aau/cs/io/TapnXmlLoader.java

@@ -318,6 +318,9 @@ private List<Constant> parseConstants(Document doc) {
 		NodeList constantNodes = doc.getElementsByTagName("constant");
 		for (int i = 0; i < constantNodes.getLength(); i++) {
 			Node c = constantNodes.item(i);
+            if (XmlUtil.isDescendantOfTag(c, "watch")) {
+                continue;
+            }
 
 			if (c instanceof Element) {
 				Constant constant = parseConstant((Element) c);

src/main/java/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java

@@ -505,7 +505,9 @@ private Element createSMCQueryElement(TAPNQuery query, Document document) {
                 .getDocumentElement();
             Node smcTag = doc.getElementsByTagName("smc").item(0);
             Node formula = doc.getElementsByTagName("formula").item(0);
+            Node observations = doc.getElementsByTagName("observations").item(0);
             queryElement.appendChild(document.importNode(smcTag, true));
+            queryElement.appendChild(document.importNode(observations, true));
             queryElement.appendChild(document.importNode(formula, true));
         } catch (SAXException | ParserConfigurationException | IOException e) {
             System.out.println(e + " thrown in savePNML() "

src/main/java/dk/aau/cs/io/XmlUtil.java

@@ -0,0 +1,23 @@
+package dk.aau.cs.io;
+
+import org.w3c.dom.Element;
+import org.w3c.dom.Node;
+
+public class XmlUtil {
+    /**
+     * Returns true if the given node is a descendant of a node with the given tag name.
+     */
+    public static boolean isDescendantOfTag(Node node, String tagName) {
+        Node parent = node.getParentNode();
+        while (parent != null) {
+            if (parent.getNodeType() == Node.ELEMENT_NODE && 
+                ((Element)parent).getTagName().equals(tagName)) {
+                return true;
+            }
+
+            parent = parent.getParentNode();
+        }
+
+        return false;
+    }
+}

src/main/java/dk/aau/cs/io/queries/TAPNQueryLoader.java

@@ -3,11 +3,21 @@
 import java.util.ArrayList;
 import java.util.Arrays;
 import java.util.List;
+import java.util.function.BiFunction;
+
 import dk.aau.cs.TCTL.*;
 import dk.aau.cs.TCTL.XMLParsing.XMLHyperLTLQueryParser;
 import dk.aau.cs.TCTL.XMLParsing.XMLLTLQueryParser;
 import dk.aau.cs.verification.SMCSettings;
 import dk.aau.cs.verification.SMCTraceType;
+import dk.aau.cs.verification.observations.Observation;
+import dk.aau.cs.verification.observations.expressions.ObsAdd;
+import dk.aau.cs.verification.observations.expressions.ObsConstant;
+import dk.aau.cs.verification.observations.expressions.ObsExpression;
+import dk.aau.cs.verification.observations.expressions.ObsMultiply;
+import dk.aau.cs.verification.observations.expressions.ObsOperator;
+import dk.aau.cs.verification.observations.expressions.ObsPlace;
+import dk.aau.cs.verification.observations.expressions.ObsSubtract;
 
 import org.w3c.dom.Document;
 import org.w3c.dom.Element;
@@ -27,6 +37,7 @@
 import dk.aau.cs.TCTL.Parsing.TAPAALQueryParser;
 import dk.aau.cs.TCTL.XMLParsing.XMLCTLQueryParser;
 import dk.aau.cs.TCTL.XMLParsing.XMLQueryParseException;
+import dk.aau.cs.model.tapn.TimedArcPetriNet;
 import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork;
 import dk.aau.cs.model.tapn.TimedPlace;
 import dk.aau.cs.translations.ReductionOption;
@@ -113,9 +124,27 @@ private TAPNQuery parseTAPNQuery(Element queryElement, TimedArcPetriNetNetwork n
             if(smcTagList.getLength() > 0) {
                 Element settingsNode = (Element) smcTagList.item(0);
                 smcSettings = parseSmcSettings(settingsNode);
+                NodeList observationsList = queryElement.getElementsByTagName("observations");
+                if (observationsList.getLength() > 0) {
+                    Element observationsNode = (Element)observationsList.item(0);
+                    NodeList watchList = observationsNode.getElementsByTagName("watch");
+
+                    List<Observation> observations = new ArrayList<>();
+                    for (int i = 0; i < watchList.getLength(); ++i) {
+                        Element watch = (Element)watchList.item(i);
+                        String name = watch.getAttribute("name");                        
+
+                        Element root = getFirstElementChild(watch);
+                        Observation observation = new Observation(name, parseObsExpression(root));
+                        observations.add(observation);
+                    }
+
+                    smcSettings.setObservations(observations);
+                }
             } else {
                 smcSettings = SMCSettings.Default();
             }
+
             query = parseLTLQueryProperty(queryElement);
         } else if (queryElement.hasAttribute("type") && queryElement.getAttribute("type").equals("LTL")) {
             query = parseLTLQueryProperty(queryElement);
@@ -165,6 +194,78 @@ public static boolean hasSmcTag(Node queryElement) {
         return false;
     }
 
+    private Element getFirstElementChild(Element parent) {
+        NodeList children = parent.getChildNodes();
+        for (int i = 0; i < children.getLength(); i++) {
+            Node child = children.item(i);
+            if (child.getNodeType() == Node.ELEMENT_NODE) {
+                return (Element)child;
+            }
+        }
+
+        return null;
+    }
+
+    private Element getSecondElementChild(Element parent) {
+        NodeList children = parent.getChildNodes();
+        int elementCount = 0;
+        for (int i = 0; i < children.getLength(); i++) {
+            Node child = children.item(i);
+            if (child.getNodeType() == Node.ELEMENT_NODE) {
+                ++elementCount;
+                if (elementCount == 2) {
+                    return (Element)child;
+                }
+            }
+        }
+
+        return null;
+    }
+
+    private ObsExpression parseObsExpression(Element element) {
+        String tagName = element.getTagName();
+
+        switch (tagName) {
+            case "add":
+                return createOperatorExpression(element, ObsAdd::new);
+            case "subtract":
+                return createOperatorExpression(element, ObsSubtract::new);
+            case "multiply":
+                return createOperatorExpression(element, ObsMultiply::new);
+            case "constant":
+                return new ObsConstant(Integer.parseInt(element.getAttribute("value")));
+            case "place":
+                return createPlaceExpression(element);
+            default:
+                throw new IllegalArgumentException("Unknown expression type: " + tagName);
+        }
+    }
+
+    private ObsExpression createOperatorExpression(Element element, BiFunction<ObsExpression, ObsExpression, ObsOperator> constructor) {
+        ObsExpression left = parseObsExpression(getFirstElementChild(element));
+        ObsExpression right = parseObsExpression(getSecondElementChild(element));
+        ObsOperator operator = constructor.apply(left, right);
+
+        if (left.isOperator()) {
+            ((ObsOperator)left).setParent(operator);
+        }
+
+        if (right.isOperator()) {
+            ((ObsOperator)right).setParent(operator);
+        }
+
+        return operator;
+    }    
+
+    private ObsExpression createPlaceExpression(Element element) {
+        String name = element.getAttribute("name");
+        String[] parts = name.split("_");
+        String templateName = parts[0];
+        String placeName = parts[1];
+
+        return new ObsPlace(templateName, placeName, network);
+    }
+
     public static SMCSettings parseSmcSettings(Element smcTag) {
         SMCSettings settings = SMCSettings.Default();
         if(smcTag.hasAttribute("time-bound"))

src/main/java/dk/aau/cs/verification/SMCSettings.java

@@ -1,5 +1,10 @@
 package dk.aau.cs.verification;
 
+import java.util.ArrayList;
+import java.util.List;
+
+import dk.aau.cs.verification.observations.Observation;
+
 public class SMCSettings {
 
     public int timeBound;
@@ -12,6 +17,8 @@ public class SMCSettings {
     public boolean compareToFloat;
     public float geqThan;
 
+    private List<Observation> observations;
+
     public static SMCSettings Default() {
         SMCSettings settings = new SMCSettings();
         settings.timeBound = 1000;
@@ -23,6 +30,7 @@ public static SMCSettings Default() {
         settings.estimationIntervalWidth = 0.05f;
         settings.compareToFloat = false;
         settings.geqThan = 0.5f;
+        settings.setObservations(new ArrayList<>());
         return settings;
     }
 
@@ -56,4 +64,12 @@ public int getTimeBound() {
     public int getStepBound() {
         return stepBound;
     }
+
+    public void setObservations(List<Observation> observations) {
+        this.observations = observations;
+    }
+
+    public List<Observation> getObservations() {
+        return observations;
+    }
 }

src/main/java/dk/aau/cs/verification/observations/Observation.java

@@ -0,0 +1,44 @@
+package dk.aau.cs.verification.observations;
+
+import dk.aau.cs.verification.observations.expressions.ObsExpression;
+import dk.aau.cs.verification.observations.expressions.ObsPlaceHolder;
+
+public class Observation {
+    private String name;
+
+    private ObsExpression expression = new ObsPlaceHolder();
+
+    public Observation(String name) {
+        this.name = name;
+    }
+
+    public Observation(String name, ObsExpression expression) {
+        this.name = name;
+        this.expression = expression;
+    }
+
+    public String getName() {
+        return name;
+    }
+
+    public ObsExpression getExpression() {
+        return expression;
+    }
+
+    public void setName(String name) {
+        this.name = name;
+    }
+
+    public void setExpression(ObsExpression expression) {
+        this.expression = expression;
+    }
+
+    @Override
+    public String toString() {
+        return name;
+    }
+
+    public String toXml() {
+        return "<watch name=\"" + name + "\">" + expression.toXml() + "</watch>";
+    }
+}

src/main/java/dk/aau/cs/verification/observations/expressions/ObsAdd.java

@@ -0,0 +1,21 @@
+package dk.aau.cs.verification.observations.expressions;
+
+public class ObsAdd extends ObsOperator {
+    public ObsAdd(ObsExpression left, ObsExpression right) {
+        super(left, right);
+    }
+
+    public ObsAdd() {
+        super();
+    }
+
+    @Override
+    protected String getOperator() {
+        return "+";
+    }
+
+    @Override
+    public String toXml() {
+        return "<add>" + left.toXml() + right.toXml() + "</add>";
+    }
+}