Module Ph_translator

module Ph_translator: sig .. end

Translation of Process Hitting into different formats.

val dump_of_ph : Ph_types.ph -> Ph_types.ctx -> string

Returns a Process Hitting source as a flat action list from the given Process Hitting.

val prism_of_ph : Ph_types.ph -> Ph_types.ctx -> string

Returns the PRISM (ctmc) translation of the given Process Hitting.

type opts = {

	`alpha : float;`
	`round_fi : float * float -> int * int;`
	`coop_priority : bool;`

}

Stochastic parameters to strict timed interval conversion options: alpha is the confidence coefficient; round_fi (d,D) converts a float interval into an integer interva;

val romeo_pid : Ph_types.ph -> Ph_types.process -> string

Returns the Romeo string representation of given process.

val romeo_of_ph : opts -> Ph_types.ph -> Ph_types.ctx -> string

Returns the Romeo translation of the given Process Hitting.

val asp_of_ph : Ph_types.ph -> Ph_types.ctx -> string

Returns the ASP translation of the given Process Hitting - WiP

val an_of_ph : opts -> Ph_types.ph -> Ph_types.ctx -> string

Returns the AN-Pint translation of the given Process Hitting.