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