From 35c57fe980126beb5d1e93a1a4df7ea30736fcfc Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 7 Aug 2020 11:52:59 +0200 Subject: [PATCH] LraViHelper: Put component utility functions to separate file. --- .../internal/ComponentUtility.h | 22 +++++++++++++++++++ .../infinitehorizon/internal/LraViHelper.cpp | 14 ++---------- 2 files changed, 24 insertions(+), 12 deletions(-) create mode 100644 src/storm/modelchecker/helper/infinitehorizon/internal/ComponentUtility.h diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/ComponentUtility.h b/src/storm/modelchecker/helper/infinitehorizon/internal/ComponentUtility.h new file mode 100644 index 000000000..221dc0430 --- /dev/null +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/ComponentUtility.h @@ -0,0 +1,22 @@ +#pragma once + +namespace storm { + namespace modelchecker { + namespace helper { + namespace internal { + + /// 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; } + // 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(); } + } + } + } +} \ No newline at end of file diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp index af4ab9dfd..3e4dfaa69 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp @@ -1,5 +1,7 @@ #include "LraViHelper.h" +#include "storm/modelchecker/helper/infinitehorizon/internal/ComponentUtility.h" + #include "storm/solver/LinearEquationSolver.h" #include "storm/solver/MinMaxLinearEquationSolver.h" #include "storm/solver/Multiplier.h" @@ -25,18 +27,6 @@ namespace storm { namespace helper { namespace internal { - /// Auxiliary functions that deal with the different kinds of components (MECs on potentially nondeterministic models and BSCCs on deterministic models) - // BSCCS: - uint64_t getComponentElementState(typename storm::storage::StronglyConnectedComponent::value_type const& element) { return element; } - uint64_t getComponentElementChoiceCount(typename storm::storage::StronglyConnectedComponent::value_type const& element) { return 1; } // Assumes deterministic model! - uint64_t const* getComponentChoicesBegin(typename storm::storage::StronglyConnectedComponent::value_type const& element) { return &element; } - uint64_t const* getComponentChoicesEnd(typename storm::storage::StronglyConnectedComponent::value_type const& element) { return &element + 1; } - // MECS: - uint64_t getComponentElementState(typename storm::storage::MaximalEndComponent::map_type::value_type const& element) { return element.first; } - uint64_t getComponentElementChoiceCount(typename storm::storage::MaximalEndComponent::map_type::value_type const& element) { return element.second.size(); } - typename storm::storage::MaximalEndComponent::set_type::const_iterator getComponentChoicesBegin(typename storm::storage::MaximalEndComponent::map_type::value_type const& element) { return element.second.begin(); } - typename storm::storage::MaximalEndComponent::set_type::const_iterator getComponentChoicesEnd(typename storm::storage::MaximalEndComponent::map_type::value_type const& element) { return element.second.end(); } - template LraViHelper::LraViHelper(ComponentType const& component, storm::storage::SparseMatrix const& transitionMatrix, ValueType const& aperiodicFactor, storm::storage::BitVector const* timedStates, std::vector const* exitRates) : _component(component), _transitionMatrix(transitionMatrix), _timedStates(timedStates), _hasInstantStates(TransitionsType == LraViTransitionsType::DetTsNondetIs || TransitionsType == LraViTransitionsType::DetTsDetIs) { // Run through the component and collect some data: