diff --git a/src/bin/common_aoutput.cc b/src/bin/common_aoutput.cc index d654811ee..8ec768c67 100644 --- a/src/bin/common_aoutput.cc +++ b/src/bin/common_aoutput.cc @@ -51,7 +51,8 @@ static const argp_option options[] = { "dot", OPT_DOT, "c|h|n|N|t|v", OPTION_ARG_OPTIONAL, "GraphViz's format (default). Add letters to chose (c) circular nodes, " "(h) horizontal layout, (v) vertical layout, (n) with name, " - "(N) without name, (t) always transition-based acceptance.", 0 }, + "(N) without name, (s) with SCCs, " + "(t) always transition-based acceptance.", 0 }, { "hoaf", 'H', "s|t|m|l", OPTION_ARG_OPTIONAL, "Output the automaton in HOA format. Add letters to select " "(s) state-based acceptance, (t) transition-based acceptance, " diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc index adadc167e..e6033e148 100644 --- a/src/bin/dstar2tgba.cc +++ b/src/bin/dstar2tgba.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -73,7 +73,8 @@ static const argp_option options[] = { "dot", OPT_DOT, "c|h|n|N|t|v", OPTION_ARG_OPTIONAL, "GraphViz's format (default). Add letters to chose (c) circular nodes, " "(h) horizontal layout, (v) vertical layout, (n) with name, " - "(N) without name, (t) always transition-based acceptance.", 0 }, + "(N) without name, (s) with SCCs, " + "(t) always transition-based acceptance.", 0 }, { "hoaf", 'H', "s|t|m|l", OPTION_ARG_OPTIONAL, "Output the automaton in HOA format. Add letters to select " "(s) state-based acceptance, (t) transition-based acceptance, " diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc index 0dfad6244..ea01f8302 100644 --- a/src/tgbaalgos/dotty.cc +++ b/src/tgbaalgos/dotty.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2014 Laboratoire de Recherche et +// Copyright (C) 2011, 2012, 2014, 2015 Laboratoire de Recherche et // Developpement 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 @@ -30,6 +30,7 @@ #include "misc/escape.hh" #include "tgba/tgbagraph.hh" #include "tgba/formula2bdd.hh" +#include "tgbaalgos/sccinfo.hh" namespace spot { @@ -43,6 +44,7 @@ namespace spot bool opt_name_ = true; bool opt_circles_ = false; bool mark_states_ = false; + bool opt_scc_ = false; const_tgba_digraph_ptr aut_; public: @@ -65,6 +67,9 @@ namespace spot case 'N': opt_name_ = false; break; + case 's': + opt_scc_ = true; + break; case 'v': opt_horizontal_ = false; break; @@ -128,11 +133,25 @@ namespace spot { aut_ = aut; mark_states_ = !opt_force_acc_trans_ && aut_->has_state_based_acc(); + auto si = + std::unique_ptr(opt_scc_ ? new scc_info(aut) : nullptr); start(); + if (si) + { + unsigned sccs = si->scc_count(); + for (unsigned i = 0; i < sccs; ++i) + { + os_ << " subgraph cluster_" << i << " {\n"; + for (auto s: si->states_of(i)) + process_state(s); + os_ << " }\n"; + } + } unsigned ns = aut_->num_states(); for (unsigned n = 0; n < ns; ++n) { - process_state(n); + if (!si) + process_state(n); for (auto& t: aut_->out(n)) process_link(t); } diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test index 6bc59505b..a5267ff30 100755 --- a/src/tgbatest/neverclaimread.test +++ b/src/tgbatest/neverclaimread.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche -# et Développement de l'Epita (LRDE). +# Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de +# Recherche et Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -322,16 +322,21 @@ accept_all: skip } EOF -../../bin/autfilt --dot stdout 2>stderr && exit 1 +../../bin/autfilt --dot=sc stdout 2>stderr && exit 1 cat >expected < 0 + subgraph cluster_0 { + 1 [label="1", peripheries=2] + } + subgraph cluster_1 { 0 [label="0"] + } 0 -> 1 [label="b"] 0 -> 0 [label="0"] - 1 [label="1", peripheries=2] 1 -> 1 [label="1"] } EOF