int
CommandGotoState(
int argc,
char ** argv
)
- Goes to a given state of a trace
- Side Effects state became the current state.
- Defined in
simulateCmd.c
int
CommandPickState(
int argc,
char ** argv
)
- Picks a state from the set of initial states
- Side Effects The state chosen is stored in the traces_hash table as
the first state of a new trace
- See Also
goto_state
simulate
- Defined in
simulateCmd.c
int
CommandPrintCurrentState(
int argc,
char ** argv
)
- Prints the current state
- Defined in
simulateCmd.c
int
CommandSimulate(
int argc,
char ** argv
)
- Performs a simulation from the current selected state
- Side Effects Generated referenced states traces are stored to be
analyzed by the user in a second time
- See Also
pick_state
goto_state
- Defined in
simulateCmd.c
SimulateTransSet_ptr
SimulateTransSet_create(
BddFsm_ptr fsm,
BddEnc_ptr enc,
bdd_ptr from_state,
bdd_ptr next_states_set,
double next_states_count
)
- 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)
- Defined in
simulateTransSet.c
void
SimulateTransSet_destroy(
SimulateTransSet_ptr self
)
- Class destructor
- Defined in
simulateTransSet.c
bdd_ptr
SimulateTransSet_get_from_state(
const SimulateTransSet_ptr self
)
- Returned BDD is referenced. NULL can be returned if
this transition set target states are the initial states set
- Defined in
simulateTransSet.c
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
- Defined in
simulateTransSet.c
int
SimulateTransSet_get_inputs_num_at_state(
const SimulateTransSet_ptr self,
int state_index
)
- Returned BDD is referenced. NULL can be returned
if self represent the initial states set
- Defined in
simulateTransSet.c
int
SimulateTransSet_get_next_state_num(
const SimulateTransSet_ptr self
)
- Returns the cardinality of the target set of states
- Defined in
simulateTransSet.c
bdd_ptr
SimulateTransSet_get_next_state(
const SimulateTransSet_ptr self,
int state_index
)
- Returned BDD is referenced
- Defined in
simulateTransSet.c
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
- Defined in
simulateTransSet.c
void
SimulateTransSet_get_state_input_det(
const SimulateTransSet_ptr self,
bdd_ptr* state,
bdd_ptr* input
)
-
- Defined in
simulateTransSet.c
void
SimulateTransSet_get_state_input_rand(
const SimulateTransSet_ptr self,
bdd_ptr* state,
bdd_ptr* input
)
-
- Defined in
simulateTransSet.c
int
SimulateTransSet_print(
const SimulateTransSet_ptr self,
boolean show_changes_only,
FILE* output
)
- Returned value is the maximum index that can be chosen by
user in interactive mode
- Defined in
simulateTransSet.c
void
Simulate_ChooseOneStateInput(
BddFsm_ptr fsm,
bdd_ptr from_state,
bdd_ptr next_set,
Simulation_Mode mode,
int display_all,
bdd_ptr* input,
bdd_ptr* state
)
-
- Defined in
simulate.c
bdd_ptr
Simulate_ChooseOneState(
BddFsm_ptr fsm,
bdd_ptr next_set,
Simulation_Mode mode,
int display_all
)
- Chooses a state among future states depending on the
given simulation policy (random, deterministic or interactive). In case of
interactive simulation, the system stops and allows the user to pick
a state from a list of possible items. If the number of future states
is too high, the system requires some further constraints to limit that
number and will asks for them until the number of states is lower than
an internal threshold. Entered expressions are accumulated in one big
constraint used only in the actual step of the simulation. It will be
discarded after a state will be chosen.
- Side Effects A referenced state (BDD) is returned. NULL if failed.
- See Also
Simulate_MultipleStep
- Defined in
simulate.c
int
Simulate_CmdPickOneState(
BddFsm_ptr fsm,
Simulation_Mode mode,
int display_all,
char * strConstr
)
- optional
- Side Effects required
- See Also
optional
- Defined in
simulate.c
void
Simulate_End(
)
- Quits the simulate package
- Defined in
simulateCmd.c
void
Simulate_Init(
)
- Initializes the simulate package.
- Defined in
simulateCmd.c
node_ptr
Simulate_MultipleSteps(
BddFsm_ptr fsm,
bdd_ptr constraint,
boolean time_shift,
Simulation_Mode mode,
int n,
int display_all
)
- Multiple step simulation: loops n times over the choice of
a state according to the picking policy given at command line. It returns a
list of at least n+1 referenced states (the first one is always the "current
state" from which any simulation must start). The obtained list can contain
a minor number of states if there are no future states at some point.
- See Also
Simulate_ChooseOneState
- Defined in
simulate.c
bdd_ptr
simulate_accumulate_constraints(
BddEnc_ptr enc,
bdd_ptr bdd,
int max_size
)
- There are 4 condition to be verified in order to accept
new further constraints:
1) entered expression must be a non-zero set;
2) entered expression must be consistent with the accumulated
constraints (i.e. the product (further / accumulated) must be
non-zero;
3) if (further / accumulated) is non-zero, it also must be
non-zero the product (further / accumulated) / next_set of
states
4) cardinality of the set obtained from the last product must
be <= shown_states
- Side Effects required
- See Also
optional
- Defined in
simulate.c
void
simulate_choose_next(
BddFsm_ptr fsm,
bdd_ptr from_state,
bdd_ptr next_state_set,
Simulation_Mode mode,
int display_all,
bdd_ptr* which_input,
bdd_ptr* which_state
)
- from_state can be NULL from the initial set of states.
At the end which_input will contained the chosen input (if any, NULL
otherwise) and which_state will contain the chosen state
- Defined in
simulate.c
bdd_ptr
simulate_get_constraints_from_string(
const char* constr_str,
BddEnc_ptr enc,
boolean allow_nexts,
boolean allow_inputs
)
- Input variables are allowed to occur in the passed
constraint iff allow_inputs is true.
Next operators are allowed to occur in the passed
constraint iff allow_nexts is true.
If an error occurs, NULL is returned and a
message is printed.
This function does not raises any
exception. Returned BDD must be freed by the
caller. In error messages it is assumed that
constr_str is read from the command line.
- Defined in
simulate.c
bdd_ptr
simulate_request_constraints(
BddEnc_ptr enc
)
- optional
- Side Effects required
- See Also
optional
- Defined in
simulate.c
void
simulate_sigterm(
int sig
)
- SIGINT signal handler inside the simulator.
- Defined in
simulate.c
void
simulate_store_and_print_trace(
BddEnc_ptr enc,
node_ptr fragment,
boolean printyesno,
boolean only_changes,
NodeList_ptr symbols
)
- Extends current simulation trace by creating a new
trace for simulation fragment and concatenating it to
existing one.
- See Also
Trace_concat
- Defined in
simulateCmd.c