Previous  Up  Next

Module Ast

module Ast: sig .. end

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_lets : (Hstring.t * Types.Term.t) list;
   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;
   tr_reset : unit -> unit;
}

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 init_instance = {
   init_cdnf : dnf list; (*

DNFs for initial states

*)
   init_cdnf_a : Types.ArrayAtom.t list list; (*

DNFs for initial states in array form

*)
   init_invs : Types.ArrayAtom.t list; (*

Instantiated negated user supplied invariants

*)
}

Type of instantiated initial formulas

type t_system = {
   t_globals : Hstring.t list; (*

Global variables

*)
   t_consts : Hstring.t list; (*

Existential constants

*)
   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, init_instance) Hashtbl.t; (*

pre-computed instances of the initial formula with invariants

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