Re: [tlaplus] Êrror-Trace Exploration not working

[Markus Alexander Kuppe <tlaplus-go...@xxxxxxxxxxx>]

On 24.08.2017 17:25, Christian Spann wrote:
> But I cannot find where the path is stored to edit the location.  If I copy the tla file and create a new spec everything is fine, but it is cumbersome to recreate the model values by hand... So my questions are:
>
> 1. Where is the location of modules for a spec stored or how it is calculated - adding a library location to the spec does not fix the error.
> 2. How can I remove a module from a spec which was added by hand.

Hi Christian,

1. FiniteSets.tla is most likely referenced from
C:\dev\tla\tlamodels\EbawaNative.toolbox\.project. Try removing the
FiniteSets.tla related link-stanza from .project while the Toolbox is
_not_ running. FiniteSets should be gone upon the next Toolbox start-up.

By the way, am I right that your TLA+ library path in the Toolbox
preferences contains the TLAPS installation?

2. I'm not sure what you mean by "added by hand"? Anyway, you have to
remove the module manually similarly to what I describe in 1. or
re-create the specification from scratch without the module.

Thanks

Markus