Skip to content
GitLab
Commit c8b399c0 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Remove futurecondcol and tgbascc. 

They are not used in Spot, and their interface is really horrible.  They
are used in SOG-ITS to implement the SLAP product from TACAS'11, so we
should support the functionality eventually, but maybe using the new
kind of properties that can be attached to automata.  In the meantime,
these classes are making refactoring harder.

* src/tgba/futurecondcol.cc, src/tgba/futurecondcol.hh,
src/tgba/tgbascc.cc, src/tgba/tgbascc.hh: Delete.
* src/tgba/Makefile.am, src/tgbatest/ltl2tgba.cc,
src/tgbatest/checkpsl.cc, src/tgbatest/emptchk.cc: Adjust.
parent baf644a9
Hide whitespace changes
Inline Side-by-side
src/tgba/Makefile.am
View file @ c8b399c0
......@@ -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
src/tgba/futurecondcol.cc deleted 100644 → 0
View file @ baf644a9
// -*- 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 <http://www.gnu.org/licenses/>.
#include <sstream>
#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();
}
}
src/tgba/futurecondcol.hh deleted 100644 → 0
View file @ baf644a9
// -*- 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 <http://www.gnu.org/licenses/>.
#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<cond_set> 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>
future_conditions_collector_ptr;
typedef std::shared_ptr<const future_conditions_collector>
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<future_conditions_collector>(aut, show);
}
}
#endif // SPOT_TGBA_FUTURECONDCOL_HH
src/tgba/tgbascc.cc deleted 100644 → 0
View file @ baf644a9
// -*- 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 <http://www.gnu.org/licenses/>.
#include <sstream>
#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);
}
}
src/tgba/tgbascc.hh deleted 100644 → 0
View file @ baf644a9
// -*- 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 <http://www.gnu.org/licenses/>.
#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
src/tgbatest/checkpsl.cc
View file @ c8b399c0
......@@ -24,7 +24,6 @@
#include <cstring>
#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);
}
{
......
src/tgbatest/emptchk.cc
View file @ c8b399c0
......@@ -24,7 +24,6 @@
#include <cstring>
#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"
......
src/tgbatest/ltl2tgba.cc
View file @ c8b399c0
......@@ -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");
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment