Improve simulation Sampler classes to handle deadlocks (in some cases). Deadlocks still not properly handled by the simulator.

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

prism/src/simulator/sampler/SamplerBoundedUntilCont.java

@@ -135,6 +135,12 @@ public class SamplerBoundedUntilCont extends SamplerBoolean
 						value = true;
 					}
 				}
+				// Or, if we are now at a deadlock
+				else if (transList != null && transList.isDeadlock()) {
+					valueKnown = true;
+					value = false;
+				}
+				// Otherwise, don't know
 			}
 		}
 		

prism/src/simulator/sampler/SamplerBoundedUntilDisc.java

@@ -87,11 +87,16 @@ public class SamplerBoundedUntilDisc extends SamplerBoolean
 				valueKnown = true;
 				value = true;
 			}
-			// Or, if not, have we violated the LJS of the until?
+			// Or, if not, have we violated the LHS of the until?
 			else if (!left.evaluateBoolean(currentState)) {
 				valueKnown = true;
 				value = false;
 			}
+			// Or, if we are now at a deadlock
+			else if (transList != null && transList.isDeadlock()) {
+				valueKnown = true;
+				value = false;
+			}
 			// Otherwise, don't know
 		}
 		

prism/src/simulator/sampler/SamplerRewardCumulCont.java

@@ -79,6 +79,14 @@ public class SamplerRewardCumulCont extends SamplerDouble
 				value -= path.getPreviousTransitionReward(rewardStructIndex);
 			}
 		}
+		// Or, if we are now at a deadlock
+		else if (transList != null && transList.isDeadlock()) {
+			valueKnown = true;
+			value = path.getTotalCumulativeReward(rewardStructIndex);
+			// Compute remaining time, i.e. how long left until time bound will be reached
+			double remainingTime = timeBound - path.getTotalTime();
+			value += path.getCurrentStateReward(rewardStructIndex) * remainingTime;
+		}
 		
 		return valueKnown;
 	}