From 20365e53f0fbccb0e98eee236a7b640875923deb Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 2 Oct 2015 11:00:00 +0200 Subject: [PATCH] Enable -Wmissing-declarations in development mode. * m4/gccwarn.m4: Add -Wmissing-declarations. * iface/ltsmin/ltsmin.cc, iface/ltsmin/modelcheck.cc, src/bin/common_trans.cc, src/bin/genltl.cc, src/bin/ltlgrind.cc, src/tests/acc.cc, src/tests/bitvect.cc, src/tests/checkpsl.cc, src/tests/checkta.cc, src/tests/complementation.cc, src/tests/consterm.cc, src/tests/emptchk.cc, src/tests/equalsf.cc, src/tests/graph.cc, src/tests/ikwiad.cc, src/tests/intvcmp2.cc, src/tests/intvcomp.cc, src/tests/kind.cc, src/tests/length.cc, src/tests/ltlprod.cc, src/tests/ltlrel.cc, src/tests/ngraph.cc, src/tests/randtgba.cc, src/tests/readltl.cc, src/tests/reduc.cc, src/tests/syntimpl.cc, src/tests/tostring.cc, src/tests/twagraph.cc, src/tl/contain.cc, src/twaalgos/dtgbacomp.cc, src/twaalgos/minimize.cc: Add "static" and move in anonymous namespace when appropriate. --- iface/ltsmin/ltsmin.cc | 120 ++++---- iface/ltsmin/modelcheck.cc | 2 +- m4/gccwarn.m4 | 3 +- src/bin/common_trans.cc | 2 +- src/bin/genltl.cc | 3 +- src/bin/ltlgrind.cc | 2 +- src/tests/acc.cc | 4 +- src/tests/bitvect.cc | 2 +- src/tests/checkpsl.cc | 2 +- src/tests/checkta.cc | 8 +- src/tests/complementation.cc | 2 +- src/tests/consterm.cc | 2 +- src/tests/emptchk.cc | 2 +- src/tests/equalsf.cc | 2 +- src/tests/graph.cc | 29 +- src/tests/ikwiad.cc | 25 +- src/tests/intvcmp2.cc | 8 +- src/tests/intvcomp.cc | 16 +- src/tests/kind.cc | 2 +- src/tests/length.cc | 2 +- src/tests/ltlprod.cc | 2 +- src/tests/ltlrel.cc | 2 +- src/tests/ngraph.cc | 22 +- src/tests/randtgba.cc | 20 +- src/tests/readltl.cc | 2 +- src/tests/reduc.cc | 2 +- src/tests/syntimpl.cc | 2 +- src/tests/tostring.cc | 2 +- src/tests/twagraph.cc | 2 +- src/tl/contain.cc | 13 - src/twaalgos/dtgbacomp.cc | 257 ++++++++-------- src/twaalgos/minimize.cc | 552 +++++++++++++++++------------------ 32 files changed, 553 insertions(+), 563 deletions(-) diff --git a/iface/ltsmin/ltsmin.cc b/iface/ltsmin/ltsmin.cc index f5f381f67..063848dbf 100644 --- a/iface/ltsmin/ltsmin.cc +++ b/iface/ltsmin/ltsmin.cc @@ -943,75 +943,75 @@ namespace spot mutable callback_context* state_condition_last_cc_; }; - } + + ////////////////////////////////////////////////////////////////////////// + // LOADER - //////////////////////////////////////////////////////////////////////////// - // LOADER + // Call spins to compile "foo.prom" as "foo.prom.spins" if the latter + // does not exist already or is older. + static bool + compile_model(std::string& filename, std::string& ext, bool verbose) + { + std::string command; + std::string compiled_ext; + if (ext == ".prom" || ext == ".pm" || ext == ".pml") + { + command = "spins " + filename; + compiled_ext = ".spins"; + } + else if (ext == ".dve") + { + command = "divine compile --ltsmin " + filename; + compiled_ext = "2C"; + } + else + { + if (verbose) + std::cerr << "Unknown extension `" << ext + << ("'. Use `.prom', `.pm', `.pml', `.dve', `.dve2C' or" + "`.prom.spins'.") << std::endl; + return false; + } - // Call spins to compile "foo.prom" as "foo.prom.spins" if the latter - // does not exist already or is older. - bool - compile_model(std::string& filename, std::string& ext, bool verbose) - { - std::string command; - std::string compiled_ext; + struct stat s; + if (stat(filename.c_str(), &s) != 0) + { + if (verbose) + { + std::cerr << "Cannot open " << filename << std::endl; + return true; + } + } - if (ext == ".prom" || ext == ".pm" || ext == ".pml") - { - command = "spins " + filename; - compiled_ext = ".spins"; - } - else if (ext == ".dve") - { - command = "divine compile --ltsmin " + filename; - compiled_ext = "2C"; - } - else - { - if (verbose) - std::cerr << "Unknown extension `" << ext - << "'. Use `.prom', `.pm', `.pml', `.dve', `.dve2C' or"\ - "`.prom.spins'." << std::endl; - return false; - } + std::string old = filename; + filename += compiled_ext; - struct stat s; - if (stat(filename.c_str(), &s) != 0) - { - if (verbose) - { - std::cerr << "Cannot open " << filename << std::endl; - return true; - } - } + // Remove any directory, because the new file will + // be compiled in the current directory. + size_t pos = filename.find_last_of("/\\"); + if (pos != std::string::npos) + filename = "./" + filename.substr(pos + 1); - std::string old = filename; - filename += compiled_ext; + struct stat d; + if (stat(filename.c_str(), &d) == 0) + if (s.st_mtime < d.st_mtime) + // The .spins or .dve2C is up-to-date, no need to recompile it. + return false; - // Remove any directory, because the new file will - // be compiled in the current directory. - size_t pos = filename.find_last_of("/\\"); - if (pos != std::string::npos) - filename = "./" + filename.substr(pos + 1); + int res = system(command.c_str()); + if (res) + { + if (verbose) + std::cerr << "Execution of `" << command.c_str() + << "' returned exit code " << WEXITSTATUS(res) + << ".\n"; + return true; + } + return false; + } - struct stat d; - if (stat(filename.c_str(), &d) == 0) - if (s.st_mtime < d.st_mtime) - // The .spins or .dve2C is up-to-date, no need to recompile it. - return false; - - int res = system(command.c_str()); - if (res) - { - if (verbose) - std::cerr << "Execution of `" << command.c_str() - << "' returned exit code " << WEXITSTATUS(res) - << ".\n"; - return true; - } - return false; } kripke_ptr diff --git a/iface/ltsmin/modelcheck.cc b/iface/ltsmin/modelcheck.cc index 19e7683fa..749c8620c 100644 --- a/iface/ltsmin/modelcheck.cc +++ b/iface/ltsmin/modelcheck.cc @@ -60,7 +60,7 @@ Options:\n\ exit(1); } -int +static int checked_main(int argc, char **argv) { spot::timer_map tm; diff --git a/m4/gccwarn.m4 b/m4/gccwarn.m4 index d2c53a840..b3792e8ad 100644 --- a/m4/gccwarn.m4 +++ b/m4/gccwarn.m4 @@ -32,7 +32,8 @@ EOF Wpointer-arith \ Wwrite-strings \ Wcast-qual \ - Wdocumentation + Wdocumentation \ + Wmissing-declarations do CXXFLAGS="$cf_save_CXXFLAGS $ac_cv_prog_gxx_warn_flags -$cf_opt" if AC_TRY_EVAL(ac_compile); then diff --git a/src/bin/common_trans.cc b/src/bin/common_trans.cc index 0dfa5944c..84eb35064 100644 --- a/src/bin/common_trans.cc +++ b/src/bin/common_trans.cc @@ -48,7 +48,7 @@ static struct shorthands_t { "spin", " -f %s>%O" }, }; -void show_shorthands() +static void show_shorthands() { std::cout << ("If a COMMANDFMT does not use any %-sequence, and starts with one of\n" diff --git a/src/bin/genltl.cc b/src/bin/genltl.cc index d75f3065d..16eb65f5a 100644 --- a/src/bin/genltl.cc +++ b/src/bin/genltl.cc @@ -321,7 +321,8 @@ phi_n(std::string name, int n) return result; } -formula N_n(std::string name, int n) +static formula +N_n(std::string name, int n) { return formula::F(phi_n(name, n)); } diff --git a/src/bin/ltlgrind.cc b/src/bin/ltlgrind.cc index 83bcfa03a..4415b63f6 100644 --- a/src/bin/ltlgrind.cc +++ b/src/bin/ltlgrind.cc @@ -108,7 +108,7 @@ namespace }; } -int +static int parse_opt(int key, char* arg, struct argp_state*) { switch (key) diff --git a/src/tests/acc.cc b/src/tests/acc.cc index c9672ffe4..eda001656 100644 --- a/src/tests/acc.cc +++ b/src/tests/acc.cc @@ -24,7 +24,7 @@ #include #include "twa/acc.hh" -void check(spot::acc_cond& ac, spot::acc_cond::mark_t m) +static void check(spot::acc_cond& ac, spot::acc_cond::mark_t m) { std::cout << '#' << m.count() << ": " << ac.format(m); if (!m) @@ -34,7 +34,7 @@ void check(spot::acc_cond& ac, spot::acc_cond::mark_t m) std::cout << '\n'; } -void print(const std::vector>& res) +static void print(const std::vector>& res) { for (auto& v: res) { diff --git a/src/tests/bitvect.cc b/src/tests/bitvect.cc index 46f31e9b6..3abd556f0 100644 --- a/src/tests/bitvect.cc +++ b/src/tests/bitvect.cc @@ -20,7 +20,7 @@ #include #include "misc/bitvect.hh" -void ruler() +static void ruler() { std::cout << "\n "; for (size_t x = 0; x < 76; ++x) diff --git a/src/tests/checkpsl.cc b/src/tests/checkpsl.cc index ac4350a16..b0432813d 100644 --- a/src/tests/checkpsl.cc +++ b/src/tests/checkpsl.cc @@ -29,7 +29,7 @@ #include "twaalgos/product.hh" #include "twaalgos/dot.hh" -void +static void syntax(char* prog) { std::cerr << prog << " file" << std::endl; diff --git a/src/tests/checkta.cc b/src/tests/checkta.cc index cf912bf6d..b973756e2 100644 --- a/src/tests/checkta.cc +++ b/src/tests/checkta.cc @@ -33,14 +33,15 @@ #include "taalgos/dot.hh" #include "taalgos/stats.hh" -void +static void syntax(char* prog) { std::cerr << prog << " file" << std::endl; exit(2); } -void stats(std::string title, const spot::ta_ptr& ta) +static void +stats(std::string title, const spot::ta_ptr& ta) { auto s = stats_reachable(ta); @@ -50,7 +51,8 @@ void stats(std::string title, const spot::ta_ptr& ta) << std::setw(6) << s.acceptance_states << '\n'; } -void stats(std::string title, const spot::twa_ptr& tg) +static void +stats(std::string title, const spot::twa_ptr& tg) { auto s = stats_reachable(tg); diff --git a/src/tests/complementation.cc b/src/tests/complementation.cc index ef051dea0..09568f917 100644 --- a/src/tests/complementation.cc +++ b/src/tests/complementation.cc @@ -34,7 +34,7 @@ #include "twa/twasafracomplement.hh" -void usage(const char* prog) +static void usage(const char* prog) { std::cout << "usage: " << prog << " [options]" << std::endl; std::cout << "with options" << std::endl diff --git a/src/tests/consterm.cc b/src/tests/consterm.cc index fdc666657..a8fca3dfe 100644 --- a/src/tests/consterm.cc +++ b/src/tests/consterm.cc @@ -24,7 +24,7 @@ #include #include "tl/parse.hh" -void +static void syntax(char *prog) { std::cerr << prog << " formula" << std::endl; diff --git a/src/tests/emptchk.cc b/src/tests/emptchk.cc index 8d55c843a..c75372ffd 100644 --- a/src/tests/emptchk.cc +++ b/src/tests/emptchk.cc @@ -32,7 +32,7 @@ #include "twaalgos/dot.hh" #include "twaalgos/emptiness.hh" -void +static void syntax(char* prog) { std::cerr << prog << " file" << std::endl; diff --git a/src/tests/equalsf.cc b/src/tests/equalsf.cc index e5878de3f..31ece43d3 100644 --- a/src/tests/equalsf.cc +++ b/src/tests/equalsf.cc @@ -32,7 +32,7 @@ #include "tl/simplify.hh" #include "tl/print.hh" -void +static void syntax(char* prog) { std::cerr << prog << " [-E] file" << std::endl; diff --git a/src/tests/graph.cc b/src/tests/graph.cc index f823497a5..8661a796f 100644 --- a/src/tests/graph.cc +++ b/src/tests/graph.cc @@ -70,8 +70,9 @@ dot(std::ostream& out, spot::digraph& g) } -bool g1(const spot::digraph& g, - unsigned s, int e) +static bool +g1(const spot::digraph& g, + unsigned s, int e) { int f = 0; for (auto& t: g.out(s)) @@ -82,7 +83,8 @@ bool g1(const spot::digraph& g, return f == e; } -bool f1() +static bool +f1() { spot::digraph g(3); @@ -111,7 +113,8 @@ bool f1() } -bool f2() +static bool +f2() { spot::digraph g(3); @@ -133,7 +136,8 @@ bool f2() return f == 5; } -bool f3() +static bool +f3() { spot::digraph g(3); @@ -155,7 +159,8 @@ bool f3() return f == 3 && g.states().size() == 3; } -bool f4() +static bool +f4() { spot::digraph g(3); @@ -177,7 +182,8 @@ bool f4() return f == 11; } -bool f5() +static bool +f5() { spot::digraph> g(3); @@ -199,7 +205,8 @@ bool f5() return f == 3 && (h > 2.49 && h < 2.51); } -bool f6() +static bool +f6() { spot::digraph> g(3); @@ -221,7 +228,8 @@ bool f6() return f == 3 && (h > 2.49 && h < 2.51); } -bool f7() +static bool +f7() { spot::digraph g(3); auto s1 = g.new_state(2); @@ -267,7 +275,8 @@ struct int_pair #endif }; -bool f8() +static bool +f8() { spot::digraph g(3); auto s1 = g.new_state(2, 4); diff --git a/src/tests/ikwiad.cc b/src/tests/ikwiad.cc index 982992f7b..ebd7e3041 100644 --- a/src/tests/ikwiad.cc +++ b/src/tests/ikwiad.cc @@ -71,25 +71,7 @@ #include "taalgos/dot.hh" #include "taalgos/stats.hh" -std::string -ltl_defs() -{ - std::string s = "\ -X=(0 1 true \ - 1 2 $0 \ - accept 2) \ -U=(0 0 $0 \ - 0 1 $1 \ - accept 1) \ -G=(0 0 $0) \ -F=U(true, $0) \ -W=G($0)|U($0, $1) \ -R=!U(!$0, !$1) \ -M=F($0)&R($0, $1)"; - return s; -} - -void +static void syntax(char* prog) { // Display the supplied name unless it appears to be a libtool wrapper. @@ -304,7 +286,8 @@ to_int(const char* s) return res; } -spot::twa_graph_ptr ensure_digraph(const spot::twa_ptr& a) +static spot::twa_graph_ptr +ensure_digraph(const spot::twa_ptr& a) { auto aa = std::dynamic_pointer_cast(a); if (aa) @@ -312,7 +295,7 @@ spot::twa_graph_ptr ensure_digraph(const spot::twa_ptr& a) return spot::make_twa_graph(a, spot::twa::prop_set::all()); } -int +static int checked_main(int argc, char** argv) { int exit_code = 0; diff --git a/src/tests/intvcmp2.cc b/src/tests/intvcmp2.cc index 6e6e821b5..9cf453216 100644 --- a/src/tests/intvcmp2.cc +++ b/src/tests/intvcmp2.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2014 Laboratoire de Recherche et Developpement +// Copyright (C) 2011, 2014, 2015 Laboratoire de Recherche et Developpement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -22,7 +22,8 @@ #include -int check_aa(int* data, int size, unsigned expected = 0) +static int +check_aa(int* data, int size, unsigned expected = 0) { int* comp = new int[size * 2]; size_t csize = size * 2; @@ -67,7 +68,8 @@ int check_aa(int* data, int size, unsigned expected = 0) return !!res; } -int check(int* comp, int size, unsigned expected = 0) +static int +check(int* comp, int size, unsigned expected = 0) { return //check_vv(comp, size, expected) + diff --git a/src/tests/intvcomp.cc b/src/tests/intvcomp.cc index 7c66efb9a..3f0205b8b 100644 --- a/src/tests/intvcomp.cc +++ b/src/tests/intvcomp.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2014 Laboratoire de Recherche et Developpement -// de l'Epita (LRDE). +// Copyright (C) 2011, 2014, 2015 Laboratoire de Recherche et +// Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -21,7 +21,8 @@ #include "misc/intvcomp.hh" #include -int check_vv(int* data, int size, unsigned expected = 0) +static int +check_vv(int* data, int size, unsigned expected = 0) { std::vector input; @@ -69,7 +70,8 @@ int check_vv(int* data, int size, unsigned expected = 0) return !!res; } -int check_av(int* data, int size, unsigned expected = 0) +static int +check_av(int* data, int size, unsigned expected = 0) { const std::vector* v = spot::int_array_vector_compress(data, size); @@ -113,7 +115,8 @@ int check_av(int* data, int size, unsigned expected = 0) return !!res; } -int check_aa(int* data, int size, unsigned expected = 0) +static int +check_aa(int* data, int size, unsigned expected = 0) { int* comp = new int[size *2]; size_t csize = size * 2; @@ -158,7 +161,8 @@ int check_aa(int* data, int size, unsigned expected = 0) return !!res; } -int check(int* comp, int size, unsigned expected = 0) +static int +check(int* comp, int size, unsigned expected = 0) { return check_vv(comp, size, expected) + diff --git a/src/tests/kind.cc b/src/tests/kind.cc index d0eef6ab2..d628bf9ac 100644 --- a/src/tests/kind.cc +++ b/src/tests/kind.cc @@ -24,7 +24,7 @@ #include #include "tl/parse.hh" -void +static void syntax(char *prog) { std::cerr << prog << " formula" << std::endl; diff --git a/src/tests/length.cc b/src/tests/length.cc index 28d438eb0..7f367ca16 100644 --- a/src/tests/length.cc +++ b/src/tests/length.cc @@ -24,7 +24,7 @@ #include "tl/parse.hh" #include "tl/length.hh" -void +static void syntax(char *prog) { std::cerr << prog << " formula" << std::endl; diff --git a/src/tests/ltlprod.cc b/src/tests/ltlprod.cc index bdeaaf60d..b981763cb 100644 --- a/src/tests/ltlprod.cc +++ b/src/tests/ltlprod.cc @@ -28,7 +28,7 @@ #include "twaalgos/ltl2tgba_fm.hh" #include "twaalgos/dot.hh" -void +static void syntax(char* prog) { std::cerr << prog << " formula1 formula2" << std::endl; diff --git a/src/tests/ltlrel.cc b/src/tests/ltlrel.cc index dc5c8a1b5..9bd5c06e0 100644 --- a/src/tests/ltlrel.cc +++ b/src/tests/ltlrel.cc @@ -24,7 +24,7 @@ #include "tl/relabel.hh" #include "tl/print.hh" -void +static void syntax(char *prog) { std::cerr << prog << " formula" << std::endl; diff --git a/src/tests/ngraph.cc b/src/tests/ngraph.cc index d718a9a3b..cee07fba3 100644 --- a/src/tests/ngraph.cc +++ b/src/tests/ngraph.cc @@ -108,8 +108,8 @@ dot(std::ostream& out, const spot::named_graph& g) } -bool g1(const spot::digraph& g, - unsigned s, int e) +static bool +g1(const spot::digraph& g, unsigned s, int e) { int f = 0; for (auto& t: g.out(s)) @@ -120,7 +120,7 @@ bool g1(const spot::digraph& g, return f == e; } -bool f1() +static bool f1() { spot::digraph g(3); spot::named_graph, std::string> gg(g); @@ -150,7 +150,7 @@ bool f1() } -bool f2() +static bool f2() { spot::digraph g(3); spot::named_graph, std::string> gg(g); @@ -173,7 +173,7 @@ bool f2() return f == 5; } -bool f3() +static bool f3() { spot::digraph g(3); spot::named_graph, std::string> gg(g); @@ -196,7 +196,7 @@ bool f3() return f == 3 && g.states().size() == 3; } -bool f4() +static bool f4() { spot::digraph g(3); spot::named_graph, std::string> gg(g); @@ -219,7 +219,7 @@ bool f4() return f == 11; } -bool f5() +static bool f5() { typedef spot::digraph> graph_t; graph_t g(3); @@ -243,7 +243,7 @@ bool f5() return f == 3 && (h > 2.49 && h < 2.51); } -bool f6() +static bool f6() { typedef spot::digraph> graph_t; graph_t g(3); @@ -267,7 +267,7 @@ bool f6() return f == 3 && (h > 2.49 && h < 2.51); } -bool f7() +static bool f7() { typedef spot::digraph graph_t; graph_t g(3); @@ -316,7 +316,7 @@ struct int_pair #endif }; -bool f8() +static bool f8() { typedef spot::digraph graph_t; graph_t g(3); @@ -382,7 +382,7 @@ public: } }; -bool f9() +static bool f9() { typedef spot::digraph graph_t; graph_t g(3); diff --git a/src/tests/randtgba.cc b/src/tests/randtgba.cc index 613d96fe9..b1ebd5807 100644 --- a/src/tests/randtgba.cc +++ b/src/tests/randtgba.cc @@ -82,7 +82,7 @@ const char* default_algos[] = { std::vector ec_algos; -spot::emptiness_check_ptr +static spot::emptiness_check_ptr cons_emptiness_check(int num, spot::const_twa_graph_ptr a, const spot::const_twa_graph_ptr& degen, unsigned int n_acc) @@ -96,7 +96,7 @@ cons_emptiness_check(int num, spot::const_twa_graph_ptr a, return nullptr; } -void +static void syntax(char* prog) { std::cerr << "Usage: "<< prog << " [OPTIONS...] PROPS..." << std::endl @@ -173,7 +173,7 @@ syntax(char* prog) } -int +static int to_int(const char* s) { char* endptr; @@ -186,7 +186,7 @@ to_int(const char* s) return res; } -int +static int to_int_pos(const char* s, const char* arg) { int res = to_int(s); @@ -199,7 +199,7 @@ to_int_pos(const char* s, const char* arg) return res; } -int +static int to_int_nonneg(const char* s, const char* arg) { int res = to_int(s); @@ -212,7 +212,7 @@ to_int_nonneg(const char* s, const char* arg) return res; } -float +static float to_float(const char* s) { char* endptr; @@ -226,7 +226,7 @@ to_float(const char* s) return res; } -float +static float to_float_nonneg(const char* s, const char* arg) { float res = to_float(s); @@ -250,7 +250,7 @@ id(const char*, unsigned x) spot::tgba_statistics prod_stats; -float +static float prod_conv(const char* name, unsigned x) { float y = static_cast(x); @@ -418,7 +418,7 @@ ar_stats_type ar_stats; // Statistics about accepting runs. ar_stats_type mar_stats; // ... about minimized accepting runs. -void +static void print_ar_stats(ar_stats_type& ar_stats, const std::string& s) { std::ios::fmtflags old = std::cout.flags(); @@ -486,7 +486,7 @@ print_ar_stats(ar_stats_type& ar_stats, const std::string& s) std::cout << std::setiosflags(old); } -spot::formula +static spot::formula generate_formula(const spot::random_ltl& rl, spot::ltl_simplifier& simp, int opt_f, int opt_s, diff --git a/src/tests/readltl.cc b/src/tests/readltl.cc index cfabb0bea..303bb5bee 100644 --- a/src/tests/readltl.cc +++ b/src/tests/readltl.cc @@ -27,7 +27,7 @@ #include "tl/parse.hh" #include "tl/dot.hh" -void +static void syntax(char* prog) { std::cerr << prog << " [-d] formula" << std::endl; diff --git a/src/tests/reduc.cc b/src/tests/reduc.cc index be847d674..08659418c 100644 --- a/src/tests/reduc.cc +++ b/src/tests/reduc.cc @@ -31,7 +31,7 @@ #include "tl/simplify.hh" #include "tl/length.hh" -void +static void syntax(char* prog) { std::cerr << prog << " option formula1 (formula2)?" << std::endl; diff --git a/src/tests/syntimpl.cc b/src/tests/syntimpl.cc index 52d49cac7..e99aa44b9 100644 --- a/src/tests/syntimpl.cc +++ b/src/tests/syntimpl.cc @@ -28,7 +28,7 @@ #include "tl/simplify.hh" #include "tl/nenoform.hh" -void +static void syntax(char* prog) { std::cerr << prog << " formula1 formula2?" << std::endl; diff --git a/src/tests/tostring.cc b/src/tests/tostring.cc index 2c56dadb6..3e4c8ab85 100644 --- a/src/tests/tostring.cc +++ b/src/tests/tostring.cc @@ -26,7 +26,7 @@ #include "tl/parse.hh" #include "tl/print.hh" -void +static void syntax(char *prog) { std::cerr << prog << " formula1" << std::endl; diff --git a/src/tests/twagraph.cc b/src/tests/twagraph.cc index c4261faed..e6f2c6e0d 100644 --- a/src/tests/twagraph.cc +++ b/src/tests/twagraph.cc @@ -23,7 +23,7 @@ #include "twaalgos/dot.hh" #include "tl/defaultenv.hh" -void f1() +static void f1() { auto d = spot::make_bdd_dict(); auto tg = make_twa_graph(d); diff --git a/src/tl/contain.cc b/src/tl/contain.cc index ca7829ad9..47db7b420 100644 --- a/src/tl/contain.cc +++ b/src/tl/contain.cc @@ -120,17 +120,4 @@ namespace spot r.translation = e; return &r; } - - - formula - reduce_tau03(formula f, bool stronger) - { - if (!f.is_psl_formula()) - return f; - - ltl_simplifier_options opt(false, false, false, - true, stronger); - ltl_simplifier simpl(opt); - return simpl.simplify(f); - } } diff --git a/src/twaalgos/dtgbacomp.cc b/src/twaalgos/dtgbacomp.cc index 8c46482b2..2c02e05c6 100644 --- a/src/twaalgos/dtgbacomp.cc +++ b/src/twaalgos/dtgbacomp.cc @@ -24,140 +24,145 @@ namespace spot { - twa_graph_ptr dtgba_complement_nonweak(const const_twa_graph_ptr& aut) + namespace { - // Clone the original automaton. - auto res = make_twa_graph(aut, - { false, // state based - false, // inherently_weak - false, // deterministic - true, // stutter inv. - }); - // Copy the old acceptance condition before we replace it. - acc_cond oldacc = aut->acc(); // Copy it! + static twa_graph_ptr + dtgba_complement_nonweak(const const_twa_graph_ptr& aut) + { + // Clone the original automaton. + auto res = make_twa_graph(aut, + { false, // state based + false, // inherently_weak + false, // deterministic + true, // stutter inv. + }); + // Copy the old acceptance condition before we replace it. + acc_cond oldacc = aut->acc(); // Copy it! - // We will modify res in place, and the resulting - // automaton will only have one acceptance set. - // This changes aut->acc(); - res->set_buchi(); - // The resulting automaton is weak. - res->prop_inherently_weak(); - res->prop_state_based_acc(); + // We will modify res in place, and the resulting + // automaton will only have one acceptance set. + // This changes aut->acc(); + res->set_buchi(); + // The resulting automaton is weak. + res->prop_inherently_weak(); + res->prop_state_based_acc(); - unsigned num_sets = oldacc.num_sets(); - unsigned n = res->num_states(); - // We will duplicate the automaton as many times as we have - // acceptance sets, and we need one extra sink state. - res->new_states(num_sets * n + 1); - unsigned sink = res->num_states() - 1; - // The sink state has an accepting self-loop. - res->new_acc_edge(sink, sink, bddtrue); + unsigned num_sets = oldacc.num_sets(); + unsigned n = res->num_states(); + // We will duplicate the automaton as many times as we have + // acceptance sets, and we need one extra sink state. + res->new_states(num_sets * n + 1); + unsigned sink = res->num_states() - 1; + // The sink state has an accepting self-loop. + res->new_acc_edge(sink, sink, bddtrue); - for (unsigned src = 0; src < n; ++src) - { - // Keep track of all conditions on edge leaving state - // SRC, so we can complete it. - bdd missingcond = bddtrue; - for (auto& t: res->out(src)) - { - if (t.dst >= n) // Ignore edges we added. - break; - missingcond -= t.cond; - acc_cond::mark_t curacc = t.acc; - // The original edge must not accept anymore. - t.acc = 0U; + for (unsigned src = 0; src < n; ++src) + { + // Keep track of all conditions on edge leaving state + // SRC, so we can complete it. + bdd missingcond = bddtrue; + for (auto& t: res->out(src)) + { + if (t.dst >= n) // Ignore edges we added. + break; + missingcond -= t.cond; + acc_cond::mark_t curacc = t.acc; + // The original edge must not accept anymore. + t.acc = 0U; - // Edge that were fully accepting are never cloned. - if (oldacc.accepting(curacc)) - continue; - // Save t.cond and t.dst as the reference to t - // is invalided by calls to new_edge(). - unsigned dst = t.dst; - bdd cond = t.cond; + // Edge that were fully accepting are never cloned. + if (oldacc.accepting(curacc)) + continue; + // Save t.cond and t.dst as the reference to t + // is invalided by calls to new_edge(). + unsigned dst = t.dst; + bdd cond = t.cond; - // Iterate over all the acceptance conditions in 'curacc', - // an duplicate it for each clone for which it does not - // belong to the acceptance set. - unsigned add = 0; - for (unsigned set = 0; set < num_sets; ++set) - { - add += n; - if (!oldacc.has(curacc, set)) - { - // Clone the edge - res->new_acc_edge(src + add, dst + add, cond); - assert(dst + add < sink); - // Using `t' is disallowed from now on as it is a - // reference to a edge that may have been - // reallocated. + // Iterate over all the acceptance conditions in 'curacc', + // an duplicate it for each clone for which it does not + // belong to the acceptance set. + unsigned add = 0; + for (unsigned set = 0; set < num_sets; ++set) + { + add += n; + if (!oldacc.has(curacc, set)) + { + // Clone the edge + res->new_acc_edge(src + add, dst + add, cond); + assert(dst + add < sink); + // Using `t' is disallowed from now on as it is a + // reference to a edge that may have been + // reallocated. - // At least one edge per cycle should have a - // nondeterministic copy from the original clone. - // We use state numbers to select it, as any cycle - // is guaranteed to have at least one edge - // with dst <= src. FIXME: Computing a feedback - // arc set would be better. - if (dst <= src) - res->new_edge(src, dst + add, cond); - } - } - assert(add == num_sets * n); - } - // Complete the original automaton. - if (missingcond != bddfalse) - res->new_edge(src, sink, missingcond); - } - res->merge_edges(); - res->purge_dead_states(); - return res; - } - - twa_graph_ptr dtgba_complement_weak(const const_twa_graph_ptr& aut) - { - // Clone the original automaton. - auto res = make_twa_graph(aut, - { true, // state based - true, // inherently weak - true, // determinisitic - true, // stutter inv. - }); - scc_info si(res); - - // We will modify res in place, and the resulting - // automaton will only have one acceptance set. - acc_cond::mark_t all_acc = res->set_buchi(); - res->prop_state_based_acc(); - - unsigned sink = res->num_states(); - - for (unsigned src = 0; src < sink; ++src) - { - acc_cond::mark_t acc = 0U; - unsigned scc = si.scc_of(src); - if (si.is_rejecting_scc(scc) && !si.is_trivial(scc)) - acc = all_acc; - - // Keep track of all conditions on edge leaving state - // SRC, so we can complete it. - bdd missingcond = bddtrue; - for (auto& t: res->out(src)) - { - missingcond -= t.cond; - t.acc = acc; - } - // Complete the original automaton. - if (missingcond != bddfalse) - { - if (res->num_states() == sink) - { - res->new_state(); - res->new_acc_edge(sink, sink, bddtrue); - } + // At least one edge per cycle should have a + // nondeterministic copy from the original clone. + // We use state numbers to select it, as any cycle + // is guaranteed to have at least one edge + // with dst <= src. FIXME: Computing a feedback + // arc set would be better. + if (dst <= src) + res->new_edge(src, dst + add, cond); + } + } + assert(add == num_sets * n); + } + // Complete the original automaton. + if (missingcond != bddfalse) res->new_edge(src, sink, missingcond); - } - } - //res->merge_edges(); - return res; + } + res->merge_edges(); + res->purge_dead_states(); + return res; + } + + static twa_graph_ptr + dtgba_complement_weak(const const_twa_graph_ptr& aut) + { + // Clone the original automaton. + auto res = make_twa_graph(aut, + { true, // state based + true, // inherently weak + true, // determinisitic + true, // stutter inv. + }); + scc_info si(res); + + // We will modify res in place, and the resulting + // automaton will only have one acceptance set. + acc_cond::mark_t all_acc = res->set_buchi(); + res->prop_state_based_acc(); + + unsigned sink = res->num_states(); + + for (unsigned src = 0; src < sink; ++src) + { + acc_cond::mark_t acc = 0U; + unsigned scc = si.scc_of(src); + if (si.is_rejecting_scc(scc) && !si.is_trivial(scc)) + acc = all_acc; + + // Keep track of all conditions on edge leaving state + // SRC, so we can complete it. + bdd missingcond = bddtrue; + for (auto& t: res->out(src)) + { + missingcond -= t.cond; + t.acc = acc; + } + // Complete the original automaton. + if (missingcond != bddfalse) + { + if (res->num_states() == sink) + { + res->new_state(); + res->new_acc_edge(sink, sink, bddtrue); + } + res->new_edge(src, sink, missingcond); + } + } + //res->merge_edges(); + return res; + } } twa_graph_ptr dtgba_complement(const const_twa_graph_ptr& aut) diff --git a/src/twaalgos/minimize.cc b/src/twaalgos/minimize.cc index bdadbfbd6..ff8d9369c 100644 --- a/src/twaalgos/minimize.cc +++ b/src/twaalgos/minimize.cc @@ -80,103 +80,100 @@ namespace spot dump_hash_set(hs, aut, s); return s.str(); } - } - // Find all states of an automaton. - void build_state_set(const const_twa_ptr& a, hash_set* seen) - { - std::queue tovisit; - // Perform breadth-first traversal. - const state* init = a->get_init_state(); - tovisit.push(init); - seen->insert(init); - while (!tovisit.empty()) - { - const state* src = tovisit.front(); - tovisit.pop(); + // Find all states of an automaton. + static void + build_state_set(const const_twa_ptr& a, hash_set* seen) + { + std::queue tovisit; + // Perform breadth-first traversal. + const state* init = a->get_init_state(); + tovisit.push(init); + seen->insert(init); + while (!tovisit.empty()) + { + const state* src = tovisit.front(); + tovisit.pop(); - for (auto sit: a->succ(src)) - { - const state* dst = sit->current_state(); - // Is it a new state ? - if (seen->find(dst) == seen->end()) - { - // Register the successor for later processing. - tovisit.push(dst); - seen->insert(dst); - } - else + for (auto sit: a->succ(src)) + { + const state* dst = sit->current_state(); + // Is it a new state ? + if (seen->find(dst) == seen->end()) + { + // Register the successor for later processing. + tovisit.push(dst); + seen->insert(dst); + } + else + dst->destroy(); + } + } + } + + // From the base automaton and the list of sets, build the minimal + // resulting automaton + static twa_graph_ptr + build_result(const const_twa_ptr& a, + std::list& sets, + hash_set* final) + { + auto dict = a->get_dict(); + auto res = make_twa_graph(dict); + res->copy_ap_of(a); + res->prop_state_based_acc(); + + // For each set, create a state in the resulting automaton. + // For a state s, state_num[s] is the number of the state in the minimal + // automaton. + hash_map state_num; + std::list::iterator sit; + for (sit = sets.begin(); sit != sets.end(); ++sit) + { + hash_set::iterator hit; + hash_set* h = *sit; + unsigned num = res->new_state(); + for (hit = h->begin(); hit != h->end(); ++hit) + state_num[*hit] = num; + } + + // For each transition in the initial automaton, add the corresponding + // transition in res. + + if (!final->empty()) + res->set_buchi(); + + for (sit = sets.begin(); sit != sets.end(); ++sit) + { + hash_set* h = *sit; + + // Pick one state. + const state* src = *h->begin(); + unsigned src_num = state_num[src]; + bool accepting = (final->find(src) != final->end()); + + // Connect it to all destinations. + for (auto succit: a->succ(src)) + { + const state* dst = succit->current_state(); + hash_map::const_iterator i = state_num.find(dst); dst->destroy(); - } - } - } - - // From the base automaton and the list of sets, build the minimal - // resulting automaton - twa_graph_ptr build_result(const const_twa_ptr& a, - std::list& sets, - hash_set* final) - { - auto dict = a->get_dict(); - auto res = make_twa_graph(dict); - res->copy_ap_of(a); - res->prop_state_based_acc(); - - // For each set, create a state in the resulting automaton. - // For a state s, state_num[s] is the number of the state in the minimal - // automaton. - hash_map state_num; - std::list::iterator sit; - for (sit = sets.begin(); sit != sets.end(); ++sit) - { - hash_set::iterator hit; - hash_set* h = *sit; - unsigned num = res->new_state(); - for (hit = h->begin(); hit != h->end(); ++hit) - state_num[*hit] = num; - } - - // For each transition in the initial automaton, add the corresponding - // transition in res. - - if (!final->empty()) - res->set_buchi(); - - for (sit = sets.begin(); sit != sets.end(); ++sit) - { - hash_set* h = *sit; - - // Pick one state. - const state* src = *h->begin(); - unsigned src_num = state_num[src]; - bool accepting = (final->find(src) != final->end()); - - // Connect it to all destinations. - for (auto succit: a->succ(src)) - { - const state* dst = succit->current_state(); - hash_map::const_iterator i = state_num.find(dst); - dst->destroy(); - if (i == state_num.end()) // Ignore useless destinations. - continue; - res->new_acc_edge(src_num, i->second, - succit->current_condition(), accepting); - } - } - res->merge_edges(); - if (res->num_states() > 0) - { - const state* init_state = a->get_init_state(); - unsigned init_num = state_num[init_state]; - init_state->destroy(); - res->set_init_state(init_num); - } - return res; - } - - - namespace - { + if (i == state_num.end()) // Ignore useless destinations. + continue; + res->new_acc_edge(src_num, i->second, + succit->current_condition(), accepting); + } + } + res->merge_edges(); + if (res->num_states() > 0) + { + const state* init_state = a->get_init_state(); + unsigned init_num = state_num[init_state]; + init_state->destroy(); + res->set_init_state(init_num); + } + return res; + } struct wdba_search_acc_loop : public bfs_steps { @@ -265,214 +262,213 @@ namespace spot return accepting; } - } + static twa_graph_ptr minimize_dfa(const const_twa_graph_ptr& det_a, + hash_set* final, hash_set* non_final) + { + typedef std::list partition_t; + partition_t cur_run; + partition_t next_run; - twa_graph_ptr minimize_dfa(const const_twa_graph_ptr& det_a, - hash_set* final, hash_set* non_final) - { - typedef std::list partition_t; - partition_t cur_run; - partition_t next_run; + // The list of equivalent states. + partition_t done; - // The list of equivalent states. - partition_t done; + hash_map state_set_map; - hash_map state_set_map; + // Size of det_a + unsigned size = final->size() + non_final->size(); + // Use bdd variables to number sets. set_num is the first variable + // available. + unsigned set_num = + det_a->get_dict()->register_anonymous_variables(size, det_a); - // Size of det_a - unsigned size = final->size() + non_final->size(); - // Use bdd variables to number sets. set_num is the first variable - // available. - unsigned set_num = - det_a->get_dict()->register_anonymous_variables(size, det_a); + std::set free_var; + for (unsigned i = set_num; i < set_num + size; ++i) + free_var.insert(i); + std::map used_var; - std::set free_var; - for (unsigned i = set_num; i < set_num + size; ++i) - free_var.insert(i); - std::map used_var; + hash_set* final_copy; - hash_set* final_copy; + if (!final->empty()) + { + unsigned s = final->size(); + used_var[set_num] = s; + free_var.erase(set_num); + if (s > 1) + cur_run.push_back(final); + else + done.push_back(final); + for (hash_set::const_iterator i = final->begin(); + i != final->end(); ++i) + state_set_map[*i] = set_num; - if (!final->empty()) - { - unsigned s = final->size(); - used_var[set_num] = s; - free_var.erase(set_num); - if (s > 1) - cur_run.push_back(final); - else - done.push_back(final); - for (hash_set::const_iterator i = final->begin(); - i != final->end(); ++i) - state_set_map[*i] = set_num; + final_copy = new hash_set(*final); + } + else + { + final_copy = final; + } - final_copy = new hash_set(*final); - } - else - { - final_copy = final; - } + if (!non_final->empty()) + { + unsigned s = non_final->size(); + unsigned num = set_num + 1; + used_var[num] = s; + free_var.erase(num); + if (s > 1) + cur_run.push_back(non_final); + else + done.push_back(non_final); + for (hash_set::const_iterator i = non_final->begin(); + i != non_final->end(); ++i) + state_set_map[*i] = num; + } + else + { + delete non_final; + } - if (!non_final->empty()) - { - unsigned s = non_final->size(); - unsigned num = set_num + 1; - used_var[num] = s; - free_var.erase(num); - if (s > 1) - cur_run.push_back(non_final); - else - done.push_back(non_final); - for (hash_set::const_iterator i = non_final->begin(); - i != non_final->end(); ++i) - state_set_map[*i] = num; - } - else - { - delete non_final; - } + // A bdd_states_map is a list of formulae (in a BDD form) + // associated with a destination set of states. + typedef std::map bdd_states_map; - // A bdd_states_map is a list of formulae (in a BDD form) associated with a - // destination set of states. - typedef std::map bdd_states_map; + bool did_split = true; - bool did_split = true; + while (did_split) + { + did_split = false; + while (!cur_run.empty()) + { + // Get a set to process. + hash_set* cur = cur_run.front(); + cur_run.pop_front(); - while (did_split) - { - did_split = false; - while (!cur_run.empty()) - { - // Get a set to process. - hash_set* cur = cur_run.front(); - cur_run.pop_front(); + trace << "processing " << format_hash_set(cur, det_a) + << std::endl; - trace << "processing " << format_hash_set(cur, det_a) << std::endl; + hash_set::iterator hi; + bdd_states_map bdd_map; + for (hi = cur->begin(); hi != cur->end(); ++hi) + { + const state* src = *hi; + bdd f = bddfalse; + for (auto si: det_a->succ(src)) + { + const state* dst = si->current_state(); + hash_map::const_iterator i = state_set_map.find(dst); + dst->destroy(); + if (i == state_set_map.end()) + // The destination state is not in our + // partition. This can happen if the initial + // FINAL and NON_FINAL supplied to the algorithm + // do not cover the whole automaton (because we + // want to ignore some useless states). Simply + // ignore these states here. + continue; + f |= (bdd_ithvar(i->second) & si->current_condition()); + } - hash_set::iterator hi; - bdd_states_map bdd_map; - for (hi = cur->begin(); hi != cur->end(); ++hi) - { - const state* src = *hi; - bdd f = bddfalse; - for (auto si: det_a->succ(src)) - { - const state* dst = si->current_state(); - hash_map::const_iterator i = state_set_map.find(dst); - dst->destroy(); - if (i == state_set_map.end()) - // The destination state is not in our - // partition. This can happen if the initial - // FINAL and NON_FINAL supplied to the algorithm - // do not cover the whole automaton (because we - // want to ignore some useless states). Simply - // ignore these states here. - continue; - f |= (bdd_ithvar(i->second) & si->current_condition()); - } + // Have we already seen this formula ? + bdd_states_map::iterator bsi = bdd_map.find(f); + if (bsi == bdd_map.end()) + { + // No, create a new set. + hash_set* new_set = new hash_set; + new_set->insert(src); + bdd_map[f] = new_set; + } + else + { + // Yes, add the current state to the set. + bsi->second->insert(src); + } + } - // Have we already seen this formula ? - bdd_states_map::iterator bsi = bdd_map.find(f); - if (bsi == bdd_map.end()) - { - // No, create a new set. - hash_set* new_set = new hash_set; - new_set->insert(src); - bdd_map[f] = new_set; - } - else - { - // Yes, add the current state to the set. - bsi->second->insert(src); - } - } + bdd_states_map::iterator bsi = bdd_map.begin(); + if (bdd_map.size() == 1) + { + // The set was not split. + trace << "set " << format_hash_set(bsi->second, det_a) + << " was not split" << std::endl; + next_run.push_back(bsi->second); + } + else + { + did_split = true; + for (; bsi != bdd_map.end(); ++bsi) + { + hash_set* set = bsi->second; + // Free the number associated to these states. + unsigned num = state_set_map[*set->begin()]; + assert(used_var.find(num) != used_var.end()); + unsigned left = (used_var[num] -= set->size()); + // Make sure LEFT does not become negative (hence bigger + // than SIZE when read as unsigned) + assert(left < size); + if (left == 0) + { + used_var.erase(num); + free_var.insert(num); + } + // Pick a free number + assert(!free_var.empty()); + num = *free_var.begin(); + free_var.erase(free_var.begin()); + used_var[num] = set->size(); + for (hash_set::iterator hit = set->begin(); + hit != set->end(); ++hit) + state_set_map[*hit] = num; + // Trivial sets can't be splitted any further. + if (set->size() == 1) + { + trace << "set " << format_hash_set(set, det_a) + << " is minimal" << std::endl; + done.push_back(set); + } + else + { + trace << "set " << format_hash_set(set, det_a) + << " should be processed further" << std::endl; + next_run.push_back(set); + } + } + } + delete cur; + } + if (did_split) + trace << "splitting did occur during this pass." << std::endl; + else + trace << "splitting did not occur during this pass." << std::endl; + std::swap(cur_run, next_run); + } - bdd_states_map::iterator bsi = bdd_map.begin(); - if (bdd_map.size() == 1) - { - // The set was not split. - trace << "set " << format_hash_set(bsi->second, det_a) - << " was not split" << std::endl; - next_run.push_back(bsi->second); - } - else - { - did_split = true; - for (; bsi != bdd_map.end(); ++bsi) - { - hash_set* set = bsi->second; - // Free the number associated to these states. - unsigned num = state_set_map[*set->begin()]; - assert(used_var.find(num) != used_var.end()); - unsigned left = (used_var[num] -= set->size()); - // Make sure LEFT does not become negative (hence bigger - // than SIZE when read as unsigned) - assert(left < size); - if (left == 0) - { - used_var.erase(num); - free_var.insert(num); - } - // Pick a free number - assert(!free_var.empty()); - num = *free_var.begin(); - free_var.erase(free_var.begin()); - used_var[num] = set->size(); - for (hash_set::iterator hit = set->begin(); - hit != set->end(); ++hit) - state_set_map[*hit] = num; - // Trivial sets can't be splitted any further. - if (set->size() == 1) - { - trace << "set " << format_hash_set(set, det_a) - << " is minimal" << std::endl; - done.push_back(set); - } - else - { - trace << "set " << format_hash_set(set, det_a) - << " should be processed further" << std::endl; - next_run.push_back(set); - } - } - } - delete cur; - } - if (did_split) - trace << "splitting did occur during this pass." << std::endl; - else - trace << "splitting did not occur during this pass." << std::endl; - std::swap(cur_run, next_run); - } - - done.splice(done.end(), cur_run); + done.splice(done.end(), cur_run); #ifdef TRACE - trace << "Final partition: "; - for (partition_t::const_iterator i = done.begin(); i != done.end(); ++i) - trace << format_hash_set(*i, det_a) << ' '; - trace << std::endl; + trace << "Final partition: "; + for (partition_t::const_iterator i = done.begin(); i != done.end(); ++i) + trace << format_hash_set(*i, det_a) << ' '; + trace << std::endl; #endif - // Build the result. - auto res = build_result(det_a, done, final_copy); + // Build the result. + auto res = build_result(det_a, done, final_copy); - // Free all the allocated memory. - delete final_copy; - hash_map::iterator hit; - for (hit = state_set_map.begin(); hit != state_set_map.end();) - { - hash_map::iterator old = hit++; - old->first->destroy(); - } - std::list::iterator it; - for (it = done.begin(); it != done.end(); ++it) - delete *it; + // Free all the allocated memory. + delete final_copy; + hash_map::iterator hit; + for (hit = state_set_map.begin(); hit != state_set_map.end();) + { + hash_map::iterator old = hit++; + old->first->destroy(); + } + std::list::iterator it; + for (it = done.begin(); it != done.end(); ++it) + delete *it; - return res; + return res; + } } - twa_graph_ptr minimize_monitor(const const_twa_graph_ptr& a) { hash_set* final = new hash_set;