package lutin

  1. Overview
  2. Docs
type atomic_ctrl_state = string
type ctrl_state = atomic_ctrl_state list
type dyn_weight =
  1. | V of int
  2. | Infin

Weigths, once evaluated (no more memories nor inputs)

type wt = children Util.StringMap.t * string

A wt (weigthed tree) is a n-ary tree encoding the set of possible formula for the next step.

and children =
  1. | Children of (dyn_weight * string) list
  2. | Leave of Exp.formula * atomic_ctrl_state
  3. | Stop of string
type t = {
  1. initial_ctrl_state : ctrl_state list;
  2. in_vars : Exp.var list;
  3. out_vars : Exp.var list;
  4. loc_vars : Exp.var list;
  5. ext_func_tbl : Exp.ext_func_tbl;
  6. memories_names : (string * Exp.var) list;
  7. bool_vars_to_gen : Exp.var list list;
  8. num_vars_to_gen : Exp.var list list;
  9. output_var_names : Var.name list list;
  10. reactive : bool;
  11. get_wtl : Var.env_in -> state -> ctrl_state -> wt list;
  12. is_final : ctrl_state list -> bool;
  13. gen_dot : ctrl_state list -> ctrl_state list -> string -> int;
}

The Digested Lucky program (form the static part of the state). Holds a list of independant programs (i.e., they don't share any I/O).

and dynamic_state_fields = {
  1. memory : Var.env;
  2. ctrl_state : ctrl_state list;
  3. last_input : Var.env;
  4. last_output : Var.env;
  5. last_local : Var.env;
  6. snt : Solver.t;
  7. verbose : int;
}

The dynamic part of the state (that changes at each cycle).

and state = {
  1. d : dynamic_state_fields;
  2. s : t;
}
val memory_of_state : state -> Var.env
val last_values_of_state : state -> Var.env * Var.env * Var.env
val compute_weight : Exp.weight -> Var.env_in -> state -> dyn_weight
val print_wt : wt -> unit

Pretty-printing

val ctrl_state_to_string : ctrl_state -> string
val ctrl_state_list_to_string_list : ctrl_state -> string list
val ctrl_state_to_string_long : ctrl_state list -> string

Used for printing information about the current control point in error messages.

OCaml

Innovation. Community. Security.