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

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

Go to the source code of this file.

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
#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 (  )     ((BddInputs) x)
Todo:
Missing synopsis
Todo:
Missing description
#define BDD_INVAR_INPUTS (  )     ((BddInvarInputs) x)
Todo:
Missing synopsis
Todo:
Missing description
#define BDD_INVAR_STATES (  )     ((BddInvarStates) x)
Todo:
Missing synopsis
Todo:
Missing description
#define BDD_STATES (  )     ((BddStates) x)
Todo:
Missing synopsis
Todo:
Missing description
#define BDD_STATES_INPUTS (  )     ((BddStatesInputs) x)
Todo:
Missing synopsis
Todo:
Missing description
#define BDD_STATES_INPUTS_NEXTS (  )     ((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 bdd_ptr BddStates
Todo:
Missing synopsis
Todo:
Missing description
typedef bdd_ptr BddStatesInputs
typedef bdd_ptr BddStatesInputsNexts

Enumeration Type Documentation

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.

See also:
Bdd_elfwd_restore_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.

See also:
Bdd_elfwd_check_set_and_save_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.

See also:
BddOregJusticeEmptinessBddAlgorithmType, Bdd_BddOregJusticeEmptinessBddAlgorithmType_to_string
All Data Structures Files Functions Variables Typedefs Enumerations Enumerator Defines

Generated on 14 Oct 2015 for NuSMV Developers Manual by  doxygen 1.6.1