prop.h
External header file
propInt.h
Internal header file
propCmd.c
Shell interface for the prop package.
propDb.c
Property database
propProp.c
Main routines for the prop data structure

prop.h

External header file

By: Marco Roveri, Roberto Cavada


propInt.h

Internal header file

By: Marco Roveri, Roberto Cavada

See Alsooptional


propCmd.c

Shell interface for the prop package.

By: Marco Roveri

This file contains the interface of the prop package with the interactive shell.

See AlsocmdCmd.c

PropPkg_init_cmd()
Initiliaze the prop package for commands
PropPkg_quit_cmd()
Quit the prop package for commands
CommandShowProperty()
Shows the currently stored properties
CommandAddProperty()
Adds a property to the list of properties
CommandCheckProperty()
Checks properties

propDb.c

Property database

By: Roberto Cavada, Marco Roveri

Primitives to create, query and manipulate a database of property is provided.

PropDb_create()
Initializes the DB of properties
PropDb_destroy()
Disposes the DB of properties
PropDb_clean()
Disposes the DB of properties
PropDb_fill()
Fills the DB of properties
PropDb_fill_game()
Fills the DB of (game) properties
PropDb_add()
Inserts a property in the DB of properties
PropDb_prop_create_and_add()
Inserts a property in the DB of properties
PropDb_get_last()
Returns the last entered property in the DB
PropDb_get_prop_at_index()
Returns the property indexed by index
PropDb_get_prop_index()
Returns the index of a property in the database
PropDb_get_size()
Returns the size of the DB
PropDb_print_list_header()
Prints the header of the property list
PropDb_print_prop_at_index()
Prints the specified property from the DB
PropDb_print_all()
Prints all the properties stored in the DB
PropDb_print_all_status_type()
Prints all the properties stored in the DB
PropDb_print_all_type()
Prints all the properties stored in the DB
PropDb_print_all_status()
Prints all the properties stored in the DB
PropDb_get_props_of_type()
Given a property type returns the list of properties of that type currently located into the property database
PropDb_prop_parse_and_add()
Add a property to the database from a string and a type
PropDb_get_prop_index_from_string()
Get a valid property index from a string
PropDb_get_prop_index_from_trace_index()
Returns the index of the property associated to a trace.
PropDb_verify_prop_at_index()
Verifies a given property
PropDb_verify_all_type()
Verifies all properties of a given type
PropDb_verify_all()
Verifies all the properties in the DB
prop_db_prop_parse_from_arg_and_add()
Add a property to the database from an arg structure and a type
prop_db_get_prop_type_as_parsing_string()
Returns the parsing type given the property type

propProp.c

Main routines for the prop data structure

By: Marco Roveri, Roberto Cavada

Main routines for the manipulation of the prop data structure. A "master" property is also defined to be used to represent the whole system, for instance to perform reachability or to perform simulation. Moreover a primitives to create, query and manipulate a database of property is provided.

