Module Luc4ocaml

module Luc4ocaml: sig .. end

Time-stamp: <modified the 08/08/2011 (at 17:05) by Erwan Jahier>

Lucky ocaml API

type var_name = string

type value =

`\|`	`F of float`
`\|`	`I of int`
`\|`	`B of bool`

type subst = var_name * value

type inputs = subst list

type outputs = subst list

type locals = subst list

type solution = outputs * locals

type state

Abtract state containing the Lucky runtime information. A step in Lucky machine updates this state.

exception MakeError

val make : ?seed:int ->
       ?fair:bool ->
       ?pp:string ->
       ?verbose:int ->
       ?precision:int -> ?main:string option -> string list -> state

Builds the initial state of the Lucky machine

To indicate whether the point used to perform the step is drawn inside, at edges, or at vertices of the convex hull of numeric solutions; the step mode is used iff at least one controllable variable is numeric.

type step_mode =

`\|`	`StepInside`
`\|`	`StepEdges`
`\|`	`StepVertices`

val step : ?mode:step_mode ->
       state -> inputs -> state * solution

the default step mode is StepInside

val step_se : ?mode:step_mode ->
       state Pervasives.ref -> inputs -> solution

side-effect version of step

val rif_read : Pervasives.in_channel -> state -> inputs

Reads from an in_channel Lucky inputs in RIF

nb: RIF = Reactive Input Format It is the input/output format of most Lustre/verimag tools.

val string_of_value : value -> string

Pretty-print

val rif_write_interface : Pervasives.out_channel -> state -> bool -> unit

writes the input and output var names and types. To be called before the first step is printed

val rif_write : Pervasives.out_channel ->
       state -> subst list -> subst list -> unit

write oc inputs outputs writes the inputs and outputs. To be called after each step.