Skip to content

Commit

Permalink
CPN Guard dialog parenthesis - fix 2046277 (#126)
Browse files Browse the repository at this point in the history 
Fixes:
https://bugs.launchpad.net/tapaal/+bug/2046277
  • Loading branch information
@srba
srba authored Jan 18, 2024
2 parents a0b9593 + ca8a83a commit 24f955a
Show file tree
Hide file tree
Showing 9 changed files with 246 additions and 48 deletions.
18 changes: 15 additions & 3 deletions src/main/java/dk/aau/cs/TCTL/TCTLAndListNode.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@
public class TCTLAndListNode extends TCTLAbstractStateProperty {

private List<TCTLAbstractStateProperty> properties;
private boolean isSimpleProperty;

public void setProperties(List<TCTLAbstractStateProperty> properties) {
this.properties = properties;
Expand Down Expand Up @@ -61,7 +62,7 @@ public void addConjunct(TCTLAbstractStateProperty conjunct) {

@Override
public boolean isSimpleProperty() {
return false;
return isSimpleProperty;
}

@Override
Expand All @@ -76,12 +77,20 @@ public String toString() {
s.append(" and ");
}

if (prop instanceof TCTLAndListNode) {
((TCTLAndListNode) prop).setSimpleProperty(isSimpleProperty);
}

s.append(prop.isSimpleProperty() ? prop.toString() : "(" + prop + ")");
firstTime = false;
}

return s.toString();
}

public void setSimpleProperty(boolean isSimpleProperty) {
this.isSimpleProperty = isSimpleProperty;
}

@Override
public StringPosition[] getChildren() {
Expand Down Expand Up @@ -138,13 +147,16 @@ public boolean equals(Object o) {

@Override
public TCTLAbstractStateProperty copy() {
ArrayList<TCTLAbstractStateProperty> copy = new ArrayList<TCTLAbstractStateProperty>();
List<TCTLAbstractStateProperty> copy = new ArrayList<>();

for (TCTLAbstractStateProperty p : properties) {
copy.add(p.copy());
}

return new TCTLAndListNode(copy);
TCTLAndListNode andListNode = new TCTLAndListNode(copy);
andListNode.setSimpleProperty(isSimpleProperty());

return andListNode;
}

@Override
Expand Down
21 changes: 17 additions & 4 deletions src/main/java/dk/aau/cs/TCTL/TCTLOrListNode.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@
public class TCTLOrListNode extends TCTLAbstractStateProperty {

private List<TCTLAbstractStateProperty> properties;
private boolean isSimpleProperty;

public void setProperties(List<TCTLAbstractStateProperty> properties) {
this.properties = properties;
Expand All @@ -31,7 +32,7 @@ public TCTLOrListNode(List<TCTLAbstractStateProperty> properties) {

public TCTLOrListNode(TCTLOrListNode orListNode) {
properties = new ArrayList<TCTLAbstractStateProperty>();

for (TCTLAbstractStateProperty p : orListNode.properties) {
addDisjunct(p.copy());
}
Expand Down Expand Up @@ -62,7 +63,7 @@ public void addDisjunct(TCTLAbstractStateProperty disjunct) {

@Override
public boolean isSimpleProperty() {
return false;
return isSimpleProperty;
}

@Override
Expand All @@ -77,13 +78,21 @@ public String toString() {
s.append(" or ");
}

if (prop instanceof TCTLOrListNode) {
((TCTLOrListNode) prop).setSimpleProperty(isSimpleProperty);
}

s.append(prop.isSimpleProperty() ? prop.toString() : "(" + prop + ")");
firstTime = false;
}

return s.toString();
}

public void setSimpleProperty(boolean isSimpleProperty) {
this.isSimpleProperty = isSimpleProperty;
}

@Override
public StringPosition[] getChildren() {
StringPosition[] children = new StringPosition[properties.size()];
Expand Down Expand Up @@ -139,18 +148,22 @@ public boolean equals(Object o) {

@Override
public TCTLAbstractStateProperty copy() {
ArrayList<TCTLAbstractStateProperty> copy = new ArrayList<TCTLAbstractStateProperty>();
List<TCTLAbstractStateProperty> copy = new ArrayList<>();

for (TCTLAbstractStateProperty p : properties) {
copy.add(p.copy());
}

return new TCTLOrListNode(copy);
TCTLOrListNode orListNode = new TCTLOrListNode(copy);
orListNode.setSimpleProperty(isSimpleProperty());

return orListNode;
}

@Override
public TCTLAbstractStateProperty replace(TCTLAbstractProperty object1,
TCTLAbstractProperty object2) {

if (this == object1 && object2 instanceof TCTLAbstractStateProperty) {
TCTLAbstractStateProperty obj2 = (TCTLAbstractStateProperty) object2;
obj2.setParent(parent);
Expand Down
17 changes: 13 additions & 4 deletions src/main/java/dk/aau/cs/io/LoadTACPN.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -397,18 +397,27 @@ public GuardExpression parseGuardExpression(Node node) throws FormatException {
return new NotExpression(childexp);
} else if (name.equals("and")) {
Tuple<GuardExpression, GuardExpression> subexps = parseLRGuardExpressions(node);
return new AndExpression(subexps.value1(), subexps.value2());
AndExpression andExpr = new AndExpression(subexps.value1(), subexps.value2());
Node isSimpleNode = node.getAttributes().getNamedItem("isSimple");
if (isSimpleNode != null) {
andExpr.setSimpleProperty(Boolean.parseBoolean(isSimpleNode.getNodeValue()));
}
return andExpr;
} else if (name.equals("or")) {
Node left = skipWS(node.getFirstChild());
Node right = skipWS(left.getNextSibling());
if(right == null){
return parseGuardExpression(left);
}
GuardExpression parentOr = new OrExpression(parseGuardExpression(left), parseGuardExpression(right));
OrExpression orExpr = new OrExpression(parseGuardExpression(left), parseGuardExpression(right));
Node isSimpleNode = node.getAttributes().getNamedItem("isSimple");
if (isSimpleNode != null) {
orExpr.setSimpleProperty(Boolean.parseBoolean(isSimpleNode.getNodeValue()));
}
for (var it = skipWS(right.getNextSibling()); it != null; it = skipWS(it.getNextSibling())){
parentOr = new OrExpression(parentOr, parseGuardExpression(it));
orExpr = new OrExpression(orExpr, parseGuardExpression(it));
}
return parentOr;
return orExpr;
} else if (name.matches("subterm|structure")) {
Node child = skipWS(node.getFirstChild());
return parseGuardExpression(child);
Expand Down
2 changes: 2 additions & 0 deletions src/main/java/dk/aau/cs/io/writeTACPN.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -222,6 +222,7 @@ private Element parseGuardExpression(Expression expression, Document document, E
Element subtermElement = document.createElement("subterm");
andElement.appendChild(subtermElement);
AndExpression expr = (AndExpression) expression;
andElement.setAttribute("isSimple", String.valueOf(expr.isSimpleProperty()));
andElement.appendChild(parseGuardExpression(expr.getLeftExpression(), document, subtermElement));
Element subtermElement2 = document.createElement("subterm");
andElement.appendChild(parseGuardExpression(expr.getRightExpression(), document, subtermElement2));
Expand All @@ -231,6 +232,7 @@ private Element parseGuardExpression(Expression expression, Document document, E
Element subtermElement = document.createElement("subterm");
orElement.appendChild(subtermElement);
OrExpression expr = (OrExpression) expression;
orElement.setAttribute("isSimple", String.valueOf(expr.isSimpleProperty()));
orElement.appendChild(parseGuardExpression(expr.getLeftExpression(), document, subtermElement));
Element subtermElement2 = document.createElement("subterm");
orElement.appendChild(parseGuardExpression(expr.getRightExpression(), document, subtermElement2));
Expand Down
31 changes: 23 additions & 8 deletions src/main/java/dk/aau/cs/model/CPN/Expressions/AndExpression.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,8 +8,11 @@
import java.util.Set;

public class AndExpression extends GuardExpression {
private GuardExpression left;
private GuardExpression left;
private GuardExpression right;

private boolean isSimpleProperty;
private String word = "and";

public AndExpression(GuardExpression left, GuardExpression right) {
this.left = left;
Expand Down Expand Up @@ -81,17 +84,16 @@ public boolean containsColor(Color color) {
}

@Override
public String toString() {
return "(" + left.toString() + " and " + right.toString() + ")";
}
public boolean isSimpleProperty() { return isSimpleProperty; }

@Override
public boolean isSimpleProperty() {return false; }
public void setSimpleProperty(boolean isSimpleProperty) {
this.isSimpleProperty = isSimpleProperty;
}

@Override
public ExprStringPosition[] getChildren() {
ExprStringPosition[] children = new ExprStringPosition[2];
int start = 1;
int start = isSimpleProperty ? 0 : 1;
int endPrev;
int end;

Expand All @@ -118,6 +120,19 @@ public boolean equals(Object o) {

@Override
public GuardExpression copy() {
return new AndExpression(left, right);
AndExpression copy = new AndExpression(left, right);
copy.setSimpleProperty(isSimpleProperty());

return copy;
}

@Override
public String toString() {
final String text = left.toString() + " " + word + " " + right.toString();
return isSimpleProperty ? text : "(" + text + ")";
}

public String getWord() {
return word;
}
}
29 changes: 22 additions & 7 deletions src/main/java/dk/aau/cs/model/CPN/Expressions/OrExpression.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,9 @@ public class OrExpression extends GuardExpression {
private GuardExpression left;
private GuardExpression right;

private boolean isSimpleProperty;
private String word = "or";

public OrExpression(GuardExpression left, GuardExpression right) {
this.left = left;
this.right = right;
Expand All @@ -23,20 +26,24 @@ public boolean containsColor(Color color) {
}

public GuardExpression getLeftExpression() {
return this.left;
return left;
}

public GuardExpression getRightExpression() {
return this.right;
return right;
}

@Override
public boolean isSimpleProperty() {return false; }
public boolean isSimpleProperty() { return isSimpleProperty; }

public void setSimpleProperty(boolean isSimpleProperty) {
this.isSimpleProperty = isSimpleProperty;
}

@Override
public ExprStringPosition[] getChildren() {
ExprStringPosition[] children = new ExprStringPosition[2];
int start = 1;
int start = isSimpleProperty ? 0 : 1;
int endPrev;
int end;

Expand Down Expand Up @@ -64,7 +71,10 @@ public boolean equals(Object o) {

@Override
public GuardExpression copy() {
return new AndExpression(left, right);
OrExpression copy = new OrExpression(left, right);
copy.setSimpleProperty(isSimpleProperty());

return copy;
}

@Override
Expand Down Expand Up @@ -117,7 +127,12 @@ public Boolean eval(ExpressionContext context) {
}

@Override
public String toString() {
return "(" + left.toString() + " or " + right.toString() + ")";
public String toString() {
final String text = left.toString() + " " + word + " " + right.toString();
return isSimpleProperty ? text : "(" + text + ")";
}

public String getWord() {
return word;
}
}
24 changes: 22 additions & 2 deletions src/main/java/net/tapaal/gui/petrinet/dialog/QueryDialog.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -273,6 +273,7 @@ public enum QueryDialogueOption {
private final static EngineSupportOptions[] engineSupportOptions = new EngineSupportOptions[]{verifyDTAPNOptions,verifyTAPNOptions,UPPAALCombiOptions,UPPAALOptimizedStandardOptions,UPPAALStandardOptions,UPPAALBroadcastOptions,UPPAALBroadcastDegree2Options,verifyPNOptions};

private TCTLAbstractProperty newProperty;
private TCTLAbstractProperty previousProp;
private JTextField queryName;

private static Boolean advancedView = false;
Expand Down Expand Up @@ -2991,6 +2992,7 @@ private void initLogicPanel() {
TCTLAndListNode andListNode = null;
if (currentSelection.getObject() instanceof TCTLAndListNode) {
andListNode = new TCTLAndListNode((TCTLAndListNode) currentSelection.getObject());
andListNode.setSimpleProperty(true);
andListNode.addConjunct(new TCTLStatePlaceHolder());
addPropertyToQuery(andListNode);
} else if (currentSelection.getObject() instanceof TCTLOrListNode) {
Expand All @@ -3014,6 +3016,7 @@ private void initLogicPanel() {
} else {
TCTLStatePlaceHolder ph = new TCTLStatePlaceHolder();
andListNode = new TCTLAndListNode(getStateProperty(currentSelection.getObject()), ph);

addPropertyToQuery(andListNode);
}
} else if (!lens.isTimed()) {
Expand All @@ -3023,8 +3026,10 @@ private void initLogicPanel() {

disjunctionButton.addActionListener(e -> {
TCTLOrListNode orListNode;

if (currentSelection.getObject() instanceof TCTLOrListNode) {
orListNode = new TCTLOrListNode((TCTLOrListNode) currentSelection.getObject());
orListNode.setSimpleProperty(true);
orListNode.addDisjunct(new TCTLStatePlaceHolder());
addPropertyToQuery(orListNode);
} else if (currentSelection.getObject() instanceof TCTLAndListNode) {
Expand All @@ -3033,7 +3038,7 @@ private void initLogicPanel() {
} else if (currentSelection.getObject() instanceof TCTLAbstractStateProperty) {
TCTLAbstractStateProperty prop = (TCTLAbstractStateProperty) currentSelection.getObject();
TCTLAbstractProperty parentNode = prop.getParent();

if (parentNode instanceof TCTLOrListNode) {
// current selection is child of an orList node => add
// new placeholder disjunct to it
Expand Down Expand Up @@ -3087,6 +3092,8 @@ private void checkUntimedAndNode() {
andListNode = new TCTLAndListNode(getStateProperty(prop), ph);
}

andListNode.setSimpleProperty(true);

TCTLAbstractPathProperty property = new TCTLStateToPathConverter(andListNode);
addPropertyToQuery(property);
} else if (currentSelection.getObject() instanceof TCTLAbstractPathProperty) {
Expand All @@ -3096,7 +3103,13 @@ private void checkUntimedAndNode() {

andListNode = new TCTLAndListNode(getStateProperty(
new TCTLPathToStateConverter((TCTLAbstractPathProperty) oldProperty)), ph);

if (previousProp instanceof TCTLAndListNode) {
andListNode.setSimpleProperty(true);
}

previousProp = andListNode;

TCTLAbstractPathProperty property = new TCTLStateToPathConverter(andListNode);
addPropertyToQuery(property);
}
Expand All @@ -3106,7 +3119,6 @@ private void checkUntimedOrNode() {
TCTLOrListNode orListNode;
if (currentSelection.getObject() instanceof TCTLStateToPathConverter) {
TCTLStatePlaceHolder ph = new TCTLStatePlaceHolder();

TCTLAbstractStateProperty prop = ((TCTLStateToPathConverter) currentSelection.getObject()).getProperty();

if (prop instanceof TCTLOrListNode) {
Expand All @@ -3118,6 +3130,8 @@ private void checkUntimedOrNode() {
orListNode = new TCTLOrListNode(getStateProperty(prop), ph);
}

orListNode.setSimpleProperty(true);

TCTLAbstractPathProperty property = new TCTLStateToPathConverter(orListNode);
addPropertyToQuery(property);
} else if (currentSelection.getObject() instanceof TCTLAbstractPathProperty) {
Expand All @@ -3126,7 +3140,13 @@ private void checkUntimedOrNode() {

orListNode = new TCTLOrListNode(getStateProperty(
new TCTLPathToStateConverter((TCTLAbstractPathProperty) oldProperty)), ph);

if (previousProp instanceof TCTLOrListNode) {
orListNode.setSimpleProperty(true);
}

previousProp = orListNode;

TCTLAbstractPathProperty property = new TCTLStateToPathConverter(orListNode);
addPropertyToQuery(property);
}
Expand Down
Loading

0 comments on commit 24f955a

Please sign in to comment.