int
CommandAddProperty(
int argc,
char** argv
)
- Adds a property to the list of properties
- See Also
show_property
- Defined in
propCmd.c
int
CommandCheckProperty(
int argc,
char ** argv
)
- Checks properties
- See Also
check_property
- Defined in
propCmd.c
int
CommandShowProperty(
int argc,
char** argv
)
- Shows the currently stored properties
- See Also
add_property
check_spec
check_ltlspec
check_invar
compute
- Defined in
propCmd.c
boolean
PropDb_add(
Prop_ptr p
)
- Insert a property in the DB of properties.
Returns true if out of memory
- Defined in
propDb.c
void
PropDb_clean(
)
- Disposes the DB of properties
- Defined in
propDb.c
void
PropDb_create(
)
- Initializes the DB of properties to an empty DB
- Defined in
propDb.c
void
PropDb_destroy(
)
- Disposes the DB of properties
- Defined in
propDb.c
int
PropDb_fill_game(
SymbTable_ptr symb_table,
node_ptr reachtarget,
node_ptr avoidtarget,
node_ptr reachdeadlock,
node_ptr avoiddeadlock,
node_ptr buchigame,
node_ptr genreactivity
)
- Given for each kind of Game property a list of
respective formulae, this function is responsible to fill the DB with
them. Returns 1 if an error occurred, 0 otherwise
- Defined in
propDb.c
int
PropDb_fill(
SymbTable_ptr symb_table,
node_ptr ctlspec,
node_ptr computespec,
node_ptr ltlspec,
node_ptr pslspec,
node_ptr invarspec
)
- Given for each kind of property a list of
respective formulae, this function is responsible to fill the DB with
them. Returns 1 if an error occurred, 0 otherwise
- Defined in
propDb.c
Prop_ptr
PropDb_get_last(
)
- Returns the last entered property in the DB of properties.
- Defined in
propDb.c
Prop_ptr
PropDb_get_prop_at_index(
const int index
)
- Returns the property whose unique identifier is
provided in input.last entered property in the DB of properties.
- Defined in
propDb.c
int
PropDb_get_prop_index_from_string(
const char* idx
)
- Gets the index of a property form a string.
If the string does not contain a valid index, an error message is emitted
and -1 is returned.
- Defined in
propDb.c
int
PropDb_get_prop_index_from_trace_index(
const int trace_idx
)
- Returns the index of the property associated to a trace.
-1 if no property is associated to the given trace.
- Defined in
propDb.c
int
PropDb_get_prop_index(
const Prop_ptr property
)
- Returns the unique identifier of a property. It
is used in the database of property to identify properties.
- Defined in
propDb.c
lsList
PropDb_get_props_of_type(
const Prop_Type type
)
- Given a property type returns the list of properties
of that type currently located into the property database
- Defined in
propDb.c
int
PropDb_get_size(
)
- Returns the size (i.e. the number of entries)
stored in the DB of properties.
- Defined in
propDb.c
void
PropDb_print_all_status_type(
FILE* file,
Prop_Status status,
Prop_Type type
)
- Prints on the given file stream all the property
stored in the DB of properties whose type and status match the
requested ones.
- Defined in
propDb.c
void
PropDb_print_all_status(
FILE* file,
Prop_Status status
)
- Prints on the given file stream all the property
stored in the DB of properties whose status match the requested one.
- Defined in
propDb.c
void
PropDb_print_all_type(
FILE* file,
Prop_Type type
)
- Prints on the given file stream all the property
stored in the DB of properties whose type match the requested one.
- Defined in
propDb.c
void
PropDb_print_all(
FILE* file
)
- Prints on the given file stream all the property
stored in the DB of properties.
- Defined in
propDb.c
void
PropDb_print_list_header(
FILE* file
)
- optional
- Defined in
propDb.c
int
PropDb_print_prop_at_index(
FILE* file,
const int index
)
- Prints on the given file stream the property
whose unique identifier is specified
- Defined in
propDb.c
int
PropDb_prop_create_and_add(
SymbTable_ptr symb_table,
node_ptr spec,
Prop_Type type
)
- Given a formula and its type, a property is
created and stored in the DB of properties. It returns either -1 in
case of failure, or the index of the inserted property.
- Defined in
propDb.c
int
PropDb_prop_parse_and_add(
SymbTable_ptr symb_table,
const char* str,
const Prop_Type type
)
- Parses and creates a property of a given type from
a string. 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.
- Defined in
propDb.c
void
PropDb_verify_all_type(
Prop_Type type
)
- The DB of properties is searched for a property
of the given type. All the found properties are then verified
calling the appropriate model checking algorithm. Properties already
checked will be ignored.
- Defined in
propDb.c
void
PropDb_verify_all(
)
- All the properties stored in the database not
yet verified will be verified. The properties are verified following
the order CTL/COMPUTE/LTL/INVAR.
- Defined in
propDb.c
void
PropDb_verify_prop_at_index(
const int index
)
- The DB of properties is searched for a property
whose unique identifier match the identifier provided and then if
such a property exists it will be verified calling the appropriate
model checking algorithm. If the property was checked before, then
the property is not checked again.
- Defined in
propDb.c
void
PropPkg_init_cmd(
)
- Initialize the prop package for commands. This must be
called independently from the package initialization function
- Defined in
propCmd.c
void
PropPkg_init(
)
- After you had called this, you must also call
PropPkg_init_cmd if you need to use the interactive shell for
commands
- Defined in
propProp.c
void
PropPkg_quit_cmd(
)
- This must be called independently from
the package initialization function
- Defined in
propCmd.c
void
PropPkg_quit(
)
- Quits the package
- Defined in
propProp.c
const char*
PropType_to_string(
const Prop_Type type
)
- Returns the string corresponding to a property
type for printing it. Returned string must NOT be deleted
- Defined in
propProp.c
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
- Defined in
propProp.c
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
- Defined in
propProp.c
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.
- Defined in
propProp.c
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.
- Defined in
propProp.c
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).
- Defined in
propProp.c
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.
- Defined in
propProp.c
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
- Defined in
propProp.c
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
- Defined in
propProp.c
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
- Defined in
propProp.c
Set_t
Prop_get_cone(
const Prop_ptr self
)
- If the cone of influence of a property has been
computed, this function returns it.
- Defined in
propProp.c
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.
- Defined in
propProp.c
struct ConcTrace_TAG*
Prop_get_ctrace(
const Prop_ptr self
)
- This function is used by CEGAR, and is available only
when mathsat is enabled
- Defined in
propProp.c
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
- Defined in
propProp.c
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
- Defined in
propProp.c
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
- Defined in
propProp.c
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
- Defined in
propProp.c
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
- Defined in
propProp.c
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.
- Defined in
propProp.c
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
- Defined in
propProp.c
int
Prop_get_index(
const Prop_ptr self
)
- Returns the unique identifier of a property
- Defined in
propProp.c
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.
- Defined in
propProp.c
int
Prop_get_number(
const Prop_ptr self
)
- For COMPUTE properties returns the number
resulting from the evaluation of the property.
- Defined in
propProp.c
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
- Defined in
propProp.c
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.
- Defined in
propProp.c
Prop_Status
Prop_get_status(
const Prop_ptr self
)
- Returns the status of the property
- Defined in
propProp.c
char*
Prop_get_text(
const Prop_ptr self
)
- The returned string must be deleted by the caller.
- Defined in
propProp.c
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
- Defined in
propProp.c
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
- Defined in
propProp.c
Prop_Type
Prop_get_type(
const Prop_ptr self
)
- Returns the property kind of the stroed
property, i.e. CTL, LTL, ...
- Defined in
propProp.c
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.
- Defined in
propProp.c
boolean
Prop_is_psl_ltl(
const Prop_ptr self
)
- Returns true if the property is PSL property and it
is LTL compatible
- Defined in
propProp.c
boolean
Prop_is_psl_obe(
const Prop_ptr self
)
- Returns true if the property is PSL property and it
is CTL compatible
- Defined in
propProp.c
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
- Defined in
propProp.c
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
- Defined in
propProp.c
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
- Defined in
propProp.c
GameBddFsm_ptr
Prop_master_get_game_bdd_fsm(
)
- Returns the Game boolean FSM in BDD stored in the
master prop
- Defined in
propProp.c
GameBeFsm_ptr
Prop_master_get_game_be_fsm(
)
- Returns the Game boolean FSM in BE stored in the
master prop
- Defined in
propProp.c
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
- Defined in
propProp.c
GameSexpFsm_ptr
Prop_master_get_game_scalar_sexp_fsm(
)
- Returns the Game scalar FSM stored in the master prop
- Defined in
propProp.c
SexpFsm_ptr
Prop_master_get_scalar_sexp_fsm(
)
- Returns the scalar FSM stored in the master prop
- Defined in
propProp.c
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.
- Defined in
propProp.c
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.
- Defined in
propProp.c
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.
- Defined in
propProp.c
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.
- Defined in
propProp.c
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.
- Defined in
propProp.c
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.
- Defined in
propProp.c
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.
- Defined in
propProp.c
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.
- Defined in
propProp.c
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, ...).
- Defined in
propProp.c
void
Prop_print(
Prop_ptr self,
FILE* file
)
- Prints a property.
PSL properties are specially handled.
- Defined in
propProp.c
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
- Defined in
propProp.c
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
- Defined in
propProp.c
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
- Defined in
propProp.c
void
Prop_set_cone(
Prop_ptr self,
Set_t cone
)
- Stores the cone of influence of the property
- Defined in
propProp.c
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
- Defined in
propProp.c
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.
- Defined in
propProp.c
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
- Defined in
propProp.c
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
- Defined in
propProp.c
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
- Defined in
propProp.c
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
- Defined in
propProp.c
void
Prop_set_index(
Prop_ptr self,
const int index
)
- Sets the unique identifier of a property
- Defined in
propProp.c
void
Prop_set_number_infinite(
Prop_ptr self
)
- Sets the to INFINITE the number resulting from the
evaluation of the property.
- Defined in
propProp.c
void
Prop_set_number_undefined(
Prop_ptr self
)
- Sets the to UNDEFINED the number resulting from the
evaluation of the property.
- Defined in
propProp.c
void
Prop_set_number(
Prop_ptr self,
int n
)
- Sets the number resulting from the
evaluation of the property.
- Defined in
propProp.c
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
- Defined in
propProp.c
void
Prop_set_status(
Prop_ptr self,
Prop_Status s
)
- Sets the status of the property
- Defined in
propProp.c
void
Prop_set_trace(
Prop_ptr self,
int t
)
- Sets the trace number for an unsatisfied property.
- Defined in
propProp.c
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.
- Defined in
propProp.c
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.
- Defined in
propDb.c
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.
- Defined in
propDb.c
void
prop_deinit(
Prop_ptr self
)
- Destroy the elements of a property
- Defined in
propProp.c
void
prop_init(
Prop_ptr self
)
- Initializes the property
- Defined in
propProp.c
void
prop_print(
const Prop_ptr self,
FILE* file
)
- Prints a property.
PSL properties and game propeties are specially handled.
- Defined in
propProp.c
void
prop_set_bdd_fsm(
Prop_ptr self,
BddFsm_ptr fsm,
const boolean duplicate
)
-
- Defined in
propProp.c
void
prop_set_be_fsm(
Prop_ptr self,
BeFsm_ptr fsm,
const boolean duplicate
)
-
- Defined in
propProp.c
void
prop_set_bool_sexp_fsm(
Prop_ptr self,
SexpFsm_ptr fsm,
const boolean duplicate
)
-
- Defined in
propProp.c
void
prop_set_game_bdd_fsm(
Prop_ptr self,
GameBddFsm_ptr fsm,
const boolean duplicate
)
-
- Defined in
propProp.c
void
prop_set_game_be_fsm(
Prop_ptr self,
GameBeFsm_ptr fsm,
const boolean duplicate
)
-
- Defined in
propProp.c
void
prop_set_game_bool_sexp_fsm(
Prop_ptr self,
GameSexpFsm_ptr fsm,
const boolean duplicate
)
-
- Defined in
propProp.c
void
prop_set_game_scalar_sexp_fsm(
Prop_ptr self,
GameSexpFsm_ptr fsm,
const boolean duplicate
)
-
- Defined in
propProp.c
void
prop_set_scalar_sexp_fsm(
Prop_ptr self,
SexpFsm_ptr fsm,
const boolean duplicate
)
-
- Defined in
propProp.c