From 990a9193b348a28f7eeb68dddcc4d3b1db34a929 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Mon, 28 Aug 2017 12:45:47 +0200
Subject: [PATCH] Parametric / exact engine: fix handling of infinite values in
 reward computations

In the state eliminator, i.e., solving for a DTMC, a state that has probability
zero of reaching the target states (i.e., that can not reach the target state)
should get infinite reward.

Previously, the check for this looked at the returned set of collectStatesBackward(),
which always returns the whole state space (used for backward elimination order).

Now, we use the variant of collectStatesBackward() that only returns the states
that can reach the target set.

Additionally, we now compute the set of infinity states for Rmin/Rmax using
prob0a / prob0e, respectively, and ensure that they get value infinity.
---
 prism/src/param/StateEliminator.java |  2 +-
 prism/src/param/ValueComputer.java   | 28 +++++++++++++++++++++++++---
 2 files changed, 26 insertions(+), 4 deletions(-)

diff --git a/prism/src/param/StateEliminator.java b/prism/src/param/StateEliminator.java
index ee8a2e3e..5c786d2e 100644
--- a/prism/src/param/StateEliminator.java
+++ b/prism/src/param/StateEliminator.java
@@ -217,7 +217,7 @@ final class StateEliminator {
 		/* search for states which might never reach a target state and thus
 		 * have to be assigned a reward of infinity. */
 		if (pmc.isUseRewards()) {
-			int[] backStatesArr = collectStatesBackward();
+			int[] backStatesArr = collectStatesBackward(true);
 			HashSet<Integer> reaching = new HashSet<Integer>();
 			for (int stateNr = 0; stateNr < backStatesArr.length; stateNr++) {
 				reaching.add(backStatesArr[stateNr]);
diff --git a/prism/src/param/ValueComputer.java b/prism/src/param/ValueComputer.java
index 428df1b3..0962c4d6 100644
--- a/prism/src/param/ValueComputer.java
+++ b/prism/src/param/ValueComputer.java
@@ -32,7 +32,9 @@ import java.util.HashMap;
 import java.util.HashSet;
 import java.util.Map.Entry;
 
+import common.IterableStateSet;
 import prism.PrismComponent;
+import prism.PrismException;
 
 
 /**
@@ -246,7 +248,7 @@ final class ValueComputer extends PrismComponent
 		this.bisimType = bisimType;
 	}
 
-	RegionValues computeUnbounded(RegionValues b1, RegionValues b2, boolean min, ParamRewardStruct rew) {
+	RegionValues computeUnbounded(RegionValues b1, RegionValues b2, boolean min, ParamRewardStruct rew) throws PrismException {
 		RegionValues result = new RegionValues(regionFactory);
 		RegionValuesIntersections co = new RegionValuesIntersections(b1, b2);
 		for (RegionIntersection inter : co) {
@@ -259,13 +261,28 @@ final class ValueComputer extends PrismComponent
 		return result;
 	}
 
-	private RegionValues computeUnbounded(Region region, StateValues b1, StateValues b2, boolean min, ParamRewardStruct rew)
+	private RegionValues computeUnbounded(Region region, StateValues b1, StateValues b2, boolean min, ParamRewardStruct rew) throws PrismException
 	{
 		BigRational requiredVolume = region.volume().multiply(BigRational.ONE.subtract(precision));		
 		RegionValues result = new RegionValues(regionFactory);
 		RegionsTODO todo = new RegionsTODO();
 		todo.add(region);
 		BigRational volume = BigRational.ZERO;
+
+		if (rew != null) {
+			// determine infinity states
+			explicit.MDPModelChecker mcExplicit = new explicit.MDPModelChecker(this);
+			mcExplicit.setSilentPrecomputations(true);
+			BitSet inf = mcExplicit.prob1(model, b1.toBitSet(), b2.toBitSet(), !min, null);
+			inf.flip(0, model.getNumStates());
+
+			for (int i : new IterableStateSet(inf, model.getNumStates())) {
+				// clear states with infinite value from b1 so they will get Infinity value
+				// in the DTMC
+				b1.setStateValue(i, false);
+			}
+		}
+
 		while (volume.compareTo(requiredVolume) == -1) {
 			Region currentRegion = todo.poll();
 			Point midPoint = ((BoxRegion)currentRegion).getMidPoint();
@@ -521,7 +538,12 @@ final class ValueComputer extends PrismComponent
 			if (isSink) {
 				pmc.addTransition(state, state, functionFactory.getOne());
 				if (null != rew) {
-					pmc.setReward(state, functionFactory.getZero());
+					if (isTarget) {
+						pmc.setReward(state, functionFactory.getZero());
+					} else {
+						// !b1 & !b2 state -> infinite (can not reach b2 via b1 states)
+						pmc.setReward(state, functionFactory.getInf());
+					}
 				}
 			} else {
 				if (rew != null) {