Approximate model checking ignores "max path length" setting when verifying time-bounded properties.

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

prism/src/simulator/SimulatorEngine.java

@@ -29,6 +29,8 @@ package simulator;
 import java.util.*;
 import java.io.*;
 
+import javax.swing.plaf.basic.BasicInternalFrameTitlePane.MaximizeAction;
+
 import simulator.method.*;
 import simulator.sampler.*;
 import parser.*;
@@ -1481,6 +1483,7 @@ public class SimulatorEngine
 		boolean deadlocksFound = false;
 		boolean allDone = false;
 		boolean allKnown = false;
+		boolean someUnknownButBounded = false;
 		boolean shouldStopSampling = false;
 		// Path stats
 		double avgPathLength = 0;
@@ -1526,18 +1529,28 @@ public class SimulatorEngine
 			// Start the new path for this iteration (sample)
 			initialisePath(initialState);
 
-			// Generate a path, up to at most maxPathLength steps
-			for (i = 0; i < maxPathLength; i++) {
-				// See if all samplers have established a value; if so, stop.
+			// Generate a path
+			allKnown = false;
+			someUnknownButBounded = false;
+			i = 0;
+			while ((!allKnown && i < maxPathLength) || someUnknownButBounded) {
+				// Check status of samplers
 				allKnown = true;
+				someUnknownButBounded = false;
 				for (Sampler sampler : propertySamplers) {
-					if (!sampler.isCurrentValueKnown())
+					if (!sampler.isCurrentValueKnown()) {
 						allKnown = false;
+						if (sampler.needsBoundedNumSteps())
+							someUnknownButBounded = true;
+					}
 				}
-				if (allKnown)
+				// Stop when all answers are known or we have reached max path length
+				// (but don't stop yet if there are "bounded" samplers with unkown values)
+				if ((allKnown || i >= maxPathLength) && !someUnknownButBounded)
 					break;
 				// Make a random transition
 				automaticTransition();
+				i++;
 			}
 
 			// TODO: Detect deadlocks so we can report a warning

prism/src/simulator/sampler/Sampler.java

@@ -52,6 +52,17 @@ public abstract class Sampler
 		return valueKnown;
 	}
 
+	/**
+	 * Does this sampler only require a bounded number of path steps?
+	 * i.e. is it safe to keep sampling beyond the maximum path length
+	 * even if this sampler does not know its value yet?
+	 * Conservatively, we assume "no"; override if required. 
+	 */
+	public boolean needsBoundedNumSteps()
+	{
+		return false;
+	}
+
 	/**
 	 * Reset the current value of the sampler and whether it is known or not.
 	 */

prism/src/simulator/sampler/SamplerBoundedUntilCont.java

@@ -140,4 +140,11 @@ public class SamplerBoundedUntilCont extends SamplerBoolean
 		
 		return valueKnown;
 	}
+	
+	@Override
+	public boolean needsBoundedNumSteps()
+	{
+		// Always bounded (although we don't know the exact num steps, just the time bound)
+		return true;
+	}
 }

prism/src/simulator/sampler/SamplerBoundedUntilDisc.java

@@ -97,4 +97,11 @@ public class SamplerBoundedUntilDisc extends SamplerBoolean
 		
 		return valueKnown;
 	}
+	
+	@Override
+	public boolean needsBoundedNumSteps()
+	{
+		// Always bounded
+		return true;
+	}
 }

prism/src/simulator/sampler/SamplerNext.java

@@ -68,4 +68,11 @@ public class SamplerNext extends SamplerBoolean
 		
 		return valueKnown;
 	}
+	
+	@Override
+	public boolean needsBoundedNumSteps()
+	{
+		// Always bounded
+		return true;
+	}
 }

prism/src/simulator/sampler/SamplerRewardCumulCont.java

@@ -81,4 +81,11 @@ public class SamplerRewardCumulCont extends SamplerDouble
 		
 		return valueKnown;
 	}
+	
+	@Override
+	public boolean needsBoundedNumSteps()
+	{
+		// Always bounded (although we don't know the exact num steps, just the time bound)
+		return true;
+	}
 }

prism/src/simulator/sampler/SamplerRewardCumulDisc.java

@@ -69,4 +69,11 @@ public class SamplerRewardCumulDisc extends SamplerDouble
 		
 		return valueKnown;
 	}
+	
+	@Override
+	public boolean needsBoundedNumSteps()
+	{
+		// Always bounded
+		return true;
+	}
 }

prism/src/simulator/sampler/SamplerRewardInstCont.java

@@ -77,4 +77,11 @@ public class SamplerRewardInstCont extends SamplerDouble
 		
 		return valueKnown;
 	}
+	
+	@Override
+	public boolean needsBoundedNumSteps()
+	{
+		// Always bounded (although we don't know the exact num steps, just the time bound)
+		return true;
+	}
 }

prism/src/simulator/sampler/SamplerRewardInstDisc.java

@@ -69,4 +69,11 @@ public class SamplerRewardInstDisc extends SamplerDouble
 		
 		return valueKnown;
 	}
+	
+	@Override
+	public boolean needsBoundedNumSteps()
+	{
+		// Always bounded
+		return true;
+	}
 }