loop operation in Lustre

[verifierlife]

Loop operation is very important for program, especially for array operation. However, if I am correct, Lustre language is applying cycle to array operation, instead of loop. Even the "normal" Lustre-v6 in Verimag is doing the same thing. I am confused with the feature in synchronous language.

For instance,

node main(in1: int[3]; in2: int[3]) returns(outp: bool; pArr: bool[3]); var out: bool; let out, pArr [0] = comput(in1[0], in2[0]); out, pArr [1] = if out then comput(in1[1], in2[1]) else (false, false); out, pArr [2] = if out then comput(in1[2], in2[2]) else (true, true); outp = pArr[0] and pArr[1] and pArr[2]; --%PROPERTY outp; tel;

node comput(arr1: int; arr2: int) returns (result: bool; resultArr: bool); let resultArr = (arr1 > 0); result = (arr2 > 0) and resultArr; --%PROPERTY result;
tel;

The code prompts the "reassign" error.
So, any comments for my confusion?

[lgwagner]

Hi.

Lustre is a synchronous dataflow language. You cannot assign a variable more than once in a given node specification. Instead you may work around this by introducing intermediate variables and using the if/then/else expression to control the assignment of outputs as you might in standard programming language.

let me try to restructure your example into valid input here:

node main(in1: int[3]; in2: int[3]) returns(outp: bool; pArr: bool[3]); var t1, t2, t3 : bool; pArr0, pArr1, pArr2 : bool; out: bool; let t1, pArr0 = comput(in1[0], in2[0]); t2, pArr1 = if t1 then comput(in1[1], in2[1]) else (false, false); t3, pArr2 = if t2 then comput(in1[2], in2[2]) else (true, true); out = t3; pArr = [pArr0, pArr1, pArr2]; outp = pArr[0] and pArr[1] and pArr[2]; --%PROPERTY outp; tel;

node comput(arr1: int; arr2: int) returns (result: bool; resultArr: bool); let resultArr = (arr1 > 0); result = (arr2 > 0) and resultArr; --%PROPERTY result; tel;

I cannot be sure I matched the intent of your original model but hopefully the example should help you understand how to work with the language to express what you would like.

[verifierlife]

Thanks @lgwagner, your interpretation means a lot to me.

Further, in the above example, there is a property for each node, respectively. I was confusing why the property "outp" (written in "main" node) was not parsed and checked. It prompts as the following:

`

JKind 4.4.1

There are 1 properties to be checked. PROPERTIES TO BE CHECKED: [result]

++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ INVALID PROPERTY: result || bmc || K = 1 || Time = 0.115s Step variable 0

INPUTS arr1 0 arr2 1

OUTPUTS result false resultArr false

++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

-------------------------------------
--^^--        SUMMARY          --^^--
-------------------------------------

INVALID PROPERTIES: [result]`

Are there any mistakes in the example?

[lgwagner]

JKind used to look for a node named "main" but we have removed that behavior. Now you have 2 options to declare your main node.

1. Place the node you want to be the main node as the last node in the file.
2. Use the --%MAIN; directive to identify your main node.

Below is your example using the second method:

---

node main(in1: int[3]; in2: int[3]) returns(outp: bool; pArr: bool[3]); var t1, t2, t3 : bool; pArr0, pArr1, pArr2 : bool; out: bool; let --%MAIN; t1, pArr0 = comput(in1[0], in2[0]); t2, pArr1 = if t1 then comput(in1[1], in2[1]) else (false, false); t3, pArr2 = if t2 then comput(in1[2], in2[2]) else (true, true); out = t3; pArr = [pArr0, pArr1, pArr2]; outp = pArr[0] and pArr[1] and pArr[2]; --%PROPERTY outp; tel;

node comput(arr1: int; arr2: int) returns (result: bool; resultArr: bool); let resultArr = (arr1 > 0); result = (arr2 > 0) and resultArr; --%PROPERTY result; tel;