lutin

Lutin: modeling stochastic reactive systems
IN THIS PACKAGE
Module AutoGen
type weightexp =
| W_huge
| W_exp of CoAlgExp.t

le type du rsultat

type gtree = string * gtree_node
and gtree_node =
| GT_leaf of Guard.t * string
| GT_choice of (weightexp option * gtree) list
| GT_stop of string
val gtree_size : gtree -> int
type trans = {
src : string;
wgt : weightexp option;
form : Guard.t;
dest : string;
}
type state_info =
| SS_stable of Expand.tbl CoTraceExp.t
| SS_transient
| SS_final of string
type t
type config
val make_config : string -> config
val source : t -> Expand.t
val init_control : t -> string
val transitions : t -> trans list
val config2gtree : t -> config -> gtree * t
val config2trans : t -> config -> trans list * t
val init : Expand.t -> t
val make : Expand.t -> t
val get_state_def : t -> string -> Expand.tbl CoTraceExp.t
val get_state_info : t -> string -> state_info
val states : t -> state_info Util.StringMap.t
val dump : t -> unit