BddFsmCache_copy_reachables()
Copies reachable states information within other into self
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_set_reachable_states()
Fills cache structure with reachable states information
BddFsmCache_set_reachables()
Fills cache structure with reachable states information
BddFsmCache_soft_copy()
Family soft copier
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.
BddFsm_check_machine()
Check that the transition relation is total
BddFsm_copy_cache()
Copies cached information of 'other' into self
BddFsm_copy_reachable_states()
Copies reachable states of 'other' into 'self'
BddFsm_copy()
Copy constructor for BddFsm
BddFsm_create()
Constructor for BddFsm
BddFsm_destroy()
Destructor of class BddFsm
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_get_backward_image()
Returns the backward image of a set of states
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_get_compassion()
Getter for compassion list
BddFsm_get_constrained_backward_image()
Returns the constrained backward image of a set of states
BddFsm_get_constrained_forward_image_states_inputs()
Returns the constrained forward image of a set of state-input pairs
BddFsm_get_constrained_forward_image()
Returns the constrained forward image of a set of states
BddFsm_get_deadlock_states()
Returns the set of deadlock states
BddFsm_get_diameter()
Returns the diameter of the machine from the inital state
BddFsm_get_distance_of_states()
Returns the distance of a given set of states from initial 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_get_forward_image_states_inputs()
Returns the forward image of a set of state-input pairs
BddFsm_get_forward_image()
Returns the forward image of a set of states
BddFsm_get_init()
Getter for init
BddFsm_get_input_constraints()
Getter for input constraints
BddFsm_get_justice()
Getter for justice list
BddFsm_get_k_backward_image()
Returns the k-backward image of a set of states
BddFsm_get_minimum_distance_of_states()
Returns the minimum distance of a given set of states from initial states
BddFsm_get_monolithic_trans_bdd()
Returns a bdd that represents the monolithic transition relation
BddFsm_get_not_successor_states()
Returns the set of states without subsequents
BddFsm_get_reachable_states_at_distance()
Returns the set of reachable states at a given distance
BddFsm_get_reachable_states()
Gets the set of reachable states of this machine
BddFsm_get_revfair_states_inputs()
Returns the set of reverse fair state-input pairs of the machine.
BddFsm_get_revfair_states()
Returns the set of reverse fair states of a fsm.
BddFsm_get_sins_constrained_forward_image()
Returns the constrained forward image of a set of states
BddFsm_get_state_constraints()
Getter for state constraints
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_get_strong_backward_image()
Returns the strong backward image of a set of states
BddFsm_get_trans()
Getter for the trans
BddFsm_get_weak_backward_image()
Returns the weak backward image of a set of states
BddFsm_has_cached_reachable_states()
Checks if the set of reachable states exists in the FSM
BddFsm_is_deadlock_free()
Returns true if this machine is deadlock free
BddFsm_is_fair_states()
Checks if a set of states is fair.
BddFsm_is_total()
Returns true if this machine is total
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_print_info()
Prints some information about this BddFsm.
BddFsm_print_reachable_states_info()
Prints statistical information about reachable states.
BddFsm_reachable_states_computed()
Returns true if the set of reachable states has already been computed
BddFsm_set_reachable_states()
Sets the whole set of reachable states for this FSM, with no onion ring informations
BddFsm_states_inputs_to_inputs()
Returns the inputs occurring in a set of states-inputs pairs.
BddFsm_states_inputs_to_states()
Returns the states occurring in a set of states-inputs pairs.
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_update_cached_reachable_states()
Updates the cached reachable states
Bdd_BddOregJusticeEmptinessBddAlgorithmType_from_string()
const char* to BddOregJusticeEmptinessBddAlgorithmType
Bdd_BddOregJusticeEmptinessBddAlgorithmType_to_string()
BddOregJusticeEmptinessBddAlgorithmType to const char*
Bdd_End()
Quit the BddFsm package
Bdd_Init()
Initializes the BddFsm package.
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
Bdd_print_available_BddOregJusticeEmptinessBddAlgorithms()
Prints the BDD-based algorithms to check language emptiness for omega-regular properties the system currently supplies
CommandCheckFsm()
Checks the fsm for totality and deadlock states.
CommandComputeReachable()
Computates the set of reachable states
CommandPrintFairStates()
Prints the fair states.
CommandPrintFairTransitions()
Prints the fair transitions.
CommandPrintReachableStates()
Prints the reachable states.
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
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
FairnessListIterator_is_end()
Use to check end of iteration
FairnessListIterator_next()
use to iterate on an list iterator
FairnessList_begin()
Use to start iteration
FairnessList_create()
Base class constructor
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
JusticeList_create()
Constructor for justice fairness constraints list
JusticeList_get_p()
Getter for BddStates pointed by given iterator
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_EXorEY_SI()
Computes the preimage (if dir = BDD_FSM_DIR_BWD) or the postimage (otherwise) of a set of states-inputs pairs.
bdd_fsm_cache_deinit_reachables()
private deinitializer for reachables states
bdd_fsm_cache_deinit()
private deinitializer
bdd_fsm_cache_init()
private initializer
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
bdd_fsm_check_init_state_invar_emptiness()
Check inits for emptiness, and prints a warning if needed
bdd_fsm_compute_EL_SI_subset_aux()
Executes the inner fixed point of the Emerson-Lei algorithm
bdd_fsm_compute_EL_SI_subset()
Executes the Emerson-Lei algorithm
bdd_fsm_compute_reachable_states()
Computes the set of reachable states of this machine
bdd_fsm_copy()
private copy constructor
bdd_fsm_deinit()
private member called by the destructor
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_get_legal_state_input()
Returns the set of states and inputs, for which a legal transition can be made.
bdd_fsm_init()
Private initializer
fairness_list_init()

Last updated on 2011/04/06 21h:16