How to remove an iterm from a Sequence?

[diaoz...@hotmail.com]

Dear all,

I'm writing a TLA program to process a message queue whlle I must remove a duplicate item from the sequence when a new message is added to the message queue. How could I do this with TLA module? Or I must write a function to deal with it?

Thanks

Regards

Diao Zegnqi.

[Stephan Merz]

You could write something like

SelectSeq(seq, LAMBDA x : x # item)

to obtain a sequence with all occurrences of `item' removed. However, it sounds a little strange to me that you model a queue where the order of elements matters while duplicates are eliminated. If the order is unimportant as well, it would be simpler to use a set.

Regards,

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/ddbdce3d-9339-44c2-98f3-58fbdf2b944c%40googlegroups.com.

[diaoz...@hotmail.com]

Hi Stephan,

Thank you for your help. 

I'm wirting a telecommunication simulating program where a wireless phone connects to a base station. During the initial setup period, the BS will allocate a temporary ID to the phone and when the initial setup period ends, the temporary ID become a permanent ID. The pnone may initiate a new setup when it needs and the BS will allocate a new temporary ID for it again untill the setup is established again when it can report its permanent ID. The BS will then recogonize the phone with its permanent ID and confirms the setup with the permanet ID. Due to some radio error, the phone may initiate the setup while the BS is processing the previous setup. When the BS finds a new setup it should disacard the old one. I make all phones' setup request in a queue(it is processed by the BS one by one and a queue is suitable for it). And I now have to choose the previous setup and discard it.

It is really strange to  do such a thing for the Sequence. But if I use a set, how can I decide the order?

Regards

Diao Zegnqi.

在 2020年5月26日星期二 UTC+8下午2:25:13，Stephan Merz写道：

You could write something like

SelectSeq(seq, LAMBDA x : x # item)

to obtain a sequence with all occurrences of `item' removed. However, it sounds a little strange to me that you model a queue where the order of elements matters while duplicates are eliminated. If the order is unimportant as well, it would be simpler to use a set.

Regards,

Stephan

On 26 May 2020, at 05:18, diaoz...@hotmail.com wrote:

Dear all,

I'm writing a TLA program to process a message queue whlle I must remove a duplicate item from the sequence when a new message is added to the message queue. How could I do this with TLA module? Or I must write a function to deal with it?

Thanks

Regards

Diao Zegnqi.

--
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/ddbdce3d-9339-44c2-98f3-58fbdf2b944c%40googlegroups.com.

在 2020年5月26日星期二 UTC+8下午2:25:13，Stephan Merz写道：

You could write something like

SelectSeq(seq, LAMBDA x : x # item)

to obtain a sequence with all occurrences of `item' removed. However, it sounds a little strange to me that you model a queue where the order of elements matters while duplicates are eliminated. If the order is unimportant as well, it would be simpler to use a set.

Regards,

Stephan

On 26 May 2020, at 05:18, diaoz...@hotmail.com wrote:

Dear all,

I'm writing a TLA program to process a message queue whlle I must remove a duplicate item from the sequence when a new message is added to the message queue. How could I do this with TLA module? Or I must write a function to deal with it?

Thanks

Regards

Diao Zegnqi.

--
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.