Previous  Up  Next

Module Ph_types

module Ph_types: sig .. end
Process Hitting related types and associated operations.
type sort = string 
type sortidx = int 
type process = sort * sortidx 
module PSet: Set.S  with type elt = process
module PMap: Map.S  with type key = process
module PCSet: Set.S  with type elt = process * process
val procs_of_ps : process list -> PSet.t
Converts a list of processus to a set of processes.
val string_of_proc : process -> string
String representation of a process.
val pintstring_of_proc : process -> string
PINT string representation of a process.
val string_of_procs : PSet.t -> string
String representation of a process Set.
type rate = (float * int) option
RateSA (rate, stochasticity_absorption) or FiringInterval (d1, d2, confidence_coefficient)
val rsa_of_stochatime : PintTypes.stochatime -> rate
Returns the rate and stochasticity absorption factor for the given parameter or None if the rate is infinite.
type hits = (process,
        (process * PintTypes.stochatime) * sortidx)
       Hashtbl.t 
type ph = process list * hits 
type action =
| Hit of (process * process * int) 
module ASet: Set.S  with type elt = action
val string_of_action : action -> string
String representation of an action.
val pintstring_of_action : action -> string
PINT string representation of an action.
val string_of_actions : action list -> string
String representation of a list of actions.
val hitter : action -> process
Returns the hitter process involved in the given action.
val target : action -> process
Returns the target process involved in the given action.
val bounce : action -> int
Returns the bounce process index involved in the given action.
val bounce2 : action -> process
Returns the bounce process involved in the given action.
type state = sortidx PintTypes.SMap.t 
val string_of_state : ?show_zero:bool -> state -> string
String representation of a state. By default, state
val state0 : process list -> state
Returns the state where all sorts have the process of index 0 present.
val merge_states : state -> state -> state
merge_states dest orig sets the processes in the state orig in the state dest.
val merge_state_with_ps : state -> process list -> state
Sets the processes in the given process list present in the given state.
val state_value : state -> sort -> sortidx
state_value s a returns the process index of sort a present in s.
val list_of_state : state -> process list
Converts a set into a list of processes.
val procs_of_state : state -> PSet.t
Converts a state to a set of processes.
val state_empty : state
Empty state
type ctx = PintTypes.ISet.t PintTypes.SMap.t
Context type
val ctx_equal : ctx -> ctx -> bool
Check ctx equality
val ctx_empty : ctx
Empty context
val ctx_sorts : ctx -> PintTypes.SSet.t
Returns the set of sorts in the context
val ctx_get : sort -> ctx -> PintTypes.ISet.t
Get indexes of the given sort in the given context.
val ctx_safe_get : sort -> ctx -> PintTypes.ISet.t
Same as previous but return empty set if sort is not present in the context keys.
val ctx_has_proc : process -> ctx -> bool
ctx_has_proc p ctx retruns true iff p is present in ctx.
val ctx_add_proc : process -> ctx -> ctx
ctx_add_proc p ctx returns the context where p has been added.
val ctx_rm_proc : process -> ctx -> ctx
ctx_rm_proc p ctx returns the context where p has been removed.
val string_of_ctx : ctx -> string
String representation of a context.
val procs_of_ctx : ctx -> PSet.t
Converts a context to a set of processes.
val procs_to_ctx : PSet.t -> ctx
Converts a set of processes to a context.
val state_of_ctx : ctx -> state
Converts a context to a state. Raise Invalid_arg if there exists more than one process per sort.
val ctx_override_by_ctx : ctx -> ctx -> ctx
Context overriding.
val ctx_override : ctx -> PSet.t -> ctx
Context overriding.
val ctx_union : ctx -> ctx -> ctx
Union between contexts.
val ctx_union_state : ctx -> state -> ctx
Union between a context and a state.
val ctx_inter : ctx -> ctx -> ctx
Intersection between contexts.
val ctx_diff : ctx -> ctx -> ctx
Difference between contexts.
val ctx_of_state : state -> ctx
State to context.
val ph_sigma : ph -> sort list
Returns the list of sorts defined in the given Process Hitting.
type t_directive = {
   mutable default_rate : float option;
   mutable default_sa : int;
   mutable sample : float;
}
Directives of a Process Hitting model

Default directives

val directive : t_directive
type objective = sort * sortidx * sortidx 
module ObjSet: Set.S  with type elt = objective
module ObjMap: Map.S  with type key = objective
val string_of_obj : objective -> string
String representation of the given objective.
val obj_sort : objective -> sort
Sort of the objective.
val obj_target : objective -> sortidx
Process index of the objective target.
val obj_bounce : objective -> sortidx
Process index of the objective bounce.
val obj_bounce_proc : objective -> process
Bounce process of the objective.
val obj_reach : state -> process -> objective
obj_reach s p returns the objective of the reachability of process p from the state s.
type anostate = int list 
type state_matching_t =
| SM of (string list * anostate list)
| SM_Not of state_matching_t
| SM_And of (state_matching_t * state_matching_t)
| SM_Or of (state_matching_t * state_matching_t)