Index of values


(=) [Ctrl]
Equality for type Ctrl.t.

A
add [Link.Lg]
add [Link.Ports]
add [Link.Face]
add [Fun]
add [Nodes]
Add a node to the set.
add_exn [Iso]
add_exn i j iso adds a new pair (i, j) to isomorphism iso.
apply [Pbrs]
Sequential application of a list of reaction rules.
apply [Sbrs]
Sequential application of a list of reaction rules.
apply [Brs]
Sequential application of a list of reaction rules.
apply [Link.Ports]
apply [Fun]
Same as Fun.apply_exn but with error-aware return type.
apply [Iso]
Same as Iso.apply_exn but with error-aware return type.
apply_exn [Big]
apply_exn i b applies isomorphism i to bigraph b.
apply_exn [Link.Ports]
Apply an isomorphism.
apply_exn [Link]
apply_exn i l computes a link graph obtained by applying isomorphism i to l.
apply_exn [Place]
apply_exn [Fun]
apply_exn f x returns f(x).
apply_exn [Iso]
apply_exn iso i returns the value associated to i by isomorphism iso.
apply_exn [Nodes]
Apply an isomorphism.
arities [Link]
arity [Ctrl]
arity c returns the arity of control c.
arity_exn [Link.Ports]
atom [Big]
Same as Big.ion but without the site.
atom_chk [Big]
Same as Big.ion_chk but without the site.
auto [Big]
auto b computes the non-trivial automorphisms of bigraph b.

B
bfs [Pbrs]
bfs ~s0 ~priorities ~predicates ~max ~iter_f computes the transition system of the PBRS specified by initial state s0 and priority classes priorities.
bfs [Sbrs]
bfs ~s0 ~priorities ~predicates ~max ~iter_f computes the transition system of the SBRS specified by initial state s0 and priority classes priorities.
bfs [Brs]
bfs ~s0 ~priorities ~max ~iter_f computes the transition system of the BRS specified by initial state s0 and priority classes priorities.
bindings [Link.Ports]

C
cardinal [Pbrs]
Return the total number of probabilistic reaction rules in a list of priority classes.
cardinal [Sbrs]
Return the total number of stochastic reaction rules in a list of priority classes.
cardinal [Brs]
Return the total number of reaction rules in a list of priority classes.
cardinal [Link.Lg]
cardinal [Link.Ports]
cardinal [Link.Face]
cardinal [Fun]
cardinal [Iso]
cardinal_ports [Link]
Compute a sorted list with the cardinalities of the port sets.
check_codom [Fun]
check_codom min max f returns true if the codomain of f is in the range [min, max].
check_match [Place]
check_match t p trans iso checks if iso from p to t is a valid match.
choose [Link.Lg]
choose [Link.Ports]
choose [Link.Face]
close [Big]
close f b closes names in f.
closed_edges [Link]
Compute the number of closed edges.
closed_edges_iso [Link]
closed_edges_iso l computes the set of closed edges of link graph l.
closure [Big]
closure f computes the closure of interface f.
codom [Fun]
Return the codomain of a function.
codom [Iso]
Return the co-domain of an isomorphism.
comp [Big]
comp a b computes the composition of bigraphs a and b.
comp [Link]
comp a b n computes the composition of link graphs a and b.
comp [Place]
comp p0 p1 returns the composition of place graphs p0 and p1.
compare [Link.Lg]
compare [Link.Ports]
compare [Link.Face]
compare [Fun]
Comparison between functions.
compare [Iso]
Comparison between isomorphisms.
compare [Ctrl]
Comparison function.
compare_placing [Place]
compare_placing a b compares placings a and b.
compat_list [Link.Ports]
Construct a list of possible node assignments starting from two compatible port sets.

