Merge branch 'master' of https://github.com/gabrielegenovese/chorer

examples/airline/agent_1_local_view.dot

@@ -5,6 +5,6 @@ digraph agent_1 {
 	n_0 -> n_1 [arrowhead=none];
 	n_2 [id="2", shape=circle, label="2"];
 
-	n_2 -> n_1 [id="[$e|3]", label="receive {booked,_}"];
 	n_1 -> n_2 [id="[$e|0]", label="send {sell,pid_self} to Pid2"];
+	n_2 -> n_1 [id="[$e|3]", label="receive {booked,_}"];
 }

examples/airline/main_0_global_view.dot

@@ -2,23 +2,20 @@ digraph global {
 	rankdir="LR";
 	n_0 [label="global", shape="plaintext"];
 	n_1 [id="5", shape=circle, label="5"];
-	n_2 [id="6", shape=circle, label="6"];
-	n_3 [id="1", shape=circle, label="1"];
-	n_0 -> n_3 [arrowhead=none];
-	n_4 [id="2", shape=circle, label="2"];
-	n_5 [id="4", shape=circle, label="4"];
-	n_6 [id="3", shape=circle, label="3"];
+	n_2 [id="1", shape=circle, label="1"];
+	n_0 -> n_2 [arrowhead=none];
+	n_3 [id="2", shape=circle, label="2"];
+	n_4 [id="4", shape=circle, label="4"];
+	n_5 [id="3", shape=circle, label="3"];
 
-	n_2 -> n_5 [id="[$e|11]", label="agent/1.1→main/0.0:{sell,pid_self}"];
-	n_2 -> n_5 [id="[$e|10]", label="agent/1.0→main/0.0:{sell,pid_self}"];
-	n_5 -> n_2 [id="[$e|7]", label="main/0.0→agent/1.1:{booked,Num}"];
-	n_6 -> n_5 [id="[$e|2]", label="agent/1.0→main/0.0:{sell,pid_self}"];
-	n_6 -> n_5 [id="[$e|3]", label="agent/1.1→main/0.0:{sell,pid_self}"];
-	n_5 -> n_1 [id="[$e|5]", label="main/0.0→agent/1.0:{booked,Num}"];
-	n_5 -> n_5 [id="[$e|6]", label="agent/1.0→main/0.0:{sell,pid_self}"];
-	n_4 -> n_6 [id="[$e|1]", label="main/0.0Δagent/1.1"];
-	n_1 -> n_5 [id="[$e|9]", label="agent/1.0→main/0.0:{sell,pid_self}"];
-	n_3 -> n_4 [id="[$e|0]", label="main/0.0Δagent/1.0"];
-	n_5 -> n_5 [id="[$e|4]", label="agent/1.1→main/0.0:{sell,pid_self}"];
-	n_1 -> n_5 [id="[$e|8]", label="agent/1.1→main/0.0:{sell,pid_self}"];
+	n_1 -> n_4 [id="[$e|8]", label="agent/1.1→main/0.0:{sell,pid_self}"];
+	n_4 -> n_5 [id="[$e|6]", label="main/0.0→agent/1.1:{booked,Num}"];
+	n_4 -> n_4 [id="[$e|5]", label="agent/1.1→main/0.0:{sell,pid_self}"];
+	n_4 -> n_1 [id="[$e|4]", label="main/0.0→agent/1.0:{booked,Num}"];
+	n_4 -> n_4 [id="[$e|7]", label="agent/1.0→main/0.0:{sell,pid_self}"];
+	n_3 -> n_5 [id="[$e|1]", label="main/0.0Δagent/1.1"];
+	n_1 -> n_4 [id="[$e|9]", label="agent/1.0→main/0.0:{sell,pid_self}"];
+	n_2 -> n_3 [id="[$e|0]", label="main/0.0Δagent/1.0"];
+	n_5 -> n_4 [id="[$e|3]", label="agent/1.1→main/0.0:{sell,pid_self}"];
+	n_5 -> n_4 [id="[$e|2]", label="agent/1.0→main/0.0:{sell,pid_self}"];
 }

examples/airline/main_0_local_view.dot

