Simulator updates: fixed display of transitions in GUI, added (some) detection of deadlocks/self-loops. (And some tidying.)

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

prism/src/parser/ast/Update.java

@@ -192,8 +192,9 @@ public class Update extends ASTElement
 	}
 
 	/**
-	 * Execute this update, based on variable values specified as a State object,
-	 * applying changes in variables to a second State object. 
+	 * Execute this update, based on variable values specified as a State object.
+	 * Apply changes in variables to a provided copy of the State object.
+	 * (i.e. oldState and newState should be equal when passed in.) 
 	 * It is assumed that any constants have already been defined.
 	 * @param oldState: Variable values in current state
 	 * @param newState: State object to apply changes to
@@ -208,8 +209,9 @@ public class Update extends ASTElement
 	}
 
 	/**
-	 * Execute this update, based on variable values specified as a State object,
-	 * applying changes in variables to a second State object.
+	 * Execute this update, based on variable values specified as a State object.
+	 * Apply changes in variables to a provided copy of the State object.
+	 * (i.e. oldState and newState should be equal when passed in.) 
 	 * Both State objects represent only a subset of the total set of variables,
 	 * with this subset being defined by the mapping varMap.
 	 * Only variables in this subset are updated.

prism/src/simulator/Choice.java

@@ -38,10 +38,11 @@ public interface Choice
 	public double getProbability();
 	public double getProbability(int i);
 	public double getProbabilitySum();
-	public String getUpdateString(int i);
-	public State computeTarget(State oldState) throws PrismLangException;
-	public void computeTarget(State oldState, State newState) throws PrismLangException;
-	public State computeTarget(int i, State oldState) throws PrismLangException;
-	public void computeTarget(int i, State oldState, State newState) throws PrismLangException;
+	public String getUpdateString(int i, State currentState) throws PrismLangException;
+	public String getUpdateStringFull(int i);
+	public State computeTarget(State currentState) throws PrismLangException;
+	public void computeTarget(State currentState, State newState) throws PrismLangException;
+	public State computeTarget(int i, State currentState) throws PrismLangException;
+	public void computeTarget(int i, State currentState, State newState) throws PrismLangException;
 	public int getIndexByProbabilitySum(double x);
 }

prism/src/simulator/ChoiceList.java

@@ -112,7 +112,7 @@ public class ChoiceList implements Choice
 		return probability.size();
 	}
 	
-	public String getUpdateString(int i)
+	public String getUpdateString(int i, State currentState) throws PrismLangException
 	{
 		String s = "(";
 		for (Update up : updates.get(i))
@@ -121,6 +121,11 @@ public class ChoiceList implements Choice
 		return s;
 	}
 	
+	public String getUpdateStringFull(int i)
+	{
+		return null;
+	}
+	
 	public State computeTarget(State oldState) throws PrismLangException
 	{
 		return computeTarget(0, oldState);

prism/src/simulator/ChoiceListFlexi.java

@@ -39,12 +39,13 @@ public class ChoiceListFlexi implements Choice
 	// where i is the 1-indexed module index.
 	// For a synchronous choice, this is the 1-indexed action index.
 	protected int moduleOrActionIndex;
-	
-	// List of multiple targets and associated info
+
+	// List of multiple updates and associated probabilities/rates
 	// Size of list is stored implicitly in target.length
+	// Probabilities/rates are already evaluated, target states are not
+	// but are just stored as lists of updates (for efficiency)
 	protected List<List<Update>> updates;
 	protected List<Double> probability;
-	protected List<Command> command;
 
 	/**
 	 * Create empty choice.
@@ -53,7 +54,6 @@ public class ChoiceListFlexi implements Choice
 	{
 		updates = new ArrayList<List<Update>>();
 		probability = new ArrayList<Double>();
-		command = new ArrayList<Command>();
 	}
 
 	// Set methods
@@ -67,18 +67,16 @@ public class ChoiceListFlexi implements Choice
 	{
 		this.moduleOrActionIndex = moduleOrActionIndex;
 	}
-	
+
 	/**
 	 * Add a transition to this choice.
 	 * @param probability Probability (or rate) of the transition
 	 * @param ups List of Update objects defining transition
-	 * @param command Corresponding Command object
 	 */
