Skip to content

tutorial0.md

Latest commit

 

History

History
318 lines (231 loc) · 11.9 KB

tutorial0.md

File metadata and controls

318 lines (231 loc) · 11.9 KB

Ecofolder features and tools tutorial

The next tutorial is conceived as a starting point to use all the features included in Ecofolder and postprocessing of the computed prefix.

Table of Contents

Features

In this tutorial, we will use a toy model of a termites colony:

Inhabitants:

  • Rp: reproductives
  • Wk: workers
  • Sd: soldiers
  • Te: termitomyces

Structures:

  • Ec: egg chambers
  • fg: fungal gardens

Resources:

  • Wd: wood

Competitors:

  • Ac: ant competitors

The rules governing this little ecosystem are:

r1. Rp+ >> Ec+, Rp+
r2. Rp+, Ec+ >> Wk+, Rp+, Ec+
r3. Wk+ >> Wd+, Te+, Fg+, Ec+, Wk+
r4. Wk+, Wd+ >> Sd+, Rp+, Wk+, Wd+
r5. Wk+, Te+ >> Wd-, Wk+, Te+
r6. Wd- >> Wk-, Te-, Wd-
r7. Wk- >> Fg-, Sd-, Te-, Wk-
r8. Wk-, Rp- >> Ec-, Wk-, Rp-
r9. Ac+, Sd- >> Wk-, Rp-, Ac+, Sd-

In a few words, workers are responsible for creating wood, termitomyces, fungal gardens and egg chambers (r3). Reproductives also create egg chambers (r1), and both groups produce workers (r2). Workers and wood produce soldiers and reproductives (r4). From r5 onwards, there begins to be consumption of resources, reduction of inhabitants, and destruction of structures. Thus, once ants are present and soldiers are absent, there is no return to ecosystem stabilization because workers will be annihilated, and so will reproductives (r9).

In examples/termites/tutorial folder you will find termites.ll_net and termites_pr.ll_net files. Both files correspond to the aforementioned example, the second one is after applying the place-replication encoding (see Efficient unfolding of contextual Petri nets)

Displaying nets

You can visualize both nets with the next command (use ecofolder as parent folder):

Original net: ./shownet examples/termites/tutorial/termites

After PR-encoding (./prencoding examples/termites/tutorial/termites.ll_net) ./shownet examples/termites/tutorial/termites_pr

Where blue arcs represent read arcs (see Efficient unfolding of contextual Petri nets)

Unfolding nets

Let's unfold the termites example (termites_pr.ll_net). The reason why we use the example after the place-replication encoding is because we need to represent the dynamics of a contextual-reset net in an ordinary occurrence net through an unfolding procedure that accounts for read (and reset) arcs (see Ecosystem causal analysis using Petri net unfoldings).

./src/ecofolder examples/termites/tutorial/termites_pr.ll_net
./src/mci2dot examples/termites/tutorial/termites_pr_unf.mci > examples/termites/tutorial/termites_pr_unf.dot
dot -T pdf examples/termites/tutorial/termites_pr_unf.dot > examples/termites/tutorial/termites_pr_unf.pdf
evince examples/termites/tutorial/termites_pr_unf.pdf

Or you can collate the four commands and run the script:

./ecofold examples/termites/tutorial/termites_pr

