diff --git a/prism/src/parser/PrismParser.java b/prism/src/parser/PrismParser.java
index 56f8b499..6d9367a4 100644
--- a/prism/src/parser/PrismParser.java
+++ b/prism/src/parser/PrismParser.java
@@ -1829,7 +1829,7 @@ public class PrismParser implements PrismParserConstants {
         Expression ret, expr;
         Token begin = null;
           begin = getToken(1);
-    ret = ExpressionOr(prop, pathprop);
+    ret = ExpressionIff(prop, pathprop);
     label_18:
     while (true) {
       switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
@@ -1841,8 +1841,32 @@ public class PrismParser implements PrismParserConstants {
         break label_18;
       }
       jj_consume_token(IMPLIES);
+      expr = ExpressionIff(prop, pathprop);
+                                                           ret = new ExpressionBinaryOp(ExpressionBinaryOp.IMPLIES, ret, expr); ret.setPosition(begin, getToken(0));
+    }
+          {if (true) return ret;}
+    throw new Error("Missing return statement in function");
+  }
+
+// Expression: if-and-only-iff
+  static final public Expression ExpressionIff(boolean prop, boolean pathprop) throws ParseException {
+        Expression ret, expr;
+        Token begin = null;
+          begin = getToken(1);
+    ret = ExpressionOr(prop, pathprop);
+    label_19:
+    while (true) {
+      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
+      case IFF:
+        ;
+        break;
+      default:
+        jj_la1[51] = jj_gen;
+        break label_19;
+      }
+      jj_consume_token(IFF);
       expr = ExpressionOr(prop, pathprop);
-                                                          ret = new ExpressionBinaryOp(ExpressionBinaryOp.IMPLIES, ret, expr); ret.setPosition(begin, getToken(0));
+                                                      ret = new ExpressionBinaryOp(ExpressionBinaryOp.IFF, ret, expr); ret.setPosition(begin, getToken(0));
     }
           {if (true) return ret;}
     throw new Error("Missing return statement in function");
