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

hoa: extract the alias formating code for reuse

Browse source 
* spot/twaalgos/hoa.hh (hoa_alias_formater): New class.
* spot/twaalgos/hoa.cc: Implement hoa_alias_formater using the code
that was previously in metadata::encode_label, and use it in place.
This commit is contained in:
Alexandre Duret-Lutz 2022-02-03 14:09:01 +01:00
parent f759697e1c
commit 4506643632
2 changed files with 321 additions and 196 deletions
Download patch file Download diff file Expand all files Collapse all files

415
spot/twaalgos/hoa.cc
View file

@ -36,6 +36,220 @@ using namespace std::string_literals;
namespace spot
{
hoa_alias_formater::hoa_alias_formater(const const_twa_graph_ptr& aut,
const char* false_str,
const char* true_str,
const char* or_str,
const char* and_str,
const char* not_str,
const char* lpar_str,
const char* rpar_str,
std::function<std::string(int)>
ap_printer)
: false_str_(false_str), true_str_(true_str), or_str_(or_str),
and_str_(and_str), not_str_(not_str), lpar_str_(lpar_str),
rpar_str_(rpar_str), ap_printer_(ap_printer)
{
auto aliases = aliases_ = aut->get_named_prop<aliases_t>("aliases");
if (!aliases)
return;
bdd sup = aut->ap_vars();
// 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::string
hoa_alias_formater::encode_label(bdd label, unsigned aliases_start)
{
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 std::string(not_str_) + '@' + a.first;
}
if (label == bddtrue)
return true_str_;
if (label == bddfalse)
return false_str_;
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 << or_str_;
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 << and_str_;
if (acube != a.second)
s2 << not_str_;
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 << and_str_;
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 << and_str_;
s2 << not_str_ << '@' << 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 = isop.next();
std::ostringstream s3;
while (cube != bddfalse)
{
if (notfirstor)
s << or_str_;
bool notfirstand = false;
s3.str("");
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)
s3 << and_str_;
if (acube != (*aliases_)[i].second)
s3 << not_str_;
s3 << '@' << (*aliases_)[i].first;
cube = rest;
if (cube == bddtrue)
break;
notfirstand = true;
}
}
while (cube != bddtrue)
{
if (notfirstand)
s3 << and_str_;
bdd h = bdd_high(cube);
if (h == bddfalse)
{
s3 << not_str_ << ap_printer_(bdd_var(cube));
cube = bdd_low(cube);
}
else
{
s3 << ap_printer_(bdd_var(cube));
cube = h;
}
if (cube == bddtrue)
break;
notfirstand = true;
}
bdd nextcube = isop.next();
if (notfirstand && (notfirstor || nextcube != bddfalse))
s << lpar_str_ << s3.str() << rpar_str_;
else
s << s3.str();
cube = nextcube;
notfirstor = true;
}
return s.str();
}
namespace
{
struct metadata final
@ -54,10 +268,7 @@ 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;
hoa_alias_formater haf;
// Label support: the set of all conditions occurring in the
// automaton.
@ -66,45 +277,15 @@ namespace spot
metadata(const const_twa_graph_ptr& aut, bool implicit,
bool state_labels)
: haf(aut, "f", "t", " | ", "&", "!", "", "",
[&ap=this->ap](int num){ return std::to_string(ap[num]); })
{
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)
{
@ -215,164 +396,7 @@ namespace spot
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();
return haf.encode_label(label, aliases_start);
}
void number_all_ap(const const_twa_graph_ptr& aut)
@ -798,9 +822,8 @@ namespace spot
}
os << nl;
}
if (md.aliases)
if (auto* aliases = md.haf.aliases())
{
auto* aliases = md.aliases;
int cnt = aliases->size();
for (int i = cnt - 1; i >= 0; --i)
os << "Alias: @" << (*aliases)[i].first << ' '

102
spot/twaalgos/hoa.hh
View file

@ -24,6 +24,7 @@
#include <spot/twa/fwd.hh>
#include <vector>
#include <utility>
#include <functional>
#include <bddx.h>
namespace spot
@ -62,4 +63,105 @@ namespace spot
/// Pass an empty vector to remove existing aliases.
SPOT_API void
set_aliases(twa_ptr g, std::vector<std::pair<std::string, bdd>> aliases);
/// \ingroup twa_io
/// \brief Help printing BDDs as text, using aliases.
class SPOT_API hoa_alias_formater final
{
public:
typedef std::vector<std::pair<std::string, bdd>> aliases_t;
private:
aliases_t* aliases_;
std::unordered_map<int, unsigned> aliases_map_;
std::vector<std::pair<bdd, unsigned>> alias_cubes_;
const char* false_str_;
const char* true_str_;
const char* or_str_;
const char* and_str_;
const char* not_str_;
const char* lpar_str_;
const char* rpar_str_;
std::function<std::string(int)> ap_printer_;
public:
/// \brief Initialize this class from the aliases defined
/// for an automaton.
///
/// The aliases are taken from the named-property "aliases",
/// defined in the automaton. If no such named-property exist,
/// the aliases() method will return a null pointer.
///
/// Note that any alias that uses an atomic proposition not
/// registered in the automaton is not only ignored, but also
/// removed from the alias list stored in the automaton.
///
/// The \a or_str, \a and_str, and \ap_printer arguments are
/// used to print operators OR, AND, and to print atomic propositions
/// that are not aliases. \a lpar_str and \a rpar_str are used
/// to group conjuncts that appear in a disjunction.
hoa_alias_formater(const const_twa_graph_ptr& aut,
const char* false_str,
const char* true_str,
const char* or_str,
const char* and_str,
const char* not_str,
const char* lpar_str,
const char* rpar_str,
std::function<std::string(int)> ap_printer);
/// \brief Attempt to format a BDD label using aliases.
///
/// The returned pair should be interpreted as a disjunction
/// between an expression involving aliases, and a BDD that could
/// not be expressed using aliases.
///
/// The conversion works in several attempts, in the following order:
///
/// - If an alias A exists for \a label, `"@A"` is returned.
///
/// - If an alias A exists for the negation of \a label, `"!@A`
/// is returned.
///
/// - If \a label is true or false, `true_str` or `false_str`
/// are returned as specified at construction.
///
/// - If \a label can be built as a disjunction of positive
/// aliases, such a disjunction is returned as `"@A | @B | @C"`.
///
/// - If \a label can be built from a conjunction of
/// aliases or negated aliases, it is returned as
/// `"@A&!@B&@C"`. Note that this check first
/// attempt to use aliases that represent cubes before trying
/// other aliases.
///
/// - Otherwise \a label is split in irredundant-sum-of-products
/// and each clause is encoded as a conjunctions of (possibly
/// negated) aliases using only those that are cubes. Any
/// remaining literal is encoded with the ap_printer() function
/// passed to the constructor.
///
/// The aliases to be used are those returned by the aliases()
/// method. The vector returned by aliases() is scanned from
/// position \a aliases_start. As this vector is stored in the
/// opposite order of how aliases should be stored in the HOA
/// output, adjusting \a aliases_start is helpful to encode an
/// aliases using only previously defined aliases (i.e., aliases
/// that appear later in the sequence returned by aliases()).
std::string
encode_label(bdd label, unsigned aliases_start = 0);
/// \brief Retrieve the list of aliases.
///
/// This points to the same list that the automaton's "aliasaes"
/// named properties points to. Will return `nullptr` if no
/// aliases are defined.
///
/// \note Aliases involving atomic propositions that are not
/// declared in the automaton have been removed by this class'
/// constructor.
aliases_t* aliases()
{
return aliases_;
}
};
}