Ongoing simulator improvements.

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

prism/src/simulator/Path.java

@@ -49,6 +49,7 @@ public class Path
 		public State state;
 		public double stateRewards[];
 		public double time;
+		public double timeCumul;
 		public int choice;
 		public String action;
 		public double transitionRewards[];
@@ -58,6 +59,8 @@ public class Path
 	protected SimulatorEngine engine;
 	// Model to which the path corresponds
 	protected ModulesFile modulesFile;
+	// Does model use continuous time?
+	protected boolean continuousTime;
 	// Model info/stats
 	protected int numRewardStructs;
 	// The path, i.e. list of states, etc.
@@ -98,6 +101,11 @@ public class Path
 		return path.get(i).time;
 	}
 
+	public double getCumulativeTime(int i)
+	{
+		return path.get(i).timeCumul;
+	}
+
 	public int getChoice(int i)
 	{
 		return path.get(i).choice;
@@ -122,6 +130,7 @@ public class Path
 		this.engine = engine;
 		// Store model and info
 		this.modulesFile = modulesFile;
+		continuousTime = modulesFile.getModelType().continuousTime();
 		numRewardStructs = modulesFile.getNumRewardStructs();
 		// Create arrays to store totals
 		totalReward = new double[numRewardStructs];
@@ -163,13 +172,28 @@ public class Path
 	}
 
 	/**
-	 * Add step...
+	 * Add a step to the path.
 	 */
 	public void addStep(int choice, String action, double[] transRewards, State newState, double[] newStateRewards)
+	{
+		addStep(0, choice, action, transRewards, newState, newStateRewards);
+	}
+
+	/**
+	 * Add a (timed) step to the path.
+	 */
+	public void addStep(double time, int choice, String action, double[] transRewards, State newState,
+			double[] newStateRewards)
 	{
 		Step step;
 		// Add info to last existing step
 		step = path.get(path.size() - 1);
+		if (continuousTime) {
+			step.time = time;
+			step.timeCumul = time;
+			if (path.size() > 1)
+				step.timeCumul += path.get(path.size() - 1).timeCumul;
+		}
 		step.choice = choice;
 		step.action = action;
 		step.transitionRewards = transRewards.clone();

prism/src/simulator/SimulatorEngine.java

@@ -337,6 +337,7 @@ public class SimulatorEngine
 		}
 		// Or pick a random one
 		else {
+			// TODO
 			//currentState...
 			throw new PrismException("Random initial start state not yet supported");
 		}
@@ -350,30 +351,30 @@ public class SimulatorEngine
 
 	/**
 	 * Execute a transition from the current transition list, specified by its index
-	 * within the (whole) list.
+	 * within the (whole) list. If this is a continuous time model, the time to be spent
+	 * in the state before leaving is picked randomly.
 	 */
 	public void manualUpdate(int index) throws PrismException
 	{
-		int choice = transitionList.getChoiceIndexOfTransition(index);
+		int i = transitionList.getChoiceIndexOfTransition(index);
 		int offset = transitionList.getChoiceOffsetOfTransition(index);
-		executeTransition(choice, offset);
+		if (modelType.continuousTime())
+			executeTimedTransition(i, offset, -1, index);
+		else
+			executeTransition(i, offset, index);
 	}
 
 	/**
-	 * This function applies the index update of the current list of updates to the model. The time spent in the last
-	 * state is also given (for ctmcs). Use -1.0 for this parameter if an automatically generated time is required.
-	 * 
-	 * @param index
-	 *            the index of the selected update to be applied.
-	 * @param time_in_state
-	 *            the time spent in the last state. Use -1.0 for this parameter if an automatically generated time is
-	 *            required.
-	 * @throws PrismException
-	 *             if the index is out of range, or there was a problem with performing the update.
+	 * Execute a transition from the current transition list, specified by its index
+	 * within the (whole) list. In addition, specify the amount of time to be spent in
+	 * the current state before this transition occurs. If -1, this is picked randomly.
+	 * [continuous-time models only]
 	 */
