Merge lp:~tapaal-contributor/tapaal/manual-edit-parsing into lp:tapaal
- manual-edit-parsing
- Merge into trunk
Status: | Superseded |
---|---|
Proposed branch: | lp:~tapaal-contributor/tapaal/manual-edit-parsing |
Merge into: | lp:tapaal |
Diff against target: |
2979 lines (+1487/-1310) (has conflicts) 6 files modified
src/dk/aau/cs/TCTL/CTLParsing/TAPAALCTLQueryParser.java (+756/-682) src/dk/aau/cs/TCTL/Parsing/TAPAALQueryParser.java (+665/-597) src/dk/aau/cs/TCTL/TCTLEFNode.java (+2/-1) src/pipe/gui/widgets/QueryDialog.java (+42/-28) src/resources/TCTLParser/TAPAALCTLQueryParser.jj (+11/-1) src/resources/TCTLParser/TAPAALQueryParser.jj (+11/-1) Text conflict in src/pipe/gui/widgets/QueryDialog.java |
To merge this branch: | bzr merge lp:~tapaal-contributor/tapaal/manual-edit-parsing |
Related bugs: |
Reviewer | Review Type | Date Requested | Status |
---|---|---|---|
Jiri Srba | Needs Fixing | ||
Kenneth Yrke Jørgensen | code | Approve | |
Review via email: mp+408607@code.launchpad.net |
This proposal supersedes a proposal from 2021-08-18.
This proposal has been superseded by a proposal from 2021-09-29.
Commit message
Ensures that everything in the query is parsed
Description of the change
Added an EOF check, to ensure that we parse everything from the query.
Before it would incorrectly accept a query such as "AF TAPN1.P0 = 0 jkdnj" by ignoring the last part of the query and it would return "AF TAPN1.P0 = 0".
Also fixed incorrect logic for checking whether the identifiers for the places and transitions included in the query existed in the net.
Jiri Srba (srba) wrote : Posted in a previous version of this proposal | # |
Lena Ernstsen (lsaid) wrote : | # |
The problem that is being fixed is ensuring that we parse everything from the query.
Before it would incorrectly accept a query such as "AF TAPN1.P0 = 0 jkdnj" by ignoring the last part of the query and it would return "AF TAPN1.P0 = 0".
Kenneth Yrke Jørgensen (yrke) : | # |
Jiri Srba (srba) wrote : | # |
Almost works, two small issues:
1. the text in case an unknown place/transition name is used says "... transitionswere used ..."
so there is missing a space (separator)
2. if you misspell place name in a query, it show the name correctly, however, for misspelled transitions, it does not show the transition name (the list is empty)
- 1140. By Lena Ernstsen
-
Fixed spacing and missing transition names in manual edit error message
- 1141. By Lena Ernstsen
-
Merged trunk
Unmerged revisions
Preview Diff
1 | === modified file 'src/dk/aau/cs/TCTL/CTLParsing/TAPAALCTLQueryParser.java' |
2 | --- src/dk/aau/cs/TCTL/CTLParsing/TAPAALCTLQueryParser.java 2019-03-22 10:13:18 +0000 |
3 | +++ src/dk/aau/cs/TCTL/CTLParsing/TAPAALCTLQueryParser.java 2021-09-29 07:20:55 +0000 |
4 | @@ -1,3 +1,4 @@ |
5 | +/* TAPAALCTLQueryParser.java */ |
6 | /* Generated By:JavaCC: Do not edit this line. TAPAALCTLQueryParser.java */ |
7 | package dk.aau.cs.TCTL.CTLParsing; |
8 | |
9 | @@ -13,6 +14,7 @@ |
10 | import dk.aau.cs.TCTL.TCTLAGNode; |
11 | import dk.aau.cs.TCTL.TCTLAUNode; |
12 | import dk.aau.cs.TCTL.TCTLAXNode; |
13 | +import dk.aau.cs.TCTL.TCTLAbstractProperty; |
14 | import dk.aau.cs.TCTL.TCTLAbstractStateProperty; |
15 | import dk.aau.cs.TCTL.TCTLAbstractPathProperty; |
16 | import dk.aau.cs.TCTL.TCTLAndListNode; |
17 | @@ -31,714 +33,786 @@ |
18 | |
19 | public class TAPAALCTLQueryParser implements TAPAALCTLQueryParserConstants { |
20 | |
21 | - private static final String ERROR_PARSING_QUERY_MESSAGE = "TAPAAL countered an error trying to parse the query"; |
22 | - |
23 | - public static TCTLAbstractPathProperty parse(String query) throws ParseException { |
24 | - TAPAALCTLQueryParser parser = new TAPAALCTLQueryParser(new StringReader(query)); |
25 | - return parser.AbstractPathProperty(); |
26 | - } |
27 | - |
28 | -/** Root production. */ |
29 | - final public TCTLAbstractPathProperty AbstractPathProperty() throws ParseException { |
30 | - TCTLAbstractStateProperty child = null; |
31 | + private static final String ERROR_PARSING_QUERY_MESSAGE = "TAPAAL countered an error trying to parse the query"; |
32 | + |
33 | + public static TCTLAbstractPathProperty parse(String query) throws ParseException { |
34 | + TAPAALCTLQueryParser parser = new TAPAALCTLQueryParser(new StringReader(query)); |
35 | + return parser.Start(); |
36 | + } |
37 | + |
38 | + /** Root production. */ |
39 | + final public TCTLAbstractPathProperty Start() throws ParseException {TCTLAbstractPathProperty child = null; |
40 | + child = AbstractPathProperty(); |
41 | + jj_consume_token(0); |
42 | + {if ("" != null) return child;} |
43 | + throw new Error("Missing return statement in function"); |
44 | + } |
45 | + |
46 | + final public TCTLAbstractPathProperty AbstractPathProperty() throws ParseException {TCTLAbstractStateProperty child = null; |
47 | TCTLAbstractStateProperty child2 = null; |
48 | - switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { |
49 | - case EF: |
50 | - jj_consume_token(EF); |
51 | - child = OrExpr(); |
52 | - {if (true) return new TCTLEFNode(child);} |
53 | - break; |
54 | - case EG: |
55 | - jj_consume_token(EG); |
56 | - child = OrExpr(); |
57 | - {if (true) return new TCTLEGNode(child);} |
58 | - break; |
59 | - case EX: |
60 | - jj_consume_token(EX); |
61 | - child = OrExpr(); |
62 | - {if (true) return new TCTLEXNode(child);} |
63 | - break; |
64 | - case E: |
65 | - jj_consume_token(E); |
66 | - jj_consume_token(26); |
67 | - child = OrExpr(); |
68 | - jj_consume_token(U); |
69 | - child2 = OrExpr(); |
70 | - jj_consume_token(27); |
71 | - {if (true) return new TCTLEUNode(child, child2);} |
72 | - break; |
73 | - case AF: |
74 | - jj_consume_token(AF); |
75 | - child = OrExpr(); |
76 | - {if (true) return new TCTLAFNode(child);} |
77 | - break; |
78 | - case AG: |
79 | - jj_consume_token(AG); |
80 | - child = OrExpr(); |
81 | - {if (true) return new TCTLAGNode(child);} |
82 | - break; |
83 | - case A: |
84 | - jj_consume_token(A); |
85 | - jj_consume_token(26); |
86 | - child = OrExpr(); |
87 | - jj_consume_token(U); |
88 | - child2 = OrExpr(); |
89 | - jj_consume_token(27); |
90 | - {if (true) return new TCTLAUNode(child, child2);} |
91 | - break; |
92 | - case AX: |
93 | - jj_consume_token(AX); |
94 | - child = OrExpr(); |
95 | - {if (true) return new TCTLAXNode(child);} |
96 | - break; |
97 | - default: |
98 | - jj_la1[0] = jj_gen; |
99 | - child = OrExpr(); |
100 | - {if (true) return new TCTLStateToPathConverter(child);} |
101 | + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { |
102 | + case EF:{ |
103 | + jj_consume_token(EF); |
104 | + child = OrExpr(); |
105 | + {if ("" != null) return new TCTLEFNode(child);} |
106 | + break; |
107 | + } |
108 | + case EG:{ |
109 | + jj_consume_token(EG); |
110 | + child = OrExpr(); |
111 | + {if ("" != null) return new TCTLEGNode(child);} |
112 | + break; |
113 | + } |
114 | + case EX:{ |
115 | + jj_consume_token(EX); |
116 | + child = OrExpr(); |
117 | + {if ("" != null) return new TCTLEXNode(child);} |
118 | + break; |
119 | + } |
120 | + case E:{ |
121 | + jj_consume_token(E); |
122 | + jj_consume_token(26); |
123 | + child = OrExpr(); |
124 | + jj_consume_token(U); |
125 | + child2 = OrExpr(); |
126 | + jj_consume_token(27); |
127 | + {if ("" != null) return new TCTLEUNode(child, child2);} |
128 | + break; |
129 | + } |
130 | + case AF:{ |
131 | + jj_consume_token(AF); |
132 | + child = OrExpr(); |
133 | + {if ("" != null) return new TCTLAFNode(child);} |
134 | + break; |
135 | + } |
136 | + case AG:{ |
137 | + jj_consume_token(AG); |
138 | + child = OrExpr(); |
139 | + {if ("" != null) return new TCTLAGNode(child);} |
140 | + break; |
141 | + } |
142 | + case A:{ |
143 | + jj_consume_token(A); |
144 | + jj_consume_token(26); |
145 | + child = OrExpr(); |
146 | + jj_consume_token(U); |
147 | + child2 = OrExpr(); |
148 | + jj_consume_token(27); |
149 | + {if ("" != null) return new TCTLAUNode(child, child2);} |
150 | + break; |
151 | + } |
152 | + case AX:{ |
153 | + jj_consume_token(AX); |
154 | + child = OrExpr(); |
155 | + {if ("" != null) return new TCTLAXNode(child);} |
156 | + break; |
157 | + } |
158 | + default: |
159 | + jj_la1[0] = jj_gen; |
160 | + child = OrExpr(); |
161 | + {if ("" != null) return new TCTLStateToPathConverter(child);} |
162 | + } |
163 | + throw new Error("Missing return statement in function"); |
164 | } |
165 | - throw new Error("Missing return statement in function"); |
166 | - } |
167 | |
168 | - final public TCTLAbstractStateProperty OrExpr() throws ParseException { |
169 | - TCTLAbstractStateProperty currentChild; |
170 | + final public TCTLAbstractStateProperty OrExpr() throws ParseException {TCTLAbstractStateProperty currentChild; |
171 | ArrayList<TCTLAbstractStateProperty> disjunctions = new ArrayList<TCTLAbstractStateProperty>(); |
172 | - currentChild = AndExpr(); |
173 | - disjunctions.add(currentChild); |
174 | - label_1: |
175 | - while (true) { |
176 | - switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { |
177 | - case OR: |
178 | - ; |
179 | - break; |
180 | - default: |
181 | - jj_la1[1] = jj_gen; |
182 | - break label_1; |
183 | - } |
184 | - jj_consume_token(OR); |
185 | - currentChild = AndExpr(); |
186 | - disjunctions.add(currentChild); |
187 | + currentChild = AndExpr(); |
188 | + disjunctions.add(currentChild); |
189 | + label_1: |
190 | + while (true) { |
191 | + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { |
192 | + case OR:{ |
193 | + ; |
194 | + break; |
195 | + } |
196 | + default: |
197 | + jj_la1[1] = jj_gen; |
198 | + break label_1; |
199 | + } |
200 | + jj_consume_token(OR); |
201 | + currentChild = AndExpr(); |
202 | + disjunctions.add(currentChild); |
203 | + } |
204 | + {if ("" != null) return disjunctions.size() == 1 ? currentChild : new TCTLOrListNode(disjunctions);} |
205 | + throw new Error("Missing return statement in function"); |
206 | } |
207 | - {if (true) return disjunctions.size() == 1 ? currentChild : new TCTLOrListNode(disjunctions);} |
208 | - throw new Error("Missing return statement in function"); |
209 | - } |
210 | |
211 | - final public TCTLAbstractStateProperty AndExpr() throws ParseException { |
212 | - TCTLAbstractStateProperty currentChild; |
213 | + final public TCTLAbstractStateProperty AndExpr() throws ParseException {TCTLAbstractStateProperty currentChild; |
214 | ArrayList<TCTLAbstractStateProperty> conjunctions = new ArrayList<TCTLAbstractStateProperty>(); |
215 | - currentChild = NotExpr(); |
216 | - conjunctions.add(currentChild); |
217 | - label_2: |
218 | - while (true) { |
219 | - switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { |
220 | - case AND: |
221 | - ; |
222 | - break; |
223 | - default: |
224 | - jj_la1[2] = jj_gen; |
225 | - break label_2; |
226 | - } |
227 | - jj_consume_token(AND); |
228 | - currentChild = NotExpr(); |
229 | - conjunctions.add(currentChild); |
230 | + currentChild = NotExpr(); |
231 | + conjunctions.add(currentChild); |
232 | + label_2: |
233 | + while (true) { |
234 | + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { |
235 | + case AND:{ |
236 | + ; |
237 | + break; |
238 | + } |
239 | + default: |
240 | + jj_la1[2] = jj_gen; |
241 | + break label_2; |
242 | + } |
243 | + jj_consume_token(AND); |
244 | + currentChild = NotExpr(); |
245 | + conjunctions.add(currentChild); |
246 | + } |
247 | + {if ("" != null) return conjunctions.size() == 1 ? currentChild : new TCTLAndListNode(conjunctions);} |
248 | + throw new Error("Missing return statement in function"); |
249 | } |
250 | - {if (true) return conjunctions.size() == 1 ? currentChild : new TCTLAndListNode(conjunctions);} |
251 | - throw new Error("Missing return statement in function"); |
252 | - } |
253 | |
254 | - final public TCTLAbstractStateProperty NotExpr() throws ParseException { |
255 | - TCTLAbstractStateProperty child; |
256 | + final public TCTLAbstractStateProperty NotExpr() throws ParseException {TCTLAbstractStateProperty child; |
257 | TCTLAbstractPathProperty childConverter; |
258 | - switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { |
259 | - case NOT: |
260 | - jj_consume_token(NOT); |
261 | - jj_consume_token(26); |
262 | - child = OrExpr(); |
263 | - jj_consume_token(27); |
264 | - {if (true) return new TCTLNotNode(child);} |
265 | - break; |
266 | - default: |
267 | - jj_la1[3] = jj_gen; |
268 | - child = Factor(); |
269 | - {if (true) return child;} |
270 | + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { |
271 | + case NOT:{ |
272 | + jj_consume_token(NOT); |
273 | + jj_consume_token(26); |
274 | + child = OrExpr(); |
275 | + jj_consume_token(27); |
276 | + {if ("" != null) return new TCTLNotNode(child);} |
277 | + break; |
278 | + } |
279 | + default: |
280 | + jj_la1[3] = jj_gen; |
281 | + child = Factor(); |
282 | + {if ("" != null) return child;} |
283 | + } |
284 | + throw new Error("Missing return statement in function"); |
285 | } |
286 | - throw new Error("Missing return statement in function"); |
287 | - } |
288 | |
289 | - final public TCTLAbstractStateProperty Factor() throws ParseException { |
290 | - TCTLAbstractStateProperty thisProp; |
291 | + final public TCTLAbstractStateProperty Factor() throws ParseException {TCTLAbstractStateProperty thisProp; |
292 | Token temp = null; |
293 | Token transition; |
294 | - switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { |
295 | - case TRUE: |
296 | - jj_consume_token(TRUE); |
297 | - thisProp = new TCTLTrueNode(); |
298 | - break; |
299 | - case FALSE: |
300 | - jj_consume_token(FALSE); |
301 | - thisProp = new TCTLFalseNode(); |
302 | - break; |
303 | - case DEADLOCK: |
304 | - jj_consume_token(DEADLOCK); |
305 | - thisProp = new TCTLDeadlockNode(); |
306 | - break; |
307 | - default: |
308 | - jj_la1[4] = jj_gen; |
309 | - if (jj_2_2(2147483647)) { |
310 | - thisProp = AtomicProposition(); |
311 | - } else { |
312 | - switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { |
313 | - case IDENT: |
314 | - if (jj_2_1(2)) { |
315 | - temp = jj_consume_token(IDENT); |
316 | - jj_consume_token(28); |
317 | - } else { |
318 | - ; |
319 | - } |
320 | - transition = jj_consume_token(IDENT); |
321 | - thisProp = new TCTLTransitionNode(temp == null ? "" : temp.image, transition.image); |
322 | - break; |
323 | - case 26: |
324 | - jj_consume_token(26); |
325 | - thisProp = OrExpr(); |
326 | - jj_consume_token(27); |
327 | - break; |
328 | - default: |
329 | - jj_la1[5] = jj_gen; |
330 | - thisProp = new TCTLPathToStateConverter(AbstractPathProperty()); |
331 | + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { |
332 | + case TRUE:{ |
333 | + jj_consume_token(TRUE); |
334 | + thisProp = new TCTLTrueNode(); |
335 | + break; |
336 | + } |
337 | + case FALSE:{ |
338 | + jj_consume_token(FALSE); |
339 | + thisProp = new TCTLFalseNode(); |
340 | + break; |
341 | + } |
342 | + case DEADLOCK:{ |
343 | + jj_consume_token(DEADLOCK); |
344 | + thisProp = new TCTLDeadlockNode(); |
345 | + break; |
346 | + } |
347 | + default: |
348 | + jj_la1[4] = jj_gen; |
349 | + if (jj_2_2(2147483647)) { |
350 | + thisProp = AtomicProposition(); |
351 | + } else { |
352 | + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { |
353 | + case IDENT:{ |
354 | + if (jj_2_1(2)) { |
355 | + temp = jj_consume_token(IDENT); |
356 | + jj_consume_token(28); |
357 | + } else { |
358 | + ; |
359 | + } |
360 | + transition = jj_consume_token(IDENT); |
361 | + thisProp = new TCTLTransitionNode(temp == null ? "" : temp.image, transition.image); |
362 | + break; |
363 | + } |
364 | + case 26:{ |
365 | + jj_consume_token(26); |
366 | + thisProp = OrExpr(); |
367 | + jj_consume_token(27); |
368 | + break; |
369 | + } |
370 | + default: |
371 | + jj_la1[5] = jj_gen; |
372 | + thisProp = new TCTLPathToStateConverter(AbstractPathProperty()); |
373 | + } |
374 | + } |
375 | } |
376 | - } |
377 | + {if ("" != null) return thisProp;} |
378 | + throw new Error("Missing return statement in function"); |
379 | } |
380 | - {if (true) return thisProp;} |
381 | - throw new Error("Missing return statement in function"); |
382 | - } |
383 | |
384 | - final public TCTLAbstractStateProperty AtomicProposition() throws ParseException { |
385 | - TCTLAbstractStateProperty left; |
386 | + final public TCTLAbstractStateProperty AtomicProposition() throws ParseException {TCTLAbstractStateProperty left; |
387 | TCTLAbstractStateProperty right; |
388 | Token op; |
389 | - left = AritmeticExpr(); |
390 | - op = jj_consume_token(OP); |
391 | - right = AritmeticExpr(); |
392 | - {if (true) return new TCTLAtomicPropositionNode(left, op.image, right);} |
393 | - throw new Error("Missing return statement in function"); |
394 | - } |
395 | - |
396 | - final public TCTLAbstractStateProperty AritmeticExpr() throws ParseException { |
397 | - TCTLAbstractStateProperty currentChild; |
398 | - ArrayList<TCTLAbstractStateProperty> terms = new ArrayList<TCTLAbstractStateProperty>(); |
399 | - Token op; |
400 | - currentChild = AritmeticMinusExpr(); |
401 | - terms.add(currentChild); |
402 | - label_3: |
403 | - while (true) { |
404 | - switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { |
405 | - case PLUS: |
406 | - ; |
407 | - break; |
408 | - default: |
409 | - jj_la1[6] = jj_gen; |
410 | - break label_3; |
411 | - } |
412 | - op = jj_consume_token(PLUS); |
413 | - currentChild = AritmeticMinusExpr(); |
414 | - terms.add(new AritmeticOperator(op.image)); |
415 | - terms.add(currentChild); |
416 | - } |
417 | - {if (true) return terms.size() == 1 ? currentChild : new TCTLTermListNode(terms);} |
418 | - throw new Error("Missing return statement in function"); |
419 | - } |
420 | - |
421 | - final public TCTLAbstractStateProperty AritmeticMinusExpr() throws ParseException { |
422 | - TCTLAbstractStateProperty currentChild; |
423 | - ArrayList<TCTLAbstractStateProperty> terms = new ArrayList<TCTLAbstractStateProperty>(); |
424 | - Token op; |
425 | - currentChild = AritmeticTerm(); |
426 | - terms.add(currentChild); |
427 | - label_4: |
428 | - while (true) { |
429 | - switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { |
430 | - case MINUS: |
431 | - ; |
432 | - break; |
433 | - default: |
434 | - jj_la1[7] = jj_gen; |
435 | - break label_4; |
436 | - } |
437 | - op = jj_consume_token(MINUS); |
438 | - currentChild = AritmeticTerm(); |
439 | - terms.add(new AritmeticOperator(op.image)); |
440 | - terms.add(currentChild); |
441 | - } |
442 | - {if (true) return terms.size() == 1 ? currentChild : new TCTLTermListNode(terms);} |
443 | - throw new Error("Missing return statement in function"); |
444 | - } |
445 | - |
446 | - final public TCTLAbstractStateProperty AritmeticTerm() throws ParseException { |
447 | - TCTLAbstractStateProperty currentChild; |
448 | + left = AritmeticExpr(); |
449 | + op = jj_consume_token(OP); |
450 | + right = AritmeticExpr(); |
451 | + {if ("" != null) return new TCTLAtomicPropositionNode(left, op.image, right);} |
452 | + throw new Error("Missing return statement in function"); |
453 | + } |
454 | + |
455 | + final public TCTLAbstractStateProperty AritmeticExpr() throws ParseException {TCTLAbstractStateProperty currentChild; |
456 | + ArrayList<TCTLAbstractStateProperty> terms = new ArrayList<TCTLAbstractStateProperty>(); |
457 | + Token op; |
458 | + currentChild = AritmeticMinusExpr(); |
459 | + terms.add(currentChild); |
460 | + label_3: |
461 | + while (true) { |
462 | + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { |
463 | + case PLUS:{ |
464 | + ; |
465 | + break; |
466 | + } |
467 | + default: |
468 | + jj_la1[6] = jj_gen; |
469 | + break label_3; |
470 | + } |
471 | + op = jj_consume_token(PLUS); |
472 | + currentChild = AritmeticMinusExpr(); |
473 | + terms.add(new AritmeticOperator(op.image)); |
474 | + terms.add(currentChild); |
475 | + } |
476 | + {if ("" != null) return terms.size() == 1 ? currentChild : new TCTLTermListNode(terms);} |
477 | + throw new Error("Missing return statement in function"); |
478 | + } |
479 | + |
480 | + final public TCTLAbstractStateProperty AritmeticMinusExpr() throws ParseException {TCTLAbstractStateProperty currentChild; |
481 | + ArrayList<TCTLAbstractStateProperty> terms = new ArrayList<TCTLAbstractStateProperty>(); |
482 | + Token op; |
483 | + currentChild = AritmeticTerm(); |
484 | + terms.add(currentChild); |
485 | + label_4: |
486 | + while (true) { |
487 | + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { |
488 | + case MINUS:{ |
489 | + ; |
490 | + break; |
491 | + } |
492 | + default: |
493 | + jj_la1[7] = jj_gen; |
494 | + break label_4; |
495 | + } |
496 | + op = jj_consume_token(MINUS); |
497 | + currentChild = AritmeticTerm(); |
498 | + terms.add(new AritmeticOperator(op.image)); |
499 | + terms.add(currentChild); |
500 | + } |
501 | + {if ("" != null) return terms.size() == 1 ? currentChild : new TCTLTermListNode(terms);} |
502 | + throw new Error("Missing return statement in function"); |
503 | + } |
504 | + |
505 | + final public TCTLAbstractStateProperty AritmeticTerm() throws ParseException {TCTLAbstractStateProperty currentChild; |
506 | ArrayList<TCTLAbstractStateProperty> factors = new ArrayList<TCTLAbstractStateProperty>(); |
507 | Token op; |
508 | - currentChild = AritmeticFactor(); |
509 | - factors.add(currentChild); |
510 | - label_5: |
511 | - while (true) { |
512 | - switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { |
513 | - case MULT: |
514 | - ; |
515 | - break; |
516 | - default: |
517 | - jj_la1[8] = jj_gen; |
518 | - break label_5; |
519 | - } |
520 | - op = jj_consume_token(MULT); |
521 | - currentChild = AritmeticFactor(); |
522 | - factors.add(new AritmeticOperator(op.image)); |
523 | - factors.add(currentChild); |
524 | + currentChild = AritmeticFactor(); |
525 | + factors.add(currentChild); |
526 | + label_5: |
527 | + while (true) { |
528 | + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { |
529 | + case MULT:{ |
530 | + ; |
531 | + break; |
532 | + } |
533 | + default: |
534 | + jj_la1[8] = jj_gen; |
535 | + break label_5; |
536 | + } |
537 | + op = jj_consume_token(MULT); |
538 | + currentChild = AritmeticFactor(); |
539 | + factors.add(new AritmeticOperator(op.image)); |
540 | + factors.add(currentChild); |
541 | + } |
542 | + {if ("" != null) return factors.size() == 1 ? currentChild : new TCTLTermListNode(factors);} |
543 | + throw new Error("Missing return statement in function"); |
544 | } |
545 | - {if (true) return factors.size() == 1 ? currentChild : new TCTLTermListNode(factors);} |
546 | - throw new Error("Missing return statement in function"); |
547 | - } |
548 | |
549 | - final public TCTLAbstractStateProperty AritmeticFactor() throws ParseException { |
550 | - TCTLAbstractStateProperty thisProp; |
551 | + final public TCTLAbstractStateProperty AritmeticFactor() throws ParseException {TCTLAbstractStateProperty thisProp; |
552 | Token temp = null; |
553 | Token place; |
554 | Token op; |
555 | Token num; |
556 | - switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { |
557 | - case IDENT: |
558 | - if (jj_2_3(2)) { |
559 | - temp = jj_consume_token(IDENT); |
560 | - jj_consume_token(28); |
561 | - } else { |
562 | - ; |
563 | - } |
564 | - place = jj_consume_token(IDENT); |
565 | - thisProp = new TCTLPlaceNode(temp == null ? "" : temp.image, place.image); |
566 | - break; |
567 | - case NUM: |
568 | - num = jj_consume_token(NUM); |
569 | - thisProp = new TCTLConstNode(Integer.parseInt(num.image)); |
570 | - break; |
571 | - case 26: |
572 | - jj_consume_token(26); |
573 | - thisProp = AritmeticExpr(); |
574 | - jj_consume_token(27); |
575 | - break; |
576 | - default: |
577 | - jj_la1[9] = jj_gen; |
578 | - jj_consume_token(-1); |
579 | - throw new ParseException(); |
580 | - } |
581 | - {if (true) return thisProp;} |
582 | - throw new Error("Missing return statement in function"); |
583 | - } |
584 | - |
585 | - private boolean jj_2_1(int xla) { |
586 | - jj_la = xla; jj_lastpos = jj_scanpos = token; |
587 | - try { return !jj_3_1(); } |
588 | - catch(LookaheadSuccess ls) { return true; } |
589 | - finally { jj_save(0, xla); } |
590 | - } |
591 | - |
592 | - private boolean jj_2_2(int xla) { |
593 | - jj_la = xla; jj_lastpos = jj_scanpos = token; |
594 | - try { return !jj_3_2(); } |
595 | - catch(LookaheadSuccess ls) { return true; } |
596 | - finally { jj_save(1, xla); } |
597 | - } |
598 | - |
599 | - private boolean jj_2_3(int xla) { |
600 | - jj_la = xla; jj_lastpos = jj_scanpos = token; |
601 | - try { return !jj_3_3(); } |
602 | - catch(LookaheadSuccess ls) { return true; } |
603 | - finally { jj_save(2, xla); } |
604 | - } |
605 | - |
606 | - private boolean jj_3R_16() { |
607 | - if (jj_scan_token(26)) return true; |
608 | - if (jj_3R_7()) return true; |
609 | - if (jj_scan_token(27)) return true; |
610 | - return false; |
611 | - } |
612 | - |
613 | - private boolean jj_3R_13() { |
614 | - if (jj_scan_token(MULT)) return true; |
615 | - if (jj_3R_12()) return true; |
616 | - return false; |
617 | - } |
618 | - |
619 | - private boolean jj_3_1() { |
620 | - if (jj_scan_token(IDENT)) return true; |
621 | - if (jj_scan_token(28)) return true; |
622 | - return false; |
623 | - } |
624 | - |
625 | - private boolean jj_3R_15() { |
626 | - if (jj_scan_token(NUM)) return true; |
627 | - return false; |
628 | - } |
629 | - |
630 | - private boolean jj_3_3() { |
631 | - if (jj_scan_token(IDENT)) return true; |
632 | - if (jj_scan_token(28)) return true; |
633 | - return false; |
634 | - } |
635 | - |
636 | - private boolean jj_3R_7() { |
637 | - if (jj_3R_8()) return true; |
638 | - Token xsp; |
639 | - while (true) { |
640 | - xsp = jj_scanpos; |
641 | - if (jj_3R_9()) { jj_scanpos = xsp; break; } |
642 | - } |
643 | - return false; |
644 | - } |
645 | - |
646 | - private boolean jj_3R_14() { |
647 | - Token xsp; |
648 | - xsp = jj_scanpos; |
649 | - if (jj_3_3()) jj_scanpos = xsp; |
650 | - if (jj_scan_token(IDENT)) return true; |
651 | - return false; |
652 | - } |
653 | - |
654 | - private boolean jj_3R_8() { |
655 | - if (jj_3R_10()) return true; |
656 | - Token xsp; |
657 | - while (true) { |
658 | - xsp = jj_scanpos; |
659 | - if (jj_3R_11()) { jj_scanpos = xsp; break; } |
660 | - } |
661 | - return false; |
662 | - } |
663 | - |
664 | - private boolean jj_3R_10() { |
665 | - if (jj_3R_12()) return true; |
666 | - Token xsp; |
667 | - while (true) { |
668 | - xsp = jj_scanpos; |
669 | - if (jj_3R_13()) { jj_scanpos = xsp; break; } |
670 | - } |
671 | - return false; |
672 | - } |
673 | - |
674 | - private boolean jj_3R_12() { |
675 | - Token xsp; |
676 | - xsp = jj_scanpos; |
677 | - if (jj_3R_14()) { |
678 | - jj_scanpos = xsp; |
679 | - if (jj_3R_15()) { |
680 | - jj_scanpos = xsp; |
681 | - if (jj_3R_16()) return true; |
682 | - } |
683 | - } |
684 | - return false; |
685 | - } |
686 | - |
687 | - private boolean jj_3R_9() { |
688 | - if (jj_scan_token(PLUS)) return true; |
689 | - if (jj_3R_8()) return true; |
690 | - return false; |
691 | - } |
692 | - |
693 | - private boolean jj_3_2() { |
694 | - if (jj_3R_6()) return true; |
695 | - return false; |
696 | - } |
697 | - |
698 | - private boolean jj_3R_6() { |
699 | - if (jj_3R_7()) return true; |
700 | - if (jj_scan_token(OP)) return true; |
701 | - if (jj_3R_7()) return true; |
702 | - return false; |
703 | - } |
704 | - |
705 | - private boolean jj_3R_11() { |
706 | - if (jj_scan_token(MINUS)) return true; |
707 | - if (jj_3R_10()) return true; |
708 | - return false; |
709 | - } |
710 | - |
711 | - /** Generated Token Manager. */ |
712 | - public TAPAALCTLQueryParserTokenManager token_source; |
713 | - SimpleCharStream jj_input_stream; |
714 | - /** Current token. */ |
715 | - public Token token; |
716 | - /** Next token. */ |
717 | - public Token jj_nt; |
718 | - private int jj_ntk; |
719 | - private Token jj_scanpos, jj_lastpos; |
720 | - private int jj_la; |
721 | - private int jj_gen; |
722 | - final private int[] jj_la1 = new int[10]; |
723 | - static private int[] jj_la1_0; |
724 | - static { |
725 | - jj_la1_init_0(); |
726 | - } |
727 | - private static void jj_la1_init_0() { |
728 | - jj_la1_0 = new int[] {0x1ef0,0x2000,0x4000,0x8000,0xe,0x4100000,0x10000,0x20000,0x40000,0x4180000,}; |
729 | - } |
730 | - final private JJCalls[] jj_2_rtns = new JJCalls[3]; |
731 | - private boolean jj_rescan = false; |
732 | - private int jj_gc = 0; |
733 | - |
734 | - /** Constructor with InputStream. */ |
735 | - public TAPAALCTLQueryParser(java.io.InputStream stream) { |
736 | - this(stream, null); |
737 | - } |
738 | - /** Constructor with InputStream and supplied encoding */ |
739 | - public TAPAALCTLQueryParser(java.io.InputStream stream, String encoding) { |
740 | - try { jj_input_stream = new SimpleCharStream(stream, encoding, 1, 1); } catch(java.io.UnsupportedEncodingException e) { throw new RuntimeException(e); } |
741 | - token_source = new TAPAALCTLQueryParserTokenManager(jj_input_stream); |
742 | - token = new Token(); |
743 | - jj_ntk = -1; |
744 | - jj_gen = 0; |
745 | - for (int i = 0; i < 10; i++) jj_la1[i] = -1; |
746 | - for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); |
747 | - } |
748 | - |
749 | - /** Reinitialise. */ |
750 | - public void ReInit(java.io.InputStream stream) { |
751 | - ReInit(stream, null); |
752 | - } |
753 | - /** Reinitialise. */ |
754 | - public void ReInit(java.io.InputStream stream, String encoding) { |
755 | - try { jj_input_stream.ReInit(stream, encoding, 1, 1); } catch(java.io.UnsupportedEncodingException e) { throw new RuntimeException(e); } |
756 | - token_source.ReInit(jj_input_stream); |
757 | - token = new Token(); |
758 | - jj_ntk = -1; |
759 | - jj_gen = 0; |
760 | - for (int i = 0; i < 10; i++) jj_la1[i] = -1; |
761 | - for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); |
762 | - } |
763 | - |
764 | - /** Constructor. */ |
765 | - public TAPAALCTLQueryParser(java.io.Reader stream) { |
766 | - jj_input_stream = new SimpleCharStream(stream, 1, 1); |
767 | - token_source = new TAPAALCTLQueryParserTokenManager(jj_input_stream); |
768 | - token = new Token(); |
769 | - jj_ntk = -1; |
770 | - jj_gen = 0; |
771 | - for (int i = 0; i < 10; i++) jj_la1[i] = -1; |
772 | - for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); |
773 | - } |
774 | - |
775 | - /** Reinitialise. */ |
776 | - public void ReInit(java.io.Reader stream) { |
777 | - jj_input_stream.ReInit(stream, 1, 1); |
778 | - token_source.ReInit(jj_input_stream); |
779 | - token = new Token(); |
780 | - jj_ntk = -1; |
781 | - jj_gen = 0; |
782 | - for (int i = 0; i < 10; i++) jj_la1[i] = -1; |
783 | - for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); |
784 | - } |
785 | - |
786 | - /** Constructor with generated Token Manager. */ |
787 | - public TAPAALCTLQueryParser(TAPAALCTLQueryParserTokenManager tm) { |
788 | - token_source = tm; |
789 | - token = new Token(); |
790 | - jj_ntk = -1; |
791 | - jj_gen = 0; |
792 | - for (int i = 0; i < 10; i++) jj_la1[i] = -1; |
793 | - for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); |
794 | - } |
795 | - |
796 | - /** Reinitialise. */ |
797 | - public void ReInit(TAPAALCTLQueryParserTokenManager tm) { |
798 | - token_source = tm; |
799 | - token = new Token(); |
800 | - jj_ntk = -1; |
801 | - jj_gen = 0; |
802 | - for (int i = 0; i < 10; i++) jj_la1[i] = -1; |
803 | - for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); |
804 | - } |
805 | - |
806 | - private Token jj_consume_token(int kind) throws ParseException { |
807 | - Token oldToken; |
808 | - if ((oldToken = token).next != null) token = token.next; |
809 | - else token = token.next = token_source.getNextToken(); |
810 | - jj_ntk = -1; |
811 | - if (token.kind == kind) { |
812 | - jj_gen++; |
813 | - if (++jj_gc > 100) { |
814 | - jj_gc = 0; |
815 | - for (int i = 0; i < jj_2_rtns.length; i++) { |
816 | - JJCalls c = jj_2_rtns[i]; |
817 | - while (c != null) { |
818 | - if (c.gen < jj_gen) c.first = null; |
819 | - c = c.next; |
820 | - } |
821 | - } |
822 | - } |
823 | - return token; |
824 | - } |
825 | - token = oldToken; |
826 | - jj_kind = kind; |
827 | - throw generateParseException(); |
828 | - } |
829 | - |
830 | - static private final class LookaheadSuccess extends java.lang.Error { } |
831 | - final private LookaheadSuccess jj_ls = new LookaheadSuccess(); |
832 | - private boolean jj_scan_token(int kind) { |
833 | - if (jj_scanpos == jj_lastpos) { |
834 | - jj_la--; |
835 | - if (jj_scanpos.next == null) { |
836 | - jj_lastpos = jj_scanpos = jj_scanpos.next = token_source.getNextToken(); |
837 | - } else { |
838 | - jj_lastpos = jj_scanpos = jj_scanpos.next; |
839 | - } |
840 | - } else { |
841 | - jj_scanpos = jj_scanpos.next; |
842 | - } |
843 | - if (jj_rescan) { |
844 | - int i = 0; Token tok = token; |
845 | - while (tok != null && tok != jj_scanpos) { i++; tok = tok.next; } |
846 | - if (tok != null) jj_add_error_token(kind, i); |
847 | - } |
848 | - if (jj_scanpos.kind != kind) return true; |
849 | - if (jj_la == 0 && jj_scanpos == jj_lastpos) throw jj_ls; |
850 | - return false; |
851 | - } |
852 | - |
853 | - |
854 | -/** Get the next Token. */ |
855 | - final public Token getNextToken() { |
856 | - if (token.next != null) token = token.next; |
857 | - else token = token.next = token_source.getNextToken(); |
858 | - jj_ntk = -1; |
859 | - jj_gen++; |
860 | - return token; |
861 | - } |
862 | - |
863 | -/** Get the specific Token. */ |
864 | - final public Token getToken(int index) { |
865 | - Token t = token; |
866 | - for (int i = 0; i < index; i++) { |
867 | - if (t.next != null) t = t.next; |
868 | - else t = t.next = token_source.getNextToken(); |
869 | - } |
870 | - return t; |
871 | - } |
872 | - |
873 | - private int jj_ntk() { |
874 | - if ((jj_nt=token.next) == null) |
875 | - return (jj_ntk = (token.next=token_source.getNextToken()).kind); |
876 | - else |
877 | - return (jj_ntk = jj_nt.kind); |
878 | - } |
879 | - |
880 | - private java.util.List<int[]> jj_expentries = new java.util.ArrayList<int[]>(); |
881 | - private int[] jj_expentry; |
882 | - private int jj_kind = -1; |
883 | - private int[] jj_lasttokens = new int[100]; |
884 | - private int jj_endpos; |
885 | - |
886 | - private void jj_add_error_token(int kind, int pos) { |
887 | - if (pos >= 100) return; |
888 | - if (pos == jj_endpos + 1) { |
889 | - jj_lasttokens[jj_endpos++] = kind; |
890 | - } else if (jj_endpos != 0) { |
891 | - jj_expentry = new int[jj_endpos]; |
892 | - for (int i = 0; i < jj_endpos; i++) { |
893 | - jj_expentry[i] = jj_lasttokens[i]; |
894 | - } |
895 | - boolean exists = false; |
896 | - for (java.util.Iterator<?> it = jj_expentries.iterator(); it.hasNext();) { |
897 | - exists = true; |
898 | - int[] oldentry = (int[])(it.next()); |
899 | - if (oldentry.length == jj_expentry.length) { |
900 | - for (int i = 0; i < jj_expentry.length; i++) { |
901 | - if (oldentry[i] != jj_expentry[i]) { |
902 | - exists = false; |
903 | - break; |
904 | - } |
905 | - } |
906 | - if (exists) break; |
907 | - } |
908 | - } |
909 | - if (!exists) jj_expentries.add(jj_expentry); |
910 | - if (pos != 0) jj_lasttokens[(jj_endpos = pos) - 1] = kind; |
911 | - } |
912 | - } |
913 | - |
914 | - /** Generate ParseException. */ |
915 | - public ParseException generateParseException() { |
916 | - jj_expentries.clear(); |
917 | - boolean[] la1tokens = new boolean[29]; |
918 | - if (jj_kind >= 0) { |
919 | - la1tokens[jj_kind] = true; |
920 | - jj_kind = -1; |
921 | - } |
922 | - for (int i = 0; i < 10; i++) { |
923 | - if (jj_la1[i] == jj_gen) { |
924 | - for (int j = 0; j < 32; j++) { |
925 | - if ((jj_la1_0[i] & (1<<j)) != 0) { |
926 | - la1tokens[j] = true; |
927 | - } |
928 | - } |
929 | - } |
930 | - } |
931 | - for (int i = 0; i < 29; i++) { |
932 | - if (la1tokens[i]) { |
933 | - jj_expentry = new int[1]; |
934 | - jj_expentry[0] = i; |
935 | - jj_expentries.add(jj_expentry); |
936 | - } |
937 | - } |
938 | - jj_endpos = 0; |
939 | - jj_rescan_token(); |
940 | - jj_add_error_token(0, 0); |
941 | - int[][] exptokseq = new int[jj_expentries.size()][]; |
942 | - for (int i = 0; i < jj_expentries.size(); i++) { |
943 | - exptokseq[i] = jj_expentries.get(i); |
944 | - } |
945 | - return new ParseException(token, exptokseq, tokenImage); |
946 | - } |
947 | - |
948 | - /** Enable tracing. */ |
949 | - final public void enable_tracing() { |
950 | - } |
951 | - |
952 | - /** Disable tracing. */ |
953 | - final public void disable_tracing() { |
954 | - } |
955 | - |
956 | - private void jj_rescan_token() { |
957 | - jj_rescan = true; |
958 | - for (int i = 0; i < 3; i++) { |
959 | - try { |
960 | - JJCalls p = jj_2_rtns[i]; |
961 | - do { |
962 | - if (p.gen > jj_gen) { |
963 | - jj_la = p.arg; jj_lastpos = jj_scanpos = p.first; |
964 | - switch (i) { |
965 | - case 0: jj_3_1(); break; |
966 | - case 1: jj_3_2(); break; |
967 | - case 2: jj_3_3(); break; |
968 | - } |
969 | - } |
970 | - p = p.next; |
971 | - } while (p != null); |
972 | - } catch(LookaheadSuccess ls) { } |
973 | - } |
974 | - jj_rescan = false; |
975 | - } |
976 | - |
977 | - private void jj_save(int index, int xla) { |
978 | - JJCalls p = jj_2_rtns[index]; |
979 | - while (p.gen > jj_gen) { |
980 | - if (p.next == null) { p = p.next = new JJCalls(); break; } |
981 | - p = p.next; |
982 | - } |
983 | - p.gen = jj_gen + xla - jj_la; p.first = token; p.arg = xla; |
984 | - } |
985 | - |
986 | - static final class JJCalls { |
987 | - int gen; |
988 | - Token first; |
989 | - int arg; |
990 | - JJCalls next; |
991 | - } |
992 | + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { |
993 | + case IDENT:{ |
994 | + if (jj_2_3(2)) { |
995 | + temp = jj_consume_token(IDENT); |
996 | + jj_consume_token(28); |
997 | + } else { |
998 | + ; |
999 | + } |
1000 | + place = jj_consume_token(IDENT); |
1001 | + thisProp = new TCTLPlaceNode(temp == null ? "" : temp.image, place.image); |
1002 | + break; |
1003 | + } |
1004 | + case NUM:{ |
1005 | + num = jj_consume_token(NUM); |
1006 | + thisProp = new TCTLConstNode(Integer.parseInt(num.image)); |
1007 | + break; |
1008 | + } |
1009 | + case 26:{ |
1010 | + jj_consume_token(26); |
1011 | + thisProp = AritmeticExpr(); |
1012 | + jj_consume_token(27); |
1013 | + break; |
1014 | + } |
1015 | + default: |
1016 | + jj_la1[9] = jj_gen; |
1017 | + jj_consume_token(-1); |
1018 | + throw new ParseException(); |
1019 | + } |
1020 | + {if ("" != null) return thisProp;} |
1021 | + throw new Error("Missing return statement in function"); |
1022 | + } |
1023 | + |
1024 | + private boolean jj_2_1(int xla) |
1025 | + { |
1026 | + jj_la = xla; jj_lastpos = jj_scanpos = token; |
1027 | + try { return (!jj_3_1()); } |
1028 | + catch(LookaheadSuccess ls) { return true; } |
1029 | + finally { jj_save(0, xla); } |
1030 | + } |
1031 | + |
1032 | + private boolean jj_2_2(int xla) |
1033 | + { |
1034 | + jj_la = xla; jj_lastpos = jj_scanpos = token; |
1035 | + try { return (!jj_3_2()); } |
1036 | + catch(LookaheadSuccess ls) { return true; } |
1037 | + finally { jj_save(1, xla); } |
1038 | + } |
1039 | + |
1040 | + private boolean jj_2_3(int xla) |
1041 | + { |
1042 | + jj_la = xla; jj_lastpos = jj_scanpos = token; |
1043 | + try { return (!jj_3_3()); } |
1044 | + catch(LookaheadSuccess ls) { return true; } |
1045 | + finally { jj_save(2, xla); } |
1046 | + } |
1047 | + |
1048 | + private boolean jj_3R_AritmeticTerm_287_9_10() |
1049 | + { |
1050 | + if (jj_3R_AritmeticFactor_308_9_12()) return true; |
1051 | + Token xsp; |
1052 | + while (true) { |
1053 | + xsp = jj_scanpos; |
1054 | + if (jj_3R_AritmeticTerm_290_17_13()) { jj_scanpos = xsp; break; } |
1055 | + } |
1056 | + return false; |
1057 | + } |
1058 | + |
1059 | + private boolean jj_3R_AritmeticFactor_308_9_12() |
1060 | + { |
1061 | + Token xsp; |
1062 | + xsp = jj_scanpos; |
1063 | + if (jj_3R_AritmeticFactor_309_17_14()) { |
1064 | + jj_scanpos = xsp; |
1065 | + if (jj_3R_AritmeticFactor_310_19_15()) { |
1066 | + jj_scanpos = xsp; |
1067 | + if (jj_3R_AritmeticFactor_311_19_16()) return true; |
1068 | + } |
1069 | + } |
1070 | + return false; |
1071 | + } |
1072 | + |
1073 | + private boolean jj_3R_AritmeticExpr_252_17_9() |
1074 | + { |
1075 | + if (jj_scan_token(PLUS)) return true; |
1076 | + if (jj_3R_AritmeticMinusExpr_268_9_8()) return true; |
1077 | + return false; |
1078 | + } |
1079 | + |
1080 | + private boolean jj_3_2() |
1081 | + { |
1082 | + if (jj_3R_AtomicProposition_234_9_6()) return true; |
1083 | + return false; |
1084 | + } |
1085 | + |
1086 | + private boolean jj_3R_AtomicProposition_234_9_6() |
1087 | + { |
1088 | + if (jj_3R_AritmeticExpr_249_9_7()) return true; |
1089 | + if (jj_scan_token(OP)) return true; |
1090 | + if (jj_3R_AritmeticExpr_249_9_7()) return true; |
1091 | + return false; |
1092 | + } |
1093 | + |
1094 | + private boolean jj_3R_AritmeticMinusExpr_271_17_11() |
1095 | + { |
1096 | + if (jj_scan_token(MINUS)) return true; |
1097 | + if (jj_3R_AritmeticTerm_287_9_10()) return true; |
1098 | + return false; |
1099 | + } |
1100 | + |
1101 | + private boolean jj_3R_AritmeticFactor_311_19_16() |
1102 | + { |
1103 | + if (jj_scan_token(26)) return true; |
1104 | + if (jj_3R_AritmeticExpr_249_9_7()) return true; |
1105 | + if (jj_scan_token(27)) return true; |
1106 | + return false; |
1107 | + } |
1108 | + |
1109 | + private boolean jj_3R_AritmeticTerm_290_17_13() |
1110 | + { |
1111 | + if (jj_scan_token(MULT)) return true; |
1112 | + if (jj_3R_AritmeticFactor_308_9_12()) return true; |
1113 | + return false; |
1114 | + } |
1115 | + |
1116 | + private boolean jj_3_1() |
1117 | + { |
1118 | + if (jj_scan_token(IDENT)) return true; |
1119 | + if (jj_scan_token(28)) return true; |
1120 | + return false; |
1121 | + } |
1122 | + |
1123 | + private boolean jj_3R_AritmeticFactor_310_19_15() |
1124 | + { |
1125 | + if (jj_scan_token(NUM)) return true; |
1126 | + return false; |
1127 | + } |
1128 | + |
1129 | + private boolean jj_3_3() |
1130 | + { |
1131 | + if (jj_scan_token(IDENT)) return true; |
1132 | + if (jj_scan_token(28)) return true; |
1133 | + return false; |
1134 | + } |
1135 | + |
1136 | + private boolean jj_3R_AritmeticExpr_249_9_7() |
1137 | + { |
1138 | + if (jj_3R_AritmeticMinusExpr_268_9_8()) return true; |
1139 | + Token xsp; |
1140 | + while (true) { |
1141 | + xsp = jj_scanpos; |
1142 | + if (jj_3R_AritmeticExpr_252_17_9()) { jj_scanpos = xsp; break; } |
1143 | + } |
1144 | + return false; |
1145 | + } |
1146 | + |
1147 | + private boolean jj_3R_AritmeticFactor_309_17_14() |
1148 | + { |
1149 | + Token xsp; |
1150 | + xsp = jj_scanpos; |
1151 | + if (jj_3_3()) jj_scanpos = xsp; |
1152 | + if (jj_scan_token(IDENT)) return true; |
1153 | + return false; |
1154 | + } |
1155 | + |
1156 | + private boolean jj_3R_AritmeticMinusExpr_268_9_8() |
1157 | + { |
1158 | + if (jj_3R_AritmeticTerm_287_9_10()) return true; |
1159 | + Token xsp; |
1160 | + while (true) { |
1161 | + xsp = jj_scanpos; |
1162 | + if (jj_3R_AritmeticMinusExpr_271_17_11()) { jj_scanpos = xsp; break; } |
1163 | + } |
1164 | + return false; |
1165 | + } |
1166 | + |
1167 | + /** Generated Token Manager. */ |
1168 | + public TAPAALCTLQueryParserTokenManager token_source; |
1169 | + SimpleCharStream jj_input_stream; |
1170 | + /** Current token. */ |
1171 | + public Token token; |
1172 | + /** Next token. */ |
1173 | + public Token jj_nt; |
1174 | + private int jj_ntk; |
1175 | + private Token jj_scanpos, jj_lastpos; |
1176 | + private int jj_la; |
1177 | + private int jj_gen; |
1178 | + final private int[] jj_la1 = new int[10]; |
1179 | + static private int[] jj_la1_0; |
1180 | + static { |
1181 | + jj_la1_init_0(); |
1182 | + } |
1183 | + private static void jj_la1_init_0() { |
1184 | + jj_la1_0 = new int[] {0x1ef0,0x2000,0x4000,0x8000,0xe,0x4100000,0x10000,0x20000,0x40000,0x4180000,}; |
1185 | + } |
1186 | + final private JJCalls[] jj_2_rtns = new JJCalls[3]; |
1187 | + private boolean jj_rescan = false; |
1188 | + private int jj_gc = 0; |
1189 | + |
1190 | + /** Constructor with InputStream. */ |
1191 | + public TAPAALCTLQueryParser(java.io.InputStream stream) { |
1192 | + this(stream, null); |
1193 | + } |
1194 | + /** Constructor with InputStream and supplied encoding */ |
1195 | + public TAPAALCTLQueryParser(java.io.InputStream stream, String encoding) { |
1196 | + try { jj_input_stream = new SimpleCharStream(stream, encoding, 1, 1); } catch(java.io.UnsupportedEncodingException e) { throw new RuntimeException(e); } |
1197 | + token_source = new TAPAALCTLQueryParserTokenManager(jj_input_stream); |
1198 | + token = new Token(); |
1199 | + jj_ntk = -1; |
1200 | + jj_gen = 0; |
1201 | + for (int i = 0; i < 10; i++) jj_la1[i] = -1; |
1202 | + for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); |
1203 | + } |
1204 | + |
1205 | + /** Reinitialise. */ |
1206 | + public void ReInit(java.io.InputStream stream) { |
1207 | + ReInit(stream, null); |
1208 | + } |
1209 | + /** Reinitialise. */ |
1210 | + public void ReInit(java.io.InputStream stream, String encoding) { |
1211 | + try { jj_input_stream.ReInit(stream, encoding, 1, 1); } catch(java.io.UnsupportedEncodingException e) { throw new RuntimeException(e); } |
1212 | + token_source.ReInit(jj_input_stream); |
1213 | + token = new Token(); |
1214 | + jj_ntk = -1; |
1215 | + jj_gen = 0; |
1216 | + for (int i = 0; i < 10; i++) jj_la1[i] = -1; |
1217 | + for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); |
1218 | + } |
1219 | + |
1220 | + /** Constructor. */ |
1221 | + public TAPAALCTLQueryParser(java.io.Reader stream) { |
1222 | + jj_input_stream = new SimpleCharStream(stream, 1, 1); |
1223 | + token_source = new TAPAALCTLQueryParserTokenManager(jj_input_stream); |
1224 | + token = new Token(); |
1225 | + jj_ntk = -1; |
1226 | + jj_gen = 0; |
1227 | + for (int i = 0; i < 10; i++) jj_la1[i] = -1; |
1228 | + for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); |
1229 | + } |
1230 | + |
1231 | + /** Reinitialise. */ |
1232 | + public void ReInit(java.io.Reader stream) { |
1233 | + if (jj_input_stream == null) { |
1234 | + jj_input_stream = new SimpleCharStream(stream, 1, 1); |
1235 | + } else { |
1236 | + jj_input_stream.ReInit(stream, 1, 1); |
1237 | + } |
1238 | + if (token_source == null) { |
1239 | + token_source = new TAPAALCTLQueryParserTokenManager(jj_input_stream); |
1240 | + } |
1241 | + |
1242 | + token_source.ReInit(jj_input_stream); |
1243 | + token = new Token(); |
1244 | + jj_ntk = -1; |
1245 | + jj_gen = 0; |
1246 | + for (int i = 0; i < 10; i++) jj_la1[i] = -1; |
1247 | + for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); |
1248 | + } |
1249 | + |
1250 | + /** Constructor with generated Token Manager. */ |
1251 | + public TAPAALCTLQueryParser(TAPAALCTLQueryParserTokenManager tm) { |
1252 | + token_source = tm; |
1253 | + token = new Token(); |
1254 | + jj_ntk = -1; |
1255 | + jj_gen = 0; |
1256 | + for (int i = 0; i < 10; i++) jj_la1[i] = -1; |
1257 | + for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); |
1258 | + } |
1259 | + |
1260 | + /** Reinitialise. */ |
1261 | + public void ReInit(TAPAALCTLQueryParserTokenManager tm) { |
1262 | + token_source = tm; |
1263 | + token = new Token(); |
1264 | + jj_ntk = -1; |
1265 | + jj_gen = 0; |
1266 | + for (int i = 0; i < 10; i++) jj_la1[i] = -1; |
1267 | + for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); |
1268 | + } |
1269 | + |
1270 | + private Token jj_consume_token(int kind) throws ParseException { |
1271 | + Token oldToken; |
1272 | + if ((oldToken = token).next != null) token = token.next; |
1273 | + else token = token.next = token_source.getNextToken(); |
1274 | + jj_ntk = -1; |
1275 | + if (token.kind == kind) { |
1276 | + jj_gen++; |
1277 | + if (++jj_gc > 100) { |
1278 | + jj_gc = 0; |
1279 | + for (int i = 0; i < jj_2_rtns.length; i++) { |
1280 | + JJCalls c = jj_2_rtns[i]; |
1281 | + while (c != null) { |
1282 | + if (c.gen < jj_gen) c.first = null; |
1283 | + c = c.next; |
1284 | + } |
1285 | + } |
1286 | + } |
1287 | + return token; |
1288 | + } |
1289 | + token = oldToken; |
1290 | + jj_kind = kind; |
1291 | + throw generateParseException(); |
1292 | + } |
1293 | + |
1294 | + @SuppressWarnings("serial") |
1295 | + static private final class LookaheadSuccess extends java.lang.Error { |
1296 | + @Override |
1297 | + public Throwable fillInStackTrace() { |
1298 | + return this; |
1299 | + } |
1300 | + } |
1301 | + static private final LookaheadSuccess jj_ls = new LookaheadSuccess(); |
1302 | + private boolean jj_scan_token(int kind) { |
1303 | + if (jj_scanpos == jj_lastpos) { |
1304 | + jj_la--; |
1305 | + if (jj_scanpos.next == null) { |
1306 | + jj_lastpos = jj_scanpos = jj_scanpos.next = token_source.getNextToken(); |
1307 | + } else { |
1308 | + jj_lastpos = jj_scanpos = jj_scanpos.next; |
1309 | + } |
1310 | + } else { |
1311 | + jj_scanpos = jj_scanpos.next; |
1312 | + } |
1313 | + if (jj_rescan) { |
1314 | + int i = 0; Token tok = token; |
1315 | + while (tok != null && tok != jj_scanpos) { i++; tok = tok.next; } |
1316 | + if (tok != null) jj_add_error_token(kind, i); |
1317 | + } |
1318 | + if (jj_scanpos.kind != kind) return true; |
1319 | + if (jj_la == 0 && jj_scanpos == jj_lastpos) throw jj_ls; |
1320 | + return false; |
1321 | + } |
1322 | + |
1323 | + |
1324 | + /** Get the next Token. */ |
1325 | + final public Token getNextToken() { |
1326 | + if (token.next != null) token = token.next; |
1327 | + else token = token.next = token_source.getNextToken(); |
1328 | + jj_ntk = -1; |
1329 | + jj_gen++; |
1330 | + return token; |
1331 | + } |
1332 | + |
1333 | + /** Get the specific Token. */ |
1334 | + final public Token getToken(int index) { |
1335 | + Token t = token; |
1336 | + for (int i = 0; i < index; i++) { |
1337 | + if (t.next != null) t = t.next; |
1338 | + else t = t.next = token_source.getNextToken(); |
1339 | + } |
1340 | + return t; |
1341 | + } |
1342 | + |
1343 | + private int jj_ntk_f() { |
1344 | + if ((jj_nt=token.next) == null) |
1345 | + return (jj_ntk = (token.next=token_source.getNextToken()).kind); |
1346 | + else |
1347 | + return (jj_ntk = jj_nt.kind); |
1348 | + } |
1349 | + |
1350 | + private java.util.List<int[]> jj_expentries = new java.util.ArrayList<int[]>(); |
1351 | + private int[] jj_expentry; |
1352 | + private int jj_kind = -1; |
1353 | + private int[] jj_lasttokens = new int[100]; |
1354 | + private int jj_endpos; |
1355 | + |
1356 | + private void jj_add_error_token(int kind, int pos) { |
1357 | + if (pos >= 100) { |
1358 | + return; |
1359 | + } |
1360 | + |
1361 | + if (pos == jj_endpos + 1) { |
1362 | + jj_lasttokens[jj_endpos++] = kind; |
1363 | + } else if (jj_endpos != 0) { |
1364 | + jj_expentry = new int[jj_endpos]; |
1365 | + |
1366 | + for (int i = 0; i < jj_endpos; i++) { |
1367 | + jj_expentry[i] = jj_lasttokens[i]; |
1368 | + } |
1369 | + |
1370 | + for (int[] oldentry : jj_expentries) { |
1371 | + if (oldentry.length == jj_expentry.length) { |
1372 | + boolean isMatched = true; |
1373 | + |
1374 | + for (int i = 0; i < jj_expentry.length; i++) { |
1375 | + if (oldentry[i] != jj_expentry[i]) { |
1376 | + isMatched = false; |
1377 | + break; |
1378 | + } |
1379 | + |
1380 | + } |
1381 | + if (isMatched) { |
1382 | + jj_expentries.add(jj_expentry); |
1383 | + break; |
1384 | + } |
1385 | + } |
1386 | + } |
1387 | + |
1388 | + if (pos != 0) { |
1389 | + jj_lasttokens[(jj_endpos = pos) - 1] = kind; |
1390 | + } |
1391 | + } |
1392 | + } |
1393 | + |
1394 | + /** Generate ParseException. */ |
1395 | + public ParseException generateParseException() { |
1396 | + jj_expentries.clear(); |
1397 | + boolean[] la1tokens = new boolean[29]; |
1398 | + if (jj_kind >= 0) { |
1399 | + la1tokens[jj_kind] = true; |
1400 | + jj_kind = -1; |
1401 | + } |
1402 | + for (int i = 0; i < 10; i++) { |
1403 | + if (jj_la1[i] == jj_gen) { |
1404 | + for (int j = 0; j < 32; j++) { |
1405 | + if ((jj_la1_0[i] & (1<<j)) != 0) { |
1406 | + la1tokens[j] = true; |
1407 | + } |
1408 | + } |
1409 | + } |
1410 | + } |
1411 | + for (int i = 0; i < 29; i++) { |
1412 | + if (la1tokens[i]) { |
1413 | + jj_expentry = new int[1]; |
1414 | + jj_expentry[0] = i; |
1415 | + jj_expentries.add(jj_expentry); |
1416 | + } |
1417 | + } |
1418 | + jj_endpos = 0; |
1419 | + jj_rescan_token(); |
1420 | + jj_add_error_token(0, 0); |
1421 | + int[][] exptokseq = new int[jj_expentries.size()][]; |
1422 | + for (int i = 0; i < jj_expentries.size(); i++) { |
1423 | + exptokseq[i] = jj_expentries.get(i); |
1424 | + } |
1425 | + return new ParseException(token, exptokseq, tokenImage); |
1426 | + } |
1427 | + |
1428 | + private boolean trace_enabled; |
1429 | + |
1430 | + /** Trace enabled. */ |
1431 | + final public boolean trace_enabled() { |
1432 | + return trace_enabled; |
1433 | + } |
1434 | + |
1435 | + /** Enable tracing. */ |
1436 | + final public void enable_tracing() { |
1437 | + } |
1438 | + |
1439 | + /** Disable tracing. */ |
1440 | + final public void disable_tracing() { |
1441 | + } |
1442 | + |
1443 | + private void jj_rescan_token() { |
1444 | + jj_rescan = true; |
1445 | + for (int i = 0; i < 3; i++) { |
1446 | + try { |
1447 | + JJCalls p = jj_2_rtns[i]; |
1448 | + |
1449 | + do { |
1450 | + if (p.gen > jj_gen) { |
1451 | + jj_la = p.arg; jj_lastpos = jj_scanpos = p.first; |
1452 | + switch (i) { |
1453 | + case 0: jj_3_1(); break; |
1454 | + case 1: jj_3_2(); break; |
1455 | + case 2: jj_3_3(); break; |
1456 | + } |
1457 | + } |
1458 | + p = p.next; |
1459 | + } while (p != null); |
1460 | + |
1461 | + } catch(LookaheadSuccess ls) { } |
1462 | + } |
1463 | + jj_rescan = false; |
1464 | + } |
1465 | + |
1466 | + private void jj_save(int index, int xla) { |
1467 | + JJCalls p = jj_2_rtns[index]; |
1468 | + while (p.gen > jj_gen) { |
1469 | + if (p.next == null) { p = p.next = new JJCalls(); break; } |
1470 | + p = p.next; |
1471 | + } |
1472 | + |
1473 | + p.gen = jj_gen + xla - jj_la; |
1474 | + p.first = token; |
1475 | + p.arg = xla; |
1476 | + } |
1477 | + |
1478 | + static final class JJCalls { |
1479 | + int gen; |
1480 | + Token first; |
1481 | + int arg; |
1482 | + JJCalls next; |
1483 | + } |
1484 | |
1485 | } |
1486 | |
1487 | === modified file 'src/dk/aau/cs/TCTL/Parsing/TAPAALQueryParser.java' |
1488 | --- src/dk/aau/cs/TCTL/Parsing/TAPAALQueryParser.java 2014-05-22 20:26:41 +0000 |
1489 | +++ src/dk/aau/cs/TCTL/Parsing/TAPAALQueryParser.java 2021-09-29 07:20:55 +0000 |
1490 | @@ -1,3 +1,4 @@ |
1491 | +/* TAPAALQueryParser.java */ |
1492 | /* Generated By:JavaCC: Do not edit this line. TAPAALQueryParser.java */ |
1493 | package dk.aau.cs.TCTL.Parsing; |
1494 | |
1495 | @@ -25,624 +26,691 @@ |
1496 | |
1497 | public class TAPAALQueryParser implements TAPAALQueryParserConstants { |
1498 | |
1499 | - private static final String ERROR_PARSING_QUERY_MESSAGE = "TAPAAL countered an error trying to parse the query"; |
1500 | - |
1501 | - public static TCTLAbstractProperty parse(String query) throws ParseException { |
1502 | - TAPAALQueryParser parser = new TAPAALQueryParser(new StringReader(query)); |
1503 | - return parser.AbstractProperty(); |
1504 | + private static final String ERROR_PARSING_QUERY_MESSAGE = "TAPAAL countered an error trying to parse the query"; |
1505 | + |
1506 | + public static TCTLAbstractProperty parse(String query) throws ParseException { |
1507 | + TAPAALQueryParser parser = new TAPAALQueryParser(new StringReader(query)); |
1508 | + return parser.Start(); |
1509 | + } |
1510 | + |
1511 | + /** Root production. */ |
1512 | + final public TCTLAbstractProperty Start() throws ParseException {TCTLAbstractProperty child = null; |
1513 | + child = AbstractProperty(); |
1514 | + jj_consume_token(0); |
1515 | + {if ("" != null) return child;} |
1516 | + throw new Error("Missing return statement in function"); |
1517 | + } |
1518 | + |
1519 | + final public TCTLAbstractProperty AbstractProperty() throws ParseException {TCTLAbstractStateProperty child = null; |
1520 | + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { |
1521 | + case EF:{ |
1522 | + jj_consume_token(EF); |
1523 | + child = OrExpr(); |
1524 | + {if ("" != null) return new TCTLEFNode(child);} |
1525 | + break; |
1526 | + } |
1527 | + case EG:{ |
1528 | + jj_consume_token(EG); |
1529 | + child = OrExpr(); |
1530 | + {if ("" != null) return new TCTLEGNode(child);} |
1531 | + break; |
1532 | + } |
1533 | + case AF:{ |
1534 | + jj_consume_token(AF); |
1535 | + child = OrExpr(); |
1536 | + {if ("" != null) return new TCTLAFNode(child);} |
1537 | + break; |
1538 | + } |
1539 | + case AG:{ |
1540 | + jj_consume_token(AG); |
1541 | + child = OrExpr(); |
1542 | + {if ("" != null) return new TCTLAGNode(child);} |
1543 | + break; |
1544 | + } |
1545 | + default: |
1546 | + jj_la1[0] = jj_gen; |
1547 | + jj_consume_token(-1); |
1548 | + throw new ParseException(); |
1549 | } |
1550 | - |
1551 | -/** Root production. */ |
1552 | - final public TCTLAbstractProperty AbstractProperty() throws ParseException { |
1553 | - TCTLAbstractStateProperty child = null; |
1554 | - switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { |
1555 | - case EF: |
1556 | - jj_consume_token(EF); |
1557 | - child = OrExpr(); |
1558 | - {if (true) return new TCTLEFNode(child);} |
1559 | - break; |
1560 | - case EG: |
1561 | - jj_consume_token(EG); |
1562 | - child = OrExpr(); |
1563 | - {if (true) return new TCTLEGNode(child);} |
1564 | - break; |
1565 | - case AF: |
1566 | - jj_consume_token(AF); |
1567 | - child = OrExpr(); |
1568 | - {if (true) return new TCTLAFNode(child);} |
1569 | - break; |
1570 | - case AG: |
1571 | - jj_consume_token(AG); |
1572 | - child = OrExpr(); |
1573 | - {if (true) return new TCTLAGNode(child);} |
1574 | - break; |
1575 | - default: |
1576 | - jj_la1[0] = jj_gen; |
1577 | - jj_consume_token(-1); |
1578 | - throw new ParseException(); |
1579 | + throw new Error("Missing return statement in function"); |
1580 | } |
1581 | - throw new Error("Missing return statement in function"); |
1582 | - } |
1583 | |
1584 | - final public TCTLAbstractStateProperty OrExpr() throws ParseException { |
1585 | - TCTLAbstractStateProperty currentChild; |
1586 | + final public TCTLAbstractStateProperty OrExpr() throws ParseException {TCTLAbstractStateProperty currentChild; |
1587 | ArrayList<TCTLAbstractStateProperty> disjunctions = new ArrayList<TCTLAbstractStateProperty>(); |
1588 | - currentChild = AndExpr(); |
1589 | - disjunctions.add(currentChild); |
1590 | - label_1: |
1591 | - while (true) { |
1592 | - switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { |
1593 | - case OR: |
1594 | - ; |
1595 | - break; |
1596 | - default: |
1597 | - jj_la1[1] = jj_gen; |
1598 | - break label_1; |
1599 | - } |
1600 | - jj_consume_token(OR); |
1601 | - currentChild = AndExpr(); |
1602 | - disjunctions.add(currentChild); |
1603 | + currentChild = AndExpr(); |
1604 | + disjunctions.add(currentChild); |
1605 | + label_1: |
1606 | + while (true) { |
1607 | + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { |
1608 | + case OR:{ |
1609 | + ; |
1610 | + break; |
1611 | + } |
1612 | + default: |
1613 | + jj_la1[1] = jj_gen; |
1614 | + break label_1; |
1615 | + } |
1616 | + jj_consume_token(OR); |
1617 | + currentChild = AndExpr(); |
1618 | + disjunctions.add(currentChild); |
1619 | + } |
1620 | + {if ("" != null) return disjunctions.size() == 1 ? currentChild : new TCTLOrListNode(disjunctions);} |
1621 | + throw new Error("Missing return statement in function"); |
1622 | } |
1623 | - {if (true) return disjunctions.size() == 1 ? currentChild : new TCTLOrListNode(disjunctions);} |
1624 | - throw new Error("Missing return statement in function"); |
1625 | - } |
1626 | |
1627 | - final public TCTLAbstractStateProperty AndExpr() throws ParseException { |
1628 | - TCTLAbstractStateProperty currentChild; |
1629 | + final public TCTLAbstractStateProperty AndExpr() throws ParseException {TCTLAbstractStateProperty currentChild; |
1630 | ArrayList<TCTLAbstractStateProperty> conjunctions = new ArrayList<TCTLAbstractStateProperty>(); |
1631 | - currentChild = NotExpr(); |
1632 | - conjunctions.add(currentChild); |
1633 | - label_2: |
1634 | - while (true) { |
1635 | - switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { |
1636 | - case AND: |
1637 | - ; |
1638 | - break; |
1639 | - default: |
1640 | - jj_la1[2] = jj_gen; |
1641 | - break label_2; |
1642 | - } |
1643 | - jj_consume_token(AND); |
1644 | - currentChild = NotExpr(); |
1645 | - conjunctions.add(currentChild); |
1646 | - } |
1647 | - {if (true) return conjunctions.size() == 1 ? currentChild : new TCTLAndListNode(conjunctions);} |
1648 | - throw new Error("Missing return statement in function"); |
1649 | - } |
1650 | - |
1651 | - final public TCTLAbstractStateProperty NotExpr() throws ParseException { |
1652 | - TCTLAbstractStateProperty child; |
1653 | - switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { |
1654 | - case NOT: |
1655 | - jj_consume_token(NOT); |
1656 | - jj_consume_token(20); |
1657 | - child = OrExpr(); |
1658 | - jj_consume_token(21); |
1659 | - {if (true) return new TCTLNotNode(child);} |
1660 | - break; |
1661 | - case TRUE: |
1662 | - case FALSE: |
1663 | - case DEADLOCK: |
1664 | - case NUM: |
1665 | - case IDENT: |
1666 | - case 20: |
1667 | - child = Factor(); |
1668 | - {if (true) return child;} |
1669 | - break; |
1670 | - default: |
1671 | - jj_la1[3] = jj_gen; |
1672 | - jj_consume_token(-1); |
1673 | - throw new ParseException(); |
1674 | - } |
1675 | - throw new Error("Missing return statement in function"); |
1676 | - } |
1677 | - |
1678 | - final public TCTLAbstractStateProperty Factor() throws ParseException { |
1679 | - TCTLAbstractStateProperty thisProp; |
1680 | - switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { |
1681 | - case TRUE: |
1682 | - jj_consume_token(TRUE); |
1683 | - thisProp = new TCTLTrueNode(); |
1684 | - break; |
1685 | - case FALSE: |
1686 | - jj_consume_token(FALSE); |
1687 | - thisProp = new TCTLFalseNode(); |
1688 | - break; |
1689 | - case DEADLOCK: |
1690 | - jj_consume_token(DEADLOCK); |
1691 | - thisProp = new TCTLDeadlockNode(); |
1692 | - break; |
1693 | - default: |
1694 | - jj_la1[4] = jj_gen; |
1695 | - if (jj_2_1(2147483647)) { |
1696 | - thisProp = AtomicProposition(); |
1697 | - } else { |
1698 | - switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { |
1699 | - case 20: |
1700 | - jj_consume_token(20); |
1701 | - thisProp = OrExpr(); |
1702 | - jj_consume_token(21); |
1703 | - break; |
1704 | - default: |
1705 | - jj_la1[5] = jj_gen; |
1706 | - jj_consume_token(-1); |
1707 | - throw new ParseException(); |
1708 | - } |
1709 | - } |
1710 | - } |
1711 | - {if (true) return thisProp;} |
1712 | - throw new Error("Missing return statement in function"); |
1713 | - } |
1714 | - |
1715 | - final public TCTLAbstractStateProperty AtomicProposition() throws ParseException { |
1716 | - TCTLAbstractStateProperty left; |
1717 | + currentChild = NotExpr(); |
1718 | + conjunctions.add(currentChild); |
1719 | + label_2: |
1720 | + while (true) { |
1721 | + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { |
1722 | + case AND:{ |
1723 | + ; |
1724 | + break; |
1725 | + } |
1726 | + default: |
1727 | + jj_la1[2] = jj_gen; |
1728 | + break label_2; |
1729 | + } |
1730 | + jj_consume_token(AND); |
1731 | + currentChild = NotExpr(); |
1732 | + conjunctions.add(currentChild); |
1733 | + } |
1734 | + {if ("" != null) return conjunctions.size() == 1 ? currentChild : new TCTLAndListNode(conjunctions);} |
1735 | + throw new Error("Missing return statement in function"); |
1736 | + } |
1737 | + |
1738 | + final public TCTLAbstractStateProperty NotExpr() throws ParseException {TCTLAbstractStateProperty child; |
1739 | + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { |
1740 | + case NOT:{ |
1741 | + jj_consume_token(NOT); |
1742 | + jj_consume_token(20); |
1743 | + child = OrExpr(); |
1744 | + jj_consume_token(21); |
1745 | + {if ("" != null) return new TCTLNotNode(child);} |
1746 | + break; |
1747 | + } |
1748 | + case TRUE: |
1749 | + case FALSE: |
1750 | + case DEADLOCK: |
1751 | + case NUM: |
1752 | + case IDENT: |
1753 | + case 20:{ |
1754 | + child = Factor(); |
1755 | + {if ("" != null) return child;} |
1756 | + break; |
1757 | + } |
1758 | + default: |
1759 | + jj_la1[3] = jj_gen; |
1760 | + jj_consume_token(-1); |
1761 | + throw new ParseException(); |
1762 | + } |
1763 | + throw new Error("Missing return statement in function"); |
1764 | + } |
1765 | + |
1766 | + final public TCTLAbstractStateProperty Factor() throws ParseException {TCTLAbstractStateProperty thisProp; |
1767 | + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { |
1768 | + case TRUE:{ |
1769 | + jj_consume_token(TRUE); |
1770 | + thisProp = new TCTLTrueNode(); |
1771 | + break; |
1772 | + } |
1773 | + case FALSE:{ |
1774 | + jj_consume_token(FALSE); |
1775 | + thisProp = new TCTLFalseNode(); |
1776 | + break; |
1777 | + } |
1778 | + case DEADLOCK:{ |
1779 | + jj_consume_token(DEADLOCK); |
1780 | + thisProp = new TCTLDeadlockNode(); |
1781 | + break; |
1782 | + } |
1783 | + default: |
1784 | + jj_la1[4] = jj_gen; |
1785 | + if (jj_2_1(2147483647)) { |
1786 | + thisProp = AtomicProposition(); |
1787 | + } else { |
1788 | + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { |
1789 | + case 20:{ |
1790 | + jj_consume_token(20); |
1791 | + thisProp = OrExpr(); |
1792 | + jj_consume_token(21); |
1793 | + break; |
1794 | + } |
1795 | + default: |
1796 | + jj_la1[5] = jj_gen; |
1797 | + jj_consume_token(-1); |
1798 | + throw new ParseException(); |
1799 | + } |
1800 | + } |
1801 | + } |
1802 | + {if ("" != null) return thisProp;} |
1803 | + throw new Error("Missing return statement in function"); |
1804 | + } |
1805 | + |
1806 | + final public TCTLAbstractStateProperty AtomicProposition() throws ParseException {TCTLAbstractStateProperty left; |
1807 | TCTLAbstractStateProperty right; |
1808 | Token op; |
1809 | - left = AritmeticExpr(); |
1810 | - op = jj_consume_token(OP); |
1811 | - right = AritmeticExpr(); |
1812 | - {if (true) return new TCTLAtomicPropositionNode(left, op.image, right);} |
1813 | - throw new Error("Missing return statement in function"); |
1814 | - } |
1815 | + left = AritmeticExpr(); |
1816 | + op = jj_consume_token(OP); |
1817 | + right = AritmeticExpr(); |
1818 | + {if ("" != null) return new TCTLAtomicPropositionNode(left, op.image, right);} |
1819 | + throw new Error("Missing return statement in function"); |
1820 | + } |
1821 | |
1822 | - final public TCTLAbstractStateProperty AritmeticExpr() throws ParseException { |
1823 | - TCTLAbstractStateProperty currentChild; |
1824 | + final public TCTLAbstractStateProperty AritmeticExpr() throws ParseException {TCTLAbstractStateProperty currentChild; |
1825 | ArrayList<TCTLAbstractStateProperty> terms = new ArrayList<TCTLAbstractStateProperty>(); |
1826 | Token op; |
1827 | - currentChild = AritmeticTerm(); |
1828 | - terms.add(currentChild); |
1829 | - label_3: |
1830 | - while (true) { |
1831 | - switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { |
1832 | - case PLUS: |
1833 | - ; |
1834 | - break; |
1835 | - default: |
1836 | - jj_la1[6] = jj_gen; |
1837 | - break label_3; |
1838 | - } |
1839 | - op = jj_consume_token(PLUS); |
1840 | - currentChild = AritmeticTerm(); |
1841 | - terms.add(new AritmeticOperator(op.image)); |
1842 | - terms.add(currentChild); |
1843 | + currentChild = AritmeticTerm(); |
1844 | + terms.add(currentChild); |
1845 | + label_3: |
1846 | + while (true) { |
1847 | + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { |
1848 | + case PLUS:{ |
1849 | + ; |
1850 | + break; |
1851 | + } |
1852 | + default: |
1853 | + jj_la1[6] = jj_gen; |
1854 | + break label_3; |
1855 | + } |
1856 | + op = jj_consume_token(PLUS); |
1857 | + currentChild = AritmeticTerm(); |
1858 | + terms.add(new AritmeticOperator(op.image)); |
1859 | + terms.add(currentChild); |
1860 | + } |
1861 | + {if ("" != null) return terms.size() == 1 ? currentChild : new TCTLPlusListNode(terms);} |
1862 | + throw new Error("Missing return statement in function"); |
1863 | } |
1864 | - {if (true) return terms.size() == 1 ? currentChild : new TCTLPlusListNode(terms);} |
1865 | - throw new Error("Missing return statement in function"); |
1866 | - } |
1867 | |
1868 | - final public TCTLAbstractStateProperty AritmeticTerm() throws ParseException { |
1869 | - TCTLAbstractStateProperty currentChild; |
1870 | + final public TCTLAbstractStateProperty AritmeticTerm() throws ParseException {TCTLAbstractStateProperty currentChild; |
1871 | ArrayList<TCTLAbstractStateProperty> factors = new ArrayList<TCTLAbstractStateProperty>(); |
1872 | Token op; |
1873 | - currentChild = AritmeticFactor(); |
1874 | - factors.add(currentChild); |
1875 | - label_4: |
1876 | - while (true) { |
1877 | - switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { |
1878 | - case MULT: |
1879 | - ; |
1880 | - break; |
1881 | - default: |
1882 | - jj_la1[7] = jj_gen; |
1883 | - break label_4; |
1884 | - } |
1885 | - op = jj_consume_token(MULT); |
1886 | - currentChild = AritmeticFactor(); |
1887 | - factors.add(new AritmeticOperator(op.image)); |
1888 | - factors.add(currentChild); |
1889 | + currentChild = AritmeticFactor(); |
1890 | + factors.add(currentChild); |
1891 | + label_4: |
1892 | + while (true) { |
1893 | + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { |
1894 | + case MULT:{ |
1895 | + ; |
1896 | + break; |
1897 | + } |
1898 | + default: |
1899 | + jj_la1[7] = jj_gen; |
1900 | + break label_4; |
1901 | + } |
1902 | + op = jj_consume_token(MULT); |
1903 | + currentChild = AritmeticFactor(); |
1904 | + factors.add(new AritmeticOperator(op.image)); |
1905 | + factors.add(currentChild); |
1906 | + } |
1907 | + {if ("" != null) return factors.size() == 1 ? currentChild : new TCTLTermListNode(factors);} |
1908 | + throw new Error("Missing return statement in function"); |
1909 | } |
1910 | - {if (true) return factors.size() == 1 ? currentChild : new TCTLTermListNode(factors);} |
1911 | - throw new Error("Missing return statement in function"); |
1912 | - } |
1913 | |
1914 | - final public TCTLAbstractStateProperty AritmeticFactor() throws ParseException { |
1915 | - TCTLAbstractStateProperty thisProp; |
1916 | + final public TCTLAbstractStateProperty AritmeticFactor() throws ParseException {TCTLAbstractStateProperty thisProp; |
1917 | Token template = null; |
1918 | Token place; |
1919 | Token op; |
1920 | Token num; |
1921 | - switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { |
1922 | - case IDENT: |
1923 | - if (jj_2_2(2)) { |
1924 | - template = jj_consume_token(IDENT); |
1925 | - jj_consume_token(22); |
1926 | - } else { |
1927 | - ; |
1928 | - } |
1929 | - place = jj_consume_token(IDENT); |
1930 | - thisProp = new TCTLPlaceNode(template == null ? "" : template.image, place.image); |
1931 | - break; |
1932 | - case NUM: |
1933 | - num = jj_consume_token(NUM); |
1934 | - thisProp = new TCTLConstNode(Integer.parseInt(num.image)); |
1935 | - break; |
1936 | - case 20: |
1937 | - jj_consume_token(20); |
1938 | - thisProp = AritmeticExpr(); |
1939 | - jj_consume_token(21); |
1940 | - break; |
1941 | - default: |
1942 | - jj_la1[8] = jj_gen; |
1943 | - jj_consume_token(-1); |
1944 | - throw new ParseException(); |
1945 | - } |
1946 | - {if (true) return thisProp;} |
1947 | - throw new Error("Missing return statement in function"); |
1948 | - } |
1949 | - |
1950 | - private boolean jj_2_1(int xla) { |
1951 | - jj_la = xla; jj_lastpos = jj_scanpos = token; |
1952 | - try { return !jj_3_1(); } |
1953 | - catch(LookaheadSuccess ls) { return true; } |
1954 | - finally { jj_save(0, xla); } |
1955 | - } |
1956 | - |
1957 | - private boolean jj_2_2(int xla) { |
1958 | - jj_la = xla; jj_lastpos = jj_scanpos = token; |
1959 | - try { return !jj_3_2(); } |
1960 | - catch(LookaheadSuccess ls) { return true; } |
1961 | - finally { jj_save(1, xla); } |
1962 | - } |
1963 | - |
1964 | - private boolean jj_3_1() { |
1965 | - if (jj_3R_5()) return true; |
1966 | - return false; |
1967 | - } |
1968 | - |
1969 | - private boolean jj_3R_8() { |
1970 | - if (jj_scan_token(PLUS)) return true; |
1971 | - if (jj_3R_7()) return true; |
1972 | - return false; |
1973 | - } |
1974 | - |
1975 | - private boolean jj_3R_5() { |
1976 | - if (jj_3R_6()) return true; |
1977 | - if (jj_scan_token(OP)) return true; |
1978 | - if (jj_3R_6()) return true; |
1979 | - return false; |
1980 | - } |
1981 | - |
1982 | - private boolean jj_3R_13() { |
1983 | - if (jj_scan_token(20)) return true; |
1984 | - if (jj_3R_6()) return true; |
1985 | - if (jj_scan_token(21)) return true; |
1986 | - return false; |
1987 | - } |
1988 | - |
1989 | - private boolean jj_3R_10() { |
1990 | - if (jj_scan_token(MULT)) return true; |
1991 | - if (jj_3R_9()) return true; |
1992 | - return false; |
1993 | - } |
1994 | - |
1995 | - private boolean jj_3R_12() { |
1996 | - if (jj_scan_token(NUM)) return true; |
1997 | - return false; |
1998 | - } |
1999 | - |
2000 | - private boolean jj_3_2() { |
2001 | - if (jj_scan_token(IDENT)) return true; |
2002 | - if (jj_scan_token(22)) return true; |
2003 | - return false; |
2004 | - } |
2005 | - |
2006 | - private boolean jj_3R_11() { |
2007 | - Token xsp; |
2008 | - xsp = jj_scanpos; |
2009 | - if (jj_3_2()) jj_scanpos = xsp; |
2010 | - if (jj_scan_token(IDENT)) return true; |
2011 | - return false; |
2012 | - } |
2013 | - |
2014 | - private boolean jj_3R_6() { |
2015 | - if (jj_3R_7()) return true; |
2016 | - Token xsp; |
2017 | - while (true) { |
2018 | - xsp = jj_scanpos; |
2019 | - if (jj_3R_8()) { jj_scanpos = xsp; break; } |
2020 | - } |
2021 | - return false; |
2022 | - } |
2023 | - |
2024 | - private boolean jj_3R_7() { |
2025 | - if (jj_3R_9()) return true; |
2026 | - Token xsp; |
2027 | - while (true) { |
2028 | - xsp = jj_scanpos; |
2029 | - if (jj_3R_10()) { jj_scanpos = xsp; break; } |
2030 | - } |
2031 | - return false; |
2032 | - } |
2033 | - |
2034 | - private boolean jj_3R_9() { |
2035 | - Token xsp; |
2036 | - xsp = jj_scanpos; |
2037 | - if (jj_3R_11()) { |
2038 | - jj_scanpos = xsp; |
2039 | - if (jj_3R_12()) { |
2040 | - jj_scanpos = xsp; |
2041 | - if (jj_3R_13()) return true; |
2042 | - } |
2043 | - } |
2044 | - return false; |
2045 | - } |
2046 | - |
2047 | - /** Generated Token Manager. */ |
2048 | - public TAPAALQueryParserTokenManager token_source; |
2049 | - SimpleCharStream jj_input_stream; |
2050 | - /** Current token. */ |
2051 | - public Token token; |
2052 | - /** Next token. */ |
2053 | - public Token jj_nt; |
2054 | - private int jj_ntk; |
2055 | - private Token jj_scanpos, jj_lastpos; |
2056 | - private int jj_la; |
2057 | - private int jj_gen; |
2058 | - final private int[] jj_la1 = new int[9]; |
2059 | - static private int[] jj_la1_0; |
2060 | - static { |
2061 | - jj_la1_init_0(); |
2062 | - } |
2063 | - private static void jj_la1_init_0() { |
2064 | - jj_la1_0 = new int[] {0xf0,0x100,0x200,0x10640e,0xe,0x100000,0x800,0x1000,0x106000,}; |
2065 | - } |
2066 | - final private JJCalls[] jj_2_rtns = new JJCalls[2]; |
2067 | - private boolean jj_rescan = false; |
2068 | - private int jj_gc = 0; |
2069 | - |
2070 | - /** Constructor with InputStream. */ |
2071 | - public TAPAALQueryParser(java.io.InputStream stream) { |
2072 | - this(stream, null); |
2073 | - } |
2074 | - /** Constructor with InputStream and supplied encoding */ |
2075 | - public TAPAALQueryParser(java.io.InputStream stream, String encoding) { |
2076 | - try { jj_input_stream = new SimpleCharStream(stream, encoding, 1, 1); } catch(java.io.UnsupportedEncodingException e) { throw new RuntimeException(e); } |
2077 | - token_source = new TAPAALQueryParserTokenManager(jj_input_stream); |
2078 | - token = new Token(); |
2079 | - jj_ntk = -1; |
2080 | - jj_gen = 0; |
2081 | - for (int i = 0; i < 9; i++) jj_la1[i] = -1; |
2082 | - for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); |
2083 | - } |
2084 | - |
2085 | - /** Reinitialise. */ |
2086 | - public void ReInit(java.io.InputStream stream) { |
2087 | - ReInit(stream, null); |
2088 | - } |
2089 | - /** Reinitialise. */ |
2090 | - public void ReInit(java.io.InputStream stream, String encoding) { |
2091 | - try { jj_input_stream.ReInit(stream, encoding, 1, 1); } catch(java.io.UnsupportedEncodingException e) { throw new RuntimeException(e); } |
2092 | - token_source.ReInit(jj_input_stream); |
2093 | - token = new Token(); |
2094 | - jj_ntk = -1; |
2095 | - jj_gen = 0; |
2096 | - for (int i = 0; i < 9; i++) jj_la1[i] = -1; |
2097 | - for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); |
2098 | - } |
2099 | - |
2100 | - /** Constructor. */ |
2101 | - public TAPAALQueryParser(java.io.Reader stream) { |
2102 | - jj_input_stream = new SimpleCharStream(stream, 1, 1); |
2103 | - token_source = new TAPAALQueryParserTokenManager(jj_input_stream); |
2104 | - token = new Token(); |
2105 | - jj_ntk = -1; |
2106 | - jj_gen = 0; |
2107 | - for (int i = 0; i < 9; i++) jj_la1[i] = -1; |
2108 | - for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); |
2109 | - } |
2110 | - |
2111 | - /** Reinitialise. */ |
2112 | - public void ReInit(java.io.Reader stream) { |
2113 | - jj_input_stream.ReInit(stream, 1, 1); |
2114 | - token_source.ReInit(jj_input_stream); |
2115 | - token = new Token(); |
2116 | - jj_ntk = -1; |
2117 | - jj_gen = 0; |
2118 | - for (int i = 0; i < 9; i++) jj_la1[i] = -1; |
2119 | - for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); |
2120 | - } |
2121 | - |
2122 | - /** Constructor with generated Token Manager. */ |
2123 | - public TAPAALQueryParser(TAPAALQueryParserTokenManager tm) { |
2124 | - token_source = tm; |
2125 | - token = new Token(); |
2126 | - jj_ntk = -1; |
2127 | - jj_gen = 0; |
2128 | - for (int i = 0; i < 9; i++) jj_la1[i] = -1; |
2129 | - for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); |
2130 | - } |
2131 | - |
2132 | - /** Reinitialise. */ |
2133 | - public void ReInit(TAPAALQueryParserTokenManager tm) { |
2134 | - token_source = tm; |
2135 | - token = new Token(); |
2136 | - jj_ntk = -1; |
2137 | - jj_gen = 0; |
2138 | - for (int i = 0; i < 9; i++) jj_la1[i] = -1; |
2139 | - for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); |
2140 | - } |
2141 | - |
2142 | - private Token jj_consume_token(int kind) throws ParseException { |
2143 | - Token oldToken; |
2144 | - if ((oldToken = token).next != null) token = token.next; |
2145 | - else token = token.next = token_source.getNextToken(); |
2146 | - jj_ntk = -1; |
2147 | - if (token.kind == kind) { |
2148 | - jj_gen++; |
2149 | - if (++jj_gc > 100) { |
2150 | - jj_gc = 0; |
2151 | - for (int i = 0; i < jj_2_rtns.length; i++) { |
2152 | - JJCalls c = jj_2_rtns[i]; |
2153 | - while (c != null) { |
2154 | - if (c.gen < jj_gen) c.first = null; |
2155 | - c = c.next; |
2156 | - } |
2157 | - } |
2158 | - } |
2159 | - return token; |
2160 | - } |
2161 | - token = oldToken; |
2162 | - jj_kind = kind; |
2163 | - throw generateParseException(); |
2164 | - } |
2165 | - |
2166 | - static private final class LookaheadSuccess extends java.lang.Error { } |
2167 | - final private LookaheadSuccess jj_ls = new LookaheadSuccess(); |
2168 | - private boolean jj_scan_token(int kind) { |
2169 | - if (jj_scanpos == jj_lastpos) { |
2170 | - jj_la--; |
2171 | - if (jj_scanpos.next == null) { |
2172 | - jj_lastpos = jj_scanpos = jj_scanpos.next = token_source.getNextToken(); |
2173 | - } else { |
2174 | - jj_lastpos = jj_scanpos = jj_scanpos.next; |
2175 | - } |
2176 | - } else { |
2177 | - jj_scanpos = jj_scanpos.next; |
2178 | - } |
2179 | - if (jj_rescan) { |
2180 | - int i = 0; Token tok = token; |
2181 | - while (tok != null && tok != jj_scanpos) { i++; tok = tok.next; } |
2182 | - if (tok != null) jj_add_error_token(kind, i); |
2183 | - } |
2184 | - if (jj_scanpos.kind != kind) return true; |
2185 | - if (jj_la == 0 && jj_scanpos == jj_lastpos) throw jj_ls; |
2186 | - return false; |
2187 | - } |
2188 | - |
2189 | - |
2190 | -/** Get the next Token. */ |
2191 | - final public Token getNextToken() { |
2192 | - if (token.next != null) token = token.next; |
2193 | - else token = token.next = token_source.getNextToken(); |
2194 | - jj_ntk = -1; |
2195 | - jj_gen++; |
2196 | - return token; |
2197 | - } |
2198 | - |
2199 | -/** Get the specific Token. */ |
2200 | - final public Token getToken(int index) { |
2201 | - Token t = token; |
2202 | - for (int i = 0; i < index; i++) { |
2203 | - if (t.next != null) t = t.next; |
2204 | - else t = t.next = token_source.getNextToken(); |
2205 | - } |
2206 | - return t; |
2207 | - } |
2208 | - |
2209 | - private int jj_ntk() { |
2210 | - if ((jj_nt=token.next) == null) |
2211 | - return (jj_ntk = (token.next=token_source.getNextToken()).kind); |
2212 | - else |
2213 | - return (jj_ntk = jj_nt.kind); |
2214 | - } |
2215 | - |
2216 | - private java.util.List<int[]> jj_expentries = new java.util.ArrayList<int[]>(); |
2217 | - private int[] jj_expentry; |
2218 | - private int jj_kind = -1; |
2219 | - private int[] jj_lasttokens = new int[100]; |
2220 | - private int jj_endpos; |
2221 | - |
2222 | - private void jj_add_error_token(int kind, int pos) { |
2223 | - if (pos >= 100) return; |
2224 | - if (pos == jj_endpos + 1) { |
2225 | - jj_lasttokens[jj_endpos++] = kind; |
2226 | - } else if (jj_endpos != 0) { |
2227 | - jj_expentry = new int[jj_endpos]; |
2228 | - for (int i = 0; i < jj_endpos; i++) { |
2229 | - jj_expentry[i] = jj_lasttokens[i]; |
2230 | - } |
2231 | - jj_entries_loop: for (java.util.Iterator<?> it = jj_expentries.iterator(); it.hasNext();) { |
2232 | - int[] oldentry = (int[])(it.next()); |
2233 | - if (oldentry.length == jj_expentry.length) { |
2234 | - for (int i = 0; i < jj_expentry.length; i++) { |
2235 | - if (oldentry[i] != jj_expentry[i]) { |
2236 | - continue jj_entries_loop; |
2237 | - } |
2238 | - } |
2239 | - jj_expentries.add(jj_expentry); |
2240 | - break jj_entries_loop; |
2241 | - } |
2242 | - } |
2243 | - if (pos != 0) jj_lasttokens[(jj_endpos = pos) - 1] = kind; |
2244 | - } |
2245 | - } |
2246 | - |
2247 | - /** Generate ParseException. */ |
2248 | - public ParseException generateParseException() { |
2249 | - jj_expentries.clear(); |
2250 | - boolean[] la1tokens = new boolean[23]; |
2251 | - if (jj_kind >= 0) { |
2252 | - la1tokens[jj_kind] = true; |
2253 | - jj_kind = -1; |
2254 | - } |
2255 | - for (int i = 0; i < 9; i++) { |
2256 | - if (jj_la1[i] == jj_gen) { |
2257 | - for (int j = 0; j < 32; j++) { |
2258 | - if ((jj_la1_0[i] & (1<<j)) != 0) { |
2259 | - la1tokens[j] = true; |
2260 | - } |
2261 | - } |
2262 | - } |
2263 | - } |
2264 | - for (int i = 0; i < 23; i++) { |
2265 | - if (la1tokens[i]) { |
2266 | - jj_expentry = new int[1]; |
2267 | - jj_expentry[0] = i; |
2268 | - jj_expentries.add(jj_expentry); |
2269 | - } |
2270 | - } |
2271 | - jj_endpos = 0; |
2272 | - jj_rescan_token(); |
2273 | - jj_add_error_token(0, 0); |
2274 | - int[][] exptokseq = new int[jj_expentries.size()][]; |
2275 | - for (int i = 0; i < jj_expentries.size(); i++) { |
2276 | - exptokseq[i] = jj_expentries.get(i); |
2277 | - } |
2278 | - return new ParseException(token, exptokseq, tokenImage); |
2279 | - } |
2280 | - |
2281 | - /** Enable tracing. */ |
2282 | - final public void enable_tracing() { |
2283 | - } |
2284 | - |
2285 | - /** Disable tracing. */ |
2286 | - final public void disable_tracing() { |
2287 | - } |
2288 | - |
2289 | - private void jj_rescan_token() { |
2290 | - jj_rescan = true; |
2291 | - for (int i = 0; i < 2; i++) { |
2292 | - try { |
2293 | - JJCalls p = jj_2_rtns[i]; |
2294 | - do { |
2295 | - if (p.gen > jj_gen) { |
2296 | - jj_la = p.arg; jj_lastpos = jj_scanpos = p.first; |
2297 | - switch (i) { |
2298 | - case 0: jj_3_1(); break; |
2299 | - case 1: jj_3_2(); break; |
2300 | - } |
2301 | - } |
2302 | - p = p.next; |
2303 | - } while (p != null); |
2304 | - } catch(LookaheadSuccess ls) { } |
2305 | - } |
2306 | - jj_rescan = false; |
2307 | - } |
2308 | - |
2309 | - private void jj_save(int index, int xla) { |
2310 | - JJCalls p = jj_2_rtns[index]; |
2311 | - while (p.gen > jj_gen) { |
2312 | - if (p.next == null) { p = p.next = new JJCalls(); break; } |
2313 | - p = p.next; |
2314 | - } |
2315 | - p.gen = jj_gen + xla - jj_la; p.first = token; p.arg = xla; |
2316 | - } |
2317 | - |
2318 | - static final class JJCalls { |
2319 | - int gen; |
2320 | - Token first; |
2321 | - int arg; |
2322 | - JJCalls next; |
2323 | - } |
2324 | + switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) { |
2325 | + case IDENT:{ |
2326 | + if (jj_2_2(2)) { |
2327 | + template = jj_consume_token(IDENT); |
2328 | + jj_consume_token(22); |
2329 | + } else { |
2330 | + ; |
2331 | + } |
2332 | + place = jj_consume_token(IDENT); |
2333 | + thisProp = new TCTLPlaceNode(template == null ? "" : template.image, place.image); |
2334 | + break; |
2335 | + } |
2336 | + case NUM:{ |
2337 | + num = jj_consume_token(NUM); |
2338 | + thisProp = new TCTLConstNode(Integer.parseInt(num.image)); |
2339 | + break; |
2340 | + } |
2341 | + case 20:{ |
2342 | + jj_consume_token(20); |
2343 | + thisProp = AritmeticExpr(); |
2344 | + jj_consume_token(21); |
2345 | + break; |
2346 | + } |
2347 | + default: |
2348 | + jj_la1[8] = jj_gen; |
2349 | + jj_consume_token(-1); |
2350 | + throw new ParseException(); |
2351 | + } |
2352 | + {if ("" != null) return thisProp;} |
2353 | + throw new Error("Missing return statement in function"); |
2354 | + } |
2355 | + |
2356 | + private boolean jj_2_1(int xla) |
2357 | + { |
2358 | + jj_la = xla; jj_lastpos = jj_scanpos = token; |
2359 | + try { return (!jj_3_1()); } |
2360 | + catch(LookaheadSuccess ls) { return true; } |
2361 | + finally { jj_save(0, xla); } |
2362 | + } |
2363 | + |
2364 | + private boolean jj_2_2(int xla) |
2365 | + { |
2366 | + jj_la = xla; jj_lastpos = jj_scanpos = token; |
2367 | + try { return (!jj_3_2()); } |
2368 | + catch(LookaheadSuccess ls) { return true; } |
2369 | + finally { jj_save(1, xla); } |
2370 | + } |
2371 | + |
2372 | + private boolean jj_3_2() |
2373 | + { |
2374 | + if (jj_scan_token(IDENT)) return true; |
2375 | + if (jj_scan_token(22)) return true; |
2376 | + return false; |
2377 | + } |
2378 | + |
2379 | + private boolean jj_3R_AritmeticFactor_256_17_11() |
2380 | + { |
2381 | + Token xsp; |
2382 | + xsp = jj_scanpos; |
2383 | + if (jj_3_2()) jj_scanpos = xsp; |
2384 | + if (jj_scan_token(IDENT)) return true; |
2385 | + return false; |
2386 | + } |
2387 | + |
2388 | + private boolean jj_3R_AritmeticExpr_215_9_6() |
2389 | + { |
2390 | + if (jj_3R_AritmeticTerm_234_9_7()) return true; |
2391 | + Token xsp; |
2392 | + while (true) { |
2393 | + xsp = jj_scanpos; |
2394 | + if (jj_3R_AritmeticExpr_218_17_8()) { jj_scanpos = xsp; break; } |
2395 | + } |
2396 | + return false; |
2397 | + } |
2398 | + |
2399 | + private boolean jj_3R_AritmeticTerm_234_9_7() |
2400 | + { |
2401 | + if (jj_3R_AritmeticFactor_255_9_9()) return true; |
2402 | + Token xsp; |
2403 | + while (true) { |
2404 | + xsp = jj_scanpos; |
2405 | + if (jj_3R_AritmeticTerm_237_17_10()) { jj_scanpos = xsp; break; } |
2406 | + } |
2407 | + return false; |
2408 | + } |
2409 | + |
2410 | + private boolean jj_3R_AritmeticFactor_255_9_9() |
2411 | + { |
2412 | + Token xsp; |
2413 | + xsp = jj_scanpos; |
2414 | + if (jj_3R_AritmeticFactor_256_17_11()) { |
2415 | + jj_scanpos = xsp; |
2416 | + if (jj_3R_AritmeticFactor_257_19_12()) { |
2417 | + jj_scanpos = xsp; |
2418 | + if (jj_3R_AritmeticFactor_258_19_13()) return true; |
2419 | + } |
2420 | + } |
2421 | + return false; |
2422 | + } |
2423 | + |
2424 | + private boolean jj_3_1() |
2425 | + { |
2426 | + if (jj_3R_AtomicProposition_200_9_5()) return true; |
2427 | + return false; |
2428 | + } |
2429 | + |
2430 | + private boolean jj_3R_AritmeticExpr_218_17_8() |
2431 | + { |
2432 | + if (jj_scan_token(PLUS)) return true; |
2433 | + if (jj_3R_AritmeticTerm_234_9_7()) return true; |
2434 | + return false; |
2435 | + } |
2436 | + |
2437 | + private boolean jj_3R_AtomicProposition_200_9_5() |
2438 | + { |
2439 | + if (jj_3R_AritmeticExpr_215_9_6()) return true; |
2440 | + if (jj_scan_token(OP)) return true; |
2441 | + if (jj_3R_AritmeticExpr_215_9_6()) return true; |
2442 | + return false; |
2443 | + } |
2444 | + |
2445 | + private boolean jj_3R_AritmeticFactor_258_19_13() |
2446 | + { |
2447 | + if (jj_scan_token(20)) return true; |
2448 | + if (jj_3R_AritmeticExpr_215_9_6()) return true; |
2449 | + if (jj_scan_token(21)) return true; |
2450 | + return false; |
2451 | + } |
2452 | + |
2453 | + private boolean jj_3R_AritmeticTerm_237_17_10() |
2454 | + { |
2455 | + if (jj_scan_token(MULT)) return true; |
2456 | + if (jj_3R_AritmeticFactor_255_9_9()) return true; |
2457 | + return false; |
2458 | + } |
2459 | + |
2460 | + private boolean jj_3R_AritmeticFactor_257_19_12() |
2461 | + { |
2462 | + if (jj_scan_token(NUM)) return true; |
2463 | + return false; |
2464 | + } |
2465 | + |
2466 | + /** Generated Token Manager. */ |
2467 | + public TAPAALQueryParserTokenManager token_source; |
2468 | + SimpleCharStream jj_input_stream; |
2469 | + /** Current token. */ |
2470 | + public Token token; |
2471 | + /** Next token. */ |
2472 | + public Token jj_nt; |
2473 | + private int jj_ntk; |
2474 | + private Token jj_scanpos, jj_lastpos; |
2475 | + private int jj_la; |
2476 | + private int jj_gen; |
2477 | + final private int[] jj_la1 = new int[9]; |
2478 | + static private int[] jj_la1_0; |
2479 | + static { |
2480 | + jj_la1_init_0(); |
2481 | + } |
2482 | + private static void jj_la1_init_0() { |
2483 | + jj_la1_0 = new int[] {0xf0,0x100,0x200,0x10640e,0xe,0x100000,0x800,0x1000,0x106000,}; |
2484 | + } |
2485 | + final private JJCalls[] jj_2_rtns = new JJCalls[2]; |
2486 | + private boolean jj_rescan = false; |
2487 | + private int jj_gc = 0; |
2488 | + |
2489 | + /** Constructor with InputStream. */ |
2490 | + public TAPAALQueryParser(java.io.InputStream stream) { |
2491 | + this(stream, null); |
2492 | + } |
2493 | + /** Constructor with InputStream and supplied encoding */ |
2494 | + public TAPAALQueryParser(java.io.InputStream stream, String encoding) { |
2495 | + try { jj_input_stream = new SimpleCharStream(stream, encoding, 1, 1); } catch(java.io.UnsupportedEncodingException e) { throw new RuntimeException(e); } |
2496 | + token_source = new TAPAALQueryParserTokenManager(jj_input_stream); |
2497 | + token = new Token(); |
2498 | + jj_ntk = -1; |
2499 | + jj_gen = 0; |
2500 | + for (int i = 0; i < 9; i++) jj_la1[i] = -1; |
2501 | + for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); |
2502 | + } |
2503 | + |
2504 | + /** Reinitialise. */ |
2505 | + public void ReInit(java.io.InputStream stream) { |
2506 | + ReInit(stream, null); |
2507 | + } |
2508 | + /** Reinitialise. */ |
2509 | + public void ReInit(java.io.InputStream stream, String encoding) { |
2510 | + try { jj_input_stream.ReInit(stream, encoding, 1, 1); } catch(java.io.UnsupportedEncodingException e) { throw new RuntimeException(e); } |
2511 | + token_source.ReInit(jj_input_stream); |
2512 | + token = new Token(); |
2513 | + jj_ntk = -1; |
2514 | + jj_gen = 0; |
2515 | + for (int i = 0; i < 9; i++) jj_la1[i] = -1; |
2516 | + for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); |
2517 | + } |
2518 | + |
2519 | + /** Constructor. */ |
2520 | + public TAPAALQueryParser(java.io.Reader stream) { |
2521 | + jj_input_stream = new SimpleCharStream(stream, 1, 1); |
2522 | + token_source = new TAPAALQueryParserTokenManager(jj_input_stream); |
2523 | + token = new Token(); |
2524 | + jj_ntk = -1; |
2525 | + jj_gen = 0; |
2526 | + for (int i = 0; i < 9; i++) jj_la1[i] = -1; |
2527 | + for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); |
2528 | + } |
2529 | + |
2530 | + /** Reinitialise. */ |
2531 | + public void ReInit(java.io.Reader stream) { |
2532 | + if (jj_input_stream == null) { |
2533 | + jj_input_stream = new SimpleCharStream(stream, 1, 1); |
2534 | + } else { |
2535 | + jj_input_stream.ReInit(stream, 1, 1); |
2536 | + } |
2537 | + if (token_source == null) { |
2538 | + token_source = new TAPAALQueryParserTokenManager(jj_input_stream); |
2539 | + } |
2540 | + |
2541 | + token_source.ReInit(jj_input_stream); |
2542 | + token = new Token(); |
2543 | + jj_ntk = -1; |
2544 | + jj_gen = 0; |
2545 | + for (int i = 0; i < 9; i++) jj_la1[i] = -1; |
2546 | + for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); |
2547 | + } |
2548 | + |
2549 | + /** Constructor with generated Token Manager. */ |
2550 | + public TAPAALQueryParser(TAPAALQueryParserTokenManager tm) { |
2551 | + token_source = tm; |
2552 | + token = new Token(); |
2553 | + jj_ntk = -1; |
2554 | + jj_gen = 0; |
2555 | + for (int i = 0; i < 9; i++) jj_la1[i] = -1; |
2556 | + for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); |
2557 | + } |
2558 | + |
2559 | + /** Reinitialise. */ |
2560 | + public void ReInit(TAPAALQueryParserTokenManager tm) { |
2561 | + token_source = tm; |
2562 | + token = new Token(); |
2563 | + jj_ntk = -1; |
2564 | + jj_gen = 0; |
2565 | + for (int i = 0; i < 9; i++) jj_la1[i] = -1; |
2566 | + for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); |
2567 | + } |
2568 | + |
2569 | + private Token jj_consume_token(int kind) throws ParseException { |
2570 | + Token oldToken; |
2571 | + if ((oldToken = token).next != null) token = token.next; |
2572 | + else token = token.next = token_source.getNextToken(); |
2573 | + jj_ntk = -1; |
2574 | + if (token.kind == kind) { |
2575 | + jj_gen++; |
2576 | + if (++jj_gc > 100) { |
2577 | + jj_gc = 0; |
2578 | + for (int i = 0; i < jj_2_rtns.length; i++) { |
2579 | + JJCalls c = jj_2_rtns[i]; |
2580 | + while (c != null) { |
2581 | + if (c.gen < jj_gen) c.first = null; |
2582 | + c = c.next; |
2583 | + } |
2584 | + } |
2585 | + } |
2586 | + return token; |
2587 | + } |
2588 | + token = oldToken; |
2589 | + jj_kind = kind; |
2590 | + throw generateParseException(); |
2591 | + } |
2592 | + |
2593 | + @SuppressWarnings("serial") |
2594 | + static private final class LookaheadSuccess extends java.lang.Error { |
2595 | + @Override |
2596 | + public Throwable fillInStackTrace() { |
2597 | + return this; |
2598 | + } |
2599 | + } |
2600 | + static private final LookaheadSuccess jj_ls = new LookaheadSuccess(); |
2601 | + private boolean jj_scan_token(int kind) { |
2602 | + if (jj_scanpos == jj_lastpos) { |
2603 | + jj_la--; |
2604 | + if (jj_scanpos.next == null) { |
2605 | + jj_lastpos = jj_scanpos = jj_scanpos.next = token_source.getNextToken(); |
2606 | + } else { |
2607 | + jj_lastpos = jj_scanpos = jj_scanpos.next; |
2608 | + } |
2609 | + } else { |
2610 | + jj_scanpos = jj_scanpos.next; |
2611 | + } |
2612 | + if (jj_rescan) { |
2613 | + int i = 0; Token tok = token; |
2614 | + while (tok != null && tok != jj_scanpos) { i++; tok = tok.next; } |
2615 | + if (tok != null) jj_add_error_token(kind, i); |
2616 | + } |
2617 | + if (jj_scanpos.kind != kind) return true; |
2618 | + if (jj_la == 0 && jj_scanpos == jj_lastpos) throw jj_ls; |
2619 | + return false; |
2620 | + } |
2621 | + |
2622 | + |
2623 | + /** Get the next Token. */ |
2624 | + final public Token getNextToken() { |
2625 | + if (token.next != null) token = token.next; |
2626 | + else token = token.next = token_source.getNextToken(); |
2627 | + jj_ntk = -1; |
2628 | + jj_gen++; |
2629 | + return token; |
2630 | + } |
2631 | + |
2632 | + /** Get the specific Token. */ |
2633 | + final public Token getToken(int index) { |
2634 | + Token t = token; |
2635 | + for (int i = 0; i < index; i++) { |
2636 | + if (t.next != null) t = t.next; |
2637 | + else t = t.next = token_source.getNextToken(); |
2638 | + } |
2639 | + return t; |
2640 | + } |
2641 | + |
2642 | + private int jj_ntk_f() { |
2643 | + if ((jj_nt=token.next) == null) |
2644 | + return (jj_ntk = (token.next=token_source.getNextToken()).kind); |
2645 | + else |
2646 | + return (jj_ntk = jj_nt.kind); |
2647 | + } |
2648 | + |
2649 | + private java.util.List<int[]> jj_expentries = new java.util.ArrayList<int[]>(); |
2650 | + private int[] jj_expentry; |
2651 | + private int jj_kind = -1; |
2652 | + private int[] jj_lasttokens = new int[100]; |
2653 | + private int jj_endpos; |
2654 | + |
2655 | + private void jj_add_error_token(int kind, int pos) { |
2656 | + if (pos >= 100) { |
2657 | + return; |
2658 | + } |
2659 | + |
2660 | + if (pos == jj_endpos + 1) { |
2661 | + jj_lasttokens[jj_endpos++] = kind; |
2662 | + } else if (jj_endpos != 0) { |
2663 | + jj_expentry = new int[jj_endpos]; |
2664 | + |
2665 | + for (int i = 0; i < jj_endpos; i++) { |
2666 | + jj_expentry[i] = jj_lasttokens[i]; |
2667 | + } |
2668 | + |
2669 | + for (int[] oldentry : jj_expentries) { |
2670 | + if (oldentry.length == jj_expentry.length) { |
2671 | + boolean isMatched = true; |
2672 | + |
2673 | + for (int i = 0; i < jj_expentry.length; i++) { |
2674 | + if (oldentry[i] != jj_expentry[i]) { |
2675 | + isMatched = false; |
2676 | + break; |
2677 | + } |
2678 | + |
2679 | + } |
2680 | + if (isMatched) { |
2681 | + jj_expentries.add(jj_expentry); |
2682 | + break; |
2683 | + } |
2684 | + } |
2685 | + } |
2686 | + |
2687 | + if (pos != 0) { |
2688 | + jj_lasttokens[(jj_endpos = pos) - 1] = kind; |
2689 | + } |
2690 | + } |
2691 | + } |
2692 | + |
2693 | + /** Generate ParseException. */ |
2694 | + public ParseException generateParseException() { |
2695 | + jj_expentries.clear(); |
2696 | + boolean[] la1tokens = new boolean[23]; |
2697 | + if (jj_kind >= 0) { |
2698 | + la1tokens[jj_kind] = true; |
2699 | + jj_kind = -1; |
2700 | + } |
2701 | + for (int i = 0; i < 9; i++) { |
2702 | + if (jj_la1[i] == jj_gen) { |
2703 | + for (int j = 0; j < 32; j++) { |
2704 | + if ((jj_la1_0[i] & (1<<j)) != 0) { |
2705 | + la1tokens[j] = true; |
2706 | + } |
2707 | + } |
2708 | + } |
2709 | + } |
2710 | + for (int i = 0; i < 23; i++) { |
2711 | + if (la1tokens[i]) { |
2712 | + jj_expentry = new int[1]; |
2713 | + jj_expentry[0] = i; |
2714 | + jj_expentries.add(jj_expentry); |
2715 | + } |
2716 | + } |
2717 | + jj_endpos = 0; |
2718 | + jj_rescan_token(); |
2719 | + jj_add_error_token(0, 0); |
2720 | + int[][] exptokseq = new int[jj_expentries.size()][]; |
2721 | + for (int i = 0; i < jj_expentries.size(); i++) { |
2722 | + exptokseq[i] = jj_expentries.get(i); |
2723 | + } |
2724 | + return new ParseException(token, exptokseq, tokenImage); |
2725 | + } |
2726 | + |
2727 | + private boolean trace_enabled; |
2728 | + |
2729 | + /** Trace enabled. */ |
2730 | + final public boolean trace_enabled() { |
2731 | + return trace_enabled; |
2732 | + } |
2733 | + |
2734 | + /** Enable tracing. */ |
2735 | + final public void enable_tracing() { |
2736 | + } |
2737 | + |
2738 | + /** Disable tracing. */ |
2739 | + final public void disable_tracing() { |
2740 | + } |
2741 | + |
2742 | + private void jj_rescan_token() { |
2743 | + jj_rescan = true; |
2744 | + for (int i = 0; i < 2; i++) { |
2745 | + try { |
2746 | + JJCalls p = jj_2_rtns[i]; |
2747 | + |
2748 | + do { |
2749 | + if (p.gen > jj_gen) { |
2750 | + jj_la = p.arg; jj_lastpos = jj_scanpos = p.first; |
2751 | + switch (i) { |
2752 | + case 0: jj_3_1(); break; |
2753 | + case 1: jj_3_2(); break; |
2754 | + } |
2755 | + } |
2756 | + p = p.next; |
2757 | + } while (p != null); |
2758 | + |
2759 | + } catch(LookaheadSuccess ls) { } |
2760 | + } |
2761 | + jj_rescan = false; |
2762 | + } |
2763 | + |
2764 | + private void jj_save(int index, int xla) { |
2765 | + JJCalls p = jj_2_rtns[index]; |
2766 | + while (p.gen > jj_gen) { |
2767 | + if (p.next == null) { p = p.next = new JJCalls(); break; } |
2768 | + p = p.next; |
2769 | + } |
2770 | + |
2771 | + p.gen = jj_gen + xla - jj_la; |
2772 | + p.first = token; |
2773 | + p.arg = xla; |
2774 | + } |
2775 | + |
2776 | + static final class JJCalls { |
2777 | + int gen; |
2778 | + Token first; |
2779 | + int arg; |
2780 | + JJCalls next; |
2781 | + } |
2782 | |
2783 | } |
2784 | |
2785 | === modified file 'src/dk/aau/cs/TCTL/TCTLEFNode.java' |
2786 | --- src/dk/aau/cs/TCTL/TCTLEFNode.java 2020-11-06 19:41:50 +0000 |
2787 | +++ src/dk/aau/cs/TCTL/TCTLEFNode.java 2021-09-29 07:20:55 +0000 |
2788 | @@ -2,6 +2,8 @@ |
2789 | |
2790 | import dk.aau.cs.TCTL.visitors.ITCTLVisitor; |
2791 | |
2792 | +import java.util.HashMap; |
2793 | + |
2794 | public class TCTLEFNode extends TCTLAbstractPathProperty { |
2795 | |
2796 | private TCTLAbstractStateProperty property; |
2797 | @@ -104,7 +106,6 @@ |
2798 | @Override |
2799 | public TCTLAbstractProperty findFirstPlaceHolder() { |
2800 | return property.findFirstPlaceHolder(); |
2801 | - |
2802 | } |
2803 | |
2804 | } |
2805 | |
2806 | === modified file 'src/pipe/gui/widgets/QueryDialog.java' |
2807 | --- src/pipe/gui/widgets/QueryDialog.java 2021-09-11 17:11:34 +0000 |
2808 | +++ src/pipe/gui/widgets/QueryDialog.java 2021-09-29 07:20:55 +0000 |
2809 | @@ -2326,42 +2326,37 @@ |
2810 | |
2811 | if (newQuery != null) // new query parsed successfully |
2812 | { |
2813 | - // check correct place names are used in atomic propositions |
2814 | - ArrayList<Tuple<String,String>> templatePlaceNames = new ArrayList<Tuple<String,String>>(); |
2815 | - for(TimedArcPetriNet tapn : tapnNetwork.activeTemplates()) { |
2816 | - for(TimedPlace p : tapn.places()) { |
2817 | - if (lens.isTimed() || !p.isShared() || lens.isGame()) { |
2818 | - templatePlaceNames.add(new Tuple<String, String>(tapn.name(), p.name())); |
2819 | - } |
2820 | - } |
2821 | - } |
2822 | - |
2823 | - for(TimedPlace p : tapnNetwork.sharedPlaces()) { |
2824 | - templatePlaceNames.add(new Tuple<String, String>("", p.name())); |
2825 | - } |
2826 | - |
2827 | - FixAbbrivPlaceNames.fixAbbrivPlaceNames(templatePlaceNames, newQuery); |
2828 | - VerifyPlaceNamesVisitor nameChecker = new VerifyPlaceNamesVisitor(templatePlaceNames); |
2829 | - VerifyPlaceNamesVisitor.Context c = nameChecker.verifyPlaceNames(newQuery); |
2830 | + VerifyPlaceNamesVisitor.Context placeContext = getPlaceContext(newQuery); |
2831 | + VerifyTransitionNamesVisitor.Context transitionContext = getTransitionContext(newQuery); |
2832 | |
2833 | boolean isResultFalse; |
2834 | |
2835 | if (lens.isTimed() || lens.isGame()) { |
2836 | - isResultFalse = !c.getResult(); |
2837 | + isResultFalse = !placeContext.getResult(); |
2838 | } else { |
2839 | - isResultFalse = checkUntimedResult(newQuery) && !c.getResult(); |
2840 | + isResultFalse = !transitionContext.getResult() || !placeContext.getResult(); |
2841 | } |
2842 | |
2843 | if (isResultFalse) { |
2844 | StringBuilder s = new StringBuilder(); |
2845 | +<<<<<<< TREE |
2846 | s.append("The following places" + (lens.isTimed() ? "" : " or transitions") + |
2847 | " were used in the query, but are not present in your model:\n\n"); |
2848 | +======= |
2849 | + s.append("The following places " + (lens.isTimed() ? "" : "or transitions") + |
2850 | + " were used in the query, but are not present in your model:\n\n"); |
2851 | +>>>>>>> MERGE-SOURCE |
2852 | |
2853 | - for (String placeName : c.getIncorrectPlaceNames()) { |
2854 | + for (String placeName : placeContext.getIncorrectPlaceNames()) { |
2855 | s.append(placeName); |
2856 | s.append('\n'); |
2857 | } |
2858 | |
2859 | + for (String transitionName : transitionContext.getIncorrectTransitionNames()) { |
2860 | + s.append(transitionName); |
2861 | + s.append('\n'); |
2862 | + } |
2863 | + |
2864 | s.append("\nThe specified query has not been saved. Do you want to edit it again?"); |
2865 | int choice = JOptionPane.showConfirmDialog( |
2866 | CreateGui.getApp(), s.toString(), |
2867 | @@ -2442,25 +2437,44 @@ |
2868 | queryPanel.add(editingButtonPanel, gbc); |
2869 | } |
2870 | |
2871 | - private boolean checkUntimedResult(TCTLAbstractProperty newQuery) { |
2872 | + private VerifyPlaceNamesVisitor.Context getPlaceContext(TCTLAbstractProperty newQuery) { |
2873 | + // check correct place names are used in atomic propositions |
2874 | + ArrayList<Tuple<String,String>> templatePlaceNames = new ArrayList<Tuple<String,String>>(); |
2875 | + for(TimedArcPetriNet tapn : tapnNetwork.activeTemplates()) { |
2876 | + for(TimedPlace p : tapn.places()) { |
2877 | + if (lens.isTimed() || !p.isShared() || lens.isGame()) { |
2878 | + templatePlaceNames.add(new Tuple<String, String>(tapn.name(), p.name())); |
2879 | + } |
2880 | + } |
2881 | + } |
2882 | + |
2883 | + for(TimedPlace p : tapnNetwork.sharedPlaces()) { |
2884 | + templatePlaceNames.add(new Tuple<String, String>("", p.name())); |
2885 | + } |
2886 | + |
2887 | + FixAbbrivPlaceNames.fixAbbrivPlaceNames(templatePlaceNames, newQuery); |
2888 | + VerifyPlaceNamesVisitor nameChecker = new VerifyPlaceNamesVisitor(templatePlaceNames); |
2889 | + return nameChecker.verifyPlaceNames(newQuery); |
2890 | + } |
2891 | + |
2892 | + private VerifyTransitionNamesVisitor.Context getTransitionContext(TCTLAbstractProperty newQuery) { |
2893 | // check correct transition names are used in atomic propositions |
2894 | - ArrayList<Tuple<String, String>> templateTransitionNames = new ArrayList<Tuple<String, String>>(); |
2895 | + ArrayList<Tuple<String,String>> templateTransitionNames = new ArrayList<Tuple<String,String>>(); |
2896 | for (TimedArcPetriNet tapn : tapnNetwork.activeTemplates()) { |
2897 | for (TimedTransition t : tapn.transitions()) { |
2898 | - if (!t.isShared()) { |
2899 | - templateTransitionNames.add(new Tuple<String, String>(tapn.name(), t.name())); |
2900 | + if (lens.isTimed() || !t.isShared() || lens.isGame()) { |
2901 | + templateTransitionNames.add(new Tuple<>(tapn.name(), t.name())); |
2902 | } |
2903 | } |
2904 | } |
2905 | |
2906 | for (SharedTransition t : tapnNetwork.sharedTransitions()) { |
2907 | - templateTransitionNames.add(new Tuple<String, String>("", t.name())); |
2908 | + templateTransitionNames.add(new Tuple<>("", t.name())); |
2909 | } |
2910 | |
2911 | FixAbbrivTransitionNames.fixAbbrivTransitionNames(templateTransitionNames, newQuery); |
2912 | - VerifyTransitionNamesVisitor transitionNameChecker = new VerifyTransitionNamesVisitor(templateTransitionNames); |
2913 | - VerifyTransitionNamesVisitor.Context c2 = transitionNameChecker.verifyTransitionNames(newQuery); |
2914 | - return !c2.getResult(); |
2915 | + VerifyTransitionNamesVisitor nameChecker = new VerifyTransitionNamesVisitor(templateTransitionNames); |
2916 | + return nameChecker.verifyTransitionNames(newQuery); |
2917 | } |
2918 | |
2919 | private void initUppaalOptionsPanel() { |
2920 | |
2921 | === modified file 'src/resources/TCTLParser/TAPAALCTLQueryParser.jj' |
2922 | --- src/resources/TCTLParser/TAPAALCTLQueryParser.jj 2017-09-05 21:24:23 +0000 |
2923 | +++ src/resources/TCTLParser/TAPAALCTLQueryParser.jj 2021-09-29 07:20:55 +0000 |
2924 | @@ -56,7 +56,7 @@ |
2925 | |
2926 | public static TCTLAbstractPathProperty parse(String query) throws ParseException { |
2927 | TAPAALCTLQueryParser parser = new TAPAALCTLQueryParser(new StringReader(query)); |
2928 | - return parser.AbstractPathProperty(); |
2929 | + return parser.Start(); |
2930 | } |
2931 | } |
2932 | |
2933 | @@ -131,6 +131,16 @@ |
2934 | } |
2935 | |
2936 | /** Root production. */ |
2937 | +TCTLAbstractPathProperty Start() : |
2938 | +{ |
2939 | + TCTLAbstractPathProperty child = null; |
2940 | +} |
2941 | +{ |
2942 | + ( |
2943 | + child = AbstractPathProperty() <EOF> {return child;} |
2944 | + ) |
2945 | +} |
2946 | + |
2947 | TCTLAbstractPathProperty AbstractPathProperty() : |
2948 | { |
2949 | TCTLAbstractStateProperty child = null; |
2950 | |
2951 | === modified file 'src/resources/TCTLParser/TAPAALQueryParser.jj' |
2952 | --- src/resources/TCTLParser/TAPAALQueryParser.jj 2014-05-22 20:26:41 +0000 |
2953 | +++ src/resources/TCTLParser/TAPAALQueryParser.jj 2021-09-29 07:20:55 +0000 |
2954 | @@ -49,7 +49,7 @@ |
2955 | |
2956 | public static TCTLAbstractProperty parse(String query) throws ParseException { |
2957 | TAPAALQueryParser parser = new TAPAALQueryParser(new StringReader(query)); |
2958 | - return parser.AbstractProperty(); |
2959 | + return parser.Start(); |
2960 | } |
2961 | } |
2962 | |
2963 | @@ -112,6 +112,16 @@ |
2964 | } |
2965 | |
2966 | /** Root production. */ |
2967 | +TCTLAbstractProperty Start() : |
2968 | +{ |
2969 | + TCTLAbstractProperty child = null; |
2970 | +} |
2971 | +{ |
2972 | + ( |
2973 | + child = AbstractProperty() <EOF> {return child;} |
2974 | + ) |
2975 | +} |
2976 | + |
2977 | TCTLAbstractProperty AbstractProperty() : |
2978 | { |
2979 | TCTLAbstractStateProperty child = null; |
What problem is this branch fixing?