Array assignment

[verifierlife]

There are two arrays: inp: int[50] and p: int[20]. I was wondering whether it is possible to split the first 20 elements of inp and assign them to p.
Further, if it is possible, how about assign the first 20 elements of inp to p in one cycle? Sometimes, this kind of assignment is very useful and important.

node main (inp: int[50]) returns (outp: bool); var p: int[20]; let p = (pre p)[0 := pre inp[0]]; outp = (p[10] <> 4) or (p[15] <> 5); --%PROPERTY outp; tel;

========================================================== In Java, we can do that for(int i = 0; i < p.length; i++){ p[i] = inp[i]; } How can we do that in Lustre.

[verifierlife]

I got it. The grammar is defined as "exp = exp[exp := exp]".

node main (inp: int[50]) returns (outp: bool); var p: int[20]; let p = (((p[0 := inp[0]])....[17 := inp[17])[18 := inp[18]])[19 := pre inp[19]]; outp = (p[10] <> 4) or (p[15] <> 5); --%PROPERTY outp; tel;

You see, it is too long when the length of array is large. So, two questions appear. Why does Lustre design its grammar in this format? Can we write this kind of assignment as follows? p[0] = inp[0]; p[1] = inp[1]; ... p[19] = inp[19];

[lgwagner]

Hi.

This is a good question. The primary use-case for JKind is to serve as a back-end analysis tool for tools such as AGREE, SpeAR, and other tools that are proprietary to Collins Aerospace. We typically use the JKind API to generate Lustre; we rarely write it by hand. So, in this case, you could imagine using the API (written in Java) to easily write the expression you are describing here.

The version of Lustre that JKind supports is not all that user friendly, as you have observed here. It does, however, map very cleanly to SMT which does the heavy lifting during our analysis.