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

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.