specifying systems book, Figure 3.1 -- bug? -- seems impossible to receive in AsyncInterface

[j.e....@gmail.com]

On page 27/Section 3.1 of

http://research.microsoft.com/en-us/um/people/lamport/tla/book-02-08-08.pdf

the book "Specifying Systems", there is a spec for AsynchInterface in Figure 3.1.

It seems to me that the interface contains an error because it can never Receive, due to the assertion that "ack = rdy" in the Init definition. The definition of Rcv requires that rdy != ack. Since the Spec insists that Init always hold, it would be impossible to ever have Rcv hold, no?

To fix this, I suppose one could either remove the ack = rdy from the Init definition, or say Spec = Init \/ [Next]_<val,rdy,ack> -- using an OR instead of an AND, but neither of these seems fully satisfactory, since they loosen the spec substantially.

[Stephan Merz]

I don't understand your argument.

As you have observed, the Rcv action is not enabled in the initial state because ack = rdy. But the Send action is enabled, and it will flip the rdy bit. This will in turn enable the Rcv action (and in fact disable Send).

This disproves your claim that the receive action can never occur. In fact, the specification forces Send and Rcv to alternate (with stuttering transitions occurring in between). The specification does not assert that the Init always holds: formula Spec asserts that Init holds initially and that every non-stuttering transition satisfies Next. Perhaps you have been confused by the meaning of the "always" operator of temporal logic?

Regards,
Stephan

> --
> 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...@googlegroups.com.
> To post to this group, send email to tla...@googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.

[Leslie Lamport]

Jason Aten's confusion was caused by a sensible literal reading of the definition of the specification, if one is unfamiliar with temporal logic.  This problem was compounded by a poor choice of example in Chapter 2 of "Specifying Systems".  I have been in contact with him and I expect he will see what's going on.

Leslie

[Jonathan Ostroff]

I have written a binary search algorithm with two modules as shown below. Both modules appear to parse and the BinarySearch seems to translate without errors.

\* BEGIN TRANSLATION …. …. …. 

Spec == /\ Init /\ [][Next]_vars

        /\ WF_vars(Next)

Termination == <>(pc = "Done")

\* END TRANSLATION

However, when selecting TLC-Model-Checker —> new Module, the No Behaviour-Spec button is selected, and the Temporal Formula button cannot be selected for Spec. So I cannot check the model.

This has not happened with other algorithms so I am wondering what I did wrong?

(Also, any help on writing the specifications for this algorithm would be appreciated).

Thanks

Jonathan

===============

------------------------ MODULE BinarySearchContext ------------------------

EXTENDS Sequences, Integers

  IsSorted(s)  == \A i,j \in DOMAIN s: i <= j => s[i] <= s[j] 

  SortedSeq(s) == { seq \in Seq(s) : IsSorted(seq) }

  Range(f) == { f[x] : x \in DOMAIN f }

  SortedSeqN(s,N) == UNION { { seq \in [ 1..n -> s ] : IsSorted(seq) } : n \in 1..N }

  N == 7

  Vals == 0..N+1

  SmallSortedS == { seq \in SortedSeqN(1..N,N) : seq[1] = 1 }

=============================================================================

PlusCal options (-termination)

---------------------------- MODULE BinarySearch ----------------------------

EXTENDS  BinarySearchContext, Integers, TLC

(***************************************************************************

--algorithm BinarySearch

variables 

      f \in SmallSortedS

    , v \in Vals \* target

    , p = 1, q = Len(f)

    , mid = -2

    , r = 0

    , found = FALSE

begin

    if v <= f[q] then

        while p <= q and ~found do

            mid := (p+q) \div 2;

            if v = f[mid] then

                r := mid[f];

                found := TRUE;

            elsif v > f[mid] then

                p := mid + 1

            else

                q := mid - 1

            end if;

        end while;

    end if;

    print v;

    assert (v \in Range(f) => r \in DOMAIN f /\ f[r] = v) ;

    assert (r = 0 <=> ~ v \in Range(f)) ;    

end algorithm 

***************************************************************************)

[Jonathan Ostroff]

To answer my own question, the first module to be defined appears to be the root module. So I needed to start the specification with BinarySearch.tla not the context module (even though the dependency is the other way). Any hints on how to improve on the specifications still appreciated. 

Jonathan

=============================

        while p <= q /\ ~found do

[Stephan Merz]

Hi Jonathan,

you already found out about the problem of what is the root module.

Your spec contained a few infelicities, such as "mid[f]", which should in fact have been "mid" or a confusion of r and v in the first assertion. I also suggest you make N a parameter that you instantiate in your model rather than defining it in the context module. The result is attached (don't forget to translate the PlusCal algorithm before running TLC), and it seems to work based on the few tests that I made.

Regards,

Stephan