package rfsm

  1. Overview
  2. Docs
package rfsm
Legend:
Library
Module
Module type
Parameter
Class
Class type
type typ = Guest.Types.typ
type expr = Guest.expr
type type_expr = Guest.type_expr
type lval = Guest.lval
type type_decl = Guest.type_decl
type program = {
  1. type_decls : type_decl list;
  2. fun_decls : fun_decl list;
  3. cst_decls : cst_decl list;
  4. models : model list;
  5. globals : global list;
  6. insts : inst list;
}
and model = (model_desc, typ) Annot.t
and model_desc = {
  1. name : Ident.t;
  2. states : state list;
  3. params : (Ident.t * type_expr) list;
  4. ios : (Ident.t * (io_cat * type_expr)) list;
  5. inps : (Ident.t * type_expr) list;
  6. outps : (Ident.t * type_expr) list;
  7. inouts : (Ident.t * type_expr) list;
  8. vars : (Ident.t * type_expr) list;
  9. trans : transition list;
  10. itrans : itransition;
}
and io_cat =
  1. | In
  2. | Out
  3. | InOut
and state = (state_desc, unit) Annot.t
and state_desc = Ident.t * (Ident.t * expr) list
and cond = (cond_desc, typ) Annot.t
and cond_desc = Ident.t * expr list
and action = (action_desc, typ) Annot.t
and action_desc =
  1. | Emit of Ident.t
  2. | Assign of lval * expr
and transition = (transition_desc, typ) Annot.t
and transition_desc = Ident.t * cond * action list * Ident.t * int
and itransition = (itransition_desc, typ) Annot.t
and itransition_desc = Ident.t * action list
and global = (global_desc, typ) Annot.t
and global_desc = Ident.t * global_cat * type_expr * stimulus option
and global_cat =
  1. | Input
  2. | Output
  3. | Shared
and stimulus = (stimulus_desc, typ) Annot.t
and stimulus_desc =
  1. | Periodic of int * int * int
  2. | Sporadic of int list
  3. | Value_change of (int * expr) list
and inst = (inst_desc, typ) Annot.t
and inst_desc = Ident.t * Ident.t * expr list * Ident.t list
and fun_decl = (fun_decl_desc, typ) Annot.t
and fun_decl_desc = {
  1. ff_name : Ident.t;
  2. ff_args : (Ident.t * type_expr) list;
  3. ff_res : type_expr;
  4. ff_body : expr;
}
and cst_decl = (cst_decl_desc, typ) Annot.t
and cst_decl_desc = {
  1. cc_name : Ident.t;
  2. cc_typ : type_expr;
  3. cc_val : expr;
}
val empty_program : program
val add_program : program -> program -> program
val subst_model_io : phi:Ident.t Subst.t -> model -> model
val subst_model_param : phi:expr Subst.t -> model -> model
val state_ios : model -> Ident.t -> Ident.t list * Ident.t list * Ident.t list * Ident.t list
val normalize_model : model -> model
val ppr_program : program -> program
val pp_typ : Stdlib.Format.formatter -> typ -> unit
val pp_expr : Stdlib.Format.formatter -> expr -> unit
val pp_type_expr : Stdlib.Format.formatter -> type_expr -> unit
val pp_cond_desc : Stdlib.Format.formatter -> cond_desc -> unit
val pp_cond : Stdlib.Format.formatter -> cond -> unit
val ppf_cond : Stdlib.Format.formatter -> cond -> unit
val pp_action : Stdlib.Format.formatter -> action -> unit
val pp_action_desc : Stdlib.Format.formatter -> action_desc -> unit
val pp_transition : Stdlib.Format.formatter -> transition -> unit
val ppf_transition : Stdlib.Format.formatter -> transition -> unit
val pp_transition_desc : Stdlib.Format.formatter -> transition_desc -> unit
val pp_itransition : Stdlib.Format.formatter -> itransition -> unit
val pp_itransition_desc : Stdlib.Format.formatter -> itransition_desc -> unit
val pp_stimulus : Stdlib.Format.formatter -> stimulus -> unit
val pp_stimulus_desc : Stdlib.Format.formatter -> stimulus_desc -> unit
val pp_state : Stdlib.Format.formatter -> state -> unit
val pp_type_decl : Stdlib.Format.formatter -> Guest.type_decl -> unit
val pp_model : Stdlib.Format.formatter -> model -> unit
val pp_model_desc : Stdlib.Format.formatter -> model_desc -> unit
val pp_model_name : Stdlib.Format.formatter -> model -> unit
val pp_global : Stdlib.Format.formatter -> global -> unit
val pp_cst_decl : Stdlib.Format.formatter -> cst_decl -> unit
val pp_fun_decl : Stdlib.Format.formatter -> fun_decl -> unit
val pp_program : Stdlib.Format.formatter -> program -> unit