-	public void manualUpdate(int index, double time_in_state) throws PrismException
+	public void manualUpdate(int index, double time) throws PrismException
 	{
-		//TODO int result = makeManualUpdate(index, time_in_state);
+		int i = transitionList.getChoiceIndexOfTransition(index);
+		int offset = transitionList.getChoiceOffsetOfTransition(index);
+		executeTimedTransition(i, offset, time, index);
 	}
 
 	/**
@@ -400,7 +401,7 @@ public class SimulatorEngine
 	{
 		// just one for now...
 
-		Choice ch;
+		Choice choice;
 		int numChoices, i, j;
 		double d;
 
@@ -413,11 +414,11 @@ public class SimulatorEngine
 				throw new PrismException("Deadlock found at state " + currentState.toString(modulesFile));
 			// Pick a random choice
 			i = rng.randomInt(numChoices);
-			ch = transitionList.getChoice(i);
+			choice = transitionList.getChoice(i);
 			// Pick a random transition from this choice
 			d = rng.randomDouble();
-			j = ch.getIndexByProbSum(d);
-			executeTransition(i, j);
+			j = choice.getIndexByProbSum(d);
+			executeTransition(i, j, -1);
 			break;
 		case CTMC:
 			// TODO: automaticUpdateContinuous();
@@ -458,21 +459,61 @@ public class SimulatorEngine
 	}
 
 	/**
-	 * Execute a transition from the current transition list, specified by index
-	 * of choice and offset within that choice. Also update path info (if required).
+	 * 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
+	 * (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
+	 * @param offset Index within choice of transition to execute
+	 * @param index (Optionally) index of transition within whole list (-1 if unknown)
 	 */
-	private void executeTransition(int choice, int offset) throws PrismException
+	private void executeTransition(int i, int offset, int index) throws PrismException
 	{
-		Choice ch;
+		// Get corresponding choice
+		Choice choice = transitionList.getChoice(i);
 		// Remember last state and compute next one (and its state rewards)
 		lastState.copy(currentState);
-		ch = transitionList.getChoice(choice); 
-		ch.computeTarget(offset, lastState, currentState);
+		choice.computeTarget(offset, lastState, currentState);
 		updater.calculateStateRewards(currentState, currentStateRewards);
-		// Stored path info (if necessary)
-		if (!onTheFly)
-			// TODO: first currentStateRewards should be new Trans rewards!
-			path.addStep(offset, ch.getAction(), currentStateRewards, currentState, currentStateRewards);
+		// Store path info (if necessary)
+		if (!onTheFly) {
+			if (index == -1)
+				index = transitionList.getTotalIndexOfTransition(i, offset);
+			path.addStep(index, choice.getAction(), currentStateRewards, currentState, currentStateRewards);
+			// TODO: first currentStateRewards in above should be new *trans* rewards!
+		}
+		// Generate updates for next state 
+		updater.calculateTransitions(currentState, transitionList);
+	}
+
+	/**
+	 * 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
+	 * (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
+	 * should be specified. If -1, this is picked randomly.
+	 * [continuous-time models only]
+	 * @param i Index of choice containing transition to execute
+	 * @param offset Index within choice of transition to execute
+	 * @param time Time for transition
+	 * @param index (Optionally) index of transition within whole list (-1 if unknown)
+	 */
+	private void executeTimedTransition(int i, int offset, double time, int index) throws PrismException
+	{
+		// Get corresponding choice
+		Choice choice = transitionList.getChoice(i);
+		// Remember last state and compute next one (and its state rewards)
+		lastState.copy(currentState);
+		choice.computeTarget(offset, lastState, currentState);
+		updater.calculateStateRewards(currentState, currentStateRewards);
+		// Store path info (if necessary)
+		if (!onTheFly) {
+			if (index == -1)
+				index = transitionList.getTotalIndexOfTransition(i, offset);
+			path.addStep(time, index, choice.getAction(), currentStateRewards, currentState, currentStateRewards);
+			// TODO: first currentStateRewards in above should be new *trans* rewards!
+		}
 		// Generate updates for next state 
 		updater.calculateTransitions(currentState, transitionList);
 	}
@@ -800,26 +841,18 @@ public class SimulatorEngine
 
 	/**
 	 * Returns the time spent in the state at the given path index.
-	 * 
-	 * @param stateIndex
-	 *            the index of the path state of interest
-	 * @return the time spent in the state at the given path index.
 	 */
-	public double getTimeSpentInPathState(int stateIndex)
+	public double getTimeSpentInPathState(int index)
 	{
-		return path.getTime(stateIndex);
+		return path.getTime(index);
 	}
 
 	/**
-	 * Returns the cumulative time spent in the states upto a given path index.
-	 * 
-	 * @param stateIndex
-	 *            the index of the path state of interest
-	 * @return the time spent in the state at the given path index.
+	 * Returns the cumulative time spent in the states up to (and including) a given path index.
 	 */
