Commit ebe3a15d authored by Alexandre GBAGUIDI AISSE's avatar Alexandre GBAGUIDI AISSE
Browse files

remfin: add is_buchi_realizable() method

* NEWS: Update.
* spot/tl/hierarchy.cc: Replace rabin_to_buchi_maybe() with
is_buchi_realizable().
* spot/twaalgos/remfin.cc: Implement it.
* spot/twaalgos/remfin.hh: Declare it.
parent 1b400240
......@@ -224,6 +224,10 @@ New in spot 2.4.4.dev (net yet released)
- The test suite is now using v4 of the Jupyter Notebook format.
- The function rabin_is_buchi_realizable() as its name suggests checks
if a rabin aut. is Büchi realizable. It is heavily based on
tra_to_tba() algorithm.
Deprecation notices:
(These functions still work but compilers emit warnings.)
......
......@@ -67,17 +67,16 @@ namespace spot
p.set_type(spot::postprocessor::Generic);
p.set_pref(spot::postprocessor::Deterministic);
p.set_level(spot::postprocessor::Low);
auto dra = p.run(aut);
if (dra->acc().is_generalized_buchi())
auto dpa = p.run(aut);
if (dpa->acc().is_generalized_buchi())
{
assert(is_deterministic(dra));
assert(is_deterministic(dpa));
return true;
}
else
{
auto ba = rabin_to_buchi_maybe(to_generalized_rabin(dra));
assert(ba);
return is_deterministic(ba);
auto dra = to_generalized_rabin(dpa);
return rabin_is_buchi_realizable(dra);
}
}
}
......
......@@ -220,7 +220,8 @@ namespace spot
auto filter_data = filter_data_t{aut, keep};
auto init = aut->edge_storage(*unknown.begin()).src;
scc_info si(aut, init, filter, &filter_data);
scc_info si(aut, init, filter, &filter_data,
scc_info_options::TRACK_STATES);
for (unsigned uscc = 0; uscc < si.scc_count(); ++uscc)
{
......@@ -274,8 +275,8 @@ namespace spot
std::vector<bool> keep(aut->edge_vector().size(), true);
for (unsigned scc = 0; scc < si.scc_count(); ++scc)
scc_is_tba_type[scc] = is_scc_tba_type(aut, si, scc, keep,
aut_pairs, final);
scc_is_tba_type[scc] = is_scc_tba_type(aut, si, scc, keep,
aut_pairs, final);
auto res = make_twa_graph(aut->get_dict());
res->copy_ap_of(aut);
......@@ -785,6 +786,31 @@ namespace spot
}
}
bool
rabin_is_buchi_realizable(const const_twa_graph_ptr& inaut)
{
auto aut = cleanup_acceptance(inaut);
std::vector<acc_cond::rs_pair> pairs;
if (!aut->acc().is_rabin_like(pairs))
return false;
auto aut_pairs = rs_pairs_view(pairs);
if (aut->get_acceptance().is_t())
return false;
// if is TBA type
scc_info si(aut, scc_info_options::TRACK_STATES);
std::vector<bool> final(aut->edge_vector().size(), false);
std::vector<bool> keep(aut->edge_vector().size(), true);
for (unsigned scc = 0; scc < si.scc_count(); ++scc)
if (!is_scc_tba_type(aut, si, scc, keep, aut_pairs, final))
return false;
return true;
}
twa_graph_ptr
rabin_to_buchi_maybe(const const_twa_graph_ptr& aut)
{
......
......@@ -23,6 +23,13 @@
namespace spot
{
/// \ingroup twa_acc_transform
/// \brief Check if \aut is Büchi-realizable. This is inspired
/// from rabin_to_buchi_maybe()'s algorithm. The main difference is that
/// here, no automaton is built.
SPOT_API bool
rabin_is_buchi_realizable(const const_twa_graph_ptr& aut);
/// \ingroup twa_acc_transform
/// \brief Convert a Rabin automaton to Büchi automaton, preserving
/// determinism when possible.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment