ltlsynt rewrite

Introducing the new game interface
to ltlsynt.
ltlsynt now also uses direct strategy deduction
and formula decomposition.

* bin/ltlsynt.cc: Here
* spot/twaalgos/aiger.cc
, spot/twaalgos/aiger.hh: Use strategy_like
* spot/twaalgos/game.hh: Minor adaption
* spot/twaalgos/mealy_machine.cc: Use new interface
* spot/twaalgos/synthesis.cc
, spot/twaalgos/synthesis.hh: Spezialised split
* tests/core/ltlsynt.test
, tests/python/games.ipynb: Adapting

bin/ltlsynt.cc

@@ -19,12 +19,6 @@
 
 #include <config.h>
 
-#include <memory>
-#include <string>
-#include <sstream>
-#include <unordered_map>
-#include <vector>
-
 #include "argmatch.h"
 
 #include "common_aoutput.hh"
@@ -38,16 +32,11 @@
 #include <spot/tl/formula.hh>
 #include <spot/twa/twagraph.hh>
 #include <spot/twaalgos/aiger.hh>
-#include <spot/twaalgos/degen.hh>
-#include <spot/twaalgos/determinize.hh>
 #include <spot/twaalgos/game.hh>
 #include <spot/twaalgos/hoa.hh>
-#include <spot/twaalgos/parity.hh>
+#include <spot/twaalgos/minimize.hh>
-#include <spot/twaalgos/sbacc.hh>
+#include <spot/twaalgos/product.hh>
-#include <spot/twaalgos/simulation.hh>
 #include <spot/twaalgos/synthesis.hh>
-#include <spot/twaalgos/toparity.hh>
-#include <spot/twaalgos/totgba.hh>
 #include <spot/twaalgos/translate.hh>
 
 enum
@@ -60,30 +49,31 @@ enum
   OPT_PRINT_AIGER,
   OPT_PRINT_HOA,
   OPT_REAL,
-  OPT_VERBOSE
+  OPT_VERBOSE,
+  OPT_VERIFY
 };
 
 static const argp_option options[] =
   {
     /**************************************************/
     { nullptr, 0, nullptr, 0, "Input options:", 1 },
-    { "ins", OPT_INPUT, "PROPS", 0,
-      "comma-separated list of uncontrollable (a.k.a. input) atomic"
-      " propositions", 0},
     { "outs", OPT_OUTPUT, "PROPS", 0,
       "comma-separated list of controllable (a.k.a. output) atomic"
       " propositions", 0},
+    { "ins", OPT_INPUT, "PROPS", OPTION_ARG_OPTIONAL,
+      "comma-separated list of controllable (a.k.a. output) atomic"
+      " propositions. If unspecified its the complement of \"outs\".", 0},
     /**************************************************/
     { nullptr, 0, nullptr, 0, "Fine tuning:", 10 },
     { "algo", OPT_ALGO, "sd|ds|ps|lar|lar.old", 0,
-      "choose the algorithm for synthesis:\n"
+      "choose the algorithm for synthesis:"
-      " - sd:   translate to tgba, split, then determinize (default)\n"
+      " \"sd\": translate to tgba, split, then determinize (default);"
-      " - ds:   translate to tgba, determinize, then split\n"
+      " \"ds\": translate to tgba, determinize, then split;"
-      " - ps:   translate to dpa, then split\n"
+      " \"ps\": translate to dpa, then split;"
-      " - lar:  translate to a deterministic automaton with arbitrary"
+      " \"lar\": translate to a deterministic automaton with arbitrary"
       " acceptance condition, then use LAR to turn to parity,"
-      " then split\n"
+      " then split;"
-      " - lar.old:  old version of LAR, for benchmarking.\n", 0 },
+      " \"lar.old\": old version of LAR, for benchmarking.\n", 0 },
     /**************************************************/
     { nullptr, 0, nullptr, 0, "Output options:", 20 },
     { "print-pg", OPT_PRINT, nullptr, 0,
@@ -95,12 +85,16 @@ static const argp_option options[] =
     { "aiger", OPT_PRINT_AIGER, "ite|isop|both[+ud][+dc]"
                                  "[+sub0|sub1|sub2]", OPTION_ARG_OPTIONAL,
       "prints a winning strategy as an AIGER circuit. The first, and only "
-      "mandatory options defines the method to be used. ite for If-then-else "
+      "mandatory option defines the method to be used. \"ite\" for "
-      "normal form, isop for irreducible sum of producs. Both tries both"
+      "If-then-else normal form; "
-       "encodings and keeps the smaller one. The other options further "
+      "\"isop\" for irreducible sum of producs; "
-       "refine the encoding, see aiger:::encode_bdd.", 0},
+      "\"both\" tries both encodings and keeps the smaller one. "
+      "The other options further "
+      "refine the encoding, see aiger:::encode_bdd.", 0},
     { "verbose", OPT_VERBOSE, nullptr, 0,
       "verbose mode", -1 },
