alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

polish previous two patches

Browse source 
* NEWS: Update.
* spot/twaalgos/genem.cc, spot/twaalgos/genem.hh, spot/twa/twa.cc:
Update copyright years.
* spot/twa/twa.hh: Update Doxygen documentation.
* spot/twaalgos/sccinfo.cc, spot/twaalgos/sccinfo.hh: Simplify data
structures, and fix failure of get_accepting_run() to compute
accepting runs in SCC that are accepting due to the self-loop
optimization of scc_info.
* tests/python/highlighting.ipynb: Add three test cases.
This commit is contained in:
Alexandre Duret-Lutz 2019-02-20 15:29:37 +01:00
parent 837f9e296b
commit c25a67b00d
8 changed files with 1007 additions and 142 deletions
Download patch file Download diff file Expand all files Collapse all files

8
NEWS
View file

@ -1,6 +1,12 @@
New in spot 2.7.1.dev (not yet released)
Nothing yet.
Library:
- Add generic_accepting_run() as a variant of generic_emptiness_check() that
returns an accepting run in an automaton with any acceptance condition.
- twa::accepting_run() now works on automata using Fin in
their acceptance condition.
New in spot 2.7.1 (2019-02-14)

2
spot/twa/twa.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2014-2018 Laboratoire de Recherche et Developpement de
// Copyright (C) 2011, 2014-2019 Laboratoire de Recherche et Developpement de
// l'EPITA (LRDE).
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre

68
spot/twa/twa.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2011, 2013-2018 Laboratoire de Recherche et
// Copyright (C) 2009, 2011, 2013-2019 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2003-2005 Laboratoire d'Informatique de Paris 6
// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@ -828,35 +828,45 @@ namespace spot
///
/// If you are calling this method on a product of two automata,
/// consider using intersects() instead.
///
/// Note that if the input automaton uses Fin-acceptance, the
/// emptiness check is not performed on-the-fly. Any on-the-fly
/// automaton would be automatically copied into a twa_graph_ptr
/// first.
virtual bool is_empty() const;
/// \brief Return an accepting run if one exists.
///
/// Note that this method currently only works for Fin-less
/// acceptance. For acceptance conditions that contain Fin
/// acceptance, you can either rely on is_empty() and not use any
/// accepting run, or remove Fin acceptance using remove_fin() and
/// compute an accepting run on that larger automaton.
///
/// Return nullptr if no accepting run were found.
///
/// If you are calling this method on a product of two automata,
/// consider using intersecting_run() instead.
///
/// Note that if the input automaton uses Fin-acceptance, this
/// computation is not performed on-the-fly. Any on-the-fly
/// automaton would be automatically copied into a twa_graph_ptr
/// first.
virtual twa_run_ptr accepting_run() const;
/// \brief Return an accepting word if one exists.
///
/// Note that this method DOES works with Fin
/// acceptance.
///
/// Return nullptr if no accepting word were found.
///
/// If you are calling this method on a product of two automata,
/// consider using intersecting_word() instead.
///
/// Note that if the input automaton uses Fin-acceptance, this
/// computation is not performed on-the-fly. Any on-the-fly
/// automaton would be automatically copied into a twa_graph_ptr
/// first.
virtual twa_word_ptr accepting_word() const;
/// \brief Check whether the language of this automaton intersects
/// that of the \a other automaton.
///
/// An emptiness check is performed on a product computed
/// on-the-fly, unless some of the operands use Fin-acceptance: in
/// this case an explicit product is performed.
virtual bool intersects(const_twa_ptr other) const;
/// \brief Return an accepting run recognizing a word accepted by
@ -864,52 +874,42 @@ namespace spot
///
/// If \a from_other is true, the returned run will be over the
/// \a other automaton. Otherwise, the run will be over this
/// automaton.
///
/// Note that this method currently only works if the automaton
/// from which the accepting run is extracted uses Fin-less acceptance.
/// (The other automaton can have any acceptance condition.)
///
/// For acceptance conditions that contain Fin acceptance, you can
/// either rely on intersects() and not use any accepting run, or
/// remove Fin acceptance using remove_fin() and compute an
/// intersecting run on this larger automaton.
/// automaton. (This argument will be deprecated soon, do not
/// use it.)
///
/// Return nullptr if no accepting run were found.
///
/// An emptiness check is performed on a product computed
/// on-the-fly, unless some of the operands use Fin-acceptance: in
/// this case an explicit product is performed.
virtual twa_run_ptr intersecting_run(const_twa_ptr other,
bool from_other = false) const;
/// \brief Return a word accepted by two automata.
///
/// Note that this method DOES works with Fin
/// acceptance.
///
/// Return nullptr if no accepting word were found.
virtual twa_word_ptr intersecting_word(const_twa_ptr other) const;
/// \brief Return an accepting run recognizing a word accepted by
/// exactly one of the two automata.
///
/// If \a from_other is true, the returned run will be over the
/// \a other automaton. Otherwise, the run will be over this
/// automaton.
///
/// Note that this method currently only works if the automaton
/// from which the accepting run is extracted uses Fin-less acceptance.
/// (The other automaton can have any acceptance condition.)
///
/// Return nullptr iff the two automata recognize the same
/// language.
///
/// This methods needs to complement at least one automaton (if
/// lucky) or maybe both automata. It will therefore be more
/// efficient on deterministic automata.
virtual twa_run_ptr exclusive_run(const_twa_ptr other) const;
/// \brief Return a word accepted by exactly one of the two
/// automata.
///
/// Note that this method DOES works with Fin acceptance.
///
/// Return nullptr iff the two automata recognize the same
/// language.
///
/// This methods needs to complement at least one automaton (if
/// lucky) or maybe both automata. It will therefore be more
/// efficient on deterministic automata.
virtual twa_word_ptr exclusive_word(const_twa_ptr other) const;
private:

