Re: [tlaplus] How to modify an element of Sequence

Your way of updating the sequence is correct. However, since a sequence is a function and you know the index at which you want to update it, you can also write

Queue' = [Queue EXCEPT ![m] = NewValue]

Best,

Stephan

On 10 Sep 2019, at 07:37, LUMING DONG <dongluming77@xxxxxxxxx> wrote:

Dear friends:

I have variable defined as a Sequnce in my Spec , and I need to modify the value of one of its element (with the index m) in the next step .

So I think the _expression_ below is possible:

Queue' = SubSeq(Queue, 1, m-1) \o << NewValue of m>> \o SubSeq(Queue, m+1, Len(s))

More over, I want to know is there any other convenient method?

Thanks a Lot!

--
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/249a64c9-4f41-4c2a-b140-736d6d4327e2%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/82971463-99F9-4365-A95E-D64ABF3A2FF2%40gmail.com.