How can I open .tla files in TLA+ Toolbox?

[James Fisher]

Hi all,

I've fallen at the first hurdle, apparently. I've installed TLA+ Toolbox 1.4.8 on OS X 10.10. I have then downloaded the files accompanying the Specifying Systems book, which includes, for example, /HourClock/HourClock.tla. How do I open this file in TLA+ Toolbox?

The first weirdness is that to open a file I have to choose "Add New Spec ..." which gives me a dialog window that says I am *creating* a spec, not opening one. Is this true, or am I missing something?

The second weirdness is that half the time when I click the "Browse..." button in this dialog, nothing happens.

The third weirdness is that on the times when the "Browse..." dialog does appear, I just get a "spinner" going around and around forever, and no files ever display in the selection pane. (Also, again, the dialog says "Save As" rather than "Open".)

When I run the application from the terminal, I see these stacktraces in the stdout, though they do not obviously correspond to any actions I take in the application:

2014-11-17 20:55:33.445 toolbox[18192:4269848] Cannot remove an observer <FI_TIconViewScrollView 0x100452cb0> for the key path "contentLayoutRect" from <SWTFileSavePanel 0x100357c10> because it is not registered as an observer.
2014-11-17 20:55:33.448 toolbox[18192:4269848] (
0 CoreFoundation 0x00007fff8447164c __exceptionPreprocess + 172
1 libobjc.A.dylib 0x00007fff88e016de objc_exception_throw + 43
2 CoreFoundation 0x00007fff844714fd +[NSException raise:format:] + 205
3 Foundation 0x00007fff8730b666 -[NSObject(NSKeyValueObserverRegistration) _removeObserver:forProperty:] + 604
4 Foundation 0x00007fff8730b369 -[NSObject(NSKeyValueObserverRegistration) removeObserver:forKeyPath:] + 114
5 Foundation 0x00007fff8731aad4 -[NSObject(NSKeyValueObserverRegistration) removeObserver:forKeyPath:context:] + 253
6 AppKit 0x00007fff89c29887 -[NSScrollView _setWindow:] + 342
7 AppKit 0x00007fff89bee3b2 -[NSView removeFromSuperview] + 453
8 AppKit 0x00007fff89df2dd0 -[NSScrollView removeFromSuperview] + 227
9 FinderKit 0x00007fff906b1282 -[FI_TBrowserContainerController destroyBrowserView:] + 176
10 FinderKit 0x00007fff906b4bbd -[FIContainerController destroyBrowserView:] + 84
11 FinderKit 0x00007fff906b0308 -[FI_TBrowserContainerController buildBrowserView:containerState:] + 332
12 FinderKit 0x00007fff906b019f -[FI_TBrowserContainerController buildBrowserView:] + 136
13 FinderKit 0x00007fff906ad62e -[FI_TBrowserContainerController setTargetPath:withViewStyle:rebuildView:] + 1326
14 FinderKit 0x00007fff906ad9ce -[FI_TBrowserContainerController forceSetTargetPath:withViewStyle:] + 85
15 FinderKit 0x00007fff906376d5 -[FIFinderViewGutsController _internalSetTargetPath:withViewStyle:] + 703
16 FinderKit 0x00007fff9063702b -[FIFinderViewGutsController setTargetNode:withViewStyle:] + 515
17 FinderKit 0x00007fff90639f31 -[FIFinderViewGutsController finderLocationPopUp:didChangeToDirectoryURL:] + 136
18 FinderKit 0x00007fff90666670 -[FILocationPopUp setTargetNode:] + 224
19 FinderKit 0x00007fff906668c0 -[FILocationPopUp retargetFromMenuItem:] + 82
20 libsystem_trace.dylib 0x00007fff8e79ecd7 _os_activity_initiate + 75
21 AppKit 0x00007fff89da45e7 -[NSApplication sendAction:to:from:] + 410
22 AppKit 0x00007fff89dbe72a -[NSMenuItem _corePerformAction] + 382
23 AppKit 0x00007fff89dbe447 -[NSCarbonMenuImpl performActionWithHighlightingForItemAtIndex:] + 114
24 libsystem_trace.dylib 0x00007fff8e79ecd7 _os_activity_initiate + 75
25 AppKit 0x00007fff89e0bce6 -[NSMenu performActionForItemAtIndex:] + 131
26 AppKit 0x00007fff89e0bc56 -[NSMenu _internalPerformActionForItemAtIndex:] + 35
27 AppKit 0x00007fff89e0baa2 -[NSCarbonMenuImpl _carbonCommandProcessEvent:handlerCallRef:] + 107
28 AppKit 0x00007fff89db403b NSSLMMenuEventHandler + 724
29 HIToolbox 0x00007fff9280532c _ZL23DispatchEventToHandlersP14EventTargetRecP14OpaqueEventRefP14HandlerCallRec + 1260
30 HIToolbox 0x00007fff9280476e _ZL30SendEventToEventTargetInternalP14OpaqueEventRefP20OpaqueEventTargetRefP14HandlerCallRec + 386
31 HIToolbox 0x00007fff92819286 SendEventToEventTarget + 40
32 HIToolbox 0x00007fff9284e795 _ZL18SendHICommandEventjPK9HICommandjjhPKvP20OpaqueEventTargetRefS5_PP14OpaqueEventRef + 428
33 HIToolbox 0x00007fff92881e8d SendMenuCommandWithContextAndModifiers + 59
34 HIToolbox 0x00007fff92881e34 SendMenuItemSelectedEvent + 188
35 HIToolbox 0x00007fff92881d06 _ZL19FinishMenuSelectionP13SelectionDataP10MenuResultS2_ + 96
36 HIToolbox 0x00007fff929b1bc1 _ZL19PopUpMenuSelectCoreP8MenuData5PointdS1_tjPK4RecttjS4_S4_PK14__CFDictionaryPK10__CFStringPP13OpaqueMenuRefPt + 1877
37 HIToolbox 0x00007fff929b0d44 _ZL26_HandlePopUpMenuSelection8P13OpaqueMenuRefP14OpaqueEventRefj5PointtjPK4RecttS6_S6_PK14__CFDictionaryPK10__CFStringPS0_Pt + 633
38 HIToolbox 0x00007fff929b0edb _HandlePopUpMenuSelectionWithDictionary + 287
39 AppKit 0x00007fff89e0a93c _NSSLMPopUpCarbonMenu3 + 5567
40 AppKit 0x00007fff89e09369 _NSPopUpCarbonMenu3 + 39
41 AppKit 0x00007fff89e09145 -[NSCarbonMenuImpl popUpMenu:atLocation:width:forView:withSelectedItem:withFont:withFlags:withOptions:] + 350
42 AppKit 0x00007fff89e07fe4 -[NSPopUpButtonCell trackMouse:inRect:ofView:untilMouseUp:] + 559
43 AppKit 0x00007fff89e06289 -[NSControl mouseDown:] + 714
44 AppKit 0x00007fff8a2fffef -[NSWindow _reallySendEvent:] + 12827
45 AppKit 0x00007fff89d8a65c -[NSWindow sendEvent:] + 368
46 AppKit 0x00007fff89d3c1e6 -[NSApplication sendEvent:] + 2238
47 libswt-pi-cocoa-3738.jnilib 0x00000001145d6c4a Java_org_eclipse_swt_internal_cocoa_OS_objc_1msgSendSuper__Lorg_eclipse_swt_internal_cocoa_objc_1super_2JJ + 97
48 ??? 0x0000000107811eee 0x0 + 4420869870
)

