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
> --
> 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 post to this group, send email to
tla...@googlegroups.com.
> Visit this group at
https://groups.google.com/group/tlaplus.
> For more options, visit
https://groups.google.com/d/optout.