void BddFsmCache_copy_reachables( BddFsmCache_ptr self, const BddFsmCache_ptr other )
BddFsmCache.c
BddFsmCache_ptr BddFsmCache_create( DdManager* dd )
BddFsmCache.c
void BddFsmCache_destroy( BddFsmCache_ptr self )
BddFsmCache.c
BddFsmCache_ptr BddFsmCache_hard_copy( const BddFsmCache_ptr self )
BddFsmCache_soft_copy
BddFsmCache.c
void BddFsmCache_reset_not_reusable_fields_after_product( BddFsmCache_ptr self )
BddFsm_apply_synchronous_product
BddFsmCache.c
void BddFsmCache_set_reachables( BddFsmCache_ptr self, BddStates states, node_ptr layers_list, const int diameter )
BddFsmCache.c
BddFsmCache_ptr BddFsmCache_soft_copy( const BddFsmCache_ptr self )
BddFsmCache_hard_copy
BddFsmCache.c
void BddFsm_apply_synchronous_product( BddFsm_ptr self, const BddFsm_ptr other )
BddFsmCache_reset_not_reusable_fields_after_product
BddFsm.c
void BddFsm_check_machine( const BddFsm_ptr self )
BddFsm.c
void BddFsm_copy_cache( BddFsm_ptr self, const BddFsm_ptr other, boolean keep_family )
BddFsm.c
void BddFsm_copy_reachable_states( BddFsm_ptr self, BddFsm_ptr other, boolean keep_family, boolean force_calculation )
BddFsm.c
BddFsm_ptr BddFsm_copy( const BddFsm_ptr self )
BddFsm.c
BddFsm_ptr BddFsm_create( BddEnc_ptr encoding, BddStates init, BddInvarStates invar_states, BddInvarInputs invar_inputs, BddTrans_ptr trans, JusticeList_ptr justice, CompassionList_ptr compassion )
BddFsm.c
void BddFsm_destroy( BddFsm_ptr self )
BddFsm.c
BddStates BddFsm_get_backward_image( const BddFsm_ptr self, BddStates states )
BddFsm.c
BddEnc_ptr BddFsm_get_bdd_encoding( const BddFsm_ptr self )
BddFsm.c
CompassionList_ptr BddFsm_get_compassion( const BddFsm_ptr self )
BddFsm.c
BddStates BddFsm_get_constrained_backward_image( const BddFsm_ptr self, BddStates states, BddStatesInputs constraints )
BddFsm.c
BddStates BddFsm_get_constrained_forward_image( const BddFsm_ptr self, BddStates states, BddStatesInputs constraints )
BddFsm.c
BddStates BddFsm_get_deadlock_states( BddFsm_ptr self )
BddFsm.c
int BddFsm_get_diameter( BddFsm_ptr self )
BddFsm.c
int BddFsm_get_distance_of_states( BddFsm_ptr self, BddStates states )
BddFsm.c
BddStatesInputs BddFsm_get_fair_states_inputs( BddFsm_ptr self )
BddFsm.c
BddStates BddFsm_get_fair_states( BddFsm_ptr self )
BddFsm.c
BddStates BddFsm_get_forward_image( const BddFsm_ptr self, BddStates states )
BddFsm.c
BddStates BddFsm_get_init( const BddFsm_ptr self )
BddFsm.c
BddInvarInputs BddFsm_get_input_constraints( const BddFsm_ptr self )
BddFsm.c
JusticeList_ptr BddFsm_get_justice( const BddFsm_ptr self )
BddFsm.c
BddStatesInputs BddFsm_get_k_backward_image( const BddFsm_ptr self, BddStates states, int k )
BddFsm.c
bdd_ptr BddFsm_get_monolithic_trans_bdd( BddFsm_ptr self )
BddFsm.c
BddStates BddFsm_get_not_successor_states( BddFsm_ptr self )
BddFsm.c
BddStates BddFsm_get_reachable_states_at_distance( BddFsm_ptr self, int distance )
BddFsm.c
BddStates BddFsm_get_reachable_states( BddFsm_ptr self )
BddFsm.c
BddInvarStates BddFsm_get_state_constraints( const BddFsm_ptr self )
BddFsm.c
BddStatesInputs BddFsm_get_states_inputs_constraints( const BddFsm_ptr self )
BddFsm.c
BddStatesInputs BddFsm_get_strong_backward_image( const BddFsm_ptr self, BddStates states )
BddFsm.c
BddTrans_ptr BddFsm_get_trans( const BddFsm_ptr self )
BddFsm.c
BddStatesInputs BddFsm_get_weak_backward_image( const BddFsm_ptr self, BddStates states )
BddFsm.c
boolean BddFsm_is_deadlock_free( BddFsm_ptr self )
BddFsm.c
boolean BddFsm_is_fair_states( const BddFsm_ptr self, BddStates states )
BddFsm.c
boolean BddFsm_is_total( BddFsm_ptr self )
BddFsm.c
void BddFsm_print_fair_states_info( const BddFsm_ptr self, const boolean print_states, FILE* file )
BddFsm.c
void BddFsm_print_fair_transitions_info( const BddFsm_ptr self, const boolean print_transitions, FILE* file )
BddFsm.c
void BddFsm_print_info( const BddFsm_ptr self, FILE* file )
BddFsm.c
void BddFsm_print_reachable_states_info( const BddFsm_ptr self, const boolean print_states, FILE* file )
BddFsm.c
boolean BddFsm_reachable_states_computed( BddFsm_ptr self )
BddFsm.c
BddStates BddFsm_states_inputs_to_inputs( const BddFsm_ptr self, BddStatesInputs si )
BddFsm.c
BddStates BddFsm_states_inputs_to_states( const BddFsm_ptr self, BddStatesInputs si )
BddFsm.c
BddInputs BddFsm_states_to_states_get_inputs( const BddFsm_ptr self, BddStates cur_states, BddStates next_states )
BddFsm.c
void Bdd_End( )
bddCmd.c
void Bdd_Init( )
bddCmd.c
int CommandCheckFsm( int argc, char ** argv )
bddCmd.c
int CommandComputeReachable( int argc, char ** argv )
bddCmd.c
int CommandPrintFairStates( int argc, char ** argv )
bddCmd.c
int CommandPrintFairTransitions( int argc, char ** argv )
bddCmd.c
int CommandPrintReachableStates( int argc, char ** argv )
bddCmd.c
void CompassionList_append_p_q( CompassionList_ptr self, BddStates p, BddStates q )
FairnessList.c
void CompassionList_apply_synchronous_product( CompassionList_ptr self, const CompassionList_ptr other )
FairnessList.c
CompassionList_ptr CompassionList_create( DdManager* dd_manager )
FairnessList.c
BddStates CompassionList_get_p( const CompassionList_ptr self, const FairnessListIterator_ptr iter )
FairnessList.c
BddStates CompassionList_get_q( const CompassionList_ptr self, const FairnessListIterator_ptr iter )
FairnessList.c
boolean FairnessListIterator_is_end( const FairnessListIterator_ptr self )
FairnessList.c
FairnessListIterator_ptr FairnessListIterator_next( const FairnessListIterator_ptr self )
FairnessList.c
FairnessListIterator_ptr FairnessList_begin( const FairnessList_ptr self )
FairnessList.c
FairnessList_ptr FairnessList_create( DdManager* dd_manager )
FairnessList.c
void JusticeList_append_p( JusticeList_ptr self, BddStates p )
FairnessList.c
void JusticeList_apply_synchronous_product( JusticeList_ptr self, const JusticeList_ptr other )
FairnessList.c
JusticeList_ptr JusticeList_create( DdManager* dd_manager )
FairnessList.c
BddStates JusticeList_get_p( const JusticeList_ptr self, const FairnessListIterator_ptr iter )
FairnessList.c
static BddStatesInputs bdd_fsm_EU_SI( const BddFsm_ptr self, BddStatesInputs f, BddStatesInputs g )
BddFsm.c
static BddStatesInputs bdd_fsm_EX_SI( const BddFsm_ptr self, BddStatesInputs si )
BddFsm.c
static void bdd_fsm_cache_deinit_reachables( BddFsmCache_ptr self )
BddFsmCache.c
static void bdd_fsm_cache_deinit( BddFsmCache_ptr self )
BddFsmCache.c
static void bdd_fsm_cache_init( BddFsmCache_ptr self, DdManager* dd )
BddFsmCache.c
static void bdd_fsm_check_fairness_emptiness( const BddFsm_ptr self )
BddFsm.c
static void bdd_fsm_check_init_state_invar_emptiness( const BddFsm_ptr self )
BddFsm.c
static void bdd_fsm_compute_reachable_states( BddFsm_ptr self )
BddFsm.c
static void bdd_fsm_copy( const BddFsm_ptr self, BddFsm_ptr copy )
BddFsm.c
static void bdd_fsm_deinit( BddFsm_ptr self )
BddFsm.c
static BddStatesInputs bdd_fsm_fair_SI_subset_aux( const BddFsm_ptr self, BddStatesInputs states, BddStatesInputs subspace )
BddFsm.c
static BddStatesInputs bdd_fsm_get_fair_SI_subset( const BddFsm_ptr self, BddStatesInputs subspace )
BddFsm.c
static BddStatesInputs bdd_fsm_get_fair_states_inputs_in_subspace( const BddFsm_ptr self, BddStatesInputs subspace )
BddFsm.c
static BddStatesInputs bdd_fsm_get_legal_state_input( BddFsm_ptr self )
BddFsm.c
static void bdd_fsm_init( BddFsm_ptr self, BddEnc_ptr encoding, BddStates init, BddInvarStates invar_states, BddInvarInputs invar_inputs, BddTrans_ptr trans, JusticeList_ptr justice, CompassionList_ptr compassion )
BddFsm.c
static void fairness_list_init( FairnessList_ptr self, DdManager* dd_manager )
FairnessList.c