TLA+ crashed after building .dot and .pdf file

[david streader]

Hi

     I set TLA+ to build the state graph. Which it successfully  did. But the tool crashed immediately  and could not be started with out crashing until I removed the model from the directory. I am running MacOS 10.14

 

Any help much appreciated 

david

The error  details are:

Process:               toolbox [4252]

Path:                  /Applications/TLA+ Toolbox.app/Contents/MacOS/toolbox

Identifier:            org.lamport.tla.toolbox.product.product

Version:               1.6.0 (1.6.0.201907102009)

Code Type:             X86-64 (Native)

Parent Process:        ??? [1]

Responsible:           toolbox [4252]

User ID:               501

Date/Time:             2020-02-17 19:08:51.621 +1300

OS Version:            Mac OS X 10.14.6 (18G3020)

Report Version:        12

Anonymous UUID:        D45FAF0A-6EDB-322F-EAA2-7076B9534619

Sleep/Wake UUID:       9C41179A-9F88-482E-A99A-377453D33504

Time Awake Since Boot: 34000 seconds

Time Since Wake:       4700 seconds

System Integrity Protection: enabled

Crashed Thread:        58

Exception Type:        EXC_BAD_ACCESS (SIGABRT)

Exception Codes:       KERN_INVALID_ADDRESS at 0x00000000000000c0

Exception Note:        EXC_CORPSE_NOTIFY

VM Regions Near 0xc0:

--> 

    __TEXT                 00000001042ca000-00000001042ce000 [   16K] r-x/rwx SM=COW  /Applications/TLA+ Toolbox.app/Contents/MacOS/toolbox

Application Specific Information:

abort() called

......

Thread 58 Crashed:

0   libsystem_kernel.dylib        0x00007fff6291a2c2 __pthread_kill + 10

1   libsystem_pthread.dylib        0x00007fff629d5bf1 pthread_kill + 284

2   libsystem_c.dylib              0x00007fff628846a6 abort + 127

3   libjvm.dylib                  0x0000000107b4e38a os::abort(bool, void*, void const*) + 22

4   libjvm.dylib                  0x0000000107cb253e VMError::report_and_die(int, char const*, char const*, __va_list_tag*, Thread*, unsigned char*, void*, void*, char const*, int, unsigned long) + 2806

5   libjvm.dylib                  0x0000000107cb1a33 VMError::report_and_die(Thread*, unsigned int, unsigned char*, void*, void*, char const*, ...) + 169

6   libjvm.dylib                  0x0000000107cb258b VMError::report_and_die(Thread*, unsigned int, unsigned char*, void*, void*) + 33

7   libjvm.dylib                  0x0000000107cb2fca crash_handler(int, __siginfo*, void*) + 184

8   libsystem_platform.dylib      0x00007fff629cab5d _sigtramp + 29

9   ???                            0x0000000000000031 0 + 49

10  libjvm.dylib                  0x0000000107c65391 ThreadsListHandle::ThreadsListHandle(Thread*) + 39

11  libjvm.dylib                  0x0000000107b4b039 os::print_location(outputStream*, long, bool) + 585

12  libjvm.dylib                  0x0000000107cb08bf VMError::report(outputStream*, bool) + 3995

13  libjvm.dylib                  0x0000000107cb201a VMError::report_and_die(int, char const*, char const*, __va_list_tag*, Thread*, unsigned char*, void*, void*, char const*, int, unsigned long) + 1490

14  libjvm.dylib                  0x0000000107cb1a33 VMError::report_and_die(Thread*, unsigned int, unsigned char*, void*, void*, char const*, ...) + 169

15  libjvm.dylib                  0x0000000107cb258b VMError::report_and_die(Thread*, unsigned int, unsigned char*, void*, void*) + 33

16  libjvm.dylib                  0x0000000107cb2fca crash_handler(int, __siginfo*, void*) + 184

17  libsystem_platform.dylib      0x00007fff629cab5d _sigtramp + 29

18  ???                            0x0000000000000008 0 + 8

19  libjvm.dylib                  0x0000000107c65391 ThreadsListHandle::ThreadsListHandle(Thread*) + 39

20  libjvm.dylib                  0x0000000107b4b039 os::print_location(outputStream*, long, bool) + 585

