From 1efb83c55e3ca3718fca377a5ba836842cac5fe6 Mon Sep 17 00:00:00 2001 From: geno Date: Tue, 16 Apr 2024 21:00:52 +0200 Subject: [PATCH] complex add vertex recv updated --- README.md | 1 + examples/airline/correct_main_gv.dot | 22 + examples/airline/main_0_global_view.dot | 29 +- examples/airline/seats_1_local_view.dot | 16 + examples/async/main_0_global_view.dot | 13 +- .../conditional-case/dummy_1_local_view.dot | 16 +- .../conditional-case/main_0_global_view.dot | 63 +- .../conditional-case/main_0_local_view.dot | 53 +- examples/customer/customer.erl | 14 +- .../customer/customer_dummy_0_local_view.dot | 19 + examples/customer/main_0_global_view.dot | 42 +- examples/customer/main_0_local_view.dot | 4 +- examples/customer/store_0_local_view.dot | 6 +- .../for-loop-recursion/main_0_global_view.dot | 25 +- .../for-loop-recursion/main_0_local_view.dot | 2 +- examples/function-call/dummy_1_local_view.dot | 4 +- examples/function-call/main_0_global_view.dot | 5 +- examples/function-call/main_0_local_view.dot | 4 +- examples/hello/hello.erl | 5 +- .../high-order-fun/greet_0_global_view.dot | 59 +- .../high-order-fun/greet_0_local_view.dot | 8 +- 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 | 107 ++-- examples/if-cases/main_0_local_view.dot | 8 +- examples/serverclient/client_0_local_view.dot | 4 +- 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 | 11 +- examples/test/foo1/test_0_local_view.dot | 4 +- examples/test/foo3/test_0_global_view.dot | 52 +- examples/test/foo3/test_0_local_view.dot | 4 +- examples/test/foo4/r_0_local_view.dot | 2 +- examples/test/foo4/test_0_global_view.dot | 63 +- examples/test/foo4/test_0_local_view.dot | 6 +- examples/test/foo4/w1_1_local_view.dot | 2 +- examples/test/foo4/w2_1_local_view.dot | 2 +- examples/test/foo5/target_0_local_view.dot | 2 +- examples/test/foo5/test_0_global_view.dot | 4 +- examples/test/foo5/test_0_local_view.dot | 6 +- 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 | 12 +- examples/ticktackloop/start_0_global_view.dot | 2 +- examples/ticktackloop/start_0_local_view.dot | 2 +- .../ticktackloop/tac_loop_0_local_view.dot | 2 +- .../ticktackloop/tic_loop_0_local_view.dot | 2 +- examples/ticktackstop/start_0_global_view.dot | 49 +- examples/ticktackstop/start_0_local_view.dot | 2 +- .../ticktackstop/tac_loop_0_local_view.dot | 4 +- .../ticktackstop/tic_loop_0_local_view.dot | 4 +- examples/trick/main_0_global_view.dot | 35 +- examples/trick/main_0_local_view.dot | 2 +- .../violation/incrementer_0_local_view.dot | 4 +- examples/violation/main_0_global_view.dot | 573 ++++++++++-------- examples/violation/main_0_local_view.dot | 24 +- examples/violation/meManager_0_local_view.dot | 2 +- .../violation/varManager_1_local_view.dot | 2 +- src/choreography/actor_emul.erl | 11 + src/choreography/eval.erl | 28 +- src/choreography/gv.erl | 187 ++++-- src/share/common_data.hrl | 21 +- src/share/share.erl | 14 +- 67 files changed, 935 insertions(+), 770 deletions(-) create mode 100644 examples/airline/correct_main_gv.dot create mode 100644 examples/airline/seats_1_local_view.dot create mode 100644 examples/customer/customer_dummy_0_local_view.dot diff --git a/README.md b/README.md index 1c016b1..5d75272 100644 --- a/README.md +++ b/README.md @@ -61,6 +61,7 @@ Try out the tool using the `./test.py` script. | function | ✅ yes | | guards | ❌ no | | register | 🟡 static eval | +| unregister | ❌ no | | rand:uniform | ✅ yes | | self | ✅ yes | | anon functions | ✅ yes | diff --git a/examples/airline/correct_main_gv.dot b/examples/airline/correct_main_gv.dot new file mode 100644 index 0000000..9d2e940 --- /dev/null +++ b/examples/airline/correct_main_gv.dot @@ -0,0 +1,22 @@ +digraph global { + n_0 [label="global", shape="plaintext"]; + n_0 -> n_1 [arrowhead=none]; + n_1 [id="1", shape=circle, label="1"]; + n_2 [id="2", shape=circle, label="2"]; + n_3 [id="3", shape=circle, label="3"]; + n_4 [id="4", shape=circle, label="4"]; + n_5 [id="5", shape=circle, label="5"]; + n_6 [id="6", shape=circle, label="6"]; + n_7 [id="7", shape=circle, label="7"]; + + n_1 -> n_2 [id="[$e|0]", label="main/0.0Δagent/1.0"]; + n_2 -> n_3 [id="[$e|1]", label="main/0.0Δagent/1.1"]; + n_3 -> n_4 [id="[$e|2]", label="agent/1.0→main/0.0:{sell,pid_self}"]; + n_3 -> n_5 [id="[$e|11]", label="agent/1.1→main/0.0:{sell,pid_self}"]; + n_4 -> n_6 [id="[$e|7]", label="main/0.0→agent/1.0:{booked,Num}"]; + n_5 -> n_7 [id="[$e|12]", label="main/0.0→agent/1.1:{booked,Num}"]; + n_6 -> n_4 [id="[$e|2]", label="agent/1.0→main/0.0:{sell,pid_self}"]; + n_7 -> n_5 [id="[$e|11]", label="agent/1.1→main/0.0:{sell,pid_self}"]; + n_7 -> n_4 [id="[$e|2]", label="agent/1.0→main/0.0:{sell,pid_self}"]; + n_6 -> n_5 [id="[$e|11]", label="agent/1.1→main/0.0:{sell,pid_self}"]; +} diff --git a/examples/airline/main_0_global_view.dot b/examples/airline/main_0_global_view.dot index cf188c9..a81ef80 100644 --- a/examples/airline/main_0_global_view.dot +++ b/examples/airline/main_0_global_view.dot @@ -7,21 +7,20 @@ digraph global { 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="7", shape=circle, label="7"]; - n_7 [id="3", shape=circle, label="3"]; + n_6 [id="3", shape=circle, label="3"]; - n_6 -> n_1 [id="[$e|10]", label="main/0.0→agent/1.0:{booked,Num}"]; - n_6 -> n_7 [id="[$e|11]", label="main/0.0→agent/1.1:{booked,Num}"]; - n_2 -> n_5 [id="[$e|9]", label="main/0.0→agent/1.1:{booked,Num}"]; - n_7 -> n_5 [id="[$e|12]", label="main/0.0→agent/1.1:{booked,Num}"]; - n_2 -> n_7 [id="[$e|8]", label="main/0.0→agent/1.0:{booked,Num}"]; - n_1 -> n_6 [id="[$e|6]", label="agent/1.0→main/0.0:{sell,pid_self}"]; - n_7 -> n_1 [id="[$e|3]", label="agent/1.1→main/0.0:{sell,pid_self}"]; - n_7 -> n_5 [id="[$e|2]", label="agent/1.0→main/0.0:{sell,pid_self}"]; - n_7 -> n_1 [id="[$e|13]", label="main/0.0→agent/1.0:{booked,Num}"]; - n_5 -> n_7 [id="[$e|5]", label="main/0.0→agent/1.0:{booked,Num}"]; - n_4 -> n_7 [id="[$e|1]", label="main/0.0Δagent/1.1"]; - n_5 -> n_2 [id="[$e|4]", label="agent/1.1→main/0.0:{sell,pid_self}"]; - n_1 -> n_7 [id="[$e|7]", label="main/0.0→agent/1.1:{booked,Num}"]; + 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_2 -> n_1 [id="[$e|13]", label="main/0.0→agent/1.0:{booked,Num}"]; + 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_1 -> n_2 [id="[$e|12]", label="main/0.0→agent/1.1:{booked,Num}"]; + 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}"]; } diff --git a/examples/airline/seats_1_local_view.dot b/examples/airline/seats_1_local_view.dot new file mode 100644 index 0000000..48e1a64 --- /dev/null +++ b/examples/airline/seats_1_local_view.dot @@ -0,0 +1,16 @@ +digraph seats_1 { + rankdir="LR"; + n_0 [label="seats_1", 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=doublecircle, label="2"]; + n_4 [id="4", shape=circle, label="4"]; + n_5 [id="3", shape=circle, label="3"]; + + n_2 -> n_3 [id="[$e|0]", label="arg (0)"]; + n_2 -> n_5 [id="[$e|1]", label="arg (Num)"]; + n_5 -> n_4 [id="[$e|2]", label="receive {sell,Pid1}"]; + n_4 -> n_1 [id="[$e|3]", label="send {booked,Num} to Pid1"]; + n_1 -> n_2 [id="[$e|4]", label="ɛ"]; +} diff --git a/examples/async/main_0_global_view.dot b/examples/async/main_0_global_view.dot index 26472eb..f1621bd 100644 --- a/examples/async/main_0_global_view.dot +++ b/examples/async/main_0_global_view.dot @@ -7,13 +7,12 @@ digraph global { 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="7", shape=circle, label="7"]; - n_7 [id="3", shape=circle, label="3"]; + n_6 [id="3", shape=circle, label="3"]; - n_7 -> n_1 [id="[$e|3]", label="dummy1/0.0→dummy2/0.0:bello"]; - n_7 -> n_5 [id="[$e|2]", label="dummy2/0.0→dummy1/0.0:ciao"]; - n_1 -> n_6 [id="[$e|5]", label="dummy2/0.0→dummy1/0.0:ciao"]; - n_4 -> n_7 [id="[$e|1]", label="main/0.0Δdummy2/0.0"]; - n_5 -> n_2 [id="[$e|4]", label="dummy1/0.0→dummy2/0.0:bello"]; + 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_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"]; } diff --git a/examples/conditional-case/dummy_1_local_view.dot b/examples/conditional-case/dummy_1_local_view.dot index 62e376e..165b05c 100644 --- a/examples/conditional-case/dummy_1_local_view.dot +++ b/examples/conditional-case/dummy_1_local_view.dot @@ -1,11 +1,15 @@ digraph dummy_1 { rankdir="LR"; n_0 [label="dummy_1", 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_1 [id="5", shape=doublecircle, 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_2 -> n_3 [id="[$e|1]", label="receive Str"]; - n_1 -> n_2 [id="[$e|0]", label="send {pid_self,integer} to Pid"]; + n_4 -> n_1 [id="[$e|3]", label="ɛ"]; + n_5 -> n_4 [id="[$e|2]", label="receive Str"]; + n_3 -> n_5 [id="[$e|1]", label="send {pid_self,integer} to Pid"]; + n_2 -> n_3 [id="[$e|0]", label="ɛ"]; } diff --git a/examples/conditional-case/main_0_global_view.dot b/examples/conditional-case/main_0_global_view.dot index 8e83714..7b730b7 100644 --- a/examples/conditional-case/main_0_global_view.dot +++ b/examples/conditional-case/main_0_global_view.dot @@ -1,47 +1,26 @@ digraph global { rankdir="LR"; n_0 [label="global", shape="plaintext"]; - n_1 [id="20", shape=circle, label="20"]; - n_2 [id="5", shape=circle, label="5"]; - n_3 [id="15", shape=circle, label="15"]; - n_4 [id="19", shape=circle, label="19"]; - n_5 [id="12", shape=circle, label="12"]; - n_6 [id="11", shape=circle, label="11"]; - n_7 [id="17", shape=circle, label="17"]; - n_8 [id="18", shape=circle, label="18"]; - n_9 [id="14", shape=circle, label="14"]; - n_10 [id="6", shape=circle, label="6"]; - n_11 [id="13", shape=circle, label="13"]; - n_12 [id="10", shape=circle, label="10"]; - n_13 [id="1", shape=circle, label="1"]; - n_0 -> n_13 [arrowhead=none]; - n_14 [id="9", shape=circle, label="9"]; - n_15 [id="2", shape=circle, label="2"]; - n_16 [id="21", shape=circle, label="21"]; - n_17 [id="8", shape=circle, label="8"]; - n_18 [id="4", shape=circle, label="4"]; - n_19 [id="7", shape=circle, label="7"]; - n_20 [id="3", shape=circle, label="3"]; - n_21 [id="16", shape=circle, label="16"]; + 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="9", shape=circle, label="9"]; + n_5 [id="2", shape=circle, label="2"]; + n_6 [id="8", shape=circle, label="8"]; + n_7 [id="4", shape=circle, label="4"]; + n_8 [id="7", shape=circle, label="7"]; + n_9 [id="3", shape=circle, label="3"]; - n_18 -> n_2 [id="[$e|3]", label="main/0.0Δdummy/1.3"]; - n_14 -> n_11 [id="[$e|11]", label="main/0.0→dummy/1.0:'Ciao"]; - n_10 -> n_9 [id="[$e|12]", label="main/0.0→dummy/1.1:'Ciao"]; - n_10 -> n_12 [id="[$e|8]", label="main/0.0→dummy/1.0:'Ciao"]; - n_15 -> n_20 [id="[$e|1]", label="main/0.0Δdummy/1.1"]; - n_2 -> n_17 [id="[$e|6]", label="dummy/1.2→main/0.0:{pid_self,integer}"]; - n_19 -> n_21 [id="[$e|14]", label="main/0.0→dummy/1.1:'Ciao"]; - n_2 -> n_10 [id="[$e|4]", label="dummy/1.0→main/0.0:{pid_self,integer}"]; - n_2 -> n_14 [id="[$e|7]", label="dummy/1.3→main/0.0:{pid_self,integer}"]; - n_17 -> n_8 [id="[$e|16]", label="main/0.0→dummy/1.1:'Ciao"]; - n_20 -> n_18 [id="[$e|2]", label="main/0.0Δdummy/1.2"]; - n_17 -> n_4 [id="[$e|17]", label="main/0.0→dummy/1.2:'Ciao"]; - n_2 -> n_19 [id="[$e|5]", label="dummy/1.1→main/0.0:{pid_self,integer}"]; - n_13 -> n_15 [id="[$e|0]", label="main/0.0Δdummy/1.0"]; - n_10 -> n_3 [id="[$e|13]", label="main/0.0→dummy/1.2:'Ciao"]; - n_14 -> n_1 [id="[$e|18]", label="main/0.0→dummy/1.1:'Ciao"]; - n_19 -> n_7 [id="[$e|15]", label="main/0.0→dummy/1.2:'Ciao"]; - n_19 -> n_6 [id="[$e|9]", label="main/0.0→dummy/1.0:'Ciao"]; - n_14 -> n_16 [id="[$e|19]", label="main/0.0→dummy/1.2:'Ciao"]; - n_17 -> n_5 [id="[$e|10]", label="main/0.0→dummy/1.0:'Ciao"]; + 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_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_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"]; } diff --git a/examples/conditional-case/main_0_local_view.dot b/examples/conditional-case/main_0_local_view.dot index 924627d..2d00c2b 100644 --- a/examples/conditional-case/main_0_local_view.dot +++ b/examples/conditional-case/main_0_local_view.dot @@ -1,21 +1,42 @@ digraph main_0 { rankdir="LR"; n_0 [label="main_0", shape="plaintext"]; - n_1 [id="5", shape=circle, label="6"]; - n_2 [id="10", shape=circle, label="3"]; - n_3 [id="1", shape=circle, label="1"]; - n_0 -> n_3 [arrowhead=none]; - n_4 [id="9", shape=circle, label="5"]; - n_5 [id="2", shape=circle, label="2"]; - n_6 [id="4", shape=circle, label="4"]; - n_7 [id="3", shape=doublecircle, label="7"]; + n_1 [id="5", shape=circle, label="5"]; + n_2 [id="15", shape=circle, label="15"]; + n_3 [id="12", shape=circle, label="12"]; + n_4 [id="11", shape=circle, label="11"]; + n_5 [id="17", shape=doublecircle, label="17"]; + n_6 [id="14", shape=circle, label="14"]; + n_7 [id="6", shape=circle, label="6"]; + n_8 [id="13", shape=circle, label="13"]; + n_9 [id="10", shape=circle, label="10"]; + n_10 [id="1", shape=circle, label="1"]; + n_0 -> n_10 [arrowhead=none]; + n_11 [id="9", shape=circle, label="9"]; + n_12 [id="2", shape=circle, label="2"]; + n_13 [id="8", shape=circle, label="8"]; + n_14 [id="4", shape=circle, label="4"]; + n_15 [id="7", shape=circle, label="7"]; + n_16 [id="3", shape=circle, label="3"]; + n_17 [id="16", shape=circle, label="16"]; - n_1 -> n_7 [id="[$e|3]", label="send 'Ciao A' to dummy/1.0"]; - n_5 -> n_2 [id="[$e|8]", label="spawn dummy/1.1"]; - n_2 -> n_6 [id="[$e|1]", label="spawn dummy/1.2"]; - n_4 -> n_1 [id="[$e|4]", label="receive {Process,_}"]; - n_6 -> n_4 [id="[$e|2]", label="spawn dummy/1.3"]; - n_3 -> n_5 [id="[$e|0]", label="spawn dummy/1.0"]; - n_1 -> n_7 [id="[$e|9]", label="send 'Ciao B' to dummy/1.1"]; - n_1 -> n_7 [id="[$e|10]", label="send 'Ciao C' to dummy/1.2"]; + n_4 -> n_3 [id="[$e|10]", label="send 'Ciao B' to dummy/1.1"]; + n_13 -> n_8 [id="[$e|11]", label="ɛ"]; + n_13 -> n_4 [id="[$e|9]", label="ɛ"]; + n_6 -> n_5 [id="[$e|17]", label="ɛ"]; + n_8 -> n_6 [id="[$e|12]", label="send 'Ciao C' to dummy/1.2"]; + n_11 -> n_9 [id="[$e|8]", label="send 'Ciao A' to dummy/1.0"]; + n_2 -> n_17 [id="[$e|14]", label="send 'Ciao D' to dummy/1.3"]; + n_15 -> n_13 [id="[$e|6]", label="ɛ"]; + n_14 -> n_1 [id="[$e|3]", label="spawn dummy/1.2"]; + n_17 -> n_5 [id="[$e|18]", label="ɛ"]; + n_3 -> n_5 [id="[$e|16]", label="ɛ"]; + n_16 -> n_14 [id="[$e|2]", label="spawn dummy/1.1"]; + n_13 -> n_2 [id="[$e|13]", label="ɛ"]; + n_7 -> n_15 [id="[$e|5]", label="receive {Process,_}"]; + n_9 -> n_5 [id="[$e|15]", label="ɛ"]; + n_12 -> n_16 [id="[$e|1]", label="spawn dummy/1.0"]; + n_1 -> n_7 [id="[$e|4]", label="spawn dummy/1.3"]; + n_13 -> n_11 [id="[$e|7]", label="ɛ"]; + n_10 -> n_12 [id="[$e|0]", label="ɛ"]; } diff --git a/examples/customer/customer.erl b/examples/customer/customer.erl index f9fe5a9..fa77ee2 100644 --- a/examples/customer/customer.erl +++ b/examples/customer/customer.erl @@ -1,6 +1,9 @@ --module(hello). --export([main/0, customer/0, store/0]). +-module(customer). +-export([main/0, customer/0, store/0, customer_dummy/0]). +customer_dummy() -> + store ! ciaooooo, + customer(). customer() -> store ! item, %%% Simulazione della decisione di un utente @@ -24,6 +27,7 @@ purchase() -> store() -> receive item -> + io:fwrite("richiesta ricevuta~n"), receive buy -> payment(); more -> store() @@ -46,7 +50,9 @@ payment() -> end. main() -> - Cstm = spawn(?MODULE, customer, []), Str = spawn(?MODULE, store, []), + register(store, Str), + timer:sleep(5), + Cstm = spawn(?MODULE, customer_dummy, []), register(customer, Cstm), - register(store, Str). + done. diff --git a/examples/customer/customer_dummy_0_local_view.dot b/examples/customer/customer_dummy_0_local_view.dot new file mode 100644 index 0000000..8d743fa --- /dev/null +++ b/examples/customer/customer_dummy_0_local_view.dot @@ -0,0 +1,19 @@ +digraph customer_dummy_0 { + rankdir="LR"; + n_0 [label="customer_dummy_0", shape="plaintext"]; + n_1 [id="5", shape=circle, label="2"]; + 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="4"]; + 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_2 -> n_4 [id="[$e|3]", label="receive reject"]; + 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"]; +} diff --git a/examples/customer/main_0_global_view.dot b/examples/customer/main_0_global_view.dot index 2cbc7bb..ab6a15a 100644 --- a/examples/customer/main_0_global_view.dot +++ b/examples/customer/main_0_global_view.dot @@ -2,22 +2,30 @@ 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="8", shape=circle, label="8"]; - n_6 [id="4", shape=circle, label="4"]; - n_7 [id="7", shape=circle, label="7"]; - n_8 [id="3", shape=circle, label="3"]; + n_2 [id="11", shape=circle, label="11"]; + n_3 [id="6", shape=circle, label="6"]; + n_4 [id="10", shape=circle, label="10"]; + n_5 [id="1", shape=circle, label="1"]; + n_0 -> n_5 [arrowhead=none]; + n_6 [id="9", shape=circle, label="9"]; + n_7 [id="2", shape=circle, label="2"]; + n_8 [id="8", shape=circle, label="8"]; + n_9 [id="4", shape=circle, label="4"]; + n_10 [id="7", shape=circle, label="7"]; + n_11 [id="3", shape=circle, label="3"]; - n_3 -> n_4 [id="[$e|0]", label="main/0.0Δcustomer/0.0"]; - n_1 -> n_7 [id="[$e|5]", label="customer/0.0→store/0.0:payment"]; - n_6 -> n_1 [id="[$e|3]", label="customer/0.0→store/0.0:buy"]; - n_7 -> n_1 [id="[$e|8]", label="store/0.0→customer/0.0:reject"]; - n_2 -> n_6 [id="[$e|6]", label="customer/0.0→store/0.0:item"]; - n_8 -> n_6 [id="[$e|2]", label="customer/0.0→store/0.0:item"]; - n_7 -> n_5 [id="[$e|7]", label="store/0.0→customer/0.0:accepted"]; - n_6 -> n_2 [id="[$e|4]", label="customer/0.0→store/0.0:more"]; - n_4 -> n_8 [id="[$e|1]", label="main/0.0Δstore/0.0"]; + n_5 -> n_7 [id="[$e|0]", label="main/0.0Δstore/0.0"]; + n_10 -> n_6 [id="[$e|9]", label="customer_dummy/0.0→store/0.0:payment"]; + n_1 -> n_10 [id="[$e|5]", label="customer_dummy/0.0→store/0.0:buy"]; + n_11 -> n_1 [id="[$e|3]", label="customer_dummy/0.0→store/0.0:item"]; + n_3 -> n_9 [id="[$e|8]", label="customer_dummy/0.0→store/0.0:item"]; + n_6 -> n_2 [id="[$e|12]", label="store/0.0→customer_dummy/0.0:reject"]; + n_9 -> n_8 [id="[$e|6]", label="customer_dummy/0.0→store/0.0:more"]; + n_11 -> n_9 [id="[$e|2]", label="customer_dummy/0.0→store/0.0:item"]; + n_8 -> n_1 [id="[$e|10]", label="customer_dummy/0.0→store/0.0:item"]; + n_9 -> n_10 [id="[$e|7]", label="customer_dummy/0.0→store/0.0:buy"]; + n_6 -> n_4 [id="[$e|11]", label="store/0.0→customer_dummy/0.0:accepted"]; + n_2 -> n_6 [id="[$e|13]", label="customer_dummy/0.0→store/0.0:payment"]; + n_9 -> n_3 [id="[$e|4]", label="customer_dummy/0.0→store/0.0:more"]; + n_7 -> n_11 [id="[$e|1]", label="main/0.0Δcustomer_dummy/0.0"]; } diff --git a/examples/customer/main_0_local_view.dot b/examples/customer/main_0_local_view.dot index 2d3ad9d..b82dae0 100644 --- a/examples/customer/main_0_local_view.dot +++ b/examples/customer/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|0]", label="spawn customer/0.0"]; - n_2 -> n_3 [id="[$e|1]", label="spawn store/0.0"]; + n_2 -> n_3 [id="[$e|0]", label="spawn customer_dummy/0.0"]; + n_1 -> n_2 [id="[$e|1]", label="spawn store/0.0"]; } diff --git a/examples/customer/store_0_local_view.dot b/examples/customer/store_0_local_view.dot index 4fdfd79..55eef7e 100644 --- a/examples/customer/store_0_local_view.dot +++ b/examples/customer/store_0_local_view.dot @@ -9,9 +9,9 @@ digraph store_0 { n_5 [id="3", shape=circle, label="2"]; n_4 -> n_3 [id="[$e|0]", label="receive payment"]; - n_3 -> n_4 [id="[$e|9]", label="send reject to customer/0.0"]; - n_5 -> n_4 [id="[$e|3]", label="receive buy"]; + 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_3 -> n_1 [id="[$e|2]", label="send accepted to customer/0.0"]; + 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 1980da0..5745757 100644 --- a/examples/for-loop-recursion/main_0_global_view.dot +++ b/examples/for-loop-recursion/main_0_global_view.dot @@ -1,19 +1,16 @@ 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="7", shape=circle, label="7"]; - n_7 [id="3", shape=circle, label="3"]; + 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="4", shape=circle, label="4"]; + n_4 [id="3", shape=circle, label="3"]; - n_7 -> n_1 [id="[$e|3]", label="dummy/1.1→main/0.0:integer"]; - n_1 -> n_6 [id="[$e|5]", label="dummy/1.0→main/0.0:integer"]; - n_3 -> n_4 [id="[$e|0]", label="main/0.0Δdummy/1.0"]; - n_4 -> n_7 [id="[$e|1]", label="main/0.0Δdummy/1.1"]; - n_5 -> n_2 [id="[$e|4]", label="dummy/1.1→main/0.0:integer"]; - n_7 -> n_5 [id="[$e|2]", label="dummy/1.0→main/0.0:integer"]; + 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"]; } diff --git a/examples/for-loop-recursion/main_0_local_view.dot b/examples/for-loop-recursion/main_0_local_view.dot index 0aca7f3..25112e9 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_1 -> n_2 [id="[$e|0]", label="spawn dummy/1.0"]; 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"]; } diff --git a/examples/function-call/dummy_1_local_view.dot b/examples/function-call/dummy_1_local_view.dot index cc93e42..8084bc2 100644 --- a/examples/function-call/dummy_1_local_view.dot +++ b/examples/function-call/dummy_1_local_view.dot @@ -1,6 +1,6 @@ -digraph dummy/1 { +digraph dummy_1 { rankdir="LR"; - n_0 [label="dummy/1", shape="plaintext"]; + n_0 [label="dummy_1", shape="plaintext"]; n_1 [id="1", shape=circle, label="1"]; n_0 -> n_1 [arrowhead=none]; n_2 [id="2", shape=circle, label="2"]; diff --git a/examples/function-call/main_0_global_view.dot b/examples/function-call/main_0_global_view.dot index a23c740..4dcb3ca 100644 --- a/examples/function-call/main_0_global_view.dot +++ b/examples/function-call/main_0_global_view.dot @@ -4,10 +4,9 @@ digraph global { 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="4", shape=circle, label="4"]; - n_4 [id="3", shape=circle, label="3"]; + 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_4 [id="[$e|1]", label="dummy/1.0→main/0.0:{pid_self,hello1}"]; + n_2 -> n_3 [id="[$e|1]", label="dummy/1.0→main/0.0:{pid_self,hello1}"]; } diff --git a/examples/function-call/main_0_local_view.dot b/examples/function-call/main_0_local_view.dot index fbcfa44..ff674e1 100644 --- a/examples/function-call/main_0_local_view.dot +++ b/examples/function-call/main_0_local_view.dot @@ -1,6 +1,6 @@ -digraph main/0 { +digraph main_0 { rankdir="LR"; - n_0 [label="main/0", shape="plaintext"]; + 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"]; diff --git a/examples/hello/hello.erl b/examples/hello/hello.erl index a1e64fb..954dbf5 100644 --- a/examples/hello/hello.erl +++ b/examples/hello/hello.erl @@ -4,11 +4,12 @@ greet() -> Me = self(), Me ! hello1, + Bool = io:fread("~p"), if - true -> + Bool -> Me ! hello2, greet(); - false -> + not Bool -> receive hello1 -> done; hello2 -> done diff --git a/examples/high-order-fun/greet_0_global_view.dot b/examples/high-order-fun/greet_0_global_view.dot index c51d0df..ab43aca 100644 --- a/examples/high-order-fun/greet_0_global_view.dot +++ b/examples/high-order-fun/greet_0_global_view.dot @@ -2,40 +2,29 @@ digraph global { rankdir="LR"; n_0 [label="global", shape="plaintext"]; n_1 [id="5", shape=circle, label="5"]; - n_2 [id="15", shape=circle, label="15"]; - n_3 [id="12", shape=circle, label="12"]; - n_4 [id="11", shape=circle, label="11"]; - n_5 [id="17", shape=circle, label="17"]; - n_6 [id="18", shape=circle, label="18"]; - n_7 [id="14", shape=circle, label="14"]; - n_8 [id="6", shape=circle, label="6"]; - n_9 [id="13", shape=circle, label="13"]; - n_10 [id="10", shape=circle, label="10"]; - n_11 [id="1", shape=circle, label="1"]; - n_0 -> n_11 [arrowhead=none]; - n_12 [id="9", shape=circle, label="9"]; - n_13 [id="2", shape=circle, label="2"]; - n_14 [id="8", shape=circle, label="8"]; - n_15 [id="4", shape=circle, label="4"]; - n_16 [id="7", shape=circle, label="7"]; - n_17 [id="3", shape=circle, label="3"]; - n_18 [id="16", shape=circle, label="16"]; + n_2 [id="6", shape=circle, label="6"]; + n_3 [id="10", shape=circle, label="10"]; + n_4 [id="1", shape=circle, label="1"]; + n_0 -> n_4 [arrowhead=none]; + n_5 [id="9", shape=circle, label="9"]; + n_6 [id="2", shape=circle, label="2"]; + n_7 [id="8", shape=circle, label="8"]; + n_8 [id="4", shape=circle, label="4"]; + n_9 [id="7", shape=circle, label="7"]; + n_10 [id="3", shape=circle, label="3"]; - n_1 -> n_12 [id="[$e|7]", label="greet/0.0→greet/0.0:hello2"]; - n_8 -> n_4 [id="[$e|9]", label="greet/0.0→greet/0.0:hello2"]; - n_17 -> n_1 [id="[$e|3]", label="greet/0.0→anonfun_15.0:hello1"]; - n_10 -> n_18 [id="[$e|14]", label="greet/0.0→greet/0.0:hello2"]; - n_15 -> n_14 [id="[$e|6]", label="greet/0.0→anonfun_10.0:hello3"]; - n_14 -> n_7 [id="[$e|12]", label="greet/0.0→anonfun_15.0:hello1"]; - n_1 -> n_10 [id="[$e|8]", label="greet/0.0→anonfun_10.0:hello3"]; - n_4 -> n_5 [id="[$e|15]", label="greet/0.0→anonfun_15.0:hello1"]; - n_12 -> n_2 [id="[$e|13]", label="greet/0.0→anonfun_10.0:hello3"]; - n_8 -> n_3 [id="[$e|10]", label="greet/0.0→anonfun_15.0:hello1"]; - n_15 -> n_16 [id="[$e|5]", label="greet/0.0→anonfun_15.0:hello1"]; - n_16 -> n_9 [id="[$e|11]", label="greet/0.0→anonfun_10.0:hello3"]; - n_11 -> n_13 [id="[$e|0]", label="greet/0.0Δanonfun_15.0"]; - n_13 -> n_17 [id="[$e|1]", label="greet/0.0Δanonfun_10.0"]; - n_3 -> n_6 [id="[$e|16]", label="greet/0.0→greet/0.0:hello2"]; - n_17 -> n_8 [id="[$e|4]", label="greet/0.0→anonfun_10.0:hello3"]; - n_17 -> n_15 [id="[$e|2]", label="greet/0.0→greet/0.0:hello2"]; + n_2 -> n_2 [id="[$e|9]", label="greet/0.0→greet/0.0:hello2"]; + 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_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_6 -> n_10 [id="[$e|1]", label="greet/0.0Δanonfun_10.0"]; } diff --git a/examples/high-order-fun/greet_0_local_view.dot b/examples/high-order-fun/greet_0_local_view.dot index 922c302..41edaa4 100644 --- a/examples/high-order-fun/greet_0_local_view.dot +++ b/examples/high-order-fun/greet_0_local_view.dot @@ -10,10 +10,10 @@ digraph greet_0 { n_6 [id="7", shape=circle, label="5"]; n_7 [id="3", shape=circle, label="2"]; - n_6 -> n_5 [id="[$e|7]", label="send hello3 to anonfun_10.0"]; - n_1 -> n_6 [id="[$e|6]", label="spawn anonfun_10.0"]; n_4 -> n_1 [id="[$e|0]", label="send hello2 to pid_self"]; - n_5 -> n_3 [id="[$e|1]", label="receive _"]; - n_7 -> n_4 [id="[$e|4]", label="send hello1 to anonfun_15.0"]; + 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 _"]; } diff --git a/examples/if-cases/a_0_local_view.dot b/examples/if-cases/a_0_local_view.dot index 256a139..08ca137 100644 --- a/examples/if-cases/a_0_local_view.dot +++ b/examples/if-cases/a_0_local_view.dot @@ -6,7 +6,7 @@ digraph a_0 { n_2 [id="2", shape=doublecircle, label="3"]; n_3 [id="3", shape=circle, label="2"]; - n_3 -> n_3 [id="[$e|1]", label="receive Pid"]; 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"]; } diff --git a/examples/if-cases/b_0_local_view.dot b/examples/if-cases/b_0_local_view.dot index ab85896..309c7c6 100644 --- a/examples/if-cases/b_0_local_view.dot +++ b/examples/if-cases/b_0_local_view.dot @@ -6,7 +6,7 @@ digraph b_0 { n_2 [id="2", shape=doublecircle, label="3"]; n_3 [id="3", shape=circle, label="2"]; - n_1 -> n_3 [id="[$e|1]", label="receive Pid"]; 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"]; } diff --git a/examples/if-cases/c_0_local_view.dot b/examples/if-cases/c_0_local_view.dot index df83148..1e9d4ec 100644 --- a/examples/if-cases/c_0_local_view.dot +++ b/examples/if-cases/c_0_local_view.dot @@ -6,7 +6,7 @@ digraph c_0 { n_2 [id="2", shape=doublecircle, label="3"]; n_3 [id="3", shape=circle, label="2"]; - n_3 -> n_3 [id="[$e|1]", label="receive Pid"]; 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"]; } diff --git a/examples/if-cases/main_0_global_view.dot b/examples/if-cases/main_0_global_view.dot index ddd732c..b4bba81 100644 --- a/examples/if-cases/main_0_global_view.dot +++ b/examples/if-cases/main_0_global_view.dot @@ -1,73 +1,44 @@ digraph global { rankdir="LR"; n_0 [label="global", shape="plaintext"]; - n_1 [id="33", shape=circle, label="33"]; - n_2 [id="34", shape=circle, label="34"]; - n_3 [id="20", shape=circle, label="20"]; - n_4 [id="27", shape=circle, label="27"]; - n_5 [id="29", shape=circle, label="29"]; - n_6 [id="23", shape=circle, label="23"]; - n_7 [id="25", shape=circle, label="25"]; - n_8 [id="5", shape=circle, label="5"]; - n_9 [id="28", shape=circle, label="28"]; - n_10 [id="15", shape=circle, label="15"]; - n_11 [id="19", shape=circle, label="19"]; - n_12 [id="12", shape=circle, label="12"]; - n_13 [id="11", shape=circle, label="11"]; - n_14 [id="17", shape=circle, label="17"]; - n_15 [id="18", shape=circle, label="18"]; - n_16 [id="14", shape=circle, label="14"]; - n_17 [id="6", shape=circle, label="6"]; - n_18 [id="13", shape=circle, label="13"]; - n_19 [id="24", shape=circle, label="24"]; - n_20 [id="10", shape=circle, label="10"]; - n_21 [id="30", shape=circle, label="30"]; - n_22 [id="22", shape=circle, label="22"]; - n_23 [id="1", shape=circle, label="1"]; - n_0 -> n_23 [arrowhead=none]; - n_24 [id="26", shape=circle, label="26"]; - n_25 [id="9", shape=circle, label="9"]; - n_26 [id="2", shape=circle, label="2"]; - n_27 [id="21", shape=circle, label="21"]; - n_28 [id="8", shape=circle, label="8"]; - n_29 [id="4", shape=circle, label="4"]; - n_30 [id="31", shape=circle, label="31"]; - n_31 [id="32", shape=circle, label="32"]; - n_32 [id="7", shape=circle, label="7"]; - n_33 [id="3", shape=circle, label="3"]; - n_34 [id="16", shape=circle, label="16"]; + n_1 [id="5", shape=circle, label="5"]; + n_2 [id="11", shape=circle, label="11"]; + n_3 [id="6", shape=circle, label="6"]; + n_4 [id="10", shape=circle, label="10"]; + n_5 [id="1", shape=circle, label="1"]; + n_0 -> n_5 [arrowhead=none]; + n_6 [id="9", shape=circle, label="9"]; + n_7 [id="2", shape=circle, label="2"]; + n_8 [id="8", shape=circle, label="8"]; + n_9 [id="4", shape=circle, label="4"]; + n_10 [id="7", shape=circle, label="7"]; + n_11 [id="3", shape=circle, label="3"]; - n_29 -> n_8 [id="[$e|3]", label="main/0.0→a/0.0:b/0.0"]; - n_17 -> n_18 [id="[$e|11]", label="main/0.0→a/0.0:b/0.0"]; - n_12 -> n_19 [id="[$e|22]", label="main/0.0→b/0.0:c/0.0"]; - n_17 -> n_16 [id="[$e|12]", label="main/0.0→c/0.0:a/0.0"]; - n_20 -> n_22 [id="[$e|20]", label="main/0.0→b/0.0:a/0.0"]; - n_3 -> n_31 [id="[$e|30]", label="main/0.0→a/0.0:c/0.0"]; - n_29 -> n_20 [id="[$e|8]", label="main/0.0→c/0.0:b/0.0"]; - n_26 -> n_33 [id="[$e|1]", label="main/0.0Δb/0.0"]; - n_34 -> n_9 [id="[$e|26]", label="main/0.0→a/0.0:b/0.0"]; - n_29 -> n_28 [id="[$e|6]", label="main/0.0→a/0.0:c/0.0"]; - n_27 -> n_1 [id="[$e|31]", label="main/0.0→b/0.0:a/0.0"]; - n_13 -> n_6 [id="[$e|21]", label="main/0.0→c/0.0:a/0.0"]; - n_14 -> n_5 [id="[$e|27]", label="main/0.0→c/0.0:b/0.0"]; - n_32 -> n_34 [id="[$e|14]", label="main/0.0→b/0.0:c/0.0"]; - n_22 -> n_2 [id="[$e|32]", label="main/0.0→a/0.0:c/0.0"]; - n_29 -> n_17 [id="[$e|4]", label="main/0.0→b/0.0:c/0.0"]; - n_11 -> n_30 [id="[$e|29]", label="main/0.0→c/0.0:b/0.0"]; - n_29 -> n_25 [id="[$e|7]", label="main/0.0→b/0.0:a/0.0"]; - n_16 -> n_24 [id="[$e|24]", label="main/0.0→a/0.0:b/0.0"]; - n_15 -> n_21 [id="[$e|28]", label="main/0.0→b/0.0:a/0.0"]; - n_28 -> n_15 [id="[$e|16]", label="main/0.0→c/0.0:b/0.0"]; - n_33 -> n_29 [id="[$e|2]", label="main/0.0Δc/0.0"]; - n_25 -> n_11 [id="[$e|17]", label="main/0.0→a/0.0:c/0.0"]; - n_29 -> n_32 [id="[$e|5]", label="main/0.0→c/0.0:a/0.0"]; - n_23 -> n_26 [id="[$e|0]", label="main/0.0Δa/0.0"]; - n_32 -> n_10 [id="[$e|13]", label="main/0.0→a/0.0:b/0.0"]; - n_10 -> n_4 [id="[$e|25]", label="main/0.0→b/0.0:c/0.0"]; - n_25 -> n_3 [id="[$e|18]", label="main/0.0→c/0.0:b/0.0"]; - n_28 -> n_14 [id="[$e|15]", label="main/0.0→b/0.0:a/0.0"]; - n_18 -> n_7 [id="[$e|23]", label="main/0.0→c/0.0:a/0.0"]; - n_8 -> n_13 [id="[$e|9]", label="main/0.0→b/0.0:c/0.0"]; - n_20 -> n_27 [id="[$e|19]", label="main/0.0→a/0.0:c/0.0"]; - n_8 -> n_12 [id="[$e|10]", label="main/0.0→c/0.0:a/0.0"]; + 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_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_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_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_5 -> n_7 [id="[$e|0]", label="main/0.0Δa/0.0"]; } diff --git a/examples/if-cases/main_0_local_view.dot b/examples/if-cases/main_0_local_view.dot index ff75e96..1ee095f 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_8 -> n_1 [id="[$e|3]", label="send b/0.0 to a/0.0"]; + 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_2 -> n_6 [id="[$e|1]", label="send a/0.0 to c/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_3 -> n_8 [id="[$e|2]", label="spawn c/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_3 -> n_8 [id="[$e|2]", label="spawn c/0.0"]; n_4 -> n_9 [id="[$e|0]", label="spawn a/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 731a0c4..9c1e1f2 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_2 [id="[$e|5]", label="send done to Handle"]; n_3 -> n_4 [id="[$e|3]", label="receive {res,Handle}"]; - n_4 -> n_4 [id="[$e|7]", label="send next to 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"]; } diff --git a/examples/serverclient/main_0_global_view.dot b/examples/serverclient/main_0_global_view.dot index 1efb420..d444fcb 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_3 -> n_4 [id="[$e|0]", label="main/0.0Δserver/0.0"]; - n_2 -> n_6 [id="[$e|5]", label="client/0.0→handle_req/1.0:done"]; n_5 -> n_1 [id="[$e|3]", label="server/0.0Δhandle_req/1.0"]; - n_2 -> n_2 [id="[$e|6]", label="client/0.0→handle_req/1.0:next"]; n_7 -> n_5 [id="[$e|2]", label="client/0.0→server/0.0:{req,pid_self}"]; - n_1 -> n_2 [id="[$e|4]", label="server/0.0→client/0.0:{res,handle_req/1.0}"]; + 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_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"]; } diff --git a/examples/serverclient/main_0_local_view.dot b/examples/serverclient/main_0_local_view.dot index b87e932..ac5bdc8 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_2 -> n_3 [id="[$e|0]", label="spawn client/0.0"]; n_1 -> n_2 [id="[$e|1]", label="spawn server/0.0"]; + n_2 -> n_3 [id="[$e|0]", label="spawn client/0.0"]; } diff --git a/examples/serverclient/server_0_local_view.dot b/examples/serverclient/server_0_local_view.dot index 209bd7c..6f7fd26 100644 --- a/examples/serverclient/server_0_local_view.dot +++ b/examples/serverclient/server_0_local_view.dot @@ -9,8 +9,8 @@ digraph server_0 { n_5 [id="3", shape=doublecircle, label="4"]; n_3 -> n_1 [id="[$e|3]", label="spawn handle_req/1.0"]; - n_4 -> n_5 [id="[$e|6]", label="spawn handle_req/1.1"]; - n_1 -> n_2 [id="[$e|7]", label="send {res,handle_req/1.0} to 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"]; } diff --git a/examples/test/barber/test_0_local_view.dot b/examples/test/barber/test_0_local_view.dot index be8f780..5b132ed 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_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"]; + 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 dadfffd..2f5e17c 100644 --- a/examples/test/foo1/test_0_global_view.dot +++ b/examples/test/foo1/test_0_global_view.dot @@ -7,13 +7,12 @@ digraph global { 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="7", shape=circle, label="7"]; - n_7 [id="3", shape=circle, label="3"]; + n_6 [id="3", shape=circle, label="3"]; - n_7 -> n_1 [id="[$e|3]", label="test/0.0→c/1.0:dos"]; - n_1 -> n_6 [id="[$e|5]", label="test/0.0→b/0.0:uno"]; + 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_4 -> n_7 [id="[$e|1]", label="test/0.0Δc/1.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_5 -> n_2 [id="[$e|4]", label="test/0.0→c/1.0:dos"]; - n_7 -> n_5 [id="[$e|2]", label="test/0.0→b/0.0:uno"]; + n_4 -> n_6 [id="[$e|1]", label="test/0.0Δc/1.0"]; } diff --git a/examples/test/foo1/test_0_local_view.dot b/examples/test/foo1/test_0_local_view.dot index 7f2c31d..60481a4 100644 --- a/examples/test/foo1/test_0_local_view.dot +++ b/examples/test/foo1/test_0_local_view.dot @@ -8,8 +8,8 @@ digraph test_0 { n_4 [id="4", shape=doublecircle, label="5"]; n_5 [id="3", shape=circle, label="4"]; - n_5 -> n_4 [id="[$e|3]", label="send dos to c/1.0"]; n_1 -> n_5 [id="[$e|0]", label="send uno to b/0.0"]; - n_2 -> n_3 [id="[$e|1]", label="spawn 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"]; } diff --git a/examples/test/foo3/test_0_global_view.dot b/examples/test/foo3/test_0_global_view.dot index 1bf2774..9b9db93 100644 --- a/examples/test/foo3/test_0_global_view.dot +++ b/examples/test/foo3/test_0_global_view.dot @@ -2,40 +2,22 @@ digraph global { rankdir="LR"; n_0 [label="global", shape="plaintext"]; n_1 [id="5", shape=circle, label="5"]; - n_2 [id="15", shape=circle, label="15"]; - n_3 [id="12", shape=circle, label="12"]; - n_4 [id="11", shape=circle, label="11"]; - n_5 [id="17", shape=circle, label="17"]; - n_6 [id="18", shape=circle, label="18"]; - n_7 [id="14", shape=circle, label="14"]; - n_8 [id="6", shape=circle, label="6"]; - n_9 [id="13", shape=circle, label="13"]; - n_10 [id="10", shape=circle, label="10"]; - n_11 [id="1", shape=circle, label="1"]; - n_0 -> n_11 [arrowhead=none]; - n_12 [id="9", shape=circle, label="9"]; - n_13 [id="2", shape=circle, label="2"]; - n_14 [id="8", shape=circle, label="8"]; - n_15 [id="4", shape=circle, label="4"]; - n_16 [id="7", shape=circle, label="7"]; - n_17 [id="3", shape=circle, label="3"]; - n_18 [id="16", shape=circle, label="16"]; + 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_17 -> n_1 [id="[$e|3]", label="a/1.0→test/0.0:3"]; - n_16 -> n_9 [id="[$e|11]", label="b/1.0→test/0.0:2"]; - n_10 -> n_18 [id="[$e|14]", label="a/1.0→test/0.0:1"]; - n_17 -> n_8 [id="[$e|4]", label="b/1.0→test/0.0:2"]; - n_4 -> n_5 [id="[$e|15]", label="a/1.0→test/0.0:3"]; - n_12 -> n_2 [id="[$e|13]", label="b/1.0→test/0.0:2"]; - n_11 -> n_13 [id="[$e|0]", label="test/0.0Δa/1.0"]; - n_15 -> n_14 [id="[$e|6]", label="b/1.0→test/0.0:2"]; - n_3 -> n_6 [id="[$e|16]", label="a/1.0→test/0.0:1"]; - n_15 -> n_16 [id="[$e|5]", label="a/1.0→test/0.0:3"]; - n_8 -> n_4 [id="[$e|9]", label="a/1.0→test/0.0:1"]; - n_14 -> n_7 [id="[$e|12]", label="a/1.0→test/0.0:3"]; - n_17 -> n_15 [id="[$e|2]", label="a/1.0→test/0.0:1"]; - n_13 -> n_17 [id="[$e|1]", label="test/0.0Δb/1.0"]; - n_8 -> n_3 [id="[$e|10]", label="a/1.0→test/0.0:3"]; - n_1 -> n_12 [id="[$e|7]", label="a/1.0→test/0.0:1"]; - n_1 -> n_10 [id="[$e|8]", label="b/1.0→test/0.0:2"]; + 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_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_6 -> n_5 [id="[$e|2]", label="a/1.0→test/0.0:1"]; } diff --git a/examples/test/foo3/test_0_local_view.dot b/examples/test/foo3/test_0_local_view.dot index db2c0f7..8f8087e 100644 --- a/examples/test/foo3/test_0_local_view.dot +++ b/examples/test/foo3/test_0_local_view.dot @@ -10,8 +10,8 @@ digraph test_0 { n_6 [id="3", shape=circle, label="4"]; n_2 -> n_6 [id="[$e|3]", label="receive X"]; - 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_4 -> n_2 [id="[$e|1]", label="spawn b/1.0"]; + n_6 -> n_5 [id="[$e|4]", label="receive Y"]; + n_3 -> n_4 [id="[$e|2]", label="spawn a/1.0"]; } diff --git a/examples/test/foo4/r_0_local_view.dot b/examples/test/foo4/r_0_local_view.dot index fe1aa35..3b88ba0 100644 --- a/examples/test/foo4/r_0_local_view.dot +++ b/examples/test/foo4/r_0_local_view.dot @@ -7,7 +7,7 @@ digraph r_0 { n_3 [id="4", shape=doublecircle, label="4"]; n_4 [id="3", shape=circle, label="2"]; + n_2 -> n_3 [id="[$e|0]", label="receive Z"]; n_4 -> n_2 [id="[$e|2]", label="receive Y"]; n_1 -> n_4 [id="[$e|1]", label="receive X"]; - n_2 -> n_3 [id="[$e|0]", label="receive Z"]; } diff --git a/examples/test/foo4/test_0_global_view.dot b/examples/test/foo4/test_0_global_view.dot index b6fe664..58199c6 100644 --- a/examples/test/foo4/test_0_global_view.dot +++ b/examples/test/foo4/test_0_global_view.dot @@ -2,42 +2,31 @@ digraph global { rankdir="LR"; n_0 [label="global", shape="plaintext"]; n_1 [id="5", shape=circle, label="5"]; - n_2 [id="15", shape=circle, label="15"]; - n_3 [id="19", shape=circle, label="19"]; - n_4 [id="12", shape=circle, label="12"]; - n_5 [id="11", shape=circle, label="11"]; - n_6 [id="17", shape=circle, label="17"]; - n_7 [id="18", shape=circle, label="18"]; - n_8 [id="14", shape=circle, label="14"]; - n_9 [id="6", shape=circle, label="6"]; - n_10 [id="13", shape=circle, label="13"]; - n_11 [id="10", shape=circle, label="10"]; - n_12 [id="1", shape=circle, label="1"]; - n_0 -> n_12 [arrowhead=none]; - n_13 [id="9", shape=circle, label="9"]; - n_14 [id="2", shape=circle, label="2"]; - n_15 [id="8", shape=circle, label="8"]; - n_16 [id="4", shape=circle, label="4"]; - n_17 [id="7", shape=circle, label="7"]; - n_18 [id="3", shape=circle, label="3"]; - n_19 [id="16", shape=circle, label="16"]; + n_2 [id="11", shape=circle, label="11"]; + n_3 [id="6", shape=circle, label="6"]; + n_4 [id="10", shape=circle, label="10"]; + n_5 [id="1", shape=circle, label="1"]; + n_0 -> n_5 [arrowhead=none]; + n_6 [id="9", shape=circle, label="9"]; + n_7 [id="2", shape=circle, label="2"]; + n_8 [id="8", shape=circle, label="8"]; + n_9 [id="4", shape=circle, label="4"]; + n_10 [id="7", shape=circle, label="7"]; + n_11 [id="3", shape=circle, label="3"]; - n_4 -> n_7 [id="[$e|16]", label="test/0.0→w1/1.0:w1"]; - n_16 -> n_1 [id="[$e|3]", label="test/0.0→r/0.0:r0"]; - n_9 -> n_11 [id="[$e|8]", label="test/0.0→r/0.0:r0"]; - n_18 -> n_16 [id="[$e|2]", label="test/0.0Δw2/1.0"]; - n_11 -> n_19 [id="[$e|14]", label="test/0.0→w2/1.0:w2"]; - n_1 -> n_15 [id="[$e|6]", label="test/0.0→w1/1.0:w1"]; - n_15 -> n_8 [id="[$e|12]", label="test/0.0→w2/1.0:w2"]; - n_5 -> n_6 [id="[$e|15]", label="test/0.0→r/0.0:r0"]; - n_16 -> n_17 [id="[$e|5]", label="test/0.0→w2/1.0:w2"]; - n_17 -> n_10 [id="[$e|11]", label="test/0.0→w1/1.0:w1"]; - n_9 -> n_5 [id="[$e|9]", label="test/0.0→w2/1.0:w2"]; - n_14 -> n_18 [id="[$e|1]", label="test/0.0Δw1/1.0"]; - n_16 -> n_9 [id="[$e|4]", label="test/0.0→w1/1.0:w1"]; - n_13 -> n_2 [id="[$e|13]", label="test/0.0→w1/1.0:w1"]; - n_10 -> n_3 [id="[$e|17]", label="test/0.0→r/0.0:r0"]; - n_12 -> n_14 [id="[$e|0]", label="test/0.0Δr/0.0"]; - n_1 -> n_13 [id="[$e|7]", label="test/0.0→w2/1.0:w2"]; - n_17 -> n_4 [id="[$e|10]", label="test/0.0→r/0.0:r0"]; + n_5 -> n_7 [id="[$e|0]", label="test/0.0Δr/0.0"]; + 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_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_6 -> n_2 [id="[$e|13]", label="test/0.0→w1/1.0:w1"]; + 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"]; } diff --git a/examples/test/foo4/test_0_local_view.dot b/examples/test/foo4/test_0_local_view.dot index 1c77c26..fadba73 100644 --- a/examples/test/foo4/test_0_local_view.dot +++ b/examples/test/foo4/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_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_2 -> n_5 [id="[$e|5]", label="send w1 to w1/1.0"]; - n_7 -> n_2 [id="[$e|1]", label="spawn w2/1.0"]; n_4 -> n_6 [id="[$e|4]", label="send r0 to r/0.0"]; - n_6 -> n_7 [id="[$e|0]", label="spawn w1/1.0"]; + n_7 -> n_2 [id="[$e|1]", label="spawn w2/1.0"]; } diff --git a/examples/test/foo4/w1_1_local_view.dot b/examples/test/foo4/w1_1_local_view.dot index d3a44e5..8a83500 100644 --- a/examples/test/foo4/w1_1_local_view.dot +++ b/examples/test/foo4/w1_1_local_view.dot @@ -6,6 +6,6 @@ digraph w1_1 { n_2 [id="2", shape=circle, label="2"]; n_3 [id="3", shape=doublecircle, label="3"]; - n_1 -> n_2 [id="[$e|1]", label="receive _X"]; n_2 -> n_3 [id="[$e|0]", label="send r1 to Reg"]; + n_1 -> n_2 [id="[$e|1]", label="receive _X"]; } diff --git a/examples/test/foo4/w2_1_local_view.dot b/examples/test/foo4/w2_1_local_view.dot index 595d37a..992296a 100644 --- a/examples/test/foo4/w2_1_local_view.dot +++ b/examples/test/foo4/w2_1_local_view.dot @@ -6,6 +6,6 @@ digraph w2_1 { n_2 [id="2", shape=circle, label="2"]; n_3 [id="3", shape=doublecircle, label="3"]; - n_1 -> n_2 [id="[$e|1]", label="receive _X"]; n_2 -> n_3 [id="[$e|0]", label="send r2 to Reg"]; + n_1 -> n_2 [id="[$e|1]", label="receive _X"]; } diff --git a/examples/test/foo5/target_0_local_view.dot b/examples/test/foo5/target_0_local_view.dot index 35c2d94..b330284 100644 --- a/examples/test/foo5/target_0_local_view.dot +++ b/examples/test/foo5/target_0_local_view.dot @@ -9,7 +9,7 @@ digraph target_0 { n_5 [id="3", shape=circle, label="2"]; 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"]; - n_2 -> n_5 [id="[$e|2]", label="receive A"]; } diff --git a/examples/test/foo5/test_0_global_view.dot b/examples/test/foo5/test_0_global_view.dot index fc1138a..552a727 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_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_7 -> n_5 [id="[$e|2]", label="test/0.0→proxy/1.0:m2"]; + 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 5e7992b..044ff5d 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_5 -> n_8 [id="[$e|4]", label="spawn proxy/1.1"]; n_4 -> n_5 [id="[$e|1]", label="spawn proxy/1.0"]; - n_6 -> n_2 [id="[$e|3]", label="send m3 to proxy/1.1"]; + 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_7 -> n_6 [id="[$e|2]", label="send m2 to proxy/1.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 c98f9a0..c7f25db 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_1 -> n_6 [id="[$e|5]", label="test/0.0Δclient/1.0"]; n_3 -> n_4 [id="[$e|0]", label="test/0.0Δserver/0.0"]; - n_7 -> n_1 [id="[$e|3]", label="test/0.0Δclient/1.1"]; + 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_4 -> n_7 [id="[$e|1]", label="test/0.0Δclient/1.1"]; + n_1 -> n_6 [id="[$e|5]", label="test/0.0Δclient/1.0"]; } diff --git a/examples/test/foo6/test_0_local_view.dot b/examples/test/foo6/test_0_local_view.dot index bedf74d..2094185 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_1 -> n_2 [id="[$e|5]", label="spawn server/0.0"]; 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"]; } diff --git a/examples/test/ping/pong_0_local_view.dot b/examples/test/ping/pong_0_local_view.dot index 420d997..3d4aed5 100644 --- a/examples/test/ping/pong_0_local_view.dot +++ b/examples/test/ping/pong_0_local_view.dot @@ -7,8 +7,8 @@ digraph pong_0 { n_3 [id="4", shape=doublecircle, label="4"]; 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_1 -> n_2 [id="[$e|4]", label="receive {S,0}"]; - n_1 -> n_4 [id="[$e|0]", label="receive {S,N}"]; } diff --git a/examples/test/ping/start_0_local_view.dot b/examples/test/ping/start_0_local_view.dot index bdbeb88..bd755ad 100644 --- a/examples/test/ping/start_0_local_view.dot +++ b/examples/test/ping/start_0_local_view.dot @@ -1,16 +1,16 @@ digraph start_0 { rankdir="LR"; n_0 [label="start_0", shape="plaintext"]; - n_1 [id="5", shape=doublecircle, label="5"]; - n_2 [id="6", shape=circle, label="4"]; + n_1 [id="5", shape=circle, label="5"]; + n_2 [id="6", shape=doublecircle, label="4"]; 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="3", shape=circle, label="3"]; - n_4 -> n_5 [id="[$e|7]", label="send 3 to pid_self"]; - n_2 -> n_5 [id="[$e|3]", label="send {pid_self,pid_self} to Pong"]; - n_5 -> n_2 [id="[$e|4]", label="receive N"]; n_3 -> n_4 [id="[$e|1]", label="spawn pong/0.0"]; - n_5 -> n_1 [id="[$e|0]", label="receive kill"]; + n_4 -> n_5 [id="[$e|7]", label="send 3 to pid_self"]; + n_5 -> n_2 [id="[$e|0]", label="receive kill"]; + n_5 -> n_1 [id="[$e|4]", label="receive N"]; + n_1 -> n_5 [id="[$e|3]", label="send {pid_self,pid_self} to Pong"]; } diff --git a/examples/ticktackloop/start_0_global_view.dot b/examples/ticktackloop/start_0_global_view.dot index 0fde053..a77ed31 100644 --- a/examples/ticktackloop/start_0_global_view.dot +++ b/examples/ticktackloop/start_0_global_view.dot @@ -9,8 +9,8 @@ digraph global { n_5 [id="3", shape=circle, label="3"]; 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_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_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"]; } diff --git a/examples/ticktackloop/start_0_local_view.dot b/examples/ticktackloop/start_0_local_view.dot index 2518cab..865aadd 100644 --- a/examples/ticktackloop/start_0_local_view.dot +++ b/examples/ticktackloop/start_0_local_view.dot @@ -7,7 +7,7 @@ digraph start_0 { n_3 [id="4", shape=circle, label="2"]; n_4 [id="3", shape=doublecircle, label="4"]; - n_2 -> n_4 [id="[$e|1]", label="send tac to tic_loop/0.0"]; 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"]; } diff --git a/examples/ticktackloop/tac_loop_0_local_view.dot b/examples/ticktackloop/tac_loop_0_local_view.dot index 157f4cb..cc628e8 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_4 -> n_3 [id="[$e|3]", label="send stop to tic_loop/0.0"]; 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_1 -> n_4 [id="[$e|0]", label="receive stop"]; } diff --git a/examples/ticktackloop/tic_loop_0_local_view.dot b/examples/ticktackloop/tic_loop_0_local_view.dot index c72bd8d..6e1ce0f 100644 --- a/examples/ticktackloop/tic_loop_0_local_view.dot +++ b/examples/ticktackloop/tic_loop_0_local_view.dot @@ -8,7 +8,7 @@ digraph tic_loop_0 { n_4 [id="3", shape=circle, label="2"]; n_2 -> n_1 [id="[$e|6]", label="send tic to tac_loop/0.0"]; - n_4 -> n_3 [id="[$e|4]", label="send stop 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"]; } diff --git a/examples/ticktackstop/start_0_global_view.dot b/examples/ticktackstop/start_0_global_view.dot index 94ac355..2f98ff8 100644 --- a/examples/ticktackstop/start_0_global_view.dot +++ b/examples/ticktackstop/start_0_global_view.dot @@ -2,32 +2,27 @@ digraph global { rankdir="LR"; n_0 [label="global", shape="plaintext"]; n_1 [id="5", shape=circle, label="5"]; - n_2 [id="12", shape=circle, label="12"]; - n_3 [id="11", shape=circle, label="11"]; - n_4 [id="14", shape=circle, label="14"]; - n_5 [id="6", shape=circle, label="6"]; - n_6 [id="13", shape=circle, label="13"]; - n_7 [id="10", shape=circle, label="10"]; - n_8 [id="1", shape=circle, label="1"]; - n_0 -> n_8 [arrowhead=none]; - n_9 [id="9", shape=circle, label="9"]; - n_10 [id="2", shape=circle, label="2"]; - n_11 [id="8", shape=circle, label="8"]; - n_12 [id="4", shape=circle, label="4"]; - n_13 [id="7", shape=circle, label="7"]; - n_14 [id="3", shape=circle, label="3"]; + n_2 [id="6", shape=circle, label="6"]; + n_3 [id="10", shape=circle, label="10"]; + n_4 [id="1", shape=circle, label="1"]; + n_0 -> n_4 [arrowhead=none]; + n_5 [id="9", shape=circle, label="9"]; + n_6 [id="2", shape=circle, label="2"]; + n_7 [id="8", shape=circle, label="8"]; + n_8 [id="4", shape=circle, label="4"]; + n_9 [id="7", shape=circle, label="7"]; + n_10 [id="3", shape=circle, label="3"]; - n_11 -> n_2 [id="[$e|10]", label="tic_loop/0.0→tac_loop/0.0:stop"]; - n_7 -> n_6 [id="[$e|11]", label="tic_loop/0.0→tac_loop/0.0:stop"]; - n_11 -> n_3 [id="[$e|9]", label="tic_loop/0.0→tac_loop/0.0:tic"]; - n_3 -> n_4 [id="[$e|12]", label="tic_loop/0.0→tac_loop/0.0:stop"]; - n_13 -> n_7 [id="[$e|8]", label="random/0.0→tic_loop/0.0:stop"]; - n_1 -> n_11 [id="[$e|6]", label="random/0.0→tic_loop/0.0:stop"]; - n_12 -> n_1 [id="[$e|3]", label="start/0.0→tic_loop/0.0:tac"]; - n_14 -> n_12 [id="[$e|2]", label="start/0.0Δrandom/0.0"]; - n_1 -> n_13 [id="[$e|5]", label="tic_loop/0.0→tac_loop/0.0:tic"]; - n_10 -> n_14 [id="[$e|1]", label="start/0.0Δtic_loop/0.0"]; - n_12 -> n_5 [id="[$e|4]", label="random/0.0→tic_loop/0.0:stop"]; - n_5 -> n_9 [id="[$e|7]", label="tic_loop/0.0→tac_loop/0.0:stop"]; - n_8 -> n_10 [id="[$e|0]", label="start/0.0Δtac_loop/0.0"]; + 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_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_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"]; } diff --git a/examples/ticktackstop/start_0_local_view.dot b/examples/ticktackstop/start_0_local_view.dot index 29bfdc2..d287270 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_1 -> n_3 [id="[$e|3]", label="spawn random/0.0"]; 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"]; } diff --git a/examples/ticktackstop/tac_loop_0_local_view.dot b/examples/ticktackstop/tac_loop_0_local_view.dot index 301ae75..d13a659 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_1 -> n_3 [id="[$e|6]", label="receive tic"]; + 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_2 [id="[$e|1]", label="receive stop"]; - n_3 -> n_1 [id="[$e|7]", label="send tac to tic_loop/0.0"]; } diff --git a/examples/ticktackstop/tic_loop_0_local_view.dot b/examples/ticktackstop/tic_loop_0_local_view.dot index 6e1ce0f..f798171 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_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_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"]; } diff --git a/examples/trick/main_0_global_view.dot b/examples/trick/main_0_global_view.dot index ff0258d..c3ceb7d 100644 --- a/examples/trick/main_0_global_view.dot +++ b/examples/trick/main_0_global_view.dot @@ -3,23 +3,22 @@ digraph global { 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="10", shape=circle, label="10"]; - n_4 [id="1", shape=circle, label="1"]; - n_0 -> n_4 [arrowhead=none]; - n_5 [id="9", shape=circle, label="9"]; - n_6 [id="2", shape=circle, label="2"]; - n_7 [id="8", shape=circle, label="8"]; - n_8 [id="4", shape=circle, label="4"]; - n_9 [id="7", shape=circle, label="7"]; - n_10 [id="3", shape=circle, label="3"]; + n_3 [id="1", shape=circle, label="1"]; + n_0 -> n_3 [arrowhead=none]; + n_4 [id="9", shape=circle, label="9"]; + n_5 [id="2", shape=circle, label="2"]; + n_6 [id="8", shape=circle, label="8"]; + n_7 [id="4", shape=circle, label="4"]; + n_8 [id="7", shape=circle, label="7"]; + n_9 [id="3", shape=circle, label="3"]; - n_8 -> n_1 [id="[$e|3]", label="a/0.0→b/0.0:v2"]; - n_7 -> n_3 [id="[$e|8]", label="b/0.0→c/0.0:v2"]; - n_6 -> n_10 [id="[$e|1]", label="main/0.0Δb/0.0"]; - n_2 -> n_7 [id="[$e|6]", label="a/0.0→b/0.0:v2"]; - n_8 -> n_2 [id="[$e|4]", label="a/0.0→c/0.0:v1"]; - n_9 -> n_5 [id="[$e|7]", label="b/0.0→c/0.0:v2"]; - n_10 -> n_8 [id="[$e|2]", label="main/0.0Δc/0.0"]; - n_1 -> n_9 [id="[$e|5]", label="a/0.0→c/0.0:v1"]; - n_4 -> n_6 [id="[$e|0]", label="main/0.0Δa/0.0"]; + 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_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_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"]; } diff --git a/examples/trick/main_0_local_view.dot b/examples/trick/main_0_local_view.dot index f2ce64f..704266d 100644 --- a/examples/trick/main_0_local_view.dot +++ b/examples/trick/main_0_local_view.dot @@ -7,7 +7,7 @@ digraph main_0 { n_3 [id="4", shape=circle, label="3"]; n_4 [id="3", shape=doublecircle, label="4"]; - n_3 -> n_4 [id="[$e|1]", label="spawn c/0.0"]; 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"]; } diff --git a/examples/violation/incrementer_0_local_view.dot b/examples/violation/incrementer_0_local_view.dot index cb7b598..f127573 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,write} to varManager/1.0"]; - 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_4 -> n_6 [id="[$e|0]", label="receive answer"]; - n_6 -> n_7 [id="[$e|4]", label="send {read,pid_self} to varManager/1.0"]; + 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/violation/main_0_global_view.dot b/examples/violation/main_0_global_view.dot index b779acc..bc930bc 100644 --- a/examples/violation/main_0_global_view.dot +++ b/examples/violation/main_0_global_view.dot @@ -5,267 +5,316 @@ digraph global { n_2 [id="34", shape=circle, label="34"]; n_3 [id="20", shape=circle, label="20"]; n_4 [id="58", shape=circle, label="58"]; - n_5 [id="119", shape=circle, label="119"]; - n_6 [id="129", shape=circle, label="129"]; - n_7 [id="57", shape=circle, label="57"]; - n_8 [id="98", shape=circle, label="98"]; - n_9 [id="91", shape=circle, label="91"]; - n_10 [id="78", shape=circle, label="78"]; - n_11 [id="102", shape=circle, label="102"]; - n_12 [id="27", shape=circle, label="27"]; - n_13 [id="118", shape=circle, label="118"]; - n_14 [id="114", shape=circle, label="114"]; - n_15 [id="89", shape=circle, label="89"]; - n_16 [id="47", shape=circle, label="47"]; - n_17 [id="29", shape=circle, label="29"]; - n_18 [id="23", shape=circle, label="23"]; - n_19 [id="110", shape=circle, label="110"]; - n_20 [id="72", shape=circle, label="72"]; - n_21 [id="122", shape=circle, label="122"]; - n_22 [id="55", shape=circle, label="55"]; - n_23 [id="82", shape=circle, label="82"]; - n_24 [id="117", shape=circle, label="117"]; - n_25 [id="25", shape=circle, label="25"]; - n_26 [id="120", shape=circle, label="120"]; - n_27 [id="68", shape=circle, label="68"]; - n_28 [id="83", shape=circle, label="83"]; - n_29 [id="36", shape=circle, label="36"]; - n_30 [id="94", shape=circle, label="94"]; - n_31 [id="84", shape=circle, label="84"]; - n_32 [id="5", shape=circle, label="5"]; - n_33 [id="81", shape=circle, label="81"]; - n_34 [id="74", shape=circle, label="74"]; - n_35 [id="92", shape=circle, label="92"]; - n_36 [id="63", shape=circle, label="63"]; - n_37 [id="28", shape=circle, label="28"]; - n_38 [id="64", shape=circle, label="64"]; - n_39 [id="86", shape=circle, label="86"]; - n_40 [id="15", shape=circle, label="15"]; - n_41 [id="87", shape=circle, label="87"]; - n_42 [id="42", shape=circle, label="42"]; - n_43 [id="19", shape=circle, label="19"]; - n_44 [id="12", shape=circle, label="12"]; - n_45 [id="11", shape=circle, label="11"]; - n_46 [id="116", shape=circle, label="116"]; - n_47 [id="112", shape=circle, label="112"]; - n_48 [id="99", shape=circle, label="99"]; - n_49 [id="17", shape=circle, label="17"]; - n_50 [id="53", shape=circle, label="53"]; - n_51 [id="50", shape=circle, label="50"]; - n_52 [id="62", shape=circle, label="62"]; - n_53 [id="67", shape=circle, label="67"]; - n_54 [id="54", shape=circle, label="54"]; - n_55 [id="18", shape=circle, label="18"]; - n_56 [id="61", shape=circle, label="61"]; - n_57 [id="113", shape=circle, label="113"]; - n_58 [id="37", shape=circle, label="37"]; - n_59 [id="80", shape=circle, label="80"]; - n_60 [id="51", shape=circle, label="51"]; - n_61 [id="14", shape=circle, label="14"]; - n_62 [id="66", shape=circle, label="66"]; - n_63 [id="93", shape=circle, label="93"]; - n_64 [id="132", shape=circle, label="132"]; - n_65 [id="100", shape=circle, label="100"]; - n_66 [id="6", shape=circle, label="6"]; - n_67 [id="126", shape=circle, label="126"]; - n_68 [id="38", shape=circle, label="38"]; - n_69 [id="13", shape=circle, label="13"]; - n_70 [id="24", shape=circle, label="24"]; - n_71 [id="10", shape=circle, label="10"]; - n_72 [id="79", shape=circle, label="79"]; - n_73 [id="43", shape=circle, label="43"]; - n_74 [id="30", shape=circle, label="30"]; - n_75 [id="71", shape=circle, label="71"]; - n_76 [id="59", shape=circle, label="59"]; - n_77 [id="40", shape=circle, label="40"]; - n_78 [id="22", shape=circle, label="22"]; - n_79 [id="105", shape=circle, label="105"]; - n_80 [id="106", shape=circle, label="106"]; - n_81 [id="101", shape=circle, label="101"]; - n_82 [id="65", shape=circle, label="65"]; - n_83 [id="73", shape=circle, label="73"]; - n_84 [id="131", shape=circle, label="131"]; - n_85 [id="39", shape=circle, label="39"]; - n_86 [id="123", shape=circle, label="123"]; - n_87 [id="108", shape=circle, label="108"]; - n_88 [id="60", shape=circle, label="60"]; - n_89 [id="1", shape=circle, label="1"]; - n_0 -> n_89 [arrowhead=none]; - n_90 [id="115", shape=circle, label="115"]; - n_91 [id="45", shape=circle, label="45"]; - n_92 [id="26", shape=circle, label="26"]; - n_93 [id="133", shape=circle, label="133"]; - n_94 [id="76", shape=circle, label="76"]; - n_95 [id="9", shape=circle, label="9"]; - n_96 [id="2", shape=circle, label="2"]; - n_97 [id="104", shape=circle, label="104"]; - n_98 [id="97", shape=circle, label="97"]; - n_99 [id="21", shape=circle, label="21"]; - n_100 [id="127", shape=circle, label="127"]; - n_101 [id="107", shape=circle, label="107"]; - n_102 [id="44", shape=circle, label="44"]; - n_103 [id="69", shape=circle, label="69"]; - n_104 [id="46", shape=circle, label="46"]; - n_105 [id="95", shape=circle, label="95"]; - n_106 [id="77", shape=circle, label="77"]; - n_107 [id="8", shape=circle, label="8"]; - n_108 [id="96", shape=circle, label="96"]; - n_109 [id="124", shape=circle, label="124"]; - n_110 [id="48", shape=circle, label="48"]; - n_111 [id="88", shape=circle, label="88"]; - n_112 [id="109", shape=circle, label="109"]; - n_113 [id="130", shape=circle, label="130"]; - n_114 [id="103", shape=circle, label="103"]; - n_115 [id="128", shape=circle, label="128"]; - n_116 [id="4", shape=circle, label="4"]; - n_117 [id="70", shape=circle, label="70"]; - n_118 [id="35", shape=circle, label="35"]; - n_119 [id="121", shape=circle, label="121"]; - n_120 [id="31", shape=circle, label="31"]; - n_121 [id="32", shape=circle, label="32"]; - n_122 [id="85", shape=circle, label="85"]; - n_123 [id="41", shape=circle, label="41"]; - n_124 [id="7", shape=circle, label="7"]; - n_125 [id="90", shape=circle, label="90"]; - n_126 [id="75", shape=circle, label="75"]; - n_127 [id="3", shape=circle, label="3"]; - n_128 [id="52", shape=circle, label="52"]; - n_129 [id="56", shape=circle, label="56"]; - n_130 [id="125", shape=circle, label="125"]; - n_131 [id="49", shape=circle, label="49"]; - n_132 [id="111", shape=circle, label="111"]; - n_133 [id="16", shape=circle, label="16"]; + n_5 [id="57", shape=circle, label="57"]; + n_6 [id="91", shape=circle, label="91"]; + n_7 [id="78", shape=circle, label="78"]; + n_8 [id="27", shape=circle, label="27"]; + n_9 [id="89", shape=circle, label="89"]; + n_10 [id="47", shape=circle, label="47"]; + n_11 [id="29", shape=circle, label="29"]; + n_12 [id="23", shape=circle, label="23"]; + n_13 [id="72", shape=circle, label="72"]; + n_14 [id="55", shape=circle, label="55"]; + n_15 [id="82", shape=circle, label="82"]; + n_16 [id="25", shape=circle, label="25"]; + n_17 [id="68", shape=circle, label="68"]; + n_18 [id="83", shape=circle, label="83"]; + n_19 [id="36", shape=circle, label="36"]; + n_20 [id="84", shape=circle, label="84"]; + n_21 [id="5", shape=circle, label="5"]; + n_22 [id="81", shape=circle, label="81"]; + n_23 [id="74", shape=circle, label="74"]; + n_24 [id="92", shape=circle, label="92"]; + n_25 [id="63", shape=circle, label="63"]; + n_26 [id="28", shape=circle, label="28"]; + n_27 [id="64", shape=circle, label="64"]; + n_28 [id="86", shape=circle, label="86"]; + n_29 [id="15", shape=circle, label="15"]; + n_30 [id="87", shape=circle, label="87"]; + n_31 [id="42", shape=circle, label="42"]; + n_32 [id="19", shape=circle, label="19"]; + n_33 [id="12", shape=circle, label="12"]; + n_34 [id="11", shape=circle, label="11"]; + n_35 [id="17", shape=circle, label="17"]; + n_36 [id="53", shape=circle, label="53"]; + n_37 [id="50", shape=circle, label="50"]; + n_38 [id="62", shape=circle, label="62"]; + n_39 [id="67", shape=circle, label="67"]; + n_40 [id="54", shape=circle, label="54"]; + n_41 [id="18", shape=circle, label="18"]; + n_42 [id="61", shape=circle, label="61"]; + n_43 [id="37", shape=circle, label="37"]; + n_44 [id="80", shape=circle, label="80"]; + n_45 [id="51", shape=circle, label="51"]; + n_46 [id="14", shape=circle, label="14"]; + n_47 [id="66", shape=circle, label="66"]; + n_48 [id="6", shape=circle, label="6"]; + n_49 [id="38", shape=circle, label="38"]; + n_50 [id="13", shape=circle, label="13"]; + n_51 [id="24", shape=circle, label="24"]; + n_52 [id="10", shape=circle, label="10"]; + n_53 [id="79", shape=circle, label="79"]; + n_54 [id="43", shape=circle, label="43"]; + n_55 [id="30", shape=circle, label="30"]; + n_56 [id="71", shape=circle, label="71"]; + n_57 [id="59", shape=circle, label="59"]; + n_58 [id="40", shape=circle, label="40"]; + n_59 [id="22", shape=circle, label="22"]; + n_60 [id="65", shape=circle, label="65"]; + n_61 [id="73", shape=circle, label="73"]; + n_62 [id="39", shape=circle, label="39"]; + n_63 [id="60", shape=circle, label="60"]; + n_64 [id="1", shape=circle, label="1"]; + n_0 -> n_64 [arrowhead=none]; + n_65 [id="45", shape=circle, label="45"]; + n_66 [id="26", shape=circle, label="26"]; + n_67 [id="76", shape=circle, label="76"]; + n_68 [id="9", shape=circle, label="9"]; + n_69 [id="2", shape=circle, label="2"]; + n_70 [id="21", shape=circle, label="21"]; + n_71 [id="44", shape=circle, label="44"]; + n_72 [id="69", shape=circle, label="69"]; + n_73 [id="46", shape=circle, label="46"]; + n_74 [id="77", shape=circle, label="77"]; + n_75 [id="8", shape=circle, label="8"]; + n_76 [id="48", shape=circle, label="48"]; + n_77 [id="88", shape=circle, label="88"]; + n_78 [id="4", shape=circle, label="4"]; + n_79 [id="70", shape=circle, label="70"]; + n_80 [id="35", shape=circle, label="35"]; + n_81 [id="31", shape=circle, label="31"]; + n_82 [id="32", shape=circle, label="32"]; + n_83 [id="85", shape=circle, label="85"]; + n_84 [id="41", shape=circle, label="41"]; + n_85 [id="7", shape=circle, label="7"]; + n_86 [id="90", shape=circle, label="90"]; + n_87 [id="75", shape=circle, label="75"]; + n_88 [id="3", shape=circle, label="3"]; + n_89 [id="52", shape=circle, label="52"]; + n_90 [id="56", shape=circle, label="56"]; + n_91 [id="49", shape=circle, label="49"]; + n_92 [id="16", shape=circle, label="16"]; - n_33 -> n_57 [id="[$e|111]", label="incrementer/0.1→meManager/0.0:{release}"]; - n_133 -> n_78 [id="[$e|20]", label="incrementer/0.1→varManager/1.0:{write,write}"]; - n_60 -> n_62 [id="[$e|64]", label="incrementer/0.1→varManager/1.0:{write,write}"]; - n_96 -> n_127 [id="[$e|1]", label="main/0.0ΔvarManager/1.0"]; - n_63 -> n_130 [id="[$e|123]", label="incrementer/0.1→varManager/1.0:{write,write}"]; - n_78 -> n_74 [id="[$e|28]", label="incrementer/0.0→meManager/0.0:{request,pid_self}"]; - n_17 -> n_85 [id="[$e|37]", label="incrementer/0.0→varManager/1.0:{read,pid_self}"]; - n_99 -> n_37 [id="[$e|26]", label="incrementer/0.1→varManager/1.0:{write,write}"]; - n_121 -> n_42 [id="[$e|40]", label="incrementer/0.1→varManager/1.0:{read,pid_self}"]; - n_99 -> n_17 [id="[$e|27]", label="meManager/0.0→incrementer/0.0:answer"]; - n_92 -> n_118 [id="[$e|33]", label="meManager/0.0→incrementer/0.1:answer"]; - n_83 -> n_79 [id="[$e|103]", label="incrementer/0.1→meManager/0.0:{release}"]; - n_27 -> n_8 [id="[$e|96]", label="incrementer/0.0→meManager/0.0:{release}"]; - n_44 -> n_40 [id="[$e|13]", label="incrementer/0.0→varManager/1.0:{write,write}"]; - n_108 -> n_115 [id="[$e|126]", label="incrementer/0.1→varManager/1.0:{write,write}"]; - n_23 -> n_14 [id="[$e|112]", label="incrementer/0.1→varManager/1.0:{write,write}"]; - n_36 -> n_111 [id="[$e|86]", label="incrementer/0.0→meManager/0.0:{release}"]; - n_54 -> n_117 [id="[$e|68]", label="incrementer/0.1→meManager/0.0:{release}"]; - n_17 -> n_68 [id="[$e|36]", label="incrementer/0.1→varManager/1.0:{write,write}"]; - n_111 -> n_26 [id="[$e|118]", label="incrementer/0.0→varManager/1.0:{write,write}"]; - n_55 -> n_25 [id="[$e|23]", label="meManager/0.0→incrementer/0.1:answer"]; - n_81 -> n_93 [id="[$e|131]", label="incrementer/0.0→meManager/0.0:{release}"]; - n_12 -> n_29 [id="[$e|34]", label="meManager/0.0→incrementer/0.1:answer"]; - n_34 -> n_80 [id="[$e|104]", label="incrementer/0.1→varManager/1.0:{write,write}"]; - n_38 -> n_9 [id="[$e|89]", label="incrementer/0.0→varManager/1.0:{write,write}"]; - n_88 -> n_23 [id="[$e|80]", label="incrementer/0.1→meManager/0.0:{release}"]; - n_95 -> n_45 [id="[$e|9]", label="incrementer/0.1→varManager/1.0:{read,pid_self}"]; - n_59 -> n_47 [id="[$e|110]", label="incrementer/0.0→varManager/1.0:{write,write}"]; - n_107 -> n_71 [id="[$e|8]", label="incrementer/0.0→varManager/1.0:{read,pid_self}"]; - n_94 -> n_87 [id="[$e|106]", label="incrementer/0.1→varManager/1.0:{write,write}"]; - n_103 -> n_65 [id="[$e|98]", label="incrementer/0.0→meManager/0.0:{release}"]; - n_91 -> n_7 [id="[$e|55]", label="incrementer/0.1→meManager/0.0:{release}"]; - n_131 -> n_36 [id="[$e|61]", label="varManager/1.0→incrementer/0.0:Val"]; - n_127 -> n_116 [id="[$e|2]", label="main/0.0Δincrementer/0.0"]; - n_22 -> n_83 [id="[$e|71]", label="incrementer/0.1→varManager/1.0:{write,write}"]; - n_88 -> n_28 [id="[$e|81]", label="incrementer/0.1→varManager/1.0:{write,write}"]; - n_56 -> n_122 [id="[$e|83]", label="incrementer/0.1→varManager/1.0:{write,write}"]; - n_126 -> n_101 [id="[$e|105]", label="incrementer/0.1→meManager/0.0:{release}"]; - n_72 -> n_132 [id="[$e|109]", label="incrementer/0.1→meManager/0.0:{release}"]; - n_53 -> n_98 [id="[$e|95]", label="incrementer/0.1→varManager/1.0:{write,write}"]; - n_7 -> n_106 [id="[$e|75]", label="incrementer/0.1→varManager/1.0:{write,write}"]; - n_118 -> n_104 [id="[$e|44]", label="incrementer/0.1→varManager/1.0:{read,pid_self}"]; - n_102 -> n_129 [id="[$e|54]", label="varManager/1.0→incrementer/0.1:Val"]; - n_66 -> n_107 [id="[$e|6]", label="meManager/0.0→incrementer/0.0:answer"]; - n_76 -> n_33 [id="[$e|79]", label="incrementer/0.0→varManager/1.0:{write,write}"]; - n_25 -> n_2 [id="[$e|32]", label="incrementer/0.1→varManager/1.0:{read,pid_self}"]; - n_76 -> n_59 [id="[$e|78]", label="incrementer/0.1→meManager/0.0:{release}"]; - n_65 -> n_64 [id="[$e|130]", label="incrementer/0.0→varManager/1.0:{write,write}"]; - n_129 -> n_126 [id="[$e|73]", label="incrementer/0.1→varManager/1.0:{write,write}"]; - n_104 -> n_88 [id="[$e|58]", label="varManager/1.0→incrementer/0.1:Val"]; - n_25 -> n_1 [id="[$e|31]", label="incrementer/0.0→varManager/1.0:{write,write}"]; - n_77 -> n_128 [id="[$e|50]", label="incrementer/0.0→varManager/1.0:{read,pid_self}"]; - n_36 -> n_15 [id="[$e|87]", label="incrementer/0.0→varManager/1.0:{write,write}"]; - n_50 -> n_103 [id="[$e|67]", label="varManager/1.0→incrementer/0.0:Val"]; - n_85 -> n_60 [id="[$e|49]", label="varManager/1.0→incrementer/0.0:Val"]; - n_116 -> n_32 [id="[$e|3]", label="main/0.0Δincrementer/0.1"]; - n_89 -> n_96 [id="[$e|0]", label="main/0.0ΔmeManager/0.0"]; - n_54 -> n_75 [id="[$e|69]", label="incrementer/0.1→varManager/1.0:{write,write}"]; - n_45 -> n_69 [id="[$e|11]", label="varManager/1.0→incrementer/0.1:Val"]; - n_37 -> n_58 [id="[$e|35]", label="meManager/0.0→incrementer/0.0:answer"]; - n_16 -> n_56 [id="[$e|59]", label="varManager/1.0→incrementer/0.1:Val"]; - n_60 -> n_82 [id="[$e|63]", label="incrementer/0.0→meManager/0.0:{release}"]; - n_41 -> n_5 [id="[$e|117]", label="incrementer/0.0→meManager/0.0:{release}"]; - n_9 -> n_86 [id="[$e|121]", label="incrementer/0.0→meManager/0.0:{release}"]; - n_42 -> n_54 [id="[$e|52]", label="varManager/1.0→incrementer/0.1:Val"]; - n_122 -> n_24 [id="[$e|115]", label="incrementer/0.1→meManager/0.0:{release}"]; - n_70 -> n_121 [id="[$e|30]", label="meManager/0.0→incrementer/0.1:answer"]; - n_8 -> n_113 [id="[$e|128]", label="incrementer/0.0→varManager/1.0:{write,write}"]; - n_31 -> n_46 [id="[$e|114]", label="incrementer/0.1→varManager/1.0:{write,write}"]; - n_128 -> n_27 [id="[$e|66]", label="varManager/1.0→incrementer/0.0:Val"]; - n_68 -> n_131 [id="[$e|47]", label="incrementer/0.0→varManager/1.0:{read,pid_self}"]; - n_61 -> n_43 [id="[$e|17]", label="incrementer/0.0→varManager/1.0:{write,write}"]; - n_27 -> n_48 [id="[$e|97]", label="incrementer/0.0→varManager/1.0:{write,write}"]; - n_69 -> n_49 [id="[$e|15]", label="incrementer/0.1→varManager/1.0:{write,write}"]; - n_103 -> n_81 [id="[$e|99]", label="incrementer/0.0→varManager/1.0:{write,write}"]; - n_32 -> n_66 [id="[$e|4]", label="incrementer/0.0→meManager/0.0:{request,pid_self}"]; - n_52 -> n_41 [id="[$e|85]", label="incrementer/0.0→varManager/1.0:{write,write}"]; - n_105 -> n_100 [id="[$e|125]", label="incrementer/0.0→meManager/0.0:{release}"]; - n_129 -> n_34 [id="[$e|72]", label="incrementer/0.1→meManager/0.0:{release}"]; - n_60 -> n_53 [id="[$e|65]", label="incrementer/0.0→varManager/1.0:{write,write}"]; - n_3 -> n_12 [id="[$e|25]", label="incrementer/0.1→meManager/0.0:{request,pid_self}"]; - n_56 -> n_31 [id="[$e|82]", label="incrementer/0.1→meManager/0.0:{release}"]; - n_43 -> n_92 [id="[$e|24]", label="incrementer/0.1→meManager/0.0:{request,pid_self}"]; - n_53 -> n_108 [id="[$e|94]", label="incrementer/0.0→meManager/0.0:{release}"]; - n_62 -> n_30 [id="[$e|92]", label="incrementer/0.0→meManager/0.0:{release}"]; - n_35 -> n_109 [id="[$e|122]", label="incrementer/0.0→varManager/1.0:{write,write}"]; - n_1 -> n_73 [id="[$e|41]", label="incrementer/0.1→varManager/1.0:{read,pid_self}"]; - n_110 -> n_52 [id="[$e|60]", label="varManager/1.0→incrementer/0.0:Val"]; - n_123 -> n_50 [id="[$e|51]", label="incrementer/0.0→varManager/1.0:{read,pid_self}"]; - n_39 -> n_13 [id="[$e|116]", label="incrementer/0.0→varManager/1.0:{write,write}"]; - n_38 -> n_125 [id="[$e|88]", label="incrementer/0.0→meManager/0.0:{release}"]; - n_4 -> n_72 [id="[$e|77]", label="incrementer/0.1→varManager/1.0:{write,write}"]; - n_62 -> n_105 [id="[$e|93]", label="incrementer/0.0→varManager/1.0:{write,write}"]; - n_82 -> n_35 [id="[$e|90]", label="incrementer/0.1→varManager/1.0:{write,write}"]; - n_29 -> n_16 [id="[$e|45]", label="incrementer/0.1→varManager/1.0:{read,pid_self}"]; - n_18 -> n_120 [id="[$e|29]", label="incrementer/0.0→meManager/0.0:{request,pid_self}"]; - n_91 -> n_4 [id="[$e|56]", label="incrementer/0.0→varManager/1.0:{write,write}"]; - n_20 -> n_97 [id="[$e|102]", label="incrementer/0.1→varManager/1.0:{write,write}"]; - n_61 -> n_55 [id="[$e|16]", label="incrementer/0.1→meManager/0.0:{request,pid_self}"]; - n_51 -> n_38 [id="[$e|62]", label="varManager/1.0→incrementer/0.0:Val"]; - n_40 -> n_3 [id="[$e|18]", label="incrementer/0.0→meManager/0.0:{release}"]; - n_75 -> n_114 [id="[$e|101]", label="incrementer/0.1→meManager/0.0:{release}"]; - n_117 -> n_11 [id="[$e|100]", label="incrementer/0.1→varManager/1.0:{write,write}"]; - n_32 -> n_124 [id="[$e|5]", label="incrementer/0.1→meManager/0.0:{request,pid_self}"]; - n_10 -> n_19 [id="[$e|108]", label="incrementer/0.1→varManager/1.0:{write,write}"]; - n_85 -> n_51 [id="[$e|48]", label="incrementer/0.1→varManager/1.0:{write,write}"]; - n_69 -> n_133 [id="[$e|14]", label="incrementer/0.1→meManager/0.0:{release}"]; - n_125 -> n_21 [id="[$e|120]", label="incrementer/0.0→varManager/1.0:{write,write}"]; - n_106 -> n_112 [id="[$e|107]", label="incrementer/0.0→varManager/1.0:{write,write}"]; - n_58 -> n_110 [id="[$e|46]", label="incrementer/0.0→varManager/1.0:{read,pid_self}"]; - n_98 -> n_6 [id="[$e|127]", label="incrementer/0.0→meManager/0.0:{release}"]; - n_4 -> n_10 [id="[$e|76]", label="incrementer/0.1→meManager/0.0:{release}"]; - n_2 -> n_102 [id="[$e|42]", label="incrementer/0.0→varManager/1.0:{write,write}"]; - n_49 -> n_18 [id="[$e|21]", label="incrementer/0.1→meManager/0.0:{release}"]; - n_15 -> n_119 [id="[$e|119]", label="incrementer/0.0→meManager/0.0:{release}"]; - n_52 -> n_39 [id="[$e|84]", label="incrementer/0.0→meManager/0.0:{release}"]; - n_22 -> n_20 [id="[$e|70]", label="incrementer/0.1→meManager/0.0:{release}"]; - n_91 -> n_76 [id="[$e|57]", label="incrementer/0.1→varManager/1.0:{write,write}"]; - n_82 -> n_63 [id="[$e|91]", label="incrementer/0.0→varManager/1.0:{write,write}"]; - n_55 -> n_70 [id="[$e|22]", label="incrementer/0.0→varManager/1.0:{write,write}"]; - n_44 -> n_61 [id="[$e|12]", label="incrementer/0.0→meManager/0.0:{release}"]; - n_124 -> n_95 [id="[$e|7]", label="meManager/0.0→incrementer/0.1:answer"]; - n_48 -> n_84 [id="[$e|129]", label="incrementer/0.0→meManager/0.0:{release}"]; - n_74 -> n_77 [id="[$e|38]", label="meManager/0.0→incrementer/0.0:answer"]; - n_30 -> n_67 [id="[$e|124]", label="incrementer/0.0→varManager/1.0:{write,write}"]; - n_73 -> n_22 [id="[$e|53]", label="varManager/1.0→incrementer/0.1:Val"]; - n_133 -> n_99 [id="[$e|19]", label="incrementer/0.0→meManager/0.0:{request,pid_self}"]; - n_7 -> n_94 [id="[$e|74]", label="incrementer/0.0→varManager/1.0:{write,write}"]; - n_120 -> n_123 [id="[$e|39]", label="meManager/0.0→incrementer/0.0:answer"]; - n_2 -> n_91 [id="[$e|43]", label="varManager/1.0→incrementer/0.1:Val"]; - n_71 -> n_44 [id="[$e|10]", label="varManager/1.0→incrementer/0.0:Val"]; - n_28 -> n_90 [id="[$e|113]", label="incrementer/0.1→meManager/0.0:{release}"]; + n_42 -> n_74 [id="[$e|170]", label="varManager/1.0→incrementer/0.3:Val"]; + n_51 -> n_12 [id="[$e|39]", label="incrementer/0.1→meManager/0.0:{release}"]; + n_75 -> n_52 [id="[$e|11]", label="meManager/0.0→incrementer/0.1:answer"]; + n_53 -> n_86 [id="[$e|180]", label="incrementer/0.3→varManager/1.0:{write,write}"]; + n_89 -> n_13 [id="[$e|113]", label="varManager/1.0→incrementer/0.0:Val"]; + n_62 -> n_5 [id="[$e|85]", label="incrementer/0.2→varManager/1.0:{write,write}"]; + n_19 -> n_89 [id="[$e|77]", label="incrementer/0.0→varManager/1.0:{read,pid_self}"]; + n_55 -> n_19 [id="[$e|55]", label="meManager/0.0→incrementer/0.0:answer"]; + n_84 -> n_38 [id="[$e|92]", label="incrementer/0.3→varManager/1.0:{read,pid_self}"]; + n_66 -> n_62 [id="[$e|84]", label="meManager/0.0→incrementer/0.0:answer"]; + n_35 -> n_70 [id="[$e|22]", label="incrementer/0.0→meManager/0.0:{release}"]; + n_15 -> n_22 [id="[$e|201]", label="incrementer/0.0→meManager/0.0:{release}"]; + n_86 -> n_9 [id="[$e|220]", label="incrementer/0.1→meManager/0.0:{release}"]; + n_51 -> n_19 [id="[$e|75]", label="meManager/0.0→incrementer/0.0:answer"]; + n_83 -> n_83 [id="[$e|197]", label="incrementer/0.3→varManager/1.0:{write,write}"]; + n_65 -> n_73 [id="[$e|102]", label="incrementer/0.1→varManager/1.0:{read,pid_self}"]; + n_21 -> n_48 [id="[$e|4]", label="main/0.0Δincrementer/0.2"]; + n_66 -> n_58 [id="[$e|87]", label="meManager/0.0→incrementer/0.1:answer"]; + n_16 -> n_81 [id="[$e|40]", label="incrementer/0.0→meManager/0.0:{request,pid_self}"]; + n_40 -> n_36 [id="[$e|115]", label="incrementer/0.1→varManager/1.0:{write,write}"]; + n_82 -> n_54 [id="[$e|64]", label="meManager/0.0→incrementer/0.1:answer"]; + n_59 -> n_1 [id="[$e|66]", label="meManager/0.0→incrementer/0.1:answer"]; + n_55 -> n_49 [id="[$e|57]", label="meManager/0.0→incrementer/0.3:answer"]; + n_55 -> n_51 [id="[$e|54]", label="incrementer/0.1→varManager/1.0:{write,write}"]; + n_11 -> n_2 [id="[$e|52]", label="meManager/0.0→incrementer/0.2:answer"]; + n_69 -> n_88 [id="[$e|1]", label="main/0.0ΔvarManager/1.0"]; + n_47 -> n_60 [id="[$e|133]", label="incrementer/0.3→varManager/1.0:{write,write}"]; + n_58 -> n_63 [id="[$e|89]", label="incrementer/0.1→varManager/1.0:{read,pid_self}"]; + n_66 -> n_16 [id="[$e|44]", label="incrementer/0.2→meManager/0.0:{release}"]; + n_81 -> n_62 [id="[$e|59]", label="meManager/0.0→incrementer/0.0:answer"]; + n_38 -> n_42 [id="[$e|127]", label="incrementer/0.2→varManager/1.0:{write,write}"]; + n_24 -> n_24 [id="[$e|217]", label="incrementer/0.3→varManager/1.0:{write,write}"]; + n_78 -> n_21 [id="[$e|3]", label="main/0.0Δincrementer/0.1"]; + n_40 -> n_61 [id="[$e|116]", label="varManager/1.0→incrementer/0.2:Val"]; + n_9 -> n_9 [id="[$e|208]", label="incrementer/0.3→varManager/1.0:{write,write}"]; + n_71 -> n_39 [id="[$e|100]", label="incrementer/0.3→varManager/1.0:{write,write}"]; + n_33 -> n_92 [id="[$e|17]", label="incrementer/0.3→varManager/1.0:{read,pid_self}"]; + n_77 -> n_77 [id="[$e|206]", label="incrementer/0.1→varManager/1.0:{write,write}"]; + n_59 -> n_80 [id="[$e|72]", label="meManager/0.0→incrementer/0.3:answer"]; + n_58 -> n_57 [id="[$e|88]", label="incrementer/0.2→varManager/1.0:{write,write}"]; + n_81 -> n_58 [id="[$e|60]", label="meManager/0.0→incrementer/0.1:answer"]; + n_32 -> n_16 [id="[$e|26]", label="incrementer/0.2→meManager/0.0:{release}"]; + n_57 -> n_63 [id="[$e|123]", label="incrementer/0.1→varManager/1.0:{read,pid_self}"]; + n_70 -> n_11 [id="[$e|31]", label="incrementer/0.2→meManager/0.0:{request,pid_self}"]; + n_13 -> n_22 [id="[$e|151]", label="incrementer/0.0→meManager/0.0:{release}"]; + n_17 -> n_44 [id="[$e|137]", label="varManager/1.0→incrementer/0.2:Val"]; + n_6 -> n_6 [id="[$e|215]", label="incrementer/0.3→varManager/1.0:{write,write}"]; + n_50 -> n_35 [id="[$e|18]", label="varManager/1.0→incrementer/0.0:Val"]; + n_8 -> n_82 [id="[$e|46]", label="incrementer/0.1→meManager/0.0:{request,pid_self}"]; + n_7 -> n_83 [id="[$e|175]", label="incrementer/0.0→meManager/0.0:{release}"]; + n_37 -> n_91 [id="[$e|109]", label="incrementer/0.0→varManager/1.0:{write,write}"]; + n_24 -> n_6 [id="[$e|216]", label="incrementer/0.3→meManager/0.0:{release}"]; + n_45 -> n_89 [id="[$e|111]", label="incrementer/0.0→varManager/1.0:{read,pid_self}"]; + n_82 -> n_71 [id="[$e|65]", label="meManager/0.0→incrementer/0.2:answer"]; + n_85 -> n_75 [id="[$e|8]", label="incrementer/0.2→meManager/0.0:{request,pid_self}"]; + n_86 -> n_86 [id="[$e|211]", label="incrementer/0.1→varManager/1.0:{write,write}"]; + n_42 -> n_38 [id="[$e|126]", label="incrementer/0.3→varManager/1.0:{read,pid_self}"]; + n_57 -> n_67 [id="[$e|166]", label="varManager/1.0→incrementer/0.1:Val"]; + n_73 -> n_72 [id="[$e|104]", label="varManager/1.0→incrementer/0.1:Val"]; + n_19 -> n_45 [id="[$e|76]", label="incrementer/0.1→varManager/1.0:{write,write}"]; + n_82 -> n_31 [id="[$e|63]", label="meManager/0.0→incrementer/0.0:answer"]; + n_11 -> n_1 [id="[$e|51]", label="meManager/0.0→incrementer/0.1:answer"]; + n_39 -> n_44 [id="[$e|182]", label="varManager/1.0→incrementer/0.2:Val"]; + n_85 -> n_75 [id="[$e|9]", label="incrementer/0.3→meManager/0.0:{request,pid_self}"]; + n_79 -> n_20 [id="[$e|144]", label="incrementer/0.0→varManager/1.0:{write,write}"]; + n_14 -> n_23 [id="[$e|158]", label="varManager/1.0→incrementer/0.3:Val"]; + n_73 -> n_65 [id="[$e|103]", label="incrementer/0.0→varManager/1.0:{write,write}"]; + n_16 -> n_81 [id="[$e|41]", label="incrementer/0.1→meManager/0.0:{request,pid_self}"]; + n_3 -> n_8 [id="[$e|28]", label="incrementer/0.3→meManager/0.0:{release}"]; + n_66 -> n_84 [id="[$e|90]", label="meManager/0.0→incrementer/0.3:answer"]; + n_7 -> n_28 [id="[$e|176]", label="incrementer/0.3→varManager/1.0:{write,write}"]; + n_27 -> n_7 [id="[$e|131]", label="varManager/1.0→incrementer/0.0:Val"]; + n_75 -> n_34 [id="[$e|12]", label="meManager/0.0→incrementer/0.2:answer"]; + n_59 -> n_2 [id="[$e|69]", label="meManager/0.0→incrementer/0.2:answer"]; + n_80 -> n_37 [id="[$e|74]", label="incrementer/0.3→varManager/1.0:{read,pid_self}"]; + n_5 -> n_4 [id="[$e|120]", label="incrementer/0.0→varManager/1.0:{read,pid_self}"]; + n_53 -> n_86 [id="[$e|181]", label="incrementer/0.1→varManager/1.0:{write,write}"]; + n_75 -> n_33 [id="[$e|13]", label="meManager/0.0→incrementer/0.3:answer"]; + n_77 -> n_77 [id="[$e|205]", label="incrementer/0.2→varManager/1.0:{write,write}"]; + n_56 -> n_28 [id="[$e|148]", label="incrementer/0.0→varManager/1.0:{write,write}"]; + n_90 -> n_14 [id="[$e|118]", label="incrementer/0.1→varManager/1.0:{write,write}"]; + n_74 -> n_24 [id="[$e|173]", label="incrementer/0.3→varManager/1.0:{write,write}"]; + n_85 -> n_75 [id="[$e|6]", label="incrementer/0.0→meManager/0.0:{request,pid_self}"]; + n_28 -> n_28 [id="[$e|200]", label="incrementer/0.0→varManager/1.0:{write,write}"]; + n_56 -> n_83 [id="[$e|147]", label="incrementer/0.3→meManager/0.0:{release}"]; + n_67 -> n_30 [id="[$e|167]", label="incrementer/0.1→meManager/0.0:{release}"]; + n_24 -> n_24 [id="[$e|218]", label="incrementer/0.2→varManager/1.0:{write,write}"]; + n_11 -> n_80 [id="[$e|53]", label="meManager/0.0→incrementer/0.3:answer"]; + n_85 -> n_75 [id="[$e|7]", label="incrementer/0.1→meManager/0.0:{request,pid_self}"]; + n_68 -> n_50 [id="[$e|14]", label="incrementer/0.0→varManager/1.0:{read,pid_self}"]; + n_25 -> n_27 [id="[$e|129]", label="incrementer/0.0→varManager/1.0:{read,pid_self}"]; + n_82 -> n_26 [id="[$e|62]", label="incrementer/0.3→varManager/1.0:{write,write}"]; + n_76 -> n_79 [id="[$e|107]", label="varManager/1.0→incrementer/0.2:Val"]; + n_8 -> n_8 [id="[$e|48]", label="incrementer/0.3→varManager/1.0:{write,write}"]; + n_79 -> n_18 [id="[$e|143]", label="incrementer/0.2→meManager/0.0:{release}"]; + n_87 -> n_18 [id="[$e|163]", label="incrementer/0.0→meManager/0.0:{release}"]; + n_8 -> n_82 [id="[$e|47]", label="incrementer/0.2→meManager/0.0:{request,pid_self}"]; + n_16 -> n_16 [id="[$e|43]", label="incrementer/0.2→varManager/1.0:{write,write}"]; + n_54 -> n_47 [id="[$e|98]", label="incrementer/0.1→varManager/1.0:{read,pid_self}"]; + n_36 -> n_40 [id="[$e|114]", label="incrementer/0.2→varManager/1.0:{read,pid_self}"]; + n_25 -> n_7 [id="[$e|174]", label="varManager/1.0→incrementer/0.0:Val"]; + n_22 -> n_22 [id="[$e|186]", label="incrementer/0.0→varManager/1.0:{write,write}"]; + n_74 -> n_6 [id="[$e|171]", label="incrementer/0.3→meManager/0.0:{release}"]; + n_8 -> n_82 [id="[$e|45]", label="incrementer/0.0→meManager/0.0:{request,pid_self}"]; + n_29 -> n_32 [id="[$e|20]", label="varManager/1.0→incrementer/0.2:Val"]; + n_70 -> n_11 [id="[$e|30]", label="incrementer/0.1→meManager/0.0:{request,pid_self}"]; + n_92 -> n_3 [id="[$e|21]", label="varManager/1.0→incrementer/0.3:Val"]; + n_23 -> n_86 [id="[$e|161]", label="incrementer/0.3→varManager/1.0:{write,write}"]; + n_31 -> n_25 [id="[$e|94]", label="incrementer/0.3→varManager/1.0:{write,write}"]; + n_43 -> n_36 [id="[$e|79]", label="incrementer/0.1→varManager/1.0:{write,write}"]; + n_11 -> n_59 [id="[$e|50]", label="incrementer/0.0→varManager/1.0:{write,write}"]; + n_67 -> n_77 [id="[$e|168]", label="incrementer/0.2→varManager/1.0:{write,write}"]; + n_13 -> n_15 [id="[$e|153]", label="incrementer/0.0→varManager/1.0:{write,write}"]; + n_32 -> n_66 [id="[$e|27]", label="incrementer/0.2→varManager/1.0:{write,write}"]; + n_5 -> n_87 [id="[$e|162]", label="varManager/1.0→incrementer/0.0:Val"]; + n_90 -> n_23 [id="[$e|119]", label="varManager/1.0→incrementer/0.3:Val"]; + n_54 -> n_60 [id="[$e|97]", label="incrementer/0.3→varManager/1.0:{write,write}"]; + n_64 -> n_69 [id="[$e|0]", label="main/0.0ΔmeManager/0.0"]; + n_15 -> n_15 [id="[$e|190]", label="incrementer/0.0→varManager/1.0:{write,write}"]; + n_53 -> n_9 [id="[$e|179]", label="incrementer/0.1→meManager/0.0:{release}"]; + n_72 -> n_15 [id="[$e|141]", label="incrementer/0.1→varManager/1.0:{write,write}"]; + n_91 -> n_56 [id="[$e|146]", label="varManager/1.0→incrementer/0.3:Val"]; + n_37 -> n_56 [id="[$e|110]", label="varManager/1.0→incrementer/0.3:Val"]; + n_30 -> n_30 [id="[$e|203]", label="incrementer/0.2→varManager/1.0:{write,write}"]; + n_44 -> n_6 [id="[$e|183]", label="incrementer/0.2→meManager/0.0:{release}"]; + n_87 -> n_20 [id="[$e|165]", label="incrementer/0.0→varManager/1.0:{write,write}"]; + n_55 -> n_43 [id="[$e|56]", label="meManager/0.0→incrementer/0.2:answer"]; + n_62 -> n_4 [id="[$e|86]", label="incrementer/0.0→varManager/1.0:{read,pid_self}"]; + n_30 -> n_30 [id="[$e|202]", label="incrementer/0.1→varManager/1.0:{write,write}"]; + n_20 -> n_20 [id="[$e|195]", label="incrementer/0.0→varManager/1.0:{write,write}"]; + n_38 -> n_74 [id="[$e|128]", label="varManager/1.0→incrementer/0.3:Val"]; + n_46 -> n_41 [id="[$e|19]", label="varManager/1.0→incrementer/0.1:Val"]; + n_63 -> n_57 [id="[$e|124]", label="incrementer/0.2→varManager/1.0:{write,write}"]; + n_74 -> n_24 [id="[$e|172]", label="incrementer/0.2→varManager/1.0:{write,write}"]; + n_6 -> n_6 [id="[$e|214]", label="incrementer/0.2→varManager/1.0:{write,write}"]; + n_41 -> n_12 [id="[$e|24]", label="incrementer/0.1→meManager/0.0:{release}"]; + n_28 -> n_83 [id="[$e|219]", label="incrementer/0.0→meManager/0.0:{release}"]; + n_23 -> n_9 [id="[$e|159]", label="incrementer/0.3→meManager/0.0:{release}"]; + n_89 -> n_45 [id="[$e|112]", label="incrementer/0.1→varManager/1.0:{write,write}"]; + n_65 -> n_72 [id="[$e|138]", label="varManager/1.0→incrementer/0.1:Val"]; + n_28 -> n_28 [id="[$e|199]", label="incrementer/0.3→varManager/1.0:{write,write}"]; + n_83 -> n_83 [id="[$e|196]", label="incrementer/0.0→varManager/1.0:{write,write}"]; + n_34 -> n_29 [id="[$e|16]", label="incrementer/0.2→varManager/1.0:{read,pid_self}"]; + n_52 -> n_46 [id="[$e|15]", label="incrementer/0.1→varManager/1.0:{read,pid_self}"]; + n_49 -> n_90 [id="[$e|83]", label="incrementer/0.3→varManager/1.0:{read,pid_self}"]; + n_41 -> n_51 [id="[$e|25]", label="incrementer/0.1→varManager/1.0:{write,write}"]; + n_20 -> n_20 [id="[$e|194]", label="incrementer/0.2→varManager/1.0:{write,write}"]; + n_36 -> n_61 [id="[$e|154]", label="varManager/1.0→incrementer/0.2:Val"]; + n_72 -> n_15 [id="[$e|140]", label="incrementer/0.0→varManager/1.0:{write,write}"]; + n_61 -> n_30 [id="[$e|155]", label="incrementer/0.2→meManager/0.0:{release}"]; + n_22 -> n_22 [id="[$e|187]", label="incrementer/0.1→varManager/1.0:{write,write}"]; + n_81 -> n_66 [id="[$e|58]", label="incrementer/0.2→varManager/1.0:{write,write}"]; + n_70 -> n_11 [id="[$e|32]", label="incrementer/0.3→meManager/0.0:{request,pid_self}"]; + n_88 -> n_78 [id="[$e|2]", label="main/0.0Δincrementer/0.0"]; + n_10 -> n_79 [id="[$e|142]", label="varManager/1.0→incrementer/0.2:Val"]; + n_12 -> n_12 [id="[$e|38]", label="incrementer/0.1→varManager/1.0:{write,write}"]; + n_20 -> n_18 [id="[$e|193]", label="incrementer/0.2→meManager/0.0:{release}"]; + n_18 -> n_18 [id="[$e|191]", label="incrementer/0.0→varManager/1.0:{write,write}"]; + n_61 -> n_77 [id="[$e|157]", label="incrementer/0.2→varManager/1.0:{write,write}"]; + n_24 -> n_6 [id="[$e|221]", label="incrementer/0.2→meManager/0.0:{release}"]; + n_7 -> n_28 [id="[$e|177]", label="incrementer/0.0→varManager/1.0:{write,write}"]; + n_3 -> n_26 [id="[$e|29]", label="incrementer/0.3→varManager/1.0:{write,write}"]; + n_28 -> n_83 [id="[$e|198]", label="incrementer/0.3→meManager/0.0:{release}"]; + n_31 -> n_27 [id="[$e|95]", label="incrementer/0.0→varManager/1.0:{read,pid_self}"]; + n_43 -> n_40 [id="[$e|80]", label="incrementer/0.2→varManager/1.0:{read,pid_self}"]; + n_91 -> n_37 [id="[$e|108]", label="incrementer/0.3→varManager/1.0:{read,pid_self}"]; + n_1 -> n_73 [id="[$e|68]", label="incrementer/0.1→varManager/1.0:{read,pid_self}"]; + n_81 -> n_84 [id="[$e|61]", label="meManager/0.0→incrementer/0.3:answer"]; + n_44 -> n_24 [id="[$e|184]", label="incrementer/0.3→varManager/1.0:{write,write}"]; + n_16 -> n_81 [id="[$e|42]", label="incrementer/0.3→meManager/0.0:{request,pid_self}"]; + n_60 -> n_53 [id="[$e|178]", label="varManager/1.0→incrementer/0.1:Val"]; + n_4 -> n_87 [id="[$e|122]", label="varManager/1.0→incrementer/0.0:Val"]; + n_48 -> n_85 [id="[$e|5]", label="main/0.0Δincrementer/0.3"]; + n_79 -> n_20 [id="[$e|145]", label="incrementer/0.2→varManager/1.0:{write,write}"]; + n_9 -> n_9 [id="[$e|207]", label="incrementer/0.1→varManager/1.0:{write,write}"]; + n_2 -> n_10 [id="[$e|70]", label="incrementer/0.0→varManager/1.0:{write,write}"]; + n_39 -> n_17 [id="[$e|135]", label="incrementer/0.2→varManager/1.0:{read,pid_self}"]; + n_26 -> n_31 [id="[$e|93]", label="meManager/0.0→incrementer/0.0:answer"]; + n_4 -> n_5 [id="[$e|121]", label="incrementer/0.2→varManager/1.0:{write,write}"]; + n_60 -> n_47 [id="[$e|132]", label="incrementer/0.1→varManager/1.0:{read,pid_self}"]; + n_76 -> n_10 [id="[$e|106]", label="incrementer/0.0→varManager/1.0:{write,write}"]; + n_67 -> n_77 [id="[$e|169]", label="incrementer/0.1→varManager/1.0:{write,write}"]; + n_1 -> n_65 [id="[$e|67]", label="incrementer/0.0→varManager/1.0:{write,write}"]; + n_15 -> n_22 [id="[$e|188]", label="incrementer/0.1→meManager/0.0:{release}"]; + n_75 -> n_68 [id="[$e|10]", label="meManager/0.0→incrementer/0.0:answer"]; + n_12 -> n_55 [id="[$e|37]", label="incrementer/0.3→meManager/0.0:{request,pid_self}"]; + n_87 -> n_20 [id="[$e|164]", label="incrementer/0.2→varManager/1.0:{write,write}"]; + n_86 -> n_9 [id="[$e|209]", label="incrementer/0.3→meManager/0.0:{release}"]; + n_44 -> n_24 [id="[$e|185]", label="incrementer/0.2→varManager/1.0:{write,write}"]; + n_26 -> n_71 [id="[$e|99]", label="meManager/0.0→incrementer/0.2:answer"]; + n_63 -> n_67 [id="[$e|125]", label="varManager/1.0→incrementer/0.1:Val"]; + n_12 -> n_55 [id="[$e|36]", label="incrementer/0.2→meManager/0.0:{request,pid_self}"]; + n_20 -> n_18 [id="[$e|212]", label="incrementer/0.0→meManager/0.0:{release}"]; + n_84 -> n_42 [id="[$e|91]", label="incrementer/0.2→varManager/1.0:{write,write}"]; + n_80 -> n_91 [id="[$e|73]", label="incrementer/0.0→varManager/1.0:{write,write}"]; + n_49 -> n_14 [id="[$e|82]", label="incrementer/0.1→varManager/1.0:{write,write}"]; + n_35 -> n_59 [id="[$e|23]", label="incrementer/0.0→varManager/1.0:{write,write}"]; + n_18 -> n_18 [id="[$e|192]", label="incrementer/0.2→varManager/1.0:{write,write}"]; + n_23 -> n_86 [id="[$e|160]", label="incrementer/0.1→varManager/1.0:{write,write}"]; + n_26 -> n_8 [id="[$e|49]", label="incrementer/0.3→meManager/0.0:{release}"]; + n_77 -> n_30 [id="[$e|213]", label="incrementer/0.1→meManager/0.0:{release}"]; + n_61 -> n_77 [id="[$e|156]", label="incrementer/0.1→varManager/1.0:{write,write}"]; + n_59 -> n_70 [id="[$e|34]", label="incrementer/0.0→meManager/0.0:{release}"]; + n_10 -> n_76 [id="[$e|105]", label="incrementer/0.2→varManager/1.0:{read,pid_self}"]; + n_71 -> n_17 [id="[$e|101]", label="incrementer/0.2→varManager/1.0:{read,pid_self}"]; + n_14 -> n_90 [id="[$e|117]", label="incrementer/0.3→varManager/1.0:{read,pid_self}"]; + n_56 -> n_28 [id="[$e|149]", label="incrementer/0.3→varManager/1.0:{write,write}"]; + n_15 -> n_15 [id="[$e|189]", label="incrementer/0.1→varManager/1.0:{write,write}"]; + n_13 -> n_15 [id="[$e|152]", label="incrementer/0.1→varManager/1.0:{write,write}"]; + n_51 -> n_49 [id="[$e|81]", label="meManager/0.0→incrementer/0.3:answer"]; + n_26 -> n_54 [id="[$e|96]", label="meManager/0.0→incrementer/0.1:answer"]; + n_17 -> n_39 [id="[$e|136]", label="incrementer/0.3→varManager/1.0:{write,write}"]; + n_12 -> n_55 [id="[$e|35]", label="incrementer/0.0→meManager/0.0:{request,pid_self}"]; + n_27 -> n_25 [id="[$e|130]", label="incrementer/0.3→varManager/1.0:{write,write}"]; + n_47 -> n_53 [id="[$e|134]", label="varManager/1.0→incrementer/0.1:Val"]; + n_2 -> n_76 [id="[$e|71]", label="incrementer/0.2→varManager/1.0:{read,pid_self}"]; + n_72 -> n_22 [id="[$e|139]", label="incrementer/0.1→meManager/0.0:{release}"]; + n_86 -> n_86 [id="[$e|210]", label="incrementer/0.3→varManager/1.0:{write,write}"]; + n_45 -> n_13 [id="[$e|150]", label="varManager/1.0→incrementer/0.0:Val"]; + n_70 -> n_70 [id="[$e|33]", label="incrementer/0.0→varManager/1.0:{write,write}"]; + n_77 -> n_30 [id="[$e|204]", label="incrementer/0.2→meManager/0.0:{release}"]; + n_51 -> n_43 [id="[$e|78]", label="meManager/0.0→incrementer/0.2:answer"]; } diff --git a/examples/violation/main_0_local_view.dot b/examples/violation/main_0_local_view.dot index 22110c4..071121e 100644 --- a/examples/violation/main_0_local_view.dot +++ b/examples/violation/main_0_local_view.dot @@ -1,15 +1,19 @@ 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_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_2 -> n_3 [id="[$e|1]", label="spawn meManager/0.0"]; - 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_5 -> n_4 [id="[$e|0]", label="spawn incrementer/0.1"]; + n_4 -> n_6 [id="[$e|4]", label="spawn varManager/1.0"]; + n_3 -> n_4 [id="[$e|1]", label="spawn meManager/0.0"]; + n_5 -> n_1 [id="[$e|3]", label="spawn incrementer/0.3"]; + n_7 -> n_2 [id="[$e|0]", label="spawn incrementer/0.1"]; + n_2 -> n_5 [id="[$e|2]", label="spawn incrementer/0.2"]; + n_6 -> n_7 [id="[$e|5]", label="spawn incrementer/0.0"]; } diff --git a/examples/violation/meManager_0_local_view.dot b/examples/violation/meManager_0_local_view.dot index 843cf23..6f96ef3 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_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}"]; - n_3 -> n_1 [id="[$e|4]", label="receive {release}"]; } diff --git a/examples/violation/varManager_1_local_view.dot b/examples/violation/varManager_1_local_view.dot index 213d5f4..d89cbb7 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_2 [id="[$e|0]", label="receive {read,Pid}"]; 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/src/choreography/actor_emul.erl b/src/choreography/actor_emul.erl index 1bbc18e..4148e42 100644 --- a/src/choreography/actor_emul.erl +++ b/src/choreography/actor_emul.erl @@ -78,7 +78,10 @@ proc_loop(Data) -> LV = share:get_localview(ProcName), G = LV#localview.min_graph, % timer:sleep(200), + VCurr = Data#actor_info.current_state, + %% TODO: considera togliere filtro e smettere di esplorare con altri (vedi TODO) + _FirstMarkedE = Data#actor_info.first_marked_edges, SecondMarkedE = Data#actor_info.second_marked_edges, MessageQueue = Data#actor_info.message_queue, SpawnVars = Data#actor_info.spawn_vars, @@ -89,6 +92,14 @@ proc_loop(Data) -> {P, get_edges} -> EL = digraph:out_edges(G, VCurr), %% APPROX: filter out edges used two times + % TODO: cambiare questo ovunque nella gv + % case EL of + % [] -> + % P ! {final_state, []}; + % _ -> + % ERet = filter_marked_edges(EL, SecondMarkedE), + % P ! {filtered, ERet} + % end, ERet = filter_marked_edges(EL, SecondMarkedE), P ! {ERet}, proc_loop(Data); diff --git a/src/choreography/eval.erl b/src/choreography/eval.erl index 02e63ba..59920ff 100644 --- a/src/choreography/eval.erl +++ b/src/choreography/eval.erl @@ -36,10 +36,10 @@ function_list(ContList, Data) -> lists:foldl( fun(FunctionBody, AccData) -> case FunctionBody of - {clause, _, Vars, Guard, Content} -> + {clause, _, Pattern, Guard, Content} -> % io:fwrite("Clause ~p~n", [Vars]), - ets:insert(?ARGUMENTS, {Data#localview.fun_name, Vars}), - clause(Content, Vars, Guard, AccData#localview{last_vertex = 1}, "arg"); + ets:insert(?ARGUMENTS, {Data#localview.fun_name, Pattern}), + clause(Content, Pattern, Guard, AccData#localview{last_vertex = 1}, "arg"); C -> share:warning("should be a clause but it's", C, ?UNDEFINED) end @@ -50,10 +50,10 @@ function_list(ContList, Data) -> %%% @doc %%% Evaluate a single clause (might be from `case', `receive' or `if'). -clause(Code, Vars, Guards, Data, BaseLabel) -> - % io:fwrite("[CLAUSE] Code ~p~n Vars ~p~n Guards ~p~n", [Code, Vars, Guards]), +clause(Code, Pattern, Guards, Data, BaseLabel) -> + % io:fwrite("[CLAUSE] Code ~p~n Vars ~p~n Guards ~p~n", [Code, Pattern, Guards]), LocalV = Data#localview.local_vars, - TempData = lv:eval_codeline(Vars, Data), + TempData = lv:eval_codeline(Pattern, Data), % should always be a list EvalVarList = TempData#localview.ret_var, TempLabel = BaseLabel ++ " " ++ var_to_string(EvalVarList) ++ guards_to_string(Guards), @@ -260,7 +260,7 @@ call_by_atom(Name, ArgList, Data) -> _ -> generic_call(Name, ArgList, Data) end. -%%% TODO: What to do with argument lists? Put them in the #localview.edge_map? +%%% TODO: What to do with argument lists? Put them in the #localview.additional_info? recursive(_ArgList, Data) -> % io:fwrite("[RECURSIVE] from vertex ~p~n", [Data#localview.last_vertex]), digraph:add_edge(Data#localview.graph, Data#localview.last_vertex, 1, 'ɛ'), @@ -290,9 +290,9 @@ spawn_three(Name, ArgList, Data) -> NewData = lv:eval_codeline(ArgList, Data), NewDataRetVar = NewData#localview.ret_var, {Label, ProcId} = format_spawn_label(Name, NewDataRetVar), - EM = maps:put(Label, NewDataRetVar, NewData#localview.edge_map), + EM = maps:put(Label, NewDataRetVar, NewData#localview.additional_info), % io:fwrite("label ~p new edge map ~p map ~p~n", [Label, NewData#localview.fun_name, EM]), - ND = NewData#localview{edge_map = EM}, + ND = NewData#localview{additional_info = EM}, RetData = add_vertex_edge(Label, ND), RetData#localview{ret_var = #variable{type = pid, value = ProcId}}. @@ -341,14 +341,14 @@ generic_call(Name, ArgList, Data) -> LastV = Data#localview.last_vertex, NewG = NewD#localview.graph, NewRet = NewD#localview.ret_var, - EM = NewD#localview.edge_map, + EM = NewD#localview.additional_info, NewLastV = merge_graph(G, NewG, LastV), % io:fwrite("LastV ~p VarRet ~p~n", [LastV, NewRet]), - % io:fwrite("OldEM ~p NewEM ~p~n", [Data#localview.edge_map, EM]), + % io:fwrite("OldEM ~p NewEM ~p~n", [Data#localview.additional_info, EM]), Data#localview{ ret_var = NewRet, last_vertex = NewLastV, - edge_map = maps:merge(Data#localview.edge_map, EM) + additional_info = maps:merge(Data#localview.additional_info, EM) } end. @@ -395,9 +395,9 @@ send(Destination, MessageContent, Data) -> VarDataSent = NewData#localview.ret_var, DataSent = var_to_string(VarDataSent), SLabel = "send " ++ share:atol(DataSent) ++ " to " ++ share:atol(ProcName), - EM = NewData#localview.edge_map, + EM = NewData#localview.additional_info, add_vertex_edge(SLabel, NewData#localview{ - edge_map = maps:put(SLabel, {VarProcName, VarDataSent}, EM) + additional_info = maps:put(SLabel, {VarProcName, VarDataSent}, EM) }). get_pid(Var) -> diff --git a/src/choreography/gv.erl b/src/choreography/gv.erl index 4701d67..2eb7ab2 100644 --- a/src/choreography/gv.erl +++ b/src/choreography/gv.erl @@ -46,8 +46,12 @@ create_globalview(Name) -> MainProcPid = spawn(actor_emul, proc_loop, [#actor_info{fun_name = Name, id = N}]), PidKey = share:atol(Name) ++ ?NSEQSEP ++ integer_to_list(N), ProcPidMap = #{share:ltoa(PidKey) => MainProcPid}, + S = sets:new(), + ets:insert(?DBMANAGER, {state_m, #{1 => sets:add_element({share:ltoa(PidKey), 1}, S)}}), % initialize first branch - progress(RetG, [new_branch(RetG, VNew, ProcPidMap)]). + BData = progress(RetG, [new_branch(RetG, VNew, ProcPidMap)]), + show_global_state(), + BData. new_branch(G, V, P) -> #branch{ @@ -61,6 +65,14 @@ new_message(F, D, E) -> from = F, data = D, edge = E }. +show_global_state() -> + [{_, StateM}] = ets:lookup(?DBMANAGER, state_m), + maps:fold( + fun(Key, Value, _F) -> io:fwrite("N ~p states ~p~n", [Key, sets:to_list(Value)]) end, + [], + StateM + ). + %%% Explore every possible branch of executions progress(GlobalViewGraph, []) -> GlobalViewGraph; @@ -124,7 +136,7 @@ gen_branch_foreach_mess(BranchData, MessageQueue, ProcName, BaseBranchList) -> ?UNDEFINED -> stop_processes(NewMap), AccList; - %%% If an edge has been found, duplicate the branch and add the transition to the graph + %%% If an edge has been found, use the duplicated branch to add the transition to the gv EdgeFound -> % io:fwrite("[RECV] Mess ~p Edge choose ~p~n", [Message, EdgeFound]), ProcFrom = Message#message.from, @@ -132,15 +144,30 @@ gen_branch_foreach_mess(BranchData, MessageQueue, ProcName, BaseBranchList) -> PidFrom = maps:get(ProcFrom, NewMap), Label = format_send_label(ProcFrom, ProcName, MessData), % io:fwrite("~n~n[RECV] LABEL ~ts~n~n", [Label]), - EFromInfo = actor_emul:get_proc_edge_info(PidFrom, Message#message.edge), + % EFromInfo = actor_emul:get_proc_edge_info(PidFrom, Message#message.edge), + % {EEE, _, _, _} = EFromInfo, + ProcFromData = actor_emul:get_proc_data(PidFrom), + CurrProcFromVertex = ProcFromData#actor_info.current_state, EToInfo = actor_emul:get_proc_edge_info(NewPid, EdgeFound), - {LastVertex, NewStateMap} = complex_add_vertex( - ProcFrom, EFromInfo, ProcName, EToInfo, DupData, Label + % {LastVertex, NewStateMap} = complex_add_vertex( + % ProcFrom, EFromInfo, ProcName, EToInfo, DupData, Label + % ), + {LastVertex, NewStateMap, Added} = complex_add_vertex_recv( + ProcFrom, CurrProcFromVertex, ProcName, EToInfo, DupData, Label ), actor_emul:del_proc_mess_queue(NewPid, Message), %%% 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, states_m = NewStateMap}] + %%% TODO: Spostare la send qua + % NewPid2 = maps:get(ProcFrom, NewMap), + % actor_emul:use_proc_transition(NewPid2, EEE), + case Added of + true -> + AccList ++ + [DupData#branch{last_vertex = LastVertex, states_m = NewStateMap}]; + false -> + AccList + end end end, BaseBranchList, @@ -274,7 +301,8 @@ eval_edge(EdgeInfo, ProcName, ProcPid, BData) -> actor_emul:use_proc_transition(ProcPid, Edge), {BData, true}; IsSpawn -> - {VNew, NewM} = add_spawn_to_global(SLabel, ProcName, BData), + EdgeInfo = actor_emul:get_proc_edge_info(ProcPid, Edge), + {VNew, NewM} = add_spawn_to_global(EdgeInfo, SLabel, ProcName, BData), NewBData = BData#branch{last_vertex = VNew, proc_pid_m = NewM}, actor_emul:use_proc_transition(ProcPid, Edge), {NewBData, true}; @@ -289,7 +317,8 @@ is_substring(S, SubS) -> is_list(string:find(S, SubS)). %%% Add a spawn transition to the global view -add_spawn_to_global(SLabel, EmulProcName, Data) -> +add_spawn_to_global(EInfo, SLabel, EmulProcName, Data) -> + {_, _, PV, _} = EInfo, % get proc name FunSpawned = string:prefix(SLabel, "spawn "), {FunSName, Counter} = remove_id_from_proc(FunSpawned), @@ -301,6 +330,10 @@ add_spawn_to_global(SLabel, EmulProcName, Data) -> lists:foreach(fun(Var) -> actor_emul:add_proc_spawnvars(FuncPid, Var) end, LocalList), % create the edge on the global graph VNew = share:add_vertex(Data#branch.graph), + [{_, StateM}] = ets:lookup(?DBMANAGER, state_m), + AggrGState = create_gv_state(NewMap, share:ltoa(FunSpawned), 1, EmulProcName, PV), + % io:fwrite("SPAWN AGGR ~p~n", [AggrGState]), + ets:insert(?DBMANAGER, {state_m, maps:put(VNew, AggrGState, StateM)}), NewLabel = share:atol(EmulProcName) ++ "Δ" ++ FunSpawned, digraph:add_edge(Data#branch.graph, Data#branch.last_vertex, VNew, NewLabel), {VNew, NewMap}. @@ -513,60 +546,106 @@ and_rec([{B, L} | T]) -> end. %%% Add a vertex to the global view, with some checks for recusive edges -complex_add_vertex(Proc1, EdgeInfo1, Proc2, EdgeInfo2, Data, Label) -> - StateM = Data#branch.states_m, + +%%% Check if a equal global state exist, otherwise add a new one. +%%% TODO: consider message queue also +complex_add_vertex_recv(Proc1, CurrVertex, Proc2, EdgeInfo2, Data, Label) -> + ProcPid = Data#branch.proc_pid_m, + [{_, StateM}] = ets:lookup(?DBMANAGER, state_m), + % io:fwrite("stateM ~p~n", [StateM]), + % io:fwrite("Label ~p~n", [share:ltoa(Label)]), VLast = Data#branch.last_vertex, G = Data#branch.graph, - {_, V1, V2, _} = EdgeInfo1, - {_, PV1, PV2, _} = EdgeInfo2, + {_, _PV1, PV2, _} = EdgeInfo2, EL = digraph:out_edges(G, VLast), - %%% Check if these vertex correspond to a global view's vertex - Vfirst = maps:get({{Proc1, V2}, {Proc2, PV2}}, StateM, ?UNDEFINED), - %%% Recheck vertexs, but in another order - Vsecond = maps:get({{Proc2, PV2}, {Proc1, V2}}, StateM, ?UNDEFINED), - %%% Check if already exist the same transition - case check_same_label(G, EL, Label) of - nomatch -> - case Vfirst of - ?UNDEFINED -> - case Vsecond of - ?UNDEFINED -> - Cond = (V1 =:= V2) and (PV1 =:= PV2), - case Cond of - true -> - digraph:add_edge(G, VLast, VLast, Label), - NewM = maps:put({{Proc1, V1}, {Proc2, PV1}}, VLast, StateM), - {VLast, NewM}; - %%% Add a new vertex, because no match found in StateM - false -> - VAdded = share:add_vertex(G), - digraph:add_edge(G, VLast, VAdded, Label), - NewM = maps:put({{Proc1, V1}, {Proc2, PV1}}, VLast, StateM), - {VAdded, NewM} - end; - _ -> - %%% Match second vertex - digraph:add_edge(G, VLast, Vsecond, Label), - NewM = maps:put({{Proc1, V1}, {Proc2, PV1}}, VLast, StateM), - {Vsecond, NewM} + SameL = check_same_label(G, EL, VLast, Label), + % io:fwrite("~n~n[COMPLEX] new check~n", []), + AggregateGlobalState = create_gv_state(ProcPid, Proc1, CurrVertex, Proc2, PV2), + {RETV, RetStateM, _Added} = + case check_if_exist(StateM, AggregateGlobalState) of + nomatch -> + VNew = share:add_vertex(G), + digraph:add_edge(G, VLast, VNew, Label), + % io:fwrite("[DEBUG] Adding new global state ~p~n", [VNew]), + NewM = maps:put(VNew, AggregateGlobalState, StateM), + {VNew, NewM, true}; + VFound -> + % io:fwrite("[EXTERNFOUND] ~p~n", [VFound]), + case SameL of + nomatch -> + digraph:add_edge(G, VLast, VFound, Label), + {VFound, StateM, false}; + VTo -> + {VTo, StateM, false} + end + end, + ets:insert(?DBMANAGER, {state_m, RetStateM}), + {RETV, RetStateM, true}. + +create_gv_state(ProcPid, Proc1, V2, Proc2, PV2) -> + maps:fold( + fun(Name, Pid, AccList) -> + RealName = share:remove_counter(Name), + LV = share:get_localview(RealName), + MG = LV#localview.min_graph, + EL = + case Name of + Proc1 -> + {_, L} = digraph:vertex(MG, V2), + {Proc1, share:if_final_get_n(L)}; + Proc2 -> + {_, L} = digraph:vertex(MG, PV2), + {Proc2, share:if_final_get_n(L)}; + N -> + Data = actor_emul:get_proc_data(Pid), + {_, L} = digraph:vertex(MG, Data#actor_info.current_state), + {N, share:if_final_get_n(L)} + end, + sets:add_element(EL, AccList) + end, + sets:new(), + ProcPid + ). + +check_if_exist(StateM, AggregateGlobalState) -> + maps:fold( + fun(Key, Value, Acc) -> + if + Acc =:= nomatch -> + Sub1 = sets:subtract(Value, AggregateGlobalState), + % io:fwrite("[CHECK] Key ~p~nV ~p~nA ~p~nS ~p~n~n", [ + % Key, Value, AggregateGlobalState, Sub + % ]), + Sub2 = sets:subtract(AggregateGlobalState, Value), + % io:fwrite("[CHECK] Key ~p~nV ~p~nA ~p~nS ~p~n~n", [ + % Key, Value, AggregateGlobalState, Sub + % ]), + Cond = sets:is_empty(Sub1) and sets:is_empty(Sub2), + % io:fwrite("[SUB] ~p~n", [Cond]), + case Cond of + true -> + % io:fwrite("[FOUND] FOUND n ~p ~n", [Key]), + Key; + false -> + Acc end; - _ -> - %%% Match First vertex - digraph:add_edge(G, VLast, Vfirst, Label), - {Vfirst, StateM} - end; - VRet -> - {VRet, StateM} - end. + true -> + Acc + end + end, + nomatch, + StateM + ). %%% Returns the outgoing vertex given a label and a list of transition -check_same_label(G, EL, Label) -> +check_same_label(G, EL, VLast, Label) -> lists:foldl( fun(E, A) -> - {E, _, VTo, VLabel} = digraph:edge(G, E), - case VLabel =:= Label of - true -> VTo; - false -> A + {E, VFrom, VTo, VLabel} = digraph:edge(G, E), + case (VLast =:= VFrom) and (VLabel =:= Label) of + true when A =:= nomatch -> VTo; + false -> A; + _ -> A end end, nomatch, diff --git a/src/share/common_data.hrl b/src/share/common_data.hrl index c8c91d0..2b42439 100644 --- a/src/share/common_data.hrl +++ b/src/share/common_data.hrl @@ -22,6 +22,12 @@ %%% RECORDS +% -record(setting, { +% more_info_lv = true, +% debug = true, +% output_dir = "./", +% save_all = true +% }). -record(setting, { more_info_lv = false, debug = false, @@ -36,7 +42,7 @@ -record(variable, { type = ?ANYDATA, - name = ?UNDEFINED, + name = unknown, value = ?ANYDATA }). @@ -48,7 +54,12 @@ last_vertex = 1, local_vars = [], ret_var = #variable{}, - edge_map = #{}, + % additioal info about the edges + % key: label, value: depends on the edge + % if key is a spawn label, value is spawn arguments + % if key is a send label, value is the data sent + % if key is a receive label, value is nothing + additional_info = #{}, settings = #setting{} }). @@ -60,11 +71,17 @@ }). -record(actor_info, { + % name of the spawned function fun_name = "", + % sequential number of the actor id = ?UNDEFINED, + % local state of lv current_state = 1, + % first filter first_marked_edges = [], + % second filter second_marked_edges = [], + % actor's spawing variable TODO: CHANGE spawn_vars = sets:new(), local_vars = sets:new(), message_queue = [] diff --git a/src/share/share.erl b/src/share/share.erl index ebf9a51..e1b43b2 100644 --- a/src/share/share.erl +++ b/src/share/share.erl @@ -28,6 +28,7 @@ find_var/2, if_final_get_n/1, inc_spawn_counter/1, + remove_counter/1, atol/1, ltoa/1 ]). @@ -115,13 +116,13 @@ get_edgedata(FunName) -> io:fwrite("[S] Not Found in edgedata ~p~n", [FunName]), not_found; [{_, A}] -> - A#localview.edge_map + A#localview.additional_info end. warning(String, Content, RetData) -> [{_, Line}] = ets:lookup(?CLINE, line), io:fwrite("[LV] WARNING on line ~p: " ++ String ++ " ~p~n", [Line, Content]), - RetData. + RetData#localview{ret_var = #variable{}}. error(String, Content, RetData) -> io:fwrite("ERROR: ~p ~p~n", [String, Content]), @@ -158,6 +159,11 @@ should_minimize(S) -> save_graph(Data, Settings, FunName, Mode) -> OutputDir = Settings#setting.output_dir, + % Minimize = + % case Mode of + % global -> false; + % _ -> true + % end, Minimize = should_minimize(atol(FunName) ++ " " ++ atol(Mode)), ToSaveG = case Minimize of @@ -166,6 +172,10 @@ save_graph(Data, Settings, FunName, Mode) -> end, save_graph_to_file(ToSaveG, OutputDir, FunName, Mode). +remove_counter(S) -> + [Rest, _] = string:split(atol(S), "."), + Rest. + %%% @doc %%% Remove the last element from a list. remove_last(Item) ->