hoa: better support for aliases on output
Part of issue #497. * doc/org/concepts.org: Declare a new "aliases" named property. * spot/parseaut/parseaut.yy: Fill the aliases named property. * spot/twa/twa.cc (copy_named_properties_of): Copy it. * spot/twaalgos/hoa.cc: Use "aliases" while encoding BDDs for output. * spot/twaalgos/hoa.hh: Add helper function to set/get aliases. * python/spot/impl.i: Create a type for aliases. * tests/core/parseaut.test: Adjust test case. * tests/python/aliases.py: New file. * tests/Makefile.am: Add it. * NEWS: Mention this change.
This commit is contained in:
Alexandre Duret-Lutz
parent
6b46dbd907
commit
dac3d78244
10 changed files with 464 additions and 75 deletions
|
|
@ -54,6 +54,10 @@ namespace spot
|
|||
bool use_implicit_labels;
|
||||
bool use_state_labels = true;
|
||||
bdd all_ap;
|
||||
typedef std::vector<std::pair<std::string, bdd>> aliases_t;
|
||||
aliases_t* aliases;
|
||||
std::unordered_map<int, unsigned> aliases_map;
|
||||
std::vector<std::pair<bdd, unsigned>> alias_cubes;
|
||||
|
||||
// Label support: the set of all conditions occurring in the
|
||||
// automaton.
|
||||
|
|
@ -66,9 +70,41 @@ namespace spot
|
|||
check_det_and_comp(aut);
|
||||
use_implicit_labels = implicit && is_universal && is_complete;
|
||||
use_state_labels &= state_labels;
|
||||
setup_aliases(aut);
|
||||
number_all_ap(aut);
|
||||
}
|
||||
|
||||
void setup_aliases(const const_twa_graph_ptr& aut)
|
||||
{
|
||||
aliases = aut->get_named_prop<aliases_t>("aliases");
|
||||
bdd sup = aut->ap_vars();
|
||||
if (aliases)
|
||||
{
|
||||
// Remove all aliases that use variables that are not
|
||||
// registered in this automaton.
|
||||
auto badvar = [sup](std::pair<std::string, bdd>& p) {
|
||||
return bdd_exist(bdd_support(p.second), sup) != bddtrue;
|
||||
};
|
||||
aliases->erase(std::remove_if(aliases->begin(),
|
||||
aliases->end(),
|
||||
badvar),
|
||||
aliases->end());
|
||||
unsigned count = aliases->size();
|
||||
for (unsigned i = 0; i < count; ++i)
|
||||
{
|
||||
bdd a = (*aliases)[i].second;
|
||||
aliases_map[a.id()] = i;
|
||||
if (bdd_is_cube(a))
|
||||
alias_cubes.emplace_back(a, i);
|
||||
bdd neg = !a;
|
||||
aliases_map[neg.id()] = i;
|
||||
if (bdd_is_cube(neg))
|
||||
alias_cubes.emplace_back(neg, i);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
std::ostream&
|
||||
emit_acc(std::ostream& os, acc_cond::mark_t b)
|
||||
{
|
||||
|
|
@ -177,6 +213,168 @@ namespace spot
|
|||
" prop_state_acc()==true");
|
||||
}
|
||||
|
||||
std::string encode_label(bdd label, unsigned aliases_start = 0)
|
||||
{
|
||||
if (aliases)
|
||||
// Check if we have a perfect alias match for this label.
|
||||
if (auto p = aliases_map.find(label.id()); p != aliases_map.end())
|
||||
if (unsigned pos = p->second; pos >= aliases_start)
|
||||
{
|
||||
auto& a = (*aliases)[pos];
|
||||
if (a.second == label)
|
||||
return '@' + a.first;
|
||||
else
|
||||
return "!@" + a.first;
|
||||
}
|
||||
if (label == bddtrue)
|
||||
return "t";
|
||||
if (label == bddfalse)
|
||||
return "f";
|
||||
std::ostringstream s;
|
||||
bool notfirstor = false;
|
||||
if (aliases)
|
||||
{
|
||||
bdd orig_label = label;
|
||||
// If we have some aliases that imply the label, we can use them
|
||||
// and try to cover most of it as a sum of labels.
|
||||
unsigned alias_count = aliases->size();
|
||||
for (unsigned i = aliases_start; i < alias_count; ++i)
|
||||
if (auto& a = (*aliases)[i]; bdd_implies(a.second, orig_label))
|
||||
{
|
||||
bdd rest = label - a.second;
|
||||
if (rest != label)
|
||||
{
|
||||
if (notfirstor)
|
||||
s << " | ";
|
||||
s << '@' << a.first;
|
||||
notfirstor = true;
|
||||
label = rest;
|
||||
if (label == bddfalse)
|
||||
return s.str();
|
||||
}
|
||||
}
|
||||
// If the label was not completely translated as a
|
||||
// disjunction of aliases, maybe we can see it as a
|
||||
// conjunction? Let's try.
|
||||
// We first try to remove cubes, from the labels, and then
|
||||
// try to cover the rest with non-cubes.
|
||||
{
|
||||
std::ostringstream s2;
|
||||
bdd labelconj = orig_label; // start again
|
||||
bool notfirstand = false;
|
||||
unsigned alias_count = aliases->size();
|
||||
// first pass using only cubes
|
||||
for (auto [acube, i]: alias_cubes)
|
||||
if (i >= aliases_start)
|
||||
if (bdd_implies(orig_label, acube))
|
||||
if (bdd rest = bdd_exist(labelconj, bdd_support(acube));
|
||||
rest != labelconj)
|
||||
{
|
||||
auto& a = (*aliases)[i];
|
||||
if (notfirstand)
|
||||
s2 << '&';
|
||||
if (acube != a.second)
|
||||
s2 << '!';
|
||||
s2 << '@' << a.first;
|
||||
notfirstand = true;
|
||||
labelconj = rest;
|
||||
if (labelconj == bddtrue)
|
||||
return s2.str();
|
||||
}
|
||||
// second pass using all non-cube aliases
|
||||
for (unsigned i = aliases_start; i < alias_count; ++i)
|
||||
{
|
||||
auto& a = (*aliases)[i];
|
||||
bdd neg = !a.second;
|
||||
if (!bdd_is_cube(a.second)
|
||||
&& bdd_implies(orig_label, a.second))
|
||||
{
|
||||
bdd rest = labelconj | neg;
|
||||
if (rest != labelconj)
|
||||
{
|
||||
if (notfirstand)
|
||||
s2 << '&';
|
||||
s2 << '@' << a.first;
|
||||
notfirstand = true;
|
||||
labelconj = rest;
|
||||
if (labelconj == bddtrue)
|
||||
return s2.str();
|
||||
}
|
||||
}
|
||||
else if (!bdd_is_cube(neg)
|
||||
&& bdd_implies(orig_label, neg))
|
||||
{
|
||||
bdd rest = labelconj | a.second;
|
||||
if (rest != labelconj)
|
||||
{
|
||||
if (notfirstand)
|
||||
s2 << '&';
|
||||
s2 << "!@" << a.first;
|
||||
notfirstand = true;
|
||||
labelconj = rest;
|
||||
if (labelconj == bddtrue)
|
||||
return s2.str();
|
||||
}
|
||||
}
|
||||
}
|
||||
// If we did not manage to make it look like a
|
||||
// conjunction of aliases, let's continue with
|
||||
// our (possibly partial) disjunction.
|
||||
}
|
||||
}
|
||||
minato_isop isop(label);
|
||||
bdd cube;
|
||||
while ((cube = isop.next()) != bddfalse)
|
||||
{
|
||||
if (notfirstor)
|
||||
s << " | ";
|
||||
bool notfirstand = false;
|
||||
if (aliases)
|
||||
{
|
||||
// We know that cube did not match any aliases. But
|
||||
// maybe it can be built as a conjunction of aliases?
|
||||
// (or negated aliases)
|
||||
bdd orig_cube = cube;
|
||||
for (auto [acube, i]: alias_cubes)
|
||||
if (i >= aliases_start)
|
||||
if (bdd_implies(orig_cube, acube))
|
||||
if (bdd rest = bdd_exist(cube, bdd_support(acube));
|
||||
rest != cube)
|
||||
{
|
||||
if (notfirstand)
|
||||
s << '&';
|
||||
if (acube != (*aliases)[i].second)
|
||||
s << '!';
|
||||
s << '@' << (*aliases)[i].first;
|
||||
notfirstand = true;
|
||||
cube = rest;
|
||||
if (cube == bddtrue)
|
||||
return s.str();
|
||||
}
|
||||
}
|
||||
while (cube != bddtrue)
|
||||
{
|
||||
if (notfirstand)
|
||||
s << '&';
|
||||
else
|
||||
notfirstand = true;
|
||||
bdd h = bdd_high(cube);
|
||||
if (h == bddfalse)
|
||||
{
|
||||
s << '!' << ap[bdd_var(cube)];
|
||||
cube = bdd_low(cube);
|
||||
}
|
||||
else
|
||||
{
|
||||
s << ap[bdd_var(cube)];
|
||||
cube = h;
|
||||
}
|
||||
}
|
||||
notfirstor = true;
|
||||
}
|
||||
return s.str();
|
||||
}
|
||||
|
||||
void number_all_ap(const const_twa_graph_ptr& aut)
|
||||
{
|
||||
// Make sure that the automaton uses only atomic propositions
|
||||
|
|
@ -206,50 +404,7 @@ namespace spot
|
|||
return;
|
||||
|
||||
for (auto& i: sup)
|
||||
{
|
||||
bdd cond = i.first;
|
||||
if (cond == bddtrue)
|
||||
{
|
||||
i.second = "t";
|
||||
continue;
|
||||
}
|
||||
if (cond == bddfalse)
|
||||
{
|
||||
i.second = "f";
|
||||
continue;
|
||||
}
|
||||
std::ostringstream s;
|
||||
bool notfirstor = false;
|
||||
|
||||
minato_isop isop(cond);
|
||||
bdd cube;
|
||||
while ((cube = isop.next()) != bddfalse)
|
||||
{
|
||||
if (notfirstor)
|
||||
s << " | ";
|
||||
bool notfirstand = false;
|
||||
while (cube != bddtrue)
|
||||
{
|
||||
if (notfirstand)
|
||||
s << '&';
|
||||
else
|
||||
notfirstand = true;
|
||||
bdd h = bdd_high(cube);
|
||||
if (h == bddfalse)
|
||||
{
|
||||
s << '!' << ap[bdd_var(cube)];
|
||||
cube = bdd_low(cube);
|
||||
}
|
||||
else
|
||||
{
|
||||
s << ap[bdd_var(cube)];
|
||||
cube = h;
|
||||
}
|
||||
}
|
||||
notfirstor = true;
|
||||
}
|
||||
i.second = s.str();
|
||||
}
|
||||
i.second = encode_label(i.first);
|
||||
}
|
||||
};
|
||||
|
||||
|
|
@ -643,6 +798,14 @@ namespace spot
|
|||
}
|
||||
os << nl;
|
||||
}
|
||||
if (md.aliases)
|
||||
{
|
||||
auto* aliases = md.aliases;
|
||||
int cnt = aliases->size();
|
||||
for (int i = cnt - 1; i >= 0; --i)
|
||||
os << "Alias: @" << (*aliases)[i].first << ' '
|
||||
<< md.encode_label((*aliases)[i].second, i + 1) << nl;
|
||||
}
|
||||
|
||||
// If we want to output implicit labels, we have to
|
||||
// fill a vector with all destinations in order.
|
||||
|
|
@ -799,4 +962,26 @@ namespace spot
|
|||
return os;
|
||||
}
|
||||
|
||||
std::vector<std::pair<std::string, bdd>>*
|
||||
get_aliases(const const_twa_ptr& g)
|
||||
{
|
||||
return
|
||||
g->get_named_prop<std::vector<std::pair<std::string, bdd>>>("aliases");
|
||||
}
|
||||
|
||||
void
|
||||
set_aliases(twa_ptr& g, std::vector<std::pair<std::string, bdd>> aliases)
|
||||
{
|
||||
if (aliases.empty())
|
||||
{
|
||||
g->set_named_prop("aliases", nullptr);
|
||||
}
|
||||
else
|
||||
{
|
||||
auto a = g->get_or_set_named_prop
|
||||
<std::vector<std::pair<std::string, bdd>>>("aliases");
|
||||
*a = aliases;
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue