Module type Brs.T

Output signature of the functor Brs.Make.

type react

The type of bigraphical reaction rules.

val pp_react : Ppx_deriving_runtime.Format.formatter -> react -> Ppx_deriving_runtime.unit
val show_react : react -> Ppx_deriving_runtime.string
val react_to_yojson : react -> Yojson.Safe.t
val react_of_yojson : Yojson.Safe.t -> react Ppx_deriving_yojson_runtime.error_or
type p_class =
  1. | P_class of react list
    (*

    Priority class.

    *)
  2. | P_rclass of react list
    (*

    Reducing priority class.

    *)

The type of priority classes.

type graph

The type of transition systems.

val graph_to_yojson : graph -> Yojson.Safe.t
val graph_of_yojson : Yojson.Safe.t -> graph Ppx_deriving_yojson_runtime.error_or
type label = unit

The type of edge labels in BRSs.

val pp_label : Ppx_deriving_runtime.Format.formatter -> label -> Ppx_deriving_runtime.unit
val show_label : label -> Ppx_deriving_runtime.string
val label_to_yojson : label -> Yojson.Safe.t
val label_of_yojson : Yojson.Safe.t -> label Ppx_deriving_yojson_runtime.error_or
type limit = int

Type of simulation limit i.e., number of execution steps or wall time.

val pp_limit : Ppx_deriving_runtime.Format.formatter -> limit -> Ppx_deriving_runtime.unit
val show_limit : limit -> Ppx_deriving_runtime.string
val stats_trans : Rs_intf.stats -> int

Number of transitions in the stats record.

type react_error

The type of reaction validity errors.

Reaction rules

val name : react -> string

The name of the reaction rule.

val lhs : react -> Big.t

The left-hand side (redex) of a reaction rule.

val rhs : react -> Big.t

The right-hand side (reactum) of a reaction rule.

val label : react -> label

The label of a reaction rule.

val conds : react -> AppCond.t list

List of application conditions.

val map : react -> Fun.t option

The instantiation map of a reaction rule.

val parse_react_unsafe : name:string -> lhs:Big.t -> rhs:Big.t -> ?conds:AppCond.t list -> ?cond_captures:string list -> label -> 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 : name:string -> lhs:Big.t -> rhs:Big.t -> ?conds:AppCond.t list -> ?cond_captures:string list -> label -> Fun.t option -> react option

Same as parse_react_unsafe but returns None if it is impossible to parse a valid reaction.

val parse_react_err : name:string -> lhs:Big.t -> rhs:Big.t -> ?conds:AppCond.t list -> ?cond_captures:string list -> label -> Fun.t option -> (react, string) Stdlib.result

Same as parse_react but returns Error string if it is impossible to parse a valid reaction (with an error message), else Ok react.

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.

exception NOT_VALID of react_error

Raised when a reaction rule is not valid.

val is_valid_react_exn : react -> bool

Same as is_valid_react but an exception is raised when the rule is not valid.

val string_of_react_err : react_error -> string

String representation of reaction validity errors.

val equal_react : react -> react -> bool

Equality for reaction rules.

val equal : Big.t -> Big.t -> bool

Bigraph isomorphism: returns true if two bigraphs are isomorphic (including parameter values). Same check used by the BFS state loop.

val step : Big.t -> react list -> (Big.t * label * react list) 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 : Stdlib.Random.State.t -> Big.t -> react list -> (Big.t * label * react list) option * int

Compute a random state reachable in one step, using the given random state for reproducibility. The total number of occurrences is also returned.

val random_step_forced : Stdlib.Random.State.t -> Big.t -> react list -> react -> (Big.t * label * react list) option * int

Compute a random state reachable in one step, conditioned on rule firing: the successor is drawn from rule's occurrences and, for SBRS, the sojourn at the exit rate of the full class rules, the CTMC path conditioned on the rule firing. The total number of occurrences of rule is also returned.

val apply : Big.t -> react list -> Big.t 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 fix : Big.t -> react list -> Big.t * int

Reduce a reducible class to the fixed point. The number of rewriting steps is also returned.

Priorities

val is_valid_priority : p_class -> bool

Return true if a priority class is valid, false otherwise.

val is_valid_priority_err : p_class -> (unit, string) Stdlib.result

Ok () if the class is valid, otherwise Error reason with a precise explanation of the violation. is_valid_priority c = Result.is_ok (is_valid_priority_err c).

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 rewrite : Big.t -> p_class list -> Big.t * 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.

val occurs : target:Big.t -> pattern:Big.t -> bool

Return true if the pattern occurs in the target. The same check used for predicate labelling in bfs and sim.

