Fast adaptive uniformisation: Fix for incomplete model exploration

During model exploration of a CTMC, when using fast adaptive uniformisation,
only the last part of an update (rate & successor state) is used, as the
indexing of the outgoing transitions is buggy.

We now store all outgoing transitions and handle the case of multiple
choices/enabled commands in the CTMC.

+ two test cases

prism-tests/bugfixes/ctmc-fau-1.sm

@@ -0,0 +1,11 @@
+// test case for fast adaptive uniformisation bug (ignoring transitions)
+
+ctmc
+
+module m1
+  s: [0..2] init 0;
+
+  [] s=0 -> 1:(s'=1) + 2:(s'=2);
+  [] s>0 -> 1:true;
+endmodule
+

prism-tests/bugfixes/ctmc-fau-1.sm.props

@@ -0,0 +1,15 @@
+const double T;
+
+// RESULT (T=1): 0.3167376343237416
+// RESULT (T=2): 0.332507070725914
+// RESULT (T=3): 0.33329218265878835
+// RESULT (T=4): 0.3333312759432579
+// RESULT (T=5): 0.33333321817286715
+P=? [ F=T s=1 ];
+
+// RESULT (T=1): 0.6334752686474832
+// RESULT (T=2): 0.665014141451828
+// RESULT (T=3): 0.6665843653175767
+// RESULT (T=4): 0.6666625518865158
+// RESULT (T=5): 0.6666664363457
+P=? [ F=T s=2 ];

prism-tests/bugfixes/ctmc-fau-1.sm.props.args

@@ -0,0 +1,3 @@
+-const T=1:1:5 -transientmethod unif
+-const T=1:1:5 -transientmethod fau
+

prism-tests/bugfixes/ctmc-fau-2.sm

@@ -0,0 +1,11 @@
+// test correct handling of multiple enabled commands in CTMC when using fast adaptive uniformisation
+
+ctmc
+
+module m1
+  s: [0..4] init 0;
+
+  [a] s=0 -> 1:(s'=1) + 2:(s'=2);
+  [b] s=0 -> 3:(s'=3) + 4:(s'=4);
+  [] s>0 -> 1:true;
+endmodule

prism-tests/bugfixes/ctmc-fau-2.sm.props

@@ -0,0 +1,31 @@
+const double T;
+
+// RESULT (T=0.2): 0.08646646794
+// RESULT (T=0.4): 0.09816843470
+// RESULT (T=0.6): 0.09975212121
+// RESULT (T=0.8): 0.09996644936
+// RESULT (T=1.0): 0.09999545617
+P=? [ F=T s=1 ];
+
+// RESULT (T=0.2): 0.1729329358997
+// RESULT (T=0.4): 0.1963368694095
+// RESULT (T=0.6): 0.1995042424355
+// RESULT (T=0.8): 0.1999328987210
+// RESULT (T=1.0): 0.1999909123404
+P=? [ F=T s=2 ];
+
+
+// RESULT (T=0.2): 0.2593994038496
+// RESULT (T=0.4): 0.2945053041143
+// RESULT (T=0.6): 0.2992563636533
+// RESULT (T=0.8): 0.2998993480815
+// RESULT (T=1.0): 0.2999863685106
+P=? [ F=T s=3 ];
+
+
+// RESULT (T=0.2): 0.3458658717995
+// RESULT (T=0.4): 0.3926737388191
+// RESULT (T=0.6): 0.3990084848710
+// RESULT (T=0.8): 0.3998657974421
+// RESULT (T=1.0): 0.3999818246808
+P=? [ F=T s=4 ];

prism-tests/bugfixes/ctmc-fau-2.sm.props.args

@@ -0,0 +1,3 @@
+-const T=0.2:0.2:1 -transientmethod unif
+-const T=0.2:0.2:1 -transientmethod fau
+

prism/src/explicit/FastAdaptiveUniformisation.java

@@ -1175,24 +1175,29 @@ public final class FastAdaptiveUniformisation extends PrismComponent
 			succRates[0] = 1.0;
 			succStates[0] = states.get(state);
 		} else {
-			int nc = modelGen.getNumChoices();
-			succRates = new double[nc];
-			succStates = new StateProp[nc];
-			for (int i = 0; i < nc; i++) {
-				int nt = modelGen.getNumTransitions(i);
-				for (int j = 0; j < nt; j++) {
-					State succState = modelGen.computeTransitionTarget(i, j);
-					StateProp succProp = states.get(succState);
-					if (null == succProp) {
-						addToModel(succState);
-						modelGen.exploreState(state);
-						succProp = states.get(succState);
+			int ntAll = modelGen.getNumTransitions();
+			if (ntAll > 0) {
+				succRates = new double[ntAll];
+				succStates = new StateProp[ntAll];
+
+				int t = 0;
+				for (int i = 0, nc = modelGen.getNumChoices(); i < nc; i++) {
+					for (int j = 0, ntChoice = modelGen.getNumTransitions(i); j < ntChoice; j++) {
+						State succState = modelGen.computeTransitionTarget(i, j);
+						StateProp succProp = states.get(succState);
+						if (null == succProp) {
+							addToModel(succState);
+							succProp = states.get(succState);
+
+							// re-explore state, as call to addToModel may have explored succState
+							modelGen.exploreState(state);
+						}
+						succRates[t] = modelGen.getTransitionProbability(i, j);
+						succStates[t] = succProp;
+						t++;
 					}
-					succRates[i] = modelGen.getTransitionProbability(i, j);
-					succStates[i] = succProp;
 				}
-			}
-			if (nc == 0) {
+			} else {
 				succRates = new double[1];
 				succStates = new StateProp[1];
 				succRates[0] = 1.0;