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/README.md b/examples/cauder_suite/airline/README.md
new file mode 100644
index 0000000..8df0b27
--- /dev/null
+++ b/examples/cauder_suite/airline/README.md
@@ -0,0 +1,7 @@
+# Airline example
+
+## Usage
+
+```bash
+./_build/default/bin/chorer ./examples/cauder_suite/airline/airline.erl main/0 ./examples/cauder_suite/airline
+```
\ No newline at end of file
diff --git a/examples/cauder_suite/airline/agent_2_local_view.dot b/examples/cauder_suite/airline/agent_2_local_view.dot
new file mode 100644
index 0000000..08be83a
--- /dev/null
+++ b/examples/cauder_suite/airline/agent_2_local_view.dot
@@ -0,0 +1,18 @@
+digraph agent_2 {
+	rankdir="LR";
+	n_0 [label="agent_2", shape="plaintext"];
+	n_1 [id="5", shape=doublecircle, label="6"];
+	n_2 [id="6", shape=circle, label="3"];
+	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="5"];
+
+	n_4 -> n_5 [id="[$e|3]", label="receive {seats,0}"];
+	n_4 -> n_2 [id="[$e|1]", label="receive {seats,Num}"];
+	n_3 -> n_4 [id="[$e|6]", label="send {numOfSeats,pid_self} to Pid"];
+	n_6 -> n_3 [id="[$e|7]", label="receive {booked,_}"];
+	n_5 -> n_1 [id="[$e|2]", label="send stop to Pid"];
+	n_2 -> n_6 [id="[$e|5]", label="send {sell,pid_self} to Pid"];
+}
diff --git a/examples/cauder_suite/airline/airline.erl b/examples/cauder_suite/airline/airline.erl
new file mode 100755
index 0000000..93130b9
--- /dev/null
+++ b/examples/cauder_suite/airline/airline.erl
@@ -0,0 +1,32 @@
+-module(airline).
+-export([main/0, agent/2]).
+
+main() ->
+    Main = self(),
+    spawn(?MODULE, agent, [1, 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);
+        stop ->
+            done
+    end.
+
+agent(NAg, Pid) ->
+    Pid ! {numOfSeats, self()},
+    receive
+        {seats, Num} when Num > 0 ->
+            Pid ! {sell, self()},
+            receive
+                {booked, _} -> agent(NAg, Pid)
+            end;
+        {seats, 0} ->
+            Pid ! stop
+    end.
diff --git a/examples/cauder_suite/airline/main_0_global_view.dot b/examples/cauder_suite/airline/main_0_global_view.dot
new file mode 100644
index 0000000..b9df23c
--- /dev/null
+++ b/examples/cauder_suite/airline/main_0_global_view.dot
@@ -0,0 +1,16 @@
+digraph global {
+	rankdir="LR";
+	n_0 [label="global", shape="plaintext"];
+	n_1 [id="5", shape=circle, label="5"];
+	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_4 -> n_1 [id="[$e|3]", label="agent/2.0→main/0.0:{sell,pid_self}"];
+	n_3 -> n_5 [id="[$e|1]", label="agent/2.0→main/0.0:{numOfSeats,pid_self}"];
+	n_1 -> n_3 [id="[$e|4]", label="main/0.0→agent/2.0:{booked,Num}"];
+	n_5 -> n_4 [id="[$e|2]", label="main/0.0→agent/2.0:{seats,Num}"];
+	n_2 -> n_3 [id="[$e|0]", label="main/0.0Δagent/2.0"];
+}
diff --git a/examples/cauder_suite/airline/main_0_local_view.dot b/examples/cauder_suite/airline/main_0_local_view.dot
new file mode 100644
index 0000000..deb170c
--- /dev/null
+++ b/examples/cauder_suite/airline/main_0_local_view.dot
@@ -0,0 +1,17 @@
+digraph main_0 {
+	rankdir="LR";
+	n_0 [label="main_0", shape="plaintext"];
+	n_1 [id="5", 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=doublecircle, label="4"];
+	n_5 [id="7", shape=circle, label="5"];
+
+	n_1 -> n_3 [id="[$e|12]", label="send {seats,Num} to Pid"];
+	n_5 -> n_3 [id="[$e|8]", label="send {booked,Num} to Pid"];
+	n_3 -> n_1 [id="[$e|1]", label="receive {numOfSeats,Pid}"];
+	n_3 -> n_5 [id="[$e|7]", label="receive {sell,Pid}"];
+	n_3 -> n_4 [id="[$e|5]", label="receive stop"];
+	n_2 -> n_3 [id="[$e|13]", label="spawn agent/2.0"];
+}
diff --git a/examples/cauder_suite/barber/README.md b/examples/cauder_suite/barber/README.md
new file mode 100644
index 0000000..0c9ce85
--- /dev/null
+++ b/examples/cauder_suite/barber/README.md
@@ -0,0 +1,7 @@
+# barber example
+
+## Usage
+
+```bash
+./_build/default/bin/chorer ./examples/cauder_suite/barber/barber.erl main/0 ./examples/cauder_suite/barber
+```
\ No newline at end of file
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..2694740
--- /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_7 -> n_1 [id="[$e|4]", label="receive {Name1,State1}"];
+	n_3 -> n_4 [id="[$e|1]", label="spawn open_barber_shop/0.0"];
+	n_4 -> n_6 [id="[$e|0]", label="spawn customer/3.0"];
+	n_1 -> n_2 [id="[$e|5]", label="receive {Name2,State2}"];
+	n_6 -> n_7 [id="[$e|3]", label="spawn customer/3.1"];
+	n_2 -> n_5 [id="[$e|2]", label="send stop to open_barber_shop/0.0"];
+}
diff --git a/examples/cauder_suite/meViolation/README.md b/examples/cauder_suite/meViolation/README.md
new file mode 100644
index 0000000..c71d691
--- /dev/null
+++ b/examples/cauder_suite/meViolation/README.md
@@ -0,0 +1,7 @@
+# Violation example
+
+## Use
+
+```bash
+./_build/default/bin/chorer ./examples/cauder_suite/meViolation/meViolation.erl main/0 examples/cauder_suite/meViolation
+```
\ No newline at end of file
diff --git a/examples/cauder_suite/meViolation/incrementer_0_local_view.dot b/examples/cauder_suite/meViolation/incrementer_0_local_view.dot
new file mode 100644
index 0000000..0ebc7cd
--- /dev/null
+++ b/examples/cauder_suite/meViolation/incrementer_0_local_view.dot
@@ -0,0 +1,19 @@
+digraph incrementer_0 {
+	rankdir="LR";
+	n_0 [label="incrementer_0", shape="plaintext"];
+	n_1 [id="5", shape=doublecircle, label="7"];
+	n_2 [id="6", shape=circle, label="5"];
+	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="6"];
+	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_3 -> n_4 [id="[$e|5]", label="send {request,pid_self} to meManager/0.0"];
+}
diff --git a/examples/cauder_suite/meViolation/main_0_global_view.dot b/examples/cauder_suite/meViolation/main_0_global_view.dot
new file mode 100644
index 0000000..8db9a52
--- /dev/null
+++ b/examples/cauder_suite/meViolation/main_0_global_view.dot
@@ -0,0 +1,84 @@
+digraph global {
+	rankdir="LR";
+	n_0 [label="global", shape="plaintext"];
+	n_1 [id="20", shape=circle, label="20"];
+	n_2 [id="27", shape=circle, label="27"];
+	n_3 [id="23", shape=circle, label="23"];
+	n_4 [id="25", shape=circle, label="25"];
+	n_5 [id="5", shape=circle, label="5"];
+	n_6 [id="28", shape=circle, label="28"];
+	n_7 [id="15", shape=circle, label="15"];
+	n_8 [id="19", shape=circle, label="19"];
+	n_9 [id="12", shape=circle, label="12"];
+	n_10 [id="11", shape=circle, label="11"];
+	n_11 [id="17", shape=circle, label="17"];
+	n_12 [id="18", shape=circle, label="18"];
+	n_13 [id="14", shape=circle, label="14"];
+	n_14 [id="6", shape=circle, label="6"];
+	n_15 [id="13", shape=circle, label="13"];
+	n_16 [id="24", shape=circle, label="24"];
+	n_17 [id="10", shape=circle, label="10"];
+	n_18 [id="22", shape=circle, label="22"];
+	n_19 [id="1", shape=circle, label="1"];
+	n_0 -> n_19 [arrowhead=none];
+	n_20 [id="26", shape=circle, label="26"];
+	n_21 [id="9", shape=circle, label="9"];
+	n_22 [id="2", shape=circle, label="2"];
+	n_23 [id="21", shape=circle, label="21"];
+	n_24 [id="8", shape=circle, label="8"];
+	n_25 [id="4", shape=circle, label="4"];
+	n_26 [id="7", shape=circle, label="7"];
+	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_26 -> n_21 [id="[$e|8]", label="incrementer/0.0→varManager/1.0:{read,pid_self}"];
+	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_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_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_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_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_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}"];
+}
diff --git a/examples/cauder_suite/meViolation/main_0_local_view.dot b/examples/cauder_suite/meViolation/main_0_local_view.dot
new file mode 100644
index 0000000..5eca4db
--- /dev/null
+++ b/examples/cauder_suite/meViolation/main_0_local_view.dot
@@ -0,0 +1,15 @@
+digraph main_0 {
+	rankdir="LR";
+	n_0 [label="main_0", shape="plaintext"];
+	n_1 [id="5", 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=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"];
+}
diff --git a/examples/cauder_suite/meViolation/meManager_0_local_view.dot b/examples/cauder_suite/meViolation/meManager_0_local_view.dot
new file mode 100644
index 0000000..6f96ef3
--- /dev/null
+++ b/examples/cauder_suite/meViolation/meManager_0_local_view.dot
@@ -0,0 +1,12 @@
+digraph meManager_0 {
+	rankdir="LR";
+	n_0 [label="meManager_0", shape="plaintext"];
+	n_1 [id="1", shape=circle, label="1"];
+	n_0 -> n_1 [arrowhead=none];
+	n_2 [id="2", shape=circle, label="2"];
+	n_3 [id="3", shape=circle, label="3"];
+
+	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/cauder_suite/meViolation/meViolation.erl b/examples/cauder_suite/meViolation/meViolation.erl
new file mode 100755
index 0000000..60bc413
--- /dev/null
+++ b/examples/cauder_suite/meViolation/meViolation.erl
@@ -0,0 +1,42 @@
+%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/0]).
+
+main() ->
+    MePid = spawn(?MODULE, meManager, []),
+    XPid = spawn(?MODULE, varManager, [0]),
+    register(xx, XPid),
+    register(mm, MePid),
+    spawn(?MODULE, incrementer, []),
+    spawn(?MODULE, incrementer, []).
+
+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() ->
+    mm ! {request, self()},
+    receive
+        answer ->
+            xx ! {read, self()},
+            receive
+                X ->
+                    xx ! {write, X + 1},
+                    mm ! {release}
+            end
+    end.
diff --git a/examples/cauder_suite/meViolation/varManager_1_local_view.dot b/examples/cauder_suite/meViolation/varManager_1_local_view.dot
new file mode 100644
index 0000000..d89cbb7
--- /dev/null
+++ b/examples/cauder_suite/meViolation/varManager_1_local_view.dot
@@ -0,0 +1,11 @@
+digraph varManager_1 {
+	rankdir="LR";
+	n_0 [label="varManager_1", shape="plaintext"];
+	n_1 [id="1", shape=circle, label="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_2 -> n_1 [id="[$e|10]", label="send Val to Pid"];
+}
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.erl b/examples/customer/customer.erl
index fa77ee2..f7a2e93 100644
--- a/examples/customer/customer.erl
+++ b/examples/customer/customer.erl
@@ -2,11 +2,11 @@
 -export([main/0, customer/0, store/0, customer_dummy/0]).
 
 customer_dummy() ->
-    store ! ciaooooo,
+    store ! ciao,
     customer().
 customer() ->
     store ! item,
-    %%% Simulazione della decisione di un utente
+    %%% Simulation of a user decition
     Done = true,
     case Done of
         true ->
@@ -27,7 +27,7 @@ purchase() ->
 store() ->
     receive
         item ->
-            io:fwrite("richiesta ricevuta~n"),
+            io:fwrite("Request received~n"),
             receive
                 buy -> payment();
                 more -> store()
@@ -37,7 +37,7 @@ store() ->
 payment() ->
     receive
         payment ->
-            %%% Simulazione del esito del pagamento
+            %%% Simulation of a payment
             PaymentDone = true,
             case PaymentDone of
                 true ->
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 8d743fa..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_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_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_4 -> n_2 [id="[$e|8]", label="send payment to store/0.0"];
-	n_3 -> n_1 [id="[$e|2]", label="send ciaooooo to store/0.0"];
-	n_5 -> n_4 [id="[$e|10]", label="send buy to store/0.0"];
-	n_2 -> n_6 [id="[$e|1]", label="receive accepted"];
+	n_2 -> n_6 [id="[$e|2]", label="receive accepted"];
+	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/producer/README.md b/examples/producer/README.md
new file mode 100644
index 0000000..f4df247
--- /dev/null
+++ b/examples/producer/README.md
@@ -0,0 +1,12 @@
+# Customer example
+
+## Usage
+
+```bash
+./_build/default/bin/chorer ./examples/producer/producer.erl main/0 ./examples/producer
+```
+
+## Description
+
+
+## Results
diff --git a/examples/producer/consumer_0_local_view.dot b/examples/producer/consumer_0_local_view.dot
new file mode 100644
index 0000000..4de5b84
--- /dev/null
+++ b/examples/producer/consumer_0_local_view.dot
@@ -0,0 +1,23 @@
+digraph consumer_0 {
+	rankdir="LR";
+	n_0 [label="consumer_0", shape="plaintext"];
+	n_1 [id="5", shape=circle, label="3"];
+	n_2 [id="6", shape=circle, label="4"];
+	n_3 [id="1", shape=circle, label="1"];
+	n_0 -> n_3 [arrowhead=none];
+	n_4 [id="9", shape=circle, label="2"];
+	n_5 [id="2", shape=circle, label="5"];
+	n_6 [id="8", shape=circle, label="7"];
+	n_7 [id="4", shape=doublecircle, label="9"];
+	n_8 [id="7", shape=circle, label="6"];
+	n_9 [id="3", shape=circle, label="8"];
+
+	n_3 -> n_4 [id="[$e|0]", label="send {req,pid_self} to producer/0.0"];
+	n_1 -> n_2 [id="[$e|7]", label="send {req,pid_self} to producer/0.0"];
+	n_2 -> n_5 [id="[$e|1]", label="receive D"];
+	n_5 -> n_8 [id="[$e|2]", label="send {req,pid_self} to producer/0.0"];
+	n_9 -> n_7 [id="[$e|3]", label="receive D"];
+	n_8 -> n_6 [id="[$e|4]", label="receive D"];
+	n_4 -> n_1 [id="[$e|6]", label="receive D"];
+	n_6 -> n_9 [id="[$e|5]", label="send {req,pid_self} to producer/0.0"];
+}
diff --git a/examples/producer/main_0_global_view.dot b/examples/producer/main_0_global_view.dot
new file mode 100644
index 0000000..1d08564
--- /dev/null
+++ b/examples/producer/main_0_global_view.dot
@@ -0,0 +1,17 @@
+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_3 -> n_4 [id="[$e|0]", label="main/0.0Δproducer/0.0"];
+	n_4 -> n_6 [id="[$e|1]", label="main/0.0Δconsumer/0.0"];
+	n_6 -> n_5 [id="[$e|2]", label="consumer/0.0→producer/0.0:{req,pid_self}"];
+	n_5 -> n_1 [id="[$e|3]", label="producer/0.0→consumer/0.0:item"];
+	n_1 -> n_2 [id="[$e|4]", label="consumer/0.0→producer/0.0:{req,pid_self}"];
+}
diff --git a/examples/producer/main_0_local_view.dot b/examples/producer/main_0_local_view.dot
new file mode 100644
index 0000000..4cd3948
--- /dev/null
+++ b/examples/producer/main_0_local_view.dot
@@ -0,0 +1,11 @@
+digraph main_0 {
+	rankdir="LR";
+	n_0 [label="main_0", shape="plaintext"];
+	n_1 [id="1", shape=circle, label="1"];
+	n_0 -> n_1 [arrowhead=none];
+	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 consumer/0.0"];
+	n_1 -> n_2 [id="[$e|1]", label="spawn producer/0.0"];
+}
diff --git a/examples/producer/producer.erl b/examples/producer/producer.erl
new file mode 100644
index 0000000..f6fa634
--- /dev/null
+++ b/examples/producer/producer.erl
@@ -0,0 +1,30 @@
+-module(producer).
+-export([main/0, consumer/0, producer/0]).
+
+recv() ->
+    receive
+        D -> D
+    end.
+
+consumer() ->
+    S = self(),
+    producer ! {req, S},
+    recv(),
+    producer ! {req, S},
+    recv(),
+    producer ! {req, S},
+    recv(),
+    producer ! {req, S},
+    recv().
+
+producer() ->
+    receive
+        {req, P} ->
+            P ! item,
+            producer()
+    end.
+
+main() ->
+    Prd = spawn(?MODULE, producer, []),
+    register(producer, Prd),
+    spawn(?MODULE, consumer, []).
diff --git a/examples/producer/producer_0_local_view.dot b/examples/producer/producer_0_local_view.dot
new file mode 100644
index 0000000..13150f4
--- /dev/null
+++ b/examples/producer/producer_0_local_view.dot
@@ -0,0 +1,12 @@
+digraph producer_0 {
+	rankdir="LR";
+	n_0 [label="producer_0", shape="plaintext"];
+	n_1 [id="1", shape=circle, label="1"];
+	n_0 -> n_1 [arrowhead=none];
+	n_2 [id="2", shape=circle, label="2"];
+	n_3 [id="3", shape=circle, label="3"];
+
+	n_1 -> n_2 [id="[$e|0]", label="receive {req,P}"];
+	n_3 -> n_2 [id="[$e|1]", label="receive {req,P}"];
+	n_2 -> n_3 [id="[$e|2]", label="send item to P"];
+}
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/src/choreography/actor_emul.erl b/src/choreography/actor_emul.erl
index 8638449..6caed54 100644
--- a/src/choreography/actor_emul.erl
+++ b/src/choreography/actor_emul.erl
@@ -19,7 +19,8 @@
     set_proc_data/2,
     get_proc_mess_queue/1,
     add_proc_mess_queue/2,
