diff --git a/coloring/bitset.lus b/bitset.lus
similarity index 92%
rename from coloring/bitset.lus
rename to bitset.lus
index aa08e13a5c9590df6ea3f08abb023f58ce0e8ba1..36b6a029a5e89e73fcf5b075ee71b9950af4f018 100644
--- a/coloring/bitset.lus
+++ b/bitset.lus
@@ -8,7 +8,8 @@ include "utils.lus"
function one_hot<<const N:int>>(x : int) returns (s : bool^N);
let
assert(x >= 0 and x < N);
- s = map<<=,N>>(x^N, range<<N>>(true));
+ s = map<<=,N>>(x^N, range<<N>>());
+ assert(boolred<<1,1,N>>(s));
tel;
-- Returns the complement of a given bitset.
@@ -24,9 +25,9 @@ let
tel;
-- Tests whether a bitset is empty or not.
-function none<<const N:int>>(s : bool^N) returns (y : bool);
+function is_empty<<const N:int>>(s : bool^N) returns (y : bool);
let
- y = pop_count<<N>>(s) = 0;
+ y = boolred<<0,0,N>>(s);
tel;
-- Bitset union.
@@ -66,7 +67,7 @@ tel;
-- Test if two bitsets are disjoint.
function disjoint<<const N:int>>(a, b : bool^N) returns (y : bool);
let
- y = none<<N>>(inter<<N>>(a, b));
+ y = is_empty<<N>>(inter<<N>>(a, b));
tel;
-- Tests whether the bitset s1 is a subset of the bitset s2.
@@ -79,7 +80,8 @@ tel;
Builds bitset of size N from a list of M elements, where each element in the
list is treated as a bit position to be set to true in the resulting bitset.
*/
-function bitset_of_list<<const N:int; const M:int>>(list : int^M) returns (set : bool^N);
+function bitset_of_list<<const N:int; const M:int>>(list : int^M)
+returns (set : bool^N);
let
set = red<<set<<N>>,M>>(false^N, list);
tel;
diff --git a/coloring/dice5_oracle.lus b/coloring/dice5_oracle.lus
index 81a79b9df93e0051be7243dcf7582899ca18137b..dbce57dfd075d670b533adbb736b6ade0ebbeb14 100644
--- a/coloring/dice5_oracle.lus
+++ b/coloring/dice5_oracle.lus
@@ -7,8 +7,8 @@ const pn = card;
node oracle(
p0_color:int;p1_color:int;p2_color:int;p3_color:int;p4_color:int;
- Enab_p0_recolor,Enab_p0_noop,Enab_p1_recolor,Enab_p1_noop,Enab_p2_recolor,Enab_p2_noop,Enab_p3_recolor,Enab_p3_noop,Enab_p4_recolor,Enab_p4_noop:bool;
- p0_recolor,p0_noop,p1_recolor,p1_noop,p2_recolor,p2_noop,p3_recolor,p3_noop,p4_recolor,p4_noop:bool)
+ Enab_p0_recolor,Enab_p1_recolor,Enab_p2_recolor,Enab_p3_recolor,Enab_p4_recolor:bool;
+ p0_recolor,p1_recolor,p2_recolor,p3_recolor,p4_recolor:bool)
returns (ok:bool);
var
Acti:bool^an^pn;
@@ -17,8 +17,8 @@ var
nodes : state^pn;
enables : bool^an^pn;
let
- Acti = [[p0_recolor,p0_noop],[p1_recolor,p1_noop],[p2_recolor,p2_noop],[p3_recolor,p3_noop],[p4_recolor,p4_noop]];
- Enab = [[Enab_p0_recolor,Enab_p0_noop],[Enab_p1_recolor,Enab_p1_noop],[Enab_p2_recolor,Enab_p2_noop],[Enab_p3_recolor,Enab_p3_noop],[Enab_p4_recolor,Enab_p4_noop]];
+ Acti = [[p0_recolor],[p1_recolor],[p2_recolor],[p3_recolor],[p4_recolor]];
+ Enab = [[Enab_p0_recolor],[Enab_p1_recolor],[Enab_p2_recolor],[Enab_p3_recolor],[Enab_p4_recolor]];
Stat = [ p0_color, p1_color, p2_color, p3_color, p4_color ];
nodes, enables = topology(pre(Acti), Stat);
diff --git a/coloring/p.lus b/coloring/p.lus
index 7b69e1d2b728e5e64730029c81dab31bd85e718c..398e2852bd18576118d446c5a2dd5dda9af6fb59 100644
--- a/coloring/p.lus
+++ b/coloring/p.lus
@@ -1,14 +1,14 @@
-include "bitset.lus"
+include "../bitset.lus"
type state = int;
-type action = enum { recolor, noop };
-const actions_number = 2;
+type action = enum { recolor };
+const actions_number = 1;
function action_of_int(i : int) returns (a : action);
let
assert(i >= 0);
- a = if i = 0 then recolor else noop;
+ a = recolor;
tel;
const K = max_degree + 1;
@@ -18,13 +18,13 @@ returns (enabled : bool^actions_number);
var conflict : bool;
let
conflict = subset<<K>>(one_hot<<K>>(this), bitset_of_list<<K,degree>>(neighbors));
- enabled = [ conflict, not conflict ];
+ enabled = [ conflict ];
tel;
function p_step<<const degree:int>>(this : state; neighbors : state^degree; action : action)
returns (new : state);
let
- new = if action = noop then this
- else first_set<<K>>(diff<<K>>(true^K, bitset_of_list<<K,degree>>(neighbors)));
+ assert(action = recolor);
+ new = first_set<<K>>(diff<<K>>(true^K, bitset_of_list<<K,degree>>(neighbors)));
assert(new >= 0);
tel;
diff --git a/coloring/p.ml b/coloring/p.ml
index 869d9bf302851b08242b9ce702a04c298eec13a9..99f279cf999ede6245b4fb547ed53dcbd4ae8005 100644
--- a/coloring/p.ml
+++ b/coloring/p.ml
@@ -3,11 +3,11 @@ module ColorSet = Set.Make (Int)
type node = { color : State.t; neighbors : State.t list }
let color_count = Algo.max_degree() + 1
-let colors = List.init color_count (fun x -> x) |> ColorSet.of_list
+let all_colors = List.init color_count (fun x -> x) |> ColorSet.of_list
let conflict p = p.neighbors |> List.exists (fun qc -> qc = p.color)
let used p = ColorSet.of_list p.neighbors
-let free p = ColorSet.diff colors (used p)
+let free p = ColorSet.diff all_colors (used p)
let color p = ColorSet.min_elt (free p)
let init_state : State.t Algo.state_init_fun = fun n _ -> Random.int n
@@ -15,10 +15,9 @@ let init_state : State.t Algo.state_init_fun = fun n _ -> Random.int n
let enable_f : State.t Algo.enable_fun = fun state neighbors ->
if conflict { color = state; neighbors = List.map Algo.state neighbors }
then [ "recolor" ]
- else [ "noop" ]
+ else [ ]
let step_f : State.t Algo.step_fun = fun state neighbors action ->
match action with
| "recolor" -> color { color = state; neighbors = List.map Algo.state neighbors }
- | "noop" -> state
| _ -> failwith "Invalid action"
diff --git a/coloring/state.ml b/coloring/state.ml
index 42413aa1133a07b72e54a2ce59abfd2ff7fcb74a..df321ce1563da4cb5510ce4cbb81d150acc950c9 100644
--- a/coloring/state.ml
+++ b/coloring/state.ml
@@ -2,4 +2,4 @@ type t = int
let to_string = Printf.sprintf "color=%i"
let of_string = None
let copy x = x
-let actions = [ "recolor"; "noop" ]
+let actions = [ "recolor" ]
diff --git a/coloring/utils.lus b/coloring/utils.lus
deleted file mode 100644
index ded8d3ceb5a5d85ac841cf644fec21bb90e61026..0000000000000000000000000000000000000000
--- a/coloring/utils.lus
+++ /dev/null
@@ -1,14 +0,0 @@
--- Generates an array of indexes: [0, 1, ..., N-1]
-function range<<const N:int>>(_ : bool) returns (r : int^N);
-let
- r = with (N = 1) then [ 0 ] else range<<N-1>>(true) | [ N-1 ];
-tel;
-
--- "First-class" if statement, since we don't have lambdas.
-function choice_of_bool<<type T; const t:T; const f:T>>(b : bool) returns (y : T);
-let
- y = if b then t else f;
-tel;
-
--- |> true -> 1 | false -> 0
-function int_of_bool = choice_of_bool<<int, 1, 0>>;
diff --git a/coloring/verify.lus b/coloring/verify.lus
index c655de56e1c839deaa13d1d87ba3bbf41c4f86fc..c9e6a67d9dae21ef3b590c92024910dd069e258d 100644
--- a/coloring/verify.lus
+++ b/coloring/verify.lus
@@ -1,33 +1,23 @@
-include "../../test/lustre/oracle_utils.lus"
-
--- Any activation Ai implies Ei was previously enabled and
--- and |A| != 0 for all non-silent states (ie. it is distributed).
-node is_proper_distributed<<const an : int; const pn: int>>(acti, enab : bool^an^pn)
-returns (res : bool);
-let
- res = all_true<<an,pn>>(map<<implies_list<<an>>,pn>>(acti, pre(enab))) and
- is_distributed<<an,pn>>(acti, enab);
-tel;
+include "../sas.lus"
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
- -- we assume the daemon is proper and locally central (no two neighbors active at once)
- assert(is_proper_distributed<<actions_number,card>>(activations, enables));
- assert(activations[0][0] => not activations[1][0] and not activations[2][0] and not activations[3][0] and not activations[4][0]);
- assert(activations[1][0] => not activations[0][0] and not activations[2][0] and not activations[4][0]);
- assert(activations[2][0] => not activations[0][0] and not activations[1][0] and not activations[3][0]);
- assert(activations[3][0] => not activations[0][0] and not activations[2][0] and not activations[4][0]);
- assert(activations[4][0] => not activations[0][0] and not activations[1][0] and not activations[3][0]);
+ assert(daemon_is_proper<<actions_number,card>>(activations, enables));
+ assert(daemon_is_locally_central<<actions_number,card>>(adjacency, activations));
nodes, enables = topology(activations, inits);
- moves = move_count<<actions_number,card>>(activations);
+ -- we assume the algo is implemented correctly and stabilizes silently
+ legitimate = silent<<actions_number,card>>(enables);
+ closure = true -> (pre(legitimate) => legitimate);
-- the execution terminates after at most |N|−1 moves
- ok = moves = card - 1 => silent<<actions_number,card>>(enables);
+ moves = move_count<<actions_number,card>>(activations);
+ ok = closure and
+ ((moves >= card - 1) => legitimate);
tel;
diff --git a/sas.lus b/sas.lus
new file mode 100644
index 0000000000000000000000000000000000000000..79bffb098e66d5f6486ee7f7ac18763987d78713
--- /dev/null
+++ b/sas.lus
@@ -0,0 +1,70 @@
+include "utils.lus"
+include "bitset.lus"
+
+-- No nodes enabled.
+function silent<<const an:int; const pn:int>>(enab: bool^an^pn)
+returns (y : bool);
+let
+ y = none<<pn>>(map<<any<<an>>, pn>>(enab));
+tel;
+
+node node_is_proper<<const an:int>>(acti, enab : bool^an) returns (y : bool);
+let
+ y = true -> all<<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);
+let
+ y = all<<pn>>(map<<node_is_proper,pn>>(acti, enab));
+tel;
+
+-- |A| >= 1 for non-silent states.
+function daemon_is_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<<any<<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 : bool^an^pn
+) returns (y : bool);
+var
+ active : bool ^ pn;
+ active_adjacencies : bool ^ pn ^ pn;
+ no_active_adjacencies : bool ^ pn;
+ locally_central : bool ^ pn;
+let
+ active = map<<any<<an>>, pn>>(acti);
+ active_adjacencies = map<<inter,pn>>(active^pn, adjacency);
+ no_active_adjacencies = map<<none<<pn>>, pn>>(active_adjacencies);
+ locally_central = map<<=>,pn>>(active, no_active_adjacencies);
+ y = all<<pn>>(locally_central);
+tel;
+
+-- |A| = 1 for non-silent states.
+function daemon_is_central<<const an:int; const pn:int>>(acti : bool^an^pn)
+returns (y : bool);
+let
+ y = silent<<an,pn>>(enab) or
+ boolred<<1,1,pn>>(map<<any<<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)
+returns (y:bool);
+let
+ y = silent<<an,pn>>(enab) or
+ boolred<<pn,pn,pn>>(map<<any<<an>>, pn>>(acti));
+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<<any<<an>>, pn>>(acti));
+tel;
diff --git a/token/verify.lus b/token/verify.lus
index 6a134fc5975a364507204c464146176db8c4fec0..49ec2000f273d78dbf661b305260ead271e419cb 100644
--- a/token/verify.lus
+++ b/token/verify.lus
@@ -1,41 +1,28 @@
-include "../../test/lustre/oracle_utils.lus"
-
--- Any activation Ai implies Ei was previously enabled and
--- and |A| != 0 for all non-silent states (ie. it is distributed).
-node is_proper_distributed<<const an : int; const pn: int>>(acti, enab : bool^an^pn)
-returns (res : bool);
-let
- res = all_true<<an,pn>>(map<<implies_list<<an>>,pn>>(acti, pre(enab))) and
- is_distributed<<an,pn>>(acti, enab);
-tel;
+include "../sas.lus"
+include "../utils.lus"
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;
tokens : int;
- legitimate : bool;
- closure : bool;
-
steps : int;
let
- -- we assume the daemon is proper and put no other limitation to activations
- assert(is_proper_distributed<<actions_number,card>>(activations, enables));
+ assert(daemon_is_proper<<actions_number,card>>(activations, enables));
+ assert(daemon_is_distributed<<actions_number,card>>(activations, enables));
nodes, enables = topology(activations, inits);
-- a node "has the token" when it is enabled
- tokens = red<<count_true_acc<<actions_number>>, card>>(0, activations);
+ tokens = pop_count<<card>>(map<<any<<actions_number>>, card>>(enables));
-- stability in this algo means mutual exclusion: 1 node enabled at a time
legitimate = tokens = 1;
+ closure = true -> (pre(legitimate) => legitimate);
- -- once in a legitimate state, the network remains in a legitimate state
- closure = true -> pre(legitimate) => legitimate;
-
- steps = count(true);
+ steps = (-1 -> pre(steps)) + 1;
ok = (closure) and
(tokens >= 1) and -- there always exists at least one token holder
- (steps >= 8 => legitimate); -- worst-case stabilization
+ ((steps >= card*(card-1) + ((card-4)*(card+1)/2) + 1) => legitimate); -- worst-case stabilization
tel;
diff --git a/utils.lus b/utils.lus
new file mode 100644
index 0000000000000000000000000000000000000000..289a88773eebfcbaf9845083ff1e241008d27d1a
--- /dev/null
+++ b/utils.lus
@@ -0,0 +1,42 @@
+-- Generates an array of indexes: [0, 1, ..., N-1]
+function range<<const N:int>>() returns (r : int^N);
+let
+ r = with (N = 1) then [ 0 ] else range<<N-1>>() | [ N-1 ];
+tel;
+
+-- "First-class" if statement, since we don't have lambdas.
+function choice_of_bool<<type T; const t:T; const f:T>>(b : bool) returns (y : T);
+let
+ y = if b then t else f;
+tel;
+
+-- |> true -> 1 | false -> 0
+function int_of_bool = choice_of_bool<<int, 1, 0>>;
+
+function none<<const N:int>>(s : bool^N) returns (y : bool);
+let
+ y = boolred<<0,0,N>>(s);
+tel;
+
+function any<<const N:int>>(s : bool^N) returns (y : bool);
+let
+ y = boolred<<1,N,N>>(s);
+tel;
+
+function all<<const N:int>>(s : bool^N) returns (y : bool);
+let
+ y = boolred<<N,N,N>>(s);
+tel;
+
+-- Whether an element is contained within an array.
+function member<<type T; const N:int>>(x : T; arr : T^N) returns (y : bool);
+let
+ y = any<<N>>(map<<=,N>>(x^N, arr));
+tel;
+
+function all_different<<type T; const N:int>>(A : T^N) returns (y : bool);
+let
+ y = with (N <= 1) then true
+ else (not member<<T,N-1>>(A[0], A[1 .. N-1])) and
+ all_different<<T,N-1>>(A[1 .. N-1]);
+tel;