diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am
index 9636a3c45..b935d4202 100644
--- a/src/tgba/Makefile.am
+++ b/src/tgba/Makefile.am
@@ -29,7 +29,6 @@ tgba_HEADERS = \
bdddict.hh \
bddprint.hh \
formula2bdd.hh \
- futurecondcol.hh \
fwd.hh \
taatgba.hh \
tgba.hh \
@@ -37,7 +36,6 @@ tgba_HEADERS = \
tgbakvcomplement.hh \
tgbamask.hh \
tgbaproxy.hh \
- tgbascc.hh \
tgbaproduct.hh \
tgbasgba.hh \
tgbasafracomplement.hh \
@@ -48,7 +46,6 @@ libtgba_la_SOURCES = \
bdddict.cc \
bddprint.cc \
formula2bdd.cc \
- futurecondcol.cc \
taatgba.cc \
tgba.cc \
tgbagraph.cc \
@@ -57,6 +54,5 @@ libtgba_la_SOURCES = \
tgbamask.cc \
tgbaproxy.cc \
tgbasafracomplement.cc \
- tgbascc.cc \
tgbasgba.cc \
wdbacomp.cc
diff --git a/src/tgba/futurecondcol.cc b/src/tgba/futurecondcol.cc
deleted file mode 100644
index 38f088666..000000000
--- a/src/tgba/futurecondcol.cc
+++ /dev/null
@@ -1,89 +0,0 @@
-// -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2014 Laboratoire de recherche et développement
-// de l'Epita.
-//
-// 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
-// the Free Software Foundation; either version 3 of the License, or
-// (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
-// along with this program. If not, see .
-
-#include
-#include "futurecondcol.hh"
-#include "bddprint.hh"
-
-namespace spot
-{
-
- void
- future_conditions_collector::map_builder_(unsigned src)
- {
- // The future conditions of a SCC are the conditions of the SCC
- // augmented with the future conditions of any descendent SCC.
- cond_set res(scc_map_.cond_set_of(src));
- const scc_map::succ_type& next = scc_map_.succ(src);
- for (scc_map::succ_type::const_iterator i = next.begin();
- i != next.end(); ++i)
- {
- unsigned dest = i->first;
- map_builder_(dest);
- res.insert(i->second);
- res.insert(future_conds_[dest].begin(), future_conds_[dest].end());
- }
- future_conds_[src] = res;
- }
-
- future_conditions_collector::future_conditions_collector
- (const const_tgba_ptr& aut, bool show)
- : tgba_scc(aut, show),
- // Initialize future_conds_ with as much empty
- // "cond_set"s as there are SCCs.
- future_conds_(scc_map_.scc_count())
- {
- // Fill future_conds by recursively visiting the (acyclic) graph
- // of SCCs.
- map_builder_(scc_map_.initial());
- }
-
- future_conditions_collector::~future_conditions_collector()
- {
- }
-
- const future_conditions_collector::cond_set&
- future_conditions_collector::future_conditions(const spot::state* st) const
- {
- // The future conditions of a state are the future conditions of
- // the SCC the state belongs to.
- unsigned s = scc_map_.scc_of_state(st);
- return future_conds_[s];
- }
-
- std::string
- future_conditions_collector::format_state(const state* state) const
- {
- if (!show_)
- return aut_->format_state(state);
-
- std::ostringstream str;
- str << this->tgba_scc::format_state(state);
- str << "\\n[";
- const cond_set& c = future_conditions(state);
- for (cond_set::const_iterator i = c.begin(); i != c.end(); ++i)
- {
- if (i != c.begin())
- str << ", ";
- bdd_print_formula(str, get_dict(), *i);
- }
- str << ']';
- return str.str();
- }
-}
diff --git a/src/tgba/futurecondcol.hh b/src/tgba/futurecondcol.hh
deleted file mode 100644
index 5409860b6..000000000
--- a/src/tgba/futurecondcol.hh
+++ /dev/null
@@ -1,81 +0,0 @@
-// -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2013, 2014 Laboratoire de recherche et développement
-// de l'Epita.
-//
-// 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
-// the Free Software Foundation; either version 3 of the License, or
-// (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
-// along with this program. If not, see .
-
-#ifndef SPOT_TGBA_FUTURECONDCOL_HH
-# define SPOT_TGBA_FUTURECONDCOL_HH
-
-#include "tgbascc.hh"
-
-namespace spot
-{
-
- /// \ingroup tgba
- /// \brief Wrap a tgba to offer information about upcoming conditions.
- ///
- /// This class is a spot::tgba wrapper that simply add a new method,
- /// future_conditions(), to any spot::tgba.
- ///
- /// This new method returns a set of conditions that can be
- /// seen on a transitions accessible (maybe indirectly) from
- /// the given state.
- class SPOT_API future_conditions_collector : public tgba_scc
- {
- public:
- typedef scc_map::cond_set cond_set;
- typedef std::vector fc_map;
-
- /// \brief Create a future_conditions_collector wrapper for \a aut.
- ///
- /// If \a show is set to true, then the format_state() method will
- /// include the set of conditions computed for the given state in
- /// its output string.
- future_conditions_collector(const const_tgba_ptr& aut, bool show = false);
- virtual ~future_conditions_collector();
-
- /// Returns the set of future conditions visible after \a s
- const cond_set& future_conditions(const spot::state* s) const;
-
- /// \brief Format a state for output.
- ///
- /// If the constructor was called with \a show set to true, then
- /// this method will include the set of conditions computed for \a
- /// state by future_conditions() in the output string.
- virtual std::string format_state(const state* state) const;
-
- protected:
- void map_builder_(unsigned s);
-
- fc_map future_conds_; // The map of future conditions for each
- // strongly connected component.
- };
-
- typedef std::shared_ptr
- future_conditions_collector_ptr;
- typedef std::shared_ptr
- const_future_conditions_collector_ptr;
-
- inline future_conditions_collector_ptr
- make_future_conditions_collector(const const_tgba_ptr& aut, bool show = false)
- {
- return std::make_shared(aut, show);
- }
-
-}
-
-#endif // SPOT_TGBA_FUTURECONDCOL_HH
diff --git a/src/tgba/tgbascc.cc b/src/tgba/tgbascc.cc
deleted file mode 100644
index 95b1351cf..000000000
--- a/src/tgba/tgbascc.cc
+++ /dev/null
@@ -1,109 +0,0 @@
-// -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2012, 2013, 2014 Laboratoire de recherche et
-// développement de l'Epita.
-//
-// 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
-// the Free Software Foundation; either version 3 of the License, or
-// (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
-// along with this program. If not, see .
-
-#include
-#include "tgbascc.hh"
-
-namespace spot
-{
-
- tgba_scc::tgba_scc(const const_tgba_ptr& aut, bool show)
- : aut_(aut), scc_map_(aut), show_(show)
- {
- scc_map_.build_map();
- }
-
- tgba_scc::~tgba_scc()
- {
- }
-
- unsigned
- tgba_scc::scc_of_state(const spot::state* st) const
- {
- return scc_map_.scc_of_state(st);
- }
-
- state*
- tgba_scc::get_init_state() const
- {
- return aut_->get_init_state();
- }
-
- tgba_succ_iterator*
- tgba_scc::succ_iter(const state* state) const
- {
- if (iter_cache_)
- {
- aut_->release_iter(iter_cache_);
- iter_cache_ = nullptr;
- }
- return aut_->succ_iter(state);
- }
-
- bdd_dict_ptr
- tgba_scc::get_dict() const
- {
- return aut_->get_dict();
- }
-
- std::string
- tgba_scc::format_state(const state* state) const
- {
- if (!show_)
- return aut_->format_state(state);
-
- std::ostringstream str;
- str << aut_->format_state(state);
- str << "\\nSCC #" << scc_of_state(state);
- return str.str();
- }
-
- std::string
- tgba_scc::transition_annotation
- (const tgba_succ_iterator* t) const
- {
- return aut_->transition_annotation(t);
- }
-
- state*
- tgba_scc::project_state(const state* s, const const_tgba_ptr& t) const
- {
- return aut_->project_state(s, t);
- }
-
- bdd
- tgba_scc::all_acceptance_conditions() const
- {
- return aut_->all_acceptance_conditions();
- }
-
- bdd
- tgba_scc::neg_acceptance_conditions() const
- {
- return aut_->neg_acceptance_conditions();
- }
-
- bdd
- tgba_scc::compute_support_conditions
- (const state* state) const
- {
- return aut_->support_conditions(state);
- }
-
-}
diff --git a/src/tgba/tgbascc.hh b/src/tgba/tgbascc.hh
deleted file mode 100644
index 973891aef..000000000
--- a/src/tgba/tgbascc.hh
+++ /dev/null
@@ -1,80 +0,0 @@
-// -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2013, 2014 Laboratoire de recherche et
-// développement de l'Epita.
-//
-// 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
-// the Free Software Foundation; either version 3 of the License, or
-// (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
-// along with this program. If not, see .
-
-#ifndef SPOT_TGBA_TGBASCC_HH
-# define SPOT_TGBA_TGBASCC_HH
-
-#include "tgba.hh"
-#include "tgbaalgos/scc.hh"
-
-namespace spot
-{
-
- /// \ingroup tgba
- /// \brief Wrap a tgba to offer information about strongly connected
- /// components.
- ///
- /// This class is a spot::tgba wrapper that simply add a new method
- /// scc_of_state() to retrieve the number of a SCC a state belongs to.
- class SPOT_API tgba_scc : public tgba
- {
- public:
- /// \brief Create a tgba_scc wrapper for \a aut.
- ///
- /// If \a show is set to true, then the format_state() method will
- /// include the SCC number computed for the given state in its
- /// output string.
- tgba_scc(const const_tgba_ptr& aut, bool show = false);
- virtual ~tgba_scc();
-
- /// Returns the number of the SCC \a s belongs to.
- unsigned scc_of_state(const spot::state* s) const;
-
- /// \brief Format a state for output.
- ///
- /// If the constructor was called with \a show set to true, then
- /// this method will include the SCC number computed for \a
- /// state in the output string.
- virtual std::string format_state(const state* state) const;
-
- // The following methods simply delegate their work to the wrapped
- // tgba.
-
- virtual state* get_init_state() const;
- virtual tgba_succ_iterator* succ_iter(const state* state) const;
- virtual bdd_dict_ptr get_dict() const;
-
- virtual std::string
- transition_annotation(const tgba_succ_iterator* t) const;
- virtual state* project_state(const state* s, const const_tgba_ptr& t) const;
- virtual bdd all_acceptance_conditions() const;
- virtual bdd neg_acceptance_conditions() const;
-
- virtual bdd compute_support_conditions(const state* state) const;
-
- protected:
- const_tgba_ptr aut_; // The wrapped TGBA.
- scc_map scc_map_; // SCC informations.
- bool show_; // Wether to show future conditions
- // in the output of format_state().
- };
-
-}
-
-#endif // SPOT_TGBA_TGBASCC_HH
diff --git a/src/tgbatest/checkpsl.cc b/src/tgbatest/checkpsl.cc
index 81a7d4e65..61dabb00e 100644
--- a/src/tgbatest/checkpsl.cc
+++ b/src/tgbatest/checkpsl.cc
@@ -24,7 +24,6 @@
#include
#include "ltlparse/public.hh"
#include "ltlast/allnodes.hh"
-#include "tgba/futurecondcol.hh"
#include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgbaalgos/ltl2taa.hh"
#include "tgbaalgos/sccfilter.hh"
@@ -80,10 +79,6 @@ main(int argc, char** argv)
std::cerr << "non-empty intersection between pos and neg (FM)\n";
exit(2);
}
-
- // Run make_future_conditions_collector, without testing the output.
- auto fc = spot::make_future_conditions_collector(apos, true);
- spot::dotty_reachable(std::cout, fc);
}
{
diff --git a/src/tgbatest/emptchk.cc b/src/tgbatest/emptchk.cc
index 8176e68dc..cdc51ea60 100644
--- a/src/tgbatest/emptchk.cc
+++ b/src/tgbatest/emptchk.cc
@@ -24,7 +24,6 @@
#include
#include "ltlparse/public.hh"
#include "ltlast/allnodes.hh"
-#include "tgba/futurecondcol.hh"
#include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgbaalgos/ltl2taa.hh"
#include "tgbaalgos/sccfilter.hh"
diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc
index 6ccec85a4..1f73b7730 100644
--- a/src/tgbatest/ltl2tgba.cc
+++ b/src/tgbatest/ltl2tgba.cc
@@ -40,7 +40,6 @@
#include "tgba/tgbasgba.hh"
#include "tgbaalgos/degen.hh"
#include "tgba/tgbaproduct.hh"
-#include "tgba/futurecondcol.hh"
#include "tgbaalgos/reducerun.hh"
#include "tgbaparse/public.hh"
#include "neverparse/public.hh"
@@ -274,8 +273,6 @@ syntax(char* prog)
<< "Output options (if no emptiness check):" << std::endl
<< " -b output the automaton in the format of spot"
<< std::endl
- << " -FC dump the automaton showing future conditions on states"
- << std::endl
<< " -k display statistics on the automaton (size and SCCs)"
<< std::endl
<< " -ks display statistics on the automaton (size only)"
@@ -384,7 +381,6 @@ checked_main(int argc, char** argv)
bool opt_bisim_ta = false;
bool opt_monitor = false;
bool containment = false;
- bool show_fc = false;
bool spin_comments = false;
const char* hoaf_opt = 0;
spot::ltl::environment& env(spot::ltl::default_environment::instance());
@@ -541,10 +537,6 @@ checked_main(int argc, char** argv)
{
file_opt = true;
}
- else if (!strcmp(argv[formula_index], "-FC"))
- {
- show_fc = true;
- }
else if (!strcmp(argv[formula_index], "-g"))
{
accepting_run = true;
@@ -1566,11 +1558,6 @@ checked_main(int argc, char** argv)
}
}
- if (show_fc)
- {
- a = spot::make_future_conditions_collector(a, true);
- }
-
if (output != -1)
{
tm.start("producing output");