[tlaplus] How to modify an element of Sequence

[LUMING DONG <dongluming77@xxxxxxxxx>]

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.