Module type `Rs.RS`

Output signature of the functor Rs.Make.

type react: The type of bigraphical reaction rules.

type ac: The type of application conditions.

type p_class = | P_class of react list Priority class. | P_rclass of react list Reducing priority class.: The type of priority classes.

type graph: The type of transition systems.

type label: The type of edge labels in BRSs.

type limit: Type of simulation limit i.e., number of execution steps.

val typ : rs_type: The kind of reactive system.

type react_error: The type of reaction validity errors.

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 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 right-hand side (reactum) of a reaction rule.

val conds : react -> ac 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:ac 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:ac list -> label -> Fun.t option -> react option: Same as Brs.parse_react_unsafe but returns None if it is impossible to parse a valid reaction.

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.

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.

raises NOT_VALID: 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 is_valid_priority : p_class -> bool: Return true if a priority class is 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 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 : Big.t -> react list -> (Big.t * label * react list) option * int: Compute a random state reachable in one step. The total number of occurrences 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.

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.

exception MAX of graph * stats: Raised when the size of the transition system reaches the maximum number of states.

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

bfs ~s0 ~priorities ~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 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.

exception DEADLOCK of graph * stats * limit: Raised when a simulation reaches a deadlock state.

exception LIMIT of graph * stats: Raised when a simulation reaches the simulation limit.

val sim : s0:Big.t -> priorities:p_class list -> predicates:(Base.Predicate.t * Big.t) list -> init_size:int -> stop:limit -> iter_f:(int -> Big.t -> unit) -> graph * stats

Simulate the raective 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.

raises DEADLOCK: when the simulation reaches a deadlock state.

raises LIMIT: when the simulation limit is exceeded.

val to_prism : graph -> string: Compute the string representation in PRISM tra format of a transition system.

val to_state_rewards : graph -> string: Compute the string representation in PRISM rews format of state rewards.

val to_transition_rewards : graph -> string: Compute the string representation in PRISM trew format of transition rewards.

val to_dot : graph -> path:string -> 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 : (int -> Big.t -> unit) -> graph -> unit: Iterators

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

`\|` `P_class of react list`	Priority class.
`\|` `P_rclass of react list`	Reducing priority class.

Iterators