From ad8836bfa7f1d418841ebcf9b2980eee78f05476 Mon Sep 17 00:00:00 2001
From: Ivan Lanese <ivan.lanese@gmail.com>
Date: Thu, 18 Apr 2024 14:41:18 +0200
Subject: [PATCH] Added cauder case studies (to test.py as well)

---
 examples/airline/agent_1_local_view.dot       |  2 +-
 examples/airline/main_0_global_view.dot       | 33 ++++---
 examples/airline/main_0_local_view.dot        |  2 +-
 examples/async/main_0_global_view.dot         |  6 +-
 examples/cauder_suite/airline/airline.erl     | 31 +++++++
 examples/cauder_suite/barber/barber.erl       | 73 ++++++++++++++++
 .../cauder_suite/barber/main_0_local_view.dot | 19 ++++
 .../cauder_suite/meViolation/meViolation.erl  | 40 +++++++++
 examples/cauder_suite/purchase/purchase.erl   | 47 ++++++++++
 .../conditional-case/dummy_1_local_view.dot   |  2 +-
 .../conditional-case/main_0_global_view.dot   | 14 +--
 .../conditional-case/main_0_local_view.dot    |  8 +-
 examples/customer/customer_0_local_view.dot   |  2 +-
 .../customer/customer_dummy_0_local_view.dot  |  6 +-
 examples/customer/main_0_global_view.dot      |  8 +-
 examples/customer/store_0_local_view.dot      |  2 +-
 .../for-loop-recursion/main_0_global_view.dot |  6 +-
 .../for-loop-recursion/main_0_local_view.dot  |  4 +-
 examples/function-call/main_0_global_view.dot |  2 +-
 examples/hello/greet_0_local_view.dot         |  4 +-
 .../high-order-fun/greet_0_global_view.dot    | 23 ++---
 .../high-order-fun/greet_0_local_view.dot     |  4 +-
 examples/if-cases/a_0_local_view.dot          |  2 +-
 examples/if-cases/b_0_local_view.dot          |  2 +-
 examples/if-cases/c_0_local_view.dot          |  2 +-
 examples/if-cases/main_0_global_view.dot      | 42 ++++-----
 examples/if-cases/main_0_local_view.dot       | 10 +--
 examples/serverclient/client_0_local_view.dot |  4 +-
 .../serverclient/handle_req_1_local_view.dot  |  2 +-
 examples/serverclient/main_0_global_view.dot  |  8 +-
 examples/serverclient/main_0_local_view.dot   |  2 +-
 examples/serverclient/server_0_local_view.dot |  4 +-
 examples/test/barber/test_0_local_view.dot    |  6 +-
 examples/test/foo1/test_0_global_view.dot     |  6 +-
 examples/test/foo1/test_0_local_view.dot      |  4 +-
 examples/test/foo2/b_0_local_view.dot         |  2 +-
 examples/test/foo2/c_0_local_view.dot         |  2 +-
 examples/test/foo2/test_0_global_view.dot     |  2 +-
 examples/test/foo2/test_0_local_view.dot      |  2 +-
 examples/test/foo3/a_1_local_view.dot         |  2 +-
 examples/test/foo3/test_0_global_view.dot     | 14 +--
 examples/test/foo3/test_0_local_view.dot      |  6 +-
 examples/test/foo4/test_0_global_view.dot     | 14 +--
 examples/test/foo4/test_0_local_view.dot      |  4 +-
 examples/test/foo5/target_0_local_view.dot    |  2 +-
 examples/test/foo5/test_0_global_view.dot     |  6 +-
 examples/test/foo5/test_0_local_view.dot      |  8 +-
 examples/test/foo6/test_0_global_view.dot     |  6 +-
 examples/test/foo6/test_0_local_view.dot      |  2 +-
 examples/test/ping/pong_0_local_view.dot      |  2 +-
 examples/test/ping/start_0_local_view.dot     |  4 +-
 examples/ticktackloop/start_0_global_view.dot |  2 +-
 examples/ticktackloop/start_0_local_view.dot  |  2 +-
 .../ticktackloop/tac_loop_0_local_view.dot    |  4 +-
 .../ticktackloop/tic_loop_0_local_view.dot    |  2 +-
 examples/ticktackstop/start_0_global_view.dot | 20 ++---
 examples/ticktackstop/start_0_local_view.dot  |  4 +-
 .../ticktackstop/tac_loop_0_local_view.dot    |  6 +-
 .../ticktackstop/tic_loop_0_local_view.dot    |  4 +-
 examples/trick/a_0_local_view.dot             |  2 +-
 examples/trick/b_0_local_view.dot             |  2 +-
 examples/trick/c_0_local_view.dot             |  2 +-
 examples/trick/main_0_global_view.dot         | 10 +--
 examples/trick/main_0_local_view.dot          |  2 +-
 .../violation/incrementer_0_local_view.dot    |  6 +-
 examples/violation/main_0_global_view.dot     | 86 +++++++++----------
 examples/violation/main_0_local_view.dot      |  4 +-
 examples/violation/meManager_0_local_view.dot |  2 +-
 .../violation/varManager_1_local_view.dot     |  2 +-
 test.py                                       |  4 +
 70 files changed, 444 insertions(+), 232 deletions(-)
 create mode 100755 examples/cauder_suite/airline/airline.erl
 create mode 100644 examples/cauder_suite/barber/barber.erl
 create mode 100644 examples/cauder_suite/barber/main_0_local_view.dot
 create mode 100755 examples/cauder_suite/meViolation/meViolation.erl
 create mode 100755 examples/cauder_suite/purchase/purchase.erl

diff --git a/examples/airline/agent_1_local_view.dot b/examples/airline/agent_1_local_view.dot
index 45fbbd4..a54322f 100644
--- a/examples/airline/agent_1_local_view.dot
+++ b/examples/airline/agent_1_local_view.dot
@@ -5,6 +5,6 @@ digraph agent_1 {
 	n_0 -> n_1 [arrowhead=none];
 	n_2 [id="2", shape=circle, label="2"];
 
-	n_2 -> n_1 [id="[$e|3]", label="receive {booked,_}"];
 	n_1 -> n_2 [id="[$e|0]", label="send {sell,pid_self} to Pid2"];
+	n_2 -> n_1 [id="[$e|3]", label="receive {booked,_}"];
 }
diff --git a/examples/airline/main_0_global_view.dot b/examples/airline/main_0_global_view.dot
index 8284287..2bd2383 100644
--- a/examples/airline/main_0_global_view.dot
+++ b/examples/airline/main_0_global_view.dot
@@ -2,23 +2,20 @@ digraph global {
 	rankdir="LR";
 	n_0 [label="global", shape="plaintext"];
 	n_1 [id="5", shape=circle, label="5"];
-	n_2 [id="6", shape=circle, label="6"];
-	n_3 [id="1", shape=circle, label="1"];
-	n_0 -> n_3 [arrowhead=none];
-	n_4 [id="2", shape=circle, label="2"];
-	n_5 [id="4", shape=circle, label="4"];
-	n_6 [id="3", shape=circle, label="3"];
+	n_2 [id="1", shape=circle, label="1"];
+	n_0 -> n_2 [arrowhead=none];
+	n_3 [id="2", shape=circle, label="2"];
+	n_4 [id="4", shape=circle, label="4"];
+	n_5 [id="3", shape=circle, label="3"];
 
-	n_2 -> n_5 [id="[$e|11]", label="agent/1.1→main/0.0:{sell,pid_self}"];
-	n_2 -> n_5 [id="[$e|10]", label="agent/1.0→main/0.0:{sell,pid_self}"];
-	n_5 -> n_2 [id="[$e|7]", label="main/0.0→agent/1.1:{booked,Num}"];
-	n_6 -> n_5 [id="[$e|2]", label="agent/1.0→main/0.0:{sell,pid_self}"];
-	n_6 -> n_5 [id="[$e|3]", label="agent/1.1→main/0.0:{sell,pid_self}"];
-	n_5 -> n_1 [id="[$e|5]", label="main/0.0→agent/1.0:{booked,Num}"];
-	n_5 -> n_5 [id="[$e|6]", label="agent/1.0→main/0.0:{sell,pid_self}"];
-	n_4 -> n_6 [id="[$e|1]", label="main/0.0Δagent/1.1"];
-	n_1 -> n_5 [id="[$e|9]", label="agent/1.0→main/0.0:{sell,pid_self}"];
-	n_3 -> n_4 [id="[$e|0]", label="main/0.0Δagent/1.0"];
-	n_5 -> n_5 [id="[$e|4]", label="agent/1.1→main/0.0:{sell,pid_self}"];
-	n_1 -> n_5 [id="[$e|8]", label="agent/1.1→main/0.0:{sell,pid_self}"];
+	n_1 -> n_4 [id="[$e|8]", label="agent/1.1→main/0.0:{sell,pid_self}"];
+	n_4 -> n_5 [id="[$e|6]", label="main/0.0→agent/1.1:{booked,Num}"];
+	n_4 -> n_4 [id="[$e|5]", label="agent/1.1→main/0.0:{sell,pid_self}"];
+	n_4 -> n_1 [id="[$e|4]", label="main/0.0→agent/1.0:{booked,Num}"];
+	n_4 -> n_4 [id="[$e|7]", label="agent/1.0→main/0.0:{sell,pid_self}"];
+	n_3 -> n_5 [id="[$e|1]", label="main/0.0Δagent/1.1"];
+	n_1 -> n_4 [id="[$e|9]", label="agent/1.0→main/0.0:{sell,pid_self}"];
+	n_2 -> n_3 [id="[$e|0]", label="main/0.0Δagent/1.0"];
+	n_5 -> n_4 [id="[$e|3]", label="agent/1.1→main/0.0:{sell,pid_self}"];
+	n_5 -> n_4 [id="[$e|2]", label="agent/1.0→main/0.0:{sell,pid_self}"];
 }
diff --git a/examples/airline/main_0_local_view.dot b/examples/airline/main_0_local_view.dot
index 9d23e06..e659f4a 100644
--- a/examples/airline/main_0_local_view.dot
+++ b/examples/airline/main_0_local_view.dot
@@ -7,8 +7,8 @@ digraph main_0 {
 	n_3 [id="2", shape=doublecircle, label="3"];
 	n_4 [id="3", shape=circle, label="2"];
 
-	n_4 -> n_3 [id="[$e|2]", label="spawn agent/1.1"];
 	n_1 -> n_3 [id="[$e|5]", label="send {booked,Num} to Pid1"];
 	n_2 -> n_4 [id="[$e|1]", label="spawn agent/1.0"];
 	n_3 -> n_1 [id="[$e|0]", label="receive {sell,Pid1}"];
+	n_4 -> n_3 [id="[$e|2]", label="spawn agent/1.1"];
 }
diff --git a/examples/async/main_0_global_view.dot b/examples/async/main_0_global_view.dot
index f1621bd..698323f 100644
--- a/examples/async/main_0_global_view.dot
+++ b/examples/async/main_0_global_view.dot
@@ -9,10 +9,10 @@ digraph global {
 	n_5 [id="4", shape=circle, label="4"];
 	n_6 [id="3", shape=circle, label="3"];
 
-	n_6 -> n_5 [id="[$e|2]", label="dummy2/0.0→dummy1/0.0:ciao"];
-	n_6 -> n_1 [id="[$e|3]", label="dummy1/0.0→dummy2/0.0:bello"];
 	n_1 -> n_2 [id="[$e|5]", label="dummy2/0.0→dummy1/0.0:ciao"];
+	n_5 -> n_2 [id="[$e|4]", label="dummy1/0.0→dummy2/0.0:bello"];
 	n_4 -> n_6 [id="[$e|1]", label="main/0.0Δdummy2/0.0"];
 	n_3 -> n_4 [id="[$e|0]", label="main/0.0Δdummy1/0.0"];
-	n_5 -> n_2 [id="[$e|4]", label="dummy1/0.0→dummy2/0.0:bello"];
+	n_6 -> n_1 [id="[$e|3]", label="dummy1/0.0→dummy2/0.0:bello"];
+	n_6 -> n_5 [id="[$e|2]", label="dummy2/0.0→dummy1/0.0:ciao"];
 }
