void
Prop_apply_coi_for_bdd(
Prop_ptr self,
FsmBuilder_ptr helper
)
- The COI is applied only for BDD-based model checking.
To apply for BMC, use Prop_apply_coi_for_bmc
- Side Effects Internal FSMs are computed
void
Prop_apply_coi_for_bmc(
Prop_ptr self,
FsmBuilder_ptr helper
)
- 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.
- Side Effects Internal FSMs are computed
int
Prop_check_type(
const Prop_ptr self,
Prop_Type type
)
- Checks if a property in the database is of a given type.
If the type is correct, value 0 is returned, otherwise an error message
is emitted and value 1 is returned.
Prop_ptr
Prop_create_partial(
Expr_ptr expr,
Prop_Type type
)
- Creates a property structure filling only the property
and property type fields. The property index within the db is not set.
Prop_ptr
Prop_create(
)
- Allocate a property. If no more room is
available then a call to numsv_exit is performed. All the
fields of the prop structure are initialized to either NULL or the
corresponding default type (e.g. Prop_NoType for property type).
void
Prop_destroy(
Prop_ptr self
)
- Free a property. Notice that before freeing the
property all the elements of the property that needs to be freed
will be automatically freed.
BddFsm_ptr
Prop_get_bdd_fsm(
Prop_ptr self
)
- Returns the BDD FSM associated to
the property. Self keeps the ownership of the given fsm
BeFsm_ptr
Prop_get_be_fsm(
const Prop_ptr self
)
- Returns the boolean BE FSM associated to
the property. Self keeps the ownership of the given fsm
SexpFsm_ptr
Prop_get_bool_sexp_fsm(
const Prop_ptr self
)
- Resturns the boolean FSM associated to
the property. Self keeps the ownership of the given fsm
Set_t
Prop_get_cone(
const Prop_ptr self
)
- If the cone of influence of a property has been
computed, this function returns it.
char*
Prop_get_context_text(
const Prop_ptr self
)
- If the property has no explicit context, 'Main' will
be returned. The returned string must be deleted by the caller.
struct ConcTrace_TAG*
Prop_get_ctrace(
const Prop_ptr self
)
- This function is used by CEGAR, and is available only
when mathsat is enabled
Expr_ptr
Prop_get_expr_core(
const Prop_ptr self
)
- Returns the property in a form that it can be handled
by the system (model checking, dependency finder, etc.). This may
imply a conversion and a different structure of the resulting
formula. For example in PSL FORALLs are expanded, SERE are removed,
global operators G and AG are simplified, etc.
Use this function at system-level, and Prop_get_expr to get the
original formula instead
- See Also
Prop_get_expr
Expr_ptr
Prop_get_expr(
const Prop_ptr self
)
- Returns the property stored in the prop. If the
property is PSL, the result should be converted to core symbols
before model checking (see Prop_get_expr_core or
PslNode_convert_psl_to_core).
If the property is a game property, cdr is returned.
- See Also
Prop_get_expr_core
GameBddFsm_ptr
Prop_get_game_bdd_fsm(
Prop_ptr self
)
- Returns the Game BDD FSM associated to
the property. Self keeps the ownership of the given fsm
GameBeFsm_ptr
Prop_get_game_be_fsm(
const Prop_ptr self
)
- Returns the Game boolean BE FSM associated to
the property. Self keeps the ownership of the given fsm
GameSexpFsm_ptr
Prop_get_game_bool_sexp_fsm(
const Prop_ptr self
)
- Resturns the Game boolean FSM in sexp associated to
the property. Self keeps the ownership of the given fsm
string_ptr
Prop_get_game_player(
const Prop_ptr self
)
- Returns true if the property is a game specifications,
i.e. one of REACHTARGET, AVOIDTARGET, REACHDEADLOCK, AVOIDDEADLOCK,
BUCHIGAME, GENREACTIVITY.
GameSexpFsm_ptr
Prop_get_game_scalar_sexp_fsm(
const Prop_ptr self
)
- Resturns the Game scalar FSM associated to
the property. Self keeps the ownership of the given fsm
int
Prop_get_index(
const Prop_ptr self
)
- Returns the unique identifier of a property
char*
Prop_get_number_as_string(
const Prop_ptr self
)
- Returns a number, 'Inifinite' or 'Unchecked'.
The returned string is dynamically created, and caller must free it.
int
Prop_get_number(
const Prop_ptr self
)
- For COMPUTE properties returns the number
resulting from the evaluation of the property.
SexpFsm_ptr
Prop_get_scalar_sexp_fsm(
const Prop_ptr self
)
- Resturns the scalar FSM associated to
the property. Self keeps the ownership of the given fsm
const char*
Prop_get_status_as_string(
const Prop_ptr self
)
- Returns the string corresponding to a property
status for printing it. The caller must NOT free the returned string,
dince it is a constant.
Prop_Status
Prop_get_status(
const Prop_ptr self
)
- Returns the status of the property
char*
Prop_get_text(
const Prop_ptr self
)
- The returned string must be deleted by the caller.
int
Prop_get_trace(
const Prop_ptr self
)
- For unsatisfied properties, the trace number of the
asscociated counterexample is returned. 0 is returned if no trace is
available
const char*
Prop_get_type_as_string(
Prop_ptr self
)
- Returns the string corresponding to a property
type for printing it. Returned string must NOT be deleted
Prop_Type
Prop_get_type(
const Prop_ptr self
)
- Returns the property kind of the stroed
property, i.e. CTL, LTL, ...
boolean
Prop_is_game_prop(
const Prop_ptr self
)
- Returns true if the property is a game specifications,
i.e. one of REACHTARGET, AVOIDTARGET, REACHDEADLOCK, AVOIDDEADLOCK,
BUCHIGAME, GENREACTIVITY.
boolean
Prop_is_psl_ltl(
const Prop_ptr self
)
- Returns true if the property is PSL property and it
is LTL compatible
boolean
Prop_is_psl_obe(
const Prop_ptr self
)
- Returns true if the property is PSL property and it
is CTL compatible
BddFsm_ptr
Prop_master_get_bdd_fsm(
)
- Returns the boolean FSM in BDD stored in the master
prop. The returned value may be NULL when coi is enabled
BeFsm_ptr
Prop_master_get_be_fsm(
)
- Returns the boolean FSM in BE stored in the master
prop. The returned value may be NULL when coi is enabled
SexpFsm_ptr
Prop_master_get_bool_sexp_fsm(
)
- Returns the boolean FSM in sexp stored in the master
prop. The prop package becomes the owner of the given fsm. The
returned value may be NULL when coi is enabled
GameBddFsm_ptr
Prop_master_get_game_bdd_fsm(
)
- Returns the Game boolean FSM in BDD stored in the
master prop
GameBeFsm_ptr
Prop_master_get_game_be_fsm(
)
- Returns the Game boolean FSM in BE stored in the
master prop
GameSexpFsm_ptr
Prop_master_get_game_bool_sexp_fsm(
)
- Returns theGame boolean FSM in sexp stored in
the master prop. The prop package becomes the owner of the given fsm
GameSexpFsm_ptr
Prop_master_get_game_scalar_sexp_fsm(
)
- Returns the Game scalar FSM stored in the master prop
SexpFsm_ptr
Prop_master_get_scalar_sexp_fsm(
)
- Returns the scalar FSM stored in the master prop
void
Prop_master_set_bdd_fsm(
BddFsm_ptr fsm
)
- Set the boolean FSM in BDD of the master prop. The
prop package becomes the owner of the given fsm. This method
destroys the previously set FSM if any.
void
Prop_master_set_be_fsm(
BeFsm_ptr fsm
)
- Set the boolean FSM in BE of the master prop. The
prop package becomes the owner of the given fsm. This method
destroys the previously set FSM if any.
void
Prop_master_set_bool_sexp_fsm(
SexpFsm_ptr fsm
)
- Set the boolean FSM in sexp of the master prop. The
prop package becomes the owner of the given fsm. This method
destroys the previously set FSM if any.
void
Prop_master_set_game_bdd_fsm(
GameBddFsm_ptr fsm
)
- Set the Game boolean FSM in BDD of the master prop. The
prop package becomes the owner of the given fsm. This method
destroys the previously set FSM if any.
void
Prop_master_set_game_be_fsm(
GameBeFsm_ptr fsm
)
- Set the Game boolean FSM in BE of the master prop. The
prop package becomes the owner of the given fsm. This method
destroys the previously set FSM if any.
void
Prop_master_set_game_bool_sexp_fsm(
GameSexpFsm_ptr fsm
)
- Set the Game boolean FSM in sexp of the master prop. The
prop package becomes the owner of the given fsm. This method
destroys the previously set FSM if any.
void
Prop_master_set_game_scalar_sexp_fsm(
GameSexpFsm_ptr fsm
)
- Set the Gamescalar FSM of the master prop. This method
destroys the previously set FSM if any.
void
Prop_master_set_scalar_sexp_fsm(
SexpFsm_ptr fsm
)
- Set the scalar FSM of the master prop. This method
destroys the previously set FSM if any.
void
Prop_print_db(
Prop_ptr self,
FILE* file
)
- Prints a property on the specified FILE
stream. Some of the information stored in the property structure are
printed out (e.g. property, property kind, property status, ...).
void
Prop_print(
Prop_ptr self,
FILE* file
)
- Prints a property.
PSL properties are specially handled.
void
Prop_set_bdd_fsm(
Prop_ptr self,
BddFsm_ptr fsm
)
- The given fsm will be duplicated, so the caller keeps
the ownership of fsm
void
Prop_set_be_fsm(
Prop_ptr self,
BeFsm_ptr fsm
)
- The given fsm will be duplicated, so the caller keeps
the ownership of fsm
void
Prop_set_bool_sexp_fsm(
Prop_ptr self,
SexpFsm_ptr fsm
)
- The given fsm will be duplicated, so the caller keeps
the ownership of fsm
void
Prop_set_cone(
Prop_ptr self,
Set_t cone
)
- Stores the cone of influence of the property
void
Prop_set_ctrace(
Prop_ptr self,
struct ConcTrace_TAG* ctrace
)
- This function is used by CEGAR, and is available only
when mathsat is enabled
void
Prop_set_fsm_to_master(
Prop_ptr self
)
- Copies the FSM informations stored in the master
prop into the corresponding fields of the given prop structure.
void
Prop_set_game_bdd_fsm(
Prop_ptr self,
GameBddFsm_ptr fsm
)
- The given fsm will be duplicated, so the caller keeps
the ownership of fsm
void
Prop_set_game_be_fsm(
Prop_ptr self,
GameBeFsm_ptr fsm
)
- The given fsm will be duplicated, so the caller keeps
the ownership of fsm
void
Prop_set_game_bool_sexp_fsm(
Prop_ptr self,
GameSexpFsm_ptr fsm
)
- The given fsm will be duplicated, so the caller keeps
the ownership of fsm
void
Prop_set_game_scalar_sexp_fsm(
Prop_ptr self,
GameSexpFsm_ptr fsm
)
- The given fsm will be duplicated, so the caller keeps
the ownership of fsm
void
Prop_set_index(
Prop_ptr self,
const int index
)
- Sets the unique identifier of a property
void
Prop_set_number_infinite(
Prop_ptr self
)
- Sets the to INFINITE the number resulting from the
evaluation of the property.
void
Prop_set_number_undefined(
Prop_ptr self
)
- Sets the to UNDEFINED the number resulting from the
evaluation of the property.
void
Prop_set_number(
Prop_ptr self,
int n
)
- Sets the number resulting from the
evaluation of the property.
void
Prop_set_scalar_sexp_fsm(
Prop_ptr self,
SexpFsm_ptr fsm
)
- The given fsm will be duplicated, so the caller keeps
the ownership of fsm
void
Prop_set_status(
Prop_ptr self,
Prop_Status s
)
- Sets the status of the property
void
Prop_set_trace(
Prop_ptr self,
int t
)
- Sets the trace number for an unsatisfied property.
void
Prop_verify(
Prop_ptr self
)
- Depending the property, different model checking
algorithms are called. The status of the property is updated
accordingly to the result of the verification process.
const char*
prop_db_get_prop_type_as_parsing_string(
const Prop_Type type
)
- Returns the parsing type given the property type.
The returned string must NOT be freed.
int
prop_db_prop_parse_from_arg_and_add(
SymbTable_ptr symb_table,
int argc,
const char** argv,
const Prop_Type type
)
- Parses and creates a property of a given type from
an arg structure. If the formula is correct, it is added to the
property database and its index is returned.
Otherwise, -1 is returned.
Valid types are Prop_Ctl, Prop_Ltl, Prop_Psl, Prop_Invar and Prop_Compute.
void
prop_deinit(
Prop_ptr self
)
- Destroy the elements of a property
void
prop_init(
Prop_ptr self
)
- Initializes the property
void
prop_print(
const Prop_ptr self,
FILE* file
)
- Prints a property.
PSL properties and game propeties are specially handled.
void
prop_set_bdd_fsm(
Prop_ptr self,
BddFsm_ptr fsm,
const boolean duplicate
)
-
void
prop_set_be_fsm(
Prop_ptr self,
BeFsm_ptr fsm,
const boolean duplicate
)
-
void
prop_set_bool_sexp_fsm(
Prop_ptr self,
SexpFsm_ptr fsm,
const boolean duplicate
)
-
void
prop_set_game_bdd_fsm(
Prop_ptr self,
GameBddFsm_ptr fsm,
const boolean duplicate
)
-
void
prop_set_game_be_fsm(
Prop_ptr self,
GameBeFsm_ptr fsm,
const boolean duplicate
)
-
void
prop_set_game_bool_sexp_fsm(
Prop_ptr self,
GameSexpFsm_ptr fsm,
const boolean duplicate
)
-
void
prop_set_game_scalar_sexp_fsm(
Prop_ptr self,
GameSexpFsm_ptr fsm,
const boolean duplicate
)
-
void
prop_set_scalar_sexp_fsm(
Prop_ptr self,
SexpFsm_ptr fsm,
const boolean duplicate
)
-