Module Fsm

module Fsm: sig .. end

Reactive Finite State Machines

type act_semantics =

`\|`	`Sequential`	`(*`	sequential (ex: `x:=x+1;y:=x` with `x=1` gives `x=2,y=2`)	`*)`
`\|`	`Synchronous`	`(*`	synchronous (ex: `x:=x+1:y=x` with `x=1` gives `x=2,y=1`)	`*)`

type fsm_config = {

	`mutable act_sep : string;`	`(*`	Default value: `" "`	`*)`
	`mutable act_sem : act_semantics;`	`(*`	Default value: `Sequential`	`*)`

}

val cfg : fsm_config

exception Undef_symbol of string * string * string

FSM, kind, name

exception Invalid_state of string * string

FSM, id

exception Typing_error of string * string * Types.typ * Types.typ

what, where, type, type

States

module State: sig .. end

Transition labels

module TransLabel: sig .. end

Internal representation

module Repr: Lts.T  with type state = State.t and type label = TransLabel.t

type state = State.t

type transition = State.t * TransLabel.t * State.t

type itransition = TransLabel.t * State.t

val string_of_transition : transition -> string

val string_of_state : state -> string

FSM model

type model = {

`fm_name : string;`	`(*`	name	`*)`
`fm_params : (string * Types.typ) list;`	`(*`	generic parameters	`*)`
`fm_ios : (string * (Types.dir * Types.typ)) list;`	`(*`	i/os	`*)`
`fm_vars : (string * Types.typ) list;`	`(*`	internal variables	`*)`
`fm_repr : Repr.t;`	`(*`	underlying LTS	`*)`

}

FSM instance

type inst = {

`f_name : string;`
`f_model : model;`
`f_params : (string * (Types.typ * Expr.value)) list;`	`(*`	name, type, actual value	`*)`
`f_inps : (string * (Types.typ * Global.global)) list;`	`(*`	local name, (type, global)	`*)`
`f_outps : (string * (Types.typ * Global.global)) list;`	`(*`	local name, (type, global)	`*)`
`f_inouts : (string * (Types.typ * Global.global)) list;`	`(*`	local name, (type, global)	`*)`
`f_vars : (string * Types.typ) list;`	`(*`	name, type	`*)`
`f_repr : Repr.t;`	`(*`	Static representation as a LTS (with _local_ names)	`*)`
`f_l2g : string -> string;`	`(*`	local -> global name	`*)`

}

Builders

val build_model : name:string ->
       states:state list ->
       params:(string * Types.typ) list ->
       ios:(Types.dir * string * Types.typ) list ->
       vars:(string * Types.typ) list ->
       trans:(state * (Condition.event * Condition.guard list) * Action.t list *
              state * int)
             list ->
       itrans:state * Action.t list -> model

val build_instance : name:string ->
       model:model ->
       params:(string * Expr.value) list -> ios:Global.global list -> inst

Accessors

val states_of : inst -> state list

val istate_of : inst -> state option

val transitions_of : inst -> transition list

val itransitions_of : inst -> itransition list

val succs : inst -> state -> (state * TransLabel.t) list

val input_events_of : inst -> string list

val output_events_of : inst -> string list

val is_rtl : inst -> bool

is_rtl f is true iff all is_rtl a for all actions a of f

Exceptions

exception Binding_mismatch of string * string * string

FSM, kind, id

exception Invalid_parameter of string * string

FSM, name

exception Uninstanciated_type_vars of string * string * string * string list

Externalizers

type dot_options =

`\|`	`OmitImplicitTransitions`
`\|`	`GlobalNames`
`\|`	`NoCaption`

val dot_output_oc : Pervasives.out_channel ->
       ?dot_options:Utils.Dot.graph_style list ->
       ?options:dot_options list -> inst -> unit

val dot_output : ?fname:string ->
       ?dot_options:Utils.Dot.graph_style list ->
       ?options:dot_options list -> dir:string -> inst -> string

dot_output dir f writes a DOT representation of FSM instance f in directory dir. Returns the name of the written file.

val dot_output_model : ?fname:string ->
       ?dot_options:Utils.Dot.graph_style list ->
       ?options:dot_options list -> dir:string -> model -> string

dot_output_model dir m writes a DOT representation of FSM model m in directory dir. Returns the name of the written file.

val dump_model : Pervasives.out_channel -> model -> unit

val dump_inst : Pervasives.out_channel -> inst -> unit