0aca26e3f9
* spot/twaalgos/parity.cc: Do not throw a pointer to an exception, throw the exception directly. Factor all the throwing code in a function. * tests/python/parity.py: Add test case.
644 lines
20 KiB
C++
644 lines
20 KiB
C++
// -*- coding: utf-8 -*-
|
|
// Copyright (C) 2016, 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/parity.hh>
|
|
#include <spot/twa/twagraph.hh>
|
|
#include <spot/twaalgos/product.hh>
|
|
#include <spot/twaalgos/complete.hh>
|
|
#include <vector>
|
|
#include <utility>
|
|
#include <functional>
|
|
#include <queue>
|
|
|
|
namespace spot
|
|
{
|
|
namespace
|
|
{
|
|
unsigned change_set(unsigned x, unsigned num_sets,
|
|
bool change_kind, bool change_style)
|
|
{
|
|
// If the parity acceptance kind is changed,
|
|
// then the index of the sets are reversed
|
|
if (change_kind)
|
|
x = num_sets - x - 1;
|
|
// If the parity style is changed, then all the existing acceptance
|
|
// sets are shifted
|
|
x += change_style;
|
|
return x;
|
|
}
|
|
|
|
void
|
|
change_acc(twa_graph_ptr& aut, unsigned num_sets, bool change_kind,
|
|
bool change_style, bool output_max, bool input_max)
|
|
{
|
|
for (auto& e: aut->edge_vector())
|
|
if (e.acc)
|
|
{
|
|
unsigned msb = (input_max ? e.acc.max_set() : e.acc.min_set()) - 1;
|
|
e.acc = acc_cond::mark_t{change_set(msb, num_sets, change_kind,
|
|
change_style)};
|
|
}
|
|
else if (output_max && change_style)
|
|
{
|
|
// If the parity is changed, a new set is introduced.
|
|
// This new set is used to mark all the transitions of the input
|
|
// that don't belong to any acceptance sets.
|
|
e.acc.set(0);
|
|
}
|
|
}
|
|
|
|
[[noreturn]] static void
|
|
input_is_not_parity(const char* fun)
|
|
{
|
|
throw std::runtime_error(std::string(fun) +
|
|
"(): input should have "
|
|
"parity acceptance");
|
|
}
|
|
}
|
|
|
|
twa_graph_ptr
|
|
change_parity(const const_twa_graph_ptr& aut,
|
|
parity_kind kind, parity_style style)
|
|
{
|
|
return change_parity_here(make_twa_graph(aut, twa::prop_set::all()),
|
|
kind, style);
|
|
}
|
|
|
|
twa_graph_ptr
|
|
change_parity_here(twa_graph_ptr aut, parity_kind kind, parity_style style)
|
|
{
|
|
bool current_max;
|
|
bool current_odd;
|
|
if (!aut->acc().is_parity(current_max, current_odd, true))
|
|
input_is_not_parity("change_parity");
|
|
auto old_num_sets = aut->num_sets();
|
|
|
|
bool output_max = true;
|
|
switch (kind)
|
|
{
|
|
case parity_kind_max:
|
|
output_max = true;
|
|
break;
|
|
case parity_kind_min:
|
|
output_max = false;
|
|
break;
|
|
case parity_kind_same:
|
|
output_max = current_max;
|
|
break;
|
|
case parity_kind_any:
|
|
// If we need to change the style we may change the kind not to
|
|
// introduce new accset.
|
|
output_max = (((style == parity_style_odd && !current_odd)
|
|
|| (style == parity_style_even && current_odd))
|
|
&& old_num_sets % 2 == 0) != current_max;
|
|
break;
|
|
}
|
|
|
|
bool change_kind = current_max != output_max;
|
|
bool toggle_style = change_kind && (old_num_sets % 2 == 0);
|
|
|
|
bool output_odd = true;
|
|
switch (style)
|
|
{
|
|
case parity_style_odd:
|
|
output_odd = true;
|
|
break;
|
|
case parity_style_even:
|
|
output_odd = false;
|
|
break;
|
|
case parity_style_same:
|
|
output_odd = current_odd;
|
|
break;
|
|
case parity_style_any:
|
|
output_odd = current_odd != toggle_style;
|
|
// If we need to change the kind we may change the style not to
|
|
// introduce new accset.
|
|
break;
|
|
}
|
|
|
|
current_odd = current_odd != toggle_style;
|
|
bool change_style = false;
|
|
auto num_sets = old_num_sets;
|
|
// If the parity neeeds to be changed, then a new acceptance set is created.
|
|
// The old acceptance sets are shifted
|
|
if (output_odd != current_odd)
|
|
{
|
|
change_style = true;
|
|
++num_sets;
|
|
}
|
|
|
|
if (change_kind || change_style)
|
|
{
|
|
auto new_acc = acc_cond::acc_code::parity(output_max,
|
|
output_odd, num_sets);
|
|
aut->set_acceptance(num_sets, new_acc);
|
|
}
|
|
change_acc(aut, old_num_sets, change_kind,
|
|
change_style, output_max, current_max);
|
|
return aut;
|
|
}
|
|
|
|
twa_graph_ptr
|
|
cleanup_parity(const const_twa_graph_ptr& aut, bool keep_style)
|
|
{
|
|
auto result = make_twa_graph(aut, twa::prop_set::all());
|
|
return cleanup_parity_here(result, keep_style);
|
|
}
|
|
|
|
twa_graph_ptr
|
|
cleanup_parity_here(twa_graph_ptr aut, bool keep_style)
|
|
{
|
|
bool current_max;
|
|
bool current_odd;
|
|
if (!aut->acc().is_parity(current_max, current_odd, true))
|
|
input_is_not_parity("cleanup_parity");
|
|
auto num_sets = aut->num_sets();
|
|
if (num_sets == 0)
|
|
return aut;
|
|
|
|
// Compute all the used sets
|
|
auto used_in_aut = acc_cond::mark_t();
|
|
for (auto& t: aut->edges())
|
|
{
|
|
if (current_max)
|
|
{
|
|
auto maxset = t.acc.max_set();
|
|
if (maxset)
|
|
t.acc = acc_cond::mark_t{maxset - 1};
|
|
}
|
|
else
|
|
{
|
|
t.acc = t.acc.lowest();
|
|
}
|
|
used_in_aut |= t.acc;
|
|
}
|
|
if (used_in_aut)
|
|
{
|
|
// Never remove the least significant acceptance set, and mark the
|
|
// acceptance set 0 to keep the style if needed.
|
|
if (current_max || keep_style)
|
|
used_in_aut.set(0);
|
|
if (!current_max)
|
|
used_in_aut.set(num_sets - 1);
|
|
|
|
// Fill the vector shift with the new acceptance sets
|
|
std::vector<unsigned> shift(num_sets);
|
|
int prev_used = -1;
|
|
bool change_style = false;
|
|
unsigned new_index = 0;
|
|
for (auto i = 0U; i < num_sets; ++i)
|
|
if (used_in_aut.has(i))
|
|
{
|
|
if (prev_used == -1)
|
|
change_style = i % 2 != 0;
|
|
else if ((i + prev_used) % 2 != 0)
|
|
++new_index;
|
|
shift[i] = new_index;
|
|
prev_used = i;
|
|
}
|
|
|
|
// Update all the transitions with the vector shift
|
|
for (auto& t: aut->edges())
|
|
{
|
|
auto maxset = t.acc.max_set();
|
|
if (maxset)
|
|
t.acc = acc_cond::mark_t{shift[maxset - 1]};
|
|
}
|
|
auto new_num_sets = new_index + 1;
|
|
if (new_num_sets < num_sets)
|
|
{
|
|
auto new_acc = acc_cond::acc_code::parity(current_max,
|
|
current_odd != change_style,
|
|
new_num_sets);
|
|
aut->set_acceptance(new_num_sets, new_acc);
|
|
}
|
|
}
|
|
else
|
|
{
|
|
if ((current_max && current_odd)
|
|
|| (!current_max && current_odd != (num_sets % 2 == 0)))
|
|
aut->set_acceptance(0, acc_cond::acc_code::t());
|
|
else
|
|
aut->set_acceptance(0, acc_cond::acc_code::f());
|
|
}
|
|
return aut;
|
|
}
|
|
|
|
twa_graph_ptr
|
|
colorize_parity(const const_twa_graph_ptr& aut, bool keep_style)
|
|
{
|
|
return colorize_parity_here(make_twa_graph(aut, twa::prop_set::all()),
|
|
keep_style);
|
|
}
|
|
|
|
twa_graph_ptr
|
|
colorize_parity_here(twa_graph_ptr aut, bool keep_style)
|
|
{
|
|
bool current_max;
|
|
bool current_odd;
|
|
if (!aut->acc().is_parity(current_max, current_odd, true))
|
|
input_is_not_parity("colorize_parity");
|
|
|
|
bool has_empty = false;
|
|
for (const auto& e: aut->edges())
|
|
if (!e.acc)
|
|
{
|
|
has_empty = true;
|
|
break;
|
|
}
|
|
auto num_sets = aut->num_sets();
|
|
int incr = 0;
|
|
if (has_empty)
|
|
{
|
|
// If the automaton has a transition that belong to any set, we need to
|
|
// introduce a new acceptance set.
|
|
// We may want to add a second acceptance set to keep the style of
|
|
// the parity acceptance
|
|
incr = 1 + (keep_style && current_max);
|
|
num_sets += incr;
|
|
bool new_style = current_odd == (keep_style || !current_max);
|
|
auto new_acc = acc_cond::acc_code::parity(current_max,
|
|
new_style, num_sets);
|
|
aut->set_acceptance(num_sets, new_acc);
|
|
}
|
|
if (current_max)
|
|
{
|
|
--incr;
|
|
for (auto& e: aut->edges())
|
|
{
|
|
auto maxset = e.acc.max_set();
|
|
e.acc = acc_cond::mark_t{maxset ? maxset + incr : incr};
|
|
}
|
|
}
|
|
else
|
|
{
|
|
auto unused_mark = num_sets - incr;
|
|
for (auto& e: aut->edges())
|
|
e.acc = e.acc ? e.acc.lowest() : acc_cond::mark_t{unused_mark};
|
|
}
|
|
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
|
|
{
|
|
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
|
|
{
|
|
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
|
|
{
|
|
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);
|
|
}
|
|
}
|