21  libjvm.dylib                  0x0000000107b52d84 os::print_register_info(outputStream*, void const*) + 82

22  libjvm.dylib                  0x0000000107cb07a9 VMError::report(outputStream*, bool) + 3717

23  libjvm.dylib                  0x0000000107cb201a VMError::report_and_die(int, char const*, char const*, __va_list_tag*, Thread*, unsigned char*, void*, void*, char const*, int, unsigned long) + 1490

24  libjvm.dylib                  0x0000000107cb1a33 VMError::report_and_die(Thread*, unsigned int, unsigned char*, void*, void*, char const*, ...) + 169

25  libjvm.dylib                  0x0000000107cb258b VMError::report_and_die(Thread*, unsigned int, unsigned char*, void*, void*) + 33

26  libjvm.dylib                  0x0000000107b52571 JVM_handle_bsd_signal + 889

27  libjvm.dylib                  0x0000000107b4fdeb signalHandler(int, __siginfo*, void*) + 45

28  libsystem_platform.dylib      0x00007fff629cab5d _sigtramp + 29

29  ???                            0x00006000011c4f00 0 + 105553134898944

30  com.adobe.acrobat.pdfviewer    0x000000012287d4d3 0x122865000 + 99539

31  com.adobe.acrobat.pdfviewer    0x0000000122867380 0x122865000 + 9088

32  com.adobe.acrobat.pdfviewer    0x0000000122867224 0x122865000 + 8740

33  com.apple.Foundation          0x00007fff38ab30e2 __NSThread__start__ + 1194

34  libsystem_pthread.dylib        0x00007fff629d32eb _pthread_body + 126

35  libsystem_pthread.dylib        0x00007fff629d6249 _pthread_start + 66

36  libsystem_pthread.dylib        0x00007fff629d240d thread_start + 13

Thread 58 crashed with X86 Thread State (64-bit):

  rax: 0x0000000000000000  rbx: 0x00007000035a7000  rcx: 0x00007000035a4b68  rdx: 0x0000000000000000

  rdi: 0x0000000000016f17  rsi: 0x0000000000000006  rbp: 0x00007000035a4ba0  rsp: 0x00007000035a4b68

   r8: 0x00000000000130a8   r9: 0x00007fff98f57f78  r10: 0x0000000000000000  r11: 0x0000000000000206

  r12: 0x0000000000016f17  r13: 0x00007000035a4e00  r14: 0x0000000000000006  r15: 0x000000000000002d

  rip: 0x00007fff6291a2c2  rfl: 0x0000000000000206  cr2: 0x00007fff98f56188

  

Logical CPU:     0

Error Code:      0x02000148

Trap Number:     133

[Markus Kuppe]

Hi David,

this appears to be a duplicate of
https://github.com/tlaplus/tlaplus/issues/357. Can you check if the
workaround in
https://github.com/tlaplus/tlaplus/issues/357#issuecomment-535770396
prevents the Toolbox from crashing?

Thanks
Markus

[david streader]

Sorry I should have said. I read the post and yes it looks very much the same  but  the work round

sudo rm -rf /Library/Internet\ Plug-Ins\AdobePDFViewer*

did not work.  But from rereading the post I downloaded the nightly build TLAToolbox-1.6.1-macosx.cocoa.x86_64.zip 

and it still crashed. david

[Markus Kuppe]

On 17.02.20 12:41, david streader wrote:
> Sorry I should have said. I read the post and yes it looks very much the
> same  but  the work round
>
> sudo rm -rf /Library/Internet\ Plug-Ins\AdobePDFViewer*
>
> did not work.  But from rereading the post I downloaded the nightly
> build TLAToolbox-1.6.1-macosx.cocoa.x86_64.zip 
> and it still crashed. david

Hi David,

until we figure out what the root cause for the crash is, please note
that you can manually generate and open the state graph:

On the Toolbox's TLC options page, add "-dump dot StateGraph.dot" into
"TLC command line parameters" (make sure to uncheck "Visualize state
graph..." to prevent the Toolbox crash). Check the model and open
StateGraph.dot with e.g. xdot (see the attached gif).

Thanks
Markus

PS: xdot and graphviz are part of homebrew.