fixed some example from the cauder suite

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

@@ -4,7 +4,6 @@
 main() ->
     Main = self(),
     spawn(?MODULE, agent, [1, Main]),
-    spawn(?MODULE, agent, [2, Main]),
     seats(3).
 
 seats(Num) ->
@@ -15,7 +14,9 @@ seats(Num) ->
         {sell, Pid} ->
             io:format("Seat sold!~n"),
             Pid ! {booked, Num},
-            seats(Num - 1)
+            seats(Num - 1);
+        stop ->
+            done
     end.
 
 agent(NAg, Pid) ->
@@ -26,6 +27,6 @@ agent(NAg, Pid) ->
             receive
                 {booked, _} -> agent(NAg, Pid)
             end;
-        _ ->
-            io:format("Agent~p done!~n", [NAg])
+        {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/main_0_local_view.dot

@@ -10,10 +10,10 @@ digraph main_0 {
 	n_6 [id="7", shape=circle, label="3"];
 	n_7 [id="3", shape=circle, label="4"];
 
-	n_1 -> n_2 [id="[$e|5]", label="receive {Name2,State2}"];
-	n_4 -> n_6 [id="[$e|0]", label="spawn customer/3.0"];
-	n_2 -> n_5 [id="[$e|2]", label="send stop to open_barber_shop/0.0"];
-	n_6 -> n_7 [id="[$e|3]", label="spawn customer/3.1"];
 	n_7 -> n_1 [id="[$e|4]", label="receive {Name1,State1}"];
 	n_3 -> n_4 [id="[$e|1]", label="spawn open_barber_shop/0.0"];
+	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"];
+}

examples/cauder_suite/meViolation/meManager_0_local_view.dot

@@ -0,0 +1,12 @@
+digraph meManager_0 {
+	rankdir="LR";
+	n_0 [label="meManager_0", shape="plaintext"];
+	n_1 [id="1", shape=circle, label="1"];
+	n_0 -> n_1 [arrowhead=none];
+	n_2 [id="2", shape=circle, label="2"];
+	n_3 [id="3", shape=circle, label="3"];
+
+	n_3 -> n_1 [id="[$e|4]", label="receive {release}"];
+	n_2 -> n_3 [id="[$e|1]", label="send answer to Pid"];
+	n_1 -> n_2 [id="[$e|2]", label="receive {request,Pid}"];
+}

examples/cauder_suite/meViolation/meViolation.erl

@@ -3,13 +3,15 @@
 %may lead to final value 1 instead of 2 under some schedulings
 
 -module(meViolation).
--export([main/0, meManager/0, varManager/1, incrementer/2]).
+-export([main/0, meManager/0, varManager/1, incrementer/0]).
 
 main() ->
     MePid = spawn(?MODULE, meManager, []),
     XPid = spawn(?MODULE, varManager, [0]),
-    spawn(?MODULE, incrementer, [MePid, XPid]),
-    spawn(?MODULE, incrementer, [MePid, XPid]).
+    register(xx, XPid),
+    register(mm, MePid),
+    spawn(?MODULE, incrementer, []),
+    spawn(?MODULE, incrementer, []).
 
 meManager() ->
     receive
@@ -27,14 +29,14 @@ varManager(Val) ->
     end,
     varManager(Val).
 
-incrementer(MePid, XPid) ->
-    MePid ! {request, self()},
+incrementer() ->
+    mm ! {request, self()},
     receive
         answer ->
-            XPid ! {read, self()},
+            xx ! {read, self()},
             receive
                 X ->
-                    XPid ! {write, X + 1},
-                    MePid ! {release}
+                    xx ! {write, X + 1},
+                    mm ! {release}
             end
     end.

examples/cauder_suite/meViolation/varManager_1_local_view.dot

@@ -0,0 +1,11 @@
+digraph varManager_1 {
+	rankdir="LR";
+	n_0 [label="varManager_1", shape="plaintext"];
+	n_1 [id="1", shape=circle, label="1"];
+	n_0 -> n_1 [arrowhead=none];
+	n_2 [id="4", shape=circle, label="2"];
+
+	n_1 -> n_1 [id="[$e|7]", label="receive {write,NewVal}"];
+	n_1 -> n_2 [id="[$e|0]", label="receive {read,Pid}"];
+	n_2 -> n_1 [id="[$e|10]", label="send Val to Pid"];
+}