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

parity: add spot::parity_product_or()

Browse source 
parity_product_or constructs the sum of two parity automata and it keeps
the parity.

* spot/twaalgos/parity.cc, spot/twaalgos/parity.hh: Here.
* tests/core/parity.cc: Add tests here.
This commit is contained in:
Laurent XU 2016-07-04 19:22:47 +02:00
parent 192fb6c1e7
commit 7a11842613
3 changed files with 81 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

55
spot/twaalgos/parity.cc
View file

@ -20,6 +20,7 @@
#include <spot/twaalgos/parity.hh>
#include <spot/twa/twagraph.hh>
#include <spot/twaalgos/product.hh>
#include <spot/twaalgos/complete.hh>
#include <vector>
#include <utility>
#include <functional>
@ -336,7 +337,7 @@ namespace spot
return right_num_sets_;
}
value_t get_max_acc_set() const
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
@ -347,7 +348,7 @@ namespace spot
while (l-- > 0)
{
auto k = get_left(l);
bool can_jump = (k & l & 1) != 1;
bool can_jump = and_cond ? (k & l & 1) != 1 : ((k | l) & 1) != 0;
if (!can_jump)
--k;
auto new_l = get_right(k);
@ -454,25 +455,26 @@ namespace spot
std::pair<sh_label_t, value_t>
push_state_history(sh_label_t label, value_t left_acc_set,
value_t right_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();
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)
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);
push_state_history(current_sh, left_acc_set,
right_acc_set, and_cond);
}
return p.first->second;
}
@ -512,8 +514,21 @@ namespace spot
twa_graph_ptr
parity_product_aux(twa_graph_ptr& left, twa_graph_ptr& right)
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;
@ -523,7 +538,7 @@ namespace spot
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, false, z_size);
auto z = acc_cond::acc_code::parity(true, !and_cond, z_size);
res->set_acceptance(z_size, z);
auto v = new product_states;
@ -535,7 +550,8 @@ namespace spot
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);
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
@ -605,12 +621,19 @@ namespace spot
if (!(left->is_existential() && right->is_existential()))
throw std::runtime_error("parity_product() does not support alternating "
"automata");
auto first = change_parity(left, parity_kind_max, parity_style_even);
auto second = change_parity(right, parity_kind_max, parity_style_even);
cleanup_parity_here(first, true);
cleanup_parity_here(second, true);
colorize_parity_here(first, true);
colorize_parity_here(second, true);
return parity_product_aux(first, second);
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);
}
}

17
spot/twaalgos/parity.hh
View file

@ -147,5 +147,22 @@ namespace spot
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);
/// @}
}

31
tests/core/parity.cc
View file

@ -27,6 +27,7 @@
#include <spot/twaalgos/product.hh>
#include <spot/twaalgos/randomgraph.hh>
#include <spot/misc/random.hh>
#include <spot/twaalgos/complete.hh>
#include <spot/twa/twagraph.hh>
#include <spot/twa/fwd.hh>
#include <spot/twa/acc.hh>
@ -389,7 +390,7 @@ int main()
unsigned acc_index = 0;
unsigned nb = 0;
// Parity product
// 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];
@ -415,9 +416,9 @@ int main()
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 = spot::parity_product(left, right);
auto ref = spot::product(left, right);
if (!are_equiv(result, ref))
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";
@ -426,12 +427,30 @@ int main()
spot::print_hoa(std::cerr, right);
assert(false && "parity_product: Not equivalent.\n");
}
assert(is_colored_printerr(result)
assert(is_colored_printerr(result_prod)
&& "parity_product: not colored.");
assert(is_right_parity(result, spot::parity_kind_any,
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;
}
}