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

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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

Markus

[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.