Re: [tlaplus] specify some action eventually will never happen

[Stephan Merz <stepha...@xxxxxxxxx>]

You can write something like

Spec => (<>[][~ MessageLoss]_vars => Liveness)

where MessageLoss describes the action of losing a message, and Liveness is your intended liveness property.

Often, you can verify the stronger property that liveness holds assuming that messages are received infinitely often (although there may be infinitely many messages lost), writing something like

Spec /\ SF_vars(Receive) => Liveness

For a concrete example, look at the specification of the alternating bit protocol in section 14 of Specifying Systems.

Regards,
Stephan


> On 14 Jul 2016, at 06:58, Gao Neal <gaoni...@xxxxxxxxx> wrote:
> 
> Hi
> I'm modeling a system with message loss/duplication. To check the liveness, I want to be able to specify the message loss/duplication action will eventually never happen. Is there anyway to do this? 
> Many thanks.
> Ning
> 
> -- 
> 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...@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.