SMC features for discrete verification

build.gradle

@@ -63,6 +63,7 @@ dependencies {
     implementation 'net.java.dev.jna:jna:5.11.0'
     implementation 'org.jetbrains:annotations:23.0.0'
     implementation 'org.jetbrains.kotlinx:kotlinx-serialization-json:1.3.3'
+    implementation 'org.jfree:jfreechart:1.5.5'
 
     testImplementation 'org.junit.jupiter:junit-jupiter-api:5.8.2'
     testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.8.2'

src/main/java/dk/aau/cs/TCTL/XMLParsing/XMLCTLQueryParser.java

@@ -399,9 +399,7 @@ else if(nodeName.equals("deadlock")){
             }
         } else if (nodeName.equals("control")) {
             return parseFormula(child);
-        }else{
-        	parseFormula(property);
-        }
+        } 
 
         throw new XMLQueryParseException(ERROR_MESSAGE + nodeName);
     }

src/main/java/dk/aau/cs/TCTL/XMLParsing/XMLLTLQueryParser.java

@@ -333,7 +333,9 @@ private TCTLAbstractProperty parseFormula(Node property)
                 }
                 return new TCTLOrListNode(transitions);
             }
-        } else{
+        } else if(nodeName.equals("deadlock")) {
+            return new TCTLDeadlockNode();
+        } else {
             parseFormula(property);
         }
 

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

