Re: Implementation checking

[Leslie Lamport <tlapl...@xxxxxxxxx>]

TLC has for years had a mode in which it checks that a
behavior satisfies the spec.  (I expect that the states have to be
specified in the restricted subset of TLA+ that TLC uses to write out
traces.)  However, I don't know of it actually being used by any
engineers, so I wonder how useful it is in practice.  However, it
should make implementing what you want to do pretty straightforward.

As for executing a TLC error trace as a spec, that's what the Toolbox does
in the trace explorer.  So the required code is already sitting inside
the Toolbox.

Leslie