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

Dear Stephan, I've learned so much from you.
Thanks for helping!

On Saturday, May 30, 2020 at 9:48:50 PM UTC+8, Stephan Merz wrote:
Again, if you use sequences (i.e., index from 1), you can just write Len(nums).

For your setup, you can define

len == 1 + (CHOOSE i \in DOMAIN nums : \A j \in DOMAIN nums : j <= i)

Stephan

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

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,

(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...@xxxxxxxxxxxxxxxx.