Commit 1a08eca8 authored by Maximilien Colange's avatar Maximilien Colange
Browse files

Add a new, parameterized, version of the Couvreur emptiness check.

This version has optimization for explicit twa, and also for weak and
terminal (depending on whether an accepting run is requested) automata.

* spot/twaalgos/couvreurnew.hh, spot/twaalgos/couvreurnew.cc,
  spot/twaalgos/Makefile.am: New files for the new algorithm.
* spot/twaalgos/emptiness.cc, tests/core/randtgba.cc:
  Register new algorithm.
parent f0416b3f
......@@ -4,6 +4,13 @@ New in spot 2.2.1.dev (Not yet released)
* A twa is required to have at least one state, the initial state.
* The Couvreur emptiness check has been rewritten to use the explicit
interface when possible, to avoid overkill memory allocations.
The new version has further optimizations for weak and terminal
automata. Overall, this new version is roughly 4x faster on explicit
automata than the former one. The old version has been kept for
compatibility.
Build:
* If the system has an installed libltdl library, use it instead of
......
......@@ -55,6 +55,7 @@ twaalgos_HEADERS = \
magic.hh \
mask.hh \
minimize.hh \
couvreurnew.hh \
neverclaim.hh \
postproc.hh \
powerset.hh \
......@@ -109,6 +110,7 @@ libtwaalgos_la_SOURCES = \
magic.cc \
mask.cc \
minimize.cc \
couvreurnew.cc \
ndfs_result.hxx \
neverclaim.cc \
postproc.cc \
......
// -*- coding: utf-8 -*-
// Copyright (C) 2016 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 <spot/twaalgos/couvreurnew.hh>
#include <spot/twa/twa.hh>
#include <spot/twa/twagraph.hh>
#include <spot/twaalgos/bfssteps.hh>
#include <spot/twaalgos/emptiness.hh>
#include <spot/twaalgos/emptiness_stats.hh>
#include <stack>
namespace spot
{
namespace
{
using explicit_iterator = twa_graph::graph_t::const_iterator;
// A proxy class that allows to manipulate an iterator from the
// explicit interface as an iterator from the abstract interface.
class explicitproxy
{
public:
explicitproxy(explicit_iterator it)
: it_(it)
{}
const explicitproxy*
operator->() const
{
return this;
}
explicitproxy*
operator->()
{
return this;
}
bool
done() const
{
return !it_;
}
unsigned
dst() const
{
return it_->dst;
}
acc_cond::mark_t
acc() const
{
return it_->acc;
}
void
next()
{
++it_;
}
private:
explicit_iterator it_;
};
template<bool is_explicit>
class twa_iteration
{
};
template<>
class twa_iteration<false>
{
public:
using state_t = const state*;
using iterator_t = twa_succ_iterator*;
template<class val>
using state_map = state_map<val>;
template<class val>
static
std::pair<std::pair<state_t, val>, bool>
h_emplace(state_map<val>& h, state_t s, val i)
{
auto p = h.emplace(s, i);
return std::make_pair(*p.first, p.second);
}
static
std::pair<state_t, int>
h_find(const state_map<int>& h, state_t s)
{
auto p = h.find(s);
if (p == h.end())
return std::make_pair(nullptr, 0);
else
return std::make_pair(p->first, p->second);
}
static
unsigned
h_count(const state_map<int>& h, const std::function<bool(int)>& p)
{
unsigned count = 0;
for (auto i : h)
if (p(i.second))
++count;
return count;
}
static
state_t
initial_state(const const_twa_ptr& twa_p)
{
return twa_p->get_init_state();
}
static
iterator_t
succ(const const_twa_ptr& twa_p, state_t s)
{
auto res = twa_p->succ_iter(s);
res->first();
return res;
}
static
void
destroy(state_t s)
{
s->destroy();
}
static
const state*
to_state(const const_twa_ptr&, state_t s)
{
return s;
}
static
state_t
from_state(const const_twa_ptr&, const state* s)
{
return s;
}
static
void
it_destroy(const const_twa_ptr& twa_p, iterator_t it)
{
twa_p->release_iter(it);
}
};
template<>
class twa_iteration<true>
{
public:
using state_t = unsigned;
using iterator_t = explicitproxy;
template<class val>
using state_map = std::vector<val>;
template<class val>
static
std::pair<std::pair<state_t, val>, bool>
h_emplace(state_map<val>& h, state_t s, val i)
{
if (h[s] == val())
{
h[s] = i;
return std::make_pair(std::make_pair(s, h[s]), true);
}
else
{
return std::make_pair(std::make_pair(s, h[s]), false);
}
}
static
std::pair<state_t, int>
h_find(const state_map<int>& h, state_t s)
{
assert(s < h.size());
return std::make_pair(s, h[s]);
}
static
unsigned
h_count(const state_map<int>& h, const std::function<bool(int)>& p)
{
unsigned count = 0;
for (auto i : h)
if (p(i))
++count;
return count;
}
static
state_t
initial_state(const const_twa_graph_ptr& twa_p)
{
return twa_p->get_init_state_number();
}
static
iterator_t
succ(const const_twa_graph_ptr& twa_p, state_t s)
{
return explicitproxy(twa_p->out(s).begin());
}
static
const state*
to_state(const const_twa_graph_ptr& twa_p, state_t s)
{
return twa_p->state_from_number(s);
}
static
state_t
from_state(const const_twa_graph_ptr& twa_p, const state* s)
{
return twa_p->state_number(s);
}
static
void
destroy(state_t)
{
}
static
void
it_destroy(const const_twa_ptr&, iterator_t)
{
}
};
// A simple struct representing an SCC.
struct scc
{
scc(int i): index(i), condition(0U) {}
int index;
acc_cond::mark_t condition;
};
template<bool is_explicit>
using automaton_ptr = typename std::conditional<is_explicit,
const_twa_graph_ptr,
const_twa_ptr>::type;
// The status of the emptiness-check on success.
// It contains everyting needed to build a counter-example:
// the automaton, the stack of SCCs traversed by the counter-example,
// and the heap of visited states with their indices.
template<bool is_explicit>
struct couvreur99_new_status
{
using T = twa_iteration<is_explicit>;
couvreur99_new_status(const automaton_ptr<is_explicit>& a)
: aut(a)
{
// Appropriate version is resolved through SFINAE.
init<is_explicit>();
}
automaton_ptr<is_explicit> aut;
std::stack<scc> root;
typename T::template state_map<int> h;
typename T::state_t cycle_seed;
private:
template<bool U>
typename std::enable_if<U>::type
init()
{
// Initialize h with the right size.
h.resize(aut->num_states(), 0);
}
template<bool U>
typename std::enable_if<!U>::type
init()
{}
};
template<bool is_explicit>
using couvreur99_new_status_ptr =
std::shared_ptr<couvreur99_new_status<is_explicit>>;
template<bool is_explicit>
class couvreur99_new_result final :
public emptiness_check_result,
public acss_statistics
{
using T = twa_iteration<is_explicit>;
public:
couvreur99_new_result(const couvreur99_new_status_ptr<is_explicit>& ecs)
: emptiness_check_result(ecs->aut), ecs_(ecs)
{}
virtual
unsigned
acss_states() const override
{
int scc_root = ecs_->root.top().index;
return T::h_count(ecs_->h,
[scc_root](int s) { return s >= scc_root; });
}
twa_run_ptr
accepting_run() override;
private:
couvreur99_new_status_ptr<is_explicit> ecs_;
twa_run_ptr run_;
void
accepting_cycle()
{
acc_cond::mark_t acc_to_traverse =
ecs_->aut->acc().accepting_sets(ecs_->root.top().condition);
// Compute an accepting cycle using successive BFS that are
// restarted from the point reached after we have discovered a
// transition with a new acceptance condition.
//
// This idea is taken from Product<T>::findWitness in LBTT 1.1.2,
// which in turn is probably inspired from
// @Article{latvala.00.fi,
// author = {Timo Latvala and Keijo Heljanko},
// title = {Coping With Strong Fairness},
// journal = {Fundamenta Informaticae},
// year = {2000},
// volume = {43},
// number = {1--4},
// pages = {1--19},
// publisher = {IOS Press}
// }
const state* substart = T::to_state(ecs_->aut, ecs_->cycle_seed);
const state* cycle_seed = T::to_state(ecs_->aut, ecs_->cycle_seed);
do
{
struct scc_bfs final: bfs_steps
{
const couvreur99_new_status<is_explicit>* ecs;
couvreur99_new_result<is_explicit>* r;
acc_cond::mark_t& acc_to_traverse;
int scc_root;
scc_bfs(const couvreur99_new_status<is_explicit>* ecs,
couvreur99_new_result<is_explicit>* r,
acc_cond::mark_t& acc_to_traverse)
: bfs_steps(ecs->aut), ecs(ecs), r(r)
, acc_to_traverse(acc_to_traverse)
, scc_root(ecs->root.top().index)
{
}
virtual const state*
filter(const state* s) override
{
auto i = T::h_find(ecs->h, T::from_state(ecs->aut, s));
s->destroy();
// Ignore unknown states.
if (i.second == 0)
return nullptr;
// Stay in the final SCC.
if (i.second < scc_root)
return nullptr;
r->inc_ars_cycle_states();
return T::to_state(ecs->aut, i.first);
}
virtual bool
match(twa_run::step& st, const state* s) override
{
acc_cond::mark_t less_acc =
acc_to_traverse - st.acc;
if (less_acc != acc_to_traverse
|| (acc_to_traverse == 0U
&& T::from_state(ecs->aut, s) == ecs->cycle_seed))
{
acc_to_traverse = less_acc;
return true;
}
return false;
}
} b(ecs_.get(), this, acc_to_traverse);
substart = b.search(substart, run_->cycle);
assert(substart);
}
while (acc_to_traverse != 0U || substart != cycle_seed);
}
};
template<bool is_explicit>
class shortest_path final : public bfs_steps
{
using T = twa_iteration<is_explicit>;
public:
shortest_path(const state_set* t,
const couvreur99_new_status_ptr<is_explicit>& ecs,
couvreur99_new_result<is_explicit>* r)
: bfs_steps(ecs->aut), target(t), ecs(ecs), r(r)
{
}
const state*
search(const state* start, twa_run::steps& l)
{
return this->bfs_steps::search(filter(start), l);
}
const state*
filter(const state* s) override
{
r->inc_ars_prefix_states();
auto i = T::h_find(ecs->h, T::from_state(ecs->aut, s));
s->destroy();
// Ignore unknown states ...
if (i.second == 0)
return nullptr;
// ... as well as dead states
if (i.second == -1)
return nullptr;
return T::to_state(ecs->aut, i.first);
}
bool
match(twa_run::step&, const state* dest) override
{
return target->find(dest) != target->end();
}
private:
state_set seen;
const state_set* target;
couvreur99_new_status_ptr<is_explicit> ecs;
couvreur99_new_result<is_explicit>* r;
};
template<bool is_explicit>
twa_run_ptr
couvreur99_new_result<is_explicit>::accepting_run()
{
run_ = std::make_shared<twa_run>(ecs_->aut);
assert(!ecs_->root.empty());
// Compute an accepting cycle.
accepting_cycle();
// Compute the prefix: it is the shorted path from the initial
// state of the automaton to any state of the cycle.
// Register all states from the cycle as targets of the BFS.
state_set ss;
for (twa_run::steps::const_iterator i = run_->cycle.begin();
i != run_->cycle.end(); ++i)
ss.insert(i->s);
shortest_path<is_explicit> shpath(&ss, ecs_, this);
const state* prefix_start =
T::to_state(ecs_->aut, T::initial_state(ecs_->aut));
// There are two cases: either the initial state is already in
// the cycle, or it is not. If it is, we will have to rotate
// the cycle so it begins at this position. Otherwise we will shift
// the cycle so it begins at the state that follows the prefix.
// cycle_entry_point is that state.
const state* cycle_entry_point;
state_set::const_iterator ps = ss.find(prefix_start);
if (ps != ss.end())
{
// The initial state is in the cycle.
prefix_start->destroy();
cycle_entry_point = *ps;
}
else
{
// This initial state is outside the cycle. Compute the prefix.
cycle_entry_point = shpath.search(prefix_start, run_->prefix);
}
// Locate cycle_entry_point on the cycle.
twa_run::steps::iterator cycle_ep_it;
for (cycle_ep_it = run_->cycle.begin();
cycle_ep_it != run_->cycle.end()
&& cycle_entry_point->compare(cycle_ep_it->s); ++cycle_ep_it)
continue;
assert(cycle_ep_it != run_->cycle.end());
// Now shift the cycle so it starts on cycle_entry_point
run_->cycle.splice(run_->cycle.end(), run_->cycle,
run_->cycle.begin(), cycle_ep_it);
return run_;
}
// A simple enum for the different automata strengths.
enum twa_strength { STRONG, WEAK, TERMINAL };
template<bool is_explicit, twa_strength strength>
class couvreur99_new : public emptiness_check, public ec_statistics
{
using T = twa_iteration<is_explicit>;
using state_t = typename T::state_t;
using iterator_t = typename T::iterator_t;
using pair_state_iter = std::pair<state_t, iterator_t>;
couvreur99_new_status_ptr<is_explicit> ecs_;
public:
couvreur99_new(const automaton_ptr<is_explicit>& a,
option_map o = option_map())
: emptiness_check(a, o)
, ecs_(std::make_shared<couvreur99_new_status<is_explicit>>(a))
{
}
virtual
emptiness_check_result_ptr
check() override
{
return check_impl<true>();
}
// The following two methods anticipe the future interface of the
// class emptiness_check. Following the interface of twa, the class
// emptiness_check_result should not be exposed.
bool
is_empty()
{
return check_impl<false>();
}
twa_run
accepting_run()
{
return check_impl<true>()->accepting_run();
}
private:
// A union-like struct to store the result of an emptiness.
// If the caller only wants to test emptiness, it is sufficient to
// store the Boolean result.
// Otherwise, we need to store all the information needed to build
// an accepting run.
struct check_result
{
enum { BOOL, PTR } tag;
union
{
bool res;
emptiness_check_result_ptr ecr;
};
// Copy constructor.
check_result(const check_result& o)
: tag(o.tag)
{
if (tag == BOOL)
res = o.res;
else
ecr = o.ecr;
}
check_result(bool r)
: tag(BOOL), res(r)
{
}