NuSMV/code/nusmv/core/enc/be/BeEnc.h File Reference

#include "nusmv/core/enc/base/BoolEncClient.h"
#include "nusmv/core/enc/bool/BoolEnc.h"
#include "nusmv/core/compile/symb_table/SymbTable.h"
#include "nusmv/core/be/be.h"
#include "nusmv/core/node/node.h"
#include "nusmv/core/utils/object.h"
#include "nusmv/core/utils/utils.h"

Go to the source code of this file.

Defines
#define	BE_CURRENT_UNTIMED   -1
	A constant representing the time a current untimed variable belong to.
#define	BE_ENC(self)   ((BeEnc_ptr) self)
	To cast and check instances of class BeEnc.
#define	BE_ENC_CHECK_INSTANCE(self)   (nusmv_assert(BE_ENC(self) != BE_ENC(NULL)))
Typedefs
typedef struct BeEnc_TAG *	BeEnc_ptr
Enumerations
enum	BeVarType {   BE_VAR_TYPE_CURR = 0x1 << 0, BE_VAR_TYPE_FROZEN = 0x1 << 1, BE_VAR_TYPE_INPUT = 0x1 << 2, BE_VAR_TYPE_NEXT = 0x1 << 3,   BE_VAR_TYPE_ALL, BE_VAR_TYPE_ERROR = 0x1 << 4 }
	The category which a be variable belongs to. More...

---

Define Documentation

#define BE_CURRENT_UNTIMED   -1

A constant representing the time a current untimed variable belong to.

The value of the constant is guaranteed to be out of the range of legal time numbers, i.e. out of \[0, BeEnc_get_max_time()\].

This constant, for example, is returned by BeEnc_index_to_time given a frozen variable (which can be only untimed).

#define BE_ENC

(

self

)

((BeEnc_ptr) self)

To cast and check instances of class BeEnc.

These macros must be used respectively to cast and to check instances of class BeEnc

#define BE_ENC_CHECK_INSTANCE

(

self

)

(nusmv_assert(BE_ENC(self) != BE_ENC(NULL)))

Todo:

Missing synopsis

Todo:

Missing description

---

Typedef Documentation

typedef struct BeEnc_TAG* BeEnc_ptr

---

Enumeration Type Documentation

enum BeVarType

The category which a be variable belongs to.

Used to classify a be variable within 3 main categories:

• current state variables
• frozen variables
• input variables
• next state variables

These values can be combined when for example the iteration is performed. In this way it is possible to iterate through the set of current and next state vars, skipping the inputs.

Enumerator:

BE_VAR_TYPE_CURR
BE_VAR_TYPE_FROZEN
BE_VAR_TYPE_INPUT
BE_VAR_TYPE_NEXT
BE_VAR_TYPE_ALL
BE_VAR_TYPE_ERROR