diff --git a/bench/stutter/stutter_invariance_randomgraph.cc b/bench/stutter/stutter_invariance_randomgraph.cc
index df80543cf..2c4ce6724 100644
--- a/bench/stutter/stutter_invariance_randomgraph.cc
+++ b/bench/stutter/stutter_invariance_randomgraph.cc
@@ -21,7 +21,7 @@
#include "ltlvisit/apcollect.hh"
#include "twaalgos/dtgbacomp.hh"
#include "twaalgos/randomgraph.hh"
-#include "twaalgos/dotty.hh"
+#include "twaalgos/dot.hh"
#include "twaalgos/product.hh"
#include "twaalgos/stutter.hh"
#include "twaalgos/stats.hh"
diff --git a/iface/ltsmin/modelcheck.cc b/iface/ltsmin/modelcheck.cc
index 8cbd42550..d47bc8193 100644
--- a/iface/ltsmin/modelcheck.cc
+++ b/iface/ltsmin/modelcheck.cc
@@ -18,7 +18,7 @@
// along with this program. If not, see .
#include "ltsmin.hh"
-#include "twaalgos/dotty.hh"
+#include "twaalgos/dot.hh"
#include "ltlenv/defaultenv.hh"
#include "ltlast/allnodes.hh"
#include "ltlparse/public.hh"
@@ -230,9 +230,9 @@ checked_main(int argc, char **argv)
if (output == DotModel)
{
- tm.start("dotty output");
- spot::dotty_reachable(std::cout, model);
- tm.stop("dotty output");
+ tm.start("dot output");
+ spot::print_dot(std::cout, model);
+ tm.stop("dot output");
goto safe_exit;
}
if (output == Kripke)
@@ -246,9 +246,9 @@ checked_main(int argc, char **argv)
if (output == DotFormula)
{
- tm.start("dotty output");
- spot::dotty_reachable(std::cout, prop);
- tm.stop("dotty output");
+ tm.start("dot output");
+ spot::print_dot(std::cout, prop);
+ tm.stop("dot output");
goto safe_exit;
}
@@ -256,9 +256,9 @@ checked_main(int argc, char **argv)
if (output == DotProduct)
{
- tm.start("dotty output");
- spot::dotty_reachable(std::cout, product);
- tm.stop("dotty output");
+ tm.start("dot output");
+ spot::print_dot(std::cout, product);
+ tm.stop("dot output");
goto safe_exit;
}
diff --git a/src/bin/common_aoutput.cc b/src/bin/common_aoutput.cc
index 8cabe4510..d6294806e 100644
--- a/src/bin/common_aoutput.cc
+++ b/src/bin/common_aoutput.cc
@@ -27,7 +27,7 @@
#include "twa/bddprint.hh"
-#include "twaalgos/dotty.hh"
+#include "twaalgos/dot.hh"
#include "twaalgos/lbtt.hh"
#include "twaalgos/hoa.hh"
#include "twaalgos/neverclaim.hh"
@@ -319,19 +319,19 @@ automaton_printer::print(const spot::twa_graph_ptr& aut,
// Do not output anything.
break;
case Dot:
- spot::dotty_reachable(*out, aut, opt_dot);
+ spot::print_dot(*out, aut, opt_dot);
break;
case Lbtt:
- spot::lbtt_reachable(*out, aut, type == spot::postprocessor::BA);
+ spot::print_lbtt(*out, aut, type == spot::postprocessor::BA);
break;
case Lbtt_t:
- spot::lbtt_reachable(*out, aut, false);
+ spot::print_lbtt(*out, aut, false);
break;
case Hoa:
spot::hoa_reachable(*out, aut, hoa_opt) << '\n';
break;
case Spin:
- spot::never_claim_reachable(*out, aut, opt_never);
+ spot::print_never_claim(*out, aut, opt_never);
break;
case Stats:
statistics.set_output(*out);
diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc
index d49281c9f..b1f66d986 100644
--- a/src/bin/dstar2tgba.cc
+++ b/src/bin/dstar2tgba.cc
@@ -32,7 +32,7 @@
#include "common_post.hh"
#include "common_file.hh"
-#include "twaalgos/dotty.hh"
+#include "twaalgos/dot.hh"
#include "twaalgos/lbtt.hh"
#include "twaalgos/hoa.hh"
#include "twaalgos/neverclaim.hh"
@@ -388,19 +388,19 @@ namespace
switch (format)
{
case Dot:
- spot::dotty_reachable(*out, aut, opt_dot);
+ spot::print_dot(*out, aut, opt_dot);
break;
case Lbtt:
- spot::lbtt_reachable(*out, aut, type == spot::postprocessor::BA);
+ spot::print_lbtt(*out, aut, type == spot::postprocessor::BA);
break;
case Lbtt_t:
- spot::lbtt_reachable(*out, aut, false);
+ spot::print_lbtt(*out, aut, false);
break;
case Hoa:
spot::hoa_reachable(*out, aut, hoa_opt) << '\n';
break;
case Spin:
- spot::never_claim_reachable(*out, aut, opt_never);
+ spot::print_never_claim(*out, aut, opt_never);
break;
case Stats:
statistics.set_output(*out);
diff --git a/src/bin/ltl2tgta.cc b/src/bin/ltl2tgta.cc
index 7580f6abc..13974256f 100644
--- a/src/bin/ltl2tgta.cc
+++ b/src/bin/ltl2tgta.cc
@@ -35,13 +35,13 @@
#include "ltlparse/public.hh"
#include "ltlvisit/print.hh"
#include "ltlvisit/simplify.hh"
-#include "twaalgos/dotty.hh"
+#include "twaalgos/dot.hh"
#include "twaalgos/ltl2tgba_fm.hh"
#include "twaalgos/translate.hh"
#include "twa/bddprint.hh"
#include "taalgos/tgba2ta.hh"
-#include "taalgos/dotty.hh"
+#include "taalgos/dot.hh"
#include "taalgos/minimize.hh"
#include "misc/optionmap.hh"
@@ -198,14 +198,14 @@ namespace
opt_with_artificial_livelock);
if (level != spot::postprocessor::Low)
testing_automaton = spot::minimize_ta(testing_automaton);
- spot::dotty_reachable(std::cout, testing_automaton);
+ spot::print_dot(std::cout, testing_automaton);
}
else
{
auto tgta = tgba_to_tgta(aut, ap_set);
if (level != spot::postprocessor::Low)
tgta = spot::minimize_tgta(tgta);
- spot::dotty_reachable(std::cout, tgta->get_ta());
+ spot::print_dot(std::cout, tgta->get_ta());
}
f->destroy();
flush_cout();
diff --git a/src/dstarparse/dra2ba.cc b/src/dstarparse/dra2ba.cc
index 7e54007c7..ff64411c1 100644
--- a/src/dstarparse/dra2ba.cc
+++ b/src/dstarparse/dra2ba.cc
@@ -23,7 +23,7 @@
#include "twaalgos/reachiter.hh"
#include "twaalgos/gtec/gtec.hh"
#include "twaalgos/sccfilter.hh"
-#include "twaalgos/dotty.hh"
+#include "twaalgos/dot.hh"
namespace spot
{
diff --git a/src/ltlvisit/Makefile.am b/src/ltlvisit/Makefile.am
index 5c56a104e..15b62810c 100644
--- a/src/ltlvisit/Makefile.am
+++ b/src/ltlvisit/Makefile.am
@@ -29,7 +29,7 @@ ltlvisit_HEADERS = \
apcollect.hh \
contain.hh \
clone.hh \
- dotty.hh \
+ dot.hh \
dump.hh \
exclusive.hh \
length.hh \
@@ -52,7 +52,7 @@ libltlvisit_la_SOURCES = \
apcollect.cc \
contain.cc \
clone.cc \
- dotty.cc \
+ dot.cc \
dump.cc \
exclusive.cc \
length.cc \
diff --git a/src/ltlvisit/dotty.cc b/src/ltlvisit/dot.cc
similarity index 90%
rename from src/ltlvisit/dotty.cc
rename to src/ltlvisit/dot.cc
index b4cf6cc58..c2684da74 100644
--- a/src/ltlvisit/dotty.cc
+++ b/src/ltlvisit/dot.cc
@@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
-// Recherche et Développement de l'Epita (LRDE).
+// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire
+// de Recherche et 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.
@@ -21,7 +21,7 @@
// along with this program. If not, see .
#include "misc/hash.hh"
-#include "dotty.hh"
+#include "dot.hh"
#include "ltlast/visitor.hh"
#include "ltlast/allnodes.hh"
#include
@@ -114,9 +114,9 @@ namespace spot
void finish()
{
- os_ << " subgraph atoms {" << std::endl
- << " rank=sink;" << std::endl
- << sinks_->str() << " }" << std::endl;
+ os_ << (" subgraph atoms {\n"
+ " rank=sink;\n")
+ << sinks_->str() << " }\n";
delete sinks_;
}
@@ -154,7 +154,7 @@ namespace spot
os_ << " [taillabel=\"L\"]";
else if (childnum == -2)
os_ << " [taillabel=\"R\"]";
- os_ << ';' << std::endl;
+ os_ << ";\n";
}
father_ = node;
@@ -177,11 +177,11 @@ namespace spot
}
std::ostream&
- dotty(std::ostream& os, const formula* f)
+ print_dot_psl(std::ostream& os, const formula* f)
{
dotty_visitor::map m;
dotty_visitor v(os, m);
- os << "digraph G {" << std::endl;
+ os << "digraph G {\n";
f->accept(v);
v.finish();
os << '}' << std::endl;
diff --git a/src/ltlvisit/dotty.hh b/src/ltlvisit/dot.hh
similarity index 90%
rename from src/ltlvisit/dotty.hh
rename to src/ltlvisit/dot.hh
index 6f5506fc2..418970a73 100644
--- a/src/ltlvisit/dotty.hh
+++ b/src/ltlvisit/dot.hh
@@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
-// Copyright (C) 2013 Laboratoire de Recherche et Développement
+// Copyright (C) 2013, 2015 Laboratoire de Recherche et 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
@@ -37,6 +37,6 @@ namespace spot
/// \c dot is part of the GraphViz package
/// http://www.research.att.com/sw/tools/graphviz/
SPOT_API
- std::ostream& dotty(std::ostream& os, const formula* f);
+ std::ostream& print_dot_psl(std::ostream& os, const formula* f);
}
}
diff --git a/src/taalgos/Makefile.am b/src/taalgos/Makefile.am
index 5b46df075..16dca9ea1 100644
--- a/src/taalgos/Makefile.am
+++ b/src/taalgos/Makefile.am
@@ -1,5 +1,5 @@
## -*- coding: utf-8 -*-
-## Copyright (C) 2010, 2012, 2013 Laboratoire de Recherche et
+## Copyright (C) 2010, 2012, 2013, 2015 Laboratoire de Recherche et
## Développement de l'Epita (LRDE).
##
## This file is part of Spot, a model checking library.
@@ -25,7 +25,7 @@ taalgosdir = $(pkgincludedir)/taalgos
taalgos_HEADERS = \
tgba2ta.hh \
- dotty.hh \
+ dot.hh \
reachiter.hh \
stats.hh \
statessetbuilder.hh \
@@ -35,7 +35,7 @@ taalgos_HEADERS = \
noinst_LTLIBRARIES = libtaalgos.la
libtaalgos_la_SOURCES = \
tgba2ta.cc \
- dotty.cc \
+ dot.cc \
reachiter.cc \
stats.cc \
statessetbuilder.cc \
diff --git a/src/taalgos/dotty.cc b/src/taalgos/dot.cc
similarity index 98%
rename from src/taalgos/dotty.cc
rename to src/taalgos/dot.cc
index aeee34f14..a17f829fa 100644
--- a/src/taalgos/dotty.cc
+++ b/src/taalgos/dot.cc
@@ -18,7 +18,7 @@
// along with this program. If not, see .
#include
-#include "dotty.hh"
+#include "dot.hh"
#include "twa/bddprint.hh"
#include "reachiter.hh"
#include "misc/escape.hh"
@@ -234,7 +234,7 @@ namespace spot
}
std::ostream&
- dotty_reachable(std::ostream& os, const const_ta_ptr& a, const char* opt)
+ print_dot(std::ostream& os, const const_ta_ptr& a, const char* opt)
{
dotty_bfs d(os, a, opt);
d.run();
diff --git a/src/taalgos/dotty.hh b/src/taalgos/dot.hh
similarity index 94%
rename from src/taalgos/dotty.hh
rename to src/taalgos/dot.hh
index ee4a538a7..0c27dcf70 100644
--- a/src/taalgos/dotty.hh
+++ b/src/taalgos/dot.hh
@@ -25,6 +25,6 @@
namespace spot
{
SPOT_API std::ostream&
- dotty_reachable(std::ostream& os, const const_ta_ptr& a,
+ print_dot(std::ostream& os, const const_ta_ptr& a,
const char* opt = nullptr);
}
diff --git a/src/tests/checkpsl.cc b/src/tests/checkpsl.cc
index 4d7bf916e..fecda1924 100644
--- a/src/tests/checkpsl.cc
+++ b/src/tests/checkpsl.cc
@@ -28,7 +28,7 @@
#include "twaalgos/ltl2taa.hh"
#include "twaalgos/sccfilter.hh"
#include "twaalgos/product.hh"
-#include "twaalgos/dotty.hh"
+#include "twaalgos/dot.hh"
void
syntax(char* prog)
diff --git a/src/tests/checkta.cc b/src/tests/checkta.cc
index d499ea5d9..8db85bd37 100644
--- a/src/tests/checkta.cc
+++ b/src/tests/checkta.cc
@@ -31,7 +31,7 @@
#include "twaalgos/stats.hh"
#include "taalgos/minimize.hh"
#include "taalgos/tgba2ta.hh"
-#include "taalgos/dotty.hh"
+#include "taalgos/dot.hh"
#include "taalgos/stats.hh"
void
diff --git a/src/tests/complementation.cc b/src/tests/complementation.cc
index e25a7ab84..aed0a2f30 100644
--- a/src/tests/complementation.cc
+++ b/src/tests/complementation.cc
@@ -19,7 +19,7 @@
#include
#include
-#include "twaalgos/dotty.hh"
+#include "twaalgos/dot.hh"
#include "twaalgos/hoa.hh"
#include "hoaparse/public.hh"
#include "twa/twaproduct.hh"
@@ -136,7 +136,7 @@ int main(int argc, char* argv[])
if (save_hoa)
spot::hoa_reachable(std::cout, complement, nullptr);
else
- spot::dotty_reachable(std::cout, complement);
+ spot::print_dot(std::cout, complement);
}
if (print_safra)
@@ -158,7 +158,7 @@ int main(int argc, char* argv[])
spot::twa_ptr complement = 0;
complement = spot::make_safra_complement(a);
- spot::dotty_reachable(std::cout, complement);
+ spot::print_dot(std::cout, complement);
f1->destroy();
}
else if (stats)
@@ -253,7 +253,7 @@ int main(int argc, char* argv[])
return_value = 1;
if (auto run = res->accepting_run())
{
- spot::dotty_reachable(std::cout, ec->automaton());
+ spot::print_dot(std::cout, ec->automaton());
spot::print_tgba_run(std::cout, ec->automaton(), run);
}
}
diff --git a/src/tests/emptchk.cc b/src/tests/emptchk.cc
index 9a9bf9fca..6a27a06f1 100644
--- a/src/tests/emptchk.cc
+++ b/src/tests/emptchk.cc
@@ -30,7 +30,7 @@
#include "twaalgos/degen.hh"
#include "twa/twaproduct.hh"
#include "twaalgos/gtec/gtec.hh"
-#include "twaalgos/dotty.hh"
+#include "twaalgos/dot.hh"
#include "twaalgos/emptiness.hh"
void
@@ -163,7 +163,7 @@ main(int argc, char** argv)
if (auto run = res->accepting_run())
{
auto ar = spot::tgba_run_to_tgba(a, run);
- spot::dotty_reachable(std::cout, ar);
+ spot::print_dot(std::cout, ar);
}
std::cout << '\n';
if (runs == 0)
diff --git a/src/tests/ltl2tgba.cc b/src/tests/ltl2tgba.cc
index 9cee95f9d..bfd8a87ee 100644
--- a/src/tests/ltl2tgba.cc
+++ b/src/tests/ltl2tgba.cc
@@ -33,7 +33,7 @@
#include "twaalgos/ltl2tgba_fm.hh"
#include "twaalgos/ltl2taa.hh"
#include "twa/bddprint.hh"
-#include "twaalgos/dotty.hh"
+#include "twaalgos/dot.hh"
#include "twaalgos/lbtt.hh"
#include "twaalgos/hoa.hh"
#include "twaalgos/degen.hh"
@@ -69,7 +69,7 @@
#include "twaalgos/stutter.hh"
#include "taalgos/tgba2ta.hh"
-#include "taalgos/dotty.hh"
+#include "taalgos/dot.hh"
#include "taalgos/stats.hh"
std::string
@@ -1368,7 +1368,7 @@ checked_main(int argc, char** argv)
switch (output)
{
case 0:
- spot::dotty_reachable(std::cout, testing_automaton);
+ spot::print_dot(std::cout, testing_automaton);
break;
case 12:
stats_reachable(testing_automaton).dump(std::cout);
@@ -1402,7 +1402,7 @@ checked_main(int argc, char** argv)
switch (output)
{
case 0:
- spot::dotty_reachable(std::cout, std::dynamic_pointer_cast
+ spot::print_dot(std::cout, std::dynamic_pointer_cast
(a)->get_ta());
break;
case 12:
@@ -1478,19 +1478,19 @@ checked_main(int argc, char** argv)
switch (output)
{
case 0:
- spot::dotty_reachable(std::cout, a);
+ spot::print_dot(std::cout, a);
break;
case 5:
a->get_dict()->dump(std::cout);
break;
case 6:
- spot::lbtt_reachable(std::cout, a);
+ spot::print_lbtt(std::cout, a);
break;
case 8:
{
assert(degeneralize_opt == DegenSBA);
if (assume_sba)
- spot::never_claim_reachable(std::cout, a, opt_never);
+ spot::print_never_claim(std::cout, a, opt_never);
else
{
// It is possible that we have applied other
@@ -1498,7 +1498,7 @@ checked_main(int argc, char** argv)
// degeneralization. Let's degeneralize again!
auto s = spot::degeneralize(ensure_digraph(a), degen_reset,
degen_order, degen_cache);
- spot::never_claim_reachable(std::cout, s, opt_never);
+ spot::print_never_claim(std::cout, s, opt_never);
}
break;
}
@@ -1700,7 +1700,7 @@ checked_main(int argc, char** argv)
if (graph_run_tgba_opt)
{
auto ar = spot::tgba_run_to_tgba(a, run);
- spot::dotty_reachable(std::cout, ar);
+ spot::print_dot(std::cout, ar);
}
else
{
diff --git a/src/tests/ltlprod.cc b/src/tests/ltlprod.cc
index 152accc02..ede56f587 100644
--- a/src/tests/ltlprod.cc
+++ b/src/tests/ltlprod.cc
@@ -27,7 +27,7 @@
#include "ltlparse/public.hh"
#include "twaalgos/product.hh"
#include "twaalgos/ltl2tgba_fm.hh"
-#include "twaalgos/dotty.hh"
+#include "twaalgos/dot.hh"
void
syntax(char* prog)
@@ -65,7 +65,7 @@ main(int argc, char** argv)
auto a2 = spot::ltl_to_tgba_fm(f2, dict);
f1->destroy();
f2->destroy();
- spot::dotty_reachable(std::cout, product(a1, a2));
+ spot::print_dot(std::cout, product(a1, a2));
}
}
assert(spot::ltl::atomic_prop::instance_count() == 0);
diff --git a/src/tests/randtgba.cc b/src/tests/randtgba.cc
index 93159b90a..0dfb7d3d2 100644
--- a/src/tests/randtgba.cc
+++ b/src/tests/randtgba.cc
@@ -40,7 +40,7 @@
#include "twaalgos/hoa.hh"
#include "twaalgos/stats.hh"
#include "ltlenv/defaultenv.hh"
-#include "twaalgos/dotty.hh"
+#include "twaalgos/dot.hh"
#include "misc/random.hh"
#include "misc/optionmap.hh"
#include "twaalgos/degen.hh"
@@ -919,7 +919,7 @@ main(int argc, char** argv)
if (opt_dot)
{
- dotty_reachable(std::cout, a);
+ print_dot(std::cout, a);
}
if (!opt_ec)
{
diff --git a/src/tests/readltl.cc b/src/tests/readltl.cc
index 6ba27277b..ddc4ec585 100644
--- a/src/tests/readltl.cc
+++ b/src/tests/readltl.cc
@@ -26,7 +26,7 @@
#include
#include "ltlparse/public.hh"
#include "ltlvisit/dump.hh"
-#include "ltlvisit/dotty.hh"
+#include "ltlvisit/dot.hh"
#include "ltlast/allnodes.hh"
void
@@ -87,7 +87,7 @@ main(int argc, char** argv)
dump_instances("before");
#ifdef DOTTY
- spot::ltl::dotty(std::cout, f);
+ spot::ltl::print_dot_psl(std::cout, f);
#else
spot::ltl::dump(std::cout, f);
std::cout << std::endl;
@@ -105,6 +105,7 @@ main(int argc, char** argv)
assert(spot::ltl::atomic_prop::instance_count() == 0);
assert(spot::ltl::unop::instance_count() == 0);
assert(spot::ltl::binop::instance_count() == 0);
+ assert(spot::ltl::bunop::instance_count() == 0);
assert(spot::ltl::multop::instance_count() == 0);
return exit_code;
}
diff --git a/src/tests/taatgba.cc b/src/tests/taatgba.cc
index 5317131d5..88fb8d06f 100644
--- a/src/tests/taatgba.cc
+++ b/src/tests/taatgba.cc
@@ -22,7 +22,7 @@
#include "misc/hash.hh"
#include "ltlenv/defaultenv.hh"
#include "ltlast/allnodes.hh"
-#include "twaalgos/dotty.hh"
+#include "twaalgos/dot.hh"
#include "twa/taatgba.hh"
int
@@ -46,7 +46,7 @@ main()
a->add_condition(t3, e.require("c"));
a->set_init_state("state 1");
- spot::dotty_reachable(std::cout, a);
+ spot::print_dot(std::cout, a);
}
assert(spot::ltl::atomic_prop::instance_count() == 0);
diff --git a/src/tests/twagraph.cc b/src/tests/twagraph.cc
index 1f53f166d..ddea8f195 100644
--- a/src/tests/twagraph.cc
+++ b/src/tests/twagraph.cc
@@ -20,7 +20,7 @@
#include
#include "twa/twagraph.hh"
-#include "twaalgos/dotty.hh"
+#include "twaalgos/dot.hh"
#include "ltlenv/defaultenv.hh"
void f1()
@@ -50,7 +50,7 @@ void f1()
tg->new_transition(s3, s2, p1 >> p2, 0U);
tg->new_transition(s3, s3, bddtrue, tg->acc().marks({0, 1}));
- spot::dotty_reachable(std::cout, tg);
+ spot::print_dot(std::cout, tg);
{
auto i = tg->get_graph().out_iteraser(s3);
@@ -58,14 +58,14 @@ void f1()
i.erase();
i.erase();
assert(!i);
- spot::dotty_reachable(std::cout, tg);
+ spot::print_dot(std::cout, tg);
}
{
auto i = tg->get_graph().out_iteraser(s3);
i.erase();
assert(!i);
- spot::dotty_reachable(std::cout, tg);
+ spot::print_dot(std::cout, tg);
}
auto all = tg->acc().marks({0, 1});
@@ -76,9 +76,9 @@ void f1()
std::cerr << tg->num_transitions() << '\n';
assert(tg->num_transitions() == 7);
- spot::dotty_reachable(std::cout, tg);
+ spot::print_dot(std::cout, tg);
tg->merge_transitions();
- spot::dotty_reachable(std::cout, tg);
+ spot::print_dot(std::cout, tg);
std::cerr << tg->num_transitions() << '\n';
assert(tg->num_transitions() == 5);
@@ -86,7 +86,7 @@ void f1()
// Add enough states so that the state vector is reallocated.
for (unsigned i = 0; i < 100; ++i)
tg->new_state();
- spot::dotty_reachable(std::cout, tg);
+ spot::print_dot(std::cout, tg);
}
int main()
diff --git a/src/twa/twa.hh b/src/twa/twa.hh
index 4efee483f..18492cb94 100644
--- a/src/twa/twa.hh
+++ b/src/twa/twa.hh
@@ -608,7 +608,7 @@ namespace spot
/// Implementing this method is optional; the default annotation
/// is the empty string.
///
- /// This method is used for instance in dotty_reachable(),
+ /// This method is used for instance in print_dot(),
/// and replay_tgba_run().
///
/// \param t a non-done twa_succ_iterator for this automaton
diff --git a/src/twa/twasafracomplement.cc b/src/twa/twasafracomplement.cc
index 3c28d0f88..ab842beae 100644
--- a/src/twa/twasafracomplement.cc
+++ b/src/twa/twasafracomplement.cc
@@ -32,7 +32,7 @@
#include "misc/hashfunc.hh"
#include "ltlast/formula.hh"
#include "ltlast/constant.hh"
-#include "twaalgos/dotty.hh"
+#include "twaalgos/dot.hh"
#include "twa/twasafracomplement.hh"
#include "twaalgos/degen.hh"
diff --git a/src/twaalgos/Makefile.am b/src/twaalgos/Makefile.am
index b7c51bdd3..fdae1e5c1 100644
--- a/src/twaalgos/Makefile.am
+++ b/src/twaalgos/Makefile.am
@@ -37,7 +37,7 @@ twaalgos_HEADERS = \
cycles.hh \
dtgbacomp.hh \
degen.hh \
- dotty.hh \
+ dot.hh \
dtbasat.hh \
dtgbasat.hh \
dupexp.hh \
@@ -95,7 +95,7 @@ libtwaalgos_la_SOURCES = \
cycles.cc \
dtgbacomp.cc \
degen.cc \
- dotty.cc \
+ dot.cc \
dtbasat.cc \
dtgbasat.cc \
dupexp.cc \
diff --git a/src/twaalgos/dotty.cc b/src/twaalgos/dot.cc
similarity index 99%
rename from src/twaalgos/dotty.cc
rename to src/twaalgos/dot.cc
index 0737f1d4a..15e2ee4bf 100644
--- a/src/twaalgos/dotty.cc
+++ b/src/twaalgos/dot.cc
@@ -23,7 +23,7 @@
#include
#include
#include "twa/twagraph.hh"
-#include "dotty.hh"
+#include "dot.hh"
#include "twa/bddprint.hh"
#include "reachiter.hh"
#include "misc/escape.hh"
@@ -528,7 +528,7 @@ namespace spot
} // anonymous namespace
std::ostream&
- dotty_reachable(std::ostream& os, const const_twa_ptr& g,
+ print_dot(std::ostream& os, const const_twa_ptr& g,
const char* options)
{
dotty_output d(os, options);
diff --git a/src/twaalgos/dotty.hh b/src/twaalgos/dot.hh
similarity index 98%
rename from src/twaalgos/dotty.hh
rename to src/twaalgos/dot.hh
index c62cdea96..df128ff0d 100644
--- a/src/twaalgos/dotty.hh
+++ b/src/twaalgos/dot.hh
@@ -41,7 +41,7 @@ namespace spot
/// automaton, 'n' shows the name, 'c' uses circle-shaped states,
/// 'a' shows the acceptance.
SPOT_API std::ostream&
- dotty_reachable(std::ostream& os,
+ print_dot(std::ostream& os,
const const_twa_ptr& g,
const char* options = nullptr);
}
diff --git a/src/twaalgos/dtbasat.cc b/src/twaalgos/dtbasat.cc
index 91a117b96..6584f2130 100644
--- a/src/twaalgos/dtbasat.cc
+++ b/src/twaalgos/dtbasat.cc
@@ -29,7 +29,7 @@
#include "stats.hh"
#include "misc/satsolver.hh"
#include "misc/timer.hh"
-#include "dotty.hh"
+#include "dot.hh"
// If you set the SPOT_TMPKEEP environment variable the temporary
// file used to communicate with the sat solver will be left in
@@ -800,7 +800,7 @@ namespace spot
}
static bool show = getenv("SPOT_SATSHOW");
if (show && res)
- dotty_reachable(std::cout, res);
+ print_dot(std::cout, res);
trace << "dtba_sat_synthetize(...) = " << res << '\n';
return res;
diff --git a/src/twaalgos/dtgbasat.cc b/src/twaalgos/dtgbasat.cc
index 87cbc6a8d..67a930164 100644
--- a/src/twaalgos/dtgbasat.cc
+++ b/src/twaalgos/dtgbasat.cc
@@ -33,7 +33,7 @@
#include "misc/timer.hh"
#include "isweakscc.hh"
#include "isdet.hh"
-#include "dotty.hh"
+#include "dot.hh"
#include "complete.hh"
#include "misc/optionmap.hh"
#include "dtbasat.hh"
@@ -1147,7 +1147,7 @@ namespace spot
}
static bool show = getenv("SPOT_SATSHOW");
if (show && res)
- dotty_reachable(std::cout, res);
+ print_dot(std::cout, res);
trace << "dtgba_sat_synthetize(...) = " << res << '\n';
return res;
diff --git a/src/twaalgos/dupexp.cc b/src/twaalgos/dupexp.cc
index b4c6867c6..6f580ce70 100644
--- a/src/twaalgos/dupexp.cc
+++ b/src/twaalgos/dupexp.cc
@@ -26,7 +26,7 @@
#include
#include