diff --git a/prism/src/explicit/BirthProcess.java b/prism/src/explicit/BirthProcess.java index fc7bc648..c8170881 100644 --- a/prism/src/explicit/BirthProcess.java +++ b/prism/src/explicit/BirthProcess.java @@ -44,7 +44,7 @@ public class BirthProcess * Must be at least as large as largest rate. */ double unifRate; /* precision of computations using Fox-Glynn algorithm */ - double termCritParam; + double epsilon; /* time to compute probabilities for */ double time; /* values used to compute probability to be in a given stage */ @@ -68,7 +68,7 @@ public class BirthProcess public BirthProcess() { stageNr = 0; - termCritParam = 1E-7; + epsilon = 1E-7; withRateArray = true; initialising = true; avoidBirthComputation = true; @@ -108,15 +108,15 @@ public class BirthProcess /** * Sets precision to be used to compute probabilities. * - * @param termCritParam precision to be used to compute probabilities + * @param epsilon precision to be used to compute probabilities */ - public void setTermCritParam(double termCritParam) + public void setEpsilon(double epsilon) { if (!initialising) { throw new IllegalArgumentException("this method might not be called after calculateNextRate"); } - this.termCritParam = termCritParam; + this.epsilon = epsilon; } /** @@ -233,7 +233,7 @@ public class BirthProcess { long left, right; double qt = unifRate * time; - double acc = termCritParam / 8.0; + double acc = epsilon / 8.0; double[] weights; double totalWeight; if (unifRate * time == 0.0) { diff --git a/prism/src/explicit/FastAdaptiveUniformisation.java b/prism/src/explicit/FastAdaptiveUniformisation.java index 771cdb7c..051f7518 100644 --- a/prism/src/explicit/FastAdaptiveUniformisation.java +++ b/prism/src/explicit/FastAdaptiveUniformisation.java @@ -408,7 +408,7 @@ public class FastAdaptiveUniformisation extends PrismComponent /** model exploration component to generate new states */ private ModelExplorer modelExplorer; /** probability allowed to drop birth process */ - private double termCritParam; + private double epsilon; /** probability threshold when to drop states in discrete-time process */ private double delta; /** number of intervals to divide time into */ @@ -466,7 +466,7 @@ public class FastAdaptiveUniformisation extends PrismComponent this.modelExplorer = modelExplorer; maxNumStates = 0; - termCritParam = settings.getDouble(PrismSettings.PRISM_TERM_CRIT_PARAM); + epsilon = settings.getDouble(PrismSettings.PRISM_FAU_EPSILON); delta = settings.getDouble(PrismSettings.PRISM_FAU_DELTA); numIntervals = settings.getInteger(PrismSettings.PRISM_FAU_INTERVALS); arrayThreshold = settings.getInteger(PrismSettings.PRISM_FAU_ARRAYTHRESHOLD); @@ -740,14 +740,14 @@ public class FastAdaptiveUniformisation extends PrismComponent { birthProc = new BirthProcess(); birthProc.setTime(interval); - birthProc.setTermCritParam(termCritParam); + birthProc.setEpsilon(epsilon); int iters = 0; birthProbSum = 0.0; itersUnchanged = 0; keepSumProb = false; - while (birthProbSum < (1 - termCritParam)) { - if (birthProbSum >= termCritParam/2) { + while (birthProbSum < (1 - epsilon)) { + if (birthProbSum >= epsilon/2) { keepSumProb = true; } if ((itersUnchanged == arrayThreshold)) { diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index 9875e6f3..0a530e05 100644 --- a/prism/src/prism/PrismSettings.java +++ b/prism/src/prism/PrismSettings.java @@ -119,6 +119,7 @@ public class PrismSettings implements Observer public static final String PRISM_PARAM_SUBSUME_REGIONS = "prism.param.subsumeRegions"; public static final String PRISM_PARAM_DAG_MAX_ERROR = "prism.param.functionDagMaxError"; + public static final String PRISM_FAU_EPSILON = "prism.fau.epsilon"; public static final String PRISM_FAU_DELTA = "prism.fau.delta"; public static final String PRISM_FAU_INTERVALS = "prism.fau.intervals"; public static final String PRISM_FAU_INITIVAL = "prism.fau.initival"; @@ -313,9 +314,11 @@ public class PrismSettings implements Observer "Maximal error probability (i.e. maximum probability of of a wrong result) in DAG function representation used for parametric model checking." }, // FAST ADAPTIVE UNIFORMISATION + { DOUBLE_TYPE, PRISM_FAU_EPSILON, "FAU epsilon", "4.1", new Double(1E-6), "", + "For fast adaptive uniformisation (FAU), states whose probability is below this value will be removed." }, { DOUBLE_TYPE, PRISM_FAU_DELTA, "FAU cut off delta", "4.1", new Double(1E-12), "", "For fast adaptive uniformisation (FAU), states whose probability is below this value will be removed." }, - { INTEGER_TYPE, PRISM_FAU_ARRAYTHRESHOLD, "FAU array threshold", "4.1", new Integer(100), "", + { INTEGER_TYPE, PRISM_FAU_ARRAYTHRESHOLD, "FAU array threshold", "4.1", new Integer(100), "", "For fast adaptive uniformisation (FAU), after this number of iterations without changes to the state space, storage is switched to a faster, fixed-size data structure." }, { INTEGER_TYPE, PRISM_FAU_INTERVALS, "FAU time intervals", "4.1", new Integer(1), "", "For fast adaptive uniformisation (FAU), the time period is split into this number of of intervals." }, @@ -1303,6 +1306,21 @@ public class PrismSettings implements Observer // FAST ADAPTIVE UNIFORMISATION + // Epsilon for fast adaptive uniformisation + else if (sw.equals("fauepsilon")) { + if (i < args.length - 1) { + try { + d = Double.parseDouble(args[++i]); + if (d < 0) + throw new NumberFormatException(""); + set(PRISM_FAU_EPSILON, d); + } catch (NumberFormatException e) { + throw new PrismException("Invalid value for -" + sw + " switch"); + } + } else { + throw new PrismException("No value specified for -" + sw + " switch"); + } + } // Delta for fast adaptive uniformisation else if (sw.equals("faudelta")) { if (i < args.length - 1) { @@ -1318,6 +1336,7 @@ public class PrismSettings implements Observer throw new PrismException("No value specified for -" + sw + " switch"); } } + // Array threshold for fast adaptive uniformisation else if (sw.equals("fauarraythreshold")) { if (i < args.length - 1) { try {