Index of values

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

Returns the ASP translation of the given Process Hitting - WiP

Returns the bounce process index involved in the given action.

Returns the bounce process involved in the given action.

List of command line options (for use with Arg module) common to the majority of tools.

(WiP) coop_priority_reachability ph s w returns the semi-decision (ternary) of the concretizability of objective sequence w in the state s in the process hitting ph.

Returns the number of actions in the given Process Hitting.

Returns the number of processes in the given Process Hitting.

Returns the number of sorts in the given Process Hitting.

Returns the total number of states of the given Process Hitting.

Create a new execution environment from the given Process Hitting.

cross [l1;..;ln] [e1;..;ek] returns e1::l1;..;ek::l1;..;e1::ln;..;ek::ln.

cross [l1;..;ln] returns the cartesian product l1 x .. x ln.

ctx_add_proc p ctx returns the context where p has been added.

Difference between contexts.

Empty context

Check ctx equality

Get indexes of the given sort in the given context.

ctx_has_proc p ctx retruns true iff p is present in ctx.

Intersection between contexts.

State to context.

Context overriding.

Context overriding.

ctx_rm_proc p ctx returns the context where p has been removed.

Same as previous but return empty set if sort is not present in the context keys.

Returns the set of sorts in the context

Union between contexts.

Union between a context and a state.

dbg msg prints msg^"\n" to standard error channel.

dbg_noendl prints msg to standard error channel.

dbglevel () returns the maximum debug level (0 for none)

Maximum debug level to display

Set to true if debug messages should be displayed.

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

dump_to_file filename str dumps str to filename.

execute env init duration plotter simulates the environment env from the initial state init and calls plotter t p each time the process p appears at time t.

firing_interval alpha r sa returns the (float) confidence interval at confidence coefficient alpha for the sum of sa exponential variables of rate r*sa.

Returns the hitter process involved in the given action.

index_of a l returns the first index of a occurrence in l.

Initialize random generators used by the machine

List of command line options (for use with Arg module) for tools taking a model as input.

Truncates given couple of floats into a couple of integers.

ISet from int list.

Json representation of bindings

Json representation of int

Json represenetation of list

Json representation of string

Json representation of ternary

list_lassoc b l acts like List.assoc with flipped key/value.

Converts a set into a list of processes.

list_remove a l removes all a occurences in l.

local_fixed_points !Ph_instance.cooperativities ph ai returns the list of semi-global states which are sufficient to ensure ai (local) stability

local_reachability env returns the semi-decision (ternary) of the concretizability of sequence of local reachability as configured in env.

Sets the processes in the given process list present in the given state.

merge_states dest orig sets the processes in the state orig in the state dest.

Process index of the objective bounce.

Bounce process of the objective.

obj_reach s p returns the objective of the reachability of process p from the state s.

Sort of the objective.

Process index of the objective target.

Reference to the input channel.

opt_default default opt returns x if opt is Some x, otherwise returns default.

Reference to the input filename.

Reference to the process list that should be present in the initial state.

Parse a Process Hitting and its initial state from given input channel.

Returns a copy of the given Process Hitting.

Returns the list of sorts defined in the given Process Hitting.

PINT string representation of an action.

PINT string representation of a process.

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

Make a list of processes from a string list alterning sort and process index.

Converts a context to a set of processes.

Converts a list of processus to a set of processes.

Converts a state to a set of processes.

Converts a set of processes to a context.

Quantile of Erlang.

random_firing_time r sa returns a random value following an Erlang (r*sa, sa).

range a b returns the list of successive elements from a to b [a;a+1;..;b].

Erlang number generation.

Returns the Romeo translation of the given Process Hitting.

Returns the Romeo string representation of given process.

Rounds given firing interval to the closest integers.

Rounds given firing interval to the bounding integer interval.

Rounds given firing interval to the bounded integer interval.

Rounds the given float to the nearest ceil or floor.

Same as range but in the reverse order.

Estimes the rate and stochasticity absorption factor corresponding to the given firing interval at the given confidence coefficient

Returns the rate and stochasticity absorption factor for the given parameter or None if the rate is infinite.

Set seed for R random number generation.

Sets opt_channel_in and opt_filename_in according to given input filename.

Sets Ph_util.opt_initial_procs to the process list represented by the given string.

Use of input_cmdopts to parse command line.

smap_remove_keys smap keys returns smap without the bindings from keys.

smap_subset equal m1 m2 returns true if and only if all bindings in m1 are in m2.

Returns the state where all sorts have the process of index 0 present.

Empty state

Converts a context to a state.

state_value s a returns the process index of sort a present in s.

string_apply match data values replaces successively the n-th match of match in data with the n-th elements of values.

String representation of an action.

String representation of a list of actions.

String representation of a context.

String representation of the given float, ensuring there is always a number after the dot (e..g, 1.

String representation of an int Set.

string_of_list str_of_el l returns string representation of the given list l using the element to string function str_of_el.

String representation of the given objective.

String representation of a process.

String representation of a process Set.

String representation of a string Set.

String representation of a state.

String representation of ternary.

Returns the target process involved in the given action.

zoom_fi factor fi multiplies the bounds of fi by factor.