Merge lp:~tapaal-contributor/tapaal/manual-edit-parsing into lp:tapaal

[Lena Ernstsen]

Ensures that everything in the query is parsed

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)]

What problem is this branch fixing?

review: Needs Information

[Lena Ernstsen (lsaid)]

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)]

review: Approve (code)

[Jiri Srba (srba)]

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)

review: Needs Fixing

[lp:~tapaal-contributor/tapaal/manual-edit-parsing]

1140. By Lena Ernstsen on 2021-09-29

Fixed spacing and missing transition names in manual edit error message

1141. By Lena Ernstsen on 2021-09-29

Merged trunk

Unmerged revisions

=== modified file 'src/dk/aau/cs/TCTL/CTLParsing/TAPAALCTLQueryParser.java'
--- src/dk/aau/cs/TCTL/CTLParsing/TAPAALCTLQueryParser.java	2019-03-22 10:13:18 +0000
+++ src/dk/aau/cs/TCTL/CTLParsing/TAPAALCTLQueryParser.java	2021-09-29 07:20:55 +0000
@@ -1,3 +1,4 @@
+/* TAPAALCTLQueryParser.java */
 /* Generated By:JavaCC: Do not edit this line. TAPAALCTLQueryParser.java */
 package dk.aau.cs.TCTL.CTLParsing;
 
@@ -13,6 +14,7 @@
 import dk.aau.cs.TCTL.TCTLAGNode;
 import dk.aau.cs.TCTL.TCTLAUNode;
 import dk.aau.cs.TCTL.TCTLAXNode;
+import dk.aau.cs.TCTL.TCTLAbstractProperty;
 import dk.aau.cs.TCTL.TCTLAbstractStateProperty;
 import dk.aau.cs.TCTL.TCTLAbstractPathProperty;
 import dk.aau.cs.TCTL.TCTLAndListNode;
@@ -31,714 +33,786 @@
 
 public class TAPAALCTLQueryParser implements TAPAALCTLQueryParserConstants {
 
-        private static final String ERROR_PARSING_QUERY_MESSAGE = "TAPAAL countered an error trying to parse the query";
-
-        public static TCTLAbstractPathProperty parse(String query) throws ParseException {
-                TAPAALCTLQueryParser parser = new TAPAALCTLQueryParser(new StringReader(query));
-                return parser.AbstractPathProperty();
-        }
-
-/** Root production. */
-  final public TCTLAbstractPathProperty AbstractPathProperty() throws ParseException {
-        TCTLAbstractStateProperty child = null;
+    private static final String ERROR_PARSING_QUERY_MESSAGE = "TAPAAL countered an error trying to parse the query";
+
+    public static TCTLAbstractPathProperty parse(String query) throws ParseException {
+        TAPAALCTLQueryParser parser = new TAPAALCTLQueryParser(new StringReader(query));
+        return parser.Start();
+    }
+
+    /** Root production. */
+    final public TCTLAbstractPathProperty Start() throws ParseException {TCTLAbstractPathProperty child = null;
+        child = AbstractPathProperty();
+        jj_consume_token(0);
+        {if ("" != null) return child;}
+        throw new Error("Missing return statement in function");
+    }
+
+    final public TCTLAbstractPathProperty AbstractPathProperty() throws ParseException {TCTLAbstractStateProperty child = null;
         TCTLAbstractStateProperty child2 = null;
-    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
-    case EF:
-      jj_consume_token(EF);
-      child = OrExpr();
-                                       {if (true) return new TCTLEFNode(child);}
-      break;
-    case EG:
-      jj_consume_token(EG);
-      child = OrExpr();
-                                         {if (true) return new TCTLEGNode(child);}
-      break;
-    case EX:
-      jj_consume_token(EX);
-      child = OrExpr();
-                                         {if (true) return new TCTLEXNode(child);}
-      break;
-    case E:
-      jj_consume_token(E);
-      jj_consume_token(26);
-      child = OrExpr();
-      jj_consume_token(U);
-      child2 = OrExpr();
-      jj_consume_token(27);
-                                                               {if (true) return new TCTLEUNode(child, child2);}
-      break;
-    case AF:
-      jj_consume_token(AF);
-      child = OrExpr();
-                                         {if (true) return new TCTLAFNode(child);}
-      break;
-    case AG:
-      jj_consume_token(AG);
-      child = OrExpr();
-                                         {if (true) return new TCTLAGNode(child);}
-      break;
-    case A:
-      jj_consume_token(A);
-      jj_consume_token(26);
-      child = OrExpr();
-      jj_consume_token(U);
-      child2 = OrExpr();
-      jj_consume_token(27);
-                                                               {if (true) return new TCTLAUNode(child, child2);}
-      break;
-    case AX:
-      jj_consume_token(AX);
-      child = OrExpr();
-                                         {if (true) return new TCTLAXNode(child);}
-      break;
-    default:
-      jj_la1[0] = jj_gen;
-      child = OrExpr();
-                             {if (true) return new TCTLStateToPathConverter(child);}
+        switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
+            case EF:{
+                jj_consume_token(EF);
+                child = OrExpr();
+                {if ("" != null) return new TCTLEFNode(child);}
+                break;
+            }
+            case EG:{
+                jj_consume_token(EG);
+                child = OrExpr();
+                {if ("" != null) return new TCTLEGNode(child);}
+                break;
+            }
+            case EX:{
+                jj_consume_token(EX);
+                child = OrExpr();
+                {if ("" != null) return new TCTLEXNode(child);}
+                break;
+            }
+            case E:{
+                jj_consume_token(E);
+                jj_consume_token(26);
+                child = OrExpr();
+                jj_consume_token(U);
+                child2 = OrExpr();
+                jj_consume_token(27);
+                {if ("" != null) return new TCTLEUNode(child, child2);}
+                break;
+            }
+            case AF:{
+                jj_consume_token(AF);
+                child = OrExpr();
+                {if ("" != null) return new TCTLAFNode(child);}
+                break;
+            }
+            case AG:{
+                jj_consume_token(AG);
+                child = OrExpr();
+                {if ("" != null) return new TCTLAGNode(child);}
+                break;
+            }
+            case A:{
+                jj_consume_token(A);
+                jj_consume_token(26);
+                child = OrExpr();
+                jj_consume_token(U);
+                child2 = OrExpr();
+                jj_consume_token(27);
+                {if ("" != null) return new TCTLAUNode(child, child2);}
+                break;
+            }
+            case AX:{
+                jj_consume_token(AX);
+                child = OrExpr();
+                {if ("" != null) return new TCTLAXNode(child);}
+                break;
+            }
+            default:
+                jj_la1[0] = jj_gen;
+                child = OrExpr();
+            {if ("" != null) return new TCTLStateToPathConverter(child);}
+        }
+        throw new Error("Missing return statement in function");
     }
-    throw new Error("Missing return statement in function");
-  }
 
-  final public TCTLAbstractStateProperty OrExpr() throws ParseException {
-        TCTLAbstractStateProperty currentChild;
+    final public TCTLAbstractStateProperty OrExpr() throws ParseException {TCTLAbstractStateProperty currentChild;
         ArrayList<TCTLAbstractStateProperty> disjunctions = new ArrayList<TCTLAbstractStateProperty>();
-    currentChild = AndExpr();
-          disjunctions.add(currentChild);
-    label_1:
-    while (true) {
-      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
-      case OR:
-        ;
-        break;
-      default:
-        jj_la1[1] = jj_gen;
-        break label_1;
-      }
-      jj_consume_token(OR);
-      currentChild = AndExpr();
-                  disjunctions.add(currentChild);
+        currentChild = AndExpr();
+        disjunctions.add(currentChild);
+        label_1:
+        while (true) {
+            switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
+                case OR:{
+                    ;
+                    break;
+                }
+                default:
+                    jj_la1[1] = jj_gen;
+                    break label_1;
+            }
+            jj_consume_token(OR);
+            currentChild = AndExpr();
+            disjunctions.add(currentChild);
+        }
+        {if ("" != null) return disjunctions.size() == 1 ? currentChild : new TCTLOrListNode(disjunctions);}
+        throw new Error("Missing return statement in function");
     }
-          {if (true) return disjunctions.size() == 1 ? currentChild : new TCTLOrListNode(disjunctions);}
-    throw new Error("Missing return statement in function");
-  }
 
-  final public TCTLAbstractStateProperty AndExpr() throws ParseException {
-        TCTLAbstractStateProperty currentChild;
+    final public TCTLAbstractStateProperty AndExpr() throws ParseException {TCTLAbstractStateProperty currentChild;
         ArrayList<TCTLAbstractStateProperty> conjunctions = new ArrayList<TCTLAbstractStateProperty>();
-    currentChild = NotExpr();
-          conjunctions.add(currentChild);
-    label_2:
-    while (true) {
-      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
-      case AND:
-        ;
-        break;
-      default:
-        jj_la1[2] = jj_gen;
-        break label_2;
-      }
-      jj_consume_token(AND);
-      currentChild = NotExpr();
-                  conjunctions.add(currentChild);
+        currentChild = NotExpr();
+        conjunctions.add(currentChild);
+        label_2:
+        while (true) {
+            switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
+                case AND:{
+                    ;
+                    break;
+                }
+                default:
+                    jj_la1[2] = jj_gen;
+                    break label_2;
+            }
+            jj_consume_token(AND);
+            currentChild = NotExpr();
+            conjunctions.add(currentChild);
+        }
+        {if ("" != null) return conjunctions.size() == 1 ? currentChild : new TCTLAndListNode(conjunctions);}
+        throw new Error("Missing return statement in function");
     }
-          {if (true) return conjunctions.size() == 1 ? currentChild : new TCTLAndListNode(conjunctions);}
-    throw new Error("Missing return statement in function");
-  }
 
-  final public TCTLAbstractStateProperty NotExpr() throws ParseException {
-        TCTLAbstractStateProperty child;
+    final public TCTLAbstractStateProperty NotExpr() throws ParseException {TCTLAbstractStateProperty child;
         TCTLAbstractPathProperty childConverter;
-    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
-    case NOT:
-      jj_consume_token(NOT);
-      jj_consume_token(26);
-      child = OrExpr();
-      jj_consume_token(27);
-                                         {if (true) return new TCTLNotNode(child);}
-      break;
-    default:
-      jj_la1[3] = jj_gen;
-      child = Factor();
-                             {if (true) return child;}
+        switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
+            case NOT:{
+                jj_consume_token(NOT);
+                jj_consume_token(26);
+                child = OrExpr();
+                jj_consume_token(27);
+                {if ("" != null) return new TCTLNotNode(child);}
+                break;
+            }
+            default:
+                jj_la1[3] = jj_gen;
+                child = Factor();
+            {if ("" != null) return child;}
+        }
+        throw new Error("Missing return statement in function");
     }
-    throw new Error("Missing return statement in function");
-  }
 
-  final public TCTLAbstractStateProperty Factor() throws ParseException {
-        TCTLAbstractStateProperty thisProp;
+    final public TCTLAbstractStateProperty Factor() throws ParseException {TCTLAbstractStateProperty thisProp;
         Token temp = null;
         Token transition;
-    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
-    case TRUE:
-      jj_consume_token(TRUE);
-                        thisProp = new TCTLTrueNode();
-      break;
-    case FALSE:
-      jj_consume_token(FALSE);
-                           thisProp = new TCTLFalseNode();
-      break;
-    case DEADLOCK:
-      jj_consume_token(DEADLOCK);
-                              thisProp = new TCTLDeadlockNode();
-      break;
-    default:
-      jj_la1[4] = jj_gen;
-      if (jj_2_2(2147483647)) {
-        thisProp = AtomicProposition();
-      } else {
-        switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
-        case IDENT:
-          if (jj_2_1(2)) {
-            temp = jj_consume_token(IDENT);
-            jj_consume_token(28);
-          } else {
-            ;
-          }
-          transition = jj_consume_token(IDENT);
-                thisProp = new TCTLTransitionNode(temp == null ? "" : temp.image, transition.image);
-          break;
-        case 26:
-          jj_consume_token(26);
-          thisProp = OrExpr();
-          jj_consume_token(27);
-          break;
-        default:
-          jj_la1[5] = jj_gen;
-                thisProp = new TCTLPathToStateConverter(AbstractPathProperty());
+        switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
+            case TRUE:{
+                jj_consume_token(TRUE);
+                thisProp = new TCTLTrueNode();
+                break;
+            }
+            case FALSE:{
+                jj_consume_token(FALSE);
+                thisProp = new TCTLFalseNode();
+                break;
+            }
+            case DEADLOCK:{
+                jj_consume_token(DEADLOCK);
+                thisProp = new TCTLDeadlockNode();
+                break;
+            }
+            default:
+                jj_la1[4] = jj_gen;
+                if (jj_2_2(2147483647)) {
+                    thisProp = AtomicProposition();
+                } else {
+                    switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
+                        case IDENT:{
+                            if (jj_2_1(2)) {
+                                temp = jj_consume_token(IDENT);
+                                jj_consume_token(28);
+                            } else {
+                                ;
+                            }
+                            transition = jj_consume_token(IDENT);
+                            thisProp = new TCTLTransitionNode(temp == null ? "" : temp.image, transition.image);
+                            break;
+                        }
+                        case 26:{
+                            jj_consume_token(26);
+                            thisProp = OrExpr();
+                            jj_consume_token(27);
+                            break;
+                        }
+                        default:
+                            jj_la1[5] = jj_gen;
+                            thisProp = new TCTLPathToStateConverter(AbstractPathProperty());
+                    }
+                }
         }
-      }
+        {if ("" != null) return thisProp;}
+        throw new Error("Missing return statement in function");
     }
-          {if (true) return thisProp;}
-    throw new Error("Missing return statement in function");
-  }
 
-  final public TCTLAbstractStateProperty AtomicProposition() throws ParseException {
-        TCTLAbstractStateProperty left;
+    final public TCTLAbstractStateProperty AtomicProposition() throws ParseException {TCTLAbstractStateProperty left;
         TCTLAbstractStateProperty right;
         Token op;
-    left = AritmeticExpr();
-    op = jj_consume_token(OP);
-    right = AritmeticExpr();
-                {if (true) return new TCTLAtomicPropositionNode(left, op.image, right);}
-    throw new Error("Missing return statement in function");
-  }
-
-  final public TCTLAbstractStateProperty AritmeticExpr() throws ParseException {
-        TCTLAbstractStateProperty currentChild;
-        ArrayList<TCTLAbstractStateProperty> terms = new ArrayList<TCTLAbstractStateProperty>();
-        Token op;
-    currentChild = AritmeticMinusExpr();
-          terms.add(currentChild);
-    label_3:
-    while (true) {
-      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
-      case PLUS:
-        ;
-        break;
-      default:
-        jj_la1[6] = jj_gen;
-        break label_3;
-      }
-      op = jj_consume_token(PLUS);
-      currentChild = AritmeticMinusExpr();
-                        terms.add(new AritmeticOperator(op.image));
-                        terms.add(currentChild);
-    }
-          {if (true) return terms.size() == 1 ? currentChild : new TCTLTermListNode(terms);}
-    throw new Error("Missing return statement in function");
-  }
-
-  final public TCTLAbstractStateProperty AritmeticMinusExpr() throws ParseException {
-        TCTLAbstractStateProperty currentChild;
-        ArrayList<TCTLAbstractStateProperty> terms = new ArrayList<TCTLAbstractStateProperty>();
-        Token op;
-    currentChild = AritmeticTerm();
-          terms.add(currentChild);
-    label_4:
-    while (true) {
-      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
-      case MINUS:
-        ;
-        break;
-      default:
-        jj_la1[7] = jj_gen;
-        break label_4;
-      }
-      op = jj_consume_token(MINUS);
-      currentChild = AritmeticTerm();
-                        terms.add(new AritmeticOperator(op.image));
-                        terms.add(currentChild);
-    }
-          {if (true) return terms.size() == 1 ? currentChild : new TCTLTermListNode(terms);}
-    throw new Error("Missing return statement in function");
-  }
-
-  final public TCTLAbstractStateProperty AritmeticTerm() throws ParseException {
-        TCTLAbstractStateProperty currentChild;
+        left = AritmeticExpr();
+        op = jj_consume_token(OP);
+        right = AritmeticExpr();
+        {if ("" != null) return new TCTLAtomicPropositionNode(left, op.image, right);}
+        throw new Error("Missing return statement in function");
+    }
+
+    final public TCTLAbstractStateProperty AritmeticExpr() throws ParseException {TCTLAbstractStateProperty currentChild;
+        ArrayList<TCTLAbstractStateProperty> terms = new ArrayList<TCTLAbstractStateProperty>();
+        Token op;
+        currentChild = AritmeticMinusExpr();
+        terms.add(currentChild);
+        label_3:
+        while (true) {
+            switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
+                case PLUS:{
+                    ;
+                    break;
+                }
+                default:
+                    jj_la1[6] = jj_gen;
+                    break label_3;
+            }
+            op = jj_consume_token(PLUS);
+            currentChild = AritmeticMinusExpr();
+            terms.add(new AritmeticOperator(op.image));
+            terms.add(currentChild);
+        }
+        {if ("" != null) return terms.size() == 1 ? currentChild : new TCTLTermListNode(terms);}
+        throw new Error("Missing return statement in function");
+    }
+
+    final public TCTLAbstractStateProperty AritmeticMinusExpr() throws ParseException {TCTLAbstractStateProperty currentChild;
+        ArrayList<TCTLAbstractStateProperty> terms = new ArrayList<TCTLAbstractStateProperty>();
+        Token op;
+        currentChild = AritmeticTerm();
+        terms.add(currentChild);
+        label_4:
+        while (true) {
+            switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
+                case MINUS:{
+                    ;
+                    break;
+                }
+                default:
+                    jj_la1[7] = jj_gen;
+                    break label_4;
+            }
+            op = jj_consume_token(MINUS);
+            currentChild = AritmeticTerm();
+            terms.add(new AritmeticOperator(op.image));
+            terms.add(currentChild);
+        }
+        {if ("" != null) return terms.size() == 1 ? currentChild : new TCTLTermListNode(terms);}
+        throw new Error("Missing return statement in function");
+    }
+
+    final public TCTLAbstractStateProperty AritmeticTerm() throws ParseException {TCTLAbstractStateProperty currentChild;
         ArrayList<TCTLAbstractStateProperty> factors = new ArrayList<TCTLAbstractStateProperty>();
         Token op;
-    currentChild = AritmeticFactor();
-          factors.add(currentChild);
-    label_5:
-    while (true) {
-      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
-      case MULT:
-        ;
-        break;
-      default:
-        jj_la1[8] = jj_gen;
-        break label_5;
-      }
-      op = jj_consume_token(MULT);
-      currentChild = AritmeticFactor();
-                        factors.add(new AritmeticOperator(op.image));
-                        factors.add(currentChild);
+        currentChild = AritmeticFactor();
+        factors.add(currentChild);
+        label_5:
+        while (true) {
+            switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
+                case MULT:{
+                    ;
+                    break;
+                }
+                default:
+                    jj_la1[8] = jj_gen;
+                    break label_5;
+            }
+            op = jj_consume_token(MULT);
+            currentChild = AritmeticFactor();
+            factors.add(new AritmeticOperator(op.image));
+            factors.add(currentChild);
+        }
+        {if ("" != null) return factors.size() == 1 ? currentChild : new TCTLTermListNode(factors);}
+        throw new Error("Missing return statement in function");
     }
-          {if (true) return factors.size() == 1 ? currentChild : new TCTLTermListNode(factors);}
-    throw new Error("Missing return statement in function");
-  }
 