5
spot/twaalgos/genem.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2017, 2018 Laboratoire de Recherche et Developpement
// Copyright (C) 2017-2019 Laboratoire de Recherche et Developpement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -255,12 +255,9 @@ namespace spot
"does not support alternating automata");
auto aut_ = std::const_pointer_cast<twa_graph>(aut);
acc_cond old = aut_->acc();
twa_run_ptr run = std::make_shared<twa_run>(aut_);
bool res = generic_emptiness_check_main_nocopy<true>(aut_, run);
aut_->set_acceptance(old);
if (!res)
return run;
return nullptr;

2
spot/twaalgos/genem.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2017, 2018 Laboratoire de Recherche et Developpement
// Copyright (C) 2017-2019 Laboratoire de Recherche et Developpement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.

148
spot/twaalgos/sccinfo.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement
// Copyright (C) 2014-2019 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -48,6 +48,13 @@ namespace spot
("scc_info was run with option STOP_ON_ACC");
}
// this one is not yet needed in the hh file
static void report_need_stop_on_acc()
{
throw std::runtime_error
("scc_info was not run with option STOP_ON_ACC");
}
namespace
{
struct scc
@ -461,30 +468,27 @@ namespace spot
determine_usefulness();
}
// Describes an explicit spot::twa_run::step
struct exp_step
{
unsigned src;
bdd cond;
acc_cond::mark_t acc;
};
// A reimplementation of spot::bfs_steps for explicit automata.
// bool filter(const twa_graph::edge_storage_t&) returns true if the
// transition has to be filtered out.
// bool match(struct exp_step&, unsigned dest) returns true if the BFS has to
// stop after this transition.
// bool match(const twa_graph::edge_storage_t&) returns true if the BFS
// has to stop after this transition.
// Returns the destination of the matched transition, or -1 if no match has
// been found.
template <typename edge_filter_type,
typename step_matcher_type>
static int explicit_bfs_steps(const const_twa_graph_ptr aut, unsigned start,
twa_run::steps& steps,
std::function<bool(const twa_graph::edge_storage_t&)> filter,
std::function<bool(exp_step&, unsigned)> match)
edge_filter_type filter,
step_matcher_type match)
{
std::unordered_map<unsigned, exp_step> backlinks;
auto& gr = aut->get_graph();
// The backlink of each state is the index of the edge that
// discovered it in the BFS, so BACKLINKS effectively describes a
// tree rooted at START.
std::vector<unsigned> backlinks(aut->num_states(), 0);
std::deque<unsigned> bfs_queue;
bfs_queue.emplace_back(start);
while (!bfs_queue.empty())
{
unsigned src = bfs_queue.front();
@ -494,55 +498,98 @@ namespace spot
if (filter(t))
continue;
exp_step s = { src, t.cond, t.acc };
if (match(s, t.dst))
if (match(t))
{
// Build the path from START to T.DST by following the
// backlinks, starting at the end.
twa_run::steps path;
for (;;)
path.emplace_front(aut->state_from_number(t.src),
t.cond, t.acc);
unsigned src = t.src;
while (src != start)
{
path.emplace_front(aut->state_from_number(s.src), s.cond, s.acc);
if (s.src == start)
break;
const auto& i = backlinks.find(s.src);
assert(i != backlinks.end());
s = i->second;
unsigned bl_num = backlinks[src];
assert(bl_num);
auto& bl_edge = gr.edge_storage(bl_num);
src = bl_edge.src;
path.emplace_front(aut->state_from_number(src),
bl_edge.cond, bl_edge.acc);
}
steps.splice(steps.end(), path);
return t.dst;
}
if (backlinks.emplace(t.dst, s).second)
if (!backlinks[t.dst])
{
backlinks[t.dst] = aut->edge_number(t);
bfs_queue.push_back(t.dst);
}
}
}
return -1;
}
void scc_info::get_accepting_run(unsigned scc, twa_run_ptr r) const
{
const scc_info::scc_node& node = node_[scc];
if (!node.is_accepting())
throw std::runtime_error("scc_info::get_accepting_cycle needs to be "
"called on an accepting scc");
acc_cond actual_cond = aut_->acc().restrict_to(node.acc_marks())
.force_inf(node.acc_marks());
assert(!actual_cond.uses_fin_acceptance());
if (SPOT_UNLIKELY(!(options_ & scc_info_options::STOP_ON_ACC)))
report_need_stop_on_acc();
unsigned init = aut_->get_init_state_number();
// The accepting cycle should honor any edge filter we have.
auto filter = [this](const twa_graph::edge_storage_t& t)
{
if (!filter_)
return false;
// Filter out ignored and cut transitions.
return filter_(t, t.dst, filter_data_)
!= edge_filter_choice::keep;
};
// The SCC exploration has a small optimization that can flag SCCs
// has accepting if they contain accepting self-loops, even if the
// SCC itself has some Fin acceptance to check. So we have to
// deal with this situation before we look for the more complex
// case of satisfying the condition with a larger cycle. We do
// this first, because it's good to return a small cycle if we
// can.
const acc_cond& acccond = aut_->acc();
for (unsigned s: node.states())
for (auto& e: aut_->out(s))
if (e.src == e.dst && !filter(e) && acccond.accepting(e.acc))
{
// We have found an accepting self-loop. That's the cycle
// part of our accepting run.
r->cycle.clear();
r->cycle.emplace_front(aut_->state_from_number(e.src),
e.cond, e.acc);
// Add the prefix.
r->prefix.clear();
if (e.src != init)
explicit_bfs_steps(aut_, init, r->prefix,
[](const twa_graph::edge_storage_t&)
{
return false; // Do not filter.
},
[&](const twa_graph::edge_storage_t& t)
{
return t.dst == e.src;
});
return;
}
// List of states of the SCC
const std::set<unsigned> scc_states(node.states().cbegin(),
node.states().cend());
// Prefix search
r->prefix.clear();
int init = aut_->get_init_state_number();
int substart;
if (scc_states.find(init) != scc_states.end())
if (scc_of(init) == scc)
{
// The initial state is in the SCC
// The initial state is in the target SCC: no prefix needed.
substart = init;
}
else
@ -552,19 +599,21 @@ namespace spot
{
return false; // Do not filter.
},
[&](exp_step&, unsigned dst)
[&](const twa_graph::edge_storage_t& t)
{
// Match any state in the SCC.
return scc_states.find(dst) != scc_states.end();
return scc_of(t.dst) == scc;
});
}
const unsigned start = (unsigned)substart;
// Cycle search
acc_cond actual_cond = acccond.restrict_to(node.acc_marks())
.force_inf(node.acc_marks());
assert(!actual_cond.uses_fin_acceptance());
assert(!actual_cond.is_f());
acc_cond::mark_t acc_to_see = actual_cond.accepting_sets(node.acc_marks());
r->cycle.clear();
do
@ -572,21 +621,16 @@ namespace spot
substart = explicit_bfs_steps(aut_, substart, r->cycle,
[&](const twa_graph::edge_storage_t& t)
{
if (scc_states.find(t.dst) == scc_states.end())
return true; // Destination is not in the SCC.
if (filter_)
// Filter out ignored and cut transitions.
return filter_(t, t.dst, filter_data_)
!= edge_filter_choice::keep;
return false;
// Stay in the specified SCC.
return scc_of(t.dst) != scc || filter(t);
},
[&](exp_step& st, unsigned dst)
[&](const twa_graph::edge_storage_t& t)
{
if (!acc_to_see) // We have seen all the marks, go back to start.
return dst == start;
if (st.acc & acc_to_see)
return t.dst == start;
if (t.acc & acc_to_see)
{
acc_to_see -= st.acc;
acc_to_see -= t.acc;
return true;
}
return false;

6
spot/twaalgos/sccinfo.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement
// Copyright (C) 2014-2019 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -598,7 +598,11 @@ namespace spot
/// \brief Retrieves an accepting run of the automaton whose cycle is in the
/// SCC.
///
/// \param scc an accepting scc
/// \param r a run to fill
///
/// This method needs the STOP_ON_ACC option.
void get_accepting_run(unsigned scc, twa_run_ptr r) const;
bool is_useful_scc(unsigned scc) const

878
tests/python/highlighting.ipynb
View file

File diff suppressed because it is too large Load diff