From e589e208bd81a1af5fc8e34b53668d0956b24d75 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 2 Apr 2015 22:23:18 +0200 Subject: [PATCH] new transformation from Fin-less to TGBA Fixes #72. * src/tgbaalgos/totgba.cc, src/tgbaalgos/totgba.hh: New files. * src/tgbaalgos/Makefile.am: Add them. * src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: Add a Generic output type, and call to_generalized_buchi() if this type is not selected. * src/tgbatest/remfin.test: Add some tests. * src/bin/autfilt.cc: Add a --generic option, and set it by default. --- src/bin/autfilt.cc | 9 ++- src/tgbaalgos/Makefile.am | 2 + src/tgbaalgos/postproc.cc | 7 +- src/tgbaalgos/postproc.hh | 2 +- src/tgbaalgos/totgba.cc | 94 +++++++++++++++++++++++ src/tgbaalgos/totgba.hh | 30 ++++++++ src/tgbatest/remfin.test | 155 ++++++++++++++++++++++++++++++++++++++ 7 files changed, 296 insertions(+), 3 deletions(-) create mode 100644 src/tgbaalgos/totgba.cc create mode 100644 src/tgbaalgos/totgba.hh 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