refactor

salut/lib/bitset.lus

@@ -73,20 +73,16 @@ let
 	y = boolred<<N,N,N>>(map<<=>,N>>(s1, s2));
 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.
-*/
+-- 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);
 let
 	set = red<<set<<N>>,M>>(false^N, list);
 tel;
 
-/*
-	Returns the index of the first enumerated element present in the set.
-	The result will be negative if the set is empty.
-*/
+-- Returns the index of the first enumerated element present in the set.
+-- The result will be negative if the set is empty.
 function first_set<<const N:int>>(s : bool^N) returns (x : int);
 var
 	found : int;
@@ -98,10 +94,8 @@ let
 	    else found + 1;
 tel;
 
-/*
-	Returns the index of the last enumerated element present in the set.
-	The result will be negative if the set is empty.
-*/
+-- Returns the index of the last enumerated element present in the set.
+-- The result will be negative if the set is empty.
 function last_set<<const N:int>>(s : bool^N) returns (x : int);
 let
 	x = with (N = 1) then (if s[0] then 0 else -1)

salut/lib/sas.lus

@@ -22,7 +22,7 @@ let
   y = boolall<<an>>(map<<=>,an>>(acti, enab));
 tel;
 
-node daemon_is_valid<<const an:int; const pn:int>>(acti, enab : bool^an^pn)
+function daemon_is_valid<<const an:int; const pn:int>>(acti, enab : bool^an^pn)
 returns (y : bool);
 let
   y = boolall<<pn>>(map<<activation_is_valid<<an>>, pn>>(acti, enab));
@@ -30,7 +30,7 @@ tel;
 
 
 -- |A| >= 1 for non-silent states.
-node daemon_is_distributed<<const an:int; const pn:int>>(acti, enab : bool^an^pn)
+function daemon_is_distributed<<const an:int; const pn:int>>(acti, enab : bool^an^pn)
 returns (y : bool);
 let
   y = daemon_is_valid<<an, pn>>(acti, enab)
@@ -42,7 +42,7 @@ returns (acti : bool^an^pn);
 var
   nb_enab,rng:int;*)
 -- Exactly one node is activated.
-node daemon_is_central<<const an:int; const pn:int>>(acti, enab : bool^an^pn)
+function daemon_is_central<<const an:int; const pn:int>>(acti, enab : bool^an^pn)
 returns (y : bool);
 let
   y = daemon_is_valid<<an, pn>>(acti, enab)
@@ -50,34 +50,8 @@ let
 
 tel;
 
-function make_activ_tab<<const an:int>>(ain:int; elem:bool^an)
-returns(aout:int; res:bool^an);
-var
-  elem_is_true:bool;
-let
-  elem_is_true = boolany<<an>>(elem);
-  res= if elem_is_true and (ain=0) then elem else false^an;
-  aout = if elem_is_true then ain-1 else ain;
-tel;
-
-function if_true_add_1<<const an:int>>(ain: int; elem: bool^an)
-returns(aout : int);
-let
-  aout= if boolany<<an>>(elem) then ain+1 else ain; 
-tel;
-
-unsafe function central<<const an:int; const pn:int>>(enab : bool^an^pn)
-returns (acti : bool^an^pn);
-var
-  nb_enab,rng,temp:int;
-let
-  nb_enab = red<<if_true_add_1<<an>>,pn>>(0,enab);
-  rng = random(nb_enab);
-  temp,acti = fillred<<make_activ_tab<<an>>,pn>>(rng,enab);
-tel; 
-
 -- No two neighboring nodes are active at once.