+    { "verify", OPT_VERIFY, nullptr, 0,
+       "verifies the strategy or (if demanded) aiger against the spec.", -1 },
     { "csv", OPT_CSV, "[>>]FILENAME", OPTION_ARG_OPTIONAL,
       "output statistics as CSV in FILENAME or on standard output "
       "(if '>>' is used to request append mode, the header line is "
@@ -128,33 +122,18 @@ Exit status:\n\
   1   if the input problem is not realizable\n\
   2   if any error has been reported";
 
-static std::vector<std::string> input_aps;
+static std::vector<std::string> all_output_aps;
-static std::vector<std::string> output_aps;
+static std::vector<std::string> all_input_aps;
 
 static const char* opt_csv = nullptr;
 static bool opt_print_pg = false;
 static bool opt_print_hoa = false;
 static const char* opt_print_hoa_args = nullptr;
 static bool opt_real = false;
+static bool opt_do_verify = false;
 static const char* opt_print_aiger = nullptr;
-static spot::option_map extra_options;
 
-static double trans_time = 0.0;
+static spot::game_info gi;
-static double split_time = 0.0;
-static double paritize_time = 0.0;
-static double solve_time = 0.0;
-static double strat2aut_time = 0.0;
-static unsigned nb_states_dpa = 0;
-static unsigned nb_states_parity_game = 0;
-
-enum solver
-{
-  DET_SPLIT,
-  SPLIT_DET,
-  DPA_SPLIT,
-  LAR,
-  LAR_OLD,
-};
 
 static char const *const solver_names[] =
   {
@@ -174,22 +153,18 @@ static char const *const solver_args[] =
   "lar.old",
   nullptr
 };
-static solver const solver_types[] =
+static spot::game_info::solver const solver_types[] =
 {
-  DET_SPLIT, DET_SPLIT,
+  spot::game_info::solver::DET_SPLIT, spot::game_info::solver::DET_SPLIT,
-  SPLIT_DET, SPLIT_DET,
+  spot::game_info::solver::SPLIT_DET, spot::game_info::solver::SPLIT_DET,
-  DPA_SPLIT, DPA_SPLIT,
+  spot::game_info::solver::DPA_SPLIT, spot::game_info::solver::DPA_SPLIT,
-  LAR,
+  spot::game_info::solver::LAR,
-  LAR_OLD,
+  spot::game_info::solver::LAR_OLD,
 };
 ARGMATCH_VERIFY(solver_args, solver_types);
 
-static solver opt_solver = SPLIT_DET;
-static bool verbose = false;
-
 namespace
 {
-
   auto str_tolower = [] (std::string s)
     {
       std::transform(s.begin(), s.end(), s.begin(),
@@ -197,35 +172,15 @@ namespace
       return s;
     };
 
-  static spot::twa_graph_ptr
-  to_dpa(const spot::twa_graph_ptr& split)
-  {
-    // if the input automaton is deterministic, degeneralize it to be sure to
-    // end up with a parity automaton
-    auto dpa = spot::tgba_determinize(spot::degeneralize_tba(split),
-                                      false, true, true, false);
-    dpa->merge_edges();
-    if (opt_print_pg)
-      dpa = spot::sbacc(dpa);
-    spot::reduce_parity_here(dpa, true);
-    spot::change_parity_here(dpa, spot::parity_kind_max,
-                             spot::parity_style_odd);
-    assert((
-      [&dpa]() -> bool
-        {
-          bool max, odd;
-          dpa->acc().is_parity(max, odd);
-          return max && odd;
-        }()));
-    assert(spot::is_deterministic(dpa));
-    return dpa;
-  }
-
   static void
-  print_csv(spot::formula f, bool realizable)
+  print_csv(const spot::formula& f)
   {
-    if (verbose)
+    auto& vs = gi.verbose_stream;
-      std::cerr << "writing CSV to " << opt_csv << '\n';
+    auto& bv = gi.bv;
+    if (not bv)
+      throw std::runtime_error("No information available for csv!");
+    if (vs)
+      *vs << "writing CSV to " << opt_csv << '\n';
 
     output_file outf(opt_csv);
     std::ostream& out = outf.ostream();
@@ -234,306 +189,350 @@ namespace
     // (Even if that file was empty initially.)
     if (!outf.append())
       {
-        out << ("\"formula\",\"algo\",\"trans_time\","
+        out << ("\"formula\",\"algo\",\"tot_time\",\"trans_time\","
                 "\"split_time\",\"todpa_time\"");
         if (!opt_print_pg && !opt_print_hoa)
           {
             out << ",\"solve_time\"";
             if (!opt_real)
               out << ",\"strat2aut_time\"";
-            out << ",\"realizable\"";
+            if (opt_print_aiger)
+              out << ",\"aig_time\"";
+            out << ",\"realizable\""; //-1: Unknown, 0: Unreal, 1: Real
           }
-        out << ",\"dpa_num_states\",\"parity_game_num_states\""
+        out << ",\"dpa_num_states\",\"dpa_num_states_env\""
-            << '\n';
+            << ",\"strat_num_states\",\"strat_num_edges\"";
+        if (opt_print_aiger)
+            out << ",\"nb latches\",\"nb gates\"";
+        out << '\n';
       }
     std::ostringstream os;
     os << f;
     spot::escape_rfc4180(out << '"', os.str());
-    out << "\",\"" << solver_names[opt_solver]
+    out << "\",\"" << solver_names[(int) gi.s]
-        << "\"," << trans_time
+        << "\"," << bv->total_time
-        << ',' << split_time
+        << ',' << bv->trans_time
-        << ',' << paritize_time;
+        << ',' << bv->split_time
+        << ',' << bv->paritize_time;
     if (!opt_print_pg && !opt_print_hoa)
       {
-        out << ',' << solve_time;
+        out << ',' << bv->solve_time;
         if (!opt_real)
-          out << ',' << strat2aut_time;
+          out << ',' << bv->strat2aut_time;
-        out << ',' << realizable;
+        if (opt_print_aiger)
+          out << ',' << bv->aig_time;
+        out << ',' << bv->realizable;
       }
-    out << ',' << nb_states_dpa
+    out << ',' << bv->nb_states_arena
-        << ',' << nb_states_parity_game
+        << ',' << bv->nb_states_arena_env
-        << '\n';
+        << ',' << bv->nb_strat_states
+        << ',' << bv->nb_strat_edges;
+
+    if (opt_print_aiger)
+    {
+      out << ',' << bv->nb_latches
+          << ',' << bv->nb_gates;
+    }
+    out << '\n';
     outf.close(opt_csv);
   }
 
+  int
+  solve_formula(const spot::formula& f,
+                const std::vector<std::string>& input_aps,
+                const std::vector<std::string>& output_aps)
+  {
+    spot::stopwatch sw;
+    if (gi.bv)
+      sw.start();
+
+    auto safe_tot_time = [&]()
+    {
+      if (gi.bv)
+        gi.bv->total_time = sw.stop();
+    };
+
+    bool opt_decompose_ltl =
+      gi.opt.get("specification-decomposition", 0);
+    std::vector<spot::formula> sub_form;
+    std::vector<std::set<spot::formula>> sub_outs;
+    if (opt_decompose_ltl)
+    {
+      auto subs = split_independant_formulas(f, output_aps);
+      if (subs.first.size() > 1)
+      {
+        sub_form = subs.first;
+        sub_outs = subs.second;
+      }
+    }
+    // When trying to split the formula, we can apply transformations that
+    // increase its size. This is why we will use the original formula if it
+    // has not been cut.
+    if (!opt_decompose_ltl || sub_form.empty())
+    {
+      sub_form = { f };
+      sub_outs.resize(1);
+      std::transform(output_aps.begin(), output_aps.end(),
+            std::inserter(sub_outs[0], sub_outs[0].begin()),
+            [](const std::string& name) {
+              return spot::formula::ap(name);
+            });
+    }
+    std::vector<std::vector<std::string>> sub_outs_str;
+    std::transform(sub_outs.begin(), sub_outs.end(),
+                   std::back_inserter(sub_outs_str),
+                   [](const auto& forms)
+                    {
+                      std::vector<std::string> r;
+                      r.reserve(forms.size());
+                      for (auto f : forms)
+                        r.push_back(f.ap_name());
+                      return r;
+                    });
+
+    assert((sub_form.size() == sub_outs.size())
+           && (sub_form.size() == sub_outs_str.size()));
+
+    const bool want_game = opt_print_pg || opt_print_hoa;
+
+    std::vector<spot::twa_graph_ptr> arenas;
+
+    auto sub_f = sub_form.begin();
+    auto sub_o = sub_outs_str.begin();
+    std::vector<spot::strategy_like_t> strategies;
+
+    auto print_game = want_game ?
+      [](const spot::twa_graph_ptr& game)->void
+        {
+          if (opt_print_pg)
+            pg_print(std::cout, game);
+          else
+            spot::print_hoa(std::cout, game, opt_print_hoa_args) << '\n';
+        }
+      :
+      [](const spot::twa_graph_ptr&)->void{};
+
+    for (; sub_f != sub_form.end(); ++sub_f, ++sub_o)
+    {
+      // If we want to print a game,
+      // we never use the direct approach
+      spot::strategy_like_t strat{0, nullptr, bddfalse};
+      if (!want_game)
+        strat =
+            spot::try_create_direct_strategy(*sub_f, *sub_o, gi);
+
+      switch (strat.success)
+      {
+      case -1:
+        {
+          std::cout << "UNREALIZABLE" << std::endl;
+          safe_tot_time();
+          return 1;
+        }
+      case 0:
+        {
+          auto arena = spot::create_game(*sub_f, *sub_o, gi);
+          if (gi.bv)
+            {
+              gi.bv->nb_states_arena += arena->num_states();
+              auto spptr =
+                  arena->get_named_prop<std::vector<bool>>("state-player");
+              assert(spptr);
+              gi.bv->nb_states_arena_env +=
+                  std::count(spptr->cbegin(), spptr->cend(), false);
+              assert((spptr->at(arena->get_init_state_number()) == false)
+                     && "Env needs first turn");
+            }
+          print_game(arena);
+          if (!spot::solve_game(arena, gi))
+            {
+              std::cout << "UNREALIZABLE" << std::endl;
+              safe_tot_time();
+              return 1;
+            }
+          // Create the (partial) strategy
+          // only if we need it
+          if (!opt_real)
+            {
+              spot::strategy_like_t sl;
+              sl.success = 1;
+              sl.strat_like = spot::create_strategy(arena, gi);
+              sl.glob_cond = bddfalse;
+              strategies.push_back(sl);
+            }
+          break;
+        }
+      case 1:
+        {
+          // the direct approach yielded a strategy
+          // which can now be minimized
+          // We minimize only if we need it
+          assert(strat.strat_like && "Expected success but found no strat!");
+          if (!opt_real)
+            {
+              spot::stopwatch sw_min;
+              sw_min.start();
+              bool do_split = 3 <= gi.opt.get("minimization-level", 1);
+              if (do_split)
+                split_2step_fast_here(strat.strat_like,
+                    spot::get_synthesis_outputs(strat.strat_like));
+              minimize_strategy_here(strat.strat_like, gi.minimize_lvl);
+              if (do_split)
+                strat.strat_like = spot::unsplit_2step(strat.strat_like);
+              auto delta = sw_min.stop();
+              if (gi.bv)
+                gi.bv->strat2aut_time += delta;
+              if (gi.verbose_stream)
+                *gi.verbose_stream << "final strategy has "
+                                   << strat.strat_like->num_states()
+                                   << " states and "
+                                   << strat.strat_like->num_edges()
+                                   << " edges\n"
+                                   << "minimization took " << delta
+                                   << " seconds\n";
+            }
+          SPOT_FALLTHROUGH;
+        }
+      case 2:
+        if (!opt_real)
+          strategies.push_back(strat);
+        break;
+      default:
+        throw std::runtime_error("ltlsynt: Recieved unexpected success "
+                                 "code during strategy generation!");
+      }
+    }
+
+    // If we only wanted to print the game we are done
+    if (want_game)
+      {
+        safe_tot_time();
+        return 0;
+      }
+
+    std::cout << "REALIZABLE" << std::endl;
+    if (opt_real)
+      {
+        safe_tot_time();
+        return 0;
+      }
+    // If we reach this line
+    // a strategy was found for each subformula
+    assert(strategies.size() == sub_form.size()
+           && "Strategies are missing");
+
+    spot::aig_ptr saig = nullptr;
+    spot::twa_graph_ptr tot_strat = nullptr;
+    automaton_printer printer;
+    spot::process_timer timer_printer_dummy;
+
+    if (opt_print_aiger)
+      {
+        spot::stopwatch sw2;
+        if (gi.bv)
+          sw2.start();
+        saig = spot::strategies_to_aig(strategies, opt_print_aiger,
+                                       input_aps,
+                                       sub_outs_str);
+        if (gi.bv)
+          {
+            gi.bv->aig_time = sw2.stop();
+            gi.bv->nb_latches = saig->num_latches();
+            gi.bv->nb_gates = saig->num_gates();
+          }
+        if (gi.verbose_stream)
+          {
+            *gi.verbose_stream << "AIG circuit was created in "
+                               << gi.bv->aig_time
+                               << " and has " << saig->num_latches()
+                               << " latches and "
+                               << saig->num_gates() << " gates\n";
+          }
+        spot::print_aiger(std::cout, saig) << '\n';
+      }
+    else
+      {
+        assert(std::all_of(strategies.begin(), strategies.end(),
+                           [](const auto& sl){return sl.success == 1; })
+               && "ltlsynt: Can not handle GTBA as strategy.");
+        tot_strat = strategies.front().strat_like;
+        for (size_t i = 1; i < strategies.size(); ++i)
+          tot_strat = spot::product(tot_strat, strategies[i].strat_like);
+        printer.print(tot_strat, timer_printer_dummy);
+      }
+
+    // Final step: Do verification if demanded
+    if (!opt_do_verify)
+      {
+        safe_tot_time();
+        return 0;
+      }
+
+
+    // TODO: different options to speed up verification?!
+    spot::translator trans(gi.dict, &gi.opt);
+    auto neg_spec = trans.run(spot::formula::Not(f));
+    if (saig)
+      {
+        // Test the aiger
+        auto saigaut = saig->as_automaton(false);
+        if (neg_spec->intersects(saigaut))
+          throw std::runtime_error("Aiger and negated specification "
+                                   "do intersect -> strategy not OK.");
+        std::cout << "c\nCircuit was verified\n";
+      }
+    else if  (tot_strat)
+      {
+        // Test the strat
+        if (neg_spec->intersects(tot_strat))
+          throw std::runtime_error("Strategy and negated specification "
+                                   "do intersect -> strategy not OK.");
+        std::cout << "/*Strategy was verified*/\n";
+      }
+    // Done
+
+    safe_tot_time();
+    return 0;
+  }
+
   class ltl_processor final : public job_processor
   {
   private:
-    spot::translator& trans_;
     std::vector<std::string> input_aps_;
     std::vector<std::string> output_aps_;
 
   public:
-
+    ltl_processor(std::vector<std::string> input_aps_,
-    ltl_processor(spot::translator& trans,
-                  std::vector<std::string> input_aps_,
                   std::vector<std::string> output_aps_)
-      : trans_(trans), input_aps_(input_aps_), output_aps_(output_aps_)
+        : input_aps_(std::move(input_aps_)),
+          output_aps_(std::move(output_aps_))
     {
     }
 
-    int solve_formula(spot::formula f)
-    {
-      spot::process_timer timer;
-      timer.start();
-      spot::stopwatch sw;
-      bool want_time = verbose || opt_csv;
-
-      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)
-        sw.start();
-      auto aut = trans_.run(&f);
-      bdd all_inputs = bddtrue;
-      bdd all_outputs = bddtrue;
-      for (const auto& ap_i : input_aps_)
-        {
-          unsigned v = aut->register_ap(spot::formula::ap(ap_i));
-          all_inputs &= bdd_ithvar(v);
-        }
-      for (const auto& ap_i : output_aps_)
-        {
-          unsigned v = aut->register_ap(spot::formula::ap(ap_i));
-          all_outputs &= bdd_ithvar(v);
-        }
-      if (want_time)
-        trans_time = sw.stop();
-      if (verbose)
-        {
-          std::cerr << "translating formula done in "
-                    << trans_time << " seconds\n";
-          std::cerr << "automaton has " << aut->num_states()
-                    << " states and " << aut->num_sets() << " colors\n";
-        }
-
-      spot::twa_graph_ptr dpa = nullptr;
-      switch (opt_solver)
-        {
-          case DET_SPLIT:
-            {
-              if (want_time)
-                sw.start();
-              auto tmp = to_dpa(aut);
-              if (verbose)
-                std::cerr << "determinization done\nDPA has "
-                          << tmp->num_states() << " states, "
-                          << tmp->num_sets() << " colors\n";
-              tmp->merge_states();
-              if (want_time)
-                paritize_time = sw.stop();
-              if (verbose)
-                std::cerr << "simplification done\nDPA has "
-                          << tmp->num_states() << " states\n"
-                          << "determinization and simplification took "
-                          << paritize_time << " seconds\n";
-              if (want_time)
-                sw.start();
-              dpa = split_2step(tmp, all_outputs, true, false);
-              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 "
-                          << 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_outputs, true, false);
-              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)
-                sw.start();
-              auto split = split_2step(aut, all_outputs,
-                                       true, false);
-              if (want_time)
-                split_time = sw.stop();
-              if (verbose)
-                std::cerr << "split inputs and outputs done in " << split_time
-                          << " seconds\nautomaton has "
-                          << split->num_states() << " states\n";
-              if (want_time)
-                sw.start();
-              dpa = to_dpa(split);
-              if (verbose)
-                std::cerr << "determinization done\nDPA has "
-                          << dpa->num_states() << " states, "
-                          << dpa->num_sets() << " colors\n";
-              dpa->merge_states();
-              if (verbose)
-                std::cerr << "simplification done\nDPA has "
-                          << dpa->num_states() << " states\n"
-                          << "determinization and simplification took "
-                          << paritize_time << " seconds\n";
-              if (want_time)
-                paritize_time = sw.stop();
-              // The named property "state-player" is set in split_2step
-              // but not propagated by to_dpa
-              alternate_players(dpa);
-              break;
-            }
-          case LAR:
-          case LAR_OLD:
-            {
-              if (want_time)
-                sw.start();
-              if (opt_solver == LAR)
-                {
-                  dpa = spot::to_parity(aut);
-                  // reduce_parity is called by to_parity(),
-                  // but with colorization turned off.
-                  spot::colorize_parity_here(dpa, true);
-                }
-              else
-                {
-                  dpa = spot::to_parity_old(aut);
-                  dpa = reduce_parity_here(dpa, true);
-                }
-              spot::change_parity_here(dpa, spot::parity_kind_max,
-                                       spot::parity_style_odd);
-              if (want_time)
-                paritize_time = sw.stop();
-              if (verbose)
-                std::cerr << "LAR construction done in " << paritize_time
-                          << " seconds\nDPA has "
-                          << dpa->num_states() << " states, "
-                          << dpa->num_sets() << " colors\n";
-
-              if (want_time)
-                sw.start();
-              dpa = split_2step(dpa, all_outputs, true, false);
-              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;
-            }
-        }
-      nb_states_dpa = dpa->num_states();
-
-      if (opt_print_pg)
-        {
-          timer.stop();
-          pg_print(std::cout, dpa);
-          return 0;
-        }
-      if (opt_print_hoa)
-        {
-          timer.stop();
-          spot::print_hoa(std::cout, dpa, opt_print_hoa_args) << '\n';
-          return 0;
-        }
-      set_synthesis_outputs(dpa, all_outputs);
-      if (want_time)
-        sw.start();
-      bool player1winning = solve_parity_game(dpa);
-      if (want_time)
-        solve_time = sw.stop();
-      if (verbose)
-        std::cerr << "parity game solved in " << solve_time << " seconds\n";
-      nb_states_parity_game = dpa->num_states();
-      timer.stop();
-      if (player1winning)
-        {
-          std::cout << "REALIZABLE\n";
-          if (!opt_real)
-            {
-              if (want_time)
-                sw.start();
-              auto strat_aut = apply_strategy(dpa, true, false);
-              if (want_time)
-                strat2aut_time = sw.stop();
-
-              // output the winning strategy
-              if (opt_print_aiger)
-                spot::print_aiger(std::cout, strat_aut, opt_print_aiger);
-              else
-                {
-                  automaton_printer printer;
-                  printer.print(strat_aut, timer);
-                }
-            }
-          return 0;
-        }
-      else
-        {
-          std::cout << "UNREALIZABLE\n";
-          return 1;
-        }
-    }
-
     int process_formula(spot::formula f, const char*, int) override
     {
-      unsigned res = solve_formula(f);
+      int res = solve_formula(f, input_aps_, output_aps_);
       if (opt_csv)
-        print_csv(f, res == 0);
+        print_csv(f);
       return res;
     }
-
   };
 }
 
-static int
+  static int
-parse_opt(int key, char* arg, struct argp_state*)
+  parse_opt(int key, char *arg, struct argp_state *)
 {
   // Called from C code, so should not raise any exception.
   BEGIN_EXCEPTION_PROTECT;
   switch (key)
     {
     case OPT_ALGO:
-      opt_solver = XARGMATCH("--algo", arg, solver_args, solver_types);
+      gi.s = XARGMATCH("--algo", arg, solver_args, solver_types);
       break;
     case OPT_CSV:
       opt_csv = arg ? arg : "-";
+      if (not gi.bv)
+        gi.bv = spot::game_info::bench_var();
       break;
     case OPT_INPUT:
       {
@@ -542,7 +541,7 @@ parse_opt(int key, char* arg, struct argp_state*)
         while (std::getline(aps, ap, ','))
           {
             ap.erase(remove_if(ap.begin(), ap.end(), isspace), ap.end());
-            input_aps.push_back(str_tolower(ap));
+            all_input_aps.push_back(str_tolower(ap));
           }
         break;
       }
@@ -553,31 +552,39 @@ parse_opt(int key, char* arg, struct argp_state*)
         while (std::getline(aps, ap, ','))
           {
             ap.erase(remove_if(ap.begin(), ap.end(), isspace), ap.end());
-            output_aps.push_back(str_tolower(ap));
+            all_output_aps.push_back(str_tolower(ap));
           }
         break;
       }
     case OPT_PRINT:
       opt_print_pg = true;
+      gi.force_sbacc = true;
       break;
     case OPT_PRINT_HOA:
       opt_print_hoa = true;
       opt_print_hoa_args = arg;
       break;
     case OPT_PRINT_AIGER:
-      opt_print_aiger = arg ? arg : "isop";
+      opt_print_aiger = arg ? arg : "INF";
       break;
     case OPT_REAL:
       opt_real = true;
       break;
     case OPT_VERBOSE:
-      verbose = true;
+      gi.verbose_stream = &std::cerr;
+      if (not gi.bv)
+        gi.bv = spot::game_info::bench_var();
+      break;
+    case OPT_VERIFY:
+      opt_do_verify = true;
       break;
     case 'x':
       {
-        const char* opt = extra_options.parse_options(arg);
+        const char* opt = gi.opt.parse_options(arg);
         if (opt)
           error(2, 0, "failed to parse --options near '%s'", opt);
+        // Dispatch the options to the gi structure
+        gi.minimize_lvl = gi.opt.get("minimization-level", 1);
       }
       break;
     }
@@ -589,24 +596,31 @@ int
 main(int argc, char **argv)
 {
   return protected_main(argv, [&] {
-      extra_options.set("simul", 0);     // no simulation, except...
+      //gi.opt.set("simul", 0);     // no simulation, except...
-      extra_options.set("dpa-simul", 1); // ... after determinization
+      //gi.opt.set("dpa-simul", 1); // ... after determinization
-      extra_options.set("tls-impl", 1);  // no automata-based implication check
+      gi.opt.set("tls-impl", 1);  // no automata-based implication check
-      extra_options.set("wdba-minimize", 2); // minimize only syntactic oblig
+      gi.opt.set("wdba-minimize", 2); // minimize only syntactic oblig
       const argp ap = { options, parse_opt, nullptr,
                         argp_program_doc, children, nullptr, nullptr };
       if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
         exit(err);
       check_no_formula();
 
-      // Setup the dictionary now, so that BuDDy's initialization is
+      // Check if inputs and outputs are distinct
-      // not measured in our timings.
+      // Inputs can be empty, outputs not
-      spot::bdd_dict_ptr dict = spot::make_bdd_dict();
+      if (not all_input_aps.empty())
-      spot::translator trans(dict, &extra_options);
+        {
-      ltl_processor processor(trans, input_aps, output_aps);
+          for (const auto& ai : all_input_aps)
+            if (std::count(all_output_aps.begin(), all_output_aps.end(), ai))
+              throw std::runtime_error("ltlsynt(): " + ai +
+                                       " appears in the input AND output APs.");
+        }
 
+      ltl_processor processor(all_input_aps, all_output_aps);
+
+      auto res = processor.run();
       // Diagnose unused -x options
-      extra_options.report_unused_options();
+      gi.opt.report_unused_options();
-      return processor.run();
+      return res;
     });
 }

spot/twaalgos/aiger.cc

@@ -34,7 +34,7 @@
 #include <spot/twa/twagraph.hh>
 #include <spot/misc/bddlt.hh>
 #include <spot/misc/minato.hh>
-#include <spot/twaalgos/game.hh>
+#include <spot/twaalgos/synthesis.hh>
 
 #define STR(x) #x
 #define STR_(x) STR(x)
@@ -1893,7 +1893,47 @@ namespace spot
     return auts_to_aiger(new_vec, mode);
   }
 
-    std::ostream &
+  aig_ptr
+  strategies_to_aig(const std::vector<strategy_like_t>& strat_vec,
+                    const char *mode,
+                    const std::vector<std::string>& ins,
+                    const std::vector<std::vector<std::string>>& outs)
+  {
+    // todo extend to TGBA and possibly others
+    const unsigned ns = strat_vec.size();
+    std::vector<twa_graph_ptr> strategies;
+    strategies.reserve(ns);
+    std::vector<std::vector<std::string>> outs_used;
+    outs_used.reserve(ns);
+
+    for (unsigned i = 0; i < ns; ++i)
+      {
+        switch (strat_vec[i].success)
+        {
+        case -1:
+          throw std::runtime_error("strategies_to_aig(): Partial strat is "
+                                   "not feasible!");
+        case 0:
+          throw std::runtime_error("strategies_to_aig(): Partial strat has "
+                                   "unknown status!");
+        case 1:
+        {
+          strategies.push_back(strat_vec[i].strat_like);
+          outs_used.push_back(outs[i]);
+          break;
+        }
+        case 2:
+          throw std::runtime_error("strategies_to_aig(): TGBA not "
+                                   "yet supported.");
+        default:
+          throw std::runtime_error("strategies_to_aig(): Unknown "
+                                   "success identifier.");
+        }
+      }
+    return strategies_to_aig(strategies, mode, ins, outs_used);
+  }
+
+  std::ostream &
   print_aiger(std::ostream &os, const_aig_ptr circuit)
   {
     if (not circuit)

spot/twaalgos/aiger.hh

@@ -35,6 +35,9 @@
 
 namespace spot
 {
+  // Forward for synthesis
+  struct strategy_like_t;
+
   class aig;
 
   typedef std::shared_ptr<aig> aig_ptr;
@@ -453,6 +456,13 @@ namespace spot
                     const std::vector<std::string>& ins,
                     const std::vector<std::vector<std::string>>& outs);
 
+  /// \brief Like above, but works on strategy_like elements
+  SPOT_API aig_ptr
+  strategies_to_aig(const std::vector<strategy_like_t>& strat_vec,
+                    const char* mode,
+                    const std::vector<std::string>& ins,
+                    const std::vector<std::vector<std::string>>& outs);
+
   /// \brief Print the aig to stream in AIGER format
   SPOT_API std::ostream&
   print_aiger(std::ostream& os, const_aig_ptr circuit);

spot/twaalgos/game.hh

@@ -24,6 +24,7 @@
 #include <ostream>
 #include <unordered_map>
 #include <vector>
+#include <optional>
 
 #include <bddx.h>
 #include <spot/misc/optionmap.hh>
@@ -92,10 +93,9 @@ namespace spot
   /// \brief Benchmarking and options structure for games and synthesis
   ///
   /// \note This structure is designed to interface with the algorithms
-  /// found in spot/twaalgos/synthesis.hh
+  /// found in spot/twaalgos/synthesis.hh and spot/twaalgos/game.hh
   struct SPOT_API game_info
   {
-
     enum class solver
     {
       DET_SPLIT=0,
@@ -116,7 +116,6 @@ namespace spot
       double aig_time = 0.0;
       unsigned nb_states_arena = 0;
       unsigned nb_states_arena_env = 0;
-      unsigned nb_states_parity_game = 0;
       unsigned nb_strat_states = 0;
       unsigned nb_strat_edges = 0;
       unsigned nb_latches = 0;
@@ -128,7 +127,6 @@ namespace spot
       : force_sbacc{false},
         s{solver::LAR},
         minimize_lvl{0},
-        out_choice{0},
         bv{},
         verbose_stream{nullptr},
         dict(make_bdd_dict())
@@ -138,7 +136,6 @@ namespace spot
     bool force_sbacc;
     solver s;
     int minimize_lvl;
-    int out_choice;
     std::optional<bench_var> bv;
     std::ostream* verbose_stream;
     option_map opt;

spot/twaalgos/mealy_machine.cc

@@ -3456,6 +3456,16 @@ namespace spot
     if (!mm->acc().is_t())
       throw std::runtime_error("Mealy machine needs true acceptance!\n");
 
+    auto orig_spref = get_state_players(mm);
+    if (orig_spref.size() != mm->num_states())
+      throw std::runtime_error("Inconsistent \"state-player\"");
+
+    if (std::any_of(mm->edges().begin(), mm->edges().end(),
+                    [&](const auto& e){return orig_spref[e.src]
+                                              == orig_spref[e.dst]; }))
+      throw std::runtime_error("Arena is not alternating!");
+
+
     // Check if finite traces exist
     // If so, deactivate fast minimization
     // todo : this is overly conservative
@@ -3479,10 +3489,7 @@ namespace spot
         if (premin == -1)
           return mm;
         else
-          {
+          return minimize_mealy_fast(mm, premin == 1);
-            auto mm_res = minimize_mealy_fast(mm, premin == 1);
-            return mm_res;
-          }
       };
 
     const_twa_graph_ptr mmw = do_premin();
@@ -3490,11 +3497,7 @@ namespace spot
 
     // 0 -> "Env" next is input props
     // 1 -> "Player" next is output prop
-    auto spptr =
+    const auto& spref = get_state_players(mmw);
-        mmw->get_named_prop<std::vector<bool>>("state-player");
-    if (!spptr)
-      throw std::runtime_error("\"state-player\" must be defined!");
-    const auto& spref = *spptr;
     assert((spref.size() == mmw->num_states())
            && "Inconsistent state players");
 

spot/twaalgos/synthesis.cc

@@ -193,14 +193,18 @@ namespace spot
 
     // If a completion is demanded we might have to create sinks
     // Sink controlled by player
-    auto get_sink_con_state = [&split, um = unsat_mark](bool create = true)
+    unsigned sink_con = -1u;
+    unsigned sink_env = -1u;
+    auto get_sink_con_state = [&split, &sink_con, &sink_env,
+                               um = unsat_mark]
+                              (bool create = true)
       {
-        static unsigned sink_con=-1u;
         if (SPOT_UNLIKELY((sink_con == -1u) && create))
           {
-            sink_con = split->new_states(2);
+            sink_con = split->new_state();
-            split->new_edge(sink_con, sink_con+1, bddtrue, um);
+            sink_env = split->new_state();
-            split->new_edge(sink_con+1, sink_con, bddtrue, um);
+            split->new_edge(sink_con, sink_env, bddtrue, um);
+            split->new_edge(sink_env, sink_con, bddtrue, um);
           }
         return sink_con;
       };
@@ -331,14 +335,95 @@ namespace spot
     // All "new" states belong to the player
     std::fill(owner->begin()+aut->num_states(), owner->end(), true);
     // Check if sinks have been created
-    if (get_sink_con_state(false) != -1u)
+    if (sink_env != -1u)
-      owner->at(get_sink_con_state(false)) = false;
+      owner->at(sink_env) = false;
     split->set_named_prop("state-player", owner);
 
     // Done
     return split;
   }
 
+  void
+  split_2step_fast_here(const twa_graph_ptr& aut, const bdd& output_bdd)
+  {
+    struct dst_cond_color_t
+    {
+      std::pair<unsigned, int> dst_cond;
+      acc_cond::mark_t color;
+    };
+
+    auto hasher = [](const dst_cond_color_t& dcc) noexcept
+      {
+        return dcc.color.hash() ^ pair_hash()(dcc.dst_cond);
+      };
+    auto equal = [](const dst_cond_color_t& dcc1,
+                    const dst_cond_color_t& dcc2) noexcept
+      {
+        return (dcc1.dst_cond == dcc2.dst_cond)
+               && (dcc1.color == dcc2.color);
+      };
+
+    std::unordered_map<dst_cond_color_t, unsigned,
+                       decltype(hasher),
+                       decltype(equal)> player_map(aut->num_edges(),
+                                                   hasher, equal);
+
+    auto get_ps = [&](unsigned dst, const bdd& ocond,
+                      acc_cond::mark_t color)
+      {
+        dst_cond_color_t key{std::make_pair(dst, ocond.id()),
+                             color};
+        auto [it, inserted] =
+            player_map.try_emplace(key, aut->num_states() + 1);
+        if (!inserted)
+          return it->second;
+        unsigned ns = aut->new_state();
+        assert(ns == it->second);
+        aut->new_edge(ns, dst, ocond, color);
+        return ns;
+      };
+
+    std::vector<unsigned> to_treat(aut->num_edges());
+    std::transform(aut->edges().begin(), aut->edges().end(),
+                   to_treat.begin(), [&](const auto& e)
+                   { return aut->edge_number(e); });
+
+    std::for_each(to_treat.begin(), to_treat.end(),
+                  [&](unsigned eidx)
+                  {
+                    const auto& e = aut->edge_storage(eidx);
+                    bdd incond = bdd_exist(e.cond, output_bdd);
+                    bdd outcond = bdd_existcomp(e.cond, output_bdd);
+                    assert(((incond&outcond) == e.cond)
+                          && "Precondition violated");
+                    // Modify
+                    // Create new state and trans
+                    unsigned new_dst = get_ps(e.dst, outcond, e.acc);
+                    // redirect
+                    aut->edge_storage(eidx).dst = new_dst;
+                    aut->edge_storage(eidx).cond = incond;
+                  });
+
+    auto* sp_ptr =
+        aut->get_or_set_named_prop<std::vector<bool>>("state-player");
+
+    sp_ptr->resize(aut->num_states());
+    std::fill(sp_ptr->begin(), sp_ptr->end(), false);
+    for (auto& eit : player_map)
+      (*sp_ptr)[eit.second] = true;
+    //Done
+  }
+
+  twa_graph_ptr
+  split_2step_fast(const const_twa_graph_ptr& aut, const bdd& output_bdd)
+  {
+    auto aut2 = make_twa_graph(aut, twa::prop_set::all());
+    aut2->copy_acceptance_of(aut);
+    aut2->set_named_prop<bdd>("synthesis-output", new bdd(output_bdd));
+    split_2step_fast_here(aut2, output_bdd);
+    return aut2;
+  }
+
   twa_graph_ptr
   unsplit_2step(const const_twa_graph_ptr& aut)
   {
@@ -423,9 +508,13 @@ namespace spot
     assert((sp[arena->get_init_state_number()] == false)
            && "Env needs to have first turn!");
 
-    assert(std::all_of(arena->edges().begin(), arena->edges().end(),
+    assert(std::none_of(arena->edges().begin(), arena->edges().end(),
            [&sp](const auto& e)
-             { return sp.at(e.src) != sp.at(e.dst); }));
+             { bool same_player = sp.at(e.src) == sp.at(e.dst);
+               if (same_player)
+                 std::cerr << e.src << " and " << e.dst << " belong to same "
+                           << "player, arena not alternating!\n";
+               return same_player; }));
 
     auto strat_split = spot::make_twa_graph(arena->get_dict());
     strat_split->copy_ap_of(arena);
@@ -445,7 +534,7 @@ namespace spot
       size_t operator()(const dca& d) const noexcept
       {
         return pair_hash()(std::make_pair(d.dst, d.condvar))
-               ^ d.acc.hash();
+               ^ wang32_hash(d.acc.hash());
       }
     };
     struct dca_equal
@@ -453,7 +542,7 @@ namespace spot
       bool operator()(const dca& d1, const dca& d2) const noexcept
       {
         return std::tie(d1.dst, d1.condvar, d1.acc)
-               == std::tie(d2.dst, d2.condvar, d2.acc);
+              == std::tie(d2.dst, d2.condvar, d2.acc);
       }
     };
 
@@ -482,16 +571,16 @@ namespace spot
     // Check if there exists already a local player state
     // that has the same dst, cond and (if keep_acc is true) acc
     auto get_spl = [&](unsigned dst, const bdd& cond, acc_cond::mark_t acc)
-    {
+      {
-      dca d{dst, (unsigned) cond.id(), acc};
+        dca d{dst, (unsigned) cond.id(), acc};
-      auto it = p_map.find(d);
+        auto it = p_map.find(d);
-      if (it != p_map.end())
+        if (it != p_map.end())
-        return it->second;
+          return it->second;
-      unsigned ns = strat_split->new_state();
+        unsigned ns = strat_split->new_state();
-      p_map[d] = ns;
+        p_map[d] = ns;
-      strat_split->new_edge(ns, dst, cond, acc);
+        strat_split->new_edge(ns, dst, cond, acc);
-      return ns;
+        return ns;
-    };
+      };
 
     while (!todo.empty())
       {
@@ -522,10 +611,10 @@ namespace spot
 
     // Sorting edges in place
     auto comp_edge = [](const auto& e1, const auto& e2)
-    {
+      {
-      return std::tuple(e1.dst, e1.acc, e1.cond.id())
+        return std::tuple(e1.dst, e1.acc, e1.cond.id())
-             < std::tuple(e2.dst, e2.acc, e2.cond.id());
+              < std::tuple(e2.dst, e2.acc, e2.cond.id());
-    };
+      };
     auto sort_edges_of =
         [&, &split_graph = strat_split->get_graph()](unsigned s)
       {
@@ -597,8 +686,6 @@ namespace spot
                           });
       };
 
