[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 22:13, Markus Kuppe wrote:
> 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).

Hi David,

this screencast [1] shows how to refine specs in different folders
(without symlinks).


[1] https://tla.msr-inria.inria.fr/kuppe/RefinementNoSymlinksToolbox.gif

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/265bdfbb-db82-6980-452e-0e4277824259%40lemmster.de.