diff --git a/NEWS b/NEWS index 14a2912d8..cc73604ce 100644 --- a/NEWS +++ b/NEWS @@ -10,6 +10,9 @@ New in spot 2.3.2.dev (not yet released) - spot::sum() and spot::sum_and() implements the union and the intersection of two automatons, respectively. + - twa objects have a new property: prop_complete(). This obviously + acts as a cache for the is_complete() function. + Bug fixes: - In "lenient" mode the parser would fail to recover from diff --git a/doc/org/concepts.org b/doc/org/concepts.org index f3a8d4d08..2de0ec80c 100644 --- a/doc/org/concepts.org +++ b/doc/org/concepts.org @@ -1056,11 +1056,12 @@ 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 | +| =state_acc= | automaton should be considered as 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 | +| =complete= | it is always possible to move the automaton forward, using any letter | | =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) | diff --git a/doc/org/hoa.org b/doc/org/hoa.org index a00ad54e3..c388e2431 100644 --- a/doc/org/hoa.org +++ b/doc/org/hoa.org @@ -661,7 +661,7 @@ particular: | =no-univ-branch= | ignored | no | only if =-Hv= | | | =univ-branch= | checked | no | checked | | | =deterministic= | checked | yes | checked | | -| =complete= | checked | no | checked | | +| =complete= | checked | yes | 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= | diff --git a/doc/org/tut21.org b/doc/org/tut21.org index 4c5a8562e..987446b17 100644 --- a/doc/org/tut21.org +++ b/doc/org/tut21.org @@ -131,6 +131,7 @@ corresponding BDD variable number, and then use for instance // would set the deterministic property on its output. In this // example, the properties that are set come from the "properties:" // line of the input file. + out << "Complete: " << aut->prop_complete() << '\n'; out << "Deterministic: " << aut->prop_deterministic() << '\n'; out << "Unambiguous: " << aut->prop_unambiguous() << '\n'; out << "State-Based Acc: " << aut->prop_state_acc() << '\n'; @@ -169,6 +170,7 @@ Number of edges: 10 Initial state: 0 Atomic propositions: a (=0) b (=1) c (=2) Name: Fa | G(Fb & Fc) +Complete: no Deterministic: no Unambiguous: yes State-Based Acc: maybe diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index a3a81f75c..986183b73 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -146,7 +146,7 @@ extern "C" int strverscmp(const char *s1, const char *s2); bool aliased_states = false; spot::trival deterministic = spot::trival::maybe(); - bool complete = false; + spot::trival complete = spot::trival::maybe(); bool trans_acc_seen = false; std::map labels; @@ -471,14 +471,15 @@ header: format-version header-items error(det.loc, "deterministic automata should have at most " "one initial state"); + res.deterministic = spot::trival::maybe(); } - res.deterministic = false; } else { // Assume the automaton is deterministic until proven // wrong, or unless we are building a Kripke structure. - res.deterministic = !res.opts.want_kripke; + if (!res.opts.want_kripke) + res.deterministic = true; } auto complete = res.prop_is_true("complete"); if (ss < 1) @@ -495,7 +496,8 @@ header: format-version header-items { // Assume the automaton is complete until proven // wrong. - res.complete = !res.opts.want_kripke; + if (!res.opts.want_kripke) + res.complete = true; } // if ap_count == 0, then a Kripke structure could be // declared complete, although that probably doesn't @@ -1034,6 +1036,7 @@ body: states // mention it in the next loop. if (s < res.info_states.size()) res.info_states[s].declared = true; + res.complete = spot::trival::maybe(); } unsigned n = res.info_states.size(); // States with number above res.states have already caused a @@ -1043,10 +1046,34 @@ body: states for (unsigned i = 0; i < n; ++i) { auto& p = res.info_states[i]; - if (p.used && !p.declared) - error(p.used_loc, - "state " + std::to_string(i) + " has no definition"); + if (!p.declared) + { + if (p.used) + error(p.used_loc, + "state " + std::to_string(i) + " has no definition"); + if (!p.used && res.complete) + if (auto p = res.prop_is_true("complete")) + { + error(res.states_loc, + "state " + std::to_string(i) + + " has no definition..."); + error(p.loc, "... despite 'properties: complete'"); + } + res.complete = false; + } } + if (res.complete) + if (auto p = res.prop_is_false("complete")) + { + error(@1, "automaton is complete..."); + error(p.loc, "... despite 'properties: !complete'"); + } + if (res.deterministic) + if (auto p = res.prop_is_false("deterministic")) + { + error(@1, "automaton is deterministic..."); + error(p.loc, "... despite 'properties: !deterministic'"); + } } state-num: INT @@ -1104,7 +1131,7 @@ checked-state-num: state-num states: | states state { - if ((res.deterministic || res.complete) && !res.opts.want_kripke) + if ((res.deterministic.is_true() || res.complete.is_true())) { bdd available = bddtrue; bool det = true; @@ -1114,7 +1141,7 @@ states: | states state det = false; available -= t.cond; } - if (res.deterministic && !det) + if (res.deterministic.is_true() && !det) { res.deterministic = false; if (auto p = res.prop_is_true("deterministic")) @@ -1124,7 +1151,7 @@ states: | states state "... despite 'properties: deterministic'"); } } - if (res.complete && available != bddfalse) + if (res.complete.is_true() && available != bddfalse) { res.complete = false; if (auto p = res.prop_is_true("complete")) @@ -1165,7 +1192,7 @@ state: state-name labeled-edges // Assume the worse. This skips the tests about determinism // we might perform on the state. res.deterministic = spot::trival::maybe(); - res.complete = false; + res.complete = spot::trival::maybe(); } @@ -1177,6 +1204,11 @@ state-name: "State:" state-label_opt checked-state-num string_opt state-acc_opt std::ostringstream o; o << "redeclaration of state " << $3; error(@1 + @3, o.str()); + // The additional transitions from extra states might + // led us to believe that the automaton is complete + // while it is not if we ignore them. + if (res.complete.is_true()) + res.complete = spot::trival::maybe(); } res.info_states[$3].declared = true; res.acc_state = $5; @@ -1499,7 +1531,7 @@ dstar_header: dstar_sizes } res.acc_style = State_Acc; res.deterministic = true; - // res.h->aut->prop_complete(); + res.complete = true; fill_guards(res); res.cur_guard = res.guards.end(); } @@ -2230,6 +2262,10 @@ static void fix_initial_state(result_& r) "a single initial state"); return; } + // Fiddling with initial state may turn an incomplete automaton + // into a complete one. + if (r.complete.is_false()) + r.complete = spot::trival::maybe(); // Multiple initial states. We might need to add a fake one, // unless one of the actual initial state has no incoming edge. auto& aut = r.h->aut; @@ -2299,7 +2335,9 @@ static void fix_initial_state(result_& r) static void fix_properties(result_& r) { r.aut_or_ks->prop_deterministic(r.deterministic); - //r.aut_or_ks->prop_complete(r.complete); + // std::cerr << "fix det: " << r.deterministic << '\n'; + // std::cerr << "fix complete: " << r.complete << '\n'; + r.aut_or_ks->prop_complete(r.complete); if (r.acc_style == State_Acc || (r.acc_style == Mixed_Acc && !r.trans_acc_seen)) r.aut_or_ks->prop_state_acc(true); diff --git a/spot/tl/exclusive.cc b/spot/tl/exclusive.cc index 399b2dc28..35e70c020 100644 --- a/spot/tl/exclusive.cc +++ b/spot/tl/exclusive.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement +// Copyright (C) 2015-2017 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -177,7 +177,7 @@ namespace spot twa_graph_ptr res = make_twa_graph(aut->get_dict()); res->copy_ap_of(aut); - res->prop_copy(aut, { true, true, false, true, true }); + res->prop_copy(aut, { true, true, false, true, false, true }); res->copy_acceptance_of(aut); if (simplify_guards) { diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index b6f216159..c9f9d07de 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -1,9 +1,9 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2013, 2014, 2015, 2016 Laboratoire de -// Recherche et Développement de l'Epita (LRDE). -// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de -// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -// Université Pierre et Marie Curie. +// Copyright (C) 2009, 2011, 2013-2017 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). +// Copyright (C) 2003-2005 Laboratoire d'Informatique de Paris 6 +// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université +// Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -992,6 +992,7 @@ namespace spot 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. + trival::repr_t complete:2; // Complete automaton. }; union { @@ -1267,6 +1268,29 @@ namespace spot } + /// \brief Whether the automaton is complete.. + /// + /// An automaton is complete if for each state the union of the + /// labels of its outgoing transitions is always true. + /// + /// Note that this method may return trival::maybe() when it is + /// unknown whether the automaton is complete or not. If you + /// need a true/false answer, prefer the is_complete() function. + /// + /// \see prop_complete() + /// \see is_complete() + trival prop_complete() const + { + return is.complete; + } + + /// \brief Set the complete property. + /// + /// \see is_complete() + void prop_complete(trival val) + { + is.complete = val.val(); + } /// \brief Whether the automaton is deterministic. /// @@ -1404,7 +1428,7 @@ namespace spot /// /// This can be used for instance as: /// \code - /// aut->prop_copy(other_aut, {true, false, false, false, true}); + /// aut->prop_copy(other_aut, {true, false, false, false, false, true}); /// \endcode /// This would copy the "state-based acceptance" and /// "stutter invariant" properties from \c other_aut to \c code. @@ -1428,8 +1452,52 @@ namespace spot bool inherently_weak; ///< preserve inherently weak, weak, & terminal bool deterministic; ///< preserve deterministic, semi-det, unambiguous bool improve_det; ///< improves deterministic, semi-det, unambiguous + bool complete; ///< preserves completeness bool stutter_inv; ///< preserve stutter invariance + prop_set() + : state_based(false), + inherently_weak(false), + deterministic(false), + improve_det(false), + complete(false), + stutter_inv(false) + { + } + + prop_set(bool state_based, + bool inherently_weak, + bool deterministic, + bool improve_det, + bool complete, + bool stutter_inv) + : state_based(state_based), + inherently_weak(inherently_weak), + deterministic(deterministic), + improve_det(improve_det), + complete(complete), + stutter_inv(stutter_inv) + { + } + +#ifndef SWIG + // The "complete" argument was added in Spot 2.4 + SPOT_DEPRECATED("prop_set() now takes 6 arguments") + prop_set(bool state_based, + bool inherently_weak, + bool deterministic, + bool improve_det, + bool stutter_inv) + : state_based(state_based), + inherently_weak(inherently_weak), + deterministic(deterministic), + improve_det(improve_det), + complete(false), + stutter_inv(stutter_inv) + { + } +#endif + /// \brief An all-true \c prop_set /// /// Use that only in algorithms that copy an automaton without @@ -1439,7 +1507,7 @@ namespace spot /// properties currently implemented, use an explicit /// /// \code - /// {true, true, true, true, true} + /// {true, true, true, true, true, true} /// \endcode /// /// instead of calling \c all(). This way, the day a new @@ -1447,7 +1515,7 @@ namespace spot /// algorithm X, in case that new property is not preserved. static prop_set all() { - return { true, true, true, true, true }; + return { true, true, true, true, true, true }; } }; @@ -1492,6 +1560,8 @@ namespace spot prop_unambiguous(true); } } + if (p.complete) + prop_complete(other->prop_complete()); if (p.stutter_inv) prop_stutter_invariant(other->prop_stutter_invariant()); } @@ -1521,6 +1591,8 @@ namespace spot if (!(p.improve_det && prop_unambiguous().is_true())) prop_unambiguous(trival::maybe()); } + if (!p.complete) + prop_complete(trival::maybe()); if (!p.stutter_inv) prop_stutter_invariant(trival::maybe()); } diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 28733cab6..18566180a 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -233,6 +233,14 @@ namespace spot v = current++; if (current == todo.size()) return; // No unreachable state. + + // Removing some non-deterministic dead state could make the + // automaton deterministic. + if (prop_deterministic().is_false()) + prop_deterministic(trival::maybe()); + if (prop_complete().is_false()) + prop_complete(trival::maybe()); + defrag_states(std::move(todo), current); } @@ -393,6 +401,14 @@ namespace spot useful[s] = -1U; if (current == num_states) return; // No useless state. + + // Removing some non-deterministic dead state could make the + // automaton deterministic. Likewise for non-complete. + if (prop_deterministic().is_false()) + prop_deterministic(trival::maybe()); + if (prop_complete().is_false()) + prop_complete(trival::maybe()); + defrag_states(std::move(useful), current); } diff --git a/spot/twaalgos/alternation.cc b/spot/twaalgos/alternation.cc index 0f4f0492c..9df955582 100644 --- a/spot/twaalgos/alternation.cc +++ b/spot/twaalgos/alternation.cc @@ -362,7 +362,7 @@ namespace spot res->copy_ap_of(aut_); // We preserve deterministic-like properties, and // stutter-invariance. - res->prop_copy(aut_, {false, false, false, true, true}); + res->prop_copy(aut_, {false, false, false, true, true, true}); res->set_generalized_buchi(has_reject_more_ + reject_1_count_); // We for easier computation of outgoing sets, we will diff --git a/spot/twaalgos/complete.cc b/spot/twaalgos/complete.cc index 60018ecaa..8ca6e1004 100644 --- a/spot/twaalgos/complete.cc +++ b/spot/twaalgos/complete.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et -// Développement de l'Epita. +// Copyright (C) 2013-2017 Laboratoire de Recherche et Développement +// de l'Epita. // // This file is part of Spot, a model checking library. // @@ -21,10 +21,12 @@ namespace spot { - unsigned complete_here(twa_graph_ptr aut) + void complete_here(twa_graph_ptr aut) { - unsigned n = aut->num_states(); unsigned sink = -1U; + if (aut->prop_complete().is_true()) + return; + unsigned n = aut->num_states(); // UM is a pair (bool, mark). If the Boolean is false, the // acceptance is always satisfiable. Otherwise, MARK is an @@ -126,24 +128,17 @@ namespace spot } } + aut->prop_complete(true); // Get rid of any named property if the automaton changed. if (t < aut->num_edges()) aut->release_named_properties(); else assert(t == aut->num_edges()); - - return sink; } twa_graph_ptr complete(const const_twa_ptr& aut) { - auto res = make_twa_graph(aut, { - true, // state based - true, // inherently_weak - true, // deterministic - true, // improve det - true, // stutter inv. - }); + auto res = make_twa_graph(aut, twa::prop_set::all()); complete_here(res); return res; } diff --git a/spot/twaalgos/complete.hh b/spot/twaalgos/complete.hh index 10c50a862..87703dcc2 100644 --- a/spot/twaalgos/complete.hh +++ b/spot/twaalgos/complete.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2013, 2014, 2015, 2017 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -25,12 +25,9 @@ namespace spot { /// \brief Complete a twa_graph in place. /// - /// If the TωA has no acceptance set, one will be added. The - /// returned value is the number of the sink state (it can be a new - /// state added for completion, or an existing non-accepting state - /// that has been reused as sink state because it had no outgoing - /// transitions apart from self-loops.) - SPOT_API unsigned complete_here(twa_graph_ptr aut); + /// If the TωA has an acceptance condition that is a tautology, + /// it will be changed into a Büchi automaton. + SPOT_API void complete_here(twa_graph_ptr aut); /// \brief Clone a twa and complete it. /// diff --git a/spot/twaalgos/degen.cc b/spot/twaalgos/degen.cc index f237ae03b..bb55b1d53 100644 --- a/spot/twaalgos/degen.cc +++ b/spot/twaalgos/degen.cc @@ -212,7 +212,7 @@ namespace spot if (want_sba) res->prop_state_acc(true); // Preserve determinism, weakness, and stutter-invariance - res->prop_copy(a, { false, true, true, true, true }); + res->prop_copy(a, { false, true, true, true, true, true }); // Create an order of acceptance conditions. Each entry in this // vector correspond to an acceptance set. Each index can diff --git a/spot/twaalgos/determinize.cc b/spot/twaalgos/determinize.cc index 3f4f68dbf..a4ebddd8b 100644 --- a/spot/twaalgos/determinize.cc +++ b/spot/twaalgos/determinize.cc @@ -641,6 +641,7 @@ namespace spot { false, // state based false, // inherently_weak false, false, // deterministic + true, // complete true // stutter inv }); diff --git a/spot/twaalgos/hoa.cc b/spot/twaalgos/hoa.cc index 469b66a32..53d576f86 100644 --- a/spot/twaalgos/hoa.cc +++ b/spot/twaalgos/hoa.cc @@ -160,8 +160,11 @@ namespace spot is_colored = colored && (!has_state_acc || nodeadend); // If the automaton declares that it is deterministic or // state-based, make sure that it really is. - assert(deterministic || aut->prop_deterministic() != true); - assert(state_acc || aut->prop_state_acc() != true); + assert(!aut->prop_deterministic().is_known() || + deterministic == aut->prop_deterministic().is_true()); + assert(!aut->prop_complete().is_known() || + complete == aut->prop_complete().is_true()); + assert(state_acc || !aut->prop_state_acc().is_true()); } void number_all_ap(const const_twa_graph_ptr& aut) diff --git a/spot/twaalgos/isdet.cc b/spot/twaalgos/isdet.cc index 5885351ed..eff3ede88 100644 --- a/spot/twaalgos/isdet.cc +++ b/spot/twaalgos/isdet.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2012-2017 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -134,6 +134,9 @@ namespace spot bool is_complete(const const_twa_graph_ptr& aut) { + trival cp = aut->prop_complete(); + if (cp.is_known()) + return cp.is_true(); unsigned ns = aut->num_states(); for (unsigned src = 0; src < ns; ++src) { @@ -141,11 +144,16 @@ namespace spot for (auto& t: aut->out(src)) available -= t.cond; if (available != bddfalse) - return false; + { + std::const_pointer_cast(aut)->prop_complete(false); + return false; + } } // The empty automaton is not complete since it does not have an // initial state. - return ns > 0; + bool res = ns > 0; + std::const_pointer_cast(aut)->prop_complete(res); + return res; } bool diff --git a/spot/twaalgos/mask.cc b/spot/twaalgos/mask.cc index c344a0778..7a2b666c1 100644 --- a/spot/twaalgos/mask.cc +++ b/spot/twaalgos/mask.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement +// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -26,7 +26,7 @@ namespace spot { auto res = make_twa_graph(in->get_dict()); res->copy_ap_of(in); - res->prop_copy(in, { true, true, true, true, false }); + res->prop_copy(in, { true, true, false, true, false, false }); unsigned na = in->num_sets(); unsigned tr = to_remove.count(); assert(tr <= na); @@ -54,7 +54,7 @@ namespace spot auto res = make_twa_graph(in->get_dict()); res->copy_ap_of(in); - res->prop_copy(in, { true, true, false, true, false }); + res->prop_copy(in, { true, true, false, true, false, false }); res->copy_acceptance_of(in); transform_copy(in, res, [&](unsigned src, bdd& cond, @@ -76,7 +76,7 @@ namespace spot auto res = make_twa_graph(in->get_dict()); res->copy_ap_of(in); - res->prop_copy(in, { true, true, false, true, false }); + res->prop_copy(in, { true, true, false, true, false, false }); res->copy_acceptance_of(in); transform_accessible(in, res, [&](unsigned src, bdd& cond, diff --git a/spot/twaalgos/minimize.cc b/spot/twaalgos/minimize.cc index 355f13fc3..753f6b51e 100644 --- a/spot/twaalgos/minimize.cc +++ b/spot/twaalgos/minimize.cc @@ -486,7 +486,7 @@ namespace spot // final is empty: there is no acceptance condition build_state_set(det_a, non_final); auto res = minimize_dfa(det_a, final, non_final); - res->prop_copy(a, { false, false, false, false, true }); + res->prop_copy(a, { false, false, false, false, true, true }); res->prop_deterministic(true); res->prop_weak(true); res->prop_state_acc(true); @@ -595,7 +595,7 @@ namespace spot } auto res = minimize_dfa(det_a, final, non_final); - res->prop_copy(a, { false, false, false, false, true }); + res->prop_copy(a, { false, false, false, false, false, true }); res->prop_deterministic(true); res->prop_weak(true); // If the input was terminal, then the output is also terminal. diff --git a/spot/twaalgos/product.cc b/spot/twaalgos/product.cc index 601b23a1d..1c9c50102 100644 --- a/spot/twaalgos/product.cc +++ b/spot/twaalgos/product.cc @@ -106,22 +106,21 @@ namespace spot } } - res->prop_deterministic(left->prop_deterministic() - && right->prop_deterministic()); - res->prop_stutter_invariant(left->prop_stutter_invariant() - && right->prop_stutter_invariant()); - // The product of X!a and Xa, two stutter-sentive formulas, - // is stutter-invariant. - //res->prop_stutter_sensitive(left->prop_stutter_sensitive() - // && right->prop_stutter_sensitive()); - res->prop_inherently_weak(left->prop_inherently_weak() - && right->prop_inherently_weak()); - res->prop_weak(left->prop_weak() - && right->prop_weak()); - res->prop_terminal(left->prop_terminal() - && right->prop_terminal()); - res->prop_state_acc(left->prop_state_acc() - && right->prop_state_acc()); + // The product of two non-deterministic automata could be + // deterministic. likewise for non-complete automata. + if (left->prop_deterministic() && right->prop_deterministic()) + res->prop_deterministic(true); + if (left->prop_complete() && right->prop_complete()) + res->prop_complete(true); + if (left->prop_stutter_invariant() && right->prop_stutter_invariant()) + res->prop_stutter_invariant(true); + if (left->prop_inherently_weak() && right->prop_inherently_weak()) + res->prop_inherently_weak(true); + if (left->prop_weak() && right->prop_weak()) + res->prop_weak(true); + if (left->prop_terminal() && right->prop_terminal()) + res->prop_terminal(true); + res->prop_state_acc(left->prop_state_acc() && right->prop_state_acc()); return res; } } diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index 5bf5d060d..f748f503e 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -224,11 +224,12 @@ namespace spot unsigned nst = aut->num_states(); auto res = make_twa_graph(aut->get_dict()); res->copy_ap_of(aut); - res->prop_copy(aut, { true, false, false, false, true }); + res->prop_copy(aut, { true, false, false, false, false, true }); res->new_states(nst); res->set_buchi(); res->set_init_state(aut->get_init_state_number()); trival deterministic = aut->prop_deterministic(); + trival complete = aut->prop_complete(); std::vector state_map(aut->num_states()); for (unsigned n = 0; n < scc_max; ++n) @@ -245,11 +246,11 @@ namespace spot for (auto& t: aut->out(s)) res->new_acc_edge(s, t.dst, t.cond, acc); } - continue; } else { deterministic = false; + complete = trival::maybe(); // The main copy is only accepting for inf_alone // and for all Inf sets that have no matching Fin @@ -300,8 +301,9 @@ namespace spot } } } - res->purge_dead_states(); + res->prop_complete(complete); res->prop_deterministic(deterministic); + res->purge_dead_states(); return res; } @@ -386,10 +388,11 @@ namespace spot auto res = make_twa_graph(aut, { true, // state based - true, // inherently weak - true, true, // determinisitic - true, // stutter inv. - }); + true, // inherently weak + true, true, // determinisitic + true, // complete + true, // stutter inv. + }); scc_info si(res); // We will modify res in place, and the resulting @@ -663,7 +666,7 @@ namespace spot unsigned nst = aut->num_states(); auto res = make_twa_graph(aut->get_dict()); res->copy_ap_of(aut); - res->prop_copy(aut, { true, false, false, false, true }); + res->prop_copy(aut, { true, false, false, false, false, true }); res->new_states(nst); res->set_acceptance(aut->num_sets() + extra_sets, new_code); res->set_init_state(aut->get_init_state_number()); diff --git a/spot/twaalgos/remprop.cc b/spot/twaalgos/remprop.cc index 8340bef7e..32e32bfdb 100644 --- a/spot/twaalgos/remprop.cc +++ b/spot/twaalgos/remprop.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2015-2017 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -130,7 +130,7 @@ namespace spot twa_graph_ptr res = make_twa_graph(d); res->copy_ap_of(aut); - res->prop_copy(aut, { true, true, false, false, false }); + res->prop_copy(aut, { true, true, false, false, false, false }); res->copy_acceptance_of(aut); for (auto ap: props_exist) diff --git a/spot/twaalgos/sbacc.cc b/spot/twaalgos/sbacc.cc index 93acc554c..2090a5fd3 100644 --- a/spot/twaalgos/sbacc.cc +++ b/spot/twaalgos/sbacc.cc @@ -57,7 +57,7 @@ namespace spot auto res = make_twa_graph(old->get_dict()); res->copy_ap_of(old); res->copy_acceptance_of(old); - res->prop_copy(old, {false, true, true, true, true}); + res->prop_copy(old, {false, true, true, true, true, true}); res->prop_state_acc(true); typedef std::pair pair_t; diff --git a/spot/twaalgos/sccfilter.cc b/spot/twaalgos/sccfilter.cc index b2ca23908..1a354aed8 100644 --- a/spot/twaalgos/sccfilter.cc +++ b/spot/twaalgos/sccfilter.cc @@ -375,7 +375,7 @@ namespace spot else res = scc_filter_apply>>(aut, given_si); - res->prop_copy(aut, { true, true, false, true, true }); + res->prop_copy(aut, { true, true, false, true, false, true }); return res; } @@ -417,6 +417,7 @@ namespace spot true, false, true, // determinism improved + false, true, }); return res; @@ -451,6 +452,7 @@ namespace spot { false, // state-based acceptance is not preserved true, false, false, // determinism may not be preserved + false, false, // stutter inv. of suspvars probably altered }); return res; diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc index e59ed5e4a..e2b4628bb 100644 --- a/spot/twaalgos/simulation.cc +++ b/spot/twaalgos/simulation.cc @@ -595,6 +595,7 @@ namespace spot { false, // state-based acc forced below true, // weakness preserved, false, true, // determinism improved + true, // completeness preserved true, // stutter inv. }); // !unambiguous and !semi-deterministic are not preserved diff --git a/spot/twaalgos/strength.cc b/spot/twaalgos/strength.cc index 7c3428eef..418583c78 100644 --- a/spot/twaalgos/strength.cc +++ b/spot/twaalgos/strength.cc @@ -295,7 +295,7 @@ namespace spot twa_graph_ptr res = make_twa_graph(aut->get_dict()); res->copy_ap_of(aut); - res->prop_copy(aut, { true, false, false, true, false }); + res->prop_copy(aut, { true, false, false, true, false, false }); if (keep & Strong) res->copy_acceptance_of(aut); @@ -362,7 +362,7 @@ namespace spot const_twa_graph_ptr aut = sm.get_aut(); twa_graph_ptr res = make_twa_graph(aut->get_dict()); res->copy_ap_of(aut); - res->prop_copy(aut, { true, false, false, true, false }); + res->prop_copy(aut, { true, false, false, true, false, false }); res->copy_acceptance_of(aut); auto um = aut->acc().unsat_mark(); diff --git a/spot/twaalgos/stutter.cc b/spot/twaalgos/stutter.cc index 1d1e7e1f1..6ecb1717a 100644 --- a/spot/twaalgos/stutter.cc +++ b/spot/twaalgos/stutter.cc @@ -400,10 +400,11 @@ namespace spot } } if (num_states != a->num_states()) - a->prop_keep({true, // state_based + a->prop_keep({true, // state_based false, // inherently_weak false, false, // deterministic - false, // stutter inv. + true, // complete + false, // stutter inv. }); a->merge_edges(); return a; @@ -423,6 +424,7 @@ namespace spot a->prop_keep({false, // state_based false, // inherently_weak false, false, // deterministic + true, // complete false, // stutter inv. }); diff --git a/spot/twaalgos/totgba.cc b/spot/twaalgos/totgba.cc index 146b8ab3d..8f56fe7c2 100644 --- a/spot/twaalgos/totgba.cc +++ b/spot/twaalgos/totgba.cc @@ -146,7 +146,7 @@ namespace spot auto out = make_twa_graph(in->get_dict()); out->copy_ap_of(in); - out->prop_copy(in, {false, false, false, false, true}); + out->prop_copy(in, {false, false, false, false, false, true}); out->set_generalized_buchi(p); acc_cond::mark_t outall = out->acc().all_sets(); diff --git a/tests/core/parseaut.test b/tests/core/parseaut.test index 9c5c64dd9..c7e952bd3 100755 --- a/tests/core/parseaut.test +++ b/tests/core/parseaut.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et -# Développement de l'Epita (LRDE). +# Copyright (C) 2014-2017 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -367,8 +367,23 @@ State: 1 { 1 } State: 2 "sink state" { 0 } 2 2 2 2 --END-- +HOA: v1.1 +name: "GFa" +States: 1 +Start: 0 +AP: 1 "a" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels trans-acc !complete +properties: !deterministic stutter-invariant +--BODY-- +State: 0 +[0] 0 {0} +[!0] 0 +--END-- EOF +err1="this might cause the following errors" expecterr input <input<" + "" ] } ], @@ -711,7 +727,7 @@ "metadata": {}, "output_type": "display_data", "text": [ - "" + "" ] } ], @@ -1066,7 +1082,7 @@ "metadata": {}, "output_type": "display_data", "text": [ - "" + "" ] } ], @@ -1487,7 +1503,7 @@ "metadata": {}, "output_type": "display_data", "text": [ - "" + "" ] }, { @@ -1664,7 +1680,7 @@ " result.set_state_names(names)\n", " \n", " # Loop over all the properties we want to preserve if they hold in both automata\n", - " for p in ('prop_deterministic', 'prop_weak', 'prop_inherently_weak', \n", + " for p in ('prop_deterministic', 'prop_complete', 'prop_weak', 'prop_inherently_weak', \n", " 'prop_terminal', 'prop_stutter_invariant', 'prop_state_acc'):\n", " if getattr(left, p)() and getattr(right, p)():\n", " getattr(result, p)(True)\n", @@ -1991,7 +2007,7 @@ "metadata": {}, "output_type": "display_data", "text": [ - "" + "" ] }, { @@ -2026,7 +2042,7 @@ "output_type": "stream", "stream": "stdout", "text": [ - "1000 loops, best of 3: 342 \u00b5s per loop\n" + "1000 loops, best of 3: 206 \u00b5s per loop\n" ] } ], @@ -2045,7 +2061,8 @@ "output_type": "stream", "stream": "stdout", "text": [ - "100000 loops, best of 3: 6.44 \u00b5s per loop\n" + "The slowest run took 6.27 times longer than the fastest. This could mean that an intermediate result is being cached.\n", + "100000 loops, best of 3: 4.2 \u00b5s per loop\n" ] } ],