-	public void add(double probability, List<Update> ups, Command command)
+	public void add(double probability, List<Update> ups)
 	{
 		this.updates.add(ups);
 		this.probability.add(probability);
-		this.command.add(command);
 	}
 
 	/**
@@ -101,7 +99,7 @@ public class ChoiceListFlexi implements Choice
 		List<Update> list;
 		int i, j, n, n2;
 		double pi;
-		
+
 		n = ch.size();
 		n2 = size();
 		// Loop through each (ith) element of new choice (skipping first)
@@ -117,7 +115,7 @@ public class ChoiceListFlexi implements Choice
 				for (Update u : ch.updates.get(i)) {
 					list.add(u);
 				}
-				add(pi * getProbability(j), list, null);
+				add(pi * getProbability(j), list);
 			}
 		}
 		// Modify elements of current choice to get (0,j) elements of product
@@ -148,6 +146,7 @@ public class ChoiceListFlexi implements Choice
 	 */
 	public String getModuleOrAction()
 	{
+		// Action label (or absence of) will be the same for all updates in a choice
 		Update u = updates.get(0).get(0);
 		Command c = u.getParent().getParent();
 		if ("".equals(c.getSynch()))
@@ -166,57 +165,92 @@ public class ChoiceListFlexi implements Choice
 
 	/**
 	 * Get the updates of the ith transition, as a string.
+	 * This is in abbreviated form, i.e. x'=1, rather than x'=x+1.
+	 * Format is: x'=1, y'=0, with empty string for empty update.
+	 * Only variables updated are included in list (even if unchanged).
+	 */
+	public String getUpdateString(int i, State currentState) throws PrismLangException
+	{
+		int j, n;
+		String s = "";
+		boolean first = true;
+		for (Update up : updates.get(i)) {
+			n = up.getNumElements();
+			for (j = 0; j < n; j++) {
+				if (first)
+					first = false;
+				else
+					s += ", ";
+				s += up.getVar(j) + "'=" + up.getExpression(j).evaluate(currentState);
+			}
+		}
+		return s;
+	}
+
+	/**
+	 * Get the updates of the ith transition, as a string.
+	 * This is in full, i.e. of the form x'=x+1, rather than x'=1.
+	 * Format is: (x'=x+1) & (y'=y-1), with empty string for empty update.
+	 * Only variables updated are included in list.
+	 * Note that expressions may have been simplified from original model. 
 	 */
-	public String getUpdateString(int i)
+	public String getUpdateStringFull(int i)
 	{
 		String s = "";
 		boolean first = true;
 		for (Update up : updates.get(i)) {
-			if (first) first = false; else s+= " & ";
+			if (up.getNumElements() == 0)
+				continue;
+			if (first)
+				first = false;
+			else
+				s += " & ";
 			s += up;
 		}
 		return s;
 	}
-	
+
 	/**
-	 * Compute the target for the ith transition, based on a current state.
+	 * Compute the target for the ith transition, based on a current state,
+	 * returning the result as a new State object copied from the existing one.
+	 * NB: for efficiency, there are no bounds checks done on i.
 	 */
-	public State computeTarget(int i, State oldState) throws PrismLangException
+	public State computeTarget(int i, State currentState) throws PrismLangException
 	{
-		if (i < 0 || i >= size())
-			throw new PrismLangException("Choice does not have an element " + i);
-		State newState = new State(oldState);
+		State newState = new State(currentState);
 		for (Update up : updates.get(i))
-			up.update(oldState, newState);
+			up.update(currentState, newState);
 		return newState;
 	}
 
 	/**
-	 * Compute the target for the ith transition, based on a current state, store in a State.
+	 * Compute the target for the ith transition, based on a current state.
+	 * Apply changes in variables to a provided copy of the State object.
+	 * (i.e. currentState and newState should be equal when passed in.) 
+	 * NB: for efficiency, there are no bounds checks done on i.
 	 */
-	public void computeTarget(int i, State oldState, State newState) throws PrismLangException
+	public void computeTarget(int i, State currentState, State newState) throws PrismLangException
 	{
-		if (i < 0 || i >= size())
-			throw new PrismLangException("Choice does not have an element " + i);
 		for (Update up : updates.get(i))
-			up.update(oldState, newState);
+			up.update(currentState, newState);
 	}
-	
-	public State computeTarget(State oldState) throws PrismLangException
+
+	public State computeTarget(State currentState) throws PrismLangException
 	{
-		return computeTarget(0, oldState);
+		return computeTarget(0, currentState);
 	}
 
-	public void computeTarget(State oldState, State newState) throws PrismLangException
+	public void computeTarget(State currentState, State newState) throws PrismLangException
 	{
-		computeTarget(0, oldState, newState);
+		computeTarget(0, currentState, newState);
 	}
 
+	/**
+	 * Get the probability rate for the ith transition.
+	 * NB: for efficiency, there are no bounds checks done on i.
+	 */
 	public double getProbability(int i)
 	{
-		if (i < 0 || i >= size())
-			return -1;
-		//throw new PrismLangException("Invalid grouped transition index " + i);
 		return probability.get(i);
 	}
 
@@ -233,19 +267,6 @@ public class ChoiceListFlexi implements Choice
 		return sum;
 	}
 
