diff --git a/NEWS b/NEWS index 4a79a551c..2833b5cd8 100644 --- a/NEWS +++ b/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 diff --git a/THANKS b/THANKS index 307d34999..fcae660e7 100644 --- a/THANKS +++ b/THANKS @@ -5,6 +5,7 @@ Andreas Tollkötter Andrew Wells Anton Pirogov Ayrat Khalimov +Blake C. Rawlings Cambridge Yang Caroline Lemieux Christian Dax diff --git a/spot/twaalgos/ltl2tgba_fm.cc b/spot/twaalgos/ltl2tgba_fm.cc index acf9511b2..09e88acae 100644 --- a/spot/twaalgos/ltl2tgba_fm.cc +++ b/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. diff --git a/spot/twaalgos/ltl2tgba_fm.hh b/spot/twaalgos/ltl2tgba_fm.hh index ac7c5645e..717ae6b1b 100644 --- a/spot/twaalgos/ltl2tgba_fm.hh +++ b/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); } diff --git a/spot/twaalgos/matchstates.cc b/spot/twaalgos/matchstates.cc index 14edfe18b..0d9595501 100644 --- a/spot/twaalgos/matchstates.cc +++ b/spot/twaalgos/matchstates.cc @@ -20,6 +20,8 @@ #include #include #include +#include +#include namespace spot { @@ -45,6 +47,43 @@ namespace spot return v; } + std::vector + 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>("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 state_formulas; + state_formulas.reserve(sz2); + for (unsigned i = 0; i < sz2; ++i) + state_formulas.push_back(parse_formula((*state_names)[i])); + std::vector res; + res.reserve(sz1); + + std::vector 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; + } } diff --git a/spot/twaalgos/matchstates.hh b/spot/twaalgos/matchstates.hh index 7bd972402..3c9bb6236 100644 --- a/spot/twaalgos/matchstates.hh +++ b/spot/twaalgos/matchstates.hh @@ -20,6 +20,7 @@ #include #include +#include #include namespace spot @@ -37,4 +38,21 @@ namespace spot SPOT_API std::vector> 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 + match_states(const const_twa_graph_ptr& aut, formula f); } diff --git a/tests/python/matchstates.py b/tests/python/matchstates.py index 050a84b84..f5d8102be 100644 --- a/tests/python/matchstates.py +++ b/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"),))