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

*From*: biao zhang <zhanbiao2000@xxxxxxxxx>*Date*: Sat, 30 May 2020 07:18:03 -0700 (PDT)*References*: <f79f5661-f069-4921-9796-420006e2f517@googlegroups.com> <997736BC-1D57-4044-ABF2-E48921171CE5@gmail.com> <779f2d1e-d4f6-49ea-86cd-5dd12922f5b1@googlegroups.com> <3DFE0683-2C25-4170-8B47-AFF7BAE8A2D9@gmail.com>

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:

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 definelen == 1 + (CHOOSE i \in DOMAIN nums : \A j \in DOMAIN nums : j <= i)StephanOn 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,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+.StephanOn 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:------------------------------

-- MODULEtry --------------------------------

EXTENDSIntegers

CONSTANTnums

CONSTANTlen

VARIABLEidx

VARIABLEmax

Init == /\ idx = 0

/\ max = nums[0]

Next == /\ idx < len

/\

IFnums[idx] > maxTHENmax' = nums[idx]ELSEmax' = 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.

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 tla...@googlegroups.com .

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/779f2d1e-d4f6- .49ea-86cd-5dd12922f5b1% 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/fce03ea8-6615-4b16-87a3-85de0894ab4b%40googlegroups.com.

**References**:**[tlaplus] how to input an array constant in TLA+ toolbox?***From:*biao zhang

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

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

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

- Prev by Date:
**Re: [tlaplus] how to input an array constant in TLA+ toolbox?** - Next by Date:
**[tlaplus] "Final" action to check hyperproperties ?** - Previous by thread:
**Re: [tlaplus] how to input an array constant in TLA+ toolbox?** - Next by thread:
**[tlaplus] "Final" action to check hyperproperties ?** - Index(es):