Commit 69cf3c55 authored by Henrich Lauko's avatar Henrich Lauko Committed by Alexandre Duret-Lutz
Browse files

tra2tba: Add support for Rabin like automata

* spot/twaalgos/tra2tba.cc: Support Rabin like input
* tests/core/tra2tba.cc: Remove C tests
* tests/core/tra2tba.test: Remove C tests
* tests/python/tra2tba.py: Convert C tests to python
* tests/Makefile.am: Remove C tests and add python tests
parent e1271bf8
...@@ -108,6 +108,7 @@ namespace spot ...@@ -108,6 +108,7 @@ namespace spot
bool is_scc_tba_type(const const_twa_graph_ptr& aut, bool is_scc_tba_type(const const_twa_graph_ptr& aut,
const scc_info& si, const scc_info& si,
const unsigned scc, const unsigned scc,
const acc_cond::mark_t fin_alone,
std::vector<bool>& final) std::vector<bool>& final)
{ {
if (si.is_rejecting_scc(scc)) if (si.is_rejecting_scc(scc))
...@@ -115,9 +116,18 @@ namespace spot ...@@ -115,9 +116,18 @@ namespace spot
auto acc_pairs = aut->get_acceptance().used_inf_fin_sets(); auto acc_pairs = aut->get_acceptance().used_inf_fin_sets();
auto infs = si.acc(scc) & acc_pairs.first; 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; auto infs_with_fins = (si.acc(scc) << 1U) & acc_pairs.first;
infs -= infs_with_fins; 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); auto& states = si.states_of(scc);
// Firstly consider whole SCC as one large cycle. // Firstly consider whole SCC as one large cycle.
// If there is no inf without matching fin then the cycle formed // If there is no inf without matching fin then the cycle formed
...@@ -172,7 +182,7 @@ namespace spot ...@@ -172,7 +182,7 @@ namespace spot
} }
if (si.is_rejecting_scc(uscc)) if (si.is_rejecting_scc(uscc))
continue; continue;
if (!is_scc_tba_type(aut, si, uscc, final)) if (!is_scc_tba_type(aut, si, uscc, fin_alone, final))
return false; return false;
} }
} }
...@@ -202,6 +212,7 @@ namespace spot ...@@ -202,6 +212,7 @@ namespace spot
{ {
if (aut->prop_state_acc().is_true()) if (aut->prop_state_acc().is_true())
return nullptr; return nullptr;
std::vector<acc_cond::rs_pair> pairs; std::vector<acc_cond::rs_pair> pairs;
if (!aut->acc().is_rabin_like(pairs)) if (!aut->acc().is_rabin_like(pairs))
return nullptr; return nullptr;
...@@ -215,9 +226,17 @@ namespace spot ...@@ -215,9 +226,17 @@ namespace spot
std::vector<bool> scc_is_tba_type(si.scc_count(), false); std::vector<bool> scc_is_tba_type(si.scc_count(), false);
std::vector<bool> final(aut->edge_vector().size(), false); std::vector<bool> 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) 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 // compute final edges
auto res = make_twa_graph(aut->get_dict()); auto res = make_twa_graph(aut->get_dict());
......
...@@ -92,7 +92,6 @@ check_PROGRAMS = \ ...@@ -92,7 +92,6 @@ check_PROGRAMS = \
core/sccif \ core/sccif \
core/syntimpl \ core/syntimpl \
core/taatgba \ core/taatgba \
core/tra2tba \
core/trival \ core/trival \
core/tgbagraph \ core/tgbagraph \
core/tostring \ core/tostring \
...@@ -140,7 +139,6 @@ core_safra_SOURCES = core/safra.cc ...@@ -140,7 +139,6 @@ core_safra_SOURCES = core/safra.cc
core_sccif_SOURCES = core/sccif.cc core_sccif_SOURCES = core/sccif.cc
core_syntimpl_SOURCES = core/syntimpl.cc core_syntimpl_SOURCES = core/syntimpl.cc
core_tostring_SOURCES = core/tostring.cc core_tostring_SOURCES = core/tostring.cc
core_tra2tba_SOURCES = core/tra2tba.cc
core_trival_SOURCES = core/trival.cc core_trival_SOURCES = core/trival.cc
core_tunabbrev_SOURCES = core/equalsf.cc core_tunabbrev_SOURCES = core/equalsf.cc
core_tunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DUNABBREV='"^ieFG"' core_tunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DUNABBREV='"^ieFG"'
...@@ -298,8 +296,7 @@ TESTS_twa = \ ...@@ -298,8 +296,7 @@ TESTS_twa = \
core/complementation.test \ core/complementation.test \
core/randpsl.test \ core/randpsl.test \
core/cycles.test \ core/cycles.test \
core/acc_word.test \ core/acc_word.test
core/tra2tba.test
############################## PYTHON ############################## ############################## PYTHON ##############################
...@@ -372,6 +369,7 @@ TESTS_python = \ ...@@ -372,6 +369,7 @@ TESTS_python = \
python/rs_like.py \ python/rs_like.py \
python/sum.py \ python/sum.py \
python/trival.py \ python/trival.py \
python/tra2tba.py \
python/twagraph.py \ python/twagraph.py \
$(TESTS_ipython) $(TESTS_ipython)
endif endif
......
// -*- 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 <http://www.gnu.org/licenses/>.
#include <iostream>
#include <spot/parseaut/public.hh>
#include <spot/twaalgos/tra2tba.hh>
#include <spot/twaalgos/hoa.hh>
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;
}
#!/bin/sh import spot
# -*- coding: utf-8 -*-
# Copyright (C) 2017 Laboratoire de Recherche et Développement # Test 1.
# de l'Epita (LRDE). aut = spot.automaton("""
#
# 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 <http://www.gnu.org/licenses/>.
. ./defs
set -e
cat >test1.hoa <<EOF
HOA: v1 HOA: v1
States: 2 States: 2
Start: 0 Start: 0
...@@ -35,10 +14,9 @@ State: 0 ...@@ -35,10 +14,9 @@ State: 0
State: 1 State: 1
[0] 1 {0} [0] 1 {0}
--END-- --END--
EOF """)
cat >out.exp << EOF exp = """HOA: v1
HOA: v1
States: 2 States: 2
Start: 0 Start: 0
AP: 2 "a" "b" AP: 2 "a" "b"
...@@ -51,13 +29,13 @@ State: 0 ...@@ -51,13 +29,13 @@ State: 0
[0] 1 [0] 1
State: 1 State: 1
[0] 1 [0] 1
--END-- --END--"""
EOF
run 0 ../tra2tba test1.hoa > out.hoa res = spot.tra_to_tba(aut)
diff out.hoa out.exp assert(res.to_str('hoa') == exp)
cat >test2.hoa <<EOF # Test 2.
aut = spot.automaton("""
HOA: v1 HOA: v1
States: 3 States: 3
Start: 0 Start: 0
...@@ -74,9 +52,9 @@ State: 2 ...@@ -74,9 +52,9 @@ State: 2
[0] 2 {1} [0] 2 {1}
--END-- --END--
EOF EOF
""")
cat >out.exp << EOF exp = """HOA: v1
HOA: v1
States: 3 States: 3
Start: 0 Start: 0
AP: 1 "a" AP: 1 "a"
...@@ -92,13 +70,13 @@ State: 1 ...@@ -92,13 +70,13 @@ State: 1
State: 2 State: 2
[!0] 1 [!0] 1
[0] 2 {0} [0] 2 {0}
--END-- --END--"""
EOF
run 0 ../tra2tba test2.hoa > out.hoa res = spot.tra_to_tba(aut)
diff out.hoa out.exp assert(res.to_str('hoa') == exp)
cat >test3.hoa <<EOF # Test 3.
aut = spot.automaton("""
HOA: v1 HOA: v1
States: 2 States: 2
Start: 0 Start: 0
...@@ -111,10 +89,9 @@ State: 0 ...@@ -111,10 +89,9 @@ State: 0
State: 1 State: 1
[0] 1 {2} [0] 1 {2}
--END-- --END--
EOF """)
cat >out.exp << EOF exp = """HOA: v1
HOA: v1
States: 2 States: 2
Start: 0 Start: 0
AP: 2 "a" "b" AP: 2 "a" "b"
...@@ -127,13 +104,13 @@ State: 0 ...@@ -127,13 +104,13 @@ State: 0
[0] 1 [0] 1
State: 1 State: 1
[0] 1 [0] 1
--END-- --END--"""
EOF
run 0 ../tra2tba test3.hoa > out.hoa res = spot.tra_to_tba(aut)
diff out.hoa out.exp assert(res.to_str('hoa') == exp)
cat >test4.hoa <<EOF # Test 4.
aut = spot.automaton("""
HOA: v1 HOA: v1
States: 3 States: 3
Start: 0 Start: 0
...@@ -149,10 +126,9 @@ State: 1 ...@@ -149,10 +126,9 @@ State: 1
State: 2 State: 2
[t] 2 {3} [t] 2 {3}
--END-- --END--
EOF """)
cat >out.exp << EOF exp = """HOA: v1
HOA: v1
States: 3 States: 3
Start: 0 Start: 0
AP: 2 "a" "b" AP: 2 "a" "b"
...@@ -168,13 +144,13 @@ State: 1 {0} ...@@ -168,13 +144,13 @@ State: 1 {0}
[t] 1 [t] 1
State: 2 {0} State: 2 {0}
[t] 2 [t] 2
--END-- --END--"""
EOF
run 0 ../tra2tba test4.hoa > out.hoa res = spot.tra_to_tba(aut)
diff out.hoa out.exp assert(res.to_str('hoa') == exp)
cat >test5.hoa <<EOF # Test 5.
aut = spot.automaton("""
HOA: v1 HOA: v1
States: 4 States: 4
Start: 0 Start: 0
...@@ -193,10 +169,9 @@ State: 2 ...@@ -193,10 +169,9 @@ State: 2
State: 3 State: 3
[t] 3 {5} [t] 3 {5}
--END-- --END--
EOF """)
cat >out.exp << EOF exp = """HOA: v1
HOA: v1
States: 4 States: 4
Start: 0 Start: 0
AP: 3 "a" "b" "c" AP: 3 "a" "b" "c"
...@@ -215,13 +190,13 @@ State: 2 {0} ...@@ -215,13 +190,13 @@ State: 2 {0}
[t] 2 [t] 2
State: 3 {0} State: 3 {0}
[t] 3 [t] 3
--END-- --END--"""
EOF
run 0 ../tra2tba test5.hoa > out.hoa res = spot.tra_to_tba(aut)
diff out.hoa out.exp assert(res.to_str('hoa') == exp)
cat >test6.hoa <<EOF # Test 6.
aut = spot.automaton("""
HOA: v1 HOA: v1
States: 2 States: 2
Start: 0 Start: 0
...@@ -239,10 +214,9 @@ State: 0 "F(Gp3|GFp2)" ...@@ -239,10 +214,9 @@ State: 0 "F(Gp3|GFp2)"
[!0&1] 1 {2 3 } [!0&1] 1 {2 3 }
[!0&!1] 0 {2 3 } [!0&!1] 0 {2 3 }
--END-- --END--
EOF """)
cat >out.exp << EOF exp = """HOA: v1
HOA: v1
States: 4 States: 4
Start: 0 Start: 0
AP: 2 "p3" "p2" AP: 2 "p3" "p2"
...@@ -269,13 +243,13 @@ State: 2 ...@@ -269,13 +243,13 @@ State: 2
State: 3 State: 3
[0&1] 3 {0} [0&1] 3 {0}
[0&!1] 2 {0} [0&!1] 2 {0}
--END-- --END--"""
EOF
run 0 ../tra2tba test6.hoa > out.hoa res = spot.tra_to_tba(aut)
diff out.hoa out.exp assert(res.to_str('hoa') == exp)
cat >test7.hoa <<EOF # Test 7.
aut = spot.automaton("""
HOA: v1 HOA: v1
name: "FG(a)" name: "FG(a)"
properties: deterministic properties: deterministic
...@@ -289,10 +263,9 @@ State: 0 "FG(a)" ...@@ -289,10 +263,9 @@ State: 0 "FG(a)"
[0] 0 {1 } [0] 0 {1 }
[!0] 0 {0 1 } [!0] 0 {0 1 }
--END-- --END--
EOF """)
cat >out.exp << EOF exp = """HOA: v1
HOA: v1
States: 2 States: 2
Start: 0 Start: 0
AP: 1 "a" AP: 1 "a"
...@@ -306,13 +279,13 @@ State: 0 ...@@ -306,13 +279,13 @@ State: 0
[0] 1 [0] 1
State: 1 {0} State: 1 {0}
[0] 1 [0] 1
--END-- --END--"""
EOF
run 0 ../tra2tba test7.hoa > out.hoa res = spot.tra_to_tba(aut)
diff out.hoa out.exp assert(res.to_str('hoa') == exp)
cat >test8.hoa <<EOF # Test 8.
aut = spot.automaton("""
HOA: v1 HOA: v1
States: 7 States: 7
Start: 0 Start: 0
...@@ -346,10 +319,9 @@ State: 3 "6" ...@@ -346,10 +319,9 @@ State: 3 "6"
[!0&2] 3 {0 1 2 } [!0&2] 3 {0 1 2 }
[!2] 4 {0 1 2 } [!2] 4 {0 1 2 }
--END-- --END--
EOF """)
cat >out.exp << EOF exp = """HOA: v1
HOA: v1
States: 8 States: 8
Start: 0 Start: 0
AP: 3 "p0" "p2" "p3" AP: 3 "p0" "p2" "p3"
...@@ -386,13 +358,13 @@ State: 6 ...@@ -386,13 +358,13 @@ State: 6
[!0] 4 [!0] 4
State: 7 State: 7
[0&2] 7 {0} [0&2] 7 {0}
--END-- --END--"""
EOF
run 0 ../tra2tba test8.hoa > out.hoa res = spot.tra_to_tba(aut)
diff out.hoa out.exp assert(res.to_str('hoa') == exp)
cat >test9.hoa <<EOF # Test 9.
aut = spot.automaton("""
HOA: v1 HOA: v1
States: 2 States: 2
Start: 0 Start: 0
...@@ -406,30 +378,29 @@ State: 1 ...@@ -406,30 +378,29 @@ State: 1
[0&!2] 1 {0 1} [0&!2] 1 {0 1}
[!0&!2] 0 {0 1} [!0&!2] 0 {0 1}
--END-- --END--
EOF """)
cat >out.exp << EOF exp = """HOA: v1
HOA: v1
States: 2 States: 2
Start: 0 Start: 0
AP: 3 "p0" "p4" "p1" AP: 3 "p4" "p0" "p1"
acc-name: Buchi acc-name: Buchi
Acceptance: 1 Inf(0) Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic properties: trans-labels explicit-labels state-acc deterministic
--BODY-- --BODY--
State: 0 {0} State: 0 {0}
[0&!2] 1 [1&!2] 1
[!0&!2] 0 [!1&!2] 0
State: 1 State: 1
[0&!2] 1 [1&!2] 1
[!0&!2] 0 [!1&!2] 0
--END-- --END--"""
EOF
run 0 ../tra2tba test9.hoa > out.hoa res = spot.tra_to_tba(aut)
diff out.hoa out.exp assert(res.to_str('hoa') == exp)
cat >test10.hoa <<EOF # Test 10.
aut = spot.automaton("""
HOA: v1 HOA: v1
States: 2 States: 2
Start: 0 Start: 0
...@@ -444,10 +415,9 @@ State: 0 "0" ...@@ -444,10 +415,9 @@ State: 0 "0"
State: 1 "1" State: 1 "1"
[1] 1 {1 } [1] 1 {1 }
--END-- --END--
EOF """)
cat >out.exp << EOF exp = """HOA: v1
HOA: v1
States: 3 States: 3
Start: 0 Start: 0
AP: 2 "p0" "p2" AP: 2 "p0" "p2"
...@@ -464,13 +434,13 @@ State: 1 {0} ...@@ -464,13 +434,13 @@ State: 1 {0}
[1] 1 [1] 1
State: 2 {0} State: 2 {0}
[0&1] 2 [0&1] 2
--END-- --END--"""