diff --git a/lib/bitset.lus b/lib/bitset.lus index 36b6a029a5e89e73fcf5b075ee71b9950af4f018..f753cb7f16c142f1a54d89a9606061295d0d21e1 100644 --- a/lib/bitset.lus +++ b/lib/bitset.lus @@ -8,7 +8,7 @@ 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>>()); + s = map<<=,N>>(x^N, range<<N>>(true)); assert(boolred<<1,1,N>>(s)); tel; diff --git a/lib/sas.lus b/lib/sas.lus index f36bb3f874cf6fac8460bae0520d7459c3003199..4a34d031a19583ad0c23ba71db9d7ab983b8729c 100644 --- a/lib/sas.lus +++ b/lib/sas.lus @@ -40,7 +40,7 @@ var locally_central : bool ^ pn; let active = map<<boolany<<an>>, pn>>(acti); - active_adjacencies = map<<inter,pn>>(active^pn, adjacency); + 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 = boolall<<pn>>(locally_central); diff --git a/lib/utils.lus b/lib/utils.lus index b17500d3585a19e495884636cde9f741f0404f2c..6185c90293e76dc93d535fde7a9c98bab0308f6c 100644 --- a/lib/utils.lus +++ b/lib/utils.lus @@ -1,7 +1,7 @@ -- Generates an array of indexes: [0, 1, ..., N-1] -function range<<const N:int>>() returns (r : int^N); +function range<<const N:int>>(_ : bool) returns (r : int^N); let - r = with (N = 1) then [ 0 ] else range<<N-1>>() | [ N-1 ]; + r = with (N = 1) then [ 0 ] else range<<N-1>>(true) | [ N-1 ]; tel; -- First-class if statement, since we don't have lambdas. diff --git a/test/coloring/verify.lus b/test/coloring/verify.lus index d5b94eb2d3268ffa73ebdbb534f9d13c4b8e6f5c..957a20cbedc0bb2cfda5f2db0d4ec99c98e09a3a 100644 --- a/test/coloring/verify.lus +++ b/test/coloring/verify.lus @@ -19,5 +19,5 @@ let -- the execution terminates after at most |N|−1 moves moves = move_count<<actions_number,card>>(activations); ok = closure and - ((moves = card - 1) => legitimate); + ((moves >= card - 1) => legitimate); tel; diff --git a/test/token/verify.lus b/test/token/verify.lus index d0b7128e25a8992b20bd66259e20307301404e01..53d11a6884141c99b917ce77afd4a64b0d6291f2 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 >= card*(card-1) + ((card-4)*(card+1)/2) + 1) => legitimate); -- worst-case stabilization tel;