use more override and final keywords
This patch is mostly focused on tagging most virtual methods that override as such. I found a few methods that where not meant to be virtual this way, and tagged a few classes "final" along the way. * bin/common_output.cc, spot/kripke/fairkripke.hh, spot/kripke/kripke.hh, spot/kripke/kripkegraph.hh, spot/ltsmin/ltsmin.cc, spot/misc/formater.hh, spot/priv/bddalloc.hh, spot/ta/ta.hh, spot/ta/taexplicit.hh, spot/ta/taproduct.hh, spot/ta/tgta.hh, spot/ta/tgtaexplicit.cc, spot/ta/tgtaexplicit.hh, spot/ta/tgtaproduct.hh, spot/taalgos/emptinessta.hh, spot/tl/declenv.hh, spot/tl/defaultenv.hh, spot/tl/randomltl.hh, spot/tl/relabel.cc, spot/twa/bdddict.cc, spot/twa/taatgba.hh, spot/twa/twagraph.hh, spot/twa/twaproduct.hh, spot/twaalgos/gtec/ce.cc, spot/twaalgos/gtec/ce.hh, spot/twaalgos/gtec/gtec.hh, spot/twaalgos/gv04.cc, spot/twaalgos/ltl2taa.cc, spot/twaalgos/magic.cc, spot/twaalgos/minimize.cc, spot/twaalgos/ndfs_result.hxx, spot/twaalgos/reachiter.hh, spot/twaalgos/se05.cc, spot/twaalgos/stutter.cc, spot/twaalgos/tau03.cc: Add more override and final keywords.
This commit is contained in:
Alexandre Duret-Lutz
parent
1ae0600cae
commit
5d272fd256
35 changed files with 249 additions and 291 deletions
|
|
@ -1,5 +1,5 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
|
||||
// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE).
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
|
|
@ -165,7 +165,7 @@ namespace
|
|||
}
|
||||
|
||||
virtual void
|
||||
print(std::ostream& os, const char*) const
|
||||
print(std::ostream& os, const char*) const override
|
||||
{
|
||||
stream_escapable_formula(os, val_->f, val_->filename, val_->line);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -54,8 +54,8 @@ namespace spot
|
|||
fair_kripke_succ_iterator(const bdd& cond, acc_cond::mark_t acc_cond);
|
||||
virtual ~fair_kripke_succ_iterator();
|
||||
|
||||
virtual bdd cond() const;
|
||||
virtual acc_cond::mark_t acc() const;
|
||||
virtual bdd cond() const override;
|
||||
virtual acc_cond::mark_t acc() const override;
|
||||
protected:
|
||||
bdd cond_;
|
||||
acc_cond::mark_t acc_cond_;
|
||||
|
|
|
|||
|
|
@ -59,8 +59,8 @@ namespace spot
|
|||
|
||||
virtual ~kripke_succ_iterator();
|
||||
|
||||
virtual bdd cond() const;
|
||||
virtual acc_cond::mark_t acc() const;
|
||||
virtual bdd cond() const override;
|
||||
virtual acc_cond::mark_t acc() const override;
|
||||
protected:
|
||||
bdd cond_;
|
||||
};
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2011, 2012, 2013, 2014, 2015 Laboratoire de Recherche
|
||||
// et Développement de l'Epita (LRDE)
|
||||
// Copyright (C) 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de
|
||||
// Recherche et Développement de l'Epita (LRDE)
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
//
|
||||
|
|
@ -39,7 +39,7 @@ namespace spot
|
|||
{
|
||||
}
|
||||
|
||||
virtual int compare(const spot::state* other) const
|
||||
virtual int compare(const spot::state* other) const override
|
||||
{
|
||||
auto o = down_cast<const kripke_graph_state*>(other);
|
||||
assert(o);
|
||||
|
|
@ -52,19 +52,19 @@ namespace spot
|
|||
return 0;
|
||||
}
|
||||
|
||||
virtual size_t hash() const
|
||||
virtual size_t hash() const override
|
||||
{
|
||||
return
|
||||
reinterpret_cast<const char*>(this) - static_cast<const char*>(nullptr);
|
||||
}
|
||||
|
||||
virtual kripke_graph_state*
|
||||
clone() const
|
||||
clone() const override
|
||||
{
|
||||
return const_cast<kripke_graph_state*>(this);
|
||||
}
|
||||
|
||||
virtual void destroy() const
|
||||
virtual void destroy() const override
|
||||
{
|
||||
}
|
||||
|
||||
|
|
@ -104,30 +104,30 @@ namespace spot
|
|||
{
|
||||
}
|
||||
|
||||
virtual void recycle(const typename Graph::state_storage_t* s)
|
||||
void recycle(const typename Graph::state_storage_t* s)
|
||||
{
|
||||
cond_ = s->cond();
|
||||
t_ = s->succ;
|
||||
}
|
||||
|
||||
virtual bool first()
|
||||
virtual bool first() override
|
||||
{
|
||||
p_ = t_;
|
||||
return p_;
|
||||
}
|
||||
|
||||
virtual bool next()
|
||||
virtual bool next() override
|
||||
{
|
||||
p_ = g_->edge_storage(p_).next_succ;
|
||||
return p_;
|
||||
}
|
||||
|
||||
virtual bool done() const
|
||||
virtual bool done() const override
|
||||
{
|
||||
return !p_;
|
||||
}
|
||||
|
||||
virtual kripke_graph_state* dst() const
|
||||
virtual kripke_graph_state* dst() const override
|
||||
{
|
||||
assert(!done());
|
||||
return const_cast<kripke_graph_state*>
|
||||
|
|
@ -138,7 +138,7 @@ namespace spot
|
|||
|
||||
/// \class kripke_graph
|
||||
/// \brief Kripke Structure.
|
||||
class SPOT_API kripke_graph : public kripke
|
||||
class SPOT_API kripke_graph final : public kripke
|
||||
{
|
||||
public:
|
||||
typedef digraph<kripke_graph_state, void> graph_t;
|
||||
|
|
@ -180,7 +180,7 @@ namespace spot
|
|||
return init_number_;
|
||||
}
|
||||
|
||||
virtual const kripke_graph_state* get_init_state() const
|
||||
virtual const kripke_graph_state* get_init_state() const override
|
||||
{
|
||||
if (num_states() == 0)
|
||||
const_cast<graph_t&>(g_).new_state();
|
||||
|
|
@ -190,7 +190,7 @@ namespace spot
|
|||
/// \brief Allow to get an iterator on the state we passed in
|
||||
/// parameter.
|
||||
virtual kripke_graph_succ_iterator<graph_t>*
|
||||
succ_iter(const spot::state* st) const
|
||||
succ_iter(const spot::state* st) const override
|
||||
{
|
||||
auto s = down_cast<const typename graph_t::state_storage_t*>(st);
|
||||
assert(s);
|
||||
|
|
@ -235,13 +235,13 @@ namespace spot
|
|||
return ss.str();
|
||||
}
|
||||
|
||||
virtual std::string format_state(const state* st) const
|
||||
virtual std::string format_state(const state* st) const override
|
||||
{
|
||||
return format_state(state_number(st));
|
||||
}
|
||||
|
||||
/// \brief Get the condition on the state
|
||||
virtual bdd state_condition(const state* s) const
|
||||
virtual bdd state_condition(const state* s) const override
|
||||
{
|
||||
return down_cast<const kripke_graph_state*>(s)->cond();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -258,7 +258,7 @@ namespace spot
|
|||
////////////////////////////////////////////////////////////////////////
|
||||
// SUCC_ITERATOR
|
||||
|
||||
class spins_succ_iterator: public kripke_succ_iterator
|
||||
class spins_succ_iterator final: public kripke_succ_iterator
|
||||
{
|
||||
public:
|
||||
|
||||
|
|
@ -280,28 +280,24 @@ namespace spot
|
|||
delete cc_;
|
||||
}
|
||||
|
||||
virtual
|
||||
bool first()
|
||||
virtual bool first() override
|
||||
{
|
||||
it_ = cc_->transitions.begin();
|
||||
return it_ != cc_->transitions.end();
|
||||
}
|
||||
|
||||
virtual
|
||||
bool next()
|
||||
virtual bool next() override
|
||||
{
|
||||
++it_;
|
||||
return it_ != cc_->transitions.end();
|
||||
}
|
||||
|
||||
virtual
|
||||
bool done() const
|
||||
virtual bool done() const override
|
||||
{
|
||||
return it_ == cc_->transitions.end();
|
||||
}
|
||||
|
||||
virtual
|
||||
state* dst() const
|
||||
virtual state* dst() const override
|
||||
{
|
||||
return (*it_)->clone();
|
||||
}
|
||||
|
|
@ -605,7 +601,7 @@ namespace spot
|
|||
////////////////////////////////////////////////////////////////////////
|
||||
// KRIPKE
|
||||
|
||||
class spins_kripke: public kripke
|
||||
class spins_kripke final: public kripke
|
||||
{
|
||||
public:
|
||||
|
||||
|
|
@ -615,7 +611,7 @@ namespace spot
|
|||
: kripke(dict),
|
||||
d_(d),
|
||||
state_size_(d_->get_state_size()),
|
||||
dict_(dict), ps_(ps),
|
||||
ps_(ps),
|
||||
compress_(compress == 0 ? nullptr
|
||||
: compress == 1 ? int_array_array_compress
|
||||
: int_array_array_compress2),
|
||||
|
|
@ -696,8 +692,7 @@ namespace spot
|
|||
delete state_condition_last_cc_; // Might be 0 already.
|
||||
}
|
||||
|
||||
virtual
|
||||
state* get_init_state() const
|
||||
virtual state* get_init_state() const override
|
||||
{
|
||||
if (compress_)
|
||||
{
|
||||
|
|
@ -848,8 +843,7 @@ namespace spot
|
|||
|
||||
|
||||
virtual
|
||||
spins_succ_iterator*
|
||||
succ_iter(const state* st) const
|
||||
spins_succ_iterator* succ_iter(const state* st) const override
|
||||
{
|
||||
// This may also compute successors in state_condition_last_cc
|
||||
bdd scond = compute_state_condition(st);
|
||||
|
|
@ -882,14 +876,13 @@ namespace spot
|
|||
}
|
||||
|
||||
virtual
|
||||
bdd
|
||||
state_condition(const state* st) const
|
||||
bdd state_condition(const state* st) const override
|
||||
{
|
||||
return compute_state_condition(st);
|
||||
}
|
||||
|
||||
virtual
|
||||
std::string format_state(const state *st) const
|
||||
std::string format_state(const state *st) const override
|
||||
{
|
||||
const int* vars = get_vars(st);
|
||||
|
||||
|
|
@ -917,16 +910,9 @@ namespace spot
|
|||
return res.str();
|
||||
}
|
||||
|
||||
virtual
|
||||
spot::bdd_dict_ptr get_dict() const
|
||||
{
|
||||
return dict_;
|
||||
}
|
||||
|
||||
private:
|
||||
spins_interface_ptr d_;
|
||||
int state_size_;
|
||||
bdd_dict_ptr dict_;
|
||||
const char** vname_;
|
||||
bool* format_filter_;
|
||||
const spot::prop_set* ps_;
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
|
||||
// de l'Epita (LRDE).
|
||||
// Copyright (C) 2012, 2013, 2016 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE).
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
//
|
||||
|
|
@ -72,7 +72,7 @@ namespace spot
|
|||
}
|
||||
|
||||
virtual void
|
||||
print(std::ostream& os, const char*) const
|
||||
print(std::ostream& os, const char*) const override
|
||||
{
|
||||
os << val_;
|
||||
}
|
||||
|
|
@ -83,7 +83,7 @@ namespace spot
|
|||
{
|
||||
public:
|
||||
virtual void
|
||||
print(std::ostream& os, const char* x) const
|
||||
print(std::ostream& os, const char* x) const override
|
||||
{
|
||||
os << '%' << *x;
|
||||
}
|
||||
|
|
@ -94,7 +94,7 @@ namespace spot
|
|||
{
|
||||
public:
|
||||
virtual void
|
||||
print(std::ostream& os, const char*) const
|
||||
print(std::ostream& os, const char*) const override
|
||||
{
|
||||
os << '%';
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2013 Laboratoire de Recherche et Développement
|
||||
// Copyright (C) 2013, 2016 Laboratoire de Recherche et Développement
|
||||
// de l'Epita (LRDE).
|
||||
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
|
|
@ -49,6 +49,6 @@ namespace spot
|
|||
private:
|
||||
/// Require more variables.
|
||||
void extvarnum(int more);
|
||||
virtual int extend(int n);
|
||||
virtual int extend(int n) override;
|
||||
};
|
||||
}
|
||||
|
|
|
|||
|
|
@ -201,20 +201,10 @@ namespace spot
|
|||
~ta_succ_iterator()
|
||||
{
|
||||
}
|
||||
|
||||
virtual bool first() = 0;
|
||||
virtual bool next() = 0;
|
||||
virtual bool done() const = 0;
|
||||
|
||||
virtual const state* dst() const = 0;
|
||||
|
||||
/// \brief Get the changeset on the transition leading to current successor.
|
||||
///
|
||||
/// This is a boolean function of atomic propositions.
|
||||
virtual bdd cond() const = 0;
|
||||
|
||||
acc_cond::mark_t acc() const = 0;
|
||||
|
||||
};
|
||||
|
||||
#ifndef SWIG
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de
|
||||
// Recherche et Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire
|
||||
// de Recherche et Développement de l'Epita (LRDE).
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
//
|
||||
|
|
@ -64,38 +64,35 @@ namespace spot
|
|||
// ta interface
|
||||
virtual
|
||||
~ta_explicit();
|
||||
virtual const_states_set_t
|
||||
get_initial_states_set() const;
|
||||
virtual const_states_set_t get_initial_states_set() const override;
|
||||
|
||||
virtual ta_succ_iterator* succ_iter(const spot::state* s) const override;
|
||||
|
||||
virtual ta_succ_iterator*
|
||||
succ_iter(const spot::state* s) const;
|
||||
succ_iter(const spot::state* s, bdd condition) const override;
|
||||
|
||||
virtual ta_succ_iterator*
|
||||
succ_iter(const spot::state* s, bdd condition) const;
|
||||
|
||||
virtual bdd_dict_ptr
|
||||
get_dict() const;
|
||||
bdd_dict_ptr get_dict() const;
|
||||
|
||||
virtual std::string
|
||||
format_state(const spot::state* s) const;
|
||||
format_state(const spot::state* s) const override;
|
||||
|
||||
virtual bool
|
||||
is_accepting_state(const spot::state* s) const;
|
||||
is_accepting_state(const spot::state* s) const override;
|
||||
|
||||
virtual bool
|
||||
is_livelock_accepting_state(const spot::state* s) const;
|
||||
is_livelock_accepting_state(const spot::state* s) const override;
|
||||
|
||||
virtual bool
|
||||
is_initial_state(const spot::state* s) const;
|
||||
is_initial_state(const spot::state* s) const override;
|
||||
|
||||
virtual bdd
|
||||
get_state_condition(const spot::state* s) const;
|
||||
get_state_condition(const spot::state* s) const override;
|
||||
|
||||
virtual void
|
||||
free_state(const spot::state* s) const;
|
||||
free_state(const spot::state* s) const override;
|
||||
|
||||
spot::state*
|
||||
get_artificial_initial_state() const
|
||||
virtual spot::state*
|
||||
get_artificial_initial_state() const override
|
||||
{
|
||||
return (spot::state*) artificial_initial_state_;
|
||||
}
|
||||
|
|
@ -107,7 +104,7 @@ namespace spot
|
|||
|
||||
}
|
||||
|
||||
virtual void
|
||||
void
|
||||
delete_stuttering_and_hole_successors(const spot::state* s);
|
||||
|
||||
ta::states_set_t
|
||||
|
|
@ -129,7 +126,7 @@ namespace spot
|
|||
|
||||
/// states used by spot::ta_explicit.
|
||||
/// \ingroup ta_representation
|
||||
class SPOT_API state_ta_explicit : public spot::state
|
||||
class SPOT_API state_ta_explicit final: public spot::state
|
||||
{
|
||||
#ifndef SWIG
|
||||
public:
|
||||
|
|
@ -156,15 +153,11 @@ namespace spot
|
|||
{
|
||||
}
|
||||
|
||||
virtual int
|
||||
compare(const spot::state* other) const;
|
||||
virtual size_t
|
||||
hash() const;
|
||||
virtual state_ta_explicit*
|
||||
clone() const;
|
||||
virtual int compare(const spot::state* other) const override;
|
||||
virtual size_t hash() const override;
|
||||
virtual state_ta_explicit* clone() const override;
|
||||
|
||||
virtual void
|
||||
destroy() const
|
||||
virtual void destroy() const override
|
||||
{
|
||||
}
|
||||
|
||||
|
|
@ -227,21 +220,21 @@ namespace spot
|
|||
};
|
||||
|
||||
/// Successor iterators used by spot::ta_explicit.
|
||||
class SPOT_API ta_explicit_succ_iterator : public ta_succ_iterator
|
||||
class SPOT_API ta_explicit_succ_iterator final: public ta_succ_iterator
|
||||
{
|
||||
public:
|
||||
ta_explicit_succ_iterator(const state_ta_explicit* s);
|
||||
|
||||
ta_explicit_succ_iterator(const state_ta_explicit* s, bdd condition);
|
||||
|
||||
virtual bool first();
|
||||
virtual bool next();
|
||||
virtual bool done() const;
|
||||
virtual bool first() override;
|
||||
virtual bool next() override;
|
||||
virtual bool done() const override;
|
||||
|
||||
virtual const state* dst() const;
|
||||
virtual bdd cond() const;
|
||||
virtual const state* dst() const override;
|
||||
virtual bdd cond() const override;
|
||||
|
||||
virtual acc_cond::mark_t acc() const;
|
||||
virtual acc_cond::mark_t acc() const override;
|
||||
|
||||
private:
|
||||
state_ta_explicit::transitions* transitions_;
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2011, 2012, 2013, 2014, 2016 Laboratoire de Recherche
|
||||
// et Développement de l'Epita (LRDE).
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
//
|
||||
|
|
@ -60,11 +60,11 @@ namespace spot
|
|||
}
|
||||
|
||||
virtual int
|
||||
compare(const state* other) const;
|
||||
compare(const state* other) const override;
|
||||
virtual size_t
|
||||
hash() const;
|
||||
hash() const override;
|
||||
virtual state_ta_product*
|
||||
clone() const;
|
||||
clone() const override;
|
||||
|
||||
private:
|
||||
const state* ta_state_; ///< State from the ta automaton.
|
||||
|
|
@ -82,22 +82,17 @@ namespace spot
|
|||
~ta_succ_iterator_product();
|
||||
|
||||
// iteration
|
||||
bool first();
|
||||
bool next();
|
||||
bool done() const;
|
||||
virtual bool first() override;
|
||||
virtual bool next() override;
|
||||
virtual bool done() const override;
|
||||
|
||||
// inspection
|
||||
state_ta_product*
|
||||
dst() const;
|
||||
bdd
|
||||
cond() const;
|
||||
|
||||
acc_cond::mark_t
|
||||
acc() const;
|
||||
virtual state_ta_product* dst() const override;
|
||||
virtual bdd cond() const override;
|
||||
virtual acc_cond::mark_t acc() const override;
|
||||
|
||||
/// \brief Return true if the changeset of the current transition is empty
|
||||
bool
|
||||
is_stuttering_transition() const;
|
||||
bool is_stuttering_transition() const;
|
||||
|
||||
protected:
|
||||
//@{
|
||||
|
|
@ -129,7 +124,7 @@ namespace spot
|
|||
/// \ingroup ta_emptiness_check
|
||||
/// \brief A lazy product between a Testing automaton and a Kripke structure.
|
||||
/// (States are computed on the fly.)
|
||||
class SPOT_API ta_product: public ta
|
||||
class SPOT_API ta_product final: public ta
|
||||
{
|
||||
public:
|
||||
/// \brief Constructor.
|
||||
|
|
@ -142,39 +137,39 @@ namespace spot
|
|||
~ta_product();
|
||||
|
||||
virtual ta::const_states_set_t
|
||||
get_initial_states_set() const;
|
||||
get_initial_states_set() const override;
|
||||
|
||||
virtual ta_succ_iterator_product*
|
||||
succ_iter(const spot::state* s) const;
|
||||
succ_iter(const spot::state* s) const override;
|
||||
|
||||
virtual ta_succ_iterator_product*
|
||||
succ_iter(const spot::state* s, bdd changeset) const;
|
||||
succ_iter(const spot::state* s, bdd changeset) const override;
|
||||
|
||||
virtual bdd_dict_ptr
|
||||
bdd_dict_ptr
|
||||
get_dict() const;
|
||||
|
||||
virtual std::string
|
||||
format_state(const spot::state* s) const;
|
||||
format_state(const spot::state* s) const override;
|
||||
|
||||
virtual bool
|
||||
is_accepting_state(const spot::state* s) const;
|
||||
is_accepting_state(const spot::state* s) const override;
|
||||
|
||||
virtual bool
|
||||
is_livelock_accepting_state(const spot::state* s) const;
|
||||
is_livelock_accepting_state(const spot::state* s) const override;
|
||||
|
||||
virtual bool
|
||||
is_initial_state(const spot::state* s) const;
|
||||
is_initial_state(const spot::state* s) const override;
|
||||
|
||||
/// \brief Return true if the state \a s has no succeseurs
|
||||
/// in the TA automaton (the TA component of the product automaton)
|
||||
virtual bool
|
||||
bool
|
||||
is_hole_state_in_ta_component(const spot::state* s) const;
|
||||
|
||||
virtual bdd
|
||||
get_state_condition(const spot::state* s) const;
|
||||
get_state_condition(const spot::state* s) const override;
|
||||
|
||||
virtual void
|
||||
free_state(const spot::state* s) const;
|
||||
free_state(const spot::state* s) const override;
|
||||
|
||||
const const_ta_ptr&
|
||||
get_ta() const
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de
|
||||
// Recherche et Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire
|
||||
// de Recherche et Développement de l'Epita (LRDE).
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
//
|
||||
|
|
@ -79,7 +79,7 @@ namespace spot
|
|||
/// longer needed.
|
||||
///
|
||||
virtual twa_succ_iterator*
|
||||
succ_iter_by_changeset(const spot::state* s, bdd change_set) const =0;
|
||||
succ_iter_by_changeset(const spot::state* s, bdd change_set) const = 0;
|
||||
};
|
||||
|
||||
typedef std::shared_ptr<tgta> tgta_ptr;
|
||||
|
|
|
|||
|
|
@ -44,12 +44,6 @@ namespace spot
|
|||
return ta_->succ_iter(state);
|
||||
}
|
||||
|
||||
bdd_dict_ptr
|
||||
tgta_explicit::get_dict() const
|
||||
{
|
||||
return ta_->get_dict();
|
||||
}
|
||||
|
||||
std::string
|
||||
tgta_explicit::format_state(const spot::state* s) const
|
||||
{
|
||||
|
|
|
|||
|
|
@ -34,7 +34,7 @@ namespace spot
|
|||
|
||||
/// Explicit representation of a spot::tgta.
|
||||
/// \ingroup ta_representation
|
||||
class SPOT_API tgta_explicit : public tgta
|
||||
class SPOT_API tgta_explicit final : public tgta
|
||||
{
|
||||
public:
|
||||
tgta_explicit(const const_twa_ptr& tgba,
|
||||
|
|
@ -42,21 +42,18 @@ namespace spot
|
|||
state_ta_explicit* artificial_initial_state);
|
||||
|
||||
// tgba interface
|
||||
virtual spot::state* get_init_state() const;
|
||||
virtual spot::state* get_init_state() const override;
|
||||
|
||||
virtual twa_succ_iterator*
|
||||
succ_iter(const spot::state* local_state) const;
|
||||
|
||||
virtual bdd_dict_ptr
|
||||
get_dict() const;
|
||||
succ_iter(const spot::state* local_state) const override;
|
||||
|
||||
const_ta_explicit_ptr get_ta() const { return ta_; }
|
||||
ta_explicit_ptr get_ta() { return ta_; }
|
||||
|
||||
virtual std::string format_state(const spot::state* s) const;
|
||||
virtual std::string format_state(const spot::state* s) const override;
|
||||
|
||||
virtual twa_succ_iterator*
|
||||
succ_iter_by_changeset(const spot::state* s, bdd change_set) const;
|
||||
succ_iter_by_changeset(const spot::state* s, bdd change_set) const override;
|
||||
protected:
|
||||
ta_explicit_ptr ta_;
|
||||
};
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2011, 2012, 2013, 2014, 2016 Laboratoire de Recherche
|
||||
// et Développement de l'Epita (LRDE).
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
//
|
||||
|
|
@ -35,10 +35,10 @@ namespace spot
|
|||
tgta_product(const const_kripke_ptr& left,
|
||||
const const_tgta_ptr& right);
|
||||
|
||||
virtual const state* get_init_state() const;
|
||||
virtual const state* get_init_state() const override;
|
||||
|
||||
virtual twa_succ_iterator*
|
||||
succ_iter(const state* local_state) const;
|
||||
succ_iter(const state* local_state) const override;
|
||||
};
|
||||
|
||||
inline twa_ptr product(const const_kripke_ptr& left,
|
||||
|
|
@ -48,7 +48,7 @@ namespace spot
|
|||
}
|
||||
|
||||
/// \brief Iterate over the successors of a product computed on the fly.
|
||||
class SPOT_API tgta_succ_iterator_product : public twa_succ_iterator
|
||||
class SPOT_API tgta_succ_iterator_product final : public twa_succ_iterator
|
||||
{
|
||||
public:
|
||||
tgta_succ_iterator_product(const state_product* s,
|
||||
|
|
|
|||
|
|
@ -109,7 +109,7 @@ namespace spot
|
|||
/// \param disable_heuristic_for_livelock_detection disable the heuristic
|
||||
/// used in the first pass to detect livelock-accepting runs,
|
||||
/// this heuristic is described in the paper cited above
|
||||
virtual bool
|
||||
bool
|
||||
check(bool disable_second_pass = false,
|
||||
bool disable_heuristic_for_livelock_detection = false);
|
||||
|
||||
|
|
@ -117,11 +117,11 @@ namespace spot
|
|||
/// a livelock-accepting run
|
||||
/// Return false if the product automaton accepts no livelock-accepting run,
|
||||
/// otherwise true
|
||||
virtual bool
|
||||
bool
|
||||
livelock_detection(const const_ta_product_ptr& t);
|
||||
|
||||
/// Print statistics, if any.
|
||||
virtual std::ostream&
|
||||
std::ostream&
|
||||
print_stats(std::ostream& os) const;
|
||||
|
||||
protected:
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2009, 2012, 2013, 2014, 2015 Laboratoire de Recherche
|
||||
// et Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2009, 2012, 2013, 2014, 2015, 2016 Laboratoire de
|
||||
// Recherche et Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
// et Marie Curie.
|
||||
|
|
@ -44,10 +44,10 @@ namespace spot
|
|||
/// proposition was already declared.
|
||||
bool declare(const std::string& prop_str);
|
||||
|
||||
virtual formula require(const std::string& prop_str);
|
||||
virtual formula require(const std::string& prop_str) override;
|
||||
|
||||
/// Get the name of the environment.
|
||||
virtual const std::string& name() const;
|
||||
virtual const std::string& name() const override;
|
||||
|
||||
typedef std::map<const std::string, formula> prop_map;
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche
|
||||
// et Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
// et Marie Curie.
|
||||
|
|
@ -38,8 +38,8 @@ namespace spot
|
|||
{
|
||||
public:
|
||||
virtual ~default_environment();
|
||||
virtual formula require(const std::string& prop_str);
|
||||
virtual const std::string& name() const;
|
||||
virtual formula require(const std::string& prop_str) override;
|
||||
virtual const std::string& name() const override;
|
||||
|
||||
/// Get the sole instance of spot::default_environment.
|
||||
static default_environment& instance();
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de
|
||||
// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de
|
||||
// Recherche et Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
|
|
@ -167,7 +167,7 @@ namespace spot
|
|||
/// constant and all Boolean operators supported by Spot.
|
||||
///
|
||||
/// By default each operator has equal chance to be selected.
|
||||
class SPOT_API random_boolean: public random_formula
|
||||
class SPOT_API random_boolean final: public random_formula
|
||||
{
|
||||
public:
|
||||
/// Create a random Boolean formula generator using atomic
|
||||
|
|
@ -207,7 +207,7 @@ namespace spot
|
|||
/// constant and all SERE operators supported by Spot.
|
||||
///
|
||||
/// By default each operator has equal chance to be selected.
|
||||
class SPOT_API random_sere: public random_formula
|
||||
class SPOT_API random_sere final: public random_formula
|
||||
{
|
||||
public:
|
||||
/// Create a random SERE genere using atomic propositions from \a ap.
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche
|
||||
// et Développement de l'Epita (LRDE).
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
//
|
||||
|
|
@ -47,7 +47,7 @@ namespace spot
|
|||
{
|
||||
}
|
||||
|
||||
formula next()
|
||||
virtual formula next() override
|
||||
{
|
||||
std::ostringstream s;
|
||||
s << 'p' << nn++;
|
||||
|
|
@ -65,7 +65,7 @@ namespace spot
|
|||
|
||||
unsigned nn;
|
||||
|
||||
formula next()
|
||||
virtual formula next() override
|
||||
{
|
||||
std::string s;
|
||||
unsigned n = nn++;
|
||||
|
|
|
|||
|
|
@ -55,7 +55,7 @@ namespace spot
|
|||
}
|
||||
|
||||
virtual int
|
||||
extend(int n)
|
||||
extend(int n) override
|
||||
{
|
||||
assert(priv_);
|
||||
int b = priv_->allocate_variables(n);
|
||||
|
|
|
|||
|
|
@ -53,9 +53,9 @@ namespace spot
|
|||
|
||||
/// TGBA interface.
|
||||
virtual ~taa_tgba();
|
||||
virtual spot::state* get_init_state() const final;
|
||||
virtual twa_succ_iterator* succ_iter(const spot::state* state) const final;
|
||||
virtual std::string format_state(const spot::state* state) const = 0;
|
||||
virtual spot::state* get_init_state() const override final;
|
||||
virtual twa_succ_iterator* succ_iter(const spot::state* state)
|
||||
const override final;
|
||||
|
||||
protected:
|
||||
|
||||
|
|
@ -81,9 +81,9 @@ namespace spot
|
|||
{
|
||||
}
|
||||
|
||||
virtual int compare(const spot::state*) const;
|
||||
virtual size_t hash() const;
|
||||
virtual set_state* clone() const;
|
||||
virtual int compare(const spot::state*) const override;
|
||||
virtual size_t hash() const override;
|
||||
virtual set_state* clone() const override;
|
||||
|
||||
virtual ~set_state()
|
||||
{
|
||||
|
|
@ -103,13 +103,13 @@ namespace spot
|
|||
taa_succ_iterator(const taa_tgba::state_set* s, const acc_cond& acc);
|
||||
virtual ~taa_succ_iterator();
|
||||
|
||||
virtual bool first();
|
||||
virtual bool next();
|
||||
virtual bool done() const;
|
||||
virtual bool first() override;
|
||||
virtual bool next() override;
|
||||
virtual bool done() const override;
|
||||
|
||||
virtual set_state* dst() const;
|
||||
virtual bdd cond() const;
|
||||
virtual acc_cond::mark_t acc() const;
|
||||
virtual set_state* dst() const override;
|
||||
virtual bdd cond() const override;
|
||||
virtual acc_cond::mark_t acc() const override;
|
||||
|
||||
private:
|
||||
/// Those typedefs are used to generate all possible successors in
|
||||
|
|
@ -206,7 +206,7 @@ namespace spot
|
|||
/// Otherwise a string composed of each string corresponding to
|
||||
/// each state->get_state() in the spot::set_state is returned,
|
||||
/// e.g. like {string_1,...,string_n}.
|
||||
virtual std::string format_state(const spot::state* s) const
|
||||
virtual std::string format_state(const spot::state* s) const override
|
||||
{
|
||||
const spot::set_state* se = down_cast<const spot::set_state*>(s);
|
||||
assert(se);
|
||||
|
|
@ -311,7 +311,8 @@ namespace spot
|
|||
~taa_tgba_string()
|
||||
{}
|
||||
protected:
|
||||
virtual std::string label_to_string(const std::string& label) const;
|
||||
virtual std::string label_to_string(const std::string& label)
|
||||
const override;
|
||||
};
|
||||
|
||||
typedef std::shared_ptr<taa_tgba_string> taa_tgba_string_ptr;
|
||||
|
|
@ -335,7 +336,8 @@ namespace spot
|
|||
~taa_tgba_formula()
|
||||
{}
|
||||
protected:
|
||||
virtual std::string label_to_string(const label_t& label) const;
|
||||
virtual std::string label_to_string(const label_t& label)
|
||||
const override;
|
||||
};
|
||||
|
||||
typedef std::shared_ptr<taa_tgba_formula> taa_tgba_formula_ptr;
|
||||
|
|
|
|||
|
|
@ -42,7 +42,7 @@ namespace spot
|
|||
{
|
||||
}
|
||||
|
||||
virtual int compare(const spot::state* other) const
|
||||
virtual int compare(const spot::state* other) const override
|
||||
{
|
||||
auto o = down_cast<const twa_graph_state*>(other);
|
||||
assert(o);
|
||||
|
|
@ -55,19 +55,19 @@ namespace spot
|
|||
return 0;
|
||||
}
|
||||
|
||||
virtual size_t hash() const
|
||||
virtual size_t hash() const override
|
||||
{
|
||||
return
|
||||
reinterpret_cast<const char*>(this) - static_cast<const char*>(nullptr);
|
||||
}
|
||||
|
||||
virtual twa_graph_state*
|
||||
clone() const
|
||||
clone() const override
|
||||
{
|
||||
return const_cast<twa_graph_state*>(this);
|
||||
}
|
||||
|
||||
virtual void destroy() const
|
||||
virtual void destroy() const override
|
||||
{
|
||||
}
|
||||
};
|
||||
|
|
@ -121,41 +121,41 @@ namespace spot
|
|||
{
|
||||
}
|
||||
|
||||
virtual void recycle(edge t)
|
||||
void recycle(edge t)
|
||||
{
|
||||
t_ = t;
|
||||
}
|
||||
|
||||
virtual bool first()
|
||||
virtual bool first() override
|
||||
{
|
||||
p_ = t_;
|
||||
return p_;
|
||||
}
|
||||
|
||||
virtual bool next()
|
||||
virtual bool next() override
|
||||
{
|
||||
p_ = g_->edge_storage(p_).next_succ;
|
||||
return p_;
|
||||
}
|
||||
|
||||
virtual bool done() const
|
||||
virtual bool done() const override
|
||||
{
|
||||
return !p_;
|
||||
}
|
||||
|
||||
virtual const twa_graph_state* dst() const
|
||||
virtual const twa_graph_state* dst() const override
|
||||
{
|
||||
assert(!done());
|
||||
return &g_->state_data(g_->edge_storage(p_).dst);
|
||||
}
|
||||
|
||||
virtual bdd cond() const
|
||||
virtual bdd cond() const override
|
||||
{
|
||||
assert(!done());
|
||||
return g_->edge_data(p_).cond;
|
||||
}
|
||||
|
||||
virtual acc_cond::mark_t acc() const
|
||||
virtual acc_cond::mark_t acc() const override
|
||||
{
|
||||
assert(!done());
|
||||
return g_->edge_data(p_).acc;
|
||||
|
|
@ -267,7 +267,7 @@ namespace spot
|
|||
return init_number_;
|
||||
}
|
||||
|
||||
virtual const twa_graph_state* get_init_state() const
|
||||
virtual const twa_graph_state* get_init_state() const override
|
||||
{
|
||||
if (num_states() == 0)
|
||||
const_cast<graph_t&>(g_).new_state();
|
||||
|
|
@ -275,7 +275,7 @@ namespace spot
|
|||
}
|
||||
|
||||
virtual twa_succ_iterator*
|
||||
succ_iter(const state* st) const
|
||||
succ_iter(const state* st) const override
|
||||
{
|
||||
auto s = down_cast<const typename graph_t::state_storage_t*>(st);
|
||||
assert(s);
|
||||
|
|
@ -313,7 +313,7 @@ namespace spot
|
|||
return ss.str();
|
||||
}
|
||||
|
||||
virtual std::string format_state(const state* st) const
|
||||
virtual std::string format_state(const state* st) const override
|
||||
{
|
||||
return format_state(state_number(st));
|
||||
}
|
||||
|
|
|
|||
|
|
@ -49,7 +49,7 @@ namespace spot
|
|||
{
|
||||
}
|
||||
|
||||
virtual void destroy() const;
|
||||
virtual void destroy() const override;
|
||||
|
||||
const state*
|
||||
left() const
|
||||
|
|
@ -63,9 +63,9 @@ namespace spot
|
|||
return right_;
|
||||
}
|
||||
|
||||
virtual int compare(const state* other) const;
|
||||
virtual size_t hash() const;
|
||||
virtual state_product* clone() const;
|
||||
virtual int compare(const state* other) const override;
|
||||
virtual size_t hash() const override;
|
||||
virtual state_product* clone() const override;
|
||||
|
||||
private:
|
||||
const state* left_; ///< State from the left automaton.
|
||||
|
|
@ -74,7 +74,7 @@ namespace spot
|
|||
fixed_size_pool* pool_;
|
||||
|
||||
virtual ~state_product();
|
||||
state_product(const state_product& o); // No implementation.
|
||||
state_product(const state_product& o) = delete;
|
||||
};
|
||||
|
||||
|
||||
|
|
@ -90,14 +90,15 @@ namespace spot
|
|||
|
||||
virtual ~twa_product();
|
||||
|
||||
virtual const state* get_init_state() const;
|
||||
virtual const state* get_init_state() const override;
|
||||
|
||||
virtual twa_succ_iterator*
|
||||
succ_iter(const state* state) const;
|
||||
succ_iter(const state* state) const override;
|
||||
|
||||
virtual std::string format_state(const state* state) const;
|
||||
virtual std::string format_state(const state* state) const override;
|
||||
|
||||
virtual state* project_state(const state* s, const const_twa_ptr& t) const;
|
||||
virtual state* project_state(const state* s, const const_twa_ptr& t)
|
||||
const override;
|
||||
|
||||
const acc_cond& left_acc() const;
|
||||
const acc_cond& right_acc() const;
|
||||
|
|
@ -120,7 +121,7 @@ namespace spot
|
|||
public:
|
||||
twa_product_init(const const_twa_ptr& left, const const_twa_ptr& right,
|
||||
const state* left_init, const state* right_init);
|
||||
virtual const state* get_init_state() const;
|
||||
virtual const state* get_init_state() const override;
|
||||
protected:
|
||||
const state* left_init_;
|
||||
const state* right_init_;
|
||||
|
|
@ -135,11 +136,11 @@ namespace spot
|
|||
|
||||
/// \brief on-the-fly TGBA product with forced initial states
|
||||
inline twa_product_ptr otf_product_at(const const_twa_ptr& left,
|
||||
const const_twa_ptr& right,
|
||||
const state* left_init,
|
||||
const state* right_init)
|
||||
const const_twa_ptr& right,
|
||||
const state* left_init,
|
||||
const state* right_init)
|
||||
{
|
||||
return std::make_shared<twa_product_init>(left, right,
|
||||
left_init, right_init);
|
||||
left_init, right_init);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2010, 2011, 2013, 2014, 2015 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2010, 2011, 2013, 2014, 2015, 2016 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.
|
||||
|
|
@ -170,7 +170,7 @@ namespace spot
|
|||
const state* substart = ecs_->cycle_seed;
|
||||
do
|
||||
{
|
||||
struct scc_bfs: bfs_steps
|
||||
struct scc_bfs final: bfs_steps
|
||||
{
|
||||
const couvreur99_check_status* ecs;
|
||||
couvreur99_check_result* r;
|
||||
|
|
@ -186,7 +186,7 @@ namespace spot
|
|||
}
|
||||
|
||||
virtual const state*
|
||||
filter(const state* s)
|
||||
filter(const state* s) override
|
||||
{
|
||||
auto i = ecs->h.find(s);
|
||||
s->destroy();
|
||||
|
|
@ -201,7 +201,7 @@ namespace spot
|
|||
}
|
||||
|
||||
virtual bool
|
||||
match(twa_run::step& st, const state* s)
|
||||
match(twa_run::step& st, const state* s) override
|
||||
{
|
||||
acc_cond::mark_t less_acc =
|
||||
acc_to_traverse - st.acc;
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement de
|
||||
// Copyright (C) 2013, 2014, 2016 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
|
||||
|
|
@ -29,7 +29,7 @@
|
|||
namespace spot
|
||||
{
|
||||
/// Compute a counter example from a spot::couvreur99_check_status
|
||||
class SPOT_API couvreur99_check_result:
|
||||
class SPOT_API couvreur99_check_result final:
|
||||
public emptiness_check_result,
|
||||
public acss_statistics
|
||||
{
|
||||
|
|
@ -38,11 +38,11 @@ namespace spot
|
|||
std::shared_ptr<const couvreur99_check_status>& ecs,
|
||||
option_map o = option_map());
|
||||
|
||||
virtual twa_run_ptr accepting_run();
|
||||
virtual twa_run_ptr accepting_run() override;
|
||||
|
||||
void print_stats(std::ostream& os) const;
|
||||
|
||||
virtual unsigned acss_states() const;
|
||||
virtual unsigned acss_states() const override;
|
||||
|
||||
protected:
|
||||
/// Called by accepting_run() to find a cycle which traverses all
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2008, 2013, 2014, 2015 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2008, 2013, 2014, 2015, 2016 Laboratoire de Recherche
|
||||
// et Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
|
||||
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
||||
// Université Pierre et Marie Curie.
|
||||
|
|
@ -146,12 +146,13 @@ namespace spot
|
|||
{
|
||||
public:
|
||||
couvreur99_check(const const_twa_ptr& a, option_map o = option_map());
|
||||
|
||||
virtual ~couvreur99_check();
|
||||
|
||||
/// Check whether the automaton's language is empty.
|
||||
virtual emptiness_check_result_ptr check();
|
||||
virtual emptiness_check_result_ptr check() override;
|
||||
|
||||
virtual std::ostream& print_stats(std::ostream& os) const;
|
||||
virtual std::ostream& print_stats(std::ostream& os) const override;
|
||||
|
||||
/// \brief Return the status of the emptiness-check.
|
||||
///
|
||||
|
|
@ -190,7 +191,7 @@ namespace spot
|
|||
couvreur99_check_shy(const const_twa_ptr& a, option_map o = option_map());
|
||||
virtual ~couvreur99_check_shy();
|
||||
|
||||
virtual emptiness_check_result_ptr check();
|
||||
virtual emptiness_check_result_ptr check() override;
|
||||
|
||||
protected:
|
||||
struct successor {
|
||||
|
|
|
|||
|
|
@ -85,7 +85,7 @@ namespace spot
|
|||
}
|
||||
|
||||
virtual emptiness_check_result_ptr
|
||||
check()
|
||||
check() override
|
||||
{
|
||||
top = dftop = -1;
|
||||
violation = false;
|
||||
|
|
@ -226,7 +226,7 @@ namespace spot
|
|||
}
|
||||
|
||||
virtual std::ostream&
|
||||
print_stats(std::ostream& os) const
|
||||
print_stats(std::ostream& os) const override
|
||||
{
|
||||
os << h.size() << " unique states visited\n";
|
||||
os << transitions() << " transitions explored\n";
|
||||
|
|
@ -264,7 +264,7 @@ namespace spot
|
|||
}
|
||||
|
||||
virtual unsigned
|
||||
acss_states() const
|
||||
acss_states() const override
|
||||
{
|
||||
// Gross!
|
||||
const_cast<result*>(this)->update_lowlinks();
|
||||
|
|
@ -282,7 +282,7 @@ namespace spot
|
|||
}
|
||||
|
||||
virtual twa_run_ptr
|
||||
accepting_run()
|
||||
accepting_run() override
|
||||
{
|
||||
auto res = std::make_shared<twa_run>(automaton());
|
||||
|
||||
|
|
@ -335,7 +335,7 @@ namespace spot
|
|||
}
|
||||
|
||||
virtual const state*
|
||||
filter(const state* s)
|
||||
filter(const state* s) override
|
||||
{
|
||||
// Do not escape the SCC
|
||||
auto j = data.h.find(s);
|
||||
|
|
@ -357,13 +357,13 @@ namespace spot
|
|||
}
|
||||
|
||||
virtual bool
|
||||
match(twa_run::step& step, const state*)
|
||||
match(twa_run::step& step, const state*) override
|
||||
{
|
||||
return step.acc != 0U;
|
||||
}
|
||||
};
|
||||
|
||||
struct second_bfs: first_bfs
|
||||
struct second_bfs final: first_bfs
|
||||
{
|
||||
const state* target;
|
||||
second_bfs(result* r, int scc_root, const state* target)
|
||||
|
|
@ -372,7 +372,7 @@ namespace spot
|
|||
}
|
||||
|
||||
virtual bool
|
||||
match(twa_run::step&, const state* s)
|
||||
match(twa_run::step&, const state* s) override
|
||||
{
|
||||
return s == target;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2009, 2010, 2012, 2013, 2014, 2015 Laboratoire de
|
||||
// Recherche et Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2009, 2010, 2012, 2013, 2014, 2015, 2016 Laboratoire
|
||||
// de Recherche et Développement de l'Epita (LRDE).
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
//
|
||||
|
|
@ -29,7 +29,7 @@ namespace spot
|
|||
namespace
|
||||
{
|
||||
/// \brief Recursively translate a formula into a TAA.
|
||||
class ltl2taa_visitor
|
||||
class ltl2taa_visitor final
|
||||
{
|
||||
public:
|
||||
ltl2taa_visitor(const taa_tgba_formula_ptr& res,
|
||||
|
|
@ -40,7 +40,6 @@ namespace spot
|
|||
{
|
||||
}
|
||||
|
||||
virtual
|
||||
~ltl2taa_visitor()
|
||||
{
|
||||
}
|
||||
|
|
|
|||
|
|
@ -87,7 +87,7 @@ namespace spot
|
|||
/// check() can be called several times (until it returns a null
|
||||
/// pointer) to enumerate all the visited accepting paths. The method
|
||||
/// visits only a finite set of accepting paths.
|
||||
virtual emptiness_check_result_ptr check()
|
||||
virtual emptiness_check_result_ptr check() override
|
||||
{
|
||||
auto t = std::static_pointer_cast<magic_search_>
|
||||
(this->emptiness_check::shared_from_this());
|
||||
|
|
@ -114,7 +114,7 @@ namespace spot
|
|||
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 << transitions() << " transitions explored" << std::endl;
|
||||
|
|
@ -128,7 +128,7 @@ namespace spot
|
|||
return os;
|
||||
}
|
||||
|
||||
virtual bool safe() const
|
||||
virtual bool safe() const override
|
||||
{
|
||||
return heap::Safe;
|
||||
}
|
||||
|
|
@ -319,7 +319,7 @@ namespace spot
|
|||
return false;
|
||||
}
|
||||
|
||||
class result_from_stack: public emptiness_check_result,
|
||||
class result_from_stack final: public emptiness_check_result,
|
||||
public acss_statistics
|
||||
{
|
||||
public:
|
||||
|
|
@ -328,7 +328,7 @@ namespace spot
|
|||
{
|
||||
}
|
||||
|
||||
virtual twa_run_ptr accepting_run()
|
||||
virtual twa_run_ptr accepting_run() override
|
||||
{
|
||||
assert(!ms_->st_blue.empty());
|
||||
assert(!ms_->st_red.empty());
|
||||
|
|
@ -366,7 +366,7 @@ namespace spot
|
|||
return run;
|
||||
}
|
||||
|
||||
unsigned acss_states() const
|
||||
virtual unsigned acss_states() const override
|
||||
{
|
||||
return 0;
|
||||
}
|
||||
|
|
@ -376,7 +376,7 @@ namespace spot
|
|||
|
||||
# define FROM_STACK "ar:from_stack"
|
||||
|
||||
class magic_search_result: public emptiness_check_result
|
||||
class magic_search_result final: public emptiness_check_result
|
||||
{
|
||||
public:
|
||||
magic_search_result(const std::shared_ptr<magic_search_>& m,
|
||||
|
|
@ -389,7 +389,7 @@ namespace spot
|
|||
computer = new ndfs_result<magic_search_<heap>, heap>(ms);
|
||||
}
|
||||
|
||||
virtual void options_updated(const option_map& old)
|
||||
virtual void options_updated(const option_map& old) override
|
||||
{
|
||||
if (old[FROM_STACK] && !options()[FROM_STACK])
|
||||
{
|
||||
|
|
@ -408,12 +408,12 @@ namespace spot
|
|||
delete computer;
|
||||
}
|
||||
|
||||
virtual twa_run_ptr accepting_run()
|
||||
virtual twa_run_ptr accepting_run() override
|
||||
{
|
||||
return computer->accepting_run();
|
||||
}
|
||||
|
||||
virtual const unsigned_statistics* statistics() const
|
||||
virtual const unsigned_statistics* statistics() const override
|
||||
{
|
||||
return computer->statistics();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -174,7 +174,7 @@ namespace spot
|
|||
return res;
|
||||
}
|
||||
|
||||
struct wdba_search_acc_loop : public bfs_steps
|
||||
struct wdba_search_acc_loop final : public bfs_steps
|
||||
{
|
||||
wdba_search_acc_loop(const const_twa_ptr& det_a,
|
||||
unsigned scc_n, scc_info& sm,
|
||||
|
|
@ -185,7 +185,7 @@ namespace spot
|
|||
}
|
||||
|
||||
virtual const state*
|
||||
filter(const state* s)
|
||||
filter(const state* s) override
|
||||
{
|
||||
s = seen(s);
|
||||
if (sm.scc_of(std::static_pointer_cast<const twa_graph>(a_)
|
||||
|
|
@ -195,7 +195,7 @@ namespace spot
|
|||
}
|
||||
|
||||
virtual bool
|
||||
match(twa_run::step&, const state* to)
|
||||
match(twa_run::step&, const state* to) override
|
||||
{
|
||||
return to == dest;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2011, 2013, 2014, 2015 Laboratoire de recherche et
|
||||
// développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2011, 2013, 2014, 2015, 2016 Laboratoire de recherche
|
||||
// et développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2004, 2005, 2006 Laboratoire d'Informatique de Paris
|
||||
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
||||
// Université Pierre et Marie Curie.
|
||||
|
|
@ -76,8 +76,8 @@ namespace spot
|
|||
struct stats_interface<T, 1>
|
||||
: public acss_statistics
|
||||
{
|
||||
unsigned
|
||||
acss_states() const
|
||||
virtual unsigned
|
||||
acss_states() const override
|
||||
{
|
||||
// all visited states are in the state space search
|
||||
return static_cast<const T*>(this)->h_.size();
|
||||
|
|
@ -88,7 +88,7 @@ namespace spot
|
|||
|
||||
|
||||
template <typename ndfs_search, typename heap>
|
||||
class ndfs_result:
|
||||
class ndfs_result final:
|
||||
public emptiness_check_result,
|
||||
// Conditionally inherit from acss_statistics or ars_statistics.
|
||||
public stats_interface<ndfs_result<ndfs_search, heap>, heap::Has_Size>
|
||||
|
|
@ -104,7 +104,7 @@ namespace spot
|
|||
{
|
||||
}
|
||||
|
||||
virtual twa_run_ptr accepting_run()
|
||||
virtual twa_run_ptr accepting_run() override
|
||||
{
|
||||
const stack_type& stb = ms_->get_st_blue();
|
||||
const stack_type& str = ms_->get_st_red();
|
||||
|
|
|
|||
|
|
@ -102,8 +102,8 @@ namespace spot
|
|||
public:
|
||||
tgba_reachable_iterator_breadth_first(const const_twa_ptr& a);
|
||||
|
||||
virtual void add_state(const state* s);
|
||||
virtual const state* next_state();
|
||||
virtual void add_state(const state* s) override;
|
||||
virtual const state* next_state() override;
|
||||
|
||||
protected:
|
||||
std::deque<const state*> todo; ///< A queue of states yet to explore.
|
||||
|
|
@ -189,8 +189,8 @@ namespace spot
|
|||
/// the stack after process_link() has been called.
|
||||
bool on_stack(int sn) const;
|
||||
protected:
|
||||
virtual void push(const state* s, int sn);
|
||||
virtual void pop();
|
||||
virtual void push(const state* s, int sn) override;
|
||||
virtual void pop() override;
|
||||
|
||||
std::unordered_set<int> stack_;
|
||||
};
|
||||
|
|
|
|||
|
|
@ -47,7 +47,7 @@ namespace spot
|
|||
/// \brief Emptiness checker on spot::tgba automata having at most one
|
||||
/// acceptance condition (i.e. a TBA).
|
||||
template <typename heap>
|
||||
class se05_search : public emptiness_check, public ec_statistics
|
||||
class se05_search final : public emptiness_check, public ec_statistics
|
||||
{
|
||||
public:
|
||||
/// \brief Initialize the Magic Search algorithm on the automaton \a a
|
||||
|
|
@ -87,7 +87,7 @@ namespace spot
|
|||
/// check() can be called several times (until it returns a null
|
||||
/// pointer) to enumerate all the visited accepting paths. The method
|
||||
/// visits only a finite set of accepting paths.
|
||||
virtual emptiness_check_result_ptr check()
|
||||
virtual emptiness_check_result_ptr check() override
|
||||
{
|
||||
auto t = std::static_pointer_cast<se05_search>
|
||||
(this->emptiness_check::shared_from_this());
|
||||
|
|
@ -114,7 +114,7 @@ namespace spot
|
|||
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 << transitions() << " transitions explored" << std::endl;
|
||||
|
|
@ -128,7 +128,7 @@ namespace spot
|
|||
return os;
|
||||
}
|
||||
|
||||
virtual bool safe() const
|
||||
virtual bool safe() const override
|
||||
{
|
||||
return heap::Safe;
|
||||
}
|
||||
|
|
@ -334,7 +334,7 @@ namespace spot
|
|||
{
|
||||
}
|
||||
|
||||
virtual twa_run_ptr accepting_run()
|
||||
virtual twa_run_ptr accepting_run() override
|
||||
{
|
||||
assert(!ms_->st_blue.empty());
|
||||
assert(!ms_->st_red.empty());
|
||||
|
|
@ -378,7 +378,7 @@ namespace spot
|
|||
return run;
|
||||
}
|
||||
|
||||
unsigned acss_states() const
|
||||
virtual unsigned acss_states() const override
|
||||
{
|
||||
return 0;
|
||||
}
|
||||
|
|
@ -388,7 +388,7 @@ namespace spot
|
|||
|
||||
# define FROM_STACK "ar:from_stack"
|
||||
|
||||
class se05_result: public emptiness_check_result
|
||||
class se05_result final: public emptiness_check_result
|
||||
{
|
||||
public:
|
||||
se05_result(const std::shared_ptr<se05_search>& m,
|
||||
|
|
@ -401,7 +401,7 @@ namespace spot
|
|||
computer = new ndfs_result<se05_search<heap>, heap>(ms);
|
||||
}
|
||||
|
||||
virtual void options_updated(const option_map& old)
|
||||
virtual void options_updated(const option_map& old) override
|
||||
{
|
||||
if (old[FROM_STACK] && !options()[FROM_STACK])
|
||||
{
|
||||
|
|
@ -420,12 +420,12 @@ namespace spot
|
|||
delete computer;
|
||||
}
|
||||
|
||||
virtual twa_run_ptr accepting_run()
|
||||
virtual twa_run_ptr accepting_run() override
|
||||
{
|
||||
return computer->accepting_run();
|
||||
}
|
||||
|
||||
virtual const unsigned_statistics* statistics() const
|
||||
virtual const unsigned_statistics* statistics() const override
|
||||
{
|
||||
return computer->statistics();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -40,7 +40,7 @@ namespace spot
|
|||
{
|
||||
namespace
|
||||
{
|
||||
class state_tgbasl: public state
|
||||
class state_tgbasl final: public state
|
||||
{
|
||||
public:
|
||||
state_tgbasl(const state* s, bdd cond) : s_(s), cond_(cond)
|
||||
|
|
@ -54,7 +54,7 @@ namespace spot
|
|||
}
|
||||
|
||||
virtual int
|
||||
compare(const state* other) const
|
||||
compare(const state* other) const override
|
||||
{
|
||||
const state_tgbasl* o =
|
||||
down_cast<const state_tgbasl*>(other);
|
||||
|
|
@ -66,13 +66,13 @@ namespace spot
|
|||
}
|
||||
|
||||
virtual size_t
|
||||
hash() const
|
||||
hash() const override
|
||||
{
|
||||
return wang32_hash(s_->hash()) ^ wang32_hash(cond_.id());
|
||||
}
|
||||
|
||||
virtual
|
||||
state_tgbasl* clone() const
|
||||
state_tgbasl* clone() const override
|
||||
{
|
||||
return new state_tgbasl(*this);
|
||||
}
|
||||
|
|
@ -94,7 +94,7 @@ namespace spot
|
|||
bdd cond_;
|
||||
};
|
||||
|
||||
class twasl_succ_iterator : public twa_succ_iterator
|
||||
class twasl_succ_iterator final : public twa_succ_iterator
|
||||
{
|
||||
public:
|
||||
twasl_succ_iterator(twa_succ_iterator* it, const state_tgbasl* state,
|
||||
|
|
@ -111,8 +111,8 @@ namespace spot
|
|||
|
||||
// iteration
|
||||
|
||||
bool
|
||||
first()
|
||||
virtual bool
|
||||
first() override
|
||||
{
|
||||
loop_ = false;
|
||||
done_ = false;
|
||||
|
|
@ -125,8 +125,8 @@ namespace spot
|
|||
return true;
|
||||
}
|
||||
|
||||
bool
|
||||
next()
|
||||
virtual bool
|
||||
next() override
|
||||
{
|
||||
if (cond_ != bddfalse)
|
||||
{
|
||||
|
|
@ -148,32 +148,32 @@ namespace spot
|
|||
}
|
||||
}
|
||||
|
||||
bool
|
||||
done() const
|
||||
virtual bool
|
||||
done() const override
|
||||
{
|
||||
return it_->done() && done_;
|
||||
}
|
||||
|
||||
// inspection
|
||||
|
||||
state_tgbasl*
|
||||
dst() const
|
||||
virtual state_tgbasl*
|
||||
dst() const override
|
||||
{
|
||||
if (loop_)
|
||||
return new state_tgbasl(state_->real_state(), state_->cond());
|
||||
return new state_tgbasl(it_->dst(), one_);
|
||||
}
|
||||
|
||||
bdd
|
||||
cond() const
|
||||
virtual bdd
|
||||
cond() const override
|
||||
{
|
||||
if (loop_)
|
||||
return state_->cond();
|
||||
return one_;
|
||||
}
|
||||
|
||||
acc_cond::mark_t
|
||||
acc() const
|
||||
virtual acc_cond::mark_t
|
||||
acc() const override
|
||||
{
|
||||
if (loop_)
|
||||
return 0U;
|
||||
|
|
|
|||
|
|
@ -50,7 +50,7 @@ namespace spot
|
|||
/// \brief Emptiness checker on spot::tgba automata having at most one
|
||||
/// acceptance condition (i.e. a TBA).
|
||||
template <typename heap>
|
||||
class tau03_search : public emptiness_check, public ec_statistics
|
||||
class tau03_search final : public emptiness_check, public ec_statistics
|
||||
{
|
||||
public:
|
||||
/// \brief Initialize the search algorithm on the automaton \a a
|
||||
|
|
@ -82,7 +82,7 @@ namespace spot
|
|||
///
|
||||
/// \return non null pointer iff the algorithm has found an
|
||||
/// accepting path.
|
||||
virtual emptiness_check_result_ptr check()
|
||||
virtual emptiness_check_result_ptr check() override
|
||||
{
|
||||
if (!st_blue.empty())
|
||||
return nullptr;
|
||||
|
|
@ -98,7 +98,7 @@ namespace spot
|
|||
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 << transitions() << " transitions explored" << std::endl;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue