SimulateTransSet Struct Reference

Pubic interface for class SimulateTransSet. More...

#include <simulateTransSet.h>

Related Functions
(Note that these are not member functions.)
SimulateTransSet_ptr	SimulateTransSet_create (BddFsm_ptr fsm, BddEnc_ptr enc, bdd_ptr from_state, bdd_ptr next_states_set, double next_states_count)
	Class constructor.
void	SimulateTransSet_destroy (SimulateTransSet_ptr self)
	Class destructor.
bdd_ptr	SimulateTransSet_get_from_state (const SimulateTransSet_ptr self)
	Getter for the state the transition set is originating from.
bdd_ptr	SimulateTransSet_get_input_at_state (const SimulateTransSet_ptr self, int state_index, int input_index)
	Returns the Ith input from the set of inputs going to the Nth state in the set of target states.
int	SimulateTransSet_get_inputs_num_at_state (const SimulateTransSet_ptr self, int state_index)
	Returns the cardinality of the inputs set going to a given state, represented by its index in the set of target states.
bdd_ptr	SimulateTransSet_get_next_state (const SimulateTransSet_ptr self, int state_index)
	Returns the Nth element of the target set of states.
int	SimulateTransSet_get_next_state_num (const SimulateTransSet_ptr self)
	Returns the cardinality of the target set of states.
void	SimulateTransSet_get_state_input_at (const SimulateTransSet_ptr self, int index, bdd_ptr *state, bdd_ptr *input)
	Index is the number corresponding to the index the user chose after having seen the result of the print method. state and input will contain referenced bdds representing the chose state-input pair, but input might be NULL for the initial state.
void	SimulateTransSet_get_state_input_det (const SimulateTransSet_ptr self, bdd_ptr *state, bdd_ptr *input)
void	SimulateTransSet_get_state_input_rand (const SimulateTransSet_ptr self, bdd_ptr *state, bdd_ptr *input)
int	SimulateTransSet_print (const SimulateTransSet_ptr self, boolean show_changes_only, OStream_ptr output)
	Returned value is the maximum index that can be chosen by user in interactive mode.

---

Detailed Description

Pubic interface for class SimulateTransSet.

Author:

Roberto Cavada

Todo:

: Missing description

Holds information about states and associated transitions. Used during interactive simulation only. During simulation several actions can be taken, with associated states. This structure holds a set of future states the simulation can go in, and for each future state it holds a set of associated inputs. This structure is privately used by the function that must take a choice about the next state/input pair during simulation

---

Friends And Related Function Documentation

SimulateTransSet_ptr SimulateTransSet_create	(	BddFsm_ptr	fsm,
		BddEnc_ptr	enc,
		bdd_ptr	from_state,
		bdd_ptr	next_states_set,
		double	next_states_count
	)			[related]

Class constructor.

from_state can be NULL when the set of initial states must be queried. next_states_count is checked to be in (1,INT_MAX)

void SimulateTransSet_destroy

(

SimulateTransSet_ptr

self

)

[related]

Class destructor.

bdd_ptr SimulateTransSet_get_from_state

(

const SimulateTransSet_ptr

self

)

[related]

Getter for the state the transition set is originating from.

Returned BDD is referenced. NULL can be returned if this transition set target states are the initial states set

bdd_ptr SimulateTransSet_get_input_at_state	(	const SimulateTransSet_ptr	self,
		int	state_index,
		int	input_index
	)			[related]

Returns the Ith input from the set of inputs going to the Nth state in the set of target states.

int SimulateTransSet_get_inputs_num_at_state	(	const SimulateTransSet_ptr	self,
		int	state_index
	)			[related]

Returns the cardinality of the inputs set going to a given state, represented by its index in the set of target states.

Returned BDD is referenced. NULL can be returned if self represent the initial states set

bdd_ptr SimulateTransSet_get_next_state	(	const SimulateTransSet_ptr	self,
		int	state_index
	)			[related]

Returns the Nth element of the target set of states.

Returned BDD is referenced

int SimulateTransSet_get_next_state_num

(

const SimulateTransSet_ptr

self

)

[related]

Returns the cardinality of the target set of states.

void SimulateTransSet_get_state_input_at	(	const SimulateTransSet_ptr	self,
		int	index,
		bdd_ptr *	state,
		bdd_ptr *	input
	)			[related]

Index is the number corresponding to the index the user chose after having seen the result of the print method. state and input will contain referenced bdds representing the chose state-input pair, but input might be NULL for the initial state.

void SimulateTransSet_get_state_input_det	(	const SimulateTransSet_ptr	self,
		bdd_ptr *	state,
		bdd_ptr *	input
	)			[related]

void SimulateTransSet_get_state_input_rand	(	const SimulateTransSet_ptr	self,
		bdd_ptr *	state,
		bdd_ptr *	input
	)			[related]

int SimulateTransSet_print	(	const SimulateTransSet_ptr	self,
		boolean	show_changes_only,
		OStream_ptr	output
	)			[related]

Returned value is the maximum index that can be chosen by user in interactive mode.

---

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

• NuSMV/code/nusmv/core/simulate/simulateTransSet.h