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

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.

--
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/779f2d1e-d4f6-49ea-86cd-5dd12922f5b1%40googlegroups.com.