diff --git a/test/coloring/Makefile b/test/coloring/Makefile index e5ff2de8a14934839d66eb0bc0fdf6afd77fd0b8..de7c523940e18e7f84424f3b76295a272f4ff297 100644 --- a/test/coloring/Makefile +++ b/test/coloring/Makefile @@ -1,4 +1,4 @@ -TOPOLOGY ?= clique3 +TOPOLOGY ?= clique4 DOT2LUSFLAGS ?= SASA_ALGOS := p.ml SASAFLAGS += --locally-central-daemon diff --git a/test/coloring/clique3.dot b/test/coloring/clique3.dot deleted file mode 100644 index 8a1d3fce7b272fe13680d975e3d8a89694c6f2e8..0000000000000000000000000000000000000000 --- a/test/coloring/clique3.dot +++ /dev/null @@ -1,11 +0,0 @@ -graph graph0 { -graph [min_deg=2 mean_deg=2. max_deg=2 is_connected=true is_cyclic=true is_tree=false links_number=3] - p0 [algo="p.ml"] - p1 [algo="p.ml"] - p2 [algo="p.ml"] - - p0 -- p1 - p0 -- p2 - p1 -- p2 -} - diff --git a/test/coloring/clique3_oracle.lus b/test/coloring/clique3_oracle.lus deleted file mode 100644 index 42222151ac27b36aa6585a2c26ba1db5b7072bc5..0000000000000000000000000000000000000000 --- a/test/coloring/clique3_oracle.lus +++ /dev/null @@ -1,26 +0,0 @@ -include "clique3.lus" -include "verify.lus" - -node topology = clique3; -const an = actions_number; -const pn = card; - -node oracle( - p0_color:int;p1_color:int;p2_color:int; - Enab_p0_recolor,Enab_p1_recolor,Enab_p2_recolor:bool; - p0_recolor,p1_recolor,p2_recolor:bool) -returns (ok:bool); -var - Acti:bool^an^pn; - Enab:bool^an^pn; - Stat : state^pn; - nodes : state^pn; - enables : bool^an^pn; -let - Acti = [[p0_recolor],[p1_recolor],[p2_recolor]]; - Enab = [[Enab_p0_recolor],[Enab_p1_recolor],[Enab_p2_recolor]]; - Stat = [ p0_color, p1_color, p2_color ]; - - nodes, enables = topology(pre(Acti), Stat); - ok = enables = Enab and boolred<<pn,pn,pn>>(map<<=,pn>>(nodes, Stat)); -tel diff --git a/test/coloring/clique4.dot b/test/coloring/clique4.dot new file mode 100644 index 0000000000000000000000000000000000000000..9509c80474fab2fdea2f2237f6992631cb387414 --- /dev/null +++ b/test/coloring/clique4.dot @@ -0,0 +1,15 @@ +graph graph0 { +graph [min_deg=3 mean_deg=3. max_deg=3 is_connected=true is_cyclic=true is_tree=false links_number=6] + p0 [algo="p.ml"] + p1 [algo="p.ml"] + p2 [algo="p.ml"] + p3 [algo="p.ml"] + + p0 -- p1 + p0 -- p2 + p0 -- p3 + p1 -- p2 + p1 -- p3 + p2 -- p3 +} + diff --git a/test/coloring/clique4_oracle.lus b/test/coloring/clique4_oracle.lus new file mode 100644 index 0000000000000000000000000000000000000000..1cd6e7bfc724e20efc5604275985b90666fee4d7 --- /dev/null +++ b/test/coloring/clique4_oracle.lus @@ -0,0 +1,26 @@ +include "clique4.lus" +include "verify.lus" + +node topology = clique4; +const an = actions_number; +const pn = card; + +node oracle( + p0_color:int;p1_color:int;p2_color:int;p3_color:int; + Enab_p0_recolor,Enab_p1_recolor,Enab_p2_recolor,Enab_p3_recolor:bool; + p0_recolor,p1_recolor,p2_recolor,p3_recolor:bool) +returns (ok:bool); +var + Acti:bool^an^pn; + Enab:bool^an^pn; + Stat : state^pn; + nodes : state^pn; + enables : bool^an^pn; +let + Acti = [[p0_recolor],[p1_recolor],[p2_recolor],[p3_recolor]]; + Enab = [[Enab_p0_recolor],[Enab_p1_recolor],[Enab_p2_recolor],[Enab_p3_recolor]]; + Stat = [ p0_color, p1_color, p2_color, p3_color ]; + + nodes, enables = topology(pre(Acti), Stat); + ok = enables = Enab and boolred<<pn,pn,pn>>(map<<=,pn>>(nodes, Stat)); +tel diff --git a/test/token/ring8.dot b/test/token/ring4.dot similarity index 53% rename from test/token/ring8.dot rename to test/token/ring4.dot index d32cc6ef38c43e69bb297e306c9412be248e4d7b..3b05c11306fc9b3129609f600aff38d976d69ded 100644 --- a/test/token/ring8.dot +++ b/test/token/ring4.dot @@ -1,22 +1,14 @@ digraph graph0 { -graph [min_deg=2 mean_deg=2. max_deg=2 is_connected=true is_cyclic=true is_tree=false links_number=8] +graph [min_deg=2 mean_deg=2. max_deg=2 is_connected=true is_cyclic=true is_tree=false links_number=4] p0 [algo="root.ml"] p1 [algo="p.ml"] p2 [algo="p.ml"] p3 [algo="p.ml"] - p4 [algo="p.ml"] - p5 [algo="p.ml"] - p6 [algo="p.ml"] - p7 [algo="p.ml"] p0 -> p1 p1 -> p2 p2 -> p3 - p3 -> p4 - p4 -> p5 - p5 -> p6 - p6 -> p7 - p7 -> p0 + p3 -> p0 } diff --git a/test/token/ring4_oracle.lus b/test/token/ring4_oracle.lus new file mode 100644 index 0000000000000000000000000000000000000000..794c50d6d31d0c8023faba7e79f66ba60bf34b09 --- /dev/null +++ b/test/token/ring4_oracle.lus @@ -0,0 +1,26 @@ +include "ring4.lus" +include "verify.lus" + +node topology = ring4; +const an = actions_number; +const pn = card; + +node oracle( + p0_c:int;p1_c:int;p2_c:int;p3_c:int; + Enab_p0_T,Enab_p1_T,Enab_p2_T,Enab_p3_T:bool; + p0_T,p1_T,p2_T,p3_T:bool) +returns (ok:bool); +var + Acti:bool^an^pn; + Enab:bool^an^pn; + Stat : state^pn; + nodes : state^pn; + enables : bool^an^pn; +let + Acti = [[p0_T],[p1_T],[p2_T],[p3_T]]; + Enab = [[Enab_p0_T],[Enab_p1_T],[Enab_p2_T],[Enab_p3_T]]; + Stat = [ p0_c, p1_c, p2_c, p3_c ]; + + nodes, enables = topology(pre(Acti), Stat); + ok = enables = Enab and boolred<<pn,pn,pn>>(map<<=,pn>>(nodes, Stat)); +tel; diff --git a/test/token/ring8_oracle.lus b/test/token/ring8_oracle.lus deleted file mode 100644 index 158cf1f8c24d2747bb9171c30d7623aabddc89ee..0000000000000000000000000000000000000000 --- a/test/token/ring8_oracle.lus +++ /dev/null @@ -1,26 +0,0 @@ -include "ring8.lus" -include "verify.lus" - -node topology = ring8; -const an = actions_number; -const pn = card; - -node oracle( - p0_c:int;p1_c:int;p2_c:int;p3_c:int;p4_c:int;p5_c:int;p6_c:int;p7_c:int; - Enab_p0_T,Enab_p1_T,Enab_p2_T,Enab_p3_T,Enab_p4_T,Enab_p5_T,Enab_p6_T,Enab_p7_T:bool; - p0_T,p1_T,p2_T,p3_T,p4_T,p5_T,p6_T,p7_T:bool) -returns (ok:bool); -var - Acti:bool^an^pn; - Enab:bool^an^pn; - Stat : state^pn; - nodes : state^pn; - enables : bool^an^pn; -let - Acti = [[p0_T],[p1_T],[p2_T],[p3_T],[p4_T],[p5_T],[p6_T],[p7_T]]; - Enab = [[Enab_p0_T],[Enab_p1_T],[Enab_p2_T],[Enab_p3_T],[Enab_p4_T],[Enab_p5_T],[Enab_p6_T],[Enab_p7_T]]; - Stat = [ p0_c, p1_c, p2_c, p3_c, p4_c, p5_c, p6_c, p7_c ]; - - nodes, enables = topology(pre(Acti), Stat); - ok = enables = Enab and boolred<<pn,pn,pn>>(map<<=,pn>>(nodes, Stat)); -tel;