diff --git a/spot/kripke/kripke.hh b/spot/kripke/kripke.hh index 0720e0d23..5a186bea8 100644 --- a/spot/kripke/kripke.hh +++ b/spot/kripke/kripke.hh @@ -20,9 +20,73 @@ #pragma once #include +#include namespace spot { + /// \brief This class is a template representation of a Kripke + /// structure. It is composed of two template parameters: State + /// represents a state of the Kripke structure, SuccIterator is + /// an iterator over the (possible) successors of a state. + /// + /// Do not delete by hand any states and/or iterator that + /// are provided by this template class. Specialisations + /// will handle it. + template + class SPOT_API kripkecube + { + public: + /// \brief Returns the initial State of the System + State initial(); + + /// \brief Provides a string representation of the parameter state + std::string to_string(const State) const; + + /// \brief Returns an iterator over the successors of the parameter state. + SuccIterator* succ(const State); + + /// \brief Allocation and deallocation of iterator is costly. This + /// method allows to reuse old iterators. + void recycle(SuccIterator*); + + /// \brief This method allow to deallocate a given state. + const std::vector get_ap(); + }; + + /// \brief This method allows to ensure (at compile time) if + /// a given parameter is of type kripkecube. It also check + /// if the iterator has the good interface. + template + bool is_a_kripkecube(kripkecube&) + { + // Hardly waiting C++17 concepts... + State (kripkecube::*test_initial)() = + &kripkecube::initial; + std::string (kripkecube::*test_to_string) + (const State) const = &kripkecube::to_string; + auto (kripkecube::*test_recycle)(SuccIter*) = + &kripkecube::recycle; + const std::vector + (kripkecube::*test_get_ap)() = + &kripkecube::get_ap; + void (SuccIter::*test_next)() = &SuccIter::next; + State (SuccIter::*test_state)() const= &SuccIter::state; + bool (SuccIter::*test_done)() const= &SuccIter::done; + cube (SuccIter::*test_condition)() const = &SuccIter::condition; + + // suppress warnings about unused variables + (void) test_initial; + (void) test_to_string; + (void) test_recycle; + (void) test_get_ap; + (void) test_next; + (void) test_state; + (void) test_done; + (void) test_condition; + + // Always return true since otherwise a compile-time error will be raised. + return true; + }; /// \ingroup kripke /// \brief Iterator code for Kripke structure