-
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 2010/11/03 21h:54