Simulator engine: Documentation of Choice object, remove some unused Choice methods, add some action-querying methods in SimulatorEngine.

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

prism/src/parser/ast/ModulesFile.java

@@ -352,11 +352,22 @@ public class ModulesFile extends ASTElement
 		return moduleNames;
 	}
 
+	/**
+	 * Get the list of action names.
+	 */
 	public Vector<String> getSynchs()
 	{
 		return synchs;
 	}
 
+	/**
+	 * Get the {@code i}th action name (0-indexed).
+	 */
+	public String getSynch(int i)
+	{
+		return synchs.get(i);
+	}
+
 	public boolean isSynch(String s)
 	{
 		if (synchs == null)

prism/src/simulator/Choice.java

@@ -31,20 +31,71 @@ import prism.*;
 
 public interface Choice
 {
-//	public void setAction(String action);
+	/**
+	 * Get the module/action for this choice, as an integer index
+	 * (-i for independent in ith module, i for synchronous on ith action)
+	 * (in both cases, modules/actions are 1-indexed)
+	 */
 	public int getModuleOrActionIndex();
+	
+	/**
+	 * Get the module/action for this choice, as a string
+	 * (form is "module" or "[action]")
+	 */
 	public String getModuleOrAction();
+	
+	/**
+	 * Get the number of transitions in this choice.
+	 */
 	public int size();
-	public double getProbability();
-	public double getProbability(int i);
-	public double getProbabilitySum();
+	
+	/**
+	 * 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;
+	
+	/**
+	 * 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 getUpdateStringFull(int i);
-	public State computeTarget(State currentState) throws PrismLangException;
-	public void computeTarget(State currentState, State newState) throws PrismLangException;
+	
+	/**
+	 * 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.
+	 */
 	public State computeTarget(int i, State currentState) throws PrismLangException;
+	
+	/**
+	 * 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.) 
+	 */
 	public void computeTarget(int i, State currentState, State newState) throws PrismLangException;
+	
+	/**
+	 * Get the probability/rate for the ith transition.
+	 */
+	public double getProbability(int i);
+	
+	/**
+	 * Get the sum of probabilities/rates for all transitions.
+	 */
+	public double getProbabilitySum();
+	
+	/**
+	 * 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 that and all prior transitions exceeds x.
+	 */
 	public int getIndexByProbabilitySum(double x);
+	
 	public void checkValid(ModelType modelType) throws PrismException;
 	
 	/**

prism/src/simulator/ChoiceListFlexi.java

@@ -153,20 +153,13 @@ public class ChoiceListFlexi implements Choice
 
 	// Get methods
 
-	/**
-	 * Get the module/action for this choice, as an integer index
-	 * (-i for independent in ith module, i for synchronous on ith action)
-	 * (in both cases, modules/actions are 1-indexed)
-	 */
+	@Override
 	public int getModuleOrActionIndex()
 	{
 		return moduleOrActionIndex;
 	}
 
-	/**
-	 * Get the module/action for this choice, as a string
-	 * (form is "module" or "[action]")
-	 */
+	@Override
 	public String getModuleOrAction()
 	{
 		// Action label (or absence of) will be the same for all updates in a choice
@@ -178,20 +171,13 @@ public class ChoiceListFlexi implements Choice
 			return "[" + c.getSynch() + "]";
 	}
 
-	/**
-	 * Get the number of transitions in this choice.
-	 */
+	@Override
 	public int size()
 	{
 		return probability.size();
 	}
 
-	/**
-	 * 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).
-	 */
+	@Override
 	public String getUpdateString(int i, State currentState) throws PrismLangException
 	{
 		int j, n;
@@ -210,13 +196,7 @@ public class ChoiceListFlexi implements Choice
 		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. 
-	 */
+	@Override
 	public String getUpdateStringFull(int i)
 	{
 		String s = "";
@@ -233,11 +213,7 @@ public class ChoiceListFlexi implements Choice
 		return s;
 	}
 
-	/**
-	 * 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.
-	 */
+	@Override
 	public State computeTarget(int i, State currentState) throws PrismLangException
 	{
 		State newState = new State(currentState);
@@ -246,42 +222,20 @@ public class ChoiceListFlexi implements Choice
 		return newState;
 	}
 
-	/**
-	 * 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.
-	 */
+	@Override
 	public void computeTarget(int i, State currentState, State newState) throws PrismLangException
 	{
 		for (Update up : updates.get(i))
 			up.update(currentState, newState);
 	}
 
-	public State computeTarget(State currentState) throws PrismLangException
-	{
-		return computeTarget(0, currentState);
-	}
-
-	public void computeTarget(State currentState, State newState) throws PrismLangException
-	{
-		computeTarget(0, currentState, newState);
-	}
-
-	/**
-	 * Get the probability rate for the ith transition.
-	 * NB: for efficiency, there are no bounds checks done on i.
-	 */
+	@Override
 	public double getProbability(int i)
 	{
 		return probability.get(i);
 	}
 
-	public double getProbability()
-	{
-		return getProbability(0);
-	}
-
+	@Override
 	public double getProbabilitySum()
 	{
 		double sum = 0.0;
@@ -290,11 +244,7 @@ public class ChoiceListFlexi implements Choice
 		return sum;
 	}
 
-	/**
-	 * 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 that and all prior transitions exceeds x.
-	 */
+	@Override
 	public int getIndexByProbabilitySum(double x)
 	{
 		int i, n;
@@ -325,6 +275,7 @@ public class ChoiceListFlexi implements Choice
 		}
 	}
 	
+	@Override
 	public String toString()
 	{
 		int i, n;

prism/src/simulator/SimulatorEngine.java

@@ -807,8 +807,8 @@ public class SimulatorEngine
 	}
 
 	/**
-	 * Get a string describing the action/module of a transition, specified by
-	 * its index/offset.
+	 * Get a string describing the action/module of a transition, specified by its index/offset.
+	 * (form is "module" or "[action]")
 	 */
 	public String getTransitionModuleOrAction(int i, int offset)
 	{
@@ -817,12 +817,53 @@ public class SimulatorEngine
 
 	/**
 	 * Get a string describing the action/module of a transition, specified by its index.
+	 * (form is "module" or "[action]")
 	 */
 	public String getTransitionModuleOrAction(int index)
 	{
 		return transitionList.getTransitionModuleOrAction(index);
 	}
 
+	/**
+	 * Get the index of the action/module of a transition, specified by its index/offset.
+	 * (-i for independent in ith module, i for synchronous on ith action)
+	 * (in both cases, modules/actions are 1-indexed)
+	 */
+	public int getTransitionModuleOrActionIndex(int i, int offset)
+	{
+		return transitionList.getTransitionModuleOrActionIndex(transitionList.getTotalIndexOfTransition(i, offset));
+	}
+
+	/**
+	 * Get the index of the action/module of a transition, specified by its index.
+	 * (-i for independent in ith module, i for synchronous on ith action)
+	 * (in both cases, modules/actions are 1-indexed)
+	 */
+	public int getTransitionModuleOrActionIndex(int index)
+	{
+		return transitionList.getTransitionModuleOrActionIndex(index);
+	}
+
+	/**
+	 * Get the action label of a transition as a string, specified by its index/offset.
+	 * (null for asynchronous/independent transitions)
+	 */
+	public String getTransitionAction(int i, int offset)
+	{
+		int a = transitionList.getTransitionModuleOrActionIndex(transitionList.getTotalIndexOfTransition(i, offset));
+		return a < 0 ? null : modulesFile.getSynch(a - 1);
+	}
+
+	/**
+	 * Get the action label of a transition as a string, specified by its index.
+	 * (null for asynchronous/independent transitions)
+	 */
+	public String getTransitionAction(int index)
+	{
+		int a = transitionList.getTransitionModuleOrActionIndex(index);
+		return a < 0 ? null : modulesFile.getSynch(a - 1);
+	}
+
 	/**
 	 * Get the probability/rate of a transition within a choice, specified by its index/offset.
 	 */

prism/src/simulator/TransitionList.java

@@ -179,12 +179,23 @@ public class TransitionList
 
 	/**
 	 * Get a string describing the action/module of a transition, specified by its index.
+	 * (form is "module" or "[action]")
 	 */
 	public String getTransitionModuleOrAction(int index)
 	{
 		return getChoiceOfTransition(index).getModuleOrAction();
 	}
 
+	/**
+	 * Get the index of the action/module of a transition, specified by its index.
+	 * (-i for independent in ith module, i for synchronous on ith action)
+	 * (in both cases, modules/actions are 1-indexed)
+	 */
+	public int getTransitionModuleOrActionIndex(int index)
+	{
+		return getChoiceOfTransition(index).getModuleOrActionIndex();
+	}
+
 	/**
 	 * Get the probability/rate of a transition, specified by its index.
 	 */