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

namespace spot
{
8
  typedef std::map<state*, int, state_ptr_less_than> 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
    seen_map::iterator i = m.find(st);
15

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

23
    node = m.size() + 1;
24
    m[st] = node;
25

26
27
    os << "  " << node << " [label=\"" 
       << g.format_state(st) << "\"]" << std::endl;
28
29
    return true;
  }
30

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

  std::ostream&
59
60
61
  dotty_reachable(std::ostream& os, const tgba& g)
  {
    seen_map m;
62
    state* state = g.get_init_state();
63
64
65
66
67
68
69
70
    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;
71
72
73
74
75

    // Finally delete all states used as keys in m:
    for (seen_map::iterator i = m.begin(); i != m.end(); ++i)
      delete i->first;

76
77
78
79
80
    return os;
  }


}