Index of values

an_of_ph [Ph_translator]
Returns the AN-Pint translation of the given Process Hitting.
asp_of_ph [Ph_translator]
Returns the ASP translation of the given Process Hitting - WiP
automata_set [An_parser]

bot_trimmed_cwA [Ph_reach]
bounce [Ph_types]
Returns the bounce process index involved in the given action.
bounce2 [Ph_types]
Returns the bounce process involved in the given action.
build_cooperation [Ph_cooperativity]
build_reflection [Ph_cooperativity]

coherent_ctx [Ph_cooperativity]
color_nodes_connected_to_trivial_sols [Ph_reach]
common_cmdopts [Ui]
List of command line options (for use with Arg module) common to the majority of tools.
coop_priority_reachability [Ph_reach]
(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.
coop_priority_ua_glc_setup [Ph_reach]
cooperativities [Ph_instance]
copy [Ph_instance]
count_actions [Ph_util]
Returns the number of actions in the given Process Hitting.
count_processes [Ph_util]
Returns the number of processes in the given Process Hitting.
count_sorts [Ph_util]
Returns the number of sorts in the given Process Hitting.
count_states [Ph_util]
Returns the total number of states of the given Process Hitting.
create_env [Ph_machine]
Create a new execution environment from the given Process Hitting.
cross [Util]
cross [l1;..;ln] [e1;..;ek] returns e1::l1;..;ek::l1;..;e1::ln;..;ek::ln.
cross_forward [Util]
cross_list [Util]
cross [l1;..;ln] returns the cartesian product l1 x .. x ln.
ctx_add_proc [Ph_types]
ctx_add_proc p ctx returns the context where p has been added.
ctx_diff [Ph_types]
Difference between contexts.
ctx_empty [Ph_types]
Empty context
ctx_equal [Ph_types]
Check ctx equality
ctx_get [Ph_types]
Get indexes of the given sort in the given context.
ctx_has_proc [Ph_types]
ctx_has_proc p ctx retruns true iff p is present in ctx.
ctx_inter [Ph_types]
Intersection between contexts.
ctx_of_state [Ph_types]
State to context.
ctx_override [Ph_types]
Context overriding.
ctx_override_by_ctx [Ph_types]
Context overriding.
ctx_rm_proc [Ph_types]
ctx_rm_proc p ctx returns the context where p has been removed.
ctx_safe_get [Ph_types]
Same as previous but return empty set if sort is not present in the context keys.
ctx_sorts [Ph_types]
Returns the set of sorts in the context
ctx_union [Ph_types]
Union between contexts.
ctx_union_state [Ph_types]
Union between a context and a state.

dbg [Debug]
dbg msg prints msg^"\n" to standard error channel.
dbg_noendl [Debug]
dbg_noendl prints msg to standard error channel.
dbglevel [Debug]
dbglevel () returns the maximum debug level (0 for none)
debuglevel [Debug]
Maximum debug level to display
directive [Ph_types]
dodebug [Debug]
Set to true if debug messages should be displayed.
dump_of_ph [Ph_translator]
Returns a Process Hitting source as a flat action list from the given Process Hitting.
dump_to_file [Util]
dump_to_file filename str dumps str to filename.

execute [Ph_machine]
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 [Param]
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.

get_Sols [Ph_reach]
goals [An_parser]

hashtbl_filter_bindings [Util]
hitter [Ph_types]
Returns the hitter process involved in the given action.

id [PintTypes]
index_of [Util]
index_of a l returns the first index of a occurrence in l.
init_env [Ph_reach]
init_random [Ph_machine]
Initialize random generators used by the machine
input_cmdopts [Ui]
List of command line options (for use with Arg module) for tools taking a model as input.
int_of_fi [Param]
Truncates given couple of floats into a couple of integers.
interaction_graph [Ph_parser]
interaction_graph [Ph_instance]
iset_of_list [PintTypes]
ISet from int list.

json_of_bindings [PintTypes]
Json representation of bindings
json_of_int [PintTypes]
Json representation of int
json_of_list [PintTypes]
Json represenetation of list
json_of_str [PintTypes]
Json representation of string
json_of_ternary [PintTypes]
Json representation of ternary

list_lassoc [Util]
list_lassoc b l acts like List.assoc with flipped key/value.
list_of_state [Ph_types]
Converts a set into a list of processes.
list_remove [Util]
list_remove a l removes all a occurences in l.
local_fixed_points [Ph_cooperativity]
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 [Ph_reach]
local_reachability env returns the semi-decision (ternary) of the concretizability of sequence of local reachability as configured in env.
local_state [An_parser]
local_state_list [An_parser]

main [Ph_parser]
main [An_parser]
merge_state_with_ps [Ph_types]
Sets the processes in the given process list present in the given state.
merge_states [Ph_types]
merge_states dest orig sets the processes in the state orig in the state dest.

obj_bounce [Ph_types]
Process index of the objective bounce.
obj_bounce_proc [Ph_types]
Bounce process of the objective.
obj_reach [Ph_types]
obj_reach s p returns the objective of the reachability of process p from the state s.
obj_sort [Ph_types]
Sort of the objective.
obj_target [Ph_types]
Process index of the objective target.
opt_channel_in [Ui]
Reference to the input channel.
opt_default [Util]
opt_default default opt returns x if opt is Some x, otherwise returns default.
opt_filename_in [Ui]
Reference to the input filename.
opt_initial_procs [Ph_util]
Reference to the process list that should be present in the initial state.

parse [Ph_util]
Parse a Process Hitting and its initial state from given input channel.
ph_copy [Ph_util]
Returns a copy of the given Process Hitting.
ph_sigma [Ph_types]
Returns the list of sorts defined in the given Process Hitting.
pintstring_of_action [Ph_types]
PINT string representation of an action.
pintstring_of_proc [Ph_types]
PINT string representation of a process.
prism_of_ph [Ph_translator]
Returns the PRISM (ctmc) translation of the given Process Hitting.
process [Ph_parser]
processlist [Ph_parser]
proclist_from_stringlist [Ui]
Make a list of processes from a string list alterning sort and process index.
procs_of_ctx [Ph_types]
Converts a context to a set of processes.
procs_of_ps [Ph_types]
Converts a list of processus to a set of processes.
procs_of_state [Ph_types]
Converts a state to a set of processes.
procs_to_ctx [Ph_types]
Converts a set of processes to a context.

qerlang [R]
Quantile of Erlang.

random_firing_time [Param]
random_firing_time r sa returns a random value following an Erlang (r*sa, sa).
range [Util]
range a b returns the list of successive elements from a to b [a;a+1;..;b].
regulators [Ph_cooperativity]
rerlang [R]
Erlang number generation.
reset [Ph_instance]
resolve [Ph_cooperativity]
restore [Ph_instance]
romeo_of_ph [Ph_translator]
Returns the Romeo translation of the given Process Hitting.
romeo_pid [Ph_translator]
Returns the Romeo string representation of given process.
round_fi_closest [Param]
Rounds given firing interval to the closest integers.
round_fi_ex [Param]
Rounds given firing interval to the bounding integer interval.
round_fi_in [Param]
Rounds given firing interval to the bounded integer interval.
round_float [Param]
Rounds the given float to the nearest ceil or floor.
rrange [Util]
Same as range but in the reverse order.
rsa_of_firinginterval [Param]
Estimes the rate and stochasticity absorption factor corresponding to the given firing interval at the given confidence coefficient
rsa_of_stochatime [Ph_types]
Returns the rate and stochasticity absorption factor for the given parameter or None if the rate is infinite.

set_of_list [PintTypes]
set_seed [R]
Set seed for R random number generation.
setup_opt_channel_in [Ui]
Sets opt_channel_in and opt_filename_in according to given input filename.
setup_opt_initial_procs [Ui]
Sets Ph_util.opt_initial_procs to the process list represented by the given string.
simple_input [Ui]
Use of input_cmdopts to parse command line.
smap_remove_keys [Util]
smap_remove_keys smap keys returns smap without the bindings from keys.
smap_subset [Util]
smap_subset equal m1 m2 returns true if and only if all bindings in m1 are in m2.
solution [ASP_parser]
srange [Util]
state0 [Ph_types]
Returns the state where all sorts have the process of index 0 present.
state_empty [Ph_types]
Empty state
state_of_ctx [Ph_types]
Converts a context to a state.
state_value [Ph_types]
state_value s a returns the process index of sort a present in s.
stream_permutations [Util]
string_apply [Util]
string_apply match data values replaces successively the n-th match of match in data with the n-th elements of values.
string_of_action [Ph_types]
String representation of an action.
string_of_actions [Ph_types]
String representation of a list of actions.
string_of_ctx [Ph_types]
String representation of a context.
string_of_float0 [Util]
String representation of the given float, ensuring there is always a number after the dot (e..g, 1.
string_of_iset [PintTypes]
String representation of an int Set.
string_of_list [Util]
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_of_map [PintTypes]
string_of_obj [Ph_types]
String representation of the given objective.
string_of_proc [Ph_types]
String representation of a process.
string_of_procs [Ph_types]
String representation of a process Set.
string_of_set [PintTypes]
string_of_sset [PintTypes]
String representation of a string Set.
string_of_state [Ph_types]
String representation of a state.
string_of_ternary [PintTypes]
String representation of ternary.

target [Ph_types]
Returns the target process involved in the given action.
tic [Debug]
toc [Debug]
top_trimmed_cwA [Ph_reach]

unordered_over_approx [Ph_reach]

zoom_fi [Param]
zoom_fi factor fi multiplies the bounds of fi by factor.