-	public Command getCommand()
-	{
-		return getCommand(0);
-	}
-
-	public Command getCommand(int i)
-	{
-		if (i < 0 || i >= size())
-			return null;
-		//throw new PrismLangException("Invalid grouped transition index " + i);
-		return command.get(i);
-	}
-
 	/**
 	 * Return the index of a transition according to a probability (or rate) sum, x.
 	 * i.e. return the index of the first transition in this choice for which the

prism/src/simulator/ChoiceSingleton.java

@@ -90,7 +90,7 @@ public class ChoiceSingleton implements Choice
 		return action;
 	}
 
-	public String getUpdateString(int i)
+	public String getUpdateString(int i, State currentState)
 	{
 		String s = "(";
 		for (Update up : updates)
@@ -99,6 +99,11 @@ public class ChoiceSingleton implements Choice
 		return s;
 	}
 	
+	public String getUpdateStringFull(int i)
+	{
+		return null;
+	}
+	
 	public State computeTarget(State oldState) throws PrismLangException
 	{
 		State newState = new State(oldState);

prism/src/simulator/SimulatorEngine.java

@@ -106,21 +106,21 @@ public class SimulatorEngine
 	private List<Expression> properties;
 	private List<Sampler> propertySamplers;
 
-	// Temporary storage for manipulating states/rewards
-	protected State tmpState;
-	protected double tmpStateRewards[];
-	protected double tmpTransitionRewards[];
-
-	// List of currently available transitions
-	protected TransitionList transitionList;
-
 	// Current path info
 	protected Path path;
 	protected boolean onTheFly;
+	// Current state (note: this info is duplicated in the path - it is always the same
+	// as path.getCurrentState(); we maintain it separately for efficiency,
+	// i.e. to avoid creating new State objects at every step)
+	protected State currentState;
+	// List of currently available transitions
+	protected TransitionList transitionList;
+	// Temporary storage for manipulating states/rewards
+	protected double tmpStateRewards[];
+	protected double tmpTransitionRewards[];
 
 	// Updater object for model
 	protected Updater updater;
-
 	// Random number generator
 	private RandomNumberGenerator rng;
 
@@ -198,22 +198,22 @@ public class SimulatorEngine
 	 */
 	public void initialisePath(State initialState) throws PrismException
 	{
-		// Store a temporary copy of passed in state
+		// Store passed in state as current state
 		if (initialState != null) {
-			tmpState.copy(new State(initialState));
+			currentState.copy(initialState);
 		}
 		// Or pick a random one
 		else {
 			throw new PrismException("Random initial start state not yet supported");
 		}
-		updater.calculateStateRewards(tmpState, tmpStateRewards);
-		// Initialise stored path if necessary
-		path.initialise(tmpState, tmpStateRewards);
+		updater.calculateStateRewards(currentState, tmpStateRewards);
+		// Initialise stored path
+		path.initialise(currentState, tmpStateRewards);
+		// Generate transitions for initial state 
+		updater.calculateTransitions(currentState, transitionList);
 		// Reset and then update samplers for any loaded properties
 		resetSamplers();
 		updateSamplers();
-		// Generate updates for initial state 
-		updater.calculateTransitions(tmpState, transitionList);
 	}
 
 	/**
@@ -350,10 +350,12 @@ public class SimulatorEngine
 		}
 		// Back track in path
 		((PathFull) path).backtrack(step);
+		// Update current state
+		currentState.copy(path.getCurrentState());
+		// Generate transitions for new current state 
+		updater.calculateTransitions(currentState, transitionList);
 		// Recompute samplers for any loaded properties
 		recomputeSamplers();
-		// Generate updates for new current state 
-		updater.calculateTransitions(path.getCurrentState(), transitionList);
 	}
 
 	/**
@@ -399,9 +401,9 @@ public class SimulatorEngine
 		}
 		// Modify path
 		((PathFull) path).removePrecedingStates(step);
+		// (No need to update currentState or re-generate transitions) 
 		// Recompute samplers for any loaded properties
 		recomputeSamplers();
-		// (No need to re-generate updates for new current state) 
 	}
 
 	/**
@@ -540,7 +542,7 @@ public class SimulatorEngine
 	 */
 	public boolean queryIsDeadlock() throws PrismLangException
 	{
-		return transitionList.getNumChoices() == 0;
+		return transitionList.isDeadlock();
 	}
 
 	/**
@@ -551,7 +553,7 @@ public class SimulatorEngine
 	public boolean queryIsDeadlock(int step) throws PrismLangException
 	{
 		// By definition, earlier states in the path cannot be deadlocks
-		return step == path.size() ? queryIsDeadlock() : false;
+		return step == path.size() ? transitionList.isDeadlock() : false;
 	}
 
 	/**
@@ -599,8 +601,8 @@ public class SimulatorEngine
 		// Evaluate constants and optimise (a copy of) modules file for simulation
 		modulesFile = (ModulesFile) modulesFile.deepCopy().replaceConstants(mfConstants).simplify();
 
-		// Create temporary state/transition storage
-		tmpState = new State(numVars);
+		// Create state/transition/rewards storage
+		currentState = new State(numVars);
 		tmpStateRewards = new double[modulesFile.getNumRewardStructs()];
 		tmpTransitionRewards = new double[modulesFile.getNumRewardStructs()];
 		transitionList = new TransitionList();
@@ -631,15 +633,17 @@ public class SimulatorEngine
 			index = transitionList.getTotalIndexOfTransition(i, offset);
 		// Compute its transition rewards
 		updater.calculateTransitionRewards(path.getCurrentState(), choice, tmpTransitionRewards);
-		// Compute next state (and its state rewards)
-		choice.computeTarget(offset, path.getCurrentState(), tmpState);
-		updater.calculateStateRewards(tmpState, tmpStateRewards);
+		// Compute next state. Note use of path.getCurrentState() because currentState
+		// will be overwritten during the call to computeTarget().
+		choice.computeTarget(offset, path.getCurrentState(), currentState);
+		// Compute state rewards for new state 
+		updater.calculateStateRewards(currentState, tmpStateRewards);
 		// Update path
-		path.addStep(index, choice.getModuleOrActionIndex(), tmpTransitionRewards, tmpState, tmpStateRewards);
+		path.addStep(index, choice.getModuleOrActionIndex(), tmpTransitionRewards, currentState, tmpStateRewards);
+		// Generate transitions for next state 
+		updater.calculateTransitions(currentState, transitionList);
 		// Update samplers for any loaded properties
 		updateSamplers();
-		// Generate updates for next state 
-		updater.calculateTransitions(tmpState, transitionList);
 	}
 
 	/**
@@ -662,19 +666,21 @@ public class SimulatorEngine
 			index = transitionList.getTotalIndexOfTransition(i, offset);
 		// Compute its transition rewards
 		updater.calculateTransitionRewards(path.getCurrentState(), choice, tmpTransitionRewards);
-		// Compute next state (and its state rewards)
-		choice.computeTarget(offset, path.getCurrentState(), tmpState);
-		updater.calculateStateRewards(tmpState, tmpStateRewards);
+		// Compute next state. Note use of path.getCurrentState() because currentState
+		// will be overwritten during the call to computeTarget().
+		choice.computeTarget(offset, path.getCurrentState(), currentState);
+		// Compute state rewards for new state 
+		updater.calculateStateRewards(currentState, tmpStateRewards);
 		// Update path
-		path.addStep(time, index, choice.getModuleOrActionIndex(), tmpTransitionRewards, tmpState, tmpStateRewards);
+		path.addStep(time, index, choice.getModuleOrActionIndex(), tmpTransitionRewards, currentState, tmpStateRewards);
+		// Generate transitions for next state 
+		updater.calculateTransitions(currentState, transitionList);
 		// Update samplers for any loaded properties
 		updateSamplers();
-		// Generate updates for next state 
-		updater.calculateTransitions(tmpState, transitionList);
 	}
 
 	/**
-	 * Reset samplers for any loaded properties that a new step has occurred.
+	 * Reset samplers for any loaded properties.
 	 */
 	private void resetSamplers() throws PrismLangException
 	{
@@ -689,7 +695,7 @@ public class SimulatorEngine
 	private void updateSamplers() throws PrismLangException
 	{
 		for (Sampler sampler : propertySamplers) {
-			sampler.update(path);
+			sampler.update(path, transitionList);
 		}
 	}
 
@@ -706,7 +712,8 @@ public class SimulatorEngine
 		for (i = 0; i <= n; i++) {
 			prefix.setPrefixLength(i);
 			for (Sampler sampler : propertySamplers) {
-				sampler.update(prefix);
+				sampler.update(prefix, null);
+				// TODO: fix this optimisation 
 			}
 		}
 	}
@@ -816,12 +823,27 @@ public class SimulatorEngine
 
 	/**
 	 * Get a string describing the updates making up a transition, specified by its index.
+	 * This is in abbreviated form, i.e. x'=1, rather than x'=x+1.
+	 * Format is: x'=1, y'=0, with empty string for empty update.
+	 * Only variables updated are included in list (even if unchanged).
 	 */
-	public String getTransitionUpdateString(int index)
+	public String getTransitionUpdateString(int index) throws PrismLangException
 	{
-		return transitionList.getTransitionUpdateString(index);
+		return transitionList.getTransitionUpdateString(index, path.getCurrentState());
 	}
-
+	
+	/**
+	 * Get a string describing the updates making up a transition, specified by its index.
+	 * This is in full, i.e. of the form x'=x+1, rather than x'=1.
+	 * Format is: (x'=x+1) & (y'=y-1), with empty string for empty update.
+	 * Only variables updated are included in list.
+	 * Note that expressions may have been simplified from original model. 
+	 */
+	public String getTransitionUpdateStringFull(int index)
+	{
+		return transitionList.getTransitionUpdateStringFull(index);
+	}
+	
 	/**
 	 * Get the target (as a new State object) of a transition within a choice, specified by its index/offset.
 	 */

prism/src/simulator/TransitionList.java

@@ -48,7 +48,7 @@ public class TransitionList
 		//int index;
 		//Choice ch;
 	}
-	
+
 	public void clear()
 	{
 		choices.clear();
@@ -58,7 +58,7 @@ public class TransitionList
 		numTransitions = 0;
 		probSum = 0.0;
 	}
-	
+
 	public void add(Choice tr)
 	{
 		int i, n;
@@ -72,9 +72,9 @@ public class TransitionList
 		numTransitions += tr.size();
 		probSum += tr.getProbabilitySum();
 	}
-	
+
 	// ACCESSORS
-	
+
 	/**
 	 * Get the number of choices.
 	 */
@@ -82,7 +82,7 @@ public class TransitionList
 	{
 		return numChoices;
 	}
-	
+
 	/**
 	 * Get the number of transitions.
 	 */
@@ -90,7 +90,7 @@ public class TransitionList
 	{
 		return numTransitions;
 	}
-	
+
 	/**
 	 * Get the total sum of all probabilities (or rates).
 	 */
@@ -98,9 +98,9 @@ public class TransitionList
 	{
 		return probSum;
 	}
-	
+
 	// Get access to Choice objects 
-	
+
 	/**
 	 * Get the ith choice.
 	 */
@@ -118,7 +118,7 @@ public class TransitionList
 	}
 
 	// Get index/offset info
-	
+
 	/**
 	 * Get the index of the choice containing a transition of a given index.
 	 */
@@ -144,7 +144,7 @@ public class TransitionList
 	}
 
 	// Random selection of a choice 