@@ -7,8 +7,8 @@ digraph main_0 {
 	n_3 [id="2", shape=doublecircle, label="3"];
 	n_4 [id="3", shape=circle, label="2"];
 
-	n_4 -> n_3 [id="[$e|2]", label="spawn agent/1.1"];
 	n_1 -> n_3 [id="[$e|5]", label="send {booked,Num} to Pid1"];
 	n_2 -> n_4 [id="[$e|1]", label="spawn agent/1.0"];
 	n_3 -> n_1 [id="[$e|0]", label="receive {sell,Pid1}"];
+	n_4 -> n_3 [id="[$e|2]", label="spawn agent/1.1"];
 }

examples/async/main_0_global_view.dot

@@ -9,10 +9,10 @@ digraph global {
 	n_5 [id="4", shape=circle, label="4"];
 	n_6 [id="3", shape=circle, label="3"];
 
-	n_6 -> n_5 [id="[$e|2]", label="dummy2/0.0→dummy1/0.0:ciao"];
-	n_6 -> n_1 [id="[$e|3]", label="dummy1/0.0→dummy2/0.0:bello"];
 	n_1 -> n_2 [id="[$e|5]", label="dummy2/0.0→dummy1/0.0:ciao"];
+	n_5 -> n_2 [id="[$e|4]", label="dummy1/0.0→dummy2/0.0:bello"];
 	n_4 -> n_6 [id="[$e|1]", label="main/0.0Δdummy2/0.0"];
 	n_3 -> n_4 [id="[$e|0]", label="main/0.0Δdummy1/0.0"];
-	n_5 -> n_2 [id="[$e|4]", label="dummy1/0.0→dummy2/0.0:bello"];
+	n_6 -> n_1 [id="[$e|3]", label="dummy1/0.0→dummy2/0.0:bello"];
+	n_6 -> n_5 [id="[$e|2]", label="dummy2/0.0→dummy1/0.0:ciao"];
 }

examples/cauder_suite/airline/README.md

@@ -0,0 +1,7 @@
+# Airline example
+
+## Usage
+
+```bash
+./_build/default/bin/chorer ./examples/cauder_suite/airline/airline.erl main/0 ./examples/cauder_suite/airline
+```

examples/cauder_suite/airline/agent_2_local_view.dot

@@ -0,0 +1,18 @@
+digraph agent_2 {
+	rankdir="LR";
+	n_0 [label="agent_2", shape="plaintext"];
+	n_1 [id="5", shape=doublecircle, label="6"];
+	n_2 [id="6", shape=circle, label="3"];
+	n_3 [id="1", shape=circle, label="1"];
+	n_0 -> n_3 [arrowhead=none];
+	n_4 [id="2", shape=circle, label="2"];
+	n_5 [id="4", shape=circle, label="4"];
+	n_6 [id="3", shape=circle, label="5"];
+
+	n_4 -> n_5 [id="[$e|3]", label="receive {seats,0}"];
+	n_4 -> n_2 [id="[$e|1]", label="receive {seats,Num}"];
+	n_3 -> n_4 [id="[$e|6]", label="send {numOfSeats,pid_self} to Pid"];
+	n_6 -> n_3 [id="[$e|7]", label="receive {booked,_}"];
+	n_5 -> n_1 [id="[$e|2]", label="send stop to Pid"];
+	n_2 -> n_6 [id="[$e|5]", label="send {sell,pid_self} to Pid"];
+}

examples/cauder_suite/airline/airline.erl

@@ -0,0 +1,32 @@
+-module(airline).
+-export([main/0, agent/2]).
+
+main() ->
+    Main = self(),
+    spawn(?MODULE, agent, [1, Main]),
+    seats(3).
+
+seats(Num) ->
+    receive
+        {numOfSeats, Pid} ->
+            Pid ! {seats, Num},
+            seats(Num);
+        {sell, Pid} ->
+            io:format("Seat sold!~n"),
+            Pid ! {booked, Num},
+            seats(Num - 1);
+        stop ->
+            done
+    end.
+
+agent(NAg, Pid) ->
+    Pid ! {numOfSeats, self()},
+    receive
+        {seats, Num} when Num > 0 ->
+            Pid ! {sell, self()},
+            receive
+                {booked, _} -> agent(NAg, Pid)
+            end;
+        {seats, 0} ->
+            Pid ! stop
+    end.

examples/cauder_suite/airline/main_0_global_view.dot

