package rfsm
Parameter Make.Static
module Syntax = Syntaxmodule Typing : Typing.TYPING with module HostSyntax = Syntaxmodule Value : Guest.VALUE with type typ = Syntax.typtype fsm = {name : Ident.t;model : Syntax.model;(*Normalized, type-refined model
*)q : Ident.t;vars : Value.t Env.t;
}FSM instances
type ctx_comp = {ct_typ : Syntax.typ;ct_stim : Syntax.stimulus_desc option;(*For inputs only
*)ct_rds : Ident.t list;(*Readers, for inputs and shareds
*)ct_wrs : Ident.t list;(*Writers, for outputs and shareds
*)
}type t = {ctx : ctx;models : Syntax.model list;(*Original, un-type-refined and un-normalized models. Not used any longer
*)fsms : fsm list;globals : Value.t Env.t;(*Functions and constants
*)fns : Syntax.fun_decl list;(*Functions
*)csts : Syntax.cst_decl list;(*Constants
*)types : Syntax.Guest.type_decl list;(*User-defined types
*)dep_order : (Ident.t * int) list;
}val build : Typing.typed_program -> Syntax.program -> tval pp : verbose_level:int -> Format.formatter -> t -> unitval pp_fsm : verbose_level:int -> Format.formatter -> fsm -> unitval is_rtl : fsm -> bool