bddprint.cc 1.48 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
#include "bddprint.hh"
#include "ltlvisit/tostring.hh"

namespace spot
{

  const tgba_bdd_dict* dict;

  static void
  print_handler(std::ostream& o, int var)
  {
    tgba_bdd_dict::vf_map::const_iterator isi = 
      dict->var_formula_map.find(var);
    if (isi != dict->var_formula_map.end())
      to_string(isi->second, o);
    else
      {
	isi = dict->prom_formula_map.find(var);
	if (isi != dict->prom_formula_map.end())
	  {
	    o << "Prom["; to_string(isi->second, o) << "]";
	  }
	else
	  {
	    isi = dict->now_formula_map.find(var);
	    if (isi != dict->now_formula_map.end())
	      {
		o << "Now["; to_string(isi->second, o) << "]";
	      }
	    else
	      {
		isi = dict->now_formula_map.find(var - 1);
		if (isi != dict->now_formula_map.end())
		  {
		    o << "Next["; to_string(isi->second, o) << "]";
		  }
		else
		  {
		    o << "?" << var;
		  }
	      }
	  }
      }
  }
  

  std::ostream& 
  bdd_print_set(std::ostream& os, const tgba_bdd_dict& d, bdd b)
  {
    dict = &d;
    bdd_strm_hook(print_handler);
    os << bddset << b;
    bdd_strm_hook(0);
    return os;
  }

  std::ostream& 
  bdd_print_dot(std::ostream& os, const tgba_bdd_dict& d, bdd b)
  {
    dict = &d;
    bdd_strm_hook(print_handler);
    os << bdddot << b;
    bdd_strm_hook(0);
    return os;
  }
  
  std::ostream& 
  bdd_print_table(std::ostream& os, const tgba_bdd_dict& d, bdd b)
  {
    dict = &d;
    bdd_strm_hook(print_handler);
    os << bddtable << b;
    bdd_strm_hook(0);
    return os;
  }

}