dotty.cc 3.45 KB
Newer Older
1
2
3
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2012, 2014 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE).
4
// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
5
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
6
7
8
9
10
11
// et Marie Curie.
//
// 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 <ostream>
24
#include "tgba/tgbagraph.hh"
25
#include "dotty.hh"
26
#include "dottydec.hh"
27
#include "tgba/bddprint.hh"
28
#include "reachiter.hh"
29
#include "misc/escape.hh"
30
#include "tgba/tgbagraph.hh"
31
#include "tgba/formula2bdd.hh"
32
33
34

namespace spot
{
35
  namespace
36
  {
37
    class dotty_bfs : public tgba_reachable_iterator_breadth_first
38
    {
39
    public:
40
41
42
43
      dotty_bfs(std::ostream& os, const tgba* a, bool mark_accepting_states,
		dotty_decorator* dd)
	: tgba_reachable_iterator_breadth_first(a), os_(os),
	  mark_accepting_states_(mark_accepting_states), dd_(dd),
44
	  sba_(dynamic_cast<const tgba_digraph*>(a))
45
46
      {
      }
47

48
49
50
      void
      start()
      {
51
52
53
	os_ << ("digraph G {\n"
		"  0 [label=\"\", style=invis, height=0]\n"
		"  0 -> 1\n");
54
      }
55

56
57
58
      void
      end()
      {
59
	os_ << '}' << std::endl;
60
      }
61

62
      void
63
      process_state(const state* s, int n, tgba_succ_iterator* si)
64
      {
65
66
67
68
69
70
71
72
73
74
75
76
77
	bool accepting;

	if (mark_accepting_states_)
	  {
	    if (sba_)
	      {
		accepting = sba_->state_is_accepting(s);
	      }
	    else
	      {
		si->first();
		accepting = ((!si->done())
			     && (si->current_acceptance_conditions() ==
78
				 aut_->all_acceptance_conditions()));
79
80
81
82
83
84
85
	      }
	  }
	else
	  {
	    accepting = false;
	  }

86
	os_ << "  " << n << ' '
87
88
	    << dd_->state_decl(aut_, s, n, si,
			       escape_str(aut_->format_state(s)),
89
			       accepting)
90
	    << '\n';
91
      }
92

93
      void
94
95
      process_link(const state* in_s, int in,
		   const state* out_s, int out, const tgba_succ_iterator* si)
96
      {
97
	std::string label =
98
	  bdd_format_formula(aut_->get_dict(),
99
100
			     si->current_condition())
	  + "\n"
101
	  + bdd_format_accset(aut_->get_dict(),
102
103
			      si->current_acceptance_conditions());

104
	std::string s = aut_->transition_annotation(si);
105
106
107
108
109
110
111
	if (!s.empty())
	  {
	    if (*label.rbegin() != '\n')
	      label += '\n';
	    label += s;
	  }

112
	os_ << "  " << in << " -> " << out << ' '
113
	    << dd_->link_decl(aut_, in_s, in, out_s, out, si,
114
			      escape_str(label))
115
	    << '\n';
116
      }
117

118
119
    private:
      std::ostream& os_;
120
      bool mark_accepting_states_;
121
      dotty_decorator* dd_;
122
      const tgba_digraph* sba_;
123
124
    };
  }
125
126

  std::ostream&
127
128
  dotty_reachable(std::ostream& os, const tgba* g,
		  bool assume_sba, dotty_decorator* dd)
129
  {
130
131
    if (!dd)
      dd = dotty_decorator::instance();
132
133
134
    if (const tgba_digraph* gd = dynamic_cast<const tgba_digraph*>(g))
      assume_sba |= gd->get_bprop(tgba_digraph::StateBasedAcc);

135
    dotty_bfs d(os, g, assume_sba, dd);
136
    d.run();
137
138
139
140
141
    return os;
  }


}