Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Existing model no longer opens after spec rename #339

Closed
lemmy opened this issue Jul 18, 2019 · 3 comments
Closed

Existing model no longer opens after spec rename #339

lemmy opened this issue Jul 18, 2019 · 3 comments
Labels
Milestone

Comments

@lemmy
Copy link
Member

@lemmy lemmy commented Jul 18, 2019

If a spec S with a model M is renamed to T, the filename of the model is updated to T_M.launch too. However, renaming does not delete the old model file S_M.launch. The Toolbox subsequently picks up S_M.launch from which it infers the spec name to be S. Since S no longer exists, the Toolbox throws an exception (see below).

The workaround for now is to manually delete any S_M.launch files (including snapshots).

org.eclipse.core.runtime.AssertionFailedException: null argument:Failed to lookup spec with name HashSet
	at org.eclipse.core.runtime.Assert.isNotNull(Assert.java:88)
	at org.lamport.tla.toolbox.tool.tlc.model.Model.getSpec(Model.java:255)
	at org.lamport.tla.toolbox.tool.tlc.model.Model.getFolder(Model.java:958)
	at org.lamport.tla.toolbox.tool.tlc.ui.modelexplorer.ModelLabelProvider.getDescription(ModelLabelProvider.java:103)
	at org.eclipse.ui.internal.navigator.extensions.SafeDelegateCommonLabelProvider.getDescription(SafeDelegateCommonLabelProvider.java:82)
	at org.eclipse.ui.internal.navigator.NavigatorContentServiceDescriptionProvider.getDescription(NavigatorContentServiceDescriptionProvider.java:69)
	at org.eclipse.ui.navigator.CommonNavigatorManager.updateStatusBar(CommonNavigatorManager.java:306)
	at org.eclipse.ui.navigator.CommonNavigatorManager.lambda$0(CommonNavigatorManager.java:70)
	at org.eclipse.jface.viewers.StructuredViewer$3.run(StructuredViewer.java:874)
	at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:45)
	at org.eclipse.ui.internal.JFaceUtil.lambda$0(JFaceUtil.java:47)
	at org.eclipse.jface.util.SafeRunnable.run(SafeRunnable.java:176)
	at org.eclipse.jface.viewers.StructuredViewer.firePostSelectionChanged(StructuredViewer.java:871)
	at org.eclipse.jface.viewers.StructuredViewer.handlePostSelect(StructuredViewer.java:1240)
	at org.eclipse.ui.navigator.CommonViewer.handlePostSelect(CommonViewer.java:460)
	at org.eclipse.jface.viewers.StructuredViewer.lambda$0(StructuredViewer.java:1263)
	at org.eclipse.swt.events.SelectionListener$1.widgetSelected(SelectionListener.java:84)
	at org.eclipse.jface.util.OpenStrategy.firePostSelectionEvent(OpenStrategy.java:264)
	at org.eclipse.jface.util.OpenStrategy.access$5(OpenStrategy.java:259)
	at org.eclipse.jface.util.OpenStrategy$1.lambda$1(OpenStrategy.java:429)
	at org.eclipse.swt.widgets.RunnableLock.run(RunnableLock.java:40)
	at org.eclipse.swt.widgets.Synchronizer.runAsyncMessages(Synchronizer.java:185)
	at org.eclipse.swt.widgets.Display.runAsyncMessages(Display.java:5026)
	at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:4586)
	at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine$5.run(PartRenderingEngine.java:1173)
	at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:339)
	at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine.run(PartRenderingEngine.java:1062)
	at org.eclipse.e4.ui.internal.workbench.E4Workbench.createAndRunUI(E4Workbench.java:156)
	at org.eclipse.ui.internal.Workbench.lambda$3(Workbench.java:628)
	at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:339)
	at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:563)
	at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:151)
	at org.lamport.tla.toolbox.Application.start(Application.java:141)
	at org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:199)
	at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:137)
	at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:107)
	at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:391)
	at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:246)
	at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(Unknown Source)
	at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(Unknown Source)
	at java.base/java.lang.reflect.Method.invoke(Unknown Source)
	at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:659)
	at org.eclipse.equinox.launcher.Main.basicRun(Main.java:595)
	at org.eclipse.equinox.launcher.Main.run(Main.java:1501)
	at org.eclipse.equinox.launcher.Main.main(Main.java:1474)

It is unclear why org.lamport.tla.toolbox.tool.tlc.model.Model.renameLaunch(Spec, String) does not delete the S_M.launch file.

@lemmy lemmy added bug Toolbox labels Jul 18, 2019
@lemmy lemmy added this to the 1.6.1 milestone Jul 18, 2019
@lemmy lemmy changed the title Existing models no longer open after spec rename Existing model no longer opens after spec rename Jul 18, 2019
@lemmy lemmy pinned this issue Jul 19, 2019
@lemmy lemmy unpinned this issue Jul 22, 2019
@lemmy lemmy mentioned this issue Jul 22, 2019
5 of 6 tasks complete
@lemmy

This comment has been minimized.

Copy link
Member Author

@lemmy lemmy commented Aug 2, 2019

When working on this issue (#339), consider fixing #343 and #346.

@quaeler

This comment has been minimized.

Copy link
Collaborator

@quaeler quaeler commented Aug 10, 2019

"Progress" update - the launchConfig.delete() does indeed delete the old launch file - but that old launch file is in S.toolbox, and there is still a copy (for whatever reason) in T.toolbox.

Making sure that the copy in T.toolbox also gets deleted works fine for the first rename. Making a second generation rename, (e.g rename T to U,) fails while attempting to locate a snapshot file which i can plainly see in both T.toolbox and U.toolbox... so: WIP.

quaeler added a commit to quaeler/tlaplus that referenced this issue Aug 11, 2019
- Renaming a specification was not deleting all of the previously-named model launch files
- Also, attempting to fetch snapshots of snapshots was both causing problems in a rename case and was nonsensical, so we now return an empty Collection if the instance's Model.isSnapshot() is true.

tlaplus#339
[Bug][Toolbox]
quaeler added a commit that referenced this issue Aug 11, 2019
- Renaming a specification was not deleting all of the previously-named model launch files
- Also, attempting to fetch snapshots of snapshots was both causing problems in a rename case and was nonsensical, so we now return an empty Collection if the instance's Model.isSnapshot() is true.

#339
[Bug][Toolbox]
@quaeler

This comment has been minimized.

Copy link
Collaborator

@quaeler quaeler commented Aug 11, 2019

Fixed with 7d391f1

@quaeler quaeler closed this Aug 11, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Linked pull requests

Successfully merging a pull request may close this issue.

None yet
2 participants
You can’t perform that action at this time.