← Back to branch summary

~tapaal-contributor/tapaal/weight-values-fix-1770637

« back to all changes in this revision

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

merged branch lp:~tapaal-contributor/tapaal/ctl-query-fix-1540367

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/dk/aau/cs/TCTL/visitors/CTLQueryVisitor.java
 
1
package dk.aau.cs.TCTL.visitors;
 
2
 
 
3
import java.util.List;
 
4
 
 
5
import dk.aau.cs.TCTL.*;
 
6
import dk.aau.cs.io.XMLFormatter;
 
7
import java.util.ArrayList;
 
8
 
 
9
public class CTLQueryVisitor extends VisitorBase {
 
10
        
 
11
        private static final String XML_NS                      = "xmlns=\"http://tapaal.net/\"";
 
12
        private static final String XML_PROPSET                 = "property-set";
 
13
        private static final String XML_PROP                    = "property";
 
14
        private static final String XML_PROPID                  = "id";
 
15
        private static final String XML_PROPDESC                = "description";
 
16
        private static final String XML_FORMULA                 = "formula";    
 
17
        private static final String XML_ALLPATHS                = "all-paths";
 
18
        private static final String XML_EXISTSPATH              = "exists-path";
 
19
        private static final String XML_NEGATION                = "negation";
 
20
        private static final String XML_CONJUNCTION             = "conjunction";
 
21
        private static final String XML_DISJUNCTION             = "disjunction";
 
22
        private static final String XML_GLOBALLY                = "globally";
 
23
        private static final String XML_FINALLY                 = "finally";
 
24
        private static final String XML_NEXT                    = "next";
 
25
        private static final String XML_UNTIL                   = "until";
 
26
        private static final String XML_BEFORE                  = "before";
 
27
        private static final String XML_REACH                   = "reach";
 
28
        private static final String XML_DEADLOCK                = "deadlock";
 
29
        private static final String XML_TRUE                    = "true";
 
30
        private static final String XML_FALSE                   = "false";
 
31
        private static final String XML_INTEGERLT               = "integer-lt";
 
32
        private static final String XML_INTEGERLE               = "integer-le";
 
33
        private static final String XML_INTEGEREQ               = "integer-eq";
 
34
        private static final String XML_INTEGERNE               = "integer-ne";
 
35
        private static final String XML_INTEGERGT               = "integer-gt";
 
36
        private static final String XML_INTEGERGE               = "integer-ge";
 
37
        private static final String XML_ISFIREABLE              = "is-fireable";
 
38
        private static final String XML_INTEGERCONSTANT         = "integer-constant";
 
39
        private static final String XML_TOKENSCOUNT             = "tokens-count";
 
40
        private static final String XML_PLACE                   = "place";
 
41
        private static final String XML_TRANSITION              = "transition";
 
42
        private static final String XML_INTEGERSUM = "integer-sum";
 
43
        private static final String XML_INTEGERPRODUCT = "integer-product";
 
44
        private static final String XML_INTEGERDIFFERENCE = "integer-difference";
 
45
 
 
46
        private StringBuffer XMLQuery;
 
47
        
 
48
        public CTLQueryVisitor() {
 
49
            this.XMLQuery = new StringBuffer();
 
50
        }
 
51
        
 
52
        public String getXMLQueryFor(TCTLAbstractProperty property, String queryName) {
 
53
            buildXMLQuery(property, queryName);
 
54
            return getFormatted();
 
55
        }
 
56
        
 
57
        public void buildXMLQuery(TCTLAbstractProperty property, String queryName) {
 
58
                XMLQuery.append(startTag(XML_PROP) + queryInfo(queryName) + startTag(XML_FORMULA));
 
59
                property.accept(this, null);
 
60
                XMLQuery.append(endTag(XML_FORMULA) + endTag(XML_PROP));              
 
61
        }
 
62
        
 
63
        public String getFormatted() {
 
64
            XMLFormatter formatter = new XMLFormatter();
 
65
            return formatter.format(getStartTag() + XMLQuery.toString() + getEndTag());
 
66
        }
 
67
        
 
68
        public String getStartTag(){
 
69
            return startTag(XML_PROPSET + " " + XML_NS) + "\n";
 
70
        }
 
71
        
 
72
        public String getEndTag(){
 
73
            return endTag(XML_PROPSET) + "\n";
 
74
        }
 
75
        
 
76
        private String queryInfo(String queryName){
 
77
                String nameToPrint = (queryName == null) ? "Query Comment/Name Here" : queryName;
 
78
                return wrapInTag(nameToPrint, XML_PROPID) + wrapInTag(nameToPrint, XML_PROPDESC);
 
79
        }
 
80
        
 
81
        public void visit(TCTLAFNode afNode, Object context) {
 
82
                XMLQuery.append(startTag(XML_ALLPATHS) + startTag(XML_FINALLY));
 
83
                afNode.getProperty().accept(this, context);
 
84
                XMLQuery.append(endTag(XML_FINALLY) + endTag(XML_ALLPATHS));
 
85
        }
 
86
 
 
87
        public void visit(TCTLAGNode agNode, Object context) {
 
88
                XMLQuery.append(startTag(XML_ALLPATHS) + startTag(XML_GLOBALLY));
 
89
                agNode.getProperty().accept(this, context);
 
90
                XMLQuery.append(endTag(XML_GLOBALLY) + endTag(XML_ALLPATHS));
 
91
        }
 
92
        
 
93
        public void visit(TCTLAXNode axNode, Object context) {
 
94
                XMLQuery.append(startTag(XML_ALLPATHS) + startTag(XML_NEXT));
 
95
                axNode.getProperty().accept(this, context);
 
96
                XMLQuery.append(endTag(XML_NEXT) + endTag(XML_ALLPATHS));
 
97
        }
 
98
        
 
99
        public void visit(TCTLAUNode auNode, Object context) {
 
100
                XMLQuery.append(startTag(XML_ALLPATHS) + startTag(XML_UNTIL) + startTag(XML_BEFORE));
 
101
                auNode.getLeft().accept(this, context);
 
102
                XMLQuery.append(endTag(XML_BEFORE) + startTag(XML_REACH));
 
103
                auNode.getRight().accept(this, context);
 
104
                XMLQuery.append(endTag(XML_REACH) + endTag(XML_UNTIL) + endTag(XML_ALLPATHS));
 
105
        }
 
106
 
 
107
        public void visit(TCTLEFNode efNode, Object context) {
 
108
                XMLQuery.append(startTag(XML_EXISTSPATH) + startTag(XML_FINALLY));
 
109
                efNode.getProperty().accept(this, context);
 
110
                XMLQuery.append(endTag(XML_FINALLY) + endTag(XML_EXISTSPATH));
 
111
        }
 
112
 
 
113
        public void visit(TCTLEGNode egNode, Object context) {
 
114
                XMLQuery.append(startTag(XML_EXISTSPATH) + startTag(XML_GLOBALLY));
 
115
                egNode.getProperty().accept(this, context);
 
116
                XMLQuery.append(endTag(XML_GLOBALLY) + endTag(XML_EXISTSPATH));
 
117
        }
 
118
        
 
119
        public void visit(TCTLEXNode exNode, Object context) {
 
120
                XMLQuery.append(startTag(XML_EXISTSPATH) + startTag(XML_NEXT));
 
121
                exNode.getProperty().accept(this, context);
 
122
                XMLQuery.append(endTag(XML_NEXT) + endTag(XML_EXISTSPATH));
 
123
        }
 
124
        
 
125
        public void visit(TCTLEUNode euNode, Object context) {
 
126
                XMLQuery.append(startTag(XML_EXISTSPATH) + startTag(XML_UNTIL) + startTag(XML_BEFORE));
 
127
                euNode.getLeft().accept(this, context);
 
128
                XMLQuery.append(endTag(XML_BEFORE) + startTag(XML_REACH));
 
129
                euNode.getRight().accept(this, context);
 
130
                XMLQuery.append(endTag(XML_REACH) + endTag(XML_UNTIL) + endTag(XML_EXISTSPATH));
 
131
        }
 
132
        
 
133
        public void visit(TCTLPathToStateConverter pathConverter, Object context) {
 
134
                pathConverter.getProperty().accept(this, context);
 
135
        }
 
136
 
 
137
        public void visit(TCTLAndListNode andListNode, Object context) {
 
138
                createList(andListNode.getProperties(), context, XML_CONJUNCTION);
 
139
        }
 
140
        
 
141
        public void visit(TCTLOrListNode orListNode, Object context) {
 
142
                createList(orListNode.getProperties(), context, XML_DISJUNCTION);
 
143
        }
 
144
 
 
145
        public void visit(TCTLTermListNode termListNode, Object context) {
 
146
                assert termListNode.getProperties().get(1) instanceof AritmeticOperator;
 
147
                AritmeticOperator operator = (AritmeticOperator)termListNode.getProperties().get(1);
 
148
                String op = operator.toString();
 
149
                if (op.equals("+")) {
 
150
                    createList(termListNode.getProperties(), context, XML_INTEGERSUM);
 
151
                } else if (op.equals("*")) {
 
152
                    createList(termListNode.getProperties(), context, XML_INTEGERPRODUCT);
 
153
                } else if (op.equals("-")) {
 
154
                    createList(termListNode.getProperties(), context, XML_INTEGERDIFFERENCE);
 
155
                }
 
156
        }
 
157
 
 
158
        private void createList(List<TCTLAbstractStateProperty> properties, Object context, String seperator) {
 
159
                XMLQuery.append(startTag(seperator));
 
160
 
 
161
                for (TCTLAbstractStateProperty p : properties) {
 
162
                        p.accept(this, context);
 
163
                }
 
164
 
 
165
                XMLQuery.append(endTag(seperator));
 
166
        }
 
167
 
 
168
        public void visit(TCTLNotNode notNode, Object context) {
 
169
                XMLQuery.append(startTag(XML_NEGATION));
 
170
                notNode.getProperty().accept(this, context);
 
171
                XMLQuery.append(endTag(XML_NEGATION));
 
172
        }
 
173
        
 
174
        public void visit(TCTLTrueNode tctlTrueNode, Object context) {          
 
175
                XMLQuery.append(emptyElement(XML_TRUE));
 
176
        }
 
177
        
 
178
        public void visit(TCTLFalseNode tctlFalseNode, Object context) {
 
179
                XMLQuery.append(emptyElement(XML_FALSE));
 
180
        }
 
181
        
 
182
        public void visit(TCTLDeadlockNode tctlDeadLockNode, Object context) {
 
183
                XMLQuery.append(emptyElement(XML_DEADLOCK));
 
184
        }
 
185
        
 
186
        public void visit(TCTLConstNode tctlConstNode, Object context){
 
187
                XMLQuery.append(wrapInTag(String.valueOf(tctlConstNode.getConstant()) + "", XML_INTEGERCONSTANT));
 
188
        }
 
189
 
 
190
        public void visit(TCTLPlaceNode tctlPlaceNode, Object context){
 
191
                XMLQuery.append(startTag(XML_TOKENSCOUNT));
 
192
                XMLQuery.append(wrapInTag(tctlPlaceNode.toString() + "", XML_PLACE));
 
193
                XMLQuery.append(endTag(XML_TOKENSCOUNT));
 
194
        }
 
195
 
 
196
        public void visit(TCTLTransitionNode tctlTransitionNode, Object context){               
 
197
                XMLQuery.append(startTag(XML_ISFIREABLE));
 
198
                XMLQuery.append(wrapInTag(tctlTransitionNode.toString() + "", XML_TRANSITION));
 
199
                XMLQuery.append(endTag(XML_ISFIREABLE));
 
200
        }
 
201
        
 
202
        @Override
 
203
        public void visit(TCTLAtomicPropositionNode atomicPropositionNode,
 
204
                        Object context) {
 
205
                String opTest = atomicPropositionNode.getOp();
 
206
                String op = new String();
 
207
                
 
208
                if (opTest.equals("<")){
 
209
                        op = XML_INTEGERLT;
 
210
                } else if(opTest.equals("<=")){
 
211
                        op = XML_INTEGERLE;
 
212
                } else if(opTest.equals("=")){
 
213
                        op = XML_INTEGEREQ;
 
214
                } else if(opTest.equals("!=")){
 
215
                        op = XML_INTEGERNE;
 
216
                } else if(opTest.equals(">")){
 
217
                        op = XML_INTEGERGT;
 
218
                } else if(opTest.equals(">=")){
 
219
                        op = XML_INTEGERGE;
 
220
                } else {
 
221
                        op = "MISSING_OPERATOR";
 
222
                }
 
223
                
 
224
                XMLQuery.append(startTag(op));
 
225
                atomicPropositionNode.getLeft().accept(this, context);
 
226
                atomicPropositionNode.getRight().accept(this, context);
 
227
                XMLQuery.append(endTag(op));
 
228
        }
 
229
        
 
230
        private String wrapInTag(String str, String tag){
 
231
                return startTag(tag) + str + endTag(tag);
 
232
        }
 
233
        private String startTag(String tag){
 
234
                return "<" + tag + ">";
 
235
        }
 
236
        private String endTag(String tag){
 
237
                return "</" + tag + ">";
 
238
        }
 
239
        private String emptyElement(String tag){
 
240
                return startTag(tag + "/");
 
241
        }       
 
242
}