From 94cca9de3dd2be8165636a7b6a839da426d04125 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 17 Dec 2015 08:42:34 +0100 Subject: [PATCH] acc_cond: rename is_tt/is_ff as is_t/is_f and add printer * spot/twa/acc.cc, spot/twa/acc.hh: Here. * spot/parseaut/parseaut.yy, spot/twa/acc.hh, spot/twaalgos/gtec/gtec.cc, spot/twaalgos/hoa.cc, spot/twaalgos/neverclaim.cc, spot/twaalgos/product.cc, spot/twaalgos/remfin.cc, spot/twaalgos/strength.cc: Adjust. * NEWS: Mention the changes. * wrap/python/spot_impl.i: Bind acc_cond the printer. * wrap/python/tests/acc_cond.ipynb: Add more examples. --- NEWS | 15 ++- spot/parseaut/parseaut.yy | 2 +- spot/twa/acc.cc | 27 +++-- spot/twa/acc.hh | 38 +++++-- spot/twaalgos/gtec/gtec.cc | 4 +- spot/twaalgos/hoa.cc | 4 +- spot/twaalgos/neverclaim.cc | 2 +- spot/twaalgos/product.cc | 2 +- spot/twaalgos/remfin.cc | 4 +- spot/twaalgos/strength.cc | 2 +- wrap/python/spot_impl.i | 18 ++- wrap/python/tests/acc_cond.ipynb | 185 ++++++++++++++++++++++++++++++- 12 files changed, 259 insertions(+), 44 deletions(-) diff --git a/NEWS b/NEWS index e45f39182..94a7c4f24 100644 --- a/NEWS +++ b/NEWS @@ -37,17 +37,22 @@ New in spot 1.99.6a (not yet released) shift_left() have been replaced by operators |=, &=, <<=, and for completeness the operators |, &, and << have been added. - * Several methods have been removed from the acc_cond class because - they were simply redundant with the methods of acc_cond::mark_t, - and more complex to use. + * Several methods have been removed from the acc_cond + class because they were simply redundant with the methods of + acc_cond::mark_t, and more complex to use. - acc_cond::marks(...) -> use acc_cond::mark_t(...) directly + acc_cond::marks(...) -> use acc_cond::mark_t(...) acc_cond::sets(m) -> use m.sets() - acc_cond::has(m, u) -> use m.has(u) directly + acc_cond::has(m, u) -> use m.has(u) acc_cond::cup(l, r) -> use l | r acc_cond::cap(l, r) -> use l & r acc_cond::set_minus(l, r) -> use l - r + Additionally, the following methods have been renamed: + + acc_cond::is_tt() -> acc_cond::is_t() + acc_cond::is_ff() -> acc_cond::is_f() + Python: * Iterating over the transitions leaving a state (the diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index 907935b26..f462e1b3b 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -572,7 +572,7 @@ header-item: "States:" INT res.ignore_more_acc = true; // Not setting the acceptance in case of error will // force it to be true. - if (res.opts.want_kripke && (!$4->is_tt() || $2 > 0)) + if (res.opts.want_kripke && (!$4->is_t() || $2 > 0)) error(@2 + @4, "the acceptance for Kripke structure must be '0 t'"); else diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index e5e229e01..9a42cf572 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -51,6 +51,11 @@ namespace spot return os; } + std::ostream& operator<<(std::ostream& os, const acc_cond& acc) + { + return os << '(' << acc.num_sets() << ", " << acc.get_acceptance() << ')'; + } + namespace { void default_set_printer(std::ostream& os, int v) @@ -411,9 +416,9 @@ namespace spot int acc_cond::is_rabin() const { - if (code_.is_ff()) + if (code_.is_f()) return num_ == 0 ? 0 : -1; - if ((num_ & 1) || code_.is_tt()) + if ((num_ & 1) || code_.is_t()) return -1; if (is_rs(code_, acc_op::Or, acc_op::And, all_sets())) @@ -424,9 +429,9 @@ namespace spot int acc_cond::is_streett() const { - if (code_.is_tt()) + if (code_.is_t()) return num_ == 0 ? 0 : -1; - if ((num_ & 1) || code_.is_ff()) + if ((num_ & 1) || code_.is_f()) return -1; if (is_rs(code_, acc_op::And, acc_op::Or, all_sets())) @@ -444,7 +449,7 @@ namespace spot pairs.resize(num_); return true; } - if (code_.is_tt() + if (code_.is_t() || code_.back().op != acc_op::Or) return false; @@ -670,7 +675,7 @@ namespace spot if (sets == 0) { max = true; - odd = is_tt(); + odd = is_t(); return true; } acc_cond::mark_t u_inf; @@ -857,7 +862,7 @@ namespace spot std::pair acc_cond::unsat_mark() const { - if (is_tt()) + if (is_t()) return {false, 0U}; if (!uses_fin_acceptance()) return {true, 0U}; @@ -1105,7 +1110,7 @@ namespace spot acc_cond::acc_code acc_cond::acc_code::complement() const { - if (is_tt()) + if (is_t()) return acc_cond::acc_code::f(); return complement_rec(&back()); } @@ -1165,7 +1170,7 @@ namespace spot acc_cond::acc_code acc_cond::acc_code::strip(acc_cond::mark_t rem, bool missing) const { - if (is_tt() || is_ff()) + if (is_t() || is_f()) return *this; return strip_rec(&back(), rem, missing); } @@ -1173,7 +1178,7 @@ namespace spot acc_cond::mark_t acc_cond::acc_code::used_sets() const { - if (is_tt() || is_ff()) + if (is_t() || is_f()) return 0U; acc_cond::mark_t used_in_cond = 0U; auto pos = &back(); @@ -1201,7 +1206,7 @@ namespace spot std::pair acc_cond::acc_code::used_inf_fin_sets() const { - if (is_tt() || is_ff()) + if (is_t() || is_f()) return {0U, 0U}; acc_cond::mark_t used_fin = 0U; diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index 489dd9dcd..97f9f8c93 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -395,14 +395,14 @@ namespace spot return !(*this == other); } - bool is_tt() const + bool is_t() const { unsigned s = size(); return s == 0 || ((*this)[s - 1].op == acc_op::Inf && (*this)[s - 2].mark == 0U); } - bool is_ff() const + bool is_f() const { unsigned s = size(); return s > 1 @@ -557,12 +557,12 @@ namespace spot acc_code& operator&=(acc_code&& r) { - if (is_tt() || r.is_ff()) + if (is_t() || r.is_f()) { *this = std::move(r); return *this; } - if (is_ff() || r.is_tt()) + if (is_f() || r.is_t()) return *this; unsigned s = size() - 1; unsigned rs = r.size() - 1; @@ -649,12 +649,12 @@ namespace spot acc_code& operator&=(const acc_code& r) { - if (is_tt() || r.is_ff()) + if (is_t() || r.is_f()) { *this = r; return *this; } - if (is_ff() || r.is_tt()) + if (is_f() || r.is_t()) return *this; unsigned s = size() - 1; unsigned rs = r.size() - 1; @@ -754,9 +754,9 @@ namespace spot acc_code& operator|=(acc_code&& r) { - if (is_tt() || r.is_ff()) + if (is_t() || r.is_f()) return *this; - if (is_ff() || r.is_tt()) + if (is_f() || r.is_t()) { *this = std::move(r); return *this; @@ -930,14 +930,24 @@ namespace spot return uses_fin_acceptance_; } - bool is_tt() const + bool is_t() const { - return code_.is_tt(); + return code_.is_t(); } - bool is_ff() const + bool is_all() const { - return code_.is_ff(); + return num_ == 0 && is_t(); + } + + bool is_f() const + { + return code_.is_f(); + } + + bool is_none() const + { + return num_ == 0 && is_f(); } bool is_buchi() const @@ -1158,6 +1168,7 @@ namespace spot mark_t::value_t all_; acc_code code_; bool uses_fin_acceptance_ = false; + }; /// \brief Parse a string into an acc_code @@ -1179,6 +1190,9 @@ namespace spot /// /// A spot::parse_error is thrown on syntax error. SPOT_API acc_cond::acc_code parse_acc_code(const char* input); + + SPOT_API + std::ostream& operator<<(std::ostream& os, const acc_cond& acc); } namespace std diff --git a/spot/twaalgos/gtec/gtec.cc b/spot/twaalgos/gtec/gtec.cc index 40c985921..272aacda1 100644 --- a/spot/twaalgos/gtec/gtec.cc +++ b/spot/twaalgos/gtec/gtec.cc @@ -133,7 +133,7 @@ namespace spot { { auto acc = ecs_->aut->acc(); - if (acc.get_acceptance().is_ff()) + if (acc.get_acceptance().is_f()) return nullptr; if (acc.uses_fin_acceptance()) throw std::runtime_error @@ -395,7 +395,7 @@ namespace spot { { auto acc = ecs_->aut->acc(); - if (acc.get_acceptance().is_ff()) + if (acc.get_acceptance().is_f()) return nullptr; if (acc.uses_fin_acceptance()) throw std::runtime_error diff --git a/spot/twaalgos/hoa.cc b/spot/twaalgos/hoa.cc index eaea788af..aee404ea6 100644 --- a/spot/twaalgos/hoa.cc +++ b/spot/twaalgos/hoa.cc @@ -313,7 +313,7 @@ namespace spot acc_cond::acc_code acc_c = aut->acc().get_acceptance(); if (aut->acc().is_generalized_buchi()) { - if (aut->acc().is_tt()) + if (aut->acc().is_all()) os << "acc-name: all"; else if (aut->acc().is_buchi()) os << "acc-name: Buchi"; @@ -323,7 +323,7 @@ namespace spot } else if (aut->acc().is_generalized_co_buchi()) { - if (aut->acc().is_ff()) + if (aut->acc().is_none()) os << "acc-name: none"; else if (aut->acc().is_co_buchi()) os << "acc-name: co-Buchi"; diff --git a/spot/twaalgos/neverclaim.cc b/spot/twaalgos/neverclaim.cc index 1d92ebf5f..e68356527 100644 --- a/spot/twaalgos/neverclaim.cc +++ b/spot/twaalgos/neverclaim.cc @@ -205,7 +205,7 @@ namespace spot print_never_claim(std::ostream& os, const const_twa_ptr& g, const char* options) { - if (!(g->acc().is_buchi() || g->acc().is_tt())) + if (!(g->acc().is_buchi() || g->acc().is_all())) throw std::runtime_error ("Never claim output only supports Büchi acceptance"); never_claim_output d(os, options); diff --git a/spot/twaalgos/product.cc b/spot/twaalgos/product.cc index 16515739c..738ba9347 100644 --- a/spot/twaalgos/product.cc +++ b/spot/twaalgos/product.cc @@ -80,7 +80,7 @@ namespace spot }; res->set_init_state(new_state(left_state, right_state)); - if (right_acc.is_ff()) + if (right_acc.is_f()) // Do not bother doing any work if the resulting acceptance is // false. return res; diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index 9fcac273c..27d47e90c 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -312,7 +312,7 @@ namespace spot auto code = aut->get_acceptance(); - if (code.is_tt()) + if (code.is_t()) return nullptr; acc_cond::mark_t inf_pairs = 0U; @@ -640,7 +640,7 @@ namespace spot auto c = acc.inf(m); for (unsigned i = 0; i < sz; ++i) { - if (!code[i].is_tt()) + if (!code[i].is_t()) continue; add[i] = m; code[i] &= std::move(c); diff --git a/spot/twaalgos/strength.cc b/spot/twaalgos/strength.cc index 22071eb70..3e29a2fbe 100644 --- a/spot/twaalgos/strength.cc +++ b/spot/twaalgos/strength.cc @@ -126,7 +126,7 @@ namespace spot bool is_safety_mwdba(const const_twa_graph_ptr& aut) { - if (!(aut->acc().is_buchi() || aut->acc().is_tt())) + if (!(aut->acc().is_buchi() || aut->acc().is_all())) throw std::runtime_error ("is_safety_mwdba() should be called on a Buchi automaton"); diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i index 00e5f8616..ce6583496 100644 --- a/wrap/python/spot_impl.i +++ b/wrap/python/spot_impl.i @@ -485,19 +485,35 @@ namespace std { return new spot::acc_cond::mark_t(f.begin(), f.end()); } - std::string __str__() + std::string __repr__() { std::ostringstream os; os << *self; return os.str(); } + std::string __str__() + { + std::ostringstream os; + os << *self; + return os.str(); + } +} + +%extend spot::acc_cond { std::string __repr__() { std::ostringstream os; os << *self; return os.str(); } + + std::string __str__() + { + std::ostringstream os; + os << *self; + return os.str(); + } } %extend spot::twa_run { diff --git a/wrap/python/tests/acc_cond.ipynb b/wrap/python/tests/acc_cond.ipynb index 15c0af6c3..d7e98d354 100644 --- a/wrap/python/tests/acc_cond.ipynb +++ b/wrap/python/tests/acc_cond.ipynb @@ -1,7 +1,23 @@ { "metadata": { - "name": "", - "signature": "sha256:f11212c3a17ce302ae81974af32b21c1ebda4aa54d8930f03787ce7ed1c9e5f5" + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.4.3+" + }, + "name": "" }, "nbformat": 3, "nbformat_minor": 0, @@ -920,7 +936,7 @@ "output_type": "pyout", "prompt_number": 34, "text": [ - " >" + "(4, (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)))" ] } ], @@ -970,17 +986,176 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "To be continued..." + "The `acc_cond` object can also be constructed using only a number of sets. In that case, the acceptance condition defaults to `t`, and it can be changed to something else later (using `set_acceptance()`). The number of acceptance sets can also be augmented with `add_sets()`." ] }, { "cell_type": "code", "collapsed": false, + "input": [ + "acc = spot.acc_cond(4)\n", + "acc" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 37, + "text": [ + "(4, t)" + ] + } + ], + "prompt_number": 37 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "acc.add_sets(2)\n", + "acc" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 38, + "text": [ + "(6, t)" + ] + } + ], + "prompt_number": 38 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "acc.set_acceptance(spot.parse_acc_code('Streett 2'))\n", + "acc" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 39, + "text": [ + "(6, (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)))" + ] + } + ], + "prompt_number": 39 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The common scenario of setting generalized B\u00fcchi acceptance can be achieved more efficiently as follows:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "acc = spot.acc_cond(4)\n", + "acc.set_generalized_buchi()\n", + "acc" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 40, + "text": [ + "(4, Inf(0)&Inf(1)&Inf(2)&Inf(3))" + ] + } + ], + "prompt_number": 40 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The `acc_cond` class has several methods for detecting acceptance conditions that match the named acceptance conditions of the HOA format. Note that in the HOA format, `Inf(0)&Inf(1)&Inf(2)&Inf(3)` is only called generalized B\u00fcchi if exactly for acceptance sets are used. So the following behavior should not be a surprise:" + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "print(acc)\n", + "print(acc.is_generalized_buchi())\n", + "acc.add_sets(1)\n", + "print(acc)\n", + "print(acc.is_generalized_buchi())" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "(4, Inf(0)&Inf(1)&Inf(2)&Inf(3))\n", + "True\n", + "(5, Inf(0)&Inf(1)&Inf(2)&Inf(3))\n", + "False\n" + ] + } + ], + "prompt_number": 41 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Similar methods like `is_t()`, `is_f()`, `is_buchi()`, `is_co_buchi()`, `is_generalized_co_buchi()` all return a Boolean.\n", + "\n", + "The `is_rabin()` and `is_streett()` methods, however, return a number of pairs. The number of pairs is always `num_sets()/2` on success, or -1 on failure." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "code = spot.parse_acc_code('Rabin 2')\n", + "acc = spot.acc_cond(code.used_sets().max_set(), code)\n", + "print(acc)\n", + "print(acc.is_rabin())\n", + "print(acc.is_streett())" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "output_type": "stream", + "stream": "stdout", + "text": [ + "(4, (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)))\n", + "2\n", + "-1\n" + ] + } + ], + "prompt_number": 42 + }, + { + "cell_type": "code", + "collapsed": true, "input": [], "language": "python", "metadata": {}, "outputs": [], - "prompt_number": 36 + "prompt_number": null } ], "metadata": {}