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 CONSTANT ProcSet VARIABLE q 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. Regards, Stephan
|