Re: [tlaplus] Indexed arrays and functions in TLA

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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

-- 
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.