# [tlaplus] Indexed arrays and functions in TLA

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}?

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.