Previous  Up  Next

Module Action

module Action: sig .. end

Actions associated to transitions

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

event

*)
| StateMove of string * string * string (*

fsm name, old state, new state

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

v := ...

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

vi := ... when v is an array

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

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

*)
| 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