@@ -0,0 +1,16 @@
+digraph global {
+	rankdir="LR";
+	n_0 [label="global", shape="plaintext"];
+	n_1 [id="5", shape=circle, label="5"];
+	n_2 [id="1", shape=circle, label="1"];
+	n_0 -> n_2 [arrowhead=none];
+	n_3 [id="2", shape=circle, label="2"];
+	n_4 [id="4", shape=circle, label="4"];
+	n_5 [id="3", shape=circle, label="3"];
+
+	n_4 -> n_1 [id="[$e|3]", label="agent/2.0→main/0.0:{sell,pid_self}"];
+	n_3 -> n_5 [id="[$e|1]", label="agent/2.0→main/0.0:{numOfSeats,pid_self}"];
+	n_1 -> n_3 [id="[$e|4]", label="main/0.0→agent/2.0:{booked,Num}"];
+	n_5 -> n_4 [id="[$e|2]", label="main/0.0→agent/2.0:{seats,Num}"];
+	n_2 -> n_3 [id="[$e|0]", label="main/0.0Δagent/2.0"];
+}

examples/cauder_suite/airline/main_0_local_view.dot

@@ -0,0 +1,17 @@
+digraph main_0 {
+	rankdir="LR";
+	n_0 [label="main_0", shape="plaintext"];
+	n_1 [id="5", shape=circle, label="3"];
+	n_2 [id="1", shape=circle, label="1"];
+	n_0 -> n_2 [arrowhead=none];
+	n_3 [id="2", shape=circle, label="2"];
+	n_4 [id="4", shape=doublecircle, label="4"];
+	n_5 [id="7", shape=circle, label="5"];
+
+	n_1 -> n_3 [id="[$e|12]", label="send {seats,Num} to Pid"];
+	n_5 -> n_3 [id="[$e|8]", label="send {booked,Num} to Pid"];
+	n_3 -> n_1 [id="[$e|1]", label="receive {numOfSeats,Pid}"];
+	n_3 -> n_5 [id="[$e|7]", label="receive {sell,Pid}"];
+	n_3 -> n_4 [id="[$e|5]", label="receive stop"];
+	n_2 -> n_3 [id="[$e|13]", label="spawn agent/2.0"];
+}

examples/cauder_suite/barber/README.md

@@ -0,0 +1,7 @@
+# barber example
+
+## Usage
+
+```bash
+./_build/default/bin/chorer ./examples/cauder_suite/barber/barber.erl main/0 ./examples/cauder_suite/barber
+```

examples/cauder_suite/barber/barber.erl

@@ -0,0 +1,73 @@
+% sleeping barber problem (with a bug)
+
+-module(barber).
+-export([main/0, open_barber_shop/0, barber/1, customer/3]).
+
+main() ->
+    io:format("~nCustomers: John and Joe~n~n"),
+    ShopPid = spawn(?MODULE, open_barber_shop, []),
+    spawn(?MODULE, customer, [ShopPid, 'John', self()]),
+    spawn(?MODULE, customer, [ShopPid, 'Joe', self()]),
+    receive
+        {Name1, State1} -> io:format("~p ~p~n", [Name1, State1])
+    end,
+    receive
+        {Name2, State2} -> io:format("~p ~p~n", [Name2, State2])
+    end,
+    ShopPid ! stop.
+
+%%customer
+customer(ShopPid, Name, MainPid) ->
+    ShopPid ! {new, {self(), Name}},
+    receive
+        X -> MainPid ! {Name, X}
+    end.
+
+%% barber %%
+barber(ShopPid) ->
+    ShopPid ! ready,
+    receive
+        wakeup ->
+            barber(ShopPid);
+        {customer, Customer} ->
+            ShopPid ! {cut, Customer},
+            barber(ShopPid)
+    end.
+
+%% shop %%
+open_barber_shop() ->
+    BarberPid = spawn(?MODULE, barber, [self()]),
+    barber_shop(BarberPid, []).
+
+%% main loop
+barber_shop(BarberPid, CustomersInChairs) ->
+    receive
+        {cut, {CustomerPid, _}} ->
+            CustomerPid ! finished,
+            barber_shop(BarberPid, CustomersInChairs);
+        ready ->
+            respond_to_barber(BarberPid, CustomersInChairs);
+        {new, CustomerInfo} ->
+            add_customer_if_available(BarberPid, CustomerInfo, CustomersInChairs);
+        stop ->
+            stop
+    end.
+
+respond_to_barber(BarberPid, []) ->
+    barber_shop(BarberPid, []);
+respond_to_barber(BarberPid, List) ->
+    BarberPid ! {customer, last(List)},
+    barber_shop(BarberPid, removeCustomer(List)).
+
+% assuming 2 chairs
+add_customer_if_available(BarberPid, {CustomerPid, _CustomerName}, [X, Y | R]) ->
+    CustomerPid ! no_room,
+    barber_shop(BarberPid, [X, Y | R]);
+add_customer_if_available(BarberPid, {CustomerPid, CustomerName}, List) ->
+    BarberPid ! wakeup,
+    barber_shop(BarberPid, [{CustomerPid, CustomerName} | List]).
+
+last([A]) -> A;
+last([_A | R]) -> last(R).
+
+removeCustomer([_A | R]) -> R.

