-
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/03/04 13h:34