From fd1f6c4d612f79f90f9efbcee5d180fde6c832c1 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 18 Feb 2015 11:28:03 +0100 Subject: [PATCH] Preliminirary support for generic acceptance. * src/tgba/acc.hh: Add creation and printing of generic acceptance code. * src/tgba/acc.cc: New file. * src/tgba/Makefile.am: Add it. * src/tgbatest/acc.cc: More tests. * src/tgbatest/acc.test: Update. * src/tgba/tgba.hh (set_acceptance, get_acceptance): New methods. * src/tgba/tgbagraph.hh: Store acceptance code. * src/hoaparse/hoaparse.yy: Read any acceptance. * src/dstarparse/nsa2tgba.cc, src/ta/taexplicit.cc, src/tgba/tgbaproduct.cc, src/tgba/tgbasafracomplement.cc, src/tgbaalgos/degen.cc, src/tgbaalgos/hoa.cc, src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/product.cc, src/tgbaalgos/stutter.cc, src/tgbatest/hoaparse.test: Adjust. --- src/dstarparse/nsa2tgba.cc | 1 + src/hoaparse/hoaparse.yy | 179 ++++++++++++++---- src/ta/taexplicit.cc | 1 + src/tgba/Makefile.am | 1 + src/tgba/acc.cc | 238 ++++++++++++++++++++++++ src/tgba/acc.hh | 309 ++++++++++++++++++++++++-------- src/tgba/tgba.hh | 19 ++ src/tgba/tgbagraph.hh | 11 +- src/tgba/tgbaproduct.cc | 8 +- src/tgba/tgbasafracomplement.cc | 5 +- src/tgbaalgos/degen.cc | 16 +- src/tgbaalgos/hoa.cc | 27 ++- src/tgbaalgos/ltl2taa.cc | 5 +- src/tgbaalgos/ltl2tgba_fm.cc | 6 +- src/tgbaalgos/product.cc | 9 +- src/tgbaalgos/stutter.cc | 1 + src/tgbatest/acc.cc | 23 ++- src/tgbatest/acc.test | 7 + src/tgbatest/hoaparse.test | 88 ++++++--- 19 files changed, 778 insertions(+), 176 deletions(-) create mode 100644 src/tgba/acc.cc diff --git a/src/dstarparse/nsa2tgba.cc b/src/dstarparse/nsa2tgba.cc index 565f3c647..a667f1e49 100644 --- a/src/dstarparse/nsa2tgba.cc +++ b/src/dstarparse/nsa2tgba.cc @@ -199,6 +199,7 @@ namespace spot while (i != bs2num.end()) delete (i++)->first.pend; + res->acc().set_generalized_buchi(); return res; } diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy index cda1be996..cbf7c91f9 100644 --- a/src/hoaparse/hoaparse.yy +++ b/src/hoaparse/hoaparse.yy @@ -135,6 +135,7 @@ spot::acc_cond::mark_t mark; pair* p; std::list* list; + spot::acc_cond::acc_code* code; } %code @@ -201,6 +202,7 @@ %type

nc-transition nc-src-dest %type nc-transitions nc-transition-block %type nc-one-ident nc-ident-list +%type acceptance-cond /**** LBTT tokens *****/ // Also using INT, STRING @@ -216,6 +218,7 @@ %destructor { delete $$; } %destructor { bdd_delref($$); } %destructor { bdd_delref($$->first); delete $$->second; delete $$; }

