active -Wsuggest-override where supported
* m4/gccwarn.m4: Add the option. * bin/autfilt.cc, bin/common_output.hh, bin/dstar2tgba.cc, bin/ltl2tgba.cc, bin/ltl2tgta.cc, bin/ltlcross.cc, bin/ltldo.cc, bin/ltlfilt.cc, bin/ltlgrind.cc, spot/kripke/kripke.hh, spot/ltsmin/ltsmin.cc, spot/ta/ta.hh, spot/ta/tgtaproduct.hh, spot/taalgos/dot.cc, spot/taalgos/reachiter.hh, spot/taalgos/statessetbuilder.cc, spot/taalgos/stats.cc, spot/twa/twaproduct.cc, spot/twaalgos/emptiness.cc, spot/twaalgos/gtec/ce.cc, spot/twaalgos/lbtt.cc, spot/twaalgos/ndfs_result.hxx, spot/twaalgos/stats.hh, spot/twaalgos/tau03opt.cc, tests/core/ngraph.cc: Add suggested override qualifiers.
This commit is contained in:
parent
da464d8199
commit
64c7036660
26 changed files with 84 additions and 94 deletions
|
|
@ -813,7 +813,7 @@ namespace
|
||||||
}
|
}
|
||||||
|
|
||||||
int
|
int
|
||||||
process_formula(spot::formula, const char*, int)
|
process_formula(spot::formula, const char*, int) override
|
||||||
{
|
{
|
||||||
SPOT_UNREACHABLE();
|
SPOT_UNREACHABLE();
|
||||||
}
|
}
|
||||||
|
|
@ -1066,7 +1066,7 @@ namespace
|
||||||
}
|
}
|
||||||
|
|
||||||
int
|
int
|
||||||
process_file(const char* filename)
|
process_file(const char* filename) override
|
||||||
{
|
{
|
||||||
auto hp = spot::automaton_stream_parser(filename, opt_parse);
|
auto hp = spot::automaton_stream_parser(filename, opt_parse);
|
||||||
int err = 0;
|
int err = 0;
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
|
// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche
|
||||||
// Développement de l'Epita (LRDE).
|
// et Développement de l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
//
|
//
|
||||||
|
|
@ -63,7 +63,7 @@ public:
|
||||||
}
|
}
|
||||||
|
|
||||||
virtual void
|
virtual void
|
||||||
print(std::ostream& os, const char*) const;
|
print(std::ostream& os, const char*) const override;
|
||||||
};
|
};
|
||||||
|
|
||||||
class aut_stat_printer: protected spot::stat_printer
|
class aut_stat_printer: protected spot::stat_printer
|
||||||
|
|
|
||||||
|
|
@ -118,7 +118,7 @@ namespace
|
||||||
}
|
}
|
||||||
|
|
||||||
int
|
int
|
||||||
process_formula(spot::formula, const char*, int)
|
process_formula(spot::formula, const char*, int) override
|
||||||
{
|
{
|
||||||
SPOT_UNREACHABLE();
|
SPOT_UNREACHABLE();
|
||||||
}
|
}
|
||||||
|
|
@ -146,7 +146,7 @@ namespace
|
||||||
}
|
}
|
||||||
|
|
||||||
int
|
int
|
||||||
process_file(const char* filename)
|
process_file(const char* filename) override
|
||||||
{
|
{
|
||||||
auto hp = spot::automaton_stream_parser(filename, opt_parse);
|
auto hp = spot::automaton_stream_parser(filename, opt_parse);
|
||||||
int err = 0;
|
int err = 0;
|
||||||
|
|
|
||||||
|
|
@ -125,7 +125,7 @@ namespace
|
||||||
|
|
||||||
int
|
int
|
||||||
process_formula(spot::formula f,
|
process_formula(spot::formula f,
|
||||||
const char* filename = nullptr, int linenum = 0)
|
const char* filename = nullptr, int linenum = 0) override
|
||||||
{
|
{
|
||||||
// This should not happen, because the parser we use can only
|
// This should not happen, because the parser we use can only
|
||||||
// read PSL/LTL formula, but since our formula type can
|
// read PSL/LTL formula, but since our formula type can
|
||||||
|
|
|
||||||
|
|
@ -175,7 +175,7 @@ namespace
|
||||||
|
|
||||||
int
|
int
|
||||||
process_formula(spot::formula f,
|
process_formula(spot::formula f,
|
||||||
const char* filename = nullptr, int linenum = 0)
|
const char* filename = nullptr, int linenum = 0) override
|
||||||
{
|
{
|
||||||
auto aut = trans.run(&f);
|
auto aut = trans.run(&f);
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -826,7 +826,7 @@ namespace
|
||||||
int
|
int
|
||||||
process_string(const std::string& input,
|
process_string(const std::string& input,
|
||||||
const char* filename,
|
const char* filename,
|
||||||
int linenum)
|
int linenum) override
|
||||||
{
|
{
|
||||||
auto pf = parse_formula(input);
|
auto pf = parse_formula(input);
|
||||||
if (!pf.f || !pf.errors.empty())
|
if (!pf.f || !pf.errors.empty())
|
||||||
|
|
@ -928,7 +928,7 @@ namespace
|
||||||
|
|
||||||
int
|
int
|
||||||
process_formula(spot::formula f,
|
process_formula(spot::formula f,
|
||||||
const char* filename = nullptr, int linenum = 0)
|
const char* filename = nullptr, int linenum = 0) override
|
||||||
{
|
{
|
||||||
static unsigned round = 0;
|
static unsigned round = 0;
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -274,7 +274,7 @@ namespace
|
||||||
int
|
int
|
||||||
process_string(const std::string& input,
|
process_string(const std::string& input,
|
||||||
const char* filename,
|
const char* filename,
|
||||||
int linenum)
|
int linenum) override
|
||||||
{
|
{
|
||||||
spot::parsed_formula pf = parse_formula(input);
|
spot::parsed_formula pf = parse_formula(input);
|
||||||
|
|
||||||
|
|
@ -294,7 +294,7 @@ namespace
|
||||||
|
|
||||||
int
|
int
|
||||||
process_formula(spot::formula f,
|
process_formula(spot::formula f,
|
||||||
const char* filename = nullptr, int linenum = 0)
|
const char* filename = nullptr, int linenum = 0) override
|
||||||
{
|
{
|
||||||
std::unique_ptr<spot::relabeling_map> relmap;
|
std::unique_ptr<spot::relabeling_map> relmap;
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -515,7 +515,7 @@ namespace
|
||||||
|
|
||||||
int
|
int
|
||||||
process_string(const std::string& input,
|
process_string(const std::string& input,
|
||||||
const char* filename = nullptr, int linenum = 0)
|
const char* filename = nullptr, int linenum = 0) override
|
||||||
{
|
{
|
||||||
spot::parsed_formula pf = parse_formula(input);
|
spot::parsed_formula pf = parse_formula(input);
|
||||||
|
|
||||||
|
|
@ -548,7 +548,7 @@ namespace
|
||||||
|
|
||||||
int
|
int
|
||||||
process_formula(spot::formula f,
|
process_formula(spot::formula f,
|
||||||
const char* filename = nullptr, int linenum = 0)
|
const char* filename = nullptr, int linenum = 0) override
|
||||||
{
|
{
|
||||||
if (opt_max_count >= 0 && match_count >= opt_max_count)
|
if (opt_max_count >= 0 && match_count >= opt_max_count)
|
||||||
{
|
{
|
||||||
|
|
|
||||||
|
|
@ -113,7 +113,7 @@ namespace
|
||||||
public:
|
public:
|
||||||
int
|
int
|
||||||
process_formula(spot::formula f, const char* filename = nullptr,
|
process_formula(spot::formula f, const char* filename = nullptr,
|
||||||
int linenum = 0)
|
int linenum = 0) override
|
||||||
{
|
{
|
||||||
auto mutations =
|
auto mutations =
|
||||||
spot::mutate(f, mut_opts, max_output, mutation_nb, opt_sort);
|
spot::mutate(f, mut_opts, max_output, mutation_nb, opt_sort);
|
||||||
|
|
|
||||||
|
|
@ -39,7 +39,8 @@ EOF
|
||||||
Wmisleading-indentation \
|
Wmisleading-indentation \
|
||||||
Wlogical-op \
|
Wlogical-op \
|
||||||
Wduplicated-cond \
|
Wduplicated-cond \
|
||||||
Wnull-dereference
|
Wnull-dereference \
|
||||||
|
Wsuggest-override
|
||||||
do
|
do
|
||||||
CXXFLAGS="$cf_save_CXXFLAGS $ac_cv_prog_gxx_warn_flags -$cf_opt"
|
CXXFLAGS="$cf_save_CXXFLAGS $ac_cv_prog_gxx_warn_flags -$cf_opt"
|
||||||
if AC_TRY_EVAL(ac_compile); then
|
if AC_TRY_EVAL(ac_compile); then
|
||||||
|
|
|
||||||
|
|
@ -97,7 +97,8 @@ namespace spot
|
||||||
|
|
||||||
virtual ~kripke();
|
virtual ~kripke();
|
||||||
|
|
||||||
virtual acc_cond::mark_t state_acceptance_conditions(const state*) const;
|
virtual
|
||||||
|
acc_cond::mark_t state_acceptance_conditions(const state*) const override;
|
||||||
};
|
};
|
||||||
|
|
||||||
typedef std::shared_ptr<kripke> kripke_ptr;
|
typedef std::shared_ptr<kripke> kripke_ptr;
|
||||||
|
|
|
||||||
|
|
@ -84,7 +84,7 @@ namespace spot
|
||||||
////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////
|
||||||
// STATE
|
// STATE
|
||||||
|
|
||||||
struct spins_state: public state
|
struct spins_state final: public state
|
||||||
{
|
{
|
||||||
spins_state(int s, fixed_size_pool* p)
|
spins_state(int s, fixed_size_pool* p)
|
||||||
: pool(p), size(s), count(1)
|
: pool(p), size(s), count(1)
|
||||||
|
|
@ -98,25 +98,25 @@ namespace spot
|
||||||
hash_value = wang32_hash(hash_value ^ vars[i]);
|
hash_value = wang32_hash(hash_value ^ vars[i]);
|
||||||
}
|
}
|
||||||
|
|
||||||
spins_state* clone() const
|
spins_state* clone() const override
|
||||||
{
|
{
|
||||||
++count;
|
++count;
|
||||||
return const_cast<spins_state*>(this);
|
return const_cast<spins_state*>(this);
|
||||||
}
|
}
|
||||||
|
|
||||||
void destroy() const
|
void destroy() const override
|
||||||
{
|
{
|
||||||
if (--count)
|
if (--count)
|
||||||
return;
|
return;
|
||||||
pool->deallocate(this);
|
pool->deallocate(this);
|
||||||
}
|
}
|
||||||
|
|
||||||
size_t hash() const
|
size_t hash() const override
|
||||||
{
|
{
|
||||||
return hash_value;
|
return hash_value;
|
||||||
}
|
}
|
||||||
|
|
||||||
int compare(const state* other) const
|
int compare(const state* other) const override
|
||||||
{
|
{
|
||||||
if (this == other)
|
if (this == other)
|
||||||
return 0;
|
return 0;
|
||||||
|
|
@ -143,7 +143,7 @@ namespace spot
|
||||||
int vars[0];
|
int vars[0];
|
||||||
};
|
};
|
||||||
|
|
||||||
struct spins_compressed_state: public state
|
struct spins_compressed_state final: public state
|
||||||
{
|
{
|
||||||
spins_compressed_state(int s, multiple_size_pool* p)
|
spins_compressed_state(int s, multiple_size_pool* p)
|
||||||
: pool(p), size(s), count(1)
|
: pool(p), size(s), count(1)
|
||||||
|
|
@ -157,25 +157,25 @@ namespace spot
|
||||||
hash_value = wang32_hash(hash_value ^ vars[i]);
|
hash_value = wang32_hash(hash_value ^ vars[i]);
|
||||||
}
|
}
|
||||||
|
|
||||||
spins_compressed_state* clone() const
|
spins_compressed_state* clone() const override
|
||||||
{
|
{
|
||||||
++count;
|
++count;
|
||||||
return const_cast<spins_compressed_state*>(this);
|
return const_cast<spins_compressed_state*>(this);
|
||||||
}
|
}
|
||||||
|
|
||||||
void destroy() const
|
void destroy() const override
|
||||||
{
|
{
|
||||||
if (--count)
|
if (--count)
|
||||||
return;
|
return;
|
||||||
pool->deallocate(this, sizeof(*this) + size * sizeof(*vars));
|
pool->deallocate(this, sizeof(*this) + size * sizeof(*vars));
|
||||||
}
|
}
|
||||||
|
|
||||||
size_t hash() const
|
size_t hash() const override
|
||||||
{
|
{
|
||||||
return hash_value;
|
return hash_value;
|
||||||
}
|
}
|
||||||
|
|
||||||
int compare(const state* other) const
|
int compare(const state* other) const override
|
||||||
{
|
{
|
||||||
if (this == other)
|
if (this == other)
|
||||||
return 0;
|
return 0;
|
||||||
|
|
|
||||||
|
|
@ -201,10 +201,6 @@ namespace spot
|
||||||
~ta_succ_iterator()
|
~ta_succ_iterator()
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
/// \brief Get the changeset on the transition leading to current successor.
|
|
||||||
///
|
|
||||||
/// This is a boolean function of atomic propositions.
|
|
||||||
virtual bdd cond() const = 0;
|
|
||||||
};
|
};
|
||||||
|
|
||||||
#ifndef SWIG
|
#ifndef SWIG
|
||||||
|
|
|
||||||
|
|
@ -60,18 +60,14 @@ namespace spot
|
||||||
~tgta_succ_iterator_product();
|
~tgta_succ_iterator_product();
|
||||||
|
|
||||||
// iteration
|
// iteration
|
||||||
bool first();
|
bool first() override;
|
||||||
bool next();
|
bool next() override;
|
||||||
bool done() const;
|
bool done() const override;
|
||||||
|
|
||||||
// inspection
|
// inspection
|
||||||
state_product*
|
state_product* dst() const override;
|
||||||
dst() const;
|
bdd cond() const override;
|
||||||
bdd
|
acc_cond::mark_t acc() const override;
|
||||||
cond() const;
|
|
||||||
|
|
||||||
acc_cond::mark_t
|
|
||||||
acc() const;
|
|
||||||
|
|
||||||
private:
|
private:
|
||||||
//@{
|
//@{
|
||||||
|
|
|
||||||
|
|
@ -141,7 +141,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
void
|
void
|
||||||
start()
|
start() override
|
||||||
{
|
{
|
||||||
os_ << "digraph G {\n";
|
os_ << "digraph G {\n";
|
||||||
|
|
||||||
|
|
@ -198,13 +198,13 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
void
|
void
|
||||||
end()
|
end() override
|
||||||
{
|
{
|
||||||
os_ << '}' << std::endl;
|
os_ << '}' << std::endl;
|
||||||
}
|
}
|
||||||
|
|
||||||
void
|
void
|
||||||
process_state(const state* s, int n)
|
process_state(const state* s, int n) override
|
||||||
{
|
{
|
||||||
|
|
||||||
std::string style;
|
std::string style;
|
||||||
|
|
@ -223,7 +223,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
void
|
void
|
||||||
process_link(int in, int out, const ta_succ_iterator* si)
|
process_link(int in, int out, const ta_succ_iterator* si) override
|
||||||
{
|
{
|
||||||
bdd_dict_ptr d = t_automata_->get_dict();
|
bdd_dict_ptr d = t_automata_->get_dict();
|
||||||
std::string label =
|
std::string label =
|
||||||
|
|
|
||||||
|
|
@ -100,10 +100,8 @@ namespace spot
|
||||||
public:
|
public:
|
||||||
ta_reachable_iterator_depth_first(const const_ta_ptr& a);
|
ta_reachable_iterator_depth_first(const const_ta_ptr& a);
|
||||||
|
|
||||||
virtual void
|
virtual void add_state(const state* s) override;
|
||||||
add_state(const state* s);
|
virtual const state* next_state() override;
|
||||||
virtual const state*
|
|
||||||
next_state();
|
|
||||||
|
|
||||||
protected:
|
protected:
|
||||||
std::stack<const state*> todo; ///< A stack of states yet to explore.
|
std::stack<const state*> todo; ///< A stack of states yet to explore.
|
||||||
|
|
@ -118,10 +116,8 @@ namespace spot
|
||||||
public:
|
public:
|
||||||
ta_reachable_iterator_breadth_first(const const_ta_ptr& a);
|
ta_reachable_iterator_breadth_first(const const_ta_ptr& a);
|
||||||
|
|
||||||
virtual void
|
virtual void add_state(const state* s) override;
|
||||||
add_state(const state* s);
|
virtual const state* next_state() override;
|
||||||
virtual const state*
|
|
||||||
next_state();
|
|
||||||
|
|
||||||
protected:
|
protected:
|
||||||
std::deque<const state*> todo; ///< A queue of states yet to explore.
|
std::deque<const state*> todo; ///< A queue of states yet to explore.
|
||||||
|
|
|
||||||
|
|
@ -36,13 +36,13 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
void
|
void
|
||||||
process_state(const state* s, int)
|
process_state(const state* s, int) override
|
||||||
{
|
{
|
||||||
states_set_.insert(s);
|
states_set_.insert(s);
|
||||||
}
|
}
|
||||||
|
|
||||||
void
|
void
|
||||||
process_link(int, int, const ta_succ_iterator*)
|
process_link(int, int, const ta_succ_iterator*) override
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -38,7 +38,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
void
|
void
|
||||||
process_state(const state* s, int)
|
process_state(const state* s, int) override
|
||||||
{
|
{
|
||||||
++s_.states;
|
++s_.states;
|
||||||
if (t_automata_->is_accepting_state(s)
|
if (t_automata_->is_accepting_state(s)
|
||||||
|
|
@ -47,7 +47,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
void
|
void
|
||||||
process_link(int, int, const ta_succ_iterator*)
|
process_link(int, int, const ta_succ_iterator*) override
|
||||||
{
|
{
|
||||||
++s_.edges;
|
++s_.edges;
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -107,7 +107,7 @@ namespace spot
|
||||||
|
|
||||||
virtual bool next_non_false_() = 0;
|
virtual bool next_non_false_() = 0;
|
||||||
|
|
||||||
bool first()
|
bool first() override
|
||||||
{
|
{
|
||||||
if (!right_)
|
if (!right_)
|
||||||
return false;
|
return false;
|
||||||
|
|
@ -125,12 +125,12 @@ namespace spot
|
||||||
return next_non_false_();
|
return next_non_false_();
|
||||||
}
|
}
|
||||||
|
|
||||||
bool done() const
|
bool done() const override
|
||||||
{
|
{
|
||||||
return !right_ || right_->done();
|
return !right_ || right_->done();
|
||||||
}
|
}
|
||||||
|
|
||||||
const state_product* dst() const
|
const state_product* dst() const override
|
||||||
{
|
{
|
||||||
return new(pool_->allocate()) state_product(left_->dst(),
|
return new(pool_->allocate()) state_product(left_->dst(),
|
||||||
right_->dst(),
|
right_->dst(),
|
||||||
|
|
@ -171,7 +171,7 @@ namespace spot
|
||||||
return right_->next();
|
return right_->next();
|
||||||
}
|
}
|
||||||
|
|
||||||
bool next_non_false_()
|
bool next_non_false_() override
|
||||||
{
|
{
|
||||||
assert(!done());
|
assert(!done());
|
||||||
do
|
do
|
||||||
|
|
@ -190,19 +190,19 @@ namespace spot
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
bool next()
|
bool next() override
|
||||||
{
|
{
|
||||||
if (step_())
|
if (step_())
|
||||||
return next_non_false_();
|
return next_non_false_();
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
bdd cond() const
|
bdd cond() const override
|
||||||
{
|
{
|
||||||
return current_cond_;
|
return current_cond_;
|
||||||
}
|
}
|
||||||
|
|
||||||
acc_cond::mark_t acc() const
|
acc_cond::mark_t acc() const override
|
||||||
{
|
{
|
||||||
return left_->acc() | (right_->acc() << prod_->left_acc().num_sets());
|
return left_->acc() | (right_->acc() << prod_->left_acc().num_sets());
|
||||||
}
|
}
|
||||||
|
|
@ -229,7 +229,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
bool next_non_false_()
|
bool next_non_false_() override
|
||||||
{
|
{
|
||||||
// All the transitions of left_ iterator have the
|
// All the transitions of left_ iterator have the
|
||||||
// same label, because it is a Kripke structure.
|
// same label, because it is a Kripke structure.
|
||||||
|
|
@ -250,7 +250,7 @@ namespace spot
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
bool next()
|
bool next() override
|
||||||
{
|
{
|
||||||
if (left_->next())
|
if (left_->next())
|
||||||
return true;
|
return true;
|
||||||
|
|
@ -260,12 +260,12 @@ namespace spot
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
bdd cond() const
|
bdd cond() const override
|
||||||
{
|
{
|
||||||
return current_cond_;
|
return current_cond_;
|
||||||
}
|
}
|
||||||
|
|
||||||
acc_cond::mark_t acc() const
|
acc_cond::mark_t acc() const override
|
||||||
{
|
{
|
||||||
return right_->acc();
|
return right_->acc();
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -313,7 +313,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
const state*
|
const state*
|
||||||
filter(const state* s)
|
filter(const state* s) override
|
||||||
{
|
{
|
||||||
state_set::const_iterator i = seen.find(s);
|
state_set::const_iterator i = seen.find(s);
|
||||||
if (i == seen.end())
|
if (i == seen.end())
|
||||||
|
|
@ -327,7 +327,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
bool
|
bool
|
||||||
match(twa_run::step&, const state* dest)
|
match(twa_run::step&, const state* dest) override
|
||||||
{
|
{
|
||||||
return target->find(dest) != target->end();
|
return target->find(dest) != target->end();
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -45,7 +45,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
const state*
|
const state*
|
||||||
filter(const state* s)
|
filter(const state* s) override
|
||||||
{
|
{
|
||||||
r->inc_ars_prefix_states();
|
r->inc_ars_prefix_states();
|
||||||
auto i = ecs->h.find(s);
|
auto i = ecs->h.find(s);
|
||||||
|
|
@ -60,7 +60,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
bool
|
bool
|
||||||
match(twa_run::step&, const state* dest)
|
match(twa_run::step&, const state* dest) override
|
||||||
{
|
{
|
||||||
return target->find(dest) != target->end();
|
return target->find(dest) != target->end();
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -74,7 +74,7 @@ namespace spot
|
||||||
|
|
||||||
|
|
||||||
void
|
void
|
||||||
process_state(const state* s, int n, twa_succ_iterator*)
|
process_state(const state* s, int n, twa_succ_iterator*) override
|
||||||
{
|
{
|
||||||
--n;
|
--n;
|
||||||
if (n == 0)
|
if (n == 0)
|
||||||
|
|
@ -93,7 +93,7 @@ namespace spot
|
||||||
|
|
||||||
void
|
void
|
||||||
process_link(const state*, int,
|
process_link(const state*, int,
|
||||||
const state*, int out, const twa_succ_iterator* si)
|
const state*, int out, const twa_succ_iterator* si) override
|
||||||
{
|
{
|
||||||
body_ << out - 1 << ' ';
|
body_ << out - 1 << ' ';
|
||||||
if (!sba_format_)
|
if (!sba_format_)
|
||||||
|
|
@ -107,7 +107,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
void
|
void
|
||||||
end()
|
end() override
|
||||||
{
|
{
|
||||||
os_ << seen.size() << ' ';
|
os_ << seen.size() << ' ';
|
||||||
if (sba_format_)
|
if (sba_format_)
|
||||||
|
|
|
||||||
|
|
@ -398,7 +398,7 @@ namespace spot
|
||||||
return nullptr;
|
return nullptr;
|
||||||
}
|
}
|
||||||
|
|
||||||
const state* filter(const state* s)
|
const state* filter(const state* s) override
|
||||||
{
|
{
|
||||||
if (!h.has_been_visited(s)
|
if (!h.has_been_visited(s)
|
||||||
|| seen.find(s) != seen.end()
|
|| seen.find(s) != seen.end()
|
||||||
|
|
@ -412,9 +412,10 @@ namespace spot
|
||||||
return s;
|
return s;
|
||||||
}
|
}
|
||||||
|
|
||||||
void finalize(const std::map<const state*, twa_run::step,
|
void
|
||||||
state_ptr_less_than>&,
|
finalize(const std::map<const state*,
|
||||||
const twa_run::step&, const state*, twa_run::steps&)
|
twa_run::step, state_ptr_less_than>&,
|
||||||
|
const twa_run::step&, const state*, twa_run::steps&) override
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -423,7 +424,7 @@ namespace spot
|
||||||
return seen;
|
return seen;
|
||||||
}
|
}
|
||||||
|
|
||||||
bool match(twa_run::step&, const state* dest)
|
bool match(twa_run::step&, const state* dest) override
|
||||||
{
|
{
|
||||||
return target->compare(dest) == 0;
|
return target->compare(dest) == 0;
|
||||||
}
|
}
|
||||||
|
|
@ -493,7 +494,7 @@ namespace spot
|
||||||
return nullptr;
|
return nullptr;
|
||||||
}
|
}
|
||||||
|
|
||||||
const state* filter(const state* s)
|
const state* filter(const state* s) override
|
||||||
{
|
{
|
||||||
ndfsr_trace << "filter: " << a_->format_state(s);
|
ndfsr_trace << "filter: " << a_->format_state(s);
|
||||||
if (!h.has_been_visited(s) || seen.find(s) != seen.end())
|
if (!h.has_been_visited(s) || seen.find(s) != seen.end())
|
||||||
|
|
@ -514,7 +515,7 @@ namespace spot
|
||||||
return s;
|
return s;
|
||||||
}
|
}
|
||||||
|
|
||||||
bool match(twa_run::step&, const state* dest)
|
bool match(twa_run::step&, const state* dest) override
|
||||||
{
|
{
|
||||||
ndfsr_trace << "match: " << a_->format_state(dest)
|
ndfsr_trace << "match: " << a_->format_state(dest)
|
||||||
<< std::endl;
|
<< std::endl;
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2008, 2011, 2012, 2013, 2014, 2015 Laboratoire de
|
// Copyright (C) 2008, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de
|
||||||
// Recherche et Développement de l'Epita (LRDE).
|
// Recherche et Développement de l'Epita (LRDE).
|
||||||
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||||
|
|
@ -66,7 +66,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
virtual void
|
virtual void
|
||||||
print(std::ostream& os, const char*) const;
|
print(std::ostream& os, const char*) const override;
|
||||||
};
|
};
|
||||||
|
|
||||||
/// \brief prints various statistics about a TGBA
|
/// \brief prints various statistics about a TGBA
|
||||||
|
|
|
||||||
|
|
@ -97,7 +97,7 @@ namespace spot
|
||||||
///
|
///
|
||||||
/// \return non null pointer iff the algorithm has found an
|
/// \return non null pointer iff the algorithm has found an
|
||||||
/// accepting path.
|
/// accepting path.
|
||||||
virtual emptiness_check_result_ptr check()
|
virtual emptiness_check_result_ptr check() override
|
||||||
{
|
{
|
||||||
if (!st_blue.empty())
|
if (!st_blue.empty())
|
||||||
return nullptr;
|
return nullptr;
|
||||||
|
|
@ -113,7 +113,7 @@ namespace spot
|
||||||
return nullptr;
|
return nullptr;
|
||||||
}
|
}
|
||||||
|
|
||||||
virtual std::ostream& print_stats(std::ostream &os) const
|
virtual std::ostream& print_stats(std::ostream &os) const override
|
||||||
{
|
{
|
||||||
os << states() << " distinct nodes visited" << std::endl;
|
os << states() << " distinct nodes visited" << std::endl;
|
||||||
os << transitions() << " transitions explored" << std::endl;
|
os << transitions() << " transitions explored" << std::endl;
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
|
// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et
|
||||||
// de l'Epita.
|
// Développement de l'Epita.
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
//
|
//
|
||||||
|
|
@ -347,7 +347,7 @@ public:
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
virtual int compare(const spot::state* other) const
|
int compare(const spot::state* other) const override
|
||||||
{
|
{
|
||||||
auto o = down_cast<const my_state*>(other);
|
auto o = down_cast<const my_state*>(other);
|
||||||
assert(o);
|
assert(o);
|
||||||
|
|
@ -360,19 +360,18 @@ public:
|
||||||
return 0;
|
return 0;
|
||||||
}
|
}
|
||||||
|
|
||||||
virtual size_t hash() const
|
size_t hash() const override
|
||||||
{
|
{
|
||||||
return
|
return
|
||||||
reinterpret_cast<const char*>(this) - static_cast<const char*>(nullptr);
|
reinterpret_cast<const char*>(this) - static_cast<const char*>(nullptr);
|
||||||
}
|
}
|
||||||
|
|
||||||
virtual my_state*
|
my_state* clone() const override
|
||||||
clone() const
|
|
||||||
{
|
{
|
||||||
return const_cast<my_state*>(this);
|
return const_cast<my_state*>(this);
|
||||||
}
|
}
|
||||||
|
|
||||||
virtual void destroy() const
|
void destroy() const override
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue