ltlsynt: generalization of the bypass

* spot/twaalgos/synthesis.cc, spot/twaalgos/synthesis.hh: generalize the
  bypass and avoid to construct a strategy when we want realizability.
* bin/ltlsynt.cc: adapt for realizability
* tests/core/ltlsynt.test: update tests

bin/ltlsynt.cc

@@ -376,7 +376,7 @@ namespace
       // we never use the direct approach
       if (!want_game)
         m_like =
-            spot::try_create_direct_strategy(*sub_f, *sub_o, *gi);
+            spot::try_create_direct_strategy(*sub_f, *sub_o, *gi, !opt_real);
 
       switch (m_like.success)
       {
@@ -431,7 +431,8 @@ namespace
           // the direct approach yielded a strategy
           // which can now be minimized
           // We minimize only if we need it
-          assert(m_like.mealy_like && "Expected success but found no mealy!");
+          assert(opt_real ||
+            (m_like.mealy_like && "Expected success but found no mealy!"));
           if (!opt_real)
             {
               // Keep the machine split for aiger

spot/twaalgos/synthesis.cc

@@ -1180,16 +1180,19 @@ namespace spot
   mealy_like
   try_create_direct_strategy(formula f,
                              const std::vector<std::string>& output_aps,
-                             synthesis_info &gi)
+                             synthesis_info &gi, bool want_strategy)
   {
     auto vs = gi.verbose_stream;
     auto& bv = gi.bv;
+    bdd_dict_ptr& dict = gi.dict;
+    int tmp;
 
     if (vs)
       *vs << "trying to create strategy directly for " << f << '\n';
 
-    auto ret_sol_maybe = [&vs]()
+    auto ret_sol_maybe = [&vs, &tmp, &dict]()
       {
+        dict->unregister_all_my_variables(&tmp);
         if (vs)
           *vs << "direct strategy might exist but was not found.\n";
         return mealy_like{
@@ -1197,8 +1200,9 @@ namespace spot
                   nullptr,
                   bddfalse};
       };
-    auto ret_sol_none = [&vs]()
+    auto ret_sol_none = [&vs, &tmp, &dict]()
       {
+        dict->unregister_all_my_variables(&tmp);
         if (vs)
           *vs << "no strategy exists.\n";
         return mealy_like{
@@ -1207,15 +1211,23 @@ namespace spot
                   bddfalse};
       };
 
-    auto ret_sol_exists = [&vs](auto strat)
+    auto ret_sol_exists =
+      [&vs, &want_strategy, &tmp, &dict](twa_graph_ptr strat)
       {
+        dict->unregister_all_my_variables(&tmp);
         if (vs)
           {
-            *vs << "direct strategy was found.\n"
+            *vs << "direct strategy was found.\n";
-                << "direct strat has " << strat->num_states()
+            if (want_strategy)
+            {
+                *vs << "direct strat has " << strat->num_states()
                 << " states, " << strat->num_edges()
                 << " edges and " << strat->num_sets() << " colors\n";
+
             }
+          }
+        if (strat)
+          strat->merge_edges();
         return mealy_like{
                   mealy_like::realizability_code::REALIZABLE_REGULAR,
                   strat,
@@ -1223,88 +1235,142 @@ namespace spot
       };
     formula_2_inout_props form2props(output_aps);
 
-    auto output_aps_set = std::set<std::string>(output_aps.begin(),
+    formula f_g, f_other;
-                                                output_aps.end());
+    // If it is G(α) ∧ G(β) ∧ …
-
-    formula f_g = formula::tt(), f_left, f_right;
-
-    // If we have a formula like G(b₁) ∧ (φ ↔ GFb₂), we extract b₁ and
-    // continue the construction for (φ ↔ GFb₂).
     if (f.is(op::And))
     {
-      if (f.size() != 2)
+      std::vector<formula> gs;
-        return ret_sol_maybe();
+      std::vector<formula> others;
-      if (f[0].is(op::G) && f[0][0].is_boolean())
+      for (auto child : f)
+        if (child.is(op::G) && child[0].is_boolean())
+          gs.push_back(child[0]);
+        else
+          others.push_back(child);
+
+      f_g = formula::And(gs);
+      f_other = formula::And(others);
+    }
+    else if (f.is(op::G) && f[0].is_boolean())
     {
       f_g = f[0];
-        f = f[1];
+      f_other = formula::tt();
-      }
-      else if (f[1].is(op::G) && f[1][0].is_boolean())
-      {
-        f_g = f[1];
-        f = f[0];
     }
     else
-        return ret_sol_maybe();
+    {
+      f_g = formula::tt();
+      f_other = f;
     }
-    if (f.is(op::Equiv))
-    {
-      auto [left_ins, left_outs] = form2props.aps_of(f[0]);
-      auto [right_ins, right_outs] = form2props.aps_of(f[1]);
 
-      auto properties_vector = [](const formula& f,
+    // We have to check if the content of G is realizable (input-complete)
-                                  const std::set<formula>& ins,
+    bdd output_bdd_tmp = bddtrue;
-                                  const std::set<formula>& outs)
+    for (auto& out : output_aps)
+      output_bdd_tmp &= bdd_ithvar(
+        dict->register_proposition(formula::ap(out), &tmp));
+
+    if (!f_g.is_tt())
     {
-        return std::vector<bool>
+      auto g_bdd = formula_to_bdd(f_g, dict, &tmp);
+      if (bdd_exist(g_bdd, output_bdd_tmp) != bddtrue)
+        return ret_sol_none();
+    }
+
+    if (f_other.is(op::Equiv))
     {
-          f.is({op::G, op::F}) && f[0][0].is_boolean() && ins.empty(),
+      // Check if FG or GF
-          f.is_syntactic_recurrence() && outs.empty(),
+      auto is_general = [&tmp, &output_bdd_tmp, &dict](const formula &f,
-          // f is FG(bool)
+                                                       op first, op second)
-          f.is({op::F, op::G}) && f[0][0].is_boolean() && ins.empty(),
+      {
-          f.is_syntactic_persistence() && outs.empty()
+        if (!f.is({first, second}) || !f[0][0].is_boolean())
+          return false;
+        auto f_bdd = formula_to_bdd(f[0][0], dict, &tmp);
+        if (bdd_exist(f_bdd, output_bdd_tmp) != bddtrue)
+          return false;
+        f_bdd = formula_to_bdd(formula::Not(f[0][0]), dict, &tmp);
+        bool res = (bdd_exist(f_bdd, output_bdd_tmp) == bddtrue);
+        return res;
       };
+
+      auto is_gf = [is_general](const formula& f)
+      {
+        return is_general(f, op::G, op::F);
       };
-      // We need to detect
+
-      // GF(outs) ↔ recurrence(ins),
+      auto is_fg = [is_general](const formula& f)
-      // recurrence(ins) ↔ GF(outs),
+      {
-      // FG(outs) ↔ persistence(ins),
+        return is_general(f, op::F, op::G);
-      // persistence(ins) ↔ FG(outs)
+      };
-      const auto left_properties = properties_vector(f[0], left_ins, left_outs),
+
-              right_properties = properties_vector(f[1], right_ins, right_outs);
+      auto is_co_bu = [](const formula &f, const std::set<formula>& outs)
+      {
+        return outs.empty() && f.is_syntactic_obligation();
+      };
+
+      auto is_buchi = [](const formula &f, const std::set<formula>& outs)
+      {
+        return outs.empty() && f.is_syntactic_recurrence();
+      };
+
+      auto properties_vector = [&](const formula &f,
+                            const std::set<formula> &outs)
+      {
+        auto is_lgf = is_gf(f);
+        auto is_lfg = is_fg(f);
+        return std::vector<bool>{
+            // f is GF(ins + outs) <-> buchi(ins)
+            is_lgf,
+            is_buchi(f, outs),
+            // f is FG(ins + outs) <-> co-buchi(ins)
+            is_lfg,
+            is_co_bu(f, outs)};
+      };
+
+
+      auto [left_ins, left_outs] = form2props.aps_of(f_other[0]);
+      auto [right_ins, right_outs] = form2props.aps_of(f_other[1]);
+
+      auto left_properties = properties_vector(f_other[0], left_outs);
+      auto right_properties = properties_vector(f_other[1], right_outs);
+
       unsigned combin = -1U;
       for (unsigned i = 0; i < 4; ++i)
-      {
+        if (left_properties[i] && right_properties[(i % 2) ? (i - 1) : (i + 1)])
-        if (left_properties[i] && right_properties[(i%2) ? (i-1) : (i+1)])
         {
           combin = i;
           break;
         }
-      }
+
+      // If we don't match, we don't know
       if (combin == -1U)
         return ret_sol_maybe();
 
-      // left is the recurrence (resp. persistence)
+      // We know that a strategy exists and we don't want to construct it.
-      // right is GF(outs) (resp. GF(outs))
+      if (!want_strategy)
-      // If f[0] is GF or FG
+        return ret_sol_exists(nullptr);
-      f_left = f[(combin+1)%2];
+
-      f_right = f[combin%2];
+      formula f_left = f_other[(combin + 1) % 2];
-      if (!(combin%2))
+      formula f_right = f_other[combin % 2];
+      if (!(combin % 2))
       {
         std::swap(left_ins, right_ins);
         std::swap(left_outs, right_outs);
       }
 
       auto trans = create_translator(gi);
-      trans.set_type(combin < 2 ? postprocessor::Buchi
+
-                                : postprocessor::CoBuchi);
       trans.set_pref(postprocessor::Deterministic | postprocessor::Complete);
+      if (combin < 2)
+        trans.set_type(postprocessor::Buchi);
+      else
+        trans.set_type(postprocessor::CoBuchi);
 
       stopwatch sw;
       if (bv)
         sw.start();
       auto res = trans.run(f_left);
 
+      if (!is_deterministic(res))
+        return ret_sol_maybe();
+
       if (bv)
       {
         auto delta = sw.stop();
@@ -1312,78 +1378,75 @@ namespace spot
         if (vs)
           *vs << "tanslating formula done in " << delta << " seconds\n";
       }
-
-      if (!is_deterministic(res))
-        return ret_sol_maybe();
-      for (auto& out : right_outs)
-          res->register_ap(out.ap_name());
-
-      // The BDD that describes the content of the G in a conjunction
-      bdd g_bdd = bddtrue;
-
-      // Convert the set of outputs to a BDD
-      bdd output_bdd = bddtrue;
-      for (auto &out : output_aps_set)
-        output_bdd &= bdd_ithvar(res->register_ap(out));
-
-      if (!f_g.is_tt())
-      {
-        g_bdd = formula_to_bdd(f_g[0], res->get_dict(), res);
-        // If the content of G is not input-complete, a simple strategy for
-        // env is to play this missing value.
-        if (bdd_exist(g_bdd, output_bdd) != bddtrue)
-        {
-          return ret_sol_none();
-        }
-      }
-
-      // For the GF(outs) (resp. GF(outs)), the content and its negation can be
-      // converted to a BDD.
-      bdd right_bdd, neg_right_bdd;
-      if (combin < 2)
-      {
-        right_bdd = formula_to_bdd(f_right[0][0], res->get_dict(), res);
-        neg_right_bdd = bdd_not(right_bdd);
-      }
-      else
-      {
-        neg_right_bdd = formula_to_bdd(f_right[0][0], res->get_dict(), res);
-        right_bdd = bdd_not(neg_right_bdd);
-      }
-      // Monitor is a special case. As we color accepting transitions, if the
-      // acceptance is true, we cannot say that a transition is accepting if
-      // a color is seen.
-      const bool is_true = res->acc().is_t();
-      scc_info si(res, scc_info_options::NONE);
-      for (auto& e : res->edges())
-      {
-        // Here the part describing the outputs is based on the fact that
-        // they must be seen infinitely often. As these edges are seen
-        // finitely often, we can let the minimization choose the value.
-        if (si.scc_of(e.src) == si.scc_of(e.dst))
-          {
-            if (e.acc || is_true)
-              e.cond &= right_bdd;
-            else
-              e.cond &= neg_right_bdd;
-          }
-        // g_bdd has to be true all the time. So we cannot only do it
-        // between SCCs.
-        e.cond &= g_bdd;
-        if (e.cond == bddfalse)
-          return ret_sol_maybe();
-        // The recurrence is Büchi but the strategy is a monitor. We need
-        // to remove the color.
-        e.acc = {};
-      }
-
-      set_synthesis_outputs(res, output_bdd);
-      res->set_acceptance(acc_cond::acc_code::t());
-
       res->prop_complete(trival::maybe());
+
+      bdd output_bdd = bddtrue;
+      auto [is, os] = form2props.aps_of(f);
+      for (auto i : is)
+        res->register_ap(i);
+      for (auto o : os)
+        output_bdd &= bdd_ithvar(res->register_ap(o));
+
+      bdd right_bdd = formula_to_bdd(f_right[0][0], dict, res);
+      bdd neg_right_bdd = bdd_not(right_bdd);
+      bdd g_bdd = formula_to_bdd(f_g, dict, res);
+
+      if (combin > 1)
+        std::swap(right_bdd, neg_right_bdd);
+
+      right_bdd = bdd_and(right_bdd, g_bdd);
+      neg_right_bdd = bdd_and(neg_right_bdd, g_bdd);
+
+      scc_info si(res, scc_info_options::NONE);
+
+      bool is_true_acc = ((combin < 2) && res->acc().is_t())
+                || ((combin > 1) && res->acc().is_f());
+      auto prop_vector = propagate_marks_vector(res);
+      auto& ev = res->edge_vector();
+      for (unsigned i = 1; i < ev.size(); ++i)
+      {
+        auto &edge = ev[i];
+        if (si.scc_of(edge.src) == si.scc_of(edge.dst))
+        {
+          if (edge.acc || is_true_acc)
+            edge.cond &= right_bdd;
+          // If we have a GF and an edge is not colored but prop_vector says
+          // that this edge could be colored, it means that we can do what we
+          // want
+          else if (!prop_vector[i])
+            edge.cond &= neg_right_bdd;
+          else
+            edge.cond &= g_bdd;
+        }
+        else
+          edge.cond &= g_bdd;
+        edge.acc = {};
+      }
+      res->set_acceptance(acc_cond::acc_code::t());
+      res->set_named_prop<bdd>("synthesis-outputs", new bdd(output_bdd));
+
+      return ret_sol_exists(res);
+    }
+    else if (f_other.is_tt())
+    {
+      if (!want_strategy)
+        return ret_sol_exists(nullptr);
+      auto res = make_twa_graph(dict);
+
+      bdd output_bdd = bddtrue;
+      auto [ins_f, _] = form2props.aps_of(f_g);
+      for (auto &out : output_aps)
+        output_bdd &= bdd_ithvar(res->register_ap(out));
+
+      for (auto &in : ins_f)
+        res->register_ap(in);
+
+      res->set_named_prop<bdd>("synthesis-outputs", new bdd(output_bdd));
+      bdd g_bdd = formula_to_bdd(f_g, dict, res);
+      res->new_state();
+      res->new_edge(0, 0, g_bdd);
       return ret_sol_exists(res);
     }
-    else
     return ret_sol_maybe();
   }
 

spot/twaalgos/synthesis.hh

@@ -241,10 +241,12 @@ namespace spot
   /// \param f The formula to synthesize a strategy for
   /// \param output_aps A vector with the name of all output properties.
   ///                   All APs not named in this vector are treated as inputs
+  /// \param want_strategy Set to false if we don't want to construct the
+  /// strategy but only test realizability.
   SPOT_API mealy_like
   try_create_direct_strategy(formula f,
                              const std::vector<std::string>& output_aps,
-                             synthesis_info& gi);
+                             synthesis_info& gi, bool want_strategy = false);
 
   /// \ingroup synthesis
   /// \brief Solve a game, and update synthesis_info

tests/core/ltlsynt.test

@@ -193,9 +193,7 @@ diff out exp
 
 cat >exp <<EOF
 trying to create strategy directly for GFa <-> GFb
-tanslating formula done in X seconds
 direct strategy was found.
-direct strat has 1 states, 2 edges and 0 colors
 EOF
 ltlsynt --ins='a' --outs='b' -f 'GFa <-> GFb' --verbose --realizability 2> out
 sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
@@ -214,9 +212,7 @@ diff outx exp
 
 cat >exp <<EOF
 trying to create strategy directly for (Fa & Fb & Fc & Fd) <-> GFe
-tanslating formula done in X seconds
 direct strategy was found.
-direct strat has 16 states, 81 edges and 0 colors
 EOF
 ltlsynt --ins='a,b,c,d' --outs='e' -f '(Fa & Fb & Fc & Fd) <-> GFe' \
         --verbose --realizability --algo=lar 2> out
@@ -526,15 +522,14 @@ REALIZABLE
 HOA: v1
 States: 1
 Start: 0
-AP: 3 "a" "b" "c"
+AP: 3 "c" "a" "b"
 acc-name: all
 Acceptance: 0 t
 properties: trans-labels explicit-labels state-acc deterministic
-controllable-AP: 2
+controllable-AP: 0
 --BODY--
 State: 0
-[!0&!2 | !1&!2] 0
+[!0&!1 | !0&!2 | 0&1&2] 0
-[0&1&2] 0
 --END--
 EOF
 ltlsynt --ins=a,b -f 'G (a & b <=> c)' >stdout
@@ -563,15 +558,8 @@ direct strategy was found.
 direct strat has 1 states, 2 edges and 0 colors
 simplification took X seconds
 trying to create strategy directly for Gc
-direct strategy might exist but was not found.
+direct strategy was found.
-translating formula done in X seconds
+direct strat has 1 states, 1 edges and 0 colors
-automaton has 1 states and 1 colors
-LAR 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 2> out
@@ -599,7 +587,6 @@ done
 # # impossible to find a strategy.
 cat >exp <<EOF
 trying to create strategy directly for (GFb <-> GFa) & G(a & c)
-tanslating formula done in X seconds
 no strategy exists.
 EOF
 ltlsynt -f '(GFb <-> GFa) && G(a&c)' --outs=b,c --verbose\
@@ -687,26 +674,12 @@ diff outx exp
 # Here, G!(!x | !y) should be Gx & Gy
 cat >exp <<EOF
 trying to create strategy directly for Gx
-direct strategy might exist but was not found.
+direct strategy was found.
-translating formula done in X seconds
+direct strat has 1 states, 1 edges and 0 colors
-automaton has 1 states and 1 colors
-LAR 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
 trying to create strategy directly for Gy
-direct strategy might exist but was not found.
+direct strategy was found.
-translating formula done in X seconds
+direct strat has 1 states, 1 edges and 0 colors
-automaton has 1 states and 1 colors
-LAR 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
 AIG circuit was created in X seconds and has 0 latches and 0 gates
 EOF
@@ -717,15 +690,7 @@ diff outx exp
 # Here, !F(a | b) should be G(!a) & G(!b)
 cat >exp <<EOF
 trying to create strategy directly for G!a
-direct strategy might exist but was not found.
+no strategy exists.
-translating formula done in X seconds
-automaton has 1 states and 1 colors
-LAR construction done in X seconds
-DPA has 1 states, 0 colors
-split inputs and outputs done in X seconds
-automaton has 4 states
-solving game with acceptance: parity max odd 3
-game solved in X seconds
 EOF
 ltlsynt -f '!F(a|b)' --outs=b --decompose=yes --aiger --verbose 2> out || true
 sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
@@ -734,15 +699,7 @@ diff outx exp
 # Here, G!(a -> b) should be G(a) & G(!b)
 cat >exp <<EOF
 trying to create strategy directly for Ga
-direct strategy might exist but was not found.
+no strategy exists.
-translating formula done in X seconds
-automaton has 1 states and 1 colors
-LAR construction done in X seconds
-DPA has 1 states, 0 colors
-split inputs and outputs done in X seconds
-automaton has 4 states
-solving game with acceptance: parity max odd 3
-game solved in X seconds
 EOF
 ltlsynt -f 'G!(a -> b)' --outs=b --decompose=yes --aiger\
                         --verbose 2> out || true
@@ -815,15 +772,7 @@ diff outx exp
 # Here, !(F(a | b)) should be G!a & G!b
 cat >exp <<EOF
 trying to create strategy directly for G!a
-direct strategy might exist but was not found.
+no strategy exists.
-translating formula done in X seconds
-automaton has 1 states and 1 colors
-LAR construction done in X seconds
-DPA has 1 states, 0 colors
-split inputs and outputs done in X seconds
-automaton has 4 states
-solving game with acceptance: parity max odd 3
-game solved in X seconds
 EOF
 ltlsynt -f '!(F(a | b))' --outs=b, --decompose=yes \
                          --verbose --aiger 2> out || true