bddCmd.c
Bdd FSM commands
BddFsm.c
Defines the public interface for the class BddFsm
BddFsmCache.c
Private module, that defines a structure privately used into each instance of the class BddFsm, to cache some information
FairnessList.c
Declares the interface for the classes that contains fairness conditions

bddCmd.c

Bdd FSM commands

By: Marco Roveri

This file contains all the shell commands to dela with computation and printing of reachable states, fair states and fair transitions.

Bdd_Init()
Initializes the BddFsm package.
Bdd_End()
Quit the BddFsm package
CommandCheckFsm()
Checks the fsm for totality and deadlock states.
CommandComputeReachable()
Enables the future computation of the set of reachable states
CommandPrintReachableStates()
Prints the reachable states.
CommandPrintFairStates()
Prints the fair states.
CommandPrintFairTransitions()
Prints the fair transitions.

BddFsm.c

Defines the public interface for the class BddFsm

By: Roberto Cavada, Marco Benedetti

A BddFsm is a Finite State Machine (FSM) whose building blocks (the set of initial state, the transition relation, the set of constraints on inputs and so on) are represented by means of BDD data structures, and whose capabilities are based on operations upon and between BDDs as well.

BddFsm_create()
Constructor for BddFsm
BddFsm_destroy()
Destructor of class BddFsm
BddFsm_copy()
Copy constructor for BddFsm
BddFsm_copy_cache()
Copies cached information of 'other' into self
BddFsm_get_justice()
Getter for justice list
BddFsm_get_compassion()
Getter for compassion list
BddFsm_get_init()
Getter for init
BddFsm_get_state_constraints()
Getter for state constraints
BddFsm_get_input_constraints()
Getter for input constraints
BddFsm_get_trans()
Getter for the trans
BddFsm_get_bdd_encoding()
Returns the be encoding associated with the given fsm instance
BddFsm_reachable_states_computed()
Returns true if the set of reachable states has already been computed
BddFsm_get_reachable_states()
Gets the set of reachable states of this machine
BddFsm_copy_reachable_states()
Copies reachable states of 'other' into 'self'
BddFsm_get_reachable_states_at_distance()
Returns the set of reachable states at a given distance
BddFsm_get_monolithic_trans_bdd()
Returns a bdd that represents the monolithic transition relation
BddFsm_get_distance_of_states()
Returns the distance of a given set of states from initial states
BddFsm_get_diameter()
Returns the diameter of the machine from the inital state
BddFsm_get_not_successor_states()
Returns the set of states without subsequents
BddFsm_get_deadlock_states()
Returns the set of deadlock states
BddFsm_is_total()
Returns true if this machine is total
BddFsm_is_deadlock_free()
Returns true if this machine is deadlock free
BddFsm_get_forward_image()
Returns the forward image of a set of states
BddFsm_get_constrained_forward_image()
Returns the constrained forward image of a set of states
BddFsm_get_backward_image()
Returns the backward image of a set of states
BddFsm_get_constrained_backward_image()
Returns the constrained backward image of a set of states
BddFsm_get_k_backward_image()
Returns the k-backward image of a set of states
BddFsm_get_weak_backward_image()
Returns the weak backward image of a set of states
BddFsm_get_strong_backward_image()
Returns the strong backward image of a set of states
BddFsm_print_info()
Prints some information about this BddFsm.
BddFsm_print_reachable_states_info()
Prints statistical information about reachable states.
BddFsm_get_fair_states_inputs()
Returns the set of fair state-input pairs of the machine.
BddFsm_get_fair_states()
Returns the set of fair states of a fsm.
BddFsm_states_to_states_get_inputs()
Given two sets of states, returns the set of inputs labeling any transition from a state in the first set to a state in the second set.
BddFsm_is_fair_states()
Checks if a set of states is fair.
BddFsm_get_states_inputs_constraints()
Returns a state-input pair for which at least one legal successor exists
BddFsm_states_inputs_to_states()
Returns the states occurring in a set of states-inputs pairs.
BddFsm_states_inputs_to_inputs()
Returns the inputs occurring in a set of states-inputs pairs.
BddFsm_print_fair_states_info()
Prints statistical information about fair states.
BddFsm_print_fair_transitions_info()
Prints statistical information about fair states and transitions.
BddFsm_check_machine()
Check that the transition relation is total
BddFsm_apply_synchronous_product()
Performs the synchronous product of two fsm
bdd_fsm_init()
Private initializer
bdd_fsm_copy()
private copy constructor
bdd_fsm_deinit()
private member called by the destructor
bdd_fsm_compute_reachable_states()
Returns the set of reachable states of this machine
bdd_fsm_get_legal_state_input()
Returns the set of states and inputs, for which a legal transition can be made.
bdd_fsm_EX_SI()
Computes the preimage of a set of states-inputs pairs.
bdd_fsm_EU_SI()
Computes the set of state-input pairs that satisfy E(f U g), with f and g sets of state-input pairs.
bdd_fsm_get_fair_SI_subset()
bdd_fsm_fair_SI_subset_aux()
bdd_fsm_get_fair_states_inputs_in_subspace()
bdd_fsm_check_init_state_invar_emptiness()
Check inits for emptiness, and prints a warning if needed
bdd_fsm_check_fairness_emptiness()
Checks fair states for emptiness, as well as fot the intersaction of fair states and inits. Prints a warning if needed

BddFsmCache.c

Private module, that defines a structure privately used into each instance of the class BddFsm, to cache some information

By: Roberto Cavada

This defines the interface of class BddFsmCache only. Since the cache is privately accessed also by the class BddFsm, the cache is declared by file bddFsmInt.h

BddFsmCache_create()
Class contructor
BddFsmCache_destroy()
Class destructor
BddFsmCache_hard_copy()
Class copy constructor
BddFsmCache_reset_not_reusable_fields_after_product()
Resets any field in the cache that must be recalculated
BddFsmCache_soft_copy()
Family soft copier
BddFsmCache_copy_reachables()
Copies reachable states indormation within other into self
BddFsmCache_set_reachables()
Fills cache structure with reachable states information
bdd_fsm_cache_init()
private initializer
bdd_fsm_cache_deinit()
private deinitializer
bdd_fsm_cache_deinit_reachables()
private deinitializer for reachables states

FairnessList.c

Declares the interface for the classes that contains fairness conditions

By: Roberto Cavada

Exported classes are: - FairnessList (pure, base class) - JusticeList - CompassionList

FairnessList_create()
Base class constructor
FairnessList_begin()
Use to start iteration
FairnessListIterator_is_end()
Use to check end of iteration
FairnessListIterator_next()
use to iterate on an list iterator
JusticeList_create()
Constructor for justice fairness constraints list
JusticeList_get_p()
Getter for BddStates pointed by given iterator
JusticeList_append_p()
Appends the given bdd to the list
JusticeList_apply_synchronous_product()
Creates the union of the two given fairness lists. Result goes into self
CompassionList_create()
Constructor for compassion fairness constraints list
CompassionList_get_p()
Getter of left-side bdd pointed by given iterator
CompassionList_get_q()
Getter of right-side bdd pointed by given iterator
CompassionList_append_p_q()
Appends the given BDDs to the list
CompassionList_apply_synchronous_product()
Creates the union of the two given fairness lists. Result goes into self
fairness_list_init()

Last updated on 2009/01/30 15h:04