[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

Hi Markus,

thanks for the fast reply.

are you running the Unicode beta of the Toolbox or the regular 1.5.3
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:

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,