Refactoring multi-objective code: readying for allowing lists of objectives in strategy operator.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10849 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/ProbModelChecker.java

@@ -28,6 +28,7 @@ package explicit;
 
 import java.io.File;
 import java.util.BitSet;
+import java.util.List;
 
 import parser.ast.Coalition;
 import parser.ast.Expression;
@@ -515,10 +516,12 @@ public class ProbModelChecker extends NonProbModelChecker
 			coalition = null;
 		}
 
-		// Strip any parentheses (they might have been needlessly wrapped around a single P or R)
-		Expression exprSub = expr.getExpression();
-		while (Expression.isParenth(exprSub))
-			exprSub = ((ExpressionUnaryOp) exprSub).getOperand();
+		// For now, just support a single expression (which may encode a Boolean combination of objectives)
+		List<Expression> exprs = expr.getOperands();
+		if (exprs.size() > 1) {
+			throw new PrismException("Cannot currently check strategy operators wth lists of expressions");
+		}
+		Expression exprSub = exprs.get(0);
 		// Pass onto relevant method:
 		// P operator
 		if (exprSub instanceof ExpressionProb) {

prism/src/parser/PrismParser.java

@@ -3066,25 +3066,36 @@ public class PrismParser implements PrismParserConstants {
     case PMAX:
     case PMIN:
     case P:
-      expr = ExpressionProb(prop, pathprop);
-      break;
     case RMAX:
     case RMIN:
     case R:
-      expr = ExpressionReward(prop, pathprop);
+      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
+      case PMAX:
+      case PMIN:
+      case P:
+        expr = ExpressionProb(prop, pathprop);
+        break;
+      case RMAX:
+      case RMIN:
+      case R:
+        expr = ExpressionReward(prop, pathprop);
+        break;
+      default:
+        jj_la1[88] = jj_gen;
+        jj_consume_token(-1);
+        throw new ParseException();
+      }
+          ret.setSingleOperand(expr);
       break;
     case LPARENTH:
       expr = ExpressionParenth(prop, pathprop);
-      break;
-    case REG_IDENT:
-      expr = ExpressionFuncOrIdent(prop, pathprop);
+          ret.addOperand(expr);
       break;
     default:
-      jj_la1[88] = jj_gen;
+      jj_la1[89] = jj_gen;
       jj_consume_token(-1);
       throw new ParseException();
     }
-          ret.setExpression(expr);
                 ret.setPosition(begin, getToken(0));
                 {if (true) return ret;}
     throw new Error("Missing return statement in function");
@@ -3100,7 +3111,7 @@ public class PrismParser implements PrismParserConstants {
                       exprStrat.setCoalitionAllPlayers();
       break;
     default:
-      jj_la1[91] = jj_gen;
+      jj_la1[92] = jj_gen;
       switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
       case REG_INT:
       case REG_IDENT:
@@ -3113,7 +3124,7 @@ public class PrismParser implements PrismParserConstants {
             ;
             break;
           default:
-            jj_la1[89] = jj_gen;
+            jj_la1[90] = jj_gen;
             break label_28;
           }
           jj_consume_token(COMMA);
@@ -3122,7 +3133,7 @@ public class PrismParser implements PrismParserConstants {
         }
         break;
       default:
-        jj_la1[90] = jj_gen;
+        jj_la1[91] = jj_gen;
         ;
       }
           exprStrat.setCoalition(coalition);
@@ -3140,7 +3151,7 @@ public class PrismParser implements PrismParserConstants {
       jj_consume_token(REG_IDENT);
       break;
     default:
-      jj_la1[92] = jj_gen;
+      jj_la1[93] = jj_gen;
       jj_consume_token(-1);
       throw new ParseException();
     }
@@ -3165,7 +3176,7 @@ public class PrismParser implements PrismParserConstants {
                                                        s = "init";
       break;
     default:
-      jj_la1[93] = jj_gen;
+      jj_la1[94] = jj_gen;
       jj_consume_token(-1);
       throw new ParseException();
     }
@@ -3210,7 +3221,7 @@ public class PrismParser implements PrismParserConstants {
       op = Identifier();
       break;
     default:
-      jj_la1[94] = jj_gen;
+      jj_la1[95] = jj_gen;
       jj_consume_token(-1);
       throw new ParseException();
     }
@@ -3222,7 +3233,7 @@ public class PrismParser implements PrismParserConstants {
       filter = Expression(prop, pathprop);
       break;
     default:
-      jj_la1[95] = jj_gen;
+      jj_la1[96] = jj_gen;
       ;
     }
     jj_consume_token(RPARENTH);
@@ -3267,7 +3278,7 @@ public class PrismParser implements PrismParserConstants {
                                                                   ident="max";
       break;
     default:
-      jj_la1[96] = jj_gen;
+      jj_la1[97] = jj_gen;
       jj_consume_token(-1);
       throw new ParseException();
     }
@@ -3300,7 +3311,7 @@ public class PrismParser implements PrismParserConstants {
               {if (true) return ExpressionBinaryOp.NE;}
       break;
     default:
-      jj_la1[97] = jj_gen;
+      jj_la1[98] = jj_gen;
       jj_consume_token(-1);
       throw new ParseException();
     }
@@ -3327,7 +3338,7 @@ public class PrismParser implements PrismParserConstants {
               {if (true) return ExpressionBinaryOp.LE;}
       break;
     default:
-      jj_la1[98] = jj_gen;
+      jj_la1[99] = jj_gen;
       jj_consume_token(-1);
       throw new ParseException();
     }
@@ -3352,7 +3363,7 @@ public class PrismParser implements PrismParserConstants {
       step = Expression(false, false);
       break;
     default:
-      jj_la1[99] = jj_gen;
+      jj_la1[100] = jj_gen;
       ;
     }
     jj_consume_token(0);