-    del_proc_mess_queue/2
+    del_proc_mess_queue/2,
+    empty_filter_proc/1
 ]).
 
 %%%===================================================================
@@ -70,6 +71,10 @@ add_proc_mess_queue(P, M) -> P ! {add_mess_queue, M}.
 %%% Delete a message from the message queue of the process.
 del_proc_mess_queue(P, M) -> P ! {del_mess_queue, M}.
 
+%%% @doc
+%%% Delete process filters
+empty_filter_proc(P) -> P ! {empty_filters}.
+
 %%% @doc
 %%% Loop function to simulate a process.
 proc_loop(Data) ->
@@ -91,34 +96,37 @@ proc_loop(Data) ->
             %% APPROX: filter out edges used two times
             case EL of
                 [] ->
-                    P ! {{final_state, []}};
+                    P ! {final_state, []};
                 _ ->
                     ERet = filter_marked_edges(EL, SecondMarkedE),
-                    P ! {{filtered, ERet}}
+                    P ! {filtered, ERet}
             end,
             proc_loop(Data);
         {P, get_edge_info, E} ->
-            P ! {digraph:edge(G, E)},
+            P ! digraph:edge(G, E),
             proc_loop(Data);
         {P, get_data} ->
-            P ! {Data},
+            P ! Data,
             proc_loop(Data);
         {set_data, NewData} ->
             proc_loop(NewData);
         {P, get_local_vars} ->
