[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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.