@@ -7,43 +7,43 @@
 
 public class LTLQueryVisitor extends VisitorBase {
 
-    private static final String XML_NS 			        = "xmlns=\"http://tapaal.net/\"";
-    private static final String XML_PROPSET 		    = "property-set";
-    private static final String XML_PROP			    = "property";
-    private static final String XML_PROPID			    = "id";
-    private static final String XML_PROPDESC		    = "description";
-    private static final String XML_FORMULA		    	= "formula";
-    private static final String XML_ALLPATHS	    	= "all-paths";
-    private static final String XML_EXISTSPATH	    	= "exists-path";
-    private static final String XML_NEGATION	    	= "negation";
-    private static final String XML_CONJUNCTION 		= "conjunction";
-    private static final String XML_DISJUNCTION 		= "disjunction";
-    private static final String XML_GLOBALLY		    = "globally";
-    private static final String XML_FINALLY			    = "finally";
-    private static final String XML_NEXT			    = "next";
-    private static final String XML_UNTIL 		    	= "until";
-    private static final String XML_BEFORE 			    = "before";
-    private static final String XML_REACH 		    	= "reach";
-    private static final String XML_DEADLOCK 		    = "deadlock";
-    private static final String XML_TRUE 			    = "true";
-    private static final String XML_FALSE 			    = "false";
-    private static final String XML_INTEGERLT 		    = "integer-lt";
-    private static final String XML_INTEGERLE 		    = "integer-le";
-    private static final String XML_INTEGEREQ		    = "integer-eq";
-    private static final String XML_INTEGERNE 		    = "integer-ne";
-    private static final String XML_INTEGERGT 		    = "integer-gt";
-    private static final String XML_INTEGERGE           = "integer-ge";
-    private static final String XML_ISFIREABLE		    = "is-fireable";
-    private static final String XML_INTEGERCONSTANT 	= "integer-constant";
-    private static final String XML_TOKENSCOUNT 		= "tokens-count";
-    private static final String XML_PLACE 			    = "place";
-    private static final String XML_TRANSITION		    = "transition";
-    private static final String XML_INTEGERSUM          = "integer-sum";
-    private static final String XML_INTEGERPRODUCT      = "integer-product";
-    private static final String XML_INTEGERDIFFERENCE   = "integer-difference";
-
-
-    private final StringBuffer xmlQuery = new StringBuffer();
+    protected static final String XML_NS 			        = "xmlns=\"http://tapaal.net/\"";
+    protected static final String XML_PROPSET 		    = "property-set";
+    protected static final String XML_PROP			    = "property";
+    protected static final String XML_PROPID			    = "id";
+    protected static final String XML_PROPDESC		    = "description";
+    protected static final String XML_FORMULA		    	= "formula";
+    protected static final String XML_ALLPATHS	    	= "all-paths";
+    protected static final String XML_EXISTSPATH	    	= "exists-path";
+    protected static final String XML_NEGATION	    	= "negation";
+    protected static final String XML_CONJUNCTION 		= "conjunction";
+    protected static final String XML_DISJUNCTION 		= "disjunction";
+    protected static final String XML_GLOBALLY		    = "globally";
+    protected static final String XML_FINALLY			    = "finally";
+    protected static final String XML_NEXT			    = "next";
+    protected static final String XML_UNTIL 		    	= "until";
+    protected static final String XML_BEFORE 			    = "before";
+    protected static final String XML_REACH 		    	= "reach";
+    protected static final String XML_DEADLOCK 		    = "deadlock";
+    protected static final String XML_TRUE 			    = "true";
+    protected static final String XML_FALSE 			    = "false";
+    protected static final String XML_INTEGERLT 		    = "integer-lt";
+    protected static final String XML_INTEGERLE 		    = "integer-le";
+    protected static final String XML_INTEGEREQ		    = "integer-eq";
+    protected static final String XML_INTEGERNE 		    = "integer-ne";
+    protected static final String XML_INTEGERGT 		    = "integer-gt";
+    protected static final String XML_INTEGERGE           = "integer-ge";
+    protected static final String XML_ISFIREABLE		    = "is-fireable";
+    protected static final String XML_INTEGERCONSTANT 	= "integer-constant";
+    protected static final String XML_TOKENSCOUNT 		= "tokens-count";
+    protected static final String XML_PLACE 			    = "place";
+    protected static final String XML_TRANSITION		    = "transition";
+    protected static final String XML_INTEGERSUM          = "integer-sum";
+    protected static final String XML_INTEGERPRODUCT      = "integer-product";
+    protected static final String XML_INTEGERDIFFERENCE   = "integer-difference";
+
+
+    protected final StringBuffer xmlQuery = new StringBuffer();
 
     public LTLQueryVisitor() {
         super();
@@ -83,7 +83,7 @@ public String getEndTag(){
         return endTag(XML_PROPSET) + "\n";
     }
 
-    private String queryInfo(String queryName){
+    protected String queryInfo(String queryName){
         String nameToPrint = (queryName == null) ? "Query Comment/Name Here" : queryName;
         return wrapInTag(nameToPrint, XML_PROPID) + wrapInTag(nameToPrint, XML_PROPDESC);
     }
@@ -234,16 +234,16 @@ public void visit(TCTLAtomicPropositionNode atomicPropositionNode, Object contex
         xmlQuery.append(endTag(op));
     }
 
-    private String wrapInTag(String str, String tag){
+    protected String wrapInTag(String str, String tag){
         return startTag(tag) + str + endTag(tag);
     }
-    private String startTag(String tag){
+    protected String startTag(String tag){
         return "<" + tag + ">";
     }
-    private String endTag(String tag){
+    protected String endTag(String tag){
         return "</" + tag + ">";
     }
-    private String emptyElement(String tag){
+    protected String emptyElement(String tag){
         return startTag(tag + "/");
     }
 }

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

@@ -0,0 +1,58 @@
+package dk.aau.cs.TCTL.visitors;
+
+import dk.aau.cs.TCTL.*;
+import dk.aau.cs.verification.SMCSettings;
+
+public class SMCQueryVisitor extends LTLQueryVisitor {
+
+    private static final String XML_SMC		    	        = "smc";
+    private static final String XML_TIME_BOUND_TAG          = "time-bound";
+    private static final String XML_STEP_BOUND_TAG          = "step-bound";
+    private static final String XML_FALSE_POS_TAG           = "false-positives";
+    private static final String XML_FALSE_NEG_TAG           = "false-negatives";
+    private static final String XML_INDIFFERENCE_TAG        = "indifference";
+    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";
+
+    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));
+        property.accept(this, null);
+        xmlQuery.append(endTag(XML_FORMULA) + endTag(XML_PROP));
+    }
+
+    private String smcTag(SMCSettings settings) {
+        String tagContent = XML_SMC;
+        if(settings.timeBound < Integer.MAX_VALUE)
+            tagContent += tagAttribute(XML_TIME_BOUND_TAG, settings.timeBound);
+        if(settings.stepBound < Integer.MAX_VALUE)
+            tagContent += tagAttribute(XML_STEP_BOUND_TAG, settings.stepBound);
+        if(settings.compareToFloat) {
+            tagContent += tagAttribute(XML_FALSE_POS_TAG, settings.falsePositives);
+            tagContent += tagAttribute(XML_FALSE_NEG_TAG, settings.falseNegatives);
+            tagContent += tagAttribute(XML_INDIFFERENCE_TAG, settings.indifferenceWidth);
+            tagContent += tagAttribute(XML_COMPARE_TO_FLOAT_TAG, settings.geqThan);
+        } else {
+            tagContent += tagAttribute(XML_CONFIDENCE_TAG, settings.confidence);
+            tagContent += tagAttribute(XML_INTERVAL_WIDTH_TAG, settings.estimationIntervalWidth);
+        }
+        return emptyElement(tagContent);
+    }
+
+    private String tagAttribute(String name, String value) {
+        return " " + name + "=\"" + value + "\"";
+    }
+
+    private String tagAttribute(String name, float value) {
+        return " " + name + "=\"" + String.valueOf(value) + "\"";
+    }
+
+    private String tagAttribute(String name, int value) {
+        return " " + name + "=\"" + String.valueOf(value) + "\"";
+    }
+}

src/main/java/dk/aau/cs/approximation/ApproximationWorker.java

@@ -456,7 +456,7 @@ else if (k instanceof TimedTransitionStep) {
 		} else {
             NameMapping nameMapping = isColored? result.getUnfoldedModel().value2(): transformedModel.value2();
             TimedArcPetriNetNetwork netNetwork = isColored? result.getUnfoldedModel().value1().parentNetwork(): model;
-            if (dataLayerQuery != null && dataLayerQuery.getCategory() == net.tapaal.gui.petrinet.verification.TAPNQuery.QueryCategory.HyperLTL) {
+            if (dataLayerQuery != null && dataLayerQuery.getCategory() == net.tapaal.gui.petrinet.verification.TAPNQuery.QueryCategory.HyperLTL || dataLayerQuery.getCategory() == net.tapaal.gui.petrinet.verification.TAPNQuery.QueryCategory.SMC) {
                 toReturn =  new VerificationResult<>(
                     result.getQueryResult(),
                     decomposeTrace(result.getTraceMap(), nameMapping, netNetwork),
@@ -486,7 +486,7 @@ else if (k instanceof TimedTransitionStep) {
 
 		options.setTraceOption(oldTraceOption);
 		// if the old traceoption was none, we need to set the results traces to null so GUI doesn't try to display the traces later
-		if (oldTraceOption == TraceOption.NONE && toReturn != null){
+		if (oldTraceOption == TraceOption.NONE && toReturn != null && dataLayerQuery.getCategory() != net.tapaal.gui.petrinet.verification.TAPNQuery.QueryCategory.SMC) {
 			toReturn.setTrace(null);
 			toReturn.setSecondaryTrace(null);
 		}
@@ -527,8 +527,9 @@ public VerificationResult<TimedArcPetriNetTrace> batchWorker(
         boolean modelIsColored = composedModel.value1().isColored();
         boolean modelIsTimed = !composedModel.value1().isUntimed();
         boolean modelIsGame = composedModel.value1().hasUncontrollableTransitions();
+        boolean modelIsStochastic = composedModel.value1().isStochastic();
 
-        TAPNLens lens = new TAPNLens(modelIsTimed, modelIsGame, modelIsColored);
+        TAPNLens lens = new TAPNLens(modelIsTimed, modelIsGame, modelIsColored, modelIsStochastic);
 
 		VerificationResult<TimedArcPetriNetTrace> verificationResult = modelChecker.verify(options, composedModel, queryToVerify, null, query, lens);
 

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

@@ -35,9 +35,10 @@ public TAPNLens getLens(){
         } else {
             boolean isNetTimed = !network().isUntimed();
             boolean isNetGame = network().hasUncontrollableTransitions();
-            boolean isNetColored = network.isColored();
+            boolean isNetColored = network().isColored();
+            boolean isNetStochastic = network().isStochastic();
 
-            return new TAPNLens(isNetTimed, isNetGame, isNetColored);
+            return new TAPNLens(isNetTimed, isNetGame, isNetColored, isNetStochastic);
         }
     }
     public boolean isColored(){

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

@@ -247,6 +247,7 @@ private Element createTransitionElement(TimedTransitionComponent inputTransition
 
 		Element transitionElement = document.createElement("transition");
 		transitionElement.setAttribute("id", (inputTransition.getId() != null ? inputTransition.getId()	: "error"));
+        inputTransition.underlyingTransition().getDistribution().writeToXml(transitionElement);
 
 		Element name = document.createElement("name"); //Name
 		transitionElement.appendChild(name);
@@ -276,6 +277,7 @@ private Element createColoredTransitionElement (TimedTransitionComponent inputTr
 
         Element transitionElement = document.createElement("transition");
         transitionElement.setAttribute("id", (inputTransition.getId() != null ? inputTransition.getId()	: "error"));
+        inputTransition.underlyingTransition().getDistribution().writeToXml(transitionElement);
 
         Element name = document.createElement("name"); //Name
         transitionElement.appendChild(name);

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

@@ -116,7 +116,7 @@ private LoadedModel parse(Document doc) throws FormatException {
         Node pnmlElement = doc.getElementsByTagName("pnml").item(0);
         Node netNode = getFirstDirectChild(pnmlElement, "net");
 
-        lens = new TAPNLens(false, false, getFirstDirectChild(netNode, "declaration") != null);
+        lens = new TAPNLens(false, false, getFirstDirectChild(netNode, "declaration") != null, false);
 
         String name = getTAPNName(netNode);