@@ -3491,12 +3502,17 @@ public class PrismParser implements PrismParserConstants {
     finally { jj_save(17, xla); }
   }
 
-  static private boolean jj_3R_189() {
+  static private boolean jj_3R_187() {
     if (jj_scan_token(COMMA)) return true;
     if (jj_3R_38()) return true;
     return false;
   }
 
+  static private boolean jj_3R_48() {
+    if (jj_scan_token(REG_IDENTPRIME)) return true;
+    return false;
+  }
+
   static private boolean jj_3R_164() {
     if (jj_3R_29()) return true;
     return false;
@@ -3510,12 +3526,7 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
-  static private boolean jj_3R_48() {
-    if (jj_scan_token(REG_IDENTPRIME)) return true;
-    return false;
-  }
-
-  static private boolean jj_3R_186() {
+  static private boolean jj_3R_184() {
     if (jj_scan_token(OR)) return true;
     return false;
   }
@@ -3533,13 +3544,13 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
-  static private boolean jj_3R_163() {
-    if (jj_scan_token(MAX)) return true;
+  static private boolean jj_3R_32() {
+    if (jj_3R_29()) return true;
     return false;
   }
 
-  static private boolean jj_3R_32() {
-    if (jj_3R_29()) return true;
+  static private boolean jj_3R_163() {
+    if (jj_scan_token(MAX)) return true;
     return false;
   }
 
@@ -3553,12 +3564,12 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
-  static private boolean jj_3R_185() {
+  static private boolean jj_3R_183() {
     if (jj_scan_token(AND)) return true;
     return false;
   }
 
-  static private boolean jj_3R_183() {
+  static private boolean jj_3R_181() {
     if (jj_scan_token(MAX)) return true;
     return false;
   }
@@ -3568,13 +3579,18 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
+  static private boolean jj_3R_29() {
+    if (jj_scan_token(REG_IDENT)) return true;
+    return false;
+  }
+
   static private boolean jj_3_4() {
     if (jj_scan_token(LABEL)) return true;
     return false;
   }
 
-  static private boolean jj_3R_29() {
-    if (jj_scan_token(REG_IDENT)) return true;
+  static private boolean jj_3R_179() {
+    if (jj_scan_token(INIT)) return true;
     return false;
   }
 
@@ -3589,8 +3605,9 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
-  static private boolean jj_3R_181() {
-    if (jj_scan_token(INIT)) return true;
+  static private boolean jj_3R_186() {
+    if (jj_scan_token(COMMA)) return true;
+    if (jj_3R_38()) return true;
     return false;
   }
 
@@ -3599,12 +3616,6 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
-  static private boolean jj_3R_188() {
-    if (jj_scan_token(COMMA)) return true;
-    if (jj_3R_38()) return true;
-    return false;
-  }
-
   static private boolean jj_3R_79() {
     if (jj_scan_token(LPARENTH)) return true;
     if (jj_3R_31()) return true;
@@ -3612,6 +3623,16 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
+  static private boolean jj_3R_185() {
+    if (jj_3R_29()) return true;
+    return false;
+  }
+
+  static private boolean jj_3R_182() {
+    if (jj_scan_token(PLUS)) return true;
+    return false;
+  }
+
   static private boolean jj_3R_154() {
     if (jj_scan_token(REG_INT)) return true;
     return false;
@@ -3624,8 +3645,8 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
-  static private boolean jj_3R_187() {
-    if (jj_3R_29()) return true;
+  static private boolean jj_3R_180() {
+    if (jj_scan_token(MIN)) return true;
     return false;
   }
 
@@ -3645,13 +3666,8 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
-  static private boolean jj_3R_184() {
-    if (jj_scan_token(PLUS)) return true;
-    return false;
-  }
-
-  static private boolean jj_3R_182() {
-    if (jj_scan_token(MIN)) return true;
+  static private boolean jj_3R_178() {
+    if (jj_3R_29()) return true;
     return false;
   }
 
@@ -3671,11 +3687,6 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
-  static private boolean jj_3R_180() {
-    if (jj_3R_29()) return true;
-    return false;
-  }
-
   static private boolean jj_3R_68() {
     Token xsp;
     xsp = jj_scanpos;
@@ -3694,17 +3705,17 @@ public class PrismParser implements PrismParserConstants {
     if (jj_scan_token(LPARENTH)) return true;
     Token xsp;
     xsp = jj_scanpos;
+    if (jj_3R_180()) {
+    jj_scanpos = xsp;
+    if (jj_3R_181()) {
+    jj_scanpos = xsp;
     if (jj_3R_182()) {
     jj_scanpos = xsp;
     if (jj_3R_183()) {
     jj_scanpos = xsp;
     if (jj_3R_184()) {
     jj_scanpos = xsp;
-    if (jj_3R_185()) {
-    jj_scanpos = xsp;
-    if (jj_3R_186()) {
-    jj_scanpos = xsp;
-    if (jj_3R_187()) return true;
+    if (jj_3R_185()) return true;
     }
     }
     }
@@ -3713,7 +3724,7 @@ public class PrismParser implements PrismParserConstants {
     if (jj_scan_token(COMMA)) return true;
     if (jj_3R_38()) return true;
     xsp = jj_scanpos;
-    if (jj_3R_188()) jj_scanpos = xsp;
+    if (jj_3R_186()) jj_scanpos = xsp;
     if (jj_scan_token(RPARENTH)) return true;
     return false;
   }
@@ -3723,7 +3734,7 @@ public class PrismParser implements PrismParserConstants {
     Token xsp;
     while (true) {
       xsp = jj_scanpos;
-      if (jj_3R_189()) { jj_scanpos = xsp; break; }
+      if (jj_3R_187()) { jj_scanpos = xsp; break; }
     }
     return false;
   }
@@ -3783,23 +3794,23 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
-  static private boolean jj_3R_179() {
-    if (jj_3R_143()) return true;
-    return false;
-  }
-
   static private boolean jj_3R_152() {
     if (jj_scan_token(DQUOTE)) return true;
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_180()) {
+    if (jj_3R_178()) {
     jj_scanpos = xsp;
-    if (jj_3R_181()) return true;
+    if (jj_3R_179()) return true;
     }
     if (jj_scan_token(DQUOTE)) return true;
     return false;
   }
 
+  static private boolean jj_3R_207() {
+    if (jj_3R_148()) return true;
+    return false;
+  }
+
   static private boolean jj_3R_80() {
     if (jj_scan_token(DIVIDE)) return true;
     if (jj_scan_token(LBRACE)) return true;
@@ -3823,11 +3834,6 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
-  static private boolean jj_3R_177() {
-    if (jj_3R_148()) return true;
-    return false;
-  }
-
   static private boolean jj_3R_58() {
     if (jj_3R_68()) return true;
     Token xsp;
@@ -3908,6 +3914,13 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
+  static private boolean jj_3R_210() {
+    Token xsp;
+    xsp = jj_scanpos;
+    if (jj_3R_214()) jj_scanpos = xsp;
+    return false;
+  }
+
   static private boolean jj_3_2() {
     if (jj_scan_token(DQUOTE)) return true;
     if (jj_3R_29()) return true;
@@ -3924,19 +3937,12 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
-  static private boolean jj_3R_210() {
-    Token xsp;
-    xsp = jj_scanpos;
-    if (jj_3R_214()) jj_scanpos = xsp;
-    return false;
-  }
-
   static private boolean jj_3R_209() {
     if (jj_scan_token(TIMES)) return true;
     return false;
   }
 
-  static private boolean jj_3R_207() {
+  static private boolean jj_3R_205() {
     Token xsp;
     xsp = jj_scanpos;
     if (jj_3R_209()) {
@@ -3979,17 +3985,17 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
-  static private boolean jj_3R_139() {
-    if (jj_3R_151()) return true;
+  static private boolean jj_3R_177() {
+    if (jj_3R_146()) return true;
     return false;
   }
 
-  static private boolean jj_3R_178() {
-    if (jj_3R_146()) return true;
+  static private boolean jj_3R_139() {
+    if (jj_3R_151()) return true;
     return false;
   }
 
-  static private boolean jj_3R_176() {
+  static private boolean jj_3R_206() {
     if (jj_3R_147()) return true;
     return false;
   }
@@ -3999,9 +4005,19 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
+  static private boolean jj_3R_176() {
+    Token xsp;
+    xsp = jj_scanpos;
+    if (jj_3R_206()) {
+    jj_scanpos = xsp;
+    if (jj_3R_207()) return true;
+    }
+    return false;
+  }
+
   static private boolean jj_3R_175() {
     if (jj_scan_token(DLBRACKET)) return true;
-    if (jj_3R_207()) return true;
+    if (jj_3R_205()) return true;
     if (jj_scan_token(DRBRACKET)) return true;
     return false;
   }
@@ -4023,7 +4039,7 @@ public class PrismParser implements PrismParserConstants {
 
   static private boolean jj_3R_174() {
     if (jj_scan_token(DLT)) return true;
-    if (jj_3R_207()) return true;
+    if (jj_3R_205()) return true;
     if (jj_scan_token(DGT)) return true;
     return false;
   }
@@ -4053,13 +4069,7 @@ public class PrismParser implements PrismParserConstants {
     xsp = jj_scanpos;
     if (jj_3R_176()) {
     jj_scanpos = xsp;
-    if (jj_3R_177()) {
-    jj_scanpos = xsp;
-    if (jj_3R_178()) {
-    jj_scanpos = xsp;
-    if (jj_3R_179()) return true;
-    }
-    }
+    if (jj_3R_177()) return true;
     }
     return false;
   }
@@ -4234,7 +4244,7 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
-  static private boolean jj_3R_206() {
+  static private boolean jj_3R_204() {
     if (jj_3R_38()) return true;
     return false;
   }
@@ -4254,7 +4264,7 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
-  static private boolean jj_3R_205() {
+  static private boolean jj_3R_203() {
     if (jj_scan_token(I)) return true;
     if (jj_scan_token(EQ)) return true;
     if (jj_3R_38()) return true;
@@ -4266,12 +4276,12 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
-  static private boolean jj_3R_204() {
+  static private boolean jj_3R_202() {
     if (jj_scan_token(C)) return true;
     return false;
   }
 
-  static private boolean jj_3R_203() {
+  static private boolean jj_3R_201() {
     if (jj_scan_token(C)) return true;
     if (jj_scan_token(LE)) return true;
     if (jj_3R_38()) return true;
@@ -4283,7 +4293,7 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
-  static private boolean jj_3R_202() {
+  static private boolean jj_3R_200() {
     if (jj_scan_token(S)) return true;
     return false;
   }
@@ -4311,7 +4321,7 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
-  static private boolean jj_3R_201() {
+  static private boolean jj_3R_199() {
     if (jj_3R_33()) return true;
     return false;
   }
@@ -4326,17 +4336,17 @@ public class PrismParser implements PrismParserConstants {
   static private boolean jj_3R_172() {
     Token xsp;
     xsp = jj_scanpos;
+    if (jj_3R_199()) {
+    jj_scanpos = xsp;
+    if (jj_3R_200()) {
+    jj_scanpos = xsp;
     if (jj_3R_201()) {
     jj_scanpos = xsp;
     if (jj_3R_202()) {
     jj_scanpos = xsp;
     if (jj_3R_203()) {
     jj_scanpos = xsp;
-    if (jj_3R_204()) {
-    jj_scanpos = xsp;
-    if (jj_3R_205()) {
-    jj_scanpos = xsp;
-    if (jj_3R_206()) return true;
+    if (jj_3R_204()) return true;
     }
     }
     }
@@ -4462,18 +4472,18 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
-  static private boolean jj_3R_197() {
+  static private boolean jj_3R_195() {
     if (jj_3R_45()) return true;
     if (jj_3R_38()) return true;
     return false;
   }
 
-  static private boolean jj_3R_196() {
+  static private boolean jj_3R_194() {
     if (jj_3R_208()) return true;
     return false;
   }
 
-  static private boolean jj_3R_195() {
+  static private boolean jj_3R_193() {
     if (jj_scan_token(LPARENTH)) return true;
     if (jj_3R_32()) return true;
     if (jj_scan_token(RPARENTH)) return true;
@@ -4486,7 +4496,7 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
-  static private boolean jj_3R_200() {
+  static private boolean jj_3R_198() {
     if (jj_scan_token(MAX)) return true;
     if (jj_scan_token(EQ)) return true;
     if (jj_scan_token(QMARK)) return true;
@@ -4500,7 +4510,7 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
-  static private boolean jj_3R_199() {
+  static private boolean jj_3R_197() {
     if (jj_scan_token(MIN)) return true;
     if (jj_scan_token(EQ)) return true;
     if (jj_scan_token(QMARK)) return true;
@@ -4524,7 +4534,7 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
-  static private boolean jj_3R_198() {
+  static private boolean jj_3R_196() {
     if (jj_scan_token(EQ)) return true;
     if (jj_scan_token(QMARK)) return true;
     return false;
@@ -4539,17 +4549,17 @@ public class PrismParser implements PrismParserConstants {
     if (jj_scan_token(R)) return true;
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_195()) jj_scanpos = xsp;
+    if (jj_3R_193()) jj_scanpos = xsp;
     xsp = jj_scanpos;
-    if (jj_3R_196()) jj_scanpos = xsp;
+    if (jj_3R_194()) jj_scanpos = xsp;
     xsp = jj_scanpos;
-    if (jj_3R_197()) {
+    if (jj_3R_195()) {
     jj_scanpos = xsp;
-    if (jj_3R_198()) {
+    if (jj_3R_196()) {
     jj_scanpos = xsp;
-    if (jj_3R_199()) {
+    if (jj_3R_197()) {
     jj_scanpos = xsp;
-    if (jj_3R_200()) return true;
+    if (jj_3R_198()) return true;
     }
     }
     }
@@ -4931,24 +4941,24 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
-  static private boolean jj_3R_191() {
+  static private boolean jj_3R_54() {
+    if (jj_scan_token(LE)) return true;
+    return false;
+  }
+
+  static private boolean jj_3R_189() {
     if (jj_3R_45()) return true;
     if (jj_3R_38()) return true;
     return false;
   }
 
-  static private boolean jj_3R_190() {
+  static private boolean jj_3R_188() {
     if (jj_scan_token(LPARENTH)) return true;
     if (jj_3R_32()) return true;
     if (jj_scan_token(RPARENTH)) return true;
     return false;
   }
 
-  static private boolean jj_3R_54() {
-    if (jj_scan_token(LE)) return true;
-    return false;
-  }
-
   static private boolean jj_3R_53() {
     if (jj_scan_token(GE)) return true;
     return false;
@@ -4980,21 +4990,21 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
-  static private boolean jj_3R_194() {
+  static private boolean jj_3R_192() {
     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_193() {
+  static private boolean jj_3R_191() {
     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_192() {
+  static private boolean jj_3R_190() {
     if (jj_scan_token(EQ)) return true;
     if (jj_scan_token(QMARK)) return true;
     return false;
@@ -5024,21 +5034,11 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
-  static private boolean jj_3R_65() {
-    if (jj_3R_76()) return true;
-    return false;
-  }
-
   static private boolean jj_3R_119() {
     if (jj_scan_token(NE)) return true;
     return false;
   }
 
-  static private boolean jj_3R_64() {
-    if (jj_scan_token(R)) return true;
-    return false;
-  }
-
   static private boolean jj_3R_115() {
     Token xsp;
     xsp = jj_scanpos;
@@ -5054,6 +5054,16 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
+  static private boolean jj_3R_65() {
+    if (jj_3R_76()) return true;
+    return false;
+  }
+
+  static private boolean jj_3R_64() {
+    if (jj_scan_token(R)) return true;
+    return false;
+  }
+
   static private boolean jj_3R_63() {
     if (jj_scan_token(W)) return true;
     return false;
@@ -5063,15 +5073,15 @@ public class PrismParser implements PrismParserConstants {
     if (jj_scan_token(P)) return true;
     Token xsp;
     xsp = jj_scanpos;
-    if (jj_3R_190()) jj_scanpos = xsp;
+    if (jj_3R_188()) jj_scanpos = xsp;
     xsp = jj_scanpos;
-    if (jj_3R_191()) {
+    if (jj_3R_189()) {
     jj_scanpos = xsp;
-    if (jj_3R_192()) {
+    if (jj_3R_190()) {
     jj_scanpos = xsp;
-    if (jj_3R_193()) {
+    if (jj_3R_191()) {
     jj_scanpos = xsp;
-    if (jj_3R_194()) return true;
+    if (jj_3R_192()) return true;
     }
     }
     }
@@ -5129,7 +5139,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[100];
+  static final private int[] jj_la1 = new int[101];
   static private int[] jj_la1_0;
   static private int[] jj_la1_1;
   static private int[] jj_la1_2;
@@ -5139,13 +5149,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,0x8000030,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,0x0,0xa0000000,0x0,0x0,0x0,0xa0000000,0x0,0x0,0x0,0x0,0x0,0xa0000000,0x0,0x0,0xa0ba0808,0xa0ba0808,0x0,0x0,0xa4ba0908,0x0,0x0,0x0,0x0,0x0,0x0,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,0x8000030,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,0x0,0xa0000000,0x0,0x0,0x0,0xa0000000,0x0,0x0,0x0,0x0,0x0,0xa0000000,0x0,0x0,0xa0ba0808,0xa0ba0808,0x0,0x0,0xa4ba0908,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x1000000,0xa0000000,0x0,0xa0000000,0x0,0x0,0x0,};
    }
    private static void jj_la1_init_1() {
-      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,0x40000000,0x0,0x38,0x0,0x0,0x0,0x40000000,0x40000000,0x0,0x40000000,0x0,0x0,0x3800,0x0,0x4012783a,0x4012783a,0x0,0x4000,0x4012783a,0x0,0x40003838,0x10000000,0x0,0x0,0x0,0x0,0x600000,0x10000000,0x0,0x0,0x0,0x4000000,};
+      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,0x40000000,0x0,0x38,0x0,0x0,0x0,0x40000000,0x40000000,0x0,0x40000000,0x0,0x0,0x3800,0x0,0x4012783a,0x4012783a,0x0,0x4000,0x4012783a,0x0,0x3838,0x40003838,0x10000000,0x0,0x0,0x0,0x0,0x600000,0x10000000,0x0,0x0,0x0,0x4000000,};
    }
    private static void jj_la1_init_2() {
-      jj_la1_2 = new int[] {0x0,0x0,0x0,0x2e08404,0x0,0x2e08404,0x2e08404,0x0,0x2e08404,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x40,0x0,0x1,0x2000000,0x0,0x1,0x2000000,0x4000,0x2e08404,0x0,0x0,0x0,0x2e08405,0x2000000,0x1,0x0,0x20010,0x0,0x0,0x20010,0x2200000,0x0,0x3341,0x0,0x0,0x3341,0x2e08404,0x2e08404,0x2e08404,0x2e08404,0x2e08404,0x3341,0x100000,0x0,0x0,0x0,0x0,0x2e08404,0xc0,0x3300,0xc000,0xc000,0x30000,0x30000,0x2e08404,0x2e00404,0x0,0x0,0x2000000,0x0,0xc00000,0x0,0x3340,0x0,0x10,0x10,0x0,0x0,0x3340,0x10,0x0,0x10,0x3340,0x0,0x10,0x2e08404,0x2e08404,0x20000,0x0,0x2e08404,0x404,0x2000000,0x0,0x2400000,0x10000,0x2400000,0x2000000,0x2004000,0x0,0x2000000,0xc0,0x3300,0x0,};
+      jj_la1_2 = new int[] {0x0,0x0,0x0,0x2e08404,0x0,0x2e08404,0x2e08404,0x0,0x2e08404,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x40,0x0,0x1,0x2000000,0x0,0x1,0x2000000,0x4000,0x2e08404,0x0,0x0,0x0,0x2e08405,0x2000000,0x1,0x0,0x20010,0x0,0x0,0x20010,0x2200000,0x0,0x3341,0x0,0x0,0x3341,0x2e08404,0x2e08404,0x2e08404,0x2e08404,0x2e08404,0x3341,0x100000,0x0,0x0,0x0,0x0,0x2e08404,0xc0,0x3300,0xc000,0xc000,0x30000,0x30000,0x2e08404,0x2e00404,0x0,0x0,0x2000000,0x0,0xc00000,0x0,0x3340,0x0,0x10,0x10,0x0,0x0,0x3340,0x10,0x0,0x10,0x3340,0x0,0x10,0x2e08404,0x2e08404,0x20000,0x0,0x2e08404,0x404,0x0,0x0,0x0,0x2400000,0x10000,0x2400000,0x2000000,0x2004000,0x0,0x2000000,0xc0,0x3300,0x0,};
    }
   static final private JJCalls[] jj_2_rtns = new JJCalls[18];
   static private boolean jj_rescan = false;
@@ -5169,7 +5179,7 @@ public class PrismParser implements PrismParserConstants {
     token = new Token();
     jj_ntk = -1;
     jj_gen = 0;
-    for (int i = 0; i < 100; i++) jj_la1[i] = -1;
+    for (int i = 0; i < 101; i++) jj_la1[i] = -1;
     for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
   }
 
@@ -5184,7 +5194,7 @@ public class PrismParser implements PrismParserConstants {
     token = new Token();
     jj_ntk = -1;
     jj_gen = 0;
-    for (int i = 0; i < 100; i++) jj_la1[i] = -1;
+    for (int i = 0; i < 101; i++) jj_la1[i] = -1;
     for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
   }
 
@@ -5202,7 +5212,7 @@ public class PrismParser implements PrismParserConstants {
     token = new Token();
     jj_ntk = -1;
     jj_gen = 0;
-    for (int i = 0; i < 100; i++) jj_la1[i] = -1;
+    for (int i = 0; i < 101; i++) jj_la1[i] = -1;
     for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
   }
 
@@ -5213,7 +5223,7 @@ public class PrismParser implements PrismParserConstants {
     token = new Token();
     jj_ntk = -1;
     jj_gen = 0;
-    for (int i = 0; i < 100; i++) jj_la1[i] = -1;
+    for (int i = 0; i < 101; i++) jj_la1[i] = -1;
     for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
   }
 
@@ -5230,7 +5240,7 @@ public class PrismParser implements PrismParserConstants {
     token = new Token();
     jj_ntk = -1;
     jj_gen = 0;
-    for (int i = 0; i < 100; i++) jj_la1[i] = -1;
+    for (int i = 0; i < 101; i++) jj_la1[i] = -1;
     for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
   }
 
@@ -5240,7 +5250,7 @@ public class PrismParser implements PrismParserConstants {
     token = new Token();
     jj_ntk = -1;
     jj_gen = 0;
-    for (int i = 0; i < 100; i++) jj_la1[i] = -1;
+    for (int i = 0; i < 101; i++) jj_la1[i] = -1;
     for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
   }
 
@@ -5357,7 +5367,7 @@ public class PrismParser implements PrismParserConstants {
       la1tokens[jj_kind] = true;
       jj_kind = -1;
     }
-    for (int i = 0; i < 100; i++) {
+    for (int i = 0; i < 101; i++) {
       if (jj_la1[i] == jj_gen) {
         for (int j = 0; j < 32; j++) {
           if ((jj_la1_0[i] & (1<<j)) != 0) {

prism/src/parser/PrismParser.jj

@@ -1776,10 +1776,12 @@ Expression ExpressionStrategy(boolean prop, boolean pathprop) :
 	(( begin = <DLT> { ret = new ExpressionStrategy(true); } ExpressionStrategyCoalition(ret) <DGT> )
 	| (begin = <DLBRACKET> { ret = new ExpressionStrategy(false); } ExpressionStrategyCoalition(ret) <DRBRACKET> ))
 	// Child expression
-	( expr = ExpressionProb(prop, pathprop) | expr = ExpressionReward(prop, pathprop)
-	| expr = ExpressionParenth(prop, pathprop) | expr = ExpressionFuncOrIdent(prop, pathprop) )
-	{ ret.setExpression(expr); }
-	)
+	(
+	( expr = ExpressionProb(prop, pathprop) | expr = ExpressionReward(prop, pathprop) )
+	{ ret.setSingleOperand(expr); }
+	| expr = ExpressionParenth(prop, pathprop)
+	{ ret.addOperand(expr); }
+	))
 	{
 		ret.setPosition(begin, getToken(0));
 		return ret;

prism/src/parser/ast/ExpressionStrategy.java

@@ -26,6 +26,7 @@
 
 package parser.ast;
 
+import java.util.ArrayList;
 import java.util.List;
 
 import parser.EvaluateContext;
@@ -44,9 +45,12 @@ public class ExpressionStrategy extends Expression
 	/** Coalition info (for game models) */
 	protected Coalition coalition = new Coalition(); 
 	
-	/** Child expression */
-	protected Expression expression = null;
-
+	/** Child expression(s) */
+	protected List<Expression> operands = new ArrayList<Expression>();
+	
+	/** Is there just a single operand (P/R operator)? If not, the operand list will be parenthesised. **/
+	protected boolean singleOperand = false;
+	
 	// Constructors
 
 	public ExpressionStrategy()
@@ -61,7 +65,8 @@ public class ExpressionStrategy extends Expression
 	public ExpressionStrategy(boolean thereExists, Expression expression)
 	{
 		this.thereExists = thereExists;
-		this.expression = expression;
+		operands.add(expression);
+		singleOperand = true;
 	}
 
 	// Set methods
@@ -81,9 +86,21 @@ public class ExpressionStrategy extends Expression
 		this.coalition.setPlayers(coalition);
 	}
 
-	public void setExpression(Expression expression)
+	public void setSingleOperand(Expression expression)
+	{
+		operands.clear();
+		operands.add(expression);
+		singleOperand = true;
+	}
+
+	public void addOperand(Expression e)
 	{
-		this.expression = expression;
+		operands.add(e);
+	}
+
+	public void setOperand(int i, Expression e)
+	{
+		operands.set(i, e);
 	}
 
 	// Get methods
@@ -116,9 +133,24 @@ public class ExpressionStrategy extends Expression
 		return coalition.getPlayers();
 	}
 	
-	public Expression getExpression()
+	public boolean hasSingleOperand()
 	{
-		return expression;
+		return singleOperand;
+	}
+	
+	public int getNumOperands()
+	{
+		return operands.size();
+	}
+
+	public Expression getOperand(int i)
+	{
+		return operands.get(i);
+	}
+
+	public List<Expression> getOperands()
+	{
+		return operands;
 	}
 
 	// Methods required for Expression:
@@ -141,11 +173,11 @@ public class ExpressionStrategy extends Expression
 		throw new PrismLangException("Cannot evaluate a " + getOperatorString() + " operator without a model");
 	}
 
-	@Override
+	/*@Override
 	public String getResultName()
 	{
 		return expression.getResultName();
-	}
+	}*/
 
 	@Override
 	public boolean returnsSingleValue()
@@ -167,7 +199,10 @@ public class ExpressionStrategy extends Expression
 		ExpressionStrategy expr = new ExpressionStrategy();
 		expr.setThereExists(isThereExists());
 		expr.coalition = new Coalition(coalition);
-		expr.setExpression(expression == null ? null : expression.deepCopy());
+		for (Expression operand : operands) {
+			expr.addOperand((Expression) operand.deepCopy());
+		}
+		expr.singleOperand = singleOperand;
 		expr.setType(type);
 		expr.setPosition(this);
 		return expr;
@@ -181,8 +216,21 @@ public class ExpressionStrategy extends Expression
 		String s = "";
 		s += (thereExists ? "<<" : "[[");
 		s += coalition;
-		s += (thereExists ? ">>" : "]]");
-		s += " " + expression.toString();
+		s += (thereExists ? ">> " : "]] ");
+		if (singleOperand) {
+			s += operands.get(0);
+		} else {
+			s += "(";
+			boolean first = true;
+			for (Expression operand : operands) {
+				if (!first)
+					s += ", ";
+				else
+					first = false;
+				s = s + operand;
+			}
+			s += ")";
+		}
 		return s;
 	}
 
@@ -192,7 +240,8 @@ public class ExpressionStrategy extends Expression
 		final int prime = 31;
 		int result = 1;
 		result = prime * result + ((coalition == null) ? 0 : coalition.hashCode());
-		result = prime * result + ((expression == null) ? 0 : expression.hashCode());
+		result = prime * result + ((operands == null) ? 0 : operands.hashCode());
+		result = prime * result + (singleOperand ? 1231 : 1237);
 		result = prime * result + (thereExists ? 1231 : 1237);
 		return result;
 	}
@@ -212,10 +261,12 @@ public class ExpressionStrategy extends Expression
 				return false;
 		} else if (!coalition.equals(other.coalition))
 			return false;
-		if (expression == null) {
-			if (other.expression != null)
+		if (operands == null) {
+			if (other.operands != null)
 				return false;
-		} else if (!expression.equals(other.expression))
+		} else if (!operands.equals(other.operands))
+			return false;
+		if (singleOperand != other.singleOperand)
 			return false;
 		if (thereExists != other.thereExists)
 			return false;

prism/src/parser/visitor/ASTTraverse.java

@@ -546,7 +546,10 @@ public class ASTTraverse implements ASTVisitor
 	public Object visit(ExpressionStrategy e) throws PrismLangException
 	{
 		visitPre(e);
-		if (e.getExpression() != null) e.getExpression().accept(this);
+		int i, n = e.getNumOperands();
+		for (i = 0; i < n; i++) {
+			if (e.getOperand(i) != null) e.getOperand(i).accept(this);
+		}
 		visitPost(e);
 		return null;
 	}

prism/src/parser/visitor/ASTTraverseModify.java

@@ -559,7 +559,10 @@ public class ASTTraverseModify implements ASTVisitor
 	public Object visit(ExpressionStrategy e) throws PrismLangException
 	{
 		visitPre(e);
-		if (e.getExpression() != null) e.setExpression((Expression)(e.getExpression().accept(this)));
+		int i, n = e.getNumOperands();
+		for (i = 0; i < n; i++) {
+			if (e.getOperand(i) != null) e.setOperand(i, (Expression)(e.getOperand(i).accept(this)));
+		}
 		visitPost(e);
 		return e;
 	}

prism/src/parser/visitor/TypeCheck.java

@@ -552,7 +552,20 @@ public class TypeCheck extends ASTTraverse
 
 	public void visitPost(ExpressionStrategy e) throws PrismLangException
 	{
-		e.setType(e.getExpression().getType());
+		// Get types of operands
+		int n = e.getNumOperands();
+		Type types[] = new Type[n];
+		for (int i = 0; i < n; i++) {
+			types[i] = e.getOperand(i).getType();
+		}
+
+		// Currently, resulting type is always same as first arg
+		if (types[0] instanceof TypeBool)
+			e.setType(TypeBool.getInstance());
+		else if (types.length == 1 || types[1] instanceof TypeBool) //in this case type[0] is TypeDouble
+			e.setType(TypeDouble.getInstance());
+		else
+			e.setType(TypeVoid.getInstance());
 	}
 
 	public void visitPost(ExpressionLabel e) throws PrismLangException

prism/src/prism/NondetModelChecker.java

@@ -202,22 +202,20 @@ public class NondetModelChecker extends NonProbModelChecker
 			coalition = null;
 		}
 
-		// Strip any parentheses
-		Expression exprSub = expr.getExpression();
-		while (Expression.isParenth(exprSub))
-			exprSub = ((ExpressionUnaryOp) exprSub).getOperand();
+		// Process operand(s)
+		List<Expression> exprs = expr.getOperands();
 		// Pass onto relevant method:
 		// Single P operator
-		if (exprSub instanceof ExpressionProb) {
-			return checkExpressionProb((ExpressionProb) exprSub, forAll);
+		if (exprs.size() == 1 && exprs.get(0) instanceof ExpressionProb) {
+			return checkExpressionProb((ExpressionProb) exprs.get(0), forAll);
 		}
 		// Single R operator
-		else if (exprSub instanceof ExpressionReward) {
-			return checkExpressionReward((ExpressionReward) exprSub, forAll);
+		else if (exprs.size() == 1 && exprs.get(0) instanceof ExpressionReward) {
+			return checkExpressionReward((ExpressionReward) exprs.get(0), forAll);
 		}
 		// Anything else is treated as multi-objective 
 		else {
-			return checkExpressionMultiObjective(expr, forAll);
+			return checkExpressionMultiObjective(exprs, forAll);
 		}
 	}
 	
@@ -350,21 +348,25 @@ public class NondetModelChecker extends NonProbModelChecker
 		}
 	}
 
-	protected StateValues checkExpressionMultiObjective(ExpressionStrategy expr, boolean forAll) throws PrismException
+	/**
+	 * Model check a multi-objective query (from the contents of a strategy operator).
+	 * Return the result as a StateValues object (usually this gives values for all states,
+	 * but for a multi-objective query, we just give a single value, usually for the initial state).
+	 * @param exprs The list of Expressions specifying the objectives
+	 * @param forAll Are we checking "for all strategies" (true) or "there exists a strategy" (false)? [irrelevant for numerical (=?) queries] 
+	 */
+	protected StateValues checkExpressionMultiObjective(List<Expression> exprs, boolean forAll) throws PrismException
 	{
-		// Copy expression because we will modify it
-		expr = (ExpressionStrategy) expr.deepCopy();
-
-		// Strip any outer parentheses in operand
-		Expression exprSub = expr.getExpression();
-		while (Expression.isParenth(exprSub)) {
-			exprSub = ((ExpressionUnaryOp) exprSub).getOperand();
+		// For now, just support a single expression (which may encode a Boolean combination of objectives)
+		if (exprs.size() > 1) {
+			throw new PrismException("Cannot currently check strategy operators with lists of expressions");
 		}
-
-		// Reduce to form that can be expressed as an old multi(...) function..
+		Expression exprSub = exprs.get(0);
 
 		// Boolean
 		if (exprSub.getType() instanceof TypeBool) {
+			// Copy expression because we will modify it
+			exprSub = (ExpressionStrategy) exprSub.deepCopy();
 			// We will solve an existential query, so negate if universal
 			if (forAll) {
 				exprSub = Expression.Not(exprSub);
@@ -412,9 +414,7 @@ public class NondetModelChecker extends NonProbModelChecker
 				return checkExpressionMultiObjective(exprMulti);
 			}
 		} else if (exprSub.getType() instanceof TypeDouble) {
-			ExpressionFunc exprMulti = new ExpressionFunc("multi");
-			exprMulti.addOperand(exprSub);
-			return checkExpressionMultiObjective(exprMulti);
+			return checkExpressionMultiObjective(exprs);
 		} else {
 			throw new PrismException("Multi-objective model checking not supported for: " + exprSub);
 		}
@@ -425,6 +425,21 @@ public class NondetModelChecker extends NonProbModelChecker
 	 * For multi-objective queries, we only find the value for one state.
 	 */
 	protected StateValues checkExpressionMultiObjective(ExpressionFunc expr) throws PrismException
+	{
+		// Extract objective list from 'multi' function
+		List<Expression> exprs = new ArrayList<Expression>();
+		int n = expr.getNumOperands();
+		for (int i = 0; i < n; i++) {
+			exprs.add(expr.getOperand(i));
+		}
+		return checkExpressionMultiObjective(exprs);
+	}
+	
+	/**
+	 * Model check a multi-objective expression and return the result.
+	 * For multi-objective queries, we only find the value for one state.
+	 */
+	protected StateValues checkExpressionMultiObjective(List<Expression> exprs) throws PrismException
 	{
 		// Objective/target info
 		List<JDDNode> multitargetDDs = null;
@@ -462,13 +477,13 @@ public class NondetModelChecker extends NonProbModelChecker
 		}*/
 
 		// Check format and extract bounds/etc.
-		int numObjectives = expr.getNumOperands();
+		int numObjectives = exprs.size();
 		OpsAndBoundsList opsAndBounds = new OpsAndBoundsList();
 		List<JDDNode> rewards = new ArrayList<JDDNode>(numObjectives);
 		List<JDDNode> transRewardsList = new ArrayList<JDDNode>(numObjectives);
 		List<Expression> pathFormulas = new ArrayList<Expression>(numObjectives);
 		for (int i = 0; i < numObjectives; i++) {
-			extractInfoFromMultiObjectiveOperand((ExpressionQuant) expr.getOperand(i), opsAndBounds, transRewardsList, pathFormulas);
+			extractInfoFromMultiObjectiveOperand((ExpressionQuant) exprs.get(i), opsAndBounds, transRewardsList, pathFormulas);
 		}
 
 		//currently we do 1 numerical subject to booleans, or multiple numericals only 
@@ -650,14 +665,14 @@ public class NondetModelChecker extends NonProbModelChecker
 			if (opsAndBounds.numberOfNumerical() == 2) {			
 				synchronized(TileList.getStoredTileLists()) {
 					//in multi-obj result probs go first, so we have to swap order if needed
-					if (expr.getOperand(0) instanceof ExpressionReward && expr.getOperand(1) instanceof ExpressionProb) {
-						TileList.storedFormulasX.add(expr.getOperand(1));
-						TileList.storedFormulasY.add(expr.getOperand(0));
+					if (exprs.get(0) instanceof ExpressionReward && exprs.get(1) instanceof ExpressionProb) {
+						TileList.storedFormulasX.add(exprs.get(1));
+						TileList.storedFormulasY.add(exprs.get(0));
 					} else {
-						TileList.storedFormulasX.add(expr.getOperand(0));
-						TileList.storedFormulasY.add(expr.getOperand(1));
+						TileList.storedFormulasX.add(exprs.get(0));
+						TileList.storedFormulasY.add(exprs.get(1));
 					}
-					TileList.storedFormulas.add(expr);
+					TileList.storedFormulas.add(exprs);
 					TileList.storedTileLists.add((TileList) value);
 				}
 			} //else, i.e. in 3D, the output was treated in the algorithm itself.

prism/src/prism/TileList.java

@@ -75,7 +75,7 @@ public class TileList
 	 */
 	protected static List<Expression> storedFormulasX;
 	protected static List<Expression> storedFormulasY;
-	protected static List<Expression> storedFormulas;
+	protected static List<List<Expression>> storedFormulas;
 
 	public static List<Expression> getStoredFormulasX()
 	{
@@ -87,7 +87,7 @@ public class TileList
 		return storedFormulasY;
 	}
 
-	public static List<Expression> getStoredFormulas()
+	public static List<List<Expression>> getStoredFormulas()
 	{
 		return storedFormulas;
 	}
@@ -104,7 +104,7 @@ public class TileList
 	static {
 		storedFormulasX = new ArrayList<Expression>();
 		storedFormulasY = new ArrayList<Expression>();
-		storedFormulas = new ArrayList<Expression>();
+		storedFormulas = new ArrayList<List<Expression>>();
 		storedTileLists = new ArrayList<TileList>();
 	}