optional

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

Last updated on 2009/01/30 14h:53