-	
+
 	/**
 	 * Get a reference to a transition according to a total probability (rate) sum, x.
 	 * i.e.the first transition for which the sum of probabilities of all prior transitions
@@ -174,7 +174,7 @@ public class TransitionList
 	}
 
 	// Direct access to transition info
-	
+
 	/**
 	 * Get a string describing the action/module of a transition, specified by its index.
 	 */
@@ -182,7 +182,7 @@ public class TransitionList
 	{
 		return getChoiceOfTransition(index).getModuleOrAction();
 	}
-	
+
 	/**
 	 * Get the probability/rate of a transition, specified by its index.
 	 */
@@ -190,34 +190,85 @@ public class TransitionList
 	{
 		return getChoiceOfTransition(index).getProbability(transitionOffsets.get(index));
 	}
-	
+
 	/**
 	 * Get a string describing the updates making up a transition, specified by its index.
+	 * This is in abbreviated form, i.e. x'=1, rather than x'=x+1.
+	 * Format is: x'=1, y'=0, with empty string for empty update.
+	 * Only variables updated are included in list (even if unchanged).
 	 */
-	public String getTransitionUpdateString(int index)
+	public String getTransitionUpdateString(int index, State currentState) throws PrismLangException
 	{
-		return getChoiceOfTransition(index).getUpdateString(transitionOffsets.get(index));
+		return getChoiceOfTransition(index).getUpdateString(transitionOffsets.get(index), currentState);
 	}
-	
+
+	/**
+	 * Get a string describing the updates making up a transition, specified by its index.
+	 * This is in full, i.e. of the form x'=x+1, rather than x'=1.
+	 * Format is: (x'=x+1) & (y'=y-1), with empty string for empty update.
+	 * Only variables updated are included in list.
+	 * Note that expressions may have been simplified from original model. 
+	 */
+	public String getTransitionUpdateStringFull(int index)
+	{
+		return getChoiceOfTransition(index).getUpdateStringFull(transitionOffsets.get(index));
+	}
+
 	/**
 	 * Get the target of a transition (as a new State object), specified by its index.
 	 */
-	public State computeTransitionTarget(int index, State oldState) throws PrismLangException
+	public State computeTransitionTarget(int index, State currentState) throws PrismLangException
+	{
+		return getChoiceOfTransition(index).computeTarget(transitionOffsets.get(index), currentState);
+	}
+
+	/**
+	 * Is there a deadlock (i.e. no available transitions)?
+	 */
+	public boolean isDeadlock()
 	{
-		return getChoiceOfTransition(index).computeTarget(transitionOffsets.get(index), oldState);
+		return numChoices == 0;
 	}
-	
+
+	/**
+	 * Is there a deterministic self-loop, i.e. do all transitions go to the current state.
+	 */
+	public boolean isDeterministicSelfLoop(State currentState)
+	{
+		// TODO: make more efficient, and also limit calls to it
+		// (e.g. only if already stayed in state twice?)
+		int i, n;
+		State newState = new State(currentState);
+		try {
+			for (Choice ch : choices) {
+				n = ch.size();
+				for (i = 0; i < n; i++) {
+					ch.computeTarget(i, currentState, newState);
+					if (!currentState.equals(newState)) {
+						// Found a non-loop
+						return false;
+					}
+				}
+			}
+		} catch (PrismLangException e) {
+			// If anything goes wrong when evaluating, just return false.
+			return false;
+		}
+		// All targets loop
+		return true;
+	}
+
 	@Override
 	public String toString()
 	{
 		String s = "";
 		boolean first = true;
-		for (Choice tr : choices) {
+		for (Choice ch : choices) {
 			if (first)
 				first = false;
 			else
 				s += ", ";
-			s += tr.toString();
+			s += ch.toString();
 		}
 		return s;
 	}

prism/src/simulator/Updater.java

@@ -294,7 +294,7 @@ public class Updater
 			sum += p;
 			list = new ArrayList<Update>();
 			list.add(ups.getUpdate(i));
-			ch.add(p, list, ups.getParent());
+			ch.add(p, list);
 		}
 		// Check distribution sums to 1 (if required)
 		if (modelType.choicesSumToOne() && Math.abs(sum - 1) > prism.getSumRoundOff()) {

prism/src/simulator/sampler/Sampler.java

@@ -59,9 +59,11 @@ 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.
+	 * We also need the transition list for the current (end) state of the path
+	 * to check if there is a deadlock or self-loop.
 	 * This returns true if the sampler's value becomes (or is already) known.
 	 */
-	public abstract boolean update(Path path) throws PrismLangException;
+	public abstract boolean update(Path path, TransitionList transList) 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 boolean update(Path path) throws PrismLangException;
+	public abstract boolean update(Path path, TransitionList transList) throws PrismLangException;
 
 	@Override
 	public void updateStats()

prism/src/simulator/sampler/SamplerBoundedUntilCont.java

@@ -63,7 +63,7 @@ public class SamplerBoundedUntilCont extends SamplerBoolean
 	}
 
 	@Override
