Indexed arrays and functions in TLA

[Mursel Musabasic]

Hi there,

I'm a newbie in TLA and formal methods at all. I am trying to figure out this line of PlusCal:

variables flag = [i \in {0,1} |-> FALSE], turn \in {0,1}; 

Variable flag is an indexed array where i is index in set of elements 0 and 1 such that flag[i] is equal to FALSE. Is this correct? Variable turn is an element of set of integers {0,1}?

Also, is this expression  [i \in {0,1} |-> FALSE] function with domain {0,1}?

Thanks in advance!

[Markus Kuppe]

On 12.02.20 06:54, Mursel Musabasic wrote:
> Hi there,
>
> I'm a newbie in TLA and formal methods at all. I am trying to figure out
> this line of PlusCal:
>
> variables flag = [i \in {0,1} |-> FALSE], turn \in {0,1}; 
>

> Variable flag is an indexed array where /i/ is index in set of elements

> 0 and 1 such that flag[i] is equal to FALSE. Is this correct? Variable
> turn is an element of set of integers {0,1}?
>
> Also, is this expression  [i \in {0,1} |-> FALSE] function with domain
> {0,1}?
>
> Thanks in advance!

Hi Mursel,

you are on the right track. The Toolbox's state space visualization
[1,2] and the logic calculator (evaluate constant expressions) [3] with
the DOMAIN operator [4] can help you test your hypotheses.

M.

[1] https://stackoverflow.com/a/53974837/6291195
[2] https://discuss.tlapl.us/msg02252.html
[3]
https://tla.msr-inria.inria.fr/tlatoolbox/doc/model/evaluate-consant-expression.html
[4] https://www.hpl.hp.com/techreports/Compaq-DEC/SRC-TN-1997-006A.pdf