Updates to simulator, including random choices for CTMCs.

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

prism/src/simulator/Choice.java

@@ -45,5 +45,5 @@ public interface Choice
 	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 int getIndexByProbSum(double x);
+	public int getIndexByProbabilitySum(double x);
 }

prism/src/simulator/ChoiceList.java

@@ -173,7 +173,7 @@ public class ChoiceList implements Choice
 		return command.get(i);
 	}
 
-	public int getIndexByProbSum(double x)
+	public int getIndexByProbabilitySum(double x)
 	{
 		int i, n;
 		double d;

prism/src/simulator/ChoiceListFlexi.java

@@ -191,12 +191,16 @@ public class ChoiceListFlexi implements Choice
 		return command.get(i);
 	}
 
-	public int getIndexByProbSum(double x)
+	/**
+	 * 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
+	 * sum of probabilities/rates for all prior transitions exceeds x.
+	 */
+	public int getIndexByProbabilitySum(double x)
 	{
 		int i, n;
 		double d;
 		n = size();
-		i = 0;
 		d = 0.0;
 		for (i = 0; x >= d && i < n; i++) {
 			d += probability.get(i);

prism/src/simulator/ChoiceSingleton.java

@@ -70,7 +70,7 @@ public class ChoiceSingleton implements Choice
 		return 1;
 	}
 	
-	public int getIndexByProbSum(double x)
+	public int getIndexByProbabilitySum(double x)
 	{
 		return 0;
 	}

prism/src/simulator/GenerateSimulationPath.java

@@ -83,6 +83,9 @@ public class GenerateSimulationPath
 		generatePath();
 	}
 
+	/**
+	 * Parse a string specifying how to generate a simulation path.
+	 */
 	private void parseDetails(String details) throws PrismException
 	{
 		String s, ss[];
@@ -185,6 +188,9 @@ public class GenerateSimulationPath
 			throw new PrismException("Invalid path details \"" + details + "\"");
 	}
 
+	/**
+	 * Generate a random path using the simulator.
+	 */
 	private void generatePath() throws PrismException
 	{
 		int i = 0, j = 0;

prism/src/simulator/RandomNumberGenerator.java

@@ -40,7 +40,7 @@ public class RandomNumberGenerator
 	/**
 	 * Pick a (uniformly) random integer in range [0,...,n-1].
 	 */
-	public int randomInt(int n)
+	public int randomUnifInt(int n)
 	{
 		return random.nextInt(n);
 	}
@@ -48,7 +48,7 @@ public class RandomNumberGenerator
 	/**
 	 * Pick a (uniformly) random double in range [0,1).
 	 */
-	public double randomDouble()
+	public double randomUnifDouble()
 	{
 		return random.nextDouble();
 	}
@@ -56,8 +56,20 @@ public class RandomNumberGenerator
 	/**
 	 * Pick a (uniformly) random double in range [0,x).
 	 */
-	public double randomDouble(double x)
+	public double randomUnifDouble(double x)
 	{
 		return x * random.nextDouble();
 	}
+	
+	/**
+	 * Pick a random double according to exponential distribution with rate x.
+	 */
+	public double randomExpDouble(double x)
+	{
+		double y;
+		// Pick (non-zero) random y in (0,1)
+		while ((y = random.nextDouble()) == 0);
+		// Sample exponential
+		return (-Math.log(y)) / x;
+	}
 }

prism/src/simulator/SimulatorEngine.java

@@ -403,25 +403,37 @@ public class SimulatorEngine
 
 		Choice choice;
 		int numChoices, i, j;
-		double d;
+		double d, r;
 
 		switch (modelType) {
 		case DTMC:
 		case MDP:
 			// Check for deadlock
-			numChoices = transitionList.numChoices;
+			numChoices = transitionList.getNumChoices();
 			if (numChoices == 0)
 				throw new PrismException("Deadlock found at state " + currentState.toString(modulesFile));
 			// Pick a random choice
-			i = rng.randomInt(numChoices);
+			i = rng.randomUnifInt(numChoices);
 			choice = transitionList.getChoice(i);
 			// Pick a random transition from this choice
-			d = rng.randomDouble();
-			j = choice.getIndexByProbSum(d);
+			d = rng.randomUnifDouble();
+			j = choice.getIndexByProbabilitySum(d);
+			// Execute
 			executeTransition(i, j, -1);
 			break;
 		case CTMC:
-			// TODO: automaticUpdateContinuous();
+			// Check for deadlock
+			numChoices = transitionList.getNumChoices();
+			if (numChoices == 0)
+				throw new PrismException("Deadlock found at state " + currentState.toString(modulesFile));
+			// Get sum of all rates
+			r = transitionList.getProbabilitySum();
+			// Pick a random number to determine choice/transition
+			d = r * rng.randomUnifDouble();
+			TransitionList.Ref ref = transitionList.new Ref();
+			transitionList.getChoiceIndexByProbabilitySum(d, ref);
+			// Execute
+			executeTimedTransition(ref.i, ref.offset, rng.randomExpDouble(r), -1);
 			break;
 		}
 
