# Module `TransSys`

Representation of a transition system

A transition system is uniquely identified by its scope. A transition system can contain subsystems. For each subsystem there is a map of all state variables of the subsystem to some state variable in this transition system, and a function to guard term in the scope of the subsystem to make them valid in this transition system. There must be no cycles in the subsystem relation, that is, a transition system cannot have itself as a subsystem.

A transition system constrains values of the set of state variables of a scope that make up the state of the transition system. The state variables in `state_vars`

are assumed to be of the same scope `scope`

. The initial state constraint `init`

is a term over these state variables at offset `init_base`

, the transition relation `trans`

is a term over state variables at offsets `trans_base`

and `trans_base - 1`

.

- author
- Christoph Sticksel

- author
- Adrien Champion

`val init_base : Numeral.t`

Offset of the current state variables in initial state constraint

`val trans_base : Numeral.t`

Offset of current state variables in transition relation, subtract one for the offset of the previous state variables

`val prop_base : Numeral.t`

Offset of current state variables in properties and invariants, subtract one for the offset of the previous state variables

`type t`

The transition system

Constructed with the function

`mk_trans_sys`

`type pred_def`

`= UfSymbol.t * (Var.t list * Term.t)`

Predicate definition

An uninterpreted function symbols and the pair of its formal parameters and its definition, to be used in an association list.

`type instance`

`=`

`{`

`pos : Lib.position;`

Position as a unique identifier of the instance

`map_down : StateVar.t StateVar.StateVarMap.t;`

Map from the state variables of this system to the state variables of the instance

`map_up : StateVar.t StateVar.StateVarMap.t;`

Map from state variables of the called system to the state variables of this system

`guard_clock : Numeral.t -> Term.t -> Term.t;`

Add a guard to the Boolean term to make it true whenver the the clock of the subsystem instance is false

`guard_clock t`

assumes that`t`

is a Boolean term and returns the term`c => t`

where`c`

is the clock of the subsystem instance.`}`

Instance of a subsystem

`val pp_print_trans_sys : Stdlib.Format.formatter -> t -> unit`

Pretty-print a transition system

`val pp_print_subsystems : bool -> Stdlib.Format.formatter -> t -> unit`

Pretty-print a transition system and its subsystems

`pp_print_subsystems t f s`

pretty-prints the top node of transition system`s`

, if parameter`t`

is set to true, and also all its subsystems.

`val pp_print_trans_sys_name : Stdlib.Format.formatter -> t -> unit`

Pretty-print the name of a transition system

## Accessors

`val init_of_bound : (UfSymbol.t -> unit) option -> t -> Numeral.t -> Term.t`

Close the initial state constraint by binding all instance identifiers, and bump the state variable offsets to be at the given bound

`val trans_of_bound : (UfSymbol.t -> unit) option -> t -> Numeral.t -> Term.t`

Close the initial state constraint by binding all instance identifiers, and bump the state variable offsets to be at the given bound

`val init_uf_symbol : t -> UfSymbol.t`

Predicate for the initial state constraint

`val trans_uf_symbol : t -> UfSymbol.t`

Predicate for the transition relation

`val trans_fun_of : t -> Numeral.t -> Numeral.t -> Term.t`

Builds a call to the transition relation function linking state

`k`

and`k'`

.

`val init_flag_state_var : t -> StateVar.t`

Return the state variable for the init flag

`val init_trans_open : t -> StateVar.t list * Term.t * Term.t`

Return the instance variables of this transition system, the initial state constraint at

`init_base`

and the transition relation at`trans_base`

with the instance variables free.

`val set_subsystem_equations : t -> Scope.t -> Term.t -> Term.t -> t`

Update the init and trans equations of a subsystem

`val get_logic : t -> TermLib.logic`

Return the logic fragment needed to express the transition system

`val get_properties : t -> Property.t list`

Returns the properties in a transition system.

`val get_real_properties : t -> Property.t list`

Return current status of all real (not candidate) properties

`val is_candidate : t -> string -> bool`

Return true if the property is a candidate invariant

`val get_candidate_properties : t -> Property.t list`

Return list of candidate invariants properties

`val get_unknown_candidates : t -> Term.t list`

Return candidate invariants that have not been proved or disproved yet

`val get_mode_requires : t -> Term.t option * (Scope.t * Term.t) list`

Returns the optional assumption term and the mode requirement terms for each mode.

Used by test generation.

`val get_split_properties : t -> Property.t list * Property.t list * Property.t list`

Returns the list of properties in a transition system, split by their status as

`valid, invalid, unknown`

.

`val mk_trans_sys : ?instance_var_id_start:int -> Scope.t -> StateVar.t option -> StateVar.t -> (StateVar.t * Term.t list) list -> StateVar.t list -> LustreExpr.expr LustreExpr.bound_or_fixed list StateVar.StateVarHashtbl.t -> Var.t list -> UfSymbol.t list -> UfSymbol.t -> Var.t list -> Term.t -> UfSymbol.t -> Var.t list -> Term.t -> (t * instance list) list -> Property.t list -> (Term.t option * (Scope.t * Term.t) list) -> Invs.t -> t * int`