-  final public TCTLAbstractStateProperty AritmeticFactor() throws ParseException {
-        TCTLAbstractStateProperty thisProp;
+    final public TCTLAbstractStateProperty AritmeticFactor() throws ParseException {TCTLAbstractStateProperty thisProp;
         Token temp = null;
         Token place;
         Token op;
         Token num;
-    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
-    case IDENT:
-      if (jj_2_3(2)) {
-        temp = jj_consume_token(IDENT);
-        jj_consume_token(28);
-      } else {
-        ;
-      }
-      place = jj_consume_token(IDENT);
-                                                                      thisProp = new TCTLPlaceNode(temp == null ? "" : temp.image, place.image);
-      break;
-    case NUM:
-      num = jj_consume_token(NUM);
-                                thisProp = new TCTLConstNode(Integer.parseInt(num.image));
-      break;
-    case 26:
-      jj_consume_token(26);
-      thisProp = AritmeticExpr();
-      jj_consume_token(27);
-      break;
-    default:
-      jj_la1[9] = jj_gen;
-      jj_consume_token(-1);
-      throw new ParseException();
-    }
-          {if (true) return thisProp;}
-    throw new Error("Missing return statement in function");
-  }
-
-  private boolean jj_2_1(int xla) {
-    jj_la = xla; jj_lastpos = jj_scanpos = token;
-    try { return !jj_3_1(); }
-    catch(LookaheadSuccess ls) { return true; }
-    finally { jj_save(0, xla); }
-  }
-
-  private boolean jj_2_2(int xla) {
-    jj_la = xla; jj_lastpos = jj_scanpos = token;
-    try { return !jj_3_2(); }
-    catch(LookaheadSuccess ls) { return true; }
-    finally { jj_save(1, xla); }
-  }
-
-  private boolean jj_2_3(int xla) {
-    jj_la = xla; jj_lastpos = jj_scanpos = token;
-    try { return !jj_3_3(); }
-    catch(LookaheadSuccess ls) { return true; }
-    finally { jj_save(2, xla); }
-  }
-
-  private boolean jj_3R_16() {
-    if (jj_scan_token(26)) return true;
-    if (jj_3R_7()) return true;
-    if (jj_scan_token(27)) return true;
-    return false;
-  }
-
-  private boolean jj_3R_13() {
-    if (jj_scan_token(MULT)) return true;
-    if (jj_3R_12()) return true;
-    return false;
-  }
-
-  private boolean jj_3_1() {
-    if (jj_scan_token(IDENT)) return true;
-    if (jj_scan_token(28)) return true;
-    return false;
-  }
-
-  private boolean jj_3R_15() {
-    if (jj_scan_token(NUM)) return true;
-    return false;
-  }
-
-  private boolean jj_3_3() {
-    if (jj_scan_token(IDENT)) return true;
-    if (jj_scan_token(28)) return true;
-    return false;
-  }
-
-  private boolean jj_3R_7() {
-    if (jj_3R_8()) return true;
-    Token xsp;
-    while (true) {
-      xsp = jj_scanpos;
-      if (jj_3R_9()) { jj_scanpos = xsp; break; }
-    }
-    return false;
-  }
-
-  private boolean jj_3R_14() {
-    Token xsp;
-    xsp = jj_scanpos;
-    if (jj_3_3()) jj_scanpos = xsp;
-    if (jj_scan_token(IDENT)) return true;
-    return false;
-  }
-
-  private boolean jj_3R_8() {
-    if (jj_3R_10()) return true;
-    Token xsp;
-    while (true) {
-      xsp = jj_scanpos;
-      if (jj_3R_11()) { jj_scanpos = xsp; break; }
-    }
-    return false;
-  }
-
-  private boolean jj_3R_10() {
-    if (jj_3R_12()) return true;
-    Token xsp;
-    while (true) {
-      xsp = jj_scanpos;
-      if (jj_3R_13()) { jj_scanpos = xsp; break; }
-    }
-    return false;
-  }
-
-  private boolean jj_3R_12() {
-    Token xsp;
-    xsp = jj_scanpos;
-    if (jj_3R_14()) {
-    jj_scanpos = xsp;
-    if (jj_3R_15()) {
-    jj_scanpos = xsp;
-    if (jj_3R_16()) return true;
-    }
-    }
-    return false;
-  }
-
-  private boolean jj_3R_9() {
-    if (jj_scan_token(PLUS)) return true;
-    if (jj_3R_8()) return true;
-    return false;
-  }
-
-  private boolean jj_3_2() {
-    if (jj_3R_6()) return true;
-    return false;
-  }
-
-  private boolean jj_3R_6() {
-    if (jj_3R_7()) return true;
-    if (jj_scan_token(OP)) return true;
-    if (jj_3R_7()) return true;
-    return false;
-  }
-
-  private boolean jj_3R_11() {
-    if (jj_scan_token(MINUS)) return true;
-    if (jj_3R_10()) return true;
-    return false;
-  }
-
-  /** Generated Token Manager. */
-  public TAPAALCTLQueryParserTokenManager token_source;
-  SimpleCharStream jj_input_stream;
-  /** Current token. */
-  public Token token;
-  /** Next token. */
-  public Token jj_nt;
-  private int jj_ntk;
-  private Token jj_scanpos, jj_lastpos;
-  private int jj_la;
-  private int jj_gen;
-  final private int[] jj_la1 = new int[10];
-  static private int[] jj_la1_0;
-  static {
-      jj_la1_init_0();
-   }
-   private static void jj_la1_init_0() {
-      jj_la1_0 = new int[] {0x1ef0,0x2000,0x4000,0x8000,0xe,0x4100000,0x10000,0x20000,0x40000,0x4180000,};
-   }
-  final private JJCalls[] jj_2_rtns = new JJCalls[3];
-  private boolean jj_rescan = false;
-  private int jj_gc = 0;
-
-  /** Constructor with InputStream. */
-  public TAPAALCTLQueryParser(java.io.InputStream stream) {
-     this(stream, null);
-  }
-  /** Constructor with InputStream and supplied encoding */
-  public TAPAALCTLQueryParser(java.io.InputStream stream, String encoding) {
-    try { jj_input_stream = new SimpleCharStream(stream, encoding, 1, 1); } catch(java.io.UnsupportedEncodingException e) { throw new RuntimeException(e); }
-    token_source = new TAPAALCTLQueryParserTokenManager(jj_input_stream);
-    token = new Token();
-    jj_ntk = -1;
-    jj_gen = 0;
-    for (int i = 0; i < 10; i++) jj_la1[i] = -1;
-    for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
-  }
-
-  /** Reinitialise. */
-  public void ReInit(java.io.InputStream stream) {
-     ReInit(stream, null);
-  }
-  /** Reinitialise. */
-  public void ReInit(java.io.InputStream stream, String encoding) {
-    try { jj_input_stream.ReInit(stream, encoding, 1, 1); } catch(java.io.UnsupportedEncodingException e) { throw new RuntimeException(e); }
-    token_source.ReInit(jj_input_stream);
-    token = new Token();
-    jj_ntk = -1;
-    jj_gen = 0;
-    for (int i = 0; i < 10; i++) jj_la1[i] = -1;
-    for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
-  }
-
-  /** Constructor. */
-  public TAPAALCTLQueryParser(java.io.Reader stream) {
-    jj_input_stream = new SimpleCharStream(stream, 1, 1);
-    token_source = new TAPAALCTLQueryParserTokenManager(jj_input_stream);
-    token = new Token();
-    jj_ntk = -1;
-    jj_gen = 0;
-    for (int i = 0; i < 10; i++) jj_la1[i] = -1;
-    for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
-  }
-
-  /** Reinitialise. */
-  public void ReInit(java.io.Reader stream) {
-    jj_input_stream.ReInit(stream, 1, 1);
-    token_source.ReInit(jj_input_stream);
-    token = new Token();
-    jj_ntk = -1;
-    jj_gen = 0;
-    for (int i = 0; i < 10; i++) jj_la1[i] = -1;
-    for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
-  }
-
-  /** Constructor with generated Token Manager. */
-  public TAPAALCTLQueryParser(TAPAALCTLQueryParserTokenManager tm) {
-    token_source = tm;
-    token = new Token();
-    jj_ntk = -1;
-    jj_gen = 0;
-    for (int i = 0; i < 10; i++) jj_la1[i] = -1;
-    for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
-  }
-
-  /** Reinitialise. */
-  public void ReInit(TAPAALCTLQueryParserTokenManager tm) {
-    token_source = tm;
-    token = new Token();
-    jj_ntk = -1;
-    jj_gen = 0;
-    for (int i = 0; i < 10; i++) jj_la1[i] = -1;
-    for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
-  }
-
-  private Token jj_consume_token(int kind) throws ParseException {
-    Token oldToken;
-    if ((oldToken = token).next != null) token = token.next;
-    else token = token.next = token_source.getNextToken();
-    jj_ntk = -1;
-    if (token.kind == kind) {
-      jj_gen++;
-      if (++jj_gc > 100) {
-        jj_gc = 0;
-        for (int i = 0; i < jj_2_rtns.length; i++) {
-          JJCalls c = jj_2_rtns[i];
-          while (c != null) {
-            if (c.gen < jj_gen) c.first = null;
-            c = c.next;
-          }
-        }
-      }
-      return token;
-    }
-    token = oldToken;
-    jj_kind = kind;
-    throw generateParseException();
-  }
-
-  static private final class LookaheadSuccess extends java.lang.Error { }
-  final private LookaheadSuccess jj_ls = new LookaheadSuccess();
-  private boolean jj_scan_token(int kind) {
-    if (jj_scanpos == jj_lastpos) {
-      jj_la--;
-      if (jj_scanpos.next == null) {
-        jj_lastpos = jj_scanpos = jj_scanpos.next = token_source.getNextToken();
-      } else {
-        jj_lastpos = jj_scanpos = jj_scanpos.next;
-      }
-    } else {
-      jj_scanpos = jj_scanpos.next;
-    }
-    if (jj_rescan) {
-      int i = 0; Token tok = token;
-      while (tok != null && tok != jj_scanpos) { i++; tok = tok.next; }
-      if (tok != null) jj_add_error_token(kind, i);
-    }
-    if (jj_scanpos.kind != kind) return true;
-    if (jj_la == 0 && jj_scanpos == jj_lastpos) throw jj_ls;
-    return false;
-  }
-
-
-/** Get the next Token. */
-  final public Token getNextToken() {
-    if (token.next != null) token = token.next;
-    else token = token.next = token_source.getNextToken();
-    jj_ntk = -1;
-    jj_gen++;
-    return token;
-  }
-
-/** Get the specific Token. */
-  final public Token getToken(int index) {
-    Token t = token;
-    for (int i = 0; i < index; i++) {
-      if (t.next != null) t = t.next;
-      else t = t.next = token_source.getNextToken();
-    }
-    return t;
-  }
-
-  private int jj_ntk() {
-    if ((jj_nt=token.next) == null)
-      return (jj_ntk = (token.next=token_source.getNextToken()).kind);
-    else
-      return (jj_ntk = jj_nt.kind);
-  }
-
-  private java.util.List<int[]> jj_expentries = new java.util.ArrayList<int[]>();
-  private int[] jj_expentry;
-  private int jj_kind = -1;
-  private int[] jj_lasttokens = new int[100];
-  private int jj_endpos;
-
-  private void jj_add_error_token(int kind, int pos) {
-    if (pos >= 100) return;
-    if (pos == jj_endpos + 1) {
-      jj_lasttokens[jj_endpos++] = kind;
-    } else if (jj_endpos != 0) {
-      jj_expentry = new int[jj_endpos];
-      for (int i = 0; i < jj_endpos; i++) {
-        jj_expentry[i] = jj_lasttokens[i];
-      }
-      boolean exists = false;
-      for (java.util.Iterator<?> it = jj_expentries.iterator(); it.hasNext();) {
-        exists = true;
-        int[] oldentry = (int[])(it.next());
-        if (oldentry.length == jj_expentry.length) {
-          for (int i = 0; i < jj_expentry.length; i++) {
-            if (oldentry[i] != jj_expentry[i]) {
-              exists = false;
-              break;
-            }
-          }
-          if (exists) break;
-        }
-      }
-      if (!exists) jj_expentries.add(jj_expentry);
-      if (pos != 0) jj_lasttokens[(jj_endpos = pos) - 1] = kind;
-    }
-  }
-
-  /** Generate ParseException. */
-  public ParseException generateParseException() {
-    jj_expentries.clear();
-    boolean[] la1tokens = new boolean[29];
-    if (jj_kind >= 0) {
-      la1tokens[jj_kind] = true;
-      jj_kind = -1;
-    }
-    for (int i = 0; i < 10; i++) {
-      if (jj_la1[i] == jj_gen) {
-        for (int j = 0; j < 32; j++) {
-          if ((jj_la1_0[i] & (1<<j)) != 0) {
-            la1tokens[j] = true;
-          }
-        }
-      }
-    }
-    for (int i = 0; i < 29; i++) {
-      if (la1tokens[i]) {
-        jj_expentry = new int[1];
-        jj_expentry[0] = i;
-        jj_expentries.add(jj_expentry);
-      }
-    }
-    jj_endpos = 0;
-    jj_rescan_token();
-    jj_add_error_token(0, 0);
-    int[][] exptokseq = new int[jj_expentries.size()][];
-    for (int i = 0; i < jj_expentries.size(); i++) {
-      exptokseq[i] = jj_expentries.get(i);
-    }
-    return new ParseException(token, exptokseq, tokenImage);
-  }
-
-  /** Enable tracing. */
-  final public void enable_tracing() {
-  }
-
-  /** Disable tracing. */
-  final public void disable_tracing() {
-  }
-
-  private void jj_rescan_token() {
-    jj_rescan = true;
-    for (int i = 0; i < 3; i++) {
-    try {
-      JJCalls p = jj_2_rtns[i];
-      do {
-        if (p.gen > jj_gen) {
-          jj_la = p.arg; jj_lastpos = jj_scanpos = p.first;
-          switch (i) {
-            case 0: jj_3_1(); break;
-            case 1: jj_3_2(); break;
-            case 2: jj_3_3(); break;
-          }
-        }
-        p = p.next;
-      } while (p != null);
-      } catch(LookaheadSuccess ls) { }
-    }
-    jj_rescan = false;
-  }
-
-  private void jj_save(int index, int xla) {
-    JJCalls p = jj_2_rtns[index];
-    while (p.gen > jj_gen) {
-      if (p.next == null) { p = p.next = new JJCalls(); break; }
-      p = p.next;
-    }
-    p.gen = jj_gen + xla - jj_la; p.first = token; p.arg = xla;
-  }
-
-  static final class JJCalls {
-    int gen;
-    Token first;
-    int arg;
-    JJCalls next;
-  }
+        switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
+            case IDENT:{
+                if (jj_2_3(2)) {
+                    temp = jj_consume_token(IDENT);
+                    jj_consume_token(28);
+                } else {
+                    ;
+                }
+                place = jj_consume_token(IDENT);
+                thisProp = new TCTLPlaceNode(temp == null ? "" : temp.image, place.image);
+                break;
+            }
+            case NUM:{
+                num = jj_consume_token(NUM);
+                thisProp = new TCTLConstNode(Integer.parseInt(num.image));
+                break;
+            }
+            case 26:{
+                jj_consume_token(26);
+                thisProp = AritmeticExpr();
+                jj_consume_token(27);
+                break;
+            }
+            default:
+                jj_la1[9] = jj_gen;
+                jj_consume_token(-1);
+                throw new ParseException();
+        }
+        {if ("" != null) return thisProp;}
+        throw new Error("Missing return statement in function");
+    }
+
+    private boolean jj_2_1(int xla)
+    {
+        jj_la = xla; jj_lastpos = jj_scanpos = token;
+        try { return (!jj_3_1()); }
+        catch(LookaheadSuccess ls) { return true; }
+        finally { jj_save(0, xla); }
+    }
+
+    private boolean jj_2_2(int xla)
+    {
+        jj_la = xla; jj_lastpos = jj_scanpos = token;
+        try { return (!jj_3_2()); }
+        catch(LookaheadSuccess ls) { return true; }
+        finally { jj_save(1, xla); }
+    }
+
+    private boolean jj_2_3(int xla)
+    {
+        jj_la = xla; jj_lastpos = jj_scanpos = token;
+        try { return (!jj_3_3()); }
+        catch(LookaheadSuccess ls) { return true; }
+        finally { jj_save(2, xla); }
+    }
+
+    private boolean jj_3R_AritmeticTerm_287_9_10()
+    {
+        if (jj_3R_AritmeticFactor_308_9_12()) return true;
+        Token xsp;
+        while (true) {
+            xsp = jj_scanpos;
+            if (jj_3R_AritmeticTerm_290_17_13()) { jj_scanpos = xsp; break; }
+        }
+        return false;
+    }
+
+    private boolean jj_3R_AritmeticFactor_308_9_12()
+    {
+        Token xsp;
+        xsp = jj_scanpos;
+        if (jj_3R_AritmeticFactor_309_17_14()) {
+            jj_scanpos = xsp;
+            if (jj_3R_AritmeticFactor_310_19_15()) {
+                jj_scanpos = xsp;
+                if (jj_3R_AritmeticFactor_311_19_16()) return true;
+            }
+        }
+        return false;
+    }
+
+    private boolean jj_3R_AritmeticExpr_252_17_9()
+    {
+        if (jj_scan_token(PLUS)) return true;
+        if (jj_3R_AritmeticMinusExpr_268_9_8()) return true;
+        return false;
+    }
+
+    private boolean jj_3_2()
+    {
+        if (jj_3R_AtomicProposition_234_9_6()) return true;
+        return false;
+    }
+
+    private boolean jj_3R_AtomicProposition_234_9_6()
+    {
+        if (jj_3R_AritmeticExpr_249_9_7()) return true;
+        if (jj_scan_token(OP)) return true;
+        if (jj_3R_AritmeticExpr_249_9_7()) return true;
+        return false;
+    }
+
+    private boolean jj_3R_AritmeticMinusExpr_271_17_11()
+    {
+        if (jj_scan_token(MINUS)) return true;
+        if (jj_3R_AritmeticTerm_287_9_10()) return true;
+        return false;
+    }
+
+    private boolean jj_3R_AritmeticFactor_311_19_16()
+    {
+        if (jj_scan_token(26)) return true;
+        if (jj_3R_AritmeticExpr_249_9_7()) return true;
+        if (jj_scan_token(27)) return true;
+        return false;
+    }
+
+    private boolean jj_3R_AritmeticTerm_290_17_13()
+    {
+        if (jj_scan_token(MULT)) return true;
+        if (jj_3R_AritmeticFactor_308_9_12()) return true;
+        return false;
+    }
+
+    private boolean jj_3_1()
+    {
+        if (jj_scan_token(IDENT)) return true;
+        if (jj_scan_token(28)) return true;
+        return false;
+    }
+
+    private boolean jj_3R_AritmeticFactor_310_19_15()
+    {
+        if (jj_scan_token(NUM)) return true;
+        return false;
+    }
+
+    private boolean jj_3_3()
+    {
+        if (jj_scan_token(IDENT)) return true;
+        if (jj_scan_token(28)) return true;
+        return false;
+    }
+
+    private boolean jj_3R_AritmeticExpr_249_9_7()
+    {
+        if (jj_3R_AritmeticMinusExpr_268_9_8()) return true;
+        Token xsp;
+        while (true) {
+            xsp = jj_scanpos;
+            if (jj_3R_AritmeticExpr_252_17_9()) { jj_scanpos = xsp; break; }
+        }
+        return false;
+    }
+
+    private boolean jj_3R_AritmeticFactor_309_17_14()
+    {
+        Token xsp;
+        xsp = jj_scanpos;
+        if (jj_3_3()) jj_scanpos = xsp;
+        if (jj_scan_token(IDENT)) return true;
+        return false;
+    }
+
+    private boolean jj_3R_AritmeticMinusExpr_268_9_8()
+    {
+        if (jj_3R_AritmeticTerm_287_9_10()) return true;
+        Token xsp;
+        while (true) {
+            xsp = jj_scanpos;
+            if (jj_3R_AritmeticMinusExpr_271_17_11()) { jj_scanpos = xsp; break; }
+        }
+        return false;
+    }
+
+    /** Generated Token Manager. */
+    public TAPAALCTLQueryParserTokenManager token_source;
+    SimpleCharStream jj_input_stream;
+    /** Current token. */
+    public Token token;
+    /** Next token. */
+    public Token jj_nt;
+    private int jj_ntk;
+    private Token jj_scanpos, jj_lastpos;
+    private int jj_la;
+    private int jj_gen;
+    final private int[] jj_la1 = new int[10];
+    static private int[] jj_la1_0;
+    static {
+        jj_la1_init_0();
+    }
+    private static void jj_la1_init_0() {
+        jj_la1_0 = new int[] {0x1ef0,0x2000,0x4000,0x8000,0xe,0x4100000,0x10000,0x20000,0x40000,0x4180000,};
+    }
+    final private JJCalls[] jj_2_rtns = new JJCalls[3];
+    private boolean jj_rescan = false;
+    private int jj_gc = 0;
+
+    /** Constructor with InputStream. */
+    public TAPAALCTLQueryParser(java.io.InputStream stream) {
+        this(stream, null);
+    }
+    /** Constructor with InputStream and supplied encoding */
+    public TAPAALCTLQueryParser(java.io.InputStream stream, String encoding) {
+        try { jj_input_stream = new SimpleCharStream(stream, encoding, 1, 1); } catch(java.io.UnsupportedEncodingException e) { throw new RuntimeException(e); }
+        token_source = new TAPAALCTLQueryParserTokenManager(jj_input_stream);
+        token = new Token();
+        jj_ntk = -1;
+        jj_gen = 0;
+        for (int i = 0; i < 10; i++) jj_la1[i] = -1;
+        for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
+    }
+
+    /** Reinitialise. */
+    public void ReInit(java.io.InputStream stream) {
+        ReInit(stream, null);
+    }
+    /** Reinitialise. */
+    public void ReInit(java.io.InputStream stream, String encoding) {
+        try { jj_input_stream.ReInit(stream, encoding, 1, 1); } catch(java.io.UnsupportedEncodingException e) { throw new RuntimeException(e); }
+        token_source.ReInit(jj_input_stream);
+        token = new Token();
+        jj_ntk = -1;
+        jj_gen = 0;
+        for (int i = 0; i < 10; i++) jj_la1[i] = -1;
+        for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
+    }
+
+    /** Constructor. */
+    public TAPAALCTLQueryParser(java.io.Reader stream) {
+        jj_input_stream = new SimpleCharStream(stream, 1, 1);
+        token_source = new TAPAALCTLQueryParserTokenManager(jj_input_stream);
+        token = new Token();
+        jj_ntk = -1;
+        jj_gen = 0;
+        for (int i = 0; i < 10; i++) jj_la1[i] = -1;
+        for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
+    }
+
+    /** Reinitialise. */
+    public void ReInit(java.io.Reader stream) {
+        if (jj_input_stream == null) {
+            jj_input_stream = new SimpleCharStream(stream, 1, 1);
+        } else {
+            jj_input_stream.ReInit(stream, 1, 1);
+        }
+        if (token_source == null) {
+            token_source = new TAPAALCTLQueryParserTokenManager(jj_input_stream);
+        }
+
+        token_source.ReInit(jj_input_stream);
+        token = new Token();
+        jj_ntk = -1;
+        jj_gen = 0;
+        for (int i = 0; i < 10; i++) jj_la1[i] = -1;
+        for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
+    }
+
+    /** Constructor with generated Token Manager. */
+    public TAPAALCTLQueryParser(TAPAALCTLQueryParserTokenManager tm) {
+        token_source = tm;
+        token = new Token();
+        jj_ntk = -1;
+        jj_gen = 0;
+        for (int i = 0; i < 10; i++) jj_la1[i] = -1;
+        for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
+    }
+
+    /** Reinitialise. */
+    public void ReInit(TAPAALCTLQueryParserTokenManager tm) {
+        token_source = tm;
+        token = new Token();
+        jj_ntk = -1;
+        jj_gen = 0;
+        for (int i = 0; i < 10; i++) jj_la1[i] = -1;
+        for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
+    }
+
+    private Token jj_consume_token(int kind) throws ParseException {
+        Token oldToken;
+        if ((oldToken = token).next != null) token = token.next;
+        else token = token.next = token_source.getNextToken();
+        jj_ntk = -1;
+        if (token.kind == kind) {
+            jj_gen++;
+            if (++jj_gc > 100) {
+                jj_gc = 0;
+                for (int i = 0; i < jj_2_rtns.length; i++) {
+                    JJCalls c = jj_2_rtns[i];
+                    while (c != null) {
+                        if (c.gen < jj_gen) c.first = null;
+                        c = c.next;
+                    }
+                }
+            }
+            return token;
+        }
+        token = oldToken;
+        jj_kind = kind;
+        throw generateParseException();
+    }
+
+    @SuppressWarnings("serial")
+    static private final class LookaheadSuccess extends java.lang.Error {
+        @Override
+        public Throwable fillInStackTrace() {
+            return this;
+        }
+    }
+    static private final LookaheadSuccess jj_ls = new LookaheadSuccess();
+    private boolean jj_scan_token(int kind) {
+        if (jj_scanpos == jj_lastpos) {
+            jj_la--;
+            if (jj_scanpos.next == null) {
+                jj_lastpos = jj_scanpos = jj_scanpos.next = token_source.getNextToken();
+            } else {
+                jj_lastpos = jj_scanpos = jj_scanpos.next;
+            }
+        } else {
+            jj_scanpos = jj_scanpos.next;
+        }
+        if (jj_rescan) {
+            int i = 0; Token tok = token;
+            while (tok != null && tok != jj_scanpos) { i++; tok = tok.next; }
+            if (tok != null) jj_add_error_token(kind, i);
+        }
+        if (jj_scanpos.kind != kind) return true;
+        if (jj_la == 0 && jj_scanpos == jj_lastpos) throw jj_ls;
+        return false;
+    }
+
+
+    /** Get the next Token. */
+    final public Token getNextToken() {
+        if (token.next != null) token = token.next;
+        else token = token.next = token_source.getNextToken();
+        jj_ntk = -1;
+        jj_gen++;
+        return token;
+    }
+
+    /** Get the specific Token. */
+    final public Token getToken(int index) {
+        Token t = token;
+        for (int i = 0; i < index; i++) {
+            if (t.next != null) t = t.next;
+            else t = t.next = token_source.getNextToken();
+        }
+        return t;
+    }
+
+    private int jj_ntk_f() {
+        if ((jj_nt=token.next) == null)
+            return (jj_ntk = (token.next=token_source.getNextToken()).kind);
+        else
+            return (jj_ntk = jj_nt.kind);
+    }
+
+    private java.util.List<int[]> jj_expentries = new java.util.ArrayList<int[]>();
+    private int[] jj_expentry;
+    private int jj_kind = -1;
+    private int[] jj_lasttokens = new int[100];
+    private int jj_endpos;
+
+    private void jj_add_error_token(int kind, int pos) {
+        if (pos >= 100) {
+            return;
+        }
+
+        if (pos == jj_endpos + 1) {
+            jj_lasttokens[jj_endpos++] = kind;
+        } else if (jj_endpos != 0) {
+            jj_expentry = new int[jj_endpos];
+
+            for (int i = 0; i < jj_endpos; i++) {
+                jj_expentry[i] = jj_lasttokens[i];
+            }
+
+            for (int[] oldentry : jj_expentries) {
+                if (oldentry.length == jj_expentry.length) {
+                    boolean isMatched = true;
+
+                    for (int i = 0; i < jj_expentry.length; i++) {
+                        if (oldentry[i] != jj_expentry[i]) {
+                            isMatched = false;
+                            break;
+                        }
+
+                    }
+                    if (isMatched) {
+                        jj_expentries.add(jj_expentry);
+                        break;
+                    }
+                }
+            }
+
+            if (pos != 0) {
+                jj_lasttokens[(jj_endpos = pos) - 1] = kind;
+            }
+        }
+    }
+
+    /** Generate ParseException. */
+    public ParseException generateParseException() {
+        jj_expentries.clear();
+        boolean[] la1tokens = new boolean[29];
+        if (jj_kind >= 0) {
+            la1tokens[jj_kind] = true;
+            jj_kind = -1;
+        }
+        for (int i = 0; i < 10; i++) {
+            if (jj_la1[i] == jj_gen) {
+                for (int j = 0; j < 32; j++) {
+                    if ((jj_la1_0[i] & (1<<j)) != 0) {
+                        la1tokens[j] = true;
+                    }
+                }
+            }
+        }
+        for (int i = 0; i < 29; i++) {
+            if (la1tokens[i]) {
+                jj_expentry = new int[1];
+                jj_expentry[0] = i;
+                jj_expentries.add(jj_expentry);
+            }
+        }
+        jj_endpos = 0;
+        jj_rescan_token();
+        jj_add_error_token(0, 0);
+        int[][] exptokseq = new int[jj_expentries.size()][];
+        for (int i = 0; i < jj_expentries.size(); i++) {
+            exptokseq[i] = jj_expentries.get(i);
+        }
+        return new ParseException(token, exptokseq, tokenImage);
+    }
+
+    private boolean trace_enabled;
+
+    /** Trace enabled. */
+    final public boolean trace_enabled() {
+        return trace_enabled;
+    }
+
+    /** Enable tracing. */
+    final public void enable_tracing() {
+    }
+
+    /** Disable tracing. */
+    final public void disable_tracing() {
+    }
+
+    private void jj_rescan_token() {
+        jj_rescan = true;
+        for (int i = 0; i < 3; i++) {
+            try {
+                JJCalls p = jj_2_rtns[i];
+
+                do {
+                    if (p.gen > jj_gen) {
+                        jj_la = p.arg; jj_lastpos = jj_scanpos = p.first;
+                        switch (i) {
+                            case 0: jj_3_1(); break;
+                            case 1: jj_3_2(); break;
+                            case 2: jj_3_3(); break;
+                        }
+                    }
+                    p = p.next;
+                } while (p != null);
+
+            } catch(LookaheadSuccess ls) { }
+        }
+        jj_rescan = false;
+    }
+
+    private void jj_save(int index, int xla) {
+        JJCalls p = jj_2_rtns[index];
+        while (p.gen > jj_gen) {
+            if (p.next == null) { p = p.next = new JJCalls(); break; }
+            p = p.next;
+        }
+
+        p.gen = jj_gen + xla - jj_la;
+        p.first = token;
+        p.arg = xla;
+    }
+
+    static final class JJCalls {
+        int gen;
+        Token first;
+        int arg;
+        JJCalls next;
+    }
 
 }
 
