accumulation: bail out of past operators when complex is forced

prism/src/explicit/AccumulationTransformation.java

@@ -97,12 +97,19 @@ public class AccumulationTransformation<M extends Model> implements ModelExpress
 		}
 		
 		// Figure out if we need a complex or a simple trafo...
-		boolean isComplex = mc.getSettings().getBoolean(PrismSettings.ACC_FORCE_COMPLEX) || accexp.hasFireOn() || !accexp.isNullary();
-		if(isComplex) {
-			mc.getLog().println(" ... which is complex!");
+		boolean isComplex    = accexp.hasFireOn() || !accexp.isNullary();
+		boolean isPast       = accexp.getSymbol().isMinus();
+		boolean forceComplex = mc.getSettings().getBoolean(PrismSettings.ACC_FORCE_COMPLEX);
+		
+		if(forceComplex && isPast) {
+			throw new PrismException("Unable to handle <->/[-] with -accforcecomplex. Bailing.");
+		}
+		
+		if(isComplex || forceComplex) {
+			mc.getLog().println(" ... using complex!");
 			doTransformationComplex(accexp, rewards);
 		} else {
-			mc.getLog().println(" ... which is simple!");
+			mc.getLog().println(" ... using simple!");
 			doTransformationSimple(accexp, rewards);
 		}
 	}