diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 5d4f5adc7..084f228cd 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -47,6 +47,7 @@ #include "tgbaalgos/are_isomorphic.hh" #include "tgbaalgos/canonicalize.hh" #include "tgbaalgos/mask.hh" +#include "tgbaalgos/sbacc.hh" static const char argp_program_doc[] ="\ @@ -74,6 +75,7 @@ Exit status:\n\ #define OPT_IS_EMPTY 15 #define OPT_INTERSECT 16 #define OPT_MASK_ACC 17 +#define OPT_SBACC 18 static const argp_option options[] = { @@ -105,6 +107,9 @@ static const argp_option options[] = { "destut", OPT_DESTUT, 0, 0, "allow less stuttering", 0 }, { "mask-acc", OPT_MASK_ACC, "NUM[,NUM...]", 0, "remove all transitions in specified acceptance sets", 0 }, + { "state-based-acceptance", OPT_SBACC, 0, 0, + "define the acceptance using states", 0 }, + { "sbacc", 0, 0, OPTION_ALIAS, 0, 0 }, /**************************************************/ { 0, 0, 0, 0, "Filtering options:", 6 }, { "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0, @@ -172,6 +177,7 @@ static int opt_max_count = -1; static bool opt_destut = false; static char opt_instut = 0; static bool opt_is_empty = false; +static bool opt_sbacc = false; static std::unique_ptr opt_uniq = nullptr; static spot::acc_cond::mark_t opt_mask_acc = 0U; @@ -299,6 +305,9 @@ parse_opt(int key, char* arg, struct argp_state*) randomize_st = true; } break; + case OPT_SBACC: + opt_sbacc = true; + break; case OPT_SEED: opt_seed = to_int(arg); break; @@ -399,6 +408,9 @@ namespace if (opt_product) aut = spot::product(std::move(aut), opt_product); + if (opt_sbacc) + aut = spot::sbacc(aut); + aut = post.run(aut, nullptr); if (randomize_st || randomize_tr) diff --git a/src/tgba/tgbagraph.hh b/src/tgba/tgbagraph.hh index 4c875b385..a82fc9e47 100644 --- a/src/tgba/tgbagraph.hh +++ b/src/tgba/tgbagraph.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014 Laboratoire de Recherche et Développement de -// l'Epita. +// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement +// de l'Epita. // // This file is part of Spot, a model checking library. // @@ -429,8 +429,7 @@ namespace spot /// \brief Copy the acceptance conditions of another tgba. void copy_acceptance_conditions_of(const const_tgba_ptr& a) { - assert(acc_.num_sets() == 0); - acc_.add_sets(a->acc().num_sets()); + set_acceptance_conditions(a->acc().num_sets()); } void copy_ap_of(const const_tgba_ptr& a) diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 38c3bdd3f..ec93a6260 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -64,6 +64,7 @@ tgbaalgos_HEADERS = \ relabel.hh \ replayrun.hh \ safety.hh \ + sbacc.hh \ sccfilter.hh \ scc.hh \ sccinfo.hh \ @@ -115,6 +116,7 @@ libtgbaalgos_la_SOURCES = \ replayrun.cc \ relabel.cc \ safety.cc \ + sbacc.cc \ scc.cc \ sccinfo.cc \ sccfilter.cc \ diff --git a/src/tgbaalgos/sbacc.cc b/src/tgbaalgos/sbacc.cc new file mode 100644 index 000000000..2a107dc2f --- /dev/null +++ b/src/tgbaalgos/sbacc.cc @@ -0,0 +1,79 @@ +// -*- 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 +#include +#include +#include "sbacc.hh" + +namespace spot +{ + tgba_digraph_ptr sbacc(tgba_digraph_ptr& old) + { + if (old->has_state_based_acc()) + return old; + + auto res = make_tgba_digraph(old->get_dict()); + res->copy_ap_of(old); + res->copy_acceptance_conditions_of(old); + + typedef std::pair pair_t; + std::map s2n; + + std::vector> todo; + + auto new_state = + [&](unsigned state, acc_cond::mark_t m) -> unsigned + { + pair_t x(state, m); + auto p = s2n.emplace(x, 0); + if (p.second) // This is a new state + { + unsigned s = res->new_state(); + p.first->second = s; + todo.emplace_back(x, s); + } + return p.first->second; + }; + + // Find any transition going into the initial state, and use its + // acceptance as mark. + acc_cond::mark_t init_acc = 0U; + unsigned old_init = old->get_init_state_number(); + for (auto& t: old->transitions()) + if (t.dst == old_init) + { + init_acc = t.acc; + break; + } + + res->set_init_state(new_state(old_init, init_acc)); + while (!todo.empty()) + { + auto one = todo.back(); + todo.pop_back(); + for (auto& t: old->out(one.first.first)) + res->new_transition(one.second, + new_state(t.dst, t.acc), + t.cond, + one.first.second); + } + return res; + } +} diff --git a/src/tgbaalgos/sbacc.hh b/src/tgbaalgos/sbacc.hh new file mode 100644 index 000000000..230aa4f1a --- /dev/null +++ b/src/tgbaalgos/sbacc.hh @@ -0,0 +1,33 @@ +// -*- 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 . + +#ifndef SPOT_TGBAALGOS_SBACC_HH +# define SPOT_TGBAALGOS_SBACC_HH + +#include "tgba/tgbagraph.hh" + +namespace spot +{ + /// \brief Transform an automaton to use state-based acceptance + /// + /// This is independent on the acceptance condition used. + SPOT_API tgba_digraph_ptr sbacc(tgba_digraph_ptr& aut); +} + +#endif // SPOT_TGBAALGOS_COMPLETE_HH diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index e93042392..dd2307e65 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -112,6 +112,7 @@ TESTS = \ randtgba.test \ isomorph.test \ uniq.test \ + sbacc.test \ stutter.test \ emptchk.test \ emptchke.test \ diff --git a/src/tgbatest/sbacc.test b/src/tgbatest/sbacc.test new file mode 100755 index 000000000..d38a9c12d --- /dev/null +++ b/src/tgbatest/sbacc.test @@ -0,0 +1,108 @@ +#! /bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2015 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 || exit 1 + +set -e + +ltl2tgba=../../bin/ltl2tgba +autfilt=../../bin/autfilt + +$ltl2tgba 'GFa & GFb' -H | run 0 $autfilt --sbacc -H > out.hoa + +cat >expected<in.hoa< out.hoa + +cat >expected < out.hoa +diff out.hoa expected + + + +../../bin/randltl --weak-fairness -n 20 2 | +../../bin/ltlcross "$ltl2tgba -DH %f >%O" "$ltl2tgba -H %f | $autfilt -H >%O"