diff --git a/NEWS b/NEWS index baa3f5d0a..d4713d5d9 100644 --- a/NEWS +++ b/NEWS @@ -27,6 +27,10 @@ New in spot 2.6.0.dev (not yet released) twa_graph_ptr::is_empty(), twa_graph_ptr::intersects(), and scc_info::determine_unknown_acceptance(). + - The new function spot::to_parity() translates an automaton + with arbitrary acceptance condition into a parity automaton, + based on a last-appearance record (LAR) construction. + New in spot 2.6 (2018-07-04) Command-line tools: diff --git a/python/spot/impl.i b/python/spot/impl.i index 6a8772b3a..23a1dbc27 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -168,6 +168,7 @@ #include #include #include +#include #include @@ -632,6 +633,7 @@ def state_is_accepting(self, src) -> "bool": %template(list_bdd) std::list; %include %include +%include %pythonprepend spot::twa::dtwa_complement %{ from warnings import warn diff --git a/spot/twaalgos/Makefile.am b/spot/twaalgos/Makefile.am index 1de39842a..01adf944a 100644 --- a/spot/twaalgos/Makefile.am +++ b/spot/twaalgos/Makefile.am @@ -92,6 +92,7 @@ twaalgos_HEADERS = \ sum.hh \ tau03.hh \ tau03opt.hh \ + toparity.hh \ totgba.hh \ toweak.hh \ translate.hh \ @@ -161,6 +162,7 @@ libtwaalgos_la_SOURCES = \ sum.cc \ tau03.cc \ tau03opt.cc \ + toparity.cc \ totgba.cc \ toweak.cc \ translate.cc \ diff --git a/spot/twaalgos/toparity.cc b/spot/twaalgos/toparity.cc new file mode 100644 index 000000000..e637dd43a --- /dev/null +++ b/spot/twaalgos/toparity.cc @@ -0,0 +1,162 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2018 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 "config.h" +#include + +#include +#include + +#include + +namespace spot +{ + + namespace + { + struct lar_state + { + unsigned state; + std::vector perm; + + bool operator<(const lar_state& s) const + { + return state == s.state ? perm < s.perm : state < s.state; + } + + std::string to_string() const + { + std::stringstream s; + s << state << " ["; + for (unsigned i = 0; i != perm.size(); ++i) + { + s << perm[i]; + if (i < perm.size() - 1) + s << ','; + } + s << ']'; + return s.str(); + } + }; + + class lar_generator + { + const const_twa_graph_ptr& aut_; + twa_graph_ptr res_; + const bool pretty_print; + + std::map lar2num; + public: + explicit lar_generator(const const_twa_graph_ptr& a, bool pretty_print) + : aut_(a) + , res_(nullptr) + , pretty_print(pretty_print) + {} + + twa_graph_ptr run() + { + res_ = make_twa_graph(aut_->get_dict()); + res_->copy_ap_of(aut_); + + std::deque todo; + auto get_state = [this, &todo](const lar_state& s) + { + auto it = lar2num.emplace(s, -1U); + if (it.second) // insertion took place + { + unsigned nb = res_->new_state(); + it.first->second = nb; + todo.push_back(s); + } + return it.first->second; + }; + + { + std::vector p0; + for (unsigned k : aut_->acc().all_sets().sets()) + p0.push_back(k); + lar_state s0{aut_->get_init_state_number(), p0}; + unsigned init = get_state(s0); // put s0 in todo + res_->set_init_state(init); + } + + // main loop + while (!todo.empty()) + { + lar_state current = todo.front(); + todo.pop_front(); + + // TODO todo could store this number to avoid one lookup + unsigned src_num = get_state(current); + + for (const auto& e : aut_->out(current.state)) + { + // find the new permutation + std::vector new_perm = current.perm; + unsigned h = 0; + for (unsigned k : e.acc.sets()) + { + auto it = std::find(new_perm.begin(), new_perm.end(), k); + h = std::max(h, unsigned(new_perm.end() - it)); + std::rotate(it, it+1, new_perm.end()); + } + + lar_state dst{e.dst, new_perm}; + unsigned dst_num = get_state(dst); + + // do the h last elements satisfy the acceptance condition? + acc_cond::mark_t m(new_perm.end() - h, new_perm.end()); + if (aut_->acc().accepting(m)) + res_->new_edge(src_num, dst_num, e.cond, {2*h}); + else + res_->new_edge(src_num, dst_num, e.cond, {2*h+1}); + } + } + + // parity max even + res_->set_acceptance(2*aut_->num_sets() + 2, + acc_cond::acc_code::parity(true, false, 2*aut_->num_sets() + 2)); + + if (pretty_print) + { + auto names = new std::vector(res_->num_states()); + for (const auto& p : lar2num) + (*names)[p.second] = p.first.to_string(); + res_->set_named_prop("state-names", names); + } + + return res_; + } + }; + } + + twa_graph_ptr + to_parity(const const_twa_graph_ptr& aut, bool pretty_print) + { + if (!aut->is_existential()) + throw std::runtime_error("LAR does not handle alternation"); + // if aut is already parity return it as is + if (aut->acc().is_parity()) + return std::const_pointer_cast(aut); + + lar_generator gen(aut, pretty_print); + return gen.run(); + } + +} diff --git a/spot/twaalgos/toparity.hh b/spot/twaalgos/toparity.hh new file mode 100644 index 000000000..c9c22985f --- /dev/null +++ b/spot/twaalgos/toparity.hh @@ -0,0 +1,33 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2018 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 . + +#pragma once + +#include + +namespace spot +{ + /// \ingroup twa_acc_transform + /// \brief Take an automaton with any acceptance condition and return an + /// equivalent parity automaton. + /// + /// The parity condition of the returned automaton is max even. + SPOT_API twa_graph_ptr + to_parity(const const_twa_graph_ptr& aut, bool pretty_print=false); +} diff --git a/tests/Makefile.am b/tests/Makefile.am index 0f6f72bdd..c331d1a1e 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -409,6 +409,7 @@ TESTS_python = \ python/streett_totgba2.py \ python/rs_like.py \ python/sum.py \ + python/toparity.py \ python/trival.py \ python/tra2tba.py \ python/twagraph.py \ diff --git a/tests/python/toparity.py b/tests/python/toparity.py new file mode 100644 index 000000000..edb8f77f1 --- /dev/null +++ b/tests/python/toparity.py @@ -0,0 +1,32 @@ +#!/usr/bin/python3 +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2018 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 + +for f in spot.randltl(4, 400): + d = spot.translate(f, "det", "G") + p = spot.to_parity(d) + assert spot.are_equivalent(p, d) + +for f in spot.randltl(5, 2000): + n = spot.translate(f) + p = spot.to_parity(n) + assert spot.are_equivalent(n, p) +