1. Define a refinement mapping that somehow shows that, e.g., 1 state transition of the implementation that unblocks N processes, is equivalent to N state transitions in the API spec where the transitions unblock processes one by one.
--
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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/734edefa-87e0-4f29-8cb4-f3d0e71c5672n%40googlegroups.com.
On 6 Sep 2020, at 11:11, Jedd Haberstro <jhabe...@gmail.com> wrote:Hi Stephan,Thanks for the guidance.I do believe a refinement is possible. Wherever the implementation takes an atomic step that is not mandated by the API (i.e. allowed by the API's TLA+ spec), the implementation's spec could be written such that artificial steps are inserted that behave like stuttering steps for all variables except those used in the refinement mapping. There would be as many of these steps inserted into the implementation's behaviour as is necessary for the refinement mapping variables to eventually equal the implementation's actual state while still representing valid state transitions in the the API spec. Do you disagree?
Admittedly, this feels like it would be quite the tedious machinery to tack onto, what I anticipate to be, a non-trivial spec, so I am not keen to go down this path..I think I agree that embracing the fact that several transitions may occur is the correct path forward. As for you specific suggestion, I suppose this would have several implications on how to write the operators that compute the result of the operation:
- No use of prime variables.
- Enabling predicates must be rewritten as IF or CASE expressions.
More importantly, I'm failing to see how to handle multiple primed variables.
Thanks,Jedd
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/26e4fbb6-100d-4d5c-8e23-da31d6d4bbf3n%40googlegroups.com.
Hi Jedd,
This is a very rough sketch and I haven't syntax-checked or polished it, but you could try something like