ltl2tgba can be slow for formulas with conjunctions of many APs
go2pins' ltlrec
tool introduces new atomic propositions via conjunctions, so "a1 == 22"
becomes ("a1 == 22" && "a2 == 22" && "a3 == 22")
when introducing 3 atomic propositions instead of 1.
The following formula:
(! (true U ((("a1 == 22")) && X (true U (("a1 == 21"))))) || (! (("a1 == 22")) U (("a1 == 25"))))
Is translated just fine by ltl2tgba --ba
and ltl2ba
, but when I grow the number of atomic propositions with go2pins' ltlrec
, ltl2tgba
's performance starts to degrade compared to ltl2ba
.
Here are the results of the above formula when "expanded" through ltlrec
, replacing "a1" with respectively 1, 3, 10, 15, 20 and 30 variables.
(! (true U ((("a1 == 22")) && X (true U (("a1 == 21"))))) || (! (("a1 == 22")) U (("a1 == 25"))))
(! (true U ((("a1 == 22") && ("a2 == 22") && ("a3 == 22")) && X (true U (("a1 == 21") && ("a2 == 21") && ("a3 == 21"))))) || (! (("a1 == 22") && ("a2 == 22") && ("a3 == 22")) U (("a1 == 25") && ("a2 == 25") && ("a3 == 25"))))
(! (true U ((("a1 == 22") && ("a2 == 22") && ("a3 == 22") && ("a4 == 22") && ("a5 == 22") && ("a6 == 22") && ("a7 == 22") && ("a8 == 22") && ("a9 == 22") && ("a10 == 22")) && X (true U (("a1 == 21") && ("a2 == 21") && ("a3 == 21") && ("a4 == 21") && ("a5 == 21") && ("a6 == 21") && ("a7 == 21") && ("a8 == 21") && ("a9 == 21") && ("a10 == 21"))))) || (! (("a1 == 22") && ("a2 == 22") && ("a3 == 22") && ("a4 == 22") && ("a5 == 22") && ("a6 == 22") && ("a7 == 22") && ("a8 == 22") && ("a9 == 22") && ("a10 == 22")) U (("a1 == 25") && ("a2 == 25") && ("a3 == 25") && ("a4 == 25") && ("a5 == 25") && ("a6 == 25") && ("a7 == 25") && ("a8 == 25") && ("a9 == 25") && ("a10 == 25"))))
(! (true U ((("a1 == 22") && ("a2 == 22") && ("a3 == 22") && ("a4 == 22") && ("a5 == 22") && ("a6 == 22") && ("a7 == 22") && ("a8 == 22") && ("a9 == 22") && ("a10 == 22") && ("a11 == 22") && ("a12 == 22") && ("a13 == 22") && ("a14 == 22") && ("a15 == 22")) && X (true U (("a1 == 21") && ("a2 == 21") && ("a3 == 21") && ("a4 == 21") && ("a5 == 21") && ("a6 == 21") && ("a7 == 21") && ("a8 == 21") && ("a9 == 21") && ("a10 == 21") && ("a11 == 21") && ("a12 == 21") && ("a13 == 21") && ("a14 == 21") && ("a15 == 21"))))) || (! (("a1 == 22") && ("a2 == 22") && ("a3 == 22") && ("a4 == 22") && ("a5 == 22") && ("a6 == 22") && ("a7 == 22") && ("a8 == 22") && ("a9 == 22") && ("a10 == 22") && ("a11 == 22") && ("a12 == 22") && ("a13 == 22") && ("a14 == 22") && ("a15 == 22")) U (("a1 == 25") && ("a2 == 25") && ("a3 == 25") && ("a4 == 25") && ("a5 == 25") && ("a6 == 25") && ("a7 == 25") && ("a8 == 25") && ("a9 == 25") && ("a10 == 25") && ("a11 == 25") && ("a12 == 25") && ("a13 == 25") && ("a14 == 25") && ("a15 == 25"))))
(! (true U ((("a1 == 22") && ("a2 == 22") && ("a3 == 22") && ("a4 == 22") && ("a5 == 22") && ("a6 == 22") && ("a7 == 22") && ("a8 == 22") && ("a9 == 22") && ("a10 == 22") && ("a11 == 22") && ("a12 == 22") && ("a13 == 22") && ("a14 == 22") && ("a15 == 22") && ("a16 == 22") && ("a17 == 22") && ("a18 == 22") && ("a19 == 22") && ("a20 == 22")) && X (true U (("a1 == 21") && ("a2 == 21") && ("a3 == 21") && ("a4 == 21") && ("a5 == 21") && ("a6 == 21") && ("a7 == 21") && ("a8 == 21") && ("a9 == 21") && ("a10 == 21") && ("a11 == 21") && ("a12 == 21") && ("a13 == 21") && ("a14 == 21") && ("a15 == 21") && ("a16 == 21") && ("a17 == 21") && ("a18 == 21") && ("a19 == 21") && ("a20 == 21"))))) || (! (("a1 == 22") && ("a2 == 22") && ("a3 == 22") && ("a4 == 22") && ("a5 == 22") && ("a6 == 22") && ("a7 == 22") && ("a8 == 22") && ("a9 == 22") && ("a10 == 22") && ("a11 == 22") && ("a12 == 22") && ("a13 == 22") && ("a14 == 22") && ("a15 == 22") && ("a16 == 22") && ("a17 == 22") && ("a18 == 22") && ("a19 == 22") && ("a20 == 22")) U (("a1 == 25") && ("a2 == 25") && ("a3 == 25") && ("a4 == 25") && ("a5 == 25") && ("a6 == 25") && ("a7 == 25") && ("a8 == 25") && ("a9 == 25") && ("a10 == 25") && ("a11 == 25") && ("a12 == 25") && ("a13 == 25") && ("a14 == 25") && ("a15 == 25") && ("a16 == 25") && ("a17 == 25") && ("a18 == 25") && ("a19 == 25") && ("a20 == 25"))))
(! (true U ((("a1 == 22") && ("a2 == 22") && ("a3 == 22") && ("a4 == 22") && ("a5 == 22") && ("a6 == 22") && ("a7 == 22") && ("a8 == 22") && ("a9 == 22") && ("a10 == 22") && ("a11 == 22") && ("a12 == 22") && ("a13 == 22") && ("a14 == 22") && ("a15 == 22") && ("a16 == 22") && ("a17 == 22") && ("a18 == 22") && ("a19 == 22") && ("a20 == 22") && ("a21 == 22") && ("a22 == 22") && ("a23 == 22") && ("a24 == 22") && ("a25 == 22") && ("a26 == 22") && ("a27 == 22") && ("a28 == 22") && ("a29 == 22") && ("a30 == 22")) && X (true U (("a1 == 21") && ("a2 == 21") && ("a3 == 21") && ("a4 == 21") && ("a5 == 21") && ("a6 == 21") && ("a7 == 21") && ("a8 == 21") && ("a9 == 21") && ("a10 == 21") && ("a11 == 21") && ("a12 == 21") && ("a13 == 21") && ("a14 == 21") && ("a15 == 21") && ("a16 == 21") && ("a17 == 21") && ("a18 == 21") && ("a19 == 21") && ("a20 == 21") && ("a21 == 21") && ("a22 == 21") && ("a23 == 21") && ("a24 == 21") && ("a25 == 21") && ("a26 == 21") && ("a27 == 21") && ("a28 == 21") && ("a29 == 21") && ("a30 == 21"))))) || (! (("a1 == 22") && ("a2 == 22") && ("a3 == 22") && ("a4 == 22") && ("a5 == 22") && ("a6 == 22") && ("a7 == 22") && ("a8 == 22") && ("a9 == 22") && ("a10 == 22") && ("a11 == 22") && ("a12 == 22") && ("a13 == 22") && ("a14 == 22") && ("a15 == 22") && ("a16 == 22") && ("a17 == 22") && ("a18 == 22") && ("a19 == 22") && ("a20 == 22") && ("a21 == 22") && ("a22 == 22") && ("a23 == 22") && ("a24 == 22") && ("a25 == 22") && ("a26 == 22") && ("a27 == 22") && ("a28 == 22") && ("a29 == 22") && ("a30 == 22")) U (("a1 == 25") && ("a2 == 25") && ("a3 == 25") && ("a4 == 25") && ("a5 == 25") && ("a6 == 25") && ("a7 == 25") && ("a8 == 25") && ("a9 == 25") && ("a10 == 25") && ("a11 == 25") && ("a12 == 25") && ("a13 == 25") && ("a14 == 25") && ("a15 == 25") && ("a16 == 25") && ("a17 == 25") && ("a18 == 25") && ("a19 == 25") && ("a20 == 25") && ("a21 == 25") && ("a22 == 25") && ("a23 == 25") && ("a24 == 25") && ("a25 == 25") && ("a26 == 25") && ("a27 == 25") && ("a28 == 25") && ("a29 == 25") && ("a30 == 25"))))
and "adapted" for ltl2ba
:
!(true U (a1__eq__22 && X(true U a1__eq__21))) || (!a1__eq__22 U a1__eq__25)
!(true U (a1__eq__22 && a2__eq__22 && a3__eq__22 && X(true U (a1__eq__21 && a2__eq__21 && a3__eq__21)))) || (!(a1__eq__22 && a2__eq__22 && a3__eq__22) U (a1__eq__25 && a2__eq__25 && a3__eq__25))
!(true U (a1__eq__22 && a2__eq__22 && a3__eq__22 && a4__eq__22 && a5__eq__22 && a6__eq__22 && a7__eq__22 && a8__eq__22 && a9__eq__22 && a10__eq__22 && X(true U (a1__eq__21 && a2__eq__21 && a3__eq__21 && a4__eq__21 && a5__eq__21 && a6__eq__21 && a7__eq__21 && a8__eq__21 && a9__eq__21 && a10__eq__21)))) || (!(a1__eq__22 && a2__eq__22 && a3__eq__22 && a4__eq__22 && a5__eq__22 && a6__eq__22 && a7__eq__22 && a8__eq__22 && a9__eq__22 && a10__eq__22) U (a1__eq__25 && a2__eq__25 && a3__eq__25 && a4__eq__25 && a5__eq__25 && a6__eq__25 && a7__eq__25 && a8__eq__25 && a9__eq__25 && a10__eq__25))
!(true U (a1__eq__22 && a2__eq__22 && a3__eq__22 && a4__eq__22 && a5__eq__22 && a6__eq__22 && a7__eq__22 && a8__eq__22 && a9__eq__22 && a10__eq__22 && a11__eq__22 && a12__eq__22 && a13__eq__22 && a14__eq__22 && a15__eq__22 && X(true U (a1__eq__21 && a2__eq__21 && a3__eq__21 && a4__eq__21 && a5__eq__21 && a6__eq__21 && a7__eq__21 && a8__eq__21 && a9__eq__21 && a10__eq__21 && a11__eq__21 && a12__eq__21 && a13__eq__21 && a14__eq__21 && a15__eq__21)))) || (!(a1__eq__22 && a2__eq__22 && a3__eq__22 && a4__eq__22 && a5__eq__22 && a6__eq__22 && a7__eq__22 && a8__eq__22 && a9__eq__22 && a10__eq__22 && a11__eq__22 && a12__eq__22 && a13__eq__22 && a14__eq__22 && a15__eq__22) U (a1__eq__25 && a2__eq__25 && a3__eq__25 && a4__eq__25 && a5__eq__25 && a6__eq__25 && a7__eq__25 && a8__eq__25 && a9__eq__25 && a10__eq__25 && a11__eq__25 && a12__eq__25 && a13__eq__25 && a14__eq__25 && a15__eq__25))
!(true U (a1__eq__22 && a2__eq__22 && a3__eq__22 && a4__eq__22 && a5__eq__22 && a6__eq__22 && a7__eq__22 && a8__eq__22 && a9__eq__22 && a10__eq__22 && a11__eq__22 && a12__eq__22 && a13__eq__22 && a14__eq__22 && a15__eq__22 && a16__eq__22 && a17__eq__22 && a18__eq__22 && a19__eq__22 && a20__eq__22 && X(true U (a1__eq__21 && a2__eq__21 && a3__eq__21 && a4__eq__21 && a5__eq__21 && a6__eq__21 && a7__eq__21 && a8__eq__21 && a9__eq__21 && a10__eq__21 && a11__eq__21 && a12__eq__21 && a13__eq__21 && a14__eq__21 && a15__eq__21 && a16__eq__21 && a17__eq__21 && a18__eq__21 && a19__eq__21 && a20__eq__21)))) || (!(a1__eq__22 && a2__eq__22 && a3__eq__22 && a4__eq__22 && a5__eq__22 && a6__eq__22 && a7__eq__22 && a8__eq__22 && a9__eq__22 && a10__eq__22 && a11__eq__22 && a12__eq__22 && a13__eq__22 && a14__eq__22 && a15__eq__22 && a16__eq__22 && a17__eq__22 && a18__eq__22 && a19__eq__22 && a20__eq__22) U (a1__eq__25 && a2__eq__25 && a3__eq__25 && a4__eq__25 && a5__eq__25 && a6__eq__25 && a7__eq__25 && a8__eq__25 && a9__eq__25 && a10__eq__25 && a11__eq__25 && a12__eq__25 && a13__eq__25 && a14__eq__25 && a15__eq__25 && a16__eq__25 && a17__eq__25 && a18__eq__25 && a19__eq__25 && a20__eq__25))
!(true U (a1__eq__22 && a2__eq__22 && a3__eq__22 && a4__eq__22 && a5__eq__22 && a6__eq__22 && a7__eq__22 && a8__eq__22 && a9__eq__22 && a10__eq__22 && a11__eq__22 && a12__eq__22 && a13__eq__22 && a14__eq__22 && a15__eq__22 && a16__eq__22 && a17__eq__22 && a18__eq__22 && a19__eq__22 && a20__eq__22 && a21__eq__22 && a22__eq__22 && a23__eq__22 && a24__eq__22 && a25__eq__22 && a26__eq__22 && a27__eq__22 && a28__eq__22 && a29__eq__22 && a30__eq__22 && X(true U (a1__eq__21 && a2__eq__21 && a3__eq__21 && a4__eq__21 && a5__eq__21 && a6__eq__21 && a7__eq__21 && a8__eq__21 && a9__eq__21 && a10__eq__21 && a11__eq__21 && a12__eq__21 && a13__eq__21 && a14__eq__21 && a15__eq__21 && a16__eq__21 && a17__eq__21 && a18__eq__21 && a19__eq__21 && a20__eq__21 && a21__eq__21 && a22__eq__21 && a23__eq__21 && a24__eq__21 && a25__eq__21 && a26__eq__21 && a27__eq__21 && a28__eq__21 && a29__eq__21 && a30__eq__21)))) || (!(a1__eq__22 && a2__eq__22 && a3__eq__22 && a4__eq__22 && a5__eq__22 && a6__eq__22 && a7__eq__22 && a8__eq__22 && a9__eq__22 && a10__eq__22 && a11__eq__22 && a12__eq__22 && a13__eq__22 && a14__eq__22 && a15__eq__22 && a16__eq__22 && a17__eq__22 && a18__eq__22 && a19__eq__22 && a20__eq__22 && a21__eq__22 && a22__eq__22 && a23__eq__22 && a24__eq__22 && a25__eq__22 && a26__eq__22 && a27__eq__22 && a28__eq__22 && a29__eq__22 && a30__eq__22) U (a1__eq__25 && a2__eq__25 && a3__eq__25 && a4__eq__25 && a5__eq__25 && a6__eq__25 && a7__eq__25 && a8__eq__25 && a9__eq__25 && a10__eq__25 && a11__eq__25 && a12__eq__25 && a13__eq__25 && a14__eq__25 && a15__eq__25 && a16__eq__25 && a17__eq__25 && a18__eq__25 && a19__eq__25 && a20__eq__25 && a21__eq__25 && a22__eq__25 && a23__eq__25 && a24__eq__25 && a25__eq__25 && a26__eq__25 && a27__eq__25 && a28__eq__25 && a29__eq__25 && a30__eq__25))
ltl2tgba
takes 3.5 seconds for 15 variables, where ltl2ba
translates it in 60 milliseconds.
For 20 variables I get a timeout after 30 seconds, ltl2ba finishes in 3.5 seconds.
I'll provide a list of all formulas from our benchmark that make ltl2tgba perform this way, this afternoon.