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

Re: [tlaplus] TLC and binary temporal operators

A general way of expressing properties that are not obviously expressible using just [] and <> is to specify a state machine expressing the property, then prove that the algorithm implements that state machine. For your example you could write a module along the following lines.

------  MODULE ProcQueue ------ 
EXTENDS Naturals, Sequences


Init == q = <<>>

Req(self) ==
  /\ ~ \E i \in 1 .. Len(q) : q[i] = self
  /\ q’ = Append(q, self)

Grant(self) ==
  /\ q # <<>>
  /\ Head(q) = self
  /\ q’ = Tail(q)

Spec == Init /\ [][\E self \in ProcSet : Req(self) \/ Grant(self)]_q

In the module that contains the specification of your filter algorithm, you then add

FCFS == INSTANCE ProcQueue WITH q <- …

and ask TLC to check the property FCFS!Spec.

The potentially tricky part is to define the substitution for q that computes the queue of waiting processes from the state of the filter algorithm (this is usually called a “refinement mapping”). The idea is that the queue contains the processes that are “in_filter” but not yet “in_cs”. The Req action of ProcQueue corresponds to a process transition from not_in_filter to in_filter in the implementation (or perhaps the first step in case this requires a sequence of transitions), and the Grant action corresponds to the transition leading to process state cs. Since the high-level state machine is explicitly based on a queue, it is obvious that it ensures an FCFS policy.


On 29 Jul 2015, at 19:29, Tim Nelson <tbne...@xxxxxxxxx> 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?

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 http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.