Module Ast

module Ast: sig .. end
Abstract syntax tree and transition systems


Abstract syntax tree and transition systems

Untyped transition system


type dnf = Types.SAtom.t list 
Disjunctive normal form: each element of the list is a disjunct
type type_constructors = Hstring.t * Hstring.t list 
Type and constructors declaration: ("t", ["A";"B"]) represents the declaration of type t with two constructors A and B. If the list of constructors is empty, the type t is defined abstract.
type swts = (Types.SAtom.t * Types.Term.t) list 
The type of case switches case | c1 : t1 | c2 : t2 | _ : tn
type glob_update = 
| UTerm of Types.Term.t
| UCase of swts (*Updates of global variables, can be a term or a case construct.*)
type update = {
   up_loc : Util.loc; (*location information*)
   up_arr : Hstring.t; (*Name of array to update (ex. A)*)
   up_arg : Variable.t list; (*list of universally quantified variables*)
   up_swts : swts; (*condition (conjunction)(ex. C) and term (ex. t*)
}
conditionnal updates with cases, ex. A[j] := case | C : t | _ ...
type transition_info = {
   tr_name : Hstring.t; (*name of the transition*)
   tr_args : Variable.t list; (*existentially quantified parameters of the transision*)
   tr_reqs : Types.SAtom.t; (*guard*)
   tr_ureq : (Variable.t * dnf) list; (*global condition of the guard, i.e. universally quantified DNF*)
   tr_assigns : (Hstring.t * glob_update) list; (*updates of global variables*)
   tr_upds : update list; (*updates of arrays*)
   tr_nondets : Hstring.t list; (*non deterministic updates (only for global variables)*)
   tr_loc : Util.loc; (*location information*)
}
type of parameterized transitions
type transition_func = Types.Term.t -> Types.op_comp -> Types.Term.t -> Types.Atom.t 
functionnal form, computed during typing phase
type transition = {
   tr_info : transition_info;
   tr_tau : transition_func;
}
type of parameterized transitions with function
type system = {
   globals : (Util.loc * Hstring.t * Smt.Type.t) list;
   consts : (Util.loc * Hstring.t * Smt.Type.t) list;
   arrays : (Util.loc * Hstring.t * (Smt.Type.t list * Smt.Type.t)) list;
   type_defs : (Util.loc * type_constructors) list;
   init : Util.loc * Variable.t list * dnf;
   invs : (Util.loc * Variable.t list * Types.SAtom.t) list;
   unsafe : (Util.loc * Variable.t list * Types.SAtom.t) list;
   trans : transition_info list;
}
type of untyped transition systems constructed by parsing

Typed transition system


type kind = 
| Approx (*approximation*)
| Orig (*original unsafe formula*)
| Node (*reguar node*)
| Inv (*or user supplied invariant*)
the kind of nodes
type node_cube = {
   cube : Cube.t; (*the associated cube*)
   tag : int; (*a unique tag (negative for approximations and positive otherwise)*)
   kind : kind; (*the kind of the node*)
   depth : int; (*its depth in the search tree*)
   mutable deleted : bool; (*flag changed when the a-posteriori simplification detects subsumption (see Cubetrie.delete_subsumed)*)
   from : trace; (*history of the node*)
}
the type of nodes, i.e. cubes with extra information
type trace_step = transition_info * Variable.t list * node_cube 
type of elementary steps of error traces
type trace = trace_step list 
type of error traces, also the type of history of nodes
type t_system = {
   t_globals : Hstring.t list; (*Global variables*)
   t_arrays : Hstring.t list; (*Array names*)
   t_init : Variable.t list * dnf; (*Formula describing the initial states of the system, universally quantified DNF : \forall i. c1 \/ c2 \/ ...*)
   t_init_instances : (int, dnf list * Types.ArrayAtom.t list list) Hashtbl.t; (*pre-computed instances of the initial formula*)
   t_invs : node_cube list; (*user supplied invariants in negated form*)
   t_unsafe : node_cube list; (*unsafe formulas (in the form of cubes*)
   t_trans : transition list; (*transition relation in the form of a list of transitions*)
}
type of typed transition systems