TLA+ crashed after building .dot and .pdf file

35 views
Skip to first unread message

david streader

unread,
Feb 17, 2020, 1:34:16 AM2/17/20
to tlaplus
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

unread,
Feb 17, 2020, 1:15:50 PM2/17/20
to tla...@googlegroups.com
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

unread,
Feb 17, 2020, 3:41:32 PM2/17/20
to tlaplus
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

unread,
Feb 17, 2020, 7:32:39 PM2/17/20
to tla...@googlegroups.com
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.
StateGraphManualXDot.gif
Reply all
Reply to author
Forward
0 new messages