Hi I am trying to develop a system (the steam
boiler problem) by stepwise refinement (as used by B and Event
B) but am having a small problem. I define the most abstract
spec as a TLA+ module
Machine0 and prove its invariants
properties. Then I specify the next module
Machine1
that is to be a refinement of
Machine0.
Can I add Machine0, that is in a separate
specification? The tool reports a warning message attached. I
am not sure if this means you can or can not import this
module but it is subsequently reported as not found.
The only way I have managed to use refinement is by
developing and verifying Machine0 and then starting
again with a new specification for Machine1 and
copying Machine0 into a New Module in the new
specification. I hope there is a better way to do this kind
of development as the next module Machine2 would
require be to copy both Machine1 and Machine0
in as New Modules. Clearly this is going to become problematic
when you have a long chain of refinement steps.
Other than this it does seem possible to encode an Event B
development in TLA+. What might be of interest is that in
Event B they require the developer to say which concrete event
(TLA+ Action) refines which abstract event. This has not
proven to be difficult for engineers to do and, I believe,
would make the evaluation of the refinement steps easier for
TLC and TLAPS.
kind
regards david