Module LustreContract

module LustreContract: sig .. end
Wraps a state variable for use in a contract.

type svar = {
   pos : Lib.position;
   num : int;
   name : string option;
   svar : StateVar.t;
   scope : (Lib.position * string) list;
}
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
type t = {
   assumes : svar list; (*
Guarantees of the contract (boolean is the candidate flag).
*)
   guarantees : (svar * bool) list; (*
Modes of the contract.
*)
   modes : mode list;
}
Type of contracts.
val empty : unit -> t
Creates an empty contract.
val mk : svar list ->
(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 : Format.formatter -> svar -> unit
Pretty prints a svar wrapper.
val pp_print_mode : bool -> Format.formatter -> mode -> unit
Pretty prints a mode.
val pp_print_contract : bool -> Format.formatter -> t -> unit
Pretty prints a contract.
module ModeTrace: sig .. end
Mode traces as cex.