formulas with large memory consumption
Carlo Sengers reports that translating the following two formulas dies with out-of-memory:
G((p0) & (((p15) <-> ((G((p5) & (((p14) xor (G(p2))) <-> (G(X(p1)))))) U ((G(p8)) M (p7)))) -> ((p12) M (p6))))
(((G((F(p5)) <-> (G(p7)))) & ((p8) <-> (F(p9)))) xor ((!(p0)) U (p1))) M ((X(p5)) & (F(p4)))
I can reproduce the issue with the first one. Aborting ltl2tgba
while it's struggling to find memory shows the following backtrace:
#0 0x00007ffff7e4bc1e in std::_Hashtable<spot::bitvect*, std::pair<spot::bitvect* const, int>, std::allocator<std::pair<spot::bitvect* const, int> >, std::__detail::_Select1st, spot::(anonymous namespace)::bv_equal, spot::(anonymous namespace)::bv_hash, std::__detail::_Mod_range_hashing, std::__detail::_Default_ranged_hash, std::__detail::_Prime_rehash_policy, std::__detail::_Hashtable_traits<false, false, true> >::_M_find_before_node
(this=this@entry=0x7fffffffc150, __n=750920, __k=@0x7fffffffc080: 0x555555636440, __code=<optimized out>)
at /usr/include/c++/9/bits/hashtable.h:1532
#1 0x00007ffff7e4d3ab in std::_Hashtable<spot::bitvect*, std::pair<spot::bitvect* const, int>, std::allocator<std::pair<spot::bitvect* const, int> >, std::__detail::_Select1st, spot::(anonymous namespace)::bv_equal, spot::(anonymous namespace)::bv_hash, std::__detail::_Mod_range_hashing, std::__detail::_Default_ranged_hash, std::__detail::_Prime_rehash_policy, std::__detail::_Hashtable_traits<false, false, true> >::_M_find_node (
__c=<optimized out>, __key=@0x7fffffffc080: 0x555555636440, __bkt=<optimized out>, this=0x7fffffffc150)
at /usr/include/c++/9/bits/hashtable.h:652
#2 std::_Hashtable<spot::bitvect*, std::pair<spot::bitvect* const, int>, std::allocator<std::pair<spot::bitvect* const, int> >, std::__detail::_Select1st, spot::(anonymous namespace)::bv_equal, spot::(anonymous namespace)::bv_hash, std::__detail::_Mod_range_hashing, std::__detail::_Default_ranged_hash, std::__detail::_Prime_rehash_policy, std::__detail::_Hashtable_traits<false, false, true> >::find (
__k=@0x7fffffffc080: 0x555555636440, this=0x7fffffffc150) at /usr/include/c++/9/bits/hashtable.h:1419
#3 std::unordered_map<spot::bitvect*, int, spot::(anonymous namespace)::bv_hash, spot::(anonymous namespace)::bv_equal, std::allocator<std::pair<spot::bitvect* const, int> > >::find (__x=@0x7fffffffc080: 0x555555636440, this=0x7fffffffc150) at /usr/include/c++/9/bits/unordered_map.h:921
#4 spot::tgba_powerset (aut=std::shared_ptr<const spot::twa_graph> (use count 2, weak count 1) = {...}, pm=..., merge=merge@entry=false,
aborter=aborter@entry=0x0) at powerset.cc:242
#5 0x00007ffff7e2f365 in spot::minimize_wdba (a=std::shared_ptr<const spot::twa_graph> (use count 2, weak count 1) = {...}, aborter=0x0)
at minimize.cc:397
#6 0x00007ffff7e31104 in spot::minimize_obligation (aut_f=std::shared_ptr<const spot::twa_graph> (use count 2, weak count 1) = {...}, f=...,
aut_neg_f=std::shared_ptr<const spot::twa_graph> (empty) = {...}, reject_bigger=<optimized out>, aborter=aborter@entry=0x0) at minimize.cc:603
#7 0x00007ffff7e48cfd in spot::postprocessor::run (this=this@entry=0x7fffffffcdc0,
a=std::shared_ptr<spot::twa_graph> (use count 2, weak count 1) = {...}, f=...) at /usr/include/c++/9/ext/atomicity.h:96
#8 0x00007ffff7eed668 in spot::translator::run_aux (this=<optimized out>, r=...) at /usr/include/c++/9/ext/atomicity.h:96
#9 0x00007ffff7eecabd in spot::translator::run (this=0x7fffffffcdc0, f=f@entry=0x7fffffffcc68) at ../../spot/tl/formula.hh:738
#10 0x000055555555db38 in (anonymous namespace)::trans_processor::process_formula (this=0x7fffffffce50, f=..., filename=0x0, linenum=0)
at ltl2tgba.cc:156
#11 0x0000555555567644 in job_processor::process_string (this=this@entry=0x7fffffffce50,
input="G((p0) & (((p15) <-> ((G((p5) & (((p14) xor (G(p2))) <-> (G(X(p1)))))) U ((G(p8)) M (p7)))) -> ((p12) M (p6))))",
filename=filename@entry=0x0, linenum=linenum@entry=0) at ../spot/tl/formula.hh:738
#12 0x000055555556740f in job_processor::run (this=this@entry=0x7fffffffce50) at /usr/include/c++/9/bits/char_traits.h:300
#13 0x000055555555e192 in <lambda()>::operator()(void) const (__closure=<optimized out>, __closure=<optimized out>) at ltl2tgba.cc:193
#14 0x00005555555687eb in std::function<int ()>::operator()() const (this=0x7fffffffdd80) at /usr/include/c++/9/bits/std_function.h:683
#15 protected_main(char**, std::function<int ()>) (progname=<optimized out>, mainfun=...) at common_setup.cc:205
Suggestion:
- try to replace the STL hash by the robin_hood version we have started using recently
- reorganize
postproc.cc
so that some sort of simulation is run before WDBA minimization - is it possible to call WDBA minimization with an output aborter? It would make sense in the
--small
setting, but it's unclear how a max size of the output of the WDBA minimization can translate into a max size on the powerset construction.