#include "nusmv/core/trans/generic/GenericTrans.h"#include "nusmv/core/trans/bdd/ClusterList.h"#include "nusmv/core/trans/bdd/ClusterOptions.h"#include "nusmv/core/dd/dd.h"Go to the source code of this file.
Defines | |
| #define | BDD_TRANS(x) ((BddTrans_ptr) x) |
| #define | BDD_TRANS_CHECK_INSTANCE(x) (nusmv_assert(BDD_TRANS(x) != BDD_TRANS(NULL))) |
| #define | TRANS_IMAGE_IS_FORWARD(kind) (!((kind) >> 1)) |
| Takes TransImageKind and returns 1 iff the kind is one of forward ones. | |
| #define | TRANS_IMAGE_IS_STATE_ONLY(kind) (!((kind) & 1)) |
| Takes TransImageKind and returns 1 iff the kind is one of image returning states only without inputs. | |
Typedefs | |
| typedef struct BddTrans_TAG * | BddTrans_ptr |
Enumerations | |
| enum | TransImageKind { TRANS_IMAGE_FORWARD_STATE = 0, TRANS_IMAGE_FORWARD_STATE_INPUT = 1, TRANS_IMAGE_BACKWARD_STATE = 2, TRANS_IMAGE_BACKWARD_STATE_INPUT = 3 } |
This is enumeration of possible kinds of image computations. More... | |
Functions | |
| BddTrans_ptr | BddTrans_generic_create (const NuSMVEnv_ptr env, const TransType trans_type, void *transition, void *(*copy)(void *tranistion), void(*destroy)(void *tranistion), bdd_ptr(*compute_image)(void *tranistion, bdd_ptr bdd, TransImageKind kind), bdd_ptr(*compute_k_image)(void *tranistion, bdd_ptr bdd, int k, TransImageKind kind), bdd_ptr(*get_monolithic_bdd)(void *tranistion), void(*synchronous_product)(void *tranistion1, void *const transition2), void(*print_short_info)(void *tranistion, FILE *file), ClusterList_ptr(*trans_get_clusterlist)(void *transition)) |
| Builds the transition relation. | |
| #define BDD_TRANS | ( | x | ) | ((BddTrans_ptr) x) |
| #define BDD_TRANS_CHECK_INSTANCE | ( | x | ) | (nusmv_assert(BDD_TRANS(x) != BDD_TRANS(NULL))) |
| #define TRANS_IMAGE_IS_FORWARD | ( | kind | ) | (!((kind) >> 1)) |
Takes TransImageKind and returns 1 iff the kind is one of forward ones.
Thus 0 is returned iff the kind is backward one.
| #define TRANS_IMAGE_IS_STATE_ONLY | ( | kind | ) | (!((kind) & 1)) |
Takes TransImageKind and returns 1 iff the kind is one of image returning states only without inputs.
Thus 0 is returned iff the image is to return both state and input vars
| typedef struct BddTrans_TAG* BddTrans_ptr |
| enum TransImageKind |
This is enumeration of possible kinds of image computations.
Image computation can be done forward or backward. In both cases it is possible to leave only state or state-input variables. For example, TRANS_IMAGE_FORWARD_STATE is the kind referring to forward image which returns state variables only, i.e. with input variables abstracted away.
Use macros TRANS_IMAGE_IS_FORWARD and TRANS_IMAGE_IS_STATE_ONLY to detect the class of kinds.
| BddTrans_ptr BddTrans_generic_create | ( | const NuSMVEnv_ptr | env, | |
| const TransType | trans_type, | |||
| void * | transition, | |||
| void *(*)(void *tranistion) | copy, | |||
| void(*)(void *tranistion) | destroy, | |||
| bdd_ptr(*)(void *tranistion, bdd_ptr bdd, TransImageKind kind) | compute_image, | |||
| bdd_ptr(*)(void *tranistion, bdd_ptr bdd, int k, TransImageKind kind) | compute_k_image, | |||
| bdd_ptr(*)(void *tranistion) | get_monolithic_bdd, | |||
| void(*)(void *tranistion1, void *const transition2) | synchronous_product, | |||
| void(*)(void *tranistion, FILE *file) | print_short_info, | |||
| ClusterList_ptr(*)(void *transition) | trans_get_clusterlist | |||
| ) |
Builds the transition relation.
This is a generic version of BddTrans constructor. It takes a generic data structure 'transition' and functions to manipulate with it. Ownership of 'transition' is passed to self and will be destroyed during BddTrans destruction by 'destroy' function.
All the parameters are used just to set up struct BddTrans_TAG. See it for the description of, and constraints on, the parameters.
1.6.1