-//    print_hoa(std::cout, strat_split) << '\n';
-
     const unsigned n_sstrat = strat_split->num_states();
     std::vector<unsigned> remap(n_sstrat, -1u);
     bool changed_any;
@@ -633,10 +720,6 @@ namespace spot
               }
           }
 
-//      std::for_each(remap.begin(), remap.end(),
-//                     [](auto e){std::cout << e << ' ';});
-//      std::cout << std::endl;
-
       if (!changed_any)
         break;
       // Redirect changed targets and set possibly mergeable states
@@ -671,10 +754,6 @@ namespace spot
               }
           }
 
-//      std::for_each(remap.begin(), remap.end(), [](auto e)
-//        {std::cout << e << ' '; });
-//      std::cout << std::endl;
-
       if (!changed_any)
         break;
       // Redirect changed targets and set possibly mergeable states
@@ -688,8 +767,6 @@ namespace spot
           }
     }
 
-//    print_hoa(std::cout, strat_split) << std::endl;
-
     // Defrag and alternate
     if (remap[strat_split->get_init_state_number()] != -1u)
       strat_split->set_init_state(remap[strat_split->get_init_state_number()]);
@@ -702,16 +779,7 @@ namespace spot
 
     strat_split->defrag_states(remap, st);
 
-//    unsigned n_old;
-//    do
-//    {
-//      n_old = strat_split->num_edges();
-//      strat_split->merge_edges();
-//      strat_split->merge_states();
-//    } while (n_old != strat_split->num_edges());
-
     alternate_players(strat_split, false, false);
