diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc index 3120c7bcb..b36aadef5 100644 --- a/src/bin/dstar2tgba.cc +++ b/src/bin/dstar2tgba.cc @@ -37,6 +37,7 @@ #include "twaalgos/hoa.hh" #include "twaalgos/neverclaim.hh" #include "twaalgos/stats.hh" +#include "twaalgos/totgba.hh" #include "twa/bddprint.hh" #include "misc/optionmap.hh" #include "misc/timer.hh" @@ -290,7 +291,7 @@ namespace } if (has('A')) - daut_acc_ = daut->accpair_count; + daut_acc_ = daut->aut->num_sets() / 2; if (has('C')) daut_scc_ = spot::scc_info(daut->aut).scc_count(); @@ -355,7 +356,7 @@ namespace spot::stopwatch sw; sw.start(); - auto nba = spot::dstar_to_tgba(daut); + auto nba = spot::to_generalized_buchi(daut->aut); auto aut = post.run(nba, 0); const double conversion_time = sw.stop(); diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index 90496d3b7..46e8bedbf 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -620,14 +620,14 @@ namespace st->in_states= s.states; st->in_edges = s.transitions; st->in_transitions = s.sub_transitions; - st->in_acc = aut->accpair_count; + st->in_acc = aut->aut->num_sets() / 2; st->in_scc = spot::scc_info(aut->aut).scc_count(); } // convert it into TGBA for further processing if (verbose) std::cerr << "info: converting " << type << " to TGBA\n"; - res = dstar_to_tgba(aut); + res = remove_fin(aut->aut); } break; } diff --git a/src/bin/ltldo.cc b/src/bin/ltldo.cc index 362a4da8e..7bb0b3e7b 100644 --- a/src/bin/ltldo.cc +++ b/src/bin/ltldo.cc @@ -40,6 +40,7 @@ #include "misc/timer.hh" #include "twaalgos/lbtt.hh" #include "twaalgos/relabel.hh" +#include "twaalgos/totgba.hh" #include "parseaut/public.hh" #include "dstarparse/public.hh" @@ -185,7 +186,7 @@ namespace } else { - res = dstar_to_tgba(aut); + res = aut->aut; } break; } diff --git a/src/dstarparse/Makefile.am b/src/dstarparse/Makefile.am index e739ba636..264553cb8 100644 --- a/src/dstarparse/Makefile.am +++ b/src/dstarparse/Makefile.am @@ -1,6 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2013 Laboratoire de Recherche et Développement de -## l'Epita (LRDE). +## Copyright (C) 2013, 2015 Laboratoire de Recherche et Développement +## de l'Epita (LRDE). ## ## This file is part of Spot, a model checking library. ## @@ -52,10 +52,6 @@ EXTRA_DIST = $(DSTARPARSE_YY) libdstarparse_la_SOURCES = \ fmterror.cc \ - dra2ba.cc \ - dstar2tgba.cc \ - nra2nba.cc \ - nsa2tgba.cc \ $(FROM_DSTARPARSE_YY) \ dstarscan.ll \ parsedecl.hh diff --git a/src/dstarparse/dra2ba.cc b/src/dstarparse/dra2ba.cc deleted file mode 100644 index fc718d038..000000000 --- a/src/dstarparse/dra2ba.cc +++ /dev/null @@ -1,352 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// -// 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 "public.hh" -#include "twa/twamask.hh" -#include "twaalgos/scc.hh" -#include "twaalgos/reachiter.hh" -#include "twaalgos/gtec/gtec.hh" -#include "twaalgos/sccfilter.hh" -#include "twaalgos/dot.hh" - -namespace spot -{ - - // IMPORTANT NOTE: If you attempt to follow Krishnan et - // al. (ISAAC'94) paper while reading this code, make sure you - // understand the difference between their Rabin acceptance - // definition and the one we are using. - // - // Here, a cycle is accepting in a Rabin automaton if there exists - // an acceptance pair (Lᵢ, Uᵢ) such that some states from Lᵢ are - // visited while no states from Uᵢ are visited. This is the - // same definition used by ltl2dstar. - // - // In the Krishnan et al. paper, a cycle is accepting in a Rabin - // automaton if there exists an acceptance pair (Lᵢ, Uᵢ) such that - // some states from Lᵢ are visited and all visited states belongs to - // Uᵢ. In other words, you can switch from one definition to - // the other by complementing the Uᵢ set. - // - // This is a source of confusion; you have been warned. - - - // This function is defined in nra2nba.cc, and used only here. - SPOT_LOCAL - twa_graph_ptr nra_to_nba(const const_dstar_aut_ptr& nra, - const const_twa_ptr& aut); - - namespace - { - typedef std::list state_list; - - // The functions that take aut and dra as first arguments are - // either called on the main automaton, in which case dra->aut == - // aut, or it is called on a sub-automaton in which case aut is a - // masked version of dra->aut. So we should always explore the - // automaton aut, but because the state of aut are states of - // dra->aut, we can use dra->aut to get labels, and dra->acccs to - // retrive acceptances. - - static bool - filter_states(const const_twa_ptr& aut, - const const_dstar_aut_ptr& dra, - const state_list& sl, - state_list& final, - state_list& nonfinal); - - static bool - filter_scc(const const_twa_ptr& aut, - const const_dstar_aut_ptr& dra, - state_list& final, - state_list& nonfinal) - { - // Iterate over all non-trivial SCCs. - scc_map sm(aut); - sm.build_map(); - for (unsigned scc_max = sm.scc_count(), scc = 0; - scc < scc_max; ++scc) - { - if (sm.trivial(scc)) - { - nonfinal.push_back(sm.one_state_of(scc)); - continue; - } - - // Get the list of states of that SCC - const std::list& sl = sm.states_of(scc); - assert(!sl.empty()); - if (!filter_states(aut, dra, sl, final, nonfinal)) - return false; - } - return true; - } - - static bool - filter_states(const const_twa_ptr& aut, - const const_dstar_aut_ptr& dra, - const state_list& sl, - state_list& final, - state_list& nonfinal) - { - // Check whether the SCC composed of all states in sl contains - // non-accepting cycles. - // - // A cycle is accepting (in a Rabin automaton) if there exists - // an acceptance pair (Lᵢ, Uᵢ) such that some states from Lᵢ - // are visited while no states from Uᵢ are visited. - // - // Consequently, a cycle is non-accepting if for all acceptance - // pairs (Lᵢ, Uᵢ), either no states from Lᵢ are visited or some - // states from Uᵢ are visited. (This corresponds to an - // accepting cycle with Streett acceptance.) - // - // Now we consider the SCC as one large cycle and check its - // intersection with all Lᵢs and Uᵢs. Let l=[l₁,l₂,...] and - // u=[u₁,u₂,...] be bitvectors where bit lᵢ (resp. uᵢ) - // indicates that Lᵢ (resp. Uᵢ) has been visited in the SCC. - state_list::const_iterator it = sl.begin(); - int num = dra->aut->state_number(*it++); - bitvect* l = dra->accsets->at(num * 2).clone(); - bitvect* u = dra->accsets->at(num * 2 + 1).clone(); - for (; it != sl.end(); ++it) - { - num = dra->aut->state_number(*it); - *l |= dra->accsets->at(num * 2); - *u |= dra->accsets->at(num * 2 + 1); - } - // If we have l&!u = [0,0,...] that means that the cycle formed - // by the entire SCC is not accepting. However that does not - // necessarily imply that all cycles in the SCC are also - // non-accepting. We may have a smaller cycle that is - // accepting, but which becomes non-accepting when extended with - // more states. - *l -= *u; - delete u; - if (l->is_fully_clear()) - { - delete l; - // Check whether the SCC is accepting. We do that by simply - // converting that SCC into a TGBA and running our emptiness - // check. This is not a really smart implementation and - // could be improved. - { - state_set keep(sl.begin(), sl.end()); - auto masked = build_twa_mask_keep(dra->aut, keep, sl.front()); - if (!nra_to_nba(dra, masked)->is_empty()) - // This SCC is not DBA-realizable. - return false; - } - for (state_list::const_iterator i = sl.begin(); - i != sl.end(); ++i) - nonfinal.push_back(*i); - return true; - } - // The bits sets in *l corresponds to Lᵢs that have been seen - // without seeing the matching Uᵢ. In this SCC, any state in Lᵢ - // is therefore final. Otherwise we do not know: it is possible - // that there is a non-accepting cycle in the SCC that do not - // visit Lᵢ. - state_set unknown; - for (it = sl.begin(); it != sl.end(); ++it) - { - num = dra->aut->state_number(*it); - bitvect* l2 = dra->accsets->at(num * 2).clone(); - *l2 &= *l; - if (!l2->is_fully_clear()) - { - final.push_back(*it); - } - else - { - unknown.insert(*it); - } - delete l2; - } - delete l; - // Check whether it is possible to build non-accepting cycles - // using only the "unknown" states. - while (!unknown.empty()) - { - //std::cerr << "unknown\n"; - // Build a sub-automaton for just the unknown states, - // starting from any state in the SCC. - auto scc_mask = build_twa_mask_keep(aut, unknown, *unknown.begin()); - state_list local_final; - state_list local_nonfinal; - bool dbarealizable = - filter_scc(scc_mask, dra, local_final, local_nonfinal); - if (!dbarealizable) - return false; - for (state_list::const_iterator i = local_final.begin(); - i != local_final.end(); ++i) - unknown.erase(*i); - final.splice(final.end(), local_final); - for (state_list::const_iterator i = local_nonfinal.begin(); - i != local_nonfinal.end(); ++i) - unknown.erase(*i); - nonfinal.splice(nonfinal.end(), local_nonfinal); - } - return true; - } - - - - class dra_to_ba_worker: public tgba_reachable_iterator_depth_first - { - public: - dra_to_ba_worker(const const_dstar_aut_ptr& a, - const state_set& final, - const scc_map& sm, - const std::vector& realizable): - tgba_reachable_iterator_depth_first(a->aut), - in_(a), - out_(make_twa_graph(a->aut->get_dict())), - final_(final), - num_states_(a->aut->num_states()), - sm_(sm), - realizable_(realizable) - { - out_->copy_ap_of(a->aut); - out_->prop_state_based_acc(); - acc_ = out_->set_buchi(); - out_->new_states(num_states_ * (a->accpair_count + 1)); - out_->set_init_state(a->aut->get_init_state_number()); - - } - - twa_graph_ptr - result() - { - return out_; - } - - void - process_link(const state* sin, int, - const state* sout, int, - const twa_succ_iterator* si) - { - int in = in_->aut->state_number(sin); - int out = in_->aut->state_number(sout); - unsigned in_scc = sm_.scc_of_state(sin); - - bdd cond = si->current_condition(); - unsigned t = out_->new_edge(in, out, cond); - - if (realizable_[in_scc]) - { - if (final_.find(sin) != final_.end()) - out_->edge_data(t).acc = acc_; - } - else if (sm_.scc_of_state(sout) == in_scc) - { - // Create one clone of the SCC per accepting pair, - // removing states from the Ui part of the (Li, Ui) pairs. - // (Or the Ei part of Löding's (Ei, Fi) pairs.) - bitvect& l = in_->accsets->at(2 * in); - bitvect& u = in_->accsets->at(2 * in + 1); - for (size_t i = 0; i < in_->accpair_count; ++i) - { - int shift = num_states_ * (i + 1); - // In the Ui set. (Löding's Ei set.) - if (!u.get(i)) - { - // Transition t1 is a non-deterministic jump - // from the original automaton to the i-th clone. - // - // Transition t2 constructs the clone. - // - // Löding creates transition t1 regardless of the - // acceptance set. We restrict it to the non-Li - // states. Both his definition and this - // implementation create more transitions than needed: - // we do not need more than one transition per - // accepting cycle. - out_->new_edge(in, out + shift, cond); - - // Acceptance transitions are those in the Li - // set. (Löding's Fi set.) - out_->new_acc_edge(in + shift, out + shift, cond, l.get(i)); - } - } - } - } - - protected: - const const_dstar_aut_ptr& in_; - twa_graph_ptr out_; - const state_set& final_; - size_t num_states_; - acc_cond::mark_t acc_; - const scc_map& sm_; - const std::vector& realizable_; - }; - - } - - - twa_graph_ptr dra_to_ba(const const_dstar_aut_ptr& dra, bool* dba) - { - assert(dra->type == Rabin); - - state_list final; - state_list nonfinal; - - // Iterate over all non-trivial SCCs. - scc_map sm(dra->aut); - sm.build_map(); - unsigned scc_max = sm.scc_count(); - - bool dba_realizable = true; - std::vector realizable(scc_max); - - for (unsigned scc = 0; scc < scc_max; ++scc) - { - if (sm.trivial(scc)) - { - realizable[scc] = true; - continue; - } - - // Get the list of states of that SCC - const std::list& sl = sm.states_of(scc); - assert(!sl.empty()); - bool scc_realizable = filter_states(dra->aut, dra, sl, final, nonfinal); - dba_realizable &= scc_realizable; - realizable[scc] = scc_realizable; - //std::cerr << "realizable[" << scc << "] = " << scc_realizable << '\n'; - } - - if (dba) - *dba = dba_realizable; - - // for (state_list::const_iterator i = final.begin(); - // i != final.end(); ++i) - // std::cerr << dra->aut->get_label(*i) << " is final\n"; - // for (state_list::const_iterator i = nonfinal.begin(); - // i != nonfinal.end(); ++i) - // std::cerr << dra->aut->get_label(*i) << " is non-final\n"; - - state_set fs(final.begin(), final.end()); - dra_to_ba_worker w(dra, fs, sm, realizable); - w.run(); - return scc_filter_states(w.result()); - } - -} diff --git a/src/dstarparse/dstar2tgba.cc b/src/dstarparse/dstar2tgba.cc deleted file mode 100644 index bdb1ec80a..000000000 --- a/src/dstarparse/dstar2tgba.cc +++ /dev/null @@ -1,36 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// -// 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 "public.hh" - -namespace spot -{ - twa_graph_ptr - dstar_to_tgba(const const_dstar_aut_ptr& daut) - { - switch (daut->type) - { - case spot::Rabin: - return dra_to_ba(daut); - case spot::Streett: - return nsa_to_tgba(daut); - } - SPOT_UNREACHABLE(); - } -} diff --git a/src/dstarparse/dstarparse.yy b/src/dstarparse/dstarparse.yy index e8fc0043b..67f7bdc0c 100644 --- a/src/dstarparse/dstarparse.yy +++ b/src/dstarparse/dstarparse.yy @@ -46,9 +46,12 @@ std::vector::const_iterator cur_guard; map_t dest_map; int cur_state; + int plus; + int minus; - unsigned state_count = 0; - unsigned start_state = 0; + unsigned state_count = 0U; + unsigned start_state = 0U; + unsigned accpair_count = 0U; std::vector aps; bool state_count_seen:1; @@ -73,6 +76,7 @@ { std::string* str; unsigned int num; + spot::acc_cond::mark_t acc; } %code @@ -102,6 +106,7 @@ %token NUMBER "number"; %type sign +%type accsigs state_accsig %destructor { delete $$; } %printer { @@ -117,9 +122,18 @@ dstar: header ENDOFHEADER eols states eols : EOL | eols EOL opt_eols: | opt_eols EOL -auttype: DRA { result.d->type = spot::Rabin; } - | DSA { result.d->type = spot::Streett; } - +auttype: DRA + { + result.d->type = spot::Rabin; + result.plus = 1; + result.minus = 0; + } + | DSA + { + result.d->type = spot::Streett; + result.plus = 0; + result.minus = 1; + } header: auttype opt_eols V2 opt_eols EXPLICIT opt_eols sizes { @@ -168,8 +182,12 @@ sizes: } | sizes ACCPAIRS opt_eols NUMBER opt_eols { - result.d->accpair_count = $4; + result.accpair_count = $4; result.accpair_count_seen = true; + result.d->aut->set_acceptance(2 * $4, + result.d->type == spot::Rabin ? + spot::acc_cond::acc_code::rabin($4) : + spot::acc_cond::acc_code::streett($4)); } | sizes STATES opt_eols NUMBER opt_eols { @@ -228,27 +246,30 @@ state_id: STATE opt_eols NUMBER opt_eols opt_name result.cur_state = $3; } -sign: '+' { $$ = 0; } - | '-' { $$ = 1; } +sign: '+' { $$ = result.plus; } + | '-' { $$ = result.minus; } // Membership to a pair is represented as (+NUM,-NUM) accsigs: opt_eols + { + $$ = 0U; + } | accsigs sign NUMBER opt_eols { if ((unsigned) result.cur_state >= result.state_count) break; - assert(result.d->accsets); - if ($3 < result.d->accpair_count) + if ($3 < result.accpair_count) { - result.d->accsets->at(result.cur_state * 2 + $2).set($3); + $$ = $1; + $$.set($3 * 2 + $2); } else { std::ostringstream o; - if (result.d->accpair_count > 0) + if (result.accpair_count > 0) { o << "acceptance pairs should be in the range [0.." - << result.d->accpair_count - 1<< "]"; + << result.accpair_count - 1 << "]"; } else { @@ -258,7 +279,7 @@ accsigs: opt_eols } } -state_accsig: ACCSIG accsigs +state_accsig: ACCSIG accsigs { $$ = $2; } transitions: | transitions NUMBER opt_eols @@ -273,9 +294,8 @@ transitions: states: | states state_id state_accsig transitions { - for (map_t::const_iterator i = result.dest_map.begin(); - i != result.dest_map.end(); ++i) - result.d->aut->new_edge(result.cur_state, i->first, i->second); + for (auto i: result.dest_map) + result.d->aut->new_edge(result.cur_state, i.first, i.second, $3); } %% @@ -301,9 +321,6 @@ static void fill_guards(result_& r) delete[] vars; r.cur_guard = r.guards.end(); - - r.d->accsets = spot::make_bitvect_array(r.d->accpair_count, - 2 * r.state_count); } void @@ -331,14 +348,15 @@ namespace spot result_ r; r.d = std::make_shared(); r.d->aut = make_twa_graph(dict); - r.d->accsets = 0; + r.d->aut->prop_deterministic(true); + r.d->aut->prop_state_based_acc(true); r.env = &env; dstaryy::parser parser(error_list, r); parser.set_debug_level(debug); parser.parse(); dstaryyclose(); - if (!r.d->aut || !r.d->accsets) + if (!r.d->aut) return nullptr; return r.d; } diff --git a/src/dstarparse/nra2nba.cc b/src/dstarparse/nra2nba.cc deleted file mode 100644 index 2c6598e7f..000000000 --- a/src/dstarparse/nra2nba.cc +++ /dev/null @@ -1,131 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). -// -// 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 "public.hh" -#include "twaalgos/reachiter.hh" -#include "twaalgos/sccfilter.hh" - -namespace spot -{ - namespace - { - // Christof Löding's Diploma Thesis: Methods for the - // Transformation of ω-Automata: Complexity and Connection to - // Second Order Logic. Section 3.4.3: Rabin to Büchi. - // - // However beware that the {...,(Ei,Fi),...} pairs used by Löding - // are reversed compared to the {...,(Li,Ui),...} pairs used by - // several other people. We have Ei=Ui and Fi=Li. - class nra_to_nba_worker: public tgba_reachable_iterator_depth_first - { - public: - // AUT is the automaton we iterate on, while A is the automaton - // we read the acceptance conditions from. Separating the two - // makes its possible to mask AUT, as needed in dra_to_ba(). - nra_to_nba_worker(const const_dstar_aut_ptr& a, const_twa_ptr aut): - tgba_reachable_iterator_depth_first(aut), - out_(make_twa_graph(aut->get_dict())), - d_(a), - num_states_(a->aut->num_states()) - { - out_->copy_ap_of(aut); - out_->set_buchi(); - out_->prop_state_based_acc(); - out_->new_states(num_states_ * (d_->accpair_count + 1)); - // This converts the initial state of aut (not a->aut) into a - // state number in a->aut. - auto i = aut->get_init_state(); - out_->set_init_state(a->aut->state_number(i)); - i->destroy(); - } - - twa_graph_ptr - result() - { - return out_; - } - - void - process_link(const state* sin, int, - const state* sout, int, - const twa_succ_iterator* si) - { - int in = d_->aut->state_number(sin); - int out = d_->aut->state_number(sout); - - bdd cond = si->current_condition(); - out_->new_edge(in, out, cond); - - // Create one clone of the automaton per accepting pair, - // removing states from the Ui part of the (Li, Ui) pairs. - // (Or the Ei part of Löding's (Ei, Fi) pairs.) - bitvect& l = d_->accsets->at(2 * in); - bitvect& u = d_->accsets->at(2 * in + 1); - for (size_t i = 0; i < d_->accpair_count; ++i) - { - int shift = num_states_ * (i + 1); - // In the Ui set. (Löding's Ei set.) - if (!u.get(i)) - { - // Transition t1 is a non-deterministic jump - // from the original automaton to the i-th clone. - // - // Transition t2 constructs the clone. - // - // Löding creates transition t1 regardless of the - // acceptance set. We restrict it to the non-Li - // states. Both his definition and this - // implementation create more transitions than needed: - // we do not need more than one transition per - // accepting cycle. - out_->new_edge(in, out + shift, cond); - - // A transition is accepting if it is in the Li - // set. (Löding's Fi set.) - out_->new_acc_edge(in + shift, out + shift, cond, l.get(i)); - } - } - } - - protected: - twa_graph_ptr out_; - const_dstar_aut_ptr d_; - size_t num_states_; - }; - - } - - // In dra_to_dba() we call this function with a second argument - // that is a masked version of nra->aut. - SPOT_LOCAL - twa_graph_ptr nra_to_nba(const const_dstar_aut_ptr& nra, - const const_twa_ptr& aut) - { - assert(nra->type == Rabin); - nra_to_nba_worker w(nra, aut); - w.run(); - return scc_filter_states(w.result()); - } - - twa_graph_ptr nra_to_nba(const const_dstar_aut_ptr& nra) - { - return nra_to_nba(nra, nra->aut); - } - -} diff --git a/src/dstarparse/nsa2tgba.cc b/src/dstarparse/nsa2tgba.cc deleted file mode 100644 index 25ab54219..000000000 --- a/src/dstarparse/nsa2tgba.cc +++ /dev/null @@ -1,206 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). -// -// 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 -#include "public.hh" -#include "twaalgos/sccfilter.hh" -#include "ltlenv/defaultenv.hh" -#include "priv/accmap.hh" - -namespace spot -{ - // Christof Löding's Diploma Thesis: Methods for the - // Transformation of ω-Automata: Complexity and Connection to - // Second Order Logic. Section 3.4.3, gives a transition - // from Streett with |Q| states to BA with |Q|*(4^n-3^n+2) - // states, if n is the number of acceptance pairs. - // - // Duret-Lutz et al. (ATVA'2009): On-the-fly Emptiness Check of - // Transition-based Streett Automata. Section 3.3 contains a - // conversion from transition-based Streett Automata to TGBA using - // the generalized Büchi acceptance to limit the explosion. It goes - // from Streett with |Q| states to (T)GBA with |Q|*(2^n+1) states. - // However the definition of the number of acceptance sets in that - // paper is suboptimal: only n are needed, not 2^n. - // - // This implements this second version. - - namespace - { - // A state in the resulting automaton corresponds is either a - // state of the original automaton (in which case bv == 0) or a - // state of the original automaton associated to a set of pending - // acceptance represented by a bitvect. - - struct build_state - { - int s; - const bitvect* pend; - - build_state(int st, const bitvect* bv = 0): - s(st), - pend(bv) - { - } - }; - - struct build_state_hash - { - size_t - operator()(const build_state& s) const - { - if (!s.pend) - return s.s; - else - return s.s ^ s.pend->hash(); - } - }; - - struct build_state_equal - { - bool - operator()(const build_state& left, - const build_state& right) const - { - if (left.s != right.s) - return false; - if (left.pend == right.pend) - return true; - if (!right.pend || !left.pend) - return false; - return *left.pend == *right.pend; - } - }; - - // Associate the build state to its number. - typedef std::unordered_map bs2num_map; - - // Queue of state to be processed. - typedef std::deque queue_t; - - } - - twa_graph_ptr nsa_to_tgba(const const_dstar_aut_ptr& nsa) - { - assert(nsa->type == Streett); - auto a = nsa->aut; - auto res = make_twa_graph(a->get_dict()); - res->copy_ap_of(a); - - // Create accpair_count acceptance sets for the output. - unsigned npairs = nsa->accpair_count; - acc_mapper_consecutive_int acc_b(res, npairs); - - // These maps make it possible to convert build_state to number - // and vice-versa. - bs2num_map bs2num; - - queue_t todo; - - build_state s(a->get_init_state_number()); - bs2num[s] = res->new_state(); - todo.push_back(s); - - while (!todo.empty()) - { - s = todo.front(); - todo.pop_front(); - int src = bs2num[s]; - - for (auto& t: a->out(s.s)) - { - bitvect* pend = 0; - acc_cond::mark_t acc = 0U; - if (s.pend) - { - pend = s.pend->clone(); - *pend |= nsa->accsets->at(2 * t.dst); // L - *pend -= nsa->accsets->at(2 * t.dst + 1); // U - - for (size_t i = 0; i < npairs; ++i) - if (!pend->get(i)) - acc |= acc_b.lookup(i).second; - } - - - build_state d(t.dst, pend); - // Have we already seen this destination? - int dest; - auto dres = bs2num.emplace(d, 0); - if (!dres.second) - { - dest = dres.first->second; - delete d.pend; - } - else // No, this is a new state - { - dest = dres.first->second = res->new_state(); - todo.push_back(d); - } - res->new_edge(src, dest, t.cond, acc); - - // Jump to level ∅ - if (s.pend == 0) - { - bitvect* pend = make_bitvect(npairs); - build_state d(t.dst, pend); - // Have we already seen this destination? - int dest; - auto dres = bs2num.emplace(d, 0); - if (!dres.second) - { - dest = dres.first->second; - delete d.pend; - } - else // No, this is a new state - { - dest = dres.first->second = res->new_state(); - todo.push_back(d); - } - res->new_edge(src, dest, t.cond); - } - } - } - - - // { - // bs2num_map::iterator i = bs2num.begin(); - // while (i != bs2num.end()) - // { - // std::cerr << i->second << ": (" << i->first.s << ','; - // if (i->first.pend) - // std::cerr << *i->first.pend << ")\n"; - // else - // std::cerr << "-)\n"; - // ++i; - // } - // } - - // Cleanup the bs2num map. - bs2num_map::iterator i = bs2num.begin(); - while (i != bs2num.end()) - delete (i++)->first.pend; - - res->acc().set_generalized_buchi(); - return res; - } - -} diff --git a/src/dstarparse/public.hh b/src/dstarparse/public.hh index 69c2c554b..5949d132a 100644 --- a/src/dstarparse/public.hh +++ b/src/dstarparse/public.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement +// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -26,7 +26,6 @@ #include #include #include -#include namespace spot { @@ -49,20 +48,6 @@ namespace spot twa_graph_ptr aut; /// Type of the acceptance. dstar_type type; - /// Number of acceptance pairs. - size_t accpair_count; - /// \brief acceptance sets encoded as 2*num_state bit-vectors of - /// num_pairs bits - /// - /// Assuming F={(L₀,U₀),…,(Lᵢ,Uᵢ),…}, - /// s∈Lᵢ iff accsets->at(s * 2).get(i), - /// s∈Uᵢ iff accsets->at(s * 2 + 1).get(i). - bitvect_array* accsets; - - ~dstar_aut() - { - delete accsets; - } }; typedef std::shared_ptr dstar_aut_ptr; @@ -102,49 +87,5 @@ namespace spot format_dstar_parse_errors(std::ostream& os, const std::string& filename, dstar_parse_error_list& error_list); - - - /// \brief Convert a non-deterministic Rabin automaton into a - /// non-deterministic Büchi automaton. - SPOT_API twa_graph_ptr - nra_to_nba(const const_dstar_aut_ptr& nra); - - /// \brief Convert a non-deterministic Rabin automaton into a - /// non-deterministic Büchi automaton. - /// - /// This version simply ignores all states in \a ignore. - SPOT_API twa_graph_ptr - nra_to_nba(const const_dstar_aut_ptr& nra, const state_set* ignore); - - /// \brief Convert a deterministic Rabin automaton into a - /// Büchi automaton, deterministic when possible. - /// - /// See "Deterministic ω-automata vis-a-vis Deterministic Büchi - /// Automata", S. Krishnan, A. Puri, and R. Brayton (ISAAC'94) for - /// more details about a DRA->DBA construction. - /// - /// We essentially apply this method SCC-wise. If an SCC is - /// DBA-realizable, we duplicate it in the output, fixing just - /// the acceptance states. If an SCC is not DBA-realizable, - /// then we apply the more usual conversion from Rabin to NBA - /// for this part. - /// - /// If the optional \a dba_output argument is non-null, the - /// pointed Boolean will be updated to indicate whether the - /// returned Büchi automaton is deterministic. - SPOT_API twa_graph_ptr - dra_to_ba(const const_dstar_aut_ptr& dra, bool* dba_output = 0); - - /// \brief Convert a non-deterministic Streett automaton into a - /// non-deterministic tgba. - SPOT_API twa_graph_ptr - nsa_to_tgba(const const_dstar_aut_ptr& nra); - - /// \brief Convert a Rabin or Streett automaton into a TGBA. - /// - /// This function calls dra_to_ba() or nsa_to_tgba(). - SPOT_API twa_graph_ptr - dstar_to_tgba(const const_dstar_aut_ptr& dstar); - /// @} } diff --git a/src/tests/degenid.test b/src/tests/degenid.test index e6dd9e7b9..fa9271a9c 100755 --- a/src/tests/degenid.test +++ b/src/tests/degenid.test @@ -139,7 +139,7 @@ test 3 = "`../../bin/ltl2tgba -B 'G(a|G(b|Fc))' --stats=%s`" # This 7-state DRA (built with # ltlfilt -f 'F(a & GFb) | (Fc & Fa & F(c & GF!b))' -l | # ltl2dstar --ltl2nba=spin:ltl2tgba@-sD - - -# should be converted in into a 6-state DBA. +# should be converted in into a 5-state DBA. cat >in.dra < out.stat -test 6 = "`cat out.stat`" +test 5 = "`cat out.stat`" # Only one state should be accepting. In spot 1.2.x an initial state # in a trivial SCC was marked as accepting: this is superfluous. diff --git a/src/tests/dstar.test b/src/tests/dstar.test index f1fc8ff71..0d7d1e003 100755 --- a/src/tests/dstar.test +++ b/src/tests/dstar.test @@ -68,9 +68,9 @@ digraph G { 0 -> 0 [label="a & !b"] 0 -> 1 [label="!a & !b"] 0 -> 2 [label="b"] - 1 [label="1"] + 1 [label="1\n{0}"] 1 -> 1 [label="1"] - 2 [label="2"] + 2 [label="2\n{1}"] 2 -> 2 [label="1"] } EOF @@ -78,7 +78,7 @@ EOF diff expected stdout -run 0 ../ikwiad -XDD dra.dstar | tee stdout +run 0 ../ikwiad -XDB -R3 dra.dstar | tee stdout cat >expected < 0 + I -> 1 0 [label="0"] - 0 -> 1 [label="1"] - 0 -> 2 [label="1"] + 0 -> 0 [label="!a"] + 0 -> 2 [label="a"] 1 [label="1"] - 1 -> 1 [label="!a"] - 1 -> 2 [label="!a"] - 1 -> 3 [label="a"] - 1 -> 4 [label="a"] + 1 -> 0 [label="1"] 2 [label="2"] - 2 -> 5 [label="!a"] - 2 -> 4 [label="a\n{0}"] - 3 [label="3"] - 3 -> 1 [label="!a"] - 3 -> 2 [label="!a"] + 2 -> 0 [label="!a"] + 2 -> 2 [label="a"] + 2 -> 3 [label="a"] + 3 [label="3", peripheries=2] 3 -> 3 [label="a"] - 3 -> 4 [label="a"] - 4 [label="4"] - 4 -> 5 [label="!a"] - 4 -> 4 [label="a\n{0}"] - 5 [label="5"] - 5 -> 5 [label="!a"] - 5 -> 6 [label="a"] - 6 [label="6"] - 6 -> 5 [label="!a"] - 6 -> 6 [label="a"] } EOF diff expected stdout -test "`../../bin/dstar2tgba -D dsa.dstar --stats '%s %t %p %d'`" = "2 5 0 0" -test "`../../bin/dstar2tgba -DC dsa.dstar --stats '%s %t %p %d'`" = "3 8 1 0" +# These one could be reduced to 2 5 0 0 and 3 8 1 0 +test "`../../bin/dstar2tgba -D dsa.dstar --stats '%s %t %p %d'`" = "4 8 0 0" +test "`../../bin/dstar2tgba -DC dsa.dstar --stats '%s %t %p %d'`" = "5 11 1 0" @@ -213,7 +200,7 @@ Acc-Sig: +0 +1 4 EOF -run 0 ../ikwiad -XDD dra.dstar | tee stdout +run 0 ../ikwiad -XDB dra.dstar | tee stdout cat >expected < 0 0 [label="0"] - 0 -> 0 [label="1"] + 0 -> 0 [label="1\n{0}"] } EOF diff --git a/src/tests/ikwiad.cc b/src/tests/ikwiad.cc index 20192ddc7..271b2b88b 100644 --- a/src/tests/ikwiad.cc +++ b/src/tests/ikwiad.cc @@ -67,6 +67,7 @@ #include "twaalgos/dtbasat.hh" #include "twaalgos/dtgbasat.hh" #include "twaalgos/stutter.hh" +#include "twaalgos/totgba.hh" #include "taalgos/tgba2ta.hh" #include "taalgos/dot.hh" @@ -120,8 +121,6 @@ syntax(char* prog) << " ltl2dstar file" << std::endl << " -XDB read the from an ltl2dstar file and convert it to " << "TGBA" << std::endl - << " -XDD read the from an ltl2dstar file and convert it to " - << "TGBA,\n keeping it deterministic when possible\n" << " -XH do not compute an automaton, read it from a" << " HOA file\n" << " -XL do not compute an automaton, read it from an" @@ -347,7 +346,6 @@ checked_main(int argc, char** argv) bool from_file = false; enum { ReadDstar, ReadHoa } readformat = ReadHoa; bool nra2nba = false; - bool dra2dba = false; bool scc_filter = false; bool simpltl = false; spot::ltl::ltl_simplifier_options redopt(false, false, false, false, @@ -876,13 +874,6 @@ checked_main(int argc, char** argv) readformat = ReadDstar; nra2nba = true; } - else if (!strcmp(argv[formula_index], "-XDD")) - { - from_file = true; - readformat = ReadDstar; - nra2nba = true; - dra2dba = true; - } else if (!strcmp(argv[formula_index], "-XH")) { from_file = true; @@ -986,20 +977,8 @@ checked_main(int argc, char** argv) tm.start("dstar2tgba"); if (nra2nba) { - if (daut->type == spot::Rabin) - { - if (dra2dba) - a = spot::dstar_to_tgba(daut); - else - a = spot::nra_to_nba(daut); - assert(a->is_sba()); - assume_sba = true; - } - else - { - a = spot::nsa_to_tgba(daut); - assume_sba = false; - } + a = spot::to_generalized_buchi(daut->aut); + assume_sba = a->is_sba(); } else { @@ -1112,7 +1091,10 @@ checked_main(int argc, char** argv) if (scc_filter) { tm.start("SCC-filter"); - a = spot::scc_filter(ensure_digraph(a), scc_filter_all); + if (a->has_state_based_acc() & !scc_filter_all) + a = spot::scc_filter_states(ensure_digraph(a)); + else + a = spot::scc_filter(ensure_digraph(a), scc_filter_all); tm.stop("SCC-filter"); assume_sba = false; }