From 4b01387817e53c64af37212905c98d7120df44e5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 29 Dec 2016 16:37:43 +0100 Subject: [PATCH] support for semi-deterministic property * spot/twa/twa.hh (prop_semi_deterministic): New methods. * spot/parseaut/parseaut.yy, spot/twaalgos/hoa.cc: Add support for the semi-deterministic property. * doc/org/concepts.org, doc/org/hoa.org: Document it. * spot/twaalgos/isdet.cc, spot/twaalgos/isdet.hh (is_semi_deterministic): New function. * bin/autfilt.cc: Add --is-semi-deterministic. * bin/common_aoutput.cc: Add --check=semi-deterministic. * tests/core/semidet.test: New file. * tests/Makefile.am: Add it. * tests/core/parseaut.test, tests/core/readsave.test: Adjust. --- NEWS | 12 ++++-- bin/autfilt.cc | 20 ++++++++-- bin/common_aoutput.cc | 6 +++ doc/org/concepts.org | 22 +++++------ doc/org/hoa.org | 50 ++++++++++++------------ spot/parseaut/parseaut.yy | 13 +++++++ spot/twa/twa.hh | 43 +++++++++++++++++++-- spot/twaalgos/hoa.cc | 4 ++ spot/twaalgos/isdet.cc | 47 ++++++++++++++++++++++- spot/twaalgos/isdet.hh | 9 +++++ tests/Makefile.am | 1 + tests/core/parseaut.test | 4 +- tests/core/readsave.test | 3 +- tests/core/semidet.test | 81 +++++++++++++++++++++++++++++++++++++++ 14 files changed, 265 insertions(+), 50 deletions(-) create mode 100755 tests/core/semidet.test diff --git a/NEWS b/NEWS index 776f39b8d..5112cc2cc 100644 --- a/NEWS +++ b/NEWS @@ -11,7 +11,10 @@ New in spot 2.2.2.dev (Not yet released) alternating automata, but in any case they should display a diagnostic: if you see a crash, please report it. - * autfilt has two new filters: --is-very-weak and --is-alternating. + * autfilt has three new filters: --is-very-weak, --is-alternating, + and --is-semi-deterministic. + + * the --check option can now take "semi-determinism" as argument. Library: @@ -60,9 +63,10 @@ New in spot 2.2.2.dev (Not yet released) https://www.lrde.epita.fr/tut24.html and https://www.lrde.epita.fr/tut31.html for some code examples. - * 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(). + * twa objects have two new properties, very-weak and + semi-deterministic, that can be set or retrieved via + twa::prop_very_weak()/twa::prop_semi_deterministic(), and that can + be tested by is_very_weak_automaton()/is_semi_deterministic(). Build: diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 42d75be6a..fa6e9a497 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -107,6 +107,7 @@ enum { OPT_IS_DETERMINISTIC, OPT_IS_EMPTY, OPT_IS_INHERENTLY_WEAK, + OPT_IS_SEMI_DETERMINISTIC, OPT_IS_STUTTER_INVARIANT, OPT_IS_TERMINAL, OPT_IS_UNAMBIGUOUS, @@ -169,6 +170,8 @@ static const argp_option options[] = "keep complete automata", 0 }, { "is-deterministic", OPT_IS_DETERMINISTIC, nullptr, 0, "keep deterministic automata", 0 }, + { "is-semi-deterministic", OPT_IS_SEMI_DETERMINISTIC, nullptr, 0, + "keep semi-deterministic automata", 0 }, { "is-empty", OPT_IS_EMPTY, nullptr, 0, "keep automata with an empty language", 0 }, { "is-stutter-invariant", OPT_IS_STUTTER_INVARIANT, nullptr, 0, @@ -415,6 +418,7 @@ static bool opt_merge = false; static bool opt_is_alternating = false; static bool opt_is_complete = false; static bool opt_is_deterministic = false; +static bool opt_is_semi_deterministic = false; static bool opt_is_unambiguous = false; static bool opt_is_terminal = false; static bool opt_is_weak = false; @@ -672,6 +676,9 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_IS_VERY_WEAK: opt_is_very_weak = true; break; + case OPT_IS_SEMI_DETERMINISTIC: + opt_is_semi_deterministic = true; + break; case OPT_IS_STUTTER_INVARIANT: opt_is_stutter_invariant = true; break; @@ -1072,9 +1079,16 @@ namespace if (opt_nondet_states_set) matched &= opt_nondet_states.contains(spot::count_nondet_states(aut)); if (opt_is_deterministic) - matched &= is_deterministic(aut); - else if (opt_is_unambiguous) - matched &= is_unambiguous(aut); + { + matched &= is_deterministic(aut); + } + else + { + if (opt_is_unambiguous) + matched &= is_unambiguous(aut); + if (opt_is_semi_deterministic) + matched &= is_semi_deterministic(aut); + } if (opt_is_terminal) matched &= is_terminal_automaton(aut); else if (opt_is_very_weak) diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index b8ebf84a1..534a8fbed 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -34,6 +34,7 @@ #include #include #include +#include automaton_format_t automaton_format = Hoa; static const char* automaton_format_opt = nullptr; @@ -45,6 +46,7 @@ enum check_type check_unambiguous = (1 << 0), check_stutter = (1 << 1), check_strength = (1 << 2), + check_semi_determinism = (1 << 3), check_all = -1U, }; static char const *const check_args[] = @@ -54,6 +56,7 @@ static char const *const check_args[] = "stutter-insensitive", "stuttering-insensitive", "stutter-sensitive", "stuttering-sensitive", "strength", "weak", "terminal", + "semi-determinism", "semi-deterministic", "all", nullptr }; @@ -64,6 +67,7 @@ static check_type const check_types[] = check_stutter, check_stutter, check_stutter, check_stutter, check_strength, check_strength, check_strength, + check_semi_determinism, check_semi_determinism, check_all }; ARGMATCH_VERIFY(check_args, check_types); @@ -527,6 +531,8 @@ automaton_printer::print(const spot::twa_graph_ptr& aut, spot::check_unambiguous(aut); if (opt_check & check_strength) spot::check_strength(aut); + if (opt_check & check_semi_determinism) + spot::is_semi_deterministic(aut); // sets the property as a side effect. } // Name the output automaton. diff --git a/doc/org/concepts.org b/doc/org/concepts.org index 2aaecf619..23410e5f7 100644 --- a/doc/org/concepts.org +++ b/doc/org/concepts.org @@ -554,7 +554,6 @@ $txt #+RESULTS: [[file:concept-twa1.png]] - * Alternating ω-automata Alternating ω-automata are ω-automata in which the destination of an @@ -1055,16 +1054,17 @@ better choices. There are actually several property flags that are stored into each automaton, and that can be queried or set by algorithms: -| flag name | meaning when =true= | -|---------------------+----------------------------------------------------------------------------------------------| -| =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) | -| =stutter_invariant= | the property recognized by the automaton is [[https://www.lrde.epita.fr/~adl/dl/adl/michaud.15.spin.pdf][stutter-invariant]] | +| flag name | meaning when =true= | +|----------------------+----------------------------------------------------------------------------------------------| +| =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 | +| =semi-deterministic= | any nondeterminism occurs before entering an accepting SCC | +| =unambiguous= | there is at most one run *accepting* a word (but it might be recognized several time) | +| =stutter_invariant= | the property recognized by the automaton is [[https://www.lrde.epita.fr/~adl/dl/adl/michaud.15.spin.pdf][stutter-invariant]] | For each flag =flagname=, the =twa= class has a method =prop_flagname()= that returns the value of the flag as an instance of diff --git a/doc/org/hoa.org b/doc/org/hoa.org index f691e443a..a00ad54e3 100644 --- a/doc/org/hoa.org +++ b/doc/org/hoa.org @@ -600,10 +600,11 @@ 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=, -=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. +=very-weak=, =terminal=, =unambiguous=, =semi-deterministic=, 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 @@ -649,26 +650,27 @@ 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= | | -| =univ-branch= | checked | no | checked | | -| =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 | | +| 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= | | +| =univ-branch= | checked | no | checked | | +| =deterministic= | checked | yes | checked | | +| =complete= | checked | no | checked | | +| =unambiguous= | trusted | yes | as stored if (=-Hv= or not =deterministic=) | can be checked with =--check=unambiguous= | +| =semi-deterministic= | trusted | yes | as stored if (=-Hv= or not =deterministic=) | can be checked with =--check=semi-deterministic= | +| =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 047ed40fc..af2eeb487 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -590,6 +590,19 @@ header: format-version header-items "... 'properties: !unambiguous' given here"); } } + auto sd = p.find("semi-deterministic"); + if (sd != e) + { + a->prop_semi_deterministic(sd->second.val); + auto d = p.find("deterministic"); + if (d != e && !sd->second.val && d->second.val) + { + error(d->second.loc, + "'properties: deterministic' contradicts..."); + error(sd->second.loc, + "... 'properties: !semi-deterministic' given here"); + } + } } } diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index 2dc564713..7e66f82f6 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -991,6 +991,7 @@ namespace spot 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 + trival::repr_t semi_deterministic:2; // semi-deterministic automaton. }; union { @@ -1285,16 +1286,17 @@ namespace spot /// \brief Set the deterministic property. /// - /// Setting the "deterministic" property automatically - /// sets the "unambiguous" property. + /// Setting the "deterministic" property automatically sets the + /// "unambiguous" and "semi-deterministic" properties. /// /// \see prop_unambiguous() + /// \see prop_semi_deterministic() void prop_deterministic(trival val) { is.deterministic = val.val(); if (val) - // deterministic implies unambiguous - is.unambiguous = val.val(); + // deterministic implies unambiguous and semi-deterministic + is.unambiguous = is.semi_deterministic = val.val(); } /// \brief Whether the automaton is unambiguous @@ -1328,6 +1330,36 @@ namespace spot is.deterministic = val.val(); } + /// \brief Whether the automaton is semi-deterministic + /// + /// An automaton is semi-deterministic if the sub-automaton + /// reachable from any accepting SCC is deterministic. + /// + /// Note that this method may return trival::maybe() when it is + /// unknown whether the automaton is semi-deterministic or not. + /// If you need a true/false answer, prefer the + /// is_semi_deterministic() function. + /// + /// \see prop_deterministic() + /// \see is_semi_deterministic() + trival prop_semi_deterministic() const + { + return is.semi_deterministic; + } + + /// \brief Sets the semi-deterministic property + /// + /// Marking an automaton as "non semi-deterministic" automatically + /// marks it as "non deterministic". + /// + /// \see prop_deterministic() + void prop_semi_deterministic(trival val) + { + is.semi_deterministic = val.val(); + if (!val) + is.deterministic = val.val(); + } + /// \brief Whether the automaton is stutter-invariant. /// /// An automaton is stutter-invariant iff any accepted word @@ -1436,6 +1468,7 @@ namespace spot if (p.deterministic) { prop_deterministic(other->prop_deterministic()); + prop_semi_deterministic(other->prop_semi_deterministic()); prop_unambiguous(other->prop_unambiguous()); } if (p.stutter_inv) @@ -1455,11 +1488,13 @@ namespace spot { prop_terminal(trival::maybe()); prop_weak(trival::maybe()); + prop_very_weak(trival::maybe()); prop_inherently_weak(trival::maybe()); } if (!p.deterministic) { prop_deterministic(trival::maybe()); + prop_semi_deterministic(trival::maybe()); prop_unambiguous(trival::maybe()); } if (!p.stutter_inv) diff --git a/spot/twaalgos/hoa.cc b/spot/twaalgos/hoa.cc index 39cd473e5..7a6c416a7 100644 --- a/spot/twaalgos/hoa.cc +++ b/spot/twaalgos/hoa.cc @@ -489,6 +489,10 @@ namespace spot prop(" unambiguous"); else if (v1_1 && !aut->prop_unambiguous()) prop(" !unambiguous"); + if (aut->prop_semi_deterministic() && (verbose || !md.is_deterministic)) + prop(" semi-deterministic"); + else if (v1_1 && !aut->prop_semi_deterministic()) + prop(" !semi-deterministic"); if (aut->prop_stutter_invariant()) prop(" stutter-invariant"); if (!aut->prop_stutter_invariant()) diff --git a/spot/twaalgos/isdet.cc b/spot/twaalgos/isdet.cc index a0eb644ea..a63892058 100644 --- a/spot/twaalgos/isdet.cc +++ b/spot/twaalgos/isdet.cc @@ -18,8 +18,7 @@ // along with this program. If not, see . #include -#include -#include +#include namespace spot { @@ -148,4 +147,48 @@ namespace spot // initial state. return ns > 0; } + + bool + is_semi_deterministic(const const_twa_graph_ptr& aut) + { + trival sd = aut->prop_semi_deterministic(); + if (sd.is_known()) + return sd.is_true(); + scc_info si(aut); + si.determine_unknown_acceptance(); + unsigned nscc = si.scc_count(); + assert(nscc); + std::vector reachable_from_acc(nscc); + bool semi_det = true; + do // iterator of SCCs in reverse topological order + { + --nscc; + if (si.is_accepting_scc(nscc) || reachable_from_acc[nscc]) + { + for (unsigned succ: si.succ(nscc)) + reachable_from_acc[succ] = true; + for (unsigned src: si.states_of(nscc)) + { + bdd available = bddtrue; + for (auto& t: aut->out(src)) + if (!bdd_implies(t.cond, available)) + { + semi_det = false; + std::cerr << "Failed on state " << src << '\n'; + goto done; + } + else + { + available -= t.cond; + } + } + } + } + while (nscc); + done: + std::const_pointer_cast(aut) + ->prop_semi_deterministic(semi_det); + return semi_det; + } + } diff --git a/spot/twaalgos/isdet.hh b/spot/twaalgos/isdet.hh index 3478fba8f..eab7e624f 100644 --- a/spot/twaalgos/isdet.hh +++ b/spot/twaalgos/isdet.hh @@ -74,4 +74,13 @@ namespace spot /// i.e., each state as a successor for any possible configuration. SPOT_API bool is_complete(const const_twa_graph_ptr& aut); + + /// \brief Return true iff \a aut is semi-deterministic. + /// + /// An automaton is semi-deterministic if the sub-automaton + /// reachable from any accepting SCC is deterministic. + SPOT_API bool + is_semi_deterministic(const const_twa_graph_ptr& aut); + + } diff --git a/tests/Makefile.am b/tests/Makefile.am index f94d44f74..c61078503 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -208,6 +208,7 @@ TESTS_twa = \ core/renault.test \ core/nondet.test \ core/det.test \ + core/semidet.test \ core/neverclaimread.test \ core/parseaut.test \ core/optba.test \ diff --git a/tests/core/parseaut.test b/tests/core/parseaut.test index 270624432..9c5c64dd9 100755 --- a/tests/core/parseaut.test +++ b/tests/core/parseaut.test @@ -427,7 +427,7 @@ cat >input<. + +. ./defs +set -e + +cat >formulas < FGp1) +Gp1 U (p1 U GFp1) +(!p1 U p1) U X(!p0 -> Fp1) +(p1 | (Fp0 R (p1 W p0))) M 1 +!G(F(p1 & Fp0) W p1) +X(!p0 W Xp1) +1 U (p0 xor p1) +GF(p0) +FG(p0) +EOF + +ltl2tgba -F formulas --check=semi-det -Hl | + sed 's/deterministic.*/deterministic/g;s/.* //g' >out + +cat out +cat >expected <out +cat out +cat >expected <out +cat out +cat >expected <