-	public double getCumulativeTimeSpentInPathState(int stateIndex)
+	public double getCumulativeTimeSpentInPathState(int index)
 	{
-		return 99;
+		return path.getCumulativeTime(index);
 	}
 
 	/**
@@ -932,15 +965,11 @@ public class SimulatorEngine
 	public static native int loopEnd();
 
 	/**
-	 * Returns the index of the update chosen for the precalculated old update set.
-	 * 
-	 * @param oldStep
-	 *            the old path step of interest
-	 * @return the index of the update chosen for the precalculated old update set.
+	 * Returns the index of the update chosen for an earlier state in the path.
 	 */
-	public int getChosenIndexOfOldUpdate(int oldStep)
+	public int getChosenIndexOfOldUpdate(int step)
 	{
-		return path.getChoice(oldStep);
+		return path.getChoice(step);
 	}
 
 	/**

prism/src/simulator/TransitionList.java

@@ -33,7 +33,7 @@ import prism.*;
 
 public class TransitionList
 {
-	public ArrayList<Choice> transitions = new ArrayList<Choice>();
+	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;
@@ -42,7 +42,7 @@ public class TransitionList
 
 	public void clear()
 	{
-		transitions.clear();
+		choices.clear();
 		transitionIndices.clear();
 		transitionOffsets.clear();
 		numChoices = 0;
@@ -53,10 +53,10 @@ public class TransitionList
 	public void add(Choice tr)
 	{
 		int i, n;
-		transitions.add(tr);
+		choices.add(tr);
 		n = tr.size();
 		for (i = 0; i < n; i++) {
-			transitionIndices.add(transitions.size() - 1);
+			transitionIndices.add(choices.size() - 1);
 			transitionOffsets.add(i);
 		}
 		numChoices++;
@@ -64,30 +64,52 @@ public class TransitionList
 		probSum += tr.getProbabilitySum();
 	}
 
-	// get ith choice
+	// Get access to Choice objects 
+	
+	/**
+	 * Get the ith choice.
+	 */
 	public Choice getChoice(int i)
 	{
-		return transitions.get(i);
+		return choices.get(i);
 	}
 
-	// get choice containing ith transition
+	/**
+	 * Get the choice containing the ith transition.
+	 */
 	public Choice getChoiceOfTransition(int i)
 	{
-		return transitions.get(transitionIndices.get(i));
+		return choices.get(transitionIndices.get(i));
 	}
 
-	// get index of choice containing ith transition
+	// Get index/offset info
+	
+	/**
+	 * Get the index of the choice containing the ith transition. 
+	 */
 	public int getChoiceIndexOfTransition(int i)
 	{
 		return transitionIndices.get(i);
 	}
 
-	// get offset in choice containing ith transition
+	/**
+	 * Get the offset of the ith transition within its containing choice.
+	 */
 	public int getChoiceOffsetOfTransition(int i)
 	{
 		return transitionOffsets.get(i);
 	}
 
