wrapper/tests/parity/parity.lus

   1 const size=8;
   2
   3 node XOR(a,b:bool) returns (Xor:bool);
   4 let
   5         Xor = if a then not b else b;
   6 tel
   7
   8 node P(const n: int; B: bool^n) returns (p:bool);
   9 let
  10  p = with n=1 then B[0]
  11       else XOR(B[n-1] , P(n-1,B[0..n-2]));
  12 tel
  13
  14 node parity (input: bool^size)
  15 returns (parity,done: bool);
  16 var b, todo: bool^size;
  17 let
  18    b[0..(size-2)] = input[0..(size-2)] ->
  19                               pre(b[1..(size-1)]);
  20    b[size-1] = input[size-1] -> false;
  21    todo[0..(size-2)] = false^(size-1) ->
  22                               pre(todo[1..(size-1)]);
  23    todo[size-1] = true -> false;
  24    done = todo[0];
  25    parity = b[0] -> XOR(pre(parity) , b[0]);
  26 tel
  27
  28 node verif_parity (input: bool^size)
  29 returns(ok: bool);
  30 var comb, seq, done: bool;
  31 let
  32    ok = not done or (comb = seq);
  33    comb =  P(size,input) -> pre(comb);
  34   (seq,done) = parity(input);
  35 tel