-
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