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

[Christian Spann <cspanns....@xxxxxxxxx>]

Hi Markus,

thanks for the fast reply.

> are you running the Unicode beta of the Toolbox or the regular 1.5.3
> release?
I am using regular 1.5.3
> Can you share the spec and model (if necessary privately) that
> cause the problem?
I could but I think I found the problem.
> Does the Toolbox's .log file indicate as to what is happening? The .log
> file is located in the Toolbox's workspace/.metadata/ directory, which
> is normally located inside the Toolbox installation directory.
Yes it does. The problem is, that the path to the FiniteSets.tla module is broken in the Project/Spec. The Error when I double click the file is:

> File not found: C:\dev\tla\tlamodels\EbawaNative.toolbox\FiniteSets.tla.


The error in the .log file when exploring the error trace is:
> !STACK 1
>
> org.eclipse.core.internal.resources.ResourceException: Problems encountered while copying resources.
>
>     at org.eclipse.core.internal.localstore.FileSystemResourceManager.copy(FileSystemResourceManager.java:316)
>
>     at org.eclipse.core.internal.resources.Resource.copy(Resource.java:551)
>
>     at org.lamport.tla.toolbox.tool.tlc.util.ModelHelper.copyExtendedModuleFiles(ModelHelper.java:1002)
>
>     at org.lamport.tla.toolbox.tool.tlc.launch.TraceExplorerDelegate.buildForLaunch(TraceExplorerDelegate.java:394)
>
>     at org.eclipse.debug.internal.core.LaunchConfiguration.launch(LaunchConfiguration.java:855)
>
>     at org.eclipse.debug.internal.core.LaunchConfiguration.launch(LaunchConfiguration.java:739)
>
>     at org.lamport.tla.toolbox.tool.tlc.model.Model.launch(Model.java:856)
>
>     at org.lamport.tla.toolbox.tool.tlc.traceexplorer.TraceExplorerComposite$5.runInWorkspace(TraceExplorerComposite.java:468)
>
>     at org.eclipse.core.internal.resources.InternalWorkspaceJob.run(InternalWorkspaceJob.java:39)
>
>     at org.eclipse.core.internal.jobs.Worker.run(Worker.java:55)
>
> Contains: Resource '/EbawaNative/FiniteSets.tla' does not exist.


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.

Best regards,
Christian