External Header File for simulation package: simulation package provides a set of utilities for traces generation (a trace is a possible execution of the model). It performs initial state picking, trace inspection, simulation according to different policies (deterministic, random, interactive) and with the possibility to specify constraints.

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

Last updated on 2010/11/03 21h:54