diff --git a/examples/customer/customer_0_local_view.dot b/examples/customer/customer_0_local_view.dot index ff70361..a9515a4 100644 --- a/examples/customer/customer_0_local_view.dot +++ b/examples/customer/customer_0_local_view.dot @@ -8,10 +8,10 @@ digraph customer_0 { n_4 [id="2", shape=circle, label="3"]; n_5 [id="5", shape=circle, label="2"]; - n_5 -> n_4 [id="[$e|1]", label="store/0.0 ! buy"]; + n_4 -> n_3 [id="[$e|5]", label="store/0.0 ! payment"]; n_5 -> n_1 [id="[$e|9]", label="store/0.0 ! more"]; n_3 -> n_2 [id="[$e|6]", label="0#receive accepted"]; - n_4 -> n_3 [id="[$e|5]", label="store/0.0 ! payment"]; - n_1 -> n_5 [id="[$e|2]", label="store/0.0 ! item"]; n_3 -> n_4 [id="[$e|8]", label="1#receive reject"]; + n_1 -> n_5 [id="[$e|2]", label="store/0.0 ! item"]; + n_5 -> n_4 [id="[$e|1]", label="store/0.0 ! buy"]; } diff --git a/examples/customer/main_0_global_view.dot b/examples/customer/main_0_global_view.dot index 4c1715f..6574ef1 100644 --- a/examples/customer/main_0_global_view.dot +++ b/examples/customer/main_0_global_view.dot @@ -1,34 +1,25 @@ digraph global { rankdir="LR"; n_0 [label="global", shape="plaintext"]; - n_1 [id="14", shape=circle, label="10"]; - n_2 [id="9", shape=circle, label="9"]; - n_3 [id="8", shape=circle, label="8"]; - n_4 [id="1", shape=circle, label="1"]; - n_0 -> n_4 [arrowhead=none]; - n_5 [id="7", shape=circle, label="4"]; - n_6 [id="16", shape=circle, label="7"]; - n_7 [id="4", shape=circle, label="3"]; - n_8 [id="6", shape=doublecircle, label="9"]; - n_9 [id="3", shape=circle, label="5"]; - n_10 [id="12", shape=circle, label="6"]; - n_11 [id="2", shape=circle, label="2"]; - n_12 [id="10", shape=circle, label="11"]; + n_1 [id="8", shape=circle, label="5"]; + n_2 [id="1", shape=circle, label="1"]; + n_0 -> n_2 [arrowhead=none]; + n_3 [id="4", shape=circle, label="6"]; + n_4 [id="6", shape=doublecircle, label="8"]; + n_5 [id="3", shape=circle, label="3"]; + n_6 [id="2", shape=circle, label="2"]; + n_7 [id="10", shape=circle, label="4"]; + n_8 [id="5", shape=circle, label="7"]; - n_6 -> n_1 [id="[$e|10]", label="customer/0.0→store/0.0:buy"]; - n_3 -> n_8 [id="[$e|21]", label="store/0.0→customer/0.0:accepted"]; - n_1 -> n_12 [id="[$e|11]", label="customer/0.0→store/0.0:payment"]; - n_3 -> n_9 [id="[$e|16]", label="store/0.0→customer/0.0:reject"]; - n_12 -> n_8 [id="[$e|25]", label="store/0.0→customer/0.0:accepted"]; - n_2 -> n_9 [id="[$e|23]", label="customer/0.0→store/0.0:buy"]; - n_5 -> n_9 [id="[$e|24]", label="customer/0.0→store/0.0:buy"]; - n_4 -> n_11 [id="[$e|7]", label="main/0.0Δstore/0.0 args nil"]; - n_5 -> n_10 [id="[$e|12]", label="customer/0.0→store/0.0:more"]; - n_12 -> n_1 [id="[$e|22]", label="store/0.0→customer/0.0:reject"]; - n_11 -> n_7 [id="[$e|27]", label="main/0.0Δcustomer/0.0 args nil"]; - n_9 -> n_3 [id="[$e|17]", label="customer/0.0→store/0.0:payment"]; - n_10 -> n_6 [id="[$e|2]", label="customer/0.0→store/0.0:item"]; - n_7 -> n_5 [id="[$e|14]", label="customer/0.0→store/0.0:item"]; - n_2 -> n_7 [id="[$e|28]", label="customer/0.0→store/0.0:more"]; - n_2 -> n_7 [id="[$e|18]", label="customer/0.0→store/0.0:more"]; + n_1 -> n_7 [id="[$e|17]", label="customer/0.0→store/0.0:item"]; + n_8 -> n_3 [id="[$e|18]", label="store/0.0→customer/0.0:reject"]; + n_3 -> n_8 [id="[$e|14]", label="customer/0.0→store/0.0:payment"]; + n_7 -> n_3 [id="[$e|5]", label="customer/0.0→store/0.0:buy"]; + n_6 -> n_5 [id="[$e|11]", label="main/0.0Δcustomer/0.0 args nil"]; + n_8 -> n_4 [id="[$e|4]", label="store/0.0→customer/0.0:accepted"]; + n_7 -> n_1 [id="[$e|9]", label="customer/0.0→store/0.0:more"]; + n_2 -> n_6 [id="[$e|6]", label="main/0.0Δstore/0.0 args nil"]; + n_5 -> n_7 [id="[$e|16]", label="customer/0.0→store/0.0:item"]; + n_5 -> n_7 [id="[$e|13]", label="customer/0.0→store/0.0:item"]; + n_7 -> n_1 [id="[$e|15]", label="customer/0.0→store/0.0:more"]; } diff --git a/examples/customer/main_0_local_view.dot b/examples/customer/main_0_local_view.dot index 52ec045..d71f97f 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="3", shape=doublecircle, label="3"]; n_3 [id="2", shape=circle, label="2"]; - n_1 -> n_3 [id="[$e|1]", label="spawn store/0.0 args nil"]; n_3 -> n_2 [id="[$e|0]", label="spawn customer/0.0 args nil"]; + n_1 -> n_3 [id="[$e|1]", label="spawn store/0.0 args nil"]; } diff --git a/examples/customer/store_0_local_view.dot b/examples/customer/store_0_local_view.dot index 2fa20be..22c43ee 100644 --- a/examples/customer/store_0_local_view.dot +++ b/examples/customer/store_0_local_view.dot @@ -8,10 +8,10 @@ digraph store_0 { n_4 [id="3", shape=circle, label="3"]; n_5 [id="2", shape=doublecircle, label="5"]; - n_4 -> n_3 [id="[$e|3]", label="0#receive payment"]; - n_1 -> n_2 [id="[$e|1]", label="0#receive item"]; n_3 -> n_4 [id="[$e|9]", label="customer/0.0 ! reject"]; - n_2 -> n_4 [id="[$e|0]", label="0#receive buy"]; n_3 -> n_5 [id="[$e|6]", label="customer/0.0 ! accepted"]; + n_2 -> n_4 [id="[$e|0]", label="0#receive buy"]; + n_4 -> n_3 [id="[$e|3]", label="0#receive payment"]; n_2 -> n_1 [id="[$e|8]", label="1#receive more"]; + n_1 -> n_2 [id="[$e|1]", label="0#receive item"]; } diff --git a/src/choreography/gv.erl b/src/choreography/gv.erl index 5ecdbb1..471df94 100644 --- a/src/choreography/gv.erl +++ b/src/choreography/gv.erl @@ -833,21 +833,16 @@ create_gv_state(ProcPid, Proc1, V2, Proc2, PV2) -> ?UNDEFINED -> AccList; Data -> - MessageQueue = Data#actor_info.message_queue, EL = - case Name of - Proc1 -> - {_, L} = digraph:vertex(Graph, V2), - % {Proc1, share:if_final_get_n(L)}; - {Proc1, share:if_final_get_n(L), sets:from_list(MessageQueue)}; - Proc2 -> - {_, L} = digraph:vertex(Graph, PV2), - % {Proc2, share:if_final_get_n(L)}; - {Proc1, share:if_final_get_n(L), sets:from_list(MessageQueue)}; - N -> - {_, L} = digraph:vertex(Graph, Data#actor_info.current_state), - % {N, share:if_final_get_n(L)} - {N, share:if_final_get_n(L), sets:from_list(MessageQueue)} + case settings:get(gstate) of + true -> + state_with_previous_messages( + Data, Graph, Name, Proc1, Proc2, V2, PV2 + ); + false -> + state_without_previous_messages( + Data, Graph, Name, Proc1, Proc2, V2, PV2 + ) end, sets:add_element(EL, AccList) end @@ -856,6 +851,33 @@ create_gv_state(ProcPid, Proc1, V2, Proc2, PV2) -> ProcPid ). +state_with_previous_messages(Data, Graph, Name, Proc1, Proc2, V2, PV2) -> + MessageQueue = Data#actor_info.message_queue, + case Name of + Proc1 -> + {_, L} = digraph:vertex(Graph, V2), + {Proc1, share:if_final_get_n(L), sets:from_list(MessageQueue)}; + Proc2 -> + {_, L} = digraph:vertex(Graph, PV2), + {Proc1, share:if_final_get_n(L), sets:from_list(MessageQueue)}; + N -> + {_, L} = digraph:vertex(Graph, Data#actor_info.current_state), + {N, share:if_final_get_n(L), sets:from_list(MessageQueue)} + end. + +state_without_previous_messages(Data, Graph, Name, Proc1, Proc2, V2, PV2) -> + case Name of + Proc1 -> + {_, L} = digraph:vertex(Graph, V2), + {Proc1, share:if_final_get_n(L)}; + Proc2 -> + {_, L} = digraph:vertex(Graph, PV2), + {Proc2, share:if_final_get_n(L)}; + N -> + {_, L} = digraph:vertex(Graph, Data#actor_info.current_state), + {N, share:if_final_get_n(L)} + end. + check_if_exist(StateM, AggregateGlobalState) -> maps:fold( fun(Key, Value, Acc) -> diff --git a/src/chorer.erl b/src/chorer.erl index 804eaab..8041d04 100644 --- a/src/chorer.erl +++ b/src/chorer.erl @@ -9,12 +9,13 @@ -module(chorer). -include("share/common_data.hrl"). --define(DEFOUTPUT, "."). +-define(DEFOUTPUT, "./"). -define(DEFMINL, true). -define(DEFMING, false). +-define(DEFGSTATE, true). %%% API --export([main/1, generate/2, generate/5]). +-export([main/1, generate/2, generate/6]). %%%=================================================================== %%% API @@ -36,17 +37,23 @@ cli() -> default => ?DEFOUTPUT, help => "Output directory for the generated dot files" }, - #{ - name => minl, - type => boolean, - default => ?DEFMINL, - help => "Minimize the localviews" - }, #{ name => ming, type => boolean, default => ?DEFMING, help => "Minimize the globalviews" + }, + #{ + name => gstate, + type => boolean, + default => ?DEFGSTATE, + help => "Global state are formed with previous messages" + }, + #{ + name => minl, + type => boolean, + default => ?DEFMINL, + help => "Minimize the localviews" } ], help => "Extract a choreography automata of an Erlang program.", @@ -56,11 +63,12 @@ cli() -> input := InputFile, entrypoint := EntryPoint, output := OutputDir, - minl := MinL, - ming := MinG + ming := MinG, + gstate := GState, + minl := MinL } ) -> - generate(InputFile, EntryPoint, OutputDir, MinL, MinG) + generate(InputFile, EntryPoint, OutputDir, MinG, GState, MinL) end }. @@ -70,20 +78,21 @@ cli() -> InputFile :: string(), EntryPoint :: atom(). generate(InputFile, EntryPoint) -> - generate(InputFile, EntryPoint, ?DEFOUTPUT, ?DEFMINL, ?DEFMINL). + generate(InputFile, EntryPoint, ?DEFOUTPUT, ?DEFMINL, ?DEFMINL, ?DEFGSTATE). %%% @doc %%% Generate the localviews and the globalview specifing the output directory. %%% It initialize the ets tables and generates the localviews and globalview. --spec generate(InputFile, EntryPoint, OutDir, MinL, MinG) -> atom() when +-spec generate(InputFile, EntryPoint, OutDir, MinG, GState, MinL) -> atom() when InputFile :: string(), EntryPoint :: atom(), OutDir :: string(), - MinL :: boolean(), - MinG :: boolean(). -generate(InputFile, EntryPoint, OutDir, MinL, MinG) -> + MinG :: boolean(), + GState :: boolean(), + MinL :: boolean(). +generate(InputFile, EntryPoint, OutDir, MinG, GState, MinL) -> io:fwrite("Analysing ~p, entrypoint: ~p, output: ~p~n", [InputFile, EntryPoint, OutDir]), - Settings = settings:new_settings(InputFile, EntryPoint, OutDir, MinL, MinG), + Settings = settings:new_settings(InputFile, EntryPoint, OutDir, MinL, MinG, GState), db:init(Settings), md:extract(), NoError = lv:generate(), diff --git a/src/share/settings.erl b/src/share/settings.erl index 0f25040..e5c91c9 100644 --- a/src/share/settings.erl +++ b/src/share/settings.erl @@ -9,7 +9,7 @@ %%% API -export([ new_settings/2, - new_settings/5, + new_settings/6, get/1 ]). @@ -22,6 +22,7 @@ % optional minimizeLocal = false, minimizeGlobal = false, + gstate = true, output_dir = "./", %%% not in input more_info_lv = false, @@ -39,13 +40,14 @@ new_settings(InputFile, EntryPoint) -> %%% @doc %%% Create a new seggings record with some optional data. -new_settings(InputFile, EntryPoint, OutDir, MinimizeL, MinimizeG) -> +new_settings(InputFile, EntryPoint, OutDir, MinimizeL, MinimizeG, GState) -> #setting{ inputfile = InputFile, entrypoint = EntryPoint, output_dir = OutDir, minimizeLocal = MinimizeL, - minimizeGlobal = MinimizeG + minimizeGlobal = MinimizeG, + gstate = GState }. %%% @doc @@ -61,6 +63,7 @@ get(What) -> output_dir -> Settings#setting.output_dir; more_info_lv -> Settings#setting.more_info_lv; save_all -> Settings#setting.save_all; + gstate -> Settings#setting.gstate; _ -> not_valid end. diff --git a/test.py b/test.py index c40b99a..3cb25e3 100755 --- a/test.py +++ b/test.py @@ -2,33 +2,34 @@ import os # import time +# default: minimize global views test_list = [ - ("./examples/account/account.erl", "main/0", "examples/account", "true", "true"), - ("./examples/dining/dining.erl", "main/0", "examples/dining", "true", "true"), - ("./examples/hello/hello.erl", "main/0", "examples/hello", "true", "true"), - ("./examples/async/simple.erl","main/0","examples/async", "true", "true"), - ("./examples/ticktackstop/tictacstop.erl","start/0","examples/ticktackstop", "true", "true"), - ("./examples/ticktackloop/tictacloop.erl","start/0","examples/ticktackloop", "true", "true"), - ("./examples/customer/customer.erl","main/0","examples/customer", "true", "true"), - ("./examples/serverclient/serverclient.erl","main/0","examples/serverclient", "true", "true"), - ("./examples/trick/trick.erl","main/0","examples/trick", "true", "true"), - ("./examples/airline/airline.erl","main/0","examples/airline", "true", "true"), - ("./examples/conditional-case/conditional_case.erl","main/0","examples/conditional-case", "true", "true"), - ("./examples/for-loop-recursion/forloop.erl","main/0","examples/for-loop-recursion", "true", "true"), - ("./examples/function-call/funny.erl","main/0","examples/function-call", "true", "true"), - ("./examples/high-order-fun/hof.erl","greet/0","examples/high-order-fun", "true", "true"), - ("./examples/if-cases/ifcases.erl","main/0","examples/if-cases", "true", "true"), - ("./examples/test/foo1/foo1.erl","test/0","examples/test/foo1", "true", "true"), - ("./examples/test/foo2/foo2.erl","test/0","examples/test/foo2", "true", "true"), - ("./examples/test/foo3/foo3.erl","test/0","examples/test/foo3", "true", "true"), - ("./examples/test/foo4/foo4.erl","test/0","examples/test/foo4", "true", "true"), - ("./examples/test/foo5/foo5.erl","test/0","examples/test/foo5", "true", "true"), - ("./examples/test/foo6/foo6.erl","test/0","examples/test/foo6", "true", "true"), - ("./examples/test/ping/ping.erl","start/0","examples/test/ping", "true", "true"), - ("./examples/cauder_suite/airline/airline.erl","main/0","examples/cauder_suite/airline", "true", "true"), - # ("./examples/cauder_suite/barber/barber.erl","main/0","examples/cauder_suite/barber", "true", "true"), - ("./examples/cauder_suite/meViolation/meViolation.erl","main/0","examples/cauder_suite/meViolation", "true", "true"), - ("./examples/cauder_suite/purchase/purchase.erl","main/0","examples/cauder_suite/purchase", "true", "true"), + ("./examples/account/account.erl", "main/0", "examples/account", "true"), + ("./examples/dining/dining.erl", "main/0", "examples/dining", "true"), + ("./examples/hello/hello.erl", "main/0", "examples/hello", "true"), + ("./examples/async/simple.erl","main/0","examples/async", "true"), + ("./examples/ticktackstop/tictacstop.erl","start/0","examples/ticktackstop", "true"), + ("./examples/ticktackloop/tictacloop.erl","start/0","examples/ticktackloop", "true"), + ("./examples/customer/customer.erl","main/0","examples/customer", "true"), + ("./examples/serverclient/serverclient.erl","main/0","examples/serverclient", "true"), + ("./examples/trick/trick.erl","main/0","examples/trick", "true"), + ("./examples/airline/airline.erl","main/0","examples/airline", "true"), + ("./examples/conditional-case/conditional_case.erl","main/0","examples/conditional-case", "true"), + ("./examples/for-loop-recursion/forloop.erl","main/0","examples/for-loop-recursion", "true"), + ("./examples/function-call/funny.erl","main/0","examples/function-call", "true"), + ("./examples/high-order-fun/hof.erl","greet/0","examples/high-order-fun", "true"), + ("./examples/if-cases/ifcases.erl","main/0","examples/if-cases", "true"), + ("./examples/test/foo1/foo1.erl","test/0","examples/test/foo1", "true"), + ("./examples/test/foo2/foo2.erl","test/0","examples/test/foo2", "true"), + ("./examples/test/foo3/foo3.erl","test/0","examples/test/foo3", "true"), + ("./examples/test/foo4/foo4.erl","test/0","examples/test/foo4", "true"), + ("./examples/test/foo5/foo5.erl","test/0","examples/test/foo5", "true"), + ("./examples/test/foo6/foo6.erl","test/0","examples/test/foo6", "true"), + ("./examples/test/ping/ping.erl","start/0","examples/test/ping", "true"), + ("./examples/cauder_suite/airline/airline.erl","main/0","examples/cauder_suite/airline", "true"), + # ("./examples/cauder_suite/barber/barber.erl","main/0","examples/cauder_suite/barber", "true"), + ("./examples/cauder_suite/meViolation/meViolation.erl","main/0","examples/cauder_suite/meViolation", "true"), + ("./examples/cauder_suite/purchase/purchase.erl","main/0","examples/cauder_suite/purchase", "true"), ] os.system("rebar3 escriptize")