-	public boolean update(Path path) throws PrismLangException
+	public boolean update(Path path, TransitionList transList) throws PrismLangException
 	{
 		// If the answer is already known we should do nothing
 		if (valueKnown)

prism/src/simulator/sampler/SamplerBoundedUntilDisc.java

@@ -59,7 +59,7 @@ public class SamplerBoundedUntilDisc extends SamplerBoolean
 	}
 
 	@Override
-	public boolean update(Path path) throws PrismLangException
+	public boolean update(Path path, TransitionList transList) throws PrismLangException
 	{
 		// If the answer is already known we should do nothing
 		if (valueKnown)

prism/src/simulator/sampler/SamplerDouble.java

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

prism/src/simulator/sampler/SamplerNext.java

@@ -52,7 +52,7 @@ public class SamplerNext extends SamplerBoolean
 	}
 
 	@Override
-	public boolean update(Path path) throws PrismLangException
+	public boolean update(Path path, TransitionList transList) throws PrismLangException
 	{
 		// If the answer is already known we should do nothing
 		if (valueKnown)

prism/src/simulator/sampler/SamplerRewardCumulCont.java

@@ -55,7 +55,7 @@ public class SamplerRewardCumulCont extends SamplerDouble
 	}
 
 	@Override
-	public boolean update(Path path) throws PrismLangException
+	public boolean update(Path path, TransitionList transList) throws PrismLangException
 	{
 		// If the answer is already known we should do nothing
 		if (valueKnown)

prism/src/simulator/sampler/SamplerRewardCumulDisc.java

@@ -55,7 +55,7 @@ public class SamplerRewardCumulDisc extends SamplerDouble
 	}
 
 	@Override
-	public boolean update(Path path) throws PrismLangException
+	public boolean update(Path path, TransitionList transList) throws PrismLangException
 	{
 		// If the answer is already known we should do nothing
 		if (valueKnown)

prism/src/simulator/sampler/SamplerRewardInstCont.java

@@ -55,7 +55,7 @@ public class SamplerRewardInstCont extends SamplerDouble
 	}
 
 	@Override
-	public boolean update(Path path) throws PrismLangException
+	public boolean update(Path path, TransitionList transList) throws PrismLangException
 	{
 		// If the answer is already known we should do nothing
 		if (valueKnown)

prism/src/simulator/sampler/SamplerRewardInstDisc.java

@@ -55,7 +55,7 @@ public class SamplerRewardInstDisc extends SamplerDouble
 	}
 
 	@Override
-	public boolean update(Path path) throws PrismLangException
+	public boolean update(Path path, TransitionList transList) throws PrismLangException
 	{
 		// If the answer is already known we should do nothing
 		if (valueKnown)

prism/src/simulator/sampler/SamplerRewardReach.java

@@ -59,7 +59,7 @@ public class SamplerRewardReach extends SamplerDouble
 	}
 
 	@Override
-	public boolean update(Path path) throws PrismLangException
+	public boolean update(Path path, TransitionList transList) throws PrismLangException
 	{
 		// If the answer is already known we should do nothing
 		if (valueKnown)

prism/src/simulator/sampler/SamplerUntil.java

@@ -57,25 +57,30 @@ public class SamplerUntil extends SamplerBoolean
 	}
 
 	@Override
-	public boolean update(Path path) throws PrismLangException
+	public boolean update(Path path, TransitionList transList) 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)) {
 			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/self-loop
+		else if (transList != null && (transList.isDeadlock() || transList.isDeterministicSelfLoop(currentState))) {
+			valueKnown = true;
+			value = false;
+		}
 		// Otherwise, don't know
-		
+
 		return valueKnown;
 	}
 }