From 55aac8e107a9ebe9c9b416b91d1c1f5e180feffc Mon Sep 17 00:00:00 2001
From: Florian Renkin <frenkin@lrde.epita.fr>
Date: Tue, 12 Apr 2022 11:19:49 +0200
Subject: [PATCH] ltlsynt: display ACD instead of LAR when needed

* spot/twaalgos/synthesis.cc: here
* tests/core/ltlsynt.test: add test
---
 spot/twaalgos/synthesis.cc |  3 ++-
 tests/core/ltlsynt.test    | 26 ++++++++++++++++++++++++++
 2 files changed, 28 insertions(+), 1 deletion(-)

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 <<EOF
+translating formula done in X seconds
+automaton has 1 states and 2 colors
+ACD construction done in X seconds
+DPA has 2 states, 2 colors
+split inputs and outputs done in X seconds
+automaton has 6 states
+solving game with acceptance: parity max odd 4
+game solved in X seconds
+simplification took X seconds
+translating formula done in X seconds
+automaton has 1 states and 1 colors
+ACD construction done in X seconds
+DPA has 1 states, 0 colors
+split inputs and outputs done in X seconds
+automaton has 2 states
+solving game with acceptance: Streett 1
+game solved in X seconds
+simplification took X seconds
+EOF
+ltlsynt -f '(GFa <-> 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