Module Brs

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

type react 
The type of 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 reaction rules. Intermediate states resulting from the application of reaction rules in reducible priority classes are ignored.
type graph 
The type of transition systems.
type occ = Big.bg 
Type of occurrences i.e., a bigraph.
type limit = int 
Type of simulation limit i.e., number of execution steps.
val typ : Rs.t
Type of transition system: BRS.
val string_of_react : react -> string
String representation of reaction rules. The representation of the redex and the reactum are computed by Big.to_string.
val parse_react_unsafe : lhs:Big.bg -> rhs:Big.bg -> Fun.t option -> react
Create a new reaction rule. If eta = None, the identity function is used as instantiation map. No validity check is performed.
val parse_react : lhs:Big.bg -> rhs:Big.bg -> Fun.t option -> react option
Same Brs.parse_ract_unsafe but returns None if it is impossible to parse a valid reaction.
val lhs_of_react : react -> Big.bg
The left-hand side (redex) of a reaction rule. *
val rhs_of_react : react -> Big.bg
The right-hand side (reactum) of a reaction rule.
val string_of_limit : limit -> string
String representation of a simulation limit.
val is_valid_react : react -> bool
Return true if the inner (outer) interfaces of the redex (reactum) are equal, the redex is solid and the instantiation map is total. 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 Brs.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_valid_priority : p_class -> bool
Return true if all the reaction rules in the priority class are valid, 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 reaction rules in a list of priority classes.
val apply : Big.bg -> react list -> Big.bg option
Sequential application of a list of reaction rules. Non-enabled rules are ignored. None is returned if no rewriting is performed i.e., when all the reaction rules are non-enabled.
val step : Big.bg -> react list -> occ list * int
Compute the set of reachable states in one step. Note that isomorphic states are merged. The total number of occurrences is also returned.
val random_step : Big.bg -> react list -> occ option * int
Compute a random state reachable in one step. State selection is performed according to a uniform distribution over all the possible states reachable in one step. The total number of occurrences is also returned.
val fix : Big.bg -> react list -> Big.bg * int
Reduce a reducible class to the fixed point. The number of rewriting steps is also returned.
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.

Transition systems


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 ~max ~iter_f computes the transition system of the BRS 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 Brs.MAX when the maximum number of states is reached.

Simulation traces


exception DEADLOCK of graph * Stats.t * int
Raised when the simulation reaches a deadlock state.
exception LIMIT of graph * Stats.t
Raised when the simulation reaches the maximum number of simulation steps.
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 the BRS 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 steps, 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 transition system.
val to_dot : graph -> name:string -> string
Compute the string representation in dot format of a transition system.
val to_lab : graph -> string
Compute the string representation in PRISM lab format of the labelling function of a transition system.
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 transition system.
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 transition system.
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 transition system.
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 transition system.
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 transition system.
Raises Rs.EXPORT_ERROR when an error occurs.