verify.lus

----------------------------------------------------------------------------
-- function verify
----------------------------------------------------------------------------
node verify(activations : bool^actions_number^card; inits : state^card) 
returns (ok : bool);
var
  config : state^card;
  enables : bool^actions_number^card;
  legitimate, closure, CD_disable, theorem, lustre_round : bool;
  lustre_round_nb:int;
let
  assert(daemon_is_distributed<<actions_number,card>>(activations, pre enables));
  assert(rangei<<0,diameter,card>>(inits)); 
  config, enables, lustre_round, lustre_round_nb = topology(activations, inits);

  legitimate = legitimate<<actions_number,card>>(enables,config);
  closure = true -> (pre(legitimate) => legitimate);
  CD_disable =  all_CD_are_false(enables);

  -- verify that the execution terminates after at most |N|−1 moves:
  theorem = ( (lustre_round_nb>=diameter+1) => CD_disable )
        and ( (lustre_round_nb>=diameter+2) => legitimate );
  ok = closure and theorem;
tel;

----------------------------------------------------------------------------
-- all states are initially in correctly
----------------------------------------------------------------------------
function rangei<<const low:int; const D:int; const card:int>>(config:state^card) returns (res:bool);
var
  e:state;
let
  e = config[card-1];
  res = with (card=1) then (e.d >=0) and (e.d < D) and (e.par = -1)
  else ((e.d >= 0) and
        (e.d < D) and
        (e.par >=0) and
        (e.par < nb_neighbors[card-1])) and rangei<<low; D; card-1>>(config[0..card-2]);
tel

-----------------------------------------------------------------------------
--function for CD_disable:
-----------------------------------------------------------------------------
function first_element(X:bool^actions_number) returns (res:bool);
let
   res = X[0];
tel 
function first_column(X:bool^actions_number^card) returns (Z:bool^card);
let
   Z = map<<first_element,card>>(X); 
tel
function all_CD_are_false (tab_enab:bool^actions_number^card) returns (res:bool);
let
  res = not (red<<or,card>>(false,first_column(tab_enab))) ;
tel
-----------------------------------------------------------------------------