-node daemon_is_locally_central<<const an:int; const pn:int>>(
+function daemon_is_locally_central<<const an:int; const pn:int>>(
 	acti, enab : bool^an^pn;
 	adjacency : bool^pn^pn
 ) returns (y : bool);
@@ -97,18 +71,12 @@ tel;
 
 
 -- All enabled nodes are activated.
-node daemon_is_synchronous<<const an:int; const pn:int>>(acti, enab : bool^an^pn)
+function daemon_is_synchronous<<const an:int; const pn:int>>(acti, enab : bool^an^pn)
 returns (y:bool);
 let
   y = (acti = enab);
 tel;
 
-node synchronous<<const an:int; const pn:int>>(enab : bool^an^pn)
-returns (acti : bool^an^pn);
-let
-  acti = enab;
-tel;
-
 -- Measures time complexity in moves.
 node move_count<<const an:int; const pn:int>>(acti : bool^an^pn)
 returns (count:int);

salut/src/dot2lus.ml

@@ -153,8 +153,7 @@ let output_topology lustre_topology (graph : Topology.t) name =
  graph.nodes
  |> List.iteri (fun i _ ->
   Printf.fprintf lustre_topology
-   "\tsel_%d = false -> boolred<<1,%s,%s>>(p[%d]);\n"
-   i action_number action_number i);
+   "\tsel_%d = false -> n_or<<%s>>(p[%d]);\n" i action_number i);
  
  let index_of_id = make_index graph in
  graph.nodes

salut/test/README.org

 This directory contains Lustre versions of the ASM algorithms available
 in Ocaml in file:../../test/
 
-More precisely, each directory contains :
+More precisely, each directory contains:
+- symbolic links to the Ocaml implementation
 - a lustre implementation of an ASM algorithm
-- some symbolic links to their Ocaml implementation
 - a lustre oracle that checks (with lurette) that both implementations behaves the same
 - a =verify.lus= that models some properties to be model-checked (with lesar or kinds2)
 - a Makefile to run simulations or model-checking
@@ -12,4 +12,4 @@ To simulate or to model-check such Lustre programs, one can use
 - =gg= and =gg-deco= to generate topologies via =.dot= files
 - =salut= to generate a lustre versions of the =.dot= files
 - the various =Makefiles= for examples of uses
-  
+ 

salut/test/coloring/p.lus

-include "../../lib/bitset.lus"
 
 const K = max_degree + 1;
 
@@ -6,13 +5,18 @@ function p_enable<<const degree:int>>(this : state; neighbors : neigh^degree)
 returns (enabled : bool^actions_number);
 	var conflict, out_of_range : bool;
 let
-	out_of_range = this < 0 or this >= K;
-	conflict = subset<<K>>(one_hot<<K>>(this), bitset_of_list<<K,degree>>(map<<state,degree>>(neighbors)));
-	enabled = [ out_of_range or conflict ];
+  out_of_range = this < 0 or this >= K;
+  conflict = subset<<K>>(one_hot<<K>>(this), 
+                         bitset_of_list<<K,degree>>(map<<state,degree>>(neighbors)));
+  enabled = [ out_of_range or conflict ];
 tel;
 
-function p_step<<const degree:int>>(this : state; neighbors : neigh^degree; action : action)
+function p_step<<const degree:int>>(this : state; 
+                                    neighbors : neigh^degree; 
+                                    action : action)
 returns (new : state);
 let
-	new = first_set<<K>>(diff<<K>>(true^K, bitset_of_list<<K,degree>>(map<<state,degree>>(neighbors))));
+  new = first_set<<K>>(diff<<K>>(
+            true^K, 
+            bitset_of_list<<K,degree>>(map<<state,degree>>(neighbors))));
 tel;

salut/test/dijkstra-ring/cost.lus

 
 -- By convention, the root is node 0. 
-node is_root(pid: int) returns (res:bool);
+function is_root(pid: int) returns (res:bool);
 let
   res = (pid = 0);
 tel
@@ -14,7 +14,7 @@ tel
 -- 2 4 5 3 0 1 3 -> convex, z=0
 -- 2 2 2 3 0 2 3 -> not convex, z=2
 
-node compute_z(config : state^card) returns (z : int);
+function compute_z(config : state^card) returns (z : int);
 var
   acc0, acc_end: acc_t;
   _ic: idx_conf;
@@ -42,14 +42,14 @@ type idx_conf = {
    c:state^card
 };
 
