diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/ComponentUtility.h b/src/storm/modelchecker/helper/infinitehorizon/internal/ComponentUtility.h index 221dc0430..2a9d62415 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/internal/ComponentUtility.h +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/ComponentUtility.h @@ -1,5 +1,8 @@ #pragma once +#include "storm/storage/StronglyConnectedComponent.h" +#include "storm/storage/MaximalEndComponent.h" + namespace storm { namespace modelchecker { namespace helper { @@ -7,15 +10,17 @@ namespace storm { /// Auxiliary functions that deal with the different kinds of components (MECs on potentially nondeterministic models and BSCCs on deterministic models) // BSCCS: - uint64_t inline getComponentElementState(typename storm::storage::StronglyConnectedComponent::value_type const& element) { return element; } - uint64_t inline getComponentElementChoiceCount(typename storm::storage::StronglyConnectedComponent::value_type const& element) { return 1; } // Assumes deterministic model! - uint64_t inline const* getComponentChoicesBegin(typename storm::storage::StronglyConnectedComponent::value_type const& element) { return &element; } - uint64_t inline const* getComponentChoicesEnd(typename storm::storage::StronglyConnectedComponent::value_type const& element) { return &element + 1; } + inline uint64_t getComponentElementState(typename storm::storage::StronglyConnectedComponent::value_type const& element) { return element; } + inline uint64_t getComponentElementChoiceCount(typename storm::storage::StronglyConnectedComponent::value_type const& element) { return 1; } // Assumes deterministic model! + inline uint64_t const* getComponentElementChoicesBegin(typename storm::storage::StronglyConnectedComponent::value_type const& element) { return &element; } + inline uint64_t const* getComponentElementChoicesEnd(typename storm::storage::StronglyConnectedComponent::value_type const& element) { return &element + 1; } + inline bool componentElementChoicesContains(typename storm::storage::StronglyConnectedComponent::value_type const& element, uint64_t choice) { return element == choice; } // MECS: - uint64_t inline getComponentElementState(typename storm::storage::MaximalEndComponent::map_type::value_type const& element) { return element.first; } - uint64_t inline getComponentElementChoiceCount(typename storm::storage::MaximalEndComponent::map_type::value_type const& element) { return element.second.size(); } - typename storm::storage::MaximalEndComponent::set_type::const_iterator inline getComponentChoicesBegin(typename storm::storage::MaximalEndComponent::map_type::value_type const& element) { return element.second.begin(); } - typename storm::storage::MaximalEndComponent::set_type::const_iterator inline getComponentChoicesEnd(typename storm::storage::MaximalEndComponent::map_type::value_type const& element) { return element.second.end(); } + inline uint64_t getComponentElementState(typename storm::storage::MaximalEndComponent::map_type::value_type const& element) { return element.first; } + inline uint64_t getComponentElementChoiceCount(typename storm::storage::MaximalEndComponent::map_type::value_type const& element) { return element.second.size(); } + inline typename storm::storage::MaximalEndComponent::set_type::const_iterator getComponentElementChoicesBegin(typename storm::storage::MaximalEndComponent::map_type::value_type const& element) { return element.second.begin(); } + inline typename storm::storage::MaximalEndComponent::set_type::const_iterator getComponentElementChoicesEnd(typename storm::storage::MaximalEndComponent::map_type::value_type const& element) { return element.second.end(); } + inline bool componentElementChoicesContains(storm::storage::MaximalEndComponent::map_type::value_type const& element, uint64_t choice) { return element.second.contains(choice); } } } }