From f74417648165d01b8238fe45046ab8c8faffad1a Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 14 Sep 2020 19:17:30 +0200 Subject: [PATCH 1/2] Fixed lib filename for carl (Fixes #85) --- resources/3rdparty/CMakeLists.txt | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 170e72033..3379689bf 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -347,7 +347,11 @@ if (STORM_SHIPPED_CARL) message(STATUS "Storm - Linking with shipped carl ${carl_VERSION} (include: ${carl_INCLUDE_DIR}, library ${carl_LIBRARIES}, CARL_USE_CLN_NUMBERS: ${CARL_USE_CLN_NUMBERS}, CARL_USE_GINAC: ${CARL_USE_GINAC}).") # install the carl dynamic library if we built it - install(FILES ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl.${carl_VERSION}${DYNAMIC_EXT} DESTINATION lib) + if(MACOSX) + install(FILES ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl.${carl_VERSION}${DYNAMIC_EXT} DESTINATION lib) + else() + install(FILES ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl${DYNAMIC_EXT}.${carl_VERSION} DESTINATION lib) + endif() endif() if(STORM_USE_CLN_RF AND NOT STORM_HAVE_CLN) From f100ff62750da1413859da87dc131dd537e5ac06 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 28 Sep 2020 11:12:38 +0200 Subject: [PATCH 2/2] LraViHelper: Fixed unordered insertion into SparseMatrixBuilder. --- .../infinitehorizon/internal/LraViHelper.cpp | 58 +++++++++++++------ .../infinitehorizon/internal/LraViHelper.h | 7 ++- 2 files changed, 45 insertions(+), 20 deletions(-) diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp index e1302665f..eb8c002ed 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp @@ -25,7 +25,9 @@ namespace storm { namespace internal { 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), _Tsx1IsCurrent(false) { + LraViHelper::LraViHelper(ComponentType const& component, storm::storage::SparseMatrix const& transitionMatrix, ValueType const& aperiodicFactor, storm::storage::BitVector const* timedStates, std::vector const* exitRates) : _transitionMatrix(transitionMatrix), _timedStates(timedStates), _hasInstantStates(TransitionsType == LraViTransitionsType::DetTsNondetIs || TransitionsType == LraViTransitionsType::DetTsDetIs), _Tsx1IsCurrent(false) { + setComponent(component); + // Run through the component and collect some data: // We create two submodels, one consisting of the timed states of the component and one consisting of the instant states of the component. // For this, we create a state index map that point from state indices of the input model to indices of the corresponding submodel of that state. @@ -38,20 +40,20 @@ namespace storm { _uniformizationRate = exitRates == nullptr ? storm::utility::one() : storm::utility::zero(); // Now run over the MEC and collect the required data. for (auto const& element : _component) { - uint64_t componentState = getComponentElementState(element); + uint64_t componentState = element.first; if (isTimedState(componentState)) { toSubModelStateMapping.emplace(componentState, numTsSubModelStates); ++numTsSubModelStates; - numTsSubModelChoices += getComponentElementChoiceCount(element); - STORM_LOG_ASSERT(nondetTs() || getComponentElementChoiceCount(element) == 1, "Timed state has multiple choices but only a single choice was expected."); + numTsSubModelChoices += element.second.size(); + STORM_LOG_ASSERT(nondetTs() || element.second.size() == 1, "Timed state has multiple choices but only a single choice was expected."); if (exitRates) { _uniformizationRate = std::max(_uniformizationRate, (*exitRates)[componentState]); } } else { toSubModelStateMapping.emplace(componentState, numIsSubModelStates); ++numIsSubModelStates; - numIsSubModelChoices += getComponentElementChoiceCount(element); - STORM_LOG_ASSERT(nondetIs() || getComponentElementChoiceCount(element) == 1, "Instant state has multiple choices but only a single choice was expected."); + numIsSubModelChoices += element.second.size(); + STORM_LOG_ASSERT(nondetIs() || element.second.size() == 1, "Instant state has multiple choices but only a single choice was expected."); } } assert(numIsSubModelStates + numTsSubModelStates == _component.size()); @@ -78,7 +80,7 @@ namespace storm { uint64_t currTsRow = 0; uint64_t currIsRow = 0; for (auto const& element : _component) { - uint64_t componentState = getComponentElementState(element); + uint64_t componentState = element.first; if (isTimedState(componentState)) { // The currently processed state is timed. if (nondetTs()) { @@ -93,9 +95,9 @@ namespace storm { } // We need to uniformize which means that a diagonal entry for the selfloop will be inserted. ValueType selfLoopProb = storm::utility::one() - uniformizationFactor; - for (auto componentChoiceIt = getComponentElementChoicesBegin(element); componentChoiceIt != getComponentElementChoicesEnd(element); ++componentChoiceIt) { + for (auto const& componentChoice : element.second) { tsTransitionsBuilder.addDiagonalEntry(currTsRow, selfLoopProb); - for (auto const& entry : this->_transitionMatrix.getRow(*componentChoiceIt)) { + for (auto const& entry : this->_transitionMatrix.getRow(componentChoice)) { uint64_t subModelColumn = toSubModelStateMapping[entry.getColumn()]; if (isTimedState(entry.getColumn())) { // We have a transition from a timed state to a timed state @@ -115,8 +117,8 @@ namespace storm { isTransitionsBuilder.newRowGroup(currIsRow); isToTsTransitionsBuilder.newRowGroup(currIsRow); } - for (auto componentChoiceIt = getComponentElementChoicesBegin(element); componentChoiceIt != getComponentElementChoicesEnd(element); ++componentChoiceIt) { - for (auto const& entry : this->_transitionMatrix.getRow(*componentChoiceIt)) { + for (auto const& componentChoice : element.second) { + for (auto const& entry : this->_transitionMatrix.getRow(componentChoice)) { uint64_t subModelColumn = toSubModelStateMapping[entry.getColumn()]; if (isTimedState(entry.getColumn())) { // We have a transition from an instant state to a timed state @@ -140,6 +142,20 @@ namespace storm { } } + template + void LraViHelper::setComponent(ComponentType component) { + _component.clear(); + for (auto const& element : component) { + uint64_t componentState = getComponentElementState(element); + std::set componentChoices; + for (auto componentChoiceIt = getComponentElementChoicesBegin(element); componentChoiceIt != getComponentElementChoicesEnd(element); ++componentChoiceIt) { + componentChoices.insert(*componentChoiceIt); + } + _component.emplace(std::move(componentState), std::move(componentChoices)); + } + } + + template ValueType LraViHelper::performValueIteration(Environment const& env, ValueGetter const& stateValueGetter, ValueGetter const& actionValueGetter, std::vector const* exitRates, storm::solver::OptimizationDirection const* dir, std::vector* choices) { initializeNewValues(stateValueGetter, actionValueGetter, exitRates); @@ -199,20 +215,20 @@ namespace storm { // Set the new choice-based values ValueType actionRewardScalingFactor = storm::utility::one() / _uniformizationRate; for (auto const& element : _component) { - uint64_t componentState = getComponentElementState(element); + uint64_t componentState = element.first; if (isTimedState(componentState)) { if (exitRates) { actionRewardScalingFactor = (*exitRates)[componentState] / _uniformizationRate; } - for (auto componentChoiceIt = getComponentElementChoicesBegin(element); componentChoiceIt != getComponentElementChoicesEnd(element); ++componentChoiceIt) { + for (auto const& componentChoice : element.second) { // Compute the values obtained for this choice. - _TsChoiceValues.push_back(stateValueGetter(componentState) / _uniformizationRate + actionValueGetter(*componentChoiceIt) * actionRewardScalingFactor); + _TsChoiceValues.push_back(stateValueGetter(componentState) / _uniformizationRate + actionValueGetter(componentChoice) * actionRewardScalingFactor); } } else { - for (auto componentChoiceIt = getComponentElementChoicesBegin(element); componentChoiceIt != getComponentElementChoicesEnd(element); ++componentChoiceIt) { + for (auto const& componentChoice : element.second) { // Compute the values obtained for this choice. // State values do not count here since no time passes in instant states. - _IsChoiceValues.push_back(actionValueGetter(*componentChoiceIt)); + _IsChoiceValues.push_back(actionValueGetter(componentChoice)); } } } @@ -301,13 +317,17 @@ namespace storm { // Transform the local choices (within this mec) to choice indices for the input model uint64_t localState = 0; for (auto const& element : _component) { - uint64_t elementState = getComponentElementState(element); + uint64_t elementState = element.first; if ((setChoiceZeroToTimedStates && isTimedState(elementState)) || (setChoiceZeroToInstantStates && !isTimedState(elementState))) { choices[elementState] = 0; } else { uint64_t choice = localMecChoices[localState]; - STORM_LOG_ASSERT(choice < getComponentElementChoiceCount(element), "The selected choice does not seem to exist."); - uint64_t globalChoiceIndex = *(getComponentElementChoicesBegin(element) + choice); + STORM_LOG_ASSERT(choice < element.second.size(), "The selected choice does not seem to exist."); + auto globalChoiceIndexIt = element.second.begin(); + for (uint64_t i = 0; i < choice; ++i) { + ++globalChoiceIndexIt; + } + uint64_t globalChoiceIndex = *(globalChoiceIndexIt); choices[elementState] = globalChoiceIndex - _transitionMatrix.getRowGroupIndices()[elementState]; ++localState; } diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h index 7cb62e9a6..bbf9207a4 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h @@ -128,8 +128,13 @@ namespace storm { bool nondetIs() const; + void setComponent(ComponentType component); - ComponentType const& _component; + // We need to make sure that states/choices will be processed in ascending order + typedef std::map> InternalComponentType; + + + InternalComponentType _component; storm::storage::SparseMatrix const& _transitionMatrix; storm::storage::BitVector const* _timedStates; // e.g. Markovian states of a Markov automaton. bool _hasInstantStates;