How to modify an element of Sequence

[LUMING DONG]

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!

 

[Stephan Merz]

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

--
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/249a64c9-4f41-4c2a-b140-736d6d4327e2%40googlegroups.com.