-
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_check_type()
- Check if a property in the database is of a given type
-
Prop_create_partial()
- Creates a property, but does not insert it within
the database, so the property can be used on the fly.
-
Prop_create()
- Allocate a property
-
Prop_destroy()
- Free a property
-
Prop_get_bdd_fsm()
- Returns the BDD FSM of a property
-
Prop_get_be_fsm()
- Returns the BE FSM of a property
-
Prop_get_bool_sexp_fsm()
- Returns the boolean FSM of a property
-
Prop_get_cone()
- Returns the cone of a property
-
Prop_get_context_text()
- Returns the context name of a property
-
Prop_get_ctrace()
- Returns the associated concrete trace structure
-
Prop_get_expr_core()
- Returns the property, but it is converted before in terms
of core symbols.
-
Prop_get_expr()
- Returns the property as it has been parsed and created
-
Prop_get_game_bdd_fsm()
- Returns the Game BDD FSM of a property
-
Prop_get_game_be_fsm()
- Returns the Game BE FSM in of a property
-
Prop_get_game_bool_sexp_fsm()
- Returns the Game boolean FSM of a property
-
Prop_get_game_player()
- Returns true if the property is a game specifications,
i.e. one of REACHTARGET, AVOIDTARGET, REACHDEADLOCK, AVOIDDEADLOCK,
BUCHIGAME, GENREACTIVITY.
-
Prop_get_game_scalar_sexp_fsm()
- Returns the Game scalar FSM of a property
-
Prop_get_index()
- Returns the index of a property
-
Prop_get_number_as_string()
- Returns the number value as a string (only for compute
types)
-
Prop_get_number()
- Returns the number of the property
-
Prop_get_scalar_sexp_fsm()
- Returns the scalar FSM of a property
-
Prop_get_status_as_string()
- Returns the a string associated to a property status
-
Prop_get_status()
- Returns the status of the property
-
Prop_get_text()
- Returns the property text, with no explicit context
-
Prop_get_trace()
- Returns the trace number associated to a property
-
Prop_get_type_as_string()
- Returns the a string associated to a property type
-
Prop_get_type()
- Returns the property type
-
Prop_is_game_prop()
- Returns true if the property is a game specifications,
i.e. one of REACHTARGET, AVOIDTARGET, REACHDEADLOCK, AVOIDDEADLOCK,
BUCHIGAME, GENREACTIVITY.
-
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_master_get_bdd_fsm()
- Returns the boolean FSM in BDD
-
Prop_master_get_be_fsm()
- Returns the boolean FSM in BE
-
Prop_master_get_bool_sexp_fsm()
- Returns the boolean FSM in sexp
-
Prop_master_get_game_bdd_fsm()
- Returns the Game boolean FSM in BDD
-
Prop_master_get_game_be_fsm()
- Returns the Game boolean FSM in BE
-
Prop_master_get_game_bool_sexp_fsm()
- Returns the Game boolean FSM in sexp
-
Prop_master_get_game_scalar_sexp_fsm()
- Returns the Game scalar FSM
-
Prop_master_get_scalar_sexp_fsm()
- Returns the scalar FSM
-
Prop_master_set_bdd_fsm()
- Set the boolean FSM in BDD
-
Prop_master_set_be_fsm()
- Set the boolean FSM in BE
-
Prop_master_set_bool_sexp_fsm()
- Set the boolean FSM in sexp
-
Prop_master_set_game_bdd_fsm()
- Set the Game boolean FSM in BDD
-
Prop_master_set_game_be_fsm()
- Set the Game boolean FSM in BE
-
Prop_master_set_game_bool_sexp_fsm()
- Set the Game boolean FSM in sexp
-
Prop_master_set_game_scalar_sexp_fsm()
- Set the Gamescalar FSM
-
Prop_master_set_scalar_sexp_fsm()
- Set the scalar FSM
-
Prop_print_db()
- Prints a property with info or its position and status
within the database
-
Prop_print()
- Prints a property
-
Prop_set_bdd_fsm()
- Sets the boolean FSM in BDD of a property
-
Prop_set_be_fsm()
- Sets the boolean BE FSM of a property
-
Prop_set_bool_sexp_fsm()
- Sets the boolean FSM of a property
-
Prop_set_cone()
- Sets the cone of a property
-
Prop_set_ctrace()
- Associates given concrete trace structure to the
property
-
Prop_set_fsm_to_master()
- Copies master prop FSM data into prop
-
Prop_set_game_bdd_fsm()
- Sets the Game BDD FSM of a property
-
Prop_set_game_be_fsm()
- Sets the Game boolean BE FSM of a property
-
Prop_set_game_bool_sexp_fsm()
- Sets the Game boolean FSM of a property
-
Prop_set_game_scalar_sexp_fsm()
- Sets the Game scalar FSM of a property
-
Prop_set_index()
- Sets the index of a 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_set_number()
- Sets the number of the property
-
Prop_set_scalar_sexp_fsm()
- Sets the scalar FSM of a property
-
Prop_set_status()
- Sets the status of the property
-
Prop_set_trace()
- Sets the trace number
-
Prop_verify()
- Verifies a given property
-
prop_db_get_prop_type_as_parsing_string()
- Returns the parsing type given the property type
-
prop_db_prop_parse_from_arg_and_add()
- Add a property to the database from an arg structure
and a type
-
prop_deinit()
- Destroy the elements of a property
-
prop_init()
- Initializes the property
-
prop_print()
- Prints a property
-
prop_set_bdd_fsm()
-
-
prop_set_be_fsm()
-
-
prop_set_bool_sexp_fsm()
-
-
prop_set_game_bdd_fsm()
-
-
prop_set_game_be_fsm()
-
-
prop_set_game_bool_sexp_fsm()
-
-
prop_set_game_scalar_sexp_fsm()
-
-
prop_set_scalar_sexp_fsm()
-
Last updated on 2009/03/04 13h:34