diff --git a/test/Makefile b/test/Makefile index 599c4245b0500e862ba5a12e43f5794b20d51a6d..307c298bfb9020d52435f26d8c2fb78a4d324754 100644 --- a/test/Makefile +++ b/test/Makefile @@ -20,6 +20,7 @@ test: cd k-clustering/ && make test cd ghosh/ && make test cd wolfram-cellular-automaton/ && make test + cd ring-orientation/ && make test echo "Every test went fine!" clean: @@ -44,6 +45,7 @@ clean: cd k-clustering/ && make clean cd ghosh/ && make clean cd wolfram-cellular-automaton/ && make clean + cd ring-orientation/ && make clean utest: cd skeleton/ && make test @@ -66,5 +68,6 @@ utest: cd k-clustering/ && make utest cd ghosh/ && make utest cd wolfram-cellular-automaton/ && make utest + cd ring-orientation/ && make utest -include Makefile.untracked diff --git a/test/ring-orientation/Makefile b/test/ring-orientation/Makefile index c6838f11868a57e32802bbf65e95ed9fe490c1ba..fe95b2839876f3f3c90df7c63e7b23570d8a75f1 100644 --- a/test/ring-orientation/Makefile +++ b/test/ring-orientation/Makefile @@ -1,4 +1,4 @@ -# Time-stamp: <modified the 21/06/2023 (at 12:04) by Erwan Jahier> +# Time-stamp: <modified the 18/10/2023 (at 16:06) by Erwan Jahier> DECO_PATTERN="0-:p.ml" -include ./Makefile.dot @@ -7,17 +7,23 @@ DECO_PATTERN="0-:p.ml" ############################################################################## # Non-regression tests -test: grid5.gm_test grid5.rdbg-test clean +test: ring5.gm_test ring5.rdbg-test lurette clean # update golden-master tests (if necessary) utest: - make grid5.ugm_test || echo "grid4 ok" + make ring5.ugm_test || echo "ring5.ugm_test ok" + +lurette: ring5.dot + lurette -o ring.rif -l 10000 \ + -sut "sasa -rif ring5.dot -cd" \ + -oracle "lv6 -2c-exec ring5_oracle.lus -n oracle" + + ############################################################################## # Other examples of use -rdbg: grid5.dot grid5.ml - rdbg --sasa -sut "sasa grid5.dot" +rdbg: ring5.dot ring5.ml + rdbg --sasa -sut "sasa ring5.dot" clean: genclean - rm -f grid*.* diring*.* clique*.* er*.* diff --git a/test/ring-orientation/ring_orientation_oracle.lus b/test/ring-orientation/ring_orientation_oracle.lus new file mode 100644 index 0000000000000000000000000000000000000000..8241f5cc9db2989e4e41e1931bfc6ebcfdcd0172 --- /dev/null +++ b/test/ring-orientation/ring_orientation_oracle.lus @@ -0,0 +1,26 @@ +-- include "../lustre/oracle_utils.lus" +include "../../salut/lib/utils.lus" + + +type state = { color_0 : bool ; phase_pos : bool ; orient_left : bool }; + +function to_state( color_0 : bool ; phase_pos : bool ; orient_left : bool ) +returns(res : state); +let + res = state { color_0 = color_0; phase_pos=phase_pos; orient_left=orient_left}; +tel; + + + +node ring_orientation_oracle<<const an:int; const pn:int>> +(legitimate:bool; Enab, Acti: bool^an^pn; Config:state^card ; round:bool; round_nb:int) +returns (ok:bool); +var + token_nb:int; converge_worst_case:bool; +let + + token_nb = count<<card>>(map<<nary_or<<an>>,pn>> (Enab)); + converge_worst_case = (round_nb >= pn*pn) => (token_nb = 1); + + ok = converge_worst_case; +tel