[tlaplus] Indexed arrays and functions in TLA

[Mursel Musabasic <murselmurga@xxxxxxxxx>]

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!

-- 
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/10cd92d0-72a4-454a-9ba9-67f0017cb119%40googlegroups.com.