@@ -460,7 +472,7 @@ public class SimulatorEngine
 
 	/**
 	 * Execute a transition from the current transition list and update path (if being stored).
-	 * Transition is specified by index of it choice and offset within it. If known, its index
+	 * Transition is specified by index of its choice and offset within it. If known, its index
 	 * (within the whole list) can optionally be specified (since this may be needed for storage
 	 * in the path). If this is -1, it will be computed automatically if needed.
 	 * @param i Index of choice containing transition to execute
@@ -488,7 +500,7 @@ public class SimulatorEngine
 
 	/**
 	 * Execute a (timed) transition from the current transition list and update path (if being stored).
-	 * Transition is specified by index of it choice and offset within it. If known, its index
+	 * Transition is specified by index of its choice and offset within it. If known, its index
 	 * (within the whole list) can optionally be specified (since this may be needed for storage
 	 * in the path). If this is -1, it will be computed automatically if needed.
 	 * In addition, the amount of time to be spent in the current state before this transition occurs
@@ -726,7 +738,7 @@ public class SimulatorEngine
 	 */
 	public int getNumTransitions()
 	{
-		return transitionList.numTransitions;
+		return transitionList.getNumTransitions();
 	}
 
 	/**
@@ -736,7 +748,7 @@ public class SimulatorEngine
 	 */
 	public String getTransitionAction(int index) throws PrismException
 	{
-		if (index < 0 || index >= transitionList.numTransitions)
+		if (index < 0 || index >= transitionList.getNumTransitions())
 			throw new PrismException("Invalid transition index " + index);
 		return transitionList.getChoiceOfTransition(index).getAction();
 	}
@@ -764,13 +776,13 @@ public class SimulatorEngine
 	public double getTransitionProbability(int index) throws PrismException
 	{
 		double p = transitionList.getTransitionProbability(index);
-		return (modelType == ModelType.DTMC ? p / transitionList.numChoices : p);
+		return (modelType == ModelType.DTMC ? p / transitionList.getNumChoices() : p);
 	}
 
 	public State computeTransitionTarget(int index) throws PrismLangException
 	{
-		// TODO
-		if (index < 0 || index >= transitionList.numTransitions)
+		// TODO: need to check bounds?
+		if (index < 0 || index >= transitionList.getNumTransitions())
 			return null;
 		//throw new PrismException("Invalid transition index " + index);
 		return transitionList.computeTransitionTarget(index, currentState);

prism/src/simulator/TransitionList.java

@@ -33,13 +33,22 @@ import prism.*;
 
 public class TransitionList
 {
-	public ArrayList<Choice> choices = new ArrayList<Choice>();
-	public ArrayList<Integer> transitionIndices = new ArrayList<Integer>();
-	public ArrayList<Integer> transitionOffsets = new ArrayList<Integer>();
-	public int numChoices = 0;
-	public int numTransitions = 0;
-	public double probSum = 0.0;
+	private ArrayList<Choice> choices = new ArrayList<Choice>();
+	private ArrayList<Integer> transitionIndices = new ArrayList<Integer>();
+	private ArrayList<Integer> transitionOffsets = new ArrayList<Integer>();
+	private int numChoices = 0;
+	private int numTransitions = 0;
+	private double probSum = 0.0;
 
+	// TODO: document this
+	public class Ref
+	{
+		public int i;
+		public int offset;
+		//int index;
+		//Choice ch;
+	}
+	
 	public void clear()
 	{
 		choices.clear();
@@ -63,7 +72,33 @@ public class TransitionList
 		numTransitions += tr.size();
 		probSum += tr.getProbabilitySum();
 	}
-
+	
+	// ACCESSORS
+	
+	/**
+	 * Get the number of choices.
+	 */
+	public int getNumChoices()
+	{
+		return numChoices;
+	}
+	
+	/**
+	 * Get the number of transitions.
+	 */
+	public int getNumTransitions()
+	{
+		return numTransitions;
+	}
+	
+	/**
+	 * Get the total sum of all probabilities (or rates).
+	 */
+	public double getProbabilitySum()
+	{
+		return probSum;
+	}
+	
 	// Get access to Choice objects 
 	
 	/**
@@ -108,6 +143,36 @@ public class TransitionList
 		return transitionOffsets.get(i);
 	}
 
+	// 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
+	 * (across all choices) exceeds x.
+	 * Note: this only really makes sense for models where these are rates, rather than probabilities.
+	 * @param x Probability (or rate) sum
+	 * @param ref Empty transition reference to store result
+	 */
+	public void getChoiceIndexByProbabilitySum(double x, Ref ref)
+	{
+		int i;
+		Choice choice;
+		double d = 0.0, tot = 0.0;
+		// Add up choice prob/rate sums to find choice
+		for (i = 0; x >= tot && i < numChoices; i++) {
+			d = getChoice(i).getProbabilitySum();
+			tot += d;
+		}
+		ref.i = i - 1;
+		// Pick transition within choice 
+		choice = getChoice(i - 1);
+		if (choice.size() > 1) {
+			ref.offset = choice.getIndexByProbabilitySum(tot - d);
+		} else {
+			ref.offset = 0;
+		}
+	}
+
 	// Access to transition info
 	
 	// get prob (or rate) of ith transition
@@ -136,8 +201,14 @@ public class TransitionList
 	public String toString()
 	{
 		String s = "";
-		for (Choice tr : choices)
+		boolean first = true;
+		for (Choice tr : choices) {
+			if (first)
+				first = false;
+			else
+				s += ", ";
 			s += tr.toString();
+		}
 		return s;
 	}
 }

prism/src/simulator/Updater.java

@@ -141,6 +141,7 @@ public class Updater
 					}
 					// Case where there are multiple choices
 					else {
+						// TODO
 						throw new PrismLangException("Don't handle local nondet yet");
 					}
 					System.out.println("prod" + j + ": " + prod);
@@ -202,10 +203,7 @@ public class Updater
 
 		// For DTMCs, need to randomise
 
-		//System.out.println(transitionList.transitionTotal);
-		System.out.println(transitionList.choices);
-		//System.out.println(transitionList.transitionIndices);
-		//System.out.println(transitionList.transitionOffsets);
+		System.out.println(transitionList);
 
 	}