diff --git a/spot/twaalgos/tra2tba.cc b/spot/twaalgos/tra2tba.cc index 2fd6d9f0e..e07b4c93f 100644 --- a/spot/twaalgos/tra2tba.cc +++ b/spot/twaalgos/tra2tba.cc @@ -108,6 +108,7 @@ namespace spot bool is_scc_tba_type(const const_twa_graph_ptr& aut, const scc_info& si, const unsigned scc, + const acc_cond::mark_t fin_alone, std::vector& final) { if (si.is_rejecting_scc(scc)) @@ -115,9 +116,18 @@ namespace spot auto acc_pairs = aut->get_acceptance().used_inf_fin_sets(); auto infs = si.acc(scc) & acc_pairs.first; + auto fins = si.acc(scc) & acc_pairs.second; auto infs_with_fins = (si.acc(scc) << 1U) & acc_pairs.first; infs -= infs_with_fins; + // If there is one fin_alone that is not in the SCC, + // any cycle in the SCC is accepting. + if ((fins & fin_alone) != fin_alone) + { + for (auto e: scc_edges(aut, si, scc)) + final[e] = true; + return true; + } 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 @@ -172,7 +182,7 @@ namespace spot } if (si.is_rejecting_scc(uscc)) continue; - if (!is_scc_tba_type(aut, si, uscc, final)) + if (!is_scc_tba_type(aut, si, uscc, fin_alone, final)) return false; } } @@ -202,6 +212,7 @@ namespace spot { if (aut->prop_state_acc().is_true()) return nullptr; + std::vector pairs; if (!aut->acc().is_rabin_like(pairs)) return nullptr; @@ -215,9 +226,17 @@ namespace spot std::vector scc_is_tba_type(si.scc_count(), false); std::vector final(aut->edge_vector().size(), false); + acc_cond::mark_t inf_alone = 0U; + acc_cond::mark_t fin_alone = 0U; + for (const auto& p: pairs) + if (!p.fin) + inf_alone &= p.inf; + else if (!p.inf) + fin_alone &= p.fin; + for (unsigned scc = 0; scc < si.scc_count(); ++scc) { - scc_is_tba_type[scc] = is_scc_tba_type(aut, si, scc, final); + scc_is_tba_type[scc] = is_scc_tba_type(aut, si, scc, fin_alone, final); } // compute final edges auto res = make_twa_graph(aut->get_dict()); diff --git a/tests/Makefile.am b/tests/Makefile.am index 05c042c4b..a853ee302 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -92,7 +92,6 @@ check_PROGRAMS = \ core/sccif \ core/syntimpl \ core/taatgba \ - core/tra2tba \ core/trival \ core/tgbagraph \ core/tostring \ @@ -140,7 +139,6 @@ 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"' @@ -298,8 +296,7 @@ TESTS_twa = \ core/complementation.test \ core/randpsl.test \ core/cycles.test \ - core/acc_word.test \ - core/tra2tba.test + core/acc_word.test ############################## PYTHON ############################## @@ -372,6 +369,7 @@ TESTS_python = \ python/rs_like.py \ python/sum.py \ python/trival.py \ + python/tra2tba.py \ python/twagraph.py \ $(TESTS_ipython) endif diff --git a/tests/core/tra2tba.cc b/tests/core/tra2tba.cc deleted file mode 100644 index 34326c825..000000000 --- a/tests/core/tra2tba.cc +++ /dev/null @@ -1,41 +0,0 @@ -// -*- 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/python/tra2tba.py old mode 100755 new mode 100644 similarity index 66% rename from tests/core/tra2tba.test rename to tests/python/tra2tba.py index 3327d6737..db78390e9 --- a/tests/core/tra2tba.test +++ b/tests/python/tra2tba.py @@ -1,28 +1,7 @@ -#!/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 . +import spot -. ./defs - -set -e - -cat >test1.hoa <out.exp << EOF -HOA: v1 +exp = """HOA: v1 States: 2 Start: 0 AP: 2 "a" "b" @@ -51,13 +29,13 @@ State: 0 [0] 1 State: 1 [0] 1 ---END-- -EOF +--END--""" -run 0 ../tra2tba test1.hoa > out.hoa -diff out.hoa out.exp +res = spot.tra_to_tba(aut) +assert(res.to_str('hoa') == exp) -cat >test2.hoa <out.exp << EOF -HOA: v1 +exp = """HOA: v1 States: 3 Start: 0 AP: 1 "a" @@ -92,13 +70,13 @@ State: 1 State: 2 [!0] 1 [0] 2 {0} ---END-- -EOF +--END--""" -run 0 ../tra2tba test2.hoa > out.hoa -diff out.hoa out.exp +res = spot.tra_to_tba(aut) +assert(res.to_str('hoa') == exp) -cat >test3.hoa <out.exp << EOF -HOA: v1 +exp = """HOA: v1 States: 2 Start: 0 AP: 2 "a" "b" @@ -127,13 +104,13 @@ State: 0 [0] 1 State: 1 [0] 1 ---END-- -EOF +--END--""" -run 0 ../tra2tba test3.hoa > out.hoa -diff out.hoa out.exp +res = spot.tra_to_tba(aut) +assert(res.to_str('hoa') == exp) -cat >test4.hoa <out.exp << EOF -HOA: v1 +exp = """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" @@ -168,13 +144,13 @@ State: 1 {0} [t] 1 State: 2 {0} [t] 2 ---END-- -EOF +--END--""" -run 0 ../tra2tba test4.hoa > out.hoa -diff out.hoa out.exp +res = spot.tra_to_tba(aut) +assert(res.to_str('hoa') == exp) -cat >test5.hoa <out.exp << EOF -HOA: v1 +exp = """HOA: v1 States: 4 Start: 0 AP: 3 "a" "b" "c" @@ -215,13 +190,13 @@ State: 2 {0} [t] 2 State: 3 {0} [t] 3 ---END-- -EOF +--END--""" -run 0 ../tra2tba test5.hoa > out.hoa -diff out.hoa out.exp +res = spot.tra_to_tba(aut) +assert(res.to_str('hoa') == exp) -cat >test6.hoa <out.exp << EOF -HOA: v1 +exp = """HOA: v1 States: 4 Start: 0 AP: 2 "p3" "p2" @@ -269,13 +243,13 @@ State: 2 State: 3 [0&1] 3 {0} [0&!1] 2 {0} ---END-- -EOF +--END--""" -run 0 ../tra2tba test6.hoa > out.hoa -diff out.hoa out.exp +res = spot.tra_to_tba(aut) +assert(res.to_str('hoa') == exp) -cat >test7.hoa <out.exp << EOF -HOA: v1 +exp = """HOA: v1 States: 2 Start: 0 AP: 1 "a" @@ -306,13 +279,13 @@ State: 0 [0] 1 State: 1 {0} [0] 1 ---END-- -EOF +--END--""" -run 0 ../tra2tba test7.hoa > out.hoa -diff out.hoa out.exp +res = spot.tra_to_tba(aut) +assert(res.to_str('hoa') == exp) -cat >test8.hoa <out.exp << EOF -HOA: v1 +exp = """HOA: v1 States: 8 Start: 0 AP: 3 "p0" "p2" "p3" @@ -386,13 +358,13 @@ State: 6 [!0] 4 State: 7 [0&2] 7 {0} ---END-- -EOF +--END--""" -run 0 ../tra2tba test8.hoa > out.hoa -diff out.hoa out.exp +res = spot.tra_to_tba(aut) +assert(res.to_str('hoa') == exp) -cat >test9.hoa <out.exp << EOF -HOA: v1 +exp = """HOA: v1 States: 2 Start: 0 -AP: 3 "p0" "p4" "p1" +AP: 3 "p4" "p0" "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 +[1&!2] 1 +[!1&!2] 0 State: 1 -[0&!2] 1 -[!0&!2] 0 ---END-- -EOF +[1&!2] 1 +[!1&!2] 0 +--END--""" -run 0 ../tra2tba test9.hoa > out.hoa -diff out.hoa out.exp +res = spot.tra_to_tba(aut) +assert(res.to_str('hoa') == exp) -cat >test10.hoa <out.exp << EOF -HOA: v1 +exp = """HOA: v1 States: 3 Start: 0 AP: 2 "p0" "p2" @@ -464,13 +434,13 @@ State: 1 {0} [1] 1 State: 2 {0} [0&1] 2 ---END-- -EOF +--END--""" -run 0 ../tra2tba test10.hoa > out.hoa -diff out.hoa out.exp +res = spot.tra_to_tba(aut) +assert(res.to_str('hoa') == exp) -cat >test11.hoa <out.exp << EOF -HOA: v1 +exp = """HOA: v1 States: 2 Start: 0 -AP: 2 "p2" "p0" +AP: 2 "p0" "p2" 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} +[0] 1 +[!0] 0 {0} State: 1 -[1] 1 {0} -[!1] 0 {0} ---END-- -EOF +[0] 1 {0} +[!0] 0 {0} +--END--""" -run 0 ../tra2tba test11.hoa > out.hoa -diff out.hoa out.exp +res = spot.tra_to_tba(aut) +assert(res.to_str('hoa') == exp) + +# Test 12. +aut = spot.automaton(""" +HOA: v1 +properties: deterministic +properties: complete +States: 2 +Start: 0 +Acceptance: 3 Fin(0) | Fin(1)&Inf(2) +AP: 2 "p2" "p0" +--BODY-- +State: 1 "1" +[1] 1 {0 1 2} +[!1] 0 {0 2} +State: 0 "3" +[1] 1 {1 2} +[!1] 0 {2} +--END-- +""") + +exp = """HOA: v1 +States: 4 +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 +[!0] 2 +[!0] 3 +State: 1 +[0] 1 +[!0] 0 +[!0] 3 +State: 2 +[!0] 2 +State: 3 {0} +[!0] 3 +--END--""" + +res = spot.tra_to_tba(aut) +assert(res.to_str('hoa') == exp) + +# Test 13. +aut = spot.automaton(""" +HOA: v1 +properties: deterministic +properties: complete +States: 2 +Start: 0 +Acceptance: 3 Inf(0) | Fin(1)&Inf(2) +AP: 2 "p3" "p2" +--BODY-- +State: 1 "F(Gp3|GFp2)" +[0&1] 1 {0 2} +[0&!1] 0 {0} +[!0&1] 1 {0 1 2} +[!0&!1] 0 {0 1 2} +State: 0 "F(Gp3|GFp2)" +[0&1] 1 {2} +[0&!1] 0 {0} +[!0&1] 1 {} +[!0&!1] 0 {2} +--END-- +""") + +res = spot.tra_to_tba(aut) +tba = spot.tgba_determinize(res) +a = spot.dtwa_complement(aut).intersects(tba) +b = spot.dtwa_complement(tba).intersects(aut) +assert(a == b)