Parameter Make.G

type t
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
val make : int -> Predicate.t list -> t
val states : t -> (int * Big.t) Base.H_int.t
val label : t -> Predicate.S.t * int Predicate.H.t
val edges : t -> (int * R.label * Base.S_string.t) Base.H_int.t
val size_s : t -> int
val size_t : t -> int
val add_s : t -> int -> Big.t -> unit
val add_s_with_key : t -> int -> Big.big_key -> Big.t -> unit
val add_t : t -> source:int -> dest:int -> R.label -> Base.S_string.t -> unit
val add_pred : t -> pred_id:Predicate.t -> state:int -> unit
val preds_of : t -> int -> Predicate.t list
val find_all : t -> Big.t -> (int * Big.t) list

Iterators

val iter_states : (int -> Big.t -> unit) -> t -> unit
val fold_states : (int -> Big.t -> 'a -> 'a) -> t -> 'a -> 'a
val iter_edges : (int -> int -> R.label -> Base.S_string.t -> unit) -> t -> unit
val fold_edges : (int -> int -> R.label -> Base.S_string.t -> 'a -> 'a) -> t -> 'a -> 'a

Export functions

val to_txt : t -> string

Compute the textual representation of a transition system.

val to_dot : t -> path:string -> name:string -> string

Compute the string representation in dot format of a transition system. See grammar at https://graphviz.org/doc/info/lang.html.

PRISM format

Specifications at https://www.prismmodelchecker.org/manual/Appendices/ExplicitModelFiles.

val to_lab : t -> string

Compute the string representation in PRISM lab format of the labelling function of a transition system.

val to_prism : t -> string

Compute the string representation in PRISM tra format of a transition system.

val to_state_rewards : t -> string

Compute the string representation in PRISM rews format of state rewards.

val to_transition_rewards : t -> string

Compute the string representation in PRISM trew format of transition rewards.