ltlcross aborts with "Too many acceptance sets used" without creating a CSV file
I received this from Fanda. Probably a regression due to the fact that ltlcross now uses the generic emptiness check, so it does not call remove_fin() and has more colors in the product. We should still produce a CSV file in this case, so maybe there is a missing try/catch somewhere. Also maybe we should consider calling remove_fin() anyway if building the product would use too many colors.
Hi Alexandre,
for the following log, I have no .csv created.
ltlcross {no.goal#pit}ltl2tgba -D -B %f > $LCW_TMP.in.hoa && $LCW_GOAL_BIN batch '$temp = complement -m piterman -eq -sp `echo $LCW_TMP.in.hoa`; save -c HOAF $temp `echo $LCW_TMP.out.hoa`;'; err=$?; rm -f $LCW_TMP.in.hoa; mv -f $LCW_TMP.out.hoa %O; exit $err {no.goal#fri}ltl2tgba -D -B %f > $LCW_TMP.in.hoa && $LCW_GOAL_BIN batch '$temp = complement -m fribourg `echo $LCW_TMP.in.hoa`; save -c HOAF $temp `echo $LCW_TMP.out.hoa`;'; err=$?; rm -f $LCW_TMP.in.hoa; mv -f $LCW_TMP.out.hoa %O; exit $err {no.roll}ltl2tgba -D -B %f > $LCW_TMP.in.hoa && java -jar other_tools/roll-library/ROLL.jar complement $LCW_TMP.in.hoa -v 0 -table -syntactic -out $LCW_TMP.out.hoa; err=$?; rm -f $LCW_TMP.in.hoa; mv -f $LCW_TMP.out.hoa %O; exit $err {no.spot}ltl2tgba -D %f | autfilt --complement --tgba > %O {no.spot_DPA}ltl2tgba -D %f | autfilt --complement > %O {no.seminator#spot}ltl2tgba -D %f | seminator --complement=spot --cut-always --postprocess-comp=0 >%O {no.seminator#pldi}ltl2tgba -D %f | seminator --complement=pldi --cut-always --postprocess-comp=0 >%O {no.seminator#best}ltl2tgba -D %f | seminator --complement=best --cut-always --postprocess-comp=0 >%O -F random_nd_check.parts/random_nd_check-489.ltl --timeout=120 --automata --save-bogus=random_nd_check.parts/random_nd_check-489_bogus.ltl --products=0 --csv=random_nd_check.parts/random_nd_check-489.csv [12.05.2020 01:13:13] ===================== random_nd_check.parts/random_nd_check-489.ltl:1: F((G(a)) | (G(((b) & ((!(c)) U (X(!(d))))) | ((!(b)) & ((c) R (X(d))))))) Running [P0: no.goal#pit]: ltl2tgba -D -B 'F((G(a)) | (G(((b) & ((!(c)) U (X(!(d))))) | ((!(b)) & ((c) R (X(d)))))))' > $LCW_TMP.in.hoa && $LCW_GOAL_BIN batch '$temp = complement -m piterman -eq -sp `echo $LCW_TMP.in.hoa`; save -c HOAF $temp `echo $LCW_TMP.out.hoa`;'; err=$?; rm -f $LCW_TMP.in.hoa; mv -f $LCW_TMP.out.hoa '/tmp/lcr-o0-9ACNT8'; exit $err Running [P1: no.goal#fri]: ltl2tgba -D -B 'F((G(a)) | (G(((b) & ((!(c)) U (X(!(d))))) | ((!(b)) & ((c) R (X(d)))))))' > $LCW_TMP.in.hoa && $LCW_GOAL_BIN batch '$temp = complement -m fribourg `echo $LCW_TMP.in.hoa`; save -c HOAF $temp `echo $LCW_TMP.out.hoa`;'; err=$?; rm -f $LCW_TMP.in.hoa; mv -f $LCW_TMP.out.hoa '/tmp/lcr-o1-d4Rsf9'; exit $err Running [P2: no.roll]: ltl2tgba -D -B 'F((G(a)) | (G(((b) & ((!(c)) U (X(!(d))))) | ((!(b)) & ((c) R (X(d)))))))' > $LCW_TMP.in.hoa && java -jar other_tools/roll-library/ROLL.jar complement $LCW_TMP.in.hoa -v 0 -table -syntactic -out $LCW_TMP.out.hoa; err=$?; rm -f $LCW_TMP.in.hoa; mv -f $LCW_TMP.out.hoa '/tmp/lcr-o2-16wicf'; exit $err 2020/05/12 01:13:20 [ info] ROLL for BA complementation... #LT = 16 // #number of letters #T.S = 6 // #states of target #T.T = 78 // #transitions of target #H.S = 15 // #states of learned automaton #H.T = 292 // #transitions of learned automaton #L.S = 1 // #states of leading automaton or L$ #P.S = [29, ] // #states of each progress automaton #F.S = 30 // #L.S + #P.S #MQ = 5628 // #membership query #EQ = 12 // #equivalence query #TMQ = 332 (ms) // time for membership queries #TEQ = 3823 (ms) // time for equivalence queries #TLEQ = 3169 (ms) // time for the last equivalence query #TTR = 0 (ms) // time for the translator #TLR = 466 (ms) // time for the learner #TLRL = 6 (ms) // time for learning leading automaton #TLRP = 449 (ms) // time for learning progress automata #TTO = 4848 (ms) // total time for learning Buchi automata Running [P3: no.spot]: ltl2tgba -D 'F((G(a)) | (G(((b) & ((!(c)) U (X(!(d))))) | ((!(b)) & ((c) R (X(d)))))))' | autfilt --complement --tgba > '/tmp/lcr-o3-e4Slyt' Running [P4: no.spot_DPA]: ltl2tgba -D 'F((G(a)) | (G(((b) & ((!(c)) U (X(!(d))))) | ((!(b)) & ((c) R (X(d)))))))' | autfilt --complement > '/tmp/lcr-o4-WMfxWH' Running [P5: no.seminator#spot]: ltl2tgba -D 'F((G(a)) | (G(((b) & ((!(c)) U (X(!(d))))) | ((!(b)) & ((c) R (X(d)))))))' | seminator --complement=spot --cut-always --postprocess-comp=0 >'/tmp/lcr-o5-mmwKmW' Running [P6: no.seminator#pldi]: ltl2tgba -D 'F((G(a)) | (G(((b) & ((!(c)) U (X(!(d))))) | ((!(b)) & ((c) R (X(d)))))))' | seminator --complement=pldi --cut-always --postprocess-comp=0 >'/tmp/lcr-o6-0SCpPa' Running [P7: no.seminator#best]: ltl2tgba -D 'F((G(a)) | (G(((b) & ((!(c)) U (X(!(d))))) | ((!(b)) & ((c) R (X(d)))))))' | seminator --complement=best --cut-always --postprocess-comp=0 >'/tmp/lcr-o7-ZjGzkp' Running [N0: no.goal#pit]: ltl2tgba -D -B '!(F((G(a)) | (G(((b) & ((!(c)) U (X(!(d))))) | ((!(b)) & ((c) R (X(d))))))))' > $LCW_TMP.in.hoa && $LCW_GOAL_BIN batch '$temp = complement -m piterman -eq -sp `echo $LCW_TMP.in.hoa`; save -c HOAF $temp `echo $LCW_TMP.out.hoa`;'; err=$?; rm -f $LCW_TMP.in.hoa; mv -f $LCW_TMP.out.hoa '/tmp/lcr-o0-6edwSD'; exit $err Running [N1: no.goal#fri]: ltl2tgba -D -B '!(F((G(a)) | (G(((b) & ((!(c)) U (X(!(d))))) | ((!(b)) & ((c) R (X(d))))))))' > $LCW_TMP.in.hoa && $LCW_GOAL_BIN batch '$temp = complement -m fribourg `echo $LCW_TMP.in.hoa`; save -c HOAF $temp `echo $LCW_TMP.out.hoa`;'; err=$?; rm -f $LCW_TMP.in.hoa; mv -f $LCW_TMP.out.hoa '/tmp/lcr-o1-aQIaO7'; exit $err Running [N2: no.roll]: ltl2tgba -D -B '!(F((G(a)) | (G(((b) & ((!(c)) U (X(!(d))))) | ((!(b)) & ((c) R (X(d))))))))' > $LCW_TMP.in.hoa && java -jar other_tools/roll-library/ROLL.jar complement $LCW_TMP.in.hoa -v 0 -table -syntactic -out $LCW_TMP.out.hoa; err=$?; rm -f $LCW_TMP.in.hoa; mv -f $LCW_TMP.out.hoa '/tmp/lcr-o2-WsAe9G'; exit $err 2020/05/12 01:13:38 [ info] ROLL for BA complementation... #LT = 16 // #number of letters #T.S = 12 // #states of target #T.T = 194 // #transitions of target #H.S = 137 // #states of learned automaton #H.T = 1236 // #transitions of learned automaton #L.S = 1 // #states of leading automaton or L$ #P.S = [28, ] // #states of each progress automaton #F.S = 29 // #L.S + #P.S #MQ = 5433 // #membership query #EQ = 12 // #equivalence query #TMQ = 261 (ms) // time for membership queries #TEQ = 10498 (ms) // time for equivalence queries #TLEQ = 9610 (ms) // time for the last equivalence query #TTR = 0 (ms) // time for the translator #TLR = 389 (ms) // time for the learner #TLRL = 4 (ms) // time for learning leading automaton #TLRP = 374 (ms) // time for learning progress automata #TTO = 11347 (ms) // total time for learning Buchi automata Running [N3: no.spot]: ltl2tgba -D '!(F((G(a)) | (G(((b) & ((!(c)) U (X(!(d))))) | ((!(b)) & ((c) R (X(d))))))))' | autfilt --complement --tgba > '/tmp/lcr-o3-Fm6Wpz' Running [N4: no.spot_DPA]: ltl2tgba -D '!(F((G(a)) | (G(((b) & ((!(c)) U (X(!(d))))) | ((!(b)) & ((c) R (X(d))))))))' | autfilt --complement > '/tmp/lcr-o4-ApdsKr' Running [N5: no.seminator#spot]: ltl2tgba -D '!(F((G(a)) | (G(((b) & ((!(c)) U (X(!(d))))) | ((!(b)) & ((c) R (X(d))))))))' | seminator --complement=spot --cut-always --postprocess-comp=0 >'/tmp/lcr-o5-lrjJ7j' Running [N6: no.seminator#pldi]: ltl2tgba -D '!(F((G(a)) | (G(((b) & ((!(c)) U (X(!(d))))) | ((!(b)) & ((c) R (X(d))))))))' | seminator --complement=pldi --cut-always --postprocess-comp=0 >'/tmp/lcr-o6-TtQPYc' Running [N7: no.seminator#best]: ltl2tgba -D '!(F((G(a)) | (G(((b) & ((!(c)) U (X(!(d))))) | ((!(b)) & ((c) R (X(d))))))))' | seminator --complement=best --cut-always --postprocess-comp=0 >'/tmp/lcr-o7-he0Hc6' Performing sanity checks and gathering statistics... ltlcross: Too many acceptance sets used. The limit is 32. 2Is it intended?
Best. Fanda