package promela

  1. Overview
  2. Docs
type t
exception Incompatible_model
val empty : t
val create : Process.t list -> Declarations.t -> t
val add : t -> Process.t -> t
val union : t -> t -> t
val processes_of : t -> Process.t list
val to_channel : Pervasives.out_channel -> t -> unit
val save : Pervasives.out_channel -> t -> unit
val load : Pervasives.in_channel -> t
val rename_variables : (Identifier.t -> Identifier.t) -> t -> t
val size : t -> int
val globals_of : t -> Declarations.t
val globals : Declarations.t -> t -> t
val add_globals : 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_stmt : (Statement.t -> Statement.t) -> t -> t
val map_rhs : (Expression.t -> Expression.t) -> t -> t