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). Markus -- 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
