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

genem: Implement accepting cycle search

Browse source 
Implement an accepting run search in spot::sccinfo, use it with the
generic emptiness check.

* spot/twaalgos/sccinfo.cc, spot/twaalgos/sccinfo.hh: Here.
* spot/twaalgos/genem.cc, spot/twaalgos/genem.hh: Use it.
* tests/python/genem.py: Test it.
This commit is contained in:
Clément Gillard 2018-12-11 13:43:53 +01:00 • committed by Alexandre Duret-Lutz
parent 4ecd066c0e
commit 51ca5ecdb1
5 changed files with 217 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

79
spot/twaalgos/genem.cc
View file

@ -50,10 +50,11 @@ namespace spot
}
};
bool scc_split_check(const scc_info& si, unsigned scc,
bool scc_split_check(const scc_info& si, unsigned scc, twa_run_ptr run,
acc_cond::mark_t tocut,
bool (*ec_scc)(const scc_info& si,
unsigned scc,
twa_run_ptr run,
acc_cond::mark_t tocut))
{
struct filter_data_t {
@ -85,14 +86,21 @@ namespace spot
acc = acc.remove(si.common_sets_of(scc), false);
temporary_acc_set tmp(si.get_aut(), acc);
scc_info upper_si(si.get_aut(), si.one_state_of(scc), filter, &data,
scc_info_options::STOP_ON_ACC);
if (upper_si.one_accepting_scc() >= 0)
scc_info_options::STOP_ON_ACC
| scc_info_options::TRACK_STATES);
const int accepting_scc = upper_si.one_accepting_scc();
if (accepting_scc >= 0)
{
if (run)
upper_si.get_accepting_run(accepting_scc, run);
return false;
}
if (!acc.uses_fin_acceptance())
return true;
unsigned nscc = upper_si.scc_count();
for (unsigned scc = 0; scc < nscc; ++scc)
if (!ec_scc(upper_si, scc, tocut))
if (!ec_scc(upper_si, scc, run, tocut))
return false;
return true;
}
@ -100,6 +108,7 @@ namespace spot
template <bool deal_with_disjunct>
bool generic_emptiness_check_for_scc_nocopy(const scc_info& si,
unsigned scc,
twa_run_ptr run,
acc_cond::mark_t
tocut = {})
{
@ -112,11 +121,15 @@ namespace spot
if (acc.is_f())
return true;
if (acc.is_t())
{
if (run)
si.get_accepting_run(scc, run);
return false;
}
temporary_acc_set tmp(si.get_aut(), acc);
if (acc_cond::mark_t fu = acc.fin_unit())
return scc_split_check
(si, scc, tocut | fu,
(si, scc, run, tocut | fu,
generic_emptiness_check_for_scc_nocopy<deal_with_disjunct>);
if (deal_with_disjunct)
@ -141,7 +154,7 @@ namespace spot
if (acc_cond::mark_t fu = one.fin_unit())
plus = fu;
if (!scc_split_check
(si, scc, tocut | plus,
(si, scc, run, tocut | plus,
generic_emptiness_check_for_scc_nocopy
<deal_with_disjunct>))
return false;
@ -157,7 +170,7 @@ namespace spot
tmp.set(acc_cond::acc_code());
for (unsigned d: pos[-1].mark.sets())
if (!scc_split_check
(si, scc,
(si, scc, run,
tocut | acc_cond::mark_t({d}),
generic_emptiness_check_for_scc_nocopy
<deal_with_disjunct>))
@ -170,36 +183,54 @@ namespace spot
assert(fo >= 0);
// Try to accept when Fin(fo) == true
if (!scc_split_check
(si, scc, tocut | acc_cond::mark_t({(unsigned) fo}),
(si, scc, run, tocut | acc_cond::mark_t({(unsigned) fo}),
generic_emptiness_check_for_scc_nocopy
<deal_with_disjunct>))
return false;
// Try to accept when Fin(fo) == false
tmp.set(acc.force_inf({(unsigned) fo}));
return generic_emptiness_check_for_scc_nocopy
<deal_with_disjunct>(si, scc, tocut);
return true;
<deal_with_disjunct>(si, scc, run, tocut);
}
template <bool deal_with_disjunct>
bool generic_emptiness_check_main_nocopy(const twa_graph_ptr& aut)
bool generic_emptiness_check_main_nocopy(const twa_graph_ptr& aut,
twa_run_ptr run)
{
cleanup_acceptance_here(aut, false);
auto& aut_acc = aut->acc();
if (aut_acc.is_f())
return true;
if (!aut->acc().uses_fin_acceptance())
{
if (run)
{
auto p = aut->accepting_run();
if (p)
{
*run = *p;
return false;
}
return true;
}
return aut->is_empty();
}
scc_info si(aut, scc_info_options::STOP_ON_ACC
| scc_info_options::TRACK_STATES);
if (si.one_accepting_scc() >= 0)
const int accepting_scc = si.one_accepting_scc();
if (accepting_scc >= 0)
{
if (run)
si.get_accepting_run(accepting_scc, run);
return false;
}
unsigned nscc = si.scc_count();
for (unsigned scc = 0; scc < nscc; ++scc)
if (!generic_emptiness_check_for_scc_nocopy
<deal_with_disjunct>(si, scc))
<deal_with_disjunct>(si, scc, run))
return false;
return true;
}
@ -212,17 +243,35 @@ namespace spot
"does not support alternating automata");
auto aut_ = std::const_pointer_cast<twa_graph>(aut);
acc_cond old = aut_->acc();
bool res = generic_emptiness_check_main_nocopy<true>(aut_);
bool res = generic_emptiness_check_main_nocopy<true>(aut_, nullptr);
aut_->set_acceptance(old);
return res;
}
twa_run_ptr generic_accepting_run(const const_twa_graph_ptr& aut)
{
if (SPOT_UNLIKELY(!aut->is_existential()))
throw std::runtime_error("generic_accepting_run() "
"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;
}
bool generic_emptiness_check_for_scc(const scc_info& si,
unsigned scc)
{
if (SPOT_UNLIKELY(!si.get_aut()->is_existential()))
throw std::runtime_error("generic_emptiness_check_for_scc() "
"does not support alternating automata");
return generic_emptiness_check_for_scc_nocopy<true>(si, scc);
return generic_emptiness_check_for_scc_nocopy<true>(si, scc, nullptr);
}
}

8
spot/twaalgos/genem.hh
View file

@ -19,6 +19,7 @@
#pragma once
#include <spot/twaalgos/emptiness.hh>
#include <spot/twaalgos/sccinfo.hh>
namespace spot
@ -28,6 +29,13 @@ namespace spot
SPOT_API bool
generic_emptiness_check(const const_twa_graph_ptr& aut);
/// \ingroup emptiness_check_algorithms
/// \brief Accepting run search in an automaton, for any acceptance condition.
/// \return An accepting run over the automaton, or nullptr if the language is
/// empty.
SPOT_API twa_run_ptr
generic_accepting_run(const const_twa_graph_ptr& aut);
/// \ingroup emptiness_check_algorithms
/// \brief Emptiness check of one SCC, for any acceptance condition.
SPOT_API bool

137
spot/twaalgos/sccinfo.cc
View file

@ -23,11 +23,11 @@
#include <algorithm>
#include <queue>
#include <spot/twa/bddprint.hh>
#include <spot/twaalgos/bfssteps.hh>
#include <spot/twaalgos/mask.hh>
#include <spot/twaalgos/genem.hh>
#include <spot/misc/escape.hh>
namespace spot
{
void scc_info::report_need_track_states()
@ -461,6 +461,141 @@ 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.
// Returns the destination of the matched transition, or -1 if no match has
// been found.
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)
{
std::unordered_map<unsigned, exp_step> backlinks;
std::deque<unsigned> bfs_queue;
bfs_queue.emplace_back(start);
while (!bfs_queue.empty())
{
unsigned src = bfs_queue.front();
bfs_queue.pop_front();
for (auto& t: aut->out(src))
{
if (filter(t))
continue;
exp_step s = { src, t.cond, t.acc };
if (match(s, t.dst))
{
twa_run::steps path;
for (;;)
{
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;
}
steps.splice(steps.end(), path);
return t.dst;
}
if (backlinks.emplace(t.dst, s).second)
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());
// 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())
{
// The initial state is in the SCC
substart = init;
}
else
{
substart = explicit_bfs_steps(aut_, init, r->prefix,
[](const twa_graph::edge_storage_t&)
{
return false; // Do not filter.
},
[&](exp_step&, unsigned dst)
{
// Match any state in the SCC.
return scc_states.find(dst) != scc_states.end();
});
}
const unsigned start = (unsigned)substart;
// Cycle search
acc_cond::mark_t acc_to_see = actual_cond.accepting_sets(node.acc_marks());
r->cycle.clear();
do
{
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;
},
[&](exp_step& st, unsigned dst)
{
if (!acc_to_see) // We have seen all the marks, go back to start.
return dst == start;
if (st.acc & acc_to_see)
{
acc_to_see -= st.acc;
return true;
}
return false;
});
assert(0 <= substart);
}
while (acc_to_see || (unsigned)substart != start);
}
std::ostream&
dump_scc_info_dot(std::ostream& out,
const_twa_graph_ptr aut, scc_info* sccinfo)

6
spot/twaalgos/sccinfo.hh
View file

@ -21,6 +21,7 @@
#include <vector>
#include <spot/twa/twagraph.hh>
#include <spot/twaalgos/emptiness.hh>
namespace spot
{
@ -595,6 +596,11 @@ namespace spot
/// determine_unknown_acceptance().
bool check_scc_emptiness(unsigned n);
/// \brief Retrieves an accepting run of the automaton whose cycle is in the
/// SCC.
/// \param scc an accepting scc
void get_accepting_run(unsigned scc, twa_run_ptr r) const;
bool is_useful_scc(unsigned scc) const
{
if (SPOT_UNLIKELY(!!(options_ & scc_info_options::STOP_ON_ACC)))

3
tests/python/genem.py
View file

@ -189,5 +189,8 @@ def run_bench(automata):
res = str(res1)[0] + str(res2)[0] + str(res3)[0]
print(res)
assert res in ('TTT', 'FFF')
if res == 'FFF':
run3 = spot.generic_accepting_run(aut)
assert run3.replay(spot.get_cout()) is True
run_bench([a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a11, a360])