diff --git a/examples/cauder_suite/airline/airline.erl b/examples/cauder_suite/airline/airline.erl
new file mode 100755
index 0000000..a0e4a04
--- /dev/null
+++ b/examples/cauder_suite/airline/airline.erl
@@ -0,0 +1,31 @@
+-module(airline).
+-export([main/0, agent/2]).
+
+main() ->
+    Main = self(),
+    spawn(?MODULE, agent, [1, Main]),
+    spawn(?MODULE, agent, [2, Main]),
+    seats(3).
+
+seats(Num) ->
+    receive
+        {numOfSeats, Pid} ->
+            Pid ! {seats, Num},
+            seats(Num);
+        {sell, Pid} ->
+            io:format("Seat sold!~n"),
+            Pid ! {booked, Num},
+            seats(Num - 1)
+    end.
+
+agent(NAg, Pid) ->
+    Pid ! {numOfSeats, self()},
+    receive
+        {seats, Num} when Num > 0 ->
+            Pid ! {sell, self()},
+            receive
+                {booked, _} -> agent(NAg, Pid)
+            end;
+        _ ->
+            io:format("Agent~p done!~n", [NAg])
+    end.
diff --git a/examples/cauder_suite/barber/barber.erl b/examples/cauder_suite/barber/barber.erl
new file mode 100644
index 0000000..e9e2508
--- /dev/null
+++ b/examples/cauder_suite/barber/barber.erl
@@ -0,0 +1,73 @@
+% sleeping barber problem (with a bug)
+
+-module(barber).
+-export([main/0, open_barber_shop/0, barber/1, customer/3]).
+
+main() ->
+    io:format("~nCustomers: John and Joe~n~n"),
+    ShopPid = spawn(?MODULE, open_barber_shop, []),
+    spawn(?MODULE, customer, [ShopPid, 'John', self()]),
+    spawn(?MODULE, customer, [ShopPid, 'Joe', self()]),
+    receive
+        {Name1, State1} -> io:format("~p ~p~n", [Name1, State1])
+    end,
+    receive
+        {Name2, State2} -> io:format("~p ~p~n", [Name2, State2])
+    end,
+    ShopPid ! stop.
+
+%%customer
+customer(ShopPid, Name, MainPid) ->
+    ShopPid ! {new, {self(), Name}},
+    receive
+        X -> MainPid ! {Name, X}
+    end.
+
+%% barber %%
+barber(ShopPid) ->
+    ShopPid ! ready,
+    receive
+        wakeup ->
+            barber(ShopPid);
+        {customer, Customer} ->
+            ShopPid ! {cut, Customer},
+            barber(ShopPid)
+    end.
+
+%% shop %%
+open_barber_shop() ->
+    BarberPid = spawn(?MODULE, barber, [self()]),
+    barber_shop(BarberPid, []).
+
+%% main loop
+barber_shop(BarberPid, CustomersInChairs) ->
+    receive
+        {cut, {CustomerPid, _}} ->
+            CustomerPid ! finished,
+            barber_shop(BarberPid, CustomersInChairs);
+        ready ->
+            respond_to_barber(BarberPid, CustomersInChairs);
+        {new, CustomerInfo} ->
+            add_customer_if_available(BarberPid, CustomerInfo, CustomersInChairs);
+        stop ->
+            stop
+    end.
+
+respond_to_barber(BarberPid, []) ->
+    barber_shop(BarberPid, []);
+respond_to_barber(BarberPid, List) ->
+    BarberPid ! {customer, last(List)},
+    barber_shop(BarberPid, removeCustomer(List)).
+
+% assuming 2 chairs
+add_customer_if_available(BarberPid, {CustomerPid, _CustomerName}, [X, Y | R]) ->
+    CustomerPid ! no_room,
+    barber_shop(BarberPid, [X, Y | R]);
+add_customer_if_available(BarberPid, {CustomerPid, CustomerName}, List) ->
+    BarberPid ! wakeup,
+    barber_shop(BarberPid, [{CustomerPid, CustomerName} | List]).
+
+last([A]) -> A;
+last([_A | R]) -> last(R).
+
+removeCustomer([_A | R]) -> R.
diff --git a/examples/cauder_suite/barber/main_0_local_view.dot b/examples/cauder_suite/barber/main_0_local_view.dot
new file mode 100644
index 0000000..c1a4155
--- /dev/null
+++ b/examples/cauder_suite/barber/main_0_local_view.dot
@@ -0,0 +1,19 @@
+digraph main_0 {
+	rankdir="LR";
+	n_0 [label="main_0", shape="plaintext"];
+	n_1 [id="5", shape=circle, label="5"];
+	n_2 [id="6", shape=circle, label="6"];
+	n_3 [id="1", shape=circle, label="1"];
+	n_0 -> n_3 [arrowhead=none];
+	n_4 [id="2", shape=circle, label="2"];
+	n_5 [id="4", shape=doublecircle, label="7"];
+	n_6 [id="7", shape=circle, label="3"];
+	n_7 [id="3", shape=circle, label="4"];
+
+	n_1 -> n_2 [id="[$e|5]", label="receive {Name2,State2}"];
+	n_4 -> n_6 [id="[$e|0]", label="spawn customer/3.0"];
+	n_2 -> n_5 [id="[$e|2]", label="send stop to open_barber_shop/0.0"];
+	n_6 -> n_7 [id="[$e|3]", label="spawn customer/3.1"];
+	n_7 -> n_1 [id="[$e|4]", label="receive {Name1,State1}"];
+	n_3 -> n_4 [id="[$e|1]", label="spawn open_barber_shop/0.0"];
+}
diff --git a/examples/cauder_suite/meViolation/meViolation.erl b/examples/cauder_suite/meViolation/meViolation.erl
new file mode 100755
index 0000000..5c7438d
--- /dev/null
+++ b/examples/cauder_suite/meViolation/meViolation.erl
@@ -0,0 +1,40 @@
+%code showing a mutual exclusion violation
+%the two concurrent increments of the variable managed by varManager
+%may lead to final value 1 instead of 2 under some schedulings
+
+-module(meViolation).
+-export([main/0, meManager/0, varManager/1, incrementer/2]).
+
+main() ->
+    MePid = spawn(?MODULE, meManager, []),
+    XPid = spawn(?MODULE, varManager, [0]),
+    spawn(?MODULE, incrementer, [MePid, XPid]),
+    spawn(?MODULE, incrementer, [MePid, XPid]).
+
+meManager() ->
+    receive
+        {request, Pid} -> Pid ! answer
+    end,
+    receive
+        {release} -> meManager()
+    end.
+
+varManager(Val) ->
+    io:format("Variable value:~b~n", [Val]),
+    receive
+        {write, NewVal} -> varManager(NewVal);
+        {read, Pid} -> Pid ! Val
+    end,
+    varManager(Val).
+
+incrementer(MePid, XPid) ->
+    MePid ! {request, self()},
+    receive
+        answer ->
+            XPid ! {read, self()},
+            receive
+                X ->
+                    XPid ! {write, X + 1},
+                    MePid ! {release}
+            end
+    end.
diff --git a/examples/cauder_suite/purchase/purchase.erl b/examples/cauder_suite/purchase/purchase.erl
new file mode 100755
index 0000000..1f7da4c
--- /dev/null
+++ b/examples/cauder_suite/purchase/purchase.erl
@@ -0,0 +1,47 @@
+%FASE 2014 example
+
+-module(purchase).
+-export([main/0, asynchAnd/2, checkCredit/2, checkAddress/1, checkItem/1]).
+
+main() ->
+    Pid = spawn(?MODULE, asynchAnd, [2, self()]),
+    spawn(?MODULE, checkCredit, [15, Pid]),
+    spawn(?MODULE, checkAddress, [Pid]),
+    spawn(?MODULE, checkItem, [Pid]),
+    receive
+        true ->
+            io:format("All checks successful.~n"),
+            true;
+        false ->
+            io:format("Check failure.~n"),
+            false
+    end.
+
+asynchAnd(N, Out) ->
+    if
+        N > 0 ->
+            receive
+                true -> asynchAnd(N - 1, Out);
+                false -> Out ! false
+            end;
+        true ->
+            Out ! true
+    end.
+
+checkCredit(Price, Pid) ->
+    if
+        Price < 10 ->
+            io:format("Credit check successful~n"),
+            Pid ! true;
+        true ->
+            io:format("Credit check failed~n"),
+            Pid ! false
+    end.
+
+checkAddress(Pid) ->
+    io:format("Address check successful~n"),
+    Pid ! true.
+
+checkItem(Pid) ->
+    io:format("Item check successful~n"),
+    Pid ! true.
diff --git a/examples/conditional-case/dummy_1_local_view.dot b/examples/conditional-case/dummy_1_local_view.dot
index 62e376e..f5817d7 100644
--- a/examples/conditional-case/dummy_1_local_view.dot
+++ b/examples/conditional-case/dummy_1_local_view.dot
@@ -6,6 +6,6 @@ digraph dummy_1 {
 	n_2 [id="2", shape=circle, label="2"];
 	n_3 [id="3", shape=doublecircle, label="3"];
 
-	n_2 -> n_3 [id="[$e|1]", label="receive Str"];
 	n_1 -> n_2 [id="[$e|0]", label="send {pid_self,integer} to Pid"];
+	n_2 -> n_3 [id="[$e|1]", label="receive Str"];
 }
diff --git a/examples/conditional-case/main_0_global_view.dot b/examples/conditional-case/main_0_global_view.dot
index 7b730b7..7b88835 100644
--- a/examples/conditional-case/main_0_global_view.dot
+++ b/examples/conditional-case/main_0_global_view.dot
@@ -12,15 +12,15 @@ digraph global {
 	n_8 [id="7", shape=circle, label="7"];
 	n_9 [id="3", shape=circle, label="3"];
 
-	n_2 -> n_4 [id="[$e|10]", label="main/0.0→dummy/1.2:'Ciao"];
-	n_2 -> n_6 [id="[$e|9]", label="main/0.0→dummy/1.1:'Ciao"];
-	n_2 -> n_8 [id="[$e|8]", label="main/0.0→dummy/1.0:'Ciao"];
-	n_1 -> n_2 [id="[$e|6]", label="dummy/1.2→main/0.0:{pid_self,integer}"];
 	n_7 -> n_1 [id="[$e|3]", label="main/0.0Δdummy/1.3"];
+	n_1 -> n_2 [id="[$e|6]", label="dummy/1.2→main/0.0:{pid_self,integer}"];
 	n_9 -> n_7 [id="[$e|2]", label="main/0.0Δdummy/1.2"];
-	n_1 -> n_2 [id="[$e|5]", label="dummy/1.1→main/0.0:{pid_self,integer}"];
+	n_2 -> n_8 [id="[$e|8]", label="main/0.0→dummy/1.0:'Ciao"];
+	n_3 -> n_5 [id="[$e|0]", label="main/0.0Δdummy/1.0"];
 	n_5 -> n_9 [id="[$e|1]", label="main/0.0Δdummy/1.1"];
-	n_1 -> n_2 [id="[$e|4]", label="dummy/1.0→main/0.0:{pid_self,integer}"];
 	n_1 -> n_2 [id="[$e|7]", label="dummy/1.3→main/0.0:{pid_self,integer}"];
-	n_3 -> n_5 [id="[$e|0]", label="main/0.0Δdummy/1.0"];
+	n_1 -> n_2 [id="[$e|4]", label="dummy/1.0→main/0.0:{pid_self,integer}"];
+	n_1 -> n_2 [id="[$e|5]", label="dummy/1.1→main/0.0:{pid_self,integer}"];
+	n_2 -> n_4 [id="[$e|10]", label="main/0.0→dummy/1.1:'Ciao"];
+	n_2 -> n_6 [id="[$e|9]", label="main/0.0→dummy/1.3:'Ciao"];
 }
diff --git a/examples/conditional-case/main_0_local_view.dot b/examples/conditional-case/main_0_local_view.dot
index 805f5f5..62a87d7 100644
--- a/examples/conditional-case/main_0_local_view.dot
+++ b/examples/conditional-case/main_0_local_view.dot
@@ -10,12 +10,12 @@ digraph main_0 {
 	n_6 [id="4", shape=circle, label="4"];
 	n_7 [id="3", shape=doublecircle, label="7"];
 
-	n_1 -> n_7 [id="[$e|10]", label="send 'Ciao C' to dummy/1.2"];
-	n_1 -> n_7 [id="[$e|9]", label="send 'Ciao B' to dummy/1.1"];
-	n_5 -> n_2 [id="[$e|8]", label="spawn dummy/1.1"];
 	n_1 -> n_7 [id="[$e|3]", label="send 'Ciao A' to dummy/1.0"];
 	n_6 -> n_4 [id="[$e|2]", label="spawn dummy/1.3"];
+	n_5 -> n_2 [id="[$e|8]", label="spawn dummy/1.1"];
+	n_3 -> n_5 [id="[$e|0]", label="spawn dummy/1.0"];
 	n_2 -> n_6 [id="[$e|1]", label="spawn dummy/1.2"];
 	n_4 -> n_1 [id="[$e|4]", label="receive {Process,_}"];
-	n_3 -> n_5 [id="[$e|0]", label="spawn dummy/1.0"];
+	n_1 -> n_7 [id="[$e|10]", label="send 'Ciao B' to dummy/1.1"];
+	n_1 -> n_7 [id="[$e|9]", label="send 'Ciao D' to dummy/1.3"];
 }
diff --git a/examples/customer/customer_0_local_view.dot b/examples/customer/customer_0_local_view.dot
index 480db9a..55a3cbb 100644
--- a/examples/customer/customer_0_local_view.dot
+++ b/examples/customer/customer_0_local_view.dot
@@ -10,8 +10,8 @@ digraph customer_0 {
 
 	n_1 -> n_3 [id="[$e|0]", label="send buy to store/0.0"];
 	n_1 -> n_2 [id="[$e|9]", label="send more to store/0.0"];
-	n_4 -> n_5 [id="[$e|5]", label="receive accepted"];
 	n_4 -> n_3 [id="[$e|8]", label="receive reject"];
+	n_4 -> n_5 [id="[$e|5]", label="receive accepted"];
 	n_3 -> n_4 [id="[$e|4]", label="send payment to store/0.0"];
 	n_2 -> n_1 [id="[$e|1]", label="send item to store/0.0"];
 }
diff --git a/examples/customer/customer_dummy_0_local_view.dot b/examples/customer/customer_dummy_0_local_view.dot
index f597cfb..0e10658 100644
--- a/examples/customer/customer_dummy_0_local_view.dot
+++ b/examples/customer/customer_dummy_0_local_view.dot
@@ -9,11 +9,11 @@ digraph customer_dummy_0 {
 	n_5 [id="8", shape=circle, label="3"];
 	n_6 [id="4", shape=doublecircle, label="6"];
 
+	n_5 -> n_4 [id="[$e|10]", label="send buy to store/0.0"];
+	n_2 -> n_4 [id="[$e|3]", label="receive reject"];
 	n_3 -> n_1 [id="[$e|0]", label="send ciao to store/0.0"];
 	n_5 -> n_1 [id="[$e|9]", label="send more to store/0.0"];
-	n_1 -> n_5 [id="[$e|5]", label="send item to store/0.0"];
-	n_2 -> n_4 [id="[$e|3]", label="receive reject"];
 	n_4 -> n_2 [id="[$e|8]", label="send payment to store/0.0"];
 	n_2 -> n_6 [id="[$e|2]", label="receive accepted"];
-	n_5 -> n_4 [id="[$e|10]", label="send buy to store/0.0"];
+	n_1 -> n_5 [id="[$e|5]", label="send item to store/0.0"];
 }
diff --git a/examples/customer/main_0_global_view.dot b/examples/customer/main_0_global_view.dot
index 69a33f5..003dd95 100644
--- a/examples/customer/main_0_global_view.dot
+++ b/examples/customer/main_0_global_view.dot
@@ -12,14 +12,14 @@ digraph global {
 	n_8 [id="7", shape=circle, label="7"];
 	n_9 [id="3", shape=circle, label="3"];
 
+	n_7 -> n_1 [id="[$e|3]", label="customer_dummy/0.0→store/0.0:buy"];
+	n_8 -> n_6 [id="[$e|7]", label="store/0.0→customer_dummy/0.0:accepted"];
 	n_3 -> n_5 [id="[$e|0]", label="main/0.0Δstore/0.0"];
 	n_4 -> n_8 [id="[$e|9]", label="customer_dummy/0.0→store/0.0:payment"];
-	n_1 -> n_8 [id="[$e|5]", label="customer_dummy/0.0→store/0.0:payment"];
-	n_7 -> n_1 [id="[$e|3]", label="customer_dummy/0.0→store/0.0:buy"];
 	n_8 -> n_4 [id="[$e|8]", label="store/0.0→customer_dummy/0.0:reject"];
-	n_2 -> n_7 [id="[$e|6]", label="customer_dummy/0.0→store/0.0:item"];
 	n_9 -> n_7 [id="[$e|2]", label="customer_dummy/0.0→store/0.0:item"];
-	n_8 -> n_6 [id="[$e|7]", label="store/0.0→customer_dummy/0.0:accepted"];
+	n_1 -> n_8 [id="[$e|5]", label="customer_dummy/0.0→store/0.0:payment"];
+	n_2 -> n_7 [id="[$e|6]", label="customer_dummy/0.0→store/0.0:item"];
 	n_7 -> n_2 [id="[$e|4]", label="customer_dummy/0.0→store/0.0:more"];
 	n_5 -> n_9 [id="[$e|1]", label="main/0.0Δcustomer_dummy/0.0"];
 }
