fix corner case: forcemulti and simple

prism/src/explicit/AccumulationTransformation.java

@@ -85,10 +85,10 @@ public class AccumulationTransformation<M extends ModelExplicit> implements Mode
 		// Get the first ExpressionAccumulation
 		mc.getLog().println("Looking for an accumulation formula...");
 		
-		boolean singleTrack = true;
+		boolean isSingleTrack = true;
 		ExpressionAccumulation accexp = transformedExpression.getFirstAccumulationExpressionWithoutTemporal();
 		if(accexp == null || mc.getSettings().getBoolean(PrismSettings.ACC_FORCE_MULTI)) {
-			singleTrack = false;
+			isSingleTrack = false;
 			accexp = transformedExpression.getFirstAccumulationExpression();
 		}
 		
@@ -120,15 +120,20 @@ public class AccumulationTransformation<M extends ModelExplicit> implements Mode
 		boolean isSimple     = !accexp.hasFireOn() && accexp.isNullary();
 		boolean isPast       = accexp.getSymbol().isMinus();
 		boolean forceComplex = mc.getSettings().getBoolean(PrismSettings.ACC_FORCE_COMPLEX);
+		boolean forceMulti   = mc.getSettings().getBoolean(PrismSettings.ACC_FORCE_MULTI);
 		
 		if(forceComplex && isPast) {
 			throw new PrismException("Unable to handle <->/[-] with -accforcecomplex. Bailing.");
 		}
 		
+		if(forceMulti && isSimple) {
+			mc.getLog().println("WARNING: accforcemulti set, but cannot be used with simple method. Using complex one.");
+		}
+		
 		// Build the AccumulationContext
 		AccumulationContext ctx = new AccumulationContext(accexp, rewards, mc);
-		ctx.singleTrack  = singleTrack;
-		ctx.simpleMethod = isSimple && !forceComplex;
+		ctx.singleTrack  = isSingleTrack && !forceMulti;
+		ctx.simpleMethod = isSimple      && !forceComplex && !forceMulti;
 		
 		// Build the product
 		clock.start("accumulation product construction");