ModelVariablesDD: preallocation of extra action variables, new settings -ddextrastatevars and -ddextraactionvars

The -ddextrastatevars setting allows to change the number of state variable pairs that are preallocated
before the actual model state variables. Previously, 20 state variable pairs were allocated for the
product construction (LTL). From now on, this is the default, but the amount can be changed, e.g., to
0 to force all automaton states to be allocated at the bottom of the MTBDD.

From now on, additionally, we also preallocate 20 action variables at the top of the MTBDD,
which will provide extra action / non-deterministic choice bits for symbolic model transformations
that require additional non-deterministic choices, e.g., additional special actions, etc.
The number of preallocated action variables is configurable by the -ddextraactionvars setting.

Adding the additional variables should not have a performance impact, as they are "don't cares"
in the normal MTBDD encoding of the models.

For the sparse and hybrid engine, allocating the nondeterministic choice variables at the top
makes sense for performance reasons (the submatrix for each choice is a sub-MTBDD), so we currently
only support extra action variables at the top.


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

prism/src/prism/ModelVariablesDD.java

@@ -50,6 +50,8 @@ public class ModelVariablesDD
 
 	/** Storage for the preallocated extra state variables */
 	private JDDVars extraStateVariables = new JDDVars();
+	/** Storage for the preallocated extra action variables */
+	private JDDVars extraActionVariables = new JDDVars();
 
 	/** Constructor */
 	public ModelVariablesDD()
@@ -67,6 +69,7 @@ public class ModelVariablesDD
 		result.ddVarNames = new Vector<String>(ddVarNames);
 		result.ddVariables = ddVariables.copy();
 		result.extraStateVariables = extraStateVariables.copy();
+		result.extraActionVariables = extraActionVariables.copy();
 		result.nextDDVarIndex = nextDDVarIndex;
 
 		return result;
@@ -77,6 +80,7 @@ public class ModelVariablesDD
 	{
 		ddVariables.derefAll();
 		extraStateVariables.derefAll();
+		extraActionVariables.derefAll();
 	}
 
 	/** Return the vector with variable names for a given variable index */
@@ -195,6 +199,47 @@ public class ModelVariablesDD
 		return result;
 	}
 
+	/** Preallocate the given number of action variables */
+	public void preallocateExtraActionVariables(int count)
+	{
+		for (int i=0;i<count;i++) {
+			JDDNode v = allocateVariable("");
+			extraActionVariables.addVar(v);
+		}
+	}
+
+	/**
+	 * Allocate {@code n} action variables.
+	 * <br>
+	 * If there is not enough space in the preallocated variable pool, throws an exception.
+	 * <br>[ REFS: <i>result</i> ]
+	 * @param n number of action variables to allocate
+	 * @param name the name of the variable
+	 * 	 */
+	public JDDVars allocateExtraActionVariable(int n, String name) throws PrismException
+	{
+		JDDVars result = new JDDVars();
+		if (n == 0) return result;
+
+		if (extraActionVariables.getNumVars() < n) {
+			throw new PrismException("Not enough extra action variables preallocated, please increase using -ddextraactionvars switch!");
+		}
+
+		int v = extraActionVariables.getNumVars() - n;
+		for (int i=0; i < n; i++) {
+			// transfer action var from extraActionVariables to result,
+			// no need to ref again
+			JDDNode action_var = extraActionVariables.getVar(v++);
+			result.addVar(action_var);
+			ddVarNames.set(action_var.getIndex(), name+"."+i);
+		}
+
+		// remove variables from extraActionVariables
+		extraActionVariables.removeVars(result);
+
+		return result;
+	}
+
 	/**
 	 * Get the extra state variables.
 	 * This is not a copy.
@@ -205,4 +250,14 @@ public class ModelVariablesDD
 		return extraStateVariables;
 	}
 
+	/**
+	 * Get the extra action variables.
+	 * This is not a copy.
+	 *
+	 * <br>[ REFs: <i>none</i>, DEREFs: <i>none</i> ]
+	 */
+	public JDDVars getExtraActionVariables() {
+		return extraActionVariables;
+	}
+
 }

prism/src/prism/Modules2MTBDD.java

@@ -346,6 +346,8 @@ public class Modules2MTBDD
 		case 1:
 		// ordering: (a ... a) (s ... s) (l ... l) (r c ... r c)
 		
+			modelVariables.preallocateExtraActionVariables(prism.getSettings().getInteger(PrismSettings.PRISM_DD_EXTRA_ACTION_VARS));
+
 			// create arrays/etc. first
 			
 			// nondeterministic variables
@@ -400,7 +402,7 @@ public class Modules2MTBDD
 			// create a gap in the dd variables
 			// this allows to prepend additional row/col vars, e.g. for constructing
 			// a product model when doing LTL model checking
-			modelVariables.preallocateExtraStateVariables(20);
+			modelVariables.preallocateExtraStateVariables(prism.getSettings().getInteger(PrismSettings.PRISM_DD_EXTRA_STATE_VARS));
 
 			
 			// allocate dd variables for module variables (i.e. rows/cols)