-node get_smallest_incre(acc:int; idx:int; root_val: int; free:bool) returns (nacc:int);
+function get_smallest_incre(acc:int; idx:int; root_val: int; free:bool) returns (nacc:int);
 let
   nacc = if free 
          then mini(acc, if root_val<idx then idx-root_val else idx-root_val+card)
          else acc;
 tel
 
-node is_free(acc:idx_conf) returns (nacc:idx_conf; res:bool);
+function is_free(acc:idx_conf) returns (nacc:idx_conf; res:bool);
 let
   nacc = idx_conf { i=acc.i+1; c=acc.c };
   res = not (member<<int,card>>(acc.i, acc.c));
@@ -61,7 +61,7 @@ type acc_t = {
      root_val: int; -- constant 
      pval_dif: bool; -- exists j <= curr_idx s.t. config[j] <> config[0]
 };
-node iter_z(acc:acc_t; curval : int) returns (res:acc_t);
+function iter_z(acc:acc_t; curval : int) returns (res:acc_t);
 let
   res = 
           acc_t{ 
@@ -75,7 +75,7 @@ tel
 
 -- Computes the sum_dist as described in the book. It is the sum of the distance
 -- from each token to the root
-node compute_sd(enabled_actions : bool^actions_number^card; config : state^card) returns (res : int);
+function compute_sd(enabled_actions : bool^actions_number^card; config : state^card) returns (res : int);
 var
   enabled_process: bool^card;
   dist_root: int^card;
@@ -86,19 +86,19 @@ let
   res= red<<root_distance, card>>(0, dist_root, enabled_process);
 tel
 -- iterated node used above
-node root_distance(ptotal, index: int; enabled:bool) returns (total:int);
+function root_distance(ptotal, index: int; enabled:bool) returns (total:int);
 let
   total = if index = 0 or not(enabled) then ptotal else index+ptotal;
 tel
 
 node test_fill= fill<<decr,card>>;
-node decr(px:int) returns (x,res:int);
+function decr(px:int) returns (x,res:int);
 let
   x = px-1;
    res = px mod card;
 --  res = if px < 0 then px+card else px; -- to be able to use lesar (via ec2ec -usrint)
 tel
-node incr_mod(px:int) returns (x,res:int);
+function incr_mod(px:int) returns (x,res:int);
 let
 --  x = (px+1) mod card;
   x = (px+1);
@@ -106,7 +106,7 @@ let
   res = px mod card;
 tel
 
-node cost(enabled : bool^actions_number^card; config : state^card) returns (res : int);
+function cost(enabled : bool^actions_number^card; config : state^card) returns (res : int);
 var
   sum_dist, z, res0 : int;
 let
@@ -114,6 +114,6 @@ let
   sum_dist = compute_sd(enabled,config);
   res0 = z * card + sum_dist - 2;
   res = if z = (card - 1)
-        then (3 * card * (card - 1) / 2) - card - 1
+        then (3 * card * (card - 1) div 2) - card - 1
         else if res0 < 0 then 0 else res0;
 tel

salut/test/unison/unison.lus

 include "k.lus"
 
-function min_clock<<const n:int>> (this : int; neighbors : neigh^n)
+function min_clock<<const n:int>> (acc : int; neighbors : neigh^n)
 returns (new: int);
 var min:int;
 let
-  min = if this <= state(neighbors[0]) then this else state(neighbors[0]) ;
+  min = if acc <= state(neighbors[0]) then acc else state(neighbors[0]) ;
   new = with (n = 1) then min
         else min_clock<< n-1 >> (min, neighbors[1 .. n-1]);
 tel;
 
-function newClockValue<<const n:int>> (this : int ; neighbors : neigh^n)
+function newClockValue<<const n:int>> (acc : int ; neighbors : neigh^n)
 returns (new: state);
 let
-  new = (min_clock<<n>>(this,neighbors)+1) mod k;
+  new = (min_clock<<n>>(acc,neighbors)+1) mod k;
 tel;
 
-function unison_enable<<const degree:int>> (this : state; neighbors : neigh^degree)
+function unison_enable<<const degree:int>> (s : state; neighbors : neigh^degree)
 returns (enabled : bool^actions_number);
 let
-  enabled= [ this <> (newClockValue<<degree>>(this,neighbors)) ];
+  enabled= [ s <> (newClockValue<<degree>>(s,neighbors)) ];
 tel;
 
 function unison_step<<const degree:int>>(
-  this : state;
+  s : state;
   neighbors : neigh^degree; action : action)
 returns (new : state);
 let
-  new = newClockValue<<degree>>(this,neighbors);
+  new = newClockValue<<degree>>(s,neighbors);
 tel;

test/coloring/state.ml

-(* Automatically generated by /home/jahier/.opam/4.10.0/bin/sasa version "4.2.1-3-g3be9fa3" ("3be9fa3")*)
-(* on crevetete the 25/6/2020 at 16:35:34*)
-(*sasa -reg ring.dot*)
 
 type t = int 
 let to_string = Printf.sprintf "c=%i"

test/lustre/round.lus

--- -- Time-stamp: <modified the 20/06/2022 (at 13:22) by Erwan Jahier>
+-- -- Time-stamp: <modified the 13/09/2022 (at 14:22) by Erwan Jahier>
 --  
 -- Computing rounds in Lustre
 -- The inputs are 2 arrays Enab and Acti, where:
@@ -22,17 +22,17 @@ var
   -- when forall i mask[i] is false, we have a round.
   pmask: bool^pn;
   init_mask, silent: bool;
-  mask0, mask: bool^pn;
+  mask_i, mask0, mask: bool^pn;
 let
   silent = silent<<an,pn>>(Enab);
   pmask = (false^pn) fby mask;
-  init_mask = boolred<<0,0,pn>>(mask0);
+  init_mask = boolnone<<pn>>(mask0);
   mask0 = false^pn -> mask_update<<an, pn>>(Enab, PreActi, pmask);
 --  mask = merge init_mask (true  -> mask_init<<an, pn>>(Enab when init_mask))
 --                         (false -> mask0 when not init_mask);
-  mask = if init_mask then mask_init<<an, pn>>(Enab)
-                      else mask0;
-  res = false -> not(silent) and (boolred<<0,0,pn>>(mask0));
+  mask_i = mask_init<<an, pn>>(Enab);
+  mask = if init_mask then mask_i else mask0;
+  res = false -> not(silent) and (boolnone<<pn>>(mask0));
 tel
 
 -- At the first instant, the round has not begun
@@ -62,8 +62,8 @@ var
 let
 --  acti = map<< red<<or, an>>, pn >>(false^pn, A);
 --  enab = map<< red<<or, an>>, pn >>(false^pn, E);
-  acti = map<< boolred<<1,an,an>>, pn >>(A); -- a process is active iff at least one action is
-  enab = map<< boolred<<1,an,an>>, pn >>(E); --              enabled
+  acti = map<< n_or<<an>>, pn >>(A); -- a process is active iff at least one action is
+  enab = map<< n_or<<an>>, pn >>(E); --              enabled
 --  res  = map<<and, pn>>(pmask,acti);
    res = map<<mask_update_one, pn>> (enab, acti, pmask);
 tel

test/unison/unison.ml

-(* Time-stamp: <2022-07-18 15:47:53 emile> *)
+(* Time-stamp: <modified the 22/11/2022 (at 13:59) by Erwan Jahier> *)
 
 open Algo
 
@@ -12,11 +12,6 @@ let (init_state: int -> string -> 'v) =
     (*     Printf.eprintf "unison.ml: tossing!\n";flush stderr;  *)
     Random.int m
 
-let list_min l =
-  match l with
-    [] -> assert false
-  | x::l -> List.fold_left min x l
-
 let new_clock_value nl clock =
   let cl = List.map (fun n -> state n) nl in
   let min_clock = List.fold_left min clock cl in