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

Re: [tlaplus] Best practice when building a series of model refinements?

On 26.02.20 19:34, david streader wrote:
>     Following the common methodology of B and Event B I want to build a
> series of ever more complex models each a refinement of the later. 
> Does TCL only work on the Root module in a directory or can I build
> models of any module in a directory?
> Last year I used symbolic links so as not to have copies of one module
> in different directories but now symbolic links do not appear to be
> recognised.
> Is best practice to build a series of directories each with a different
> Root-module but containing a copies of the more abstract modules that
> the Root module refines?  Or have I missed some thing? david

Hi David,

lets assume HashSet refines ArraySet refines Set.   Set.tla,
ArraySet.tla, and HashSet.tla are all located in the same (OS)
directory.  In the Toolbox, however, add a dedicated spec HashSet,
ArraySet, and Set to model check each one of them (see screenshot).


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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c5ee479f-fc7f-1e67-c99f-cb36b722cdc0%40lemmster.de.

Attachment: Screenshot from 2020-02-26 22-01-19.png
Description: PNG image