Inheritance diagram for stamina.InfCTMCModelGenerator:

Public Member Functions
	InfCTMCModelGenerator (ModulesFile modulesFile) throws PrismException

	InfCTMCModelGenerator (ModulesFile modulesFile, PrismComponent parent) throws PrismException

State	getAbsorbingState ()

void	setReachabilityThreshold (double th)

void	setPropertyExpression (ExpressionTemporal expr)

void	clearPerimeterStatesVector ()

Vector< String >	getPerimeterStatesVector ()

HashMap< State, ProbState >	getGlobalStateSet ()

boolean	finalModelHasAbsorbing ()

ModelType	getModelType ()

void	setSomeUndefinedConstants (Values someValues) throws PrismException

void	setSomeUndefinedConstants (Values someValues, boolean exact) throws PrismException

Values	getConstantValues ()

boolean	containsUnboundedVariables ()

int	getNumVars ()

List< String >	getVarNames ()

List< Type >	getVarTypes ()

int	getNumLabels ()

List< String >	getLabelNames ()

String	getLabelName (int i) throws PrismException

int	getLabelIndex (String label)

int	getNumRewardStructs ()

List< String >	getRewardStructNames ()

int	getRewardStructIndex (String name)

RewardStruct	getRewardStruct (int i)

boolean	hasSingleInitialState () throws PrismException

State	getInitialState () throws PrismException

State	getInitialStateForTransitionFile () throws PrismException

List< State >	getInitialStates () throws PrismException

List< State >	getInitialStatesForTransitionFile () throws PrismException

void	exploreState (State exploreState) throws PrismException

State	getExploreState ()

int	getNumChoices () throws PrismException

int	getNumTransitions () throws PrismException

int	getNumTransitions (int index) throws PrismException

String	getTransitionAction (int index) throws PrismException

String	getTransitionAction (int index, int offset) throws PrismException

String	getChoiceAction (int index) throws PrismException

double	getTransitionProbability (int index, int offset) throws PrismException

double	getTransitionProbability (int index) throws PrismException

State	computeTransitionTarget (int index, int offset) throws PrismException

State	computeTransitionTarget (int index) throws PrismException

boolean	isLabelTrue (int i) throws PrismException

double	getStateReward (int r, State state) throws PrismException

double	getStateActionReward (int r, State state, Object action) throws PrismException

void	calculateStateRewards (State state, double[] store) throws PrismLangException

VarList	createVarList ()

void	getRandomInitialState (RandomNumberGenerator rng, State initialState) throws PrismException

boolean	rewardStructHasTransitionRewards (int i)

void	doReachabilityAnalysis () throws PrismException

Protected Attributes
PrismComponent	parent

Updater	updater

TransitionList	transitionList

boolean	transitionListBuilt

Constructor & Destructor Documentation

◆ InfCTMCModelGenerator() [1/2]

stamina.InfCTMCModelGenerator.InfCTMCModelGenerator ( ModulesFile modulesFile ) throws PrismException

inline

Build a ModulesFileModelGenerator for a particular PRISM model, represented by a ModuleFile instance.

Parameters

modulesFile The PRISM model

◆ InfCTMCModelGenerator() [2/2]

stamina.InfCTMCModelGenerator.InfCTMCModelGenerator	(	ModulesFile	modulesFile,
		PrismComponent	parent
	)		throws PrismException

inline

Build a ModulesFileModelGenerator for a particular PRISM model, represented by a ModuleFile instance.

Parameters

modulesFile The PRISM model

Member Function Documentation

◆ calculateStateRewards()

void stamina.InfCTMCModelGenerator.calculateStateRewards	(	State	state,
		double[]	store
	)		throws PrismLangException

inline

Calculates the state rewards associated with a specific state and store array.

Parameters

state	The state the rewards are associated with
store	The array of stored probabilities. TODO: not 100% sure this is correct

Exceptions

PrismLangException

◆ clearPerimeterStatesVector()

void stamina.InfCTMCModelGenerator.clearPerimeterStatesVector ( )

inline

Clears the perimeter states vector

◆ computeTransitionTarget() [1/2]

State stamina.InfCTMCModelGenerator.computeTransitionTarget ( int index ) throws PrismException

inline

Computes the transition target just based on a single index.

Parameters

index The index of the choice.

Returns: TODO: not implemented

Exceptions

PrismException

◆ computeTransitionTarget() [2/2]

State stamina.InfCTMCModelGenerator.computeTransitionTarget	(	int	index,
		int	offset
	)		throws PrismException

inline

Computes the target state of a transition from the current state based on the transition list. If state is absorbing, will always return a pointer to the current state.

Parameters

index	The index of the choice.
offset	The offset from that index to compute the target state for.

Returns: The state we will be travelling to.

Exceptions

PrismException

◆ containsUnboundedVariables()

boolean stamina.InfCTMCModelGenerator.containsUnboundedVariables ( )

inline

Checks to see if the modules file contains unbounded variables.

Returns: Whether or not there are unbounded variables

◆ createVarList()

VarList stamina.InfCTMCModelGenerator.createVarList ( )

inline

Provides the list of variables associated with the PRISM model. TODO: why is this named createVarList() and not getVarList()?

Returns: The list of variables.

◆ doReachabilityAnalysis()

void stamina.InfCTMCModelGenerator.doReachabilityAnalysis ( ) throws PrismException

inline

Does reachability analysis and truncates state space based on values of Kappa (κ), and its reduction factor. This method performs a breadth first search to find most of the probability mass of the state space.

Exceptions

PrismException Does not support anything other than CTMCs.

◆ exploreState()

void stamina.InfCTMCModelGenerator.exploreState ( State exploreState ) throws PrismException

inline

Explores a particular state. If it's an absorbing state, clears its transition list, otherwise, it calculates a transition list for it.

Parameters

exploreState The state to explore.

Exceptions

PrismException

◆ finalModelHasAbsorbing()

boolean stamina.InfCTMCModelGenerator.finalModelHasAbsorbing ( )

inline

Determines if the final (truncated) model has absorbing states

Returns: a boolean value reflective of whether or not absorbing states exist in the final model.

◆ getAbsorbingState()

State stamina.InfCTMCModelGenerator.getAbsorbingState ( )

inline

Returns: The absorbingState for this model

◆ getChoiceAction()

String stamina.InfCTMCModelGenerator.getChoiceAction ( int index ) throws PrismException

inline

Gets the choice action at an index. TODO: Why does this return null?

Parameters

index Index to look at.

Returns: null

Exceptions

PrismException

◆ getConstantValues()

Values stamina.InfCTMCModelGenerator.getConstantValues ( )

inline

Gets the constant values associated with this PRISM model

Returns: The constant values

◆ getExploreState()

State stamina.InfCTMCModelGenerator.getExploreState ( )

inline

Gets the state the model generator is about to explore.

Returns: The state we are about to explore.

◆ getGlobalStateSet()

HashMap< State, ProbState > stamina.InfCTMCModelGenerator.getGlobalStateSet ( )

inline

Gets the global state set.

Returns: A hash map containing all states in the global state set.

◆ getInitialState()

State stamina.InfCTMCModelGenerator.getInitialState ( ) throws PrismException

inline

Gets the default initial state after model truncation.

Returns: The default initial state.

Exceptions

PrismException

◆ getInitialStateForTransitionFile()

State stamina.InfCTMCModelGenerator.getInitialStateForTransitionFile ( ) throws PrismException

inline

Gets initial state for transition file.

Returns: Initial state for transition matrix file.

Exceptions

PrismException

◆ getInitialStates()

List< State > stamina.InfCTMCModelGenerator.getInitialStates ( ) throws PrismException

inline

Gets all initial states after model truncation.

Returns: A List of type State with all of the initial states.

Exceptions

PrismException

◆ getInitialStatesForTransitionFile()

List< State > stamina.InfCTMCModelGenerator.getInitialStatesForTransitionFile ( ) throws PrismException

inline

Gets all initial states for transition matrix file.

Returns: A List of type State that contains all of the initial states for a transition file.

Exceptions

PrismException

◆ getLabelIndex()

int stamina.InfCTMCModelGenerator.getLabelIndex ( String label )

inline

Given a string with a desired label name, gets the index corresponding to that label.

Parameters

label The name of the label.

Returns: The index of the label.

◆ getLabelName()

String stamina.InfCTMCModelGenerator.getLabelName ( int i ) throws PrismException

inline

Gets a label name at a particular index.

Parameters

i	The index of the label name to get.

Returns: The label at index i.

Exceptions

PrismException

◆ getLabelNames()

List< String > stamina.InfCTMCModelGenerator.getLabelNames ( )

inline

Gets the label names.

Returns: A List of type String with the label names.

◆ getModelType()

ModelType stamina.InfCTMCModelGenerator.getModelType ( )

inline

Gets the model type

Returns: the model type

◆ getNumChoices()

int stamina.InfCTMCModelGenerator.getNumChoices ( ) throws PrismException

inline

Gets the number of choices available for the state we are about to explore.

Returns: The number of choices available.

Exceptions

PrismException

◆ getNumLabels()

int stamina.InfCTMCModelGenerator.getNumLabels ( )

inline

Gets the number of labels.