The ouput will display a big prefix of the unfolding which is stopped by a cutoff criterion, here we refer as the Esparza criterion (see An improvement of McMillan's unfolding algorithm). However, you can also run with another one, which we refer as the McMillan criterion (see Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits).

./src/ecofolder -mcmillan examples/termites/tutorial/termites_pr.ll_net

Compressing or merging conditions in the prefix

All of the prefixes generated so far are big enough that makes it difficult to see in detail. One can try to merge conditions (circles) according to their pre- postsets. The next commands achieve a more compact view:

./src/ecofolder -c examples/termites/tutorial/termites_pr.ll_net
./src/mci2dot_cpr examples/termites/tutorial/termites_pr_unf.mci > examples/termites/tutorial/termites_pr_unf.dot
dot -T pdf examples/termites/tutorial/termites_pr_unf.dot > examples/termites/tutorial/termites_pr_unf.pdf
evince examples/termites/tutorial/termites_pr_unf.pdf

Stopping unfolding process

You can also decide where to stop the unfolding process before all cutoff events have truncated all branching processes either by:

  1. Stopping when a transition is inserted, for instance:
./src/ecofolder -T "R5" examples/termites/tutorial/termites_pr.ll_net
./src/mci2dot examples/termites/tutorial/termites_pr_unf.mci > examples/termites/tutorial/termites_pr_unf.dot
dot ...
evince ...
  1. Or halting according to a certain depth, with respect to the number of times a triple of cond-event (first level) (cond-event (second level), cond-event (third level), and so forth) has been added.
./src/ecofolder -d 5 examples/termites/tutorial/termites_pr.ll_net
./src/mci2dot examples/termites/tutorial/termites_pr_unf.mci > examples/termites/tutorial/termites_pr_unf.dot
dot ...
evince ...

Interactive and maximal configurations mode

If one want to manipulate the unfolding process and see how it goes step by step, an interactive mode can be enabled:

./src/ecofolder -i examples/termites/tutorial/termites_pr.ll_net
./src/mci2dot ...
dot ...
evince ...

Moreover, one can enable a mode where an individual branching process is unfolded until it's stopped by a cutoff event (note that in this case both Esparza and McMillan criteria produce the same output since we only consider a branching process and not all). In other words, we unfold until we find a marking already visited (or a loop 🙂).

./src/ecofolder -confmax examples/termites/tutorial/termites_pr.ll_net
./src/mci2dot ...
dot ...
evince ...

Querying markings in the prefix

One can also query a marking that appear in the prefix to be highlighted. The marking must have been used in the cutoff procedure to be found, otherwise it will not be highlighted (note that it's not a reachability check).

Say that we want to highlight this marking:

Ac+,Ec-,Fg-,Rp-,Sd-,Te-,Wd+,Wk-

So we proceed as follows (-q is to add a marking to be queried and -r is to say that we want to highlight certain instance, eg. -r 1 is the first instance, and -r 0 is to highlight all instances):

./src/ecofolder -q Ac+,Ec-,Fg-,Rp-,Sd-,Te-,Wd+,Wk- examples/termites/tutorial/termites_pr.ll_net
./src/mci2dot -r 0 examples/termites/tutorial/termites_pr_unf.mci > examples/termites/tutorial/termites_pr_unf.dot
dot ...
evince ...

Restricting places and blocking transitions

One can restrict a place to appear (say you don't want a place to be used, i.e. to receive tokens):

./src/ecofolder -rst Wd-,Wk- examples/termites/tutorial/termites_pr.ll_net
./src/mci2dot examples/termites/tutorial/termites_pr_unf.mci > examples/termites/tutorial/termites_pr_unf.dot
dot ...
evince ...

In this case, the absence of wood and workers cannot have tokens, so only rules (or transitions) that do not put tokens in those places can be used. Similarly, one can block transitions to be fired:

./src/ecofolder -blc R1,R2,R3,R4,R5 examples/termites/tutorial/termites_pr.ll_net
./src/mci2dot examples/termites/tutorial/termites_pr_unf.mci > examples/termites/tutorial/termites_pr_unf.dot
dot ...
evince ...

Event structure extraction

One can extract an event structure from a prefix. An event structure is basically a graph with only a type of node where conditions have been removed and events are interconnected. Since conditions are not present, we need to consider conflicts, and they are represented with dashed lines in the output. The next commands allow you to extract an event structure:

./src/ecofolder examples/termites/tutorial/termites_pr.ll_net
./src/mci2dot_ev examples/termites/tutorial/termites_pr_unf.mci > examples/termites/tutorial/termites_pr_unf.dot
dot ...
evince ...

Export to CSV format

One can export the prefix structure to be expressed in comma-separated values as follows:

./src/mci2csv examples/termites/tutorial/termites_pr_unf.mci

This command will output two files: termites_pr_unf_nodes.csv and termites_pr_unf_ends.csv.

termites_pr_unf_nodes.csv

A file formatted with five columns containing the node id, its type, its name or label, number of tokens (if any) and whether the node is a cutoff event (empty field for conditions). For example:

id,type,name,tokens,cutoff
"c1","condition","Wk-_2","0",
"c2","condition","Rp+_2","0",
"c3","condition","Wd+","0",
"e21","event","R6",,"0"
"e22","event","R2",,"0"
"e23","event","R9",,"1"

termites_pr_unf_ends.csv

A file formatted with three columns containing edge type, id node source and id node destination. For example:

type,src,dst
"edge","c1","e11"
"edge","c1","e60"
"edge","c1","e8"
"edge","c1","e7"
"edge","e68","c45"
"edge","e68","c46"
"edge","e3","c47"
"edge","c47","e11"
"edge","c47","e60"

Alternatively, one can generate a CSV file in case conditions are merged (compressed) in .mci file. The next command achieves that:

./src/mci2csv -c examples/termites/tutorial/termites_pr_unf.mci

Which will generate the same files as before but changing some fields in termites_pr_unf_nodes.csv when conditions are packed in the same entry. For example,

id,type,name,tokens,cutoff
"c1,c2","condition","Wk-_1,Wk-_2","0,0",
"c3,c4","condition","Rp+_1,Rp+_2","0,0",
"c5","condition","Wd+","0",
"c6,c7","condition","Fg-,Fg+","1,0",
"c175,c176,c177","condition","Fg+,Sd+,Fg-","0,0,1",
"e1","event","R3",,"0"
"e2","event","R6",,"0"
"e3","event","R4",,"0"
"e4","event","R5",,"0"

The output with multiple conditions on the same line should be interpreted as follows: each condition feature is listed in the order they appear, e.g., "c1,c2","condition","Wk-_1,Wk-_2","0,0",. The label for c1 is Wk-_1 and it has 0 tokens. Both nodes are of condition type.

In addition, CSV files can be generated from an event structure created by mci2dot_ev module, the following command do this task from a .mci file (note that the prefix saved as binary in mci has to be generated without merging conditions, so do not use c option):

./src/ecofolder examples/termites/tutorial/termites_pr.ll_net
./src/mci2dot_ev -csv examples/termites/tutorial/termites_pr_unf.mci

The command creates the two files, but with a slight modification to include conflicts but no conditions:

termites_pr_unf_nodes.csv

id,type,name,tokens,cutoff
"e20","event","R5",,"0"
"e21","event","R6",,"0"
"e22","event","R2",,"0"
"e23","event","R9",,"1"
"e24","event","R6",,"1"
"e25","event","R3",,"1"

termites_pr_unf_ends.csv

type,src,dst
"edge","e1","e3"
"edge","e1","e4"
"edge","e1","e5"
"edge","e0","e2"
"edge","e0","e68"
"conflict","e1","e2"
"conflict","e1","e68"
"conflict","e2","e68"

Contact

If you find bugs or issues while running this tutorial or any other example, feel free to contact me via email:

(λx.λy.λz. x@y.z) giannkas1 gmail com hint