On Thursday, November 13, 2014 1:09:16 AM UTC-8, Markus Alexander Kuppe wrote:
On 12.11.2014 00:28, chri...@xxxxxxxxx wrote:
>
> Hi Chris,
>
> can you share the disk content¹ of your spec/model including the nested
> *.toolbox directory? Then I can (locally) debug why TLC won't run on
> it.
>
> Cheers
> Markus
>
> ¹ The path is shown at the top of the spec editor.
>
>
> Attached.
Hi Chris,
all four Euclid models can be successfully checked with TLC here. The
only parts I had to adapt are the mappings to TLAPS' standard modules
(I'm on Linux).
Is there anything helpful in the .log file located in the Toolbox's
installation directory under workspace/.metadata/?
Markus
Hi Markus, it looks to me like maybe there is some sort of naming case problem. It complains about GCD resource exists with different case gcd. I may have started development with it called GCD and renamed it so it may have cached this version of the name somewhere. I can't see anywhere in the current version of the files that calls the module GCD, though the gcd module does contain a GCD definition.
I tried deleting the gcd and euclid_pluscal toolbox and tlaps dirs and it worked after I deleted the euclid_pluscal dirs.
Regards,
Chris.
Logs below.
!ENTRY org.lamport.tla.toolbox 4 0 2014-11-13 10:38:17.053
!MESSAGE Error creating resource link to C:\work\docs\tla\gcd.tla
!STACK 1
org.eclipse.core.internal.resources.ResourceException: A resource exists with a different case: '/euclid_pluscal/GCD.tla'.
at org.eclipse.core.internal.resources.Resource.checkDoesNotExist(Resource.java:308)
at org.eclipse.core.internal.resources.Resource.assertLinkRequirements(Resource.java:155)
at org.eclipse.core.internal.resources.Resource.createLink(Resource.java:649)
at org.eclipse.core.internal.resources.Resource.createLink(Resource.java:623)
at org.lamport.tla.toolbox.util.ResourceHelper.getLinkedFile(ResourceHelper.java:383)
at org.lamport.tla.toolbox.spec.parser.ModuleParserLauncher.parseModule(ModuleParserLauncher.java:317)
at org.lamport.tla.toolbox.spec.parser.ModuleParserLauncher.parseModule(ModuleParserLauncher.java:84)
at org.lamport.tla.toolbox.spec.parser.ModuleParserLauncher.parseModule(ModuleParserLauncher.java:57)
at org.lamport.tla.toolbox.spec.parser.SpecificationParserLauncher.parseSpecification(SpecificationParserLauncher.java:38)
at org.lamport.tla.toolbox.spec.nature.ParserHelper$2.run(ParserHelper.java:75)
at org.eclipse.core.internal.resources.Workspace.run(Workspace.java:2344)
at org.eclipse.core.internal.resources.Workspace.run(Workspace.java:2326)
at org.lamport.tla.toolbox.spec.nature.ParserHelper.rebuildSpec(ParserHelper.java:84)
at org.lamport.tla.toolbox.spec.nature.TLAParsingBuilder.build(TLAParsingBuilder.java:81)
at org.eclipse.core.internal.events.BuildManager$2.run(BuildManager.java:728)
at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:42)
at org.eclipse.core.internal.events.BuildManager.basicBuild(BuildManager.java:199)
at org.eclipse.core.internal.events.BuildManager.basicBuild(BuildManager.java:239)
at org.eclipse.core.internal.events.BuildManager$1.run(BuildManager.java:292)
at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:42)
at org.eclipse.core.internal.events.BuildManager.basicBuild(BuildManager.java:295)
at org.eclipse.core.internal.events.BuildManager.basicBuildLoop(BuildManager.java:351)
at org.eclipse.core.internal.events.BuildManager.build(BuildManager.java:374)
at org.eclipse.core.internal.events.AutoBuildJob.doBuild(AutoBuildJob.java:143)
at org.eclipse.core.internal.events.AutoBuildJob.run(AutoBuildJob.java:241)
at org.eclipse.core.internal.jobs.Worker.run(Worker.java:54)
!SUBENTRY 1 org.eclipse.core.resources 4 275 2014-11-13 10:38:17.054
!MESSAGE A resource exists with a different case: '/euclid_pluscal/GCD.tla'.
!ENTRY org.lamport.tla.toolbox 1 -1 2014-11-13 10:38:17.071
!MESSAGE Resulting status is: parsed
... build invocation finished.
!ENTRY org.lamport.tla.toolbox.tool.tlc.ui 4 0 2014-11-13 10:38:17.807
!MESSAGE Error launching the configuration euclid_pluscal___Model_3
!STACK 1
org.eclipse.core.internal.resources.ResourceException: Resource '/euclid_pluscal/gcd.tla' does not exist.
at org.eclipse.core.internal.resources.Resource.checkExists(Resource.java:320)
at org.eclipse.core.internal.resources.Resource.checkAccessible(Resource.java:194)
at org.eclipse.core.internal.resources.Resource.checkAccessibleAndLocal(Resource.java:200)
at org.eclipse.core.internal.resources.Resource.checkCopyRequirements(Resource.java:232)
at org.eclipse.core.internal.resources.Resource.assertCopyRequirements(Resource.java:139)
at org.eclipse.core.internal.resources.Resource.copy(Resource.java:540)
at org.lamport.tla.toolbox.tool.tlc.launch.TLCModelLaunchDelegate.buildForLaunch(TLCModelLaunchDelegate.java:294)
at org.eclipse.debug.internal.core.LaunchConfiguration.launch(LaunchConfiguration.java:822)
at org.eclipse.debug.internal.core.LaunchConfiguration.launch(LaunchConfiguration.java:703)
at org.lamport.tla.toolbox.tool.tlc.ui.editor.ModelEditor.launchModel(ModelEditor.java:688)
at org.lamport.tla.toolbox.tool.tlc.ui.editor.page.BasicFormPage.doRun(BasicFormPage.java:783)
at org.lamport.tla.toolbox.tool.tlc.ui.editor.page.BasicFormPage$RunAction.run(BasicFormPage.java:858)
at org.eclipse.jface.action.Action.runWithEvent(Action.java:498)
at org.eclipse.jface.action.ActionContributionItem.handleWidgetSelection(ActionContributionItem.java:584)
at org.eclipse.jface.action.ActionContributionItem.access$2(ActionContributionItem.java:501)
at org.eclipse.jface.action.ActionContributionItem$6.handleEvent(ActionContributionItem.java:452)
at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:84)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1053)
at org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:4165)
at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3754)
at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2696)
at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2660)
at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2494)
at org.eclipse.ui.internal.Workbench$7.run(Workbench.java:674)
at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)
at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:667)
at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
at org.lamport.tla.toolbox.Application.start(Application.java:41)
at org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:196)
at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)
at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)
at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:344)
at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(Unknown Source)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(Unknown Source)
at java.lang.reflect.Method.invoke(Unknown Source)
at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:622)
at org.eclipse.equinox.launcher.Main.basicRun(Main.java:577)
at org.eclipse.equinox.launcher.Main.run(Main.java:1410)
!SUBENTRY 1 org.eclipse.core.resources 4 368 2014-11-13 10:38:18.250
!MESSAGE Resource '/euclid_pluscal/gcd.tla' does not exist.
!ENTRY org.lamport.tla.toolbox 1 -1 2014-11-13 10:38:18.295
!MESSAGE Spec build invoked on euclid_pluscal ...
!ENTRY org.lamport.tla.toolbox 4 0 2014-11-13 10:38:19.437
!MESSAGE Error creating resource link to C:\work\docs\tla\gcd.tla
!STACK 1
org.eclipse.core.internal.resources.ResourceException: A resource exists with a different case: '/euclid_pluscal/GCD.tla'.
at org.eclipse.core.internal.resources.Resource.checkDoesNotExist(Resource.java:308)
at org.eclipse.core.internal.resources.Resource.assertLinkRequirements(Resource.java:155)
at org.eclipse.core.internal.resources.Resource.createLink(Resource.java:649)
at org.eclipse.core.internal.resources.Resource.createLink(Resource.java:623)
at org.lamport.tla.toolbox.util.ResourceHelper.getLinkedFile(ResourceHelper.java:383)
at org.lamport.tla.toolbox.spec.parser.ModuleParserLauncher.parseModule(ModuleParserLauncher.java:317)
at org.lamport.tla.toolbox.spec.parser.ModuleParserLauncher.parseModule(ModuleParserLauncher.java:84)
at org.lamport.tla.toolbox.spec.parser.ModuleParserLauncher.parseModule(ModuleParserLauncher.java:57)
at org.lamport.tla.toolbox.spec.parser.SpecificationParserLauncher.parseSpecification(SpecificationParserLauncher.java:38)
at org.lamport.tla.toolbox.spec.nature.ParserHelper$2.run(ParserHelper.java:75)
at org.eclipse.core.internal.resources.Workspace.run(Workspace.java:2344)
at org.eclipse.core.internal.resources.Workspace.run(Workspace.java:2326)
at org.lamport.tla.toolbox.spec.nature.ParserHelper.rebuildSpec(ParserHelper.java:84)
at org.lamport.tla.toolbox.spec.nature.TLAParsingBuilder.build(TLAParsingBuilder.java:81)
at org.eclipse.core.internal.events.BuildManager$2.run(BuildManager.java:728)
at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:42)
at org.eclipse.core.internal.events.BuildManager.basicBuild(BuildManager.java:199)
at org.eclipse.core.internal.events.BuildManager.basicBuild(BuildManager.java:239)
at org.eclipse.core.internal.events.BuildManager$1.run(BuildManager.java:292)
at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:42)
at org.eclipse.core.internal.events.BuildManager.basicBuild(BuildManager.java:295)
at org.eclipse.core.internal.events.BuildManager.basicBuildLoop(BuildManager.java:351)
at org.eclipse.core.internal.events.BuildManager.build(BuildManager.java:374)
at org.eclipse.core.internal.events.AutoBuildJob.doBuild(AutoBuildJob.java:143)
at org.eclipse.core.internal.events.AutoBuildJob.run(AutoBuildJob.java:241)
at org.eclipse.core.internal.jobs.Worker.run(Worker.java:54)
!SUBENTRY 1 org.eclipse.core.resources 4 275 2014-11-13 10:38:19.443
!MESSAGE A resource exists with a different case: '/euclid_pluscal/GCD.tla'.
!ENTRY org.lamport.tla.toolbox 1 -1 2014-11-13 10:38:19.494
!MESSAGE Resulting status is: parsed
... build invocation finished.
!ENTRY org.lamport.tla.toolbox 1 -1 2014-11-13 10:38:26.029
!MESSAGE Removed a parse result listener.There are now 0 listeners.