Transpose a matrix with Lustre V6

This Tiny Tutorial:

1. shows how one can transpose a Lustre V6 matrix;
2. illustrates the concepts of parametric nodes and static recursivity in Lustre V6;
3. illustrates how to use the lesar model-checker to validate it.

In order to write a generic transpose, that works whatever the size of the matrix is, we will use 2 static parameters n and m:

function transpose<<const n:int; const m:int; type t>>(x:t^m^n) returns (y:t^n^m);

Now to perform the transposition of a generic matrix, we need to use a Statically Recursive function using the with/then/else construct.

let
  y =
  -- with n = 0 then []
  -- No empty array in Lustre! grrr.
  with n = 1 then
     map<<scal_to_array<<t>>, m >>(x[0])
  else
     add_vect_to_matrix <<n-1,m,t>>(x[0], transpose<<n-1,m,t>>(x[1..n-1]));
tel

A current limitation of the Verimag Lustre V6 compiler prevents us to manipulate empty arrays. Therefore we need to finish our recursion with n=1. The trivial function scal_to_array lifts scalars to arrays of size 1.

function scal_to_array<<type t>>(x:t) returns (res:t^1);
let
  res = [x];
tel

The add_vect_to_matrix function appends a vector to a matrix.

function add_vect_to_matrix<<const n:int; const m:int; type t>>(x:t^m; y:t^n^m)
returns (res:t^(n+1)^m);
let
  res =
  with m = 1 then [ [ x[0]] | y[0] ]
  else            [ [ x[0]] | y[0] ]
                  | add_vect_to_matrix<<n,m-1,t>> (x[1..m-1], y[1..m-1]);
tel

Of course, in order to test this node, one need to set values for the matrix sizes.

function test_transpose(x:int^4^2) returns (res:int^2^4);
let
  res = transpose<<2,4,int>>(x);
tel

And then, one can to simulate this node:

  lv6 -exec transpose.lus -n test_transpose

  luciole-rif lv6 -exec transpose.lus -n test_transpose

Now, let’s show with lesar that transpose is an involution. We can not prove this property for any n and m with a model-checker, but we can do it for some specific values:

function transpose_is_involutive(x:bool^4^2) returns (res:bool);
var
  y: bool^2^4;
  z: bool^4^2;
let
  y = transpose<<2,4,bool>>(x);
  z = transpose<<4,2,bool>>(y);
  res = ( x = z );
tel

In order to model-check with lesar the transpose program against the property transpose_is_involutive property, we need to convert it into a language that it can handle (Lustre V4 or ec). Here we first compile transpose into ec:

lv6 transpose.lus -n transpose_is_involutive -ec -o proove_me.ec &&
lesar proove_me.ec transpose_is_involutive