Tweaks to Sampler design + non-compilation bugfix.

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

prism/src/simulator/ChoiceList.java

@@ -92,6 +92,16 @@ public class ChoiceList implements Choice
 	
 	// Get methods
 	
+	public int getModuleOrActionIndex()
+	{
+		return 0; // TODO
+	}
+
+	public String getModuleOrAction()
+	{
+		return null; // TODO
+	}
+
 	public String getAction()
 	{
 		return action;

prism/src/simulator/ChoiceSingleton.java

@@ -65,6 +65,16 @@ public class ChoiceSingleton implements Choice
 
 	// Get methods
 	
+	public int getModuleOrActionIndex()
+	{
+		return 0; // TODO
+	}
+
+	public String getModuleOrAction()
+	{
+		return null; // TODO
+	}
+
 	public int size()
 	{
 		return 1;

prism/src/simulator/SimulatorEngine.java

@@ -863,7 +863,6 @@ public class SimulatorEngine
 	private void updateSamplers() throws PrismLangException
 	{
 		for (Sampler sampler : propertySamplers) {
-			if (!sampler.isCurrentValueKnown())
 			sampler.update(path);
 		}
 	}
@@ -881,7 +880,6 @@ public class SimulatorEngine
 		for (i = 0; i <= n; i++) {
 			prefix.setPrefixLength(i);
 			for (Sampler sampler : propertySamplers) {
-				if (!sampler.isCurrentValueKnown())
 				sampler.update(prefix);
 			}
 		}

prism/src/simulator/sampler/Sampler.java

@@ -59,9 +59,9 @@ public abstract class Sampler
 	/**
 	 * Update the current value of the sampler based on the current simulation path.
 	 * It is assumed that this is called at every step of the path.
-	 * It is also assumed that this is not called after the value becomes known. 
+	 * This returns true if the sampler's value becomes (or is already) known.
 	 */
-	public abstract void update(Path path) throws PrismLangException;
+	public abstract boolean update(Path path) throws PrismLangException;
 
 	/**
 	 * Update the statistics for the sampler, assuming that the current path is finished.

prism/src/simulator/sampler/SamplerBoolean.java

@@ -57,7 +57,7 @@ public abstract class SamplerBoolean extends Sampler
 	}
 
 	@Override
-	public abstract void update(Path path) throws PrismLangException;
+	public abstract boolean update(Path path) throws PrismLangException;
 
 	@Override
 	public void updateStats()

prism/src/simulator/sampler/SamplerBoundedUntilCont.java

@@ -63,8 +63,12 @@ public class SamplerBoundedUntilCont extends SamplerBoolean
 	}
 
 	@Override
-	public void update(Path path) throws PrismLangException
+	public boolean update(Path path) throws PrismLangException
 	{
+		// If the answer is already known we should do nothing
+		if (valueKnown)
+			return true;
+		
 		// For continuous-time bounded until, we may need to look back at previous state.
 		// So, treat first/subsequent calls to update() differently. 
 
@@ -133,5 +137,7 @@ public class SamplerBoundedUntilCont extends SamplerBoolean
 				}
 			}
 		}
+		
+		return valueKnown;
 	}
 }

prism/src/simulator/sampler/SamplerBoundedUntilDisc.java

@@ -59,8 +59,12 @@ public class SamplerBoundedUntilDisc extends SamplerBoolean
 	}
 
 	@Override
-	public void update(Path path) throws PrismLangException
+	public boolean update(Path path) throws PrismLangException
 	{
+		// If the answer is already known we should do nothing
+		if (valueKnown)
+			return true;
+		
 		int pathSize = path.size();
 		// Upper bound exceeded
 		if (pathSize > ub) {
@@ -90,5 +94,7 @@ public class SamplerBoundedUntilDisc extends SamplerBoolean
 			}
 			// Otherwise, don't know
 		}
+		
+		return valueKnown;
 	}
 }

prism/src/simulator/sampler/SamplerDouble.java

@@ -55,7 +55,7 @@ public abstract class SamplerDouble extends Sampler
 	}
 
 	@Override
-	public abstract void update(Path path) throws PrismLangException;
+	public abstract boolean update(Path path) throws PrismLangException;
 
 	@Override
 	public void updateStats()

prism/src/simulator/sampler/SamplerNext.java

@@ -52,8 +52,12 @@ public class SamplerNext extends SamplerBoolean
 	}
 
 	@Override
-	public void update(Path path) throws PrismLangException
+	public boolean update(Path path) throws PrismLangException
 	{
+		// If the answer is already known we should do nothing
+		if (valueKnown)
+			return true;
+		
 		// X "target" is true iff state 1 satisfies "target"
 		if (path.size() == 1) {
 			valueKnown = true;
@@ -61,5 +65,7 @@ public class SamplerNext extends SamplerBoolean
 		}
 		// Nothing else to do: if path size is 0, can't decide;
 		// if path size > 1 (should never happen), nothing changes
+		
+		return valueKnown;
 	}
 }

prism/src/simulator/sampler/SamplerRewardCumulCont.java

@@ -55,8 +55,12 @@ public class SamplerRewardCumulCont extends SamplerDouble
 	}
 
 	@Override
-	public void update(Path path) throws PrismLangException
+	public boolean update(Path path) throws PrismLangException
 	{
+		// If the answer is already known we should do nothing
+		if (valueKnown)
+			return true;
+		
 		// As soon as time bound exceeded, compute reward total
 		if (path.getTotalTime() >= timeBound) {
 			valueKnown = true;
@@ -75,5 +79,7 @@ public class SamplerRewardCumulCont extends SamplerDouble
 				value -= path.getPreviousTransitionReward(rewardStructIndex);
 			}
 		}
+		
+		return valueKnown;
 	}
 }

prism/src/simulator/sampler/SamplerRewardCumulDisc.java

@@ -55,12 +55,18 @@ public class SamplerRewardCumulDisc extends SamplerDouble
 	}
 
 	@Override
-	public void update(Path path) throws PrismLangException
+	public boolean update(Path path) throws PrismLangException
 	{
+		// If the answer is already known we should do nothing
+		if (valueKnown)
+			return true;
+		
 		// As soon as time bound reached, store current reward total
 		if (path.size() == timeBound) {
 			valueKnown = true;
 			value = path.getTotalCumulativeReward(rewardStructIndex);
 		}
+		
+		return valueKnown;
 	}
 }

prism/src/simulator/sampler/SamplerRewardInstCont.java

@@ -55,8 +55,12 @@ public class SamplerRewardInstCont extends SamplerDouble
 	}
 
 	@Override
-	public void update(Path path) throws PrismLangException
+	public boolean update(Path path) throws PrismLangException
 	{
+		// If the answer is already known we should do nothing
+		if (valueKnown)
+			return true;
+		
 		// As soon as time bound exceeded, compute reward
 		if (path.getTotalTime() >= time) {
 			valueKnown = true;
@@ -70,5 +74,7 @@ public class SamplerRewardInstCont extends SamplerDouble
 				value = path.getCurrentStateReward(rewardStructIndex);
 			}
 		}
+		
+		return valueKnown;
 	}
 }

prism/src/simulator/sampler/SamplerRewardInstDisc.java

@@ -55,12 +55,18 @@ public class SamplerRewardInstDisc extends SamplerDouble
 	}
 
 	@Override
-	public void update(Path path) throws PrismLangException
+	public boolean update(Path path) throws PrismLangException
 	{
+		// If the answer is already known we should do nothing
+		if (valueKnown)
+			return true;
+		
 		// As soon as time bound reached, store current state reward
 		if (path.size() == time) {
 			valueKnown = true;
 			value = path.getCurrentStateReward(rewardStructIndex);
 		}
+		
+		return valueKnown;
 	}
 }

prism/src/simulator/sampler/SamplerRewardReach.java

@@ -43,6 +43,10 @@ public class SamplerRewardReach extends SamplerDouble
 	 */
 	public SamplerRewardReach(ExpressionTemporal expr, int rewardStructIndex) throws PrismException
 	{
+		// If the answer is already known we should do nothing
+		if (valueKnown)
+			return;
+		
 		// Make sure expression is of the correct type
 		// Then extract other required info
 		if (expr.getOperator() != ExpressionTemporal.R_F)
@@ -55,11 +59,17 @@ public class SamplerRewardReach extends SamplerDouble
 	}
 
 	@Override
-	public void update(Path path) throws PrismLangException
+	public boolean update(Path path) throws PrismLangException
 	{
+		// If the answer is already known we should do nothing
+		if (valueKnown)
+			return true;
+		
 		if (target.evaluateBoolean(path.getCurrentState())) {
 			valueKnown = true;
 			value = path.getTotalCumulativeReward(rewardStructIndex);
 		}
+		
+		return valueKnown;
 	}
 }

prism/src/simulator/sampler/SamplerUntil.java

@@ -57,8 +57,12 @@ public class SamplerUntil extends SamplerBoolean
 	}
 
 	@Override
-	public void update(Path path) throws PrismLangException
+	public boolean update(Path path) throws PrismLangException
 	{
+		// If the answer is already known we should do nothing
+		if (valueKnown)
+			return true;
+		
 		State currentState = path.getCurrentState();
 		// Have we reached the target (i.e. RHS of until)?
 		if (right.evaluateBoolean(currentState)) {
@@ -71,5 +75,7 @@ public class SamplerUntil extends SamplerBoolean
 			value = false;
 		}
 		// Otherwise, don't know
+		
+		return valueKnown;
 	}
 }