dot.cc 17.7 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2011, 2012, 2014, 2015, 2016 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 <stdexcept>
25
26
27
28
29
30
31
32
33
#include <spot/twa/twagraph.hh>
#include <spot/twaalgos/dot.hh>
#include <spot/twa/bddprint.hh>
#include <spot/twaalgos/reachiter.hh>
#include <spot/misc/escape.hh>
#include <spot/twa/twagraph.hh>
#include <spot/twa/formula2bdd.hh>
#include <spot/twaalgos/copy.hh>
#include <spot/twaalgos/sccinfo.hh>
34
#include <spot/kripke/fairkripke.hh>
35
#include <cstdlib>
36
#include <cstring>
37
#include <algorithm>
38
39
#include <ctype.h>

40
41
42

namespace spot
{
43
  namespace
44
  {
45
46
    constexpr int MAX_BULLET = 20;

47
48
49
50
51
    class dotty_output
    {
      std::ostream& os_;
      bool opt_force_acc_trans_ = false;
      bool opt_horizontal_ = true;
52
      bool opt_name_ = false;
53
54
      enum { ShapeAuto = 0, ShapeCircle, ShapeEllipse }
	opt_shape_ = ShapeAuto;
55
      bool opt_show_acc_ = false;
56
      bool mark_states_ = false;
57
      bool opt_scc_ = false;
58
      bool opt_html_labels_ = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
59
      bool opt_state_labels_ = false;
60
      const_twa_graph_ptr aut_;
61
      std::vector<std::string>* sn_ = nullptr;
62
63
      std::map<unsigned, unsigned>* highlight_edges_ = nullptr;
      std::map<unsigned, unsigned>* highlight_states_ = nullptr;
64
      std::vector<std::pair<unsigned, unsigned>>* sprod_ = nullptr;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
65
      std::set<unsigned>* incomplete_;
66
      std::string* name_ = nullptr;
67
68
69
70
      acc_cond::mark_t inf_sets_ = 0U;
      acc_cond::mark_t fin_sets_ = 0U;
      bool opt_rainbow = false;
      bool opt_bullet = false;
71
      bool opt_bullet_but_buchi = false;
72
      bool opt_all_bullets = false;
73
      bool opt_ordered_edges_ = false;
74
      bool opt_numbered_edges_ = false;
75
      bool opt_want_state_names_ = true;
76
      unsigned opt_shift_sets_ = 0;
77
      std::string opt_font_;
78
      std::string opt_node_color_;
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93

      const char* const palette9[9] =
	{
	  "#5DA5DA", /* blue */
	  "#F17CB0", /* pink */
	  "#FAA43A", /* orange */
	  "#B276B2", /* purple */
	  "#60BD68", /* green */
	  "#F15854", /* red */
	  "#B2912F", /* brown */
	  "#4D4D4D", /* gray */
	  "#DECF3F", /* yellow */
	};
      const char*const* palette = palette9;
      int palette_mod = 9;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
94
95
      unsigned max_states_ = -1U;
      bool max_states_given_ = false;
96
97

    public:
98

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
99
100
101
102
103
104
105
106
107
108
      unsigned max_states()
      {
	return max_states_;
      }

      bool max_states_given()
      {
	return max_states_given_;
      }

109
110
      void
      parse_opts(const char* options)
111
      {
112
113
114
115
116
	const char* orig = options;
	while (char c = *options++)
	  switch (c)
	    {
	    case '.':
117
	      {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
118
		// Copy the value in a string, so future calls to
119
120
121
122
123
124
125
126
127
		// parse_opts do not fail if the environment has
		// changed.  (This matters particularly in an ipython
		// notebook, where it is tempting to redefine
		// SPOT_DOTDEFAULT.)
		static std::string def = []()
		  {
		    auto s = getenv("SPOT_DOTDEFAULT");
		    return s ? s : "";
		  }();
128
		// Prevent infinite recursions...
129
		if (orig == def.c_str())
130
131
		  throw std::runtime_error
		    (std::string("SPOT_DOTDEFAULT should not contain '.'"));
132
133
		if (!def.empty())
		  parse_opts(def.c_str());
134
		break;
135
	      }
136
137
138
139
140
141
142
143
144
145
	    case '+':
	      {
		char* end;
		opt_shift_sets_ = strtoul(options, &end, 10);
		if (options == end)
		  throw std::runtime_error
		    ("missing number after '+' in print_dot() options");
		options = end;
		break;
	      }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
	    case '<':
	      {
		char* end;
		max_states_ = strtoul(options, &end, 10);
		if (options == end)
		  throw std::runtime_error
		    ("missing number after '<' in print_dot() options");
		if (max_states_ == 0)
		  {
		    max_states_ = -1U;
		    max_states_given_ = false;
		  }
		else
		  {
		    max_states_given_ = true;
		  }
		options = end;
		break;
	      }
165
166
167
	    case '#':
	      opt_numbered_edges_ = true;
	      break;
168
169
170
	    case '1':
	      opt_want_state_names_ = false;
	      break;
171
172
173
174
175
	    case 'a':
	      opt_show_acc_ = true;
	      break;
	    case 'b':
	      opt_bullet = true;
176
	      opt_bullet_but_buchi = false;
177
	      break;
178
179
180
181
	    case 'B':
	      opt_bullet = true;
	      opt_bullet_but_buchi = true;
	      break;
182
	    case 'c':
183
	      opt_shape_ = ShapeCircle;
184
	      break;
185
186
187
188
189
190
191
192
193
194
195
196
197
	    case 'C':
	      if (*options != '(')
		throw std::runtime_error
		  ("invalid node color specification for print_dot()");
	      {
		auto* end = strchr(++options, ')');
		if (!end)
		  throw std::runtime_error
		    ("invalid node color specification for print_dot()");
		opt_node_color_ = std::string(options, end - options);
		options = end + 1;
	      }
	      break;
198
199
	    case 'e':
	      opt_shape_ = ShapeEllipse;
200
201
202
	      break;
	    case 'f':
	      if (*options != '(')
203
		throw std::runtime_error
204
		  ("invalid font specification for print_dot()");
205
206
207
208
	      {
		auto* end = strchr(++options, ')');
		if (!end)
		  throw std::runtime_error
209
		    ("invalid font specification for print_dot()");
210
211
		opt_font_ = std::string(options, end - options);
		options = end + 1;
212
	      }
213
	      break;
214
215
216
	    case 'h':
	      opt_horizontal_ = true;
	      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
217
218
219
	    case 'k':
	      opt_state_labels_ = true;
	      break;
220
221
222
223
224
225
	    case 'n':
	      opt_name_ = true;
	      break;
	    case 'N':
	      opt_name_ = false;
	      break;
226
	    case 'o':
227
	      opt_ordered_edges_ = true;
228
	      break;
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
	    case 'r':
	      opt_html_labels_ = true;
	      opt_rainbow = true;
	      break;
	    case 'R':
	      opt_html_labels_ = true;
	      opt_rainbow = false;
	      break;
	    case 's':
	      opt_scc_ = true;
	      break;
	    case 'v':
	      opt_horizontal_ = false;
	      break;
	    case 't':
	      opt_force_acc_trans_ = true;
	      break;
	    default:
	      throw std::runtime_error
248
		(std::string("unknown option for print_dot(): ") + c);
249
250
251
252
253
254
255
256
257
258
259
260
	    }
      }

      dotty_output(std::ostream& os, const char* options)
	: os_(os)
      {
	parse_opts(options ? options : ".");
      }

      void
      output_set(std::ostream& os, int v) const
      {
261
	v += opt_shift_sets_;
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
	if (opt_bullet && (v >= 0) & (v <= MAX_BULLET))
	  {
	    static const char* const tab[MAX_BULLET + 1] = {
	      "⓿", "❶", "❷", "❸",
	      "❹", "❺", "❻", "❼",
	      "❽", "❾", "❿", "⓫",
	      "⓬", "⓭", "⓮", "⓯",
	      "⓰", "⓱", "⓲", "⓳",
	      "⓴",
	    };
	    os << tab[v];
	  }
	else
	  {
	    os << v;
	  }
      }

280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
      void
      output_set(acc_cond::mark_t a) const
      {
	if (!opt_all_bullets)
	  os_ << '{';
	const char* space = "";
	for (auto v: a.sets())
	  {
	    if (!opt_all_bullets)
	      os_ << space;
	    output_set(os_, v);
	    space = ",";
	  }
	if (!opt_all_bullets)
	  os_ << '}';
      }
296
297
298
299
300

      const char*
      html_set_color(int v) const
      {
	if (opt_rainbow)
301
	  return palette[(v + opt_shift_sets_) % palette_mod];
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
	// Color according to Fin/Inf
	if (inf_sets_.has(v))
	  {
	    if (fin_sets_.has(v))
	      return palette[2];
	    else
	      return palette[0];
	  }
	else
	  {
	    return palette[1];
	  }
      }

      void
      output_html_set_aux(std::ostream& os, int v) const
      {
	os << "<font color=\"" << html_set_color(v) << "\">";
	output_set(os, v);
	os << "</font>";
      }

      void
      output_html_set(int v) const
      {
	output_html_set_aux(os_, v);
328
329
      }

330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
      void
      output_html_set(acc_cond::mark_t a) const
      {
	if (!opt_all_bullets)
	  os_ << '{';
	const char* space = "";
	for (auto v: a.sets())
	  {
	    if (!opt_all_bullets)
	      os_ << space;
	    output_html_set(v);
	    space = ",";
	  }
	if (!opt_all_bullets)
	  os_ << '}';
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
      std::string
      state_label(unsigned s) const
      {
	bdd label = bddfalse;
	for (auto& t: aut_->out(s))
	  {
	    label = t.cond;
	    break;
	  }
	if (label == bddfalse
	    && incomplete_ && incomplete_->find(s) != incomplete_->end())
	  return "...";
	return bdd_format_formula(aut_->get_dict(), label);
      }

362
363
364
      void
      start()
      {
365
366
367
	if (opt_html_labels_)
	  std::tie(inf_sets_, fin_sets_) =
	    aut_->get_acceptance().used_inf_fin_sets();
368
	if (opt_bullet && aut_->num_sets() <= MAX_BULLET)
369
	  opt_all_bullets = true;
370
371
372
	os_ << "digraph G {\n";
	if (opt_horizontal_)
	  os_ << "  rankdir=LR\n";
373
374
	if (name_ || opt_show_acc_)
	  {
375
	    if (!opt_html_labels_)
376
	      {
377
378
379
380
381
382
383
		os_ << "  label=\"";
		if (name_)
		  {
		    escape_str(os_, *name_);
		    if (opt_show_acc_)
		      os_ << "\\n";
		  }
384
		if (opt_show_acc_)
385
386
387
388
389
390
		  aut_->get_acceptance().to_text
		    (os_, [this](std::ostream& os, int v)
		     {
		       this->output_set(os, v);
		     });
		os_ << "\"\n";
391
	      }
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
	    else
	      {
		os_ << "  label=<";
		if (name_)
		  {
		    escape_html(os_, *name_);
		    if (opt_show_acc_)
		      os_ << "<br/>";
		  }
		if (opt_show_acc_)
		  aut_->get_acceptance().to_html
		    (os_, [this](std::ostream& os, int v)
		     {
		       this->output_html_set_aux(os, v);
		     });
		os_ << ">\n";
	      }
	    os_ << "  labelloc=\"t\"\n";
410
	  }
411
412
413
414
415
416
417
418
419
420
421
422
	switch (opt_shape_)
	  {
	  case ShapeCircle:
	    os_ << "  node [shape=\"circle\"]\n";
	    break;
	  case ShapeEllipse:
	    // Do not print anything.  Ellipse is
	    // the default shape used by GraphViz.
	    break;
	  case ShapeAuto:
	    SPOT_UNREACHABLE();
	  }
423
424
425
	if (!opt_node_color_.empty())
	  os_ << "  node [style=\"filled\", fillcolor=\""
	      << opt_node_color_ << "\"]\n";
426
427
428
429
430
	if (!opt_font_.empty())
	  os_ << "  fontname=\"" << opt_font_
	      << "\"\n  node [fontname=\"" << opt_font_
	      << "\"]\n  edge [fontname=\"" << opt_font_
	      << "\"]\n";
431
432
433
434
435
436
437
438
	// Always copy the environment variable into a static string,
	// so that we (1) look it up once, but (2) won't crash if the
	// environment is changed.
	static std::string extra = []()
	  {
	    auto s = getenv("SPOT_DOTEXTRA");
	    return s ? s : "";
	  }();
439
440
441
	// Any extra text passed in the SPOT_DOTEXTRA environment
	// variable should be output at the end of the "header", so
	// that our setup can be overridden.
442
	if (!extra.empty())
443
	  os_ << "  " << extra << '\n';
444
445
446
447
448
449
450
451
452
453
454
455
456
457
	os_ << "  I [label=\"\", style=invis, ";
	os_ << (opt_horizontal_ ? "width" : "height");
	os_ << "=0]\n  I -> " << aut_->get_init_state_number() << '\n';
      }

      void
      end()
      {
	os_ << '}' << std::endl;
      }

      void
      process_state(unsigned s)
      {
458
459
	if (mark_states_ &&
	    ((opt_bullet && !opt_bullet_but_buchi)
460
	     || aut_->num_sets() != 1))
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
	  {
	    acc_cond::mark_t acc = 0U;
	    for (auto& t: aut_->out(s))
	      {
		acc = t.acc;
		break;
	      }

	    bool has_name = sn_ && s < sn_->size() && !(*sn_)[s].empty();

	    os_ << "  " << s << " [label=";
	    if (!opt_html_labels_)
	      {
		os_ << '"';
		if (has_name)
		  escape_str(os_, (*sn_)[s]);
477
478
		else if (sprod_)
		  os_ << (*sprod_)[s].first << ',' << (*sprod_)[s].second;
479
480
481
482
483
484
485
		else
		  os_ << s;
		if (acc)
		  {
		    os_ << "\\n";
		    output_set(acc);
		  }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
486
487
		if (opt_state_labels_)
		  escape_str(os_ << "\\n", state_label(s));
488
489
490
491
492
493
494
		os_ << '"';
	      }
	    else
	      {
		os_ << '<';
		if (has_name)
		  escape_html(os_, (*sn_)[s]);
495
496
		else if (sprod_)
		  os_ << (*sprod_)[s].first << ',' << (*sprod_)[s].second;
497
498
499
500
501
502
503
		else
		  os_ << s;
		if (acc)
		  {
		    os_ << "<br/>";
		    output_html_set(acc);
		  }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
504
505
		if (opt_state_labels_)
		  escape_html(os_ << "<br/>", state_label(s));
506
507
508
		os_ << '>';
	      }
	  }
509
	else
510
511
512
513
	  {
	    os_ << "  " << s << " [label=\"";
	    if (sn_ && s < sn_->size() && !(*sn_)[s].empty())
	      escape_str(os_, (*sn_)[s]);
514
515
	    else if (sprod_)
	      os_ << (*sprod_)[s].first << ',' << (*sprod_)[s].second;
516
517
	    else
	      os_ << s;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
518
519
	    if (opt_state_labels_)
	      escape_str(os_ << "\\n", state_label(s));
520
	    os_ << '"';
521
522
523
524
	    // Use state_acc_sets(), not state_is_accepting() because
	    // on co-Büchi automata we want to mark the rejecting
	    // states.
	    if (mark_states_ && aut_->state_acc_sets(s))
525
526
	      os_ << ", peripheries=2";
	  }
527
528
529
530
	if (highlight_states_)
	  {
	    auto iter = highlight_states_->find(s);
	    if (iter != highlight_states_->end())
531
532
533
534
535
536
537
	      {
		os_ << ", style=\"bold";
		if (!opt_node_color_.empty())
		  os_ << ",filled";
		os_ << "\", color=\"" << palette[iter->second % palette_mod]
		    << '"';
	      }
538
539
	  }
	os_ << "]\n";
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
540
541
542
	if (incomplete_ && incomplete_->find(s) != incomplete_->end())
	  os_ << "  u" << s << " [label=\"...\", shape=none, width=0, height=0"
	    "]\n  " << s << " -> u" << s << " [style=dashed]\n";
543
544
545
      }

      void
546
      process_link(const twa_graph::edge_storage_t& t, int number)
547
      {
548
	os_ << "  " << t.src << " -> " << t.dst;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
549
550
551
	std::string label;
	if (!opt_state_labels_)
	  label = bdd_format_formula(aut_->get_dict(), t.cond);
552
553
554
555
556
557
558
	if (!opt_html_labels_)
	  {
	    os_ << " [label=\"";
	    escape_str(os_, label);
	    if (!mark_states_)
	      if (auto a = t.acc)
		{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
559
560
		  if (!opt_state_labels_)
		    os_ << "\\n";
561
		  output_set(a);
562
		}
563
	    os_ << '"';
564
565
566
567
568
569
570
571
	  }
	else
	  {
	    os_ << " [label=<";
	    escape_html(os_, label);
	    if (!mark_states_)
	      if (auto a = t.acc)
		{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
572
573
		  if (!opt_state_labels_)
		    os_ << "<br/>";
574
		  output_html_set(a);
575
		}
576
	    os_ << '>';
577
	  }
578
579
580
581
582
583
584
585
586
587
588
	if (opt_ordered_edges_ || opt_numbered_edges_)
	  {
	    os_ << ", taillabel=\"";
	    if (opt_ordered_edges_)
	      os_ << number;
	    if (opt_ordered_edges_ && opt_numbered_edges_)
	      os_ << ' ';
	    if (opt_numbered_edges_)
	      os_ << '#' << aut_->get_graph().index_of_edge(t);
	    os_ << '"';
	  }
589
590
591
592
593
594
595
596
597
	if (highlight_edges_)
	  {
	    auto idx = aut_->get_graph().index_of_edge(t);
	    auto iter = highlight_edges_->find(idx);
	    if (iter != highlight_edges_->end())
	      os_ << ", style=bold, color=\""
		  << palette[iter->second % palette_mod]
		  << '"';
	  }
598
	os_ << "]\n";
599
600
      }

601
      void print(const const_twa_graph_ptr& aut)
602
603
      {
	aut_ = aut;
604
	if (opt_want_state_names_)
605
606
607
608
609
610
611
612
613
614
615
616
	  {
	    sn_ = aut->get_named_prop<std::vector<std::string>>("state-names");
	    // We have no names.  Do we have product sources?
	    if (!sn_)
	      {
		sprod_ = aut->get_named_prop
		  <std::vector<std::pair<unsigned, unsigned>>>
		  ("product-states");
		if (sprod_ && aut->num_states() != sprod_->size())
		  sprod_ = nullptr;
	      }
	  }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
	if (opt_state_labels_)
	  {
	    // Verify that we can use state labels for this automaton.
	    unsigned n = aut->num_states();
	    for (unsigned s = 0; s < n; ++s)
	      {
		bool first = true;
		bdd cond = bddfalse;
		for (auto& t: aut->out(s))
		  if (first)
		    {
		      cond = t.cond;
		      first = false;
		    }
		  else if (t.cond != cond)
		    {
		      opt_state_labels_ = false;
		      break;
		    }
	      }
	  }
638
639
640
641
	highlight_edges_ =
	  aut->get_named_prop<std::map<unsigned, unsigned>>("highlight-edges");
	highlight_states_ =
	  aut->get_named_prop<std::map<unsigned, unsigned>>("highlight-states");
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
642
643
	incomplete_ =
	  aut->get_named_prop<std::set<unsigned>>("incomplete-states");
644
645
	if (opt_name_)
	  name_ = aut_->get_named_prop<std::string>("automaton-name");
646
647
	mark_states_ = (!opt_force_acc_trans_
			&& aut_->prop_state_acc().is_true());
648
649
	if (opt_shape_ == ShapeAuto)
	  {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
650
	    if (sn_ || sprod_ || aut->num_states() > 100 || opt_state_labels_)
651
652
653
	      {
		opt_shape_ = ShapeEllipse;
		// If all state names are short, prefer circles.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
654
655
		if (!opt_state_labels_ &&
		    sn_ && std::all_of(sn_->begin(), sn_->end(),
656
657
658
659
				       [](const std::string& s)
				       { return s.size() <= 2; }))
		  opt_shape_ = ShapeCircle;
	      }
660
	    else
661
662
663
	      {
		opt_shape_ = ShapeCircle;
	      }
664
	  }
665
666
	auto si =
	  std::unique_ptr<scc_info>(opt_scc_ ? new scc_info(aut) : nullptr);
667

668
	start();
669
670
	if (si)
	  {
671
672
	    si->determine_unknown_acceptance();

673
674
675
676
	    unsigned sccs = si->scc_count();
	    for (unsigned i = 0; i < sccs; ++i)
	      {
		os_ << "  subgraph cluster_" << i << " {\n";
677
678
679
680
681
682
683
684
685
686
687

		// Color the SCC to indicate whether is it accepting.
		if (!si->is_useful_scc(i))
		  os_ << "  color=grey\n";
		else if (si->is_trivial(i))
		  os_ << "  color=black\n";
		else if (si->is_accepting_scc(i))
		  os_ << "  color=green\n";
		else if (si->is_rejecting_scc(i))
		  os_ << "  color=red\n";
		else
688
689
		  // May only occur if the call to
		  // determine_unknown_acceptance() above is removed.
690
691
		  os_ << "  color=orange\n";

692
		if (name_ || opt_show_acc_)
693
694
695
696
697
		  {
		    // Reset the label, otherwise the graph label would
		    // be inherited by the cluster.
		    os_ << "  label=\"\"\n";
		  }
698
699
700
701
702
		for (auto s: si->states_of(i))
		  process_state(s);
		os_ << "  }\n";
	      }
	  }
703
704
705
	unsigned ns = aut_->num_states();
	for (unsigned n = 0; n < ns; ++n)
	  {
706
	    if (!si || !si->reachable_state(n))
707
	      process_state(n);
708
	    int trans_num = 0;
709
	    for (auto& t: aut_->out(n))
710
	      process_link(t, trans_num++);
711
712
713
714
	  }
	end();
      }
    };
715
  } // anonymous namespace
716
717

  std::ostream&
718
  print_dot(std::ostream& os, const const_twa_ptr& g,
719
		  const char* options)
720
  {
721
    dotty_output d(os, options);
722
    // Enable automatic state labels for Kripke structure.
723
    if (std::dynamic_pointer_cast<const fair_kripke>(g))
724
      d.parse_opts("k");
725
    auto aut = std::dynamic_pointer_cast<const twa_graph>(g);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
726
727
    if (!aut || (d.max_states_given() && aut->num_states() >= d.max_states()))
      aut = copy(g, twa::prop_set::all(), true, d.max_states() - 1);
728
    d.print(aut);
729
730
731
732
733
    return os;
  }


}