twaalgos: add a match_states variant with a formula argument

This is related to issue #591, reported by Blake C. Rawlings.

* spot/twaalgos/ltl2tgba_fm.cc, spot/twaalgos/ltl2tgba_fm.hh
(ltl_to_tgba_fm): Add option to keep LTL labels.
* spot/twaalgos/matchstates.cc, spot/twaalgos/matchstates.hh
(match_states): Add variant with a formula as second argument.
* tests/python/matchstates.py: Test it.
* NEWS: Mention it.
* THANKS: Add reporter.

NEWS

@@ -62,6 +62,12 @@ New in spot 2.12.0.dev (not yet released)
      and B accept the same language, any word accepted by A from state
      x can be accepted in B from some state in V[x].
 
+     That function also has a variant spot::match_states(A, f) where f
+     is an LTL formula.  In this case it returns and array of
+     formulas.  If f represents a superset of the language of A, then
+     any word accepted by A from state x satisfies V[x].  Related to
+     Issue #591.
+
   Bug fixes:
 
   - Generating random formulas without any unary opertor would very

THANKS

@@ -5,6 +5,7 @@ Andreas Tollkötter
 Andrew Wells
 Anton Pirogov
 Ayrat Khalimov
+Blake C. Rawlings
 Cambridge Yang
 Caroline Lemieux
 Christian Dax

spot/twaalgos/ltl2tgba_fm.cc

@@ -1887,7 +1887,7 @@ namespace spot
                  bool exprop, bool symb_merge, bool branching_postponement,
                  bool fair_loop_approx, const atomic_prop_set* unobs,
                  tl_simplifier* simplifier, bool unambiguous,
-                 const output_aborter* aborter)
+                 const output_aborter* aborter, bool label_with_ltl)
   {
     tl_simplifier* s = simplifier;
 
@@ -2216,8 +2216,9 @@ namespace spot
         if (orig_f.is_syntactic_guarantee())
           a->prop_terminal(true);
       }
-    // Set the following to true to preserve state names.
+
-    a->release_formula_namer(namer, false);
+    // This gives each state a name of label_with_ltl is set.
+    a->release_formula_namer(namer, label_with_ltl);
 
     if (!simplifier)
       // This should not be deleted before we have registered all propositions.

spot/twaalgos/ltl2tgba_fm.hh

@@ -74,6 +74,10 @@ namespace spot
   /// constructed automaton would become larger than specified by the
   /// output_aborter.
   ///
+  /// \param label_with_ltl keep one LTL formula equivalent the
+  /// language recognized by each state, and use that to name each
+  /// state.
+  ///
   /// \return A spot::twa_graph that recognizes the language of \a f.
   SPOT_API twa_graph_ptr
   ltl_to_tgba_fm(formula f, const bdd_dict_ptr& dict,
@@ -83,5 +87,6 @@ namespace spot
                  const atomic_prop_set* unobs = nullptr,
                  tl_simplifier* simplifier = nullptr,
                  bool unambiguous = false,
-                 const output_aborter* aborter = nullptr);
+                 const output_aborter* aborter = nullptr,
+                 bool label_with_ltl = false);
 }

spot/twaalgos/matchstates.cc

@@ -20,6 +20,8 @@
 #include <spot/twaalgos/matchstates.hh>
 #include <spot/twaalgos/sccinfo.hh>
 #include <spot/twaalgos/product.hh>
+#include <spot/twaalgos/ltl2tgba_fm.hh>
+#include <spot/tl/parse.hh>
 
 namespace spot
 {
@@ -45,6 +47,43 @@ namespace spot
     return v;
   }
 
+  std::vector<formula>
+  match_states(const const_twa_graph_ptr& aut1, formula f)
+  {
+    twa_graph_ptr aut2 = ltl_to_tgba_fm(f, aut1->get_dict(),
+                                        false /* exprop */,
+                                        true /* symbolic merge */,
+                                        false /* branching postponement */,
+                                        false /* fair loop approx. */,
+                                        nullptr /* unobs event */,
+                                        nullptr /* simplifier */,
+                                        false /* unambiguous */,
+                                        nullptr /* aborter */,
+                                        true /* label with LTL */);
+    auto state_names =
+      aut2->get_named_prop<std::vector<std::string>>("state-names");
+    auto v = match_states(aut1, aut2);
+    unsigned sz1 = aut1->num_states();
+    unsigned sz2 = aut2->num_states();
 
+    // State are labeled with strings, but we know those strings to
+    // represent LTL formulas, so convert those.
+    std::vector<formula> state_formulas;
+    state_formulas.reserve(sz2);
+    for (unsigned i = 0; i < sz2; ++i)
+      state_formulas.push_back(parse_formula((*state_names)[i]));
 
+    std::vector<formula> res;
+    res.reserve(sz1);
+
+    std::vector<formula> disjuncts;
+    for (unsigned i = 0; i < sz1; ++i)
+      {
+        disjuncts.clear();
+        for (unsigned j: v[i])
+          disjuncts.push_back(state_formulas[j]);
+        res.push_back(formula::Or(disjuncts));
+      }
+    return res;
+  }
 }

spot/twaalgos/matchstates.hh

@@ -20,6 +20,7 @@
 
 #include <spot/misc/common.hh>
 #include <spot/twa/fwd.hh>
+#include <spot/tl/formula.hh>
 #include <vector>
 
 namespace spot
@@ -37,4 +38,21 @@ namespace spot
   SPOT_API std::vector<std::vector<unsigned>>
   match_states(const const_twa_graph_ptr& aut1,
                const const_twa_graph_ptr& aut2);
+
+  /// \ingroup twa_algorithms \brief match the states of \a aut with
+  /// formulas "reachable" from \a f.
+  ///
+  /// The returned vector V assigns each state `x` of \a aut to a
+  /// formula `V[x]`.
+  ///
+  /// This translates \a f as an automaton B in which states are labeled
+  /// by formulas, match the states of \a aut with the states of B, and
+  /// use that to find formulas associated to each state of \a aut.
+  ///
+  /// In particular, if the language of \a f is a superset of the
+  /// language of \a aut, then every word accepted in \a aut from
+  /// state `x` will satisfy formula `V[x]`.  However `V[x]` may
+  /// accept more than the words accepted from `a` in \a aut.
+  SPOT_API std::vector<formula>
+  match_states(const const_twa_graph_ptr& aut, formula f);
 }

tests/python/matchstates.py

@@ -60,3 +60,18 @@ m3 = spot.match_states(a, c)
 tc.assertEqual(m3, ((), (), (), ()))
 m4 = spot.match_states(c, a)
 tc.assertEqual(m4, ((), ))
+
+f = spot.formula("Ga | Gb | Gc")
+m5 = spot.match_states(a, f)
+tc.assertEqual(m5, (f, f, f, f))
+m6 = spot.match_states(b, f)
+tc.assertEqual(m6, (spot.formula("Gc"),
+                    spot.formula("Gb | Gc"),
+                    spot.formula("Gb"),
+                    spot.formula("Ga"),
+                    spot.formula("Ga | Gc"),
+                    spot.formula("Ga | Gb"),
+                    spot.formula("Ga | Gb | Gc")))
+
+m7 = spot.match_states(c, f)  # Note that f is not the formula for c
+tc.assertEqual(m7, (spot.formula("0"),))