=== modified file 'src/dk/aau/cs/TCTL/Parsing/TAPAALQueryParser.java'
--- src/dk/aau/cs/TCTL/Parsing/TAPAALQueryParser.java	2014-05-22 20:26:41 +0000
+++ src/dk/aau/cs/TCTL/Parsing/TAPAALQueryParser.java	2021-09-29 07:20:55 +0000
@@ -1,3 +1,4 @@
+/* TAPAALQueryParser.java */
 /* Generated By:JavaCC: Do not edit this line. TAPAALQueryParser.java */
 package dk.aau.cs.TCTL.Parsing;
 
@@ -25,624 +26,691 @@
 
 public class TAPAALQueryParser implements TAPAALQueryParserConstants {
 
-        private static final String ERROR_PARSING_QUERY_MESSAGE = "TAPAAL countered an error trying to parse the query";
-
-        public static TCTLAbstractProperty parse(String query) throws ParseException {
-                TAPAALQueryParser parser = new TAPAALQueryParser(new StringReader(query));
-                return parser.AbstractProperty();
+    private static final String ERROR_PARSING_QUERY_MESSAGE = "TAPAAL countered an error trying to parse the query";
+
+    public static TCTLAbstractProperty parse(String query) throws ParseException {
+        TAPAALQueryParser parser = new TAPAALQueryParser(new StringReader(query));
+        return parser.Start();
+    }
+
+    /** Root production. */
+    final public TCTLAbstractProperty Start() throws ParseException {TCTLAbstractProperty child = null;
+        child = AbstractProperty();
+        jj_consume_token(0);
+        {if ("" != null) return child;}
+        throw new Error("Missing return statement in function");
+    }
+
+    final public TCTLAbstractProperty AbstractProperty() throws ParseException {TCTLAbstractStateProperty child = null;
+        switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
+            case EF:{
+                jj_consume_token(EF);
+                child = OrExpr();
+                {if ("" != null) return new TCTLEFNode(child);}
+                break;
+            }
+            case EG:{
+                jj_consume_token(EG);
+                child = OrExpr();
+                {if ("" != null) return new TCTLEGNode(child);}
+                break;
+            }
+            case AF:{
+                jj_consume_token(AF);
+                child = OrExpr();
+                {if ("" != null) return new TCTLAFNode(child);}
+                break;
+            }
+            case AG:{
+                jj_consume_token(AG);
+                child = OrExpr();
+                {if ("" != null) return new TCTLAGNode(child);}
+                break;
+            }
+            default:
+                jj_la1[0] = jj_gen;
+                jj_consume_token(-1);
+                throw new ParseException();
         }
-
-/** Root production. */
-  final public TCTLAbstractProperty AbstractProperty() throws ParseException {
-        TCTLAbstractStateProperty child = null;
-    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
-    case EF:
-      jj_consume_token(EF);
-      child = OrExpr();
-                                       {if (true) return new TCTLEFNode(child);}
-      break;
-    case EG:
-      jj_consume_token(EG);
-      child = OrExpr();
-                                         {if (true) return new TCTLEGNode(child);}
-      break;
-    case AF:
-      jj_consume_token(AF);
-      child = OrExpr();
-                                         {if (true) return new TCTLAFNode(child);}
-      break;
-    case AG:
-      jj_consume_token(AG);
-      child = OrExpr();
-                                         {if (true) return new TCTLAGNode(child);}
-      break;
-    default:
-      jj_la1[0] = jj_gen;
-      jj_consume_token(-1);
-      throw new ParseException();
+        throw new Error("Missing return statement in function");
     }
-    throw new Error("Missing return statement in function");
-  }
 
-  final public TCTLAbstractStateProperty OrExpr() throws ParseException {
-        TCTLAbstractStateProperty currentChild;
+    final public TCTLAbstractStateProperty OrExpr() throws ParseException {TCTLAbstractStateProperty currentChild;
         ArrayList<TCTLAbstractStateProperty> disjunctions = new ArrayList<TCTLAbstractStateProperty>();
-    currentChild = AndExpr();
-          disjunctions.add(currentChild);
-    label_1:
-    while (true) {
-      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
-      case OR:
-        ;
-        break;
-      default:
-        jj_la1[1] = jj_gen;
-        break label_1;
-      }
-      jj_consume_token(OR);
-      currentChild = AndExpr();
-                  disjunctions.add(currentChild);
+        currentChild = AndExpr();
+        disjunctions.add(currentChild);
+        label_1:
+        while (true) {
+            switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
+                case OR:{
+                    ;
+                    break;
+                }
+                default:
+                    jj_la1[1] = jj_gen;
+                    break label_1;
+            }
+            jj_consume_token(OR);
+            currentChild = AndExpr();
+            disjunctions.add(currentChild);
+        }
+        {if ("" != null) return disjunctions.size() == 1 ? currentChild : new TCTLOrListNode(disjunctions);}
+        throw new Error("Missing return statement in function");
     }
-          {if (true) return disjunctions.size() == 1 ? currentChild : new TCTLOrListNode(disjunctions);}
-    throw new Error("Missing return statement in function");
-  }
 
