`s->destroy();`

instead of `delete s;`

.
virtual ~state()
{
}
};
/// \ingroup tgba_essentials
/// \brief Strict Weak Ordering for \c state*.
///
/// This is meant to be used as a comparison functor for
/// STL \c map whose key are of type \c state*.
///
/// For instance here is how one could declare
/// a map of \c state*.
/// \code
/// // Remember how many times each state has been visited.
/// std::map`aut->acc().is_generalized_buchi())`

returns true.
///
/// Browsing such automaton can be achieved using two functions:
/// \c get_init_state, and \c succ. The former returns
/// the initial state while the latter lists the
/// successor states of any state.
///
/// Note that although this is a transition-based automata, we never
/// represent transitions in the API! Transition data are
/// obtained by querying the iterator over the successors of a
/// state.
class SPOT_API twa: public std::enable_shared_from_this`for (auto i: aut->succ(s)) { /* i->current_state() */ }`

.
succ_iterable
succ(const state* s) const
{
return {this, succ_iter(s)};
}
#endif
/// \brief Release an iterator after usage.
///
/// This iterator can then be reused by succ_iter() to avoid
/// memory allocation.
void release_iter(tgba_succ_iterator* i) const
{
if (iter_cache_)
delete i;
else
iter_cache_ = i;
}
/// \brief Get a formula that must hold whatever successor is taken.
///
/// \return A formula which must be verified for all successors
/// of \a state.
///
/// This can be as simple as \c bddtrue, or more completely
/// the disjunction of the condition of all successors. This
/// is used as an hint by \c succ_iter() to reduce the number
/// of successor to compute in a product.
///
/// Sub classes should implement compute_support_conditions(),
/// this function is just a wrapper that will cache the
/// last return value for efficiency.
bdd support_conditions(const state* state) const;
/// \brief Get the dictionary associated to the automaton.
///
/// Atomic propositions and acceptance conditions are represented
/// as BDDs. The dictionary allows to map BDD variables back to
/// formulae, and vice versa. This is useful when dealing with
/// several automata (which may use the same BDD variable for
/// different formula), or simply when printing.
bdd_dict_ptr get_dict() const
{
return dict_;
}
/// \brief Format the state as a string for printing.
///
/// This formating is the responsability of the automata
/// that owns the state.
virtual std::string format_state(const state* state) const = 0;
/// \brief Return a possible annotation for the transition
/// pointed to by the iterator.
///
/// You may decide to use annotations when building a tgba class
/// that represents the state space of a model, for instance to
/// indicate how the tgba transitions relate to the original model
/// (e.g. the annotation could be the name of a PetriNet
/// transition, or the line number of some textual formalism).
///
/// Implementing this method is optional; the default annotation
/// is the empty string.
///
/// This method is used for instance in dotty_reachable(),
/// and replay_tgba_run().
///
/// \param t a non-done tgba_succ_iterator for this automaton
virtual std::string
transition_annotation(const tgba_succ_iterator* t) const;
/// \brief Project a state on an automaton.
///
/// This converts \a s, into that corresponding spot::state for \a
/// t. This is useful when you have the state of a product, and
/// want restrict this state to a specific automata occuring in
/// the product.
///
/// It goes without saying that \a s and \a t should be compatible
/// (i.e., \a s is a state of \a t).
///
/// \return 0 if the projection fails (\a s is unrelated to \a t),
/// or a new \c state* (the projected state) that must be
/// destroyed by the caller.
virtual state* project_state(const state* s,
const const_tgba_ptr& t) const;
const acc_cond& acc() const
{
return acc_;
}
acc_cond& acc()
{
return acc_;
}
virtual bool is_empty() const;
protected:
acc_cond acc_;
void set_num_sets_(unsigned num)
{
if (num < acc_.num_sets())
{
acc_.~acc_cond();
new (&acc_) acc_cond;
}
acc_.add_sets(num - acc_.num_sets());
}
public:
const acc_cond::acc_code& get_acceptance() const
{
return acc_.get_acceptance();
}
void set_acceptance(unsigned num, const acc_cond::acc_code& c)
{
set_num_sets_(num);
acc_.set_acceptance(c);
if (num == 0)
prop_state_based_acc();
}
/// \brief Copy the acceptance condition of another tgba.
void copy_acceptance_of(const const_tgba_ptr& a)
{
acc_ = a->acc();
unsigned num = acc_.num_sets();
if (num == 0)
prop_state_based_acc();
}
void copy_ap_of(const const_tgba_ptr& a)
{
get_dict()->register_all_propositions_of(a, this);
}
void set_generalized_buchi(unsigned num)
{
set_num_sets_(num);
acc_.set_generalized_buchi();
if (num == 0)
prop_state_based_acc();
}
acc_cond::mark_t set_buchi()
{
set_generalized_buchi(1);
return acc_.mark(0);
}
protected:
/// Do the actual computation of tgba::support_conditions().
virtual bdd compute_support_conditions(const state* state) const = 0;
mutable const state* last_support_conditions_input_;
private:
mutable bdd last_support_conditions_output_;
protected:
// Boolean properties. Beware: true means that the property
// holds, but false means the property is unknown.
struct bprop
{
bool state_based_acc:1; // State-based acceptance.
bool inherently_weak:1; // Weak automaton.
bool deterministic:1; // Deterministic automaton.
bool stutter_inv:1; // Stutter invariant
};
union
{
unsigned props;
bprop is;
};
#ifndef SWIG
// Dynamic properties, are given with a name and a destructor function.
std::unordered_map