diff --git a/spot/twaalgos/emptiness_stats.hh b/spot/twaalgos/emptiness_stats.hh index 0e52e6085..c56915efa 100644 --- a/spot/twaalgos/emptiness_stats.hh +++ b/spot/twaalgos/emptiness_stats.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de +// Copyright (C) 2015-2017 Laboratoire de Recherche et Développement de // l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -52,67 +52,6 @@ namespace spot stats_map stats; }; - /// \brief comparable statistics - /// - /// This must be built from a spot::unsigned_statistics. But unlike - /// spot::unsigned_statistics, it supports equality and inequality tests. - /// (It's the only operations it supports, BTW.) - class unsigned_statistics_copy - { - public: - unsigned_statistics_copy() - : set(false) - { - } - - unsigned_statistics_copy(const unsigned_statistics& o) - : set(false) - { - seteq(o); - } - - bool - seteq(const unsigned_statistics& o) - { - if (!set) - { - for (auto& i: o.stats) - stats[i.first] = (o.*i.second)(); - set = true; - return true; - } - if (*this == o) - return true; - return false; - } - - typedef std::map stats_map; - stats_map stats; - - - bool - operator==(const unsigned_statistics_copy& o) const - { - for (auto& i: stats) - { - auto i2 = o.stats.find(i.first); - if (i2 == o.stats.end()) - return false; - if (i.second != i2->second) - return false; - } - return true; - } - - bool - operator!=(const unsigned_statistics_copy& o) const - { - return !(*this == o); - } - - bool set; - }; - /// \brief Emptiness-check statistics /// /// Implementations of spot::emptiness_check may also implement diff --git a/tests/core/randtgba.cc b/tests/core/randtgba.cc index b1ef86d6b..3bc655f78 100644 --- a/tests/core/randtgba.cc +++ b/tests/core/randtgba.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015, 2016 Laboratoire -// de Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2008-2012, 2014-2017 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -145,8 +145,6 @@ syntax(char* prog) << " otherwise be skipped (implies -e)" << std::endl << " -e N compare result of all " << "emptiness checks on N randomly generated graphs" << std::endl - << " -H halt on the first statistic difference in algorithms" - << std::endl << " -m try to reduce runs, in a second pass (implies -r)" << std::endl << " -R N repeat each emptiness-check and accepting run " @@ -572,8 +570,6 @@ main(int argc, char** argv) int exit_code = 0; - bool stop_on_first_difference = false; - spot::twa_graph_ptr formula = nullptr; spot::twa_graph_ptr product = nullptr; @@ -677,12 +673,6 @@ main(int argc, char** argv) { opt_dot = true; } - else if (!strcmp(argv[argn], "-H")) - { - if (argc < argn + 1) - syntax(argv[0]); - stop_on_first_difference = true; - } else if (!strcmp(argv[argn], "-i")) { if (argc < argn + 2) @@ -925,7 +915,6 @@ main(int argc, char** argv) int n_empty = 0; int n_non_empty = 0; int n_maybe_empty = 0; - spot::unsigned_statistics_copy ostats_ec, ostats_arc; for (int i = 0; i < n_alg; ++i) { @@ -973,14 +962,6 @@ main(int argc, char** argv) } } - if (stop_on_first_difference && ecs) - if (!ostats_ec.seteq(*ecs)) - { - std::cout << "DIFFERING STATS for emptiness check," - << " halting... "; - opt_ec = n_alg = opt_F = 0; - } - if (res) { if (!opt_paper) @@ -1011,14 +992,6 @@ main(int argc, char** argv) sc_arc.count(algo, s); arc_ratio_stats.count(algo, s); } - if (stop_on_first_difference && s) - if (!ostats_arc.seteq(*s)) - { - std::cout << "DIFFERING STATS for " - << "accepting runs," - << " halting... "; - opt_ec = n_alg = opt_F = 0; - } if (!run) { if (!opt_paper)