-  final public TCTLAbstractStateProperty AndExpr() throws ParseException {
-        TCTLAbstractStateProperty currentChild;
+    final public TCTLAbstractStateProperty AndExpr() throws ParseException {TCTLAbstractStateProperty currentChild;
         ArrayList<TCTLAbstractStateProperty> conjunctions = new ArrayList<TCTLAbstractStateProperty>();
-    currentChild = NotExpr();
-          conjunctions.add(currentChild);
-    label_2:
-    while (true) {
-      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
-      case AND:
-        ;
-        break;
-      default:
-        jj_la1[2] = jj_gen;
-        break label_2;
-      }
-      jj_consume_token(AND);
-      currentChild = NotExpr();
-                  conjunctions.add(currentChild);
-    }
-          {if (true) return conjunctions.size() == 1 ? currentChild : new TCTLAndListNode(conjunctions);}
-    throw new Error("Missing return statement in function");
-  }
-
-  final public TCTLAbstractStateProperty NotExpr() throws ParseException {
-        TCTLAbstractStateProperty child;
-    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
-    case NOT:
-      jj_consume_token(NOT);
-      jj_consume_token(20);
-      child = OrExpr();
-      jj_consume_token(21);
-                                         {if (true) return new TCTLNotNode(child);}
-      break;
-    case TRUE:
-    case FALSE:
-    case DEADLOCK:
-    case NUM:
-    case IDENT:
-    case 20:
-      child = Factor();
-                             {if (true) return child;}
-      break;
-    default:
-      jj_la1[3] = jj_gen;
-      jj_consume_token(-1);
-      throw new ParseException();
-    }
-    throw new Error("Missing return statement in function");
-  }
-
-  final public TCTLAbstractStateProperty Factor() throws ParseException {
-        TCTLAbstractStateProperty thisProp;
-    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
-    case TRUE:
-      jj_consume_token(TRUE);
-                        thisProp = new TCTLTrueNode();
-      break;
-    case FALSE:
-      jj_consume_token(FALSE);
-                           thisProp = new TCTLFalseNode();
-      break;
-    case DEADLOCK:
-      jj_consume_token(DEADLOCK);
-                              thisProp = new TCTLDeadlockNode();
-      break;
-    default:
-      jj_la1[4] = jj_gen;
-      if (jj_2_1(2147483647)) {
-        thisProp = AtomicProposition();
-      } else {
-        switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
-        case 20:
-          jj_consume_token(20);
-          thisProp = OrExpr();
-          jj_consume_token(21);
-          break;
-        default:
-          jj_la1[5] = jj_gen;
-          jj_consume_token(-1);
-          throw new ParseException();
-        }
-      }
-    }
-          {if (true) return thisProp;}
-    throw new Error("Missing return statement in function");
-  }
-
-  final public TCTLAbstractStateProperty AtomicProposition() throws ParseException {
-        TCTLAbstractStateProperty left;
+        currentChild = NotExpr();
+        conjunctions.add(currentChild);
+        label_2:
+        while (true) {
+            switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
+                case AND:{
+                    ;
+                    break;
+                }
+                default:
+                    jj_la1[2] = jj_gen;
+                    break label_2;
+            }
+            jj_consume_token(AND);
+            currentChild = NotExpr();
+            conjunctions.add(currentChild);
+        }
+        {if ("" != null) return conjunctions.size() == 1 ? currentChild : new TCTLAndListNode(conjunctions);}
+        throw new Error("Missing return statement in function");
+    }
+
+    final public TCTLAbstractStateProperty NotExpr() throws ParseException {TCTLAbstractStateProperty child;
+        switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
+            case NOT:{
+                jj_consume_token(NOT);
+                jj_consume_token(20);
+                child = OrExpr();
+                jj_consume_token(21);
+                {if ("" != null) return new TCTLNotNode(child);}
+                break;
+            }
+            case TRUE:
+            case FALSE:
+            case DEADLOCK:
+            case NUM:
+            case IDENT:
+            case 20:{
+                child = Factor();
+                {if ("" != null) return child;}
+                break;
+            }
+            default:
+                jj_la1[3] = jj_gen;
+                jj_consume_token(-1);
+                throw new ParseException();
+        }
+        throw new Error("Missing return statement in function");
+    }
+
+    final public TCTLAbstractStateProperty Factor() throws ParseException {TCTLAbstractStateProperty thisProp;
+        switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
+            case TRUE:{
+                jj_consume_token(TRUE);
+                thisProp = new TCTLTrueNode();
+                break;
+            }
+            case FALSE:{
+                jj_consume_token(FALSE);
+                thisProp = new TCTLFalseNode();
+                break;
+            }
+            case DEADLOCK:{
+                jj_consume_token(DEADLOCK);
+                thisProp = new TCTLDeadlockNode();
+                break;
+            }
+            default:
+                jj_la1[4] = jj_gen;
+                if (jj_2_1(2147483647)) {
+                    thisProp = AtomicProposition();
+                } else {
+                    switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
+                        case 20:{
+                            jj_consume_token(20);
+                            thisProp = OrExpr();
+                            jj_consume_token(21);
+                            break;
+                        }
+                        default:
+                            jj_la1[5] = jj_gen;
+                            jj_consume_token(-1);
+                            throw new ParseException();
+                    }
+                }
+        }
+        {if ("" != null) return thisProp;}
+        throw new Error("Missing return statement in function");
+    }
+
+    final public TCTLAbstractStateProperty AtomicProposition() throws ParseException {TCTLAbstractStateProperty left;
         TCTLAbstractStateProperty right;
         Token op;
-    left = AritmeticExpr();
-    op = jj_consume_token(OP);
-    right = AritmeticExpr();
-                {if (true) return new TCTLAtomicPropositionNode(left, op.image, right);}
-    throw new Error("Missing return statement in function");
-  }
+        left = AritmeticExpr();
+        op = jj_consume_token(OP);
+        right = AritmeticExpr();
+        {if ("" != null) return new TCTLAtomicPropositionNode(left, op.image, right);}
+        throw new Error("Missing return statement in function");
+    }
 
-  final public TCTLAbstractStateProperty AritmeticExpr() throws ParseException {
-        TCTLAbstractStateProperty currentChild;
+    final public TCTLAbstractStateProperty AritmeticExpr() throws ParseException {TCTLAbstractStateProperty currentChild;
         ArrayList<TCTLAbstractStateProperty> terms = new ArrayList<TCTLAbstractStateProperty>();
         Token op;
-    currentChild = AritmeticTerm();
-          terms.add(currentChild);
-    label_3:
-    while (true) {
-      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
-      case PLUS:
-        ;
-        break;
-      default:
-        jj_la1[6] = jj_gen;
-        break label_3;
-      }
-      op = jj_consume_token(PLUS);
-      currentChild = AritmeticTerm();
-                        terms.add(new AritmeticOperator(op.image));
-                        terms.add(currentChild);
+        currentChild = AritmeticTerm();
+        terms.add(currentChild);
+        label_3:
+        while (true) {
+            switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
+                case PLUS:{
+                    ;
+                    break;
+                }
+                default:
+                    jj_la1[6] = jj_gen;
+                    break label_3;
+            }
+            op = jj_consume_token(PLUS);
+            currentChild = AritmeticTerm();
+            terms.add(new AritmeticOperator(op.image));
+            terms.add(currentChild);
+        }
+        {if ("" != null) return terms.size() == 1 ? currentChild : new TCTLPlusListNode(terms);}
+        throw new Error("Missing return statement in function");
     }
-          {if (true) return terms.size() == 1 ? currentChild : new TCTLPlusListNode(terms);}
-    throw new Error("Missing return statement in function");
-  }
 
