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

* src/tgba/bddprint.cc (print_accset_handler, bdd_print_accset): New

functions.
* src/tgba/bddprint.cc (bdd_print_accset): Declare it.
* src/tgbaalgos/dotty.cc (dotty_bfs::process_link): Use it.
* src/tgbatest/tgbaread.test, src/tgbatest/explicit.test: Adjust
expected output.
parent 6877f378
2003-11-26 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgba/bddprint.cc (print_accset_handler, bdd_print_accset): New
functions.
* src/tgba/bddprint.cc (bdd_print_accset): Declare it.
* src/tgbaalgos/dotty.cc (dotty_bfs::process_link): Use it.
* src/tgbatest/tgbaread.test, src/tgbatest/explicit.test: Adjust
expected output.
2003-11-25 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaparse/tgbaparse.yy: Remove a random character.
......
......@@ -117,15 +117,11 @@ namespace spot
print_acc_handler(char* varset, int size)
{
for (int v = 0; v < size; ++v)
{
if (varset[v] < 0)
continue;
if (varset[v] > 0)
{
*where << " ";
print_handler(*where, v);
}
}
if (varset[v] > 0)
{
*where << " ";
print_handler(*where, v);
}
}
std::ostream&
......@@ -138,6 +134,32 @@ namespace spot
return os;
}
static bool first_done = false;
static void
print_accset_handler(char* varset, int size)
{
for (int v = 0; v < size; ++v)
if (varset[v] > 0)
{
*where << (first_done ? ", " : "{");
print_handler(*where, v);
first_done = true;
}
}
std::ostream&
bdd_print_accset(std::ostream& os, const bdd_dict* d, bdd b)
{
dict = d;
where = &os;
want_acc = true;
first_done = false;
bdd_allsat(b, print_accset_handler);
if (first_done)
*where << "}";
return os;
}
std::string
bdd_format_sat(const bdd_dict* d, bdd b)
{
......
......@@ -57,6 +57,16 @@ namespace spot
std::ostream& bdd_print_acc(std::ostream& os,
const bdd_dict* dict, bdd b);
/// \brief Print a BDD as a set of accepting conditions.
///
/// This is used when saving a TGBA.
/// \param os The output stream.
/// \param dict The dictionary to use, to lookup variables.
/// \param b The BDD to print.
/// \return The BDD formated as a string.
std::ostream& bdd_print_accset(std::ostream& os,
const bdd_dict* dict, bdd b);
/// \brief Print a BDD as a set.
/// \param os The output stream.
/// \param dict The dictionary to use, to lookup variables.
......
......@@ -62,8 +62,9 @@ namespace spot
os_ << " " << in << " -> " << out << " [label=\"";
bdd_print_formula(os_, automata_->get_dict(),
si->current_condition()) << "\\n";
bdd_print_set(os_, automata_->get_dict(),
si->current_accepting_conditions()) << "\"]" << std::endl;
bdd_print_accset(os_, automata_->get_dict(),
si->current_accepting_conditions()) << "\"]"
<< std::endl;
}
private:
......
......@@ -32,11 +32,11 @@ digraph G {
0 [label="", style=invis, height=0]
0 -> 1
1 [label="state 0"]
1 -> 2 [label="1\n<Acc[p]:0, Acc[q]:1, Acc[r]:0><Acc[p]:1, Acc[q]:0, Acc[r]:0>"]
1 -> 2 [label="1\n{Acc[q], Acc[p]}"]
2 [label="state 1"]
2 -> 3 [label="a\n<Acc[p]:0, Acc[q]:0, Acc[r]:1>"]
2 -> 3 [label="a\n{Acc[r]}"]
3 [label="state 2"]
3 -> 1 [label="(b & c)\nF"]
3 -> 1 [label="(b & c)\n"]
}
EOF
......
......@@ -39,11 +39,11 @@ digraph G {
0 [label="", style=invis, height=0]
0 -> 1
1 [label="s1"]
1 -> 2 [label="(a & !b)\n<Acc[c]:0, Acc[d]:1><Acc[c]:1, Acc[d]:0>"]
1 -> 2 [label="(a & !b)\n{Acc[d], Acc[c]}"]
2 [label="s2"]
2 -> 3 [label="a\n<Acc[c]:1, Acc[d]:0>"]
2 -> 3 [label="a\n{Acc[c]}"]
3 [label="state 3"]
3 -> 1 [label="1\nF"]
3 -> 1 [label="1\n"]
}
EOF
......
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