Skip to content

Commit

Permalink
Added cauder case studies (to test.py as well)
Browse files Browse the repository at this point in the history
  • Loading branch information
lanese committed Apr 18, 2024
1 parent d45f49b commit ad8836b
Show file tree
Hide file tree
Showing 70 changed files with 444 additions and 232 deletions.
2 changes: 1 addition & 1 deletion examples/airline/agent_1_local_view.dot
Original file line number Diff line number Diff line change
Expand Up @@ -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,_}"];
}
33 changes: 15 additions & 18 deletions examples/airline/main_0_global_view.dot
Original file line number Diff line number Diff line change
Expand Up @@ -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}"];
}
2 changes: 1 addition & 1 deletion examples/airline/main_0_local_view.dot
Original file line number Diff line number Diff line change
Expand Up @@ -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"];
}
6 changes: 3 additions & 3 deletions examples/async/main_0_global_view.dot
Original file line number Diff line number Diff line change
Expand Up @@ -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"];
}
31 changes: 31 additions & 0 deletions examples/cauder_suite/airline/airline.erl
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
-module(airline).
-export([main/0, agent/2]).

main() ->
Main = self(),
spawn(?MODULE, agent, [1, Main]),
spawn(?MODULE, agent, [2, Main]),
seats(3).

seats(Num) ->
receive
{numOfSeats, Pid} ->
Pid ! {seats, Num},
seats(Num);
{sell, Pid} ->
io:format("Seat sold!~n"),
Pid ! {booked, Num},
seats(Num - 1)
end.

agent(NAg, Pid) ->
Pid ! {numOfSeats, self()},
receive
{seats, Num} when Num > 0 ->
Pid ! {sell, self()},
receive
{booked, _} -> agent(NAg, Pid)
end;
_ ->
io:format("Agent~p done!~n", [NAg])
end.
73 changes: 73 additions & 0 deletions examples/cauder_suite/barber/barber.erl
Original file line number Diff line number Diff line change
@@ -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.
19 changes: 19 additions & 0 deletions examples/cauder_suite/barber/main_0_local_view.dot
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
digraph main_0 {
rankdir="LR";
n_0 [label="main_0", shape="plaintext"];
n_1 [id="5", shape=circle, label="5"];
n_2 [id="6", shape=circle, label="6"];
n_3 [id="1", shape=circle, label="1"];
n_0 -> n_3 [arrowhead=none];
n_4 [id="2", shape=circle, label="2"];
n_5 [id="4", shape=doublecircle, label="7"];
n_6 [id="7", shape=circle, label="3"];
n_7 [id="3", shape=circle, label="4"];

n_1 -> n_2 [id="[$e|5]", label="receive {Name2,State2}"];
n_4 -> n_6 [id="[$e|0]", label="spawn customer/3.0"];
n_2 -> n_5 [id="[$e|2]", label="send stop to open_barber_shop/0.0"];
n_6 -> n_7 [id="[$e|3]", label="spawn customer/3.1"];
n_7 -> n_1 [id="[$e|4]", label="receive {Name1,State1}"];
n_3 -> n_4 [id="[$e|1]", label="spawn open_barber_shop/0.0"];
}
40 changes: 40 additions & 0 deletions examples/cauder_suite/meViolation/meViolation.erl
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@
%code showing a mutual exclusion violation
%the two concurrent increments of the variable managed by varManager
%may lead to final value 1 instead of 2 under some schedulings

-module(meViolation).
-export([main/0, meManager/0, varManager/1, incrementer/2]).

main() ->
MePid = spawn(?MODULE, meManager, []),
XPid = spawn(?MODULE, varManager, [0]),
spawn(?MODULE, incrementer, [MePid, XPid]),
spawn(?MODULE, incrementer, [MePid, XPid]).

meManager() ->
receive
{request, Pid} -> Pid ! answer
end,
receive
{release} -> meManager()
end.

varManager(Val) ->
io:format("Variable value:~b~n", [Val]),
receive
{write, NewVal} -> varManager(NewVal);
{read, Pid} -> Pid ! Val
end,
varManager(Val).

incrementer(MePid, XPid) ->
MePid ! {request, self()},
receive
answer ->
XPid ! {read, self()},
receive
X ->
XPid ! {write, X + 1},
MePid ! {release}
end
end.
47 changes: 47 additions & 0 deletions examples/cauder_suite/purchase/purchase.erl
Original file line number Diff line number Diff line change
@@ -0,0 +1,47 @@
%FASE 2014 example

-module(purchase).
-export([main/0, asynchAnd/2, checkCredit/2, checkAddress/1, checkItem/1]).

main() ->
Pid = spawn(?MODULE, asynchAnd, [2, self()]),
spawn(?MODULE, checkCredit, [15, Pid]),
spawn(?MODULE, checkAddress, [Pid]),
spawn(?MODULE, checkItem, [Pid]),
receive
true ->
io:format("All checks successful.~n"),
true;
false ->
io:format("Check failure.~n"),
false
end.

