remove parity_product and parity_product_or
* NEWS: document it * spot/twaalgos/parity.cc, spot/twaalgos/parity.hh, tests/core/parity.cc: here
This commit is contained in:
Maximilien Colange
parent
8120587fbf
commit
1aaeccf1d3
4 changed files with 4 additions and 451 deletions
4
NEWS
4
NEWS
|
|
@ -84,6 +84,10 @@ New in spot 2.5.3.dev (not yet released)
|
||||||
They are most welcome in Python, since we used to redefine
|
They are most welcome in Python, since we used to redefine
|
||||||
them every now and them.
|
them every now and them.
|
||||||
|
|
||||||
|
- spot::parity_product() and spot::parity_product_or() were dropped.
|
||||||
|
The code was buggy, hard to maintain, and these functions do not
|
||||||
|
seem to be used.
|
||||||
|
|
||||||
Python:
|
Python:
|
||||||
|
|
||||||
- New spot.jupyter package. This currently contains a function for
|
- New spot.jupyter package. This currently contains a function for
|
||||||
|
|
|
||||||
|
|
@ -338,350 +338,4 @@ namespace spot
|
||||||
return aut;
|
return aut;
|
||||||
}
|
}
|
||||||
|
|
||||||
namespace
|
|
||||||
{
|
|
||||||
using state_history_value_t = unsigned;
|
|
||||||
|
|
||||||
class state_history : public std::vector<state_history_value_t>
|
|
||||||
{
|
|
||||||
public:
|
|
||||||
|
|
||||||
using value_t = state_history_value_t;
|
|
||||||
|
|
||||||
state_history(unsigned left_num_sets, unsigned right_num_sets) :
|
|
||||||
left_num_sets_(left_num_sets),
|
|
||||||
right_num_sets_(right_num_sets)
|
|
||||||
{
|
|
||||||
resize(left_num_sets + right_num_sets, 0);
|
|
||||||
}
|
|
||||||
|
|
||||||
value_t get_left(value_t right) const
|
|
||||||
{
|
|
||||||
return get(right, true);
|
|
||||||
}
|
|
||||||
|
|
||||||
value_t get_right(value_t left) const
|
|
||||||
{
|
|
||||||
return get(left, false);
|
|
||||||
}
|
|
||||||
|
|
||||||
void set_left(value_t right, value_t val)
|
|
||||||
{
|
|
||||||
set(right, true, val);
|
|
||||||
}
|
|
||||||
|
|
||||||
void set_right(value_t left, value_t val)
|
|
||||||
{
|
|
||||||
set(left, false, val);
|
|
||||||
}
|
|
||||||
|
|
||||||
unsigned get_left_num_sets() const
|
|
||||||
{
|
|
||||||
return left_num_sets_;
|
|
||||||
}
|
|
||||||
|
|
||||||
unsigned get_right_num_sets() const
|
|
||||||
{
|
|
||||||
return right_num_sets_;
|
|
||||||
}
|
|
||||||
|
|
||||||
value_t get_max_acc_set(bool and_cond) const
|
|
||||||
{
|
|
||||||
// i is the index of the resulting automaton acceptance set
|
|
||||||
// If i is even, it means that the according set is a set with
|
|
||||||
// transitions that need to be infinitly often as the
|
|
||||||
// acceptance is a parity even. Then k, the index of the
|
|
||||||
// first automaton must be even too.
|
|
||||||
unsigned l = right_num_sets_;
|
|
||||||
while (l-- > 0)
|
|
||||||
{
|
|
||||||
auto k = get_left(l);
|
|
||||||
bool can_jump = and_cond ? (k & l & 1) != 1 : ((k | l) & 1) != 0;
|
|
||||||
if (!can_jump)
|
|
||||||
--k;
|
|
||||||
auto new_l = get_right(k);
|
|
||||||
if (new_l >= l)
|
|
||||||
return k + l;
|
|
||||||
else if (can_jump)
|
|
||||||
l = new_l + 1;
|
|
||||||
}
|
|
||||||
return 0;
|
|
||||||
}
|
|
||||||
|
|
||||||
state_history make_succ(value_t left_acc_set,
|
|
||||||
value_t right_acc_set) const
|
|
||||||
{
|
|
||||||
auto mat = state_history(left_num_sets_, right_num_sets_);
|
|
||||||
for (unsigned i = 0; i < right_num_sets_; ++i)
|
|
||||||
{
|
|
||||||
auto old = get_left(i);
|
|
||||||
mat.set_left(i, std::max(left_acc_set, old));
|
|
||||||
}
|
|
||||||
for (unsigned i = 0; i < left_num_sets_; ++i)
|
|
||||||
{
|
|
||||||
auto old = get_right(i);
|
|
||||||
mat.set_right(i, std::max(right_acc_set, old));
|
|
||||||
}
|
|
||||||
return mat;
|
|
||||||
}
|
|
||||||
|
|
||||||
void clean_here()
|
|
||||||
{
|
|
||||||
auto mat = state_history(*this);
|
|
||||||
for (unsigned l = 0; l < right_num_sets_; ++l)
|
|
||||||
{
|
|
||||||
set_left(l, 0);
|
|
||||||
for (unsigned k = 0; k < left_num_sets_; ++k)
|
|
||||||
{
|
|
||||||
if (mat.get_right(k) < l)
|
|
||||||
set_left(l, std::min(mat.get_left(l), k));
|
|
||||||
else
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
for (unsigned k = 0; k < left_num_sets_; ++k)
|
|
||||||
{
|
|
||||||
set_right(k, 0);
|
|
||||||
for (unsigned l = 0; l < right_num_sets_; ++l)
|
|
||||||
{
|
|
||||||
if (mat.get_left(l) < k)
|
|
||||||
set_right(k, std::min(mat.get_right(k), l));
|
|
||||||
else
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
private:
|
|
||||||
const unsigned left_num_sets_;
|
|
||||||
const unsigned right_num_sets_;
|
|
||||||
|
|
||||||
value_t get(value_t index, bool first) const
|
|
||||||
{
|
|
||||||
return at(index + (first ? 0 : right_num_sets_));
|
|
||||||
}
|
|
||||||
|
|
||||||
void set(value_t index, bool first, value_t val)
|
|
||||||
{
|
|
||||||
at(index + (first ? 0 : right_num_sets_)) = val;
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
struct state_history_hash
|
|
||||||
{
|
|
||||||
size_t
|
|
||||||
operator()(const state_history& mat) const noexcept
|
|
||||||
{
|
|
||||||
unsigned result = 0;
|
|
||||||
for (unsigned i = 0; i < mat.get_left_num_sets(); ++i)
|
|
||||||
result = wang32_hash(result ^ wang32_hash(mat.get_right(i)));
|
|
||||||
for (unsigned i = 0; i < mat.get_right_num_sets(); ++i)
|
|
||||||
result = wang32_hash(result ^ wang32_hash(mat.get_left(i)));
|
|
||||||
return result;
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
using sh_label_t = unsigned;
|
|
||||||
|
|
||||||
class state_history_set
|
|
||||||
{
|
|
||||||
private:
|
|
||||||
using value_t = state_history::value_t;
|
|
||||||
|
|
||||||
public:
|
|
||||||
sh_label_t
|
|
||||||
push_state_history(state_history sh)
|
|
||||||
{
|
|
||||||
auto p = sh2l_.emplace(sh, 0);
|
|
||||||
if (p.second)
|
|
||||||
{
|
|
||||||
l2sh_.push_back(p.first);
|
|
||||||
p.first->second = l2sh_.size() - 1;
|
|
||||||
}
|
|
||||||
return p.first->second;
|
|
||||||
}
|
|
||||||
|
|
||||||
std::pair<sh_label_t, value_t>
|
|
||||||
push_state_history(sh_label_t label, value_t left_acc_set,
|
|
||||||
value_t right_acc_set, bool and_cond)
|
|
||||||
{
|
|
||||||
state_history new_sh = l2sh_[label]->first;
|
|
||||||
auto succ = new_sh.make_succ(left_acc_set, right_acc_set);
|
|
||||||
auto max_acc_set = succ.get_max_acc_set(and_cond);
|
|
||||||
succ.clean_here();
|
|
||||||
return std::make_pair(push_state_history(succ), max_acc_set);
|
|
||||||
}
|
|
||||||
|
|
||||||
std::pair<sh_label_t, value_t>
|
|
||||||
get_succ(sh_label_t current_sh, value_t left_acc_set,
|
|
||||||
value_t right_acc_set, bool and_cond)
|
|
||||||
{
|
|
||||||
auto f_args = std::make_tuple(current_sh, left_acc_set, right_acc_set);
|
|
||||||
auto p = succ_.emplace(f_args, std::make_pair(0, 0));
|
|
||||||
if (p.second)
|
|
||||||
{
|
|
||||||
p.first->second =
|
|
||||||
push_state_history(current_sh, left_acc_set,
|
|
||||||
right_acc_set, and_cond);
|
|
||||||
}
|
|
||||||
return p.first->second;
|
|
||||||
}
|
|
||||||
|
|
||||||
private:
|
|
||||||
using sh_dict_t = std::unordered_map<const state_history,
|
|
||||||
value_t,
|
|
||||||
state_history_hash>;
|
|
||||||
sh_dict_t sh2l_;
|
|
||||||
|
|
||||||
struct sh_succ_hash
|
|
||||||
{
|
|
||||||
size_t
|
|
||||||
operator()(std::tuple<sh_label_t, value_t, value_t> x) const noexcept
|
|
||||||
{
|
|
||||||
return wang32_hash(std::get<0>(x) ^ wang32_hash(std::get<1>(x)
|
|
||||||
^ wang32_hash(std::get<2>(x))));
|
|
||||||
}
|
|
||||||
};
|
|
||||||
std::unordered_map<std::tuple<sh_label_t, value_t, value_t>,
|
|
||||||
std::pair<sh_label_t, value_t>,
|
|
||||||
sh_succ_hash> succ_;
|
|
||||||
std::vector<sh_dict_t::const_iterator> l2sh_;
|
|
||||||
};
|
|
||||||
|
|
||||||
using product_state_t = std::tuple<unsigned, unsigned, sh_label_t>;
|
|
||||||
|
|
||||||
struct product_state_hash
|
|
||||||
{
|
|
||||||
size_t
|
|
||||||
operator()(product_state_t s) const noexcept
|
|
||||||
{
|
|
||||||
return wang32_hash(std::get<0>(s) ^ wang32_hash(std::get<1>(s)
|
|
||||||
^ wang32_hash(std::get<2>(s))));
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
|
|
||||||
twa_graph_ptr
|
|
||||||
parity_product_aux(const const_twa_graph_ptr& first,
|
|
||||||
const const_twa_graph_ptr& second,
|
|
||||||
bool and_cond)
|
|
||||||
{
|
|
||||||
auto left = change_parity(first, parity_kind_max, parity_style_even);
|
|
||||||
auto right = change_parity(second, parity_kind_max, parity_style_even);
|
|
||||||
if (!and_cond)
|
|
||||||
{
|
|
||||||
complete_here(left);
|
|
||||||
complete_here(right);
|
|
||||||
}
|
|
||||||
cleanup_parity_here(left, true);
|
|
||||||
cleanup_parity_here(right, true);
|
|
||||||
colorize_parity_here(left, true);
|
|
||||||
colorize_parity_here(right, true);
|
|
||||||
std::unordered_map<product_state_t, unsigned, product_state_hash> s2n;
|
|
||||||
state_history_set sh_set;
|
|
||||||
std::queue<std::pair<product_state_t, unsigned>> todo;
|
|
||||||
auto res = make_twa_graph(left->get_dict());
|
|
||||||
res->copy_ap_of(left);
|
|
||||||
res->copy_ap_of(right);
|
|
||||||
unsigned left_num_sets = left->num_sets();
|
|
||||||
unsigned right_num_sets = right->num_sets();
|
|
||||||
unsigned z_size = left_num_sets + right_num_sets - 1;
|
|
||||||
auto z = acc_cond::acc_code::parity(true, !and_cond, z_size);
|
|
||||||
res->set_acceptance(z_size, z);
|
|
||||||
|
|
||||||
auto v = new product_states;
|
|
||||||
res->set_named_prop("product-states", v);
|
|
||||||
|
|
||||||
auto new_state =
|
|
||||||
[&](const sh_label_t sh_label,
|
|
||||||
unsigned left_state, unsigned right_state,
|
|
||||||
unsigned left_acc_set, unsigned right_acc_set)
|
|
||||||
-> std::pair<unsigned, unsigned>
|
|
||||||
{
|
|
||||||
auto succ = sh_set.get_succ(sh_label, left_acc_set, right_acc_set,
|
|
||||||
and_cond);
|
|
||||||
product_state_t x(left_state, right_state, succ.first);
|
|
||||||
auto p = s2n.emplace(x, 0);
|
|
||||||
if (p.second) // This is a new state
|
|
||||||
{
|
|
||||||
auto new_state = res->new_state();
|
|
||||||
p.first->second = new_state;
|
|
||||||
v->push_back(std::make_pair(left_state, right_state));
|
|
||||||
todo.emplace(x, new_state);
|
|
||||||
}
|
|
||||||
return std::make_pair(p.first->second, succ.second);
|
|
||||||
};
|
|
||||||
|
|
||||||
state_history init_state_history(left_num_sets, right_num_sets);
|
|
||||||
auto init_sh_label = sh_set.push_state_history(init_state_history);
|
|
||||||
product_state_t init_state(left->get_init_state_number(),
|
|
||||||
right->get_init_state_number(), init_sh_label);
|
|
||||||
auto init_state_index = res->new_state();
|
|
||||||
s2n.emplace(init_state, init_state_index);
|
|
||||||
todo.emplace(init_state, init_state_index);
|
|
||||||
res->set_init_state(init_state_index);
|
|
||||||
|
|
||||||
while (!todo.empty())
|
|
||||||
{
|
|
||||||
auto& top = todo.front();
|
|
||||||
for (auto& l: left->out(std::get<0>(top.first)))
|
|
||||||
for (auto& r: right->out(std::get<1>(top.first)))
|
|
||||||
{
|
|
||||||
auto cond = l.cond & r.cond;
|
|
||||||
if (cond == bddfalse)
|
|
||||||
continue;
|
|
||||||
auto left_acc = l.acc.max_set() - 1;
|
|
||||||
auto right_acc = r.acc.max_set() - 1;
|
|
||||||
auto dst = new_state(std::get<2>(top.first), l.dst, r.dst,
|
|
||||||
left_acc, right_acc);
|
|
||||||
auto acc = acc_cond::mark_t{dst.second};
|
|
||||||
res->new_edge(top.second, dst.first, cond, acc);
|
|
||||||
}
|
|
||||||
todo.pop();
|
|
||||||
}
|
|
||||||
|
|
||||||
// The product of two non-deterministic automata could be
|
|
||||||
// deterministic. likewise for non-complete automata.
|
|
||||||
if (left->prop_universal() && right->prop_universal())
|
|
||||||
res->prop_universal(true);
|
|
||||||
if (left->prop_complete() && right->prop_complete())
|
|
||||||
res->prop_complete(true);
|
|
||||||
if (left->prop_stutter_invariant() && right->prop_stutter_invariant())
|
|
||||||
res->prop_stutter_invariant(true);
|
|
||||||
if (left->prop_inherently_weak() && right->prop_inherently_weak())
|
|
||||||
res->prop_inherently_weak(true);
|
|
||||||
if (left->prop_weak() && right->prop_weak())
|
|
||||||
res->prop_weak(true);
|
|
||||||
if (left->prop_terminal() && right->prop_terminal())
|
|
||||||
res->prop_terminal(true);
|
|
||||||
res->prop_state_acc(left->prop_state_acc() && right->prop_state_acc());
|
|
||||||
return res;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
twa_graph_ptr
|
|
||||||
parity_product(const const_twa_graph_ptr& left,
|
|
||||||
const const_twa_graph_ptr& right)
|
|
||||||
{
|
|
||||||
if (left->get_dict() != right->get_dict())
|
|
||||||
throw std::runtime_error("parity_product: left and right automata "
|
|
||||||
"should share their bdd_dict");
|
|
||||||
if (!(left->is_existential() && right->is_existential()))
|
|
||||||
throw std::runtime_error("parity_product() does not support alternating "
|
|
||||||
"automata");
|
|
||||||
return parity_product_aux(left, right, true);
|
|
||||||
}
|
|
||||||
|
|
||||||
twa_graph_ptr
|
|
||||||
parity_product_or(const const_twa_graph_ptr& left,
|
|
||||||
const const_twa_graph_ptr& right)
|
|
||||||
{
|
|
||||||
if (left->get_dict() != right->get_dict())
|
|
||||||
throw std::runtime_error("parity_product_or: left and right automata "
|
|
||||||
"should share their bdd_dict");
|
|
||||||
if (!(left->is_existential() && right->is_existential()))
|
|
||||||
throw std::runtime_error("parity_product_or() does not support "
|
|
||||||
"alternating automata");
|
|
||||||
return parity_product_aux(left, right, false);
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -133,39 +133,4 @@ namespace spot
|
||||||
SPOT_API twa_graph_ptr
|
SPOT_API twa_graph_ptr
|
||||||
colorize_parity_here(twa_graph_ptr aut, bool keep_style = false);
|
colorize_parity_here(twa_graph_ptr aut, bool keep_style = false);
|
||||||
/// @}
|
/// @}
|
||||||
|
|
||||||
/// \brief Construct a product performing the intersection of two automata
|
|
||||||
/// with parity acceptance and keeping their parity acceptance
|
|
||||||
///
|
|
||||||
/// This is based on an algorithm introduced by Olivier Carton (Theoretical
|
|
||||||
/// Computer Science 161, 1-2 (1996)). The output is a parity max even
|
|
||||||
/// automaton. The inputs must be automata with a parity acceptance, otherwise
|
|
||||||
/// an invalid_argument exception is thrown.
|
|
||||||
///
|
|
||||||
/// \param left the first automaton
|
|
||||||
///
|
|
||||||
/// \param right the second automaton
|
|
||||||
///
|
|
||||||
/// \result the product, which is a parity automaton
|
|
||||||
SPOT_API twa_graph_ptr
|
|
||||||
parity_product(const const_twa_graph_ptr& left,
|
|
||||||
const const_twa_graph_ptr& right);
|
|
||||||
|
|
||||||
/// \brief Construct a product performing the union of two automata
|
|
||||||
/// with parity acceptance and keeping their parity acceptance
|
|
||||||
///
|
|
||||||
/// This is based on an algorithm introduced by Olivier Carton (Theoretical
|
|
||||||
/// Computer Science 161, 1-2 (1996)). The output is a parity max even
|
|
||||||
/// automaton. The inputs must be automata with a parity acceptance, otherwise
|
|
||||||
/// an invalid_argument exception is thrown.
|
|
||||||
///
|
|
||||||
/// \param left the first automaton
|
|
||||||
///
|
|
||||||
/// \param right the second automaton
|
|
||||||
///
|
|
||||||
/// \result the sum which is a parity automaton
|
|
||||||
SPOT_API twa_graph_ptr
|
|
||||||
parity_product_or(const const_twa_graph_ptr& left,
|
|
||||||
const const_twa_graph_ptr& right);
|
|
||||||
/// @}
|
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -385,75 +385,5 @@ int main()
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
std::random_shuffle(automata_tuples.begin(), automata_tuples.end());
|
|
||||||
unsigned num_left = 15;
|
|
||||||
unsigned num_right = 15;
|
|
||||||
unsigned acc_index = 0;
|
|
||||||
|
|
||||||
unsigned nb = 0;
|
|
||||||
// Parity product and sum
|
|
||||||
for (unsigned left_index = 0; left_index < num_left; ++left_index)
|
|
||||||
{
|
|
||||||
auto& aut_tuple_first = automata_tuples[left_index % num_automata];
|
|
||||||
auto& left = aut_tuple_first.first;
|
|
||||||
auto aut_num_sets_first = aut_tuple_first.second;
|
|
||||||
while (std::get<3>(acceptance_sets[acc_index]) < aut_num_sets_first)
|
|
||||||
acc_index = (acc_index + 1) % num_acceptance;
|
|
||||||
auto acc_tuple_first = acceptance_sets[acc_index];
|
|
||||||
acc_index = (acc_index + 1) % num_acceptance;
|
|
||||||
auto acc_first = std::get<0>(acc_tuple_first);
|
|
||||||
auto acc_num_sets_first = std::get<3>(acc_tuple_first);
|
|
||||||
left->set_acceptance(acc_num_sets_first, acc_first);
|
|
||||||
for (unsigned right_index = 0; right_index < num_right; ++right_index)
|
|
||||||
{
|
|
||||||
auto& aut_tuple_second =
|
|
||||||
automata_tuples[(num_left + right_index) % num_automata];
|
|
||||||
auto& right = aut_tuple_second.first;
|
|
||||||
auto aut_num_sets_second = aut_tuple_second.second;
|
|
||||||
while (std::get<3>(acceptance_sets[acc_index]) < aut_num_sets_second)
|
|
||||||
acc_index = (acc_index + 1) % num_acceptance;
|
|
||||||
auto acc_tuple_second = acceptance_sets[acc_index];
|
|
||||||
acc_index = (acc_index + 1) % num_acceptance;
|
|
||||||
auto acc_second = std::get<0>(acc_tuple_second);
|
|
||||||
auto acc_num_sets_second = std::get<3>(acc_tuple_second);
|
|
||||||
right->set_acceptance(acc_num_sets_second, acc_second);
|
|
||||||
auto result_prod = spot::parity_product(left, right);
|
|
||||||
auto ref_prod = spot::product(left, right);
|
|
||||||
if (!are_equiv(result_prod, ref_prod))
|
|
||||||
{
|
|
||||||
std::cerr << nb << ": parity_product: Not equivalent.\n"
|
|
||||||
<< "=====First Automaton=====\n";
|
|
||||||
spot::print_hoa(std::cerr, left);
|
|
||||||
std::cerr << "=====Second Automaton=====\n";
|
|
||||||
spot::print_hoa(std::cerr, right);
|
|
||||||
assert(false && "parity_product: Not equivalent.\n");
|
|
||||||
}
|
|
||||||
assert(is_colored_printerr(result_prod)
|
|
||||||
&& "parity_product: not colored.");
|
|
||||||
assert(is_right_parity(result_prod, spot::parity_kind_any,
|
|
||||||
spot::parity_style_any,
|
|
||||||
true, true, 2)
|
|
||||||
&& "parity_product: not a parity acceptance condition");
|
|
||||||
|
|
||||||
auto result_sum = spot::parity_product_or(left, right);
|
|
||||||
auto ref_sum = spot::product_or(left, right);
|
|
||||||
if (!are_equiv(result_sum, ref_sum))
|
|
||||||
{
|
|
||||||
std::cerr << nb << ": parity_product_or: Not equivalent.\n"
|
|
||||||
<< "=====First Automaton=====\n";
|
|
||||||
spot::print_hoa(std::cerr, left);
|
|
||||||
std::cerr << "=====Second Automaton=====\n";
|
|
||||||
spot::print_hoa(std::cerr, right);
|
|
||||||
assert(false && "parity_product_or: Not equivalent.\n");
|
|
||||||
}
|
|
||||||
assert(is_colored_printerr(result_sum)
|
|
||||||
&& "parity_product_or: not colored.");
|
|
||||||
assert(is_right_parity(result_sum, spot::parity_kind_any,
|
|
||||||
spot::parity_style_any,
|
|
||||||
true, true, 2)
|
|
||||||
&& "parity_product_or: not a parity acceptance condition");
|
|
||||||
++nb;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
return 0;
|
return 0;
|
||||||
}
|
}
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue