From 582d455c23b44d68a47c10ab7513ec62b9967cfd Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 1 Dec 2016 18:27:54 +0100 Subject: [PATCH] twa: add support for very-weak property * spot/twa/twa.hh: Implement the property. * spot/parseaut/parseaut.yy, spot/twaalgos/hoa.cc: Add input and output for it. * spot/twaalgos/strength.cc, spot/twaalgos/strength.hh (is_very_weak_automaton): New function. * tests/core/alternating.test: Add a test for --check=strength on an alternating automaton. * tests/core/strength.test, tests/core/parseaut.test: Adjust expected output. * NEWS, doc/org/hoa.org, doc/org/concepts.org: Document it. --- NEWS | 4 ++++ doc/org/concepts.org | 1 + doc/org/hoa.org | 45 +++++++++++++++++++------------------ spot/parseaut/parseaut.yy | 19 ++++++++++++++++ spot/twa/twa.hh | 37 +++++++++++++++++++++++++++--- spot/twaalgos/hoa.cc | 8 ++++++- spot/twaalgos/strength.cc | 28 ++++++++++++++++++++--- spot/twaalgos/strength.hh | 21 ++++++++++++++++- tests/core/alternating.test | 7 ++++++ tests/core/parseaut.test | 3 +++ tests/core/strength.test | 6 ++--- 11 files changed, 146 insertions(+), 33 deletions(-) diff --git a/NEWS b/NEWS index d362c6688..0f56837bc 100644 --- a/NEWS +++ b/NEWS @@ -14,6 +14,10 @@ New in spot 2.2.2.dev (Not yet released) * The new version of the Couvreur emptiness check is now the default one, used by is_empty() and accepting_run(). + * twa objects have a new property, very-weak, that can be set or + retrieved via twa::prop_very_weak(), and that can be tested by + is_very_weak_automaton(). + Build: * The configure script has a new option --enable-c++14, to compile in diff --git a/doc/org/concepts.org b/doc/org/concepts.org index 54ad43fe1..fb2cd24e1 100644 --- a/doc/org/concepts.org +++ b/doc/org/concepts.org @@ -995,6 +995,7 @@ automaton, and that can be queried or set by algorithms: | =state_acc= | automaton should be considered has having state-based acceptance | | =inherently_weak= | accepting and rejecting cycles cannot be mixed in the same SCC | | =weak= | transitions of an SCC all belong to the same acceptance sets | +| =very-weak= | weak automaton where all SCCs have size 1 | | =terminal= | automaton is weak, accepting SCCs are complete, accepting edges may not go to rejecting SCCs | | =deterministic= | there is at most one run *recognizing* a word, but not necessarily accepting it | | =unambiguous= | there is at most one run *accepting* a word (but it might be recognized several time) | diff --git a/doc/org/hoa.org b/doc/org/hoa.org index 48dd67d21..3ba4941d5 100644 --- a/doc/org/hoa.org +++ b/doc/org/hoa.org @@ -603,10 +603,10 @@ body of the file, and then return and error if what has been declared does not correspond to the reality. Some supported properties (like =weak=, =inherently-weak=, -=unambiguous=, or =stutter-invariant=) are not double-checked, because -that would require more operations. Command-line tools that -read HOA files all take a =--trust-hoa=no= option to ignore properties -that are not double-checked by the parser. +=very-weak=, =terminal=, =unambiguous=, or =stutter-invariant=) are +not double-checked, because that would require more operations. +Command-line tools that read HOA files all take a =--trust-hoa=no= +option to ignore properties that are not double-checked by the parser. It should be noted that each property can take three values: true, false, or maybe. So actually two bits are used per property. For @@ -652,24 +652,25 @@ particular: to detect deterministic automata that have been output by algorithms that do not try to output deterministic automata. -| property | parser | stored | printer | notes | -|---------------------+---------+--------+---------------------------------------------+------------------------------------------------------------------| -| =state-labels= | checked | no | checked if =-Hk= | state labels are converted to transition labels when reading TωA | -| =trans-labels= | checked | no | always, unless =-Hi= or =-Hk= | | -| =implicit-labels= | checked | no | if =-Hi= | =-Hi= only works for deterministic automata | -| =explicit-labels= | checked | no | always, unless =-Hi= | | -| =state-acc= | checked | yes | checked, unless =-Ht= or =-Hm= | | -| =trans-acc= | checked | no | if not =state-acc= and not =-Hm= | | -| =no-univ-branch= | ignored | no | only if =-Hv= | | -| =deterministic= | checked | yes | checked | | -| =complete= | checked | no | checked | | -| =unambiguous= | trusted | yes | as stored if (=-Hv= or not =deterministic=) | can be checked with =--check=unambiguous= | -| =stutter-invariant= | trusted | yes | as stored | can be checked with =--check=stuttering= | -| =stutter-sensitive= | trusted | yes | as stored (opposite of =stutter-invariant=) | can be checked with =--check=stuttering= | -| =terminal= | trusted | yes | as stored | can be checked with =--check=strength= | -| =weak= | trusted | yes | as stored if (=-Hv= or not =terminal=) | can be checked with =--check=strength= | -| =inherently-weak= | trusted | yes | as stored if (=-Hv= or not =weak=) | can be checked with =--check=strength= | -| =colored= | ignored | no | checked | | +| property | parser | stored | printer | notes | +|---------------------+---------+--------+---------------------------------------------------------+------------------------------------------------------------------| +| =state-labels= | checked | no | checked if =-Hk= | state labels are converted to transition labels when reading TωA | +| =trans-labels= | checked | no | always, unless =-Hi= or =-Hk= | | +| =implicit-labels= | checked | no | if =-Hi= | =-Hi= only works for deterministic automata | +| =explicit-labels= | checked | no | always, unless =-Hi= | | +| =state-acc= | checked | yes | checked, unless =-Ht= or =-Hm= | | +| =trans-acc= | checked | no | if not =state-acc= and not =-Hm= | | +| =no-univ-branch= | ignored | no | only if =-Hv= | | +| =deterministic= | checked | yes | checked | | +| =complete= | checked | no | checked | | +| =unambiguous= | trusted | yes | as stored if (=-Hv= or not =deterministic=) | can be checked with =--check=unambiguous= | +| =stutter-invariant= | trusted | yes | as stored | can be checked with =--check=stuttering= | +| =stutter-sensitive= | trusted | yes | as stored (opposite of =stutter-invariant=) | can be checked with =--check=stuttering= | +| =terminal= | trusted | yes | as stored | can be checked with =--check=strength= | +| =very-weak= | trusted | yes | as stored if (=-Hv= or not =terminal=) | can be checked with =--check=strength= | +| =weak= | trusted | yes | as stored if (=-Hv= or not (=terminal= or =very-weak=)) | can be checked with =--check=strength= | +| =inherently-weak= | trusted | yes | as stored if (=-Hv= or not =weak=) | can be checked with =--check=strength= | +| =colored= | ignored | no | checked | | The above table is for version 1 of the format. When version 1.1 is selected (using =-H1.1=), some negated properties may be output. In diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index 71581ea07..0ec23f95d 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -526,8 +526,27 @@ header: format-version header-items a->prop_stutter_invariant(!ss->second.val); } auto iw = p.find("inherently-weak"); + auto vw = p.find("very-weak"); auto w = p.find("weak"); auto t = p.find("terminal"); + if (vw != e) + { + a->prop_very_weak(vw->second.val); + if (w != e && !w->second.val && vw->second.val) + { + error(w->second.loc, + "'properties: !weak' contradicts..."); + error(vw->second.loc, + "... 'properties: very-weak' given here"); + } + if (iw != e && !iw->second.val && vw->second.val) + { + error(iw->second.loc, + "'properties: !inherently-weak' contradicts..."); + error(vw->second.loc, + "... 'properties: very-weak' given here"); + } + } if (iw != e) { a->prop_inherently_weak(iw->second.val); diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index e6c7a4889..2dc564713 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -990,6 +990,7 @@ namespace spot trival::repr_t deterministic:2; // Deterministic automaton. trival::repr_t unambiguous:2; // Unambiguous automaton. trival::repr_t stutter_invariant:2; // Stutter invariant language. + trival::repr_t very_weak:2; // very-weak, or 1-weak }; union { @@ -1167,7 +1168,7 @@ namespace spot /// \brief Set the "inherently weak" proeprty. /// /// Setting "inherently weak" to false automatically - /// disables "terminal" and "weak". + /// disables "terminal", "very weak", and "weak". /// /// \see prop_weak() /// \see prop_terminal() @@ -1175,7 +1176,7 @@ namespace spot { is.inherently_weak = val.val(); if (!val) - is.terminal = is.weak = val.val(); + is.very_weak = is.terminal = is.weak = val.val(); } /// \brief Whether the automaton is terminal. @@ -1234,9 +1235,38 @@ namespace spot if (val) is.inherently_weak = val.val(); if (!val) - is.terminal = val.val(); + is.very_weak = is.terminal = val.val(); } + /// \brief Whether the automaton is very-weak. + /// + /// An automaton is very-weak if it is weak (inside each strongly connected + /// component, all transitions belong to the same acceptance sets) + /// and each SCC contains only one state. + /// + /// \see prop_terminal() + /// \see prop_weak() + trival prop_very_weak() const + { + return is.very_weak; + } + + /// \brief Set the very-weak property. + /// + /// Marking an automaton as "very-weak" automatically marks it as + /// "weak" and "inherently weak". + /// + /// \see prop_terminal() + /// \see prop_weak() + void prop_very_weak(trival val) + { + is.very_weak = val.val(); + if (val) + is.weak = is.inherently_weak = val.val(); + } + + + /// \brief Whether the automaton is deterministic. /// /// An automaton is deterministic if the conjunction between the @@ -1400,6 +1430,7 @@ namespace spot { prop_terminal(other->prop_terminal()); prop_weak(other->prop_weak()); + prop_very_weak(other->prop_very_weak()); prop_inherently_weak(other->prop_inherently_weak()); } if (p.deterministic) diff --git a/spot/twaalgos/hoa.cc b/spot/twaalgos/hoa.cc index 49f984e17..39cd473e5 100644 --- a/spot/twaalgos/hoa.cc +++ b/spot/twaalgos/hoa.cc @@ -500,12 +500,18 @@ namespace spot } if (aut->prop_terminal()) prop(" terminal"); - if (aut->prop_weak() && (verbose || aut->prop_terminal() != true)) + if (aut->prop_very_weak() && (verbose || aut->prop_terminal() != true)) + prop(" very-weak"); + if (aut->prop_weak() && (verbose || (aut->prop_terminal() != true && + aut->prop_very_weak() != true))) prop(" weak"); if (aut->prop_inherently_weak() && (verbose || aut->prop_weak() != true)) prop(" inherently-weak"); if (v1_1 && !aut->prop_terminal() && (verbose || aut->prop_weak() != false)) prop(" !terminal"); + if (v1_1 && !aut->prop_very_weak() && (verbose + || aut->prop_weak() != false)) + prop(" !very-weak"); if (v1_1 && !aut->prop_weak() && (verbose || aut->prop_inherently_weak() != false)) prop(" !weak"); diff --git a/spot/twaalgos/strength.cc b/spot/twaalgos/strength.cc index b547a0ac6..fcce611db 100644 --- a/spot/twaalgos/strength.cc +++ b/spot/twaalgos/strength.cc @@ -34,22 +34,29 @@ namespace spot bool need_si = !si; if (need_si) si = new scc_info(aut); - si->determine_unknown_acceptance(); + if (inweak) + si->determine_unknown_acceptance(); bool is_inweak = true; bool is_weak = true; + bool is_single_state_scc = true; bool is_term = true; unsigned n = si->scc_count(); for (unsigned i = 0; i < n; ++i) { if (si->is_trivial(i)) continue; + if (si->states_of(i).size() > 1) + is_single_state_scc = false; bool first = true; acc_cond::mark_t m = 0U; if (is_weak) for (auto src: si->states_of(i)) for (auto& t: aut->out(src)) - if (si->scc_of(t.dst) == i) + // In case of a universal edge we only need to check + // the first destination of an inside the SCC, because + // the other have the same t.acc. + if (si->scc_of(*aut->univ_dests(t.dst).begin()) == i) { if (first) { @@ -98,6 +105,7 @@ namespace spot if (terminal) aut->prop_terminal(is_term && is_weak); aut->prop_weak(is_weak); + aut->prop_very_weak(is_single_state_scc && is_weak); if (inweak) aut->prop_inherently_weak(is_inweak); } @@ -131,6 +139,17 @@ namespace spot return res; } + bool + is_very_weak_automaton(const const_twa_graph_ptr& aut, scc_info* si) + { + trival v = aut->prop_very_weak(); + if (v.is_known()) + return v.is_true(); + is_type_automaton + (std::const_pointer_cast(aut), si); + return aut->prop_very_weak().is_true(); + } + bool is_inherently_weak_automaton(const const_twa_graph_ptr& aut, scc_info* si) { @@ -145,7 +164,10 @@ namespace spot void check_strength(const twa_graph_ptr& aut, scc_info* si) { - is_type_automaton(aut, si); + if (aut->is_alternating()) + is_type_automaton(aut, si); + else + is_type_automaton(aut, si); } bool is_safety_mwdba(const const_twa_graph_ptr& aut) diff --git a/spot/twaalgos/strength.hh b/spot/twaalgos/strength.hh index b0ef98900..66cea4db2 100644 --- a/spot/twaalgos/strength.hh +++ b/spot/twaalgos/strength.hh @@ -60,6 +60,24 @@ namespace spot SPOT_API bool is_weak_automaton(const const_twa_graph_ptr& aut, scc_info* sm = nullptr); + /// \brief Check whether an automaton is very-weak. + /// + /// An automaton is very-weak if in any given SCC, all transitions + /// belong to the same acceptance sets, and the SCC has only one + /// state. + /// + /// \param aut the automaton to check + /// + /// \param sm an scc_info object for the automaton if available (it + /// will be built otherwise). + /// + /// In addition to returning the result as a Boolean, this will set + /// the prop_very_weak() and prop_weak() properties of the automaton + /// as a side-effect, so further calls will return in constant-time. + SPOT_API bool + is_very_weak_automaton(const const_twa_graph_ptr& aut, + scc_info* sm = nullptr); + /// \brief Check whether an automaton is inherently weak. /// /// An automaton is inherently weak if in any given SCC, there @@ -90,7 +108,8 @@ namespace spot /// \brief Check whether an automaton is weak or terminal. /// - /// This sets the "weak" and "terminal" property as appropriate. + /// This sets the "inherently weak", "weak", "very-weak" and + /// "terminal" properties as appropriate. /// /// \param aut the automaton to check /// diff --git a/tests/core/alternating.test b/tests/core/alternating.test index 49eedb9b9..a09c8f0d2 100644 --- a/tests/core/alternating.test +++ b/tests/core/alternating.test @@ -126,3 +126,10 @@ digraph G { EOF diff expect.dot alt.dot + +autfilt --trust=no --check=strength alt.hoa | grep properties: >output +cat >expected <