From 85508a0ea6e6da090f0c1f556d475e2c6a5997a9 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 24 Feb 2015 09:10:20 +0100 Subject: [PATCH] Add a remove_fin() algorithm * src/bin/autfilt.cc: Add remove_fin(). * src/tgba/acc.cc, src/tgba/acc.hh: Add is_dnf() and simplify eval(). * src/tgbaalgos/remfin.cc, src/tgbaalgos/remfin.hh: New files. * src/tgbaalgos/Makefile.am: Add them. * src/tgbatest/remfin.test: New file. * src/tgbatest/Makefile.am: Add it. --- src/bin/autfilt.cc | 10 ++ src/tgba/acc.cc | 68 ++++++--- src/tgba/acc.hh | 4 +- src/tgbaalgos/Makefile.am | 2 + src/tgbaalgos/remfin.cc | 308 ++++++++++++++++++++++++++++++++++++++ src/tgbaalgos/remfin.hh | 32 ++++ src/tgbatest/Makefile.am | 1 + src/tgbatest/remfin.test | 266 ++++++++++++++++++++++++++++++++ 8 files changed, 667 insertions(+), 24 deletions(-) create mode 100644 src/tgbaalgos/remfin.cc create mode 100644 src/tgbaalgos/remfin.hh create mode 100755 src/tgbatest/remfin.test diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index b40b07de0..acd9bf9f7 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -49,6 +49,7 @@ #include "tgbaalgos/mask.hh" #include "tgbaalgos/sbacc.hh" #include "tgbaalgos/stripacc.hh" +#include "tgbaalgos/remfin.hh" static const char argp_program_doc[] ="\ @@ -80,6 +81,7 @@ Exit status:\n\ #define OPT_STRIPACC 19 #define OPT_KEEP_STATES 20 #define OPT_DNF_ACC 21 +#define OPT_REM_FIN 22 static const argp_option options[] = { @@ -121,6 +123,8 @@ static const argp_option options[] = "initial state", 0 }, { "dnf-acceptance", OPT_DNF_ACC, 0, 0, "put the acceptance condition in Disjunctive Normal Form", 0 }, + { "remove-fin", OPT_REM_FIN, 0, 0, + "rewrite the automaton without using Fin acceptance", 0 }, /**************************************************/ { 0, 0, 0, 0, "Filtering options:", 6 }, { "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0, @@ -201,6 +205,7 @@ static bool opt_is_empty = false; static bool opt_sbacc = false; static bool opt_stripacc = false; static bool opt_dnf_acc = false; +static bool opt_rem_fin = false; static spot::acc_cond::mark_t opt_mask_acc = 0U; static std::vector opt_keep_states = {}; static unsigned int opt_keep_states_initial = 0; @@ -342,6 +347,9 @@ parse_opt(int key, char* arg, struct argp_state*) randomize_st = true; } break; + case OPT_REM_FIN: + opt_rem_fin = true; + break; case OPT_SBACC: opt_sbacc = true; break; @@ -413,6 +421,8 @@ namespace if (opt_dnf_acc) aut->set_acceptance(aut->acc().num_sets(), aut->get_acceptance().to_dnf()); + if (opt_rem_fin) + aut = remove_fin(aut); // Filters. diff --git a/src/tgba/acc.cc b/src/tgba/acc.cc index 4bf52a504..54a8060f3 100644 --- a/src/tgba/acc.cc +++ b/src/tgba/acc.cc @@ -149,40 +149,38 @@ namespace spot static bool - eval(acc_cond::mark_t inf, acc_cond::mark_t fin, - const acc_cond::acc_code& code, unsigned pos) + eval(acc_cond::mark_t inf, const acc_cond::acc_word* pos) { - auto& w = code[pos]; - switch (w.op) + switch (pos->op) { case acc_cond::acc_op::And: { - unsigned sub = pos - w.size; + auto sub = pos - pos->size; while (sub < pos) { --pos; - if (!eval(inf, fin, code, pos)) + if (!eval(inf, pos)) return false; - pos -= code[pos].size; + pos -= pos->size; } return true; } case acc_cond::acc_op::Or: { - unsigned sub = pos - w.size; + auto sub = pos - pos->size; while (sub < pos) { --pos; - if (eval(inf, fin, code, pos)) + if (eval(inf, pos)) return true; - pos -= code[pos].size; + pos -= pos->size; } return false; } case acc_cond::acc_op::Inf: - return (code[pos - 1].mark & inf) == code[pos - 1].mark; + return (pos[-1].mark & inf) == pos[-1].mark; case acc_cond::acc_op::Fin: - return (code[pos - 1].mark & fin) != 0U; + return (pos[-1].mark & inf) == 0U; case acc_cond::acc_op::FinNeg: case acc_cond::acc_op::InfNeg: SPOT_UNREACHABLE(); @@ -192,19 +190,11 @@ namespace spot } } - bool acc_cond::accepting(mark_t inf, mark_t fin) const + bool acc_cond::accepting(mark_t inf) const { if (code_.empty()) return true; - return eval(inf, fin, code_, code_.size() - 1); - } - - bool acc_cond::accepting(mark_t inf) const - { - if (uses_fin_acceptance()) - throw std::runtime_error - ("Fin acceptance is not supported by this code path."); - return accepting(inf, 0U); + return eval(inf, &code_.back()); } bool acc_cond::check_fin_acceptance() const @@ -225,6 +215,11 @@ namespace spot pos -= 2; break; case acc_cond::acc_op::Fin: + if (code_[pos - 2].mark == 0U) // f + { + pos -= 2; + break; + } case acc_cond::acc_op::FinNeg: return true; } @@ -330,6 +325,35 @@ namespace spot return res; } + bool acc_cond::acc_code::is_dnf() const + { + if (empty()) + return true; + auto pos = &back(); + auto start = &front(); + if (pos->op == acc_cond::acc_op::Or) + --pos; + while (pos > start) + { + switch (pos->op) + { + case acc_cond::acc_op::Or: + return false; + case acc_cond::acc_op::And: + --pos; + break; + case acc_cond::acc_op::Inf: + case acc_cond::acc_op::InfNeg: + case acc_cond::acc_op::Fin: + case acc_cond::acc_op::FinNeg: + pos -= 2; + break; + } + } + return true; + } + + std::ostream& operator<<(std::ostream& os, const spot::acc_cond::acc_code& code) { diff --git a/src/tgba/acc.hh b/src/tgba/acc.hh index 8f7a70858..80699c87a 100644 --- a/src/tgba/acc.hh +++ b/src/tgba/acc.hh @@ -556,6 +556,8 @@ namespace spot while (pos > 0); } + bool is_dnf() const; + acc_code to_dnf() const; SPOT_API @@ -743,8 +745,6 @@ namespace spot return all_; } - bool accepting(mark_t inf, mark_t fin) const; - bool accepting(mark_t inf) const; std::ostream& format(std::ostream& os, mark_t m) const diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index ec93a6260..9d32fd470 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -62,6 +62,7 @@ tgbaalgos_HEADERS = \ reachiter.hh \ reducerun.hh \ relabel.hh \ + remfin.hh \ replayrun.hh \ safety.hh \ sbacc.hh \ @@ -113,6 +114,7 @@ libtgbaalgos_la_SOURCES = \ randomize.cc \ reachiter.cc \ reducerun.cc \ + remfin.cc \ replayrun.cc \ relabel.cc \ safety.cc \ diff --git a/src/tgbaalgos/remfin.cc b/src/tgbaalgos/remfin.cc new file mode 100644 index 000000000..f6a87bcb5 --- /dev/null +++ b/src/tgbaalgos/remfin.cc @@ -0,0 +1,308 @@ +// -*- 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 "remfin.hh" +#include "sccinfo.hh" +#include + +//#define TRACE +#ifdef TRACE +#define trace std::cerr +#else +#define trace while (0) std::cerr +#endif + +namespace spot +{ + namespace + { + // If the DNF is + // Fin(1)&Inf(2)&Inf(4) | Fin(2)&Fin(3)&Inf(1) | + // Inf(1)&Inf(3) | Inf(1)&Inf(2) | Fin(4) + // this returns the following map: + // {1} => Inf(2)&Inf(4) + // {2,3} => Inf(1) + // {} => Inf(3) | Inf(2) + // {4} => t + static std::map + split_dnf_acc_by_fin(const acc_cond::acc_code& acc) + { + std::map res; + auto pos = &acc.back(); + if (pos->op == acc_cond::acc_op::Or) + --pos; + auto start = &acc.front(); + while (pos > start) + { + if (pos->op == acc_cond::acc_op::Fin) + { + // We have only a Fin term, without Inf. In this case + // only, the Fin() may encode a disjunction of sets. + for (auto s: pos[-1].mark.sets()) + { + acc_cond::mark_t fin = 0U; + fin.set(s); + res[fin] = acc_cond::acc_code{}; + } + pos -= pos->size + 1; + } + else + { + // We have a conjunction of Fin and Inf sets. + auto end = pos - pos->size - 1; + acc_cond::mark_t fin = 0U; + acc_cond::mark_t inf = 0U; + while (pos > end) + { + switch (pos->op) + { + case acc_cond::acc_op::And: + --pos; + break; + case acc_cond::acc_op::Fin: + fin |= pos[-1].mark; + assert(pos[-1].mark.count() == 1); + pos -= 2; + break; + case acc_cond::acc_op::Inf: + inf |= pos[-1].mark; + pos -= 2; + break; + case acc_cond::acc_op::FinNeg: + case acc_cond::acc_op::InfNeg: + case acc_cond::acc_op::Or: + SPOT_UNREACHABLE(); + break; + } + } + assert(pos == end); + acc_cond::acc_word w[2]; + w[0].mark = inf; + w[1].op = acc_cond::acc_op::Inf; + w[1].size = 1; + acc_cond::acc_code c; + c.insert(c.end(), w, w + 2); + auto p = res.emplace(fin, c); + if (!p.second) + p.first->second.append_or(std::move(c)); + } + } + return res; + } + } + + tgba_digraph_ptr remove_fin(const const_tgba_digraph_ptr& aut) + { + if (!aut->acc().uses_fin_acceptance()) + return std::const_pointer_cast(aut); + + std::vector code; + std::vector rem; + std::vector keep; + std::vector add; + bool has_true_term = false; + { + auto acccode = aut->get_acceptance(); + + if (!acccode.is_dnf()) + acccode = acccode.to_dnf(); + + auto split = split_dnf_acc_by_fin(acccode); + + auto sz = split.size(); + assert(sz > 0); + + rem.reserve(sz); + code.reserve(sz); + keep.reserve(sz); + add.reserve(sz); + for (auto p: split) + { + // The empty Fin should always come first + assert(p.first != 0U || rem.empty()); + rem.push_back(p.first); + acc_cond::mark_t inf = 0U; + if (!p.second.empty()) + { + auto pos = &p.second.back(); + auto end = &p.second.front(); + while (pos > end) + { + switch (pos->op) + { + case acc_cond::acc_op::And: + case acc_cond::acc_op::Or: + --pos; + break; + case acc_cond::acc_op::Inf: + inf |= pos[-1].mark; + pos -= 2; + break; + case acc_cond::acc_op::Fin: + case acc_cond::acc_op::FinNeg: + case acc_cond::acc_op::InfNeg: + SPOT_UNREACHABLE(); + break; + } + } + } + else + { + has_true_term = true; + } + code.push_back(std::move(p.second)); + keep.push_back(inf); + add.push_back(0U); + } + } + assert(add.size() > 0); + + acc_cond acc = aut->acc(); + unsigned extra_sets = 0; + + // Do we have common sets between the acceptance terms? + // If so, we need extra sets to distinguish the terms. + bool interference = false; + { + auto sz = keep.size(); + acc_cond::mark_t sofar = 0U; + for (unsigned i = 0; i < sz; ++i) + { + auto k = keep[i]; + if (k & sofar) + { + interference = true; + break; + } + sofar |= k; + } + if (interference) + { + trace << "We have interferences\n"; + unsigned base = acc.add_sets(sz); + extra_sets += sz; + for (unsigned i = 0; i < sz; ++i) + { + auto m = acc.marks({base + i}); + add[i] = m; + code[i].append_and(acc.inf(m)); + trace << "code[" << i << "] = " << code[i] << '\n'; + } + } + else if (has_true_term) + { + trace << "We have a true term\n"; + unsigned one = acc.add_sets(1); + extra_sets += 1; + auto m = acc.marks({one}); + auto c = acc.inf(m); + for (unsigned i = 0; i < sz; ++i) + { + if (!code[i].is_true()) + continue; + add[i] = m; + code[i].append_and(c); + c = acc.fin(0U); // Use false for the other terms. + trace << "code[" << i << "] = " << code[i] << '\n'; + } + + } + } + + acc_cond::acc_code new_code = aut->acc().fin(0U); + for (auto c: code) + new_code.append_or(std::move(c)); + + unsigned cs = code.size(); + for (unsigned i = 0; i < cs; ++i) + trace << i << " Rem " << rem[i] << " Code " << code[i] + << " Keep " << keep[i] << '\n'; + + scc_info si(aut); + + unsigned nst = aut->num_states(); + auto res = make_tgba_digraph(aut->get_dict()); + res->copy_ap_of(aut); + res->new_states(nst); + res->set_acceptance(aut->acc().num_sets() + extra_sets, new_code); + res->set_init_state(aut->get_init_state_number()); + + unsigned nscc = si.scc_count(); + std::vector state_map(nst); + for (unsigned n = 0; n < nscc; ++n) + { + // What to keep and add to the main copy + acc_cond::mark_t main_sets = 0U; + acc_cond::mark_t main_add = 0U; + + auto m = si.acc(n); + auto states = si.states_of(n); + trace << "SCC #" << n << " uses " << m << '\n'; + + for (unsigned i = 0; i < cs; ++i) + if (!(m & rem[i])) + { + main_sets |= keep[i]; + main_add |= add[i]; + } + // Create the main copy + for (auto s: states) + for (auto& t: aut->out(s)) + res->new_transition(s, t.dst, t.cond, + (t.acc & main_sets) | main_add); + + // Create clones + for (unsigned i = 0; i < cs; ++i) + if (m & rem[i]) + { + auto r = rem[i]; + trace << "rem[" << i << "] = " << r << " requires a copy\n"; + unsigned base = res->new_states(states.size()); + for (auto s: states) + state_map[s] = base++; + auto k = keep[i]; + auto a = add[i]; + for (auto s: states) + { + auto ns = state_map[s]; + for (auto& t: aut->out(s)) + { + if ((t.acc & r) || si.scc_of(t.dst) != n) + continue; + auto nd = state_map[t.dst]; + res->new_transition(ns, nd, t.cond, (t.acc & k) | a); + // We need only one non-deterministic jump per + // cycle. As an approximation, we only do + // them on back-links. + // + // The acceptance marks on these transition + // are useless, but we keep them to preserve + // state-based acceptance if any. + if (t.dst <= s) + res->new_transition(s, nd, t.cond, + (t.acc & main_sets) | main_add); + } + } + } + + + } + return res; + } +} diff --git a/src/tgbaalgos/remfin.hh b/src/tgbaalgos/remfin.hh new file mode 100644 index 000000000..59e647033 --- /dev/null +++ b/src/tgbaalgos/remfin.hh @@ -0,0 +1,32 @@ +// -*- 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_REMFIN_HH +# define SPOT_TGBAALGOS_REMFIN_HH + +#include "tgba/tgbagraph.hh" + +namespace spot +{ + /// \brief Rewrite an automaton without Fin acceptance. + SPOT_API tgba_digraph_ptr + remove_fin(const const_tgba_digraph_ptr& aut); +} + +#endif // SPOT_TGBAALGOS_DTGBACOMP_HH diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 6384b024b..d1a916752 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -72,6 +72,7 @@ TESTS = \ det.test \ neverclaimread.test \ hoaparse.test \ + remfin.test \ dstar.test \ readsave.test \ ltldo.test \ diff --git a/src/tgbatest/remfin.test b/src/tgbatest/remfin.test new file mode 100755 index 000000000..ef93b38fb --- /dev/null +++ b/src/tgbatest/remfin.test @@ -0,0 +1,266 @@ +#!/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 + +set -e + +autfilt=../../bin/autfilt + +cat >test1 <expected < output +cat output +diff -u output expected -- GitLab