#include "nusmv/core/dd/dd.h"
Go to the source code of this file.
#define BDD_ELFWD_OPT_ALL |
(BDD_ELFWD_OPT_FORWARD_SEARCH | \ BDD_ELFWD_OPT_LTL_TABLEAU_FORWARD_SEARCH | \ BDD_ELFWD_OPT_USE_REACHABLE_STATES | \ BDD_ELFWD_OPT_COUNTER_EXAMPLES)
#define BDD_ELFWD_OPT_FORWARD_SEARCH 1 |
#define BDD_INVAR_INPUTS | ( | x | ) | ((BddInvarInputs) x) |
#define BDD_INVAR_STATES | ( | x | ) | ((BddInvarStates) x) |
#define BDD_STATES_INPUTS | ( | x | ) | ((BddStatesInputs) x) |
#define BDD_STATES_INPUTS_NEXTS | ( | x | ) | ((BddStatesInputsNexts) x) |
typedef struct BddELFwdSavedOptions_TAG* BddELFwdSavedOptions_ptr |
typedef bdd_ptr BddInputs |
typedef bdd_ptr BddInvarInputs |
typedef bdd_ptr BddInvarStates |
typedef bdd_ptr BddStatesInputs |
typedef bdd_ptr BddStatesInputsNexts |
Enumeration of algorithms for determining language emptiness of a Buchi fair transition system with BDDs.
Currently only has backward and forward variants of Emerson-Lei.
The ..._MIN/MAX_VALID values can be used to determine the least and greatest valid elements so as to eliminate some need for change when other algorithms are added. These values might need to be adapted below when new algorithms are added.
BddOregJusticeEmptinessBddAlgorithmType Bdd_BddOregJusticeEmptinessBddAlgorithmType_from_string | ( | const char * | name | ) |
const char* to BddOregJusticeEmptinessBddAlgorithmType
AutomaticStart
Converts the given type from string "name" to a BddOregJusticeEmptinessBddAlgorithmType object.
None.
const char* Bdd_BddOregJusticeEmptinessBddAlgorithmType_to_string | ( | const BddOregJusticeEmptinessBddAlgorithmType | self | ) |
BddOregJusticeEmptinessBddAlgorithmType to const char*.
It takes BddOregJusticeEmptinessBddAlgorithmType of self and returns a string specifying the type of it. Returned string is statically allocated and must not be freed.
None.
boolean Bdd_elfwd_check_options | ( | NuSMVEnv_ptr | env, | |
unsigned int | which_options, | |||
boolean | on_fail_print | |||
) |
Checks options for forward Emerson-Lei algorithm.
Depending on the value of which_options, it checks that forward search, ltl_tableau_forward_search, and use_reachable_states are enabled and counter_examples is disabled. Returns true if the checks are successful, false otherwise. If on_fail_print is true, it prints an error message on failure.
None.
BddELFwdSavedOptions_ptr Bdd_elfwd_check_set_and_save_options | ( | NuSMVEnv_ptr | env, | |
unsigned int | which_options | |||
) |
Checks, sets and saves previous values of options for forward Emerson-Lei.
Which values are actually checked, set, and saved is determined by the value of which_options. If set in which_options, forward search, ltl_tableau_forward_search, and use_reachable_states are enabled and counter_examples is disabled. Previous values are stored and returned.
Creates the returned BddELFwdSavedOptions_ptr. It does *not* belong to caller - it will be destroyed by the corresponding call to Bdd_elfwd_restore_options.
Modifies options.
void Bdd_elfwd_restore_options | ( | NuSMVEnv_ptr | env, | |
unsigned int | which_options, | |||
BddELFwdSavedOptions_ptr | saved_options | |||
) |
Restores previous values of options for forward Emerson-Lei.
Which values are actually restored from saved_options is determined by the value of which_options.
Modifies options.
void Bdd_print_available_BddOregJusticeEmptinessBddAlgorithms | ( | FILE * | file | ) |
Prints the BDD-based algorithms to check language emptiness for omega-regular properties the system currently supplies.
None.