From e8ba560afa5b9d7f2475e43b88c679080e169b99 Mon Sep 17 00:00:00 2001
From: "Gabriel B. Sant'Anna" <baiocchi.gabriel@gmail.com>
Date: Sun, 16 May 2021 20:46:58 +0200
Subject: [PATCH] Fix daemon predicates
---
lib/sas.lus | 51 +++++++++++++++++--------------------
test/coloring/Makefile | 2 +-
test/coloring/verify.lus | 15 ++++++-----
test/token/Makefile | 2 +-
test/token/ring4.dot | 14 ----------
test/token/ring4_oracle.lus | 26 -------------------
test/token/verify.lus | 13 +++++-----
7 files changed, 40 insertions(+), 83 deletions(-)
delete mode 100644 test/token/ring4.dot
delete mode 100644 test/token/ring4_oracle.lus
diff --git a/lib/sas.lus b/lib/sas.lus
index 304a99fb..f2b66164 100644
--- a/lib/sas.lus
+++ b/lib/sas.lus
@@ -1,37 +1,32 @@
include "utils.lus"
include "bitset.lus"
--- No nodes enabled.
+-- No nodes enabled, the network is silent.
function silent<<const an:int; const pn:int>>(enab: bool^an^pn)
returns (y : bool);
let
y = boolnone<<pn>>(map<<boolany<<an>>, pn>>(enab));
tel;
-node node_is_proper<<const an:int>>(acti, enab : bool^an) returns (y : bool);
-let
- y = true -> boolall<<an>>(map<<=>,an>>(acti, pre(enab)));
-tel;
-
-- Any activation Ai implies Ei was previously enabled.
-node daemon_is_proper<<const an:int; const pn:int>>(acti, enab : bool^an^pn)
-returns (y : bool);
+node activation_is_valid<<const an:int>>(acti, enab : bool^an) returns (y : bool);
let
- y = boolall<<pn>>(map<<node_is_proper,pn>>(acti, enab));
+ y = true -> boolall<<an>>(map<<=>,an>>(acti, pre(enab)));
tel;
-- |A| >= 1 for non-silent states.
-function daemon_is_distributed<<const an:int; const pn:int>>(acti, enab : bool^an^pn)
+node daemon_is_proper_distributed<<const an:int; const pn:int>>(acti, enab : bool^an^pn)
returns (y : bool);
let
- y = silent<<an,pn>>(enab) or
- boolred<<1,pn,pn>>(map<<boolany<<an>>, pn>>(acti));
+ y = boolall<<pn>>(map<<activation_is_valid<<an>>, pn>>(acti, enab))
+ and (silent<<an,pn>>(enab)
+ or boolred<<1,pn,pn>>(map<<boolany<<an>>, pn>>(acti)));
tel;
-- No two neighboring nodes are active at once.
-function daemon_is_locally_central<<const an:int; const pn:int>>(
- adjacency : bool^pn^pn;
- acti,enab : bool^an^pn
+node daemon_is_locally_central<<const an:int; const pn:int>>(
+ acti, enab : bool^an^pn;
+ adjacency : bool^pn^pn
) returns (y : bool);
var
active : bool ^ pn;
@@ -43,30 +38,32 @@ let
active_adjacencies = map<<inter<<pn>>, pn>>(active^pn, adjacency);
no_active_adjacencies = map<<boolnone<<pn>>, pn>>(active_adjacencies);
locally_central = map<<=>,pn>>(active, no_active_adjacencies);
- y = silent<<an,pn>>(enab) or
- (boolall<<pn>>(locally_central) and daemon_is_central<< an, pn >>(acti, enab));
+ y = daemon_is_proper_distributed<<an,pn>>(acti, enab)
+ and boolall<<pn>>(locally_central);
tel;
-
--- |A| = 1 for non-silent states.
-function daemon_is_central<<const an:int; const pn:int>>(acti,enab : bool^an^pn)
+-- At most one node is activated.
+node daemon_is_central<<const an:int; const pn:int>>(acti, enab : bool^an^pn)
returns (y : bool);
let
- y = silent<<an,pn>>(enab) or
- boolred<<1,1,pn>>(map<<boolany<<an>>, pn>>(acti));
+ y = daemon_is_proper_distributed<<an,pn>>(acti, enab)
+ and boolred<<1,1,pn>>(map<<boolany<<an>>, pn>>(acti));
tel;
--- |A| = n for non-silent states.
-function daemon_is_synchronous<<const an:int; const pn:int>>(acti, enab : bool^an^pn)
+-- All enabled nodes are activated.
+node daemon_is_synchronous<<const an:int; const pn:int>>(acti, enab : bool^an^pn)
returns (y:bool);
+var
+ enabled, active: bool ^ pn;
let
- y = silent<<an,pn>>(enab) or
- boolred<<pn,pn,pn>>(map<<boolany<<an>>, pn>>(acti));
+ enabled = map<<boolany<<an>>, pn>>(enab);
+ active = map<<boolany<<an>>, pn>>(acti);
+ y = daemon_is_proper_distributed<<an,pn>>(acti, enab) and active = enabled;
tel;
-- Measures time complexity in moves.
node move_count<<const an:int; const pn:int>>(acti : bool^an^pn)
returns (count:int);
let
- count = (0 -> pre(count)) + pop_count<<pn>>(map<<boolany<<an>>, pn>>(acti));
+ count = (-1 -> pre(count)) + pop_count<<pn>>(map<<boolany<<an>>, pn>>(acti));
tel;
diff --git a/test/coloring/Makefile b/test/coloring/Makefile
index e6bc54cd..e5ff2de8 100644
--- a/test/coloring/Makefile
+++ b/test/coloring/Makefile
@@ -1,4 +1,4 @@
-TOPOLOGY ?= dice5
+TOPOLOGY ?= clique3
DOT2LUSFLAGS ?=
SASA_ALGOS := p.ml
SASAFLAGS += --locally-central-daemon
diff --git a/test/coloring/verify.lus b/test/coloring/verify.lus
index 862084f3..82b21a96 100644
--- a/test/coloring/verify.lus
+++ b/test/coloring/verify.lus
@@ -1,13 +1,13 @@
include "../../lib/sas.lus"
-node verify(activations : bool^actions_number^card; inits : state^card)
-returns (ok : bool; legitimate, closure : bool; moves : int);
+node verify(activations : bool^actions_number^card; inits : state^card) returns (ok : bool);
var
nodes : state^card;
enables : bool^actions_number^card;
+ legitimate, closure : bool;
+ moves : int;
let
- assert(daemon_is_proper<<actions_number,card>>(activations, enables));
- assert(daemon_is_locally_central<<actions_number,card>>(adjacency, activations, enables));
+ assert(daemon_is_locally_central<<actions_number,card>>(activations, enables, adjacency));
nodes, enables = topology(activations, inits);
@@ -16,7 +16,8 @@ let
closure = true -> (pre(legitimate) => legitimate);
moves = move_count<<actions_number,card>>(activations);
- ok = closure and
- -- the execution terminates after at most |N|−1 moves
- ((moves >= card-1) => legitimate);
+ -- verify that the execution terminates after at most |N|−1 moves:
+ -- since we can't constrain the color domain (e.g., an initial state may
+ -- have values outside the [0,K) range), the upper bound is actually |N|
+ ok = closure and (moves >= card => legitimate);
tel;
diff --git a/test/token/Makefile b/test/token/Makefile
index cd08a78b..1450b750 100644
--- a/test/token/Makefile
+++ b/test/token/Makefile
@@ -1,4 +1,4 @@
-TOPOLOGY ?= ring4
+TOPOLOGY ?= ring3
DOT2LUSFLAGS ?=
SASA_ALGOS := p.ml root.ml
diff --git a/test/token/ring4.dot b/test/token/ring4.dot
deleted file mode 100644
index 3b05c113..00000000
--- a/test/token/ring4.dot
+++ /dev/null
@@ -1,14 +0,0 @@
-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
deleted file mode 100644
index 794c50d6..00000000
--- a/test/token/ring4_oracle.lus
+++ /dev/null
@@ -1,26 +0,0 @@
-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 ef363d2e..e0c1969c 100644
--- a/test/token/verify.lus
+++ b/test/token/verify.lus
@@ -6,11 +6,10 @@ var
nodes : state^card;
enables : bool^actions_number^card;
legitimate, closure : bool;
- tokens : int;
steps : int;
+ tokens : int;
let
- assert(daemon_is_proper<<actions_number,card>>(activations, enables));
- assert(daemon_is_distributed<<actions_number,card>>(activations, enables));
+ assert(daemon_is_proper_distributed<<actions_number,card>>(activations, enables));
nodes, enables = topology(activations, inits);
@@ -21,8 +20,8 @@ let
legitimate = tokens = 1;
closure = true -> (pre(legitimate) => legitimate);
- steps = (0 -> pre(steps)) + 1;
- ok = closure and
- tokens >= 1 and -- there always exists at least one token holder
- ((steps >= 4) => legitimate); -- worst-case stabilization
+ steps = (-1 -> pre(steps)) + 1;
+ ok = tokens >= 1 -- there should always be at least one token holder
+ and closure
+ and (steps >= 3*card*(card-1)/2 - card - 1 => legitimate); -- worst-case stabilization
tel;
--
GitLab