package promela

  1. Overview
  2. Docs
type t
exception Incompatible_process
val create : ?active:bool -> ?locals:Declarations.t -> Identifier.t -> Statement.t list -> t
val never : ?locals:Declarations.t -> Statement.t list -> t
val id_of : t -> Identifier.t
val body_of : t -> Statement.t list
val body_to : t -> Statement.t list -> t
val is_active : t -> bool
val is_never : t -> bool
val rename_variables : (Identifier.t -> Identifier.t) -> t -> t
val to_channel : Pervasives.out_channel -> t -> unit
val locals_of : t -> Declarations.t
val locals : Declarations.t -> t -> t
val identifiers_read : t -> Identifierset.t
val identifiers_written : t -> Identifierset.t
val filter : (Statement.t -> bool) -> t -> t
val map : (Statement.t -> Statement.t) -> t -> t
val map_rhs : (Expression.t -> Expression.t) -> t -> t