Module Murphi (.ml)

module Murphi: sig .. end

Oracle for BRAB that calls the explicit state model checker Murphi.

We recommend the distribution CMurphi which works with most recent compilers.

val print_system : int -> int -> Format.formatter -> Ast.t_system -> unit

print_system p a fmt sys prints the system sys in Murphi's syntax with p processes and infinite types abstracted with the subrange [1;a].

include Oracle.S