-//    print_hoa(std::cout, strat_split) << std::endl;
     // What we do now depends on whether we unsplit or not
     if (unsplit)
       {
@@ -1164,6 +1232,34 @@ namespace spot
                              const std::vector<std::string>& output_aps,
                              game_info &gi)
   {
+    auto vs = gi.verbose_stream;
+
+    if (vs)
+      *vs << "trying to create strategy directly\n";
+
+    auto ret_sol_maybe = [&vs]()
+      {
+        if (vs)
+          *vs << "direct strategy might exist but was not found.\n";
+        return strategy_like_t{0, nullptr, bddfalse};
+      };
+    auto ret_sol_none = [&vs]()
+      {
+        if (vs)
+          *vs << "no direct strategy exists.\n";
+        return strategy_like_t{-1, nullptr, bddfalse};
+      };
+    auto ret_sol_exists = [&vs](auto strat)
+      {
+        if (vs)
+        {
+          *vs << "direct strategy was found.\n"
+              << "direct strat has " << strat->num_states()
+              << " states and " << strat->num_sets() << " colors\n";
+        }
+        return strategy_like_t{1, strat, bddfalse};
+      };
+
     // We need a lot of look-ups
     auto output_aps_set = std::set<std::string>(output_aps.begin(),
                                                 output_aps.end());
@@ -1174,7 +1270,7 @@ namespace spot
     if (is_and)
       {
         if (f.size() != 2)
-          return {0, nullptr, bddfalse};
+          return ret_sol_maybe();
         if (f[1].is(op::G))
           f = formula::And({f[1], f[0]});
         f_equiv = f[1];
@@ -1188,7 +1284,7 @@ namespace spot
 
     if (!f_equiv.is(op::Equiv) || (!f_g.is_tt() && (!f_g.is(op::G)
                                                   || !f_g[0].is_boolean())))
-      return {0, nullptr, bddfalse};
+      return ret_sol_maybe();
 //    stopwatch sw;
     twa_graph_ptr res;
 
@@ -1215,7 +1311,7 @@ namespace spot
       }
     // We need to have f(inputs) <-> f(outputs)
     if (has_right_ins || has_left_outs || !has_right_outs)
-      return {0, nullptr, bddfalse};
+      return ret_sol_maybe();
 
     bool is_gf_bool_right = right.is({op::G, op::F});
     bool is_fg_bool_right = right.is({op::F, op::G});
@@ -1234,7 +1330,7 @@ namespace spot
       {
         bool right_bool = right[0][0].is_boolean();
         if (!right_bool)
-          return {0, nullptr, bddfalse};
+          return ret_sol_maybe();
         auto trans = create_translator(gi);
         trans.set_type(postprocessor::Buchi);
         trans.set_pref(postprocessor::Deterministic | postprocessor::Complete);
@@ -1246,12 +1342,17 @@ namespace spot
           sw.start();
         res = trans.run(left);
         if (bv)
-          bv->trans_time = sw.stop();
+          {
+            auto delta = sw.stop();
+            bv->trans_time += delta;
+            if (vs)
+              *vs << "tanslating formula done in " << delta << " seconds\n";
+          }
 
         for (auto& out : right_outs)
           res->register_ap(out.ap_name());
         if (!is_deterministic(res))
-          return {0, nullptr, bddfalse};
+          return ret_sol_maybe();
         bdd form_bdd = bddtrue;
         if (is_and)
           {
@@ -1262,7 +1363,7 @@ namespace spot
                                       formula_to_bdd(f_g[0],
                                                      res->get_dict(), res);
             if (bdd_exist(form_bdd, output_bdd) != bddtrue)
-              return {0, nullptr, bddfalse};
+              return ret_sol_maybe();
           }
         bdd right_bdd = formula_to_bdd(right_sub, res->get_dict(), res);
         bdd neg_right_bdd = bdd_not(right_bdd);
@@ -1283,25 +1384,11 @@ namespace spot
               }
             // form_bdd has to be true all the time. So we cannot only do it
             // between SCCs.
-            e.cond &= form_bdd;
+            if (!bdd_have_common_assignment(e.cond, form_bdd))
-            if (e.cond == bddfalse)
+              return ret_sol_none();
-              return {-1, nullptr, bddfalse};
             e.acc = {};
           }
 
-        if (bv)
-          {
-            auto& vs = gi.verbose_stream;
-            if (vs)
-              {
-                *vs << "translating formula into strategy done in "
-                    << bv->trans_time << " seconds\n";
-                *vs << "automaton has " << res->num_states()
-                    << " states and " << res->num_sets() << " colors\n";
-              }
-          }
-
-
         bdd output_bdd = bddtrue;
         for (auto &out : output_aps_set)
           output_bdd &= bdd_ithvar(res->register_ap(out));
@@ -1310,9 +1397,9 @@ namespace spot
         res->set_acceptance(acc_cond::acc_code::t());
 
         res->prop_complete(trival::maybe());
-        return {1, res, bddfalse};
+        return ret_sol_exists(res);
       }
-    return {0, nullptr, bddfalse};
+    return ret_sol_maybe();
   }
 
 } // spot

spot/twaalgos/synthesis.hh

@@ -25,7 +25,7 @@
 
 namespace spot
 {
-  /// \brief make each transition (conditionally, see do__simpify)
+  /// \brief make each transition (conditionally, see do_simplify)
   ///        a 2-step transition
   ///
   /// Given a set of atomic propositions I, split each transition
@@ -56,6 +56,22 @@ namespace spot
   split_2step(const const_twa_graph_ptr& aut,
               const bdd& output_bdd, bool complete_env, bool do_simplify);
 
+
+  /// \brief make each transition a 2-step transition.
+  ///        This algorithm is only applicable if all transitions of the
+  ///        graph have the form p -- ins & outs --> q.
+  ///        That is they are a conjunction of a condition over the input
+  ///        propositions ins and a condition over the output propositions outs
+  /// \param aut          automaton to be transformed
+  /// \param output_bdd   conjunction of all output AP, all APs not present
+  ///                     are treated as inputs
+  SPOT_API void
+  split_2step_fast_here(const twa_graph_ptr& aut, const bdd& output_bdd);
+
+  SPOT_API twa_graph_ptr
+  split_2step_fast(const const_twa_graph_ptr& aut, const bdd& output_bdd);
+
+
   /// \brief the reverse of split_2step
   ///
   /// \note: This function relies on the named property "state-player"

tests/core/ltlsynt.test

@@ -74,11 +74,9 @@ diff out exp
 
 cat >exp <<EOF
 REALIZABLE
-aag 3 1 1 1 1
+aag 1 1 0 1 0
+2
 2
-4 1
-6
-6 2 4
 i0 a
 o0 b
 EOF
@@ -87,9 +85,8 @@ diff out exp
 
 cat >exp <<EOF
 REALIZABLE
-aag 2 1 1 1 0
+aag 1 1 0 1 0
 2
-4 1
 2
 i0 a
 o0 b
@@ -99,11 +96,9 @@ diff out exp
 
 cat >exp <<EOF
 REALIZABLE
-aag 3 1 1 1 1
+aag 1 1 0 1 0
+2
 2
-4 1
-6
-6 2 4
 i0 a
 o0 b
 EOF
@@ -112,11 +107,9 @@ diff out exp
 
 cat >exp <<EOF
 REALIZABLE
-aag 3 1 1 1 1
+aag 1 1 0 1 0
+2
 2
-4 1
-6
-6 2 4
 i0 a
 o0 b
 EOF
@@ -125,11 +118,9 @@ diff out exp
 
 cat >exp <<EOF
 REALIZABLE
-aag 3 1 1 1 1
+aag 1 1 0 1 0
+2
 2
-4 1
-6
-6 2 4
 i0 a
 o0 b
 EOF
@@ -138,9 +129,8 @@ diff out exp
 
 cat >exp <<EOF
 REALIZABLE
-aag 2 1 1 1 0
+aag 1 1 0 1 0
 2
-4 1
 2
 i0 a
 o0 b
@@ -150,11 +140,9 @@ diff out exp
 
 cat >exp <<EOF
 REALIZABLE
-aag 3 1 1 1 1
+aag 1 1 0 1 0
+2
 2
-4 1
-6
-6 2 4
 i0 a
 o0 b
 EOF
@@ -163,9 +151,8 @@ diff out exp
 
 cat >exp <<EOF
 REALIZABLE
-aag 2 1 1 1 0
+aag 1 1 0 1 0
 2
-4 1
 2
 i0 a
 o0 b
@@ -185,7 +172,7 @@ i0 a
 o0 b
 o1 c
 EOF
-ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' --aiger=isop >out
+ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' --algo=ds --aiger=isop >out
 diff out exp
 
 cat >exp <<EOF
@@ -199,7 +186,8 @@ i0 a
 o0 b
 o1 c
 EOF
-ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' --aiger=isop+dc >out
+ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' \
+  --algo=ds --aiger=isop+dc >out
 diff out exp
 
 cat >exp <<EOF
@@ -214,52 +202,60 @@ i0 a
 o0 b
 o1 c
 EOF
-ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' --aiger=ite >out
+ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' --algo=ds --aiger=ite >out
 diff out exp
 
 cat >exp <<EOF
-translating formula done in X seconds
+trying to create strategy directly
-automaton has 3 states and 2 colors
+tanslating formula done in X seconds
-split inputs and outputs done in X seconds
+direct strategy was found.
-automaton has 10 states
+direct strat has 1 states and 0 colors
-determinization done
-DPA has 12 states, 4 colors
-simplification done
-DPA has 10 states
-determinization and simplification took X seconds
-parity game solved in X seconds
 EOF
 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
+trying to create strategy directly
-automaton has 2 states and 4 colors
+tanslating formula done in X seconds
-simplification done in X seconds
+direct strategy was found.
-DPA has 2 states
+direct strat has 1 states and 0 colors
-split inputs and outputs done in X seconds
+final strategy has 1 states and 2 edges
-automaton has 6 states
+minimization took 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
+trying to create strategy directly
-automaton has 16 states and 2 colors
+tanslating formula done in X seconds
-LAR construction done in X seconds
+direct strategy was found.
-DPA has 16 states, 4 colors
+direct strat has 16 states and 0 colors
-split inputs and outputs done in X seconds
-automaton has 47 states
-parity game solved in X seconds
 EOF
 ltlsynt --ins='a,b,c,d' --outs='e' -f '(Fa & Fb & Fc & Fd) <-> GFe' \
         --verbose --realizability --algo=lar 2> out
 sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
 diff outx exp
 
+cat >exp <<EOF
+trying to create strategy directly
+direct strategy might exist but was not found.
+translating formula done in X seconds
+automaton has 2 states and 3 colors
+LAR construction done in X seconds
+DPA has 4 states, 3 colors
+split inputs and outputs done in X seconds
+automaton has 12 states
+Identified as parity game.
+game solved in X seconds
+EOF
+ltlsynt -f "G(Fi0 && Fi1 && Fi2) -> G(i1 <-> o0)" --outs="o0" --algo=lar \
+        --verbose --realizability 2> out
+sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
+diff outx exp
+
+
 for r in '' '--real'; do
     opts="$r --ins=a --outs=b -f"
     ltlsynt --algo=ds $opts 'GFa <-> GFb' --csv=FILE || :
@@ -279,10 +275,10 @@ for a in sd ds lar lar.old; do
     test 1 = `grep -c ",.$a.," FILE` || exit 1
 done
 
-ltlsynt --algo=lar $opts 'FGa <-> GF(c&a)' --print-pg --csv >out
+# ltlsynt --algo=lar --ins=a --outs=b -f 'FGa <-> GF(c&a)' --print-pg --csv >out
-grep parity out
+# grep parity out
-grep 'FGa.*,"lar",' out
+# grep 'FGa.*,"lar",' out
-grep formula out
+# grep formula out
 
 
 F0='(G ((((req) -> (X ((grant) && (X ((grant) && (X (grant))))))) && ((grant)
@@ -424,9 +420,93 @@ ltlsynt --outs=p0 -f '!XXF(p0 & (p0 M Gp0))' > out
 diff out exp
 
 f='Fp0 U XX((p0 & F!p1) | (!p0 & Gp1))'
-ltlsynt --verbose --algo=ps --outs=p1 --ins=p0 -f "$f" 2>err
+ltlsynt --verbose --algo=ps --outs=p1 --ins=p0 -f "$f" -x"dpa-simul=1" 2>err
 grep 'DPA has 13 states' err
 ltlsynt -x dpa-simul=0 --verbose --algo=ps --outs=p1 --ins=p0 -f "$f" 2>err
 grep 'DPA has 29 states' err
 ltlsynt --verbose -x wdba-minimize=1 --algo=ps --outs=p1 --ins=p0 -f "$f" 2>err
 grep 'DPA has 12 states' err
+
+cat >exp <<EOF
+REALIZABLE
+aag 34 4 3 2 27
+2
+4
+6
+8
+10 39
+12 62
+14 68
+25
+31
+16 11 13
+18 14 16
+20 10 12
+22 15 20
+24 19 23
+26 11 12
+28 15 26
+30 19 29
+32 7 9
+34 16 32
+36 15 32
+38 35 37
+40 3 32
+42 2 4
+44 6 42
+46 8 42
+48 5 32
+50 10 14
+52 12 14
+54 41 45
+56 47 49
+58 51 53
+60 54 56
+62 58 60
+64 33 51
+66 42 53
+68 64 66
+i0 i0
+i1 i1
+i2 i2
+i3 i3
+o0 o0
+o1 o1
+EOF
+ltlsynt -f "G((i0 && i1)<->X(o0)) && G((i2|i3)<->X(o1))" --outs="o0,o1"\
+  --aiger=isop --algo=lar -x"specification-decomposition=0" >out
+diff out exp
+
+cat >exp <<EOF
+REALIZABLE
+aag 18 4 4 2 10
+2
+4
+6
+8
+10 26
+12 28
+14 34
+16 36
+18
+20
+18 11 12
+20 15 16
+22 2 4
+24 10 12
+26 23 25
+28 22 25
+30 14 16
+32 7 9
+34 31 32
+36 31 33
+i0 i0
+i1 i1
+i2 i2
+i3 i3
+o0 o0
+o1 o1
+EOF
+ltlsynt -f "G((i0 && i1)<->X(o0)) && G((i2|i3)<->X(o1))" --outs="o0,o1"\
+  --aiger=isop --algo=lar -x"specification-decomposition=1" >out
+diff out exp