Topological interval iteration: Fix bug preventing convergence in some cases

When using an iteration method with two alternating solution vectors (power, jacobi),
we did not copy the result to the second vector when we have detected convergence in
an SCC (for topological interval iteration). Subsequently, as the values for finished
SCCs will never be updated anymore, the values for this states will oscillate between
the final value and the value from the iteration step before, potentially preventing
convergence. This will be mitigated if we enfore convergence from below / above, but
at least from below enforcing convergence should not be necessary.

An example would be

prism prism-examples/dice/two_dice.nm -pf 'Rmin=?[ F s1=7]' -explicit -topological -ii:nomonotonicbelow

where oscillation between 0 and 1 inhibits convergence.

To fix, we tell the iteration method when we are done with an SCC so that we can
copy the results. For singleton SCCs, we already copied the results to both vectors.


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

prism/src/explicit/IterationMethod.java

@@ -57,6 +57,16 @@ public abstract class IterationMethod {
 		/** Perform one iteration (over the set of states) and return true if convergence has been detected. */
 		public boolean iterateAndCheckConvergence(IntSet states) throws PrismException;
 
+		/**
+		 * Notify that the given states are done (e.g., because the given SCC is finished
+		 * during a topological iteration).
+		 * <br>
+		 * This allows the two-vector iteration methods to store the current values for these
+		 * states into the second vector, so that switching the vector does not return to
+		 * previous values.
+		 */
+		public void doneWith(IntSet states);
+
 		/**
 		 * Solve for a given singleton SCC consisting of {@code state} using {@code solver},
 		 * store the result in the solution vector(s).
@@ -81,6 +91,16 @@ public abstract class IterationMethod {
 		/** Perform one iteration (over the set of states) */
 		public void iterate(IntSet states) throws PrismException;
 
+		/**
+		 * Notify that the given states are done (e.g., because the given SCC is finished
+		 * during a topological iteration).
+		 * <br>
+		 * This allows the two-vector iteration methods to store the current values for these
+		 * states into the second vector, so that switching the vector does not return to
+		 * previous values.
+		 */
+		public void doneWith(IntSet states);
+
 		/**
 		 * Solve for a given singleton SCC consisting of {@code state} using {@code solver},
 		 * store the result in the solution vector(s).
@@ -111,11 +131,18 @@ public abstract class IterationMethod {
 			return soln;
 		}
 
+		/* see IterationValIter.solveSingletonSCC() */
 		public void solveSingletonSCC(int state, SingletonSCCSolver solver)
 		{
 			solver.solveFor(state, soln);
 		}
 
+		/* see IterationValIter.doneWith() */
+		public void doneWith(IntSet states)
+		{
+			// single vector, nothing to do
+		}
+
 		public Model getModel()
 		{
 			return model;
@@ -222,6 +249,19 @@ public abstract class IterationMethod {
 			return done;
 		}
 
+		@Override
+		public void doneWith(IntSet states)
+		{
+			// we copy the values for the given states to the
+			// second vector, so that switching between vectors
+			// does not change their values
+			PrimitiveIterator.OfInt it = states.iterator();
+			while (it.hasNext()) {
+				int state = it.nextInt();
+				soln2[state] = soln[state];
+			}
+		}
+
 		@Override
 		public void solveSingletonSCC(int state, SingletonSCCSolver solver)
 		{
@@ -444,6 +484,9 @@ public abstract class IterationMethod {
 				int state = sccs.getStatesForSCC(scc).iterator().nextInt();
 				iterator.solveSingletonSCC(state, singletonSCCSolver);
 
+				// no need to call doneWith(...), as solveSingletonSCC updates
+				// both vectors for two-iteration methods
+
 				mvCount += countTransitions(iterator.getModel(), IntSet.asIntSet(state));
 
 				iters++;
@@ -474,6 +517,11 @@ public abstract class IterationMethod {
 
 				}
 
+				// notify the iterator that the states are done so that
+				// their values can be copied to the second vector in a two-vector
+				// iterator
+				iterator.doneWith(statesForSCC);
+
 				mvCount += itersInSCC * countTransitions(iterator.getModel(), statesForSCC);
 			}
 
@@ -637,6 +685,9 @@ public abstract class IterationMethod {
 					below.solveSingletonSCC(state, singletonSCCSolver);
 					above.solveSingletonSCC(state, singletonSCCSolver);
 
+					// no need to call doneWith(...), as solveSingletonSCC updates
+					// both vectors for two-iteration methods
+
 					iters++;
 					mvCount += 2 * countTransitions(below.getModel(), IntSet.asIntSet(state));
 
@@ -692,6 +743,12 @@ public abstract class IterationMethod {
 						}
 					}
 
+					// notify the iterators that the states are done so that
+					// their values can be copied to the second vector in a two-vector
+					// iterator
+					below.doneWith(statesForSCC);
+					above.doneWith(statesForSCC);
+
 					mvCount += 2 * itersInSCC * countTransitions(below.getModel(), statesForSCC);
 					finishedNonSingletonSCCs++;
 				}