case where ltlcross consumes too much memory
This is a very large automaton created by ltl2dstar, and remove_fin create even larger automata. Maybe there is something to improve.
% ltlcross --verbose -f 'F(Ga | Gb | Gc | Gd | Ge)' 'ltl2dstar --union=no --ltl2nba=spin:ltl2tgba@-Ds --output-format=hoa %L %O'
F | | | | G p0 G p1 G p2 G p3 G p4
Running [P0]: ltl2dstar --union=no --ltl2nba=spin:ltl2tgba@-Ds --output-format=hoa 'lcr-i0-kcDtFC' 'lcr-o0-DaCj7N'
Running [N0]: ltl2dstar --union=no --ltl2nba=spin:ltl2tgba@-Ds --output-format=hoa 'lcr-i0-iJErXM' 'lcr-o0-P5qANL'
Performing sanity checks and gathering statistics...
info: getting rid of any Fin acceptance...
info: P0 (58852 st., 1883264 ed., 18 sets) -> (250133 st., 5917479 ed., 1 sets)
info: Comp(P0) (58852 st., 1883264 ed., 18 sets) -> (3896448 st., 103304326 ed., 18 sets)
info: Comp(N0) (11 st., 352 ed., 1 sets) -> (16 st., 610 ed., 1 sets)
info: check_empty P0*N0
^C
To upload designs, you'll need to enable LFS and have admin enable hashed storage. More information