Added (self-loop) deterministic loop detection to simulator.

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

prism/NOTES

@@ -16,9 +16,6 @@ PTAs:
 * non-zeno checks?
 * Sort VarList (two types - before and after constants evaluated). Need for simulator too.
 
-Sim(?):
-* Auto x100 in GUI sim doesn't stop on even simple loops
-
 =======================================================
 
 TODO (before public release)
@@ -105,7 +102,7 @@ PTAs:
 
 Simulator:
 * Investigate efficiency wrt old simulator
-* Add (back) support for full loop detection? (embedded into Path*?)
+* Add (back) support for *full* loop detection? (not just *single* self-loops)
 * Add (back) early manual termination of sampling (thru expt stop?)
 * Random initial state
 * Variable overflow etc.

prism/src/simulator/GenerateSimulationPath.java

@@ -226,8 +226,7 @@ public class GenerateSimulationPath
 			done = false;
 			while (!done) {
 				// generate a single step of path
-				// TODO: engine.automaticTransitions(1, simLoopCheck);
-				engine.automaticTransitions(1);
+				engine.automaticTransitions(1, simLoopCheck);
 				if (stochastic)
 					t += engine.getTimeSpentInPathStep(i++);
 				else

prism/src/simulator/LoopDetector.java

@@ -0,0 +1,125 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package simulator;
+
+/**
+ * Detects deterministic loops in a path though a model.
+ * (Currently, only detects single-step loops.)
+ */
+public class LoopDetector
+{
+	// Deterministic loop info
+	private boolean isLooping;
+	private int loopStart;
+	private int loopEnd;
+
+	/**
+	 * Initialise the loop detector.
+	 */
+	public void initialise()
+	{
+		isLooping = false;
+		loopStart = loopEnd = -1;
+	}
+	
+	/**
+	 * Update loop detector after a step has just been added to the path.
+	 */
+	public void addStep(Path path, TransitionList transitionList)
+	{
+		// If already looping, nothing to do
+		if (isLooping)
+			return;
+		// Deterministic loops cannot occur in continuous-time models
+		if (path.continuousTime())
+			return;
+		// Check transitions from previous step were deterministic
+		if (!transitionList.isDeterministic())
+			return;
+		// Check successive states were identical
+		if (path.getPreviousState().equals(path.getCurrentState())) {
+			isLooping = true;
+			loopStart = path.size() - 1;
+			loopEnd = path.size();
+		}
+	}
+	
+	/**
+	 * Update loop detector after a backtrack within the path has been made.
+	 */
+	public void backtrack(Path path)
+	{
+		if (isLooping) {
+			if (path.size() < loopEnd) {
+				isLooping = false;
+				loopStart = loopEnd = -1;
+			}
+		}
+	}
+	
+	/**
+	 * Update loop detector after a prefix of the path has been removed.
+	 * @param path Path object (already updated)
+	 * @param step Index of old path that is now start of path (i.e. num states removed)
+	 */
+	public void removePrecedingStates(Path path, int step)
+	{
+		if (isLooping) {
+			if (step > loopStart) {
+				isLooping = false;
+				loopStart = loopEnd = -1;
+			} else {
+				loopStart -= step;
+				loopEnd -= step;
+			}
+		}
+	}
+	
+	/**
+	 * Does the path contain a deterministic loop?
+	 */
+	public boolean isLooping()
+	{
+		return isLooping;
+	}
+	
+	/**
+	 * What is the step index of the start of the deterministic loop, if it exists?
+	 */
+	public int loopStart()
+	{
+		return loopStart;
+	}
+	
+	/**
+	 * What is the step index of the end of the deterministic loop, if it exists?
+	 */
+	public int loopEnd()
+	{
+		return loopEnd;
+	}
+}

prism/src/simulator/Path.java

@@ -45,16 +45,21 @@ public abstract class Path
 	 * Add a step to the path.
 	 * Note: State object and arrays will be copied, not stored directly.
 	 */
-	public abstract void addStep(int choice, int actionIndex, double[] transRewards, State newState, double[] newStateRewards);
+	public abstract void addStep(int choice, int actionIndex, double[] transRewards, State newState, double[] newStateRewards, TransitionList transitionList);
 
 	/**
 	 * Add a timed step to the path.
 	 * Note: State object and arrays will be copied, not stored directly.
 	 */
-	public abstract void addStep(double time, int choice, int actionIndex, double[] transRewards, State newState, double[] newStateRewards);
+	public abstract void addStep(double time, int choice, int actionIndex, double[] transRewards, State newState, double[] newStateRewards, TransitionList transitionList);
 
 	// ACCESSORS
 
+	/**
+	 * Check whether this path includes continuous-time information, e.g. delays for a CTMC.
+	 */
+	public abstract boolean continuousTime();
+
 	/**
 	 * Get the size of the path (number of steps; or number of states - 1).
 	 */
@@ -107,4 +112,19 @@ public abstract class Path
 	 * @param rsi Reward structure index
 	 */
 	public abstract double getCurrentStateReward(int rsi);
+	
+	/**
+	 * Does the path contain a deterministic loop?
+	 */
+	public abstract boolean isLooping();
+	
+	/**
+	 * What is the step index of the start of the deterministic loop, if it exists?
+	 */
+	public abstract int loopStart();
+	
+	/**
+	 * What is the step index of the end of the deterministic loop, if it exists?
+	 */
+	public abstract int loopEnd();
 }

