package lutin
-
lutin
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package lutin
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
type ctrl_state = atomic_ctrl_state listtype wt = children Util.StringMap.t * stringA wt (weigthed tree) is a n-ary tree encoding the set of possible formula for the next step.
and children = | Children of (dyn_weight * string) list| Leave of Exp.formula * atomic_ctrl_state| Stop of string
type t = {initial_ctrl_state : ctrl_state list;in_vars : Exp.var list;out_vars : Exp.var list;loc_vars : Exp.var list;ext_func_tbl : Exp.ext_func_tbl;memories_names : (string * Exp.var) list;bool_vars_to_gen : Exp.var list list;num_vars_to_gen : Exp.var list list;output_var_names : Var.name list list;reactive : bool;get_wtl : Var.env_in -> state -> ctrl_state -> wt list;is_final : ctrl_state list -> bool;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 = {memory : Var.env;ctrl_state : ctrl_state list;last_input : Var.env;last_output : Var.env;last_local : Var.env;snt : Solver.t;verbose : int;
}The dynamic part of the state (that changes at each cycle).
val compute_weight : Exp.weight -> Var.env_in -> state -> dyn_weightval print_wt : wt -> unitPretty-printing
val ctrl_state_to_string : ctrl_state -> stringval ctrl_state_list_to_string_list : ctrl_state -> string listval ctrl_state_to_string_long : ctrl_state list -> stringUsed for printing information about the current control point in error messages.