out of memory in ltlcross
Vitus Lam reported randpsl.test
failing with:
-:17: (F(({{{(p0) | {[*0]}}:{{{(p1)}[*2]}[:*]}[*]:[*2]}[:*0..3]}[]-> (G(F(p1)))) & (G((!(p1)) | ((!(p2)) W (G(!(p0))))))))
Running [P0]: ../ikwiad -R3 -t '(F(({{{(p0) | {[*0]}}:{{{(p1)}[*2]}[:*]}[*]:[*2]}[:*0..3]}[]-> (G(F(p1)))) & (G((!(p1)) | ((!(p2)) W (G(!(p0))))))))' >'lcr-o0-rfpqTF'
Running [P1]: ../ikwiad -x -R3 -t '(F(({{{(p0) | {[*0]}}:{{{(p1)}[*2]}[:*]}[*]:[*2]}[:*0..3]}[]-> (G(F(p1)))) & (G((!(p1)) | ((!(p2)) W (G(!(p0))))))))' >'lcr-o1-TdrzQJ'
Running [N0]: ../ikwiad -R3 -t '(!(F(({{{(p0) | {[*0]}}:{{{(p1)}[*2]}[:*]}[*]:[*2]}[:*0..3]}[]-> (G(F(p1)))) & (G((!(p1)) | ((!(p2)) W (G(!(p0)))))))))' >'lcr-o0-W91t5N'
Running [N1]: ../ikwiad -x -R3 -t '(!(F(({{{(p0) | {[*0]}}:{{{(p1)}[*2]}[:*]}[*]:[*2]}[:*0..3]}[]-> (G(F(p1)))) & (G((!(p1)) | ((!(p2)) W (G(!(p0)))))))))' >'lcr-o1-GEQAIy'
Performing sanity checks and gathering statistics...
terminate called after throwing an instance of 'std::bad_alloc'
what(): std::bad_alloc
./randpsl.test: line 32: 7714 Broken pipe ../../bin/randltl -n -1 --tree-size 30 --seed 12 --psl a b c
7715 | ../../bin/ltlfilt -r --size-min 12 --unique
7716 Done | ../../bin/ltlfilt -v --ltl -n 50
7717 Done | tee formulas
7718 Aborted (core dumped) | ../../bin/ltlcross '../ikwiad -R3 -t %f >%T' '../ikwiad -x -R3 -t %f >%T' -F - -f '{{(p1)}[*]:{(p3) && {{!(p1)} xor {!(p3)}}}}'
He runs in a 32-bit VM with 4GB of RAM.
This particular formula actually takes a lot of time to run through ltlcross (when it works), so after fixing the memory problem (if possible) we might want to skip this case to speedup the builds.