-            P ! {sets:to_list(LocalVars)},
+            P ! sets:to_list(LocalVars),
             proc_loop(Data);
         {add_spawn_var, V} ->
             proc_loop(Data#actor_info{spawn_vars = sets:add_element(V, SpawnVars)});
         {add_local_var, V} ->
+            io:fwrite("local v~p~n", [Data#actor_info.local_vars]),
             proc_loop(Data#actor_info{local_vars = sets:add_element(V, LocalVars)});
         {P, get_mess_queue} ->
-            P ! {MessageQueue},
+            P ! MessageQueue,
             proc_loop(Data);
         {add_mess_queue, M} ->
             proc_loop(Data#actor_info{message_queue = MessageQueue ++ [M]});
         {del_mess_queue, M} ->
             proc_loop(Data#actor_info{message_queue = lists:delete(M, MessageQueue)});
+        {empty_filters} ->
+            proc_loop(Data#actor_info{first_marked_edges = [], second_marked_edges = []});
         stop ->
             ok
     end.
@@ -164,6 +172,7 @@ check_recursion(G, VCurr, VNew, LocalVars) ->
             % io:fwrite("[EMUL] RESET LOCALV IN ~p from ~p to ~p~n", [
             %     ProcName, FromLabel, ToLabel
             % ]),
+            % LocalVars;
             sets:new();
         false ->
             LocalVars
@@ -174,5 +183,5 @@ filter_marked_edges(EdgeL, MarkedE) -> [E || E <- EdgeL, not lists:member(E, Mar
 send_recv(P, Data) ->
     P ! Data,
     receive
-        {D} -> D
+        D -> D
     end.
diff --git a/src/choreography/gv.erl b/src/choreography/gv.erl
index 253f96d..fa03794 100644
--- a/src/choreography/gv.erl
+++ b/src/choreography/gv.erl
@@ -151,6 +151,7 @@ gen_branch_foreach_mess(BranchData, MessageQueue, ProcName, BaseBranchList) ->
                         ProcFrom, CurrProcFromVertex, ProcName, EToInfo, DupData, Label
                     ),
                     actor_emul:del_proc_mess_queue(NewPid, Message),
+                    % empty_filter_all_proc(NewMap),
                     %%% NOTE: the last operation MUST be the use_proc_transition, otherwise the final graph might be wrong
                     actor_emul:use_proc_transition(NewPid, EdgeFound),
                     AccList ++ [DupData#branch{last_vertex = LastVertex}]
@@ -160,6 +161,14 @@ gen_branch_foreach_mess(BranchData, MessageQueue, ProcName, BaseBranchList) ->
         MessageQueue
     ).
 
+empty_filter_all_proc(ProcPidMap) ->
+    maps:foreach(
+        fun(_, Pid) ->
+            actor_emul:empty_filter_proc(Pid)
+        end,
+        ProcPidMap
+    ).
+
 %%% Format the send label for the global view
 format_send_label(ProcFrom, ProcTo, Data) ->
     share:atol(ProcFrom) ++ "→" ++ share:atol(ProcTo) ++ ":" ++ share:atol(Data).
@@ -465,7 +474,7 @@ is_pm_msg_compatible(ProcPid, CallingProc, PatternMatching, Message) ->
     {IsCompatible, ToRegisterList} = check_msg_comp(
         ProcPid, CallingProc, PatternMatching, Message#message.data
     ),
-    % io:fwrite("Reg List ~p~n", [RegList]),
+    % io:fwrite("Reg List ~p~n", [ToRegisterList]),
     lists:foreach(
         fun(Item) -> register_var(Item) end,
         ToRegisterList
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")