[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

specify some action eventually will never happen

From: Gao Neal <gaoni...@xxxxxxxxx>
Date: Wed, 13 Jul 2016 21:58:44 -0700 (PDT)

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

Follow-Ups:
- Re: [tlaplus] specify some action eventually will never happen
  - From: Stephan Merz

Prev by Date: Any examples of a specification of an S3-like object store API?
Next by Date: Re: [tlaplus] specify some action eventually will never happen
Previous by thread: Re: Any examples of a specification of an S3-like object store API?
Next by thread: Re: [tlaplus] specify some action eventually will never happen
Index(es):
- Date
- Thread