The eden framework provides tools for the formal modelling and analysis of social-ecological systems and their dynamics. In particular, it features the rr modelling language (for reaction rules) that allows defining systems as Boolean variables and guarded actions to update them. This language is equipped with a compact semantics in terms of Petri nets extended with read-arcs, inhibitor arcs, reset arcs, and transition priorities. Apart from the last one, these extensions can be implemented in standard Petri nets at the price of building bigger nets. In this paper, we extend the rr language with multivalued variables, spatial information inspired by membrane computing, and timing. The resulting language, called mrr (for multivalued rr), is equipped with a compact colored Petri nets semantics extended with only transition priorities.
The eden framework has been developed and used in the field of ecology for years [
However, having only Boolean variables sometimes requires awkward modelling tricks, which
leads to the need for multivalued variables. For instance, a population of animals may have distinct
efects on the system depending on distinct thresholds that are known to exist even if not precisely
quantified. In such a case, we would like to move from “not enough”/“enough” to, for instance, “not
enough”/“low”/“high” [
This paper extends the rr language [
Finally, we further extend rr with a representation of spatial information inspired from membrane
systems [
In this paper, we thus present the mrr language that extends rr with these three aspects. Both
languages use discrete variables, with actions to model their changes. Actions are split into rules and
constraints, the latter having a higher priority. Actions are composed of a guard on the variables, and a
series of assignments to update them. An mrr system consists of as a set of nested locations in which
the variables and actions are declared. Each action may refer only to the variables in the same location
where it was defined, or those in the location that immediately contains it, or those in the locations
immediately contained in it. Variables in mrr are allowed to have several initial states, which means
that the system itself is analyzed starting from several initial states [
The next section describes the syntax and semantics of mrr, with an example to illustrate the operational semantics. Since mrr is an extension of rr, references to the latter will point out where the languages coincide. The Petri nets semantics is defined in Section 3. Section 4 describes the implementation of mrr in ecco, and shows a second example that is quickly analyzed within ecco. Before the conclusion, related works are presented and discussed.
We start with a presentation of the concrete mrr language, from a modeller’s perspective. The concrete syntax is given for reference in Figure 1, but it is presented more intuitively below. The end of the section will define the language from a more abstract perspective, which will allow giving its formal semantics.
The structure of an mrr file is as follows: 1 clocks: 2 # here: clocks declarations 3 variables: 4 # here: variables declarations 5 # here: locations declarations 6 constraints: 7 # here: constraints declarations 8 rules: 9 # here: rules declarations Above, #... are comments that start with # and end at the end of the line. Every part above is optional and may be skipped, but if a section (e.g. variables: ) is used, then it must not be empty, and its whole content should be indented. mrr is using indentation as blocks delimitation like in the Python programming language.
Every clock is declared as NAME: description on a single line. NAME must start with a letter and may continue with letters or digits. The name given to each clock will be used later on to link variables to this clock, in order to indicate that the linked variables have to be incremented when the clock ticks. system clocks clockdecl
model variables constraints
rules location vardecl
type scalar
init simpleinit
var index quantifier
NAME
NAT INT
CMP DESC ∣ ∣ actdecl ∶∶= condition ∶∶=
∣ assignment ∶∶= ∶∶= ∶∶= ∶∶= ∶∶= ∶∶= ∶∶= ∶∶= ∶∶= ∶∶=
∣ ∶∶= ∶∶=
∣ ∶∶= ∶∶=
∣ ∶∶= ∶∶=
∣
∶∶=
∶∶=
∶∶=
∶∶=
∶∶=
∶∶=
[clocks] model
“clocks:” ↲ →∣ clockdecl+ ∣ ←
NAME “:” DESC ↲
[variables] location∗ [constraints] [rules]
“variables:” ↲ →∣ vardecl+ ∣ ←
“constraints:” ↲ →∣ actdecl+ ∣ ←
“rules:” ↲ →∣ actdecl+ ∣ ←
“location” NAME [“[” NAT “]”] “:” ↲ →∣ model ∣ ←
type NAME “=” init “:” DESC ↲
NAME /[+*-]/ “:” DESC ↲
scalar [“[” NAT “]”]
“bool”
“{” [NAME “:”] INT “..” INT “}”
simpleinit (“|” simpleinit)∗
INT [“..” INT]
“(” simpleinit (“,” simpleinit)∗ “)”
“*”
[“[” /[^\]]+/ “]”] condition (“,” condition)∗
“>>” assignment (“,” assignment)∗ [quantifier] ↲
(var ∣ INT) CMP (var ∣ INT)
var /[+-]/
var /[+-]?=/ (var ∣ INT)
var /[+*-]|\+\+|--/
NAME [“[” index “]”] [“@@” ∣ “@” NAME [“[” index “]”]]
NAT
NAME [(“+” ∣ “-”) NAT]
“for” (“any” ∣ “all”) NAME (“,” NAME)∗ (“,” quantifier)∗
/[a-z][a-z0-9]*/
/[
mrr is using the so-called causal time model of time in which a time reference is just a tick event in
the system that increments variables used to measure the passing of time by counting the ticks [
In mrr, clocked variables (i.e. integer variables linked to clocks) are necessarily bounded as mrr only
allows finite ranges for every variable. This ensures that every state-space (often called state-transition
graph [18, Sec. 1.1] in ecology) is finite, even if it may be so huge that it cannot be computed. This has a
consequence that is well known in causal time approaches: when a clocked variable has reached its
maximal value, the corresponding tick cannot occur anymore as it would overcome the variable range.
So time progression is blocked, but only in appearance. Indeed, when using causal time, two situations
become logically equivalent:
• an action will always be taken before the next tick;
• no tick can occur until the action has been taken.
This is also called the deadline paradox that disappears when time is treated in a strictly causal way [
The simplest form of a variable declaration in mrr is, like in rr, one of: • NAME+: description to declare a Boolean variable initialized on; • NAME-: description to declare a Boolean variable initialized off; • NAME*: description to declare a Boolean variable with two initial states on and off. More generally, a variable is declared as TYPE NAME = INIT: description where: • TYPE is the type of the variable, i.e. the range of values it can hold, which can be: – bool for a Boolean variable, – {MIN..MAX} for an integer variable ranging from MIN to MAX , – {CLOCK: MIN..MAX} for an integer variable that is incremented when CLOCK ticks; • NAME is the name of the variable that is used to refer to it within actions, this name must be unique at the level of the location where it is declared; • INIT is the set of initial values for the variables: – INT specifies a single value, – INT..INT specifies a full range of values, – INIT|INIT specifies the union of two sets of values, – * specifies the full range of possible values for the variable.
For instance, declaration {0..1} var = 0: my variable is equivalent to the shorter declaration bool var = 0: my variable (because Boolean are implemented as 0/1-valuated integers), or the even shorter var-: my variable . Declaration {0..4} level = 2: a description is a declaration of a variable called level that ranges between 0 and 4 and is initially set to 2.
Note that, when a variable is clocked, initial value * has the special meaning that time can pass without changing the variable.
Finally, variables may be declared as arrays by adding [SIZE] after their type, where SIZE is
a positive integer value. In such a case, INIT may be a single initialization as above to set all the
array to the same initial value, or a sequence of initialization to set diferent initial values for each cell.
For instance bool[
1 location NAME: 2 variables: 3 # ... 4 # here: further nested locations 5 constraints: 6 # ... 7 rules: 8 # ... location NAME: introduces the new location, and its content is indented and corresponds exactly to the structure described above for the top location, except that clocks are not allowed here. Contrasting with the top location that has no name, a nested location is always named, and its name must be unique at the level of the location where it is declared. It is also possible to declare an array of locations by adding [SIZE] after its name, where SIZE is a positive integer value: 1 location NAME[SIZE]: 2 # as previously Arrays of locations are convenient for declaring several identical locations that will evolve independently during the execution.
Actions are all declared the same way, but in two separate sections to distinguish between constraints and rules. The only diference is that constraints execute with a higher priority. Every action is declared following the same structure [TAG, ...] COND, ... >> ASSIGN, ... QUANT where: • [TAG, ...] is an optional comma-separated sequence of arbitrary tags that decorate the action, at the level of mrr they have no special meaning, but they may be used during the analysis; • COND, ... is a mandatory comma-separated sequence of conditions, all of which must be validated to allow the execution of the action; • ASSIGN, ... is a mandatory comma-separated sequence of assignments, all of which is performed upon the execution of the action; • QUANT is a quantification of the free variables used in each COND or ASSIGN (see below). A COND must be one of: • VAR OP VAL or VAL OP VAR to compare a variable to a value; • VAR OP VAR to compare two variables; • VAR+ like in rr, that is here a shorthand for VAR==1 ; • VAR- like in rr, that is here a shorthand for VAR==0 ; where OP is one of == , != , < , > , <= , >= . Every VAR must be either: • NAME to refer to a variable declared in the same location as the action; • NAME[IDX] to refer to a cell of an array declared in the same location; • NAME@LOC to refer to a variable declared in a location named LOC nested immediately inside that where the action is defined; • NAME[IDX]@LOC to refer to an array in nested location LOC ; • NAME@LOC[IDX] to refer to a variable declared in a nested array of locations; • NAME[IDX]@LOC[IDX] to refer to an array declared in a nested array of locations; • NAME@@ to refer to a variable declared in the enclosing location; • NAME[IDX]@@ to refer to an array declared in the enclosing location. Then, every IDX must be either an integer literal, a free variable (a name that does not refer to a known variable, clock, or location), or a simple expression as i+1 or i-2 involving a free variable, plus or minus operator, and a constant. We will come back to free variables below.
On the right-hand side of an action, following >> , every ASSIGN must be one of: • VAR = EXPR to assign a new value expressed by EXPR to TARGET ; • VAR += EXPR or VAR -= EXPR to perform so-called augmented assignment; • VAR++ , VAR-- as shorthands for the longer forms above; • VAR+ like in rr, that is here a shorthand for VAR=1 ; • VAR- like in rr, that is here a shorthand for VAR=0 ; • VAR* that is a special form reserved to clocked variables that lets time pass (i.e. ticks occur) without changing the variable.
Here VAR is as described for conditions, and EXPR must be either another VAR or an integer.
As presented above, an IDX may refer to free variables, e.g. we could have an action such as array[i]<2 >> array[i]++ . Such an action needs to be completed by a quantifier for i in order to specify its semantics.
First, array[i]<2 >> array[i]++ for all i means that the condition and assignment will be
evaluated for all the possible values of i , which depends on the declaration of the array and on its
size in particular. Assuming, for instance, that array was declared with size 2, the action above
is equivalent to array[0]<2, array[
Then, array[i]<2 >> array[i]++ for any i means that the condition and assignment will be
evaluated using any but only one of the possible values of i . Assuming the same size, this is equivalent
to having actually two actions: array[0]<2 >> array[0]++ and array[
In general, quantifiers may be combined arbitrarily when there is more than one free variable. For instance, arr[i]>vec[j] >> tab[k]++ for all i, j, for any k is a valid action assuming arr , vec , and tab are arrays.
To conclude on arrays within actions, one special free variable self needs no quantification and can be used only from within an array of locations, in which case it refers to the index within the array of the location that executes the action. This is illustrated just below.
This model has a static number of nests and animals in each nest, but this can be changed easily thanks to the #define directives at the beginning. An mrr model is always passed to the C preprocessor before it is parsed, so mrr supports the full range of C preprocessor directives even if not all are meaningful in this context.
An mrr system and its constituting elements will be formally defined in terms of structures with typed ifelds, like in programming languages, and we will use the dot notation to access these fields. For instance, if is a structure ⟨clocks∣ top⟩ then .clocks and .top are its two fields. We implement value * used to assign clocked variables as −1, thus, we assume that the domain of every clocked variable, is augmented with value −1 that does not need to be declared in the concrete syntax but will be present in the abstract syntax so that variables are valued in Z instead of in N. Then, we consider a set I of identifiers, i.e. arbitrary names including forms like nest[0] that is considered as an identifier. Names can be combined with dots, to form new names, for instance, if nest[0] and in are identifiers, then nest[0].in is also an identifier.
Definition 1 ( mrr abstract syntax). A variable is a structure ⟨name∣ dom∣ init∣ clock⟩ where: • name ∈ I; • dom ⊂ Z is its domain; • init ⊆ dom is its set of initial values; • clock ∈ I ∪ {⊥} is its clock, if any.
A condition is a structure ⟨left∣ op∣ right⟩ where: • target ∈ I; • value is an expression or a value in Z, the augmented assignments allowed by the concrete syntax are thus here translated to regular assignments. • left ∈ I; • op ∈ { == , != , < , > , <= , >= }; • right ∈ I ∪ Z.
An expression is a structure ⟨left∣ op∣ right⟩ where: • left ∈ I; • op ∈ { + , - , * , / }; • right ∈ I ∪ Z.
An assignment is a structure ⟨target∣ value⟩ where: An action is a structure ⟨left∣ right∣ tag⟩ where: • left is a set of conditions; • right is a set of assignments; • tag is arbitrary text. • name ∈ I; • vars is a set of variables; • locs is a set of locations; • cons is a set of actions; • rules is a set of actions.
A location is a structure ⟨name∣ vars∣ locs∣ cons∣ rules⟩ where: An mrr system is a structure ⟨clocks∣ top⟩ where: • clocks ⊂ I; • top is a location such that top.name = .
An mrr system so defined must validate varied constraints, in particular no two items declared at the same level can have the same name. For instance, for every location , we must have {.name}, {.name ∣ ∈ .vars}, {.name ∣ ∈ .locs}, and .clocks be pairwise disjoint. Moreover, a variable cannot be assigned twice in the right-hand-side of an action. Finally, in an mrr obtained from the concrete syntax, the identifiers involved in actions must be either: • names of variables defined in the same location as the action; • names of the form ..name to refer to variables defined in the enclosing location; • names of the form .name to refer to variables defined in a sub-location .
With respect to the concrete syntax defined in the beginning of the section, the abstract syntax
does not provide arrays that are thus unrolled into their components. Thus, a variable bool[
Finally, an mrr system can be flattened by defining all its variable in its top-level locations with a
name referring to their paths within the nested structures. For instance, the variables in the model from
Figure 2 can be flattened as out[0], out[
The state of a flattened mrr system is a vector of integers indexed by its variables. For a state and a variable , we denote by [] the value of at state . From the declarations of these variables, several initial states may be defined. Our example, however, has a unique initial state.
Definition 2 (Operational semantics). .top.cons ∪ .top.rules is enabled if:
Let be a flattened mrr. From a state , an action ∈ • all the conditions in .left evaluate to true at ; • calling the state defined by applying onto all the assignments in .right, then we must have ≠ .
Firing in this situation is denoted by −→ , and we say that enables . Moreover, a system may perform time transitions from a state if: for every clock ∈ .clocks and every variable ∈ .top.vars such that .clock = and [] ≥ 0, then we must have [] < max(.dom); i n which case a new state is obtained by incrementing all the considered [] ≥ 0. This is denoted by →− just like actions firing.
An mrr system can generate a state-space that is defined as a graph (, ) where is the set of reachable states and is the set of transitions, defined inductively by: • includes the initial states defined in the model;
• for ∈ and a constraint such that →− , then we have ∈ and (, , ) ∈ ; • for ∈ that enables no constraints and a rule , if −→ , then we have ∈ and (, , ) ∈ ; • for ∈ that enables no constraints and a clock , if →− then we have ∈ and (, , ) ∈ ; • if ∈ enables no actions and no clock ticks, it is called a deadlock.
In this paper, we define (colored) Petri nets as in [ 20, Sec. 2.2], with respect to a set of variables V ranging on Z and a set of expressions E ⊃ V that includes all the arithmetic and Boolean expressions nest[0].R1
R1[i=0] 2/2 that mrr can express. Given ∈ E, we denote by vars() the subset of variables involved in . A binding of is a function vars() → Z that maps variables to values. Then, we denote by () the evaluation of under the binding , which may be a value in Z if the evaluation is possible, or an error value ⊥ if the evaluation is not possible for one reason or another.
Definition 3 (Petri nets).
A Petri net is a tuple (, , ℓ) where: • is the finite set of places; • , disjoint from , is the finite set of transitions; • ℓ is a labelling function such that: – for all ∈ , ℓ() ⊂ Z is the type of , – for all ∈ , ℓ() ∈ E is the guard of ; – for all (, ) ∈ ( × ) ∪ ( × ), ℓ(, ) is a multiset over E defining the arc from to , the empty multiset implementing to the absence of arc.
A marking of a Petri net (, , ℓ) is a function mapping each place to a multiset over ℓ(). A transition is enabled at a marking with a binding , which is denoted by [, ⟩ if: • has enough tokens: for all ∈ , (ℓ(, ))≤ (); • the guard is satisfied: (ℓ())is true; • place types are respected: for all ∈ , (ℓ(, ))is a multiset over ℓ().
If ∈ is enabled at with binding then it may fire yielding a new marking ′ such that for all ∈ , ′() = () − (ℓ(, ))+ (ℓ(, )). This is denoted by [, ⟩ ′. This allows defining the reachability graph (or marking graph) of a Petri net as usual, similarly to the state-space of an mrr system, by firing transitions from the initial marking until saturation.
• adding transitions priorities with two levels to implement constraints and rules: is partitioned into ∪ and the firing semantics is modified so that whenever [, ⟩ for ∈ then every ∈ is inhibited and cannot be enabled at ; • forbidding side-loops, i.e. no firing [, ⟩ being allowed; this can be enforced at the semantics level or side-loops can be removed from the marking graph afterward.
To translate a flattened mrr system into a Petri net, we first consider that it declares only variables such that .init is a singleton because Petri nets do not support having multiple initial marking. From this, we can have one reachability graph for each initial state of , and we can take their union to get a graph that matches the state-space of . Moreover, we assume a function ⌊⌉ that translate elements of an mrr structure into Petri nets variables or expressions: • for a variable structure , ⌊⌉ ∈ V is its translation into a Petri net variable; • for an mrr expression ( COND or EXPR ), ⌊⌉ ∈ E is a Petri net expression that implements ; • for a clock ∈ I, ⌊⌉ ∈ V is a Petri net variable that cannot be obtained as ⌊⌉ for any variable . For , , ∈ E, we shall use ternary if-then-else expressions as ⟦ ? ∶ ⟧ that evaluates to if is true and to otherwise.
Definition 4 (Petri nets semantics of mrr). Let be a flattened mrr system with a unique initial state. Its Petri net semantics is a Petri net (, , ℓ), with partitioned into ∪ , and marked with such that: • = { ∣ ∈ .top.vars} with – ℓ() = .dom, and – () = .init; • = { ∣ ∈ .top.cons} and = { ∣ ∈ .top.rules} ∪ { ∣ ∈ .clocks} with – for all ∈ .top.cons ∪ .top.rules, ℓ() = ⋀ ∈.left ⌊⌉, – for all ∈ .clocks, ℓ() is true; • for all ∈ , for all variable involved in , ℓ(, ) = {⌊⌉}and – ℓ(, ) = {⌊.value⌉}if .name = .target for some ∈ .right, – ℓ(, ) = {⌊⌉}, otherwise; • for every ∈ .clock and every variable such that .clock = : – ℓ(, ) = {⌊⌉}, and – ℓ(, ) = {⟦⌊⌉ ≥ 0 ? ⌊⌉ + 1 ∶ ⌊⌉⟧}; • every ℓ(, ) not listed above is the empty multiset (no arc).
As an example, Figure 5 shows the semantics of the mrr model from Figure 2.
Given how direct is the translation, it is easy to check that an mrr system and its Petri net semantics are strongly equivalent.
Claim 1. Let be a flattened mrr system with one initial state, and be its Petri nets semantics. Then, the state-space of is isomorphic to the marking graph on .
⇋ + 1
> 1 1 ⇋ − 1 out[]
0 ⇋ − 1
> 0 0 ⇋ + 1
5 nest[].in ⇋ −1 ⇋ 0 nest[].time ⇋ 0 −1 2 = 1 ⇋ ⟦ ≥ 0 ? + 1 ∶ ⟧
tick ⇋ + 1
eden is equipped with the tool ecco [
The mrr language has been implemented within ecco [
To illustrate how ecco can be used with an mrr model, we present a new version of the termites colony
model originally presented in [
The two last rules are directly adapted from [
A Jupyter session for this illustration is displayed in Figure 7. To analyze this model, we first load it
into ecco (In[
The resulting component graph is saved into variable g and then displayed.
It has 6 components, within ecco, we can click them and explore their characteristics, which shows that #1 has a unique state that is the initial state (which is visible from tag ▶ that tells us this component is exactly the set of initial states). From #1, firing rule R1 lead to #10, from which the termites may be killed either by the ants (rule R3 ) or by failing to build a nest (rule nest[0].R11 ). In both cases, this leads to #7 that is tagged by which means it contains deadlocks. Another path from #10 is to fire nest[0].R5 leading to #9 where the system may stay forever. Indeed, tag tells us that this component is the convex hull of some SCCs. From #9, termites may die (rules nest[].R11 ) or be killed by ants (rule R3 ). From #7 and #9, termites may kill ants (rule R4 ) which is surprising when starting from #7 because it is reached when termites die. But this can be explained looking at rule nest[].R11 where only reproductives and workers die, so that there may still be soldiers in the nests. They will die later on because of rule nest[].R9 but before they have a chance to kill the ants. Component #6 is tagged with •, which tells us that it is a SCC.
Cell In[
Finally, to clarify the dynamics related to the colonizing of new nests, cell In[
R4
R4
In[
In[
We shall not push further this analysis because it is already suficient to see that the spirit and
principles of ecco as presented in [
The rr modelling language has been developed on the basis of a theory of social-ecological systems
requiring to grasp their cores and inner structures. The rr syntax is summarizing the interaction
network of each system which we need to compute its qualitative and coarse-grain dynamics. Such a
long term system dynamics is conveniently modeled by a qualitative and abstract representation of the
system [
Extending a Boolean formalism to support multivalued variables is classical, for instance this was
made in [
Extending an untimed formalism to support time is also classical. In this work we have chosen causal
time and our extension is very similar to what was made in [
Extending a formalism with a representation of space is probably much less classical than with
multivalued variables or time, and spatial information is usually built-in from the beginning as a
prominent feature of a formalism. (See [
We presented the mrr language that is an extension of the existing rr language for the formal modelling of social-ecological systems. mrr extends rr in several ways: first, it adds multivalued variables, including statically-sized arrays; then, it adds time as clock ticks incrementing counters; finally, it adds spatial organization of the model as nested locations. The syntax of mrr has been presented and illustrated with examples, and its formal semantics has been defined in terms of rules operating on a lfattened version of a system ( i.e. with a unique location). Then, a colored Petri nets semantics of mrr has been provided, which is consistent with the operational semantics and opens the way for Petri net based analysis. Finally, we presented the implementation of mrr in ecco tool, and illustrated its usage on a concrete example adapted from our early works on rr.
As discussed above, extending rr to mrr leads to several sources of increased combinatorial explosion.
While this is interesting as an incentive to keep models abstract, it is sometimes desirable to introduce
more details when more data is available about the system being modelled. Multivaluated variables
are perhaps the least of our concerns because ecco is built on the top of data decision diagrams that
already deal eficiently with them. Introducing spaces is not specifically a source of combinatorial
explosion, but having arrays of locations is a way to quickly grow the size of a model. See for instance
our termites example with two nests that has 11,842 states when the same model with a unique nest
only has 110 states (and note that 1102 = 12,100 ≃ 11,842 which is consistent with the fact that two
nests evolve largely independently of one another). One future direction will be to consider hierarchical
data decision diagrams, called set decision diagrams, which are known to be an eficient way of factoring
the states of similar sub-systems into shared sub-diagrams [
Clocked variables introduced by the causal time approach are however more specific than multivalued
variables. For instance, in our first example from Figure 2, the intermediate counts between 0 and MAX-1
do not constrain the system. Only when one nest[].time reaches MAX the system is constrained and
animals are forced to go back to the nest before time can pass again. This is well known in timed systems
where only the constants that are compared to time measures are meaningful, which led to symbolic
representations of time-states such as zones [
Analyzing rr models is also possible using Petri nets unfoldings à la McMillan as in [
Last but not least, mrr has been created with the aim it will be used by ecologists and other environmental scientists (e.g. sociologists or economists), to conduct studies on social-ecological systems, just like rr has been already, either from a theoretical or from a practical perspective. Next steps in this direction will be to work with ecologists in order to help them become familiar with this new language and the changes it led to make in ecco. In this perspective, having mrr be an extension of rr will certainly help and allow a progressive transition from one language to another.
We warmly thank Sergiu Ivanov for our fruitful discussions about membrane systems formalisms, which helped a lot to design a suitable representation of space in mrr.