Fix daemon predicates

lib/sas.lus

 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;

test/coloring/Makefile

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

test/coloring/verify.lus

 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;

test/token/Makefile

-TOPOLOGY ?= ring4
+TOPOLOGY ?= ring3
 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

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