Skip to content
Snippets Groups Projects
Commit 3b40afa0 authored by erwan's avatar erwan
Browse files

test: add the ring-orientation in the test suite

nb : it currently fails as the legitimate predicate is wrong.
parent a38d4757
No related branches found
No related tags found
No related merge requests found
...@@ -20,6 +20,7 @@ test: ...@@ -20,6 +20,7 @@ test:
cd k-clustering/ && make test cd k-clustering/ && make test
cd ghosh/ && make test cd ghosh/ && make test
cd wolfram-cellular-automaton/ && make test cd wolfram-cellular-automaton/ && make test
cd ring-orientation/ && make test
echo "Every test went fine!" echo "Every test went fine!"
clean: clean:
...@@ -44,6 +45,7 @@ clean: ...@@ -44,6 +45,7 @@ clean:
cd k-clustering/ && make clean cd k-clustering/ && make clean
cd ghosh/ && make clean cd ghosh/ && make clean
cd wolfram-cellular-automaton/ && make clean cd wolfram-cellular-automaton/ && make clean
cd ring-orientation/ && make clean
utest: utest:
cd skeleton/ && make test cd skeleton/ && make test
...@@ -66,5 +68,6 @@ utest: ...@@ -66,5 +68,6 @@ utest:
cd k-clustering/ && make utest cd k-clustering/ && make utest
cd ghosh/ && make utest cd ghosh/ && make utest
cd wolfram-cellular-automaton/ && make utest cd wolfram-cellular-automaton/ && make utest
cd ring-orientation/ && make utest
-include Makefile.untracked -include Makefile.untracked
# 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" DECO_PATTERN="0-:p.ml"
-include ./Makefile.dot -include ./Makefile.dot
...@@ -7,17 +7,23 @@ DECO_PATTERN="0-:p.ml" ...@@ -7,17 +7,23 @@ DECO_PATTERN="0-:p.ml"
############################################################################## ##############################################################################
# Non-regression tests # 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) # update golden-master tests (if necessary)
utest: 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 # Other examples of use
rdbg: grid5.dot grid5.ml rdbg: ring5.dot ring5.ml
rdbg --sasa -sut "sasa grid5.dot" rdbg --sasa -sut "sasa ring5.dot"
clean: genclean clean: genclean
rm -f grid*.* diring*.* clique*.* er*.*
-- 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
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment