Skip to content

Commit

Permalink
added thesis and better readme
Browse files Browse the repository at this point in the history
  • Loading branch information
gabrielegenovese committed Jul 17, 2023
1 parent 8e1dfc2 commit a4c3af7
Show file tree
Hide file tree
Showing 13 changed files with 44 additions and 21 deletions.
20 changes: 17 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,11 +1,25 @@
# ChorEr

A static analyzer to generate Choreography Automata from Erlang source.
ChorEr is a static analyzer to generate Choreography Automata from Erlang source code.

## Requirements

The project requires `erlang` and `rebar3` to run.

## Usage

Use `rebar3` to run the program from the Command Line.

```erlang
# rebar3 shell
1> chorer_app:gen_chor("./example/simple.erl", "out").
...
1> chorer_app:generate("./examples/ticktack/tictacstop.erl", start).
finished
```

The tool will create a DOT file for each actor's local view and a DOT for the global view in your folder. To visualize the Choreography Automatas, copy paste the content's files in a [DOT viewer](https://dreampuf.github.io/GraphvizOnline).


## Credits

This project was made for the Bachelor's degree Thesis of the Computer Science course at Alma Mater Studiotum - University of Bologna.
I am grateful to the professor [Ivan Lanese](https://github.com/lanese), who supervised the develpment of this project.
2 changes: 1 addition & 1 deletion examples/async/dummy1_local_view.dot
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,6 @@ digraph dummy1 {
n_2 [id="2", shape=circle, label="2"];
n_3 [id="3", shape=doublecircle, label="3"];

n_1 -> n_2 [id="[$e|1]", label="send ciao to dummy20"];
n_1 -> n_2 [id="[$e|1]", label="send bello to dummy20"];
n_2 -> n_3 [id="[$e|0]", label="receive ciao"];
}
2 changes: 1 addition & 1 deletion examples/async/dummy2_local_view.dot
Original file line number Diff line number Diff line change
Expand Up @@ -7,5 +7,5 @@ digraph dummy2 {
n_3 [id="3", shape=doublecircle, label="3"];

n_1 -> n_2 [id="[$e|1]", label="send ciao to dummy10"];
n_2 -> n_3 [id="[$e|0]", label="receive ciao"];
n_2 -> n_3 [id="[$e|0]", label="receive bello"];
}
4 changes: 2 additions & 2 deletions examples/async/main_global_view.dot
Original file line number Diff line number Diff line change
Expand Up @@ -11,9 +11,9 @@ digraph global {
n_7 [id="3", shape=circle, label="3"];

n_4 -> n_7 [id="[$e|1]", label="mainΔdummy20"];
n_5 -> n_1 [id="[$e|3]", label="dummy10→dummy20:ciao"];
n_5 -> n_1 [id="[$e|3]", label="dummy10→dummy20:bello"];
n_2 -> n_6 [id="[$e|5]", label="dummy20→dummy10:ciao"];
n_3 -> n_4 [id="[$e|0]", label="mainΔdummy10"];
n_7 -> n_2 [id="[$e|4]", label="dummy10→dummy20:ciao"];
n_7 -> n_2 [id="[$e|4]", label="dummy10→dummy20:bello"];
n_7 -> n_5 [id="[$e|2]", label="dummy20→dummy10:ciao"];
}
4 changes: 2 additions & 2 deletions examples/async/simple.erl
Original file line number Diff line number Diff line change
Expand Up @@ -2,15 +2,15 @@
-export([main/0, dummy1/0, dummy2/0]).

dummy1() ->
d2 ! ciao,
d2 ! bello,
receive
ciao -> done
end.

dummy2() ->
d1 ! ciao,
receive
ciao -> done
bello -> done
end.

main() ->
Expand Down
7 changes: 7 additions & 0 deletions examples/async/super_dummy_local_view.dot
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
digraph super_dummy {
rankdir="LR";
n_0 [label="super_dummy", shape="plaintext"];
n_1 [id="1", shape=circle, label="1"];
n_0 -> n_1 [arrowhead=none];

}
12 changes: 6 additions & 6 deletions examples/ticktack/start_global_view.dot
Original file line number Diff line number Diff line change
Expand Up @@ -13,14 +13,14 @@ digraph global {
n_9 [id="7", shape=circle, label="7"];
n_10 [id="3", shape=circle, label="3"];

n_10 -> n_8 [id="[$e|2]", label="startΔrandom0"];
n_4 -> n_6 [id="[$e|0]", label="startΔtac_loop0"];
n_6 -> n_10 [id="[$e|1]", label="startΔtic_loop0"];
n_8 -> n_1 [id="[$e|3]", label="start→tic_loop0:tac"];
n_2 -> n_9 [id="[$e|6]", label="random0→tic_loop0:stop"];
n_9 -> n_7 [id="[$e|7]", label="tic_loop0→tac_loop0:stop"];
n_2 -> n_1 [id="[$e|5]", label="tac_loop0→tic_loop0:tac"];
n_4 -> n_6 [id="[$e|0]", label="startΔtac_loop0"];
n_8 -> n_5 [id="[$e|8]", label="random0→tic_loop0:stop"];
n_1 -> n_2 [id="[$e|4]", label="tic_loop0→tac_loop0:tic"];
n_10 -> n_8 [id="[$e|2]", label="startΔrandom0"];
n_2 -> n_9 [id="[$e|6]", label="random0→tic_loop0:stop"];
n_5 -> n_3 [id="[$e|9]", label="tic_loop0→tac_loop0:stop"];
n_8 -> n_1 [id="[$e|3]", label="start→tic_loop0:tac"];
n_1 -> n_2 [id="[$e|4]", label="tic_loop0→tac_loop0:tic"];
n_8 -> n_5 [id="[$e|8]", label="random0→tic_loop0:stop"];
}
4 changes: 2 additions & 2 deletions examples/ticktack/start_local_view.dot
Original file line number Diff line number Diff line change
Expand Up @@ -8,8 +8,8 @@ digraph start {
n_4 [id="4", shape=doublecircle, label="4"];
n_5 [id="3", shape=circle, label="3"];

n_3 -> n_5 [id="[$e|2]", label="spawn tic_loop0"];
n_1 -> n_4 [id="[$e|0]", label="send tac to tic_loop0"];
n_2 -> n_3 [id="[$e|1]", label="spawn tac_loop0"];
n_5 -> n_1 [id="[$e|3]", label="spawn random0"];
n_1 -> n_4 [id="[$e|0]", label="send tac to tic_loop0"];
n_3 -> n_5 [id="[$e|2]", label="spawn tic_loop0"];
}
2 changes: 1 addition & 1 deletion examples/ticktack/tac_loop_local_view.dot
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ digraph tac_loop {
n_2 [id="2", shape=circle, label="2"];
n_3 [id="4", shape=doublecircle, label="4"];

n_1 -> n_3 [id="[$e|2]", label="receive stop"];
n_1 -> n_2 [id="[$e|1]", label="receive tic"];
n_2 -> n_1 [id="[$e|5]", label="send tac to tic_loop0"];
n_1 -> n_3 [id="[$e|2]", label="receive stop"];
}
4 changes: 2 additions & 2 deletions examples/ticktack/tic_loop_local_view.dot
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@ digraph tic_loop {
n_3 [id="2", shape=circle, label="2"];
n_4 [id="3", shape=doublecircle, label="3"];

n_2 -> n_1 [id="[$e|3]", label="receive stop"];
n_3 -> n_2 [id="[$e|6]", label="send tic to tac_loop0"];
n_2 -> n_3 [id="[$e|0]", label="receive tac"];
n_3 -> n_2 [id="[$e|6]", label="send tic to tac_loop0"];
n_2 -> n_1 [id="[$e|3]", label="receive stop"];
n_1 -> n_4 [id="[$e|4]", label="send stop to tac_loop0"];
}
4 changes: 3 additions & 1 deletion src/choreography/local_view.erl
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@
%%%===================================================================

%%% Generate a local view for each actor
generate(OutputDir,Options) ->
generate(OutputDir, Options) ->
ActorList = db_manager:get_actors(),
%%% For each actor, create and save the local view
lists:foreach(
Expand Down Expand Up @@ -219,6 +219,8 @@ eval_codeline(CodeLine, FunName, G, AccData, SetPm) ->
{nil, _} ->
{#variable{type = list, value = []}, VLast, LocalVarL};
_ ->
%%% TODO Mettere warning
io:fwrite("WARNING: couldn't parse code line ~p~n", [CodeLine]),
AccData
end.

Expand Down
Binary file added thesis.pdf
Binary file not shown.
Binary file added thesis_presentation.pdf
Binary file not shown.

0 comments on commit a4c3af7

Please # to comment.