dotty.cc 4.02 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche et
3
4
5
6
// Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6
// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
// Pierre et Marie Curie.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
7
8
9
10
11
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
12
// the Free Software Foundation; either version 3 of the License, or
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
13
14
15
16
17
18
19
20
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
21
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
22

23
#include "misc/hash.hh"
24
#include "dotty.hh"
25
26
#include "ltlast/visitor.hh"
#include "ltlast/allnodes.hh"
27
#include <ostream>
28
#include <sstream>
29

30
namespace spot
31
32
33
{
  namespace ltl
  {
34
    namespace
35
    {
36
      class dotty_visitor: public visitor
37
      {
38
      public:
39
	typedef std::unordered_map<const formula*, int, ptr_hash<formula>> map;
40
	dotty_visitor(std::ostream& os, map& m)
41
	  : os_(os), father_(-1), node_(m), sinks_(new std::ostringstream)
42
43
	{
	}
44

45
46
47
48
	virtual
	~dotty_visitor()
	{
	}
49

50
51
52
53
54
	void
	visit(const atomic_prop* ap)
	{
	  draw_node_(ap, ap->name(), true);
	}
55

56
57
58
59
60
	void
	visit(const constant* c)
	{
	  draw_node_(c, c->val_name(), true);
	}
61

62
63
64
	void
	visit(const bunop* so)
	{
65
	  if (draw_node_(so, so->format()))
66
	    {
67
	      childnum = 0;
68
69
70
71
	      so->child()->accept(*this);
	    }
	}

72
73
74
75
76
	void
	visit(const binop* bo)
	{
	  if (draw_node_(bo, bo->op_name()))
	    {
77
	      childnum = -1;
78
79
	      dotty_visitor v(*this);
	      bo->first()->accept(v);
80
	      childnum = -2;
81
82
83
	      bo->second()->accept(*this);
	    }
	}
84

85
86
87
88
	void
	visit(const unop* uo)
	{
	  if (draw_node_(uo, uo->op_name()))
89
	    {
90
	      childnum = 0;
91
92
	      uo->child()->accept(*this);
	    }
93
	}
94

95
96
97
98
99
100
	void
	visit(const automatop*)
	{
	  assert(0);
	}

101
102
103
104
105
	void
	visit(const multop* mo)
	{
	  if (!draw_node_(mo, mo->op_name()))
	    return;
106
	  childnum = 0;
107
	  unsigned max = mo->size();
108
109
110
111
	  multop::type op = mo->op();
	  bool update_childnum = (op == multop::Fusion ||
				  op == multop::Concat);

112
113
	  for (unsigned n = 0; n < max; ++n)
	    {
114
115
	      if (update_childnum)
		++childnum;
116
117
118
119
	      dotty_visitor v(*this);
	      mo->nth(n)->accept(v);
	    }
	}
120
121
122
123
124
125
126
127
128

	void finish()
	{
	  os_ << "  subgraph atoms {" << std::endl
	      << "    rank=sink;" << std::endl
	      << sinks_->str() << "  }" << std::endl;
	  delete sinks_;
	}

129
	int childnum;
130

131
132
133
134
      private:
	std::ostream& os_;
	int father_;
	map& node_;
135
	std::ostringstream* sinks_;
136

137
	bool
138
	draw_node_(const formula* f, const std::string& str, bool sink = false)
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
	{
	  map::iterator i = node_.find(f);
	  int node;
	  bool node_exists = false;
	  if (i != node_.end())
	    {
	      node = i->second;
	      node_exists = true;
	    }
	  else
	    {
	      node = node_.size();
	      node_[f] = node;
	    }
	  // the link
	  if (father_ >= 0)
155
156
	    {
	      os_ << "  " << father_ << " -> " << node;
157
158
159
	      if (childnum > 0)
		os_ << " [taillabel=\"" << childnum << "\"]";
	      if (childnum == -1)
160
		os_ << " [taillabel=\"L\"]";
161
	      else if (childnum == -2)
162
163
164
		os_ << " [taillabel=\"R\"]";
	      os_ << ";" << std::endl;
	    }
165
	  father_ = node;
166

167
168
169
	  // the node
	  if (node_exists)
	    return false;
170
171
172
173
174
175
176
177
178
179

	  if (!sink)
	    {
	      os_ << "  " << node << " [label=\"" << str << "\"];";
	    }
	  else
	    {
	      *sinks_ << "    " << node
		      << " [label=\"" << str << "\", shape=box];\n";
	    }
180
181
182
183
	  return true;
	}
      };
    }
184

185
    std::ostream&
186
    dotty(std::ostream& os, const formula* f)
187
    {
188
189
      dotty_visitor::map m;
      dotty_visitor v(os, m);
190
      os << "digraph G {" << std::endl;
191
      f->accept(v);
192
      v.finish();
193
      os << "}" << std::endl;
194
      return os;
195
196
197
198
    }

  }
}