Commit 85508a0e authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

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.
parent 1441c4fe
......@@ -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<bool> 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.
......
......@@ -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)
{
......
......@@ -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
......
......@@ -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 \
......
// -*- 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 <http://www.gnu.org/licenses/>.
#include "remfin.hh"
#include "sccinfo.hh"
#include <iostream>
//#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<acc_cond::mark_t, acc_cond::acc_code>
split_dnf_acc_by_fin(const acc_cond::acc_code& acc)
{
std::map<acc_cond::mark_t, acc_cond::acc_code> 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<tgba_digraph>(aut);
std::vector<acc_cond::acc_code> code;
std::vector<acc_cond::mark_t> rem;
std::vector<acc_cond::mark_t> keep;
std::vector<acc_cond::mark_t> 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<unsigned> 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;
}
}
// -*- 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 <http://www.gnu.org/licenses/>.
#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
......@@ -72,6 +72,7 @@ TESTS = \
det.test \
neverclaimread.test \
hoaparse.test \
remfin.test \
dstar.test \
readsave.test \
ltldo.test \
......
#!/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 <http://www.gnu.org/licenses/>.
. ./defs
set -e
autfilt=../../bin/autfilt
cat >test1 <<EOF
/*
** This was a TGBA for GFa & GFb, but
** the acceptance has been changed to Fin(0)|Fin(1)
** so this is now the complement automaton.
**/
HOA: v1
States: 1
Start: 0
AP: 2 "a" "b"
Acceptance: 2 Fin(0)|Fin(1)
--BODY--
State: 0
[0&1] 0 {0 1}
[!0&!1] 0
[!0&1] 0 {1}
[0&!1] 0 {0}
--END--
/*
** This one has a mix of Inf and Fin acceptance, but no interference
** between the Fin sets
**/
HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
Acceptance: 5 Inf(0)&Fin(1)&Fin(3) | Inf(2)&Inf(3) | Inf(4)
--BODY--
State: 0
[t] 0
[0] 1 {1}
[!0] 2 {0}
State: 1
[1] 0
[0&1] 1 {0}
[!0&1] 2 {2}
State: 2
[!1] 0
[0&!1] 1 {0}
[!0&!1] 2 {0}
--END--
/*
** This one is similar, but Inf(0) is ised in two terms, so
** we to introduce extra sets in the output.
**/
HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 4 Inf(0)&Fin(1)&Fin(3) | Inf(2)&Inf(3) | Inf(0)
--BODY--
State: 0
[t] 0
[0] 1 {1}
[!0] 2 {0}
State: 1
[1] 0
[0&1] 1 {0}
[!0&1] 2 {2}
State: 2
[!1] 0
[0&!1] 1 {0}
[!0&!1] 2 {0}