dotty.cc 1.63 KB
Newer Older
1
#include <map>
2
#include "tgba/tgba.hh"
3
4
5
6
7
8
#include "dotty.hh"
#include "tgba/bddprint.hh"

namespace spot
{
  typedef std::map<int, int> seen_map;
9

10
11
  static bool
  dotty_state(std::ostream& os,
12
	      const tgba& g, state* st, seen_map& m, int& node)
13
  {
14
    bdd s = st->as_bdd();
15
    seen_map::iterator i = m.find(s.id());
16

17
18
19
20
21
22
    // Already drawn?
    if (i != m.end())
      {
	node = i->second;
	return false;
      }
23

24
25
    node = m.size() + 1;
    m[s.id()] = node;
26

27
28
29
30
    std::cout << "  " << node << " [label=\"";
    bdd_print_set(os, g.get_dict(), s) << "\"]" << std::endl;
    return true;
  }
31

32
33
  static void
  dotty_rec(std::ostream& os,
34
	    const tgba& g, state* st, seen_map& m, int father)
35
  {
36
    tgba_succ_iterator* si = g.succ_iter(st);
37
38
39
    for (si->first(); !si->done(); si->next())
      {
	int node;
40
	state* s = si->current_state();
41
42
43
	bool recurse = dotty_state(os, g, s, m, node);
	os << "  " << father << " -> " << node << " [label=\"";
	bdd_print_set(os, g.get_dict(), si->current_condition()) << "\\n";
44
	bdd_print_set(os, g.get_dict(), si->current_promise()) << "\"]"
45
46
47
							       << std::endl;
	if (recurse)
	  dotty_rec(os, g, s, m, node);
48
	delete s;
49
50
51
      }
    delete si;
  }
52
53

  std::ostream&
54
55
56
  dotty_reachable(std::ostream& os, const tgba& g)
  {
    seen_map m;
57
    state* state = g.get_init_state();
58
59
60
61
62
63
64
65
    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;
66
    delete state;
67
68
69
70
71
    return os;
  }


}