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

* src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh: New files.

* src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES): Add them.
parent 53f8f29a
2003-05-26 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgba/tgbabddtranslatefactory.cc
* src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh: New files.
* src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES): Add them.
* src/tgba/tgbabddtranslatefactory.cc
(tgba_bdd_translate_factory::compute_pairs): Be quiet.
* src/Makefile.am (SUBDIRS): Add tgbaalgos.
......
......@@ -2,4 +2,6 @@ AM_CPPFLAGS = -I$(srcdir)/..
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
noinst_LTLIBRARIES = libtgbaalgos.la
libtgbaalgos_la_SOURCES =
libtgbaalgos_la_SOURCES = \
dotty.cc \
dotty.hh
#include <map>
#include "dotty.hh"
#include "tgba/bddprint.hh"
namespace spot
{
typedef std::map<int, int> seen_map;
static bool
dotty_state(std::ostream& os,
const tgba& g, state_bdd state, seen_map& m, int& node)
{
bdd s = state.as_bdd();
seen_map::iterator i = m.find(s.id());
// Already drawn?
if (i != m.end())
{
node = i->second;
return false;
}
node = m.size() + 1;
m[s.id()] = node;
std::cout << " " << node << " [label=\"";
bdd_print_set(os, g.get_dict(), s) << "\"]" << std::endl;
return true;
}
static void
dotty_rec(std::ostream& os,
const tgba& g, state_bdd state, seen_map& m, int father)
{
tgba_succ_iterator* si = g.succ_iter(state);
for (si->first(); !si->done(); si->next())
{
int node;
state_bdd s = si->current_state();
bool recurse = dotty_state(os, g, s, m, node);
os << " " << father << " -> " << node << " [label=\"";
bdd_print_set(os, g.get_dict(), si->current_condition()) << "\\n";
bdd_print_set(os, g.get_dict(), si->current_promise()) << "\"]"
<< std::endl;
if (recurse)
dotty_rec(os, g, s, m, node);
}
delete si;
}
std::ostream&
dotty_reachable(std::ostream& os, const tgba& g)
{
seen_map m;
state_bdd state = g.get_init_state();
os << "digraph G {" << std::endl;
os << " size=\"7.26,10.69\"" << std::endl;
os << " 0 [label=\"\", style=invis]" << std::endl;
int init;
dotty_state(os, g, state, m, init);
os << " 0 -> " << init << std::endl;
dotty_rec(os, g, state, m, init);
os << "}" << std::endl;
return os;
}
}
#ifndef SPOT_TGBAALGOS_DOTTY_HH
# define SPOT_TGBAALGOS_DOTTY_HH
#include "tgba/tgba.hh"
#include <iostream>
namespace spot
{
/// \brief Print reachable states in dot format.
std::ostream& dotty_reachable(std::ostream& os, const tgba& g);
}
#endif // SPOT_TGBAALGOS_DOTTY_HH
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