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