prism/src/simulator/PathFull.java

@@ -55,6 +55,9 @@ public class PathFull extends Path
 	// The path length (just for convenience; equal to steps.size() - 1)
 	private int size;
 	
+	// Loop detector for path
+	protected LoopDetector loopDet;
+
 	/**
 	 * Constructor: creates a new (empty) PathFull object for a specific model.
 	 */
@@ -70,6 +73,8 @@ public class PathFull extends Path
 		steps = new ArrayList<Step>(100);
 		// Initialise variables
 		clear();
+		// Create loop detector
+		loopDet = new LoopDetector();
 	}
 
 	/**
@@ -98,16 +103,18 @@ public class PathFull extends Path
 		for (int i = 0; i < numRewardStructs; i++) {
 			step.rewardsCumul[i] = 0.0;
 		}
+		// Initialise loop detector
+		loopDet.initialise();
 	}
 
 	@Override
-	public void addStep(int choice, int moduleOrActionIndex, double[] transitionRewards, State newState, double[] newStateRewards)
+	public void addStep(int choice, int moduleOrActionIndex, double[] transitionRewards, State newState, double[] newStateRewards, TransitionList transitionList)
 	{
-		addStep(0.0, choice, moduleOrActionIndex, transitionRewards, newState, newStateRewards);
+		addStep(0.0, choice, moduleOrActionIndex, transitionRewards, newState, newStateRewards, transitionList);
 	}
 
 	@Override
-	public void addStep(double time, int choice, int moduleOrActionIndex, double[] transitionRewards, State newState, double[] newStateRewards)
+	public void addStep(double time, int choice, int moduleOrActionIndex, double[] transitionRewards, State newState, double[] newStateRewards, TransitionList transitionList)
 	{
 		Step stepOld, stepNew;
 		// Add info to last existing step
@@ -134,6 +141,8 @@ public class PathFull extends Path
 		}
 		// Update size too
 		size++;
+		// Update loop detector
+		loopDet.addStep(this, transitionList);
 	}
 
 	// MUTATORS (additional)
@@ -158,16 +167,18 @@ public class PathFull extends Path
 			last.transitionRewards[i] = 0.0;
 		// Update size too
 		size = step;
+		// Update loop detector
+		loopDet.backtrack(this);
 	}
 	
 	/**
 	 * Remove the prefix of the current path up to the given path step.
 	 * Index step should be >=0 and <= the total path size. 
-	 * @param step The step before which state will be removed.
+	 * @param step The step before which states will be removed.
 	 */
 	public void removePrecedingStates(int step)
 	{
-		int i, j, n, n2;
+		int i, j, numKeep, sizeOld;
 		double timeCumul, rewardsCumul[];
 		
 		// Ignore trivial case
@@ -180,8 +191,8 @@ public class PathFull extends Path
 			rewardsCumul[j] = getCumulativeReward(step, j);
 		// Move later steps of path 'step' places forward 
 		// and subtract time/reward as appropriate 
-		n = steps.size() - step;
-		for (i = 0; i < n; i++) {
+		numKeep = steps.size() - step;
+		for (i = 0; i < numKeep; i++) {
 			Step tmp = steps.get(i + step);
 			tmp.timeCumul -= timeCumul;
 			for (j = 0; j < numRewardStructs; j++)
@@ -189,20 +200,26 @@ public class PathFull extends Path
 			steps.set(i, tmp);
 		}
 		// Remove steps after index 'step'
-		n2 = steps.size() - 1;
-		for (i = n2; i >= n; i--)
+		sizeOld = steps.size();
+		for (i = sizeOld - 1; i >= numKeep; i--)
 			steps.remove(i);
 		// Update size too
 		size = steps.size() - 1;
+		// Update loop detector
+		loopDet.removePrecedingStates(this, step);
 	}
 	
 	// ACCESSORS (for Path)
 
+	@Override
+	public boolean continuousTime()
+	{
+		return continuousTime;
+	}
+	
 	@Override
 	public int size()
 	{
-		// TODO: remove this sanity check
-		if (size != steps.size() - 1) throw new Error("size != size");
 		return size;
 	}
 
@@ -254,6 +271,24 @@ public class PathFull extends Path
 		return steps.get(steps.size() - 1).stateRewards[rsi];
 	}
 	
