~tapaal-contributor/tapaal/disappearing-tokens-1940098

« back to all changes in this revision

Viewing changes to src/dk/aau/cs/TCTL/visitors/VerifyPlaceNamesVisitor.java

  • Committer: Kenneth Yrke Jørgensen
  • Date: 2011-04-12 09:50:16 UTC
  • mfrom: (329.1.188 tapaal-1.5)
  • Revision ID: mail@yrke.dk-20110412095016-e4hqdgab5596ja09
Merged with branch addning support for new 1.5 features

Show diffs side-by-side

added added

removed removed

Lines of Context:
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;
18
19
 
19
20
public class VerifyPlaceNamesVisitor implements ITCTLVisitor {
20
 
        
21
 
        private ArrayList<String> placeNames;
22
 
 
23
 
        public VerifyPlaceNamesVisitor(ArrayList<String> placeNames) {
24
 
                this.placeNames = placeNames;
 
21
 
 
22
        private ArrayList<Tuple<String, String>> templatePlaceNames;
 
23
 
 
24
        public VerifyPlaceNamesVisitor(ArrayList<Tuple<String, String>> templatePlaceNames) {
 
25
                this.templatePlaceNames = templatePlaceNames;
25
26
        }
26
27
 
27
 
        public Context VerifyPlaceNames(TCTLAbstractProperty query)
28
 
        {
 
28
        public Context VerifyPlaceNames(TCTLAbstractProperty query) {
29
29
                Context c = new Context();
30
 
                
 
30
 
31
31
                query.accept(this, c);
32
 
                
 
32
 
33
33
                return c;
34
34
        }
35
 
        
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); }
 
35
 
 
36
        public void visit(TCTLAFNode afNode, Object context) {
 
37
                afNode.getProperty().accept(this, context);
 
38
        }
 
39
 
 
40
        public void visit(TCTLAGNode agNode, Object context) {
 
41
                agNode.getProperty().accept(this, context);
 
42
        }
 
43
 
 
44
        public void visit(TCTLEFNode efNode, Object context) {
 
45
                efNode.getProperty().accept(this, context);
 
46
        }
 
47
 
 
48
        public void visit(TCTLEGNode egNode, Object context) {
 
49
                egNode.getProperty().accept(this, context);
 
50
        }
40
51
 
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);
46
57
                }
47
58
        }
48
59
 
49
 
        public void visit(TCTLStatePlaceHolder statePlaceHolderNode, Object context) { }
50
 
        public void visit(TCTLPathPlaceHolder pathPlaceHolderNode, Object context) { }
 
60
        public void visit(TCTLStatePlaceHolder statePlaceHolderNode, Object context) {
 
61
        }
 
62
 
 
63
        public void visit(TCTLPathPlaceHolder pathPlaceHolderNode, Object context) {
 
64
        }
51
65
 
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);
59
 
                }               
 
73
                }
60
74
        }
61
 
        
 
75
 
62
76
        public void visit(TCTLOrListNode orListNode, Object context) {
63
77
                for (TCTLAbstractStateProperty p : orListNode.getProperties()) {
64
78
                        p.accept(this, context);
65
 
                }               
 
79
                }
66
80
        }
67
 
        
68
 
        
69
 
        /// context class
70
 
        public class Context
71
 
        {
 
81
 
 
82
        // / context class
 
83
        public class Context {
72
84
                private Boolean result;
73
85
                private HashSet<String> incorrectPlaceNames;
74
 
                
75
 
                public Boolean getResult()
76
 
                {
 
86
 
 
87
                public Boolean getResult() {
77
88
                        return result;
78
89
                }
79
 
                
 
90
 
80
91
                public void setResult(Boolean result) {
81
92
                        this.result = result;
82
93
                }
85
96
                        return incorrectPlaceNames;
86
97
                }
87
98
 
88
 
                public void AddIncorrectPlaceName(String incorrectPlaceName)
89
 
                {
 
99
                public void AddIncorrectPlaceName(String incorrectPlaceName) {
90
100
                        incorrectPlaceNames.add(incorrectPlaceName);
91
101
                }
92
102
 
93
 
                public Context()
94
 
                {
 
103
                public Context() {
95
104
                        this.result = true;
96
105
                        this.incorrectPlaceNames = new HashSet<String>();
97
106
                }