-
BddFsmCache_copy_reachables()
- Copies reachable states indormation 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_reachables()
- Fills cache structure with reachable states information
-
BddFsmCache_soft_copy()
- Family soft copier
-
BddFsm_apply_synchronous_product()
- Performs the synchronous product of two fsm
-
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_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_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()
- 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()
- 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_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_state_constraints()
- Getter for state constraints
-
BddFsm_get_states_inputs_constraints()
- Returns a state-input pair for which at least one
legal successor 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_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_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.
-
Bdd_End()
- Quit the BddFsm package
-
Bdd_Init()
- Initializes the BddFsm package.
-
CommandCheckFsm()
- Checks the fsm for totality and deadlock states.
-
CommandComputeReachable()
- Enables the future computation of 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_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_EX_SI()
- Computes the preimage 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_reachable_states()
- Returns 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_fair_SI_subset_aux()
-
-
bdd_fsm_get_fair_SI_subset()
-
-
bdd_fsm_get_fair_states_inputs_in_subspace()
-
-
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 2009/03/04 13h:34