-  final public TCTLAbstractStateProperty AritmeticTerm() throws ParseException {
-        TCTLAbstractStateProperty currentChild;
+    final public TCTLAbstractStateProperty AritmeticTerm() throws ParseException {TCTLAbstractStateProperty currentChild;
         ArrayList<TCTLAbstractStateProperty> factors = new ArrayList<TCTLAbstractStateProperty>();
         Token op;
-    currentChild = AritmeticFactor();
-          factors.add(currentChild);
-    label_4:
-    while (true) {
-      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
-      case MULT:
-        ;
-        break;
-      default:
-        jj_la1[7] = jj_gen;
-        break label_4;
-      }
-      op = jj_consume_token(MULT);
-      currentChild = AritmeticFactor();
-                        factors.add(new AritmeticOperator(op.image));
-                        factors.add(currentChild);
+        currentChild = AritmeticFactor();
+        factors.add(currentChild);
+        label_4:
+        while (true) {
+            switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
+                case MULT:{
+                    ;
+                    break;
+                }
+                default:
+                    jj_la1[7] = jj_gen;
+                    break label_4;
+            }
+            op = jj_consume_token(MULT);
+            currentChild = AritmeticFactor();
+            factors.add(new AritmeticOperator(op.image));
+            factors.add(currentChild);
+        }
+        {if ("" != null) return factors.size() == 1 ? currentChild : new TCTLTermListNode(factors);}
+        throw new Error("Missing return statement in function");
     }
-          {if (true) return factors.size() == 1 ? currentChild : new TCTLTermListNode(factors);}
-    throw new Error("Missing return statement in function");
-  }
 
