Hi Ernie,
the hidden state can change in many different ways
(any pending transaction might execute atomically in any step),
so you can't just delete the temporal existential quantifier and get
a witnessed model to check;
Any canonical TLA+ specification (initial predicate, next-state
relation, plus fairness) can, in principle, be model checked in
exactly this way. Whether or not model checking is possible for a
large enough model to be useful depends on the nature of the spec. I
don't think I've ever encountered a real TLA+ spec, written in
canonical form, that couldn't be at least simulated--checked on
randomly generated behaviors. Of course, I'm talking here about
checking the spec, not checking that something implements the spec.
Even though a spec may allow too many behaviors for a model checker to
deal with, it is often possible for a model checker to do useful
checking that an implementation satisfies the spec. That's because
only behaviors that satisfy the implementation have to be checked, not
all behaviors that satisfy the spec.
you have to write a witnessing formula, which requires
understanding why the protocol works
You have to do that for any method of verifying behavioral properties
specified with internal (hidden) variables. And those are the only
general methods I know of that provide practical methods of verifying
arbitrary behavioral properties. Putting a monkey at a keyboard who
has no idea why the program he's writing might work may be common
practice, and it might be satisfactory for programs that compute an
answer and are easy to test, but it doesn't work too well for
protocols.
Moreover, even for strict serializability, this instantiation might
require prophecy, which you can't put directly into a TLC model
(though I assume you can code it up by choosing the right property to
check).
This is unavoidable, unless you write the specification for the
explicit purpose of verifying your particular implementation. With
the obvious specifications of serializability that require recording
the entire history, the use of auxiliary variables will almost always
be necessary. With my spec of serializability, I used able to verify
safety of the lazy caching algorithm without a prophecy variable. (I
needed a prophecy variable predicting whether or not something
eventually happened for proving liveness.) In fact, the "witness
formula" (which in the TLA world and other places is called a
refinement mapping), provided a lovely, easy to understand explanation
of why the algorithm works. I don't know if the same will be true for
other implementations of serializability, but I have a hunch that it
will.
Cheers,
Leslie