`val iter_subsystems : ?include_top:bool -> (t -> unit) -> t -> unit`

Iterate bottom-up over subsystems, including the top level system without repeating subsystems already seen

`iter_subsystems f t`

evaluates`f`

for all subsystem of`t`

. The subsystems are presented bottom-up such that for each evaluation`f t`

the function`f s`

has already been evaluated for each subsystem`s`

of`t`

. If`t`

contains a subsystem`s`

twice, no matter at which level,`f s`

is evaluated only once.

`val fold_subsystems : ?include_top:bool -> ('a -> t -> 'a) -> 'a -> t -> 'a`

Fold bottom-up over subsystems, including or excluding the top level system, without repeating subsystems already seen

`fold_subsystems f t`

first evaluates`f a s`

for some subsystem`s`

of`t`

that does not have subsystems itself. It then passes the result as first argument to`f`

with the second argument being a subsystem for which all subsystems have been evaluated with`f`

. If`t`

contains a subsystem`s`

twice, no matter at which level,`f s`

is evaluated only once.The systems are passes in topological order such that the each system is presented to

`f`

only after all its subsystems. The function`f`

is evaluated for the top system last, unless the optional labelled parameter`include_top`

is set to false.

`val fold_subsystem_instances : (t -> (t * instance) list -> 'a list -> 'a) -> t -> 'a`

Fold bottom-up over subsystem instances

`fold_subsystem_instances f t`

evaluates`f s i l`

for each subsystem instance in the system`t`

, including`t`

itself. The function`f`

is evaluated with the subsystem`s`

, the reverse sequence of instantiations`i`

that reach the top system`t`

, and the evaluations of`f`

on the subsystems of`s`

. The sequence of instantiations`i`

contains at its head a system that has`s`

as a direct subsystem, together with the instance parameters. For the top system`i`

is the empty list.The systems are presented in topological order such that each system is presented to

`f`

after all its subsystem instances have been presented.

`val get_subsystem_instances : t -> (t * instance list) list`

Return the direct subsystems of a system and their instances

`val find_subsystem_of_scope : t -> Scope.t -> t`

Find the named subsystem

`find_subsystem_of_scope t s`

returns the subsystem of`t`

identified by the scope`s`

. We assume that all subsystems with the same scope are identical. The transition system`t`

itself is returned if`s`

is its scope.Raise

`Not_found`

if there is no transition system of scope`s`

in the subsystems of`t`

.

`val get_max_depth : t -> int`

`val map_cex_prop_to_subsystem : (Scope.t -> instance -> (StateVar.t * Model.value list) list -> Model.value list -> Model.value list) -> t -> (StateVar.t * Model.value list) list -> Property.t -> t * instance list * (StateVar.t * Model.value list) list * Property.t`

## State Variables

`val state_vars : t -> StateVar.t list`

Return the state variables of a transition system

`val add_global_constant : t -> Var.t -> t`

Add a global constant to the transition system and all the subnodes

`val vars_of_bounds : ?with_init_flag:bool -> t -> Numeral.t -> Numeral.t -> Var.t list`

Return instances of the state variables of the transition system between given instants

`vars_of_bounds t l u`

returns the list of instances of the state variables of the transition system`t`

between and including`l`

and`u`

. Include the state variable for the init flag unless the optional labelled argument`with_init_flag`

is set to false.

`val declare_vars_of_bounds : ?declare_init_flag:bool -> t -> (UfSymbol.t -> unit) -> Numeral.t -> Numeral.t -> unit`

Declare variables of the transition system between given instants

`declare_vars_of_bounds t f l u`

evaluates`f`

with the uninterpreted function symbol of each state variable of the transition system`t`

at each instant between and including`l`

and`u`

. Include the state variable for the init flag unless the optional labelled argument`declare_init_flag`

is set to false.

`val declare_const_vars : t -> (UfSymbol.t -> unit) -> unit`

`val declare_init_flag_of_bounds : t -> (UfSymbol.t -> unit) -> Numeral.t -> Numeral.t -> unit`

Declare the init flag of the transition system between given instants

`declare_init_flag_of_bounds t f l u`

evaluates`f`

with the uninterpreted function symbol of the state variable for the init flag of the transition system`t`

at each instant between and including`l`

and`u`

.

`val declare_sorts_ufs_const : t -> (UfSymbol.t -> unit) -> (Type.t -> unit) -> unit`

Declare the sorts, uninterpreted functions and const variables of this system and its subsystems.

`val define_subsystems : t -> (UfSymbol.t -> Var.t list -> Term.t -> unit) -> unit`

Declare the init and trans functions of the subsystems

`val define_and_declare_of_bounds : ?declare_sub_vars:bool -> t -> (UfSymbol.t -> Var.t list -> Term.t -> unit) -> (UfSymbol.t -> unit) -> (Type.t -> unit) -> Numeral.t -> Numeral.t -> unit`

Define predicates and declare constant and global state variables, declare state variables of top system between and including the given offsets

`define_and_declare_of_bounds t f g l u`

first evaluates the function`f`

for the definition of the initial state constraint predicate and the transitions relation predicate of the top system in the transition system`t`