asynchAnd(N, Out) ->
if
N > 0 ->
receive
true -> asynchAnd(N - 1, Out);
false -> Out ! false
end;
true ->
Out ! true
end.

checkCredit(Price, Pid) ->
if
Price < 10 ->
io:format("Credit check successful~n"),
Pid ! true;
true ->
io:format("Credit check failed~n"),
Pid ! false
end.

checkAddress(Pid) ->
io:format("Address check successful~n"),
Pid ! true.

checkItem(Pid) ->
io:format("Item check successful~n"),
Pid ! true.
2 changes: 1 addition & 1 deletion examples/conditional-case/dummy_1_local_view.dot
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,6 @@ digraph dummy_1 {
n_2 [id="2", shape=circle, label="2"];
n_3 [id="3", shape=doublecircle, label="3"];

n_2 -> n_3 [id="[$e|1]", label="receive Str"];
n_1 -> n_2 [id="[$e|0]", label="send {pid_self,integer} to Pid"];
n_2 -> n_3 [id="[$e|1]", label="receive Str"];
}
14 changes: 7 additions & 7 deletions examples/conditional-case/main_0_global_view.dot
Original file line number Diff line number Diff line change
Expand Up @@ -12,15 +12,15 @@ digraph global {
n_8 [id="7", shape=circle, label="7"];
n_9 [id="3", shape=circle, label="3"];

n_2 -> n_4 [id="[$e|10]", label="main/0.0→dummy/1.2:'Ciao"];
n_2 -> n_6 [id="[$e|9]", label="main/0.0→dummy/1.1:'Ciao"];
n_2 -> n_8 [id="[$e|8]", label="main/0.0→dummy/1.0:'Ciao"];
n_1 -> n_2 [id="[$e|6]", label="dummy/1.2→main/0.0:{pid_self,integer}"];
n_7 -> n_1 [id="[$e|3]", label="main/0.0Δdummy/1.3"];
n_1 -> n_2 [id="[$e|6]", label="dummy/1.2→main/0.0:{pid_self,integer}"];
n_9 -> n_7 [id="[$e|2]", label="main/0.0Δdummy/1.2"];
n_1 -> n_2 [id="[$e|5]", label="dummy/1.1→main/0.0:{pid_self,integer}"];
n_2 -> n_8 [id="[$e|8]", label="main/0.0→dummy/1.0:'Ciao"];
n_3 -> n_5 [id="[$e|0]", label="main/0.0Δdummy/1.0"];
n_5 -> n_9 [id="[$e|1]", label="main/0.0Δdummy/1.1"];
n_1 -> n_2 [id="[$e|4]", label="dummy/1.0→main/0.0:{pid_self,integer}"];
n_1 -> n_2 [id="[$e|7]", label="dummy/1.3→main/0.0:{pid_self,integer}"];
n_3 -> n_5 [id="[$e|0]", label="main/0.0Δdummy/1.0"];
n_1 -> n_2 [id="[$e|4]", label="dummy/1.0→main/0.0:{pid_self,integer}"];
n_1 -> n_2 [id="[$e|5]", label="dummy/1.1→main/0.0:{pid_self,integer}"];
n_2 -> n_4 [id="[$e|10]", label="main/0.0→dummy/1.1:'Ciao"];
n_2 -> n_6 [id="[$e|9]", label="main/0.0→dummy/1.3:'Ciao"];
}
8 changes: 4 additions & 4 deletions examples/conditional-case/main_0_local_view.dot
Original file line number Diff line number Diff line change
Expand Up @@ -10,12 +10,12 @@ digraph main_0 {
n_6 [id="4", shape=circle, label="4"];
n_7 [id="3", shape=doublecircle, label="7"];

n_1 -> n_7 [id="[$e|10]", label="send 'Ciao C' to dummy/1.2"];
n_1 -> n_7 [id="[$e|9]", label="send 'Ciao B' to dummy/1.1"];
n_5 -> n_2 [id="[$e|8]", label="spawn dummy/1.1"];
n_1 -> n_7 [id="[$e|3]", label="send 'Ciao A' to dummy/1.0"];
n_6 -> n_4 [id="[$e|2]", label="spawn dummy/1.3"];
n_5 -> n_2 [id="[$e|8]", label="spawn dummy/1.1"];
n_3 -> n_5 [id="[$e|0]", label="spawn dummy/1.0"];
n_2 -> n_6 [id="[$e|1]", label="spawn dummy/1.2"];
n_4 -> n_1 [id="[$e|4]", label="receive {Process,_}"];
n_3 -> n_5 [id="[$e|0]", label="spawn dummy/1.0"];
n_1 -> n_7 [id="[$e|10]", label="send 'Ciao B' to dummy/1.1"];
n_1 -> n_7 [id="[$e|9]", label="send 'Ciao D' to dummy/1.3"];
}
2 changes: 1 addition & 1 deletion examples/customer/customer_0_local_view.dot
Original file line number Diff line number Diff line change
Expand Up @@ -10,8 +10,8 @@ digraph customer_0 {

n_1 -> n_3 [id="[$e|0]", label="send buy to store/0.0"];
n_1 -> n_2 [id="[$e|9]", label="send more to store/0.0"];
n_4 -> n_5 [id="[$e|5]", label="receive accepted"];
n_4 -> n_3 [id="[$e|8]", label="receive reject"];
n_4 -> n_5 [id="[$e|5]", label="receive accepted"];
n_3 -> n_4 [id="[$e|4]", label="send payment to store/0.0"];
n_2 -> n_1 [id="[$e|1]", label="send item to store/0.0"];
}
6 changes: 3 additions & 3 deletions examples/customer/customer_dummy_0_local_view.dot
Original file line number Diff line number Diff line change
Expand Up @@ -9,11 +9,11 @@ digraph customer_dummy_0 {
n_5 [id="8", shape=circle, label="3"];
n_6 [id="4", shape=doublecircle, label="6"];

n_5 -> n_4 [id="[$e|10]", label="send buy to store/0.0"];
n_2 -> n_4 [id="[$e|3]", label="receive reject"];
n_3 -> n_1 [id="[$e|0]", label="send ciao to store/0.0"];
n_5 -> n_1 [id="[$e|9]", label="send more to store/0.0"];
n_1 -> n_5 [id="[$e|5]", label="send item to store/0.0"];
n_2 -> n_4 [id="[$e|3]", label="receive reject"];
n_4 -> n_2 [id="[$e|8]", label="send payment to store/0.0"];
n_2 -> n_6 [id="[$e|2]", label="receive accepted"];
n_5 -> n_4 [id="[$e|10]", label="send buy to store/0.0"];
n_1 -> n_5 [id="[$e|5]", label="send item to store/0.0"];
}
8 changes: 4 additions & 4 deletions examples/customer/main_0_global_view.dot
Original file line number Diff line number Diff line change
Expand Up @@ -12,14 +12,14 @@ digraph global {
n_8 [id="7", shape=circle, label="7"];
n_9 [id="3", shape=circle, label="3"];

n_7 -> n_1 [id="[$e|3]", label="customer_dummy/0.0→store/0.0:buy"];
n_8 -> n_6 [id="[$e|7]", label="store/0.0→customer_dummy/0.0:accepted"];
n_3 -> n_5 [id="[$e|0]", label="main/0.0Δstore/0.0"];
n_4 -> n_8 [id="[$e|9]", label="customer_dummy/0.0→store/0.0:payment"];
n_1 -> n_8 [id="[$e|5]", label="customer_dummy/0.0→store/0.0:payment"];
n_7 -> n_1 [id="[$e|3]", label="customer_dummy/0.0→store/0.0:buy"];
n_8 -> n_4 [id="[$e|8]", label="store/0.0→customer_dummy/0.0:reject"];
n_2 -> n_7 [id="[$e|6]", label="customer_dummy/0.0→store/0.0:item"];
n_9 -> n_7 [id="[$e|2]", label="customer_dummy/0.0→store/0.0:item"];
n_8 -> n_6 [id="[$e|7]", label="store/0.0→customer_dummy/0.0:accepted"];
n_1 -> n_8 [id="[$e|5]", label="customer_dummy/0.0→store/0.0:payment"];
n_2 -> n_7 [id="[$e|6]", label="customer_dummy/0.0→store/0.0:item"];
n_7 -> n_2 [id="[$e|4]", label="customer_dummy/0.0→store/0.0:more"];
n_5 -> n_9 [id="[$e|1]", label="main/0.0Δcustomer_dummy/0.0"];
}
2 changes: 1 addition & 1 deletion examples/customer/store_0_local_view.dot
Original file line number Diff line number Diff line change
Expand Up @@ -8,9 +8,9 @@ digraph store_0 {
n_4 [id="4", shape=circle, label="3"];
n_5 [id="3", shape=circle, label="2"];

n_3 -> n_1 [id="[$e|3]", label="send accepted to customer_dummy/0.0"];
n_4 -> n_3 [id="[$e|0]", label="receive payment"];
n_3 -> n_4 [id="[$e|9]", label="send reject to customer_dummy/0.0"];
n_3 -> n_1 [id="[$e|3]", label="send accepted to customer_dummy/0.0"];
n_5 -> n_2 [id="[$e|8]", label="receive more"];
n_2 -> n_5 [id="[$e|6]", label="receive item"];
n_5 -> n_4 [id="[$e|1]", label="receive buy"];
Expand Down
Loading

0 comments on commit ad8836b

Please # to comment.