+	/**
+	 * Get the (total) index of a transition from the index of its containing choice and its offset within it.
+	 */
+	public int getTotalIndexOfTransition(int i, int offset)
+	{
+		return transitionOffsets.get(i);
+	}
+
+	// Access to transition info
+	
 	// get prob (or rate) of ith transition
 	public double getTransitionProbability(int i)
 	{
@@ -114,7 +136,7 @@ public class TransitionList
 	public String toString()
 	{
 		String s = "";
-		for (Choice tr : transitions)
+		for (Choice tr : choices)
 			s += tr.toString();
 		return s;
 	}

prism/src/simulator/Updater.java

@@ -40,6 +40,7 @@ public class Updater
 
 	// Model to which the path corresponds
 	protected ModulesFile modulesFile;
+	protected ModelType modelType;
 	protected int numModules;
 	// Synchronising action info
 	protected Vector<String> synchs;
@@ -58,6 +59,7 @@ public class Updater
 		this.simulator = simulator;
 		prism = simulator.getPrism();
 		this.modulesFile = modulesFile;
+		modelType = modulesFile.getModelType();
 		numModules = modulesFile.getNumModules();
 		synchs = modulesFile.getSynchs();
 		numSynchs = synchs.size();
@@ -107,9 +109,10 @@ public class Updater
 		System.out.println("updateLists: " + updateLists);
 
 		// Combination of updates depends on model type
-		switch (modulesFile.getModelType()) {
+		switch (modelType) {
 
 		case DTMC:
+		case CTMC:
 			ch = new ChoiceListFlexi();
 			n = 0;
 			// Independent choices for each (enabled) module
@@ -194,13 +197,13 @@ public class Updater
 			break;
 
 		default:
-			throw new PrismException("Unhandled model type \"" + modulesFile.getModelType() + "\"");
+			throw new PrismException("Unhandled model type \"" + modelType + "\"");
 		}
 
 		// For DTMCs, need to randomise
 
 		//System.out.println(transitionList.transitionTotal);
-		System.out.println(transitionList.transitions);
+		System.out.println(transitionList.choices);
 		//System.out.println(transitionList.transitionIndices);
 		//System.out.println(transitionList.transitionOffsets);
 
@@ -224,8 +227,8 @@ public class Updater
 			list.add(ups.getUpdate(i));
 			ch.add("", p, list, ups.getParent());
 		}
-		// Check distribution sums to 1
-		if (Math.abs(sum - 1) > prism.getSumRoundOff()) {
+		// Check distribution sums to 1 (if required)
+		if (modelType.choicesSumToOne() && Math.abs(sum - 1) > prism.getSumRoundOff()) {
 			throw new PrismLangException("Probabilities sum to " + sum + " in state " + state.toString(modulesFile), ups);
 		}
 
@@ -247,8 +250,8 @@ public class Updater
 			list.add(ups.getUpdate(i));
 			ch.add("", p, list, ups.getParent());
 		}
-		// Check distribution sums to 1
-		if (Math.abs(sum - 1) > prism.getSumRoundOff()) {
+		// Check distribution sums to 1 (if required)
+		if (modelType.choicesSumToOne() && Math.abs(sum - 1) > prism.getSumRoundOff()) {
 			throw new PrismLangException("Probabilities sum to " + sum + " in state " + state);
 		}
 

prism/src/userinterface/simulator/GUISimulator.java

@@ -619,6 +619,9 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 	public void a_manualUpdate()
 	{
 		try {
+			if (currentUpdatesTable.getSelectedRow() == -1)
+				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) {
 					displayPathLoops = false;
@@ -638,10 +641,11 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 				//Double.parseDouble(stateTimeField.getText());
 
 				setComputing(true);
-
-				if (currentUpdatesTable.getSelectedRow() == -1)
-					throw new PrismException("No current update is selected");
+				if (time == -1) {
+					engine.manualUpdate(currentUpdatesTable.getSelectedRow());
+				} else {
 					engine.manualUpdate(currentUpdatesTable.getSelectedRow(), time);
+				}
 
 				pathTableModel.updatePathTable();
 				updateTableModel.updateUpdatesTable();
@@ -657,8 +661,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 			} else {
 
 				setComputing(true);
-				if (currentUpdatesTable.getSelectedRow() == -1)
-					throw new PrismException("No current update is selected");
+				
 				engine.manualUpdate(currentUpdatesTable.getSelectedRow());
 
 				pathTableModel.updatePathTable();
@@ -2183,6 +2186,37 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 		}
 	}
 
+	public class ActionValue
+	{
+		private String value;
+		private boolean actionValueUnknown;
+
+		public ActionValue(String value)
+		{
+			this.value = value;
+		}
+
+		public String getValue()
+		{
+			return value;
+		}
+
+		public void setValue(String value)
+		{
+			this.value = value;
+		}
+
+		public void setActionValueUnknown(boolean unknown)
+		{
+			this.actionValueUnknown = unknown;
+		}
+
+		public boolean isActionValueUnknown()
+		{
+			return this.actionValueUnknown;
+		}
+	}
+
 	public class TimeValue
 	{
 		private Double value;
@@ -2714,6 +2748,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 		private RewardStructureValue rewardStructureValue;
 		private VariableValue variableValue;
 		private TimeValue timeValue;
+		private ActionValue actionValue;
 
 		public PathTableModel(SimulationView view)
 		{
@@ -3113,7 +3148,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 
 				// The step column
 				if (stepStart <= columnIndex && columnIndex < actionStart) {
-					return "Step index";
+					return "Index of state in path";
 				} else if (actionStart <= columnIndex && columnIndex < timeStart) {
 					return "Action label or module name";
 				} else if (timeStart <= columnIndex && columnIndex < cumulativeTimeStart) {
@@ -3159,13 +3194,14 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 				}
 				// The action column
 				else if (actionStart <= columnIndex && columnIndex < timeStart) {
-					return engine.getActionOfPathStep(rowIndex);
+					actionValue = new ActionValue(engine.getActionOfPathStep(rowIndex));
+					actionValue.setActionValueUnknown(rowIndex >= engine.getPathSize() - 1);
+					return actionValue;
 				}
 				// Time column
 				else if (timeStart <= columnIndex && columnIndex < cumulativeTimeStart) {
 					timeValue = new TimeValue(engine.getTimeSpentInPathState(rowIndex), false);
 					timeValue.setTimeValueUnknown(rowIndex >= engine.getPathSize() - 1);
-
 					return timeValue;
 				}
 				// Cumulative time column
@@ -3173,30 +3209,24 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 					timeValue = new TimeValue((rowIndex == 0) ? 0.0 : engine
 							.getCumulativeTimeSpentInPathState(rowIndex - 1), true);
 					timeValue.setTimeValueUnknown(rowIndex >= engine.getPathSize());
-
 					return timeValue;
 				}
 				// A variable column
 				else if (varStart <= columnIndex && columnIndex < rewardStart) {
 					Variable var = ((Variable) view.getVisibleVariables().get(columnIndex - varStart));
-
-					Type type = var.getType();
 					Object result = engine.getPathData(var.getIndex(), rowIndex);
 					variableValue.setVariable(var);
 					variableValue.setValue(result);
 					variableValue.setChanged(rowIndex == 0
 							|| !engine.getPathData(var.getIndex(), rowIndex - 1).equals(result));
-
 					return variableValue;
 				}
 				// A reward column
 				else if (rewardStart <= columnIndex) {
 					RewardStructureColumn rewardColumn = (RewardStructureColumn) view.getVisibleRewardColumns().get(
 							columnIndex - rewardStart);
-
 					rewardStructureValue.setRewardStructureColumn(rewardColumn);
 					rewardStructureValue.setRewardValueUnknown(false);
-
 					// A state reward column
 					if (rewardColumn.isStateReward()) {
 						double value = engine.getStateRewardOfPathState(rowIndex, rewardColumn.getRewardStructure()
@@ -3205,7 +3235,6 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 								|| value != engine.getStateRewardOfPathState(rowIndex - 1, rewardColumn
 										.getRewardStructure().getIndex()));
 						rewardStructureValue.setRewardValue(new Double(value));
-
 						rewardStructureValue.setRewardValueUnknown(rowIndex > engine.getPathSize() - 1);
 					}
 					// A transition reward column
@@ -3216,7 +3245,6 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 								|| value != engine.getTransitionRewardOfPathState(rowIndex - 1, rewardColumn
 										.getRewardStructure().getIndex()));
 						rewardStructureValue.setRewardValue(new Double(value));
-
 						rewardStructureValue.setRewardValueUnknown(rowIndex >= engine.getPathSize() - 1);
 					}
 					// A cumulative reward column
@@ -3241,7 +3269,6 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 							rewardStructureValue.setRewardValueUnknown(rowIndex >= engine.getPathSize());
 						}
 					}