@@ -424,6 +426,8 @@ public class Modules2MTBDD
 		case 2:
 		// ordering: (a ... a) (l ... l) (s r c ... r c) (s r c ... r c) ...
 	
+			modelVariables.preallocateExtraActionVariables(prism.getSettings().getInteger(PrismSettings.PRISM_DD_EXTRA_ACTION_VARS));
+
 			// create arrays/etc. first
 			
 			// nondeterministic variables

prism/src/prism/PrismSettings.java

@@ -92,6 +92,8 @@ public class PrismSettings implements Observer
 	
 	public static final	String PRISM_CUDD_MAX_MEM					= "prism.cuddMaxMem";
 	public static final	String PRISM_CUDD_EPSILON					= "prism.cuddEpsilon";
+	public static final	String PRISM_DD_EXTRA_STATE_VARS				= "prism.ddExtraStateVars";
+	public static final	String PRISM_DD_EXTRA_ACTION_VARS				= "prism.ddExtraActionVars";
 	public static final	String PRISM_NUM_SB_LEVELS					= "prism.numSBLevels";//"prism.hybridNumLevels";
 	public static final	String PRISM_SB_MAX_MEM						= "prism.SBMaxMem";//"prism.hybridMaxMemory";
 	public static final	String PRISM_NUM_SOR_LEVELS					= "prism.numSORLevels";//"prism.hybridSORLevels";
@@ -307,6 +309,12 @@ public class PrismSettings implements Observer
 																			"Maximum memory available to CUDD (underlying BDD/MTBDD library), e.g. 125k, 50m, 4g. Note: Restart PRISM after changing this." },
 			{ DOUBLE_TYPE,		PRISM_CUDD_EPSILON,						"CUDD epsilon",							"2.1",			new Double(1.0E-15),														"0.0,",																						
 																			"Epsilon value used by CUDD (underlying BDD/MTBDD library) for terminal cache comparisons." },
+			{ INTEGER_TYPE,		PRISM_DD_EXTRA_STATE_VARS,				"Extra DD state var allocation",		"4.3.1",			new Integer(20),														"",
+																			"Number of extra DD state variables preallocated for use in model transformation." },
+			{ INTEGER_TYPE,		PRISM_DD_EXTRA_ACTION_VARS,				"Extra DD action var allocation",		"4.3.1",			new Integer(20),														"",
+																			"Number of extra DD action variables preallocated for use in model transformation." },
+
+
 			// ADVERSARIES/COUNTEREXAMPLES:
 			{ CHOICE_TYPE,		PRISM_EXPORT_ADV,						"Adversary export",						"3.3",			"None",																	"None,DTMC,MDP",																
 																			"Type of adversary to generate and export during MDP model checking" },
@@ -1267,6 +1275,32 @@ public class PrismSettings implements Observer
 			} else {
 				throw new PrismException("No value specified for -" + sw + " switch");
 			}
+		} else if (sw.equals("ddextrastatevars")) {
+			if (i < args.length - 1) {
+				try {
+					int v = Integer.parseInt(args[++i]);
+					if (v < 0)
+						throw new NumberFormatException("");
+					set(PRISM_DD_EXTRA_STATE_VARS, v);
+				} catch (NumberFormatException e) {
+					throw new PrismException("Invalid value for -" + sw + " switch");
+				}
+			} else {
+				throw new PrismException("No value specified for -" + sw + " switch");
+			}
+		} else if (sw.equals("ddextraactionvars")) {
+			if (i < args.length - 1) {
+				try {
+					int v = Integer.parseInt(args[++i]);
+					if (v < 0)
+						throw new NumberFormatException("");
+					set(PRISM_DD_EXTRA_ACTION_VARS, v);
+				} catch (NumberFormatException e) {
+					throw new PrismException("Invalid value for -" + sw + " switch");
+				}
+			} else {
+				throw new PrismException("No value specified for -" + sw + " switch");
+			}
 		}
 		
 		// ADVERSARIES/COUNTEREXAMPLES:
@@ -1658,6 +1692,8 @@ public class PrismSettings implements Observer
 		mainLog.println("-cuddmaxmem <n> ................ Set max memory for CUDD package, e.g. 125k, 50m, 4g [default: 1g]");
 		mainLog.println("-cuddepsilon <x> ............... Set epsilon value for CUDD package [default: 1e-15]");
 		mainLog.println("-ddsanity ...................... Enable internal sanity checks (causes slow-down)");
+		mainLog.println("-ddextrastatevars <n> .......... Set the number of preallocated state vars [default: 20]");
+		mainLog.println("-ddextraactionvars <n> ......... Set the number of preallocated action vars [default: 20]");
 		mainLog.println();
 		mainLog.println("PARAMETRIC MODEL CHECKING OPTIONS:");
 		mainLog.println("-param <vals> .................. Do parametric model checking with parameters (and ranges) <vals>");