diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 33a3065a4..3da677203 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -51,6 +51,7 @@ #include "twaalgos/canonicalize.hh" #include "twaalgos/mask.hh" #include "twaalgos/sbacc.hh" +#include "twaalgos/sepsets.hh" #include "twaalgos/stripacc.hh" #include "twaalgos/remfin.hh" #include "twaalgos/cleanacc.hh" @@ -93,6 +94,7 @@ enum { OPT_REM_FIN, OPT_SBACC, OPT_SEED, + OPT_SEP_SETS, OPT_SIMPLIFY_EXCLUSIVE_AP, OPT_STATES, OPT_STRIPACC, @@ -167,7 +169,9 @@ static const argp_option options[] = { "remove-dead-states", OPT_REM_DEAD, 0, 0, "remove states that are unreachable, or that cannot belong to an " "infinite path", 0 }, - /**************************************************/ + { "separate-sets", OPT_SEP_SETS, 0, 0, + "if both Inf(x) and Fin(x) appear in the acceptance condition, replace " + "Fin(x) by a new Fin(y) and adjust the automaton", 0 }, { 0, 0, 0, 0, "Filtering options:", 6 }, { "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0, "keep automata that are isomorphic to the automaton in FILENAME", 0 }, @@ -262,6 +266,7 @@ static spot::remove_ap rem_ap; static bool opt_simplify_exclusive_ap = false; static bool opt_rem_dead = false; static bool opt_rem_unreach = false; +static bool opt_sep_sets = false; static int parse_opt(int key, char* arg, struct argp_state*) @@ -438,6 +443,9 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_SEED: opt_seed = to_int(arg); break; + case OPT_SEP_SETS: + opt_sep_sets = true; + break; case OPT_SIMPLIFY_EXCLUSIVE_AP: opt_simplify_exclusive_ap = true; opt_merge = true; @@ -507,6 +515,8 @@ namespace aut->merge_transitions(); if (opt_clean_acc || opt_rem_fin) cleanup_acceptance_here(aut); + if (opt_sep_sets) + separate_sets_here(aut); if (opt_complement_acc) aut->set_acceptance(aut->acc().num_sets(), aut->get_acceptance().complement()); diff --git a/src/tests/Makefile.am b/src/tests/Makefile.am index 31527fffc..543fe6548 100644 --- a/src/tests/Makefile.am +++ b/src/tests/Makefile.am @@ -204,6 +204,7 @@ TESTS_twa = \ scc.test \ sccdot.test \ sccsimpl.test \ + sepsets.test \ dbacomp.test \ obligation.test \ wdba.test \ diff --git a/src/tests/sepsets.test b/src/tests/sepsets.test new file mode 100755 index 000000000..457e502e0 --- /dev/null +++ b/src/tests/sepsets.test @@ -0,0 +1,66 @@ +#!/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 + +cat >in <expected < out +diff out expected diff --git a/src/twa/acc.hh b/src/twa/acc.hh index 879e03e94..d759af105 100644 --- a/src/twa/acc.hh +++ b/src/twa/acc.hh @@ -744,6 +744,11 @@ namespace spot return code_; } + acc_code& get_acceptance() + { + return code_; + } + bool uses_fin_acceptance() const { return uses_fin_acceptance_; diff --git a/src/twaalgos/Makefile.am b/src/twaalgos/Makefile.am index ee8317328..b7c51bdd3 100644 --- a/src/twaalgos/Makefile.am +++ b/src/twaalgos/Makefile.am @@ -73,6 +73,7 @@ twaalgos_HEADERS = \ scc.hh \ sccinfo.hh \ se05.hh \ + sepsets.hh \ simulation.hh \ stats.hh \ stripacc.hh \ @@ -130,6 +131,7 @@ libtwaalgos_la_SOURCES = \ sccinfo.cc \ sccfilter.cc \ se05.cc \ + sepsets.cc \ simulation.cc \ stats.cc \ stripacc.cc \ diff --git a/src/twaalgos/sepsets.cc b/src/twaalgos/sepsets.cc new file mode 100644 index 000000000..e9d9051c0 --- /dev/null +++ b/src/twaalgos/sepsets.cc @@ -0,0 +1,101 @@ +// -*- 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 "sepsets.hh" +#include "sccinfo.hh" + + +namespace spot +{ + namespace + { + static acc_cond::mark_t common_sets(const const_twa_graph_ptr& aut) + { + auto p = aut->get_acceptance().used_inf_fin_sets(); + return p.first & p.second; + } + } + + bool has_separate_sets(const const_twa_graph_ptr& aut) + { + return common_sets(aut) == 0U; + } + + twa_graph_ptr + separate_sets_here(const twa_graph_ptr& aut) + { + auto common = common_sets(aut); + if (common == 0U) + return aut; + // Each Fin(first) should be replaced by Fin(second). + std::vector> map; + { + unsigned base = aut->acc().add_sets(common.count()); + for (auto s: common.sets()) + map.emplace_back(acc_cond::mark_t({s}), + acc_cond::mark_t({base++})); + } + + // Fix the acceptance condition + auto& code = aut->acc().get_acceptance(); + // If code were empty, then common would have been 0. + assert (!code.empty()); + acc_cond::acc_word* pos = &code.back(); + acc_cond::acc_word* start = &code.front(); + while (pos > start) + { + switch (pos->op) + { + case acc_cond::acc_op::Or: + case acc_cond::acc_op::And: + --pos; + break; + case acc_cond::acc_op::Fin: + case acc_cond::acc_op::FinNeg: + if ((pos[-1].mark & common) == 0U) + break; + for (auto p: map) + if (pos[-1].mark & p.first) + { + pos[-1].mark -= p.first; + pos[-1].mark |= p.second; + } + /* fall through */ + case acc_cond::acc_op::Inf: + case acc_cond::acc_op::InfNeg: + pos -= 2; + break; + } + } + + // Fix the transitions + for (auto& t: aut->transitions()) + { + if ((t.acc & common) == 0U) + continue; + for (auto p: map) + if (t.acc & p.first) + t.acc |= p.second; + } + return aut; + } + + + +} diff --git a/src/twaalgos/sepsets.hh b/src/twaalgos/sepsets.hh new file mode 100644 index 000000000..334f7d489 --- /dev/null +++ b/src/twaalgos/sepsets.hh @@ -0,0 +1,36 @@ +// -*- 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 "twa/twagraph.hh" + +namespace spot +{ + /// \brief Whether the Inf and Fin numbers are disjoints + SPOT_API bool + has_separate_sets(const const_twa_graph_ptr& aut); + + /// \brief Separate the Fin and Inf sets used by an automaton + /// + /// This makes sure that the numbers used a Fin and Inf are + /// disjoints. + SPOT_API twa_graph_ptr + separate_sets_here(const twa_graph_ptr& aut); +}