EpiM is a sofware package devoloped for computing execution spaces of π-calculus processes. It is build upon the general graph transformation framework in MØD.
The software is implemented in Python 3, but utilizes the core of MØD, which is implemented in C++, for the computation of execution spaces. The package also includes a large visualisation module that makes it possible to visualise (recursive) processes and their execution spaces. Examples of how to use the interface of EpiM can be found below, and they can be explored interactively in the live playground below.
This page accompanies the paper
We provide access to a server with an EpiM installation, for illustrating the examples. When it is online an editor and a read-only terminal will appear in the frame below. The Python snippets from the example section can be loaded into the editor and edited at will.
To run the code in the editor, press the Run button. You can abort your run with the Kill button. After a successful run, a summary link will appear where you can access a PDF with the figures you have printed. During the run the terminal on the right will show the exact output of running your script, meaning any print calls will show up there.
Note If the frame below is empty the playground server is temporarily offline.
These examples shows the basic usage of EpiM. After each run a PDF summary is compiled. We let in(x) and out(x) denote the input and output operators of a process respectively.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
from process import Process, names
#MOD print options
printer = GraphPrinter()
# Specify the names to be used:
x, y, z, w = names("x y z w")
# Specify the behavior of a process
p1 = Process().input(x, z).output(z, w)
p2 = Process().output(x, y)
P = p1 | p2
# Encode the process as a MOD graph:
G = P.encode()
# Put a visualisation of the encoding in the summary:
G.print(printer)
We can restrict names of a process.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
from process import Process, names
#MOD print options
printer = GraphPrinter()
# Specify the names to be used:
x, y, z, w = names("x y z w")
# Specify the behavior of a process
p1 = Process().input(x, z).output(z, w)
p2 = Process().restrict(x).output(x, y)
P = p1 | p2
# Encode the process as a MOD graph:
G = P.encode()
# Put a visualisation of the encoding in the summary:
G.print(printer)
We can also specify process calls in an encoding.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
from process import Process, names
#MOD print options
printer = GraphPrinter()
# Specify the names to be used:
x, y = names("x y")
# Specify the behavior of a process
# Note, the second argument to call() is
# the arguments passed to the recursive invocation of "A".
A = Process().input(x, y).call("A", [x])
# Encode A and put a visualisation of the encoding in the summary:
A.encode().print(printer)
The graphs of the encoded processes can be filtered and “prettified” using either the print options used by MOD for graph visualization or the image config provided by EpiM.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
from gen_image import image_config
from process import Process, names
# Show the names of a process encoding:
image_config.show_variables = True
# Show the pointer vertices used for encoding process calls:
image_config.show_pointers = True
# Show the special root vertex "go" of an encoding:
image_config.show_root = True
# Hide implementation detail specific vertices such as
# the vertices with terms t(p) or t(s) with degrees of 2:
image_config.collapse_two_edges = False
#MOD print options
printer = GraphPrinter()
# Specify the names to be used:
x, y, z, w = names("x y z w")
# Specify the behavior of a process:
p1 = Process().input(x, z).output(z, w)
p2 = Process().output(x, y)
P = p1 | p2
# Encode and print P
G = P.encode()
G.print(printer)
We can compute the execution space of a process.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
from transform.reduction_dg import ReductionDG
from process import Process, names
# Specify the names to be used:
x, y, z, w = names("x y z w")
# Specify the behavior of a process:
p1 = Process().input(x, z).output(z, w)
p2 = Process().output(x, y) + Process().output(x, y)
P = (p1 | p2)
# Compute the execution space for P
exec_space = ReductionDG(P)
exec_space.calc()
# Print the resulting derivation graph to the summary PDF:
exec_space.print()
# exec_space.print(True) #prints the entire derivation graph
We can compute the execution space of processes defined with recursive processes.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
from transform.reduction_dg import ReductionDG
from process import Process, names
from recursive_process import RecursiveProcess
# Specify the names to be used:
x, y, z = names("x y z")
# Define a recursive process:
rp = RecursiveProcess()
# Specify the name, arguments, and behavior of a recursive process:
A = Process().input(x, y).call("A", [y])
rp.add("A", [x], A)
B = Process().output(x, x).call("B", [x])
rp.add("B", [x], B)
# Specify the behavior of a process:
P = A | B
# Compute the execution space for P provided with the recursive process rp:
exec_space = ReductionDG(P, rp)
exec_space.calc()
# Print the resulting derivation graph to the summary PDF:
exec_space.print()
The execution space for the process Hospital. From the execution space, we see that Hospital can end up in a deadlock. This happens specifically, when the process P synchronizes with the process H.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
from process import Process, names, Name, process_config
from transform.reduction_dg import ReductionDG
from recursive_process import RecursiveProcess
# Do not print the arguments of an encoded process call:
process_config.print_args = False
# Specify the names to be used:
s, n, pn, j, h, cu, ki, d, x = names("s n pn j h cu ki d x")
free_names = [s, n, ki, cu]
# Define a recursive process:
rp = RecursiveProcess()
# Specify the name, arguments, and behavior of a recursive process:
P = Process().output(s, n).input(n, d).call("Pp", free_names)
rp.add("P", free_names, P)
Pp = Process().input(ki, x) + Process().input(cu, x).call("P", free_names)
rp.add("Pp", free_names, Pp)
J = Process().input(s, pn).output(pn, j).output(cu, j).call("J", free_names)
rp.add("J", free_names, J)
H = Process().input(s, pn).output(pn, h).output(ki, h).call("H", free_names)
rp.add("H", free_names, H)
# Define the process Hospital:
Hospital = P | J | H
# Compute the execution space of Hospital given the recursive process rp:
exec_space = ReductionDG(Hospital, rp)
exec_space.calc()
# Print the resulting derivation graph to the summary PDF:
exec_space.print()