WIP: trying to debug a fake ring proof

test/token/Makefile

-TOPOLOGY ?= ring8
+TOPOLOGY ?= ring4
 DOT2LUSFLAGS ?=
 SASA_ALGOS := p.ml root.ml
 

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=4]
+  p0 [algo="root.ml"]
+  p1 [algo="p.ml"]
+  p2 [algo="p.ml"]
+  p3 [algo="p.ml"]
+
+
+  p0 -> p1
+  p1 -> p2
+  p2 -> p3
+  p3 -> p0
+}
+

test/token/ring4_oracle.lus

+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;

test/token/verify.lus

@@ -24,5 +24,5 @@ let
 	steps = (-1 -> pre(steps)) + 1;
 	ok = closure and
 	     tokens >= 1 and -- there always exists at least one token holder
-	     ((steps >= card*(card-1) + ((card-4)*(card+1)/2) + 1) => legitimate); -- worst-case stabilization
+	     ((steps >= 4) => legitimate); -- worst-case stabilization
 tel;