+	@Override
+	public boolean isLooping()
+	{
+		return loopDet.isLooping();
+	}
+	
+	@Override
+	public int loopStart()
+	{
+		return loopDet.loopStart();
+	}
+	
+	@Override
+	public int loopEnd()
+	{
+		return loopDet.loopEnd();
+	}
+	
 	// ACCESSORS (additional)
 
 	/**

prism/src/simulator/PathFullPrefix.java

@@ -57,13 +57,13 @@ public class PathFullPrefix extends Path
 	}
 
 	@Override
-	public void addStep(int choice, int moduleOrActionIndex, double[] transitionRewards, State newState, double[] newStateRewards)
+	public void addStep(int choice, int moduleOrActionIndex, double[] transitionRewards, State newState, double[] newStateRewards, TransitionList transitionList)
 	{
 		// Do nothing (we are not allowed to modify the underlying PathFull)
 	}
 
 	@Override
-	public void addStep(double time, int choice, int moduleOrActionIndex, double[] transitionRewards, State newState, double[] newStateRewards)
+	public void addStep(double time, int choice, int moduleOrActionIndex, double[] transitionRewards, State newState, double[] newStateRewards, TransitionList transitionList)
 	{
 		// Do nothing (we are not allowed to modify the underlying PathFull)
 	}
@@ -77,6 +77,12 @@ public class PathFullPrefix extends Path
 	
 	// ACCESSORS (for Path)
 
+	@Override
+	public boolean continuousTime()
+	{
+		return pathFull.continuousTime();
+	}
+	
 	@Override
 	public int size()
 	{
@@ -130,4 +136,22 @@ public class PathFullPrefix extends Path
 	{
 		return pathFull.getStateReward(prefixLength, rsi);
 	}
+	
+	@Override
+	public boolean isLooping()
+	{
+		return pathFull.isLooping() && pathFull.loopEnd() < prefixLength;
+	}
+	
+	@Override
+	public int loopStart()
+	{
+		return isLooping() ? pathFull.loopStart() : -1;
+	}
+	
+	@Override
+	public int loopEnd()
+	{
+		return isLooping() ? pathFull.loopEnd() : -1;
+	}
 }

prism/src/simulator/PathOnTheFly.java

@@ -55,6 +55,9 @@ public class PathOnTheFly extends Path
 	protected double previousTransitionRewards[];
 	protected double currentStateRewards[];
 	
+	// Loop detector for path
+	protected LoopDetector loopDet;
+
 	/**
 	 * Constructor: creates a new (empty) PathOnTheFly object for a specific model.
 	 */
@@ -76,6 +79,8 @@ public class PathOnTheFly extends Path
 		currentStateRewards = new double[numRewardStructs];
 		// Initialise path info
 		clear();
