diff --git a/lib/sasacore/genOracle.ml b/lib/sasacore/genOracle.ml index f02599a00e6c021f2b68db827ed46c3f9d8d9b96..72d135566d4cebff3261754abbfd89f882b4a048 100644 --- a/lib/sasacore/genOracle.ml +++ b/lib/sasacore/genOracle.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 05/07/2019 (at 11:30) by Erwan Jahier> *) +(* Time-stamp: <modified the 05/07/2019 (at 15:25) by Erwan Jahier> *) open Process @@ -35,8 +35,8 @@ let (f: 'v Process.t list -> string) = Str.global_replace (Str.regexp "[-,\\.]") "_" algo in Printf.sprintf "%sinclude \"%s_oracle.lus\" -const n=%d; -const m=%d; +const an=%d; -- actions number +const pn=%d; -- processes number const degree=%d; const diameter=%d; @@ -44,12 +44,12 @@ node oracle(%s) returns (ok:bool); var %slet %s %s - ok = %s_oracle<<m,n>>(Enab,Acti); + ok = %s_oracle<<an,pn>>(Enab,Acti); tel " (Mypervasives.entete "--" SasaVersion.str SasaVersion.sha) algo - n m degree diameter + m n degree diameter input_decl array_decl array_def_acti diff --git a/test/Makefile.inc b/test/Makefile.inc index c04b14bba63f1b23d68d18381a0857662f3a0da2..bb7781da9ed4e821b1a03d9dec75652c2058f163 100644 --- a/test/Makefile.inc +++ b/test/Makefile.inc @@ -1,4 +1,4 @@ -# Time-stamp: <modified the 20/06/2019 (at 17:26) by Erwan Jahier> +# Time-stamp: <modified the 05/07/2019 (at 15:18) by Erwan Jahier> DIR=../../_build/install/default @@ -18,6 +18,9 @@ LIB=-package algo %.lut: %.dot $(sasa) -gld $^ +%_oracle.lus: %.dot + $(sasa) -glos $^ + %.rif: cmxs %.dot $(sasa) $(sasaopt) $*.dot -rif > $*.rif diff --git a/test/bfs-spanning-tree/Makefile b/test/bfs-spanning-tree/Makefile index f1cfbb4242be0e68ee94af09e4e23f7805f0df53..2b9bc3ad9255255487ce3faa194b8f9ac6032470 100644 --- a/test/bfs-spanning-tree/Makefile +++ b/test/bfs-spanning-tree/Makefile @@ -1,4 +1,4 @@ -# Time-stamp: <modified the 05/07/2019 (at 11:09) by Erwan Jahier> +# Time-stamp: <modified the 05/07/2019 (at 15:30) by Erwan Jahier> test: test0 test2 lurette0 lurette1 @@ -26,15 +26,14 @@ gnuplot: fig5.1-noinit.rif gnuplot2: fig5.2.rif gnuplot-rif $< -lurette0:cmxs fig5.1-noinit.lut +lurette0:cmxs fig5.1-noinit.lut fig5.1-noinit_oracle.lus lurette -o lurette.rif \ -env "$(sasa) fig5.1-noinit.dot -custd -rif" \ -sut "lutin fig5.1-noinit.lut -n distributed" -lurette1:cmxs fig5.1.lut +lurette1:cmxs fig5.1.lut fig5.1_oracle.lus rdbg -lurette -o lurette.rif \ - -env "$(sasa) fig5.1.dot -custd -rif" \ - -sut "lutin fig5.1.lut -n distributed" \ + -env "$(sasa) fig5.1.dot -dd -rif" \ -oracle "lv6 fig5.1_oracle.lus -n oracle" lurette: lurette0 @@ -61,3 +60,5 @@ manual:cmxs fig5.1-noinit.lut -include ../Makefile.inc +lclean: clean + rm fig*oracle.lus diff --git a/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus b/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus new file mode 100644 index 0000000000000000000000000000000000000000..bfaed4c4ca880802d3b34c71838fd278f148af07 --- /dev/null +++ b/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus @@ -0,0 +1,14 @@ + +include "round.lus" + +node bfs_spanning_tree_oracle<<const an:int; const pn:int>> (Enab, Acti: bool^an^pn) +returns (ok:bool); +var + Round, Silent:bool; + RoundNb:int; +let + Silent = silent<<an,pn>>(Enab); + Round = round <<an,pn>>(Enab,Acti); + RoundNb = count(Round); + ok = (RoundNb>=diameter+2) => Silent; -- from theorem 5.18 page 57 +tel diff --git a/test/bfs-spanning-tree/fig5.1-noinit_oracle.lus b/test/bfs-spanning-tree/fig5.1-noinit_oracle.lus deleted file mode 100644 index d1a7e83588b88254394caa3a1e28969b496692d3..0000000000000000000000000000000000000000 --- a/test/bfs-spanning-tree/fig5.1-noinit_oracle.lus +++ /dev/null @@ -1,31 +0,0 @@ - -include "round.lus" - -const n=8; -const m=2; -const degree=2; -const diameter=8; - -node oracle(root_CD,root_CP,p1_CD,p1_CP,p2_CD,p2_CP,p3_CD,p3_CP,p4_CD,p4_CP,p5_CD,p5_CP, - p6_CD,p6_CP,p7_CD,p7_CP, - Enab_root_CD,Enab_root_CP,Enab_p1_CD,Enab_p1_CP,Enab_p2_CD,Enab_p2_CP, - Enab_p3_CD,Enab_p3_CP,Enab_p4_CD,Enab_p4_CP,Enab_p5_CD,Enab_p5_CP, - Enab_p6_CD,Enab_p6_CP,Enab_p7_CD,Enab_p7_CP - :bool) -returns (ok,Round, Silent:bool; RoundNb:int); -var - Acti:bool^2^8; - Enab:bool^2^8; -let - Acti = [[root_CD,root_CP],[p1_CD,p1_CP],[p2_CD,p2_CP],[p3_CD,p3_CP],[p4_CD,p4_CP], - [p5_CD,p5_CP],[p6_CD,p6_CP],[p7_CD,p7_CP]]; - - Enab = [[Enab_root_CD,Enab_root_CP],[Enab_p1_CD,Enab_p1_CP],[Enab_p2_CD,Enab_p2_CP], - [Enab_p3_CD,Enab_p3_CP],[Enab_p4_CD,Enab_p4_CP],[Enab_p5_CD,Enab_p5_CP], - [Enab_p6_CD,Enab_p6_CP],[Enab_p7_CD,Enab_p7_CP]]; - - Round = round <<m,n>>(Enab,Acti); - RoundNb = count(Round); - Silent = silent<<m,n>>(Enab); - ok = (RoundNb>=diameter+2) => Silent; -- from theorem 5.18 page 57 -tel