15
15
import dk.aau.cs.TCTL.TCTLOrListNode;
16
16
import dk.aau.cs.TCTL.TCTLPathPlaceHolder;
17
17
import dk.aau.cs.TCTL.TCTLStatePlaceHolder;
18
import dk.aau.cs.util.Tuple;
19
20
public class VerifyPlaceNamesVisitor implements ITCTLVisitor {
21
private ArrayList<String> placeNames;
23
public VerifyPlaceNamesVisitor(ArrayList<String> placeNames) {
24
this.placeNames = placeNames;
22
private ArrayList<Tuple<String, String>> templatePlaceNames;
24
public VerifyPlaceNamesVisitor(ArrayList<Tuple<String, String>> templatePlaceNames) {
25
this.templatePlaceNames = templatePlaceNames;
27
public Context VerifyPlaceNames(TCTLAbstractProperty query)
28
public Context VerifyPlaceNames(TCTLAbstractProperty query) {
29
29
Context c = new Context();
31
31
query.accept(this, c);
36
public void visit(TCTLAFNode afNode, Object context) { afNode.getProperty().accept(this, context); }
37
public void visit(TCTLAGNode agNode, Object context) { agNode.getProperty().accept(this, context); }
38
public void visit(TCTLEFNode efNode, Object context) { efNode.getProperty().accept(this, context); }
39
public void visit(TCTLEGNode egNode, Object context) { egNode.getProperty().accept(this, context); }
36
public void visit(TCTLAFNode afNode, Object context) {
37
afNode.getProperty().accept(this, context);
40
public void visit(TCTLAGNode agNode, Object context) {
41
agNode.getProperty().accept(this, context);
44
public void visit(TCTLEFNode efNode, Object context) {
45
efNode.getProperty().accept(this, context);
48
public void visit(TCTLEGNode egNode, Object context) {
49
egNode.getProperty().accept(this, context);
41
52
public void visit(TCTLAtomicPropositionNode atomicPropositionNode, Object context) {
42
Context c = (Context)context;
43
if(!placeNames.contains(atomicPropositionNode.getPlace())) {
44
c.AddIncorrectPlaceName(atomicPropositionNode.getPlace());
53
Context c = (Context) context;
54
if (!templatePlaceNames.contains(new Tuple<String,String>(atomicPropositionNode.getTemplate(), atomicPropositionNode.getPlace()))) {
55
c.AddIncorrectPlaceName(atomicPropositionNode.getTemplate() + "." + atomicPropositionNode.getPlace());
45
56
c.setResult(false);
49
public void visit(TCTLStatePlaceHolder statePlaceHolderNode, Object context) { }
50
public void visit(TCTLPathPlaceHolder pathPlaceHolderNode, Object context) { }
60
public void visit(TCTLStatePlaceHolder statePlaceHolderNode, Object context) {
63
public void visit(TCTLPathPlaceHolder pathPlaceHolderNode, Object context) {
52
66
public void visit(TCTLNotNode notNode, Object context) {
53
67
notNode.getProperty().accept(this, context);
56
70
public void visit(TCTLAndListNode andListNode, Object context) {
57
71
for (TCTLAbstractStateProperty p : andListNode.getProperties()) {
58
72
p.accept(this, context);
62
76
public void visit(TCTLOrListNode orListNode, Object context) {
63
77
for (TCTLAbstractStateProperty p : orListNode.getProperties()) {
64
78
p.accept(this, context);
83
public class Context {
72
84
private Boolean result;
73
85
private HashSet<String> incorrectPlaceNames;
75
public Boolean getResult()
87
public Boolean getResult() {
80
91
public void setResult(Boolean result) {
81
92
this.result = result;