diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc index ed4915c4b..b249acce9 100644 --- a/spot/twaalgos/synthesis.cc +++ b/spot/twaalgos/synthesis.cc @@ -1022,7 +1022,8 @@ namespace spot if (bv) bv->paritize_time += sw.stop(); if (vs) - *vs << "LAR construction done in " << bv->paritize_time + *vs << (gi.s == algo::ACD ? "ACD" : "LAR") + << " construction done in " << bv->paritize_time << " seconds\nDPA has " << dpa->num_states() << " states, " << dpa->num_sets() << " colors\n"; diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index 07e2690e7..7a7084099 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -903,3 +903,29 @@ EOF sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx diff outx exp + +# ACD verbose +cat >exp < GFb) && (Gc)' --outs=b,c --verbose --bypass=no\ + --algo=acd 2> out +sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx +diff outx exp