-
 					return rewardStructureValue;
 				}
 			}

prism/src/userinterface/simulator/GUISimulatorPathTable.java

@@ -275,6 +275,20 @@ public class GUISimulatorPathTable extends GUIGroupedTable
 				stringValue = (String)value;
 				this.setToolTipText("State " + row);
 			}	
+			else if (value instanceof GUISimulator.ActionValue)
+			{	
+				GUISimulator.ActionValue actionValue = (GUISimulator.ActionValue)value;
+				if (actionValue.isActionValueUnknown())
+				{	
+					stringValue = "?";
+					this.setToolTipText("Action label or module name for transition from state " + (row) + " to " + (row + 1) + " (not yet known)");
+				}
+				else
+				{
+					stringValue = actionValue.getValue();
+					this.setToolTipText("Action label or module name for transition from state " + (row) + " to " + (row + 1));
+				}
+			}
 			else if (value instanceof GUISimulator.TimeValue)
 			{	
 				GUISimulator.TimeValue timeValue = (GUISimulator.TimeValue)value;
@@ -347,8 +361,8 @@ public class GUISimulatorPathTable extends GUIGroupedTable
 			width = (int)Math.ceil(rect.getWidth());
 			height = (int)Math.ceil(rect.getHeight());
 			
-			// State index
-			if (value instanceof String) {
+			// State index/action
+			if (value instanceof String || value instanceof GUISimulator.ActionValue) {
 				// Position (horiz centred, vert centred)
 	   			x = (getWidth()/2) - (width/2);
 	   			y = (getHeight()/2) + (height/2);