[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] stepwise refinement?

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

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+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

Attachment: Error.png
Description: PNG image