rfsm
  1. Overview
  2. Docs

Actions associated to transitions

type t =
  1. | Assign of lhs * Expr.t
  2. | Emit of string
    (*

    event

    *)
  3. | StateMove of string * string * string
    (*

    fsm name, old state, new state

    *)
and lhs = {
  1. mutable l_desc : lhs_desc;
}
and lhs_desc =
  1. | LhsVar of string
    (*

    v := ...

    *)
  2. | LhsArrInd of string * Expr.t
    (*

    vi := ... when v is an array

    *)
  3. | LhsArrRange of string * Expr.t * Expr.t
    (*

    vhi:lo := ... when v is an int

    *)
  4. | LhsRField of string * string
    (*

    v.field_name when v has a record type

    *)

Builders

val mk_lhs : string -> lhs

Accessors

val lhs_name : lhs -> string
val vars_of : t -> Expr.VarSet.t * Expr.VarSet.t

vars_of a returns the name of the variables read (resp. written) by action a

Operations

val rename : (string -> string) -> t -> t

rename f a renames f v each variable v occurring in a

val subst : Eval.env -> t -> t

subst env a replaces each variable v occuring in a by its value if found in env, simplifying the resulting expression whenever possible.

Printers

val string_of_lhs : lhs -> string
val to_string : t -> string