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

module Hashtbl : Stdlib.Hashtbl.S with type Hashtbl.key = t: Hash table over transition systems.

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 equal_scope : t -> t -> bool: Return true if scopes of transition systems are equal

val compare_scope : t -> t -> int: Compare transition systems by their scope

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 init_formals : t -> Var.t list: Variables in the initial state constraint

val trans_formals : t -> Var.t list: Variables in the transition relation

val init_fun_of : t -> Numeral.t -> Term.t: Builds a call to the initial function on state k.

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_flag_of_bound : t -> Numeral.t -> Term.t: Return the init flag at the given bound

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 scope_of_trans_sys : t -> Scope.t: Return the scope identifying 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_candidates : t -> Term.t list: Return list of candidate invariants

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 copy : t -> t: Make a copy of every mutable field of the transition system and its subsystems.

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_subsystems : t -> t list: Return the direct subsystems of a system

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

After

define_and_declare_of_bounds 
  t
  (SMTSolver.define_fun s)
  (SMTSolver.declare_fun t) 
  (SMTSolver.declare_sort t) 
  l
  u

with the solver instance s, initial state constraint and transition relation can be asserted for all offsets between and including l and u.

To extend the range of declared offsets to the range including l and v, use

declare_vars_of_bounds
  (SMTSolver.declare_fun t) 
  (Numeral.succ u)
  v

Evaluating define_and_declare_of_bounds is only needed once per solver instance, and only for the top level transition system.

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_inv : t -> Term.t -> bool: Returns true if the input term is a known invariant of the system.

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 get_invariants : t -> Invs.t: Return invariants with their certificates

val get_all_invariants : t -> Invs.t Scope.Map.t: Returns the invariants for all (sub)systems.

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

`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.