-  final public TCTLAbstractStateProperty AritmeticFactor() throws ParseException {
-        TCTLAbstractStateProperty thisProp;
+    final public TCTLAbstractStateProperty AritmeticFactor() throws ParseException {TCTLAbstractStateProperty thisProp;
         Token template = null;
         Token place;
         Token op;
         Token num;
-    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
-    case IDENT:
-      if (jj_2_2(2)) {
-        template = jj_consume_token(IDENT);
-        jj_consume_token(22);
-      } else {
-        ;
-      }
-      place = jj_consume_token(IDENT);
-                                                                          thisProp = new TCTLPlaceNode(template == null ? "" : template.image, place.image);
-      break;
-    case NUM:
-      num = jj_consume_token(NUM);
-                                thisProp = new TCTLConstNode(Integer.parseInt(num.image));
-      break;
-    case 20:
-      jj_consume_token(20);
-      thisProp = AritmeticExpr();
-      jj_consume_token(21);
-      break;
-    default:
-      jj_la1[8] = jj_gen;
-      jj_consume_token(-1);
-      throw new ParseException();
-    }
-          {if (true) return thisProp;}
-    throw new Error("Missing return statement in function");
-  }
-
-  private boolean jj_2_1(int xla) {
-    jj_la = xla; jj_lastpos = jj_scanpos = token;
-    try { return !jj_3_1(); }
-    catch(LookaheadSuccess ls) { return true; }
-    finally { jj_save(0, xla); }
-  }
-
-  private boolean jj_2_2(int xla) {
-    jj_la = xla; jj_lastpos = jj_scanpos = token;
-    try { return !jj_3_2(); }
-    catch(LookaheadSuccess ls) { return true; }
-    finally { jj_save(1, xla); }
-  }
-
-  private boolean jj_3_1() {
-    if (jj_3R_5()) return true;
-    return false;
-  }
-
-  private boolean jj_3R_8() {
-    if (jj_scan_token(PLUS)) return true;
-    if (jj_3R_7()) return true;
-    return false;
-  }
-
-  private boolean jj_3R_5() {
-    if (jj_3R_6()) return true;
-    if (jj_scan_token(OP)) return true;
-    if (jj_3R_6()) return true;
-    return false;
-  }
-
-  private boolean jj_3R_13() {
-    if (jj_scan_token(20)) return true;
-    if (jj_3R_6()) return true;
-    if (jj_scan_token(21)) return true;
-    return false;
-  }
-
-  private boolean jj_3R_10() {
-    if (jj_scan_token(MULT)) return true;
-    if (jj_3R_9()) return true;
-    return false;
-  }
-
-  private boolean jj_3R_12() {
-    if (jj_scan_token(NUM)) return true;
-    return false;
-  }
-
-  private boolean jj_3_2() {
-    if (jj_scan_token(IDENT)) return true;
-    if (jj_scan_token(22)) return true;
-    return false;
-  }
-
-  private boolean jj_3R_11() {
-    Token xsp;
-    xsp = jj_scanpos;
-    if (jj_3_2()) jj_scanpos = xsp;
-    if (jj_scan_token(IDENT)) return true;
-    return false;
-  }
-
-  private boolean jj_3R_6() {
-    if (jj_3R_7()) return true;
-    Token xsp;
-    while (true) {
-      xsp = jj_scanpos;
-      if (jj_3R_8()) { jj_scanpos = xsp; break; }
-    }
-    return false;
-  }
-
-  private boolean jj_3R_7() {
-    if (jj_3R_9()) return true;
-    Token xsp;
-    while (true) {
-      xsp = jj_scanpos;
-      if (jj_3R_10()) { jj_scanpos = xsp; break; }
-    }
-    return false;
-  }
-
-  private boolean jj_3R_9() {
-    Token xsp;
-    xsp = jj_scanpos;
-    if (jj_3R_11()) {
-    jj_scanpos = xsp;
-    if (jj_3R_12()) {
-    jj_scanpos = xsp;
-    if (jj_3R_13()) return true;
-    }
-    }
-    return false;
-  }
-
-  /** Generated Token Manager. */
-  public TAPAALQueryParserTokenManager token_source;
-  SimpleCharStream jj_input_stream;
-  /** Current token. */
-  public Token token;
-  /** Next token. */
-  public Token jj_nt;
-  private int jj_ntk;
-  private Token jj_scanpos, jj_lastpos;
-  private int jj_la;
-  private int jj_gen;
-  final private int[] jj_la1 = new int[9];
-  static private int[] jj_la1_0;
-  static {
-      jj_la1_init_0();
-   }
-   private static void jj_la1_init_0() {
-      jj_la1_0 = new int[] {0xf0,0x100,0x200,0x10640e,0xe,0x100000,0x800,0x1000,0x106000,};
-   }
-  final private JJCalls[] jj_2_rtns = new JJCalls[2];
-  private boolean jj_rescan = false;
-  private int jj_gc = 0;
-
-  /** Constructor with InputStream. */
-  public TAPAALQueryParser(java.io.InputStream stream) {
-     this(stream, null);
-  }
-  /** Constructor with InputStream and supplied encoding */
-  public TAPAALQueryParser(java.io.InputStream stream, String encoding) {
-    try { jj_input_stream = new SimpleCharStream(stream, encoding, 1, 1); } catch(java.io.UnsupportedEncodingException e) { throw new RuntimeException(e); }
-    token_source = new TAPAALQueryParserTokenManager(jj_input_stream);
-    token = new Token();
-    jj_ntk = -1;
-    jj_gen = 0;
-    for (int i = 0; i < 9; i++) jj_la1[i] = -1;
-    for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
-  }
-
-  /** Reinitialise. */
-  public void ReInit(java.io.InputStream stream) {
-     ReInit(stream, null);
-  }
-  /** Reinitialise. */
-  public void ReInit(java.io.InputStream stream, String encoding) {
-    try { jj_input_stream.ReInit(stream, encoding, 1, 1); } catch(java.io.UnsupportedEncodingException e) { throw new RuntimeException(e); }
-    token_source.ReInit(jj_input_stream);
-    token = new Token();
-    jj_ntk = -1;
-    jj_gen = 0;
-    for (int i = 0; i < 9; i++) jj_la1[i] = -1;
-    for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
-  }
-
-  /** Constructor. */
-  public TAPAALQueryParser(java.io.Reader stream) {
-    jj_input_stream = new SimpleCharStream(stream, 1, 1);
-    token_source = new TAPAALQueryParserTokenManager(jj_input_stream);
-    token = new Token();
-    jj_ntk = -1;
-    jj_gen = 0;
-    for (int i = 0; i < 9; i++) jj_la1[i] = -1;
-    for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
-  }
-
-  /** Reinitialise. */
-  public void ReInit(java.io.Reader stream) {
-    jj_input_stream.ReInit(stream, 1, 1);
-    token_source.ReInit(jj_input_stream);
-    token = new Token();
-    jj_ntk = -1;
-    jj_gen = 0;
-    for (int i = 0; i < 9; i++) jj_la1[i] = -1;
-    for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
-  }
-
-  /** Constructor with generated Token Manager. */
-  public TAPAALQueryParser(TAPAALQueryParserTokenManager tm) {
-    token_source = tm;
-    token = new Token();
-    jj_ntk = -1;
-    jj_gen = 0;
-    for (int i = 0; i < 9; i++) jj_la1[i] = -1;
-    for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
-  }
-
-  /** Reinitialise. */
-  public void ReInit(TAPAALQueryParserTokenManager tm) {
-    token_source = tm;
-    token = new Token();
-    jj_ntk = -1;
-    jj_gen = 0;
-    for (int i = 0; i < 9; i++) jj_la1[i] = -1;
-    for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
-  }
-
-  private Token jj_consume_token(int kind) throws ParseException {
-    Token oldToken;
-    if ((oldToken = token).next != null) token = token.next;
-    else token = token.next = token_source.getNextToken();
-    jj_ntk = -1;
-    if (token.kind == kind) {
-      jj_gen++;
-      if (++jj_gc > 100) {
-        jj_gc = 0;
-        for (int i = 0; i < jj_2_rtns.length; i++) {
-          JJCalls c = jj_2_rtns[i];
-          while (c != null) {
-            if (c.gen < jj_gen) c.first = null;
-            c = c.next;
-          }
-        }
-      }
-      return token;
-    }
-    token = oldToken;
-    jj_kind = kind;
-    throw generateParseException();
-  }
-
-  static private final class LookaheadSuccess extends java.lang.Error { }
-  final private LookaheadSuccess jj_ls = new LookaheadSuccess();
-  private boolean jj_scan_token(int kind) {
-    if (jj_scanpos == jj_lastpos) {
-      jj_la--;
-      if (jj_scanpos.next == null) {
-        jj_lastpos = jj_scanpos = jj_scanpos.next = token_source.getNextToken();
-      } else {
-        jj_lastpos = jj_scanpos = jj_scanpos.next;
-      }
-    } else {
-      jj_scanpos = jj_scanpos.next;
-    }
-    if (jj_rescan) {
-      int i = 0; Token tok = token;
-      while (tok != null && tok != jj_scanpos) { i++; tok = tok.next; }
-      if (tok != null) jj_add_error_token(kind, i);
-    }
-    if (jj_scanpos.kind != kind) return true;
-    if (jj_la == 0 && jj_scanpos == jj_lastpos) throw jj_ls;
-    return false;
-  }
-
-
-/** Get the next Token. */
-  final public Token getNextToken() {
-    if (token.next != null) token = token.next;
-    else token = token.next = token_source.getNextToken();
-    jj_ntk = -1;
-    jj_gen++;
-    return token;
-  }
-
-/** Get the specific Token. */
-  final public Token getToken(int index) {
-    Token t = token;
-    for (int i = 0; i < index; i++) {
-      if (t.next != null) t = t.next;
-      else t = t.next = token_source.getNextToken();
-    }
-    return t;
-  }
-
-  private int jj_ntk() {
-    if ((jj_nt=token.next) == null)
-      return (jj_ntk = (token.next=token_source.getNextToken()).kind);
-    else
-      return (jj_ntk = jj_nt.kind);
-  }
-
-  private java.util.List<int[]> jj_expentries = new java.util.ArrayList<int[]>();
-  private int[] jj_expentry;
-  private int jj_kind = -1;
-  private int[] jj_lasttokens = new int[100];
-  private int jj_endpos;
-
-  private void jj_add_error_token(int kind, int pos) {
-    if (pos >= 100) return;
-    if (pos == jj_endpos + 1) {
-      jj_lasttokens[jj_endpos++] = kind;
-    } else if (jj_endpos != 0) {
-      jj_expentry = new int[jj_endpos];
-      for (int i = 0; i < jj_endpos; i++) {
-        jj_expentry[i] = jj_lasttokens[i];
-      }
-      jj_entries_loop: for (java.util.Iterator<?> it = jj_expentries.iterator(); it.hasNext();) {
-        int[] oldentry = (int[])(it.next());
-        if (oldentry.length == jj_expentry.length) {
-          for (int i = 0; i < jj_expentry.length; i++) {
-            if (oldentry[i] != jj_expentry[i]) {
-              continue jj_entries_loop;
-            }
-          }
-          jj_expentries.add(jj_expentry);
-          break jj_entries_loop;
-        }
-      }
-      if (pos != 0) jj_lasttokens[(jj_endpos = pos) - 1] = kind;
-    }
-  }
-
-  /** Generate ParseException. */
-  public ParseException generateParseException() {
-    jj_expentries.clear();
-    boolean[] la1tokens = new boolean[23];
-    if (jj_kind >= 0) {
-      la1tokens[jj_kind] = true;
-      jj_kind = -1;
-    }
-    for (int i = 0; i < 9; i++) {
-      if (jj_la1[i] == jj_gen) {
-        for (int j = 0; j < 32; j++) {
-          if ((jj_la1_0[i] & (1<<j)) != 0) {
-            la1tokens[j] = true;
-          }
-        }
-      }
-    }
-    for (int i = 0; i < 23; i++) {
-      if (la1tokens[i]) {
-        jj_expentry = new int[1];
-        jj_expentry[0] = i;
-        jj_expentries.add(jj_expentry);
-      }
-    }
-    jj_endpos = 0;
-    jj_rescan_token();
-    jj_add_error_token(0, 0);
-    int[][] exptokseq = new int[jj_expentries.size()][];
-    for (int i = 0; i < jj_expentries.size(); i++) {
-      exptokseq[i] = jj_expentries.get(i);
-    }
-    return new ParseException(token, exptokseq, tokenImage);
-  }
-
-  /** Enable tracing. */
-  final public void enable_tracing() {
-  }
-
-  /** Disable tracing. */
-  final public void disable_tracing() {
-  }
-
-  private void jj_rescan_token() {
-    jj_rescan = true;
-    for (int i = 0; i < 2; i++) {
-    try {
-      JJCalls p = jj_2_rtns[i];
-      do {
-        if (p.gen > jj_gen) {
-          jj_la = p.arg; jj_lastpos = jj_scanpos = p.first;
-          switch (i) {
-            case 0: jj_3_1(); break;
-            case 1: jj_3_2(); break;
-          }
-        }
-        p = p.next;
-      } while (p != null);
-      } catch(LookaheadSuccess ls) { }
-    }
-    jj_rescan = false;
-  }
-
-  private void jj_save(int index, int xla) {
-    JJCalls p = jj_2_rtns[index];
-    while (p.gen > jj_gen) {
-      if (p.next == null) { p = p.next = new JJCalls(); break; }
-      p = p.next;
-    }
-    p.gen = jj_gen + xla - jj_la; p.first = token; p.arg = xla;
-  }
-
-  static final class JJCalls {
-    int gen;
-    Token first;
-    int arg;
-    JJCalls next;
-  }
+        switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
+            case IDENT:{
+                if (jj_2_2(2)) {
+                    template = jj_consume_token(IDENT);
+                    jj_consume_token(22);
+                } else {
+                    ;
+                }
+                place = jj_consume_token(IDENT);
+                thisProp = new TCTLPlaceNode(template == null ? "" : template.image, place.image);
+                break;
+            }
+            case NUM:{
+                num = jj_consume_token(NUM);
+                thisProp = new TCTLConstNode(Integer.parseInt(num.image));
+                break;
+            }
+            case 20:{
+                jj_consume_token(20);
+                thisProp = AritmeticExpr();
+                jj_consume_token(21);
+                break;
+            }
+            default:
+                jj_la1[8] = jj_gen;
+                jj_consume_token(-1);
+                throw new ParseException();
+        }
+        {if ("" != null) return thisProp;}
+        throw new Error("Missing return statement in function");
+    }
+
+    private boolean jj_2_1(int xla)
+    {
+        jj_la = xla; jj_lastpos = jj_scanpos = token;
+        try { return (!jj_3_1()); }
+        catch(LookaheadSuccess ls) { return true; }
+        finally { jj_save(0, xla); }
+    }
+
+    private boolean jj_2_2(int xla)
+    {
+        jj_la = xla; jj_lastpos = jj_scanpos = token;
+        try { return (!jj_3_2()); }
+        catch(LookaheadSuccess ls) { return true; }
+        finally { jj_save(1, xla); }
+    }
+
+    private boolean jj_3_2()
+    {
+        if (jj_scan_token(IDENT)) return true;
+        if (jj_scan_token(22)) return true;
+        return false;
+    }
+
+    private boolean jj_3R_AritmeticFactor_256_17_11()
+    {
+        Token xsp;
+        xsp = jj_scanpos;
+        if (jj_3_2()) jj_scanpos = xsp;
+        if (jj_scan_token(IDENT)) return true;
+        return false;
+    }
+
+    private boolean jj_3R_AritmeticExpr_215_9_6()
+    {
+        if (jj_3R_AritmeticTerm_234_9_7()) return true;
+        Token xsp;
+        while (true) {
+            xsp = jj_scanpos;
+            if (jj_3R_AritmeticExpr_218_17_8()) { jj_scanpos = xsp; break; }
+        }
+        return false;
+    }
+
+    private boolean jj_3R_AritmeticTerm_234_9_7()
+    {
+        if (jj_3R_AritmeticFactor_255_9_9()) return true;
+        Token xsp;
+        while (true) {
+            xsp = jj_scanpos;
+            if (jj_3R_AritmeticTerm_237_17_10()) { jj_scanpos = xsp; break; }
+        }
+        return false;
+    }
+
+    private boolean jj_3R_AritmeticFactor_255_9_9()
+    {
+        Token xsp;
+        xsp = jj_scanpos;
+        if (jj_3R_AritmeticFactor_256_17_11()) {
+            jj_scanpos = xsp;
+            if (jj_3R_AritmeticFactor_257_19_12()) {
+                jj_scanpos = xsp;
+                if (jj_3R_AritmeticFactor_258_19_13()) return true;
+            }
+        }
+        return false;
+    }
+
+    private boolean jj_3_1()
+    {
+        if (jj_3R_AtomicProposition_200_9_5()) return true;
+        return false;
+    }
+
+    private boolean jj_3R_AritmeticExpr_218_17_8()
+    {
+        if (jj_scan_token(PLUS)) return true;
+        if (jj_3R_AritmeticTerm_234_9_7()) return true;
+        return false;
+    }
+
+    private boolean jj_3R_AtomicProposition_200_9_5()
+    {
+        if (jj_3R_AritmeticExpr_215_9_6()) return true;
+        if (jj_scan_token(OP)) return true;
+        if (jj_3R_AritmeticExpr_215_9_6()) return true;
+        return false;
+    }
+
+    private boolean jj_3R_AritmeticFactor_258_19_13()
+    {
+        if (jj_scan_token(20)) return true;
+        if (jj_3R_AritmeticExpr_215_9_6()) return true;
+        if (jj_scan_token(21)) return true;
+        return false;
+    }
+
+    private boolean jj_3R_AritmeticTerm_237_17_10()
+    {
+        if (jj_scan_token(MULT)) return true;
+        if (jj_3R_AritmeticFactor_255_9_9()) return true;
+        return false;
+    }
+
+    private boolean jj_3R_AritmeticFactor_257_19_12()
+    {
+        if (jj_scan_token(NUM)) return true;
+        return false;
+    }
+
+    /** Generated Token Manager. */
+    public TAPAALQueryParserTokenManager token_source;
+    SimpleCharStream jj_input_stream;
+    /** Current token. */
+    public Token token;
+    /** Next token. */
+    public Token jj_nt;
+    private int jj_ntk;
+    private Token jj_scanpos, jj_lastpos;
+    private int jj_la;
+    private int jj_gen;
+    final private int[] jj_la1 = new int[9];
+    static private int[] jj_la1_0;
+    static {
+        jj_la1_init_0();
+    }
+    private static void jj_la1_init_0() {
+        jj_la1_0 = new int[] {0xf0,0x100,0x200,0x10640e,0xe,0x100000,0x800,0x1000,0x106000,};
+    }
+    final private JJCalls[] jj_2_rtns = new JJCalls[2];
+    private boolean jj_rescan = false;
+    private int jj_gc = 0;
+
+    /** Constructor with InputStream. */
+    public TAPAALQueryParser(java.io.InputStream stream) {
+        this(stream, null);
+    }
+    /** Constructor with InputStream and supplied encoding */
+    public TAPAALQueryParser(java.io.InputStream stream, String encoding) {
+        try { jj_input_stream = new SimpleCharStream(stream, encoding, 1, 1); } catch(java.io.UnsupportedEncodingException e) { throw new RuntimeException(e); }
+        token_source = new TAPAALQueryParserTokenManager(jj_input_stream);
+        token = new Token();
+        jj_ntk = -1;
+        jj_gen = 0;
+        for (int i = 0; i < 9; i++) jj_la1[i] = -1;
+        for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
+    }
+
+    /** Reinitialise. */
+    public void ReInit(java.io.InputStream stream) {
+        ReInit(stream, null);
+    }
+    /** Reinitialise. */
+    public void ReInit(java.io.InputStream stream, String encoding) {
+        try { jj_input_stream.ReInit(stream, encoding, 1, 1); } catch(java.io.UnsupportedEncodingException e) { throw new RuntimeException(e); }
+        token_source.ReInit(jj_input_stream);
+        token = new Token();
+        jj_ntk = -1;
+        jj_gen = 0;
+        for (int i = 0; i < 9; i++) jj_la1[i] = -1;
+        for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
+    }
+
+    /** Constructor. */
+    public TAPAALQueryParser(java.io.Reader stream) {
+        jj_input_stream = new SimpleCharStream(stream, 1, 1);
+        token_source = new TAPAALQueryParserTokenManager(jj_input_stream);
+        token = new Token();
+        jj_ntk = -1;
+        jj_gen = 0;
+        for (int i = 0; i < 9; i++) jj_la1[i] = -1;
+        for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
+    }
+
+    /** Reinitialise. */
+    public void ReInit(java.io.Reader stream) {
+        if (jj_input_stream == null) {
+            jj_input_stream = new SimpleCharStream(stream, 1, 1);
+        } else {
+            jj_input_stream.ReInit(stream, 1, 1);
+        }
+        if (token_source == null) {
+            token_source = new TAPAALQueryParserTokenManager(jj_input_stream);
+        }
+
+        token_source.ReInit(jj_input_stream);
+        token = new Token();
+        jj_ntk = -1;
+        jj_gen = 0;
+        for (int i = 0; i < 9; i++) jj_la1[i] = -1;
+        for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
+    }
+
+    /** Constructor with generated Token Manager. */
+    public TAPAALQueryParser(TAPAALQueryParserTokenManager tm) {
+        token_source = tm;
+        token = new Token();
+        jj_ntk = -1;
+        jj_gen = 0;
+        for (int i = 0; i < 9; i++) jj_la1[i] = -1;
+        for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
+    }
+
+    /** Reinitialise. */
+    public void ReInit(TAPAALQueryParserTokenManager tm) {
+        token_source = tm;
+        token = new Token();
+        jj_ntk = -1;
+        jj_gen = 0;
+        for (int i = 0; i < 9; i++) jj_la1[i] = -1;
+        for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
+    }
+
+    private Token jj_consume_token(int kind) throws ParseException {
+        Token oldToken;
+        if ((oldToken = token).next != null) token = token.next;
+        else token = token.next = token_source.getNextToken();
+        jj_ntk = -1;
+        if (token.kind == kind) {
+            jj_gen++;
+            if (++jj_gc > 100) {
+                jj_gc = 0;
+                for (int i = 0; i < jj_2_rtns.length; i++) {
+                    JJCalls c = jj_2_rtns[i];
+                    while (c != null) {
+                        if (c.gen < jj_gen) c.first = null;
+                        c = c.next;
+                    }
+                }
+            }
+            return token;
+        }
+        token = oldToken;
+        jj_kind = kind;
+        throw generateParseException();
+    }
+
+    @SuppressWarnings("serial")
+    static private final class LookaheadSuccess extends java.lang.Error {
+        @Override
+        public Throwable fillInStackTrace() {
+            return this;
+        }
+    }
+    static private final LookaheadSuccess jj_ls = new LookaheadSuccess();
+    private boolean jj_scan_token(int kind) {
+        if (jj_scanpos == jj_lastpos) {
+            jj_la--;
+            if (jj_scanpos.next == null) {
+                jj_lastpos = jj_scanpos = jj_scanpos.next = token_source.getNextToken();
+            } else {
+                jj_lastpos = jj_scanpos = jj_scanpos.next;
+            }
+        } else {
+            jj_scanpos = jj_scanpos.next;
+        }
+        if (jj_rescan) {
+            int i = 0; Token tok = token;
+            while (tok != null && tok != jj_scanpos) { i++; tok = tok.next; }
+            if (tok != null) jj_add_error_token(kind, i);
+        }
+        if (jj_scanpos.kind != kind) return true;
+        if (jj_la == 0 && jj_scanpos == jj_lastpos) throw jj_ls;
+        return false;
+    }
+
+
+    /** Get the next Token. */
+    final public Token getNextToken() {
+        if (token.next != null) token = token.next;
+        else token = token.next = token_source.getNextToken();
+        jj_ntk = -1;
+        jj_gen++;
+        return token;
+    }
+
+    /** Get the specific Token. */
+    final public Token getToken(int index) {
+        Token t = token;
+        for (int i = 0; i < index; i++) {
+            if (t.next != null) t = t.next;
+            else t = t.next = token_source.getNextToken();
+        }
+        return t;
+    }
+
+    private int jj_ntk_f() {
+        if ((jj_nt=token.next) == null)
+            return (jj_ntk = (token.next=token_source.getNextToken()).kind);
+        else
+            return (jj_ntk = jj_nt.kind);
+    }
+
+    private java.util.List<int[]> jj_expentries = new java.util.ArrayList<int[]>();
+    private int[] jj_expentry;
+    private int jj_kind = -1;
+    private int[] jj_lasttokens = new int[100];
+    private int jj_endpos;
+
+    private void jj_add_error_token(int kind, int pos) {
+        if (pos >= 100) {
+            return;
+        }
+
+        if (pos == jj_endpos + 1) {
+            jj_lasttokens[jj_endpos++] = kind;
+        } else if (jj_endpos != 0) {
+            jj_expentry = new int[jj_endpos];
+
+            for (int i = 0; i < jj_endpos; i++) {
+                jj_expentry[i] = jj_lasttokens[i];
+            }
+
+            for (int[] oldentry : jj_expentries) {
+                if (oldentry.length == jj_expentry.length) {
+                    boolean isMatched = true;
+
+                    for (int i = 0; i < jj_expentry.length; i++) {
+                        if (oldentry[i] != jj_expentry[i]) {
+                            isMatched = false;
+                            break;
+                        }
+
+                    }
+                    if (isMatched) {
+                        jj_expentries.add(jj_expentry);
+                        break;
+                    }
+                }
+            }
+
+            if (pos != 0) {
+                jj_lasttokens[(jj_endpos = pos) - 1] = kind;
+            }
+        }
+    }
+
+    /** Generate ParseException. */
+    public ParseException generateParseException() {
+        jj_expentries.clear();
+        boolean[] la1tokens = new boolean[23];
+        if (jj_kind >= 0) {
+            la1tokens[jj_kind] = true;
+            jj_kind = -1;
+        }
+        for (int i = 0; i < 9; i++) {
+            if (jj_la1[i] == jj_gen) {
+                for (int j = 0; j < 32; j++) {
+                    if ((jj_la1_0[i] & (1<<j)) != 0) {
+                        la1tokens[j] = true;
+                    }
+                }
+            }
+        }
+        for (int i = 0; i < 23; i++) {
+            if (la1tokens[i]) {
+                jj_expentry = new int[1];
+                jj_expentry[0] = i;
+                jj_expentries.add(jj_expentry);
+            }
+        }
+        jj_endpos = 0;
+        jj_rescan_token();
+        jj_add_error_token(0, 0);
+        int[][] exptokseq = new int[jj_expentries.size()][];
+        for (int i = 0; i < jj_expentries.size(); i++) {
+            exptokseq[i] = jj_expentries.get(i);
+        }
+        return new ParseException(token, exptokseq, tokenImage);
+    }
+
+    private boolean trace_enabled;
+
+    /** Trace enabled. */
+    final public boolean trace_enabled() {
+        return trace_enabled;
+    }
+
+    /** Enable tracing. */
+    final public void enable_tracing() {
+    }
+
+    /** Disable tracing. */
+    final public void disable_tracing() {
+    }
+
+    private void jj_rescan_token() {
+        jj_rescan = true;
+        for (int i = 0; i < 2; i++) {
+            try {
+                JJCalls p = jj_2_rtns[i];
+
+                do {
+                    if (p.gen > jj_gen) {
+                        jj_la = p.arg; jj_lastpos = jj_scanpos = p.first;
+                        switch (i) {
+                            case 0: jj_3_1(); break;
+                            case 1: jj_3_2(); break;
+                        }
+                    }
+                    p = p.next;
+                } while (p != null);
+
+            } catch(LookaheadSuccess ls) { }
+        }
+        jj_rescan = false;
+    }
+
+    private void jj_save(int index, int xla) {
+        JJCalls p = jj_2_rtns[index];
+        while (p.gen > jj_gen) {
+            if (p.next == null) { p = p.next = new JJCalls(); break; }
+            p = p.next;
+        }
+
+        p.gen = jj_gen + xla - jj_la;
+        p.first = token;
+        p.arg = xla;
+    }
+
+    static final class JJCalls {
+        int gen;
+        Token first;
+        int arg;
+        JJCalls next;
+    }
 
 }
 
