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

Re: [tlaplus] Indexed arrays and functions in TLA

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.


[1] https://stackoverflow.com/a/53974837/6291195
[2] https://discuss.tlapl.us/msg02252.html
[4] https://www.hpl.hp.com/techreports/Compaq-DEC/SRC-TN-1997-006A.pdf

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/bc4a5d8f-264a-ee73-d13c-ee53263c6e2e%40lemmster.de.