diff --git a/src/main/java/dk/aau/cs/TCTL/visitors/SMCQueryVisitor.java b/src/main/java/dk/aau/cs/TCTL/visitors/SMCQueryVisitor.java index 7d9d406a5..12447cad2 100644 --- a/src/main/java/dk/aau/cs/TCTL/visitors/SMCQueryVisitor.java +++ b/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,6 +17,10 @@ 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); @@ -21,7 +28,13 @@ public String getXMLQueryFor(TCTLAbstractProperty property, String queryName, SM } 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 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 + "\""; } diff --git a/src/main/java/dk/aau/cs/io/LoadTACPN.java b/src/main/java/dk/aau/cs/io/LoadTACPN.java index 11c9b3e83..f69c4bcbf 100644 --- a/src/main/java/dk/aau/cs/io/LoadTACPN.java +++ b/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 ceVector = new Vector<>(); ceVector.add(new AllExpression(ct)); diff --git a/src/main/java/dk/aau/cs/io/TapnEngineXmlLoader.java b/src/main/java/dk/aau/cs/io/TapnEngineXmlLoader.java index f82129bf9..d02d973da 100644 --- a/src/main/java/dk/aau/cs/io/TapnEngineXmlLoader.java +++ b/src/main/java/dk/aau/cs/io/TapnEngineXmlLoader.java @@ -277,16 +277,21 @@ private List parseConstants(Document doc) { List constants = new ArrayList(); 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); diff --git a/src/main/java/dk/aau/cs/io/TapnLegacyXmlLoader.java b/src/main/java/dk/aau/cs/io/TapnLegacyXmlLoader.java index 0bc8472dd..816c01dbd 100644 --- a/src/main/java/dk/aau/cs/io/TapnLegacyXmlLoader.java +++ b/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); diff --git a/src/main/java/dk/aau/cs/io/TapnXmlLoader.java b/src/main/java/dk/aau/cs/io/TapnXmlLoader.java index b1ee3f143..31574fe8d 100644 --- a/src/main/java/dk/aau/cs/io/TapnXmlLoader.java +++ b/src/main/java/dk/aau/cs/io/TapnXmlLoader.java @@ -318,6 +318,9 @@ private List 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); diff --git a/src/main/java/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java b/src/main/java/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java index cf8affc78..263a9ef24 100644 --- a/src/main/java/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java +++ b/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() " diff --git a/src/main/java/dk/aau/cs/io/XmlUtil.java b/src/main/java/dk/aau/cs/io/XmlUtil.java new file mode 100644 index 000000000..5c687e57e --- /dev/null +++ b/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; + } +} diff --git a/src/main/java/dk/aau/cs/io/queries/TAPNQueryLoader.java b/src/main/java/dk/aau/cs/io/queries/TAPNQueryLoader.java index 855a1ec5e..fc9bf54fe 100644 --- a/src/main/java/dk/aau/cs/io/queries/TAPNQueryLoader.java +++ b/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 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 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")) diff --git a/src/main/java/dk/aau/cs/verification/SMCSettings.java b/src/main/java/dk/aau/cs/verification/SMCSettings.java index d64910c27..f40063d16 100644 --- a/src/main/java/dk/aau/cs/verification/SMCSettings.java +++ b/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 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 observations) { + this.observations = observations; + } + + public List getObservations() { + return observations; + } } diff --git a/src/main/java/dk/aau/cs/verification/observations/Observation.java b/src/main/java/dk/aau/cs/verification/observations/Observation.java new file mode 100644 index 000000000..35c64395b --- /dev/null +++ b/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 "" + expression.toXml() + ""; + } +} diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsAdd.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsAdd.java new file mode 100644 index 000000000..d0d9eea3e --- /dev/null +++ b/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 "" + left.toXml() + right.toXml() + ""; + } +} diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsConstant.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsConstant.java new file mode 100644 index 000000000..df962a917 --- /dev/null +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsConstant.java @@ -0,0 +1,24 @@ +package dk.aau.cs.verification.observations.expressions; + +public class ObsConstant extends ObsLeaf { + private final int value; + + public ObsConstant(int value) { + this.value = value; + } + + @Override + public String toString() { + return Integer.toString(value); + } + + @Override + public String toXml() { + return ""; + } + + @Override + public ObsExpression deepCopy() { + return new ObsConstant(value); + } +} diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsExprPosition.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsExprPosition.java new file mode 100644 index 000000000..8d2fdc404 --- /dev/null +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsExprPosition.java @@ -0,0 +1,29 @@ +package dk.aau.cs.verification.observations.expressions; + +public class ObsExprPosition { + private final int start; + private final int end; + private final ObsExpression object; + + public ObsExprPosition(int start, int end, ObsExpression object) { + this.start = start; + this.end = end; + this.object = object; + } + + public int getStart() { + return start; + } + + public int getEnd() { + return end; + } + + public ObsExpression getObject() { + return object; + } + + public ObsExprPosition addOffset(int offset) { + return new ObsExprPosition(start + offset, end + offset, object); + } +} \ No newline at end of file diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsExpression.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsExpression.java new file mode 100644 index 000000000..8233cf73c --- /dev/null +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsExpression.java @@ -0,0 +1,10 @@ +package dk.aau.cs.verification.observations.expressions; + +public interface ObsExpression { + ObsExpression deepCopy(); + ObsExprPosition getObjectPosition(int index); + boolean isOperator(); + boolean isLeaf(); + boolean isPlaceHolder(); + String toXml(); +} diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsLeaf.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsLeaf.java new file mode 100644 index 000000000..38bb2250b --- /dev/null +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsLeaf.java @@ -0,0 +1,23 @@ +package dk.aau.cs.verification.observations.expressions; + +public abstract class ObsLeaf implements ObsExpression { + @Override + public ObsExprPosition getObjectPosition(int index) { + return new ObsExprPosition(0, toString().length(), this); + } + + @Override + public boolean isOperator() { + return false; + } + + @Override + public boolean isLeaf() { + return true; + } + + @Override + public boolean isPlaceHolder() { + return false; + } +} diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsMultiply.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsMultiply.java new file mode 100644 index 000000000..d186e9995 --- /dev/null +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsMultiply.java @@ -0,0 +1,21 @@ +package dk.aau.cs.verification.observations.expressions; + +public class ObsMultiply extends ObsOperator { + public ObsMultiply(ObsExpression left, ObsExpression right) { + super(left, right); + } + + public ObsMultiply() { + super(); + } + + @Override + protected String getOperator() { + return "*"; + } + + @Override + public String toXml() { + return "" + left.toXml() + right.toXml() + ""; + } +} diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsOperator.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsOperator.java new file mode 100644 index 000000000..51ee8d30f --- /dev/null +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsOperator.java @@ -0,0 +1,132 @@ +package dk.aau.cs.verification.observations.expressions; + +public abstract class ObsOperator implements ObsExpression { + protected ObsExpression left; + protected ObsExpression right; + private ObsExpression parent; + private boolean hadParentheses = false; + + protected ObsOperator(ObsExpression left, ObsExpression right) { + this.left = left; + this.right = right; + } + + protected ObsOperator() { + this(new ObsPlaceHolder(), new ObsPlaceHolder()); + } + + public void insertLeftMost(ObsExpression expr) { + if (expr.isOperator()) { + ((ObsOperator)expr).parent = this; + } + + if (left.isOperator()) { + ((ObsOperator)left).insertLeftMost(expr); + } else { + left = expr; + } + } + + public void setLeft(ObsExpression left) { + this.left = left; + } + + public void setRight(ObsExpression right) { + this.right = right; + } + + public void replace(ObsExpression selectedExpr, ObsExpression newExpr) { + if (left.equals(selectedExpr) || right.equals(selectedExpr)) { + if (newExpr.isOperator()) { + ((ObsOperator)newExpr).parent = this; + if (selectedExpr.isOperator()) { + ((ObsOperator)newExpr).left = ((ObsOperator)selectedExpr).left; + ((ObsOperator)newExpr).right = ((ObsOperator)selectedExpr).right; + } + } + + if (left.equals(selectedExpr)) { + left = newExpr; + } else if (right.equals(selectedExpr)) { + right = newExpr; + } + } + + if (left.isOperator()) { + ((ObsOperator)left).replace(selectedExpr, newExpr); + } + + if (right.isOperator()) { + ((ObsOperator)right).replace(selectedExpr, newExpr); + } + } + + @Override + public ObsExpression deepCopy() { + try { + ObsOperator copy = getClass() + .getConstructor(ObsExpression.class, ObsExpression.class) + .newInstance(left.deepCopy(), right.deepCopy()); + copy.setParent(this.parent); + return copy; + } catch (Exception e) { + throw new RuntimeException("Failed to copy ObsOperator", e); + } + } + + public void setParent(ObsExpression parent) { + this.parent = parent; + } + + public void hadParentheses(boolean hadParentheses) { + this.hadParentheses = hadParentheses; + } + + private boolean addParenthesis() { + return (parent != null && parent.getClass() != getClass()) || hadParentheses; + } + + @Override + public ObsExprPosition getObjectPosition(int index) { + int leftLen = left.toString().length(); + int rightLen = right.toString().length(); + int totalLen = toString().length(); + int thisLen = totalLen - leftLen - rightLen; + + int parenOffset = addParenthesis() ? 1 : 0; + if (index < leftLen + parenOffset) { + return left.getObjectPosition(index - parenOffset).addOffset(parenOffset); + } else if (index >= leftLen + thisLen - parenOffset) { + return right.getObjectPosition(index - leftLen - thisLen).addOffset(leftLen + thisLen - parenOffset); + } + + return new ObsExprPosition(0, totalLen, this); + } + + @Override + public boolean isOperator() { + return true; + } + + @Override + public boolean isLeaf() { + return false; + } + + @Override + public boolean isPlaceHolder() { + return false; + } + + @Override + public String toString() { + String operator = getOperator(); + if (addParenthesis()) { + return "(" + left + " " + operator + " " + right + ")"; + } + + return left + " " + operator + " " + right; + } + + protected abstract String getOperator(); +} \ No newline at end of file diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlace.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlace.java new file mode 100644 index 000000000..c025b8bdf --- /dev/null +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlace.java @@ -0,0 +1,41 @@ +package dk.aau.cs.verification.observations.expressions; + +import dk.aau.cs.model.tapn.TimedArcPetriNet; +import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork; +import dk.aau.cs.model.tapn.TimedPlace; + +public class ObsPlace extends ObsLeaf { + private final Object template; + private final TimedPlace place; + + public ObsPlace(Object template, TimedPlace place) { + this.template = template; + this.place = place; + } + + public ObsPlace(String templateName, String placeName, TimedArcPetriNetNetwork network) { + if (templateName.equals("Shared")) { + template = templateName; + place = network.getSharedPlaceByName(placeName); + } else { + TimedArcPetriNet net = network.getTAPNByName(templateName); + template = net; + place = net.getPlaceByName(placeName); + } + } + + @Override + public String toString() { + return template + "." + place.name(); + } + + @Override + public String toXml() { + return ""; + } + + @Override + public ObsExpression deepCopy() { + return new ObsPlace(template, place); + } +} diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlaceHolder.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlaceHolder.java new file mode 100644 index 000000000..53e02a2f8 --- /dev/null +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsPlaceHolder.java @@ -0,0 +1,23 @@ +package dk.aau.cs.verification.observations.expressions; + +public class ObsPlaceHolder extends ObsLeaf { + @Override + public String toString() { + return "<*>"; + } + + @Override + public String toXml() { + throw new UnsupportedOperationException("Cannot convert a placeholder to XML"); + } + + @Override + public ObsExpression deepCopy() { + return new ObsPlaceHolder(); + } + + @Override + public boolean isPlaceHolder() { + return true; + } +} \ No newline at end of file diff --git a/src/main/java/dk/aau/cs/verification/observations/expressions/ObsSubtract.java b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsSubtract.java new file mode 100644 index 000000000..efa4cf0f5 --- /dev/null +++ b/src/main/java/dk/aau/cs/verification/observations/expressions/ObsSubtract.java @@ -0,0 +1,21 @@ +package dk.aau.cs.verification.observations.expressions; + +public class ObsSubtract extends ObsOperator { + public ObsSubtract(ObsExpression left, ObsExpression right) { + super(left, right); + } + + public ObsSubtract() { + super(); + } + + @Override + protected String getOperator() { + return "-"; + } + + @Override + public String toXml() { + return "" + left.toXml() + right.toXml() + ""; + } +} diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/ObservationDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/ObservationDialog.java new file mode 100644 index 000000000..b12472126 --- /dev/null +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/ObservationDialog.java @@ -0,0 +1,494 @@ +package net.tapaal.gui.petrinet.dialog; + +import javax.swing.BorderFactory; +import javax.swing.DefaultListModel; +import javax.swing.JButton; +import javax.swing.JComboBox; +import javax.swing.JLabel; +import javax.swing.JOptionPane; +import javax.swing.JPanel; +import javax.swing.JScrollPane; +import javax.swing.JTextField; +import javax.swing.JTextPane; +import javax.swing.ScrollPaneConstants; +import javax.swing.text.MutableAttributeSet; +import javax.swing.text.SimpleAttributeSet; +import javax.swing.text.StyleConstants; +import javax.swing.text.StyledDocument; +import javax.swing.undo.AbstractUndoableEdit; +import javax.swing.undo.UndoManager; + +import dk.aau.cs.model.SMC.TokenMgrError; +import dk.aau.cs.model.SMC.ParseException; +import dk.aau.cs.model.SMC.ObservationParser; +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.verification.observations.Observation; +import dk.aau.cs.verification.observations.expressions.ObsExprPosition; +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.ObsPlaceHolder; +import dk.aau.cs.verification.observations.expressions.ObsSubtract; +import net.tapaal.helpers.Enabler; +import net.tapaal.swinghelpers.CustomJSpinner; +import pipe.gui.TAPAALGUI; +import pipe.gui.swingcomponents.EscapableDialog; +import java.awt.GridBagLayout; +import java.awt.Insets; +import java.awt.event.MouseAdapter; +import java.awt.event.MouseEvent; +import java.awt.Dimension; +import java.awt.GridBagConstraints; + +public class ObservationDialog extends EscapableDialog { + private static final String SHARED = "Shared"; + + private final DefaultListModel observationModel; + private final Observation observation; + + private final TimedArcPetriNetNetwork tapnNetwork; + private final JTextPane expressionField = new JTextPane(); + private final UndoManager undoManager = new UndoManager(); + + private JPanel placesPanel; + private JPanel constantsPanel; + private JPanel operationsPanel; + private JButton saveButton; + private JButton undoButton; + private JButton redoButton; + private JButton resetExpression; + private JButton editExpression; + + private ObsExpression currentExpr; + private ObsExpression selectedExpr; + + private boolean isNewObservation; + private boolean isEditing; + + public ObservationDialog(TimedArcPetriNetNetwork tapnNetwork, DefaultListModel observationModel, Observation observation) { + super(TAPAALGUI.getApp(), observation.getName(), true); + this.tapnNetwork = tapnNetwork; + this.observationModel = observationModel; + this.observation = observation; + this.currentExpr = observation.getExpression(); + + init(); + } + + public ObservationDialog(TimedArcPetriNetNetwork tapnNetwork, DefaultListModel observationModel) { + this(tapnNetwork, observationModel, new Observation("New Observation")); + isNewObservation = true; + } + + private void init() { + setSize(1200, 425); + setResizable(false); + + setLayout(new GridBagLayout()); + GridBagConstraints gbc = new GridBagConstraints(); + gbc.gridx = 0; + gbc.gridy = 0; + gbc.insets = new Insets(10, 10, 10, 10); + gbc.anchor = GridBagConstraints.WEST; + + JPanel namePanel = new JPanel(); + namePanel.setLayout(new GridBagLayout()); + + JLabel nameLabel = new JLabel("Observation name:"); + JTextField nameField = new JTextField(observation.getName(), 25); + + GridBagConstraints nameGbc = new GridBagConstraints(); + nameGbc.gridx = 0; + nameGbc.gridy = 0; + nameGbc.anchor = GridBagConstraints.WEST; + nameGbc.insets = new Insets(0, 0, 0, 5); + namePanel.add(nameLabel, nameGbc); + + ++nameGbc.gridx; + nameGbc.insets = new Insets(0, 0, 0, 0); + namePanel.add(nameField, nameGbc); + + add(namePanel, gbc); + + StyledDocument doc = expressionField.getStyledDocument(); + MutableAttributeSet standard = new SimpleAttributeSet(); + StyleConstants.setAlignment(standard, StyleConstants.ALIGN_CENTER); + StyleConstants.setFontSize(standard, 14); + doc.setParagraphAttributes(0, 0, standard, true); + expressionField.setText(currentExpr.toString()); + expressionField.setEditable(false); + + expressionField.addMouseListener(new MouseAdapter() { + @Override + public void mouseClicked(MouseEvent e) { + if (isEditing) return; + + int pos = expressionField.viewToModel2D(e.getPoint()); + ObsExprPosition exprPos = currentExpr.getObjectPosition(pos - 1); + expressionField.select(exprPos.getStart(), exprPos.getEnd()); + selectedExpr = exprPos.getObject(); + + Enabler.setAllEnabled(placesPanel, selectedExpr.isLeaf()); + Enabler.setAllEnabled(constantsPanel, selectedExpr.isLeaf()); + } + }); + + JScrollPane expressionScrollPane = new JScrollPane(expressionField); + expressionScrollPane.setVerticalScrollBarPolicy(ScrollPaneConstants.VERTICAL_SCROLLBAR_AS_NEEDED); + Dimension d = new Dimension(900, 80); + expressionScrollPane.setPreferredSize(d); + expressionScrollPane.setMinimumSize(d); + + operationsPanel = new JPanel(); + operationsPanel.setLayout(new GridBagLayout()); + operationsPanel.setBorder(BorderFactory.createTitledBorder("Operations")); + JButton plusButton = new JButton("+"); + JButton minusButton = new JButton("-"); + JButton multiplyButton = new JButton("*"); + JButton divideButton = new JButton("/"); + divideButton.setVisible(false); // Division is not supported yet + + plusButton.addActionListener(e -> updateExpression(new ObsAdd())); + minusButton.addActionListener(e -> updateExpression(new ObsSubtract())); + multiplyButton.addActionListener(e -> updateExpression(new ObsMultiply())); + + GridBagConstraints operationsGbc = new GridBagConstraints(); + operationsGbc.gridx = 0; + operationsGbc.gridy = 0; + operationsGbc.weightx = 1; + operationsGbc.fill = GridBagConstraints.HORIZONTAL; + operationsGbc.insets = new Insets(0, 10, 0, 10); + operationsPanel.add(plusButton, operationsGbc); + ++operationsGbc.gridy; + operationsGbc.insets = new Insets(5, 10, 0, 10); + operationsPanel.add(minusButton, operationsGbc); + ++operationsGbc.gridy; + operationsPanel.add(multiplyButton, operationsGbc); + ++operationsGbc.gridy; + operationsPanel.add(divideButton, operationsGbc); + + placesPanel = new JPanel(); + placesPanel.setLayout(new GridBagLayout()); + placesPanel.setBorder(BorderFactory.createTitledBorder("Places")); + + JComboBox templateComboBox = new JComboBox<>(); + tapnNetwork.activeTemplates().forEach(templateComboBox::addItem); + if (tapnNetwork.sharedPlaces().size() > 0) { + templateComboBox.addItem(SHARED); + } + + JComboBox placeComboBox = new JComboBox<>(); + templateComboBox.addActionListener(e -> { + placeComboBox.removeAllItems(); + if (templateComboBox.getSelectedItem().equals(SHARED)) { + tapnNetwork.sharedPlaces().forEach(place -> placeComboBox.addItem(place)); + } else { + TimedArcPetriNet template = (TimedArcPetriNet) templateComboBox.getSelectedItem(); + template.places().forEach(place -> placeComboBox.addItem(place)); + } + }); + + // Initialize the placeComboBox with the first template + if (templateComboBox.getItemCount() > 0) { + templateComboBox.setSelectedIndex(0); + } + + JButton addPlaceButton = new JButton("Add place"); + addPlaceButton.addActionListener(e -> { + Object template = templateComboBox.getSelectedItem(); + TimedPlace place = (TimedPlace)placeComboBox.getSelectedItem(); + ObsExpression placeExpr = new ObsPlace(template, place); + updateExpression(placeExpr); + Enabler.setAllEnabled(placesPanel, false); + Enabler.setAllEnabled(constantsPanel, false); + }); + + GridBagConstraints placesGbc = new GridBagConstraints(); + placesGbc.gridx = 0; + placesGbc.gridy = 0; + placesGbc.weightx = 1; + placesGbc.fill = GridBagConstraints.HORIZONTAL; + placesGbc.insets = new Insets(0, 10, 0, 10); + placesPanel.add(templateComboBox, placesGbc); + ++placesGbc.gridy; + placesGbc.insets = new Insets(5, 10, 0, 10); + placesPanel.add(placeComboBox, placesGbc); + ++placesGbc.gridy; + placesPanel.add(addPlaceButton, placesGbc); + + Enabler.setAllEnabled(placesPanel, false); + + constantsPanel = new JPanel(); + constantsPanel.setLayout(new GridBagLayout()); + constantsPanel.setBorder(BorderFactory.createTitledBorder("Constants")); + + CustomJSpinner constantSpinner = new CustomJSpinner(1, 1, Integer.MAX_VALUE); + JButton addConstantButton = new JButton("Add constant"); + addConstantButton.addActionListener(e -> { + int value = (int)constantSpinner.getValue(); + ObsExpression constantExpr = new ObsConstant(value); + updateExpression(constantExpr); + Enabler.setAllEnabled(placesPanel, false); + Enabler.setAllEnabled(constantsPanel, false); + }); + + GridBagConstraints constantsGbc = new GridBagConstraints(); + constantsGbc.gridx = 0; + constantsGbc.gridy = 0; + constantsGbc.weightx = 1; + constantsGbc.fill = GridBagConstraints.HORIZONTAL; + constantsGbc.insets = new Insets(0, 10, 0, 10); + constantsPanel.add(constantSpinner, constantsGbc); + ++constantsGbc.gridy; + constantsGbc.insets = new Insets(5, 10, 0, 10); + constantsPanel.add(addConstantButton, constantsGbc); + + Enabler.setAllEnabled(constantsPanel, false); + + JPanel editingPanel = new JPanel(); + editingPanel.setLayout(new GridBagLayout()); + editingPanel.setBorder(BorderFactory.createTitledBorder("Editing")); + + undoButton = new JButton("Undo"); + redoButton = new JButton("Redo"); + undoButton.setEnabled(false); + redoButton.setEnabled(false); + + undoButton.addActionListener(e -> { + if (undoManager.canUndo()) { + undoManager.undo(); + } + }); + + redoButton.addActionListener(e -> { + if (undoManager.canRedo()) { + undoManager.redo(); + } + }); + + JButton deleteSelection = new JButton("Delete Selection"); + deleteSelection.setEnabled(false); + resetExpression = new JButton("Reset Expression"); + + resetExpression.addActionListener(e -> { + if (isEditing) { + try { + System.out.println("Parsing expression: " + expressionField.getText()); + ObsExpression parsedExpr = ObservationParser.parse(expressionField.getText(), tapnNetwork); + toggleManualEditing(); + currentExpr = parsedExpr; + expressionField.setText(currentExpr.toString()); + undoManager.addEdit(new ExpressionEdit(new ObsPlaceHolder(), currentExpr.deepCopy())); + refreshUndoRedoButtons(); + saveButton.setEnabled(!includesPlaceHolder()); + } catch (ParseException | TokenMgrError ex) { + JOptionPane.showMessageDialog(TAPAALGUI.getApp(), ex.getMessage(), "Error during parsing", JOptionPane.ERROR_MESSAGE); + } + } else { + ObsExpression oldExpr = currentExpr.deepCopy(); + currentExpr = new ObsPlaceHolder(); + expressionField.setText(currentExpr.toString()); + + if (!oldExpr.isPlaceHolder()) { + undoManager.addEdit(new ExpressionEdit(oldExpr, currentExpr.deepCopy())); + refreshUndoRedoButtons(); + } + } + }); + + editExpression = new JButton("Edit Expression"); + editExpression.addActionListener(e -> toggleManualEditing()); + + GridBagConstraints editingGbc = new GridBagConstraints(); + editingGbc.gridx = 0; + editingGbc.gridy = 0; + editingGbc.weightx = 1; + editingGbc.fill = GridBagConstraints.HORIZONTAL; + editingGbc.insets = new Insets(0, 10, 0, 5); + editingPanel.add(undoButton, editingGbc); + ++editingGbc.gridx; + editingGbc.insets = new Insets(0, 0, 0, 10); + editingPanel.add(redoButton, editingGbc); + editingGbc.gridx = 0; + ++editingGbc.gridy; + editingGbc.gridwidth = 2; + editingGbc.insets = new Insets(5, 10, 0, 10); + editingPanel.add(deleteSelection, editingGbc); + ++editingGbc.gridy; + editingPanel.add(resetExpression, editingGbc); + ++editingGbc.gridy; + editingPanel.add(editExpression, editingGbc); + + JPanel expressionPanel = new JPanel(); + expressionPanel.setLayout(new GridBagLayout()); + expressionPanel.setBorder(BorderFactory.createTitledBorder("Observation Expression")); + + GridBagConstraints expressionGbc = new GridBagConstraints(); + expressionGbc.gridx = 0; + expressionGbc.gridy = 0; + expressionGbc.weightx = 1; + expressionGbc.weighty = 1; + expressionGbc.fill = GridBagConstraints.BOTH; + expressionGbc.insets = new Insets(0, 30, 0, 30); + expressionGbc.gridwidth = 4; + expressionPanel.add(expressionScrollPane, expressionGbc); + expressionGbc.gridwidth = 1; + ++expressionGbc.gridy; + expressionGbc.insets = new Insets(0, 30, 0, 0); + expressionPanel.add(operationsPanel, expressionGbc); + ++expressionGbc.gridx; + expressionGbc.insets = new Insets(0, 0, 0, 0); + expressionPanel.add(placesPanel, expressionGbc); + ++expressionGbc.gridx; + expressionPanel.add(constantsPanel, expressionGbc); + ++expressionGbc.gridx; + expressionGbc.insets = new Insets(0, 0, 0, 30); + expressionPanel.add(editingPanel, expressionGbc); + + ++gbc.gridy; + gbc.weightx = 1; + gbc.weighty = 1; + gbc.fill = GridBagConstraints.HORIZONTAL; + add(expressionPanel, gbc); + + JPanel buttonPanel = new JPanel(); + buttonPanel.setLayout(new GridBagLayout()); + JButton cancelButton = new JButton("Cancel"); + saveButton = new JButton("Save"); + saveButton.setEnabled(!includesPlaceHolder()); + + cancelButton.addActionListener(e -> dispose()); + saveButton.addActionListener(e -> { + boolean nameExists = false; + for (int i = 0; i < observationModel.getSize(); i++) { + Observation obs = observationModel.getElementAt(i); + if (obs.getName().equals(nameField.getText()) && + !obs.equals(observation)) { + nameExists = true; + break; + } + } + + if (nameExists) { + JOptionPane.showMessageDialog(TAPAALGUI.getApp(), "An observation with the name \"" + observation.getName() + "\" already exists.", "Error", JOptionPane.ERROR_MESSAGE); + } else { + observation.setName(nameField.getText()); + observation.setExpression(currentExpr); + + if (isNewObservation) { + observationModel.addElement(observation); + } else { + observationModel.setElementAt(observation, observationModel.indexOf(observation)); + } + + dispose(); + } + }); + + GridBagConstraints buttonGbc = new GridBagConstraints(); + buttonGbc.gridx = 0; + buttonGbc.gridy = 0; + buttonGbc.weightx = 1; + buttonGbc.anchor = GridBagConstraints.EAST; + buttonGbc.insets = new Insets(0, 0, 0, 5); + buttonPanel.add(cancelButton, buttonGbc); + buttonGbc.insets = new Insets(0, 0, 0, 0); + ++buttonGbc.gridx; + buttonPanel.add(saveButton, buttonGbc); + + ++gbc.gridy; + gbc.anchor = GridBagConstraints.EAST; + gbc.fill = GridBagConstraints.NONE; + gbc.weightx = 0; + gbc.weighty = 0; + add(buttonPanel, gbc); + + pack(); + } + + private void toggleManualEditing() { + isEditing = !isEditing; + + Enabler.setAllEnabled(operationsPanel, !isEditing); + Enabler.setAllEnabled(placesPanel, !isEditing); + Enabler.setAllEnabled(constantsPanel, !isEditing); + + if (isEditing) { + saveButton.setEnabled(false); + } else { + saveButton.setEnabled(!includesPlaceHolder()); + } + + expressionField.setEditable(isEditing); + + if (isEditing) { + resetExpression.setText("Parse Expression"); + editExpression.setText("Cancel"); + } else { + resetExpression.setText("Reset Expression"); + editExpression.setText("Edit Expression"); + } + } + + private void updateExpression(ObsExpression newExpr) { + String selectedText = expressionField.getSelectedText(); + String fullText = expressionField.getText(); + ObsExpression oldExpr = currentExpr.deepCopy(); + if (selectedText != null && + !selectedText.equals(fullText) && + currentExpr.isOperator()) { + ((ObsOperator)currentExpr).replace(selectedExpr, newExpr); + } else if (currentExpr.isOperator() && selectedText == null) { + ((ObsOperator)currentExpr).insertLeftMost(newExpr); + } else { + currentExpr = newExpr; + } + + if (!currentExpr.toString().equals(oldExpr.toString())) { + expressionField.setText(currentExpr.toString()); + undoManager.addEdit(new ExpressionEdit(oldExpr, currentExpr.deepCopy())); + refreshUndoRedoButtons(); + saveButton.setEnabled(!includesPlaceHolder()); + } + } + + private void refreshUndoRedoButtons() { + undoButton.setEnabled(undoManager.canUndo()); + redoButton.setEnabled(undoManager.canRedo()); + } + + private boolean includesPlaceHolder() { + return currentExpr.toString().contains(new ObsPlaceHolder().toString()); + } + + private class ExpressionEdit extends AbstractUndoableEdit { + private final ObsExpression oldExpr; + private final ObsExpression newExpr; + + public ExpressionEdit(ObsExpression oldExpr, ObsExpression newExpr) { + this.oldExpr = oldExpr; + this.newExpr = newExpr; + } + + @Override + public void undo() { + super.undo(); + currentExpr = oldExpr; + expressionField.setText(currentExpr.toString()); + refreshUndoRedoButtons(); + } + + @Override + public void redo() { + super.redo(); + currentExpr = newExpr; + expressionField.setText(currentExpr.toString()); + refreshUndoRedoButtons(); + } + } +} diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/ObservationListDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/ObservationListDialog.java new file mode 100644 index 000000000..4612f5527 --- /dev/null +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/ObservationListDialog.java @@ -0,0 +1,162 @@ +package net.tapaal.gui.petrinet.dialog; + +import javax.swing.DefaultListModel; +import javax.swing.JButton; +import javax.swing.JList; +import javax.swing.JPanel; +import javax.swing.JScrollPane; +import javax.swing.event.ListDataListener; +import javax.swing.event.ListDataEvent; + +import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork; +import dk.aau.cs.verification.observations.Observation; +import pipe.gui.TAPAALGUI; +import pipe.gui.swingcomponents.EscapableDialog; + +import java.awt.Dimension; +import java.awt.GridBagLayout; +import java.awt.Insets; +import java.awt.GridBagConstraints; +import java.util.List; + +public class ObservationListDialog extends EscapableDialog { + private final TimedArcPetriNetNetwork tapnNetwork; + + private final List observations; + + public ObservationListDialog(TimedArcPetriNetNetwork tapnNetwork, List observations) { + super(TAPAALGUI.getApp(), "Observations", true); + this.tapnNetwork = tapnNetwork; + this.observations = observations; + + init(); + } + + private void init() { + setSize(500, 350); + setResizable(false); + + setLayout(new GridBagLayout()); + + JPanel observationPanel = new JPanel(); + observationPanel.setLayout(new GridBagLayout()); + DefaultListModel listModel = new DefaultListModel<>(); + for (Observation observation : observations) { + listModel.addElement(observation); + } + + listModel.addListDataListener(new ListDataListener() { + @Override + public void intervalAdded(ListDataEvent e) { + for (int i = e.getIndex0(); i <= e.getIndex1(); ++i) { + observations.add(i, listModel.getElementAt(i)); + } + } + + @Override + public void intervalRemoved(ListDataEvent e) { + for (int i = e.getIndex0(); i <= e.getIndex1(); ++i) { + observations.remove(i); + } + } + + @Override + public void contentsChanged(ListDataEvent e) { + for (int i = e.getIndex0(); i <= e.getIndex1(); ++i) { + observations.set(i, listModel.getElementAt(i)); + } + } + }); + + JList observationList = new JList<>(listModel); + + JScrollPane observationScrollPane = new JScrollPane(observationList); + observationScrollPane.setPreferredSize(new Dimension(500, observationScrollPane.getPreferredSize().height)); + + JButton editButton = new JButton("Edit"); + editButton.setEnabled(false); + editButton.addActionListener(e -> { + int selectedIndex = observationList.getSelectedIndex(); + if (selectedIndex != -1) { + ObservationDialog observationDialog = new ObservationDialog(tapnNetwork, listModel, listModel.get(selectedIndex)); + + observationDialog.setLocationRelativeTo(this); + observationDialog.setVisible(true); + } + }); + + JButton removeButton = new JButton("Remove"); + removeButton.setEnabled(false); + removeButton.addActionListener(e -> { + for (Observation observation : observationList.getSelectedValuesList()) { + listModel.removeElement(observation); + } + }); + + JButton newButton = new JButton("New"); + newButton.addActionListener(e -> { + ObservationDialog observationDialog = new ObservationDialog(tapnNetwork, listModel); + observationDialog.setLocationRelativeTo(this); + observationDialog.setVisible(true); + }); + + observationList.addListSelectionListener(e -> { + if (!e.getValueIsAdjusting()) { + boolean elemIsSelected = observationList.getSelectedIndex() != -1; + editButton.setEnabled(elemIsSelected); + removeButton.setEnabled(elemIsSelected); + } + }); + + GridBagConstraints observationGbc = new GridBagConstraints(); + observationGbc.gridx = 0; + observationGbc.gridy = 0; + observationGbc.weightx = 1; + observationGbc.weighty = 1; + observationGbc.fill = GridBagConstraints.BOTH; + observationGbc.gridwidth = 3; + observationPanel.add(observationScrollPane, observationGbc); + ++observationGbc.gridy; + observationGbc.gridwidth = 1; + observationGbc.fill = GridBagConstraints.HORIZONTAL; + observationPanel.add(editButton, observationGbc); + ++observationGbc.gridx; + observationPanel.add(removeButton, observationGbc); + ++observationGbc.gridx; + observationPanel.add(newButton, observationGbc); + + GridBagConstraints gbc = new GridBagConstraints(); + gbc.gridx = 0; + gbc.gridy = 0; + gbc.weightx = 1; + gbc.weighty = 1; + gbc.fill = GridBagConstraints.BOTH; + gbc.insets = new Insets(10, 10, 10, 10); + + add(observationPanel, gbc); + + JPanel buttonPanel = new JPanel(); + buttonPanel.setLayout(new GridBagLayout()); + + JButton okButton = new JButton("OK"); + + okButton.addActionListener(e -> { + dispose(); + }); + + GridBagConstraints buttonGbc = new GridBagConstraints(); + + buttonGbc.gridx = 0; + buttonGbc.gridy = 0; + buttonGbc.anchor = GridBagConstraints.EAST; + buttonPanel.add(okButton, buttonGbc); + + ++gbc.gridy; + gbc.anchor = GridBagConstraints.EAST; + gbc.fill = GridBagConstraints.NONE; + gbc.weightx = 0; + add(buttonPanel, gbc); + + pack(); + } +} diff --git a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java index 75f210b54..45764522e 100644 --- a/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java +++ b/src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java @@ -43,6 +43,7 @@ import dk.aau.cs.model.CPN.Variable; import dk.aau.cs.model.tapn.*; import dk.aau.cs.verification.VerifyTAPN.*; +import dk.aau.cs.verification.observations.Observation; import net.tapaal.gui.petrinet.verification.*; import net.tapaal.swinghelpers.CustomJSpinner; import pipe.gui.petrinet.dataLayer.DataLayer; @@ -52,6 +53,7 @@ import net.tapaal.gui.petrinet.verification.TAPNQuery.SearchOption; import net.tapaal.gui.petrinet.verification.TAPNQuery.TraceOption; import net.tapaal.gui.petrinet.verification.TAPNQuery.VerificationType; +import net.tapaal.helpers.Enabler; import pipe.gui.*; import dk.aau.cs.TCTL.Parsing.TAPAALQueryParser; import dk.aau.cs.approximation.OverApproximation; @@ -256,6 +258,7 @@ public enum QueryDialogueOption { private boolean smcMustUpdateTime = true; private boolean doingBenchmark = false; private RunVerificationBase benchmarkThread = null; + private java.util.List smcObservations; // Buttons in the bottom of the dialogue private JPanel buttonPanel; @@ -854,6 +857,8 @@ private void setSMCSettings(SMCSettings settings) { smcTimeBoundInfinite.setEnabled(!smcStepBoundInfinite.isSelected()); smcStepBoundInfinite.setEnabled(!smcTimeBoundInfinite.isSelected()); + smcObservations = settings.getObservations(); + smcConfidence.setText(String.valueOf(settings.confidence)); if(!doingBenchmark) smcEstimationIntervalWidth.setText(precisionFormat.format(settings.estimationIntervalWidth)); @@ -1620,8 +1625,9 @@ private void disableEditingButtons() { private void enableEditingButtons() { refreshUndoRedo(); - if (currentSelection != null) - deleteButton.setEnabled(true); + if (currentSelection != null) { + deleteButton.setEnabled(currentSelection != null); + } } private void returnFromManualEdit(TCTLAbstractProperty newQuery) { @@ -3076,6 +3082,17 @@ public void focusLost(FocusEvent focusEvent) { guiDialog.pack(); }); + JButton smcObservationsButton = new JButton("Edit observations"); + smcObservationsButton.addActionListener(evt -> { + ObservationListDialog dialog = new ObservationListDialog(tapnNetwork, smcObservations); + dialog.setLocationRelativeTo(guiDialog); + dialog.setVisible(true); + }); + + gbc.gridx = 0; + gbc.gridy = 1; + smcSettingsPanel.add(smcObservationsButton, gbc); + GridBagConstraints gridBagConstraints = new GridBagConstraints(); gridBagConstraints.gridx = 0; gridBagConstraints.gridy = 3; @@ -5343,16 +5360,16 @@ private void showEngineHelp() { } private void setVerificationOptionsEnabled(boolean isEnabled) { - setAllEnabled(reductionOptionsPanel, isEnabled); + Enabler.setAllEnabled(reductionOptionsPanel, isEnabled); if (unfoldingOptionsPanel != null) { - setAllEnabled(unfoldingOptionsPanel, isEnabled); + Enabler.setAllEnabled(unfoldingOptionsPanel, isEnabled); } - setAllEnabled(traceOptionsPanel, isEnabled); - setAllEnabled(boundednessCheckPanel, isEnabled); - setAllEnabled(searchOptionsPanel, isEnabled); - setAllEnabled(smcTracePanel, isEnabled); + Enabler.setAllEnabled(traceOptionsPanel, isEnabled); + Enabler.setAllEnabled(boundednessCheckPanel, isEnabled); + Enabler.setAllEnabled(searchOptionsPanel, isEnabled); + Enabler.setAllEnabled(smcTracePanel, isEnabled); smcVerificationTypeLabel.setEnabled(isEnabled); smcVerificationType.setEnabled(isEnabled); @@ -5362,18 +5379,6 @@ private void setVerificationOptionsEnabled(boolean isEnabled) { setEnabledOptionsAccordingToCurrentReduction(); } - // Enables or disables the container + all children recursively - private void setAllEnabled(Container container, boolean isEnabled) { - for (Component component : container.getComponents()) { - component.setEnabled(isEnabled); - if (component instanceof Container) { - setAllEnabled((Container) component, isEnabled); - } - } - - container.setEnabled(isEnabled); - } - protected void setEnabledOptionsAccordingToCurrentReduction() { refreshQueryEditingButtons(); diff --git a/src/main/java/net/tapaal/helpers/Enabler.java b/src/main/java/net/tapaal/helpers/Enabler.java new file mode 100644 index 000000000..483bad7c8 --- /dev/null +++ b/src/main/java/net/tapaal/helpers/Enabler.java @@ -0,0 +1,22 @@ +package net.tapaal.helpers; + +import java.awt.Component; +import java.awt.Container; + +public class Enabler { + /** + * Set all components in a container to be enabled or disabled. + * @param container The container to set the components of. + * @param isEnabled Whether the components should be enabled or disabled. + */ + public static void setAllEnabled(Container container, boolean isEnabled) { + for (Component component : container.getComponents()) { + component.setEnabled(isEnabled); + if (component instanceof Container) { + setAllEnabled((Container) component, isEnabled); + } + } + + container.setEnabled(isEnabled); + } +} diff --git a/src/main/javacc/dk/aau/cs/model/SMC/ObservationParser.jj b/src/main/javacc/dk/aau/cs/model/SMC/ObservationParser.jj new file mode 100644 index 000000000..3b508d3c3 --- /dev/null +++ b/src/main/javacc/dk/aau/cs/model/SMC/ObservationParser.jj @@ -0,0 +1,148 @@ +options { + STATIC = false; +} + +PARSER_BEGIN(ObservationParser) + +package dk.aau.cs.model.SMC; + +import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork; +import dk.aau.cs.verification.observations.expressions.ObsConstant; +import dk.aau.cs.verification.observations.expressions.ObsPlace; +import dk.aau.cs.verification.observations.expressions.ObsExpression; +import dk.aau.cs.verification.observations.expressions.ObsAdd; +import dk.aau.cs.verification.observations.expressions.ObsSubtract; +import dk.aau.cs.verification.observations.expressions.ObsMultiply; +import dk.aau.cs.verification.observations.expressions.ObsOperator; +import java.io.StringReader; + +public class ObservationParser { + private static TimedArcPetriNetNetwork network; + + public static ObsExpression parse(String observationExpressionStr, TimedArcPetriNetNetwork network) throws ParseException, TokenMgrError { + ObservationParser.network = network; + ObservationParser parser = new ObservationParser(new StringReader(observationExpressionStr)); + + return parser.startParsing(); + } +} + +PARSER_END(ObservationParser) + +TOKEN: +{ + + | + + | + + | + + | + + | + + | + + | + <#ALPHA: ["a"-"z","A"-"Z"]> + | + <#ALPHANUM: (["a"-"z","A"-"Z","0"-"9"])> + | + ("_" | )*> +} + +SKIP : +{ + " " + | "\t" + | "\n" + | "\r" +} + +ObsExpression startParsing(): { + ObsExpression expr; +} { + expr = expression() { return expr; } +} + +ObsExpression expression(): { + ObsExpression left, right; + ObsOperator root; + Token op; +} { + left = term() + ( + (op = | op = ) + { + root = op.kind == PLUS ? + new ObsAdd(left, null) : + new ObsSubtract(left, null); + + if (left.isOperator()) { + ((ObsOperator)left).setParent(root); + } + } + + right = term() + { + root.setRight(right); + if (right.isOperator()) { + ((ObsOperator)right).setParent(root); + } + left = root; + } + )* + { return left; } +} + +ObsExpression term(): { + ObsExpression left, right; + ObsOperator root; +} { + left = factor() + ( + + { + root = new ObsMultiply(left, null); + if (left.isOperator()) { + ((ObsOperator)left).setParent(root); + } + } + + right = factor() + { + root.setRight(right); + if (right.isOperator()) { + ((ObsOperator)right).setParent(root); + } + left = root; + } + )* + { return left; } +} + +ObsExpression factor(): { + ObsExpression expr; +} { + ( + expr = atom() | + expr = expression() + { + if (expr.isOperator()) { + ((ObsOperator)expr).hadParentheses(true); + } + } + ) + { return expr; } +} + +ObsExpression atom(): { + Token value, templateName, placeName; +} { + value = + { return new ObsConstant(Integer.parseInt(value.image)); } + | + templateName = placeName = + { return new ObsPlace(templateName.image, placeName.image, network); } +}