+%destructor { delete $$; } %destructor { for (std::list::iterator i = $$->begin(); i != $$->end(); ++i) @@ -484,7 +487,7 @@ header-item: "States:" INT } else { - res.h->aut->set_acceptance_conditions($2); + res.h->aut->acc().add_sets($2); res.accset = $2; res.accset_loc = @1 + @2; } @@ -492,6 +495,8 @@ header-item: "States:" INT acceptance-cond { res.ignore_more_acc = true; + res.h->aut->set_acceptance($2, *$4); + delete $4; } | "acc-name:" IDENTIFIER acc-spec { @@ -659,36 +664,65 @@ acc-set: INT acceptance-cond: IDENTIFIER '(' acc-set ')' { - if (!res.ignore_more_acc && *$1 != "Inf") - error(@1, "this implementation only supports " - "'Inf' acceptance"); if ($3 != -1U) - res.pos_acc_sets |= res.h->aut->acc().mark($3); + { + res.pos_acc_sets |= res.h->aut->acc().mark($3); + if (*$1 == "Inf") + $$ = new spot::acc_cond::acc_code + (res.h->aut->acc().inf({$3})); + else + $$ = new spot::acc_cond::acc_code + (res.h->aut->acc().fin({$3})); + } + else + { + $$ = new spot::acc_cond::acc_code; + } delete $1; } | IDENTIFIER '(' '!' acc-set ')' { - if (!res.ignore_more_acc && *$1 != "Inf") - error(@1, "this implementation only supports " - "'Inf' acceptance"); if ($4 != -1U) - res.neg_acc_sets |= res.h->aut->acc().mark($4); + { + res.neg_acc_sets |= res.h->aut->acc().mark($4); + if (*$1 == "Inf") + $$ = new spot::acc_cond::acc_code + (res.h->aut->acc().inf_neg({$4})); + else + $$ = new spot::acc_cond::acc_code + (res.h->aut->acc().fin_neg({$4})); + } + else + { + $$ = new spot::acc_cond::acc_code; + } delete $1; } | '(' acceptance-cond ')' + { + $$ = $2; + } | acceptance-cond '&' acceptance-cond + { + $3->append_and(std::move(*$1)); + $$ = $3; + delete $1; + } | acceptance-cond '|' acceptance-cond { - if (!res.ignore_more_acc) - error(@2, "this implementation does not support " - "disjunction in acceptance conditions"); + $3->append_or(std::move(*$1)); + $$ = $3; + delete $1; } | 't' + { + $$ = new spot::acc_cond::acc_code; + } | 'f' { - if (!res.ignore_more_acc) - error(@$, "this implementation does not support " - "false acceptance"); + { + $$ = new spot::acc_cond::acc_code(res.h->aut->acc().fin({})); + } } @@ -1213,7 +1247,10 @@ nc-transition: lbtt: lbtt-header lbtt-body ENDAUT { - res.pos_acc_sets = res.h->aut->acc().all_sets(); + auto& acc = res.h->aut->acc(); + unsigned num = acc.num_sets(); + res.h->aut->set_acceptance_conditions(num); + res.pos_acc_sets = acc.all_sets(); assert(!res.states_map.empty()); auto n = res.states_map.size(); if (n != (unsigned) res.states) @@ -1375,33 +1412,113 @@ static void fill_guards(result_& r) void hoayy::parser::error(const location_type& location, - const std::string& message) + const std::string& message) { error_list.emplace_back(location, message); } +static spot::acc_cond::acc_code +fix_acceptance_aux(spot::acc_cond& acc, + spot::acc_cond::acc_code in, unsigned pos, + spot::acc_cond::mark_t onlyneg, + spot::acc_cond::mark_t both, + unsigned base) +{ + auto& w = in[pos]; + switch (w.op) + { + case spot::acc_cond::acc_op::And: + { + unsigned sub = pos - w.size; + --pos; + auto c = fix_acceptance_aux(acc, in, pos, onlyneg, both, base); + pos -= in[pos].size; + while (sub < pos) + { + --pos; + c.append_and(fix_acceptance_aux(acc, in, pos, onlyneg, both, base)); + pos -= in[pos].size; + } + return c; + } + case spot::acc_cond::acc_op::Or: + { + unsigned sub = pos - w.size; + --pos; + auto c = fix_acceptance_aux(acc, in, pos, onlyneg, both, base); + pos -= in[pos].size; + while (sub < pos) + { + --pos; + c.append_or(fix_acceptance_aux(acc, in, pos, onlyneg, both, base)); + pos -= in[pos].size; + } + return c; + } + case spot::acc_cond::acc_op::Inf: + return acc.inf(in[pos - 1].mark); + case spot::acc_cond::acc_op::Fin: + return acc.fin(in[pos - 1].mark); + case spot::acc_cond::acc_op::FinNeg: + { + auto m = in[pos - 1].mark; + auto c = acc.fin(onlyneg & m); + spot::acc_cond::mark_t tmp = 0U; + for (auto i: both.sets()) + { + if (m.has(i)) + tmp.set(base); + ++base; + } + if (tmp) + c.append_or(acc.fin(tmp)); + return c; + } + case spot::acc_cond::acc_op::InfNeg: + { + auto m = in[pos - 1].mark; + auto c = acc.inf(onlyneg & m); + spot::acc_cond::mark_t tmp = 0U; + for (auto i: both.sets()) + { + if (m.has(i)) + tmp.set(base); + ++base; + } + if (tmp) + c.append_and(acc.inf(tmp)); + return c; + } + } + SPOT_UNREACHABLE(); + return {}; +} + static void fix_acceptance(result_& r) { auto& acc = r.h->aut->acc(); - // Compute the unused sets before possibly adding some below. - auto unused = acc.comp(r.neg_acc_sets | r.pos_acc_sets); // If a set x appears only as Inf(!x), we can complement it so that // we work with Inf(x) instead. - if (auto onlyneg = r.neg_acc_sets - r.pos_acc_sets) - for (auto& t: r.h->aut->transition_vector()) - t.acc ^= onlyneg; + auto onlyneg = r.neg_acc_sets - r.pos_acc_sets; + if (onlyneg) + { + for (auto& t: r.h->aut->transition_vector()) + t.acc ^= onlyneg; + } // However if set x is used elsewhere, for instance in // Inf(!x) & Inf(x) // complementing x would be wrong. We need to create a // new set, y, that is the complement of x, and rewrite // this as Inf(y) & Inf(x). - if (auto both = r.neg_acc_sets & r.pos_acc_sets) + auto both = r.neg_acc_sets & r.pos_acc_sets; + unsigned base = 0; + if (both) { auto v = acc.sets(both); auto vs = v.size(); - unsigned base = acc.add_sets(vs); + base = acc.add_sets(vs); for (auto& t: r.h->aut->transition_vector()) if ((t.acc & both) != both) for (unsigned i = 0; i < vs; ++i) @@ -1409,15 +1526,13 @@ static void fix_acceptance(result_& r) t.acc |= acc.mark(base + i); } - // Remove all acceptance sets that are not used in the acceptance - // condition. Because the rest of the code still assume that all - // acceptance sets have to be seen. See - // https://github.com/adl/hoaf/issues/36 - if (unused) + if (onlyneg || both) { - for (auto& t: r.h->aut->transition_vector()) - t.acc = acc.strip(t.acc, unused); - r.h->aut->set_acceptance_conditions(acc.num_sets() - unused.count()); + auto& acc = r.h->aut->acc(); + auto code = acc.get_acceptance(); + r.h->aut->set_acceptance(acc.num_sets(), + fix_acceptance_aux(acc, code, code.size() - 1, + onlyneg, both, base)); } } diff --git a/src/ta/taexplicit.cc b/src/ta/taexplicit.cc index 93b2bdc24..eaed7c432 100644 --- a/src/ta/taexplicit.cc +++ b/src/ta/taexplicit.cc @@ -359,6 +359,7 @@ namespace spot { get_dict()->register_all_variables_of(&tgba_, this); acc().add_sets(n_acc); + acc().set_generalized_buchi(); if (artificial_initial_state != 0) { state_ta_explicit* is = add_state(artificial_initial_state); diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index 12f36f7a0..1133ca9a7 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -41,6 +41,7 @@ tgba_HEADERS = \ noinst_LTLIBRARIES = libtgba.la libtgba_la_SOURCES = \ + acc.cc \ bdddict.cc \ bddprint.cc \ formula2bdd.cc \ diff --git a/src/tgba/acc.cc b/src/tgba/acc.cc new file mode 100644 index 000000000..2c02a83c4 --- /dev/null +++ b/src/tgba/acc.cc @@ -0,0 +1,238 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2015 Laboratoire de Recherche et Développement de +// l'Epita. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 3 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with this program. If not, see . + + +#include +#include "acc.hh" + +namespace spot +{ + std::ostream& operator<<(std::ostream& os, spot::acc_cond::mark_t m) + { + auto a = m.id; + os << '{'; + unsigned level = 0; + const char* comma = ""; + while (a) + { + if (a & 1) + { + os << comma << level; + comma = ","; + } + a >>= 1; + ++level; + } + os << '}'; + return os; + } + + namespace + { + static void + print_code(std::ostream& os, + const acc_cond::acc_code& code, unsigned pos) + { + const char* op = " | "; + auto& w = code[pos]; + const char* negated = ""; + bool top = pos == code.size() - 1; + switch (w.op) + { + case acc_cond::acc_op::And: + op = " & "; + case acc_cond::acc_op::Or: + { + unsigned sub = pos - w.size; + if (!top) + os << '('; + bool first = true; + while (sub < pos) + { + --pos; + if (first) + first = false; + else + os << op; + print_code(os, code, pos); + pos -= code[pos].size; + } + if (!top) + os << ')'; + } + break; + case acc_cond::acc_op::InfNeg: + negated = "!"; + case acc_cond::acc_op::Inf: + { + auto a = code[pos - 1].mark.id; + if (a == 0U) + { + os << 't'; + } + else + { + unsigned level = 0; + const char* and_ = ""; + if (!top) + os << '('; + while (a) + { + if (a & 1) + { + os << and_ << "Inf(" << negated << level << ')'; + and_ = "&"; + } + a >>= 1; + ++level; + } + if (!top) + os << ')'; + } + } + break; + case acc_cond::acc_op::FinNeg: + negated = "!"; + case acc_cond::acc_op::Fin: + { + auto a = code[pos - 1].mark.id; + if (a == 0U) + { + os << 'f'; + } + else + { + unsigned level = 0; + const char* or_ = ""; + if (!top) + os << '('; + while (a) + { + if (a & 1) + { + os << or_ << "Fin(" << negated << level << ')'; + or_ = "|"; + } + a >>= 1; + ++level; + } + if (!top) + os << ')'; + } + } + break; + } + } + + + static bool + eval(acc_cond::mark_t inf, acc_cond::mark_t fin, + const acc_cond::acc_code& code, unsigned pos) + { + auto& w = code[pos]; + switch (w.op) + { + case acc_cond::acc_op::And: + { + unsigned sub = pos - w.size; + while (sub < pos) + { + --pos; + if (!eval(inf, fin, code, pos)) + return false; + pos -= code[pos].size; + } + return true; + } + case acc_cond::acc_op::Or: + { + unsigned sub = pos - w.size; + while (sub < pos) + { + --pos; + if (eval(inf, fin, code, pos)) + return true; + pos -= code[pos].size; + } + return false; + } + case acc_cond::acc_op::Inf: + return (code[pos - 1].mark & inf) == code[pos - 1].mark; + case acc_cond::acc_op::Fin: + return (code[pos - 1].mark & fin) != 0U; + case acc_cond::acc_op::FinNeg: + case acc_cond::acc_op::InfNeg: + SPOT_UNREACHABLE(); + } + SPOT_UNREACHABLE(); + return false; + } + } + + bool acc_cond::accepting(mark_t inf, mark_t fin) const + { + if (code_.empty()) + return true; + return eval(inf, fin, code_, code_.size() - 1); + } + + bool acc_cond::accepting(mark_t inf) const + { + if (uses_fin_acceptance()) + throw std::runtime_error + ("Fin acceptance is not supported by this code path."); + return accepting(inf, 0U); + } + + bool acc_cond::check_fin_acceptance() const + { + if (code_.empty()) + return false; + unsigned pos = code_.size(); + do + { + switch (code_[pos - 1].op) + { + case acc_cond::acc_op::And: + case acc_cond::acc_op::Or: + --pos; + break; + case acc_cond::acc_op::Inf: + case acc_cond::acc_op::InfNeg: + pos -= 2; + break; + case acc_cond::acc_op::Fin: + case acc_cond::acc_op::FinNeg: + return true; + } + } + while (pos > 0); + return false; + } + + std::ostream& operator<<(std::ostream& os, + const spot::acc_cond::acc_code& code) + { + if (code.empty()) + os << 't'; + else + print_code(os, code, code.size() - 1); + return os; + } +} diff --git a/src/tgba/acc.hh b/src/tgba/acc.hh index c7fbf35a6..3dd56361d 100644 --- a/src/tgba/acc.hh +++ b/src/tgba/acc.hh @@ -25,10 +25,11 @@ # include # include # include "ltlenv/defaultenv.hh" +# include namespace spot { - class acc_cond + class SPOT_API acc_cond { public: struct mark_t @@ -90,7 +91,6 @@ namespace spot return id != 0; } - bool has(unsigned u) const { return id & (1U << u); @@ -170,25 +170,142 @@ namespace spot return *this; } - friend std::ostream& operator<<(std::ostream& os, mark_t m) + template + void fill(iterator here) const { - auto a = m.id; - os << '{'; + auto a = id; unsigned level = 0; - const char* comma = ""; while (a) { if (a & 1) - { - os << comma << level; - comma = ","; - } - a >>= 1; + *here++ = level; ++level; + a >>= 1; } - os << '}'; - return os; } + + // FIXME: Return some iterable object without building a vector. + std::vector sets() const + { + std::vector res; + fill(std::back_inserter(res)); + return res; + } + + SPOT_API + friend std::ostream& operator<<(std::ostream& os, mark_t m); + }; + + // This encodes either an operator or set of acceptance sets. + enum class acc_op : unsigned char + { Inf, Fin, InfNeg, FinNeg, And, Or }; + union acc_word + { + mark_t mark; + struct { + acc_op op; // Operator + unsigned char size; // Size of the subtree (number of acc_word), + // not counting this node. + }; + }; + + struct acc_code: public std::vector + { + bool is_true() const + { + unsigned s = size(); + return s == 0 + || ((*this)[s - 1].op == acc_op::Inf && (*this)[s - 2].mark == 0U); + } + + bool is_false() const + { + unsigned s = size(); + return s > 1 + && (*this)[s - 1].op == acc_op::Fin && (*this)[s - 2].mark == 0U; + } + + void append_and(acc_code&& r) + { + if (is_true() || r.is_false()) + { + *this = std::move(r); + return; + } + if (is_false() || r.is_true()) + return; + unsigned s = size() - 1; + unsigned rs = r.size() - 1; + // Inf(a) & Inf(b) = Inf(a & b) + if (((*this)[s].op == acc_op::Inf && r[rs].op == acc_op::Inf) + || ((*this)[s].op == acc_op::InfNeg && r[rs].op == acc_op::InfNeg)) + { + (*this)[s - 1].mark |= r[rs - 1].mark; + return; + } + if ((*this)[s].op == acc_op::And) + pop_back(); + insert(this->end(), r.begin(), r.end()); + acc_word w; + w.op = acc_op::And; + w.size = size(); + push_back(w); + } + + void append_or(acc_code&& r) + { + if (is_true() || r.is_false()) + return; + if (is_false() || r.is_true()) + { + *this = std::move(r); + return; + } + unsigned s = size() - 1; + unsigned rs = r.size() - 1; + // Fin(a) | Fin(b) = Fin(a | b) + if (((*this)[s].op == acc_op::Fin && r[rs].op == acc_op::Fin) + || ((*this)[s].op == acc_op::FinNeg && r[rs].op == acc_op::FinNeg)) + { + (*this)[s - 1].mark |= r[rs - 1].mark; + return; + } + if ((*this)[s].op == acc_op::Or) + pop_back(); + insert(this->end(), r.begin(), r.end()); + acc_word w; + w.op = acc_op::Or; + w.size = size(); + push_back(w); + } + + void shift_left(unsigned sets) + { + if (empty()) + return; + unsigned pos = size(); + do + { + switch ((*this)[pos - 1].op) + { + case acc_cond::acc_op::And: + case acc_cond::acc_op::Or: + --pos; + break; + case acc_cond::acc_op::Inf: + case acc_cond::acc_op::InfNeg: + case acc_cond::acc_op::Fin: + case acc_cond::acc_op::FinNeg: + pos -= 2; + (*this)[pos].mark.id <<= sets; + break; + } + } + while (pos > 0); + } + + SPOT_API + friend std::ostream& operator<<(std::ostream& os, const acc_code& code); }; acc_cond(unsigned n_sets = 0) @@ -198,7 +315,7 @@ namespace spot } acc_cond(const acc_cond& o) - : num_(o.num_), all_(o.all_) + : num_(o.num_), all_(o.all_), code_(o.code_) { } @@ -206,6 +323,91 @@ namespace spot { } + void set_acceptance(const acc_code& code) + { + code_ = code; + uses_fin_acceptance_ = check_fin_acceptance(); + } + + acc_code get_acceptance() const + { + return code_; + } + + bool uses_fin_acceptance() const + { + return uses_fin_acceptance_; + } + + void set_generalized_buchi() + { + set_acceptance(inf(all_sets())); + } + + bool is_generalized_buchi() const + { + unsigned s = code_.size(); + return (s == 0 && num_ == 0) || + (s == 2 && code_[1].op == acc_op::Inf && code_[0].mark == all_sets()); + } + + protected: + bool check_fin_acceptance() const; + + acc_code primitive(mark_t mark, acc_op op) const + { + acc_word w1; + w1.mark = mark; + acc_word w2; + w2.op = op; + w2.size = 1; + acc_code c; + c.push_back(w1); + c.push_back(w2); + return c; + } + + public: + acc_code inf(mark_t mark) const + { + return primitive(mark, acc_op::Inf); + } + + acc_code inf(std::initializer_list vals) const + { + return inf(marks(vals.begin(), vals.end())); + } + + acc_code inf_neg(mark_t mark) const + { + return primitive(mark, acc_op::InfNeg); + } + + acc_code inf_neg(std::initializer_list vals) const + { + return inf_neg(marks(vals.begin(), vals.end())); + } + + acc_code fin(mark_t mark) const + { + return primitive(mark, acc_op::Fin); + } + + acc_code fin(std::initializer_list vals) const + { + return fin(marks(vals.begin(), vals.end())); + } + + acc_code fin_neg(mark_t mark) const + { + return primitive(mark, acc_op::FinNeg); + } + + acc_code fin_neg(std::initializer_list vals) const + { + return fin_neg(marks(vals.begin(), vals.end())); + } + unsigned add_sets(unsigned num) { if (num == 0) @@ -225,7 +427,7 @@ namespace spot mark_t mark(unsigned u) const { - return out(mark_(u)); + return mark_(u); } template @@ -234,7 +436,7 @@ namespace spot mark_t::value_t res = 0U; for (iterator i = begin; i != end; ++i) res |= mark_(*i); - return out(res); + return res; } mark_t marks(std::initializer_list vals) const @@ -242,27 +444,10 @@ namespace spot return marks(vals.begin(), vals.end()); } - template - void fill_from(mark_t m, iterator here) const - { - auto a = in(m); - unsigned level = 0; - while (a) - { - if (a & 1) - *here++ = level; - ++level; - a >>= 1; - } - assert(level <= num_sets()); - } - // FIXME: Return some iterable object without building a vector. std::vector sets(mark_t m) const { - std::vector res; - fill_from(m, std::back_inserter(res)); - return res; + return m.sets(); } // whether m contains u @@ -290,47 +475,27 @@ namespace spot const acc_cond& ra, mark_t rm) const { assert(la.num_sets() + ra.num_sets() == num_sets()); - return la.in(lm) | (ra.in(rm) << la.num_sets()); + (void)ra; + return lm.id | (rm.id << la.num_sets()); } mark_t comp(mark_t l) const { - return out(all_ ^ in(l)); + return all_ ^ l.id; } mark_t all_sets() const { - return out(all_); + return all_; } - bool accepting(mark_t inf) const - { - return in(inf) == all_; - } + bool accepting(mark_t inf, mark_t fin) const; - std::ostream& format_quoted(std::ostream& os, mark_t m) const - { - auto a = in(m); - if (a == 0U) - return os; - unsigned level = 0; - const char* space = ""; - while (a) - { - if (a & 1) - { - os << space << '"' << level << '"'; - space = " "; - } - a >>= 1; - ++level; - } - return os; - } + bool accepting(mark_t inf) const; std::ostream& format(std::ostream& os, mark_t m) const { - auto a = in(m); + auto a = m; if (a == 0U) return os; return os << m; @@ -360,7 +525,7 @@ namespace spot unsigned all = all_ ^ (u | (1 << x)); for (iterator y = begin; y != end; ++y) { - auto v = in(*y); + auto v = y->id; if (v & (1 << x)) { all &= v; @@ -370,7 +535,7 @@ namespace spot } u |= all; } - return out(u); + return u; } mark_t strip(mark_t x, mark_t y) const @@ -381,8 +546,8 @@ namespace spot // == 10 1 11 100 // == 10111100 - auto xv = in(x); // 100101110100 - auto yv = in(y); // 001011001000 + auto xv = x.id; // 100101110100 + auto yv = y.id; // 001011001000 while (yv && xv) { @@ -394,7 +559,7 @@ namespace spot yv = (yv & lm) >> 1; } - return out(xv); + return xv; } protected: @@ -411,18 +576,10 @@ namespace spot return -1U >> (8 * sizeof(mark_t::value_t) - num_); } - mark_t::value_t in(mark_t m) const - { - return m.id; - } - - mark_t out(mark_t::value_t r) const - { - return r; - } - unsigned num_; mark_t::value_t all_; + acc_code code_; + bool uses_fin_acceptance_ = false; }; } diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh index 37d4b2503..fb92326b1 100644 --- a/src/tgba/tgba.hh +++ b/src/tgba/tgba.hh @@ -638,6 +638,25 @@ namespace spot protected: acc_cond acc_; + public: + auto get_acceptance() const + SPOT_RETURN(acc_.get_acceptance()); + + void set_acceptance(unsigned num, const acc_cond::acc_code& c) + { + if (num < acc_.num_sets()) + { + acc_.~acc_cond(); + new (&acc_) acc_cond; + } + acc_.add_sets(num - acc_.num_sets()); + acc_.set_acceptance(c); + prop_single_acc_set(!acc_.uses_fin_acceptance() && num == 1); + if (num == 0) + prop_state_based_acc(); + } + + protected: /// Do the actual computation of tgba::support_conditions(). virtual bdd compute_support_conditions(const state* state) const = 0; mutable const state* last_support_conditions_input_; diff --git a/src/tgba/tgbagraph.hh b/src/tgba/tgbagraph.hh index b08e84978..b22fa10f4 100644 --- a/src/tgba/tgbagraph.hh +++ b/src/tgba/tgbagraph.hh @@ -334,6 +334,7 @@ namespace spot return g_.trans_data(t); } + // FIXME: Should be renamed as set_generalized_buchi() void set_acceptance_conditions(unsigned num) { if (num < acc_.num_sets()) @@ -342,9 +343,10 @@ namespace spot new (&acc_) acc_cond; } acc_.add_sets(num - acc_.num_sets()); - prop_single_acc_set(num == 1); + prop_single_acc_set(!acc_.uses_fin_acceptance() && num == 1); if (num == 0) prop_state_based_acc(); + acc_.set_generalized_buchi(); } acc_cond::mark_t set_single_acceptance_set() @@ -429,7 +431,12 @@ namespace spot /// \brief Copy the acceptance conditions of another tgba. void copy_acceptance_conditions_of(const const_tgba_ptr& a) { - set_acceptance_conditions(a->acc().num_sets()); + // FIXME: Should rename as copy_acceptance_condition*_of + acc_ = a->acc(); + unsigned num = acc_.num_sets(); + prop_single_acc_set(!acc_.uses_fin_acceptance() && num == 1); + if (num == 0) + prop_state_based_acc(); } void copy_ap_of(const const_tgba_ptr& a) diff --git a/src/tgba/tgbaproduct.cc b/src/tgba/tgbaproduct.cc index 6af31f0bd..f8adacb18 100644 --- a/src/tgba/tgbaproduct.cc +++ b/src/tgba/tgbaproduct.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2012, 2014 Laboratoire de Recherche et +// Copyright (C) 2009, 2011, 2012, 2014, 2015 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -311,7 +311,11 @@ namespace spot d->register_all_propositions_of(&right_, this); assert(acc_.num_sets() == 0); - acc_.add_sets(left->acc().num_sets() + right->acc().num_sets()); + auto left_num = left->acc().num_sets(); + auto right_acc = right->get_acceptance(); + right_acc.shift_left(left_num); + right_acc.append_and(left->get_acceptance()); + set_acceptance(left_num + right->acc().num_sets(), right_acc); } tgba_product::~tgba_product() diff --git a/src/tgba/tgbasafracomplement.cc b/src/tgba/tgbasafracomplement.cc index b0838fb95..35d2f7e28 100644 --- a/src/tgba/tgbasafracomplement.cc +++ b/src/tgba/tgbasafracomplement.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de -// Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire +// de Recherche et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -1091,6 +1091,7 @@ namespace spot for (unsigned i = 0; i < nb_acc; ++i) acceptance_cond_vec_.push_back(acc_.mark(acc_.add_set())); #endif + acc_.set_generalized_buchi(); } tgba_safra_complement::~tgba_safra_complement() diff --git a/src/tgbaalgos/degen.cc b/src/tgbaalgos/degen.cc index f5d99330e..712d0c030 100644 --- a/src/tgbaalgos/degen.cc +++ b/src/tgbaalgos/degen.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -128,13 +128,12 @@ namespace spot public: unsigned - next_level(const acc_cond& acc, int slevel, - acc_cond::mark_t set, bool skip_levels) + next_level(int slevel, acc_cond::mark_t set, bool skip_levels) { // Update the order with any new set we discover if (auto newsets = set - found_) { - acc.fill_from(newsets, std::back_inserter(order_)); + newsets.fill(std::back_inserter(order_)); found_ |= newsets; } @@ -161,20 +160,19 @@ namespace spot // Accepting order for each SCC class scc_orders { - const acc_cond& acc_; std::map orders_; bool skip_levels_; public: - scc_orders(const acc_cond& acc, bool skip_levels): - acc_(acc), skip_levels_(skip_levels) + scc_orders(bool skip_levels): + skip_levels_(skip_levels) { } unsigned next_level(int scc, int slevel, acc_cond::mark_t set) { - return orders_[scc].next_level(acc_, slevel, set, skip_levels_); + return orders_[scc].next_level(slevel, set, skip_levels_); } void @@ -226,7 +224,7 @@ namespace spot } // Initialize scc_orders - scc_orders orders(a->acc(), skip_levels); + scc_orders orders(skip_levels); // and vice-versa. ds2num_map ds2num; diff --git a/src/tgbaalgos/hoa.cc b/src/tgbaalgos/hoa.cc index e4b7c427c..d1285a821 100644 --- a/src/tgbaalgos/hoa.cc +++ b/src/tgbaalgos/hoa.cc @@ -252,25 +252,18 @@ namespace spot } os << nl; unsigned num_acc = aut->acc().num_sets(); - if (num_acc == 0) - os << "acc-name: all"; - else if (num_acc == 1) - os << "acc-name: Buchi"; - else - os << "acc-name: generalized-Buchi " << num_acc; - os << nl; - os << "Acceptance: " << num_acc; - if (num_acc > 0) + if (aut->acc().is_generalized_buchi()) { - os << " Inf(0"; - for (unsigned i = 1; i < num_acc; ++i) - os << ")&Inf(" << i; - os << ')'; - } - else - { - os << " t"; + if (num_acc == 0) + os << "acc-name: all"; + else if (num_acc == 1) + os << "acc-name: Buchi"; + else + os << "acc-name: generalized-Buchi " << num_acc; + os << nl; } + os << "Acceptance: " << num_acc << ' '; + os << aut->acc().get_acceptance(); os << nl; os << "properties: trans-labels explicit-labels"; if (acceptance == Hoa_Acceptance_States) diff --git a/src/tgbaalgos/ltl2taa.cc b/src/tgbaalgos/ltl2taa.cc index 01ce00ac4..09c2d60df 100644 --- a/src/tgbaalgos/ltl2taa.cc +++ b/src/tgbaalgos/ltl2taa.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2012, 2013, 2014 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2012, 2013, 2014, 2015 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -423,6 +423,7 @@ namespace spot auto taa = v.result(); // Careful: before the destroy! f2->destroy(); delete lcc; + taa->acc().set_generalized_buchi(); return taa; } } diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index cd838df5f..cd0bebef3 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -2505,10 +2505,14 @@ namespace spot dict->register_propositions(fc.used_vars(), a); + auto& acc = a->acc(); + unsigned ns = a->num_states(); for (unsigned s = 0; s < ns; ++s) for (auto& t: a->out(s)) - t.acc = a->acc().comp(t.acc); + t.acc = acc.comp(t.acc); + + acc.set_generalized_buchi(); if (!simplifier) // This should not be deleted before we have registered all propositions. diff --git a/src/tgbaalgos/product.cc b/src/tgbaalgos/product.cc index 3f6f21f24..83291ac1c 100644 --- a/src/tgbaalgos/product.cc +++ b/src/tgbaalgos/product.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014 Laboratoire de Recherche et +// Copyright (C) 2014, 2015 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -52,8 +52,11 @@ namespace spot auto res = make_tgba_digraph(left->get_dict()); res->copy_ap_of(left); res->copy_ap_of(right); - res->set_acceptance_conditions(left->acc().num_sets() - + right->acc().num_sets()); + auto left_num = left->acc().num_sets(); + auto right_acc = right->get_acceptance(); + right_acc.shift_left(left_num); + right_acc.append_and(left->get_acceptance()); + res->set_acceptance(left_num + right->acc().num_sets(), right_acc); auto v = new product_states; res->set_named_prop("product-states", v); diff --git a/src/tgbaalgos/stutter.cc b/src/tgbaalgos/stutter.cc index 658a651fc..6d9be18b4 100644 --- a/src/tgbaalgos/stutter.cc +++ b/src/tgbaalgos/stutter.cc @@ -210,6 +210,7 @@ namespace spot get_dict()->register_all_propositions_of(&a_, this); assert(acc_.num_sets() == 0); acc_.add_sets(a_->acc().num_sets()); + acc_.set_generalized_buchi(); } virtual ~tgbasl() diff --git a/src/tgbatest/acc.cc b/src/tgbatest/acc.cc index 1bc97e565..37d12b116 100644 --- a/src/tgbatest/acc.cc +++ b/src/tgbatest/acc.cc @@ -37,6 +37,8 @@ void check(spot::acc_cond& ac, spot::acc_cond::mark_t m) int main() { spot::acc_cond ac(4); + ac.set_generalized_buchi(); + std::cout << ac.get_acceptance() << '\n'; auto m1 = ac.marks({0, 2}); auto m2 = ac.marks({0, 3}); @@ -50,6 +52,7 @@ int main() check(ac, m1 | m2 | m3); ac.add_set(); + ac.set_generalized_buchi(); check(ac, m1); check(ac, m2); @@ -62,9 +65,11 @@ int main() check(ac, ac.comp(m2 & m3)); spot::acc_cond ac2(ac.num_sets()); + ac2.set_generalized_buchi(); check(ac2, m3); spot::acc_cond ac3(ac.num_sets() + ac2.num_sets()); + ac3.set_generalized_buchi(); std::cout << ac.num_sets() << " + " << ac2.num_sets() << " = " << ac3.num_sets() << '\n'; auto m5 = ac3.join(ac, m2, ac2, m3); @@ -74,10 +79,8 @@ int main() auto m7 = ac3.join(ac, ac.comp(m2 & m3), ac2, ac2.all_sets()); check(ac3, m7); - std::vector v; - ac3.fill_from(m7, std::back_inserter(v)); const char* comma = ""; - for (auto i: v) + for (auto i: m7.sets()) { std::cout << comma << i; comma = ","; @@ -85,6 +88,7 @@ int main() std::cout << '\n'; spot::acc_cond ac4; + ac4.set_generalized_buchi(); check(ac4, ac4.all_sets()); check(ac4, ac4.comp(ac4.all_sets())); @@ -102,4 +106,17 @@ int main() check(ac, ac.strip(v, u)); } + + auto code1 = ac.inf({0, 1, 3}); + std::cout << code1.size() << ' ' << code1 << '\n'; + code1.append_or(ac.fin({2})); + std::cout << code1.size() << ' ' << code1 << '\n'; + code1.append_or(ac.fin({0})); + std::cout << code1.size() << ' ' << code1 << '\n'; + code1.append_or(ac.fin({})); + std::cout << code1.size() << ' ' << code1 << '\n'; + code1.append_and(ac.inf({})); + std::cout << code1.size() << ' ' << code1 << '\n'; + code1.append_and(ac.fin({})); + std::cout << code1.size() << ' ' << code1 << '\n'; } diff --git a/src/tgbatest/acc.test b/src/tgbatest/acc.test index 96df71f8c..bab703707 100755 --- a/src/tgbatest/acc.test +++ b/src/tgbatest/acc.test @@ -24,6 +24,7 @@ set -e cat >expect <input < output -# 0 -> 0 -# 1 -> removed -# 2 -> 1 -# 3 -> removed -# 4 -> 2 -# !2 -> 3 -expectok input < output +# # 0 -> 0 +# # 1 -> removed +# # 2 -> 1 +# # 3 -> removed +# # 4 -> 2 +# # !2 -> 3 +# expectok input <