ltlsynt: add --algo=ps

* bin/ltlsynt.cc: Implement this.
* tests/core/ltlsynt.test: Add a test case.
* NEWS: Mention it.

NEWS

@@ -18,6 +18,9 @@ New in spot 2.9.0.dev (not yet released)
     The default is 1 in "--high" mode, 2 in "--medium" mode or in
     "--deterministic --low" mode, and 0 in other "--low" modes.
 
+  - ltlsynt learned --algo=ps to use the default conversion to
+    deterministic parity automata (the same as ltl2tgba -DP'max odd').
+
   Library:
 
   - product_xor() and product_xnor() are two new versions of the

bin/ltlsynt.cc

@@ -74,10 +74,11 @@ static const argp_option options[] =
       " propositions", 0},
     /**************************************************/
     { nullptr, 0, nullptr, 0, "Fine tuning:", 10 },
-    { "algo", OPT_ALGO, "ds|sd|lar|lar.old", 0,
+    { "algo", OPT_ALGO, "sd|ds|ps|lar|lar.old", 0,
       "choose the algorithm for synthesis:\n"
-      " - sd:   split then determinize with Safra (default)\n"
+      " - sd:   translate to tgba, split, then determinize (default)\n"
-      " - ds:   determinize (Safra) then split\n"
+      " - ds:   translate to tgba, determinize, then split\n"
+      " - ps:   translate to dpa, then split\n"
       " - lar:  translate to a deterministic automaton with arbitrary"
       " acceptance condition, then use LAR to turn to parity,"
       " then split\n"
@@ -136,6 +137,7 @@ enum solver
 {
   DET_SPLIT,
   SPLIT_DET,
+  DPA_SPLIT,
   LAR,
   LAR_OLD,
 };
@@ -144,6 +146,7 @@ static char const *const solver_names[] =
   {
    "ds",
    "sd",
+   "ps",
    "lar",
    "lar.old"
   };
@@ -152,6 +155,7 @@ static char const *const solver_args[] =
 {
   "detsplit", "ds",
   "splitdet", "sd",
+  "dpasplit", "ps",
   "lar",
   "lar.old",
   nullptr
@@ -160,6 +164,7 @@ static solver const solver_types[] =
 {
   DET_SPLIT, DET_SPLIT,
   SPLIT_DET, SPLIT_DET,
+  DPA_SPLIT, DPA_SPLIT,
   LAR,
   LAR_OLD,
 };
@@ -354,10 +359,21 @@ namespace
       spot::stopwatch sw;
       bool want_time = verbose || opt_csv;
 
-      if (opt_solver == LAR || opt_solver == LAR_OLD)
+      switch (opt_solver)
         {
+        case LAR:
+        case LAR_OLD:
           trans_.set_type(spot::postprocessor::Generic);
           trans_.set_pref(spot::postprocessor::Deterministic);
+          break;
+        case DPA_SPLIT:
+          trans_.set_type(spot::postprocessor::ParityMaxOdd);
+          trans_.set_pref(spot::postprocessor::Deterministic
+                          | spot::postprocessor::Colored);
+          break;
+        case DET_SPLIT:
+        case SPLIT_DET:
+          break;
         }
 
       if (want_time)
@@ -423,6 +439,29 @@ namespace
                           << tmp->num_states() << " states\n";
               break;
             }
+          case DPA_SPLIT:
+            {
+              if (want_time)
+                sw.start();
+              aut->merge_states();
+              if (want_time)
+                paritize_time = sw.stop();
+              if (verbose)
+                std::cerr << "simplification done in " << paritize_time
+                          << " seconds\nDPA has " << aut->num_states()
+                          << " states\n";
+              if (want_time)
+                sw.start();
+              dpa = split_2step(aut, all_inputs);
+              spot::colorize_parity_here(dpa, true);
+              if (want_time)
+                split_time = sw.stop();
+              if (verbose)
+                std::cerr << "split inputs and outputs done in " << split_time
+                          << " seconds\nautomaton has "
+                          << dpa->num_states() << " states\n";
+              break;
+            }
           case SPLIT_DET:
             {
               if (want_time)

tests/core/ltlsynt.test

@@ -118,6 +118,20 @@ ltlsynt --ins='a' --outs='b' -f 'GFa <-> GFb' --verbose --realizability 2> out
 sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
 diff outx exp
 
+cat >exp <<EOF
+translating formula done in X seconds
+automaton has 3 states and 4 colors
+simplification done in X seconds
+DPA has 3 states
+split inputs and outputs done in X seconds
+automaton has 9 states
+parity game built in X seconds
+parity game solved in X seconds
+EOF
+ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --verbose --algo=ps 2> out
+sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
+diff outx exp
+
 cat >exp <<EOF
 translating formula done in X seconds
 automaton has 16 states and 2 colors
@@ -137,9 +151,10 @@ for r in '' '--real'; do
     opts="$r --ins=a --outs=b -f"
     ltlsynt --algo=ds $opts 'GFa <-> GFb' --csv=FILE || :
     ltlsynt --algo=sd $opts 'FGa <-> GF(b&XXb)' --csv='>>FILE' || :
+    ltlsynt --algo=ps $opts 'FGa <-> GF(b&XXb)' --csv='>>FILE' || :
     ltlsynt --algo=lar $opts 'FGc <-> GF(!b&XXb)' --csv='>>FILE' || :
     ltlsynt --algo=lar.old $opts 'FGa <-> GF(c&a)' --csv='>>FILE' || :
-    test 5 = `wc -l < FILE`
+    test 6 = `wc -l < FILE`
     # Make sure all lines in FILE have the same number of comas
     sed 's/[^,]//g' < FILE |
         ( read first
@@ -242,7 +257,7 @@ for i in 2 3 4 5 6 10; do
   ltl2tgba -f "!($F)" > negf_aut$i
 
   # test ltlsynt
-  for algo in sd ds lar lar.old; do
+  for algo in sd ds ps lar lar.old; do
     ltlsynt -f "$F" --ins="$IN" --outs="$OUT" --algo=$algo > out$i || true
     REAL=`head -1 out$i`
     test $REAL = $EXP