Commit e6ea90e3 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

remove tgba_explicit variants and the old scc_filter

* src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh: Delete.
* src/tgba/Makefile.am: Adjust.
* src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim.hh:
Delete these obsoleted algorithms.
* src/tgbaalgos/Makefile.am: Adjust.
* src/tgbatest/explicit.cc, src/tgbatest/explicit.test,
src/tgbatest/explicit2.cc, src/tgbatest/explicit2.test,
src/tgbatest/explicit3.cc, src/tgbatest/explicit3.test:
Delete.
* src/tgbatest/Makefile.am: Adjust.
* src/bin/ltl2tgba.cc, src/priv/countstates.cc,
src/tgbaalgos/isweakscc.cc, src/tgbaalgos/lbtt.cc,
src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/minimize.cc,
src/tgbaalgos/minimize.hh, src/tgbaalgos/powerset.cc,
src/tgbaalgos/powerset.hh, src/tgbaalgos/sccfilter.cc,
src/tgbaalgos/sccfilter.hh, src/tgbaalgos/simulation.cc,
src/tgbatest/explprod.cc, src/tgbatest/ltl2tgba.cc,
src/tgbatest/powerset.cc, src/tgbatest/tgbaread.cc,
src/tgbatest/tripprod.cc, wrap/python/ajax/spot.in,
wrap/python/spot.i: Remove all remaining references to
tgba_explicit.
parent 6c9d5e4b
......@@ -35,7 +35,6 @@
#include "ltlast/formula.hh"
#include "ltlvisit/tostring.hh"
#include "tgba/tgbaexplicit.hh"
#include "tgbaalgos/dotty.hh"
#include "tgbaalgos/lbtt.hh"
#include "tgbaalgos/neverclaim.hh"
......
......@@ -18,7 +18,6 @@
// along with this program. If not, see <http://www.gnu.org/licenses/>.
#include "countstates.hh"
#include "tgba/tgbaexplicit.hh"
#include "tgba/tgbagraph.hh"
#include "tgbaalgos/stats.hh"
......@@ -28,10 +27,6 @@ namespace spot
{
if (auto b = dynamic_cast<const tgba_digraph*>(a))
return b->num_states();
if (auto b = dynamic_cast<const sba_explicit_number*>(a))
return b->num_states();
if (auto b = dynamic_cast<const tgba_explicit_number*>(a))
return b->num_states();
return stats_reachable(a).states;
}
}
......@@ -35,7 +35,6 @@ tgba_HEADERS = \
succiter.hh \
taatgba.hh \
tgba.hh \
tgbaexplicit.hh \
tgbagraph.hh \
tgbakvcomplement.hh \
tgbamask.hh \
......@@ -56,7 +55,6 @@ libtgba_la_SOURCES = \
futurecondcol.cc \
taatgba.cc \
tgba.cc \
tgbaexplicit.cc \
tgbakvcomplement.cc \
tgbaproduct.cc \
tgbamask.cc \
......
// Copyright (C) 2012 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// 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 "tgbaexplicit.hh"
#include "ltlast/constant.hh"
namespace spot
{
const std::string state_explicit_string::default_val("empty");
const int state_explicit_number::default_val(0);
const ltl::formula*
state_explicit_formula::default_val(ltl::constant::true_instance());
}
This diff is collapsed.
......@@ -56,7 +56,6 @@ tgbaalgos_HEADERS = \
randomgraph.hh \
reachiter.hh \
reducerun.hh \
reductgba_sim.hh \
replayrun.hh \
rundotdec.hh \
safety.hh \
......@@ -103,7 +102,6 @@ libtgbaalgos_la_SOURCES = \
randomgraph.cc \
reachiter.cc \
reducerun.cc \
reductgba_sim.cc \
replayrun.cc \
rundotdec.cc \
safety.cc \
......
......@@ -18,7 +18,6 @@
// along with this program. If not, see <http://www.gnu.org/licenses/>.
#include "cycles.hh"
#include "tgba/tgbaexplicit.hh"
#include "ltlast/formula.hh"
#include "isweakscc.hh"
......
......@@ -25,7 +25,6 @@
#include <string>
#include <ostream>
#include <memory>
#include "tgba/tgbaexplicit.hh"
#include "tgba/formula2bdd.hh"
#include "reachiter.hh"
#include "misc/bddlt.hh"
......@@ -81,11 +80,13 @@ namespace spot
all_acc_conds_(a->all_acceptance_conditions()),
acs_(all_acc_conds_),
sba_format_(sba_format),
// If outputting with state-based acceptance, check if the
// automaton can be converted into an sba. This makes the
// state_is_accepting() function more efficient.
sba_(sba_format ? dynamic_cast<const sba*>(a) : 0)
// Check if the automaton can be converted into a
// tgba_digraph. This makes the state_is_accepting()
// function more efficient.
sba_(dynamic_cast<const tgba_digraph*>(a))
{
if (sba_ && !sba_->get_bprop(tgba_digraph::SBA))
sba_ = nullptr;
}
bool
......@@ -165,7 +166,7 @@ namespace spot
bdd all_acc_conds_;
acceptance_cond_splitter acs_;
bool sba_format_;
const sba* sba_;
const tgba_digraph* sba_;
};
static
......
......@@ -37,7 +37,6 @@
#include "ltl2tgba_fm.hh"
#include "tgba/bddprint.hh"
#include "tgbaalgos/sccinfo.hh"
#include "tgba/tgbaexplicit.hh"
//#include "tgbaalgos/dotty.hh"
#include "priv/acccompl.hh"
......
......@@ -615,7 +615,7 @@ namespace spot
tgba_digraph*
minimize_obligation(const tgba_digraph* aut_f,
const ltl::formula* f, const tgba* aut_neg_f,
const ltl::formula* f, const tgba_digraph* aut_neg_f,
bool reject_bigger)
{
auto min_aut_f = minimize_wdba(aut_f);
......@@ -656,7 +656,7 @@ namespace spot
neg_f->destroy();
// Remove useless SCCs.
const tgba* tmp = scc_filter(aut_neg_f, true);
auto tmp = scc_filter(aut_neg_f, true);
delete aut_neg_f;
to_free = aut_neg_f = tmp;
}
......
......@@ -152,7 +152,7 @@ namespace spot
/// that the minimized WDBA is correct.
SPOT_API tgba_digraph* minimize_obligation(const tgba_digraph* aut_f,
const ltl::formula* f = 0,
const tgba* aut_neg_f = 0,
const tgba_digraph* aut_neg_f = 0,
bool reject_bigger = false);
/// @}
......
......@@ -328,7 +328,7 @@ namespace spot
unsigned threshold_states,
unsigned threshold_cycles,
const ltl::formula* f,
const tgba* neg_aut)
const tgba_digraph* neg_aut)
{
const tgba* built = 0;
if (f == 0 && neg_aut == 0)
......@@ -349,7 +349,7 @@ namespace spot
neg_f->destroy();
// Remove useless SCCs.
const tgba* tmp = scc_filter(neg_aut, true);
auto tmp = scc_filter(neg_aut, true);
delete neg_aut;
built = neg_aut = tmp;
}
......
......@@ -143,7 +143,7 @@ namespace spot
unsigned threshold_states = 0,
unsigned threshold_cycles = 0,
const ltl::formula* f = 0,
const tgba* neg_aut = 0);
const tgba_digraph* neg_aut = 0);
}
......
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2011, 2012, 2013 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2004, 2005, 2007 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
//
// 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/>.
#define SKIP_DEPRECATED_WARNING
#include "reductgba_sim.hh"
#include "sccfilter.hh"
#include "simulation.hh"
#include "dupexp.hh"
namespace spot
{
const tgba*
reduc_tgba_sim(const tgba* f, int opt)
{
if (opt & Reduce_Scc)
{
f = scc_filter(f);
// No more reduction requested? Return the automaton as-is.
if (opt == Reduce_Scc)
return f;
}
if (opt & (Reduce_quotient_Dir_Sim | Reduce_transition_Dir_Sim
| Reduce_quotient_Del_Sim | Reduce_transition_Del_Sim))
{
tgba* res = simulation(f);
if (opt & Reduce_Scc)
delete f;
return res;
}
return tgba_dupexp_dfs(f);
}
}
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013 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.
//
// 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_TGBAALGOS_REDUCTGBA_SIM_HH
#define SPOT_TGBAALGOS_REDUCTGBA_SIM_HH
#if __GNUC__
#ifndef SKIP_DEPRECATED_WARNING
#warning This file is deprecated. Use postproc.hh instead.
#endif
#endif
#include "misc/common.hh"
namespace spot
{
class tgba;
/// \addtogroup tgba_reduction
/// @{
/// Options for reduce.
enum reduce_tgba_options
{
// Reduce_None and Reduce_All clash with the definitions in ltl::reduce
// for Swig because Swig does not handle namespaces.
#ifndef SWIG
/// No reduction.
Reduce_None = 0,
#endif
/// Reduction of state using direct simulation relation.
Reduce_quotient_Dir_Sim = 1,
/// Reduction of transitions using direct simulation relation.
Reduce_transition_Dir_Sim = 2,
/// Reduction of state using delayed simulation relation.
Reduce_quotient_Del_Sim = 4,
/// Reduction of transition using delayed simulation relation.
Reduce_transition_Del_Sim = 8,
/// Reduction using SCC.
Reduce_Scc = 16,
#ifndef SWIG
/// All reductions.
Reduce_All = -1U
#endif
};
/// \brief Simplify the automaton using a simulation relation.
///
/// Do not use this obsolete function.
///
/// \param a the automata to reduce
/// \param opt a conjonction of spot::reduce_tgba_options specifying
/// which optimizations to apply. Actually any
/// simulation-related flag will cause direct simulation
/// to be applied.
/// \return the reduced automaton
/// \deprecated Use scc_filter(), minimize_wdba(), simulation(),
/// or postprocessor.
SPOT_API SPOT_DEPRECATED
const tgba* reduc_tgba_sim(const tgba* a, int opt = Reduce_All);
/// @}
}
#endif // SPOT_TGBAALGOS_REDUCTGBA_SIM_HH
......@@ -17,7 +17,6 @@
// 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 "tgba/tgbaexplicit.hh"
#include "sccfilter.hh"
#include "reachiter.hh"
#include "scc.hh"
......@@ -31,492 +30,6 @@ namespace spot
typedef std::map<int, unsigned> accremap_t;
typedef std::vector<accremap_t> remap_table_t;
static
state_explicit_number::transition*
create_transition(const tgba*, tgba_explicit_number* out_aut,
const state*, int in, const state*, int out)
{
return out_aut->create_transition(in, out);
}
static
state_explicit_string::transition*
create_transition(const tgba* aut, tgba_explicit_string* out_aut,
const state* in_s, int, const state* out_s, int)
{
const tgba_explicit_string* a =
static_cast<const tgba_explicit_string*>(aut);
return out_aut->create_transition(a->get_label(in_s),
a->get_label(out_s));
}
static
state_explicit_formula::transition*
create_transition(const tgba* aut, tgba_explicit_formula* out_aut,
const state* in_s, int, const state* out_s, int)
{
const tgba_explicit_formula* a =
static_cast<const tgba_explicit_formula*>(aut);
const ltl::formula* in_f = a->get_label(in_s);
const ltl::formula* out_f = a->get_label(out_s);
if (!out_aut->has_state(in_f))
in_f->clone();
if ((in_f != out_f) && !out_aut->has_state(out_f))
out_f->clone();
return out_aut->create_transition(in_f, out_f);
}
template<class T>
class filter_iter_states: public tgba_reachable_iterator_depth_first
{
public:
typedef T output_t;
filter_iter_states(const tgba* a,
const scc_map& sm,
const std::vector<bool>& useless)
: tgba_reachable_iterator_depth_first(a),
out_(new T(a->get_dict())),
sm_(sm),
useless_(useless)
{
a->get_dict()->register_all_variables_of(a, out_);
out_->set_acceptance_conditions(a->all_acceptance_conditions());
}
T*
result()
{
return out_;
}
bool
want_state(const state* s) const
{
return !useless_[sm_.scc_of_state(s)];
}
void
process_link(const state* in_s, int in,
const state* out_s, int out,
const tgba_succ_iterator* si)
{
typename output_t::state::transition* t =
create_transition(this->aut_, out_, in_s, in, out_s, out);
t->condition = si->current_condition();
t->acceptance_conditions = si->current_acceptance_conditions();
}
protected:
T* out_;
const scc_map& sm_;
const std::vector<bool>& useless_;
};
template<class T>
class filter_iter: public tgba_reachable_iterator_depth_first
{
public:
typedef T output_t;
typedef std::map<int, bdd> map_t;
typedef std::vector<map_t> remap_t;
filter_iter(const tgba* a,
const scc_map& sm,
const std::vector<bool>& useless,
remap_table_t& remap_table,
unsigned max_num,
bool remove_all_useless)
: tgba_reachable_iterator_depth_first(a),
out_(new T(a->get_dict())),
sm_(sm),
useless_(useless),
all_(remove_all_useless),
acc_(max_num)
{
acc_[0] = bddfalse;
bdd tmp = a->all_acceptance_conditions();
bdd_dict* d = a->get_dict();
assert(a->number_of_acceptance_conditions() >= max_num - 1);
if (tmp != bddfalse)
{
for (unsigned n = max_num - 1; n > 0; --n)
{
assert(tmp != bddfalse);
const ltl::formula* a = d->oneacc_to_formula(bdd_var(tmp));
out_->declare_acceptance_condition(a->clone());
tmp = bdd_low(tmp);
}
tmp = a->all_acceptance_conditions();
for (unsigned n = max_num - 1; n > 0; --n)
{
const ltl::formula* a = d->oneacc_to_formula(bdd_var(tmp));
acc_[n] = out_->get_acceptance_condition(a->clone());
tmp = bdd_low(tmp);
}
}
else
{
assert(max_num == 1);
}
unsigned c = sm.scc_count();
remap_.resize(c);
bdd all_orig_neg = aut_->neg_acceptance_conditions();
bdd all_sup = bdd_support(all_orig_neg);
for (unsigned n = 0; n < c; ++n)
{
//std::cerr << "SCC #" << n << '\n';
if (!sm.accepting(n))
continue;
bdd all = sm.useful_acc_of(n);
while (all != bddfalse)
{
bdd one = bdd_satoneset(all, all_sup, bddtrue);
all -= one;
bdd res = bddfalse;
bdd resacc = bddfalse;
while (one != bddtrue)
{
if (bdd_high(one) == bddfalse)
{
one = bdd_low(one);
continue;
}
int vn = bdd_var(one);
bdd v = bdd_ithvar(vn);
resacc |= bdd_exist(all_orig_neg, v) & v;
res |= acc_[remap_table[n][vn]];
one = bdd_high(one);
}
int id = resacc.id();
//std::cerr << resacc << " -> " << res << '\n';
remap_[n][id] = res;
}
}
}
T*
result()
{
return out_;
}
bool
want_state(const state* s) const
{
return !useless_[sm_.scc_of_state(s)];
}
void
process_link(const state* in_s, int in,
const state* out_s, int out,
const tgba_succ_iterator* si)
{
typename output_t::state::transition* t =
create_transition(this->aut_, out_, in_s, in, out_s, out);
out_->add_conditions(t, si->current_condition());
// Regardless of all_, do not output any acceptance condition
// if the destination is not in an accepting SCC.
//
// If all_ is set, do not output any acceptance condition if the
// source is not in the same SCC as dest.
//
// (See the documentation of scc_filter() for a rational.)
unsigned u = sm_.scc_of_state(out_s);
unsigned v = sm_.scc_of_state(in_s);
if (sm_.accepting(u) && (!all_ || u == v))
{
bdd acc = si->current_acceptance_conditions();
if (acc == bddfalse)
return;
map_t::const_iterator i = this->remap_[u].find(acc.id());
if (i != this->remap_[u].end())
{
t->acceptance_conditions = i->second;
}
else
{
//t->acceptance_conditions = this->remap_[v][acc.id()];
}
}
}
protected:
T* out_;
const scc_map& sm_;
const std::vector<bool>& useless_;
bool all_;
std::vector<bdd> acc_;
remap_t remap_;
};
} // anonymous
tgba* scc_filter(const tgba* aut, bool remove_all_useless,
scc_map* given_sm)
{
scc_map* sm = given_sm;
if (!sm)
{
sm = new scc_map(aut);
sm->build_map();
}
scc_stats ss = build_scc_stats(*sm);
remap_table_t remap_table(ss.scc_total);
std::vector<unsigned> max_table(ss.scc_total);
std::vector<bdd> useful_table(ss.scc_total);
std::vector<bdd> useless_table(ss.scc_total);
unsigned max_num = 1;
for (unsigned n = 0; n < ss.scc_total; ++n)
{
if (!sm->accepting(n))
continue;
bdd all = sm->useful_acc_of(n);
bdd negall = aut->neg_acceptance_conditions();
//std::cerr << "SCC #" << n << "; used = " << all << std::endl;
// Compute a set of useless acceptance sets.
// If the acceptance combinations occurring in
// the automata are { a, ab, abc, bd }, then
// ALL contains (a&!b&!c&!d)|(a&b&!c&!d)|(a&b&c&!d)|(!a&b&!c&d)
// and we want to find that 'a' and 'b' are useless because
// they always occur with 'c'.
// The way we check if 'a' is useless is to look whether ALL
// implies (x -> a) for some other acceptance set x.
//
// The two while() loops in the code perform the equivalent of
// for all a in allconds_a:
// for all x in allconds_x:
// check whether x -> a
// ...