search

mCRL2org / mCRL2

The Git repository for the mCRL2 toolset.
https://mcrl2.org/
Boost Software License 1.0
88 stars 36 forks source link

Assertion failure in ATmakeAFun using lps2lts #1009

Closed jgroote closed 12 years ago

jgroote commented 12 years ago

Issue migrated from trac ticket # 1007

component: lps2lts | priority: blocker | resolution: fixed

2012-03-27 18:52:15: @jkeiren created the issue

Using r10420 I get the following assertion failure, when generating the state space of examples/industrial/garage/garage-ver.mcrl2.

lps2lts -vrjittyc garage-ver.lps bla.aut
[Thread debugging using libthread_db enabled]
[18:44:23 verbose] Detected Aldebaran extension.
[18:44:25 verbose] removing unused parts of the data specification.
[18:44:26 verbose] using 'mcrl2compilerewriter' to compile rewriter.
[18:44:30 verbose] compiling rewriter...
[18:44:37 verbose] loading rewriter...
[18:44:37 verbose] writing state space in AUT format to 'bla.aut'.
[18:44:37 verbose] generating state space with 'breadth' strategy...
[18:44:38 verbose] monitor: level 1 done. (1 state, 49 transitions)
[18:44:52 verbose] monitor: level 2 done. (11 states, 564 transitions)
lps2lts: /data/projects/mcrl2/src/libraries/aterm/source/afun.cpp:316: AFun aterm::ATmakeAFun(const char *, const size_t, const bool): Assertion `free_entry<=at_lookup_table.size()' failed.

Program received signal SIGABRT, Aborted.

Backtrace:


0x00002aaaad2493a5 in __GI_raise (sig=6)
    at ../nptl/sysdeps/unix/sysv/linux/raise.c:64
64  ../nptl/sysdeps/unix/sysv/linux/raise.c: No such file or directory.
    in ../nptl/sysdeps/unix/sysv/linux/raise.c
(gdb) bt
#0  0x00002aaaad2493a5 in __GI_raise (sig=6)
    at ../nptl/sysdeps/unix/sysv/linux/raise.c:64
#1  0x00002aaaad24cb0b in __GI_abort () at abort.c:92
#2  0x00002aaaad241d4d in __GI___assert_fail (
    assertion=0x2aaaac898223 "free_entry<=at_lookup_table.size()", 
    file=<optimized out>, line=316, function=<optimized out>) at assert.c:81
#3  0x00002aaaac88ba54 in aterm::ATmakeAFun (name=0xbc9cd8 "@x@15636", 
    arity=0, quoted=true)
    at /data/projects/mcrl2/src/libraries/aterm/source/afun.cpp:316
#4  0x00000000004cd11c in atermpp::detail::str2appl (s=...)
    at /data/projects/mcrl2/src/libraries/atermpp/include/mcrl2/atermpp/detail/utility.h:31
#5  0x00000000004cd009 in atermpp::aterm_string::aterm_string (
    this=0x7fffffff69c8, s=..., quoted=true)
    at /data/projects/mcrl2/src/libraries/atermpp/include/mcrl2/atermpp/aterm_string.h:72
#6  0x00000000004ccfbc in atermpp::aterm_string::aterm_string (
    this=0x7fffffff69c8, s=..., quoted=true)
    at /data/projects/mcrl2/src/libraries/atermpp/include/mcrl2/atermpp/aterm_string.h:76
#7  0x0000000000515090 in mcrl2::data::identifier_generator<mcrl2::utilities::number_postfix_generator>::operator() (this=0x84f008, hint=..., 
    add_to_context=false)

I suspect this is caused by the recent ATerm library changes.

jgroote commented 12 years ago

2012-04-02 09:59:35: anonymous changed status from new to closed

jgroote commented 12 years ago

2012-04-02 09:59:35: anonymous set resolution to fixed

jgroote commented 12 years ago

2012-04-02 09:59:35: anonymous commented

Resolved in r10438.