1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
|
package dk.aau.cs.TCTL;
import dk.aau.cs.TCTL.visitors.ITCTLVisitor;
public class TCTLAtomicPropositionNode extends TCTLAbstractStateProperty {
private TCTLAbstractStateProperty left;
private TCTLAbstractStateProperty right;
private String op;
public TCTLAbstractStateProperty getLeft() {
return left;
}
public void setLeft(TCTLAbstractStateProperty left) {
this.left = left;
}
public TCTLAbstractStateProperty getRight() {
return right;
}
public void setRight(TCTLAbstractStateProperty right) {
this.right = right;
}
public String getOp() {
return op;
}
public void setOp(String op) {
this.op = op;
}
public TCTLAtomicPropositionNode(TCTLAbstractStateProperty left, String op, TCTLAbstractStateProperty right) {
this.left = left;
this.op = op;
this.right = right;
}
@Override
public TCTLAbstractStateProperty copy() {
return new TCTLAtomicPropositionNode(left.copy(), op, right.copy());
}
@Override
public boolean equals(Object o) {
if (o instanceof TCTLAtomicPropositionNode) {
TCTLAtomicPropositionNode node = (TCTLAtomicPropositionNode) o;
// TODO: Not sure if this is intentional but this is reference
// equals and not equality
return left.equals(node.left)
&& right.equals(node.right) && op.equals(node.getOp());
}
return false;
}
@Override
public TCTLAbstractStateProperty replace(TCTLAbstractProperty object1,
TCTLAbstractProperty object2) {
if (this == object1 && object2 instanceof TCTLAbstractStateProperty) {
TCTLAbstractStateProperty obj2 = (TCTLAbstractStateProperty) object2;
obj2.setParent(parent);
return obj2;
} else {
return this;
}
}
@Override
public String toString() {
return left + " " + op + " " + right;
}
@Override
public void accept(ITCTLVisitor visitor, Object context) {
visitor.visit(this, context);
}
@Override
public boolean containsPlaceHolder() {
return left.containsPlaceHolder() || right.containsPlaceHolder();
}
@Override
public boolean hasNestedPathQuantifiers() {
return false;
}
@Override
public TCTLAbstractProperty findFirstPlaceHolder() {
TCTLAbstractProperty rightP = right.findFirstPlaceHolder();
return rightP == null ? left.findFirstPlaceHolder() : rightP;
}
public boolean containsAtomicPropositionWithSpecificPlaceInTemplate(String templateName, String placeName) {
return right.containsAtomicPropositionWithSpecificPlaceInTemplate(templateName, placeName) ||
left.containsAtomicPropositionWithSpecificPlaceInTemplate(templateName, placeName);
}
public boolean containsAtomicPropositionWithSpecificTransitionInTemplate(String templateName, String transitionName) {
return right.containsAtomicPropositionWithSpecificTransitionInTemplate(templateName, transitionName) ||
left.containsAtomicPropositionWithSpecificTransitionInTemplate(templateName, transitionName);
}
}
|