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

[Gao Neal <gaoni...@xxxxxxxxx>]

On Thursday, July 14, 2016 at 1:31:47 AM UTC-6, Stephan Merz wrote:
> 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.

Thanks a lot. This works for me.