Module LustreContract

type svar = {
pos : Lib.position;
num : int;
name : string option;
svar : StateVar.t;
scope : (Lib.position * string) list;
}

Wraps a state variable for use in a contract.

val mk_svar : Lib.position -> int -> string option -> StateVar.t -> (Lib.position * string) list -> svar

Creates a svar.

val prop_name_of_svar : svar -> string -> string -> string

Generates a property name.

prop_name_of_svar svar kind name generates a property name with the trace of contract call / position pairs. kind and name are concatenated and placed between the trace and the svar position and number.

type mode = {
name : LustreIdent.t;

Position of the mode.

pos : Lib.position;

Path of contract imports to this node.

path : string list;

Requires of the mode.

requires : svar list;

Ensures of the mode.

ensures : svar list;

Is this mode a candidate?.

candidate : bool;
}

Type of modes.

Creates a mode.

val mk_mode : LustreIdent.t -> Lib.position -> string list -> svar list -> svar list -> bool -> mode

Creates a mode.

type t = {
assumes : svar list;

State variable to model Sofar(/\ assumes)

sofar_assump : StateVar.t;

Guarantees of the contract (boolean is the candidate flag).

guarantees : (svar * bool) list;

Modes of the contract.

modes : mode list;
}

Type of contracts.

val mk : svar list -> StateVar.t -> (svar * bool) list -> mode list -> t

Creates a new contract from a set of assumes, a set of guarantess, and a list of modes.

val add_ass : t -> svar list -> t

Adds assumes to a contract.

val add_gua : t -> (svar * bool) list -> t

Adds guarantees to a contract.

val add_modes : t -> mode list -> t

Adds modes to a contract.

val svars_of : t -> StateVar.StateVarSet.t
val pp_print_svar : Stdlib.Format.formatter -> svar -> unit

Pretty prints a svar wrapper.

val pp_print_mode : bool -> Stdlib.Format.formatter -> mode -> unit

Pretty prints a mode.

val pp_print_contract : bool -> Stdlib.Format.formatter -> t -> unit

Pretty prints a contract.

module ModeTrace : sig ... end

Mode traces as cex.