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

degen: always compose original-states with the input

Browse source 
* spot/twaalgos/degen.cc (degeneralize, partial_degeneralize): Here.
* spot/twaalgos/degen.hh: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2020-02-10 14:55:13 +01:00
parent dd8c00fff0
commit 6a988f6884
2 changed files with 26 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

39
spot/twaalgos/degen.cc
View file

@ -351,6 +351,9 @@ namespace spot
// Preserve determinism, weakness, and stutter-invariance
res->prop_copy(a, { false, true, true, true, true, true });
auto old_orig_states =
a->get_named_prop<std::vector<unsigned>>("original-states");
auto orig_states = new std::vector<unsigned>();
auto levels = new std::vector<unsigned>();
orig_states->reserve(a->num_states()); // likely more are needed.
@ -459,7 +462,10 @@ namespace spot
todo.emplace_back(ds);
assert(ns == orig_states->size());
orig_states->emplace_back(ds.first);
unsigned orig = ds.first;
if (old_orig_states)
orig = (*old_orig_states)[orig];
orig_states->emplace_back(orig);
levels->emplace_back(ds.second);
// Level cache stores one encountered level for each state
@ -935,6 +941,8 @@ namespace spot
// auto* names = new std::vector<std::string>;
// res->set_named_prop("state-names", names);
auto old_orig_states =
a->get_named_prop<std::vector<unsigned>>("original-states");
auto orig_states = new std::vector<unsigned>();
auto levels = new std::vector<unsigned>();
unsigned ns = a->num_states();
@ -988,8 +996,12 @@ namespace spot
// std::ostringstream os;
// os << ds.first << ',' << ds.second;
// names->push_back(os.str());
unsigned orig = ds.first;
if (old_orig_states)
orig = (*old_orig_states)[orig];
assert(ns == orig_states->size());
orig_states->emplace_back(ds.first);
orig_states->emplace_back(orig);
levels->emplace_back(ds.second);
return ns;
};
@ -1094,32 +1106,11 @@ namespace spot
twa_graph_ptr
partial_degeneralize(twa_graph_ptr a)
{
bool composeorig = false;
while (acc_cond::mark_t m = is_partially_degeneralizable(a))
{
twa_graph_ptr b = partial_degeneralize(a, m);
// After the first partial degeneralization, we need to compose
// the original-states, so that original-states still appear
// to reference the original automaton.
if (composeorig)
{
auto origa =
a->get_named_prop<std::vector<unsigned>>("original-states");
auto origb =
b->get_named_prop<std::vector<unsigned>>("original-states");
for (auto& s: *origb)
s = (*origa)[s];
}
else
{
composeorig = true;
}
a = b;
}
a = partial_degeneralize(a, m);
return a;
}
std::vector<acc_cond::mark_t>
propagate_marks_vector(const const_twa_graph_ptr& aut,
scc_info* si)

13
spot/twaalgos/degen.hh
View file

@ -57,9 +57,16 @@ namespace spot
/// and the original state of the input automaton is stored in the
/// "original-states" named property of the produced automaton. Call
/// `aut->get_named_prop<std::vector<unsigned>>("original-states")`
/// to retrieve it. Note that these functions may return the original
/// to retrieve it. However be aware that if the input automaton
/// already defines the "original-states" named property, it will
/// be composed with the new one, so the "original-states" of the
/// degeneralized automaton will refer to the same automaton as the
/// "original-states" of the input automaton.
///
/// Note that these functions may return the original
/// automaton as-is if it is already degeneralized; in this case
/// the "original-states" property is not defined.
/// the "original-states" property is not defined (or not changed).
///
/// Similarly, the property "degen-levels" keeps track of the degeneralization
/// levels. To retrieve it, call
/// `aut->get_named_prop<std::vector<unsigned>>("degen-levels")`.
@ -113,6 +120,8 @@ namespace spot
/// the input automaton unmodified if no partial degeneralization is
/// possible.
///
/// The "original-state" and "degen-levels" named properties are
/// updated as for degeneralize() and degeneralize_tba().
/// @{
SPOT_API twa_graph_ptr
partial_degeneralize(const const_twa_graph_ptr& a,