diff --git a/spot/mc/mc_instanciator.hh b/spot/mc/mc_instanciator.hh index 7f7e5123b..7d63c7442 100644 --- a/spot/mc/mc_instanciator.hh +++ b/spot/mc/mc_instanciator.hh @@ -36,6 +36,47 @@ namespace spot { + /// \brief This class allows to ensure (at compile time) if + /// a given parameter can be compsidered as a modelchecking algorithm + /// (i.e., usable by instanciate) + template + class SPOT_API is_a_mc_algorithm + { + private: + using yes = std::true_type; + using no = std::false_type; + + // Hardly waiting C++ concepts... + template static auto test_mc_algo(U u) + -> decltype( + // Check the kripke + std::is_samesetup())>::value && + std::is_samerun())>::value && + std::is_samefinalize())>::value && + std::is_samefinisher())>::value && + std::is_samestates())>::value && + std::is_sametransitions())>::value && + std::is_samewalltime())>::value && + std::is_samename())>::value && + std::is_samesccs())>::value && + std::is_sameresult())>::value && + std::is_sametrace())>::value + + // finally return the type "yes" + , yes()); + + // For all other cases return the type "no" + template static no test_mc_algo(...); + + public: + + /// \brief Checking this value will ensure, at compile time, that the + /// Kripke specialisation respects the required interface. + static constexpr bool value = + std::is_same< decltype(test_mc_algo(nullptr)), yes>::value; + }; + + template static SPOT_API ec_stats instanciate(kripke_ptr sys, @@ -60,6 +101,10 @@ namespace spot { ss[i] = algo_name::make_shared_structure(map, i); swarmed[i] = new algo_name(*sys, prop, map, ss[i], i, stop); + + static_assert(spot::is_a_mc_algorithm::value, + "error: does not match the kripkecube requirements"); + } tm.stop("Initialisation");