diff --git a/examples/customer/store_0_local_view.dot b/examples/customer/store_0_local_view.dot
index 55eef7e..aee51c9 100644
--- a/examples/customer/store_0_local_view.dot
+++ b/examples/customer/store_0_local_view.dot
@@ -8,9 +8,9 @@ digraph store_0 {
 	n_4 [id="4", shape=circle, label="3"];
 	n_5 [id="3", shape=circle, label="2"];
 
+	n_3 -> n_1 [id="[$e|3]", label="send accepted to customer_dummy/0.0"];
 	n_4 -> n_3 [id="[$e|0]", label="receive payment"];
 	n_3 -> n_4 [id="[$e|9]", label="send reject to customer_dummy/0.0"];
-	n_3 -> n_1 [id="[$e|3]", label="send accepted to customer_dummy/0.0"];
 	n_5 -> n_2 [id="[$e|8]", label="receive more"];
 	n_2 -> n_5 [id="[$e|6]", label="receive item"];
 	n_5 -> n_4 [id="[$e|1]", label="receive buy"];
diff --git a/examples/for-loop-recursion/main_0_global_view.dot b/examples/for-loop-recursion/main_0_global_view.dot
index 5745757..2c12586 100644
--- a/examples/for-loop-recursion/main_0_global_view.dot
+++ b/examples/for-loop-recursion/main_0_global_view.dot
@@ -7,10 +7,10 @@ digraph global {
 	n_3 [id="4", shape=circle, label="4"];
 	n_4 [id="3", shape=circle, label="3"];
 
-	n_4 -> n_3 [id="[$e|3]", label="dummy/1.1→main/0.0:integer"];
-	n_3 -> n_3 [id="[$e|4]", label="dummy/1.1→main/0.0:integer"];
-	n_1 -> n_2 [id="[$e|0]", label="main/0.0Δdummy/1.0"];
 	n_3 -> n_3 [id="[$e|5]", label="dummy/1.0→main/0.0:integer"];
 	n_4 -> n_3 [id="[$e|2]", label="dummy/1.0→main/0.0:integer"];
 	n_2 -> n_4 [id="[$e|1]", label="main/0.0Δdummy/1.1"];
+	n_1 -> n_2 [id="[$e|0]", label="main/0.0Δdummy/1.0"];
+	n_3 -> n_3 [id="[$e|4]", label="dummy/1.1→main/0.0:integer"];
+	n_4 -> n_3 [id="[$e|3]", label="dummy/1.1→main/0.0:integer"];
 }
diff --git a/examples/for-loop-recursion/main_0_local_view.dot b/examples/for-loop-recursion/main_0_local_view.dot
index 25112e9..485ee11 100644
--- a/examples/for-loop-recursion/main_0_local_view.dot
+++ b/examples/for-loop-recursion/main_0_local_view.dot
@@ -6,7 +6,7 @@ digraph main_0 {
 	n_2 [id="2", shape=circle, label="2"];
 	n_3 [id="3", shape=doublecircle, label="3"];
 
-	n_2 -> n_3 [id="[$e|4]", label="spawn dummy/1.1"];
-	n_1 -> n_2 [id="[$e|0]", label="spawn dummy/1.0"];
 	n_3 -> n_3 [id="[$e|2]", label="receive Num"];
+	n_1 -> n_2 [id="[$e|0]", label="spawn dummy/1.0"];
+	n_2 -> n_3 [id="[$e|4]", label="spawn dummy/1.1"];
 }
diff --git a/examples/function-call/main_0_global_view.dot b/examples/function-call/main_0_global_view.dot
index 4dcb3ca..58c6330 100644
--- a/examples/function-call/main_0_global_view.dot
+++ b/examples/function-call/main_0_global_view.dot
@@ -7,6 +7,6 @@ digraph global {
 	n_3 [id="3", shape=circle, label="3"];
 
 	n_1 -> n_2 [id="[$e|0]", label="main/0.0Δdummy/1.0"];
-	n_2 -> n_3 [id="[$e|2]", label="dummy/1.0→main/0.0:{pid_self,hello2}"];
 	n_2 -> n_3 [id="[$e|1]", label="dummy/1.0→main/0.0:{pid_self,hello1}"];
+	n_2 -> n_3 [id="[$e|2]", label="dummy/1.0→main/0.0:{pid_self,hello2}"];
 }
diff --git a/examples/hello/greet_0_local_view.dot b/examples/hello/greet_0_local_view.dot
index 36862c1..5a85a02 100644
--- a/examples/hello/greet_0_local_view.dot
+++ b/examples/hello/greet_0_local_view.dot
@@ -6,8 +6,8 @@ digraph greet_0 {
 	n_2 [id="2", shape=circle, label="2"];
 	n_3 [id="3", shape=doublecircle, label="3"];
 
-	n_1 -> n_2 [id="[$e|3]", label="send hello1 to pid_self"];
-	n_2 -> n_3 [id="[$e|6]", label="receive hello1"];
 	n_2 -> n_1 [id="[$e|5]", label="send hello2 to pid_self"];
+	n_2 -> n_3 [id="[$e|6]", label="receive hello1"];
 	n_2 -> n_3 [id="[$e|0]", label="receive hello2"];
+	n_1 -> n_2 [id="[$e|3]", label="send hello1 to pid_self"];
 }
diff --git a/examples/high-order-fun/greet_0_global_view.dot b/examples/high-order-fun/greet_0_global_view.dot
index ab43aca..d1dd488 100644
--- a/examples/high-order-fun/greet_0_global_view.dot
+++ b/examples/high-order-fun/greet_0_global_view.dot
@@ -13,18 +13,19 @@ digraph global {
 	n_9 [id="7", shape=circle, label="7"];
 	n_10 [id="3", shape=circle, label="3"];
 
-	n_2 -> n_2 [id="[$e|9]", label="greet/0.0→greet/0.0:hello2"];
+	n_8 -> n_3 [id="[$e|12]", label="greet/0.0→anonfun_15.0:hello1"];
 	n_2 -> n_5 [id="[$e|10]", label="greet/0.0→anonfun_15.0:hello1"];
-	n_7 -> n_3 [id="[$e|12]", label="greet/0.0→anonfun_15.0:hello1"];
-	n_8 -> n_9 [id="[$e|5]", label="greet/0.0→anonfun_15.0:hello1"];
-	n_5 -> n_5 [id="[$e|13]", label="greet/0.0→greet/0.0:hello2"];
-	n_9 -> n_3 [id="[$e|11]", label="greet/0.0→anonfun_10.0:hello3"];
+	n_1 -> n_1 [id="[$e|8]", label="greet/0.0→greet/0.0:hello2"];
 	n_4 -> n_6 [id="[$e|0]", label="greet/0.0Δanonfun_15.0"];
-	n_8 -> n_7 [id="[$e|6]", label="greet/0.0→anonfun_10.0:hello3"];
-	n_10 -> n_1 [id="[$e|3]", label="greet/0.0→anonfun_15.0:hello1"];
-	n_10 -> n_8 [id="[$e|2]", label="greet/0.0→greet/0.0:hello2"];
-	n_1 -> n_1 [id="[$e|7]", label="greet/0.0→greet/0.0:hello2"];
-	n_10 -> n_2 [id="[$e|4]", label="greet/0.0→anonfun_10.0:hello3"];
-	n_1 -> n_5 [id="[$e|8]", label="greet/0.0→anonfun_10.0:hello3"];
+	n_2 -> n_7 [id="[$e|9]", label="greet/0.0→anonfun_10.0:hello3"];
+	n_9 -> n_9 [id="[$e|11]", label="greet/0.0→greet/0.0:hello2"];
+	n_8 -> n_9 [id="[$e|5]", label="greet/0.0→anonfun_15.0:hello1"];
+	n_8 -> n_8 [id="[$e|6]", label="greet/0.0→greet/0.0:hello2"];
+	n_10 -> n_2 [id="[$e|4]", label="greet/0.0→greet/0.0:hello2"];
+	n_7 -> n_3 [id="[$e|13]", label="greet/0.0→anonfun_15.0:hello1"];
 	n_6 -> n_10 [id="[$e|1]", label="greet/0.0Δanonfun_10.0"];
+	n_10 -> n_8 [id="[$e|2]", label="greet/0.0→anonfun_10.0:hello3"];
+	n_10 -> n_1 [id="[$e|3]", label="greet/0.0→anonfun_15.0:hello1"];
+	n_1 -> n_9 [id="[$e|7]", label="greet/0.0→anonfun_10.0:hello3"];
+	n_5 -> n_3 [id="[$e|14]", label="greet/0.0→anonfun_10.0:hello3"];
 }
diff --git a/examples/high-order-fun/greet_0_local_view.dot b/examples/high-order-fun/greet_0_local_view.dot
index 41edaa4..8fa2858 100644
--- a/examples/high-order-fun/greet_0_local_view.dot
+++ b/examples/high-order-fun/greet_0_local_view.dot
@@ -12,8 +12,8 @@ digraph greet_0 {
 
 	n_4 -> n_1 [id="[$e|0]", label="send hello2 to pid_self"];
 	n_1 -> n_6 [id="[$e|6]", label="spawn anonfun_10.0"];
-	n_2 -> n_7 [id="[$e|2]", label="spawn anonfun_15.0"];
-	n_6 -> n_5 [id="[$e|7]", label="send hello3 to anonfun_10.0"];
 	n_7 -> n_4 [id="[$e|4]", label="send hello1 to anonfun_15.0"];
 	n_5 -> n_3 [id="[$e|1]", label="receive _"];
+	n_2 -> n_7 [id="[$e|2]", label="spawn anonfun_15.0"];
+	n_6 -> n_5 [id="[$e|7]", label="send hello3 to anonfun_10.0"];
 }
diff --git a/examples/if-cases/a_0_local_view.dot b/examples/if-cases/a_0_local_view.dot
index 08ca137..3b279fb 100644
--- a/examples/if-cases/a_0_local_view.dot
+++ b/examples/if-cases/a_0_local_view.dot
@@ -7,6 +7,6 @@ digraph a_0 {
 	n_3 [id="3", shape=circle, label="2"];
 
 	n_1 -> n_3 [id="[$e|2]", label="receive Pid"];
-	n_3 -> n_3 [id="[$e|1]", label="receive Pid"];
 	n_3 -> n_2 [id="[$e|0]", label="send 'Hi, i'm A' to Pid"];
+	n_3 -> n_3 [id="[$e|1]", label="receive Pid"];
 }
diff --git a/examples/if-cases/b_0_local_view.dot b/examples/if-cases/b_0_local_view.dot
index 309c7c6..0ad2b74 100644
--- a/examples/if-cases/b_0_local_view.dot
+++ b/examples/if-cases/b_0_local_view.dot
@@ -7,6 +7,6 @@ digraph b_0 {
 	n_3 [id="3", shape=circle, label="2"];
 
 	n_3 -> n_2 [id="[$e|2]", label="send 'Hi, i'm B' to Pid"];
-	n_1 -> n_3 [id="[$e|1]", label="receive Pid"];
 	n_3 -> n_3 [id="[$e|0]", label="receive Pid"];
+	n_1 -> n_3 [id="[$e|1]", label="receive Pid"];
 }
diff --git a/examples/if-cases/c_0_local_view.dot b/examples/if-cases/c_0_local_view.dot
index 1e9d4ec..d52c458 100644
--- a/examples/if-cases/c_0_local_view.dot
+++ b/examples/if-cases/c_0_local_view.dot
@@ -7,6 +7,6 @@ digraph c_0 {
 	n_3 [id="3", shape=circle, label="2"];
 
 	n_1 -> n_3 [id="[$e|2]", label="receive Pid"];
-	n_3 -> n_3 [id="[$e|1]", label="receive Pid"];
 	n_3 -> n_2 [id="[$e|0]", label="send 'Hi, i'm C' to Pid"];
+	n_3 -> n_3 [id="[$e|1]", label="receive Pid"];
 }
diff --git a/examples/if-cases/main_0_global_view.dot b/examples/if-cases/main_0_global_view.dot
index b4bba81..8ebecb6 100644
--- a/examples/if-cases/main_0_global_view.dot
+++ b/examples/if-cases/main_0_global_view.dot
@@ -14,31 +14,31 @@ digraph global {
 	n_10 [id="7", shape=circle, label="7"];
 	n_11 [id="3", shape=circle, label="3"];
 
-	n_1 -> n_6 [id="[$e|10]", label="main/0.0→c/0.0:a/0.0"];
-	n_3 -> n_8 [id="[$e|11]", label="main/0.0→a/0.0:b/0.0"];
-	n_1 -> n_8 [id="[$e|9]", label="main/0.0→b/0.0:c/0.0"];
-	n_3 -> n_8 [id="[$e|17]", label="main/0.0→a/0.0:c/0.0"];
-	n_10 -> n_4 [id="[$e|20]", label="main/0.0→b/0.0:a/0.0"];
-	n_3 -> n_4 [id="[$e|12]", label="main/0.0→c/0.0:a/0.0"];
-	n_9 -> n_10 [id="[$e|8]", label="main/0.0→c/0.0:b/0.0"];
-	n_10 -> n_4 [id="[$e|14]", label="main/0.0→b/0.0:c/0.0"];
-	n_6 -> n_2 [id="[$e|22]", label="main/0.0→b/0.0:c/0.0"];
-	n_9 -> n_1 [id="[$e|6]", label="main/0.0→a/0.0:c/0.0"];
 	n_9 -> n_1 [id="[$e|3]", label="main/0.0→a/0.0:b/0.0"];
-	n_3 -> n_4 [id="[$e|18]", label="main/0.0→c/0.0:b/0.0"];
-	n_6 -> n_2 [id="[$e|25]", label="main/0.0→b/0.0:a/0.0"];
-	n_1 -> n_6 [id="[$e|16]", label="main/0.0→c/0.0:b/0.0"];
-	n_4 -> n_2 [id="[$e|23]", label="main/0.0→a/0.0:b/0.0"];
+	n_4 -> n_2 [id="[$e|26]", label="main/0.0→a/0.0:c/0.0"];
+	n_9 -> n_1 [id="[$e|6]", label="main/0.0→a/0.0:c/0.0"];
 	n_11 -> n_9 [id="[$e|2]", label="main/0.0Δc/0.0"];
 	n_10 -> n_6 [id="[$e|13]", label="main/0.0→a/0.0:b/0.0"];
-	n_9 -> n_10 [id="[$e|5]", label="main/0.0→c/0.0:a/0.0"];
-	n_8 -> n_2 [id="[$e|21]", label="main/0.0→c/0.0:a/0.0"];
-	n_1 -> n_8 [id="[$e|15]", label="main/0.0→b/0.0:a/0.0"];
-	n_7 -> n_11 [id="[$e|1]", label="main/0.0Δb/0.0"];
-	n_9 -> n_3 [id="[$e|4]", label="main/0.0→b/0.0:c/0.0"];
+	n_10 -> n_4 [id="[$e|14]", label="main/0.0→b/0.0:c/0.0"];
+	n_3 -> n_4 [id="[$e|18]", label="main/0.0→c/0.0:b/0.0"];
 	n_10 -> n_6 [id="[$e|19]", label="main/0.0→a/0.0:c/0.0"];
-	n_9 -> n_3 [id="[$e|7]", label="main/0.0→b/0.0:a/0.0"];
+	n_1 -> n_8 [id="[$e|15]", label="main/0.0→b/0.0:a/0.0"];
+	n_3 -> n_4 [id="[$e|12]", label="main/0.0→c/0.0:a/0.0"];
+	n_4 -> n_2 [id="[$e|23]", label="main/0.0→a/0.0:b/0.0"];
 	n_8 -> n_2 [id="[$e|24]", label="main/0.0→c/0.0:b/0.0"];
-	n_4 -> n_2 [id="[$e|26]", label="main/0.0→a/0.0:c/0.0"];
+	n_9 -> n_10 [id="[$e|8]", label="main/0.0→c/0.0:b/0.0"];
+	n_8 -> n_2 [id="[$e|21]", label="main/0.0→c/0.0:a/0.0"];
+	n_10 -> n_4 [id="[$e|20]", label="main/0.0→b/0.0:a/0.0"];
 	n_5 -> n_7 [id="[$e|0]", label="main/0.0Δa/0.0"];
+	n_7 -> n_11 [id="[$e|1]", label="main/0.0Δb/0.0"];
+	n_9 -> n_3 [id="[$e|7]", label="main/0.0→b/0.0:a/0.0"];
+	n_9 -> n_3 [id="[$e|4]", label="main/0.0→b/0.0:c/0.0"];
+	n_6 -> n_2 [id="[$e|22]", label="main/0.0→b/0.0:c/0.0"];
+	n_1 -> n_6 [id="[$e|16]", label="main/0.0→c/0.0:b/0.0"];
+	n_9 -> n_10 [id="[$e|5]", label="main/0.0→c/0.0:a/0.0"];
+	n_3 -> n_8 [id="[$e|17]", label="main/0.0→a/0.0:c/0.0"];
+	n_3 -> n_8 [id="[$e|11]", label="main/0.0→a/0.0:b/0.0"];
+	n_6 -> n_2 [id="[$e|25]", label="main/0.0→b/0.0:a/0.0"];
+	n_1 -> n_6 [id="[$e|10]", label="main/0.0→c/0.0:a/0.0"];
+	n_1 -> n_8 [id="[$e|9]", label="main/0.0→b/0.0:c/0.0"];
 }
diff --git a/examples/if-cases/main_0_local_view.dot b/examples/if-cases/main_0_local_view.dot
index 1ee095f..2935292 100644
--- a/examples/if-cases/main_0_local_view.dot
+++ b/examples/if-cases/main_0_local_view.dot
@@ -12,13 +12,13 @@ digraph main_0 {
 	n_8 [id="7", shape=doublecircle, label="4"];
 	n_9 [id="3", shape=circle, label="2"];
 
-	n_7 -> n_6 [id="[$e|9]", label="send a/0.0 to b/0.0"];
-	n_1 -> n_2 [id="[$e|8]", label="send c/0.0 to b/0.0"];
-	n_8 -> n_5 [id="[$e|6]", label="send c/0.0 to a/0.0"];
 	n_8 -> n_1 [id="[$e|3]", label="send b/0.0 to a/0.0"];
+	n_8 -> n_5 [id="[$e|6]", label="send c/0.0 to a/0.0"];
 	n_3 -> n_8 [id="[$e|2]", label="spawn c/0.0"];
+	n_1 -> n_2 [id="[$e|8]", label="send c/0.0 to b/0.0"];
+	n_4 -> n_9 [id="[$e|0]", label="spawn a/0.0"];
 	n_2 -> n_6 [id="[$e|1]", label="send a/0.0 to c/0.0"];
-	n_5 -> n_7 [id="[$e|4]", label="send b/0.0 to c/0.0"];
 	n_9 -> n_3 [id="[$e|7]", label="spawn b/0.0"];
-	n_4 -> n_9 [id="[$e|0]", label="spawn a/0.0"];
+	n_5 -> n_7 [id="[$e|4]", label="send b/0.0 to c/0.0"];
+	n_7 -> n_6 [id="[$e|9]", label="send a/0.0 to b/0.0"];
 }
diff --git a/examples/serverclient/client_0_local_view.dot b/examples/serverclient/client_0_local_view.dot
index 9c1e1f2..bd6b8c0 100644
--- a/examples/serverclient/client_0_local_view.dot
+++ b/examples/serverclient/client_0_local_view.dot
@@ -7,8 +7,8 @@ digraph client_0 {
 	n_3 [id="4", shape=circle, label="2"];
 	n_4 [id="3", shape=circle, label="3"];
 
+	n_4 -> n_4 [id="[$e|7]", label="send next to Handle"];
 	n_3 -> n_4 [id="[$e|3]", label="receive {res,Handle}"];
-	n_4 -> n_2 [id="[$e|5]", label="send done to Handle"];
 	n_1 -> n_3 [id="[$e|1]", label="send {req,pid_self} to server/0.0"];
-	n_4 -> n_4 [id="[$e|7]", label="send next to Handle"];
+	n_4 -> n_2 [id="[$e|5]", label="send done to Handle"];
 }
diff --git a/examples/serverclient/handle_req_1_local_view.dot b/examples/serverclient/handle_req_1_local_view.dot
index 6056680..564771d 100644
--- a/examples/serverclient/handle_req_1_local_view.dot
+++ b/examples/serverclient/handle_req_1_local_view.dot
@@ -5,6 +5,6 @@ digraph handle_req_1 {
 	n_0 -> n_1 [arrowhead=none];
 	n_2 [id="2", shape=doublecircle, label="2"];
 
-	n_1 -> n_1 [id="[$e|5]", label="receive next"];
 	n_1 -> n_2 [id="[$e|1]", label="receive done"];
+	n_1 -> n_1 [id="[$e|5]", label="receive next"];
 }
diff --git a/examples/serverclient/main_0_global_view.dot b/examples/serverclient/main_0_global_view.dot
index d444fcb..6881f8a 100644
--- a/examples/serverclient/main_0_global_view.dot
+++ b/examples/serverclient/main_0_global_view.dot
@@ -10,11 +10,11 @@ digraph global {
 	n_6 [id="7", shape=circle, label="7"];
 	n_7 [id="3", shape=circle, label="3"];
 
-	n_5 -> n_1 [id="[$e|3]", label="server/0.0Δhandle_req/1.0"];
+	n_3 -> n_4 [id="[$e|0]", label="main/0.0Δserver/0.0"];
 	n_7 -> n_5 [id="[$e|2]", label="client/0.0→server/0.0:{req,pid_self}"];
 	n_2 -> n_2 [id="[$e|6]", label="client/0.0→handle_req/1.0:next"];
-	n_2 -> n_6 [id="[$e|5]", label="client/0.0→handle_req/1.0:done"];
-	n_4 -> n_7 [id="[$e|1]", label="main/0.0Δclient/0.0"];
+	n_5 -> n_1 [id="[$e|3]", label="server/0.0Δhandle_req/1.0"];
 	n_1 -> n_2 [id="[$e|4]", label="server/0.0→client/0.0:{res,handle_req/1.0}"];
-	n_3 -> n_4 [id="[$e|0]", label="main/0.0Δserver/0.0"];
+	n_4 -> n_7 [id="[$e|1]", label="main/0.0Δclient/0.0"];
+	n_2 -> n_6 [id="[$e|5]", label="client/0.0→handle_req/1.0:done"];
 }
diff --git a/examples/serverclient/main_0_local_view.dot b/examples/serverclient/main_0_local_view.dot
index ac5bdc8..b87e932 100644
--- a/examples/serverclient/main_0_local_view.dot
+++ b/examples/serverclient/main_0_local_view.dot
@@ -6,6 +6,6 @@ digraph main_0 {
 	n_2 [id="2", shape=circle, label="2"];
 	n_3 [id="3", shape=doublecircle, label="3"];
 
-	n_1 -> n_2 [id="[$e|1]", label="spawn server/0.0"];
 	n_2 -> n_3 [id="[$e|0]", label="spawn client/0.0"];
+	n_1 -> n_2 [id="[$e|1]", label="spawn server/0.0"];
 }
diff --git a/examples/serverclient/server_0_local_view.dot b/examples/serverclient/server_0_local_view.dot
index 6f7fd26..2244081 100644
--- a/examples/serverclient/server_0_local_view.dot
+++ b/examples/serverclient/server_0_local_view.dot
@@ -8,9 +8,9 @@ digraph server_0 {
 	n_4 [id="4", shape=circle, label="3"];
 	n_5 [id="3", shape=doublecircle, label="4"];
 
-	n_3 -> n_1 [id="[$e|3]", label="spawn handle_req/1.0"];
+	n_2 -> n_3 [id="[$e|0]", label="receive {req,P}"];
 	n_2 -> n_4 [id="[$e|2]", label="receive ciao"];
 	n_4 -> n_5 [id="[$e|6]", label="spawn handle_req/1.1"];
-	n_2 -> n_3 [id="[$e|0]", label="receive {req,P}"];
 	n_1 -> n_2 [id="[$e|7]", label="send {res,handle_req/1.0} to P"];
+	n_3 -> n_1 [id="[$e|3]", label="spawn handle_req/1.0"];
 }
diff --git a/examples/test/barber/test_0_local_view.dot b/examples/test/barber/test_0_local_view.dot
index 5b132ed..6071a46 100644
--- a/examples/test/barber/test_0_local_view.dot
+++ b/examples/test/barber/test_0_local_view.dot
@@ -10,10 +10,10 @@ digraph test_0 {
 	n_6 [id="7", shape=circle, label="3"];
 	n_7 [id="3", shape=circle, label="4"];
 
-	n_1 -> n_2 [id="[$e|5]", label="receive {Name2,State2}"];
+	n_7 -> n_1 [id="[$e|4]", label="receive {Name1,State1}"];
 	n_6 -> n_7 [id="[$e|3]", label="spawn customer/3.1"];
+	n_3 -> n_4 [id="[$e|1]", label="spawn open_barber_shop/0.0"];
 	n_2 -> n_5 [id="[$e|2]", label="send stop to open_barber_shop/0.0"];
+	n_1 -> n_2 [id="[$e|5]", label="receive {Name2,State2}"];
 	n_4 -> n_6 [id="[$e|0]", label="spawn customer/3.0"];
-	n_7 -> n_1 [id="[$e|4]", label="receive {Name1,State1}"];
-	n_3 -> n_4 [id="[$e|1]", label="spawn open_barber_shop/0.0"];
 }
diff --git a/examples/test/foo1/test_0_global_view.dot b/examples/test/foo1/test_0_global_view.dot
index 2f5e17c..e68c57a 100644
--- a/examples/test/foo1/test_0_global_view.dot
+++ b/examples/test/foo1/test_0_global_view.dot
@@ -9,10 +9,10 @@ digraph global {
 	n_5 [id="4", shape=circle, label="4"];
 	n_6 [id="3", shape=circle, label="3"];
 
-	n_1 -> n_2 [id="[$e|5]", label="test/0.0→b/0.0:uno"];
 	n_3 -> n_4 [id="[$e|0]", label="test/0.0Δb/0.0"];
-	n_6 -> n_1 [id="[$e|3]", label="test/0.0→c/1.0:dos"];
-	n_6 -> n_5 [id="[$e|2]", label="test/0.0→b/0.0:uno"];
+	n_1 -> n_2 [id="[$e|5]", label="test/0.0→b/0.0:uno"];
 	n_5 -> n_2 [id="[$e|4]", label="test/0.0→c/1.0:dos"];
 	n_4 -> n_6 [id="[$e|1]", label="test/0.0Δc/1.0"];
+	n_6 -> n_5 [id="[$e|2]", label="test/0.0→b/0.0:uno"];
+	n_6 -> n_1 [id="[$e|3]", label="test/0.0→c/1.0:dos"];
 }
diff --git a/examples/test/foo1/test_0_local_view.dot b/examples/test/foo1/test_0_local_view.dot
index 60481a4..2cf6d1a 100644
--- a/examples/test/foo1/test_0_local_view.dot
+++ b/examples/test/foo1/test_0_local_view.dot
@@ -9,7 +9,7 @@ digraph test_0 {
 	n_5 [id="3", shape=circle, label="4"];
 
 	n_1 -> n_5 [id="[$e|0]", label="send uno to b/0.0"];
-	n_5 -> n_4 [id="[$e|3]", label="send dos to c/1.0"];
-	n_3 -> n_1 [id="[$e|2]", label="spawn c/1.0"];
 	n_2 -> n_3 [id="[$e|1]", label="spawn b/0.0"];
+	n_3 -> n_1 [id="[$e|2]", label="spawn c/1.0"];
+	n_5 -> n_4 [id="[$e|3]", label="send dos to c/1.0"];
 }
diff --git a/examples/test/foo2/b_0_local_view.dot b/examples/test/foo2/b_0_local_view.dot
index ad304bc..f84044e 100644
--- a/examples/test/foo2/b_0_local_view.dot
+++ b/examples/test/foo2/b_0_local_view.dot
@@ -6,6 +6,6 @@ digraph b_0 {
 	n_2 [id="2", shape=doublecircle, label="3"];
 	n_3 [id="3", shape=circle, label="2"];
 
-	n_3 -> n_2 [id="[$e|0]", label="receive Z"];
 	n_1 -> n_3 [id="[$e|1]", label="receive X"];
+	n_3 -> n_2 [id="[$e|0]", label="receive Z"];
 }
diff --git a/examples/test/foo2/c_0_local_view.dot b/examples/test/foo2/c_0_local_view.dot
index d9a29db..b99e700 100644
--- a/examples/test/foo2/c_0_local_view.dot
+++ b/examples/test/foo2/c_0_local_view.dot
@@ -6,6 +6,6 @@ digraph c_0 {
 	n_2 [id="2", shape=circle, label="2"];
 	n_3 [id="3", shape=doublecircle, label="3"];
 
-	n_2 -> n_3 [id="[$e|0]", label="send 4 to unknown"];
 	n_1 -> n_2 [id="[$e|1]", label="receive _"];
+	n_2 -> n_3 [id="[$e|0]", label="send 4 to unknown"];
 }
diff --git a/examples/test/foo2/test_0_global_view.dot b/examples/test/foo2/test_0_global_view.dot
index 24ea431..76c883b 100644
--- a/examples/test/foo2/test_0_global_view.dot
+++ b/examples/test/foo2/test_0_global_view.dot
@@ -6,6 +6,6 @@ digraph global {
 	n_2 [id="2", shape=circle, label="2"];
 	n_3 [id="3", shape=circle, label="3"];
 
-	n_1 -> n_2 [id="[$e|0]", label="test/0.0Δc/0.0"];
 	n_2 -> n_3 [id="[$e|1]", label="test/0.0Δa/1.0"];
+	n_1 -> n_2 [id="[$e|0]", label="test/0.0Δc/0.0"];
 }
diff --git a/examples/test/foo2/test_0_local_view.dot b/examples/test/foo2/test_0_local_view.dot
index d216c76..7500814 100644
--- a/examples/test/foo2/test_0_local_view.dot
+++ b/examples/test/foo2/test_0_local_view.dot
@@ -6,6 +6,6 @@ digraph test_0 {
 	n_2 [id="2", shape=circle, label="2"];
 	n_3 [id="3", shape=doublecircle, label="3"];
 
-	n_2 -> n_3 [id="[$e|0]", label="spawn a/1.0"];
 	n_1 -> n_2 [id="[$e|1]", label="spawn c/0.0"];
+	n_2 -> n_3 [id="[$e|0]", label="spawn a/1.0"];
 }
diff --git a/examples/test/foo3/a_1_local_view.dot b/examples/test/foo3/a_1_local_view.dot
index 97264bf..7b3780d 100644
--- a/examples/test/foo3/a_1_local_view.dot
+++ b/examples/test/foo3/a_1_local_view.dot
@@ -6,6 +6,6 @@ digraph a_1 {
 	n_2 [id="2", shape=circle, label="2"];
 	n_3 [id="3", shape=doublecircle, label="3"];
 
-	n_1 -> n_2 [id="[$e|0]", label="send 1 to S"];
 	n_2 -> n_3 [id="[$e|1]", label="send 3 to S"];
+	n_1 -> n_2 [id="[$e|0]", label="send 1 to S"];
 }
diff --git a/examples/test/foo3/test_0_global_view.dot b/examples/test/foo3/test_0_global_view.dot
index 9b9db93..5e83b91 100644
--- a/examples/test/foo3/test_0_global_view.dot
+++ b/examples/test/foo3/test_0_global_view.dot
@@ -9,15 +9,15 @@ digraph global {
 	n_5 [id="4", shape=circle, label="4"];
 	n_6 [id="3", shape=circle, label="3"];
 
-	n_5 -> n_1 [id="[$e|7]", label="a/1.0→test/0.0:1"];
-	n_1 -> n_2 [id="[$e|9]", label="a/1.0→test/0.0:3"];
-	n_6 -> n_5 [id="[$e|3]", label="a/1.0→test/0.0:3"];
-	n_5 -> n_1 [id="[$e|6]", label="b/1.0→test/0.0:2"];
-	n_1 -> n_2 [id="[$e|8]", label="b/1.0→test/0.0:2"];
 	n_1 -> n_2 [id="[$e|10]", label="a/1.0→test/0.0:1"];
 	n_5 -> n_1 [id="[$e|5]", label="a/1.0→test/0.0:3"];
-	n_3 -> n_4 [id="[$e|0]", label="test/0.0Δa/1.0"];
+	n_5 -> n_1 [id="[$e|7]", label="a/1.0→test/0.0:1"];
 	n_4 -> n_6 [id="[$e|1]", label="test/0.0Δb/1.0"];
-	n_6 -> n_5 [id="[$e|4]", label="b/1.0→test/0.0:2"];
+	n_5 -> n_1 [id="[$e|6]", label="b/1.0→test/0.0:2"];
+	n_1 -> n_2 [id="[$e|9]", label="a/1.0→test/0.0:3"];
+	n_3 -> n_4 [id="[$e|0]", label="test/0.0Δa/1.0"];
 	n_6 -> n_5 [id="[$e|2]", label="a/1.0→test/0.0:1"];
+	n_6 -> n_5 [id="[$e|3]", label="a/1.0→test/0.0:3"];
+	n_6 -> n_5 [id="[$e|4]", label="b/1.0→test/0.0:2"];
+	n_1 -> n_2 [id="[$e|8]", label="b/1.0→test/0.0:2"];
 }
diff --git a/examples/test/foo3/test_0_local_view.dot b/examples/test/foo3/test_0_local_view.dot
index 8f8087e..d021031 100644
--- a/examples/test/foo3/test_0_local_view.dot
+++ b/examples/test/foo3/test_0_local_view.dot
@@ -9,9 +9,9 @@ digraph test_0 {
 	n_5 [id="4", shape=circle, label="5"];
 	n_6 [id="3", shape=circle, label="4"];
 
-	n_2 -> n_6 [id="[$e|3]", label="receive X"];
-	n_5 -> n_1 [id="[$e|0]", label="receive Z"];
 	n_4 -> n_2 [id="[$e|1]", label="spawn b/1.0"];
-	n_6 -> n_5 [id="[$e|4]", label="receive Y"];
+	n_5 -> n_1 [id="[$e|0]", label="receive Z"];
 	n_3 -> n_4 [id="[$e|2]", label="spawn a/1.0"];
+	n_2 -> n_6 [id="[$e|3]", label="receive X"];
+	n_6 -> n_5 [id="[$e|4]", label="receive Y"];
 }
diff --git a/examples/test/foo4/test_0_global_view.dot b/examples/test/foo4/test_0_global_view.dot
index 58199c6..4e64cc7 100644
--- a/examples/test/foo4/test_0_global_view.dot
+++ b/examples/test/foo4/test_0_global_view.dot
@@ -15,18 +15,18 @@ digraph global {
 	n_11 [id="3", shape=circle, label="3"];
 
 	n_5 -> n_7 [id="[$e|0]", label="test/0.0Δr/0.0"];
+	n_8 -> n_2 [id="[$e|12]", label="test/0.0→w2/1.0:w2"];
+	n_3 -> n_8 [id="[$e|8]", label="test/0.0→r/0.0:r0"];
 	n_3 -> n_4 [id="[$e|9]", label="test/0.0→w2/1.0:w2"];
 	n_4 -> n_2 [id="[$e|14]", label="test/0.0→r/0.0:r0"];
-	n_9 -> n_10 [id="[$e|5]", label="test/0.0→w2/1.0:w2"];
-	n_9 -> n_1 [id="[$e|3]", label="test/0.0→r/0.0:r0"];
-	n_3 -> n_8 [id="[$e|8]", label="test/0.0→r/0.0:r0"];
-	n_8 -> n_2 [id="[$e|12]", label="test/0.0→w2/1.0:w2"];
-	n_1 -> n_8 [id="[$e|6]", label="test/0.0→w1/1.0:w1"];
 	n_11 -> n_9 [id="[$e|2]", label="test/0.0Δw2/1.0"];
-	n_10 -> n_6 [id="[$e|10]", label="test/0.0→r/0.0:r0"];
+	n_1 -> n_8 [id="[$e|6]", label="test/0.0→w1/1.0:w1"];
 	n_1 -> n_6 [id="[$e|7]", label="test/0.0→w2/1.0:w2"];
-	n_10 -> n_4 [id="[$e|11]", label="test/0.0→w1/1.0:w1"];
+	n_10 -> n_6 [id="[$e|10]", label="test/0.0→r/0.0:r0"];
 	n_6 -> n_2 [id="[$e|13]", label="test/0.0→w1/1.0:w1"];
+	n_10 -> n_4 [id="[$e|11]", label="test/0.0→w1/1.0:w1"];
+	n_9 -> n_1 [id="[$e|3]", label="test/0.0→r/0.0:r0"];
 	n_9 -> n_3 [id="[$e|4]", label="test/0.0→w1/1.0:w1"];
 	n_7 -> n_11 [id="[$e|1]", label="test/0.0Δw1/1.0"];
+	n_9 -> n_10 [id="[$e|5]", label="test/0.0→w2/1.0:w2"];
 }
diff --git a/examples/test/foo4/test_0_local_view.dot b/examples/test/foo4/test_0_local_view.dot
index fadba73..30b07f9 100644
--- a/examples/test/foo4/test_0_local_view.dot
+++ b/examples/test/foo4/test_0_local_view.dot
@@ -11,9 +11,9 @@ digraph test_0 {
 	n_7 [id="3", shape=circle, label="4"];
 
 	n_6 -> n_7 [id="[$e|0]", label="spawn w1/1.0"];
-	n_2 -> n_5 [id="[$e|5]", label="send w1 to w1/1.0"];
-	n_3 -> n_4 [id="[$e|3]", label="spawn r/0.0"];
 	n_5 -> n_1 [id="[$e|2]", label="send w2 to w2/1.0"];
+	n_3 -> n_4 [id="[$e|3]", label="spawn r/0.0"];
 	n_4 -> n_6 [id="[$e|4]", label="send r0 to r/0.0"];
 	n_7 -> n_2 [id="[$e|1]", label="spawn w2/1.0"];
+	n_2 -> n_5 [id="[$e|5]", label="send w1 to w1/1.0"];
 }
diff --git a/examples/test/foo5/target_0_local_view.dot b/examples/test/foo5/target_0_local_view.dot
index b330284..809f91d 100644
--- a/examples/test/foo5/target_0_local_view.dot
+++ b/examples/test/foo5/target_0_local_view.dot
@@ -8,8 +8,8 @@ digraph target_0 {
 	n_4 [id="4", shape=circle, label="4"];
 	n_5 [id="3", shape=circle, label="2"];
 
+	n_5 -> n_3 [id="[$e|3]", label="receive B"];
 	n_4 -> n_1 [id="[$e|1]", label="receive D"];
 	n_2 -> n_5 [id="[$e|2]", label="receive A"];
-	n_5 -> n_3 [id="[$e|3]", label="receive B"];
 	n_3 -> n_4 [id="[$e|0]", label="receive C"];
 }
diff --git a/examples/test/foo5/test_0_global_view.dot b/examples/test/foo5/test_0_global_view.dot
index 552a727..174f858 100644
--- a/examples/test/foo5/test_0_global_view.dot
+++ b/examples/test/foo5/test_0_global_view.dot
@@ -10,10 +10,10 @@ digraph global {
 	n_6 [id="7", shape=circle, label="7"];
 	n_7 [id="3", shape=circle, label="3"];
 
+	n_7 -> n_1 [id="[$e|3]", label="test/0.0→proxy/1.1:m3"];
+	n_1 -> n_6 [id="[$e|5]", label="test/0.0→proxy/1.0:m2"];
+	n_5 -> n_2 [id="[$e|4]", label="test/0.0→proxy/1.1:m3"];
 	n_4 -> n_7 [id="[$e|1]", label="test/0.0Δproxy/1.1"];
 	n_7 -> n_5 [id="[$e|2]", label="test/0.0→proxy/1.0:m2"];
-	n_7 -> n_1 [id="[$e|3]", label="test/0.0→proxy/1.1:m3"];
 	n_3 -> n_4 [id="[$e|0]", label="test/0.0Δproxy/1.0"];
-	n_5 -> n_2 [id="[$e|4]", label="test/0.0→proxy/1.1:m3"];
-	n_1 -> n_6 [id="[$e|5]", label="test/0.0→proxy/1.0:m2"];
 }
diff --git a/examples/test/foo5/test_0_local_view.dot b/examples/test/foo5/test_0_local_view.dot
index 044ff5d..f260a85 100644
--- a/examples/test/foo5/test_0_local_view.dot
+++ b/examples/test/foo5/test_0_local_view.dot
@@ -11,11 +11,11 @@ digraph test_0 {
 	n_7 [id="7", shape=circle, label="5"];
 	n_8 [id="3", shape=circle, label="4"];
 
+	n_6 -> n_2 [id="[$e|3]", label="send m3 to proxy/1.1"];
+	n_2 -> n_1 [id="[$e|5]", label="send m4 to target/0.0"];
+	n_5 -> n_8 [id="[$e|4]", label="spawn proxy/1.1"];
+	n_8 -> n_7 [id="[$e|6]", label="send m1 to target/0.0"];
 	n_4 -> n_5 [id="[$e|1]", label="spawn proxy/1.0"];
 	n_7 -> n_6 [id="[$e|2]", label="send m2 to proxy/1.0"];
-	n_8 -> n_7 [id="[$e|6]", label="send m1 to target/0.0"];
-	n_6 -> n_2 [id="[$e|3]", label="send m3 to proxy/1.1"];
 	n_3 -> n_4 [id="[$e|0]", label="spawn target/0.0"];
-	n_5 -> n_8 [id="[$e|4]", label="spawn proxy/1.1"];
-	n_2 -> n_1 [id="[$e|5]", label="send m4 to target/0.0"];
 }
diff --git a/examples/test/foo6/test_0_global_view.dot b/examples/test/foo6/test_0_global_view.dot
index c7f25db..0137b15 100644
--- a/examples/test/foo6/test_0_global_view.dot
+++ b/examples/test/foo6/test_0_global_view.dot
@@ -10,10 +10,10 @@ digraph global {
 	n_6 [id="7", shape=circle, label="7"];
 	n_7 [id="3", shape=circle, label="3"];
 
-	n_3 -> n_4 [id="[$e|0]", label="test/0.0Δserver/0.0"];
-	n_4 -> n_7 [id="[$e|1]", label="test/0.0Δclient/1.1"];
-	n_4 -> n_5 [id="[$e|2]", label="test/0.0Δclient/1.0"];
 	n_7 -> n_1 [id="[$e|3]", label="test/0.0Δclient/1.1"];
 	n_7 -> n_2 [id="[$e|4]", label="test/0.0Δclient/1.0"];
 	n_1 -> n_6 [id="[$e|5]", label="test/0.0Δclient/1.0"];
+	n_4 -> n_7 [id="[$e|1]", label="test/0.0Δclient/1.1"];
+	n_4 -> n_5 [id="[$e|2]", label="test/0.0Δclient/1.0"];
+	n_3 -> n_4 [id="[$e|0]", label="test/0.0Δserver/0.0"];
 }
diff --git a/examples/test/foo6/test_0_local_view.dot b/examples/test/foo6/test_0_local_view.dot
index 2094185..62acd74 100644
--- a/examples/test/foo6/test_0_local_view.dot
+++ b/examples/test/foo6/test_0_local_view.dot
@@ -6,7 +6,7 @@ digraph test_0 {
 	n_2 [id="2", shape=circle, label="2"];
 	n_3 [id="3", shape=doublecircle, label="3"];
 
-	n_2 -> n_2 [id="[$e|0]", label="spawn client/1.1"];
 	n_2 -> n_3 [id="[$e|4]", label="spawn client/1.0"];
 	n_1 -> n_2 [id="[$e|5]", label="spawn server/0.0"];
+	n_2 -> n_2 [id="[$e|0]", label="spawn client/1.1"];
 }
diff --git a/examples/test/ping/pong_0_local_view.dot b/examples/test/ping/pong_0_local_view.dot
index 3d4aed5..9ec2f57 100644
--- a/examples/test/ping/pong_0_local_view.dot
+++ b/examples/test/ping/pong_0_local_view.dot
@@ -8,7 +8,7 @@ digraph pong_0 {
 	n_4 [id="3", shape=circle, label="2"];
 
 	n_1 -> n_4 [id="[$e|0]", label="receive {S,N}"];
-	n_2 -> n_3 [id="[$e|5]", label="send kill to S"];
 	n_4 -> n_1 [id="[$e|6]", label="send N to S"];
+	n_2 -> n_3 [id="[$e|5]", label="send kill to S"];
 	n_1 -> n_2 [id="[$e|4]", label="receive {S,0}"];
 }
diff --git a/examples/test/ping/start_0_local_view.dot b/examples/test/ping/start_0_local_view.dot
index 41efcb3..660e8ce 100644
--- a/examples/test/ping/start_0_local_view.dot
+++ b/examples/test/ping/start_0_local_view.dot
@@ -8,9 +8,9 @@ digraph start_0 {
 	n_4 [id="2", shape=circle, label="2"];
 	n_5 [id="3", shape=circle, label="3"];
 
-	n_3 -> n_4 [id="[$e|1]", label="spawn pong/0.0"];
+	n_5 -> n_1 [id="[$e|3]", label="receive N"];
 	n_4 -> n_5 [id="[$e|7]", label="send 3 to pid_self"];
+	n_3 -> n_4 [id="[$e|1]", label="spawn pong/0.0"];
 	n_5 -> n_2 [id="[$e|0]", label="receive kill"];
 	n_1 -> n_5 [id="[$e|5]", label="send {pid_self,unknown} to Pong"];
-	n_5 -> n_1 [id="[$e|3]", label="receive N"];
 }
diff --git a/examples/ticktackloop/start_0_global_view.dot b/examples/ticktackloop/start_0_global_view.dot
index a77ed31..099f998 100644
--- a/examples/ticktackloop/start_0_global_view.dot
+++ b/examples/ticktackloop/start_0_global_view.dot
@@ -10,7 +10,7 @@ digraph global {
 
 	n_4 -> n_1 [id="[$e|3]", label="tic_loop/0.0→tac_loop/0.0:tic"];
 	n_5 -> n_4 [id="[$e|2]", label="start/0.0→tic_loop/0.0:tac"];
+	n_2 -> n_3 [id="[$e|0]", label="start/0.0Δtac_loop/0.0"];
 	n_3 -> n_5 [id="[$e|1]", label="start/0.0Δtic_loop/0.0"];
 	n_1 -> n_4 [id="[$e|4]", label="tac_loop/0.0→tic_loop/0.0:tac"];
-	n_2 -> n_3 [id="[$e|0]", label="start/0.0Δtac_loop/0.0"];
 }
diff --git a/examples/ticktackloop/start_0_local_view.dot b/examples/ticktackloop/start_0_local_view.dot
index 865aadd..47ebd52 100644
--- a/examples/ticktackloop/start_0_local_view.dot
+++ b/examples/ticktackloop/start_0_local_view.dot
@@ -8,6 +8,6 @@ digraph start_0 {
 	n_4 [id="3", shape=doublecircle, label="4"];
 
 	n_1 -> n_3 [id="[$e|2]", label="spawn tac_loop/0.0"];
-	n_2 -> n_4 [id="[$e|1]", label="send tac to tic_loop/0.0"];
 	n_3 -> n_2 [id="[$e|0]", label="spawn tic_loop/0.0"];
+	n_2 -> n_4 [id="[$e|1]", label="send tac to tic_loop/0.0"];
 }
diff --git a/examples/ticktackloop/tac_loop_0_local_view.dot b/examples/ticktackloop/tac_loop_0_local_view.dot
index cc628e8..62d8931 100644
--- a/examples/ticktackloop/tac_loop_0_local_view.dot
+++ b/examples/ticktackloop/tac_loop_0_local_view.dot
@@ -7,8 +7,8 @@ digraph tac_loop_0 {
 	n_3 [id="4", shape=doublecircle, label="4"];
 	n_4 [id="3", shape=circle, label="2"];
 
-	n_2 -> n_1 [id="[$e|6]", label="send tac to tic_loop/0.0"];
 	n_4 -> n_3 [id="[$e|3]", label="send stop to tic_loop/0.0"];
-	n_1 -> n_2 [id="[$e|4]", label="receive tic"];
+	n_2 -> n_1 [id="[$e|6]", label="send tac to tic_loop/0.0"];
 	n_1 -> n_4 [id="[$e|0]", label="receive stop"];
+	n_1 -> n_2 [id="[$e|4]", label="receive tic"];
 }
diff --git a/examples/ticktackloop/tic_loop_0_local_view.dot b/examples/ticktackloop/tic_loop_0_local_view.dot
index 6e1ce0f..ab38518 100644
--- a/examples/ticktackloop/tic_loop_0_local_view.dot
+++ b/examples/ticktackloop/tic_loop_0_local_view.dot
@@ -9,6 +9,6 @@ digraph tic_loop_0 {
 
 	n_2 -> n_1 [id="[$e|6]", label="send tic to tac_loop/0.0"];
 	n_1 -> n_2 [id="[$e|2]", label="receive tac"];
-	n_4 -> n_3 [id="[$e|4]", label="send stop to tac_loop/0.0"];
 	n_1 -> n_4 [id="[$e|0]", label="receive stop"];
+	n_4 -> n_3 [id="[$e|4]", label="send stop to tac_loop/0.0"];
 }
diff --git a/examples/ticktackstop/start_0_global_view.dot b/examples/ticktackstop/start_0_global_view.dot
index 2f98ff8..2023104 100644
--- a/examples/ticktackstop/start_0_global_view.dot
+++ b/examples/ticktackstop/start_0_global_view.dot
@@ -13,16 +13,16 @@ digraph global {
 	n_9 [id="7", shape=circle, label="7"];
 	n_10 [id="3", shape=circle, label="3"];
 
-	n_3 -> n_7 [id="[$e|11]", label="tic_loop/0.0→tac_loop/0.0:stop"];
-	n_5 -> n_7 [id="[$e|10]", label="tic_loop/0.0→tac_loop/0.0:stop"];
-	n_2 -> n_7 [id="[$e|7]", label="tic_loop/0.0→tac_loop/0.0:stop"];
-	n_10 -> n_8 [id="[$e|2]", label="start/0.0Δrandom/0.0"];
-	n_8 -> n_1 [id="[$e|3]", label="start/0.0→tic_loop/0.0:tac"];
-	n_1 -> n_9 [id="[$e|5]", label="tic_loop/0.0→tac_loop/0.0:tic"];
-	n_1 -> n_2 [id="[$e|6]", label="random/0.0→tic_loop/0.0:stop"];
+	n_7 -> n_5 [id="[$e|8]", label="random/0.0→tic_loop/0.0:stop"];
+	n_2 -> n_7 [id="[$e|6]", label="tic_loop/0.0→tac_loop/0.0:tic"];
+	n_3 -> n_9 [id="[$e|11]", label="tic_loop/0.0→tac_loop/0.0:stop"];
+	n_1 -> n_9 [id="[$e|5]", label="tic_loop/0.0→tac_loop/0.0:stop"];
+	n_8 -> n_2 [id="[$e|4]", label="start/0.0→tic_loop/0.0:tac"];
+	n_5 -> n_9 [id="[$e|10]", label="tic_loop/0.0→tac_loop/0.0:stop"];
+	n_2 -> n_1 [id="[$e|7]", label="random/0.0→tic_loop/0.0:stop"];
 	n_6 -> n_10 [id="[$e|1]", label="start/0.0Δtic_loop/0.0"];
-	n_2 -> n_3 [id="[$e|9]", label="tic_loop/0.0→tac_loop/0.0:tic"];
+	n_1 -> n_3 [id="[$e|9]", label="tic_loop/0.0→tac_loop/0.0:tic"];
 	n_4 -> n_6 [id="[$e|0]", label="start/0.0Δtac_loop/0.0"];
-	n_8 -> n_2 [id="[$e|4]", label="random/0.0→tic_loop/0.0:stop"];
-	n_9 -> n_5 [id="[$e|8]", label="random/0.0→tic_loop/0.0:stop"];
+	n_8 -> n_1 [id="[$e|3]", label="random/0.0→tic_loop/0.0:stop"];
+	n_10 -> n_8 [id="[$e|2]", label="start/0.0Δrandom/0.0"];
 }
diff --git a/examples/ticktackstop/start_0_local_view.dot b/examples/ticktackstop/start_0_local_view.dot
index d287270..d387a07 100644
--- a/examples/ticktackstop/start_0_local_view.dot
+++ b/examples/ticktackstop/start_0_local_view.dot
@@ -8,8 +8,8 @@ digraph start_0 {
 	n_4 [id="4", shape=doublecircle, label="5"];
 	n_5 [id="3", shape=circle, label="2"];
 
-	n_5 -> n_1 [id="[$e|2]", label="spawn tic_loop/0.0"];
-	n_1 -> n_3 [id="[$e|3]", label="spawn random/0.0"];
 	n_2 -> n_5 [id="[$e|1]", label="spawn tac_loop/0.0"];
 	n_3 -> n_4 [id="[$e|0]", label="send tac to tic_loop/0.0"];
+	n_1 -> n_3 [id="[$e|3]", label="spawn random/0.0"];
+	n_5 -> n_1 [id="[$e|2]", label="spawn tic_loop/0.0"];
 }
diff --git a/examples/ticktackstop/tac_loop_0_local_view.dot b/examples/ticktackstop/tac_loop_0_local_view.dot
index d13a659..4715a2b 100644
--- a/examples/ticktackstop/tac_loop_0_local_view.dot
+++ b/examples/ticktackstop/tac_loop_0_local_view.dot
@@ -6,9 +6,9 @@ digraph tac_loop_0 {
 	n_2 [id="4", shape=doublecircle, label="3"];
 	n_3 [id="3", shape=circle, label="2"];
 
-	n_3 -> n_1 [id="[$e|7]", label="send tac to tic_loop/0.0"];
-	n_1 -> n_2 [id="[$e|3]", label="receive stop"];
-	n_3 -> n_3 [id="[$e|5]", label="receive tic"];
 	n_1 -> n_3 [id="[$e|6]", label="receive tic"];
+	n_3 -> n_3 [id="[$e|5]", label="receive tic"];
+	n_3 -> n_1 [id="[$e|7]", label="send tac to tic_loop/0.0"];
 	n_3 -> n_2 [id="[$e|1]", label="receive stop"];
+	n_1 -> n_2 [id="[$e|3]", label="receive stop"];
 }
diff --git a/examples/ticktackstop/tic_loop_0_local_view.dot b/examples/ticktackstop/tic_loop_0_local_view.dot
index f798171..9539e03 100644
--- a/examples/ticktackstop/tic_loop_0_local_view.dot
+++ b/examples/ticktackstop/tic_loop_0_local_view.dot
@@ -7,8 +7,8 @@ digraph tic_loop_0 {
 	n_3 [id="4", shape=doublecircle, label="4"];
 	n_4 [id="3", shape=circle, label="2"];
 
-	n_1 -> n_2 [id="[$e|2]", label="receive tac"];
 	n_2 -> n_1 [id="[$e|6]", label="send tic to tac_loop/0.0"];
-	n_1 -> n_4 [id="[$e|0]", label="receive stop"];
 	n_4 -> n_3 [id="[$e|4]", label="send stop to tac_loop/0.0"];
+	n_1 -> n_4 [id="[$e|0]", label="receive stop"];
+	n_1 -> n_2 [id="[$e|2]", label="receive tac"];
 }
diff --git a/examples/trick/a_0_local_view.dot b/examples/trick/a_0_local_view.dot
index 00074b9..a48da64 100644
--- a/examples/trick/a_0_local_view.dot
+++ b/examples/trick/a_0_local_view.dot
@@ -6,6 +6,6 @@ digraph a_0 {
 	n_2 [id="2", shape=circle, label="2"];
 	n_3 [id="3", shape=doublecircle, label="3"];
 
-	n_1 -> n_2 [id="[$e|1]", label="send v1 to c/0.0"];
 	n_2 -> n_3 [id="[$e|0]", label="send v2 to b/0.0"];
+	n_1 -> n_2 [id="[$e|1]", label="send v1 to c/0.0"];
 }
diff --git a/examples/trick/b_0_local_view.dot b/examples/trick/b_0_local_view.dot
index 8e3e9a3..8192571 100644
--- a/examples/trick/b_0_local_view.dot
+++ b/examples/trick/b_0_local_view.dot
@@ -6,6 +6,6 @@ digraph b_0 {
 	n_2 [id="2", shape=circle, label="2"];
 	n_3 [id="3", shape=doublecircle, label="3"];
 
-	n_2 -> n_3 [id="[$e|1]", label="send v2 to c/0.0"];
 	n_1 -> n_2 [id="[$e|0]", label="receive v2"];
+	n_2 -> n_3 [id="[$e|1]", label="send v2 to c/0.0"];
 }
diff --git a/examples/trick/c_0_local_view.dot b/examples/trick/c_0_local_view.dot
index d301c97..ab22b7e 100644
--- a/examples/trick/c_0_local_view.dot
+++ b/examples/trick/c_0_local_view.dot
@@ -6,6 +6,6 @@ digraph c_0 {
 	n_2 [id="2", shape=doublecircle, label="3"];
 	n_3 [id="3", shape=circle, label="2"];
 
-	n_3 -> n_2 [id="[$e|1]", label="receive v2"];
 	n_1 -> n_3 [id="[$e|0]", label="receive v1"];
+	n_3 -> n_2 [id="[$e|1]", label="receive v2"];
 }
diff --git a/examples/trick/main_0_global_view.dot b/examples/trick/main_0_global_view.dot
index c3ceb7d..8f51ff1 100644
--- a/examples/trick/main_0_global_view.dot
+++ b/examples/trick/main_0_global_view.dot
@@ -12,13 +12,13 @@ digraph global {
 	n_8 [id="7", shape=circle, label="7"];
 	n_9 [id="3", shape=circle, label="3"];
 
-	n_6 -> n_4 [id="[$e|8]", label="b/0.0→c/0.0:v2"];
-	n_2 -> n_6 [id="[$e|6]", label="a/0.0→b/0.0:v2"];
 	n_7 -> n_1 [id="[$e|3]", label="a/0.0→b/0.0:v2"];
+	n_2 -> n_6 [id="[$e|6]", label="a/0.0→b/0.0:v2"];
 	n_9 -> n_7 [id="[$e|2]", label="main/0.0Δc/0.0"];
-	n_1 -> n_8 [id="[$e|5]", label="a/0.0→c/0.0:v1"];
+	n_6 -> n_4 [id="[$e|8]", label="b/0.0→c/0.0:v2"];
+	n_3 -> n_5 [id="[$e|0]", label="main/0.0Δa/0.0"];
 	n_5 -> n_9 [id="[$e|1]", label="main/0.0Δb/0.0"];
-	n_7 -> n_2 [id="[$e|4]", label="a/0.0→c/0.0:v1"];
 	n_8 -> n_4 [id="[$e|7]", label="b/0.0→c/0.0:v2"];
-	n_3 -> n_5 [id="[$e|0]", label="main/0.0Δa/0.0"];
+	n_7 -> n_2 [id="[$e|4]", label="a/0.0→c/0.0:v1"];
+	n_1 -> n_8 [id="[$e|5]", label="a/0.0→c/0.0:v1"];
 }
diff --git a/examples/trick/main_0_local_view.dot b/examples/trick/main_0_local_view.dot
index 704266d..7014615 100644
--- a/examples/trick/main_0_local_view.dot
+++ b/examples/trick/main_0_local_view.dot
@@ -8,6 +8,6 @@ digraph main_0 {
 	n_4 [id="3", shape=doublecircle, label="4"];
 
 	n_2 -> n_3 [id="[$e|2]", label="spawn b/0.0"];
-	n_3 -> n_4 [id="[$e|1]", label="spawn c/0.0"];
 	n_1 -> n_2 [id="[$e|0]", label="spawn a/0.0"];
+	n_3 -> n_4 [id="[$e|1]", label="spawn c/0.0"];
 }
diff --git a/examples/violation/incrementer_0_local_view.dot b/examples/violation/incrementer_0_local_view.dot
index 0ebc7cd..8c02acf 100644
--- a/examples/violation/incrementer_0_local_view.dot
+++ b/examples/violation/incrementer_0_local_view.dot
@@ -10,10 +10,10 @@ digraph incrementer_0 {
 	n_6 [id="7", shape=circle, label="3"];
 	n_7 [id="3", shape=circle, label="4"];
 
-	n_6 -> n_7 [id="[$e|4]", label="send {read,pid_self} to varManager/1.0"];
-	n_2 -> n_5 [id="[$e|1]", label="send {write,unknown} to varManager/1.0"];
-	n_5 -> n_1 [id="[$e|3]", label="send {release} to meManager/0.0"];
 	n_4 -> n_6 [id="[$e|0]", label="receive answer"];
 	n_7 -> n_2 [id="[$e|2]", label="receive X"];
+	n_5 -> n_1 [id="[$e|3]", label="send {release} to meManager/0.0"];
+	n_6 -> n_7 [id="[$e|4]", label="send {read,pid_self} to varManager/1.0"];
+	n_2 -> n_5 [id="[$e|1]", label="send {write,unknown} to varManager/1.0"];
 	n_3 -> n_4 [id="[$e|5]", label="send {request,pid_self} to meManager/0.0"];
 }
diff --git a/examples/violation/main_0_global_view.dot b/examples/violation/main_0_global_view.dot
index 8db9a52..8e3f20c 100644
--- a/examples/violation/main_0_global_view.dot
+++ b/examples/violation/main_0_global_view.dot
@@ -31,54 +31,54 @@ digraph global {
 	n_27 [id="3", shape=circle, label="3"];
 	n_28 [id="16", shape=circle, label="16"];
 
-	n_4 -> n_2 [id="[$e|39]", label="incrementer/0.1→meManager/0.0:{release}"];
-	n_17 -> n_9 [id="[$e|11]", label="varManager/1.0→incrementer/0.1:Val"];
-	n_11 -> n_13 [id="[$e|22]", label="incrementer/0.0→varManager/1.0:{write,unknown}"];
-	n_5 -> n_14 [id="[$e|4]", label="incrementer/0.0→meManager/0.0:{request,pid_self}"];
-	n_4 -> n_6 [id="[$e|40]", label="incrementer/0.0→varManager/1.0:{write,unknown}"];
-	n_22 -> n_27 [id="[$e|1]", label="main/0.0ΔvarManager/1.0"];
-	n_20 -> n_6 [id="[$e|44]", label="incrementer/0.1→varManager/1.0:{write,unknown}"];
-	n_25 -> n_5 [id="[$e|3]", label="main/0.0Δincrementer/0.1"];
-	n_15 -> n_15 [id="[$e|17]", label="incrementer/0.0→varManager/1.0:{write,unknown}"];
-	n_13 -> n_8 [id="[$e|26]", label="meManager/0.0→incrementer/0.1:answer"];
-	n_1 -> n_16 [id="[$e|31]", label="incrementer/0.0→varManager/1.0:{read,pid_self}"];
-	n_13 -> n_15 [id="[$e|18]", label="incrementer/0.0→meManager/0.0:{release}"];
-	n_6 -> n_2 [id="[$e|46]", label="incrementer/0.1→meManager/0.0:{release}"];
+	n_15 -> n_11 [id="[$e|16]", label="incrementer/0.1→meManager/0.0:{request,pid_self}"];
+	n_19 -> n_22 [id="[$e|0]", label="main/0.0ΔmeManager/0.0"];
+	n_10 -> n_15 [id="[$e|12]", label="incrementer/0.0→meManager/0.0:{release}"];
+	n_28 -> n_1 [id="[$e|31]", label="meManager/0.0→incrementer/0.0:answer"];
+	n_3 -> n_16 [id="[$e|35]", label="incrementer/0.0→varManager/1.0:{read,pid_self}"];
+	n_16 -> n_3 [id="[$e|37]", label="incrementer/0.1→varManager/1.0:{write,unknown}"];
+	n_1 -> n_16 [id="[$e|30]", label="incrementer/0.0→varManager/1.0:{read,pid_self}"];
 	n_26 -> n_21 [id="[$e|8]", label="incrementer/0.0→varManager/1.0:{read,pid_self}"];
+	n_1 -> n_3 [id="[$e|29]", label="incrementer/0.1→varManager/1.0:{write,unknown}"];
 	n_24 -> n_17 [id="[$e|9]", label="incrementer/0.1→varManager/1.0:{read,pid_self}"];
-	n_4 -> n_6 [id="[$e|41]", label="incrementer/0.1→varManager/1.0:{write,unknown}"];
-	n_8 -> n_18 [id="[$e|28]", label="incrementer/0.1→varManager/1.0:{read,pid_self}"];
-	n_10 -> n_15 [id="[$e|12]", label="incrementer/0.0→meManager/0.0:{release}"];
-	n_10 -> n_13 [id="[$e|13]", label="incrementer/0.0→varManager/1.0:{write,unknown}"];
-	n_14 -> n_26 [id="[$e|6]", label="meManager/0.0→incrementer/0.0:answer"];
-	n_14 -> n_24 [id="[$e|7]", label="meManager/0.0→incrementer/0.1:answer"];
+	n_23 -> n_18 [id="[$e|32]", label="incrementer/0.1→varManager/1.0:{read,pid_self}"];
+	n_20 -> n_2 [id="[$e|42]", label="incrementer/0.0→meManager/0.0:{release}"];
 	n_9 -> n_7 [id="[$e|14]", label="incrementer/0.1→meManager/0.0:{release}"];
-	n_6 -> n_6 [id="[$e|48]", label="incrementer/0.0→varManager/1.0:{write,unknown}"];
-	n_6 -> n_6 [id="[$e|47]", label="incrementer/0.1→varManager/1.0:{write,unknown}"];
-	n_20 -> n_2 [id="[$e|43]", label="incrementer/0.0→meManager/0.0:{release}"];
-	n_20 -> n_6 [id="[$e|45]", label="incrementer/0.0→varManager/1.0:{write,unknown}"];
-	n_7 -> n_7 [id="[$e|20]", label="incrementer/0.1→varManager/1.0:{write,unknown}"];
-	n_1 -> n_3 [id="[$e|30]", label="incrementer/0.1→varManager/1.0:{write,unknown}"];
+	n_27 -> n_25 [id="[$e|2]", label="main/0.0Δincrementer/0.0"];
+	n_4 -> n_6 [id="[$e|39]", label="incrementer/0.0→varManager/1.0:{write,unknown}"];
 	n_28 -> n_7 [id="[$e|21]", label="incrementer/0.1→meManager/0.0:{release}"];
-	n_8 -> n_23 [id="[$e|27]", label="incrementer/0.0→varManager/1.0:{write,unknown}"];
-	n_19 -> n_22 [id="[$e|0]", label="main/0.0ΔmeManager/0.0"];
+	n_20 -> n_6 [id="[$e|43]", label="incrementer/0.1→varManager/1.0:{write,unknown}"];
+	n_14 -> n_26 [id="[$e|6]", label="meManager/0.0→incrementer/0.0:answer"];
+	n_4 -> n_2 [id="[$e|38]", label="incrementer/0.1→meManager/0.0:{release}"];
+	n_20 -> n_6 [id="[$e|44]", label="incrementer/0.0→varManager/1.0:{write,unknown}"];
+	n_12 -> n_1 [id="[$e|24]", label="meManager/0.0→incrementer/0.0:answer"];
+	n_3 -> n_20 [id="[$e|45]", label="varManager/1.0→incrementer/0.0:Val"];
+	n_18 -> n_4 [id="[$e|33]", label="varManager/1.0→incrementer/0.1:Val"];
+	n_14 -> n_24 [id="[$e|7]", label="meManager/0.0→incrementer/0.1:answer"];
+	n_11 -> n_13 [id="[$e|23]", label="incrementer/0.0→varManager/1.0:{write,unknown}"];
 	n_7 -> n_12 [id="[$e|19]", label="incrementer/0.0→meManager/0.0:{request,pid_self}"];
-	n_12 -> n_28 [id="[$e|24]", label="incrementer/0.1→varManager/1.0:{write,unknown}"];
-	n_15 -> n_11 [id="[$e|16]", label="incrementer/0.1→meManager/0.0:{request,pid_self}"];
-	n_9 -> n_28 [id="[$e|15]", label="incrementer/0.1→varManager/1.0:{write,unknown}"];
-	n_12 -> n_1 [id="[$e|25]", label="meManager/0.0→incrementer/0.0:answer"];
-	n_23 -> n_18 [id="[$e|32]", label="incrementer/0.1→varManager/1.0:{read,pid_self}"];
-	n_27 -> n_25 [id="[$e|2]", label="main/0.0Δincrementer/0.0"];
-	n_23 -> n_4 [id="[$e|38]", label="varManager/1.0→incrementer/0.1:Val"];
-	n_28 -> n_1 [id="[$e|29]", label="meManager/0.0→incrementer/0.0:answer"];
-	n_3 -> n_20 [id="[$e|42]", label="varManager/1.0→incrementer/0.0:Val"];
-	n_5 -> n_14 [id="[$e|5]", label="incrementer/0.1→meManager/0.0:{request,pid_self}"];
+	n_8 -> n_23 [id="[$e|26]", label="incrementer/0.0→varManager/1.0:{write,unknown}"];
+	n_7 -> n_7 [id="[$e|20]", label="incrementer/0.1→varManager/1.0:{write,unknown}"];
 	n_21 -> n_10 [id="[$e|10]", label="varManager/1.0→incrementer/0.0:Val"];
-	n_16 -> n_20 [id="[$e|37]", label="varManager/1.0→incrementer/0.0:Val"];
-	n_16 -> n_3 [id="[$e|36]", label="incrementer/0.1→varManager/1.0:{write,unknown}"];
-	n_11 -> n_8 [id="[$e|23]", label="meManager/0.0→incrementer/0.1:answer"];
+	n_16 -> n_20 [id="[$e|36]", label="varManager/1.0→incrementer/0.0:Val"];
+	n_10 -> n_13 [id="[$e|13]", label="incrementer/0.0→varManager/1.0:{write,unknown}"];
+	n_17 -> n_9 [id="[$e|11]", label="varManager/1.0→incrementer/0.1:Val"];
+	n_25 -> n_5 [id="[$e|3]", label="main/0.0Δincrementer/0.1"];
+	n_5 -> n_14 [id="[$e|4]", label="incrementer/0.0→meManager/0.0:{request,pid_self}"];
 	n_6 -> n_2 [id="[$e|49]", label="incrementer/0.0→meManager/0.0:{release}"];
-	n_18 -> n_4 [id="[$e|34]", label="varManager/1.0→incrementer/0.1:Val"];
-	n_3 -> n_16 [id="[$e|35]", label="incrementer/0.0→varManager/1.0:{read,pid_self}"];
-	n_18 -> n_23 [id="[$e|33]", label="incrementer/0.0→varManager/1.0:{write,unknown}"];
+	n_6 -> n_2 [id="[$e|46]", label="incrementer/0.1→meManager/0.0:{release}"];
+	n_15 -> n_15 [id="[$e|17]", label="incrementer/0.0→varManager/1.0:{write,unknown}"];
+	n_8 -> n_18 [id="[$e|27]", label="incrementer/0.1→varManager/1.0:{read,pid_self}"];
+	n_18 -> n_23 [id="[$e|34]", label="incrementer/0.0→varManager/1.0:{write,unknown}"];
+	n_13 -> n_15 [id="[$e|18]", label="incrementer/0.0→meManager/0.0:{release}"];
+	n_4 -> n_6 [id="[$e|40]", label="incrementer/0.1→varManager/1.0:{write,unknown}"];
+	n_9 -> n_28 [id="[$e|15]", label="incrementer/0.1→varManager/1.0:{write,unknown}"];
+	n_11 -> n_8 [id="[$e|22]", label="meManager/0.0→incrementer/0.1:answer"];
+	n_22 -> n_27 [id="[$e|1]", label="main/0.0ΔvarManager/1.0"];
+	n_13 -> n_8 [id="[$e|28]", label="meManager/0.0→incrementer/0.1:answer"];
+	n_23 -> n_4 [id="[$e|41]", label="varManager/1.0→incrementer/0.1:Val"];
+	n_12 -> n_28 [id="[$e|25]", label="incrementer/0.1→varManager/1.0:{write,unknown}"];
+	n_5 -> n_14 [id="[$e|5]", label="incrementer/0.1→meManager/0.0:{request,pid_self}"];
+	n_6 -> n_6 [id="[$e|47]", label="incrementer/0.1→varManager/1.0:{write,unknown}"];
+	n_6 -> n_6 [id="[$e|48]", label="incrementer/0.0→varManager/1.0:{write,unknown}"];
 }
diff --git a/examples/violation/main_0_local_view.dot b/examples/violation/main_0_local_view.dot
index 5eca4db..b27d6f3 100644
--- a/examples/violation/main_0_local_view.dot
+++ b/examples/violation/main_0_local_view.dot
@@ -8,8 +8,8 @@ digraph main_0 {
 	n_4 [id="4", shape=doublecircle, label="5"];
 	n_5 [id="3", shape=circle, label="4"];
 
-	n_2 -> n_3 [id="[$e|1]", label="spawn meManager/0.0"];
-	n_1 -> n_5 [id="[$e|3]", label="spawn incrementer/0.0"];
 	n_5 -> n_4 [id="[$e|0]", label="spawn incrementer/0.1"];
 	n_3 -> n_1 [id="[$e|2]", label="spawn varManager/1.0"];
+	n_1 -> n_5 [id="[$e|3]", label="spawn incrementer/0.0"];
+	n_2 -> n_3 [id="[$e|1]", label="spawn meManager/0.0"];
 }
diff --git a/examples/violation/meManager_0_local_view.dot b/examples/violation/meManager_0_local_view.dot
index 6f96ef3..4a198a1 100644
--- a/examples/violation/meManager_0_local_view.dot
+++ b/examples/violation/meManager_0_local_view.dot
@@ -6,7 +6,7 @@ digraph meManager_0 {
 	n_2 [id="2", shape=circle, label="2"];
 	n_3 [id="3", shape=circle, label="3"];
 
+	n_1 -> n_2 [id="[$e|2]", label="receive {request,Pid}"];
 	n_3 -> n_1 [id="[$e|4]", label="receive {release}"];
 	n_2 -> n_3 [id="[$e|1]", label="send answer to Pid"];
-	n_1 -> n_2 [id="[$e|2]", label="receive {request,Pid}"];
 }
diff --git a/examples/violation/varManager_1_local_view.dot b/examples/violation/varManager_1_local_view.dot
index d89cbb7..213d5f4 100644
--- a/examples/violation/varManager_1_local_view.dot
+++ b/examples/violation/varManager_1_local_view.dot
@@ -5,7 +5,7 @@ digraph varManager_1 {
 	n_0 -> n_1 [arrowhead=none];
 	n_2 [id="4", shape=circle, label="2"];
 
-	n_1 -> n_1 [id="[$e|7]", label="receive {write,NewVal}"];
 	n_1 -> n_2 [id="[$e|0]", label="receive {read,Pid}"];
+	n_1 -> n_1 [id="[$e|7]", label="receive {write,NewVal}"];
 	n_2 -> n_1 [id="[$e|10]", label="send Val to Pid"];
 }
diff --git a/test.py b/test.py
index c37ec4a..0c45779 100755
--- a/test.py
+++ b/test.py
@@ -24,6 +24,10 @@
     ("./examples/test/foo5/foo5.erl","test/0","examples/test/foo5"),
     ("./examples/test/foo6/foo6.erl","test/0","examples/test/foo6"),
     ("./examples/test/ping/ping.erl","start/0","examples/test/ping"),
+    ("./examples/cauder_suite/airline/airline.erl","main/0","examples/cauder_suite/airline"),
+    ("./examples/cauder_suite/barber/barber.erl","main/0","examples/cauder_suite/barber"),
+    ("./examples/cauder_suite/meViolation/meViolation.erl","main/0","examples/cauder_suite/meViolation"),
+    ("./examples/cauder_suite/purchase/purchase.erl","main/0","examples/cauder_suite/purchase"),
 ]
 
 os.system("rebar3 escriptize")