NuSMV/code/nusmv/core/fsm/bdd/bdd.h File Reference

#include "nusmv/core/dd/dd.h"

Defines
#define	BDD_ELFWD_OPT_ALL
#define	BDD_ELFWD_OPT_COUNTER_EXAMPLES 8
#define	BDD_ELFWD_OPT_FORWARD_SEARCH 1
	Declares the public interface for the package fsm.bdd.
#define	BDD_ELFWD_OPT_LTL_TABLEAU_FORWARD_SEARCH 2
#define	BDD_ELFWD_OPT_USE_REACHABLE_STATES 4
#define	BDD_INPUTS(x) ((BddInputs) x)
#define	BDD_INVAR_INPUTS(x) ((BddInvarInputs) x)
#define	BDD_INVAR_STATES(x) ((BddInvarStates) x)
#define	BDD_STATES(x) ((BddStates) x)
#define	BDD_STATES_INPUTS(x) ((BddStatesInputs) x)
#define	BDD_STATES_INPUTS_NEXTS(x) ((BddStatesInputsNexts) x)
Typedefs
typedef struct BddELFwdSavedOptions_TAG *	BddELFwdSavedOptions_ptr
typedef bdd_ptr	BddInputs
typedef bdd_ptr	BddInvarInputs
typedef bdd_ptr	BddInvarStates
typedef enum BddOregJusticeEmptinessBddAlgorithmType_TAG	BddOregJusticeEmptinessBddAlgorithmType
typedef bdd_ptr	BddStates
typedef bdd_ptr	BddStatesInputs
typedef bdd_ptr	BddStatesInputsNexts
Enumerations
enum	BddOregJusticeEmptinessBddAlgorithmType_TAG { BDD_OREG_JUSTICE_EMPTINESS_BDD_ALGORITHM_INVALID = -1, BDD_OREG_JUSTICE_EMPTINESS_BDD_ALGORITHM_EL_BWD = 0, BDD_OREG_JUSTICE_EMPTINESS_BDD_ALGORITHM_EL_FWD, BDD_OREG_JUSTICE_EMPTINESS_BDD_ALGORITHM_MIN_VALID, BDD_OREG_JUSTICE_EMPTINESS_BDD_ALGORITHM_MAX_VALID }
	Enumeration of algorithms for determining language emptiness of a Buchi fair transition system with BDDs. More...
Functions
BddOregJusticeEmptinessBddAlgorithmType	Bdd_BddOregJusticeEmptinessBddAlgorithmType_from_string (const char *name)
	const char* to BddOregJusticeEmptinessBddAlgorithmType
const char *	Bdd_BddOregJusticeEmptinessBddAlgorithmType_to_string (const BddOregJusticeEmptinessBddAlgorithmType self)
	BddOregJusticeEmptinessBddAlgorithmType to const char*.
boolean	Bdd_elfwd_check_options (NuSMVEnv_ptr env, unsigned int which_options, boolean on_fail_print)
	Checks options for forward Emerson-Lei algorithm.
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.
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.
void	Bdd_print_available_BddOregJusticeEmptinessBddAlgorithms (FILE *file)
	Prints the BDD-based algorithms to check language emptiness for omega-regular properties the system currently supplies.

Define Documentation

#define BDD_ELFWD_OPT_ALL

Value:

(BDD_ELFWD_OPT_FORWARD_SEARCH | \
                           BDD_ELFWD_OPT_LTL_TABLEAU_FORWARD_SEARCH | \
                           BDD_ELFWD_OPT_USE_REACHABLE_STATES | \
                           BDD_ELFWD_OPT_COUNTER_EXAMPLES)

Todo:: Missing synopsis

Todo:: Missing description

#define BDD_ELFWD_OPT_COUNTER_EXAMPLES 8

Todo:: Missing synopsis

Todo:: Missing description

#define BDD_ELFWD_OPT_FORWARD_SEARCH 1

Declares the public interface for the package fsm.bdd.

Author:: Roberto Cavada

Todo:: : Missing description

Todo:: Missing synopsis

Todo:: Missing description

#define BDD_ELFWD_OPT_LTL_TABLEAU_FORWARD_SEARCH 2

Todo:: Missing synopsis

Todo:: Missing description

#define BDD_ELFWD_OPT_USE_REACHABLE_STATES 4

Todo:: Missing synopsis

Todo:: Missing description

#define BDD_INPUTS ( x ) ((BddInputs) x)

Todo:: Missing synopsis

Todo:: Missing description

#define BDD_INVAR_INPUTS ( x ) ((BddInvarInputs) x)

Todo:: Missing synopsis

Todo:: Missing description

#define BDD_INVAR_STATES ( x ) ((BddInvarStates) x)

Todo:: Missing synopsis

Todo:: Missing description

#define BDD_STATES ( x ) ((BddStates) x)

Todo:: Missing synopsis

Todo:: Missing description

#define BDD_STATES_INPUTS ( x ) ((BddStatesInputs) x)

Todo:: Missing synopsis

Todo:: Missing description

#define BDD_STATES_INPUTS_NEXTS ( x ) ((BddStatesInputsNexts) x)

Todo:: Missing synopsis

Todo:: Missing description

Typedef Documentation

typedef struct BddELFwdSavedOptions_TAG* BddELFwdSavedOptions_ptr

typedef bdd_ptr BddInputs

typedef bdd_ptr BddInvarInputs

typedef bdd_ptr BddInvarStates

typedef enum BddOregJusticeEmptinessBddAlgorithmType_TAG BddOregJusticeEmptinessBddAlgorithmType

typedef bdd_ptr BddStates

Todo:: Missing synopsis

Todo:: Missing description

typedef bdd_ptr BddStatesInputs

typedef bdd_ptr BddStatesInputsNexts

Enumeration Type Documentation

enum BddOregJusticeEmptinessBddAlgorithmType_TAG

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.

Enumerator:

BDD_OREG_JUSTICE_EMPTINESS_BDD_ALGORITHM_INVALID
BDD_OREG_JUSTICE_EMPTINESS_BDD_ALGORITHM_EL_BWD
BDD_OREG_JUSTICE_EMPTINESS_BDD_ALGORITHM_EL_FWD
BDD_OREG_JUSTICE_EMPTINESS_BDD_ALGORITHM_MIN_VALID
BDD_OREG_JUSTICE_EMPTINESS_BDD_ALGORITHM_MAX_VALID

Function Documentation

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.

See also:: BddOregJusticeEmptinessBddAlgorithmType_to_string

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.

See also:: Bdd_BddOregJusticeEmptinessBddAlgorithmType_from_string

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.