diff --git a/NEWS b/NEWS index 2feeb4b4d..b63630d6a 100644 --- a/NEWS +++ b/NEWS @@ -83,6 +83,11 @@ New in spot 2.4.4.dev (net yet released) New functions in the library: + - spot::iar() and spot::iar_maybe() use index appearance records (IAR) + to translate Rabin-like automata into equivalent parity automaton. + This translation preserves determinism and is especially useful when + the input automaton is deterministic. + - spot::print_aiger() encodes an automaton as an AIGER circuit, as required by the SYNTCOMP competition. It relies on a new named property "synthesis outputs" that describes which atomic diff --git a/python/spot/impl.i b/python/spot/impl.i index de6fdc039..1f200cd1e 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -163,6 +163,7 @@ #include #include #include +#include #include @@ -617,6 +618,7 @@ def state_is_accepting(self, src) -> "bool": %include %template(list_bdd) std::list; %include +%include %pythonprepend spot::twa::dtwa_complement %{ from warnings import warn diff --git a/spot/twaalgos/Makefile.am b/spot/twaalgos/Makefile.am index 78ae1720d..5d1d7fa3b 100644 --- a/spot/twaalgos/Makefile.am +++ b/spot/twaalgos/Makefile.am @@ -67,6 +67,7 @@ twaalgos_HEADERS = \ postproc.hh \ powerset.hh \ product.hh \ + rabin2parity.hh \ randomgraph.hh \ randomize.hh \ reachiter.hh \ @@ -132,6 +133,7 @@ libtwaalgos_la_SOURCES = \ postproc.cc \ powerset.cc \ product.cc \ + rabin2parity.cc \ randomgraph.cc \ randomize.cc \ reachiter.cc \ diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index 2e23ba693..8769d2978 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -38,6 +38,7 @@ #include #include #include +#include namespace spot { @@ -240,7 +241,15 @@ namespace spot if ((via_gba && !a->acc().is_generalized_buchi()) || (want_parity && !a->acc().is_parity())) { - a = to_generalized_buchi(a); + twa_graph_ptr b = nullptr; + if (want_parity && is_deterministic(a)) + b = iar_maybe(a); + // possible only if a was deterministic and Rabin-like and + // we want parity + if (b) + a = b; + else + a = to_generalized_buchi(a); if (PREF_ == Any && level_ == Low) a = do_scc_filter(a, true); } diff --git a/spot/twaalgos/rabin2parity.cc b/spot/twaalgos/rabin2parity.cc new file mode 100644 index 000000000..0847803dc --- /dev/null +++ b/spot/twaalgos/rabin2parity.cc @@ -0,0 +1,293 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2017-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 + +#include + +#include +#include + +namespace spot +{ + namespace + { + + using perm_t = std::vector; + struct iar_state + { + unsigned state; + perm_t perm; + + bool + operator<(const iar_state& other) const + { + return state == other.state ? perm < other.perm : state < other.state; + } + }; + + class iar_generator + { + public: + explicit iar_generator(const const_twa_graph_ptr& a, + const std::vector& p) + : aut_(a) + , pairs_(p) + , scc_(scc_info(a)) + {} + + twa_graph_ptr + run() + { + res_ = make_twa_graph(aut_->get_dict()); + res_->copy_ap_of(aut_); + + build_iar_scc(scc_.initial()); + + // resulting automaton has acceptance condition: parity max odd + // with priorities ranging from 0 to 2*(nb Rabin pairs) + // /!\ priorities are shifted by -1 compared to the original paper + res_->set_acceptance(2*pairs_.size() + 1, + acc_cond::acc_code::parity(true, true, 2*pairs_.size() + 1)); + + // set initial state + res_->set_init_state( + iar2num.at(state2iar.at(aut_->get_init_state_number()))); + + // there could be quite a number of unreachable states, prune them + res_->purge_unreachable_states(); + + return res_; + } + + void + build_iar_scc(unsigned scc_num) + { + // we are working on an SCC: the state we start from does not matter + unsigned init = scc_.one_state_of(scc_num); + + std::deque todo; + auto get_state = [&](const iar_state& s) + { + auto it = iar2num.find(s); + if (it == iar2num.end()) + { + unsigned nb = res_->new_state(); + iar2num[s] = nb; + num2iar[nb] = s; + todo.push_back(s); + return nb; + } + return it->second; + }; + + auto get_other_scc = [this](unsigned state) + { + auto it = state2iar.find(state); + // recursively build the destination SCC if we detect that it has + // not been already built. + if (it == state2iar.end()) + build_iar_scc(scc_.scc_of(state)); + return iar2num.at(state2iar.at(state)); + }; + + if (scc_.is_trivial(scc_num)) + { + iar_state iar_s{init, perm_t()}; + state2iar[init] = iar_s; + unsigned src_num = get_state(iar_s); + // Do not forget to connect to subsequent SCCs + for (const auto& e : aut_->out(init)) + res_->new_edge(src_num, get_other_scc(e.dst), e.cond); + return; + } + + // determine the Rabin pairs that appear in the SCC + auto colors = scc_.acc_sets_of(scc_num); + std::set scc_pairs; + for (unsigned k = 0; k != pairs_.size(); ++k) + if (colors & (pairs_[k].fin | pairs_[k].inf)) + scc_pairs.insert(k); + + perm_t p0; + for (unsigned k : scc_pairs) + p0.push_back(k); + + iar_state s0{init, p0}; + get_state(s0); // put s0 in todo + + // the main loop + while (!todo.empty()) + { + iar_state current = todo.front(); + todo.pop_front(); + + unsigned src_num = get_state(current); + + for (const auto& e : aut_->out(current.state)) + { + // connect to the appropriate state + if (scc_.scc_of(e.dst) != scc_num) + res_->new_edge(src_num, get_other_scc(e.dst), e.cond); + else + { + // find the new permutation + perm_t new_perm = current.perm; + // Count pairs whose fin-part is seen on this transition + unsigned seen_nb = 0; + std::vector seen; + // consider the pairs for this SCC only + for (unsigned k : scc_pairs) + if (e.acc & pairs_[k].fin) + { + ++seen_nb; + auto it = std::find(new_perm.begin(), + new_perm.end(), + k); + // move the pair in front of the permutation + std::rotate(new_perm.begin(), it, it+1); + } + + iar_state dst; + unsigned dst_num = -1U; + + // Optimization: when several indices are seen in the + // transition, they move at the front of new_perm in any + // order. Check whether there already exists an iar_state + // that matches this condition. + for (unsigned i = 0; i != num2iar.size(); ++i) + if (num2iar[i].state == e.dst) + if (std::equal(new_perm.begin() + seen_nb, + new_perm.end(), + num2iar[i].perm.begin() + seen_nb)) + { + dst = num2iar[i]; + dst_num = i; + break; + } + // if such a state was not found, build it + if (dst_num == -1U) + { + dst = iar_state{e.dst, new_perm}; + dst_num = get_state(dst); + } + + // find the maximal index encountered by this transition + unsigned maxint = -1U; + for (unsigned k = 0; k != current.perm.size(); ++k) + { + unsigned pk = current.perm[k]; + if (e.acc & (pairs_[pk].fin | pairs_[pk].inf)) + // k increases in the loop, so k > maxint necessarily + maxint = k; + } + + acc_cond::mark_t acc = 0U; + if (maxint == -1U) + acc = {0}; + else if (e.acc & pairs_[current.perm[maxint]].fin) + acc = {2*maxint+2}; + else + acc = {2*maxint+1}; + + res_->new_edge(src_num, dst_num, e.cond, acc); + } + } + } + + // Optimization: find the bottom SCC of the sub-automaton we have just + // built. To that end, we have to ignore edges going out of scc_num. + auto leaving_edge = [&](unsigned d) + { + return scc_.scc_of(num2iar.at(d).state) != scc_num; + }; + auto filter_edge = [](const twa_graph::edge_storage_t&, + unsigned dst, + void* filter_data) + { + decltype(leaving_edge)* data = + static_cast(filter_data); + + if ((*data)(dst)) + return scc_info::edge_filter_choice::ignore; + return scc_info::edge_filter_choice::keep; + }; + scc_info sub_scc(res_, get_state(s0), filter_edge, &leaving_edge); + // SCCs are numbered in reverse topological order, so the bottom SCC has + // index 0. + const unsigned bscc = 0; + assert(sub_scc.succ(0).empty()); + assert( + [&]() + { + for (unsigned s = 1; s != sub_scc.scc_count(); ++s) + if (sub_scc.succ(s).empty()) + return false; + return true; + } ()); + + assert(sub_scc.states_of(bscc).size() + >= scc_.states_of(scc_num).size()); + + // update state2iar + for (const auto& scc_state : sub_scc.states_of(bscc)) + { + iar_state iar = num2iar.at(scc_state); + if (state2iar.find(iar.state) == state2iar.end()) + state2iar[iar.state] = iar; + } + } + + private: + const const_twa_graph_ptr& aut_; + const std::vector& pairs_; + const scc_info scc_; + twa_graph_ptr res_; + + // to be used when entering a new SCC + // maps a state of aut_ onto an iar_state with the appropriate perm + std::map state2iar; + + std::map iar2num; + std::map num2iar; + }; + } + + twa_graph_ptr + iar_maybe(const const_twa_graph_ptr& aut) + { + std::vector rabin_pairs; + if (!aut->acc().is_rabin_like(rabin_pairs)) + return nullptr; + + iar_generator gen(aut, rabin_pairs); + return gen.run(); + } + + twa_graph_ptr + iar(const const_twa_graph_ptr& aut) + { + auto res = iar_maybe(aut); + if (!res) + throw std::runtime_error("rabin2parity works only for Rabin-like " + "automata"); + + return res; + } +} + diff --git a/spot/twaalgos/rabin2parity.hh b/spot/twaalgos/rabin2parity.hh new file mode 100644 index 000000000..64b74b414 --- /dev/null +++ b/spot/twaalgos/rabin2parity.hh @@ -0,0 +1,46 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2017-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 +{ + /// \brief Turn a Rabin-like automaton into a parity automaton based on the + /// index appearence record (IAR) + /// + /// If the input automaton has n states and k pairs, the output automaton has + /// at most k!*n states and 2k+1 colors. If the input automaton is + /// deterministic, the output automaton is deterministic as well, which is the + /// intended use case for this function. If the input automaton is + /// non-deterministic, the result is still correct, but way larger than an + /// equivalent Büchi automaton. The output parity automaton has max odd + /// acceptance condition. + /// Details on the algorithm can be found in: + /// https://arxiv.org/pdf/1701.05738.pdf (published at TACAS 2017) + SPOT_API + twa_graph_ptr + iar(const const_twa_graph_ptr& aut); + + /// Return nullptr if the input automaton is not Rabin-like, and calls iar() + /// otherwise. + SPOT_API + twa_graph_ptr + iar_maybe(const const_twa_graph_ptr& aut); +} diff --git a/tests/Makefile.am b/tests/Makefile.am index 39b2e4a90..7622c69b8 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -313,7 +313,8 @@ TESTS_twa = \ core/dnfstreett.test \ core/parity.test \ core/parity2.test \ - core/ltlsynt.test + core/ltlsynt.test \ + core/rabin2parity.test ############################## PYTHON ############################## diff --git a/tests/core/rabin2parity.test b/tests/core/rabin2parity.test new file mode 100644 index 000000000..a5fe2d6ea --- /dev/null +++ b/tests/core/rabin2parity.test @@ -0,0 +1,49 @@ +#!/bin/sh +# -*- 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 . + +. ./defs +set -e + +( +cat <