From 8d9597d80dcaa1ef98f65985a7c8a0964e2631df Mon Sep 17 00:00:00 2001
From: Florian Renkin <frenkin@lrde.epita.fr>
Date: Mon, 21 Mar 2022 15:58:58 +0100
Subject: [PATCH] ltlsynt: add --algo=acd

* bin/ltlsynt.cc: Add "acd" to the list of possible paritization
		  algorithms used by ltlsynt
* spot/twaalgos/synthesis.cc, spot/twaalgos/synthesis.hh: Add
	ACD as paritisation algorithm
* tests/core/ltlsynt.test: add tests
---
 bin/ltlsynt.cc             | 12 +++++++++---
 spot/twaalgos/synthesis.cc | 14 ++++++++++++--
 spot/twaalgos/synthesis.hh |  1 +
 tests/core/ltlsynt.test    | 12 +++++++++++-
 4 files changed, 33 insertions(+), 6 deletions(-)

diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc
index 25b8bb04a..8dcd9511a 100644
--- a/bin/ltlsynt.cc
+++ b/bin/ltlsynt.cc
@@ -69,7 +69,7 @@ static const argp_option options[] =
       " propositions", 0},
     /**************************************************/
     { nullptr, 0, nullptr, 0, "Fine tuning:", 10 },
-    { "algo", OPT_ALGO, "sd|ds|ps|lar|lar.old", 0,
+    { "algo", OPT_ALGO, "sd|ds|ps|lar|lar.old|acd", 0,
       "choose the algorithm for synthesis:"
       " \"sd\": translate to tgba, split, then determinize;"
       " \"ds\": translate to tgba, determinize, then split;"
@@ -77,7 +77,10 @@ static const argp_option options[] =
       " \"lar\": translate to a deterministic automaton with arbitrary"
       " acceptance condition, then use LAR to turn to parity,"
       " then split (default);"
-      " \"lar.old\": old version of LAR, for benchmarking.\n", 0 },
+      " \"lar.old\": old version of LAR, for benchmarking;"
+      " \"acd\": translate to a deterministic automaton with arbitrary"
+      " acceptance condition, then use ACD to turn to parity,"
+      " then split.\n", 0 },
     { "decompose", OPT_DECOMPOSE, "yes|no", 0,
       "whether to decompose the specification as multiple output-disjoint "
       "problems to solve independently (enabled by default)", 0 },
@@ -154,7 +157,8 @@ static char const *const algo_names[] =
    "sd",
    "ps",
    "lar",
-   "lar.old"
+   "lar.old",
+   "acd",
   };
 
 static char const *const algo_args[] =
@@ -164,6 +168,7 @@ static char const *const algo_args[] =
   "dpasplit", "ps",
   "lar",
   "lar.old",
+  "acd",
   nullptr
 };
 static spot::synthesis_info::algo const algo_types[] =
@@ -173,6 +178,7 @@ static spot::synthesis_info::algo const algo_types[] =
   spot::synthesis_info::algo::DPA_SPLIT, spot::synthesis_info::algo::DPA_SPLIT,
   spot::synthesis_info::algo::LAR,
   spot::synthesis_info::algo::LAR_OLD,
+  spot::synthesis_info::algo::ACD,
 };
 ARGMATCH_VERIFY(algo_args, algo_types);
 
diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc
index 7620a1098..95e0725d9 100644
--- a/spot/twaalgos/synthesis.cc
+++ b/spot/twaalgos/synthesis.cc
@@ -29,6 +29,7 @@
 #include <spot/twaalgos/sbacc.hh>
 #include <spot/twaalgos/synthesis.hh>
 #include <spot/twaalgos/translate.hh>
+#include <spot/twaalgos/zlktree.hh>
 #include <spot/misc/minato.hh>
 #include <spot/twaalgos/totgba.hh>
 #include <spot/twaalgos/toparity.hh>
@@ -741,6 +742,9 @@ namespace spot
       case (algo::LAR_OLD):
         name = "lar.old";
         break;
+      case (algo::ACD):
+        name = "acd";
+        break;
     }
     return os << name;
 }
@@ -775,6 +779,8 @@ namespace spot
       translator trans(dict, &extra_options);
       switch (sol)
       {
+      case algo::ACD:
+        SPOT_FALLTHROUGH;
       case algo::LAR:
         SPOT_FALLTHROUGH;
       case algo::LAR_OLD:
@@ -965,6 +971,8 @@ namespace spot
         alternate_players(dpa);
         break;
       }
+      case algo::ACD:
+        SPOT_FALLTHROUGH;
       case algo::LAR:
         SPOT_FALLTHROUGH;
       case algo::LAR_OLD:
@@ -976,11 +984,13 @@ namespace spot
             dpa = to_parity(aut);
             // reduce_parity is called by to_parity()
           }
-        else
+        else if (gi.s == algo::LAR_OLD)
           {
             dpa = to_parity_old(aut);
-            dpa = reduce_parity_here(dpa, true);
+            reduce_parity_here(dpa, true);
           }
+        else
+          dpa = acd_transform(aut);
         if (bv)
           bv->paritize_time += sw.stop();
         if (vs)
diff --git a/spot/twaalgos/synthesis.hh b/spot/twaalgos/synthesis.hh
index 46c0bc2bd..a5fced429 100644
--- a/spot/twaalgos/synthesis.hh
+++ b/spot/twaalgos/synthesis.hh
@@ -86,6 +86,7 @@ namespace spot
       DPA_SPLIT,
       LAR,
       LAR_OLD,
+      ACD,
     };
 
     struct bench_var
diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test
index c22cd4e6b..742f05a5e 100644
--- a/tests/core/ltlsynt.test
+++ b/tests/core/ltlsynt.test
@@ -836,4 +836,14 @@ ltlsynt --outs="" -f "GFb" | grep "UNREALIZABLE"
 ltlsynt --outs="" -f "1"
 
 ltlsynt --outs="" --ins="" -f "GFa" 2>&1 | \
-  grep "both --ins and --outs are specified"
\ No newline at end of file
+  grep "both --ins and --outs are specified"
+
+LTL='(((((G (((((((g_0) && (G (! (r_0)))) -> (F (! (g_0)))) && (((g_0) &&
+(X ((! (r_0)) && (! (g_0))))) -> (X ((r_0) R (! (g_0)))))) && (((g_1) &&
+(G (! (r_1)))) -> (F (! (g_1))))) && (((g_1) && (X ((! (r_1)) && (! (g_1))))) ->
+(X ((r_1) R (! (g_1)))))) && (((! (g_0)) && (true)) || ((true) && (! (g_1))))))
+&& ((r_0) R (! (g_0)))) && (G ((r_0) -> (F (g_0))))) && ((r_1) R (! (g_1)))) &&
+(G ((r_1) -> (F (g_1)))))'
+OUT='g_0, g_1'
+ltlsynt --outs="$OUT" -f "$LTL" --aiger=both --algo=acd | grep "aag 8 2 2 2 4"
+ltlsynt --outs="$OUT" -f "$LTL" --aiger=both --algo=lar | grep "aag 34 2 3 2 29"