Returns: The number of labels as int.

◆ getNumRewardStructs()

int stamina.InfCTMCModelGenerator.getNumRewardStructs ( )

inline

Gets the number of rewards structs.

Returns: The number of rewards structs in the PRISM model.

◆ getNumTransitions() [1/2]

int stamina.InfCTMCModelGenerator.getNumTransitions ( ) throws PrismException

inline

Gets the number of transitions for the current state.

Returns: Not implemented.

Exceptions

PrismException

◆ getNumTransitions() [2/2]

int stamina.InfCTMCModelGenerator.getNumTransitions ( int index ) throws PrismException

inline

Gets the number of transitions for the choice at a specific index in the transitions list.

Parameters

index The index of the choice within the transition list to look at.

Returns: The number of transitions associated with that choice.

Exceptions

PrismException

◆ getNumVars()

int stamina.InfCTMCModelGenerator.getNumVars ( )

inline

Gets the number of variables in the PRISM modules file.

Returns: The number of variables

◆ getPerimeterStatesVector()

Vector< String > stamina.InfCTMCModelGenerator.getPerimeterStatesVector ( )

inline

Gets a pointer to a vector containing all perimter states

Returns: Perimeter states (in the format of a Vector<String>)

◆ getRandomInitialState()

void stamina.InfCTMCModelGenerator.getRandomInitialState	(	RandomNumberGenerator	rng,
		State	initialState
	)		throws PrismException

inline

Gets a random initial state given a random number generator.

Parameters

rng	The RandomNumberGenerator to pass into the method.
initialState	A pointer to the current initial state.

Exceptions

PrismException Multiple initial states not yet supported.

◆ getRewardStruct()

RewardStruct stamina.InfCTMCModelGenerator.getRewardStruct ( int i )

inline

Gets a particular reward struct at an index.

Parameters

i	The index of the reward struct desired.

Returns: The RewardStruct at index i.

◆ getRewardStructIndex()

int stamina.InfCTMCModelGenerator.getRewardStructIndex ( String name )

inline

Given a name of a rewards structure, gets the index of that rewards structure.

Parameters

name	The name of the rewards structure.

Returns: The index corresponding to the name.

◆ getRewardStructNames()

List< String > stamina.InfCTMCModelGenerator.getRewardStructNames ( )

inline

Gets all rewards structure names.

Returns: A List of type String with the reward structure names.

◆ getStateActionReward()

double stamina.InfCTMCModelGenerator.getStateActionReward	(	int	r,
		State	state,
		Object	action
	)		throws PrismException

inline

Gets the rewards from a rewards structure witha specific index associated with being at a certain state and taking a certain action.

Parameters

r	The index of the rewards structure.
state	The state we are at.
action	The action we wish to take.

Returns: The total reward associated with that state-action combination.

Exceptions

PrismException

◆ getStateReward()

double stamina.InfCTMCModelGenerator.getStateReward	(	int	r,
		State	state
	)		throws PrismException

inline

Gets the total state reward at a specific index of rewards structure and a specific state.

Parameters

r	The index of the reward structure.
state	The state to evaluate the rewards structure at.

Returns: The total state reward at the given state.

Exceptions

PrismException

◆ getTransitionAction() [1/2]

String stamina.InfCTMCModelGenerator.getTransitionAction ( int index ) throws PrismException

inline

Gets the action of the transition list at an index. If no transition list exists then it means that state is absorbing, so returns [Absorbing_State]

Parameters

index The index of the transition list to get.

Returns: The transition action in the form of a String.

Exceptions

PrismException

◆ getTransitionAction() [2/2]

String stamina.InfCTMCModelGenerator.getTransitionAction	(	int	index,
		int	offset
	)		throws PrismException

inline

Gets the action of the transition list at an index and offset. If no transition list exists then state is absorbing, so returns [Absorbing_State].

Parameters

index	The index to look at.
offset	The offset to look at.

Returns: The action at that location of the transition list.

Exceptions

PrismException

◆ getTransitionProbability() [1/2]

double stamina.InfCTMCModelGenerator.getTransitionProbability ( int index ) throws PrismException

inline

Gets the transition probability using just an index.

Parameters

index The index to get the transition probability.

Returns: The probability. TODO: not implemented.

Exceptions

PrismException

◆ getTransitionProbability() [2/2]

double stamina.InfCTMCModelGenerator.getTransitionProbability	(	int	index,
		int	offset
	)		throws PrismException

inline

Gets the probability that a particular choice and offset are taken. If the transistion list is not built, then the state is absorbing and the probability is 1.0.

Parameters

index	The index of the choice.
offset	The offset of the choice to get the probability from.

Returns: The probability of transition.

