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.

exception PropertyNotFound of string
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 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 fn_congruence_group = {
  1. fcg_template : Term.t;
  2. fcg_a_vars : Var.t list;
  3. fcg_b_vars : Var.t list;
  4. fcg_apps : StateVar.t list list;
}

Functional congruence group of an (abstracted) function with container-typed arguments: a quantifier-free template over one pair of free variables per function argument, together with the argument state variable tuples of the function's applications in the system's subtree. Substituting two applications (at two bounds) into the template yields a ground congruence instance (see fn_congruence_instances).

type instance = {
  1. uid : int;
    (*

    Unique identifier of the instance

    *)
  2. pos : Lib.position;
    (*

    Position of the call.

    It is used as a unique identifier, which works provided the call is not expanded in the definition of an array. TODO: Change code to use uid for equality instead.

    *)
  3. map_down : StateVar.t StateVar.StateVarMap.t;
    (*

    Map from the state variables of this system to the state variables of the instance. If the same variable is passed in multiple arguments, the variable is only associated to one of the formal parameters. Notice that for output and local variables there is a one-to-one correspondence.

    *)
  4. map_up : StateVar.t StateVar.StateVarMap.t;
    (*

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

    *)
  5. 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.

    *)
  6. assumes : (Term.t list * Term.t) option;
    (*

    None if there is no assumption associated to the call. Otherwise, Some (l,s) where l is the list of instantiated assume terms, and s is SoFar(conjunction of instantiated assume terms)

    *)
}

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 global_constraints : t -> Term.t list

Return global constraints on free constants

val fn_congruence_groups : t -> fn_congruence_group list

Return the functional congruence groups of the system's subtree

val fn_congruence_instances : t -> Numeral.t -> Term.t list

fn_congruence_instances t k returns the ground functional congruence instances for every pair of function applications over bounds 0..k. Empty when the system's subtree has no function with container-typed arguments.

Each is a valid formula of the intended semantics, so asserting any subset of them is sound, and an engine can leave them all out until a query comes back satisfiable. Given to the solver as terms to evaluate, those the model makes false are exactly the instances that refute it; when there are none the model satisfies determinism, so the counterexample it represents is genuine.

val has_fn_congruence_groups : t -> bool

Return true if the system's subtree has at least one functional congruence group

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 set_global_constraints : t -> Term.t list -> t
val set_logic : t -> TermLib.logic -> t

Set the logic of the transition system

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 get_function_symbols : t -> UfSymbol.t list

Returns function symbols declared in the transition system

val subsystem_includes_function_symbol : t -> bool

Returns true if any subsystem (including top-level system) includes a function symbol

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 -> ?datatype_types:Type.t list -> ?fn_congruence_groups:fn_congruence_group list -> Scope.t -> StateVar.t option -> StateVar.t -> StateVar.t list -> StateVar.StateVarSet.t -> LustreExpr.expr LustreExpr.bound_or_fixed list StateVar.StateVarHashtbl.t -> Var.t list -> Term.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 -> bool -> 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_sofar_term : t -> Lib.position -> (Term.t * bool) option

Get SoFar expression associated to a given node call (if any), and its invariance status

get_sofar_term t p returns None if the subsystem instance identified by position p does not exist or does not have assumptions. Otherwise, it returns Some (t,b) where t corresponds to SoFar(conjunction of instantiated assume terms), and b is true if the term has proven invariant.

val get_max_depth : t -> int

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 unconstrained_inputs : t -> StateVar.StateVarSet.t

Return unconstrained inputs 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 assert_global_constraints : t -> (Term.t -> unit) -> unit

assert_global_constraints t a uses function a to assert the global constraints of transition system t

The signature of a is that of SMTSolver.assert_term

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.

val get_ufs : t -> UfSymbol.t list

Return the uninterpreted function symbols declared in this system (e.g. the symbols introduced for imported functions), excluding the uninterpreted symbols of state variables and the init and trans predicates.

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 get_prop_expr : t -> string -> string option

Return the expression of the property

get_prop_expr t n returns the saved source expression in the transition system of the first property of name n.

val get_prop_kind : t -> string -> Property.prop_kind

Return current kind of the property

get_prop_kind t n returns the kind 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_all_nocands t returns the status saved in the transition system of each property along with the name of the property.

val get_prop_kind_all_nocands : t -> (string * Property.prop_kind) list

Return the kind of all properties excepted candidates

get_prop_kind_all_nocands t returns the kind saved in the transition system of each property along with the name of the property.

val get_ctr : t -> StateVar.t option

Return the internally generated counter for reachability queries (if it exists)

val get_prop_status_and_kind_all_nocands : t -> (string * Property.prop_status * Property.prop_kind) list

Return current status and kind of all properties excepted candidates

get_prop_status_and_kind_all_nocands 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 get_prop_status_and_kind_and_expr_all_nocands : t -> (string * Property.prop_status * Property.prop_kind * Term.t) list
val props_list_of_bound : t -> Numeral.t -> (string * Term.t) list

Instantiate all properties to the bound

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

Instantiate all properties to the bound, but only properties where the BMC engine CANNOT skip steps. This only includes invariant properties and reachability queries without lower bounds.

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

Instantiate all properties to the bound, but only properties where the BMC engine CAN skip steps. This only includes reachability queries with lower bounds.

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_real_property : t -> bool

Returns true iff sys has at least one real (not candidate) 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 -> Scope.t -> 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 get_is_visible : t -> bool
val scope_is_visible : Scope.t -> t -> bool
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

val enforce_constantness_via_equations : t -> t * StateVar.t list

Return a semantically equivalent system where constantness is enforced by making the current value of a constant stream equal to its previous value in the transition relation predicate, and the list of constant variables that have been converted to a state variable

val global_const_state_vars : t -> StateVar.t list

Return the global constant state variables of the transition system

val slice_system : t -> StateVar.StateVarSet.t -> t

slice_system sys vars returns a new system obtained by restricting sys to only the state variables in vars. Technically the state variables not in vars are retained in the system but terms referencing them are removed. That is if `x` and `y` are both not in vars then the declaration of `x` and `y` remain in the system however a term of the form `x and y` will be removed.

  • parameter sys

    The original system.

  • parameter vars

    The set of state variables to retain in the sliced system.

  • returns

    A new system where terms wich do not refer to variables in the sliced system are removed.