@@ -1854,15 +1878,15 @@ public class PrismParser implements PrismParserConstants {
         Token begin = null;
           begin = getToken(1);
     ret = ExpressionAnd(prop, pathprop);
-    label_19:
+    label_20:
     while (true) {
       switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
       case OR:
         ;
         break;
       default:
-        jj_la1[51] = jj_gen;
-        break label_19;
+        jj_la1[52] = jj_gen;
+        break label_20;
       }
       jj_consume_token(OR);
       expr = ExpressionAnd(prop, pathprop);
@@ -1878,15 +1902,15 @@ public class PrismParser implements PrismParserConstants {
         Token begin = null;
           begin = getToken(1);
     ret = ExpressionNot(prop, pathprop);
-    label_20:
+    label_21:
     while (true) {
       switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
       case AND:
         ;
         break;
       default:
-        jj_la1[52] = jj_gen;
-        break label_20;
+        jj_la1[53] = jj_gen;
+        break label_21;
       }
       jj_consume_token(AND);
       expr = ExpressionNot(prop, pathprop);
@@ -1930,7 +1954,7 @@ public class PrismParser implements PrismParserConstants {
       ret = ExpressionEquality(prop, pathprop);
       break;
     default:
-      jj_la1[53] = jj_gen;
+      jj_la1[54] = jj_gen;
       jj_consume_token(-1);
       throw new ParseException();
     }
@@ -1945,7 +1969,7 @@ public class PrismParser implements PrismParserConstants {
         Token begin = null;
           begin = getToken(1);
     ret = ExpressionRelop(prop, pathprop);
-    label_21:
+    label_22:
     while (true) {
       switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
       case EQ:
@@ -1953,8 +1977,8 @@ public class PrismParser implements PrismParserConstants {
         ;
         break;
       default:
-        jj_la1[54] = jj_gen;
-        break label_21;
+        jj_la1[55] = jj_gen;
+        break label_22;
       }
       op = EqNeq();
       expr = ExpressionRelop(prop, pathprop);
@@ -1971,7 +1995,7 @@ public class PrismParser implements PrismParserConstants {
         Token begin = null;
           begin = getToken(1);
     ret = ExpressionPlusMinus(prop, pathprop);
-    label_22:
+    label_23:
     while (true) {
       switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
       case LT:
@@ -1981,8 +2005,8 @@ public class PrismParser implements PrismParserConstants {
         ;
         break;
       default:
-        jj_la1[55] = jj_gen;
-        break label_22;
+        jj_la1[56] = jj_gen;
+        break label_23;
       }
       op = LtGt();
       expr = ExpressionPlusMinus(prop, pathprop);
@@ -2006,7 +2030,7 @@ public class PrismParser implements PrismParserConstants {
         Token begin = null;
           begin = getToken(1);
     ret = ExpressionTimesDivide(prop, pathprop);
-    label_23:
+    label_24:
     while (true) {
       switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
       case PLUS:
@@ -2014,8 +2038,8 @@ public class PrismParser implements PrismParserConstants {
         ;
         break;
       default:
-        jj_la1[56] = jj_gen;
-        break label_23;
+        jj_la1[57] = jj_gen;
+        break label_24;
       }
       switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
       case PLUS:
@@ -2027,7 +2051,7 @@ public class PrismParser implements PrismParserConstants {
                                                                        op = ExpressionBinaryOp.MINUS;
         break;
       default:
-        jj_la1[57] = jj_gen;
+        jj_la1[58] = jj_gen;
         jj_consume_token(-1);
         throw new ParseException();
       }
@@ -2045,7 +2069,7 @@ public class PrismParser implements PrismParserConstants {
         Token begin = null;
           begin = getToken(1);
     ret = ExpressionUnaryMinus(prop, pathprop);
-    label_24:
+    label_25:
     while (true) {
       switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
       case TIMES:
@@ -2053,8 +2077,8 @@ public class PrismParser implements PrismParserConstants {
         ;
         break;
       default:
-        jj_la1[58] = jj_gen;
-        break label_24;
+        jj_la1[59] = jj_gen;
+        break label_25;
       }
       switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
       case TIMES:
@@ -2066,7 +2090,7 @@ public class PrismParser implements PrismParserConstants {
                                                                           op = ExpressionBinaryOp.DIVIDE;
         break;
       default:
-        jj_la1[59] = jj_gen;
+        jj_la1[60] = jj_gen;
         jj_consume_token(-1);
         throw new ParseException();
       }
@@ -2110,7 +2134,7 @@ public class PrismParser implements PrismParserConstants {
       ret = ExpressionBasic(prop, pathprop);
       break;
     default:
-      jj_la1[60] = jj_gen;
+      jj_la1[61] = jj_gen;
       jj_consume_token(-1);
       throw new ParseException();
     }
@@ -2168,7 +2192,7 @@ public class PrismParser implements PrismParserConstants {
       ret = ExpressionFilter(prop, pathprop);
       break;
     default:
-      jj_la1[61] = jj_gen;
+      jj_la1[62] = jj_gen;
       jj_consume_token(-1);
       throw new ParseException();
     }
@@ -2199,7 +2223,7 @@ public class PrismParser implements PrismParserConstants {
       jj_consume_token(RPARENTH);
       break;
     default:
-      jj_la1[62] = jj_gen;
+      jj_la1[63] = jj_gen;
       ;
     }
           ret.setPosition(begin, getToken(0)); {if (true) return ret;}
@@ -2221,7 +2245,7 @@ public class PrismParser implements PrismParserConstants {
                                                          s = "max";
       break;
     default:
-      jj_la1[63] = jj_gen;
+      jj_la1[64] = jj_gen;
       jj_consume_token(-1);
       throw new ParseException();
     }
@@ -2253,7 +2277,7 @@ public class PrismParser implements PrismParserConstants {
       s = Identifier();
       break;
     default:
-      jj_la1[64] = jj_gen;
+      jj_la1[65] = jj_gen;
       jj_consume_token(-1);
       throw new ParseException();
     }
@@ -2270,15 +2294,15 @@ public class PrismParser implements PrismParserConstants {
         Expression expr;
     expr = Expression(prop, pathprop);
                                             func.addOperand(expr);
-    label_25:
+    label_26:
     while (true) {
       switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
       case COMMA:
         ;
         break;
       default:
-        jj_la1[65] = jj_gen;
-        break label_25;
+        jj_la1[66] = jj_gen;
+        break label_26;
       }
       jj_consume_token(COMMA);
       expr = Expression(prop, pathprop);
@@ -2321,7 +2345,7 @@ public class PrismParser implements PrismParserConstants {
                   ret = new ExpressionLiteral(TypeBool.getInstance(), new Boolean(false));
       break;
     default:
-      jj_la1[66] = jj_gen;
+      jj_la1[67] = jj_gen;
       jj_consume_token(-1);
       throw new ParseException();
     }
@@ -2385,7 +2409,7 @@ public class PrismParser implements PrismParserConstants {
                                        relOp = "max="; isBool = false;
         break;
       default:
-        jj_la1[67] = jj_gen;
+        jj_la1[68] = jj_gen;
         jj_consume_token(-1);
         throw new ParseException();
       }
@@ -2403,7 +2427,7 @@ public class PrismParser implements PrismParserConstants {
                                          relOp = "max="; isBool = false;
       break;
     default:
-      jj_la1[68] = jj_gen;
+      jj_la1[69] = jj_gen;
       jj_consume_token(-1);
       throw new ParseException();
     }
@@ -2414,7 +2438,7 @@ public class PrismParser implements PrismParserConstants {
       filter = Filter();
       break;
     default:
-      jj_la1[69] = jj_gen;
+      jj_la1[70] = jj_gen;
       ;
     }
     jj_consume_token(RBRACKET);
@@ -2444,15 +2468,15 @@ public class PrismParser implements PrismParserConstants {
     expr = Expression(true, false);
                                                           filter = new Filter(expr);
     jj_consume_token(RBRACE);
-    label_26:
+    label_27:
     while (true) {
       switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
       case LBRACE:
         ;
         break;
       default:
-        jj_la1[70] = jj_gen;
-        break label_26;
+        jj_la1[71] = jj_gen;
+        break label_27;
       }
       jj_consume_token(LBRACE);
       switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
@@ -2465,7 +2489,7 @@ public class PrismParser implements PrismParserConstants {
                           filter.setMaxRequested(true);
         break;
       default:
-        jj_la1[71] = jj_gen;
+        jj_la1[72] = jj_gen;
         jj_consume_token(-1);
         throw new ParseException();
       }
@@ -2503,7 +2527,7 @@ public class PrismParser implements PrismParserConstants {
                                  relOp = "="; isBool = false;
       break;
     default:
-      jj_la1[72] = jj_gen;
+      jj_la1[73] = jj_gen;
       jj_consume_token(-1);
       throw new ParseException();
     }
@@ -2514,7 +2538,7 @@ public class PrismParser implements PrismParserConstants {
       filter = Filter();
       break;
     default:
-      jj_la1[73] = jj_gen;
+      jj_la1[74] = jj_gen;
       ;
     }
     jj_consume_token(RBRACKET);
@@ -2555,7 +2579,7 @@ public class PrismParser implements PrismParserConstants {
         index = RewardIndex();
         break;
       default:
-        jj_la1[74] = jj_gen;
+        jj_la1[75] = jj_gen;
         ;
       }
       switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
@@ -2585,7 +2609,7 @@ public class PrismParser implements PrismParserConstants {
                                    relOp = "max="; isBool = false;
         break;
       default:
-        jj_la1[75] = jj_gen;
+        jj_la1[76] = jj_gen;
         jj_consume_token(-1);
         throw new ParseException();
       }
@@ -2603,7 +2627,7 @@ public class PrismParser implements PrismParserConstants {
                                          relOp = "max="; isBool = false;
       break;
     default:
-      jj_la1[76] = jj_gen;
+      jj_la1[77] = jj_gen;
       jj_consume_token(-1);
       throw new ParseException();
     }
@@ -2614,7 +2638,7 @@ public class PrismParser implements PrismParserConstants {
       filter = Filter();
       break;
     default:
-      jj_la1[77] = jj_gen;
+      jj_la1[78] = jj_gen;
       ;
     }
     jj_consume_token(RBRACKET);
@@ -2674,7 +2698,7 @@ public class PrismParser implements PrismParserConstants {
         index = Expression(false, false);
         break;
       default:
-        jj_la1[78] = jj_gen;
+        jj_la1[79] = jj_gen;
         jj_consume_token(-1);
         throw new ParseException();
       }
@@ -2712,7 +2736,7 @@ public class PrismParser implements PrismParserConstants {
                         ret = new ExpressionTemporal(ExpressionTemporal.R_S, null, null);
       break;
     default:
-      jj_la1[79] = jj_gen;
+      jj_la1[80] = jj_gen;
       jj_consume_token(-1);
       throw new ParseException();
     }
@@ -2768,7 +2792,7 @@ public class PrismParser implements PrismParserConstants {
                                                        s = "init";
       break;
     default:
-      jj_la1[80] = jj_gen;
+      jj_la1[81] = jj_gen;
       jj_consume_token(-1);
       throw new ParseException();
     }
@@ -2813,7 +2837,7 @@ public class PrismParser implements PrismParserConstants {
       op = Identifier();
       break;
     default:
-      jj_la1[81] = jj_gen;
+      jj_la1[82] = jj_gen;
       jj_consume_token(-1);
       throw new ParseException();
     }
@@ -2825,7 +2849,7 @@ public class PrismParser implements PrismParserConstants {
       filter = Expression(prop, pathprop);
       break;
     default:
-      jj_la1[82] = jj_gen;
+      jj_la1[83] = jj_gen;
       ;
     }
     jj_consume_token(RPARENTH);
@@ -2870,7 +2894,7 @@ public class PrismParser implements PrismParserConstants {
                                                                   ident="max";
       break;
     default:
-      jj_la1[83] = jj_gen;
+      jj_la1[84] = jj_gen;
       jj_consume_token(-1);
       throw new ParseException();
     }
@@ -2903,7 +2927,7 @@ public class PrismParser implements PrismParserConstants {
               {if (true) return ExpressionBinaryOp.NE;}
       break;
     default:
-      jj_la1[84] = jj_gen;
+      jj_la1[85] = jj_gen;
       jj_consume_token(-1);
       throw new ParseException();
     }
@@ -2930,7 +2954,7 @@ public class PrismParser implements PrismParserConstants {
               {if (true) return ExpressionBinaryOp.LE;}
       break;
     default:
-      jj_la1[85] = jj_gen;
+      jj_la1[86] = jj_gen;
       jj_consume_token(-1);
       throw new ParseException();
     }
@@ -2955,7 +2979,7 @@ public class PrismParser implements PrismParserConstants {
       step = Expression(false, false);
       break;
     default:
-      jj_la1[86] = jj_gen;
+      jj_la1[87] = jj_gen;
       ;
     }
     jj_consume_token(0);
@@ -3067,184 +3091,199 @@ public class PrismParser implements PrismParserConstants {
   }
 
   static private boolean jj_3_13() {
-    if (jj_3R_29()) return true;
+    if (jj_3R_30()) return true;
     if (jj_scan_token(LPARENTH)) return true;
     return false;
   }
 
-  static private boolean jj_3R_57() {
-    if (jj_3R_67()) return true;
+  static private boolean jj_3R_58() {
+    if (jj_3R_68()) return true;
     Token xsp;
     while (true) {
       xsp = jj_scanpos;
-      if (jj_3R_68()) { jj_scanpos = xsp; break; }
+      if (jj_3R_69()) { jj_scanpos = xsp; break; }
     }
     return false;
   }
 
   static private boolean jj_3_11() {
-    if (jj_3R_29()) return true;
+    if (jj_3R_30()) return true;
     if (jj_scan_token(LPARENTH)) return true;
     return false;
   }
 
-  static private boolean jj_3R_65() {
-    if (jj_3R_29()) return true;
+  static private boolean jj_3R_66() {
+    if (jj_3R_30()) return true;
     return false;
   }
 
-  static private boolean jj_3R_58() {
+  static private boolean jj_3R_59() {
     if (jj_scan_token(IMPLIES)) return true;
-    if (jj_3R_57()) return true;
+    if (jj_3R_58()) return true;
     return false;
   }
 
-  static private boolean jj_3R_61() {
-    if (jj_3R_29()) return true;
+  static private boolean jj_3R_62() {
+    if (jj_3R_30()) return true;
     return false;
   }
 
-  static private boolean jj_3R_50() {
-    if (jj_3R_57()) return true;
+  static private boolean jj_3R_51() {
+    if (jj_3R_58()) return true;
     Token xsp;
     while (true) {
       xsp = jj_scanpos;
-      if (jj_3R_58()) { jj_scanpos = xsp; break; }
+      if (jj_3R_59()) { jj_scanpos = xsp; break; }
     }
     return false;
   }
 
-  static private boolean jj_3R_51() {
+  static private boolean jj_3R_140() {
+    if (jj_scan_token(EQ)) return true;
     if (jj_scan_token(QMARK)) return true;
-    if (jj_3R_50()) return true;
+    return false;
+  }
+
+  static private boolean jj_3R_139() {
+    if (jj_3R_84()) return true;
+    if (jj_3R_35()) return true;
+    return false;
+  }
+
+  static private boolean jj_3R_52() {
+    if (jj_scan_token(QMARK)) return true;
+    if (jj_3R_51()) return true;
     if (jj_scan_token(COLON)) return true;
-    if (jj_3R_48()) return true;
+    if (jj_3R_49()) return true;
     return false;
   }
 
   static private boolean jj_3_12() {
-    if (jj_3R_29()) return true;
+    if (jj_3R_30()) return true;
     if (jj_scan_token(LPARENTH)) return true;
     return false;
   }
 
   static private boolean jj_3_10() {
-    if (jj_3R_29()) return true;
+    if (jj_3R_30()) return true;
     if (jj_scan_token(LPARENTH)) return true;
     return false;
   }
 
-  static private boolean jj_3R_137() {
-    if (jj_scan_token(EQ)) return true;
-    if (jj_scan_token(QMARK)) return true;
+  static private boolean jj_3R_118() {
+    if (jj_scan_token(S)) return true;
+    Token xsp;
+    xsp = jj_scanpos;
+    if (jj_3R_139()) {
+    jj_scanpos = xsp;
+    if (jj_3R_140()) return true;
+    }
+    if (jj_scan_token(LBRACKET)) return true;
+    if (jj_3R_35()) return true;
+    xsp = jj_scanpos;
+    if (jj_3R_141()) jj_scanpos = xsp;
+    if (jj_scan_token(RBRACKET)) return true;
     return false;
   }
 
-  static private boolean jj_3R_136() {
-    if (jj_3R_81()) return true;
-    if (jj_3R_34()) return true;
+  static private boolean jj_3R_49() {
+    if (jj_3R_51()) return true;
+    Token xsp;
+    xsp = jj_scanpos;
+    if (jj_3R_52()) jj_scanpos = xsp;
     return false;
   }
 
-  static private boolean jj_3R_48() {
-    if (jj_3R_50()) return true;
-    Token xsp;
-    xsp = jj_scanpos;
-    if (jj_3R_51()) jj_scanpos = xsp;
+  static private boolean jj_3R_64() {
+    if (jj_3R_30()) return true;
     return false;
   }
 
-  static private boolean jj_3R_63() {
-    if (jj_3R_29()) return true;
+  static private boolean jj_3R_138() {
+    if (jj_3R_161()) return true;
     return false;
   }
 
-  static private boolean jj_3R_59() {
-    if (jj_3R_29()) return true;
+  static private boolean jj_3R_174() {
+    if (jj_scan_token(MAX)) return true;
     return false;
   }
 
-  static private boolean jj_3R_56() {
-    if (jj_scan_token(LBRACKET)) return true;
-    if (jj_3R_34()) return true;
-    if (jj_scan_token(COMMA)) return true;
-    if (jj_3R_34()) return true;
-    if (jj_scan_token(RBRACKET)) return true;
+  static private boolean jj_3R_60() {
+    if (jj_3R_30()) return true;
     return false;
   }
 
-  static private boolean jj_3R_115() {
-    if (jj_scan_token(S)) return true;
-    Token xsp;
-    xsp = jj_scanpos;
-    if (jj_3R_136()) {
-    jj_scanpos = xsp;
-    if (jj_3R_137()) return true;
-    }
+  static private boolean jj_3R_173() {
+    if (jj_scan_token(MIN)) return true;
+    return false;
+  }
+
+  static private boolean jj_3R_57() {
     if (jj_scan_token(LBRACKET)) return true;
-    if (jj_3R_34()) return true;
-    xsp = jj_scanpos;
-    if (jj_3R_138()) jj_scanpos = xsp;
+    if (jj_3R_35()) return true;
+    if (jj_scan_token(COMMA)) return true;
+    if (jj_3R_35()) return true;
     if (jj_scan_token(RBRACKET)) return true;
     return false;
   }
 
-  static private boolean jj_3R_55() {
+  static private boolean jj_3R_56() {
     if (jj_scan_token(GT)) return true;
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_65()) {
+    if (jj_3R_66()) {
     jj_scanpos = xsp;
-    if (jj_3R_66()) return true;
+    if (jj_3R_67()) return true;
     }
     return false;
   }
 
-  static private boolean jj_3R_54() {
+  static private boolean jj_3R_55() {
     if (jj_scan_token(GE)) return true;
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_63()) {
+    if (jj_3R_64()) {
     jj_scanpos = xsp;
-    if (jj_3R_64()) return true;
+    if (jj_3R_65()) return true;
     }
     return false;
   }
 
-  static private boolean jj_3R_53() {
+  static private boolean jj_3R_54() {
     if (jj_scan_token(LT)) return true;
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_61()) {
+    if (jj_3R_62()) {
     jj_scanpos = xsp;
-    if (jj_3R_62()) return true;
+    if (jj_3R_63()) return true;
     }
     return false;
   }
 
-  static private boolean jj_3R_52() {
+  static private boolean jj_3R_53() {
     if (jj_scan_token(LE)) return true;
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_59()) {
+    if (jj_3R_60()) {
     jj_scanpos = xsp;
-    if (jj_3R_60()) return true;
+    if (jj_3R_61()) return true;
     }
     return false;
   }
 
-  static private boolean jj_3R_49() {
+  static private boolean jj_3R_50() {
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_52()) {
-    jj_scanpos = xsp;
     if (jj_3R_53()) {
     jj_scanpos = xsp;
     if (jj_3R_54()) {
     jj_scanpos = xsp;
     if (jj_3R_55()) {
     jj_scanpos = xsp;
-    if (jj_3R_56()) return true;
+    if (jj_3R_56()) {
+    jj_scanpos = xsp;
+    if (jj_3R_57()) return true;
     }
     }
     }
@@ -3252,223 +3291,215 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
-  static private boolean jj_3R_135() {
-    if (jj_3R_158()) return true;
-    return false;
-  }
-
   static private boolean jj_3R_171() {
-    if (jj_scan_token(MAX)) return true;
+    if (jj_scan_token(LBRACE)) return true;
+    Token xsp;
+    xsp = jj_scanpos;
+    if (jj_3R_173()) {
+    jj_scanpos = xsp;
+    if (jj_3R_174()) return true;
+    }
+    if (jj_scan_token(RBRACE)) return true;
     return false;
   }
 
-  static private boolean jj_3R_170() {
-    if (jj_scan_token(MIN)) return true;
+  static private boolean jj_3R_161() {
+    if (jj_scan_token(LBRACE)) return true;
+    if (jj_3R_35()) return true;
+    if (jj_scan_token(RBRACE)) return true;
+    Token xsp;
+    while (true) {
+      xsp = jj_scanpos;
+      if (jj_3R_171()) { jj_scanpos = xsp; break; }
+    }
     return false;
   }
 
-  static private boolean jj_3R_39() {
-    if (jj_3R_48()) return true;
+  static private boolean jj_3R_40() {
+    if (jj_3R_49()) return true;
     return false;
   }
 
-  static private boolean jj_3R_47() {
-    if (jj_3R_49()) return true;
+  static private boolean jj_3R_48() {
+    if (jj_3R_50()) return true;
     return false;
   }
 
-  static private boolean jj_3R_46() {
+  static private boolean jj_3R_47() {
     if (jj_scan_token(G)) return true;
     return false;
   }
 
-  static private boolean jj_3R_45() {
+  static private boolean jj_3R_46() {
     if (jj_scan_token(F)) return true;
     return false;
   }
 
-  static private boolean jj_3R_44() {
+  static private boolean jj_3R_45() {
     if (jj_scan_token(X)) return true;
     return false;
   }
 
-  static private boolean jj_3R_168() {
-    if (jj_scan_token(LBRACE)) return true;
+  static private boolean jj_3R_39() {
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_170()) {
+    if (jj_3R_45()) {
+    jj_scanpos = xsp;
+    if (jj_3R_46()) {
     jj_scanpos = xsp;
-    if (jj_3R_171()) return true;
+    if (jj_3R_47()) return true;
     }
-    if (jj_scan_token(RBRACE)) return true;
+    }
+    xsp = jj_scanpos;
+    if (jj_3R_48()) jj_scanpos = xsp;
+    if (jj_3R_37()) return true;
     return false;
   }
 
-  static private boolean jj_3R_38() {
+  static private boolean jj_3R_157() {
+    if (jj_3R_84()) return true;
+    if (jj_3R_35()) return true;
+    return false;
+  }
+
+  static private boolean jj_3R_37() {
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_44()) {
-    jj_scanpos = xsp;
-    if (jj_3R_45()) {
+    if (jj_3R_39()) {
     jj_scanpos = xsp;
-    if (jj_3R_46()) return true;
-    }
+    if (jj_3R_40()) return true;
     }
-    xsp = jj_scanpos;
-    if (jj_3R_47()) jj_scanpos = xsp;
-    if (jj_3R_36()) return true;
     return false;
   }
 
-  static private boolean jj_3R_158() {
-    if (jj_scan_token(LBRACE)) return true;
-    if (jj_3R_34()) return true;
-    if (jj_scan_token(RBRACE)) return true;
-    Token xsp;
-    while (true) {
-      xsp = jj_scanpos;
-      if (jj_3R_168()) { jj_scanpos = xsp; break; }
-    }
+  static private boolean jj_3R_160() {
+    if (jj_scan_token(MAX)) return true;
+    if (jj_scan_token(EQ)) return true;
+    if (jj_scan_token(QMARK)) return true;
     return false;
   }
 
-  static private boolean jj_3R_36() {
-    Token xsp;
-    xsp = jj_scanpos;
-    if (jj_3R_38()) {
-    jj_scanpos = xsp;
-    if (jj_3R_39()) return true;
-    }
+  static private boolean jj_3R_44() {
+    if (jj_3R_50()) return true;
     return false;
   }
 
-  static private boolean jj_3R_43() {
-    if (jj_3R_49()) return true;
+  static private boolean jj_3R_159() {
+    if (jj_scan_token(MIN)) return true;
+    if (jj_scan_token(EQ)) return true;
+    if (jj_scan_token(QMARK)) return true;
     return false;
   }
 
-  static private boolean jj_3R_42() {
+  static private boolean jj_3R_43() {
     if (jj_scan_token(R)) return true;
     return false;
   }
 
-  static private boolean jj_3R_41() {
-    if (jj_scan_token(W)) return true;
-    return false;
-  }
-
-  static private boolean jj_3R_40() {
-    if (jj_scan_token(U)) return true;
-    return false;
-  }
-
-  static private boolean jj_3R_37() {
-    Token xsp;
-    xsp = jj_scanpos;
-    if (jj_3R_40()) {
-    jj_scanpos = xsp;
-    if (jj_3R_41()) {
-    jj_scanpos = xsp;
-    if (jj_3R_42()) return true;
-    }
-    }
-    xsp = jj_scanpos;
-    if (jj_3R_43()) jj_scanpos = xsp;
-    if (jj_3R_36()) return true;
-    return false;
-  }
-
-  static private boolean jj_3R_154() {
-    if (jj_3R_81()) return true;
-    if (jj_3R_34()) return true;
+  static private boolean jj_3R_158() {
+    if (jj_scan_token(EQ)) return true;
+    if (jj_scan_token(QMARK)) return true;
     return false;
   }
 
-  static private boolean jj_3R_157() {
-    if (jj_scan_token(MAX)) return true;
-    if (jj_scan_token(EQ)) return true;
-    if (jj_scan_token(QMARK)) return true;
+  static private boolean jj_3R_42() {
+    if (jj_scan_token(W)) return true;
     return false;
   }
 
-  static private boolean jj_3R_156() {
-    if (jj_scan_token(MIN)) return true;
-    if (jj_scan_token(EQ)) return true;
-    if (jj_scan_token(QMARK)) return true;
+  static private boolean jj_3R_41() {
+    if (jj_scan_token(U)) return true;
     return false;
   }
 
-  static private boolean jj_3R_155() {
+  static private boolean jj_3R_137() {
+    if (jj_scan_token(PMAX)) return true;
     if (jj_scan_token(EQ)) return true;
     if (jj_scan_token(QMARK)) return true;
     return false;
   }
 
-  static private boolean jj_3R_134() {
-    if (jj_scan_token(PMAX)) return true;
+  static private boolean jj_3R_136() {
+    if (jj_scan_token(PMIN)) return true;
     if (jj_scan_token(EQ)) return true;
     if (jj_scan_token(QMARK)) return true;
     return false;
   }
 
-  static private boolean jj_3R_35() {
-    if (jj_3R_36()) return true;
+  static private boolean jj_3R_38() {
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_37()) jj_scanpos = xsp;
-    return false;
-  }
-
-  static private boolean jj_3R_133() {
-    if (jj_scan_token(PMIN)) return true;
-    if (jj_scan_token(EQ)) return true;
-    if (jj_scan_token(QMARK)) return true;
+    if (jj_3R_41()) {
+    jj_scanpos = xsp;
+    if (jj_3R_42()) {
+    jj_scanpos = xsp;
+    if (jj_3R_43()) return true;
+    }
+    }
+    xsp = jj_scanpos;
+    if (jj_3R_44()) jj_scanpos = xsp;
+    if (jj_3R_37()) return true;
     return false;
   }
 
-  static private boolean jj_3R_132() {
+  static private boolean jj_3R_135() {
     if (jj_scan_token(P)) return true;
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_154()) {
+    if (jj_3R_157()) {
     jj_scanpos = xsp;
-    if (jj_3R_155()) {
+    if (jj_3R_158()) {
     jj_scanpos = xsp;
-    if (jj_3R_156()) {
+    if (jj_3R_159()) {
     jj_scanpos = xsp;
-    if (jj_3R_157()) return true;
+    if (jj_3R_160()) return true;
     }
     }
     }
     return false;
   }
 
-  static private boolean jj_3R_114() {
+  static private boolean jj_3R_117() {
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_132()) {
+    if (jj_3R_135()) {
     jj_scanpos = xsp;
-    if (jj_3R_133()) {
+    if (jj_3R_136()) {
     jj_scanpos = xsp;
-    if (jj_3R_134()) return true;
+    if (jj_3R_137()) return true;
     }
     }
     if (jj_scan_token(LBRACKET)) return true;
-    if (jj_3R_34()) return true;
+    if (jj_3R_35()) return true;
     xsp = jj_scanpos;
-    if (jj_3R_135()) jj_scanpos = xsp;
+    if (jj_3R_138()) jj_scanpos = xsp;
     if (jj_scan_token(RBRACKET)) return true;
     return false;
   }
 
-  static private boolean jj_3R_153() {
+  static private boolean jj_3R_36() {
+    if (jj_3R_37()) return true;
+    Token xsp;
+    xsp = jj_scanpos;
+    if (jj_3R_38()) jj_scanpos = xsp;
+    return false;
+  }
+
+  static private boolean jj_3R_156() {
     if (jj_scan_token(COMMA)) return true;
-    if (jj_3R_34()) return true;
+    if (jj_3R_35()) return true;
     return false;
   }
 
-  static private boolean jj_3R_131() {
-    if (jj_3R_27()) return true;
+  static private boolean jj_3R_134() {
+    if (jj_3R_28()) return true;
+    return false;
+  }
+
+  static private boolean jj_3R_116() {
+    if (jj_scan_token(LPARENTH)) return true;
+    if (jj_3R_35()) return true;
+    if (jj_scan_token(RPARENTH)) return true;
     return false;
   }
 
@@ -3483,382 +3514,369 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
-  static private boolean jj_3R_34() {
-    if (jj_3R_35()) return true;
-    return false;
-  }
-
-  static private boolean jj_3R_113() {
-    if (jj_scan_token(LPARENTH)) return true;
-    if (jj_3R_34()) return true;
-    if (jj_scan_token(RPARENTH)) return true;
+  static private boolean jj_3R_133() {
+    if (jj_scan_token(MAX)) return true;
     return false;
   }
 
-  static private boolean jj_3R_130() {
-    if (jj_scan_token(MAX)) return true;
+  static private boolean jj_3R_35() {
+    if (jj_3R_36()) return true;
     return false;
   }
 
-  static private boolean jj_3R_124() {
+  static private boolean jj_3R_127() {
     if (jj_scan_token(FALSE)) return true;
     return false;
   }
 
-  static private boolean jj_3R_123() {
+  static private boolean jj_3R_126() {
     if (jj_scan_token(TRUE)) return true;
     return false;
   }
 
-  static private boolean jj_3R_122() {
+  static private boolean jj_3R_125() {
     if (jj_scan_token(REG_DOUBLE)) return true;
     return false;
   }
 
-  static private boolean jj_3_8() {
-    if (jj_scan_token(OR)) return true;
-    if (jj_scan_token(OR)) return true;
-    if (jj_scan_token(OR)) return true;
-    return false;
-  }
-
-  static private boolean jj_3R_129() {
+  static private boolean jj_3R_132() {
     if (jj_scan_token(MIN)) return true;
     return false;
   }
 
-  static private boolean jj_3R_121() {
+  static private boolean jj_3R_124() {
     if (jj_scan_token(REG_INT)) return true;
     return false;
   }
 
-  static private boolean jj_3R_109() {
+  static private boolean jj_3R_112() {
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_121()) {
+    if (jj_3R_124()) {
     jj_scanpos = xsp;
-    if (jj_3R_122()) {
+    if (jj_3R_125()) {
     jj_scanpos = xsp;
-    if (jj_3R_123()) {
+    if (jj_3R_126()) {
     jj_scanpos = xsp;
-    if (jj_3R_124()) return true;
+    if (jj_3R_127()) return true;
     }
     }
     }
     return false;
   }
 
-  static private boolean jj_3R_127() {
+  static private boolean jj_3R_130() {
     if (jj_scan_token(MAX)) return true;
     return false;
   }
 
-  static private boolean jj_3R_91() {
+  static private boolean jj_3R_94() {
     if (jj_scan_token(LE)) return true;
     return false;
   }
 
-  static private boolean jj_3R_90() {
+  static private boolean jj_3R_93() {
     if (jj_scan_token(GE)) return true;
     return false;
   }
 
-  static private boolean jj_3R_89() {
+  static private boolean jj_3_8() {
+    if (jj_scan_token(OR)) return true;
+    if (jj_scan_token(OR)) return true;
+    if (jj_scan_token(OR)) return true;
+    return false;
+  }
+
+  static private boolean jj_3R_92() {
     if (jj_scan_token(LT)) return true;
     return false;
   }
 
-  static private boolean jj_3R_81() {
+  static private boolean jj_3R_84() {
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_88()) {
+    if (jj_3R_91()) {
     jj_scanpos = xsp;
-    if (jj_3R_89()) {
+    if (jj_3R_92()) {
     jj_scanpos = xsp;
-    if (jj_3R_90()) {
+    if (jj_3R_93()) {
     jj_scanpos = xsp;
-    if (jj_3R_91()) return true;
+    if (jj_3R_94()) return true;
     }
     }
     }
     return false;
   }
 
-  static private boolean jj_3R_88() {
+  static private boolean jj_3R_91() {
     if (jj_scan_token(GT)) return true;
     return false;
   }
 
-  static private boolean jj_3R_128() {
-    if (jj_3R_34()) return true;
+  static private boolean jj_3R_131() {
+    if (jj_3R_35()) return true;
     Token xsp;
     while (true) {
       xsp = jj_scanpos;
-      if (jj_3R_153()) { jj_scanpos = xsp; break; }
+      if (jj_3R_156()) { jj_scanpos = xsp; break; }
     }
     return false;
   }
 
-  static private boolean jj_3_2() {
-    if (jj_scan_token(DQUOTE)) return true;
-    if (jj_3R_27()) return true;
-    if (jj_scan_token(DQUOTE)) return true;
-    if (jj_scan_token(COLON)) return true;
-    return false;
-  }
-
-  static private boolean jj_3_7() {
-    if (jj_scan_token(OR)) return true;
-    if (jj_scan_token(OR)) return true;
-    return false;
-  }
-
-  static private boolean jj_3R_83() {
+  static private boolean jj_3R_86() {
     if (jj_scan_token(NE)) return true;
     return false;
   }
 
-  static private boolean jj_3R_82() {
-    if (jj_scan_token(EQ)) return true;
-    return false;
-  }
-
-  static private boolean jj_3R_78() {
+  static private boolean jj_3R_81() {
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_82()) {
+    if (jj_3R_85()) {
     jj_scanpos = xsp;
-    if (jj_3R_83()) return true;
+    if (jj_3R_86()) return true;
     }
     return false;
   }
 
-  static private boolean jj_3R_112() {
+  static private boolean jj_3R_85() {
+    if (jj_scan_token(EQ)) return true;
+    return false;
+  }
+
+  static private boolean jj_3R_115() {
     if (jj_scan_token(FUNC)) return true;
     if (jj_scan_token(LPARENTH)) return true;
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_129()) {
+    if (jj_3R_132()) {
     jj_scanpos = xsp;
-    if (jj_3R_130()) {
+    if (jj_3R_133()) {
     jj_scanpos = xsp;
-    if (jj_3R_131()) return true;
+    if (jj_3R_134()) return true;
     }
     }
     if (jj_scan_token(COMMA)) return true;
-    if (jj_3R_128()) return true;
+    if (jj_3R_131()) return true;
     if (jj_scan_token(RPARENTH)) return true;
     return false;
   }
 
-  static private boolean jj_3_9() {
+  static private boolean jj_3_2() {
+    if (jj_scan_token(DQUOTE)) return true;
+    if (jj_3R_28()) return true;
+    if (jj_scan_token(DQUOTE)) return true;
+    if (jj_scan_token(COLON)) return true;
+    return false;
+  }
+
+  static private boolean jj_3_7() {
+    if (jj_scan_token(OR)) return true;
     if (jj_scan_token(OR)) return true;
-    if (jj_scan_token(LBRACKET)) return true;
     return false;
   }
 
-  static private boolean jj_3R_126() {
+  static private boolean jj_3R_129() {
     if (jj_scan_token(MIN)) return true;
     return false;
   }
 
-  static private boolean jj_3R_111() {
+  static private boolean jj_3R_114() {
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_126()) {
+    if (jj_3R_129()) {
     jj_scanpos = xsp;
-    if (jj_3R_127()) return true;
+    if (jj_3R_130()) return true;
     }
     if (jj_scan_token(LPARENTH)) return true;
-    if (jj_3R_128()) return true;
+    if (jj_3R_131()) return true;
     if (jj_scan_token(RPARENTH)) return true;
     return false;
   }
 
-  static private boolean jj_3R_33() {
+  static private boolean jj_3R_34() {
     if (jj_scan_token(REG_IDENTPRIME)) return true;
     return false;
   }
 
-  static private boolean jj_3R_150() {
+  static private boolean jj_3_9() {
     if (jj_scan_token(OR)) return true;
+    if (jj_scan_token(LBRACKET)) return true;
     return false;
   }
 
-  static private boolean jj_3R_125() {
+  static private boolean jj_3R_153() {
+    if (jj_scan_token(OR)) return true;
+    return false;
+  }
+
+  static private boolean jj_3R_128() {
     if (jj_scan_token(LPARENTH)) return true;
-    if (jj_3R_128()) return true;
+    if (jj_3R_131()) return true;
     if (jj_scan_token(RPARENTH)) return true;
     return false;
   }
 
-  static private boolean jj_3R_110() {
-    if (jj_3R_27()) return true;
+  static private boolean jj_3R_113() {
+    if (jj_3R_28()) return true;
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_125()) jj_scanpos = xsp;
+    if (jj_3R_128()) jj_scanpos = xsp;
     return false;
   }
 
-  static private boolean jj_3R_29() {
-    if (jj_3R_27()) return true;
+  static private boolean jj_3R_30() {
+    if (jj_3R_28()) return true;
     return false;
   }
 
-  static private boolean jj_3R_108() {
-    if (jj_3R_120()) return true;
+  static private boolean jj_3R_111() {
+    if (jj_3R_123()) return true;
     return false;
   }
 
-  static private boolean jj_3R_147() {
+  static private boolean jj_3R_150() {
     if (jj_scan_token(MAX)) return true;
     return false;
   }
 
-  static private boolean jj_3R_149() {
+  static private boolean jj_3R_152() {
     if (jj_scan_token(AND)) return true;
     return false;
   }
 
-  static private boolean jj_3R_107() {
-    if (jj_3R_119()) return true;
+  static private boolean jj_3R_110() {
+    if (jj_3R_122()) return true;
     return false;
   }
 
-  static private boolean jj_3R_106() {
-    if (jj_3R_118()) return true;
+  static private boolean jj_3R_109() {
+    if (jj_3R_121()) return true;
     return false;
   }
 
-  static private boolean jj_3R_27() {
+  static private boolean jj_3R_28() {
     if (jj_scan_token(REG_IDENT)) return true;
     return false;
   }
 
-  static private boolean jj_3R_105() {
-    if (jj_3R_117()) return true;
+  static private boolean jj_3R_108() {
+    if (jj_3R_120()) return true;
     return false;
   }
 
-  static private boolean jj_3R_95() {
+  static private boolean jj_3R_98() {
     if (jj_scan_token(DIVIDE)) return true;
     return false;
   }
 
-  static private boolean jj_3R_104() {
-    if (jj_3R_116()) return true;
+  static private boolean jj_3R_107() {
+    if (jj_3R_119()) return true;
     return false;
   }
 
-  static private boolean jj_3R_145() {
+  static private boolean jj_3R_148() {
     if (jj_scan_token(INIT)) return true;
     return false;
   }
 
-  static private boolean jj_3R_103() {
-    if (jj_3R_115()) return true;
+  static private boolean jj_3R_106() {
+    if (jj_3R_118()) return true;
     return false;
   }
 
-  static private boolean jj_3R_102() {
-    if (jj_3R_114()) return true;
+  static private boolean jj_3R_105() {
+    if (jj_3R_117()) return true;
     return false;
   }
 
-  static private boolean jj_3R_101() {
-    if (jj_3R_113()) return true;
+  static private boolean jj_3R_104() {
+    if (jj_3R_116()) return true;
     return false;
   }
 
-  static private boolean jj_3R_100() {
-    if (jj_3R_112()) return true;
+  static private boolean jj_3R_103() {
+    if (jj_3R_115()) return true;
     return false;
   }
 
-  static private boolean jj_3R_152() {
+  static private boolean jj_3R_155() {
     if (jj_scan_token(COMMA)) return true;
-    if (jj_3R_34()) return true;
+    if (jj_3R_35()) return true;
     return false;
   }
 
-  static private boolean jj_3R_99() {
-    if (jj_3R_111()) return true;
+  static private boolean jj_3R_102() {
+    if (jj_3R_114()) return true;
     return false;
   }
 
-  static private boolean jj_3R_98() {
-    if (jj_3R_110()) return true;
+  static private boolean jj_3R_101() {
+    if (jj_3R_113()) return true;
     return false;
   }
 
-  static private boolean jj_3R_151() {
-    if (jj_3R_27()) return true;
+  static private boolean jj_3R_154() {
+    if (jj_3R_28()) return true;
     return false;
   }
 
-  static private boolean jj_3R_97() {
-    if (jj_3R_109()) return true;
+  static private boolean jj_3R_100() {
+    if (jj_3R_112()) return true;
     return false;
   }
 
-  static private boolean jj_3R_148() {
+  static private boolean jj_3R_151() {
     if (jj_scan_token(PLUS)) return true;
     return false;
   }
 
-  static private boolean jj_3R_146() {
+  static private boolean jj_3R_149() {
     if (jj_scan_token(MIN)) return true;
     return false;
   }
 
-  static private boolean jj_3R_87() {
+  static private boolean jj_3R_90() {
     if (jj_scan_token(MINUS)) return true;
     return false;
   }
 
-  static private boolean jj_3R_144() {
-    if (jj_3R_27()) return true;
+  static private boolean jj_3R_147() {
+    if (jj_3R_28()) return true;
     return false;
   }
 
-  static private boolean jj_3R_120() {
+  static private boolean jj_3R_123() {
     if (jj_scan_token(FILTER)) return true;
     if (jj_scan_token(LPARENTH)) return true;
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_146()) {
+    if (jj_3R_149()) {
     jj_scanpos = xsp;
-    if (jj_3R_147()) {
+    if (jj_3R_150()) {
     jj_scanpos = xsp;
-    if (jj_3R_148()) {
+    if (jj_3R_151()) {
     jj_scanpos = xsp;
-    if (jj_3R_149()) {
+    if (jj_3R_152()) {
     jj_scanpos = xsp;
-    if (jj_3R_150()) {
+    if (jj_3R_153()) {
     jj_scanpos = xsp;
-    if (jj_3R_151()) return true;
+    if (jj_3R_154()) return true;
     }
     }
     }
     }
     }
     if (jj_scan_token(COMMA)) return true;
-    if (jj_3R_34()) return true;
+    if (jj_3R_35()) return true;
     xsp = jj_scanpos;
-    if (jj_3R_152()) jj_scanpos = xsp;
+    if (jj_3R_155()) jj_scanpos = xsp;
     if (jj_scan_token(RPARENTH)) return true;
     return false;
   }
 
-  static private boolean jj_3R_96() {
+  static private boolean jj_3R_99() {
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_97()) {
-    jj_scanpos = xsp;
-    if (jj_3R_98()) {
-    jj_scanpos = xsp;
-    if (jj_3R_99()) {
-    jj_scanpos = xsp;
     if (jj_3R_100()) {
     jj_scanpos = xsp;
     if (jj_3R_101()) {
@@ -3875,7 +3893,13 @@ public class PrismParser implements PrismParserConstants {
     jj_scanpos = xsp;
     if (jj_3R_107()) {
     jj_scanpos = xsp;
-    if (jj_3R_108()) return true;
+    if (jj_3R_108()) {
+    jj_scanpos = xsp;
+    if (jj_3R_109()) {
+    jj_scanpos = xsp;
+    if (jj_3R_110()) {
+    jj_scanpos = xsp;
+    if (jj_3R_111()) return true;
     }
     }
     }
@@ -3890,416 +3914,432 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
-  static private boolean jj_3R_93() {
-    if (jj_3R_96()) return true;
-    return false;
-  }
-
-  static private boolean jj_3_1() {
-    if (jj_scan_token(MODULE)) return true;
-    if (jj_3R_27()) return true;
-    if (jj_scan_token(EQ)) return true;
+  static private boolean jj_3R_96() {
+    if (jj_3R_99()) return true;
     return false;
   }
 
-  static private boolean jj_3R_173() {
-    if (jj_3R_34()) return true;
+  static private boolean jj_3R_176() {
+    if (jj_3R_35()) return true;
     return false;
   }
 
-  static private boolean jj_3R_92() {
+  static private boolean jj_3R_95() {
     if (jj_scan_token(MINUS)) return true;
-    if (jj_3R_84()) return true;
+    if (jj_3R_87()) return true;
     return false;
   }
 
-  static private boolean jj_3R_84() {
+  static private boolean jj_3R_87() {
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_92()) {
+    if (jj_3R_95()) {
     jj_scanpos = xsp;
-    if (jj_3R_93()) return true;
+    if (jj_3R_96()) return true;
     }
     return false;
   }
 
-  static private boolean jj_3R_119() {
+  static private boolean jj_3R_122() {
     if (jj_scan_token(DQUOTE)) return true;
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_144()) {
+    if (jj_3R_147()) {
     jj_scanpos = xsp;
-    if (jj_3R_145()) return true;
+    if (jj_3R_148()) return true;
     }
     if (jj_scan_token(DQUOTE)) return true;
     return false;
   }
 
-  static private boolean jj_3R_94() {
+  static private boolean jj_3_1() {
+    if (jj_scan_token(MODULE)) return true;
+    if (jj_3R_28()) return true;
+    if (jj_scan_token(EQ)) return true;
+    return false;
+  }
+
+  static private boolean jj_3R_97() {
     if (jj_scan_token(TIMES)) return true;
     return false;
   }
 
-  static private boolean jj_3R_85() {
+  static private boolean jj_3R_88() {
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_94()) {
+    if (jj_3R_97()) {
     jj_scanpos = xsp;
-    if (jj_3R_95()) return true;
+    if (jj_3R_98()) return true;
     }
-    if (jj_3R_84()) return true;
-    return false;
-  }
-
-  static private boolean jj_3_6() {
-    if (jj_scan_token(DQUOTE)) return true;
+    if (jj_3R_87()) return true;
     return false;
   }
 
-  static private boolean jj_3R_79() {
-    if (jj_3R_84()) return true;
+  static private boolean jj_3R_82() {
+    if (jj_3R_87()) return true;
     Token xsp;
     while (true) {
       xsp = jj_scanpos;
-      if (jj_3R_85()) { jj_scanpos = xsp; break; }
+      if (jj_3R_88()) { jj_scanpos = xsp; break; }
     }
     return false;
   }
 
-  static private boolean jj_3R_118() {
+  static private boolean jj_3R_121() {
     if (jj_scan_token(A)) return true;
     if (jj_scan_token(LBRACKET)) return true;
-    if (jj_3R_34()) return true;
+    if (jj_3R_35()) return true;
     if (jj_scan_token(RBRACKET)) return true;
     return false;
   }
 
-  static private boolean jj_3R_86() {
+  static private boolean jj_3R_89() {
     if (jj_scan_token(PLUS)) return true;
     return false;
   }
 
-  static private boolean jj_3R_80() {
+  static private boolean jj_3R_83() {
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_86()) {
+    if (jj_3R_89()) {
     jj_scanpos = xsp;
-    if (jj_3R_87()) return true;
+    if (jj_3R_90()) return true;
     }
-    if (jj_3R_79()) return true;
+    if (jj_3R_82()) return true;
     return false;
   }
 
-  static private boolean jj_3R_76() {
-    if (jj_3R_79()) return true;
+  static private boolean jj_3_6() {
+    if (jj_scan_token(DQUOTE)) return true;
+    return false;
+  }
+
+  static private boolean jj_3R_79() {
+    if (jj_3R_82()) return true;
     Token xsp;
     while (true) {
       xsp = jj_scanpos;
-      if (jj_3R_80()) { jj_scanpos = xsp; break; }
+      if (jj_3R_83()) { jj_scanpos = xsp; break; }
     }
     return false;
   }
 
-  static private boolean jj_3R_143() {
-    if (jj_3R_158()) return true;
-    return false;
-  }
-
-  static private boolean jj_3R_66() {
-    if (jj_3R_34()) return true;
+  static private boolean jj_3R_146() {
+    if (jj_3R_161()) return true;
     return false;
   }
 
-  static private boolean jj_3R_117() {
+  static private boolean jj_3R_120() {
     if (jj_scan_token(E)) return true;
     if (jj_scan_token(LBRACKET)) return true;
-    if (jj_3R_34()) return true;
+    if (jj_3R_35()) return true;
     if (jj_scan_token(RBRACKET)) return true;
     return false;
   }
 
-  static private boolean jj_3R_62() {
-    if (jj_3R_34()) return true;
-    return false;
-  }
-
   static private boolean jj_3_14() {
     if (jj_scan_token(DQUOTE)) return true;
     return false;
   }
 
-  static private boolean jj_3R_167() {
+  static private boolean jj_3R_170() {
     if (jj_scan_token(S)) return true;
     return false;
   }
 
-  static private boolean jj_3R_77() {
-    if (jj_3R_81()) return true;
-    if (jj_3R_76()) return true;
+  static private boolean jj_3R_80() {
+    if (jj_3R_84()) return true;
+    if (jj_3R_79()) return true;
     return false;
   }
 
-  static private boolean jj_3R_166() {
+  static private boolean jj_3R_67() {
+    if (jj_3R_35()) return true;
+    return false;
+  }
+
+  static private boolean jj_3R_169() {
     if (jj_scan_token(F)) return true;
-    if (jj_3R_34()) return true;
+    if (jj_3R_35()) return true;
     return false;
   }
 
-  static private boolean jj_3R_165() {
+  static private boolean jj_3R_168() {
     if (jj_scan_token(I)) return true;
     if (jj_scan_token(EQ)) return true;
-    if (jj_3R_34()) return true;
+    if (jj_3R_35()) return true;
     return false;
   }
 
-  static private boolean jj_3R_164() {
+  static private boolean jj_3R_63() {
+    if (jj_3R_35()) return true;
+    return false;
+  }
+
+  static private boolean jj_3R_167() {
     if (jj_scan_token(C)) return true;
     if (jj_scan_token(LE)) return true;
-    if (jj_3R_34()) return true;
+    if (jj_3R_35()) return true;
     return false;
   }
 
-  static private boolean jj_3R_74() {
-    if (jj_3R_76()) return true;
+  static private boolean jj_3R_77() {
+    if (jj_3R_79()) return true;
     Token xsp;
     while (true) {
       xsp = jj_scanpos;
-      if (jj_3R_77()) { jj_scanpos = xsp; break; }
+      if (jj_3R_80()) { jj_scanpos = xsp; break; }
     }
     return false;
   }
 
-  static private boolean jj_3R_172() {
+  static private boolean jj_3R_175() {
     if (jj_scan_token(DQUOTE)) return true;
-    if (jj_3R_27()) return true;
+    if (jj_3R_28()) return true;
     if (jj_scan_token(DQUOTE)) return true;
     return false;
   }
 
-  static private boolean jj_3R_142() {
+  static private boolean jj_3R_145() {
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_164()) {
+    if (jj_3R_167()) {
     jj_scanpos = xsp;
-    if (jj_3R_165()) {
+    if (jj_3R_168()) {
     jj_scanpos = xsp;
-    if (jj_3R_166()) {
+    if (jj_3R_169()) {
     jj_scanpos = xsp;
-    if (jj_3R_167()) return true;
+    if (jj_3R_170()) return true;
     }
     }
     }
     return false;
   }
 
-  static private boolean jj_3R_32() {
-    if (jj_scan_token(AND)) return true;
-    if (jj_3R_31()) return true;
-    return false;
-  }
-
-  static private boolean jj_3R_64() {
-    if (jj_3R_34()) return true;
-    return false;
-  }
-
-  static private boolean jj_3R_75() {
-    if (jj_3R_78()) return true;
-    if (jj_3R_74()) return true;
-    return false;
-  }
-
-  static private boolean jj_3R_60() {
-    if (jj_3R_34()) return true;
+  static private boolean jj_3R_78() {
+    if (jj_3R_81()) return true;
+    if (jj_3R_77()) return true;
     return false;
   }
 
-  static private boolean jj_3R_73() {
-    if (jj_3R_74()) return true;
+  static private boolean jj_3R_76() {
+    if (jj_3R_77()) return true;
     Token xsp;
     while (true) {
       xsp = jj_scanpos;
-      if (jj_3R_75()) { jj_scanpos = xsp; break; }
+      if (jj_3R_78()) { jj_scanpos = xsp; break; }
     }
     return false;
   }
 
-  static private boolean jj_3R_169() {
+  static private boolean jj_3R_172() {
     if (jj_scan_token(LBRACE)) return true;
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_172()) {
+    if (jj_3R_175()) {
     jj_scanpos = xsp;
-    if (jj_3R_173()) return true;
+    if (jj_3R_176()) return true;
     }
     if (jj_scan_token(RBRACE)) return true;
     return false;
   }
 
-  static private boolean jj_3R_31() {
-    if (jj_scan_token(LPARENTH)) return true;
-    if (jj_3R_33()) return true;
-    if (jj_scan_token(EQ)) return true;
-    if (jj_3R_34()) return true;
-    if (jj_scan_token(RPARENTH)) return true;
+  static private boolean jj_3R_33() {
+    if (jj_scan_token(AND)) return true;
+    if (jj_3R_32()) return true;
     return false;
   }
 
-  static private boolean jj_3R_72() {
-    if (jj_3R_73()) return true;
+  static private boolean jj_3R_75() {
+    if (jj_3R_76()) return true;
     return false;
   }
 
-  static private boolean jj_3R_71() {
+  static private boolean jj_3R_74() {
     if (jj_scan_token(NOT)) return true;
-    if (jj_3R_69()) return true;
+    if (jj_3R_72()) return true;
     return false;
   }
 
-  static private boolean jj_3R_30() {
-    if (jj_3R_31()) return true;
-    Token xsp;
-    while (true) {
-      xsp = jj_scanpos;
-      if (jj_3R_32()) { jj_scanpos = xsp; break; }
-    }
+  static private boolean jj_3R_65() {
+    if (jj_3R_35()) return true;
     return false;
   }
 
-  static private boolean jj_3_5() {
-    if (jj_3R_28()) return true;
+  static private boolean jj_3R_61() {
+    if (jj_3R_35()) return true;
     return false;
   }
 
-  static private boolean jj_3R_69() {
+  static private boolean jj_3R_72() {
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_71()) {
+    if (jj_3R_74()) {
     jj_scanpos = xsp;
-    if (jj_3R_72()) return true;
+    if (jj_3R_75()) return true;
     }
     return false;
   }
 
-  static private boolean jj_3R_28() {
-    Token xsp;
-    xsp = jj_scanpos;
-    if (jj_3R_30()) {
-    jj_scanpos = xsp;
-    if (jj_scan_token(49)) return true;
-    }
+  static private boolean jj_3R_32() {
+    if (jj_scan_token(LPARENTH)) return true;
+    if (jj_3R_34()) return true;
+    if (jj_scan_token(EQ)) return true;
+    if (jj_3R_35()) return true;
+    if (jj_scan_token(RPARENTH)) return true;
     return false;
   }
 
-  static private boolean jj_3R_159() {
-    if (jj_3R_169()) return true;
+  static private boolean jj_3R_162() {
+    if (jj_3R_172()) return true;
     return false;
   }
 
-  static private boolean jj_3R_70() {
+  static private boolean jj_3R_73() {
     if (jj_scan_token(AND)) return true;
-    if (jj_3R_69()) return true;
+    if (jj_3R_72()) return true;
     return false;
   }
 
-  static private boolean jj_3R_138() {
-    if (jj_3R_158()) return true;
+  static private boolean jj_3R_31() {
+    if (jj_3R_32()) return true;
+    Token xsp;
+    while (true) {
+      xsp = jj_scanpos;
+      if (jj_3R_33()) { jj_scanpos = xsp; break; }
+    }
     return false;
   }
 
-  static private boolean jj_3R_163() {
+  static private boolean jj_3R_141() {
+    if (jj_3R_161()) return true;
+    return false;
+  }
+
+  static private boolean jj_3R_166() {
     if (jj_scan_token(MAX)) return true;
     if (jj_scan_token(EQ)) return true;
     if (jj_scan_token(QMARK)) return true;
     return false;
   }
 
-  static private boolean jj_3R_67() {
-    if (jj_3R_69()) return true;
+  static private boolean jj_3_5() {
+    if (jj_3R_29()) return true;
+    return false;
+  }
+
+  static private boolean jj_3R_70() {
+    if (jj_3R_72()) return true;
     Token xsp;
     while (true) {
       xsp = jj_scanpos;
-      if (jj_3R_70()) { jj_scanpos = xsp; break; }
+      if (jj_3R_73()) { jj_scanpos = xsp; break; }
     }
     return false;
   }
 
-  static private boolean jj_3R_141() {
+  static private boolean jj_3R_144() {
     if (jj_scan_token(RMAX)) return true;
     if (jj_scan_token(EQ)) return true;
     if (jj_scan_token(QMARK)) return true;
     return false;
   }
 
-  static private boolean jj_3R_162() {
+  static private boolean jj_3R_165() {
     if (jj_scan_token(MIN)) return true;
     if (jj_scan_token(EQ)) return true;
     if (jj_scan_token(QMARK)) return true;
     return false;
   }
 
-  static private boolean jj_3R_140() {
+  static private boolean jj_3R_143() {
     if (jj_scan_token(RMIN)) return true;
     if (jj_scan_token(EQ)) return true;
     if (jj_scan_token(QMARK)) return true;
     return false;
   }
 
-  static private boolean jj_3R_161() {
+  static private boolean jj_3R_164() {
     if (jj_scan_token(EQ)) return true;
     if (jj_scan_token(QMARK)) return true;
     return false;
   }
 
-  static private boolean jj_3R_160() {
-    if (jj_3R_81()) return true;
-    if (jj_3R_34()) return true;
+  static private boolean jj_3R_29() {
+    Token xsp;
+    xsp = jj_scanpos;
+    if (jj_3R_31()) {
+    jj_scanpos = xsp;
+    if (jj_scan_token(49)) return true;
+    }
     return false;
   }
 
-  static private boolean jj_3R_139() {
+  static private boolean jj_3R_163() {
+    if (jj_3R_84()) return true;
+    if (jj_3R_35()) return true;
+    return false;
+  }
+
+  static private boolean jj_3R_142() {
     if (jj_scan_token(R)) return true;
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_159()) jj_scanpos = xsp;
+    if (jj_3R_162()) jj_scanpos = xsp;
     xsp = jj_scanpos;
-    if (jj_3R_160()) {
+    if (jj_3R_163()) {
     jj_scanpos = xsp;
-    if (jj_3R_161()) {
+    if (jj_3R_164()) {
     jj_scanpos = xsp;
-    if (jj_3R_162()) {
+    if (jj_3R_165()) {
     jj_scanpos = xsp;
-    if (jj_3R_163()) return true;
+    if (jj_3R_166()) return true;
     }
     }
     }
     return false;
   }
 
-  static private boolean jj_3R_68() {
+  static private boolean jj_3R_71() {
     if (jj_scan_token(OR)) return true;
-    if (jj_3R_67()) return true;
+    if (jj_3R_70()) return true;
     return false;
   }
 
-  static private boolean jj_3R_116() {
+  static private boolean jj_3R_119() {
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_139()) {
+    if (jj_3R_142()) {
     jj_scanpos = xsp;
-    if (jj_3R_140()) {
+    if (jj_3R_143()) {
     jj_scanpos = xsp;
-    if (jj_3R_141()) return true;
+    if (jj_3R_144()) return true;
     }
     }
     if (jj_scan_token(LBRACKET)) return true;
-    if (jj_3R_142()) return true;
+    if (jj_3R_145()) return true;
     xsp = jj_scanpos;
-    if (jj_3R_143()) jj_scanpos = xsp;
+    if (jj_3R_146()) jj_scanpos = xsp;
     if (jj_scan_token(RBRACKET)) return true;
     return false;
   }
 
+  static private boolean jj_3R_68() {
+    if (jj_3R_70()) return true;
+    Token xsp;
+    while (true) {
+      xsp = jj_scanpos;
+      if (jj_3R_71()) { jj_scanpos = xsp; break; }
+    }
+    return false;
+  }
+
+  static private boolean jj_3R_69() {
+    if (jj_scan_token(IFF)) return true;
+    if (jj_3R_68()) return true;
+    return false;
+  }
+
   static private boolean jj_initialized_once = false;
   /** Generated Token Manager. */
   static public PrismParserTokenManager token_source;
@@ -4312,7 +4352,7 @@ public class PrismParser implements PrismParserConstants {
   static private Token jj_scanpos, jj_lastpos;
   static private int jj_la;
   static private int jj_gen;
-  static final private int[] jj_la1 = new int[87];
+  static final private int[] jj_la1 = new int[88];
   static private int[] jj_la1_0;
   static private int[] jj_la1_1;
   static private int[] jj_la1_2;
@@ -4322,13 +4362,13 @@ public class PrismParser implements PrismParserConstants {
       jj_la1_init_2();
    }
    private static void jj_la1_init_0() {
-      jj_la1_0 = new int[] {0x514404c0,0x504404c0,0x1000000,0xb01a0848,0x0,0xb01a0848,0xb01a0848,0x0,0xb01a0848,0x400,0x40000000,0x80,0x40000480,0x8000210,0x8000210,0x0,0x40,0x0,0x1000000,0x30,0x0,0x2000000,0x0,0x0,0x0,0xa0ba0808,0x0,0x0,0x0,0xa0ba0808,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0xa00000,0x0,0xa0ba0808,0xa0ba0808,0xa0ba0808,0xa0ba0808,0xa0ba0808,0x0,0x0,0x0,0x0,0x0,0xa01a0808,0x0,0x0,0x0,0x0,0x0,0x0,0xa01a0808,0xa01a0808,0x0,0xa0000000,0xa0000000,0x0,0x20000,0xa0000000,0x0,0x0,0x0,0xa0000000,0x0,0x0,0x0,0xa0000000,0x0,0x0,0xa0ba0808,0x4200100,0x1000000,0xa0000000,0x0,0xa0000000,0x0,0x0,0x0,};
+      jj_la1_0 = new int[] {0x514404c0,0x504404c0,0x1000000,0xb01a0848,0x0,0xb01a0848,0xb01a0848,0x0,0xb01a0848,0x400,0x40000000,0x80,0x40000480,0x8000210,0x8000210,0x0,0x40,0x0,0x1000000,0x30,0x0,0x2000000,0x0,0x0,0x0,0xa0ba0808,0x0,0x0,0x0,0xa0ba0808,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0xa00000,0x0,0xa0ba0808,0xa0ba0808,0xa0ba0808,0xa0ba0808,0xa0ba0808,0x0,0x0,0x0,0x0,0x0,0x0,0xa01a0808,0x0,0x0,0x0,0x0,0x0,0x0,0xa01a0808,0xa01a0808,0x0,0xa0000000,0xa0000000,0x0,0x20000,0xa0000000,0x0,0x0,0x0,0xa0000000,0x0,0x0,0x0,0xa0000000,0x0,0x0,0xa0ba0808,0x4200100,0x1000000,0xa0000000,0x0,0xa0000000,0x0,0x0,0x0,};
    }
    private static void jj_la1_init_1() {
-      jj_la1_1 = new int[] {0x187c5,0x83c4,0x10401,0x20127ab8,0x4000000,0x20127ab8,0x20127ab8,0x4000000,0x20127ab8,0x40,0x4,0x8000,0x8144,0x0,0x0,0x280,0x280,0x0,0x0,0x80000000,0x0,0x0,0x80000000,0x0,0x0,0x2012783a,0x200000,0x20020000,0x8000000,0xa012783a,0x0,0x80000000,0x8000000,0x0,0x8000000,0x8000000,0x0,0x20000000,0xc2000,0x80000000,0xc2000,0x2,0x80000000,0x2012783a,0x2012783a,0x2012783a,0x2012783a,0x2012783a,0x80000000,0x0,0x800000,0x400000,0x200000,0x20127838,0x0,0x0,0x0,0x0,0x0,0x0,0x20027838,0x20027838,0x20000000,0x0,0x0,0x8000000,0x20000,0x0,0x38,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x3800,0x0,0x2012783a,0x4000,0x0,0x600000,0x8000000,0x0,0x0,0x0,0x2000000,};
+      jj_la1_1 = new int[] {0x187c5,0x83c4,0x10401,0x40127ab8,0x8000000,0x40127ab8,0x40127ab8,0x8000000,0x40127ab8,0x40,0x4,0x8000,0x8144,0x0,0x0,0x280,0x280,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x4012783a,0x200000,0x40020000,0x10000000,0x4012783a,0x0,0x0,0x10000000,0x0,0x10000000,0x10000000,0x0,0x40000000,0xc2000,0x0,0xc2000,0x2,0x0,0x4012783a,0x4012783a,0x4012783a,0x4012783a,0x4012783a,0x0,0x0,0x800000,0x1000000,0x400000,0x200000,0x40127838,0x0,0x0,0x0,0x0,0x0,0x0,0x40027838,0x40027838,0x40000000,0x0,0x0,0x10000000,0x20000,0x0,0x38,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x3800,0x0,0x4012783a,0x4000,0x0,0x600000,0x10000000,0x0,0x0,0x0,0x4000000,};
    }
    private static void jj_la1_init_2() {
-      jj_la1_2 = new int[] {0x0,0x0,0x0,0x170400,0x0,0x170400,0x170400,0x0,0x170400,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x8,0x0,0x0,0x100000,0x0,0x0,0x100000,0x200,0x170400,0x0,0x0,0x0,0x170400,0x100000,0x0,0x0,0x1002,0x0,0x0,0x1002,0x100000,0x0,0x1e0,0x0,0x0,0x1e0,0x170400,0x170400,0x170400,0x170400,0x170400,0x1e0,0x8000,0x0,0x0,0x0,0x170400,0x18,0x1e0,0x600,0x600,0x1800,0x1800,0x170400,0x170000,0x0,0x0,0x100000,0x0,0x60000,0x1e8,0x0,0x2,0x2,0x0,0x1e8,0x2,0x2,0x1e8,0x0,0x2,0x170400,0x0,0x100000,0x100200,0x0,0x100000,0x18,0x1e0,0x0,};
+      jj_la1_2 = new int[] {0x0,0x0,0x0,0x2e0800,0x0,0x2e0800,0x2e0800,0x0,0x2e0800,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x10,0x0,0x1,0x200000,0x0,0x1,0x200000,0x400,0x2e0800,0x0,0x0,0x0,0x2e0801,0x200000,0x1,0x0,0x2004,0x0,0x0,0x2004,0x200000,0x0,0x3c1,0x0,0x0,0x3c1,0x2e0800,0x2e0800,0x2e0800,0x2e0800,0x2e0800,0x3c1,0x10000,0x0,0x0,0x0,0x0,0x2e0800,0x30,0x3c0,0xc00,0xc00,0x3000,0x3000,0x2e0800,0x2e0000,0x0,0x0,0x200000,0x0,0xc0000,0x3d0,0x0,0x4,0x4,0x0,0x3d0,0x4,0x4,0x3d0,0x0,0x4,0x2e0800,0x0,0x200000,0x200400,0x0,0x200000,0x30,0x3c0,0x0,};
    }
   static final private JJCalls[] jj_2_rtns = new JJCalls[14];
   static private boolean jj_rescan = false;
@@ -4352,7 +4392,7 @@ public class PrismParser implements PrismParserConstants {
     token = new Token();
     jj_ntk = -1;
     jj_gen = 0;
-    for (int i = 0; i < 87; i++) jj_la1[i] = -1;
+    for (int i = 0; i < 88; i++) jj_la1[i] = -1;
     for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
   }
 
@@ -4367,7 +4407,7 @@ public class PrismParser implements PrismParserConstants {
     token = new Token();
     jj_ntk = -1;
     jj_gen = 0;
-    for (int i = 0; i < 87; i++) jj_la1[i] = -1;
+    for (int i = 0; i < 88; i++) jj_la1[i] = -1;
     for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
   }
 
@@ -4385,7 +4425,7 @@ public class PrismParser implements PrismParserConstants {
     token = new Token();
     jj_ntk = -1;
     jj_gen = 0;
-    for (int i = 0; i < 87; i++) jj_la1[i] = -1;
+    for (int i = 0; i < 88; i++) jj_la1[i] = -1;
     for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
   }
 
@@ -4396,7 +4436,7 @@ public class PrismParser implements PrismParserConstants {
     token = new Token();
     jj_ntk = -1;
     jj_gen = 0;
-    for (int i = 0; i < 87; i++) jj_la1[i] = -1;
+    for (int i = 0; i < 88; i++) jj_la1[i] = -1;
     for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
   }
 
@@ -4413,7 +4453,7 @@ public class PrismParser implements PrismParserConstants {
     token = new Token();
     jj_ntk = -1;
     jj_gen = 0;
-    for (int i = 0; i < 87; i++) jj_la1[i] = -1;
+    for (int i = 0; i < 88; i++) jj_la1[i] = -1;
     for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
   }
 
@@ -4423,7 +4463,7 @@ public class PrismParser implements PrismParserConstants {
     token = new Token();
     jj_ntk = -1;
     jj_gen = 0;
-    for (int i = 0; i < 87; i++) jj_la1[i] = -1;
+    for (int i = 0; i < 88; i++) jj_la1[i] = -1;
     for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
   }
 
@@ -4535,12 +4575,12 @@ public class PrismParser implements PrismParserConstants {
   /** Generate ParseException. */
   static public ParseException generateParseException() {
     jj_expentries.clear();
-    boolean[] la1tokens = new boolean[87];
+    boolean[] la1tokens = new boolean[88];
     if (jj_kind >= 0) {
       la1tokens[jj_kind] = true;
       jj_kind = -1;
     }
-    for (int i = 0; i < 87; i++) {
+    for (int i = 0; i < 88; i++) {
       if (jj_la1[i] == jj_gen) {
         for (int j = 0; j < 32; j++) {
           if ((jj_la1_0[i] & (1<<j)) != 0) {
@@ -4555,7 +4595,7 @@ public class PrismParser implements PrismParserConstants {
         }
       }
     }
-    for (int i = 0; i < 87; i++) {
+    for (int i = 0; i < 88; i++) {
       if (la1tokens[i]) {
         jj_expentry = new int[1];
         jj_expentry[0] = i;
diff --git a/prism/src/parser/PrismParser.jj b/prism/src/parser/PrismParser.jj
index cbe54082..6ce95039 100644
--- a/prism/src/parser/PrismParser.jj
+++ b/prism/src/parser/PrismParser.jj
@@ -411,6 +411,7 @@ TOKEN :
 |	< AND:			"&" >
 |	< OR:			"|" >
 |	< IMPLIES:		"=>" >
+|	< IFF:			"<=>" >
 |	< RARROW:		"->" >
 |	< COLON:		":" >
 |	< SEMICOLON:	";" >
@@ -1120,9 +1121,22 @@ Expression ExpressionImplies(boolean prop, boolean pathprop) :
 	Expression ret, expr;
 	Token begin = null;
 }
+{
+	{ begin = getToken(1); } ret = ExpressionIff(prop, pathprop)
+	( <IMPLIES> expr = ExpressionIff(prop, pathprop) { ret = new ExpressionBinaryOp(ExpressionBinaryOp.IMPLIES, ret, expr); ret.setPosition(begin, getToken(0)); } )*
+	{ return ret; }
+}
+
+// Expression: if-and-only-iff
+
+Expression ExpressionIff(boolean prop, boolean pathprop) :
+{
+	Expression ret, expr;
+	Token begin = null;
+}
 {
 	{ begin = getToken(1); } ret = ExpressionOr(prop, pathprop)
-	( <IMPLIES> expr = ExpressionOr(prop, pathprop) { ret = new ExpressionBinaryOp(ExpressionBinaryOp.IMPLIES, ret, expr); ret.setPosition(begin, getToken(0)); } )*
+	( <IFF> expr = ExpressionOr(prop, pathprop) { ret = new ExpressionBinaryOp(ExpressionBinaryOp.IFF, ret, expr); ret.setPosition(begin, getToken(0)); } )*
 	{ return ret; }
 }
 
diff --git a/prism/src/parser/PrismParserConstants.java b/prism/src/parser/PrismParserConstants.java
index 3b0a4f7d..3c92faa4 100644
--- a/prism/src/parser/PrismParserConstants.java
+++ b/prism/src/parser/PrismParserConstants.java
@@ -121,67 +121,69 @@ public interface PrismParserConstants {
   /** RegularExpression Id. */
   int IMPLIES = 55;
   /** RegularExpression Id. */
-  int RARROW = 56;
+  int IFF = 56;
   /** RegularExpression Id. */
-  int COLON = 57;
+  int RARROW = 57;
   /** RegularExpression Id. */
-  int SEMICOLON = 58;
+  int COLON = 58;
   /** RegularExpression Id. */
-  int COMMA = 59;
+  int SEMICOLON = 59;
   /** RegularExpression Id. */
-  int DOTS = 60;
+  int COMMA = 60;
   /** RegularExpression Id. */
-  int LPARENTH = 61;
+  int DOTS = 61;
   /** RegularExpression Id. */
-  int RPARENTH = 62;
+  int LPARENTH = 62;
   /** RegularExpression Id. */
-  int LBRACKET = 63;
+  int RPARENTH = 63;
   /** RegularExpression Id. */
-  int RBRACKET = 64;
+  int LBRACKET = 64;
   /** RegularExpression Id. */
-  int LBRACE = 65;
+  int RBRACKET = 65;
   /** RegularExpression Id. */
-  int RBRACE = 66;
+  int LBRACE = 66;
   /** RegularExpression Id. */
-  int EQ = 67;
+  int RBRACE = 67;
   /** RegularExpression Id. */
-  int NE = 68;
+  int EQ = 68;
   /** RegularExpression Id. */
-  int LT = 69;
+  int NE = 69;
   /** RegularExpression Id. */
-  int GT = 70;
+  int LT = 70;
   /** RegularExpression Id. */
-  int LE = 71;
+  int GT = 71;
   /** RegularExpression Id. */
-  int GE = 72;
+  int LE = 72;
   /** RegularExpression Id. */
-  int PLUS = 73;
+  int GE = 73;
   /** RegularExpression Id. */
-  int MINUS = 74;
+  int PLUS = 74;
   /** RegularExpression Id. */
-  int TIMES = 75;
+  int MINUS = 75;
   /** RegularExpression Id. */
-  int DIVIDE = 76;
+  int TIMES = 76;
   /** RegularExpression Id. */
-  int PRIME = 77;
+  int DIVIDE = 77;
   /** RegularExpression Id. */
-  int RENAME = 78;
+  int PRIME = 78;
   /** RegularExpression Id. */
-  int QMARK = 79;
+  int RENAME = 79;
   /** RegularExpression Id. */
-  int DQUOTE = 80;
+  int QMARK = 80;
   /** RegularExpression Id. */
-  int REG_INT = 81;
+  int DQUOTE = 81;
   /** RegularExpression Id. */
-  int REG_DOUBLE = 82;
+  int REG_INT = 82;
   /** RegularExpression Id. */
-  int REG_IDENTPRIME = 83;
+  int REG_DOUBLE = 83;
   /** RegularExpression Id. */
-  int REG_IDENT = 84;
+  int REG_IDENTPRIME = 84;
   /** RegularExpression Id. */
-  int PREPROC = 85;
+  int REG_IDENT = 85;
   /** RegularExpression Id. */
-  int LEXICAL_ERROR = 86;
+  int PREPROC = 86;
+  /** RegularExpression Id. */
+  int LEXICAL_ERROR = 87;
 
   /** Lexical state. */
   int DEFAULT = 0;
@@ -244,6 +246,7 @@ public interface PrismParserConstants {
     "\"&\"",
     "\"|\"",
     "\"=>\"",
+    "\"<=>\"",
     "\"->\"",
     "\":\"",
     "\";\"",
diff --git a/prism/src/parser/PrismParserTokenManager.java b/prism/src/parser/PrismParserTokenManager.java
index de290989..17dac422 100644
--- a/prism/src/parser/PrismParserTokenManager.java
+++ b/prism/src/parser/PrismParserTokenManager.java
@@ -23,33 +23,36 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac
       case 0:
          if ((active0 & 0xc783a04a00908L) != 0L)
             return 23;
-         if ((active1 & 0x1000L) != 0L)
+         if ((active1 & 0x2000L) != 0L)
             return 1;
-         if ((active0 & 0x1000000000000000L) != 0L)
+         if ((active0 & 0x2000000000000000L) != 0L)
             return 11;
          if ((active0 & 0x387c5fb5ff6f0L) != 0L)
          {
-            jjmatchedKind = 84;
+            jjmatchedKind = 85;
             return 23;
          }
          return -1;
       case 1:
          if ((active0 & 0x39fddfb5ff6f0L) != 0L)
          {
-            jjmatchedKind = 84;
-            jjmatchedPos = 1;
+            if (jjmatchedPos != 1)
+            {
+               jjmatchedKind = 85;
+               jjmatchedPos = 1;
+            }
             return 23;
          }
          return -1;
       case 2:
-         if ((active0 & 0x100e8000000L) != 0L)
-            return 23;
          if ((active0 & 0x39edd135ff6f0L) != 0L)
          {
-            jjmatchedKind = 84;
+            jjmatchedKind = 85;
             jjmatchedPos = 2;
             return 23;
          }
+         if ((active0 & 0x100e8000000L) != 0L)
+            return 23;
          return -1;
       case 3:
          if ((active0 & 0x21ad801100490L) != 0L)
@@ -58,66 +61,66 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac
          {
             if (jjmatchedPos != 3)
             {
-               jjmatchedKind = 84;
+               jjmatchedKind = 85;
                jjmatchedPos = 3;
             }
             return 23;
          }
          return -1;
       case 4:
-         if ((active0 & 0x10020060L) != 0L)
-            return 23;
          if ((active0 & 0x18445024df200L) != 0L)
          {
-            jjmatchedKind = 84;
+            jjmatchedKind = 85;
             jjmatchedPos = 4;
             return 23;
          }
+         if ((active0 & 0x10020060L) != 0L)
+            return 23;
          return -1;
       case 5:
          if ((active0 & 0x1000100480200L) != 0L)
             return 23;
          if ((active0 & 0x84440205f000L) != 0L)
          {
-            jjmatchedKind = 84;
+            jjmatchedKind = 85;
             jjmatchedPos = 5;
             return 23;
          }
          return -1;
       case 6:
-         if ((active0 & 0x40000041000L) != 0L)
-            return 23;
          if ((active0 & 0x80440201e000L) != 0L)
          {
-            jjmatchedKind = 84;
+            jjmatchedKind = 85;
             jjmatchedPos = 6;
             return 23;
          }
+         if ((active0 & 0x40000041000L) != 0L)
+            return 23;
          return -1;
       case 7:
          if ((active0 & 0x80440201e000L) != 0L)
          {
-            jjmatchedKind = 84;
+            jjmatchedKind = 85;
             jjmatchedPos = 7;
             return 23;
          }
          return -1;
       case 8:
-         if ((active0 & 0x2014000L) != 0L)
-            return 23;
          if ((active0 & 0x80440000a000L) != 0L)
          {
-            jjmatchedKind = 84;
+            jjmatchedKind = 85;
             jjmatchedPos = 8;
             return 23;
          }
+         if ((active0 & 0x2014000L) != 0L)
+            return 23;
          return -1;
       case 9:
          if ((active0 & 0x800000008000L) != 0L)
             return 23;
          if ((active0 & 0x4400002000L) != 0L)
          {
-            jjmatchedKind = 84;
+            jjmatchedKind = 85;
             jjmatchedPos = 9;
             return 23;
          }
@@ -125,7 +128,7 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac
       case 10:
          if ((active0 & 0x4400002000L) != 0L)
          {
-            jjmatchedKind = 84;
+            jjmatchedKind = 85;
             jjmatchedPos = 10;
             return 23;
          }
@@ -135,7 +138,7 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac
             return 23;
          if ((active0 & 0x4400000000L) != 0L)
          {
-            jjmatchedKind = 84;
+            jjmatchedKind = 85;
             jjmatchedPos = 11;
             return 23;
          }
@@ -145,7 +148,7 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac
             return 23;
          if ((active0 & 0x400000000L) != 0L)
          {
-            jjmatchedKind = 84;
+            jjmatchedKind = 85;
             jjmatchedPos = 12;
             return 23;
          }
@@ -153,7 +156,7 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac
       case 13:
          if ((active0 & 0x400000000L) != 0L)
          {
-            jjmatchedKind = 84;
+            jjmatchedKind = 85;
             jjmatchedPos = 13;
             return 23;
          }
@@ -161,7 +164,7 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac
       case 14:
          if ((active0 & 0x400000000L) != 0L)
          {
-            jjmatchedKind = 84;
+            jjmatchedKind = 85;
             jjmatchedPos = 14;
             return 23;
          }
@@ -186,45 +189,45 @@ static private int jjMoveStringLiteralDfa0_0()
    {
       case 33:
          jjmatchedKind = 52;
-         return jjMoveStringLiteralDfa1_0(0x0L, 0x10L);
+         return jjMoveStringLiteralDfa1_0(0x0L, 0x20L);
       case 34:
-         return jjStopAtPos(0, 80);
+         return jjStopAtPos(0, 81);
       case 38:
          return jjStopAtPos(0, 53);
       case 39:
-         return jjStopAtPos(0, 77);
+         return jjStopAtPos(0, 78);
       case 40:
-         return jjStopAtPos(0, 61);
-      case 41:
          return jjStopAtPos(0, 62);
+      case 41:
+         return jjStopAtPos(0, 63);
       case 42:
-         return jjStopAtPos(0, 75);
+         return jjStopAtPos(0, 76);
       case 43:
-         return jjStopAtPos(0, 73);
+         return jjStopAtPos(0, 74);
       case 44:
-         return jjStopAtPos(0, 59);
+         return jjStopAtPos(0, 60);
       case 45:
-         jjmatchedKind = 74;
-         return jjMoveStringLiteralDfa1_0(0x100000000000000L, 0x0L);
+         jjmatchedKind = 75;
+         return jjMoveStringLiteralDfa1_0(0x200000000000000L, 0x0L);
       case 46:
-         return jjMoveStringLiteralDfa1_0(0x1000000000000000L, 0x0L);
+         return jjMoveStringLiteralDfa1_0(0x2000000000000000L, 0x0L);
       case 47:
-         return jjStartNfaWithStates_0(0, 76, 1);
+         return jjStartNfaWithStates_0(0, 77, 1);
       case 58:
-         return jjStopAtPos(0, 57);
-      case 59:
          return jjStopAtPos(0, 58);
+      case 59:
+         return jjStopAtPos(0, 59);
       case 60:
-         jjmatchedKind = 69;
-         return jjMoveStringLiteralDfa1_0(0x0L, 0x4080L);
+         jjmatchedKind = 70;
+         return jjMoveStringLiteralDfa1_0(0x100000000000000L, 0x8100L);
       case 61:
-         jjmatchedKind = 67;
+         jjmatchedKind = 68;
          return jjMoveStringLiteralDfa1_0(0x80000000000000L, 0x0L);
       case 62:
-         jjmatchedKind = 70;
-         return jjMoveStringLiteralDfa1_0(0x0L, 0x100L);
+         jjmatchedKind = 71;
+         return jjMoveStringLiteralDfa1_0(0x0L, 0x200L);
       case 63:
-         return jjStopAtPos(0, 79);
+         return jjStopAtPos(0, 80);
       case 65:
          return jjStartNfaWithStates_0(0, 3, 23);
       case 67:
@@ -252,9 +255,9 @@ static private int jjMoveStringLiteralDfa0_0()
       case 88:
          return jjStartNfaWithStates_0(0, 33, 23);
       case 91:
-         return jjStopAtPos(0, 63);
-      case 93:
          return jjStopAtPos(0, 64);
+      case 93:
+         return jjStopAtPos(0, 65);
       case 98:
          return jjMoveStringLiteralDfa1_0(0x10L, 0x0L);
       case 99:
@@ -284,11 +287,11 @@ static private int jjMoveStringLiteralDfa0_0()
       case 116:
          return jjMoveStringLiteralDfa1_0(0x2000000000000L, 0x0L);
       case 123:
-         return jjStopAtPos(0, 65);
+         return jjStopAtPos(0, 66);
       case 124:
          return jjStopAtPos(0, 54);
       case 125:
-         return jjStopAtPos(0, 66);
+         return jjStopAtPos(0, 67);
       default :
          return jjMoveNfa_0(0, 0);
    }
@@ -303,26 +306,29 @@ static private int jjMoveStringLiteralDfa1_0(long active0, long active1)
    switch(curChar)
    {
       case 45:
-         if ((active1 & 0x4000L) != 0L)
-            return jjStopAtPos(1, 78);
+         if ((active1 & 0x8000L) != 0L)
+            return jjStopAtPos(1, 79);
          break;
       case 46:
-         if ((active0 & 0x1000000000000000L) != 0L)
-            return jjStopAtPos(1, 60);
+         if ((active0 & 0x2000000000000000L) != 0L)
+            return jjStopAtPos(1, 61);
          break;
       case 61:
-         if ((active1 & 0x10L) != 0L)
-            return jjStopAtPos(1, 68);
-         else if ((active1 & 0x80L) != 0L)
-            return jjStopAtPos(1, 71);
+         if ((active1 & 0x20L) != 0L)
+            return jjStopAtPos(1, 69);
          else if ((active1 & 0x100L) != 0L)
-            return jjStopAtPos(1, 72);
-         break;
+         {
+            jjmatchedKind = 72;
+            jjmatchedPos = 1;
+         }
+         else if ((active1 & 0x200L) != 0L)
+            return jjStopAtPos(1, 73);
+         return jjMoveStringLiteralDfa2_0(active0, 0x100000000000000L, active1, 0L);
       case 62:
          if ((active0 & 0x80000000000000L) != 0L)
             return jjStopAtPos(1, 55);
-         else if ((active0 & 0x100000000000000L) != 0L)
-            return jjStopAtPos(1, 56);
+         else if ((active0 & 0x200000000000000L) != 0L)
+            return jjStopAtPos(1, 57);
          break;
       case 97:
          return jjMoveStringLiteralDfa2_0(active0, 0x20030020000L, active1, 0L);
@@ -364,6 +370,10 @@ static private int jjMoveStringLiteralDfa2_0(long old0, long active0, long old1,
    }
    switch(curChar)
    {
+      case 62:
+         if ((active0 & 0x100000000000000L) != 0L)
+            return jjStopAtPos(2, 56);
+         break;
       case 97:
          if ((active0 & 0x10000000000L) != 0L)
             return jjStartNfaWithStates_0(2, 40, 23);
@@ -853,14 +863,14 @@ static private int jjMoveNfa_0(int startState, int curPos)
                case 23:
                   if ((0x3ff000000000000L & l) != 0L)
                   {
-                     if (kind > 84)
-                        kind = 84;
+                     if (kind > 85)
+                        kind = 85;
                      jjCheckNAdd(22);
                   }
                   else if (curChar == 39)
                   {
-                     if (kind > 83)
-                        kind = 83;
+                     if (kind > 84)
+                        kind = 84;
                   }
                   if ((0x3ff000000000000L & l) != 0L)
                      jjCheckNAddTwoStates(20, 21);
@@ -868,8 +878,8 @@ static private int jjMoveNfa_0(int startState, int curPos)
                case 0:
                   if ((0x3ff000000000000L & l) != 0L)
                   {
-                     if (kind > 82)
-                        kind = 82;
+                     if (kind > 83)
+                        kind = 83;
                      jjCheckNAddStates(0, 3);
                   }
                   else if ((0x100002600L & l) != 0L)
@@ -885,14 +895,14 @@ static private int jjMoveNfa_0(int startState, int curPos)
                      jjstateSet[jjnewStateCnt++] = 1;
                   if ((0x3fe000000000000L & l) != 0L)
                   {
-                     if (kind > 81)
-                        kind = 81;
+                     if (kind > 82)
+                        kind = 82;
                      jjCheckNAdd(8);
                   }
                   else if (curChar == 48)
                   {
-                     if (kind > 81)
-                        kind = 81;
+                     if (kind > 82)
+                        kind = 82;
                   }
                   break;
                case 1:
@@ -922,20 +932,20 @@ static private int jjMoveNfa_0(int startState, int curPos)
                case 7:
                   if ((0x3fe000000000000L & l) == 0L)
                      break;
-                  if (kind > 81)
-                     kind = 81;
+                  if (kind > 82)
+                     kind = 82;
                   jjCheckNAdd(8);
                   break;
                case 8:
                   if ((0x3ff000000000000L & l) == 0L)
                      break;
-                  if (kind > 81)
-                     kind = 81;
+                  if (kind > 82)
+                     kind = 82;
                   jjCheckNAdd(8);
                   break;
                case 9:
-                  if (curChar == 48 && kind > 81)
-                     kind = 81;
+                  if (curChar == 48 && kind > 82)
+                     kind = 82;
                   break;
                case 10:
                   if (curChar == 46)
@@ -944,8 +954,8 @@ static private int jjMoveNfa_0(int startState, int curPos)
                case 11:
                   if ((0x3ff000000000000L & l) == 0L)
                      break;
-                  if (kind > 82)
-                     kind = 82;
+                  if (kind > 83)
+                     kind = 83;
                   jjCheckNAddTwoStates(11, 12);
                   break;
                case 13:
@@ -955,8 +965,8 @@ static private int jjMoveNfa_0(int startState, int curPos)
                case 14:
                   if ((0x3ff000000000000L & l) == 0L)
                      break;
-                  if (kind > 82)
-                     kind = 82;
+                  if (kind > 83)
+                     kind = 83;
                   jjCheckNAdd(14);
                   break;
                case 15:
@@ -968,14 +978,14 @@ static private int jjMoveNfa_0(int startState, int curPos)
                      jjCheckNAddTwoStates(16, 17);
                   break;
                case 17:
-                  if (curChar == 35 && kind > 85)
-                     kind = 85;
+                  if (curChar == 35 && kind > 86)
+                     kind = 86;
                   break;
                case 18:
                   if ((0x3ff000000000000L & l) == 0L)
                      break;
-                  if (kind > 82)
-                     kind = 82;
+                  if (kind > 83)
+                     kind = 83;
                   jjCheckNAddStates(0, 3);
                   break;
                case 20:
@@ -983,14 +993,14 @@ static private int jjMoveNfa_0(int startState, int curPos)
                      jjCheckNAddTwoStates(20, 21);
                   break;
                case 21:
-                  if (curChar == 39 && kind > 83)
-                     kind = 83;
+                  if (curChar == 39 && kind > 84)
+                     kind = 84;
                   break;
                case 22:
                   if ((0x3ff000000000000L & l) == 0L)
                      break;
-                  if (kind > 84)
-                     kind = 84;
+                  if (kind > 85)
+                     kind = 85;
                   jjCheckNAdd(22);
                   break;
                default : break;
@@ -1007,8 +1017,8 @@ static private int jjMoveNfa_0(int startState, int curPos)
                case 23:
                   if ((0x7fffffe87fffffeL & l) != 0L)
                   {
-                     if (kind > 84)
-                        kind = 84;
+                     if (kind > 85)
+                        kind = 85;
                      jjCheckNAdd(22);
                   }
                   if ((0x7fffffe87fffffeL & l) != 0L)
@@ -1017,8 +1027,8 @@ static private int jjMoveNfa_0(int startState, int curPos)
                case 0:
                   if ((0x7fffffe87fffffeL & l) == 0L)
                      break;
-                  if (kind > 84)
-                     kind = 84;
+                  if (kind > 85)
+                     kind = 85;
                   jjCheckNAddStates(7, 9);
                   break;
                case 2:
@@ -1038,8 +1048,8 @@ static private int jjMoveNfa_0(int startState, int curPos)
                case 22:
                   if ((0x7fffffe87fffffeL & l) == 0L)
                      break;
-                  if (kind > 84)
-                     kind = 84;
+                  if (kind > 85)
+                     kind = 85;
                   jjCheckNAdd(22);
                   break;
                default : break;
@@ -1113,17 +1123,17 @@ public static final String[] jjstrLiteralImages = {
 "\160\162\157\142\141\142\151\154\151\163\164\151\143", "\160\162\157\142", "\160\164\141", "\162\141\164\145", 
 "\162\145\167\141\162\144\163", "\122\155\141\170", "\122\155\151\156", "\122", "\123", 
 "\163\164\157\143\150\141\163\164\151\143", "\163\171\163\164\145\155", "\164\162\165\145", "\125", "\127", "\41", "\46", 
-"\174", "\75\76", "\55\76", "\72", "\73", "\54", "\56\56", "\50", "\51", "\133", 
-"\135", "\173", "\175", "\75", "\41\75", "\74", "\76", "\74\75", "\76\75", "\53", 
-"\55", "\52", "\57", "\47", "\74\55", "\77", "\42", null, null, null, null, null, 
-null, };
+"\174", "\75\76", "\74\75\76", "\55\76", "\72", "\73", "\54", "\56\56", "\50", "\51", 
+"\133", "\135", "\173", "\175", "\75", "\41\75", "\74", "\76", "\74\75", "\76\75", 
+"\53", "\55", "\52", "\57", "\47", "\74\55", "\77", "\42", null, null, null, null, 
+null, null, };
 
 /** Lexer state names. */
 public static final String[] lexStateNames = {
    "DEFAULT",
 };
 static final long[] jjtoToken = {
-   0xfffffffffffffff9L, 0x7fffffL, 
+   0xfffffffffffffff9L, 0xffffffL, 
 };
 static final long[] jjtoSkip = {
    0x6L, 0x0L, 
@@ -1236,9 +1246,9 @@ public static Token getNextToken()
    jjmatchedKind = 0x7fffffff;
    jjmatchedPos = 0;
    curPos = jjMoveStringLiteralDfa0_0();
-   if (jjmatchedPos == 0 && jjmatchedKind > 86)
+   if (jjmatchedPos == 0 && jjmatchedKind > 87)
    {
-      jjmatchedKind = 86;
+      jjmatchedKind = 87;
    }
    if (jjmatchedKind != 0x7fffffff)
    {
diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java
index f188809e..0f489e06 100644
--- a/prism/src/parser/ast/Expression.java
+++ b/prism/src/parser/ast/Expression.java
@@ -369,6 +369,11 @@ public abstract class Expression extends ASTElement
 		return new ExpressionBinaryOp(ExpressionBinaryOp.OR, expr1, expr2);
 	}
 
+	public static Expression Iff(Expression expr1, Expression expr2)
+	{
+		return new ExpressionBinaryOp(ExpressionBinaryOp.IFF, expr1, expr2);
+	}
+
 	public static Expression Implies(Expression expr1, Expression expr2)
 	{
 		return new ExpressionBinaryOp(ExpressionBinaryOp.IMPLIES, expr1, expr2);
@@ -437,6 +442,12 @@ public abstract class Expression extends ASTElement
 		return expr instanceof ExpressionBinaryOp && ((ExpressionBinaryOp) expr).getOperator() == ExpressionBinaryOp.OR;
 	}
 
+	public static boolean isIff(Expression expr)
+	{
+		return expr instanceof ExpressionBinaryOp
+				&& ((ExpressionBinaryOp) expr).getOperator() == ExpressionBinaryOp.IFF;
+	}
+
 	public static boolean isImplies(Expression expr)
 	{
 		return expr instanceof ExpressionBinaryOp
diff --git a/prism/src/parser/ast/ExpressionBinaryOp.java b/prism/src/parser/ast/ExpressionBinaryOp.java
index 29091d6f..cb3b343c 100644
--- a/prism/src/parser/ast/ExpressionBinaryOp.java
+++ b/prism/src/parser/ast/ExpressionBinaryOp.java
@@ -35,22 +35,23 @@ public class ExpressionBinaryOp extends Expression
 {
 	// Operator constants
 	public static final int IMPLIES = 1;
-	public static final int OR = 2;
-	public static final int AND = 3;
-	public static final int EQ = 4;
-	public static final int NE = 5;
-	public static final int GT = 6;
-	public static final int GE = 7;
-	public static final int LT = 8;
-	public static final int LE = 9;
-	public static final int PLUS = 10;
-	public static final int MINUS = 11;
-	public static final int TIMES = 12;
-	public static final int DIVIDE = 13;
+	public static final int IFF = 2;
+	public static final int OR = 3;
+	public static final int AND = 4;
+	public static final int EQ = 5;
+	public static final int NE = 6;
+	public static final int GT = 7;
+	public static final int GE = 8;
+	public static final int LT = 9;
+	public static final int LE = 10;
+	public static final int PLUS = 11;
+	public static final int MINUS = 12;
+	public static final int TIMES = 13;
+	public static final int DIVIDE = 14;
 	// Operator symbols
-	public static final String opSymbols[] = { "", "=>", "|", "&", "=", "!=", ">", ">=", "<", "<=", "+", "-", "*", "/" };
+	public static final String opSymbols[] = { "", "=>", "<=>", "|", "&", "=", "!=", ">", ">=", "<", "<=", "+", "-", "*", "/" };
 	// Operator type testers
-	public static boolean isLogical(int op) { return op==IMPLIES || op==OR || op==AND; }
+	public static boolean isLogical(int op) { return op==IMPLIES || op==IFF || op==OR || op==AND; }
 	public static boolean isRelOp(int op) { return op==EQ || op==NE || op==GT ||  op==GE || op==LT || op==LE; }
 	public static boolean isArithmetic(int op) { return op==PLUS || op==MINUS || op==TIMES ||  op==DIVIDE; }
 	
@@ -131,6 +132,8 @@ public class ExpressionBinaryOp extends Expression
 		switch (op) {
 		case IMPLIES:
 			return new Boolean(!operand1.evaluateBoolean(ec) || operand2.evaluateBoolean(ec));
+		case IFF:
+			return new Boolean(operand1.evaluateBoolean(ec) == operand2.evaluateBoolean(ec));
 		case OR:
 			return new Boolean(operand1.evaluateBoolean(ec) || operand2.evaluateBoolean(ec));
 		case AND:
diff --git a/prism/src/parser/visitor/ConvertForJltl2ba.java b/prism/src/parser/visitor/ConvertForJltl2ba.java
index 5809149e..5299f94d 100644
--- a/prism/src/parser/visitor/ConvertForJltl2ba.java
+++ b/prism/src/parser/visitor/ConvertForJltl2ba.java
@@ -96,6 +96,9 @@ public class ConvertForJltl2ba extends ASTTraverseModify
 		case ExpressionBinaryOp.IMPLIES:
 			res = new SimpleLTL(SimpleLTL.LTLType.IMPLIES, ltl1, ltl2);
 			break;
+		case ExpressionBinaryOp.IFF:
+			res = new SimpleLTL(SimpleLTL.LTLType.EQUIV, ltl1, ltl2);
+			break;
 		case ExpressionBinaryOp.OR:
 			res = new SimpleLTL(SimpleLTL.LTLType.OR, ltl1, ltl2);
 			break;
diff --git a/prism/src/parser/visitor/Simplify.java b/prism/src/parser/visitor/Simplify.java
index e8fe8dc8..9814acc6 100644
--- a/prism/src/parser/visitor/Simplify.java
+++ b/prism/src/parser/visitor/Simplify.java
@@ -54,6 +54,22 @@ public class Simplify extends ASTTraverseModify
 			if (Expression.isTrue(e.getOperand1()))
 				return e.getOperand2();
 			break;
+		case ExpressionBinaryOp.IFF:
+			if (Expression.isFalse(e.getOperand1())) {
+				if (Expression.isFalse(e.getOperand2())) {
+					return Expression.True();
+				} else if (Expression.isTrue(e.getOperand2())) {
+					return Expression.False();
+				}
+			}
+			if (Expression.isTrue(e.getOperand1())) {
+				if (Expression.isFalse(e.getOperand2())) {
+					return Expression.False();
+				} else if (Expression.isTrue(e.getOperand2())) {
+					return Expression.True();
+				}
+			}
+			break;
 		case ExpressionBinaryOp.OR:
 			if (Expression.isTrue(e.getOperand1()) || Expression.isTrue(e.getOperand2()))
 				return Expression.True();
diff --git a/prism/src/parser/visitor/TypeCheck.java b/prism/src/parser/visitor/TypeCheck.java
index 4a76f88f..43fe4c8c 100644
--- a/prism/src/parser/visitor/TypeCheck.java
+++ b/prism/src/parser/visitor/TypeCheck.java
@@ -246,6 +246,7 @@ public class TypeCheck extends ASTTraverse
 
 		switch (e.getOperator()) {
 		case ExpressionBinaryOp.IMPLIES:
+		case ExpressionBinaryOp.IFF:
 		case ExpressionBinaryOp.OR:
 		case ExpressionBinaryOp.AND:
 			if (!(t1 instanceof TypeBool) && !(t1 instanceof TypePathBool)) {
diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java
index 22a31f1c..accfb1c8 100644
--- a/prism/src/prism/StateModelChecker.java
+++ b/prism/src/prism/StateModelChecker.java
@@ -401,6 +401,9 @@ public class StateModelChecker implements ModelChecker
 			case ExpressionBinaryOp.IMPLIES:
 				dd = JDD.Or(JDD.Not(dd1), dd2);
 				break;
+			case ExpressionBinaryOp.IFF:
+				dd = JDD.Not(JDD.Xor(dd1, dd2));
+				break;
 			case ExpressionBinaryOp.OR:
 				dd = JDD.Or(dd1, dd2);
 				break;