examples/cauder_suite/barber/main_0_local_view.dot

@@ -0,0 +1,19 @@
+digraph main_0 {
+	rankdir="LR";
+	n_0 [label="main_0", shape="plaintext"];
+	n_1 [id="5", shape=circle, label="5"];
+	n_2 [id="6", shape=circle, label="6"];
+	n_3 [id="1", shape=circle, label="1"];
+	n_0 -> n_3 [arrowhead=none];
+	n_4 [id="2", shape=circle, label="2"];
+	n_5 [id="4", shape=doublecircle, label="7"];
+	n_6 [id="7", shape=circle, label="3"];
+	n_7 [id="3", shape=circle, label="4"];
+
+	n_7 -> n_1 [id="[$e|4]", label="receive {Name1,State1}"];
+	n_3 -> n_4 [id="[$e|1]", label="spawn open_barber_shop/0.0"];
+	n_4 -> n_6 [id="[$e|0]", label="spawn customer/3.0"];
+	n_1 -> n_2 [id="[$e|5]", label="receive {Name2,State2}"];
+	n_6 -> n_7 [id="[$e|3]", label="spawn customer/3.1"];
+	n_2 -> n_5 [id="[$e|2]", label="send stop to open_barber_shop/0.0"];
+}

examples/cauder_suite/meViolation/README.md

@@ -0,0 +1,7 @@
+# Violation example
+
+## Use
+
+```bash
+./_build/default/bin/chorer ./examples/cauder_suite/meViolation/meViolation.erl main/0 examples/cauder_suite/meViolation
+```

examples/cauder_suite/meViolation/incrementer_0_local_view.dot

@@ -0,0 +1,19 @@
+digraph incrementer_0 {
+	rankdir="LR";
+	n_0 [label="incrementer_0", shape="plaintext"];
+	n_1 [id="5", shape=doublecircle, label="7"];
+	n_2 [id="6", shape=circle, label="5"];
+	n_3 [id="1", shape=circle, label="1"];
+	n_0 -> n_3 [arrowhead=none];
+	n_4 [id="2", shape=circle, label="2"];
+	n_5 [id="4", shape=circle, label="6"];
+	n_6 [id="7", shape=circle, label="3"];
+	n_7 [id="3", shape=circle, label="4"];
+
+	n_6 -> n_7 [id="[$e|4]", label="send {read,pid_self} to varManager/1.0"];
+	n_2 -> n_5 [id="[$e|1]", label="send {write,unknown} to varManager/1.0"];
+	n_5 -> n_1 [id="[$e|3]", label="send {release} to meManager/0.0"];
+	n_4 -> n_6 [id="[$e|0]", label="receive answer"];
+	n_7 -> n_2 [id="[$e|2]", label="receive X"];
+	n_3 -> n_4 [id="[$e|5]", label="send {request,pid_self} to meManager/0.0"];
+}

examples/cauder_suite/meViolation/main_0_global_view.dot