=== modified file 'src/dk/aau/cs/TCTL/TCTLEFNode.java'
--- src/dk/aau/cs/TCTL/TCTLEFNode.java	2020-11-06 19:41:50 +0000
+++ src/dk/aau/cs/TCTL/TCTLEFNode.java	2021-09-29 07:20:55 +0000
@@ -2,6 +2,8 @@
 
 import dk.aau.cs.TCTL.visitors.ITCTLVisitor;
 
+import java.util.HashMap;
+
 public class TCTLEFNode extends TCTLAbstractPathProperty {
 
 	private TCTLAbstractStateProperty property;
@@ -104,7 +106,6 @@
 	@Override
 	public TCTLAbstractProperty findFirstPlaceHolder() {
 		return property.findFirstPlaceHolder();
-
 	}
 
 }
 
=== modified file 'src/pipe/gui/widgets/QueryDialog.java'
--- src/pipe/gui/widgets/QueryDialog.java	2021-09-11 17:11:34 +0000
+++ src/pipe/gui/widgets/QueryDialog.java	2021-09-29 07:20:55 +0000
@@ -2326,42 +2326,37 @@
 
 					if (newQuery != null) // new query parsed successfully
 					{
-						// check correct place names are used in atomic propositions
-						ArrayList<Tuple<String,String>> templatePlaceNames = new ArrayList<Tuple<String,String>>();
-						for(TimedArcPetriNet tapn : tapnNetwork.activeTemplates()) {
-							for(TimedPlace p : tapn.places()) {
-                                if (lens.isTimed() || !p.isShared() || lens.isGame()) {
-                                    templatePlaceNames.add(new Tuple<String, String>(tapn.name(), p.name()));
-                                }
-							}
-						}
-
-						for(TimedPlace p : tapnNetwork.sharedPlaces()) {
-							templatePlaceNames.add(new Tuple<String, String>("", p.name()));
-						}
-
-						FixAbbrivPlaceNames.fixAbbrivPlaceNames(templatePlaceNames, newQuery);
-						VerifyPlaceNamesVisitor nameChecker = new VerifyPlaceNamesVisitor(templatePlaceNames);
-						VerifyPlaceNamesVisitor.Context c = nameChecker.verifyPlaceNames(newQuery);
+						VerifyPlaceNamesVisitor.Context placeContext = getPlaceContext(newQuery);
+                        VerifyTransitionNamesVisitor.Context transitionContext = getTransitionContext(newQuery);
 
                         boolean isResultFalse;
 
                         if (lens.isTimed() || lens.isGame()) {
-                            isResultFalse = !c.getResult();
+                            isResultFalse = !placeContext.getResult();
                         } else {
-                            isResultFalse = checkUntimedResult(newQuery) && !c.getResult();
+                            isResultFalse = !transitionContext.getResult() || !placeContext.getResult();
                         }
 
 						if (isResultFalse) {
 							StringBuilder s = new StringBuilder();
+<<<<<<< TREE
 							s.append("The following places" + (lens.isTimed() ? "" : " or transitions") +
                                 " were used in the query, but are not present in your model:\n\n");
+=======
+							s.append("The following places " + (lens.isTimed() ? "" : "or transitions") +
+                                " were used in the query, but are not present in your model:\n\n");
+>>>>>>> MERGE-SOURCE
 
-							for (String placeName : c.getIncorrectPlaceNames()) {
+							for (String placeName : placeContext.getIncorrectPlaceNames()) {
 								s.append(placeName);
 								s.append('\n');
 							}
 
+                            for (String transitionName : transitionContext.getIncorrectTransitionNames()) {
+                                s.append(transitionName);
+                                s.append('\n');
+                            }
+
 							s.append("\nThe specified query has not been saved. Do you want to edit it again?");
 							int choice = JOptionPane.showConfirmDialog(
 									CreateGui.getApp(), s.toString(),
@@ -2442,25 +2437,44 @@
 		queryPanel.add(editingButtonPanel, gbc);
 	}
 
-    private boolean checkUntimedResult(TCTLAbstractProperty newQuery) {
+    private VerifyPlaceNamesVisitor.Context getPlaceContext(TCTLAbstractProperty newQuery) {
+        // check correct place names are used in atomic propositions
+        ArrayList<Tuple<String,String>> templatePlaceNames = new ArrayList<Tuple<String,String>>();
+        for(TimedArcPetriNet tapn : tapnNetwork.activeTemplates()) {
+            for(TimedPlace p : tapn.places()) {
+                if (lens.isTimed() || !p.isShared() || lens.isGame()) {
+                    templatePlaceNames.add(new Tuple<String, String>(tapn.name(), p.name()));
+                }
+            }
+        }
+
+        for(TimedPlace p : tapnNetwork.sharedPlaces()) {
+            templatePlaceNames.add(new Tuple<String, String>("", p.name()));
+        }
+
+        FixAbbrivPlaceNames.fixAbbrivPlaceNames(templatePlaceNames, newQuery);
+        VerifyPlaceNamesVisitor nameChecker = new VerifyPlaceNamesVisitor(templatePlaceNames);
+        return nameChecker.verifyPlaceNames(newQuery);
+    }
+
+    private VerifyTransitionNamesVisitor.Context getTransitionContext(TCTLAbstractProperty newQuery) {
         // check correct transition names are used in atomic propositions
-        ArrayList<Tuple<String, String>> templateTransitionNames = new ArrayList<Tuple<String, String>>();
+        ArrayList<Tuple<String,String>> templateTransitionNames = new ArrayList<Tuple<String,String>>();
         for (TimedArcPetriNet tapn : tapnNetwork.activeTemplates()) {
             for (TimedTransition t : tapn.transitions()) {
-                if (!t.isShared()) {
-                    templateTransitionNames.add(new Tuple<String, String>(tapn.name(), t.name()));
+                if (lens.isTimed() || !t.isShared() || lens.isGame()) {
+                    templateTransitionNames.add(new Tuple<>(tapn.name(), t.name()));
                 }
             }
         }
 
         for (SharedTransition t : tapnNetwork.sharedTransitions()) {
-            templateTransitionNames.add(new Tuple<String, String>("", t.name()));
+            templateTransitionNames.add(new Tuple<>("", t.name()));
         }
 
         FixAbbrivTransitionNames.fixAbbrivTransitionNames(templateTransitionNames, newQuery);
-        VerifyTransitionNamesVisitor transitionNameChecker = new VerifyTransitionNamesVisitor(templateTransitionNames);
-        VerifyTransitionNamesVisitor.Context c2 = transitionNameChecker.verifyTransitionNames(newQuery);
-        return !c2.getResult();
+        VerifyTransitionNamesVisitor nameChecker = new VerifyTransitionNamesVisitor(templateTransitionNames);
+        return nameChecker.verifyTransitionNames(newQuery);
     }
 
 	private void initUppaalOptionsPanel() {
 
=== modified file 'src/resources/TCTLParser/TAPAALCTLQueryParser.jj'
--- src/resources/TCTLParser/TAPAALCTLQueryParser.jj	2017-09-05 21:24:23 +0000
+++ src/resources/TCTLParser/TAPAALCTLQueryParser.jj	2021-09-29 07:20:55 +0000
@@ -56,7 +56,7 @@
 
 	public static TCTLAbstractPathProperty parse(String query) throws ParseException {
 		TAPAALCTLQueryParser parser = new TAPAALCTLQueryParser(new StringReader(query));
-		return parser.AbstractPathProperty();
+		return parser.Start();
 	}
 }
 
@@ -131,6 +131,16 @@
 }
 
 /** Root production. */
+TCTLAbstractPathProperty Start() :
+{
+	TCTLAbstractPathProperty child = null;
+}
+{
+	(
+		child = AbstractPathProperty() <EOF> {return child;}
+	)
+}
+
 TCTLAbstractPathProperty AbstractPathProperty() :
 {
 	TCTLAbstractStateProperty child = null; 
 
=== modified file 'src/resources/TCTLParser/TAPAALQueryParser.jj'
--- src/resources/TCTLParser/TAPAALQueryParser.jj	2014-05-22 20:26:41 +0000
+++ src/resources/TCTLParser/TAPAALQueryParser.jj	2021-09-29 07:20:55 +0000
@@ -49,7 +49,7 @@
 
 	public static TCTLAbstractProperty parse(String query) throws ParseException {
 		TAPAALQueryParser parser = new TAPAALQueryParser(new StringReader(query));
-		return parser.AbstractProperty();
+		return parser.Start();
 	}
 }
 
@@ -112,6 +112,16 @@
 }
 
 /** Root production. */
+TCTLAbstractProperty Start() :
+{
+	TCTLAbstractProperty child = null;
+}
+{
+	(
+		child = AbstractProperty() <EOF> {return child;}
+	)
+}
+
 TCTLAbstractProperty AbstractProperty() :
 {
 	TCTLAbstractStateProperty child = null;