pbessolvesymbolic crashes when merging the data specification with the data specification containing the PropositionalVariable struct

[mlaveaux]

The following commands can be used to reproduce this issue. Somehow the the fact that the pbes is made from an LTS and the number of equations is large seems to be important.

mcrl22lps 1394-fin.mcrl2 temp.lps
lps2lts --cached temp.lps temp.lts
lts2pbes -f examples/modal-formulas/nodeadlock.mcf temp.lts temp.nodeadlock.pbes
pbessolvesymbolic temp.nodeadlock.pbes

See the stack trace below:

#0  mcrl2::data::find_normal_form (e=..., map1=..., sorts_already_seen=...) at /scratch/mlaveaux/MCRL2/mCRL2/libraries/data/source/data_specification.cpp:252
#1  0x00007ffff799ad40 in mcrl2::data::sort_specification::reconstruct_m_normalised_aliases (this=<optimized out>) at /usr/include/c++/9/bits/stl_tree.h:211
#2  0x00005555555bd86f in mcrl2::data::sort_specification::normalise_sort_specification_if_required (this=0x7fffffff95b0) at /scratch/mlaveaux/MCRL2/mCRL2/libraries/data/include/mcrl2/data/sort_specification.h:279
#3  0x00007ffff791348f in mcrl2::data::sort_specification::sort_alias_map (this=0x7fffffff95b0) at /scratch/mlaveaux/MCRL2/mCRL2/libraries/data/include/mcrl2/data/sort_specification.h:249
#4  mcrl2::data::detail::normalize_sorts_function::normalize_sorts_function (sort_spec=..., this=0x7fffffff8c80) at /scratch/mlaveaux/MCRL2/mCRL2/libraries/data/include/mcrl2/data/normalize_sorts.h:36
#5  mcrl2::data::normalize_sorts<mcrl2::data::sort_expression> (sort_spec=..., x=...) at /scratch/mlaveaux/MCRL2/mCRL2/libraries/data/include/mcrl2/data/normalize_sorts.h:130
#6  mcrl2::data::normalize_sorts (x=..., sortspec=...) at /scratch/mlaveaux/MCRL2/mCRL2/libraries/data/source/data.cpp:86
#7  0x00007ffff7a4418b in mcrl2::data::data_type_checker::add_constant (this=0x7fffffff95b0, f=..., msg=...) at /scratch/mlaveaux/MCRL2/mCRL2/libraries/data/include/mcrl2/data/sort_type_checker.h:44
#8  0x00007ffff7a59281 in mcrl2::data::data_type_checker::read_sort (this=0x7fffffff95b0, sort_expr=...) at /usr/include/c++/9/ext/new_allocator.h:80
#9  0x00007ffff7a69e30 in mcrl2::data::data_type_checker::data_type_checker (this=0x7fffffff95b0, data_spec=...) at /scratch/mlaveaux/MCRL2/mCRL2/libraries/atermpp/include/mcrl2/atermpp/detail/aterm_appl.h:95
#10 0x00005555555cfebe in mcrl2::data::merge_data_specifications (dataspec1=..., dataspec2=...) at /scratch/mlaveaux/MCRL2/mCRL2/libraries/data/include/mcrl2/data/merge_data_specifications.h:77
#11 0x000055555566afdf in mcrl2::pbes_system::pbesreach_algorithm::preprocess (this=<optimized out>, pbesspec=..., make_total=<optimized out>) at /scratch/mlaveaux/MCRL2/mCRL2/libraries/pbes/include/mcrl2/pbes/srf_pbes.h:604
#12 0x000055555566c05c in mcrl2::pbes_system::pbesreach_algorithm::pbesreach_algorithm (this=0x7fffffffd2c0, pbesspec=..., options_=...)
    at /scratch/mlaveaux/MCRL2/mCRL2/libraries/atermpp/include/mcrl2/atermpp/detail/aterm_implementation.h:81
#13 0x000055555566f95d in pbessolvesymbolic_tool::run (this=0x7fffffffdc00) at /scratch/mlaveaux/MCRL2/mCRL2/tools/release/pbessolvesymbolic/pbessolvesymbolic.cpp:373
#14 0x00005555555d96b0 in mcrl2::utilities::tools::tool::execute (this=0x7fffffffdc00, argc=<optimized out>, argv=<optimized out>) at /scratch/mlaveaux/MCRL2/mCRL2/libraries/utilities/include/mcrl2/utilities/tool.h:220
#15 0x000055555559bf02 in main (argc=3, argv=0x7fffffffdf98) at /scratch/mlaveaux/MCRL2/mCRL2/tools/release/pbessolvesymbolic/pbessolvesymbolic.cpp:391

[jgroote]

This was caused by a residual bug due the transformation to the parallel framework. For lists longer than 10000 elements the empty list at the end was not inserted. As this only occurred in very long lists, this was never caught by the soundness checks. Problem is resolved in above mentioned commit.