+		// Create loop detector
+		loopDet = new LoopDetector();
 	}
 
 	/**
@@ -107,16 +112,18 @@ public class PathOnTheFly extends Path
 		for (int i = 0; i < numRewardStructs; i++) {
 			currentStateRewards[i] = initialStateRewards[i];
 		}
+		// Initialise loop detector
+		loopDet.initialise();
 	}
 
 	@Override
-	public void addStep(int choice, int actionIndex, double[] transRewards, State newState, double[] newStateRewards)
+	public void addStep(int choice, int actionIndex, double[] transRewards, State newState, double[] newStateRewards, TransitionList transitionList)
 	{
-		addStep(0, choice, actionIndex, transRewards, newState, newStateRewards);
+		addStep(0, choice, actionIndex, transRewards, newState, newStateRewards, transitionList);
 	}
 
 	@Override
-	public void addStep(double time, int choice, int actionIndex, double[] transRewards, State newState, double[] newStateRewards)
+	public void addStep(double time, int choice, int actionIndex, double[] transRewards, State newState, double[] newStateRewards, TransitionList transitionList)
 	{
 		size++;
 		previousState.copy(currentState);
@@ -133,10 +140,18 @@ public class PathOnTheFly extends Path
 			previousTransitionRewards[i] = transRewards[i];
 			currentStateRewards[i] = newStateRewards[i];
 		}
+		// Update loop detector
+		loopDet.addStep(this, transitionList);
 	}
 
 	// ACCESSORS (for Path)
 
+	@Override
+	public boolean continuousTime()
+	{
+		return continuousTime;
+	}
+	
 	@Override
 	public int size()
 	{
@@ -190,4 +205,22 @@ public class PathOnTheFly extends Path
 	{
 		return currentStateRewards[rsi];
 	}
+	
+	@Override
+	public boolean isLooping()
+	{
+		return loopDet.isLooping();
+	}
+	
+	@Override
+	public int loopStart()
+	{
+		return loopDet.loopStart();
+	}
+	
+	@Override
+	public int loopEnd()
+	{
+		return loopDet.loopEnd();
+	}
 }

prism/src/simulator/SimulatorEngine.java

@@ -294,12 +294,13 @@ public class SimulatorEngine
 	 * Select, at random, n successive transitions and execute them.
 	 * For continuous-time models, the time to be spent in each state before leaving is also picked randomly.
 	 * If a deadlock is found, the process stops.
+	 * Optionally, if a deterministic loop is detected, the process stops.
 	 * The function returns the number of transitions successfully taken. 
 	 */
