diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc
index 4da23a865..716090130 100644
--- a/src/bin/autfilt.cc
+++ b/src/bin/autfilt.cc
@@ -74,6 +74,7 @@ enum {
OPT_DNF_ACC,
OPT_EDGES,
OPT_EXCLUSIVE_AP,
+ OPT_GENERIC,
OPT_INSTUT,
OPT_INTERSECT,
OPT_IS_COMPLETE,
@@ -102,8 +103,10 @@ static const argp_option options[] =
"process the automaton in FILENAME", 0 },
/**************************************************/
{ 0, 0, 0, 0, "Output automaton type:", 2 },
+ { "generic", OPT_GENERIC, 0, 0,
+ "Any acceptance is allowed (default)", 0 },
{ "tgba", OPT_TGBA, 0, 0,
- "Transition-based Generalized Büchi Automaton (default)", 0 },
+ "Transition-based Generalized Büchi Automaton", 0 },
{ "ba", 'B', 0, 0, "Büchi Automaton", 0 },
{ "monitor", 'M', 0, 0, "Monitor (accepts all finite prefixes "
"of the given property)", 0 },
@@ -310,6 +313,8 @@ parse_opt(int key, char* arg, struct argp_state*)
case OPT_EXCLUSIVE_AP:
excl_ap.add_group(arg);
break;
+ case OPT_GENERIC:
+ type = spot::postprocessor::Generic;
case OPT_INSTUT:
if (!arg || (arg[0] == '1' && arg[1] == 0))
opt_instut = 1;
@@ -423,6 +428,7 @@ parse_opt(int key, char* arg, struct argp_state*)
if (automaton_format == Spin)
error(2, 0, "--spin and --tgba are incompatible");
type = spot::postprocessor::TGBA;
+ opt_rem_fin = true;
break;
case ARGP_KEY_ARG:
jobs.emplace_back(arg, true);
@@ -621,6 +627,7 @@ main(int argc, char** argv)
// Disable post-processing as much as possible by default.
level = spot::postprocessor::Low;
pref = spot::postprocessor::Any;
+ type = spot::postprocessor::Generic;
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0))
exit(err);
diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am
index 56ca96595..8dd060122 100644
--- a/src/tgbaalgos/Makefile.am
+++ b/src/tgbaalgos/Makefile.am
@@ -78,6 +78,7 @@ tgbaalgos_HEADERS = \
stutter.hh \
tau03.hh \
tau03opt.hh \
+ totgba.hh \
translate.hh \
word.hh
@@ -133,6 +134,7 @@ libtgbaalgos_la_SOURCES = \
stutter.cc \
tau03.cc \
tau03opt.cc \
+ totgba.cc \
translate.cc \
weight.cc \
weight.hh \
diff --git a/src/tgbaalgos/postproc.cc b/src/tgbaalgos/postproc.cc
index cee662cdd..00357ce03 100644
--- a/src/tgbaalgos/postproc.cc
+++ b/src/tgbaalgos/postproc.cc
@@ -30,6 +30,7 @@
#include "dtbasat.hh"
#include "dtgbasat.hh"
#include "complete.hh"
+#include "totgba.hh"
namespace spot
{
@@ -140,8 +141,12 @@ namespace spot
tgba_digraph_ptr
postprocessor::run(tgba_digraph_ptr a, const ltl::formula* f)
{
+ if (type_ != Generic && !a->acc().is_generalized_buchi())
+ a = to_generalized_buchi(a);
+
if (PREF_ == Any && level_ == Low)
- if (type_ == TGBA
+ if (type_ == Generic
+ || type_ == TGBA
|| (type_ == BA && a->is_sba())
|| (type_ == Monitor && a->acc().num_sets() == 0))
{
diff --git a/src/tgbaalgos/postproc.hh b/src/tgbaalgos/postproc.hh
index 90568da2f..71a7e5e8f 100644
--- a/src/tgbaalgos/postproc.hh
+++ b/src/tgbaalgos/postproc.hh
@@ -64,7 +64,7 @@ namespace spot
/// options used for debugging or benchmarking.
postprocessor(const option_map* opt = 0);
- enum output_type { TGBA, BA, Monitor };
+ enum output_type { TGBA, BA, Monitor, Generic };
void
set_type(output_type type)
{
diff --git a/src/tgbaalgos/totgba.cc b/src/tgbaalgos/totgba.cc
new file mode 100644
index 000000000..3b54195f3
--- /dev/null
+++ b/src/tgbaalgos/totgba.cc
@@ -0,0 +1,94 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2015 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 "totgba.hh"
+#include "remfin.hh"
+#include "cleanacc.hh"
+#include "tgba/tgbagraph.hh"
+
+namespace spot
+{
+ namespace
+ {
+ typedef std::vector terms_t;
+
+ terms_t cnf_terms(const acc_cond::acc_code& code)
+ {
+ assert(!code.empty());
+ terms_t res;
+ auto pos = &code.back();
+ auto end = &code.front();
+ if (pos->op == acc_cond::acc_op::And)
+ --pos;
+ while (pos >= end)
+ {
+ auto term_end = pos - 1 - pos->size;
+ if (pos->op == acc_cond::acc_op::Or)
+ --pos;
+ acc_cond::mark_t m = 0U;
+ while (pos > term_end)
+ {
+ assert(pos->op == acc_cond::acc_op::Inf);
+ m |= pos[-1].mark;
+ pos -= 2;
+ }
+ res.push_back(m);
+ }
+ return res;
+ }
+ }
+
+
+
+ /// \brief Take an automaton with any acceptance condition and return
+ /// an equivalent Generalized Büchi automaton.
+ tgba_digraph_ptr
+ to_generalized_buchi(const const_tgba_digraph_ptr& aut)
+ {
+ auto res = remove_fin(cleanup_acceptance(aut));
+ if (res->acc().is_generalized_buchi())
+ return res;
+
+ auto cnf = res->get_acceptance().to_cnf();
+ // If we are very lucky, building a CNF actually gave us a GBA...
+ if (cnf.empty() ||
+ (cnf.size() == 2 && cnf.back().op == acc_cond::acc_op::Fin))
+ {
+ res->set_acceptance(res->acc().num_sets(), cnf);
+ cleanup_acceptance_here(res);
+ return res;
+ }
+
+ auto terms = cnf_terms(cnf);
+ unsigned nterms = terms.size();
+ assert(nterms > 0);
+ res->set_generalized_buchi(nterms);
+
+ for (auto& t: res->transitions())
+ {
+ acc_cond::mark_t cur_m = t.acc;
+ acc_cond::mark_t new_m = 0U;
+ for (unsigned n = 0; n < nterms; ++n)
+ if (cur_m & terms[n])
+ new_m.set(n);
+ t.acc = new_m;
+ }
+ return res;
+ }
+}
diff --git a/src/tgbaalgos/totgba.hh b/src/tgbaalgos/totgba.hh
new file mode 100644
index 000000000..b05e35cca
--- /dev/null
+++ b/src/tgbaalgos/totgba.hh
@@ -0,0 +1,30 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2015 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 "tgba/tgbagraph.hh"
+
+namespace spot
+{
+ /// \brief Take an automaton with any acceptance condition and return
+ /// an equivalent Generalized Büchi automaton.
+ SPOT_API tgba_digraph_ptr
+ to_generalized_buchi(const const_tgba_digraph_ptr& aut);
+}
diff --git a/src/tgbatest/remfin.test b/src/tgbatest/remfin.test
index 0c6d68a02..da241d870 100755
--- a/src/tgbatest/remfin.test
+++ b/src/tgbatest/remfin.test
@@ -308,6 +308,161 @@ State: 9 {1}
--END--
EOF
+cat >expected-tgba < output
cat output
diff -u output expected
+
+run 0 $autfilt -H --tgba test1 > output
+cat output
+diff -u output expected-tgba