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

[Shiyao MA <i@xxxxxxxxx>]

Hi Markus,

Could you post the source of the set, arrayset, and hashset.

Refinement is relatively opaque to me.  I'd like to know what role "refinement" plays here.

On Friday, 28 February 2020 09:34:15 UTC+8, Markus Alexander Kuppe wrote:

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/8c134272-a33a-4041-a827-424448f8a658%40googlegroups.com.