type rule_info = {
  1. ri_idx : int;
    (*

    Index of the rule in its priority class.

    *)
  2. ri_name : string;
    (*

    Name of the rule.

    *)
  3. ri_occ : int;
    (*

    Number of occurrences of the rule's redex.

    *)
  4. ri_enabled : bool;
    (*

    Whether at least one occurrence of the rule is applicable.

    *)
}
type class_info = {
  1. ci_idx : int;
    (*

    Index of the class in the priority list.

    *)
  2. ci_reducing : bool;
    (*

    Whether the class is a reducing (instantaneous) class.

    *)
  3. ci_rules : rule_info list;
    (*

    Information about all the rules in the class.

    *)
  4. ci_enabled_rules : rule_info list;
    (*

    Information about the enabled rules in the class.

    *)
}
val scan_all_enabled : Big.t -> p_class list -> class_info list

Return all the priority classes with at least one enabled rule, in priority order.

val scan_top_enabled : Big.t -> p_class list -> class_info option

Return the first priority class with at least one enabled rule (highest priority first), or None if no rule is enabled (deadlock).

val rewrite_trace : Big.t -> p_class list -> Big.t * (string list * int) list

Same reduction as rewrite, but also record a trace of the reducing classes that fired: for each, the names of the rules enabled at the start of the reduction and the number of fixing steps. The trace is returned in firing order.

val set_wildcard_threshold : int -> unit

Set the group-size threshold for wildcard structural matching. Groups with fewer than n rules use direct per-rule matching; larger groups use wildcard structural matching (one solve + partition). Default is 3. Call before select_path.

val select_path : unit -> unit

Resolve all matching implementation refs. Call once after priorities are compiled, before any matching or state exploration.

Reactive systems

Functions to generate the labelled transition system of a reactive system.

exception MAX of graph * Rs_intf.stats

Raised when a new state would be assigned an index greater than the maximum state index.

val bfs : s0:Big.t -> priorities:p_class list -> predicates:Rs_intf.pred_entry list -> max:int -> (int -> Big.t -> unit) -> graph * Rs_intf.stats

bfs ~s0 ~priorities ~predicates ~max iter_f computes the transition system of the reactive system specified by initial state s0 and priority classes priorities. Arguments ~max and iter_f are the maximum state index of the transition system and a function to be applied whenever a new state is discovered, respectively. States are indexed from 0, so the transition system holds at most max + 1 states, including the initial state. iter_f takes two arguments, the index of the current state (starting from 0) and the corresponding bigraph. 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. The generation of the transition system is performed in a breadth-first search fashion.

  • raises MAX

    when a new state would be assigned an index greater than max.

exception DEADLOCK of graph * Rs_intf.stats * limit

Raised when a simulation reaches a deadlock state.

exception LIMIT of graph * Rs_intf.stats

Raised when a simulation reaches the simulation limit.

val sim : s0:Big.t -> ?seed:int -> priorities:p_class list -> predicates:Rs_intf.pred_entry list -> init_size:int -> stop:limit -> (int -> Big.t -> limit -> unit) -> graph * Rs_intf.stats

Simulate the reactive system specified by initial state s0 and priority classes priorities. Arguments init_size and stop are the initial size of the state set and the simulation limit, respectively. Function iter_f is applied to every new state discovered during the simulation. It takes three arguments, the index of the current state (starting from 0), the corresponding bigraph, and the simulation progress, i.e. the current number of simulation steps or the current simulation time. Optional argument seed is used to initialise the random generator with a specific seed. List of predicates predicates is also checked for every state.

  • raises DEADLOCK

    when the simulation reaches a deadlock state.

  • raises LIMIT

    when the simulation limit is exceeded.

Export functions

val to_txt : graph -> string
val to_dot : graph -> path:string -> name:string -> string
val to_state_rewards : graph -> string
val to_prism : graph -> string
val to_transition_rewards : graph -> string
val to_lab : graph -> string

Incremental transition system

Functions to accumulate a transition system as steps are taken, mirroring what bfs and sim build internally.

val trace_make : Rs_intf.pred_entry list -> graph

Create an empty transition system for the given predicates. The entries' patterns are ignored here; they are checked by check_predicates as states are added.

val add_state : graph -> int -> Big.t -> unit

Add a state to the transition system.

val add_transition : graph -> source:int -> dest:int -> label -> react list -> unit

Add a transition from source to dest, with the given label and the rules that fired.

val check_predicates : graph -> Rs_intf.pred_entry list -> int -> Big.t -> Predicate.t list

Check the predicates against a state and record which ones match; return the recorded predicates, in the entries' order.

val state_preds : graph -> int -> Predicate.t list

Return the predicates recorded as matching a state.

Iterators

val iter_states : (int -> Big.t -> unit) -> graph -> unit
val fold_states : (int -> Big.t -> 'a -> 'a) -> graph -> 'a -> 'a
val iter_edges : (int -> int -> label -> Base.S_string.t -> unit) -> graph -> unit
val fold_edges : (int -> int -> label -> Base.S_string.t -> 'a -> 'a) -> graph -> 'a -> 'a
val rules_fired : graph -> int

Number of distinct reaction rules that fired along at least one transition of the transition system.

val kind : Rs.rs_type

The kind of reactive system.