simulate.h
External header file
simulate.c
Simulator routines
simulateCmd.c
Model Checker Simulator Commands
simulateTransSet.c
Module that exports a class representing a transitions set

simulate.h

External header file

By: Andrea Morichetti


simulate.c

Simulator routines

By: Andrea Morichetti, Roberto Cavada

This file contains functions for image computation, for state picking in a set (according to three different policies), for states display and constraints insertion.

Simulate_MultipleSteps()
Multiple step simulation
Simulate_ChooseOneState()
Chooses one state among future states
Simulate_ChooseOneStateInput()
Simulate_CmdPickOneState()
Picks one state, to be used for BDD simulation
simulate_get_constraints_from_string()
Converts given constraint expression (as a string) to a bdd
simulate_choose_next()
simulate_sigterm()
Signal handler
simulate_accumulate_constraints()
required
simulate_request_constraints()
required

simulateCmd.c

Model Checker Simulator Commands

By: Andrea Morichetti

This file contains commands to be used for the simulation feature.

See Alsosimulate.c

Simulate_Init()
Initializes the simulate package.
Simulate_End()
Quits the simulate package
CommandPickState()
Picks a state from the set of initial states
CommandSimulate()
Performs a simulation from the current selected state
CommandGotoState()
Goes to a given state of a trace
CommandPrintCurrentState()
Prints the current state
simulate_extend_print_curr_trace()
Extends current simulation trace and prints it

simulateTransSet.c

Module that exports a class representing a transitions set

By: Roberto Cavada

SimulateTransSet_create()
Class constructor
SimulateTransSet_destroy()
Class destructor
SimulateTransSet_get_from_state()
Getter for the state the transition set is originating from
SimulateTransSet_get_next_state_num()
Returns the cardinality of the target set of states
SimulateTransSet_get_next_state()
Returns the Nth element of the target set of states
SimulateTransSet_get_inputs_num_at_state()
Returns the cardinality of the inputs set going to a given state, represented by its index in the set of target states
SimulateTransSet_get_input_at_state()
Returns the Ith input from the set of inputs going to the Nth state in the set of target states
SimulateTransSet_get_state_input_at()
SimulateTransSet_get_state_input_rand()
SimulateTransSet_get_state_input_det()
SimulateTransSet_print()

Last updated on 2012/11/18 14h:16