@@ -0,0 +1,84 @@
+digraph global {
+	rankdir="LR";
+	n_0 [label="global", shape="plaintext"];
+	n_1 [id="20", shape=circle, label="20"];
+	n_2 [id="27", shape=circle, label="27"];
+	n_3 [id="23", shape=circle, label="23"];
+	n_4 [id="25", shape=circle, label="25"];
+	n_5 [id="5", shape=circle, label="5"];
+	n_6 [id="28", shape=circle, label="28"];
+	n_7 [id="15", shape=circle, label="15"];
+	n_8 [id="19", shape=circle, label="19"];
+	n_9 [id="12", shape=circle, label="12"];
+	n_10 [id="11", shape=circle, label="11"];
+	n_11 [id="17", shape=circle, label="17"];
+	n_12 [id="18", shape=circle, label="18"];
+	n_13 [id="14", shape=circle, label="14"];
+	n_14 [id="6", shape=circle, label="6"];
+	n_15 [id="13", shape=circle, label="13"];
+	n_16 [id="24", shape=circle, label="24"];
+	n_17 [id="10", shape=circle, label="10"];
+	n_18 [id="22", shape=circle, label="22"];
+	n_19 [id="1", shape=circle, label="1"];
+	n_0 -> n_19 [arrowhead=none];
+	n_20 [id="26", shape=circle, label="26"];
+	n_21 [id="9", shape=circle, label="9"];
+	n_22 [id="2", shape=circle, label="2"];
+	n_23 [id="21", shape=circle, label="21"];
+	n_24 [id="8", shape=circle, label="8"];
+	n_25 [id="4", shape=circle, label="4"];
+	n_26 [id="7", shape=circle, label="7"];
+	n_27 [id="3", shape=circle, label="3"];
+	n_28 [id="16", shape=circle, label="16"];
+
+	n_4 -> n_2 [id="[$e|39]", label="incrementer/0.1→meManager/0.0:{release}"];
+	n_17 -> n_9 [id="[$e|11]", label="varManager/1.0→incrementer/0.1:Val"];
+	n_11 -> n_13 [id="[$e|22]", label="incrementer/0.0→varManager/1.0:{write,unknown}"];
+	n_5 -> n_14 [id="[$e|4]", label="incrementer/0.0→meManager/0.0:{request,pid_self}"];
+	n_4 -> n_6 [id="[$e|40]", label="incrementer/0.0→varManager/1.0:{write,unknown}"];
+	n_22 -> n_27 [id="[$e|1]", label="main/0.0ΔvarManager/1.0"];
+	n_20 -> n_6 [id="[$e|44]", label="incrementer/0.1→varManager/1.0:{write,unknown}"];
+	n_25 -> n_5 [id="[$e|3]", label="main/0.0Δincrementer/0.1"];
+	n_15 -> n_15 [id="[$e|17]", label="incrementer/0.0→varManager/1.0:{write,unknown}"];
+	n_13 -> n_8 [id="[$e|26]", label="meManager/0.0→incrementer/0.1:answer"];
+	n_1 -> n_16 [id="[$e|31]", label="incrementer/0.0→varManager/1.0:{read,pid_self}"];
+	n_13 -> n_15 [id="[$e|18]", label="incrementer/0.0→meManager/0.0:{release}"];
+	n_6 -> n_2 [id="[$e|46]", label="incrementer/0.1→meManager/0.0:{release}"];
+	n_26 -> n_21 [id="[$e|8]", label="incrementer/0.0→varManager/1.0:{read,pid_self}"];
+	n_24 -> n_17 [id="[$e|9]", label="incrementer/0.1→varManager/1.0:{read,pid_self}"];
+	n_4 -> n_6 [id="[$e|41]", label="incrementer/0.1→varManager/1.0:{write,unknown}"];
+	n_8 -> n_18 [id="[$e|28]", label="incrementer/0.1→varManager/1.0:{read,pid_self}"];
+	n_10 -> n_15 [id="[$e|12]", label="incrementer/0.0→meManager/0.0:{release}"];
+	n_10 -> n_13 [id="[$e|13]", label="incrementer/0.0→varManager/1.0:{write,unknown}"];
+	n_14 -> n_26 [id="[$e|6]", label="meManager/0.0→incrementer/0.0:answer"];
+	n_14 -> n_24 [id="[$e|7]", label="meManager/0.0→incrementer/0.1:answer"];
+	n_9 -> n_7 [id="[$e|14]", label="incrementer/0.1→meManager/0.0:{release}"];
+	n_6 -> n_6 [id="[$e|48]", label="incrementer/0.0→varManager/1.0:{write,unknown}"];
+	n_6 -> n_6 [id="[$e|47]", label="incrementer/0.1→varManager/1.0:{write,unknown}"];
+	n_20 -> n_2 [id="[$e|43]", label="incrementer/0.0→meManager/0.0:{release}"];
+	n_20 -> n_6 [id="[$e|45]", label="incrementer/0.0→varManager/1.0:{write,unknown}"];
+	n_7 -> n_7 [id="[$e|20]", label="incrementer/0.1→varManager/1.0:{write,unknown}"];
+	n_1 -> n_3 [id="[$e|30]", label="incrementer/0.1→varManager/1.0:{write,unknown}"];
+	n_28 -> n_7 [id="[$e|21]", label="incrementer/0.1→meManager/0.0:{release}"];
+	n_8 -> n_23 [id="[$e|27]", label="incrementer/0.0→varManager/1.0:{write,unknown}"];
+	n_19 -> n_22 [id="[$e|0]", label="main/0.0ΔmeManager/0.0"];
+	n_7 -> n_12 [id="[$e|19]", label="incrementer/0.0→meManager/0.0:{request,pid_self}"];
+	n_12 -> n_28 [id="[$e|24]", label="incrementer/0.1→varManager/1.0:{write,unknown}"];
+	n_15 -> n_11 [id="[$e|16]", label="incrementer/0.1→meManager/0.0:{request,pid_self}"];
+	n_9 -> n_28 [id="[$e|15]", label="incrementer/0.1→varManager/1.0:{write,unknown}"];
+	n_12 -> n_1 [id="[$e|25]", label="meManager/0.0→incrementer/0.0:answer"];
+	n_23 -> n_18 [id="[$e|32]", label="incrementer/0.1→varManager/1.0:{read,pid_self}"];
+	n_27 -> n_25 [id="[$e|2]", label="main/0.0Δincrementer/0.0"];
+	n_23 -> n_4 [id="[$e|38]", label="varManager/1.0→incrementer/0.1:Val"];
+	n_28 -> n_1 [id="[$e|29]", label="meManager/0.0→incrementer/0.0:answer"];
+	n_3 -> n_20 [id="[$e|42]", label="varManager/1.0→incrementer/0.0:Val"];
+	n_5 -> n_14 [id="[$e|5]", label="incrementer/0.1→meManager/0.0:{request,pid_self}"];
+	n_21 -> n_10 [id="[$e|10]", label="varManager/1.0→incrementer/0.0:Val"];
+	n_16 -> n_20 [id="[$e|37]", label="varManager/1.0→incrementer/0.0:Val"];
+	n_16 -> n_3 [id="[$e|36]", label="incrementer/0.1→varManager/1.0:{write,unknown}"];
+	n_11 -> n_8 [id="[$e|23]", label="meManager/0.0→incrementer/0.1:answer"];
+	n_6 -> n_2 [id="[$e|49]", label="incrementer/0.0→meManager/0.0:{release}"];
+	n_18 -> n_4 [id="[$e|34]", label="varManager/1.0→incrementer/0.1:Val"];
+	n_3 -> n_16 [id="[$e|35]", label="incrementer/0.0→varManager/1.0:{read,pid_self}"];
+	n_18 -> n_23 [id="[$e|33]", label="incrementer/0.0→varManager/1.0:{write,unknown}"];
+}

examples/cauder_suite/meViolation/main_0_local_view.dot

@@ -0,0 +1,15 @@
+digraph main_0 {
+	rankdir="LR";
+	n_0 [label="main_0", shape="plaintext"];
+	n_1 [id="5", shape=circle, label="3"];
+	n_2 [id="1", shape=circle, label="1"];
+	n_0 -> n_2 [arrowhead=none];
+	n_3 [id="2", shape=circle, label="2"];
+	n_4 [id="4", shape=doublecircle, label="5"];
+	n_5 [id="3", shape=circle, label="4"];
+
+	n_2 -> n_3 [id="[$e|1]", label="spawn meManager/0.0"];
+	n_1 -> n_5 [id="[$e|3]", label="spawn incrementer/0.0"];
+	n_5 -> n_4 [id="[$e|0]", label="spawn incrementer/0.1"];
+	n_3 -> n_1 [id="[$e|2]", label="spawn varManager/1.0"];
+}