From b272e987445f9a25c777e345a6412d7f46b583e6 Mon Sep 17 00:00:00 2001
From: "Gabriel B. Sant'Anna" <baiocchi.gabriel@gmail.com>
Date: Mon, 26 Apr 2021 14:58:19 +0200
Subject: [PATCH] WIP: trying to debug a fake ring proof
---
test/token/Makefile | 2 +-
test/token/ring4.dot | 14 ++++++++++++++
test/token/ring4_oracle.lus | 26 ++++++++++++++++++++++++++
test/token/verify.lus | 2 +-
4 files changed, 42 insertions(+), 2 deletions(-)
create mode 100644 test/token/ring4.dot
create mode 100644 test/token/ring4_oracle.lus
diff --git a/test/token/Makefile b/test/token/Makefile
index ee04475b..cd08a78b 100644
--- a/test/token/Makefile
+++ b/test/token/Makefile
@@ -1,4 +1,4 @@
-TOPOLOGY ?= ring8
+TOPOLOGY ?= ring4
DOT2LUSFLAGS ?=
SASA_ALGOS := p.ml root.ml
diff --git a/test/token/ring4.dot b/test/token/ring4.dot
new file mode 100644
index 00000000..3b05c113
--- /dev/null
+++ b/test/token/ring4.dot
@@ -0,0 +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=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
+}
+
diff --git a/test/token/ring4_oracle.lus b/test/token/ring4_oracle.lus
new file mode 100644
index 00000000..794c50d6
--- /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/verify.lus b/test/token/verify.lus
index 53d11a68..27898491 100644
--- a/test/token/verify.lus
+++ b/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;
--
GitLab