diff --git a/prism/src/prism/ModelVariablesDD.java b/prism/src/prism/ModelVariablesDD.java index 50872714..7373503d 100644 --- a/prism/src/prism/ModelVariablesDD.java +++ b/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(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 + * If there is not enough space in the preallocated variable pool, throws an exception. + *
[ REFS: result ] + * @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. + * + *
[ REFs: none, DEREFs: none ] + */ + public JDDVars getExtraActionVariables() { + return extraActionVariables; + } + } diff --git a/prism/src/prism/Modules2MTBDD.java b/prism/src/prism/Modules2MTBDD.java index dafa9b91..b124d272 100644 --- a/prism/src/prism/Modules2MTBDD.java +++ b/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 diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index a3e9f400..8e7c41b8 100644 --- a/prism/src/prism/PrismSettings.java +++ b/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 ................ Set max memory for CUDD package, e.g. 125k, 50m, 4g [default: 1g]"); mainLog.println("-cuddepsilon ............... Set epsilon value for CUDD package [default: 1e-15]"); mainLog.println("-ddsanity ...................... Enable internal sanity checks (causes slow-down)"); + mainLog.println("-ddextrastatevars .......... Set the number of preallocated state vars [default: 20]"); + mainLog.println("-ddextraactionvars ......... Set the number of preallocated action vars [default: 20]"); mainLog.println(); mainLog.println("PARAMETRIC MODEL CHECKING OPTIONS:"); mainLog.println("-param .................. Do parametric model checking with parameters (and ranges) ");