and all its subsystems. It then evaluates the function`g`

with the declarations of all constant and global state variables of the top system, and with the declarations of the remaining state variables of the top system between and including the offsets`l`

and`u`

.If

`l > u`

, only declarations of constant and global state are passed to`g`

, and`f`

is still evaluated with all definitions.If the optional parameter

`declare_sub_vars`

is`true`

, it also iterates over all subsystems and evaluates`g`

with the declarations of their constants and global state variables, and their state variables between and including`l`

and`u`

. Thus the subsystems can be run in parallel to the top system.The signatures of

`f`

and`g`

are those of`SMTSolver.define_fun`

and`SMTSolver.declare_fun`

, repsectively, partially evaluated with their first argument.

`val uf_defs : t -> pred_def list`

Return predicate definitions of initial state and transition relation of the top system and all its subsystem in reverse topological order

`uf_defs t`

returns a list of predicate definitions of the top system`t`

and all its subsystems such that the definitions of a subsystem precede the definitions of all systems containing it. The definition of the initial state predicate precedes the definition of the transition relation predicate.

## Properties

`val property_of_name : t -> string -> Property.t`

`val get_prop_term : t -> string -> Term.t`

Return term of the property

`get_prop_term t n`

returns the term of the first property of name`n`

in the transistion system`t`

.

`val get_prop_status : t -> string -> Property.prop_status`

Return current status of the property

`get_prop_status t n`

returns the status saved in the transition system of the first property of name`n`

.

`val is_proved : t -> string -> bool`

Return true if the property is proved invariant

`val is_disproved : t -> string -> bool`

Return true if the property is proved not invariant

`val get_prop_status_all_nocands : t -> (string * Property.prop_status) list`

Return current status of all properties excepted candidates

`get_prop_status t`

returns the status saved in the transition system of each property along with the name of the property.

`val get_prop_status_all_unknown : t -> (string * Property.prop_status) list`

Return current status of all unknown properties

`get_prop_status_all_unknown t`

returns the status saved in the transition system of each property which is considered to be unknown along with the name of the property.According to

`Property.prop_status_known`

, a property is known if it is invariant, or has a`k`

-step counterexample.

`val props_list_of_bound : t -> Numeral.t -> (string * Term.t) list`

Instantiate all properties to the bound

`val set_prop_status : t -> string -> Property.prop_status -> unit`

Update current status of the property

`set_prop_status t n s`

sets the status saved in the transition system of the first property of name`n`

to`s`

.

`val set_prop_invariant : t -> string -> Certificate.t -> unit`

Mark property as invariant

`val set_prop_false : t -> string -> (StateVar.t * Model.value list) list -> unit`

Mark property as false

`val set_prop_ktrue : t -> int -> string -> unit`

Mark property as k-true

`val set_prop_unknown : t -> string -> unit`

`val set_subsystem_properties : t -> Scope.t -> Property.t list -> t`

`val has_properties : t -> bool`

Returns true iff sys has at least one property.

`val all_props_proved : t -> bool`

Return true if all properties which are not candidates are either valid or invalid

`val at_least_one_prop_falsified : t -> bool`

Return true if at least one prop has been falsified

`val add_properties : t -> Property.t list -> t`

Add properties to the transition system

`val add_invariant : t -> Term.t -> Certificate.t -> bool -> Term.t`

Add an invariant to the transition system.

`val add_scoped_invariant : t -> string list -> Term.t -> Certificate.t -> bool -> Term.t`

Add an invariant to the transition system.

Returns the normalized terms and a boolean indicating whether it is one state.

`val invars_of_bound : ?one_state_only:bool -> t -> Numeral.t -> Term.t list`

Instantiate invariants and valid properties to the bound

`val clear_invariants : t -> unit`

Clear invariants of the top_level system

`val clear_all_invariants : t -> unit`

Clear invariants of all (sub)systems

`val instantiate_term_all_levels : t -> Numeral.t -> Scope.t -> Term.t -> bool -> (t * Term.t list) * (t * Term.t list) list`

Instantiate a term of a given scope from all instances of the system of that scope upwards to the top system

`instantiate_term_all_levels t i s e ts`

instantiates the Boolean term`e`

of scope`s`

in all systems it is a subsystem of, and further upwards until the top system`t`

. The offset`i`

is the offset of the current instant in the term`e`

.`ts`

is true if the invariant is two states.Return the top system

`s`

paired with the instances of the term in it, and a list of all systems between the top system`t`

and the system`s`

, including`s`

but excluding`t`

, each system paired with the instances of`e`

in it.The offset

`i`

is needed to properly guard the term`e`

for clocked system instances.

`val get_state_var_bounds : t -> LustreExpr.expr LustreExpr.bound_or_fixed list StateVar.StateVarHashtbl.t`

Return arrays bounds of state variables of array type used in the system

`val instantiate_term_cert_all_levels : t -> Numeral.t -> Scope.t -> (Term.t * Certificate.t) -> bool -> (t * (Term.t * Certificate.t) list) * (t * (Term.t * Certificate.t) list) list`

Same as above but with certificates