how to input an array constant in TLA+ toolbox?

[biao zhang]

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!

[Stephan Merz]

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

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

[biao zhang]

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.

Stephan

To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.

[Stephan Merz]

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

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/779f2d1e-d4f6-49ea-86cd-5dd12922f5b1%40googlegroups.com.

[biao zhang]

Dear Stephan, I've learned so much from you.

Thanks for helping!

Stephan

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/779f2d1e-d4f6-49ea-86cd-5dd12922f5b1%40googlegroups.com.