#include "nusmv/core/fsm/FsmBuilder.h"#include "nusmv/core/wff/ExprMgr.h"#include "nusmv/core/set/set.h"#include "nusmv/core/fsm/sexp/SexpFsm.h"#include "nusmv/core/fsm/sexp/BoolSexpFsm.h"#include "nusmv/core/fsm/bdd/BddFsm.h"#include "nusmv/core/fsm/be/BeFsm.h"#include "nusmv/core/utils/object.h"#include "nusmv/core/utils/utils.h"#include "nusmv/core/utils/OStream.h"Go to the source code of this file.
Defines | |
| #define | PROP(self) ((Prop_ptr) self) |
| To cast and check instances of class Prop. | |
| #define | PROP_CHECK_INSTANCE(self) (nusmv_assert(PROP(self) != PROP(NULL))) |
| #define | PROP_COMPUTE_STRING "Quantitative" |
| #define | PROP_CTL_STRING "CTL" |
| #define | PROP_FALSE_STRING "False" |
| #define | PROP_INVAR_STRING "Invar" |
| #define | PROP_LTL_STRING "LTL" |
| #define | PROP_NOSTATUS_STRING "NoStatus" |
| #define | PROP_NOTYPE_STRING "NoType" |
| #define | PROP_NUMBER_STRING "Number" |
| #define | PROP_PSL_STRING "PSL" |
| #define | PROP_TRUE_STRING "True" |
| #define | PROP_UNCHECKED_STRING "Unchecked" |
Typedefs | |
| typedef enum _Prop_PrintFmt | Prop_PrintFmt |
| typedef struct Prop_TAG * | Prop_ptr |
| typedef enum _Prop_Status | Prop_Status |
| typedef enum _Prop_Type | Prop_Type |
| typedef enum _PropDb_PrintFmt | PropDb_PrintFmt |
Enumerations | |
| enum | _Prop_PrintFmt { PROP_PRINT_FMT_FORMULA, PROP_PRINT_FMT_FORMULA_TRUNC, PROP_PRINT_FMT_INDEX, PROP_PRINT_FMT_NAME, PROP_PRINT_FMT_DEFAULT = PROP_PRINT_FMT_FORMULA } |
| enum | _Prop_Status { Prop_NoStatus, Prop_Unchecked, Prop_True, Prop_False, Prop_Number, Prop_Error } |
Public interface of class 'Prop'. More... | |
| enum | _Prop_Type { Prop_Prop_Type_First = 100, Prop_NoType, Prop_Ctl, Prop_Ltl, Prop_Psl, Prop_Invar, Prop_Compute, Prop_CompId, Prop_Prop_Type_Last } |
Enumerates the different types of a specification. More... | |
| enum | _PropDb_PrintFmt { PROPDB_PRINT_FMT_TABULAR, PROPDB_PRINT_FMT_DEFAULT = PROPDB_PRINT_FMT_TABULAR, PROPDB_PRINT_FMT_XML } |
Format used when printing. More... | |
Functions | |
| void | Prop_apply_coi_for_bdd (const NuSMVEnv_ptr env, Prop_ptr self) |
| Applies cone of influence to the given property. | |
| void | Prop_apply_coi_for_bmc (const NuSMVEnv_ptr env, Prop_ptr self) |
| Applies cone of influence to the given property. | |
| void | Prop_apply_coi_for_scalar (const NuSMVEnv_ptr env, Prop_ptr self) |
| Applies cone of influence to the given property. | |
| BddFsm_ptr | Prop_compute_ground_bdd_fsm (const NuSMVEnv_ptr env, const Prop_ptr self) |
| Computes ground bdd fsm for property \"self\". | |
| BeFsm_ptr | Prop_compute_ground_be_fsm (const NuSMVEnv_ptr env, const Prop_ptr self) |
| Computes ground be fsm for property \"self\". | |
| SexpFsm_ptr | Prop_compute_ground_sexp_fsm (const NuSMVEnv_ptr env, const Prop_ptr self) |
| Computes ground scalar sexp fsm for property \"self\". | |
| Prop_ptr | Prop_copy (Prop_ptr input) |
| The Prop class copier. | |
| boolean | Prop_needs_rewriting (SymbTable_ptr st, const Prop_ptr self) |
| void | Prop_set_environment_fsms (const NuSMVEnv_ptr env, Prop_ptr prop) |
| Sets the FSMs in the property from the environment. | |
| Set_t | Prop_set_from_formula_list (NuSMVEnv_ptr env, node_ptr list, Prop_Type type) |
| Utils function that builds a set of properties out of a cons list of formulae. | |
| short int | PropType_to_node_type (const Prop_Type type) |
| const char * | PropType_to_parsing_string (const Prop_Type type) |
| Returns the parsing type given the property type. | |
| const char * | PropType_to_string (const Prop_Type type) |
| Returns the a string associated to a property type. | |
| #define PROP | ( | self | ) | ((Prop_ptr) self) |
| #define PROP_CHECK_INSTANCE | ( | self | ) | (nusmv_assert(PROP(self) != PROP(NULL))) |
| typedef enum _Prop_PrintFmt Prop_PrintFmt |
| typedef struct Prop_TAG* Prop_ptr |
| typedef enum _Prop_Status Prop_Status |
| typedef enum _Prop_Type Prop_Type |
| typedef enum _PropDb_PrintFmt PropDb_PrintFmt |
| enum _Prop_PrintFmt |
| enum _Prop_Status |
| enum _Prop_Type |
| enum _PropDb_PrintFmt |
| void Prop_apply_coi_for_bdd | ( | const NuSMVEnv_ptr | env, | |
| Prop_ptr | self | |||
| ) |
Applies cone of influence to the given property.
The COI is applied only for BDD-based model checking. To apply for BMC, use Prop_apply_coi_for_bmc. If psl2core is false, then the PSL property is only expanded to remove forall, otherwise it is converted into LTL.
Internal FSMs are computed
| void Prop_apply_coi_for_bmc | ( | const NuSMVEnv_ptr | env, | |
| Prop_ptr | self | |||
| ) |
Applies cone of influence to the given property.
The COI is applied only for BMC-based model checking. To apply for BDD, use Prop_apply_coi_for_bdd. This method creates a new layer for those determinization vars that derives from the booleanization of the fsm deriving from the property cone. That layer will be committed to the BoolEnc and BeEnc encodings only, not to the BddEnc. The newly created layer will be assigned to a name that depends on the property number within the database DbProp. If psl2core is false, then the PSL property is only expanded to remove forall, otherwise it is converted into LTL.
Internal FSMs are computed
| void Prop_apply_coi_for_scalar | ( | const NuSMVEnv_ptr | env, | |
| Prop_ptr | self | |||
| ) |
Applies cone of influence to the given property.
The COI is applied only on the scalar FSM
Internal Scalar FSM is computed
| BddFsm_ptr Prop_compute_ground_bdd_fsm | ( | const NuSMVEnv_ptr | env, | |
| const Prop_ptr | self | |||
| ) |
Computes ground bdd fsm for property \"self\".
Ground bdd fsm is computed (taking COI into account if needed) and registered into self.
| BeFsm_ptr Prop_compute_ground_be_fsm | ( | const NuSMVEnv_ptr | env, | |
| const Prop_ptr | self | |||
| ) |
Computes ground be fsm for property \"self\".
Ground be fsm is computed (taking COI into account if needed) and registered into self.
| SexpFsm_ptr Prop_compute_ground_sexp_fsm | ( | const NuSMVEnv_ptr | env, | |
| const Prop_ptr | self | |||
| ) |
Computes ground scalar sexp fsm for property \"self\".
Ground sexp fsm is computed (taking COI into account if needed) and registered into self.
The Prop class copier.
Note for developers: we do not take an env in input because the fms copy functions do not take it. In order to have copy to another environment we need to extend also those copiers
| boolean Prop_needs_rewriting | ( | SymbTable_ptr | st, | |
| const Prop_ptr | self | |||
| ) |
| void Prop_set_environment_fsms | ( | const NuSMVEnv_ptr | env, | |
| Prop_ptr | prop | |||
| ) |
Sets the FSMs in the property from the environment.
Sets the FSMs in the property from the environment
| Set_t Prop_set_from_formula_list | ( | NuSMVEnv_ptr | env, | |
| node_ptr | list, | |||
| Prop_Type | type | |||
| ) |
Utils function that builds a set of properties out of a cons list of formulae.
The set must be freed by the caller
| short int PropType_to_node_type | ( | const Prop_Type | type | ) |
| const char* PropType_to_parsing_string | ( | const Prop_Type | type | ) |
Returns the parsing type given the property type.
Returns the parsing type given the property type. The returned string must NOT be freed.
| const char* PropType_to_string | ( | const Prop_Type | type | ) |
Returns the a string associated to a property type.
Returns the string corresponding to a property type for printing it. Returned string must NOT be deleted
1.6.1