D
decomp [Big]
decomp t p i_n i_e f_e computes the decomposition of target t given pattern p, node isomorphism i_n and edge isomorphism i_e.
decomp [Link]
decomp target pattern i_e i_c i_d f_e computes the decomposition of target given pattern, iso i_e, and isos from nodes in t to nodes of c and d, respectively.
decomp [Place]
decomp t p i computes the decomposition of target t given pattern p and node isomorphism i from p to t.
decomp_d [Place]
Compute the decomposition D = D' X D_id.
deg_regions [Place]
Compute the outer degree of the regions of a place graph.
deg_sites [Place]
Compute the inner degree of the sites of a place graph.
diff [Link.Lg]
diff [Link.Face]
dom [Fun]
Return the domain of a function.
dom [Iso]
Return the domain of an isomorphism.

E
edges [Place]
Compute the number of edges in the DAG.
elementary_id [Link]
elementary_id f computes the identity over face f, i.e.
elementary_id [Place]
elementary_id m computes a place graph in the form of an identity of m.
elementary_ion [Link]
elementary_ion f computes an elementary ion with outer face f.
elementary_ion [Place]
An ion.
elementary_merge [Place]
elementary_merge m computes an elementary place graph formed by one region containing m sites.
elementary_split [Place]
elementary_split m computes an elementary place graph formed by one site shared by m regions.
elementary_sub [Link]
elementary_sub inner outer computes a substitution consisting of a single edge in which inner and outer are the inner and outer face, respectively.
elementary_sym [Place]
elementary_sym m n computes an place graph consisting of a symmetry between m and n.
elements [Link.Lg]
elements [Link.Face]
empty [Link.Lg]
empty [Link.Ports]
empty [Link.Face]
empty [Fun]
empty [Iso]
empty [Nodes]
The empty node set.
equal [Big]
equal a b returns true if bigraphs a and b are isomorphic, false otherwise.
equal [Link.Lg]
equal [Link.Ports]
equal [Link.Face]
equal [Fun]
Equality between functions.
equal [Iso]
Equality between isomorphisms.
equal [Nodes]
Equality test.
equal_opt [Big]
Same as Big.equal but with fewer checks prior to the SAT solver invocation.
equal_placing [Place]
equal_placing a b returns true if placings a and b are equal.
exists [Link.Lg]
exists [Link.Ports]
exists [Link.Face]