PropPkg_init()
Initializes the package: master property and property database are allocated
PropPkg_quit()
Quits the package
Prop_create()
Allocate a property
Prop_destroy()
Free a property
Prop_get_expr()
Returns the property as it has been parsed and created
Prop_get_expr_core()
Returns the property, but it is converted before in terms of core symbols.
Prop_get_cone()
Returns the cone of a property
Prop_set_cone()
Sets the cone of a property
Prop_get_type()
Returns the property type
Prop_get_status()
Returns the status of the property
Prop_set_status()
Sets the status of the property
Prop_get_number()
Returns the number of the property
Prop_set_number()
Sets the number of the property
Prop_set_number_infinite()
Sets the number of the property to INFINITE
Prop_set_number_undefined()
Sets the number of the property to UNDEFINED
Prop_get_trace()
Returns the trace number associated to a property
Prop_set_trace()
Sets the trace number
Prop_get_scalar_sexp_fsm()
Returns the scalar FSM of a property
Prop_get_game_scalar_sexp_fsm()
Returns the Game scalar FSM of a property
Prop_set_scalar_sexp_fsm()
Sets the scalar FSM of a property
Prop_set_game_scalar_sexp_fsm()
Sets the Game scalar FSM of a property
Prop_get_bool_sexp_fsm()
Returns the boolean FSM of a property
Prop_get_game_bool_sexp_fsm()
Returns the Game boolean FSM of a property
Prop_set_bool_sexp_fsm()
Sets the boolean FSM of a property
Prop_set_game_bool_sexp_fsm()
Sets the Game boolean FSM of a property
Prop_get_bdd_fsm()
Returns the BDD FSM of a property
Prop_get_game_bdd_fsm()
Returns the Game BDD FSM of a property
Prop_set_bdd_fsm()
Sets the boolean FSM in BDD of a property
Prop_set_game_bdd_fsm()
Sets the Game BDD FSM of a property
Prop_get_be_fsm()
Returns the BE FSM of a property
Prop_get_game_be_fsm()
Returns the Game BE FSM in of a property
Prop_set_be_fsm()
Sets the boolean BE FSM of a property
Prop_set_game_be_fsm()
Sets the Game boolean BE FSM of a property
Prop_apply_coi_for_bdd()
Applies cone of influence to the given property
Prop_apply_coi_for_bmc()
Applies cone of influence to the given property
Prop_print_db()
Prints a property with info or its position and status within the database
Prop_print()
Prints a property
Prop_get_number_as_string()
Returns the number value as a string (only for compute types)
Prop_get_context_text()
Returns the context name of a property
Prop_get_text()
Returns the property text, with no explicit context
Prop_master_get_scalar_sexp_fsm()
Returns the scalar FSM
Prop_master_get_game_scalar_sexp_fsm()
Returns the Game scalar FSM
Prop_master_set_scalar_sexp_fsm()
Set the scalar FSM
Prop_master_set_game_scalar_sexp_fsm()
Set the Gamescalar FSM
Prop_master_get_bool_sexp_fsm()
Returns the boolean FSM in sexp
Prop_master_get_game_bool_sexp_fsm()
Returns the Game boolean FSM in sexp
Prop_master_set_bool_sexp_fsm()
Set the boolean FSM in sexp
Prop_master_set_game_bool_sexp_fsm()
Set the Game boolean FSM in sexp
Prop_master_get_bdd_fsm()
Returns the boolean FSM in BDD
Prop_master_get_game_bdd_fsm()
Returns the Game boolean FSM in BDD
Prop_master_set_bdd_fsm()
Set the boolean FSM in BDD
Prop_master_set_game_bdd_fsm()
Set the Game boolean FSM in BDD
Prop_master_get_be_fsm()
Returns the boolean FSM in BE
Prop_master_get_game_be_fsm()
Returns the Game boolean FSM in BE
Prop_master_set_be_fsm()
Set the boolean FSM in BE
Prop_master_set_game_be_fsm()
Set the Game boolean FSM in BE
Prop_set_fsm_to_master()
Copies master prop FSM data into prop
Prop_get_type_as_string()
Returns the a string associated to a property type
Prop_get_status_as_string()
Returns the a string associated to a property status
Prop_check_type()
Check if a property in the database is of a given type
Prop_verify()
Verifies a given property
PropType_to_string()
Returns the a string associated to a property type
Prop_is_psl_ltl()
Returns true if the property is PSL property and it is LTL compatible
Prop_is_psl_obe()
Returns true if the property is PSL property and it is CTL compatible
Prop_is_game_prop()
Returns true if the property is a game specifications, i.e. one of REACHTARGET, AVOIDTARGET, REACHDEADLOCK, AVOIDDEADLOCK, BUCHIGAME, GENREACTIVITY.
Prop_get_game_player()
Returns true if the property is a game specifications, i.e. one of REACHTARGET, AVOIDTARGET, REACHDEADLOCK, AVOIDDEADLOCK, BUCHIGAME, GENREACTIVITY.
Prop_create_partial()
Creates a property, but does not insert it within the database, so the property can be used on the fly.
Prop_get_ctrace()
Returns the associated concrete trace structure
Prop_set_ctrace()
Associates given concrete trace structure to the property
Prop_get_index()
Returns the index of a property
Prop_set_index()
Sets the index of a property
prop_init()
Initializes the property
prop_deinit()
Destroy the elements of a property
prop_print()
Prints a property
prop_set_scalar_sexp_fsm()
prop_set_game_scalar_sexp_fsm()
prop_set_bool_sexp_fsm()
prop_set_game_bool_sexp_fsm()
prop_set_bdd_fsm()
prop_set_game_bdd_fsm()
prop_set_be_fsm()
prop_set_game_be_fsm()

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