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

use the generic emptiness check

Browse source 
* spot/twa/twa.cc (is_empty, intersects): Here.
* spot/twaalgos/sccinfo.cc (check_scc_emptiness): Here.
* spot/twaalgos/genem.cc: Report error if the input is alternating.
* spot/twaalgos/isunamb.cc, spot/twaalgos/sccinfo.hh: Adjust.
* NEWS: Mention the change.
This commit is contained in:
Alexandre Duret-Lutz 2018-07-24 10:54:36 +02:00
parent 86b6506268
commit da996ecbaf
6 changed files with 51 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

6
spot/twaalgos/genem.cc
View file

@ -207,6 +207,9 @@ namespace spot
bool generic_emptiness_check(const const_twa_graph_ptr& aut)
{
if (SPOT_UNLIKELY(!aut->is_existential()))
throw std::runtime_error("generic_emptiness_check() "
"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_);
@ -217,6 +220,9 @@ namespace spot
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);
}
}

5
spot/twaalgos/isunamb.cc
View file

@ -118,9 +118,8 @@ namespace spot
if (!accepting)
continue;
// We can't avoid it any more, we have to check the
// acceptance if the SCC.
std::vector<bool> k;
useful[n] = !sccmap_prod.check_scc_emptiness(n, &k);
// acceptance of the SCC.
useful[n] = !sccmap_prod.check_scc_emptiness(n);
}
}

12
spot/twaalgos/sccinfo.cc
View file

@ -24,6 +24,7 @@
#include <queue>
#include <spot/twa/bddprint.hh>
#include <spot/twaalgos/mask.hh>
#include <spot/twaalgos/genem.hh>
#include <spot/misc/escape.hh>
@ -423,23 +424,18 @@ namespace spot
return support;
}
bool scc_info::check_scc_emptiness(unsigned n, std::vector<bool>* k)
bool scc_info::check_scc_emptiness(unsigned n)
{
if (SPOT_UNLIKELY(!aut_->is_existential()))
throw std::runtime_error("scc_info::check_scc_emptiness() "
"does not support alternating automata");
if (SPOT_UNLIKELY(!(options_ & scc_info_options::TRACK_STATES)))
report_need_track_states();
k->assign(aut_->num_states(), false);
auto& node = node_[n];
for (auto i: node.states_)
(*k)[i] = true;
return mask_keep_accessible_states(aut_, *k, node.one_state_)->is_empty();
return generic_emptiness_check_for_scc(*this, n);
}
void scc_info::determine_unknown_acceptance()
{
std::vector<bool> k;
unsigned s = scc_count();
bool changed = false;
// iterate over SCCs in topological order
@ -453,7 +449,7 @@ namespace spot
"scc_info::determine_unknown_acceptance() "
"does not support alternating automata");
auto& node = node_[s];
if (check_scc_emptiness(s, &k))
if (check_scc_emptiness(s))
node.rejecting_ = true;
else
node.accepting_ = true;

6
spot/twaalgos/sccinfo.hh
View file

@ -592,10 +592,8 @@ namespace spot
/// \brief Recompute whether an SCC is accepting or not.
///
/// This is an internal function of
/// determine_unknown_acceptance(). The Boolean vector k will be
/// used by the method to mark the state that belong to the SCC.
/// It can be shared between multiple calls.
bool check_scc_emptiness(unsigned n, std::vector<bool>* k);
/// determine_unknown_acceptance().
bool check_scc_emptiness(unsigned n);
bool is_useful_scc(unsigned scc) const
{