F
face_of_inter [Big]
Compute the face (i.e.
filter [Link.Lg]
filter [Link.Ports]
filter [Link.Face]
filter_apply_iso [Nodes]
Apply an isomorphism only to nodes in the domain of the isomorphism.
find [Link.Ports]
find_all [Nodes]
find_all ns c returns the set of nodes of control c in node set ns.
fix [Pbrs]
Reduce a reducible class to the fixed point.
fix [Sbrs]
Reduce a reducible class to the fixed point.
fix [Brs]
Reduce a reducible class to the fixed point.
fold [Link.Lg]
fold [Link.Ports]
fold [Link.Face]
fold [Fun]
fold [Iso]
fold [Nodes]
Fold over a set.
for_all [Link.Lg]
for_all [Link.Ports]
for_all [Link.Face]

G
gen_isos_exn [Iso]
gen_isos_exn iso autos generates the symmetric isomorphisms of iso by using autos, a list of automorphisms over the domain of iso.
get_ctrl_exn [Nodes]
get_ctrl_exn i ns returns the control of node i in node set ns.
get_dot [Link]
get_dot l computes a four-elements tuple encoding the dot representation of link graph l.
get_dot [Place]
get_dot p returns three strings expressing place graph p in dot format.

I
id [Big]
Identity over interface i.
id0 [Place]
id0 is the empty place graph.
id_empty [Link]
id_empty is the empty link graph.
id_eps [Big]
The empty identity.
inner [Big]
inner b computes the inner face of bigraph b.
inner [Link]
inner l computes the inner face of link graph l.
inter [Link.Lg]
inter [Link.Face]
inter_equal [Big]
Equality over interfaces.
intro [Big]
intro f computes an empty bigraph providing a fresh set of names f.
inverse [Fun]
Return the inverse of a function.
inverse [Iso]
Return the inverse of an isomorphism.
ion [Big]
ion ns c computes an ion of control c.
ion_chk [Big]
Same as Big.ion but with arity check.
is_determ [Pbrs]
Return true if a reaction rule is deterministic (i.e.
is_empty [Link.Lg]
is_empty [Link.Ports]
is_empty [Link.Face]
is_empty [Fun]
is_empty [Iso]
is_empty [Nodes]
Return true if the set is empty.
is_epi [Big]
is_epi b returns true if bigraph b is epimorphic, false otherwise.
is_epi [Link]
is_epi l is true if link graph l is epimorphic, false otherwise.
is_epi [Place]
is_epi p is true if place graph p is epimorphic, false otherwise.
is_ground [Big]
is_ground b returns true if bigraph b is an ground, false otherwise.
is_ground [Link]
is_ground l is true if link graph l has no inner names, false otherwise.
is_ground [Place]
is_ground p is true if place graph p has no sites, false otherwise.
is_guard [Big]
is_guard b returns true if bigraph b is an guarded, false otherwise.
is_guard [Link]
is_guard l is true if no edges in link graph l have both inner and outer names, false otherwise.
is_guard [Place]
is_guard p is true if place graph p is guarded, false otherwise.
is_id [Big]
is_id b returns true if bigraph b is an identity, false otherwise.
is_id [Link]
is_id l is true if link graph l is an identity, false otherwise.
is_id [Place]
is_id p returns true if place graph p is an identity, false otherwise.
is_id [Iso]
Returns true if an isomorphism is an identity, false otherwise.
is_inst [Sbrs]
Return true if a reaction rule is instantaneous, false otherwise.
is_mono [Big]
is_mono b returns true if bigraph b is monomorphic, false otherwise.
is_mono [Link]
is_mono l is true if link graph l is monomorphic, false otherwise.
is_mono [Place]
is_mono p is true if place graph p is monomorphic, false otherwise.
is_plc [Big]
is_plc b returns true if bigraph b is a placing, false otherwise.
is_plc [Place]
Test for the absence of nodes.
is_solid [Big]
is_solid b returns true if bigraph b is solid, false otherwise.
is_total [Fun]
Return true if a function is total, false otherwise.
is_valid_priority [Pbrs]
Return true if all the reaction rules in a priority class are valid, all the reaction rules in a reducible classes are deterministic.
is_valid_priority [Sbrs]
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.
is_valid_priority [Brs]
Return true if all the reaction rules in the priority class are valid, false otherwise.
is_valid_priority_list [Pbrs]
Return true if a list of priority classes contains at least a non reducible priority class, false otherwise.
is_valid_priority_list [Sbrs]
Return true if a list of priority classes contains at least a non reducible priority class, false otherwise.
is_valid_priority_list [Brs]
Return true if a list of priority classes contains at least a non reducible priority class, false otherwise.
is_valid_react [Pbrs]
Return true if the inner (outer) interfaces of the redex (reactum) are equal, the redex is solid, the instantiation map is total and the probability is greater than zero and less or equal than one.
is_valid_react [Sbrs]
Return true if the inner (outer) interfaces of the redex (reactum) are equal, the redex is solid, the instantiation map is total and the rate is greater than zero.
is_valid_react [Brs]
Return true if the inner (outer) interfaces of the redex (reactum) are equal, the redex is solid and the instantiation map is total.
is_valid_react_exn [Pbrs]
Same as Pbrs.is_valid_react but an exception is raised when the rule is not valid.
is_valid_react_exn [Sbrs]
Same as Sbrs.is_valid_react but an exception is raised when the rule is not valid.
is_valid_react_exn [Brs]
Same as Brs.is_valid_react but an exception is raised when the rule is not valid.
is_wir [Big]
is_wir b returns true if bigraph b is a wiring, false otherwise.
iter [Link.Lg]
iter [Link.Ports]
iter [Link.Face]
iter [Fun]
iter [Iso]
iter_states [Pbrs]
Apply f to every state.
iter_states [Sbrs]
Apply f to every state.
iter_states [Brs]
Apply f to every state.

J
json_of_big [Big]
Return a JSON representation of a bigraph.
json_of_link [Link]
Return a JSON representation of a link graph.
json_of_link_f [Link]
json_of_nodes [Nodes]
Return a JSON representation of a node set.
json_of_nodes_f [Nodes]
json_of_place [Place]
Return a JSON representation of a place graph.
json_of_place_f [Place]

K
key [Big]
Compute the key of a bigraph.

L
leaves [Place]
Compute the set of nodes with no children.
lhs_of_react [Pbrs]
The left-hand side (redex) of a reaction rule.
lhs_of_react [Sbrs]
The left-hand side (redex) of a reaction rule.
lhs_of_react [Brs]
The left-hand side (redex) of a reaction rule.
limit_msg [Rs]
limit_type [Rs]

M
map [Link.Ports]
mapi [Link.Ports]
match_edges [Link]
Compute constraints to match closed edges in the pattern to closed edges in the target.
match_leaves [Place]
match_leaves t p n_t n_p computes constraints to match the leaves (i.e.
match_list [Place]
match_list t p n_t n_p computes constraints to match edges in pattern p with compatible edges in target t.
match_list_eq [Link]
Similar to Link.match_edges but constraints are for equality.
match_list_eq [Place]
Compute constraints for equality.
match_nodes_sites [Place]
match_orphans [Place]
match_peers [Link]
Compute constraints to match peers in the pattern with peers in the target.
match_ports [Link]
Compute constraints to match isomorphic port sets in closed edges.
match_ports_eq [Link]
Similar to Link.match_ports but constraints are for equality.
match_region_nodes [Place]
Compute constraints for equality: regions must have children with the same controls.
match_regions [Place]
Compute constraints to match regions.
match_sites [Place]
match_trans [Place]
Compute constraints to block matches between unconnected pairs of nodes with sites and nodes with regions.
max_binding [Link.Ports]
max_elt [Link.Lg]
max_elt [Link.Face]
max_ports [Link]
Compute the maximum number of ports in one edge of a link graph.
mem [Link.Lg]
mem [Link.Ports]
mem [Link.Face]
mem [Fun]
mem [Iso]
merge [Big]
Bigraph consisting of one root and n sites.
min_binding [Link.Ports]
min_elt [Link.Lg]
min_elt [Link.Face]
module_id [Rs]

N
name [Ctrl]
name c returns the arity of control c.
nest [Big]
nest a b computes the bigraph resulting from nesting bigraph b in bigraph a.
norm [Link]
Normalise link graph l as follows: l = omega o l' where omega is a linking and l' is the same as l but with all links open.
norm [Nodes]
Compute the norm of a set.
not_sub [Nodes]
not_sub a b returns true when node set a is not a subset of node set b.

O
occurrence [Big]
occurrence t p trans returns a pair of isomorphisms (i,j) if pattern p occurs in target t.
occurrences [Big]
occurrences t p returns a list of occurrences.
occurs [Big]
occurs t p returns true if pattern p occurs in target t, false otherwise.
of_list [Fun]
Inverse of Fun.to_list.
of_list_exn [Iso]
of_list l returns an isomorphism with the elements in list l.
of_nodes [Link.Ports]
of_nodes ns transform a set of nodes into a set of ports.
offset [Link.Ports]
one [Big]
Elementary bigraph consisting of one root.
one [Place]
one is the place graph formed by an idle region.
ord_of_inter [Big]
Compute the ordinal of an interface.
orphans [Place]
Compute the set of nodes with no parents.
outer [Big]
outer b computes the outer face of bigraph b.
outer [Link]
outer l computes the outer face of link graph l.

P
par [Big]
par a b computes the merge product of bigraphs a and b.
par_of_list [Big]
par_of_list bs computes the merge product of all the bigraphs in list bs.
parse [Big]
Parse a bigraph.
parse [Link]
Parse a list of strings.
parse [Place]
parse r n s lines computes a place graph with r regions, n nodes and s sites.
parse [Fun]
parse l returns a function in which the numbers from 0 to n - 1 (with n the length of l) are mapped to the elements of l, in the given order.
parse [Nodes]
parse s m parses the string representation of a node set.
parse_face [Link]
parse_face ns computes a face starting from list of string names ns.
parse_placing [Place]
parse_placing l r returns the placing with r regions defined by list l in which each element is a site's parent set.
parse_react [Pbrs]
Create a new reaction rule.
parse_react [Sbrs]
Create a new reaction rule.
parse_react [Brs]
Create a new reaction rule.
partition [Link.Lg]
partition [Link.Ports]
partition [Link.Face]
placing [Big]
placing l r f computes a placing with r roots by parsing list l.
ppar [Big]
ppar a b computes the parallel product of bigraphs a and b.
ppar [Link]
ppar a b n computes the parallel composition of link graphs a and b.
ppar_of_list [Big]
ppar_of_list bs computes the parallel product of all the bigraphs in list bs.
prime_components [Link]
Compute the prime components of a link graph.
prime_components [Place]
Compute the prime components (i.e.

R
random_step [Pbrs]
Compute a random state reachable in one step.
random_step [Sbrs]
Select step of Gillespie SSA.
random_step [Brs]
Compute a random state reachable in one step.
remove [Link.Lg]
remove [Link.Ports]
remove [Link.Face]
rename [Big]
rename inner outer b renames the names in in to the names in out.
rewrite [Pbrs]
Scan priority classes and reduce a state.
rewrite [Sbrs]
Scan priority classes and reduce a state.
rewrite [Brs]
Scan priority classes and reduce a state.
rewrite [Big]
rewrite o s r0 r1 eta computes a bigraph obtained by replacing the occurrence of r0 (specified by occurrence o) in s with eta r1, where eta is a valid (no check performed) instantiation map.
rhs_of_react [Pbrs]
The right-hand side (reactum) of a reaction rule.
rhs_of_react [Sbrs]
The right-hand side (reactum) of a reaction rule.
rhs_of_react [Brs]
The right-hand side (reactum) of a reaction rule.

S
share [Big]
share f psi g computes the bigraphs obtained by sharing bigraph f in bigraph g by using placing psi.
sim [Pbrs]
Simulate the PBRS specified by initial state s0 and priority classes priorities.
sim [Sbrs]
Simulate (using Gillespie SSA) the SBRS specified by initial state s0 and priority classes priorities.
sim [Brs]
Simulate the BRS specified by initial state s0 and priority classes priorities.
sim_type [Rs]
singleton [Link.Lg]
singleton [Link.Ports]
singleton [Link.Face]
split [Big]
Bigraph consisting of one site and n roots.
split [Link.Lg]
split [Link.Ports]
split [Link.Face]
step [Pbrs]
Compute the set of reachable states in one step.
step [Sbrs]
Compute the set of reachable states in one step.
step [Brs]
Compute the set of reachable states in one step.
string_of_face [Link]
string_of_face f computes the string representation of face f.
string_of_inter [Big]
Compute the string representation of an interface.
string_of_limit [Pbrs]
String representation of a simulation limit.
string_of_limit [Sbrs]
String representation of a simulation limit.
string_of_limit [Brs]
String representation of a simulation limit.
string_of_react [Pbrs]
String representation of a probabilistic reaction rule.
string_of_react [Sbrs]
String representation of a stochastic reaction rule.
string_of_react [Brs]
String representation of reaction rules.
string_of_react_err [Pbrs]
String representation of reaction validity errors.
string_of_react_err [Sbrs]
String representation of reaction validity errors.
string_of_react_err [Brs]
String representation of reaction validity errors.
string_of_sorts [Nodes]
Return a string representation of the sorts of a node set.
string_of_stats [Pbrs]
Stats are representated as a list whose elements are strings in the following form: (description, value, flag).
string_of_stats [Sbrs]
Stats are represented as a list whose elements are strings in the following form: (description, value, flag).
string_of_stats [Brs]
Stats are represented as a list whose elements are strings in the following form: (description, value, flag).
sub [Big]
sub inner outer computes a substitution where inner and outer are the inner and outer faces, respectively.
subset [Link.Lg]
subset [Link.Face]
sum [Link.Ports]
sym [Big]
Symmetry on interfaces i and j.

T
tens [Big]
tens a b computes the tensor product of bigraphs a and b.
tens [Link]
tens a b n computes the tensor product of link graphs a and b.
tens [Place]
tens p0 p1 returns the tensor product of place graphs p0 and p1.
tens [Nodes]
tens n0 n1 returns the disjoint union of name sets n0 and n1.
tens_of_list [Place]
Same as Place.tens but on a list of place graphs.
to_IntSet [Link.Ports]
to_IntSet ps returns a set of node identifiers form a set of ports.
to_dot [Pbrs]
Compute the string representation in dot format of a DTMC.
to_dot [Sbrs]
Compute the string representation in dot format of a CTMC.
to_dot [Brs]
Compute the string representation in dot format of a transition system.
to_dot [Big]
to_dot b i compute the string expressing bigraph b named i in dot format.
to_dot [Nodes]
to_dot ns returns a string expressing node shapes in dot format.
to_lab [Pbrs]
Compute the string representation in PRISM lab format of the labelling function of a DTMC.
to_lab [Sbrs]
Compute the string representation in PRISM lab format of the labelling function of a CTMC.
to_lab [Brs]
Compute the string representation in PRISM lab format of the labelling function of a transition system.
to_list [Fun]
Return the list of pairs defined by a function.
to_list [Iso]
Return the list of pairs defined by an isomorphism.
to_prism [Pbrs]
Compute the string representation in PRISM tra format of a DTMC.
to_prism [Sbrs]
Compute the string representation in PRISM tra format of a CTMC.
to_prism [Brs]
Compute the string representation in PRISM tra format of a transition system.
to_string [Big]
Compute the string representation of a bigraph.
to_string [Link.Ports]
to_string s gives the string representation of port set s.
to_string [Link]
to_string l computes the string representation of link graph l.
to_string [Place]
to_string p returns a string representation of place graph p.
to_string [Rs]
to_string [Fun]
Return the string representation of a function.
to_string [Iso]
Return the string representation of an isomorphism.
to_string [Nodes]
Return a string representation of a node set.
to_string [Ctrl]
to_string c gives the string representation of control c in the form name:arity.
to_string_ext [Rs]
transform_exn [Fun]
transform_exn f iso_d iso_c returns the function obtained by applying iso_d and iso_c to the domain and codomain of f, respectively.
transform_exn [Iso]
transform_exn i iso_d iso_c returns the isomorphism obtained by applying iso_d and iso_c to the domain and co-domain of i, respectively.
ts_type [Rs]
typ [Pbrs]
Type of transition system: PBRS .
typ [Sbrs]
Type of transition system: SBRS .
typ [Brs]
Type of transition system: BRS.
types [Link.Ports]
Construct a list of control strings.

U
union [Link.Lg]
union [Link.Face]

W
write_dot [Pbrs]
Export to file the string representation in dot format of a DTMC.
write_dot [Sbrs]
Export to file the string representation in dot format of a CTMC.
write_dot [Brs]
Export to file the string representation in dot format of a transition system.
write_dot [Big]
Export to file the string representation in dot format of a bigraph.
write_json [Pbrs]
Export to file the string representation in json format of a DTMC.
write_json [Sbrs]
Export to file the string representation in json format of a CTMC.
write_json [Brs]
Export to file the string representation in json format of a transition system.
write_json [Big]
Export to file the string representation in json format of a bigraph.
write_lab [Pbrs]
Export to file the string representation in PRISM lab format of the labelling function of a DTMC.
write_lab [Sbrs]
Export to file the string representation in PRISM lab format of the labelling function of a CTMC.
write_lab [Brs]
Export to file the string representation in PRISM lab format of the labelling function of a transition system.
write_prism [Pbrs]
Export to file the string representation in PRISM tra format of a DTMC.
write_prism [Sbrs]
Export to file the string representation in PRISM tra format of a CTMC.
write_prism [Brs]
Export to file the string representation in PRISM tra format of a transition system.
write_svg [Pbrs]
Export to file the string representation in svg format of a DTMC.
write_svg [Sbrs]
Export to file the string representation in svg format of a CTMC.
write_svg [Brs]
Export to file the string representation in svg format of a transition system.
write_svg [Big]
Export to file the string representation in svg format of a bigraph.
write_txt [Big]
Export to file the string representation in txt format of a bigraph.

Z
zero [Big]
Elementary bigraphs consisting of one site.
zero [Place]
zero is the place graph formed by an orphaned site.