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 
)


Last updated on 2009/03/04 13h:34