diff --git a/build.gradle b/build.gradle index e52a0f599..60c552d3c 100644 --- a/build.gradle +++ b/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' diff --git a/src/main/java/dk/aau/cs/TCTL/XMLParsing/XMLCTLQueryParser.java b/src/main/java/dk/aau/cs/TCTL/XMLParsing/XMLCTLQueryParser.java index f92faeeb5..bbf037797 100644 --- a/src/main/java/dk/aau/cs/TCTL/XMLParsing/XMLCTLQueryParser.java +++ b/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); } diff --git a/src/main/java/dk/aau/cs/TCTL/XMLParsing/XMLLTLQueryParser.java b/src/main/java/dk/aau/cs/TCTL/XMLParsing/XMLLTLQueryParser.java index 0c69b2162..2421f61d6 100644 --- a/src/main/java/dk/aau/cs/TCTL/XMLParsing/XMLLTLQueryParser.java +++ b/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); } diff --git a/src/main/java/dk/aau/cs/TCTL/visitors/LTLQueryVisitor.java b/src/main/java/dk/aau/cs/TCTL/visitors/LTLQueryVisitor.java index 3bcb9b75c..04e7d3c33 100644 --- a/src/main/java/dk/aau/cs/TCTL/visitors/LTLQueryVisitor.java +++ b/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 ""; } - private String emptyElement(String tag){ + protected String emptyElement(String tag){ return startTag(tag + "/"); } } diff --git a/src/main/java/dk/aau/cs/TCTL/visitors/SMCQueryVisitor.java b/src/main/java/dk/aau/cs/TCTL/visitors/SMCQueryVisitor.java new file mode 100644 index 000000000..7d9d406a5 --- /dev/null +++ b/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) + "\""; + } +} diff --git a/src/main/java/dk/aau/cs/approximation/ApproximationWorker.java b/src/main/java/dk/aau/cs/approximation/ApproximationWorker.java index 3d7e61805..1d2ac37ea 100644 --- a/src/main/java/dk/aau/cs/approximation/ApproximationWorker.java +++ b/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 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 verificationResult = modelChecker.verify(options, composedModel, queryToVerify, null, query, lens); diff --git a/src/main/java/dk/aau/cs/io/LoadedModel.java b/src/main/java/dk/aau/cs/io/LoadedModel.java index dd07ce3a7..21a44ea25 100644 --- a/src/main/java/dk/aau/cs/io/LoadedModel.java +++ b/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(){ diff --git a/src/main/java/dk/aau/cs/io/PNMLWriter.java b/src/main/java/dk/aau/cs/io/PNMLWriter.java index 414f4d970..11e0e9d94 100644 --- a/src/main/java/dk/aau/cs/io/PNMLWriter.java +++ b/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); diff --git a/src/main/java/dk/aau/cs/io/PNMLoader.java b/src/main/java/dk/aau/cs/io/PNMLoader.java index d9d109a89..50196874a 100644 --- a/src/main/java/dk/aau/cs/io/PNMLoader.java +++ b/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); diff --git a/src/main/java/dk/aau/cs/io/TapnEngineXmlLoader.java b/src/main/java/dk/aau/cs/io/TapnEngineXmlLoader.java index 46b8eb2da..2480b4e1a 100644 --- a/src/main/java/dk/aau/cs/io/TapnEngineXmlLoader.java +++ b/src/main/java/dk/aau/cs/io/TapnEngineXmlLoader.java @@ -6,6 +6,10 @@ import dk.aau.cs.model.CPN.*; import dk.aau.cs.model.CPN.Expressions.*; import dk.aau.cs.model.tapn.*; +import dk.aau.cs.model.tapn.simulation.FiringMode; +import dk.aau.cs.model.tapn.simulation.OldestFiringMode; +import dk.aau.cs.model.tapn.simulation.RandomFiringMode; +import dk.aau.cs.model.tapn.simulation.YoungestFiringMode; import dk.aau.cs.util.FormatException; import dk.aau.cs.util.Require; import kotlin.Pair; @@ -104,7 +108,7 @@ private LoadedModel parse(Document doc) throws FormatException { network.add(ColorType.COLORTYPE_DOT); } parseSharedPlaces(doc, network, constants); - parseSharedTransitions(doc, network); + parseSharedTransitions(doc, network, constants); Collection