-	public int automaticTransitions(int n) throws PrismException
+	public int automaticTransitions(int n, boolean stopOnLoops) throws PrismException
 	{
 		int i = 0;
-		while (i < n) {
+		while (i < n && !(stopOnLoops && path.isLooping())) {
 			if (!automaticTransition())
 				break;
 			i++;
@@ -314,11 +315,11 @@ public class SimulatorEngine
 	 * If a deadlock is found, the process stops.
 	 * The function returns the number of transitions successfully taken. 
 	 */
-	public int automaticTransitions(double time) throws PrismException
+	public int automaticTransitions(double time, boolean stopOnLoops) throws PrismException
 	{
 		// For discrete-time models, this just results in ceil(time) steps being executed.
 		if (!modelType.continuousTime()) {
-			return automaticTransitions((int) Math.ceil(time));
+			return automaticTransitions((int) Math.ceil(time), false);
 		} else {
 			int i = 0;
 			double targetTime = path.getTotalTime() + time;
@@ -638,7 +639,7 @@ public class SimulatorEngine
 		// Compute state rewards for new state 
 		updater.calculateStateRewards(currentState, tmpStateRewards);
 		// Update path
-		path.addStep(index, choice.getModuleOrActionIndex(), tmpTransitionRewards, currentState, tmpStateRewards);
+		path.addStep(index, choice.getModuleOrActionIndex(), tmpTransitionRewards, currentState, tmpStateRewards, transitionList);
 		// Generate transitions for next state 
 		updater.calculateTransitions(currentState, transitionList);
 		// Update samplers for any loaded properties
@@ -671,7 +672,7 @@ public class SimulatorEngine
 		// Compute state rewards for new state 
 		updater.calculateStateRewards(currentState, tmpStateRewards);
 		// Update path
-		path.addStep(time, index, choice.getModuleOrActionIndex(), tmpTransitionRewards, currentState, tmpStateRewards);
+		path.addStep(time, index, choice.getModuleOrActionIndex(), tmpTransitionRewards, currentState, tmpStateRewards, transitionList);
 		// Generate transitions for next state 
 		updater.calculateTransitions(currentState, transitionList);
 		// Update samplers for any loaded properties
@@ -1012,23 +1013,23 @@ public class SimulatorEngine
 	 */
 	public boolean isPathLooping()
 	{
-		return false; // TODO
+		return path.isLooping();
 	}
 
 	/**
-	 * Check whether a deterministic loop (if present) starts.
+	 * Get at which step a deterministic loop (if present) starts.
 	 */
 	public int loopStart()
 	{
-		return -1; // TODO
+		return path.loopStart();
 	}
 
 	/**
-	 * Check whether a deterministic loop (if present) starts.
+	 * Get at which step a deterministic loop (if present) ends.
 	 */
 	public int loopEnd()
 	{
-		return -1; // TODO
+		return path.loopEnd();
 	}
 
 	/**

prism/src/simulator/TransitionList.java

@@ -243,6 +243,8 @@ public class TransitionList
 
 	/**
 	 * Are the choices deterministic? (i.e. a single probability 1.0 transition)
+	 * (will also return true for a continuous-time model matching this
+	 * definition, since TransitionList does not know about model type)
 	 */
 	public boolean isDeterministic()
 	{

prism/src/simulator/sampler/SamplerUntil.java

@@ -75,7 +75,8 @@ public class SamplerUntil extends SamplerBoolean
 			value = false;
 		}
 		// Or, if we are now at a deadlock/self-loop
-		else if (transList != null && (transList.isDeadlock() || transList.isDeterministicSelfLoop(currentState))) {
+		else if (transList != null && (transList.isDeadlock() || path.isLooping())) {
+		//else if (transList != null && (transList.isDeadlock() || transList.isDeterministicSelfLoop(currentState))) {
 			valueKnown = true;
 			value = false;
 		}

prism/src/userinterface/simulator/GUISimulator.java

@@ -397,10 +397,8 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 	public void a_autoStep(int noSteps)
 	{
 		try {
-			int oldPathSize = engine.getPathSize();
-
 			if (displayPathLoops && pathTableModel.isPathLooping()) {
-				if (questionYesNo("The current path contains a deterministic loop. Do you wish to disable the detection of deterministic loops and extend the path anyway?") == 0) {
+				if (questionYesNo("The current path contains a deterministic loop. \nDo you wish to disable detection of such loops and extend the path anyway?") == 0) {
 					displayPathLoops = false;
 					pathTable.repaint();
 				} else
@@ -413,8 +411,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 				engine.computeTransitionsForCurrentState();
 			}
 
-			// TODO engine.automaticTransitions(noSteps, displayPathLoops);
-			engine.automaticTransitions(noSteps);
+			int noStepsTaken = engine.automaticTransitions(noSteps, displayPathLoops);
 
 			pathTableModel.updatePathTable();
 			updateTableModel.updateUpdatesTable();
@@ -428,11 +425,9 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 			pathFormulaeList.repaint();
 			setComputing(false);
 
-			int newPathSize = engine.getPathSize();
-
-			if (displayPathLoops && pathTableModel.isPathLooping() && (newPathSize - oldPathSize) < noSteps) {
-				message("Exploration has stopped early because a deterministic loop has been detected.");
-			}
+			//if (displayPathLoops && pathTableModel.isPathLooping() && (noStepsTaken < noSteps) {
+			//	message("Exploration has stopped early because a deterministic loop has been detected.");
+			//}
 		} catch (PrismException e) {
 			this.error(e.getMessage());
 			guiMultiModel.getHandler().modelParseFailed((PrismLangException) e, false);
@@ -447,7 +442,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 			double oldPathTime = engine.getTotalTimeForPath();
 
 			if (displayPathLoops && pathTableModel.isPathLooping()) {
-				if (questionYesNo("The current path contains a deterministic loop. Do you wish to disable the detection of deterministic loops and extend the path anyway?") == 0) {
+				if (questionYesNo("The current path contains a deterministic loop. \nDo you wish to disable detection of such loops and extend the path anyway?") == 0) {
 					displayPathLoops = false;
 					pathTable.repaint();
 				} else
@@ -460,8 +455,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 				engine.computeTransitionsForCurrentState();
 			}
 
-			// TODO engine.automaticTransitions(time, displayPathLoops);
-			engine.automaticTransitions(time);
+			engine.automaticTransitions(time, displayPathLoops);
 
 			pathTableModel.updatePathTable();
 			updateTableModel.updateUpdatesTable();
@@ -475,11 +469,9 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 			pathFormulaeList.repaint();
 			setComputing(false);
 
-			double newPathTime = engine.getTotalTimeForPath();
-
-			if (displayPathLoops && pathTableModel.isPathLooping() && (newPathTime - oldPathTime) < time) {
-				message("Exploration has stopped early because a deterministic loop has been detected.");
-			}
+			//if (displayPathLoops && pathTableModel.isPathLooping() && (engine.getTotalTimeForPath() - oldPathTime) < time) {
+			//	message("Exploration has stopped early because a deterministic loop has been detected.");
+			//}
 		} catch (PrismException e) {
 			this.error(e.getMessage());
 		}
@@ -587,7 +579,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 				throw new PrismException("No current update is selected");
 
 			if (displayPathLoops && pathTableModel.isPathLooping()) {
-				if (questionYesNo("A loop in the path has been detected. Do you wish to disable loop detection and extend the path?") == 0) {
+				if (questionYesNo("The current path contains a deterministic loop. \nDo you wish to disable detection of such loops and extend the path anyway?") == 0) {
 					displayPathLoops = false;
 					pathTable.repaint();
 				} else