I suggest that you use something like this definition instead:FirstComeFirstServed ==
(\A self \in ProcSet: \A other \in ProcSet :
((pc[self] = "in_filter" /\
pc[other] = "not_in_filter") /\ (pc[self] /= "in_cs")
(pc[other] /= "in_cs")))It's not equivalent to your definition, but if you think about it, youshould realize that the two are equivalent for any safety spec of a system
that can't predict the future. (A safety spec allows the system to stoptaking steps at any point.)
On Wednesday, July 29, 2015 at 10:29:28 AM UTC-7, Tim Nelson wrote:I'm getting started with TLA+ and TLC, and exercising myself by verifying (orfalsifying!) properties about simple locking algorithms like Peterson andfilter. "First-Come, First-Served" (FCFS) is on the list, and I'd like tocheck it in TLC.My trouble is that FCFS wants the Until temporal operator, which TLA doesn'tinclude. I can express FCFS using the -+-> operator (where F -+-> G true if Gholds at least one step longer than F) but I then get the error "TLC cannothandle the temporal formula...". I was using something like this:FirstComeFirstServed ==(\A self \in ProcSet: \A other \in ProcSet :((pc[self] = "in_filter" /\pc[other] = "not_in_filter") =>(pc[other] /= "in_cs" -+-> pc[self] = "in_cs")))What is the preferred way to check a property like FCFS in TLC? Moregenerally, what should I try first when I come up against something that seemsto need a binary LTL operator?