Test bigger topologies

test/coloring/Makefile

-TOPOLOGY ?= clique3
+TOPOLOGY ?= clique4
 DOT2LUSFLAGS ?=
 SASA_ALGOS := p.ml
 SASAFLAGS += --locally-central-daemon

test/coloring/clique3.dot → test/coloring/clique4.dot

 graph graph0 {
-graph [min_deg=2 mean_deg=2. max_deg=2 is_connected=true is_cyclic=true is_tree=false links_number=3]
+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
 }
 

test/token/ring8_oracle.lus → test/coloring/clique4_oracle.lus

-include "ring8.lus"
+include "clique4.lus"
 include "verify.lus"
 
-node topology = ring8;
+node topology = clique4;
 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)
+	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;
@@ -17,10 +17,10 @@ var
 	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 ];
+	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;
+tel

test/token/ring8.dot → test/token/ring4.dot

 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
 }
 

test/coloring/clique3_oracle.lus → test/token/ring4_oracle.lus

-include "clique3.lus"
+include "ring4.lus"
 include "verify.lus"
 
-node topology = clique3;
+node topology = ring4;
 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)
+	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;
@@ -17,10 +17,10 @@ var
 	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 ];
+	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
+tel;