NuSMV/code/nusmv/core/wff/lr/MasterLogicRecognizer.h File Reference

#include "nusmv/core/node/MasterNodeWalker.h"
#include "nusmv/core/utils/defs.h"

Defines
#define	LOGIC_RECOGNIZED_ASSERT_HAS_VALUE(self) nusmv_assert(self > EXP_NONE && self < EXP_ERROR);
#define	LOGIC_RECOGNIZED_ASSERT_VALID(self) nusmv_assert(self > EXP_FIRST && self < EXP_ERROR);
#define	LOGIC_RECOGNIZED_CHECK_INSTANCE(self) nusmv_assert(self > EXP_FIRST && self < EXP_LAST);
#define	MASTER_LOGIC_RECOGNIZER(self) ((MasterLogicRecognizer_ptr) self)
	To cast and check instances of class MasterLogicRecognizer.
#define	MASTER_LOGIC_RECOGNIZER_CHECK_INSTANCE(self) (nusmv_assert(MASTER_LOGIC_RECOGNIZER(self) != MASTER_LOGIC_RECOGNIZER(NULL)))
Typedefs
typedef struct MasterLogicRecognizer_TAG *	MasterLogicRecognizer_ptr
Enumerations
enum	LogicType { EXP_FIRST = -1, EXP_NONE = 0, EXP_SIMPLE, EXP_NEXT, EXP_LTL, EXP_CTL, EXP_ERROR, EXP_LAST }
	Public interface of class 'MasterLogicRecognizer'. More...

Define Documentation

#define LOGIC_RECOGNIZED_ASSERT_HAS_VALUE ( self ) nusmv_assert(self > EXP_NONE && self < EXP_ERROR);

#define LOGIC_RECOGNIZED_ASSERT_VALID ( self ) nusmv_assert(self > EXP_FIRST && self < EXP_ERROR);

#define LOGIC_RECOGNIZED_CHECK_INSTANCE ( self ) nusmv_assert(self > EXP_FIRST && self < EXP_LAST);

#define MASTER_LOGIC_RECOGNIZER ( self ) ((MasterLogicRecognizer_ptr) self)

To cast and check instances of class MasterLogicRecognizer.

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

#define MASTER_LOGIC_RECOGNIZER_CHECK_INSTANCE ( self ) (nusmv_assert(MASTER_LOGIC_RECOGNIZER(self) != MASTER_LOGIC_RECOGNIZER(NULL)))

typedef struct MasterLogicRecognizer_TAG* MasterLogicRecognizer_ptr

Public interface of class 'MasterLogicRecognizer'.

We exploit the equivalance of the NULL pointer and 0

Enumerator: