Module `Lib.ReservedIds`

Reserved identifiers.

val abs_ident_string : string

New variables from abstraction.

New oracle input.

val oracle_ident_string : string

New oracle input.

Unique identifier for node instance.

val instance_ident_string : string

Unique identifier for node instance.

First instant flag.

val init_flag_ident_string : string

First instant flag.

Observer for contract requirements.

val all_req_ident_string : string

Observer for contract requirements.

Observer for contract ensures.

val all_ens_ident_string : string

Observer for contract ensures.

New variables from node instance.

val inst_ident_string : string

New variables from node instance.

Initial predicate.

val init_uf_string : string

Initial predicate.

Transition relation.

val trans_uf_string : string

Transition relation.

New clock initialization flag.

val restart_string : string

val state_selected_string : string

val restart_selected_string : string

val state_selected_next_string : string

val restart_selected_next_string : string

val handler_string : string

val unless_string : string

val init_flag_string : string

Init flag string.

Abstraction depth input string.

val depth_input_string : string

Abstraction depth input string.

val max_depth_input_string : string

Abstraction depth input string.

Suffix used for the name of the function encoding functional systems.

val function_of_inputs : string: Suffix used for the name of the function encoding functional systems.