Commit ebf4d258 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Make it easier to convert acc-conditions to associated formulae.

This is motivated by the fact that sog-its used the low-level data
structures used by the bdd_dict to do such work, and broke because of
the recent changes in this area.

* src/tgba/bdddict.cc, src/tgba/bdddict.hh (oneacc_to_formula):
New method.
* src/tgbaalgos/save.cc: Use it.
parent 8893f34d
......@@ -159,7 +159,6 @@ namespace spot
register_acceptance_variables(bdd_low(f), for_me);
}
int
bdd_dict::register_clone_acc(int v, const void* for_me)
{
......@@ -178,6 +177,26 @@ namespace spot
return res;
}
const ltl::formula*
bdd_dict::oneacc_to_formula(int var) const
{
assert(unsigned(var) < bdd_map.size());
const bdd_info& i = bdd_map[var];
assert(i.type == acc);
return i.f;
}
const ltl::formula*
bdd_dict::oneacc_to_formula(bdd oneacc) const
{
assert(oneacc != bddfalse);
while (bdd_high(oneacc) == bddfalse)
{
oneacc = bdd_low(oneacc);
assert(oneacc != bddfalse);
}
return oneacc_to_formula(bdd_var(oneacc));
}
int
bdd_dict::register_anonymous_variables(int n, const void* for_me)
......
......@@ -148,6 +148,27 @@ namespace spot
/// automaton).
void register_acceptance_variables(bdd f, const void* for_me);
/// \brief Convert one acceptance condition into the associated
/// formula.
///
/// This version accepts a conjunction of Acc variables, in which
/// only one must be positive. This positive variable will be
/// converted back into the associated formula.
///
/// The returned formula is not cloned, and is valid until the BDD
/// variable used in \a oneacc are unregistered.
const ltl::formula* oneacc_to_formula(bdd oneacc) const;
/// \brief Convert one acceptance condition into the associated
/// formula.
///
/// This version takes the number of a BDD variable that must has
/// been returned by a call to register_acceptance_variable().
///
/// The returned formula is not cloned, and is valid until the BDD
/// variable \a var is unregistered.
const ltl::formula* oneacc_to_formula(int var) const;
/// \brief Register anonymous BDD variables.
///
/// Return (and maybe allocate) \a n consecutive BDD variables which
......
......@@ -77,29 +77,16 @@ namespace spot
{
bdd cube = bdd_satone(acc);
acc -= cube;
while (cube != bddtrue)
const ltl::formula* f = d->oneacc_to_formula(cube);
std::string s = ltl::to_string(f);
if (is_atomic_prop(f) && s[0] == '"')
{
assert(cube != bddfalse);
// Display the first variable that is positive.
// There should be only one per satisfaction.
if (bdd_high(cube) != bddfalse)
{
int v = bdd_var(cube);
const bdd_dict::bdd_info& i = d->bdd_map[v];
assert(i.type == bdd_dict::acc);
std::string s = ltl::to_string(i.f);
if (is_atomic_prop(i.f) && s[0] == '"')
{
// Unquote atomic propositions.
s.erase(s.begin());
s.resize(s.size() - 1);
}
os_ << " \"";
escape_str(os_, s) << "\"";
break;
}
cube = bdd_low(cube);
// Unquote atomic propositions.
s.erase(s.begin());
s.resize(s.size() - 1);
}
os_ << " \"";
escape_str(os_, s) << "\"";
}
return os_;
}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment