alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
spot/spot/twaalgos/cobuchi.cc
Alexandre Duret-Lutz c920825fad work around issue #317 
* spot/twaalgos/cobuchi.cc: Call sbacc() on transition-based input.
* tests/Makefile.am: Remove XFAIL_TESTS.
* NEWS: Adjust.
2018-01-14 22:18:55 +01:00

695 lines
25 KiB
C++
Raw Blame History

// -*- 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 = 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)),
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);
}
}
Reference in a new issue View git blame Copy permalink