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

Re: TLC and binary temporal operators



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, you
should 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 stop
taking steps at any point.)

Leslie


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 (or
falsifying!) properties about simple locking algorithms like Peterson and
filter. "First-Come, First-Served" (FCFS) is on the list, and I'd like to
check it in TLC.

My trouble is that FCFS wants the Until temporal operator, which TLA doesn't
include. I can express FCFS using the -+-> operator (where F -+-> G true if G
holds at least one step longer than F) but I then get the error "TLC cannot
handle 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? More
generally, what should I try first when I come up against something that seems
to need a binary LTL operator?