-------------------------------- MODULE try --------------------------------
EXTENDS Integers
CONSTANT nums
CONSTANT len
VARIABLE idx
VARIABLE max
Init == /\ idx = 0
/\ max = nums[0]
Next == /\ idx < len
/\ IF nums[idx] > max THEN max' = nums[idx] ELSE max' = max
/\ idx' = idx + 1
Invariant == /\ \A i \in {0..idx} : max >= nums[i]
/\ \E i \in {0..idx} : max = nums[i]
=============================================================================
It seems to be correct, but I don't know how to specify the value for nums constant in Model Overview Page of TLA+ toolbox.
I have tried this: nums <- [ 0 |-> 5, 1 |-> 8, 2 |-> 4 ]
But TLA+ toolbox reports error for the input.
Any ideas would be appreciated.
Thanks!