From e1271bf8b34c4b3fecb05ea3f5dbeb0d4345303a Mon Sep 17 00:00:00 2001 From: xlauko Date: Tue, 9 May 2017 10:16:53 +0200 Subject: [PATCH] tra2tba: Implement transformation of TRA to TBA acceptance condition * python/spot/impl.i: Add bindings for tra2tba * spot/twaalgos/Makefile.am: Record tra2tba.cc, tra2tba.hh * spot/twaalgos/tra2tba.cc: Implement transformation of TRA to TBA * spot/twaalgos/tra2tba.hh: Introduce declaration of tra_to_tba * tests/Makefile.am: Record tra2tba tests * tests/core/tra2tba.cc: Add driver for tests * tests/core/tra2tba.test: Add tests of tra2tba transformation --- python/spot/impl.i | 2 + spot/twaalgos/Makefile.am | 2 + spot/twaalgos/tra2tba.cc | 297 ++++++++++++++++++++++ spot/twaalgos/tra2tba.hh | 37 +++ tests/Makefile.am | 6 +- tests/core/tra2tba.cc | 41 +++ tests/core/tra2tba.test | 509 ++++++++++++++++++++++++++++++++++++++ 7 files changed, 892 insertions(+), 2 deletions(-) create mode 100644 spot/twaalgos/tra2tba.cc create mode 100644 spot/twaalgos/tra2tba.hh create mode 100644 tests/core/tra2tba.cc create mode 100755 tests/core/tra2tba.test diff --git a/python/spot/impl.i b/python/spot/impl.i index 956ec8fb7..90bf39e82 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -151,6 +151,7 @@ #include #include #include +#include #include #include #include @@ -581,6 +582,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..df8c1ae3d 100644 --- a/spot/twaalgos/Makefile.am +++ b/spot/twaalgos/Makefile.am @@ -84,6 +84,7 @@ twaalgos_HEADERS = \ tau03.hh \ tau03opt.hh \ totgba.hh \ + tra2tba.hh \ translate.hh \ word.hh @@ -145,6 +146,7 @@ libtwaalgos_la_SOURCES = \ tau03.cc \ tau03opt.cc \ totgba.cc \ + tra2tba.cc \ translate.cc \ word.cc diff --git a/spot/twaalgos/tra2tba.cc b/spot/twaalgos/tra2tba.cc new file mode 100644 index 000000000..2fd6d9f0e --- /dev/null +++ b/spot/twaalgos/tra2tba.cc @@ -0,0 +1,297 @@ +// -*- 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 + +namespace spot +{ + namespace + { + std::vector scc_edges(const const_twa_graph_ptr& aut, + const scc_info& si, + const unsigned scc) + { + std::vector edges; + for (unsigned s : si.states_of(scc)) + for (const auto& t: aut->succ(aut->state_from_number(s))) + edges.push_back(aut->edge_number(t)); + return edges; + + } + // + std::vector scc_inner_edges(const const_twa_graph_ptr& aut, + const scc_info& si, + const unsigned scc) + { + auto edges = scc_edges(aut, si, scc); + edges.erase(std::remove_if(edges.begin(), edges.end(), + [&](unsigned e) + { + return si.scc_of(aut->edge_storage(e).dst) != scc; + }), + edges.end()); + return edges; + } + + twa_graph_ptr mask_keep_edges(const const_twa_graph_ptr& aut, + std::vector& to_keep, + unsigned int init) + { + if (to_keep.size() < aut->edge_vector().size()) + to_keep.resize(aut->edge_vector().size(), false); + + auto res = make_twa_graph(aut->get_dict()); + res->copy_ap_of(aut); + res->prop_copy(aut, { false, true, false, true, false, false }); + res->copy_acceptance_of(aut); + + size_t states = aut->num_states(); + std::vector> edges; + edges.resize(states); + for (size_t i = 0; i < states; ++i) + edges[i].resize(states, false); + + for (size_t i = 0; i < aut->edge_vector().size(); ++i) + { + if (to_keep[i]) + { + const auto& es = aut->edge_storage(i); + edges[es.src][es.dst] = true; + } + } + + transform_copy(aut, res, + [&](unsigned src, bdd& cond, acc_cond::mark_t&, + unsigned dst) + { + if (!edges[src][dst]) + cond = bddfalse; + }, + init); + return res; + } + + // Check whether the SCC contains non-accepting cycles. + // + // A cycle is accepting (in a Rabin automaton) if there exists an + // acceptance pair (Fᵢ, Iᵢ) such that some states from Iᵢ are + // visited while no states from Fᵢ are visited. + // + // Consequently, a cycle is non-accepting if for all acceptance + // pairs (Fᵢ, Iᵢ), either no states from Iᵢ are visited or some + // states from Fᵢ are visited. (This corresponds to an accepting + // cycle with Streett acceptance.) + // + // final are those edges which are used in the resulting tba + // acceptance condition. + bool is_scc_tba_type(const const_twa_graph_ptr& aut, + const scc_info& si, + const unsigned scc, + std::vector& final) + { + if (si.is_rejecting_scc(scc)) + return true; + + auto acc_pairs = aut->get_acceptance().used_inf_fin_sets(); + auto infs = si.acc(scc) & acc_pairs.first; + auto infs_with_fins = (si.acc(scc) << 1U) & acc_pairs.first; + infs -= infs_with_fins; + + auto& states = si.states_of(scc); + // Firstly consider whole SCC as one large cycle. + // If there is no inf without matching fin then 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. + if (!infs) + { + // 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. + std::vector keep(aut->num_states(), false); + for (auto s: states) + keep[s] = true; + auto sccaut = mask_keep_accessible_states(aut, + keep, + states.front()); + sccaut->prop_state_acc(false); + return sccaut->is_empty(); + } + + // Remaining infs corresponds to I₁s that have been seen with seeing + // the mathing F₁. In this SCC any edge in these I₁ 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 Fᵢ. + std::set unknown; + for (auto e: scc_inner_edges(aut, si, scc)) + if (aut->edge_data(e).acc & infs) + final[e] = true; + else + unknown.insert(e); + // Check whether it is possible to build non-accepting cycles + // using only the "unknown" edges. + std::vector keep(aut->edge_vector().size(), false); + for (auto e: unknown) + keep[e] = true; + + while (!unknown.empty()) + { + unsigned init = aut->edge_storage(*unknown.begin()).src; + scc_info si(mask_keep_edges(aut, keep, init)); + unsigned scc_max = si.scc_count(); + for (unsigned uscc = 0; uscc < scc_max; ++uscc) + { + for (auto e: scc_edges(aut, si, uscc)) + { + unknown.erase(e); + keep[e] = false; + } + if (si.is_rejecting_scc(uscc)) + continue; + if (!is_scc_tba_type(aut, si, uscc, final)) + return false; + } + } + return true; + } + } + + // Specialized conversion from transition based Rabin acceptance to + // transition based Büchi acceptance. + // Is able to detect SCCs that are TBA-type (i.e., they can be + // converted to Büchi acceptance without chaning their structure). + // + // See "Deterministic ω-automata vis-a-vis Deterministic Büchi + // Automata", S. Krishnan, A. Puri, and R. Brayton (ISAAC'94) for + // some details about detecting Büchi-typeness. + // + // We essentially apply this method SCC-wise. The paper is + // concerned about *deterministic* automata, but we apply the + // algorithm on non-deterministic automata as well: in the worst + // case it is possible that a TBA-type SCC with some + // non-deterministic has one accepting and one rejecting run for + // the same word. In this case we may fail to detect the + // TBA-typeness of the SCC, but the resulting automaton should + // be correct nonetheless. + twa_graph_ptr + tra_to_tba(const const_twa_graph_ptr& aut) + { + if (aut->prop_state_acc().is_true()) + return nullptr; + std::vector pairs; + if (!aut->acc().is_rabin_like(pairs)) + return nullptr; + + auto code = aut->get_acceptance(); + if (code.is_t()) + return nullptr; + + // if is TBA type + scc_info si{aut}; + std::vector scc_is_tba_type(si.scc_count(), false); + std::vector final(aut->edge_vector().size(), false); + + for (unsigned scc = 0; scc < si.scc_count(); ++scc) + { + scc_is_tba_type[scc] = is_scc_tba_type(aut, si, scc, final); + } + // compute final edges + auto res = make_twa_graph(aut->get_dict()); + res->copy_ap_of(aut); + res->prop_copy(aut, { false, false, false, false, false, true }); + res->new_states(aut->num_states()); + res->set_buchi(); + res->set_init_state(aut->get_init_state_number()); + trival deterministic = aut->prop_universal(); + trival complete = aut->prop_complete(); + + std::vector state_map(aut->num_states()); + for (unsigned scc = 0; scc < si.scc_count(); ++scc) + { + auto states = si.states_of(scc); + + if (scc_is_tba_type[scc]) + { + for (unsigned e: scc_edges(aut, si, scc)) + { + const auto& ed = aut->edge_data(e); + const auto& es = aut->edge_storage(e); + bool acc = final[e]; + res->new_acc_edge(es.src, es.dst, ed.cond, acc); + } + } + else + { + deterministic = false; + complete = trival::maybe(); + + auto acc_pairs = aut->get_acceptance().used_inf_fin_sets(); + auto infs = si.acc(scc) & acc_pairs.first; + auto infs_with_fins = (si.acc(scc) << 1U) & acc_pairs.first; + infs -= infs_with_fins; + + for (auto e: scc_edges(aut, si, scc)) + { + const auto& ed = aut->edge_data(e); + const auto& es = aut->edge_storage(e); + bool acc{ ed.acc & infs }; + res->new_acc_edge(es.src, es.dst, ed.cond, acc); + } + + auto rem = si.acc(scc) & acc_pairs.second; + assert(rem != 0U); + for (auto r: rem.sets()) + { + unsigned base = res->new_states(states.size()); + for (auto s: states) + state_map[s] = base++; + for (auto e: scc_inner_edges(aut, si, scc)) + { + const auto& ed = aut->edge_data(e); + const auto& es = aut->edge_storage(e); + if (ed.acc.has(r)) + continue; + auto src = state_map[es.src]; + auto dst = state_map[es.dst]; + res->new_acc_edge(src, dst, ed.cond, ed.acc.has(r + 1)); + // We need only one non-deterministic jump per + // cycle. As an approximation, we only do + // them on back-links. + bool jacc{ed.acc & inf_alone}; + if (es.dst <= es.src) + res->new_acc_edge(es.src, dst, ed.cond, jacc); + } + } + } + } + res->prop_complete(complete); + res->prop_universal(deterministic); + res->purge_dead_states(); + return res; + } + +} diff --git a/spot/twaalgos/tra2tba.hh b/spot/twaalgos/tra2tba.hh new file mode 100644 index 000000000..3f812a7e1 --- /dev/null +++ b/spot/twaalgos/tra2tba.hh @@ -0,0 +1,37 @@ +// -*- 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 . + +#pragma once + +#include + +namespace spot +{ + /// \brief Convert a transition-based Rabin automaton to Büchi automaton, + /// preserving determinism when possible. + /// + /// Return nullptr if the input is not a Rabin automaton, or is not + /// transition-based. + /// + /// This modifies the algorithm from "Deterministic + /// ω-automata vis-a-vis Deterministic Büchi Automata", S. Krishnan, + /// A. Puri, and R. Brayton (ISAAC'94), but SCC-wise. + SPOT_API twa_graph_ptr + tra_to_tba(const const_twa_graph_ptr& aut); +} diff --git a/tests/Makefile.am b/tests/Makefile.am index c7439289d..05c042c4b 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -92,6 +92,7 @@ check_PROGRAMS = \ core/sccif \ core/syntimpl \ core/taatgba \ + core/tra2tba \ core/trival \ core/tgbagraph \ core/tostring \ @@ -139,6 +140,7 @@ core_safra_SOURCES = core/safra.cc core_sccif_SOURCES = core/sccif.cc core_syntimpl_SOURCES = core/syntimpl.cc core_tostring_SOURCES = core/tostring.cc +core_tra2tba_SOURCES = core/tra2tba.cc core_trival_SOURCES = core/trival.cc core_tunabbrev_SOURCES = core/equalsf.cc core_tunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DUNABBREV='"^ieFG"' @@ -296,8 +298,8 @@ TESTS_twa = \ core/complementation.test \ core/randpsl.test \ core/cycles.test \ - core/acc_word.test - + core/acc_word.test \ + core/tra2tba.test ############################## PYTHON ############################## diff --git a/tests/core/tra2tba.cc b/tests/core/tra2tba.cc new file mode 100644 index 000000000..34326c825 --- /dev/null +++ b/tests/core/tra2tba.cc @@ -0,0 +1,41 @@ +// -*- 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 + +int main(int, char* argv[]) +{ + char* input = argv[1]; + if (!input) + return 1; + auto pa = parse_aut(input, spot::make_bdd_dict()); + if (pa->format_errors(std::cerr)) + return 1; + if (pa->aborted) + { + std::cerr << "--ABORT-- read\n"; + return 1; + } + auto tba = spot::tra_to_tba(pa->aut); + spot::print_hoa(std::cout, tba) << '\n'; + return 0; +} diff --git a/tests/core/tra2tba.test b/tests/core/tra2tba.test new file mode 100755 index 000000000..3327d6737 --- /dev/null +++ b/tests/core/tra2tba.test @@ -0,0 +1,509 @@ +#!/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 >test1.hoa <out.exp << EOF +HOA: v1 +States: 2 +Start: 0 +AP: 2 "a" "b" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels trans-acc deterministic +--BODY-- +State: 0 +[!0] 0 {0} +[0] 1 +State: 1 +[0] 1 +--END-- +EOF + +run 0 ../tra2tba test1.hoa > out.hoa +diff out.hoa out.exp + +cat >test2.hoa <out.exp << EOF +HOA: v1 +States: 3 +Start: 0 +AP: 1 "a" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels trans-acc deterministic +--BODY-- +State: 0 +[!0] 0 +[0] 1 +State: 1 +[0] 2 +State: 2 +[!0] 1 +[0] 2 {0} +--END-- +EOF + +run 0 ../tra2tba test2.hoa > out.hoa +diff out.hoa out.exp + +cat >test3.hoa <out.exp << EOF +HOA: v1 +States: 2 +Start: 0 +AP: 2 "a" "b" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc deterministic +--BODY-- +State: 0 +[!0] 0 +[0] 1 +State: 1 +[0] 1 +--END-- +EOF + +run 0 ../tra2tba test3.hoa > out.hoa +diff out.hoa out.exp + +cat >test4.hoa <out.exp << EOF +HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc complete +--BODY-- +State: 0 +[0&1] 0 +[!0] 1 +[!1] 2 +State: 1 {0} +[t] 1 +State: 2 {0} +[t] 2 +--END-- +EOF + +run 0 ../tra2tba test4.hoa > out.hoa +diff out.hoa out.exp + +cat >test5.hoa <out.exp << EOF +HOA: v1 +States: 4 +Start: 0 +AP: 3 "a" "b" "c" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc complete +--BODY-- +State: 0 +[0&1&2] 0 +[!0] 1 +[!1] 2 +[!2] 3 +State: 1 {0} +[t] 1 +State: 2 {0} +[t] 2 +State: 3 {0} +[t] 3 +--END-- +EOF + +run 0 ../tra2tba test5.hoa > out.hoa +diff out.hoa out.exp + +cat >test6.hoa <out.exp << EOF +HOA: v1 +States: 4 +Start: 0 +AP: 2 "p3" "p2" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels trans-acc +--BODY-- +State: 0 +[0&1] 1 +[0&!1] 0 +[!0&1] 1 +[!0&!1] 0 +[0&!1] 2 +State: 1 +[0&1] 1 {0} +[0&!1] 0 {0} +[!0&1] 1 {0} +[!0&!1] 0 {0} +[0&1] 3 +[0&!1] 2 +State: 2 +[0&1] 3 {0} +[0&!1] 2 {0} +State: 3 +[0&1] 3 {0} +[0&!1] 2 {0} +--END-- +EOF + +run 0 ../tra2tba test6.hoa > out.hoa +diff out.hoa out.exp + +cat >test7.hoa <out.exp << EOF +HOA: v1 +States: 2 +Start: 0 +AP: 1 "a" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc +--BODY-- +State: 0 +[0] 0 +[!0] 0 +[0] 1 +State: 1 {0} +[0] 1 +--END-- +EOF + +run 0 ../tra2tba test7.hoa > out.hoa +diff out.hoa out.exp + +cat >test8.hoa <out.exp << EOF +HOA: v1 +States: 8 +Start: 0 +AP: 3 "p0" "p2" "p3" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels trans-acc +--BODY-- +State: 0 +[!0&1&2] 3 +[!0&1&!2 | 0&!1&!2] 4 +[!0&!1 | 0&1] 1 +[0&!1&2] 2 +State: 1 +[t] 1 {0} +State: 2 +[0&2] 5 +[0&!2] 6 +[!0&2] 3 +[!0&!2] 4 +State: 3 +[0&2] 2 +[!0&2] 3 +[!2] 4 +State: 4 +[t] 4 +State: 5 +[0&2] 5 +[0&!2] 6 +[!0&2] 3 +[!0&!2] 4 +[0&2] 7 +State: 6 +[0] 6 {0} +[!0] 4 +State: 7 +[0&2] 7 {0} +--END-- +EOF + +run 0 ../tra2tba test8.hoa > out.hoa +diff out.hoa out.exp + +cat >test9.hoa <out.exp << EOF +HOA: v1 +States: 2 +Start: 0 +AP: 3 "p0" "p4" "p1" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc deterministic +--BODY-- +State: 0 {0} +[0&!2] 1 +[!0&!2] 0 +State: 1 +[0&!2] 1 +[!0&!2] 0 +--END-- +EOF + +run 0 ../tra2tba test9.hoa > out.hoa +diff out.hoa out.exp + +cat >test10.hoa <out.exp << EOF +HOA: v1 +States: 3 +Start: 0 +AP: 2 "p0" "p2" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc +--BODY-- +State: 0 +[0&1] 0 +[!0&1] 1 +[0&!1] 0 +[0&1] 2 +State: 1 {0} +[1] 1 +State: 2 {0} +[0&1] 2 +--END-- +EOF + +run 0 ../tra2tba test10.hoa > out.hoa +diff out.hoa out.exp + +cat >test11.hoa <out.exp << EOF +HOA: v1 +States: 2 +Start: 0 +AP: 2 "p2" "p0" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels trans-acc complete +properties: deterministic +--BODY-- +State: 0 +[1] 1 +[!1] 0 {0} +State: 1 +[1] 1 {0} +[!1] 0 {0} +--END-- +EOF + +run 0 ../tra2tba test11.hoa > out.hoa +diff out.hoa out.exp