Exceptions

PrismException

◆ getVarNames()

List< String > stamina.InfCTMCModelGenerator.getVarNames ( )

inline

Gets the variable names from the modules file.

Returns: A List of type String with the variable names in it.

◆ getVarTypes()

List< Type > stamina.InfCTMCModelGenerator.getVarTypes ( )

inline

Gets the types of each variable corresponding to the modules file.

Returns: A List of type Type with the variable types in it.

◆ hasSingleInitialState()

boolean stamina.InfCTMCModelGenerator.hasSingleInitialState ( ) throws PrismException

inline

Checks to see if there is an initial state.

Returns: boolean indicating whether or not there is a single initial state.

Exceptions

PrismException

◆ isLabelTrue()

boolean stamina.InfCTMCModelGenerator.isLabelTrue ( int i ) throws PrismException

inline

Evaluates a label at an index and indicates whether it is currently true for the exploreState

Parameters

i	The index of the label.

Returns: Whether or not that label is currently true.

Exceptions

PrismException

◆ rewardStructHasTransitionRewards()

boolean stamina.InfCTMCModelGenerator.rewardStructHasTransitionRewards ( int i )

inline

Determines if a rewards structure at a specific index has transition rewards.

Parameters

i	The index of the rewards structure.

Returns: Whether or not that structure has transition rewards associated with it.

◆ setPropertyExpression()

void stamina.InfCTMCModelGenerator.setPropertyExpression ( ExpressionTemporal expr )

inline

Set the property description

Parameters

expr	(ExpressionTemporal) The property expression to set.

◆ setReachabilityThreshold()

void stamina.InfCTMCModelGenerator.setReachabilityThreshold ( double th )

inline

set reachability threshold

Parameters

th	(double) The new reachability threshold to set

◆ setSomeUndefinedConstants() [1/2]

void stamina.InfCTMCModelGenerator.setSomeUndefinedConstants ( Values someValues ) throws PrismException

inline

Sets constants which are undefined by the PRISM file passed in. This corresponds to the -const parameter passed into the stamina binary. This function is a wrapper for setSomeUndefinedConstants(Values, boolean)

Parameters

someValues The values to be passed in.

Exceptions

PrismException

◆ setSomeUndefinedConstants() [2/2]

void stamina.InfCTMCModelGenerator.setSomeUndefinedConstants	(	Values	someValues,
		boolean	exact
	)		throws PrismException

inline

Sets constants undefined by the PRISM file passed in. This corresponds to the -const parameter and allows the constants to be defined as exact or not.

Parameters

someValues	The values to be passed in.
exact	are these constants exact?

Exceptions

PrismException

The documentation for this class was generated from the following file:

/home/josh/Documents/Work/Research/stamina/stamina/src/stamina/InfCTMCModelGenerator.java

Public Member Functions

Protected Attributes

Constructor & Destructor Documentation

◆ InfCTMCModelGenerator() [1/2]

◆ InfCTMCModelGenerator() [2/2]

Member Function Documentation

◆ calculateStateRewards()

◆ clearPerimeterStatesVector()

◆ computeTransitionTarget() [1/2]

◆ computeTransitionTarget() [2/2]

◆ containsUnboundedVariables()

◆ createVarList()

◆ doReachabilityAnalysis()

◆ exploreState()

◆ finalModelHasAbsorbing()

◆ getAbsorbingState()

◆ getChoiceAction()

◆ getConstantValues()

◆ getExploreState()

◆ getGlobalStateSet()

◆ getInitialState()

◆ getInitialStateForTransitionFile()

◆ getInitialStates()

◆ getInitialStatesForTransitionFile()

◆ getLabelIndex()

◆ getLabelName()

◆ getLabelNames()

◆ getModelType()

◆ getNumChoices()

◆ getNumLabels()

◆ getNumRewardStructs()

◆ getNumTransitions() [1/2]

◆ getNumTransitions() [2/2]

◆ getNumVars()

◆ getPerimeterStatesVector()

◆ getRandomInitialState()

◆ getRewardStruct()

◆ getRewardStructIndex()

◆ getRewardStructNames()

◆ getStateActionReward()

◆ getStateReward()

◆ getTransitionAction() [1/2]

◆ getTransitionAction() [2/2]

◆ getTransitionProbability() [1/2]

◆ getTransitionProbability() [2/2]

◆ getVarNames()

◆ getVarTypes()

◆ hasSingleInitialState()

◆ isLabelTrue()

◆ rewardStructHasTransitionRewards()

◆ setPropertyExpression()

◆ setReachabilityThreshold()

◆ setSomeUndefinedConstants() [1/2]

◆ setSomeUndefinedConstants() [2/2]