Very slow translation to deterministic parity automaton on some formulas
So Ayrat Khalimov and I were wondering if there is a way to speed up the SPOT translation to parity automata a bit.
In particular, while using SPOT we encountered formulas that are hard for the "ltl2tgba" tool, and we are wondering if this is fixable - either through changes in the code or by using other parameters.
The following ltl2tgba runs exemplify the problem:
./ltl2tgba --colored-parity="min even" -D -C --hoaf=t "(TRUE & (G F ~v13)& (( G F v29 -> G F v15))) -> (TRUE & (G F (v1 -> (v31 & v21)))& (G F (v3 -> (v32 & v21)))& (G F (v5 -> (v33 & v21)))& (G F (v7 -> (v34 & v21)))& (G F (v9 -> (v35 & v21)))& (G F (v11 -> (v36 & v21)))& (G F (v31 | (v1 | (v3 | (v5 | (v7 | (v9 | v11))))))))"
(0.8 seconds)
./ltl2tgba --colored-parity="min even" -D -C --hoaf=t "(TRUE & (G F ~v15)& (( G F v31 -> G F v17))) -> (TRUE & (G F (v1 -> (v33 & v23)))& (G F (v3 -> (v34 & v23)))& (G F (v5 -> (v35 & v23)))& (G F (v7 -> (v36 & v23)))& (G F (v9 -> (v37 & v23)))& (G F (v11 -> (v38 & v23)))& (G F (v13 -> (v39 & v23)))& (G F (v33 | (v1 | (v3 | (v5 | (v7 | (v9 | (v11 | v13)))))))))"
(3.8 seconds)
./ltl2tgba --colored-parity="min even" -D -C --hoaf=t "(TRUE & (G F ~v17)& (( G F v33 -> G F v19))) -> (TRUE & (G F (v1 -> (v35 & v25)))& (G F (v3 -> (v36 & v25)))& (G F (v5 -> (v37 & v25)))& (G F (v7 -> (v38 & v25)))& (G F (v9 -> (v39 & v25)))& (G F (v11 -> (v40 & v25)))& (G F (v13 -> (v41 & v25)))& (G F (v15 -> (v42 & v25)))& (G F (v35 | (v1 | (v3 | (v5 | (v7 | (v9 | (v11 | (v13 | v15))))))))))"
(23 seconds)
./ltl2tgba --colored-parity="min even" -D -C --hoaf=t "(TRUE & (G F ~v21)& (( G F v39 -> G F v23))) -> (TRUE & (G F (v1 -> (v41 & v29)))& (G F (v3 -> (v42 & v29)))& (G F (v5 -> (v43 & v29)))& (G F (v7 -> (v44 & v29)))& (G F (v9 -> (v45 & v29)))& (G F (v11 -> (v46 & v29)))& (G F (v13 -> (v47 & v29)))& (G F (v15 -> (v48 & v29)))& (G F (v17 -> (v49 & v29)))& (G F (v19 -> (v50 & v29)))& (G F (v41 | (v1 | (v3 | (v5 | (v7 | (v9 | (v11 | (v13 | (v15 | (v17 | v19))))))))))))"
(out of memory after 5 minutes)
It would be great if you could have a look and check if we are doing something wrong. Perhaps we are not the only ones running into this problem.