accumulation: add -accforcemulti to disable single track opt

prism/src/explicit/AccumulationTransformation.java

@@ -72,15 +72,12 @@ public class AccumulationTransformation<M extends ModelExplicit> implements Mode
 		
 		mc.getLog().println("Performing accumulation transformation...");
 		
-		// Is this whole thing an ExpressionAccumulation?
-		//if(transformedExpression.isAccumulationExpression()) { System.out.println("HEYOOOO!!! " + transformedExpression); }
-
 		// TODO: WHILE getFirstAccumulationExpression
 		
 		// Get the first ExpressionAccumulation
 		boolean singleTrack = true;
 		ExpressionAccumulation accexp = transformedExpression.getFirstAccumulationExpressionWithoutTemporal();
-		if(accexp == null) {
+		if(accexp == null || mc.getSettings().getBoolean(PrismSettings.ACC_FORCE_MULTI)) {
 			singleTrack = false;
 			accexp = transformedExpression.getFirstAccumulationExpression();
 		}

prism/src/prism/PrismSettings.java

@@ -161,6 +161,7 @@ public class PrismSettings implements Observer
 	//Accumulation
 	public static final String ACC_GENERATE_DOTS                    = "accumulation.generateDots";
 	public static final String ACC_FORCE_COMPLEX                    = "accumulation.forceComplex";
+	public static final String ACC_FORCE_MULTI						= "accumulation.forceMulti";
 	
 	//GUI Model
 	public static final	String MODEL_AUTO_PARSE						= "model.autoParse";
@@ -416,7 +417,9 @@ public class PrismSettings implements Observer
 		},		
 		{
 			{ BOOLEAN_TYPE,     ACC_GENERATE_DOTS,                      "Accumulation: generate DOT files",     "4.4",          false, "", "Generate DOT files for accumulation monitors and products"},
-			{ BOOLEAN_TYPE,     ACC_FORCE_COMPLEX,                      "Accumulation: force U-construction",   "4.4",          false, "", "Force compxe accumulation construction"}
+			{ BOOLEAN_TYPE,     ACC_FORCE_COMPLEX,                      "Accumulation: force U-construction",   "4.4",          false, "", "Force complex accumulation construction"},
+			{ BOOLEAN_TYPE,     ACC_FORCE_MULTI,                        "Accumulation: force multiple tracks",  "4.4",          false, "", "Force multiple accumulation tracks"}
+
 		},
 		{
 			{ BOOLEAN_TYPE,		MODEL_AUTO_PARSE,						"Auto parse",							"2.1",			new Boolean(true),															"",																							"Parse PRISM models automatically as they are loaded/edited in the text editor." },
@@ -1700,6 +1703,10 @@ public class PrismSettings implements Observer
 			set(ACC_FORCE_COMPLEX, true);
 		}
 
+		else if (sw.equals("accforcemulti")) {
+			set(ACC_FORCE_MULTI, true);
+		}
+
 		// HIDDEN OPTIONS
 		
 		// export property automaton to file (hidden option)
@@ -1900,6 +1907,7 @@ public class PrismSettings implements Observer
 		mainLog.println();
 		mainLog.println("ACCUMULATION MODEL CHECKING OPTIONS:");
 		mainLog.println("-accforcecomplex ............... Force rewriting into complex until formulae for accumulation");
+		mainLog.println("-accforcemulti.. ............... Force multiple accumulation tracks");
 		mainLog.println("-accgeneratedots ............... Generate DOT files for accumulation automata and products");
 	}