diff --git a/NEWS b/NEWS index a69eb839a..0dbd03bff 100644 --- a/NEWS +++ b/NEWS @@ -144,6 +144,10 @@ New in spot 2.3.5.dev (not yet released) more (this threshold can be changed, see -x relabel-bool=N in the spot-x(7) man page). + - The new function spot::to_weak_alternating() is able to take an + input automaton with generalized Büchi/co-Büchi acceptance and + convert it to a weak alternating automaton. + Python: - The 'spot.gen' package exports the functions from libspotgen. diff --git a/python/spot/impl.i b/python/spot/impl.i index 956ec8fb7..eaa12edfb 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -152,6 +152,7 @@ #include #include #include +#include #include #include #include @@ -582,6 +583,7 @@ def state_is_accepting(self, src) -> "bool": %include %include %include +%include %include %include %include diff --git a/spot/twaalgos/Makefile.am b/spot/twaalgos/Makefile.am index 38cc4136b..c78a82e00 100644 --- a/spot/twaalgos/Makefile.am +++ b/spot/twaalgos/Makefile.am @@ -84,6 +84,7 @@ twaalgos_HEADERS = \ tau03.hh \ tau03opt.hh \ totgba.hh \ + toweak.hh \ translate.hh \ word.hh @@ -145,6 +146,7 @@ libtwaalgos_la_SOURCES = \ tau03.cc \ tau03opt.cc \ totgba.cc \ + toweak.cc \ translate.cc \ word.cc diff --git a/spot/twaalgos/toweak.cc b/spot/twaalgos/toweak.cc new file mode 100644 index 000000000..c368cf939 --- /dev/null +++ b/spot/twaalgos/toweak.cc @@ -0,0 +1,228 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2017 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 +#include +#include +#include + +#include +#include + +namespace spot +{ + namespace + { + struct rc_state + { + unsigned id; + unsigned rank; + acc_cond::mark_t mark; + + rc_state(unsigned state_id, unsigned state_rank, acc_cond::mark_t m = 0U) + : id(state_id), rank(state_rank), mark(m) + { + } + }; + + struct rc_state_hash + { + size_t + operator()(const rc_state& s) const + { + using std::hash; + return ((hash()(s.id) + ^ (hash()(s.rank))) + ^ (hash()(s.mark.id))); + } + }; + + struct rc_state_equal + { + size_t + operator()(const rc_state& left, const rc_state& right) const + { + return left.id == right.id + && left.rank == right.rank + && left.mark == right.mark; + } + }; + + class to_weak + { + private: + const const_twa_graph_ptr aut_; + const unsigned numsets_; + std::unordered_map state_map_; + std::vector state_to_var_; + std::unordered_map var_to_state_; + bdd all_states_; + twa_graph_ptr res_; + std::queue todo_; + bool less_; + + unsigned new_state(unsigned st, unsigned rank, acc_cond::mark_t mark) + { + rc_state s(st, rank, mark); + auto p = state_map_.emplace(s, 0); + if (p.second) + { + p.first->second = res_->new_state(); + todo_.emplace(s); + int v = aut_->get_dict()->register_anonymous_variables(1, this); + bdd var = bdd_ithvar(v); + all_states_ &= var; + state_to_var_.push_back(var); + var_to_state_.emplace(var, p.first->second); + } + return p.first->second; + }; + + bdd transition_function(rc_state st) + { + unsigned id = st.id; + unsigned rank = st.rank; + + bdd res = bddfalse; + + bool rank_odd = rank % 2; + for (auto& e : aut_->out(id)) + { + // If we are on odd level and the edge is marked with the set we + // don't want to see, skip. (delete transition). + if (rank_odd && (e.acc & st.mark)) + continue; + + bdd dest = bddtrue; + for (unsigned d : aut_->univ_dests(e.dst)) + { + bdd levels = bddfalse; + int curr = static_cast(rank); + // We must always be able to go to the previous even rank + int lower = less_ ? ((curr - 1) & ~1) : 0; + for (int i = curr; i >= lower; --i) + { + if (i % 2) + for (unsigned m = 0; m < numsets_; ++m) + levels |= state_to_var_[new_state(d, i, {m})]; + else + levels |= state_to_var_[new_state(d, i, 0U)]; + } + dest &= levels; + } + res |= (dest & e.cond); + } + return res; + } + + public: + to_weak(const const_twa_graph_ptr& aut, bool less) + : aut_(aut), + numsets_(aut_->num_sets()), + all_states_(bddtrue), + res_(make_twa_graph(aut_->get_dict())), + less_(less) + { + res_->copy_ap_of(aut_); + res_->set_buchi(); + res_->prop_weak(true); + } + + ~to_weak() + { + aut_->get_dict()->unregister_all_my_variables(this); + } + + twa_graph_ptr run() + { + std::vector states; + for (unsigned d: aut_->univ_dests(aut_->get_init_state_number())) + states.push_back(new_state(d, aut_->num_states() * 2, 0U)); + + res_->set_univ_init_state(states.begin(), states.end()); + + while (!todo_.empty()) + { + rc_state st = todo_.front(); + + acc_cond::mark_t mark = 0U; + if (st.rank % 2) + mark = {0}; + + bdd delta = transition_function(st); + bdd ap = bdd_exist(bdd_support(delta), all_states_); + bdd letters = bdd_exist(delta, all_states_); + + while (letters != bddfalse) + { + bdd oneletter = bdd_satoneset(letters, ap, bddtrue); + letters -= oneletter; + + minato_isop isop(delta & oneletter); + bdd cube; + + while ((cube = isop.next()) != bddfalse) + { + bdd cond = bdd_exist(cube, all_states_); + bdd dest = bdd_existcomp(cube, all_states_); + + states.clear(); + while (dest != bddtrue) + { + assert(bdd_low(dest) == bddfalse); + bdd v = bdd_ithvar(bdd_var(dest)); + auto it = var_to_state_.find(v); + assert(it != var_to_state_.end()); + states.push_back(it->second); + dest = bdd_high(dest); + } + res_->new_univ_edge(new_state(st.id, st.rank, st.mark), + states.begin(), states.end(), + cond, mark); + } + } + todo_.pop(); + } + res_->merge_edges(); + return res_; + } + }; + } + twa_graph_ptr to_weak_alternating(const_twa_graph_ptr& aut, bool less) + { + if (is_weak_automaton(aut)) + return make_twa_graph(aut, twa::prop_set::all()); + /* The current implementation of is_inherently_weak does not support + alternating automata. In case the input automaton is inherently weak, + it can be easily transformed to weak without the need to call to_weak + */ + if (aut->acc().is_generalized_buchi()) + return dualize(to_weak(dualize(aut), less).run()); + else if (aut->acc().is_generalized_co_buchi()) + return to_weak(aut, less).run(); + + throw std::runtime_error("to_weak_alternating does only support gen. Büchi" + " and gen. co-Büchi automata."); + } +} diff --git a/spot/twaalgos/toweak.hh b/spot/twaalgos/toweak.hh new file mode 100644 index 000000000..0b77749af --- /dev/null +++ b/spot/twaalgos/toweak.hh @@ -0,0 +1,69 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2017 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 . + +#pragma once + +#include + +namespace spot +{ + /// \brief Convert an alternating automaton to a weak alternating automaton. + /// + /// The input automaton must have a generalized co-Büchi or Büchi acceptance + /// condition. + /// The automaton will be converted into a weak Büchi automaton. If the input + /// automaton is already weak, it will simply be copied. + /// + /// For details about the algorithm used, see the following papers: + /** \verbatim + @article{kupferman.01.tocl, + author = {Orna Kupferman and Moshe Y. Vardi}, + title = {Weak alternating automata are not that weak}, + journal = {ACM Transactions on Computational Logic (TOCL)}, + month = {July}, + year = 2001, + pages = {408--429}, + volume = {2}, + number = {3}, + publisher = {ACM New York, NY, USA} + } + @article{kupferman.05.tcs, + author = {Orna Kupferman and Moshe Y. Vardi}, + title = {From complementation to certification}, + journal = {Theoretical Computer Science}, + month = {November}, + year = 2005, + pages = {83--100}, + volume = {345}, + number = {1}, + publisher = {Elsevier} + } + \endverbatim */ + /// Although at the end of the above paper there is a hint at an optimization + /// that greatly reduces the number of transition in the resulting automaton, + /// but in return makes the run of remove_alternation algorithm way slower. + /// Hence, the optimization is disabled by default. + /// + /// \param aut the automaton to convert to weak + /// \param less whether to activate the optimization on the number of + /// transitions or not, disabled by default + SPOT_API + twa_graph_ptr to_weak_alternating(const_twa_graph_ptr& aut, + bool less = false); +} diff --git a/tests/Makefile.am b/tests/Makefile.am index a853ee302..9410309b5 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -371,6 +371,7 @@ TESTS_python = \ python/trival.py \ python/tra2tba.py \ python/twagraph.py \ + python/toweak.py \ $(TESTS_ipython) endif diff --git a/tests/python/toweak.py b/tests/python/toweak.py new file mode 100644 index 000000000..120d23e00 --- /dev/null +++ b/tests/python/toweak.py @@ -0,0 +1,55 @@ +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2017 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 . + +import spot + +phi1 = """GFb +X(!b | GF!a) +!a U X(b | GF!b) +GFa +G(a M b) +(!a | b) & GFb +(a U Xa) | G(b & Fa) +GF!b +(b & GF!b) | (!b & FGb) +b | (a & XF(b R a)) | (!a & XG(!b U !a))""" + +phi1 = phi1.split('\n') + +bdddict = spot.make_bdd_dict() + +def equivalent(a, phi): + negphi = spot.formula.Not(phi) + nega = spot.dualize(a) + a2 = spot.translate(phi, 'TGBA', 'SBAcc' ) + nega2 = spot.translate(negphi, 'TGBA', 'SBAcc') + ra = spot.remove_alternation(a) + ran = spot.remove_alternation(nega) + return spot.product(spot.remove_alternation(a), nega2).is_empty()\ + and spot.product(spot.remove_alternation(nega), a2).is_empty() + +def test_phi(phi): + a = spot.translate(phi, 'TGBA', 'SBAcc') + a0 = spot.dualize(a) + + res = spot.to_weak_alternating(a0) + assert equivalent(res, spot.formula.Not(spot.formula(phi))) + +for p in phi1: + test_phi(p)