Re: [tlaplus] how to input an array constant in TLA+ toolbox?

It works well! Thanks Stephan.

Another question, is there any convenient method to get the length of nums so that I don't need to input the constant len?

I've searched a lot and found nothing.

On Saturday, May 30, 2020 at 8:32:42 PM UTC+8, Stephan Merz wrote:

Hello,

your syntax for specifying the function is not correct. Instead, try

(0 :> 5) @@ (1 :> 8) @@ (2 :> 4)

or

[x \in 0 .. 2 |-> IF x = 0 THEN 5 ELSE IF x = 1 THEN 8 ELSE 4]

If you choose to index your functions from 1, you can simply write <<5 ,8 4>> since a function with domain 1..N is a sequence in TLA+.

Stephan

On 30 May 2020, at 14:17, biao zhang <zhanbi...@xxxxxxxxx> wrote:

Hi,

I'm learning TLA+ recently. I'm trying to specify a simple program which find the max element in an array as below:

-------------------------------- MODULE try --------------------------------
EXTENDS Integers

CONSTANT nums
CONSTANT len
VARIABLE idx
VARIABLE max

Init == /\ idx = 0
/\ max = nums[0]

Next == /\ idx < len
/\ IF nums[idx] > max THEN max' = nums[idx] ELSE max' = max
/\ idx' = idx + 1

Invariant == /\ \A i \in {0..idx} : max >= nums[i]
/\ \E i \in {0..idx} : max = nums[i]

=============================================================================

It seems to be correct, but I don't know how to specify the value for nums constant in Model Overview Page of TLA+ toolbox.
I have tried this: nums <- [ 0 |-> 5, 1 |-> 8, 2 |-> 4 ]
But TLA+ toolbox reports error for the input.

Any ideas would be appreciated.

Thanks!

--
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 tla...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/f79f5661-f069-4921-9796-420006e2f517%40googlegroups.com.