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

#include "nusmv/core/fsm/bdd/bdd.h"
#include "nusmv/core/fsm/bdd/FairnessList.h"
#include "nusmv/core/dd/dd.h"
#include "nusmv/core/trans/bdd/BddTrans.h"
#include "nusmv/core/enc/bdd/BddEnc.h"
#include "nusmv/core/fsm/sexp/sexp.h"

Go to the source code of this file.

Defines
#define	BDD_FSM(x)   ((BddFsm_ptr) x)
#define	BDD_FSM_CHECK_INSTANCE(x)   (nusmv_assert( BDD_FSM(x) != BDD_FSM(NULL) ))
Typedefs
typedef enum Bdd_Fsm_dir_TAG	BddFsm_dir
typedef struct BddFsm_TAG *	BddFsm_ptr
Enumerations
enum	Bdd_Fsm_dir_TAG { BDD_FSM_DIR_BWD, BDD_FSM_DIR_FWD }
enum	BddFsmTransPrinterFormat {   BDD_FSM_TRANS_PRINTER_SILENT, BDD_FSM_TRANS_PRINTER_SMV, BDD_FSM_TRANS_PRINTER_CSV, BDD_FSM_TRANS_PRINTER_DOT,   BDD_FSM_TRANS_PRINTER_INVALID = -1 }
	Format used by printers of transitions. More...
Functions
enum BddFsmTransPrinterFormat	BddFsm_trans_printer_format_from_string (const char *format_str)
	Converts from string the format for trans printer.
const char *	BddFsm_trans_printer_format_to_string (enum BddFsmTransPrinterFormat format)
	Returns the string representation of the given format. NULL is returned if the format does not exist. The returned string must be NOT freed by the caller.
enum BddFsmTransPrinterFormat *	BddFsm_trans_printer_get_avail_formats (size_t *num)
	Returns the list of available formats for trans printer.

---

Define Documentation

#define BDD_FSM

(

x

)

((BddFsm_ptr) x)

Todo:

Missing synopsis

Todo:

Missing description

#define BDD_FSM_CHECK_INSTANCE

(

x

)

(nusmv_assert( BDD_FSM(x) != BDD_FSM(NULL) ))

Todo:

Missing synopsis

Todo:

Missing description

---

Typedef Documentation

typedef enum Bdd_Fsm_dir_TAG BddFsm_dir

typedef struct BddFsm_TAG* BddFsm_ptr

---

Enumeration Type Documentation

enum Bdd_Fsm_dir_TAG

Enumerator:

BDD_FSM_DIR_BWD
BDD_FSM_DIR_FWD

enum BddFsmTransPrinterFormat

Format used by printers of transitions.

Enumerator:

BDD_FSM_TRANS_PRINTER_SILENT
BDD_FSM_TRANS_PRINTER_SMV
BDD_FSM_TRANS_PRINTER_CSV
BDD_FSM_TRANS_PRINTER_DOT
BDD_FSM_TRANS_PRINTER_INVALID

---

Function Documentation

enum BddFsmTransPrinterFormat BddFsm_trans_printer_format_from_string

(

const char *

format_str

)

Converts from string the format for trans printer.

BDD_FSM_TRANS_PRINTER_INVALID is returned if the string does not correspond to any valid format.

const char* BddFsm_trans_printer_format_to_string

(

enum BddFsmTransPrinterFormat

format

)

Returns the string representation of the given format. NULL is returned if the format does not exist. The returned string must be NOT freed by the caller.

enum BddFsmTransPrinterFormat* BddFsm_trans_printer_get_avail_formats

(

size_t *

num

)

Returns the list of available formats for trans printer.

The number of entries is written by the function in num. The returned list must be freeded by the caller.