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
bddMisc.c
Miscellanous routines not really specific to other files
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()
Computates 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. Note: a state is an assignment to state and frozen variables. an input is an assigment to input variables.

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_get_cached_reachable_states()
Returns the cached reachable states
BddFsm_set_reachable_states()
Sets the whole set of reachable states for this FSM, with no onion ring informations
BddFsm_has_cached_reachable_states()
Checks if the set of reachable states exists in the FSM
BddFsm_update_cached_reachable_states()
Updates the cached reachable states
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_minimum_distance_of_states()
Returns the minimum 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_sins_constrained_forward_image()
Returns the constrained forward image of a set of states
BddFsm_get_forward_image_states_inputs()
Returns the forward image of a set of state-input pairs
BddFsm_get_constrained_forward_image_states_inputs()
Returns the constrained forward image of a set of state-input pairs
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_revfair_states_inputs()
Returns the set of reverse fair state-input pairs of the machine.
BddFsm_get_fair_states()
Returns the set of fair states of a fsm.
BddFsm_get_revfair_states()
Returns the set of reverse 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 (if dir = BDD_FSM_DIR_BWD) or predecessor (otherwise) exists
BddFsm_states_inputs_to_states()
Returns the states occurring in a set of states-inputs pairs.
BddFsm_expand_cached_reachable_states()
Makes k steps of expansion of the set of reachable states of this machine but limit the computation to terminate in the number of seconds specified (even if this limit can be exceeded for the termination of the last cycle)
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_custom_varsets()
Performs the synchronous product of two fsm
BddFsm_apply_synchronous_product()
Variant of BddFsm_apply_synchronous_product_custom_varsets that simply takes all variables in the encoding into account.
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()
Computes 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_EXorEY_SI()
Computes the preimage (if dir = BDD_FSM_DIR_BWD) or the postimage (otherwise) of a set of states-inputs pairs.
bdd_fsm_EUorES_SI()
Computes the set of state-input pairs that satisfy E(f U g) (if dir = BDD_FSM_DIR_BWD) or E(f S g) (otherwise), with f and g sets of state-input pairs.
bdd_fsm_compute_EL_SI_subset()
Executes the Emerson-Lei algorithm
bdd_fsm_compute_EL_SI_subset_aux()
Executes the inner fixed point of the Emerson-Lei algorithm
bdd_fsm_get_fair_or_revfair_states_inputs_in_subspace()
Computes the set of (reverse) fair states in subspace
bdd_fsm_get_fair_or_revfair_states_inputs()
Computes the set of (reverse) fair states
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 information within other into self
BddFsmCache_set_reachable_states()
Fills cache structure with reachable states information
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

bddMisc.c

Miscellanous routines not really specific to other files

By: Viktor Schuppan

Miscellanous routines not really specific to other files: - Conversion between BddOregJusticeEmptinessBddAlgorithmType and const char* - Ensuring the preconditions for forward Emerson-Lei algorithm are met

Bdd_BddOregJusticeEmptinessBddAlgorithmType_from_string()
const char* to BddOregJusticeEmptinessBddAlgorithmType
Bdd_BddOregJusticeEmptinessBddAlgorithmType_to_string()
BddOregJusticeEmptinessBddAlgorithmType to const char*
Bdd_print_available_BddOregJusticeEmptinessBddAlgorithms()
Prints the BDD-based algorithms to check language emptiness for omega-regular properties the system currently supplies
Bdd_elfwd_check_options()
Checks options for forward Emerson-Lei algorithm
Bdd_elfwd_check_set_and_save_options()
Checks, sets and saves previous values of options for forward Emerson-Lei
Bdd_elfwd_restore_options()
Restores previous values of options for forward Emerson-Lei

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 2010/11/04 13h:33