reduce_parity: expose the internal vectors of colors
* spot/twaalgos/parity.cc, spot/twaalgos/parity.hh: Add a reduce_parity_data class for access to the vectors of colors computed by reduce_parity. * python/spot/impl.i: Add bindings for std::vector<int>.
This commit is contained in:
Alexandre Duret-Lutz
parent
b0c299b9e9
commit
67722db78f
3 changed files with 64 additions and 35 deletions
|
|
@ -520,6 +520,7 @@ namespace std {
|
|||
%template(vectorbdd) vector<bdd>;
|
||||
%template(aliasvector) vector<pair<string, bdd>>;
|
||||
%template(vectorstring) vector<string>;
|
||||
%template(vectorint) vector<int>;
|
||||
%template(pair_formula_vectorstring) pair<spot::formula, vector<string>>;
|
||||
%template(atomic_prop_set) set<spot::formula>;
|
||||
%template(relabeling_map) map<spot::formula, spot::formula>;
|
||||
|
|
|
|||
|
|
@ -387,27 +387,15 @@ namespace spot
|
|||
return aut;
|
||||
}
|
||||
|
||||
twa_graph_ptr
|
||||
reduce_parity(const const_twa_graph_ptr& aut, bool colored, bool layered)
|
||||
reduce_parity_data::reduce_parity_data(const const_twa_graph_ptr& aut,
|
||||
bool layered)
|
||||
{
|
||||
return reduce_parity_here(make_twa_graph(aut, twa::prop_set::all()),
|
||||
colored, layered);
|
||||
}
|
||||
|
||||
twa_graph_ptr
|
||||
reduce_parity_here(twa_graph_ptr aut, bool colored, bool layered)
|
||||
{
|
||||
unsigned num_sets = aut->num_sets();
|
||||
if (!colored && num_sets == 0)
|
||||
return aut;
|
||||
|
||||
bool current_max;
|
||||
bool current_odd;
|
||||
if (!aut->acc().is_parity(current_max, current_odd, true))
|
||||
input_is_not_parity("reduce_parity");
|
||||
if (!aut->acc().is_parity(parity_max, parity_odd, true))
|
||||
input_is_not_parity("reduce_parity_data");
|
||||
if (!aut->is_existential())
|
||||
throw std::runtime_error
|
||||
("reduce_parity_here() does not support alternation");
|
||||
("reduce_parity_data() does not support alternation");
|
||||
unsigned num_sets = aut->num_sets();
|
||||
|
||||
// The algorithm assumes "max odd" or "max even" parity. "min"
|
||||
// parity is handled by converting it to "max" while the algorithm
|
||||
|
|
@ -466,8 +454,8 @@ namespace spot
|
|||
//
|
||||
// -2 means the edge was never assigned a color.
|
||||
unsigned evs = aut->edge_vector().size();
|
||||
std::vector<int> piprime1(evs, -2); // k=1
|
||||
std::vector<int> piprime2(evs, -2); // k=0
|
||||
piprime1.resize(evs, -2); // k=1
|
||||
piprime2.resize(evs, -2); // k=0
|
||||
bool sba = aut->prop_state_acc().is_true();
|
||||
|
||||
auto rec =
|
||||
|
|
@ -481,7 +469,7 @@ namespace spot
|
|||
{
|
||||
int piri; // π(Rᵢ)
|
||||
int color; // corresponding color, to deal with "min" kind
|
||||
if (current_max)
|
||||
if (parity_max)
|
||||
{
|
||||
piri = color = si.acc_sets_of(scc).max_set() - 1;
|
||||
}
|
||||
|
|
@ -538,11 +526,28 @@ namespace spot
|
|||
};
|
||||
scc_and_mark_filter filter1(aut, {});
|
||||
rec(filter1, rec);
|
||||
}
|
||||
|
||||
twa_graph_ptr
|
||||
reduce_parity(const const_twa_graph_ptr& aut, bool colored, bool layered)
|
||||
{
|
||||
return reduce_parity_here(make_twa_graph(aut, twa::prop_set::all()),
|
||||
colored, layered);
|
||||
}
|
||||
|
||||
twa_graph_ptr
|
||||
reduce_parity_here(twa_graph_ptr aut, bool colored, bool layered)
|
||||
{
|
||||
unsigned num_sets = aut->num_sets();
|
||||
if (!colored && num_sets == 0)
|
||||
return aut;
|
||||
|
||||
reduce_parity_data pd(aut, layered);
|
||||
|
||||
// compute the used range for each vector.
|
||||
int min1 = num_sets;
|
||||
int max1 = -2;
|
||||
for (int m : piprime1)
|
||||
for (int m : pd.piprime1)
|
||||
{
|
||||
if (m <= -2)
|
||||
continue;
|
||||
|
|
@ -559,7 +564,7 @@ namespace spot
|
|||
}
|
||||
int min2 = num_sets;
|
||||
int max2 = -2;
|
||||
for (int m : piprime2)
|
||||
for (int m : pd.piprime2)
|
||||
{
|
||||
if (m <= -2)
|
||||
continue;
|
||||
|
|
@ -575,13 +580,13 @@ namespace spot
|
|||
{
|
||||
std::swap(size1, size2);
|
||||
std::swap(min1, min2);
|
||||
std::swap(piprime1, piprime2);
|
||||
std::swap(pd.piprime1, pd.piprime2);
|
||||
}
|
||||
|
||||
unsigned new_num_sets = size1;
|
||||
if (current_max)
|
||||
if (pd.parity_max)
|
||||
{
|
||||
for (int& m : piprime1)
|
||||
for (int& m : pd.piprime1)
|
||||
if (m > -2)
|
||||
m -= min1;
|
||||
else
|
||||
|
|
@ -589,7 +594,7 @@ namespace spot
|
|||
}
|
||||
else
|
||||
{
|
||||
for (int& m : piprime1)
|
||||
for (int& m : pd.piprime1)
|
||||
if (m > -2)
|
||||
m = new_num_sets - (m - min1) - 1;
|
||||
else
|
||||
|
|
@ -597,8 +602,8 @@ namespace spot
|
|||
}
|
||||
|
||||
// The parity style changes if we shift colors by an odd number.
|
||||
bool new_odd = current_odd ^ (min1 & 1);
|
||||
if (!current_max)
|
||||
bool new_odd = pd.parity_odd ^ (min1 & 1);
|
||||
if (!pd.parity_max)
|
||||
// Switching from min<->max changes the parity style every time
|
||||
// the number of colors is even. If the input was "min", we
|
||||
// switched once to "max" to apply the reduction and once again
|
||||
|
|
@ -607,7 +612,7 @@ namespace spot
|
|||
new_odd ^= !(num_sets & 1) ^ !(new_num_sets & 1);
|
||||
if (!colored)
|
||||
{
|
||||
new_odd ^= current_max;
|
||||
new_odd ^= pd.parity_max;
|
||||
new_num_sets -= 1;
|
||||
|
||||
// It seems we have nothing to win by changing automata with a
|
||||
|
|
@ -617,18 +622,18 @@ namespace spot
|
|||
}
|
||||
|
||||
aut->set_acceptance(new_num_sets,
|
||||
acc_cond::acc_code::parity(current_max, new_odd,
|
||||
acc_cond::acc_code::parity(pd.parity_max, new_odd,
|
||||
new_num_sets));
|
||||
if (colored)
|
||||
for (auto& e: aut->edges())
|
||||
{
|
||||
unsigned n = aut->edge_number(e);
|
||||
e.acc = acc_cond::mark_t({unsigned(piprime1[n])});
|
||||
e.acc = acc_cond::mark_t({unsigned(pd.piprime1[n])});
|
||||
}
|
||||
else if (current_max)
|
||||
else if (pd.parity_max)
|
||||
for (auto& e: aut->edges())
|
||||
{
|
||||
unsigned n = piprime1[aut->edge_number(e)];
|
||||
unsigned n = pd.piprime1[aut->edge_number(e)];
|
||||
if (n == 0)
|
||||
e.acc = acc_cond::mark_t({});
|
||||
else
|
||||
|
|
@ -637,7 +642,7 @@ namespace spot
|
|||
else
|
||||
for (auto& e: aut->edges())
|
||||
{
|
||||
unsigned n = piprime1[aut->edge_number(e)];
|
||||
unsigned n = pd.piprime1[aut->edge_number(e)];
|
||||
if (n >= new_num_sets)
|
||||
e.acc = acc_cond::mark_t({});
|
||||
else
|
||||
|
|
|
|||
|
|
@ -21,6 +21,7 @@
|
|||
|
||||
#include <spot/misc/common.hh>
|
||||
#include <spot/twa/fwd.hh>
|
||||
#include <vector>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -194,5 +195,27 @@ namespace spot
|
|||
SPOT_API twa_graph_ptr
|
||||
reduce_parity_here(twa_graph_ptr aut,
|
||||
bool colored = false, bool layered = false);
|
||||
|
||||
/// @}
|
||||
|
||||
/// \brief Internal data computed by the reduce_parity function
|
||||
///
|
||||
/// `piprime1` and `piprime2` have the size of `aut`'s edge vector,
|
||||
/// represent two possible colorations of the edges. piprime1 assumes
|
||||
/// that terminal cases of the recursion are odd, and piprime2 assumes
|
||||
/// they are even.
|
||||
///
|
||||
/// reduce_parity() actually compare the range of values in these
|
||||
/// two vectors to limit the number of colors.
|
||||
struct SPOT_API reduce_parity_data
|
||||
{
|
||||
bool parity_max; ///< Whether the input automaton is parity max
|
||||
bool parity_odd; ///< Whether the input automaton is parity odd
|
||||
std::vector<int> piprime1;
|
||||
std::vector<int> piprime2;
|
||||
|
||||
reduce_parity_data(const const_twa_graph_ptr& aut, bool layered = false);
|
||||
};
|
||||
|
||||
/// @}
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue