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_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(
Encoding_ptr senc,
node_ptr ctlspec,
node_ptr computespec,
node_ptr ltlspec,
node_ptr invarspec
)
- Given for each kind of property a list of
respective fomulae, 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(
Encoding_ptr senc,
node_ptr prop,
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(
Encoding_ptr senc,
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_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
- 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(
int index,
Expr_ptr expr,
Prop_Type type
)
- Creates a property structure filling only the property
and property type fields. This private function must be accessed
from module PropDb
- 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 boolean FSM in BDD associated to
the property. Self keeps the ownership of the given fsm
- Defined in
propProp.c
Bmc_Fsm_ptr
Prop_get_be_fsm(
const Prop_ptr self
)
- Returns the boolean FSM in BE 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 in sexp 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
Expr_ptr
Prop_get_expr(
const Prop_ptr self
)
- Returns the property stored in the prop
- 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 in sexp 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.
- 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
BddFsm_ptr
Prop_master_get_bdd_fsm(
)
- Returns the boolean FSM in BDD stored in the master prop
- Defined in
propProp.c
Bmc_Fsm_ptr
Prop_master_get_be_fsm(
)
- Returns the boolean FSM in BE stored in the master prop
- 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
- 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
- Defined in
propProp.c
void
Prop_master_set_be_fsm(
Bmc_Fsm_ptr fsm
)
- Set the boolean FSM in BE of the master prop. The
prop package becomes the owner of the given fsm
- 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
- Defined in
propProp.c
void
Prop_master_set_scalar_sexp_fsm(
SexpFsm_ptr fsm
)
- Set the scalar FSM of the master prop
- Defined in
propProp.c
void
Prop_print(
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_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,
Bmc_Fsm_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_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_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(
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
- Defined in
propDb.c
int
prop_db_prop_parse_from_arg_and_add(
Encoding_ptr senc,
int argc,
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_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
- 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,
Bmc_Fsm_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_scalar_sexp_fsm(
Prop_ptr self,
SexpFsm_ptr fsm,
const boolean duplicate
)
-
- Defined in
propProp.c