I am able to open .tla files by constructing the absolute path to them and pasting this into the field in the "Add New Spec ..." dialog. But this is a pain.

So ... is my installation just completely FUBAR, or does anyone else have these issues?

Thanks,

James

[Stephan Merz]

Hello,

the TLA+ Toolbox is based (AFAIK) on Eclipse 3.7, which is no longer supported. I am having the exact same problems that you describe, and they appear to be confirmed (e.g. https://bugs.eclipse.org/bugs/show_bug.cgi?id=420682) with no fixes planned due to the obsolete Eclipse version. I have also taken to manually copy and paste the full file name into the dialog, sigh.

Unfortunately, porting the Toolbox to an up to date version of Eclipse appears to be non-trivial. We hope to have somebody to look at the problem in the near future, as more and more stability problems are bound to appear. Volunteers welcome!

Stephan

> --
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
> To post to this group, send email to tla...@googlegroups.com.
> Visit this group at http://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.

--
Stephan Merz

[Markus Alexander Kuppe]

On 18.11.2014 08:54, Stephan Merz wrote:
> Unfortunately, porting the Toolbox to an up to date version of
> Eclipse appears to be non-trivial. We hope to have somebody to look
> at the problem in the near future, as more and more stability
> problems are bound to appear. Volunteers welcome!

Hi,

I have started porting the toolbox [1] a while ago and used today's
discussion as an impetus to make toolbox builds available [2] that are
based on the most recent Eclipse 4.4.

Consider these builds as highly unstable and likely to wreak havoc on
your computer. Please only use them if you know what you are doing and
want to help overhaul the toolbox. You should have a clear
understanding of how the toolbox is supposed to behave.

Thanks
Markus

[1]
http://tlaplus.codeplex.com/SourceControl/changeset/c7b4a4ce7a491bb3d413faf04e45bf05069d91e4
[2] http://tla.msr-inria.inria.fr/kuppe/e4/products/

[James Fisher]

Hi Markus,

Woohoo! Your build seems to fix the open/save dialog.

It also fixes the awful pixelation I was seeing (possibly something to do with "retina" display). Strangely, the pixelation still appears in a few places though. Here's a screenshot; you can see the pixelation on the field labels "View:", "Depth:", etc: http://i.imgur.com/0S5YJb4.png

Also, the "Spec Status:" has moved from the bottom right to the bottom left-ish.

I'll play around with it some more and report anything odd that I find.

Best wishes,

James