Module Sbrs

module Sbrs: sig .. end
This module provides operations on stochastic BRS.
Author(s): Michele Sevegnani

type react 
The type of stochastic bigraphical reaction rules.
type p_class = 
| P_class of react list (*
Priority class
*)
| P_rclass of react list (*
Reducible priority class
*)
The type of priority classes, i.e., lists of stochastic reaction rules. Intermediate states resulting from the application of reaction rules in reducible priority classes are ignored.
type graph 
The type of Continuous Time Markov Chains (CTMC).
type occ = Big.bg * float 
Type of occurrences i.e., a bigraph and a
type limit = float 
Type of simulation limit i.e., execution time.
val typ : Rs.t
Type of transition system: SBRS.
val string_of_react : react -> string
Same as Brs.string_of_stats for stochastic reaction rules.
val parse_react_unsafe : lhs:Big.bg -> rhs:Big.bg -> float -> Fun.t option -> react
Same as Brs.parse_react_unsafe for stochastic reaction rules.
val parse_react : lhs:Big.bg -> rhs:Big.bg -> float -> Fun.t option -> react option
Same as Brs.parse_react for stochastic reaction rules.
val lhs_of_react : react -> Big.bg
The left-hand side (redex) of a stochastic reaction rule. *
val rhs_of_react : react -> Big.bg
The right-hand side (reactum) of a stochastic reaction rule.
val string_of_limit : limit -> string
String representation of a simulation limit.
val is_valid_react : react -> bool
Same as Brs.is_valid_react but also checks that the rate is greater than zero. Return false otherwise. See Big.is_solid.
type react_error 
The type of reaction validity errors.
exception NOT_VALID of react_error
Raised when a reaction rule is not valid.
val is_valid_react_exn : react -> bool
Same as Sbrs.is_valid_react but an exception is raised when the rule is not valid.
Raises NOT_VALID when the rule is not valid.
val string_of_react_err : react_error -> string
String representation of reaction validity errors.
val is_inst : react -> bool
Return true if a reaction rule is instantaneous, false otherwise.
val is_valid_priority : p_class -> bool
Return true if all the reaction rules in a priority class are valid, all the reaction rules in a reducible classes are instantaneous and no instantaneous reaction rules are present in a non reducible class. Return false otherwise.
val is_valid_priority_list : p_class list -> bool
Return true if a list of priority classes contains at least a non reducible priority class, false otherwise.
val cardinal : p_class list -> int
Return the total number of stochastic reaction rules in a list of priority classes.
val apply : Big.bg -> react list -> Big.bg option
Same as Brs.apply. Note that stochastic rates are ignored.
val step : Big.bg -> react list -> occ list * int
Compute the set of reachable states in one step. Note that isomorphic states are merged and each state is associated to a transition rate. The total number of occurrences is also returned.
val random_step : Big.bg -> react list -> occ option * int
Select step of Gillespie SSA. The total number of occurrences is also returned.
val fix : Big.bg -> react list -> Big.bg * int
Same as Brs.fix for probabilistic reaction rules. Note that stochastic rates are ignored.
val rewrite : Big.bg -> p_class list -> Big.bg * int
Scan priority classes and reduce a state. Stop when no more rules can be applied or when a non reducible priority class is enabled. Also return the number of rewriting steps performed in the loop.

Continuous Time Markov Chains


exception MAX of graph * Stats.t
Raised when the size of the transition system reaches the maximum number of states.
val bfs : s0:Big.bg ->
priorities:p_class list ->
predicates:(string * Big.bg) list ->
max:int -> iter_f:(int -> Big.bg -> unit) -> graph * Stats.t
bfs ~s0 ~priorities ~predicates ~max ~iter_f computes the transition system of the SBRS specified by initial state s0 and priority classes priorities. Arguments ~max and ~iter_f are the maximum number of states of the transition system and a function to be applied whenever a new state is discovered, respectively. Priority classes are assumed to be sorted by priority, i.e. the first element in the list is the class with the highest priority. List of predicates ~predicates is also checked for every state.
Raises Sbrs.MAX when the maximum number of states is reached.

Stochastic simulation traces


exception DEADLOCK of graph * Stats.t * float
Raised when the simulation reaches a deadlock state.
exception LIMIT of graph * Stats.t
Raised when the simulation reaches the maximum simulation time.
val sim : s0:Big.bg ->
priorities:p_class list ->
predicates:(string * Big.bg) list ->
init_size:int ->
stop:limit -> iter_f:(int -> Big.bg -> unit) -> graph * Stats.t
Simulate (using Gillespie SSA) the SBRS specified by initial state s0 and priority classes priorities. Arguments init_size and stop are the initial size of the state set and the maximum simulation time, respectively. Function iter_f is applied to every new state discovered during the simulation.
Raises

Export functions


val to_prism : graph -> string
Compute the string representation in PRISM tra format of a CTMC.
val to_dot : graph -> name:string -> string
Compute the string representation in dot format of a CTMC.
val to_lab : graph -> string
Compute the string representation in PRISM lab format of the labelling function of a CTMC.
val iter_states : f:(int -> Big.bg -> unit) -> graph -> unit
Apply f to every state.
val write_dot : graph -> name:string -> path:string -> int
Export to file the string representation in dot format of a CTMC.
Raises Rs.EXPORT_ERROR when an error occurs.
val write_lab : graph -> name:string -> path:string -> int
Export to file the string representation in PRISM lab format of the labelling function of a CTMC.
Raises Rs.EXPORT_ERROR when an error occurs.
val write_prism : graph -> name:string -> path:string -> int
Export to file the string representation in PRISM tra format of a CTMC.
Raises Rs.EXPORT_ERROR when an error occurs.
val write_svg : graph -> name:string -> path:string -> int
Export to file the string representation in svg format of a CTMC.
Raises Rs.EXPORT_ERROR when an error occurs.
val write_json : graph -> name:string -> path:string -> int
Export to file the string representation in json format of a CTMC.
Raises Rs.EXPORT_ERROR when an error occurs.