3d5b5be693
* spot/twaalgos/cobuchi.cc: Add scc_info_options::TRACK_SUCCS in nsa_to_nca(). * spot/twaalgos/sccinfo.cc: Add scc_info_options::TRACK_SUCCS and is_useful_scc() in states_on_acc_cycle_of().
710 lines
25 KiB
C++
710 lines
25 KiB
C++
// -*- coding: utf-8 -*-
|
|
// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement
|
|
// de l'Epita (LRDE).
|
|
//
|
|
// 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/cobuchi.hh>
|
|
|
|
#include <spot/misc/bddlt.hh>
|
|
#include <spot/misc/bitvect.hh>
|
|
#include <spot/misc/hash.hh>
|
|
#include <spot/twa/acc.hh>
|
|
#include <spot/twa/bddprint.hh>
|
|
#include <spot/twa/twagraph.hh>
|
|
#include <spot/twaalgos/powerset.hh>
|
|
#include <spot/twaalgos/product.hh>
|
|
#include <spot/twaalgos/sccinfo.hh>
|
|
#include <spot/twaalgos/totgba.hh>
|
|
#include <spot/twaalgos/isdet.hh>
|
|
#include <spot/twaalgos/strength.hh>
|
|
#include <spot/twaalgos/sbacc.hh> // For issue #317
|
|
#include <stack>
|
|
#include <unordered_map>
|
|
|
|
#define DEBUG 0
|
|
#if DEBUG
|
|
#define debug std::cerr
|
|
#else
|
|
#define debug while (0) std::cout
|
|
#endif
|
|
|
|
namespace spot
|
|
{
|
|
namespace
|
|
{
|
|
typedef std::pair<unsigned, unsigned> pair_state_nca;
|
|
|
|
// Helper function that returns the called 'augmented subset construction'
|
|
// of the given automaton, i.e. the product of the automaton with its
|
|
// powerset construction.
|
|
//
|
|
// 'aut_power' is the automaton that will be used for the powerset
|
|
// construction and 'aut_prod' is the one that will be used for the
|
|
// product. They may be confusing in the sense that why the same automaton
|
|
// is not used for the product and the powerset construction. Actually,
|
|
// when dealing with an automaton A with Rabin acceptance, it is firstly
|
|
// converted into an automaton B with Streett-like acceptance. The powerset
|
|
// construction of B happens to be isomorphic with the powerset construction
|
|
// of A. Therefore, you would like to use A (which is smaller than B) for
|
|
// the powerset construction and B for the product.
|
|
static
|
|
twa_graph_ptr
|
|
aug_subset_cons(const const_twa_graph_ptr& aut_prod,
|
|
const const_twa_graph_ptr& aut_power,
|
|
bool named_states,
|
|
struct power_map& pmap)
|
|
{
|
|
twa_graph_ptr res = nullptr;
|
|
|
|
if (is_deterministic(aut_prod))
|
|
{
|
|
res = make_twa_graph(aut_prod, twa::prop_set::all());
|
|
auto v = new product_states;
|
|
res->set_named_prop("product-states", v);
|
|
for (unsigned s = 0; s < aut_power->num_states(); ++s)
|
|
v->emplace_back(s, s);
|
|
for (unsigned s = 0; s < aut_power->num_states(); ++s)
|
|
pmap.map_.push_back({s});
|
|
}
|
|
else
|
|
{
|
|
res = product(aut_prod, tgba_powerset(aut_power, pmap));
|
|
}
|
|
|
|
if (named_states)
|
|
{
|
|
const product_states* res_map = res->get_named_prop
|
|
<product_states>("product-states");
|
|
|
|
auto v = new std::vector<std::string>;
|
|
res->set_named_prop("state-names", v);
|
|
|
|
auto get_st_name =
|
|
[&](const pair_state_nca& x)
|
|
{
|
|
std::stringstream os;
|
|
os << x.first << ",{";
|
|
bool not_first = false;
|
|
for (auto& a : pmap.states_of(x.second))
|
|
{
|
|
if (not_first)
|
|
os << ',';
|
|
else
|
|
not_first = true;
|
|
os << a;
|
|
}
|
|
os << '}';
|
|
return os.str();
|
|
};
|
|
|
|
unsigned num_states = res->num_states();
|
|
for (unsigned i = 0; i < num_states; ++i)
|
|
v->emplace_back(get_st_name((*res_map)[i]));
|
|
}
|
|
return res;
|
|
}
|
|
|
|
class nsa_to_nca_converter final
|
|
{
|
|
protected:
|
|
struct power_map pmap_; // Sets of sts (powerset cons.).
|
|
|
|
const_twa_graph_ptr aut_; // The given automaton.
|
|
bool state_based_; // Is it state based?
|
|
std::vector<acc_cond::rs_pair> pairs_; // All pairs of the acc. cond.
|
|
unsigned nb_pairs_; // Nb pair in the acc. cond.
|
|
bool named_states_; // Name states for display?
|
|
twa_graph_ptr res_; // The augmented subset const.
|
|
product_states* res_map_; // States of the aug. sub. cons.
|
|
scc_info si_; // SCC information.
|
|
unsigned nb_states_; // Number of states.
|
|
unsigned was_rabin_; // Was it Rabin before Streett?
|
|
std::vector<unsigned>* orig_states_; // Match old Rabin st. from new.
|
|
unsigned orig_num_st_; // Rabin original nb states.
|
|
|
|
// Keep information of states that are wanted to be seen infinitely
|
|
// often (cf Header).
|
|
void save_inf_nca_st(unsigned s, acc_cond::mark_t m,
|
|
vect_nca_info* nca_info)
|
|
{
|
|
if (was_rabin_ && m)
|
|
{
|
|
for (unsigned p = 0; p < nb_pairs_; ++p)
|
|
if (pairs_[p].fin || m & pairs_[p].inf)
|
|
{
|
|
const pair_state_nca& st = (*res_map_)[s];
|
|
auto bv = make_bitvect(orig_num_st_);
|
|
for (unsigned state : pmap_.states_of(st.second))
|
|
bv->set(state);
|
|
assert(!was_rabin_
|
|
|| ((int)(*orig_states_)[st.first] >= 0));
|
|
unsigned state = was_rabin_ ? (*orig_states_)[st.first]
|
|
: st.first;
|
|
unsigned clause_nb = was_rabin_ ? p / 2 : p;
|
|
nca_info->push_back(new nca_st_info(clause_nb, state, bv));
|
|
}
|
|
}
|
|
else if (!was_rabin_)
|
|
{
|
|
const pair_state_nca& st = (*res_map_)[s];
|
|
auto bv = make_bitvect(aut_->num_states());
|
|
for (unsigned state : pmap_.states_of(st.second))
|
|
bv->set(state);
|
|
nca_info->push_back(new nca_st_info(0, st.first, bv));
|
|
}
|
|
}
|
|
|
|
// Helper function that marks states that we want to see finitely often
|
|
// and save some information about states that we want to see infinitely
|
|
// often (cf Header).
|
|
void set_marks_using(std::vector<bool>& nca_is_inf_state,
|
|
vect_nca_info* nca_info)
|
|
{
|
|
for (unsigned s = 0; s < nb_states_; ++s)
|
|
{
|
|
unsigned src_scc = si_.scc_of(s);
|
|
if (nca_is_inf_state[s])
|
|
{
|
|
acc_cond::mark_t m = 0u;
|
|
for (auto& e : res_->out(s))
|
|
{
|
|
if (nca_info && e.acc && (si_.scc_of(e.dst) == src_scc
|
|
|| state_based_))
|
|
m |= e.acc;
|
|
e.acc = 0u;
|
|
}
|
|
|
|
if (nca_info)
|
|
save_inf_nca_st(s, m, nca_info);
|
|
}
|
|
else
|
|
{
|
|
for (auto& e : res_->out(s))
|
|
{
|
|
if (si_.scc_of(e.dst) == src_scc || state_based_)
|
|
e.acc = acc_cond::mark_t({0});
|
|
else
|
|
e.acc = 0u;
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
public:
|
|
|
|
nsa_to_nca_converter(const const_twa_graph_ptr ref_prod,
|
|
const const_twa_graph_ptr ref_power,
|
|
std::vector<acc_cond::rs_pair>& pairs,
|
|
bool named_states = false,
|
|
bool was_rabin = false,
|
|
unsigned orig_num_st = 0)
|
|
: aut_(ref_prod),
|
|
state_based_(aut_->prop_state_acc().is_true()),
|
|
pairs_(pairs),
|
|
nb_pairs_(pairs.size()),
|
|
named_states_(named_states),
|
|
res_(aug_subset_cons(ref_prod, ref_power, named_states_, pmap_)),
|
|
res_map_(res_->get_named_prop<product_states>("product-states")),
|
|
si_(scc_info(res_, scc_info_options::TRACK_STATES
|
|
| scc_info_options::TRACK_SUCCS)),
|
|
nb_states_(res_->num_states()),
|
|
was_rabin_(was_rabin),
|
|
orig_num_st_(orig_num_st)
|
|
{
|
|
if (was_rabin)
|
|
orig_states_ = ref_prod->get_named_prop<std::vector<unsigned>>
|
|
("original-states");
|
|
}
|
|
|
|
~nsa_to_nca_converter()
|
|
{}
|
|
|
|
twa_graph_ptr run(vect_nca_info* nca_info)
|
|
{
|
|
std::vector<bool> nca_is_inf_state; // Accepting or rejecting sts.
|
|
nca_is_inf_state.resize(nb_states_, false);
|
|
|
|
// Iterate over all SCCs and check for accepting states. A state 's'
|
|
// is accepting if there is a cycle containing 's' that visits
|
|
// finitely often all acceptance sets marked as Fin or infinitely
|
|
// often acceptance sets marked by Inf.
|
|
unsigned nb_scc = si_.scc_count();
|
|
for (unsigned scc = 0; scc < nb_scc; ++scc)
|
|
for (unsigned st : si_.states_on_acc_cycle_of(scc))
|
|
nca_is_inf_state[st] = true;
|
|
|
|
set_marks_using(nca_is_inf_state, nca_info);
|
|
|
|
res_->prop_state_acc(state_based_);
|
|
res_->set_co_buchi();
|
|
res_->merge_edges();
|
|
return res_;
|
|
}
|
|
};
|
|
}
|
|
|
|
|
|
twa_graph_ptr
|
|
nsa_to_nca(const_twa_graph_ptr ref,
|
|
bool named_states,
|
|
vect_nca_info* nca_info)
|
|
{
|
|
if (ref->acc().is_parity())
|
|
ref = to_generalized_streett(ref);
|
|
|
|
std::vector<acc_cond::rs_pair> pairs;
|
|
if (!ref->acc().is_streett_like(pairs))
|
|
throw std::runtime_error("nsa_to_nca() only works with Streett-like or "
|
|
"Parity acceptance condition");
|
|
|
|
// FIXME: At the moment this algorithm does not support
|
|
// transition-based acceptance. See issue #317. Once that is
|
|
// fixed we may remove the next line.
|
|
ref = sbacc(std::const_pointer_cast<twa_graph>(ref));
|
|
|
|
nsa_to_nca_converter nca_converter(ref, ref, pairs, named_states, false);
|
|
return nca_converter.run(nca_info);
|
|
}
|
|
|
|
|
|
twa_graph_ptr
|
|
dnf_to_nca(const_twa_graph_ptr ref, bool named_states,
|
|
vect_nca_info* nca_info)
|
|
{
|
|
const acc_cond::acc_code& code = ref->get_acceptance();
|
|
if (!code.is_dnf())
|
|
throw std::runtime_error("dnf_to_nca() only works with DNF acceptance "
|
|
"condition");
|
|
|
|
// FIXME: At the moment this algorithm does not support
|
|
// transition-based acceptance. See issue #317. Once that is
|
|
// fixed we may remove the next line.
|
|
ref = sbacc(std::const_pointer_cast<twa_graph>(ref));
|
|
|
|
auto streett_aut = spot::dnf_to_streett(ref, true);
|
|
|
|
std::vector<acc_cond::rs_pair> pairs;
|
|
if (!streett_aut->acc().is_streett_like(pairs))
|
|
throw std::runtime_error("dnf_to_nca() could not convert the original "
|
|
"automaton into an intermediate Streett-like automaton");
|
|
|
|
nsa_to_nca_converter nca_converter(streett_aut,
|
|
ref,
|
|
pairs,
|
|
named_states,
|
|
true,
|
|
ref->num_states());
|
|
return nca_converter.run(nca_info);
|
|
}
|
|
|
|
namespace
|
|
{
|
|
twa_graph_ptr
|
|
weak_to_cobuchi(const const_twa_graph_ptr& aut)
|
|
{
|
|
trival iw = aut->prop_inherently_weak();
|
|
if (iw.is_false())
|
|
return nullptr;
|
|
scc_info si(aut);
|
|
if (iw.is_maybe() && !is_weak_automaton(aut, &si))
|
|
return nullptr;
|
|
auto res = make_twa_graph(aut->get_dict());
|
|
res->copy_ap_of(aut);
|
|
res->prop_copy(aut, twa::prop_set::all());
|
|
res->new_states(aut->num_states());
|
|
si.determine_unknown_acceptance();
|
|
unsigned ns = si.scc_count();
|
|
for (unsigned s = 0; s < ns; ++s)
|
|
{
|
|
acc_cond::mark_t m = 0U;
|
|
if (si.is_rejecting_scc(s))
|
|
m = acc_cond::mark_t{0};
|
|
else
|
|
assert(si.is_accepting_scc(s));
|
|
|
|
for (auto& e: si.edges_of(s))
|
|
res->new_edge(e.src, e.dst, e.cond, m);
|
|
}
|
|
res->set_co_buchi();
|
|
res->set_init_state(aut->get_init_state_number());
|
|
res->prop_weak(true);
|
|
res->prop_state_acc(true);
|
|
return res;
|
|
}
|
|
}
|
|
|
|
twa_graph_ptr
|
|
to_nca(const_twa_graph_ptr aut, bool named_states)
|
|
{
|
|
if (auto weak = weak_to_cobuchi(aut))
|
|
return weak;
|
|
|
|
const acc_cond::acc_code& code = aut->get_acceptance();
|
|
|
|
std::vector<acc_cond::rs_pair> pairs;
|
|
if (aut->acc().is_streett_like(pairs) || aut->acc().is_parity())
|
|
return nsa_to_nca(aut, named_states);
|
|
else if (code.is_dnf())
|
|
return dnf_to_nca(aut, named_states);
|
|
|
|
auto tmp = make_twa_graph(aut, twa::prop_set::all());
|
|
tmp->set_acceptance(aut->acc().num_sets(),
|
|
aut->get_acceptance().to_dnf());
|
|
return to_nca(tmp, named_states);
|
|
}
|
|
|
|
namespace
|
|
{
|
|
struct mp_hash
|
|
{
|
|
size_t
|
|
operator()(std::pair<unsigned, const bitvect_array*> bv) const noexcept
|
|
{
|
|
size_t res = 0;
|
|
size_t size = bv.second->size();
|
|
for (unsigned i = 0; i < size; ++i)
|
|
res = wang32_hash(res ^ wang32_hash(bv.second->at(i).hash()));
|
|
res = wang32_hash(res ^ bv.first);
|
|
return res;
|
|
}
|
|
};
|
|
|
|
struct mp_equal
|
|
{
|
|
bool operator()(std::pair<unsigned, const bitvect_array*> bvl,
|
|
std::pair<unsigned, const bitvect_array*> bvr) const
|
|
{
|
|
if (bvl.first != bvr.first)
|
|
return false;
|
|
size_t size = bvl.second->size();
|
|
for (unsigned i = 0; i < size; ++i)
|
|
if (bvl.second->at(i) != bvr.second->at(i))
|
|
return false;
|
|
return true;
|
|
}
|
|
};
|
|
|
|
typedef std::unordered_map
|
|
<std::pair<unsigned, const bitvect_array*>, unsigned, mp_hash, mp_equal>
|
|
dca_st_mapping;
|
|
class dca_breakpoint_cons final
|
|
{
|
|
protected:
|
|
const_twa_graph_ptr aut_; // The given automaton.
|
|
vect_nca_info* nca_info_; // Info (cf Header).
|
|
unsigned nb_copy_; // != 0 if was Rabin.
|
|
bdd ap_; // All AP.
|
|
std::vector<bdd> num2bdd_; // Get bdd from AP num.
|
|
std::map<bdd, unsigned, bdd_less_than> bdd2num_; // Get AP num from bdd.
|
|
|
|
// Each state is characterized by a bitvect_array of 2 bitvects:
|
|
// bv1 -> the set of original states that it represents
|
|
// bv2 -> a set of marked states (~)
|
|
// To do so, we keep a correspondance between a state number and its
|
|
// bitvect representation.
|
|
dca_st_mapping bv_to_num_;
|
|
std::vector<std::pair<unsigned, bitvect_array*>> num_2_bv_;
|
|
|
|
// Next states to process.
|
|
std::stack<std::pair<std::pair<unsigned, bitvect_array*>, unsigned>>
|
|
todo_;
|
|
// All allocated bitvect that must be freed at the end.
|
|
std::vector<const bitvect_array*> toclean_;
|
|
|
|
public:
|
|
dca_breakpoint_cons(const const_twa_graph_ptr aut,
|
|
vect_nca_info* nca_info,
|
|
unsigned nb_copy)
|
|
: aut_(aut),
|
|
nca_info_(nca_info),
|
|
nb_copy_(nb_copy),
|
|
ap_(aut->ap_vars())
|
|
{
|
|
// Get all bdds.
|
|
bdd all = bddtrue;
|
|
for (unsigned i = 0; all != bddfalse; ++i)
|
|
{
|
|
bdd one = bdd_satoneset(all, ap_, bddfalse);
|
|
num2bdd_.push_back(one);
|
|
bdd2num_[one] = i;
|
|
all -= one;
|
|
}
|
|
}
|
|
|
|
~dca_breakpoint_cons()
|
|
{
|
|
for (auto p : *nca_info_)
|
|
delete p;
|
|
}
|
|
|
|
twa_graph_ptr run(bool named_states)
|
|
{
|
|
unsigned ns = aut_->num_states();
|
|
unsigned nc = num2bdd_.size();
|
|
|
|
// Fill bv_aut_trans_ which is a bitvect of all possible transitions
|
|
// of each state for each letter.
|
|
auto bv_aut_trans_ = std::unique_ptr<bitvect_array>(
|
|
make_bitvect_array(ns, ns * nc));
|
|
for (unsigned src = 0; src < ns; ++src)
|
|
{
|
|
size_t base = src * nc;
|
|
for (auto& t: aut_->out(src))
|
|
{
|
|
bdd all = t.cond;
|
|
while (all != bddfalse)
|
|
{
|
|
bdd one = bdd_satoneset(all, ap_, bddfalse);
|
|
all -= one;
|
|
bv_aut_trans_->at(base + bdd2num_[one]).set(t.dst);
|
|
}
|
|
}
|
|
}
|
|
debug << "All_states:\n" << *bv_aut_trans_ << std::endl;
|
|
|
|
twa_graph_ptr res = make_twa_graph(aut_->get_dict());
|
|
res->copy_ap_of(aut_);
|
|
res->set_co_buchi();
|
|
|
|
// Rename states of resulting automata (for display purposes).
|
|
std::vector<std::string>* state_name = nullptr;
|
|
if (named_states)
|
|
{
|
|
state_name = new std::vector<std::string>();
|
|
res->set_named_prop("state-names", state_name);
|
|
}
|
|
|
|
// Function used to add a new state. A new state number is associated
|
|
// to the state if has never been added before, otherwise the old
|
|
// state number is returned.
|
|
auto new_state = [&](std::pair<unsigned, bitvect_array*> bv_st)
|
|
-> unsigned
|
|
{
|
|
auto p = bv_to_num_.emplace(bv_st, 0);
|
|
if (!p.second)
|
|
return p.first->second;
|
|
|
|
p.first->second = res->new_state();
|
|
todo_.emplace(bv_st, p.first->second);
|
|
assert(num_2_bv_.size() == p.first->second);
|
|
num_2_bv_.push_back(bv_st);
|
|
|
|
// For display purposes only.
|
|
if (named_states)
|
|
{
|
|
assert(p.first->second == state_name->size());
|
|
std::ostringstream os;
|
|
bool not_first = false;
|
|
os << '{';
|
|
for (unsigned s = 0; s < ns; ++s)
|
|
{
|
|
if (bv_st.second->at(1).get(s))
|
|
{
|
|
if (not_first)
|
|
os << ',';
|
|
else
|
|
not_first = true;
|
|
os << '~';
|
|
}
|
|
if (bv_st.second->at(0).get(s))
|
|
os << s;
|
|
}
|
|
os << '|' << bv_st.first << '}';
|
|
state_name->emplace_back(os.str());
|
|
}
|
|
return p.first->second;
|
|
};
|
|
|
|
// Set init state
|
|
auto bv_init = make_bitvect_array(ns, 2);
|
|
toclean_.push_back(bv_init);
|
|
bv_init->at(0).set(aut_->get_init_state_number());
|
|
res->set_init_state(new_state(std::make_pair(0, bv_init)));
|
|
|
|
// Processing loop
|
|
while (!todo_.empty())
|
|
{
|
|
auto top = todo_.top();
|
|
todo_.pop();
|
|
|
|
// Bitvect array of all possible moves for each letter.
|
|
auto bv_trans = make_bitvect_array(ns, nc);
|
|
for (unsigned s = 0; s < ns; ++s)
|
|
if (top.first.second->at(0).get(s))
|
|
for (unsigned l = 0; l < nc; ++l)
|
|
bv_trans->at(l) |= bv_aut_trans_->at(s * nc + l);
|
|
toclean_.push_back(bv_trans);
|
|
|
|
// Bitvect array of all possible moves for each state marked
|
|
// for each letter. If no state is marked (breakpoint const.),
|
|
// nothing is set.
|
|
bool marked = !top.first.second->at(1).is_fully_clear();
|
|
auto bv_trans_mark = make_bitvect_array(ns, nc);
|
|
if (marked)
|
|
for (unsigned s = 0; s < ns; ++s)
|
|
if (top.first.second->at(1).get(s))
|
|
for (unsigned l = 0; l < nc; ++l)
|
|
bv_trans_mark->at(l) |= bv_aut_trans_->at(s * nc + l);
|
|
toclean_.push_back(bv_trans_mark);
|
|
|
|
debug << "src:" << top.second << std::endl;
|
|
for (unsigned l = 0; l < nc; ++l)
|
|
{
|
|
debug << "l:"
|
|
<< bdd_format_formula(aut_->get_dict(), num2bdd_[l])
|
|
<< '\n';
|
|
|
|
auto bv_res = make_bitvect_array(ns, 2);
|
|
toclean_.push_back(bv_res);
|
|
bv_res->at(0) |= bv_trans->at(l);
|
|
// If this state has not any outgoing edges.
|
|
if (bv_res->at(0).is_fully_clear())
|
|
continue;
|
|
|
|
// Set states that must be marked.
|
|
for (const auto& p : *nca_info_)
|
|
{
|
|
if (p->clause_num != top.first.first)
|
|
continue;
|
|
|
|
if (*p->all_dst == bv_res->at(0))
|
|
if ((marked && bv_trans_mark->at(l).get(p->state_num))
|
|
|| (!marked && bv_res->at(0).get(p->state_num)))
|
|
bv_res->at(1).set(p->state_num);
|
|
}
|
|
|
|
unsigned i = bv_res->at(1).is_fully_clear() ?
|
|
(top.first.first + 1) % (nb_copy_ + 1)
|
|
: top.first.first;
|
|
|
|
debug << "dest\n" << *bv_res << "i: " << i
|
|
<< std::endl;
|
|
res->new_edge(top.second,
|
|
new_state(std::make_pair(i, bv_res)),
|
|
num2bdd_[l]);
|
|
}
|
|
debug << '\n';
|
|
}
|
|
|
|
// Set accepting states.
|
|
scc_info si(res);
|
|
bool state_based = (bool)aut_->prop_state_acc();
|
|
unsigned res_size = res->num_states();
|
|
for (unsigned s = 0; s < res_size; ++s)
|
|
if (num_2_bv_[s].second->at(1).is_fully_clear())
|
|
for (auto& edge : res->out(s))
|
|
if (si.scc_of(edge.dst) == si.scc_of(s) || state_based)
|
|
edge.acc = acc_cond::mark_t({0});
|
|
|
|
// Delete all bitvect arrays allocated by this method (run).
|
|
for (auto v: toclean_)
|
|
delete v;
|
|
|
|
res->merge_edges();
|
|
return res;
|
|
}
|
|
};
|
|
}
|
|
|
|
|
|
twa_graph_ptr
|
|
nsa_to_dca(const_twa_graph_ptr aut, bool named_states)
|
|
{
|
|
debug << "NSA_to_dca" << std::endl;
|
|
std::vector<acc_cond::rs_pair> pairs;
|
|
if (!aut->acc().is_streett_like(pairs) && !aut->acc().is_parity())
|
|
throw std::runtime_error("nsa_to_dca() only works with Streett-like or "
|
|
"Parity acceptance condition");
|
|
|
|
// FIXME: At the moment this algorithm does not support
|
|
// transition-based acceptance. See issue #317. Once that is
|
|
// fixed we may remove the next line.
|
|
aut = sbacc(std::const_pointer_cast<twa_graph>(aut));
|
|
|
|
// Get states that must be visited infinitely often in NCA.
|
|
vect_nca_info nca_info;
|
|
nsa_to_nca(aut, named_states, &nca_info);
|
|
|
|
#if DEBUG
|
|
debug << "PRINTING INFO" << std::endl;
|
|
for (unsigned i = 0; i < nca_info.size(); ++i)
|
|
debug << '<' << nca_info[i]->clause_num << ',' << nca_info[i]->state_num
|
|
<< ',' << nca_info[i]->all_dst << '>' << std::endl;
|
|
#endif
|
|
|
|
dca_breakpoint_cons dca(aut, &nca_info, 0);
|
|
return dca.run(named_states);
|
|
}
|
|
|
|
|
|
twa_graph_ptr
|
|
dnf_to_dca(const_twa_graph_ptr aut, bool named_states)
|
|
{
|
|
debug << "DNF_to_dca" << std::endl;
|
|
const acc_cond::acc_code& code = aut->get_acceptance();
|
|
std::vector<acc_cond::rs_pair> pairs;
|
|
if (!code.is_dnf())
|
|
throw std::runtime_error("dnf_to_dca() only works with DNF (Rabin-like "
|
|
"included) acceptance condition");
|
|
|
|
// FIXME: At the moment this algorithm does not support
|
|
// transition-based acceptance. See issue #317. Once that is
|
|
// fixed we may remove the next line.
|
|
aut = sbacc(std::const_pointer_cast<twa_graph>(aut));
|
|
|
|
// Get states that must be visited infinitely often in NCA.
|
|
vect_nca_info nca_info;
|
|
dnf_to_nca(aut, false, &nca_info);
|
|
|
|
#if DEBUG
|
|
debug << "PRINTING INFO" << std::endl;
|
|
for (unsigned i = 0; i < nca_info.size(); ++i)
|
|
debug << '<' << nca_info[i]->clause_num << ',' << nca_info[i]->state_num
|
|
<< ',' << nca_info[i]->all_dst << '>' << std::endl;
|
|
#endif
|
|
|
|
unsigned nb_copy = 0;
|
|
for (const auto& p : nca_info)
|
|
if (nb_copy < p->clause_num)
|
|
nb_copy = p->clause_num;
|
|
|
|
dca_breakpoint_cons dca(aut, &nca_info, nb_copy);
|
|
return dca.run(named_states);
|
|
}
|
|
|
|
|
|
twa_graph_ptr
|
|
to_dca(const_twa_graph_ptr aut, bool named_states)
|
|
{
|
|
if (is_deterministic(aut))
|
|
if (auto weak = weak_to_cobuchi(aut))
|
|
return weak;
|
|
|
|
const acc_cond::acc_code& code = aut->get_acceptance();
|
|
|
|
std::vector<acc_cond::rs_pair> pairs;
|
|
if (aut->acc().is_streett_like(pairs) || aut->acc().is_parity())
|
|
return nsa_to_dca(aut, named_states);
|
|
else if (code.is_dnf())
|
|
return dnf_to_dca(aut, named_states);
|
|
|
|
auto tmp = make_twa_graph(aut, twa::prop_set::all());
|
|
tmp->set_acceptance(aut->acc().num_sets(),
|
|
aut->get_acceptance().to_dnf());
|
|
return to_nca(tmp, named_states);
|
|
}
|
|
}
|