FAU uses its own "-fauepsilon" setting, not the main "-epsilon" one for iterative numerical methods.

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

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) {

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)) {

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 {