From 562198b95d9b44c01ae9e8b6f01738c15b4caae9 Mon Sep 17 00:00:00 2001 From: Alex Bork Date: Tue, 18 Aug 2026 15:31:51 +0200 Subject: [PATCH 01/11] Changes to Storm for revised belief exploration --- src/storm/logic/BoundedUntilFormula.cpp | 16 ++ src/storm/logic/BoundedUntilFormula.h | 3 + .../SparseModelValueTypeTransformer.cpp | 114 +++++++++ .../SparseModelValueTypeTransformer.h | 23 ++ .../TransitionToActionRewardTransformer.cpp | 232 ++++++++++++++++++ .../TransitionToActionRewardTransformer.h | 42 ++++ 6 files changed, 430 insertions(+) create mode 100644 src/storm/transformer/SparseModelValueTypeTransformer.cpp create mode 100644 src/storm/transformer/SparseModelValueTypeTransformer.h create mode 100644 src/storm/transformer/TransitionToActionRewardTransformer.cpp create mode 100644 src/storm/transformer/TransitionToActionRewardTransformer.h diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp index d97b4341d7..ab8389d182 100644 --- a/src/storm/logic/BoundedUntilFormula.cpp +++ b/src/storm/logic/BoundedUntilFormula.cpp @@ -251,6 +251,22 @@ storm::expressions::Expression const& BoundedUntilFormula::getUpperBound(unsigne return upperBound.at(i).get().getBound(); } +std::optional BoundedUntilFormula::getLowerBoundAsOptionalTimeBound(unsigned i) const { + if (hasLowerBound(i)) { + return lowerBound.at(i).get(); + } else { + return std::nullopt; + } +} + +std::optional BoundedUntilFormula::getUpperBoundAsOptionalTimeBound(unsigned i) const { + if (hasUpperBound(i)) { + return upperBound.at(i).get(); + } else { + return std::nullopt; + } +} + template<> double BoundedUntilFormula::getLowerBound(unsigned i) const { if (!hasLowerBound(i)) { diff --git a/src/storm/logic/BoundedUntilFormula.h b/src/storm/logic/BoundedUntilFormula.h index 1e82ff4926..e70ce26172 100644 --- a/src/storm/logic/BoundedUntilFormula.h +++ b/src/storm/logic/BoundedUntilFormula.h @@ -59,6 +59,9 @@ class BoundedUntilFormula : public PathFormula { storm::expressions::Expression const& getLowerBound(unsigned i = 0) const; storm::expressions::Expression const& getUpperBound(unsigned i = 0) const; + std::optional getLowerBoundAsOptionalTimeBound(unsigned i = 0) const; + std::optional getUpperBoundAsOptionalTimeBound(unsigned i = 0) const; + template ValueType getLowerBound(unsigned i = 0) const; diff --git a/src/storm/transformer/SparseModelValueTypeTransformer.cpp b/src/storm/transformer/SparseModelValueTypeTransformer.cpp new file mode 100644 index 0000000000..eb4c9ec3eb --- /dev/null +++ b/src/storm/transformer/SparseModelValueTypeTransformer.cpp @@ -0,0 +1,114 @@ +#include "SparseModelValueTypeTransformer.h" + +#include "storm/exceptions/IllegalArgumentTypeException.h" +#include "storm/models/sparse/Ctmc.h" +#include "storm/models/sparse/Dtmc.h" +#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/Pomdp.h" +#include "storm/models/sparse/Smg.h" +#include "storm/models/sparse/StochasticTwoPlayerGame.h" +#include "storm/storage/sparse/ModelComponents.h" +#include "storm/utility/macros.h" +#include "storm/utility/vector.h" + +namespace storm::transformer { +template +std::shared_ptr> SparseModelValueTypeTransformer::transformModel( + std::shared_ptr> const& inputModel) { + STORM_LOG_THROW(inputModel, storm::exceptions::IllegalArgumentTypeException, "Cannot transform a null model."); + storm::storage::sparse::ModelComponents convertedComponents; + convertedComponents.transitionMatrix = inputModel->getTransitionMatrix().template toValueType(); + convertedComponents.choiceLabeling = inputModel->getOptionalChoiceLabeling(); + convertedComponents.stateLabeling = inputModel->getStateLabeling(); + convertedComponents.stateValuations = inputModel->getOptionalStateValuations(); + convertedComponents.choiceOrigins = inputModel->getOptionalChoiceOrigins(); + for (auto const& [rewardModelName, rewardModel] : inputModel->getRewardModels()) { + // Transform reward models + std::optional> optionalStateRewardVector = std::nullopt; + std::optional> optionalStateActionRewardVector = std::nullopt; + std::optional> optionalTransitionRewardMatrix = std::nullopt; + if (rewardModel.hasStateRewards()) { + std::vector resultVector; + resultVector.reserve(rewardModel.getStateRewardVector().size()); + for (auto const& oldValue : rewardModel.getStateRewardVector()) { + resultVector.push_back(storm::utility::convertNumber(oldValue)); + } + optionalStateRewardVector = resultVector; + } + if (rewardModel.hasStateActionRewards()) { + std::vector resultVector; + resultVector.reserve(rewardModel.getStateActionRewardVector().size()); + for (auto const& oldValue : rewardModel.getStateActionRewardVector()) { + resultVector.push_back(storm::utility::convertNumber(oldValue)); + } + optionalStateActionRewardVector = resultVector; + } + if (rewardModel.hasTransitionRewards()) { + optionalTransitionRewardMatrix = rewardModel.getTransitionRewardMatrix().template toValueType(); + } + convertedComponents.rewardModels.emplace( + rewardModelName, storm::models::sparse::StandardRewardModel( + std::move(optionalStateRewardVector), std::move(optionalStateActionRewardVector), std::move(optionalTransitionRewardMatrix))); + } + switch (inputModel->getType()) { + case storm::models::ModelType::Dtmc: + return std::make_shared>(storm::models::sparse::Dtmc(convertedComponents)); + case storm::models::ModelType::Mdp: + return std::make_shared>(storm::models::sparse::Mdp(convertedComponents)); + case storm::models::ModelType::Ctmc: { + auto ctmc = inputModel->template as>(); + std::vector resultVector; + resultVector.reserve(ctmc->getExitRateVector().size()); + for (auto const& oldValue : ctmc->getExitRateVector()) { + resultVector.push_back(storm::utility::convertNumber(oldValue)); + } + convertedComponents.exitRates = resultVector; + // Markov automata store probabilities in their transition matrix and rates separately in exitRates. + convertedComponents.rateTransitions = false; + return std::make_shared>(storm::models::sparse::Ctmc(convertedComponents)); + } + case storm::models::ModelType::MarkovAutomaton: { + auto ma = inputModel->template as>(); + std::vector resultVector; + resultVector.reserve(ma->getExitRates().size()); + for (auto const& oldValue : ma->getExitRates()) { + resultVector.push_back(storm::utility::convertNumber(oldValue)); + } + convertedComponents.exitRates = resultVector; + convertedComponents.rateTransitions = true; + convertedComponents.markovianStates = ma->getMarkovianStates(); + return std::make_shared>( + storm::models::sparse::MarkovAutomaton(convertedComponents)); + } + case storm::models::ModelType::Pomdp: { + auto pomdp = inputModel->template as>(); + convertedComponents.observabilityClasses = pomdp->getObservations(); + convertedComponents.observationValuations = pomdp->getOptionalObservationValuations(); + return std::make_shared>(models::sparse::Pomdp(convertedComponents, pomdp->isCanonic())); + } + case storm::models::ModelType::Smg: { + auto smg = inputModel->template as>(); + convertedComponents.statePlayerIndications = smg->getStatePlayerIndications(); + convertedComponents.playerNameToIndexMap = smg->getPlayerNamesToIndex(); + return std::make_shared>(models::sparse::Smg(convertedComponents)); + } + case storm::models::ModelType::S2pg: { + auto s2pg = inputModel->template as>(); + convertedComponents.player1Matrix = s2pg->getPlayer1Matrix(); + return std::make_shared>( + models::sparse::StochasticTwoPlayerGame(convertedComponents)); + } + default: + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentTypeException, + "Value type transformation is not supported for models of type " << inputModel->getType() << "."); + } + return nullptr; +} + +template class SparseModelValueTypeTransformer; +template class SparseModelValueTypeTransformer; +template class SparseModelValueTypeTransformer; +template class SparseModelValueTypeTransformer; + +} // namespace storm::transformer diff --git a/src/storm/transformer/SparseModelValueTypeTransformer.h b/src/storm/transformer/SparseModelValueTypeTransformer.h new file mode 100644 index 0000000000..f6f02ca7e0 --- /dev/null +++ b/src/storm/transformer/SparseModelValueTypeTransformer.h @@ -0,0 +1,23 @@ +#pragma once + +#include + +#include "storm/models/sparse/Model.h" + +namespace storm::transformer { + +template +/** Converts the numeric values of a sparse model while preserving its model-specific metadata. */ +class SparseModelValueTypeTransformer { + public: + explicit SparseModelValueTypeTransformer() = default; + + /** + * Returns a model equivalent to @p inputModel with all probabilities, rates, and rewards converted to OutputValueType. + * + * @pre inputModel is not null. + */ + std::shared_ptr> transformModel(std::shared_ptr> const& inputModel); +}; + +} // namespace storm::transformer diff --git a/src/storm/transformer/TransitionToActionRewardTransformer.cpp b/src/storm/transformer/TransitionToActionRewardTransformer.cpp new file mode 100644 index 0000000000..eb84521130 --- /dev/null +++ b/src/storm/transformer/TransitionToActionRewardTransformer.cpp @@ -0,0 +1,232 @@ +#include "storm/transformer/TransitionToActionRewardTransformer.h" + +#include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/adapters/RationalNumberAdapter.h" +#include "storm/exceptions/UnexpectedException.h" +#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/storage/SparseMatrix.h" +#include "storm/storage/sparse/ModelComponents.h" +#include "storm/utility/OptionalRef.h" +#include "storm/utility/builder.h" +#include "storm/utility/macros.h" +#include "storm/utility/vector.h" + +namespace storm::transformer { + +namespace detail { +template +using MultiRewardVector = std::vector; + +template +class RewardTransitionIterator { + public: + RewardTransitionIterator(storm::storage::SparseMatrix const& m) : transitionMatrix(m) {} + + void addRewardModel(storm::models::sparse::StandardRewardModel const& rewardModel) { + if (rewardModel.hasTransitionRewards()) { + transitionRewards.emplace_back(rewardModel.getTransitionRewardMatrix()); + STORM_LOG_ASSERT(transitionRewards.back()->isSubmatrixOf(transitionMatrix), "Invalid reward matrix."); + } else { + transitionRewards.emplace_back(); + } + } + + template + void forEachRowEntry(uint64_t rowIndex, bool skip0RewardEntries, CallBackType&& callBack) { + // Set-up iterators + std::vector::const_iterator> rewardIterators; + std::vector::const_iterator> rewardIteratorsEnd; + for (auto const& rewardMatrix : transitionRewards) { + if (rewardMatrix) { + rewardIterators.push_back(rewardMatrix->begin(rowIndex)); + rewardIteratorsEnd.push_back(rewardMatrix->end(rowIndex)); + } else { + rewardIterators.emplace_back(); + rewardIteratorsEnd.emplace_back(); + } + } + + std::vector rewards(transitionRewards.size()); + for (auto const& entry : transitionMatrix.getRow(rowIndex)) { + // Fill in rewards for this entry + bool skipEntry = skip0RewardEntries; + for (uint64_t i = 0; i < transitionRewards.size(); ++i) { + if (rewardIterators[i] != rewardIteratorsEnd[i] && rewardIterators[i]->getColumn() == entry.getColumn()) { + rewards[i] = rewardIterators[i]->getValue(); + ++rewardIterators[i]; + skipEntry = skipEntry && storm::utility::isZero(rewards[i]); + } else { + rewards[i] = storm::utility::zero(); + } + } + if (!skipEntry) { + callBack(entry.getColumn(), entry.getValue(), rewards); + } + } + } + + private: + storm::storage::SparseMatrix const& transitionMatrix; + std::vector const>> transitionRewards; +}; + +} // namespace detail + +template +TransitionToActionRewardTransformerReturnType transformTransitionToActionRewards( + std::shared_ptr> originalModel, std::vector const& relevantRewardModelNames) { + STORM_LOG_ASSERT(originalModel, "Model must not be null."); + detail::RewardTransitionIterator rewardTransitionIterator(originalModel->getTransitionMatrix()); + bool hasTransitionRewards = false; + for (auto const& rewardModelName : relevantRewardModelNames) { + auto const& rewardModel = originalModel->getRewardModel(rewardModelName); + if (rewardModel.hasTransitionRewards()) { + hasTransitionRewards = true; + } + rewardTransitionIterator.addRewardModel(rewardModel); + } + if (!hasTransitionRewards) { + return {originalModel->template as>(), + {storm::utility::vector::buildVectorForRange(0, originalModel->getNumberOfStates())}}; + } + + // Make a pass to find the different rewards with which a state is entered + std::vector>> incomingRewards(originalModel->getNumberOfStates()); + auto const& transitions = originalModel->getTransitionMatrix(); + for (uint64_t row = 0; row < transitions.getRowCount(); ++row) { + rewardTransitionIterator.forEachRowEntry( + row, true, + [&incomingRewards](uint64_t column, ValueType, detail::MultiRewardVector const& rewards) { incomingRewards[column].insert(rewards); }); + } + + // Create a mapping from original to new indices + std::vector originalToNewIndex; + uint64_t numStates = 0; + for (auto const& incRewardsSet : incomingRewards) { + numStates += incRewardsSet.size(); + originalToNewIndex.push_back(numStates); + ++numStates; + } + + // Populate the new transition matrix and (action) rewards for intermediate states + uint64_t const numIntermediateStates = numStates - originalModel->getNumberOfStates(); + bool const useGroups = !transitions.hasTrivialRowGrouping(); + storm::storage::SparseMatrixBuilder newTransitionsBuilder(transitions.getRowCount() + numIntermediateStates, numStates, + transitions.getEntryCount() + numIntermediateStates, true, useGroups, + useGroups ? numStates : 0ull); + std::vector> newActionRewards(relevantRewardModelNames.size(), + std::vector(transitions.getRowCount() + numIntermediateStates)); + uint64_t currNewRow = 0; + for (uint64_t currOrigState = 0; currOrigState < originalModel->getNumberOfStates(); ++currOrigState) { + uint64_t const currNewState = originalToNewIndex[currOrigState]; + // First add the transitions and rewards for the intermediate states + for (auto const& incRewardsSet : incomingRewards[currOrigState]) { + if (useGroups) { + newTransitionsBuilder.newRowGroup(currNewRow); + } + newTransitionsBuilder.addNextValue(currNewRow, currNewState, storm::utility::one()); + auto newRewIt = newActionRewards.begin(); + for (auto const& rew : incRewardsSet) { + (*newRewIt)[currNewRow] = rew; + ++newRewIt; + } + ++currNewRow; + } + // Add the transitions and rewards for the original state + if (useGroups) { + newTransitionsBuilder.newRowGroup(currNewRow); + } + for (auto origRowIndex : transitions.getRowGroupIndices(currOrigState)) { + rewardTransitionIterator.forEachRowEntry( + origRowIndex, false, + [&newTransitionsBuilder, &originalToNewIndex, &incomingRewards, &currNewRow](uint64_t column, ValueType prob, + detail::MultiRewardVector const& rewards) { + if (std::all_of(rewards.begin(), rewards.end(), [](ValueType const& r) { return storm::utility::isZero(r); })) { + // No transition reward collected so use originial state + newTransitionsBuilder.addNextValue(currNewRow, originalToNewIndex[column], prob); + } else { + // Redirect to intermediate state + auto incomingRewardsIt = incomingRewards[column].find(rewards); + STORM_LOG_ASSERT(incomingRewardsIt != incomingRewards[column].end(), "Invalid incoming rewards."); + uint64_t const intermediateStateIndex = + originalToNewIndex[column] - incomingRewards[column].size() + std::distance(incomingRewards[column].begin(), incomingRewardsIt); + newTransitionsBuilder.addNextValue(currNewRow, intermediateStateIndex, prob); + } + }); + ++currNewRow; + } + } + + // create new state labels and init components + storm::models::sparse::StateLabeling newLabeling(numStates); + for (auto const& l : originalModel->getStateLabeling().getLabels()) { + newLabeling.addLabel(l); + for (auto origIndex : originalModel->getStateLabeling().getStates(l)) { + newLabeling.addLabelToState(l, originalToNewIndex[origIndex]); + } + } + storm::storage::sparse::ModelComponents components(newTransitionsBuilder.build(), std::move(newLabeling)); + + // create new reward models + uint64_t rewardIndex = 0; + for (auto const& rewardModelName : relevantRewardModelNames) { + auto& newActionRewardVector = newActionRewards[rewardIndex++]; + auto const& oldRewardModel = originalModel->getRewardModel(rewardModelName); + for (uint64_t oldState = 0; oldState < originalModel->getNumberOfStates(); ++oldState) { + uint64_t const oldStartRow = transitions.getRowGroupIndices()[oldState]; + uint64_t const newState = originalToNewIndex[oldState]; + uint64_t const newStartRow = useGroups ? components.transitionMatrix.getRowGroupIndices()[newState] : newState; + uint64_t const numRowsInGroup = useGroups ? transitions.getRowGroupSize(oldState) : 1ull; + for (uint64_t groupOffset = 0; groupOffset < numRowsInGroup; ++groupOffset) { + auto& rewValue = newActionRewardVector[newStartRow + groupOffset]; + if (oldRewardModel.hasStateRewards()) { + rewValue += oldRewardModel.getStateReward(oldState); + } + if (oldRewardModel.hasStateActionRewards()) { + rewValue += oldRewardModel.getStateActionReward(oldStartRow + groupOffset); + } + } + } + storm::models::sparse::StandardRewardModel newRewardModel(std::nullopt, std::move(newActionRewardVector)); + components.rewardModels.emplace(rewardModelName, std::move(newRewardModel)); + } + + STORM_LOG_WARN_COND(!originalModel->hasChoiceLabeling(), "Choice labellings will be dropped as the transformation is currently not implemented."); + STORM_LOG_WARN_COND(!originalModel->hasStateValuations(), "State valuations will be dropped as the transformation is currently not implemented."); + STORM_LOG_WARN_COND(!originalModel->hasChoiceOrigins(), "Choice origins will be dropped as the transformation is currently not implemented."); + + // Model type specific components + if (originalModel->isOfType(storm::models::ModelType::MarkovAutomaton)) { + auto const& ma = *originalModel->template as>(); + components.markovianStates = storm::storage::BitVector(numStates); + components.exitRates = std::vector(numStates, storm::utility::zero()); + for (uint64_t origState = 0; origState < originalModel->getNumberOfStates(); ++origState) { + uint64_t const newState = originalToNewIndex[origState]; + if (ma.isMarkovianState(origState)) { + components.markovianStates->set(newState, true); + components.exitRates->at(newState) = ma.getExitRate(origState); + } + } + components.rateTransitions = false; // Note that originalModel->getTransitionMatrix() contains probabilities + } else if (originalModel->isOfType(storm::models::ModelType::Ctmc)) { + components.rateTransitions = true; + } else { + STORM_LOG_THROW(originalModel->isOfType(storm::models::ModelType::Dtmc) || originalModel->isOfType(storm::models::ModelType::Mdp), + storm::exceptions::UnexpectedException, "Unhandled model type."); + } + return {storm::utility::builder::buildModelFromComponents(originalModel->getType(), std::move(components)), std::move(originalToNewIndex)}; +} + +template struct TransitionToActionRewardTransformerReturnType; +template struct TransitionToActionRewardTransformerReturnType; +template struct TransitionToActionRewardTransformerReturnType; + +template TransitionToActionRewardTransformerReturnType transformTransitionToActionRewards( + std::shared_ptr> originalModel, std::vector const& relevantRewardModelNames); +template TransitionToActionRewardTransformerReturnType transformTransitionToActionRewards( + std::shared_ptr> originalModel, std::vector const& relevantRewardModelNames); +template TransitionToActionRewardTransformerReturnType transformTransitionToActionRewards( + std::shared_ptr> originalModel, std::vector const& relevantRewardModelNames); + +} // namespace storm::transformer diff --git a/src/storm/transformer/TransitionToActionRewardTransformer.h b/src/storm/transformer/TransitionToActionRewardTransformer.h new file mode 100644 index 0000000000..3af168f198 --- /dev/null +++ b/src/storm/transformer/TransitionToActionRewardTransformer.h @@ -0,0 +1,42 @@ +#pragma once + +#include +#include +#include + +#include "storm/models/sparse/Model.h" +#include "storm/storage/BitVector.h" + +namespace storm::transformer { + +template +struct TransitionToActionRewardTransformerReturnType { + std::shared_ptr> model; + std::vector originalToNewStateIndices; +}; +/*! + * + * Replaces transition branch rewards from all given reward models and replaces them by equivalent state-action based rewards. + * This is done by potentially adding intermediate states at which the corresponding reward is collected and which have a Dirac transition to the original + * state. + * Notes: + * - this construction potentially invalidates step-based properties, e.g., step-bounded reachability or discrete-time LRA properties. + * Also Until formulas with non-trivial left-hand-side will likely be invalidated + * - originalToNewStateIndices maps states of the original model to their positions within the transformed model. Those states are kept in the same order. + * - the introduced intermediate states that lead to original state 's' are located directly in front of 's'. + * - the number of intermediate states is kept small, e.g., if two distinct states 's_1' and 's_2' transition to 's' with the same transition reward + * (w.r.t. *all* reward models), only one intermediate state is introduced. + * - for Markov automata, the intermediate states are probabilistic (instantaneous). For CTMCs, the intermediate states have rate 1. + * - intermediate states do not get any label. All labels from the original model are preserved at the original states + * + * possible improvement: Preprocessing: move transition rewards to action if it is the same for all successor states + * + * @param originalModel The original model. + * @param relevantRewardModelNames The names of the reward models that should be transformed. Error if the model does not contain a reward model with this name. + * @return The transformed model and the positions of the original model states in the new (larger) transformed model. + */ +template +TransitionToActionRewardTransformerReturnType transformTransitionToActionRewards( + std::shared_ptr> originalModel, std::vector const& relevantRewardModelNames); + +} // namespace storm::transformer From 946179744181c9f21744cbc4250b538bcd8438d4 Mon Sep 17 00:00:00 2001 From: Alex Bork Date: Thu, 20 Aug 2026 12:39:46 +0200 Subject: [PATCH 02/11] Change boost::optional to std::optional in BoundedUntilFormula --- src/storm-gspn/builder/JaniGSPNBuilder.cpp | 3 +- .../SparseParametricDtmcSimplifier.cpp | 4 ++- .../SparseParametricMdpSimplifier.cpp | 4 ++- .../parser/FormulaParserGrammar.cpp | 35 +++++++++++++++---- src/storm-parsers/parser/JaniParser.cpp | 11 +++--- src/storm/logic/BoundedUntilFormula.cpp | 18 +++++----- src/storm/logic/BoundedUntilFormula.h | 13 ++++--- src/storm/logic/CloneVisitor.cpp | 3 +- .../logic/ExpressionSubstitutionVisitor.cpp | 3 +- .../ExtractMaximalStateFormulasVisitor.cpp | 3 +- .../RewardAccumulationEliminationVisitor.cpp | 3 +- .../RewardModelNameSubstitutionVisitor.cpp | 3 +- .../helper/rewardbounded/QuantileHelper.cpp | 11 +++--- 13 files changed, 73 insertions(+), 41 deletions(-) diff --git a/src/storm-gspn/builder/JaniGSPNBuilder.cpp b/src/storm-gspn/builder/JaniGSPNBuilder.cpp index 4cef958b08..7cedff54f8 100644 --- a/src/storm-gspn/builder/JaniGSPNBuilder.cpp +++ b/src/storm-gspn/builder/JaniGSPNBuilder.cpp @@ -1,6 +1,7 @@ #include "JaniGSPNBuilder.h" #include +#include #include "storm/logic/Formulas.h" @@ -310,7 +311,7 @@ std::vector JaniGSPNBuilder::getStandardProperties(storm: auto trueFormula = std::make_shared(true); auto reachTimeBoundFormula = std::make_shared( - std::make_shared(trueFormula, atomicFormula, boost::none, tb, tbr), + std::make_shared(trueFormula, atomicFormula, std::nullopt, tb, tbr), storm::logic::OperatorInformation(optimizationDirection)); standardProperties.emplace_back(dirShort + "PrReach" + name + "TB", reachTimeBoundFormula, emptySet, "The " + dirLong + " probability to reach " + description + " within 'TIME_BOUND' steps."); diff --git a/src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp b/src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp index 8ddebc5dca..9c86ccd1bf 100644 --- a/src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp +++ b/src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp @@ -1,5 +1,7 @@ #include "storm-pars/transformer/SparseParametricDtmcSimplifier.h" +#include + #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/exceptions/NotSupportedException.h" #include "storm/exceptions/UnexpectedException.h" @@ -132,7 +134,7 @@ bool SparseParametricDtmcSimplifier::simplifyForBoundedUntilPro // obtain the simplified formula for the simplified model auto labelFormula = std::make_shared(targetLabel); auto boundedUntilFormula = - std::make_shared(storm::logic::Formula::getTrueFormula(), labelFormula, boost::none, + std::make_shared(storm::logic::Formula::getTrueFormula(), labelFormula, std::nullopt, storm::logic::TimeBound(formula.getSubformula().asBoundedUntilFormula().isUpperBoundStrict(), formula.getSubformula().asBoundedUntilFormula().getUpperBound()), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Steps)); diff --git a/src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp b/src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp index eafa605ce8..7ab93a9f33 100644 --- a/src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp +++ b/src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp @@ -1,5 +1,7 @@ #include "storm-pars/transformer/SparseParametricMdpSimplifier.h" +#include + #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/exceptions/NotSupportedException.h" #include "storm/exceptions/UnexpectedException.h" @@ -159,7 +161,7 @@ bool SparseParametricMdpSimplifier::simplifyForBoundedUntilProb // obtain the simplified formula for the simplified model auto labelFormula = std::make_shared(targetLabel); auto boundedUntilFormula = - std::make_shared(storm::logic::Formula::getTrueFormula(), labelFormula, boost::none, + std::make_shared(storm::logic::Formula::getTrueFormula(), labelFormula, std::nullopt, storm::logic::TimeBound(formula.getSubformula().asBoundedUntilFormula().isUpperBoundStrict(), formula.getSubformula().asBoundedUntilFormula().getUpperBound()), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Steps)); diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index 7e2dd65d32..19a4c87314 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -1,6 +1,7 @@ #include "FormulaParserGrammar.h" #include +#include #include "storm/storage/expressions/ExpressionManager.h" @@ -473,11 +474,21 @@ std::shared_ptr FormulaParserGrammar::createEventua std::shared_ptr>>> const& timeBounds, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const { if (timeBounds && !timeBounds.get().empty()) { - std::vector> lowerBounds, upperBounds; + std::vector> lowerBounds, upperBounds; std::vector timeBoundReferences; for (auto const& timeBound : timeBounds.get()) { - lowerBounds.push_back(std::get<0>(timeBound)); - upperBounds.push_back(std::get<1>(timeBound)); + auto const& lowerBound = std::get<0>(timeBound); + auto const& upperBound = std::get<1>(timeBound); + if (lowerBound) { + lowerBounds.emplace_back(lowerBound.get()); + } else { + lowerBounds.emplace_back(); + } + if (upperBound) { + upperBounds.emplace_back(upperBound.get()); + } else { + upperBounds.emplace_back(); + } timeBoundReferences.emplace_back(*std::get<2>(timeBound)); } return std::shared_ptr( @@ -501,11 +512,21 @@ std::shared_ptr FormulaParserGrammar::createUntilFo std::shared_ptr>>> const& timeBounds, std::shared_ptr const& rightSubformula) { if (timeBounds && !timeBounds.get().empty()) { - std::vector> lowerBounds, upperBounds; + std::vector> lowerBounds, upperBounds; std::vector timeBoundReferences; for (auto const& timeBound : timeBounds.get()) { - lowerBounds.push_back(std::get<0>(timeBound)); - upperBounds.push_back(std::get<1>(timeBound)); + auto const& lowerBound = std::get<0>(timeBound); + auto const& upperBound = std::get<1>(timeBound); + if (lowerBound) { + lowerBounds.emplace_back(lowerBound.get()); + } else { + lowerBounds.emplace_back(); + } + if (upperBound) { + upperBounds.emplace_back(upperBound.get()); + } else { + upperBounds.emplace_back(); + } timeBoundReferences.emplace_back(*std::get<2>(timeBound)); } return std::shared_ptr( @@ -656,7 +677,7 @@ bool FormulaParserGrammar::isValidMultiBoundedPathFormulaOperand(std::shared_ptr std::shared_ptr FormulaParserGrammar::createMultiBoundedPathFormula( std::vector> const& subformulas) { std::vector> leftSubformulas, rightSubformulas; - std::vector> lowerBounds, upperBounds; + std::vector> lowerBounds, upperBounds; std::vector timeBoundReferences; for (auto const& subformula : subformulas) { STORM_LOG_THROW(subformula->isBoundedUntilFormula(), storm::exceptions::WrongFormatException, diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index d743cd2869..0089e89ffb 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/src/storm-parsers/parser/JaniParser.cpp @@ -33,6 +33,7 @@ #include #include #include +#include #include #include "storm/io/file.h" @@ -313,17 +314,17 @@ storm::logic::RewardAccumulation JaniParser::parseRewardAccumulation( return storm::logic::RewardAccumulation(accSteps, accTime, accExit); } -void insertLowerUpperTimeBounds(std::vector>& lowerBounds, - std::vector>& upperBounds, storm::jani::PropertyInterval const& pi) { +void insertLowerUpperTimeBounds(std::vector>& lowerBounds, + std::vector>& upperBounds, storm::jani::PropertyInterval const& pi) { if (pi.hasLowerBound()) { lowerBounds.push_back(storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound)); } else { - lowerBounds.push_back(boost::none); + lowerBounds.push_back(std::nullopt); } if (pi.hasUpperBound()) { upperBounds.push_back(storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound)); } else { - upperBounds.push_back(boost::none); + upperBounds.push_back(std::nullopt); } } @@ -516,7 +517,7 @@ std::shared_ptr JaniParser::parseFormula args[0] = storm::logic::BooleanLiteralFormula::getTrueFormula(); } - std::vector> lowerBounds, upperBounds; + std::vector> lowerBounds, upperBounds; std::vector tbReferences; if (propertyStructure.count("step-bounds") > 0) { STORM_LOG_WARN_COND(model.getJaniVersion() == 1, "Jani model not compliant: Contains step-bounds in " << scope.description << "."); diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp index d97b4341d7..387fa95c8f 100644 --- a/src/storm/logic/BoundedUntilFormula.cpp +++ b/src/storm/logic/BoundedUntilFormula.cpp @@ -14,7 +14,7 @@ namespace storm { namespace logic { BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, - boost::optional const& lowerBound, boost::optional const& upperBound, + std::optional const& lowerBound, std::optional const& upperBound, TimeBoundReference const& timeBoundReference) : PathFormula(), leftSubformula({leftSubformula}), @@ -26,7 +26,7 @@ BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr const& l } BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, - std::vector> const& lowerBounds, std::vector> const& upperBounds, + std::vector> const& lowerBounds, std::vector> const& upperBounds, std::vector const& timeBoundReferences) : PathFormula(), leftSubformula({leftSubformula}), @@ -40,7 +40,7 @@ BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr const& l BoundedUntilFormula::BoundedUntilFormula(std::vector> const& leftSubformulas, std::vector> const& rightSubformulas, - std::vector> const& lowerBounds, std::vector> const& upperBounds, + std::vector> const& lowerBounds, std::vector> const& upperBounds, std::vector const& timeBoundReferences) : PathFormula(), leftSubformula(leftSubformulas), @@ -199,7 +199,7 @@ bool BoundedUntilFormula::isLowerBoundStrict(unsigned i) const { if (!hasLowerBound(i)) { return false; } - return lowerBound.at(i).get().isStrict(); + return lowerBound.at(i).value().isStrict(); } bool BoundedUntilFormula::hasLowerBound() const { @@ -219,11 +219,11 @@ bool BoundedUntilFormula::hasIntegerLowerBound(unsigned i) const { if (!hasLowerBound(i)) { return true; } - return lowerBound.at(i).get().getBound().hasIntegerType(); + return lowerBound.at(i).value().getBound().hasIntegerType(); } bool BoundedUntilFormula::isUpperBoundStrict(unsigned i) const { - return upperBound.at(i).get().isStrict(); + return upperBound.at(i).value().isStrict(); } bool BoundedUntilFormula::hasUpperBound() const { @@ -240,15 +240,15 @@ bool BoundedUntilFormula::hasUpperBound(unsigned i) const { } bool BoundedUntilFormula::hasIntegerUpperBound(unsigned i) const { - return upperBound.at(i).get().getBound().hasIntegerType(); + return upperBound.at(i).value().getBound().hasIntegerType(); } storm::expressions::Expression const& BoundedUntilFormula::getLowerBound(unsigned i) const { - return lowerBound.at(i).get().getBound(); + return lowerBound.at(i).value().getBound(); } storm::expressions::Expression const& BoundedUntilFormula::getUpperBound(unsigned i) const { - return upperBound.at(i).get().getBound(); + return upperBound.at(i).value().getBound(); } template<> diff --git a/src/storm/logic/BoundedUntilFormula.h b/src/storm/logic/BoundedUntilFormula.h index 1e82ff4926..06d7515bf1 100644 --- a/src/storm/logic/BoundedUntilFormula.h +++ b/src/storm/logic/BoundedUntilFormula.h @@ -1,6 +1,6 @@ #pragma once -#include +#include #include "storm/logic/BinaryPathFormula.h" @@ -12,13 +12,12 @@ namespace logic { class BoundedUntilFormula : public PathFormula { public: BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, - boost::optional const& lowerBound, boost::optional const& upperBound, - TimeBoundReference const& timeBoundReference); + std::optional const& lowerBound, std::optional const& upperBound, TimeBoundReference const& timeBoundReference); BoundedUntilFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, - std::vector> const& lowerBounds, std::vector> const& upperBounds, + std::vector> const& lowerBounds, std::vector> const& upperBounds, std::vector const& timeBoundReferences); BoundedUntilFormula(std::vector> const& leftSubformulas, std::vector> const& rightSubformulas, - std::vector> const& lowerBounds, std::vector> const& upperBounds, + std::vector> const& lowerBounds, std::vector> const& upperBounds, std::vector const& timeBoundReferences); virtual bool isBoundedUntilFormula() const override; @@ -81,8 +80,8 @@ class BoundedUntilFormula : public PathFormula { std::vector> leftSubformula; std::vector> rightSubformula; std::vector timeBoundReference; - std::vector> lowerBound; - std::vector> upperBound; + std::vector> lowerBound; + std::vector> upperBound; }; } // namespace logic } // namespace storm diff --git a/src/storm/logic/CloneVisitor.cpp b/src/storm/logic/CloneVisitor.cpp index f3531aa60c..9a02149fb6 100644 --- a/src/storm/logic/CloneVisitor.cpp +++ b/src/storm/logic/CloneVisitor.cpp @@ -1,5 +1,6 @@ #include "storm/logic/CloneVisitor.h" #include +#include #include "storm/logic/Formulas.h" @@ -36,7 +37,7 @@ boost::any CloneVisitor::visit(BooleanLiteralFormula const& f, boost::any const& } boost::any CloneVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { - std::vector> lowerBounds, upperBounds; + std::vector> lowerBounds, upperBounds; std::vector timeBoundReferences; for (uint64_t i = 0; i < f.getDimension(); ++i) { if (f.hasLowerBound(i)) { diff --git a/src/storm/logic/ExpressionSubstitutionVisitor.cpp b/src/storm/logic/ExpressionSubstitutionVisitor.cpp index 0f6a7a87eb..2a58ea4ee4 100644 --- a/src/storm/logic/ExpressionSubstitutionVisitor.cpp +++ b/src/storm/logic/ExpressionSubstitutionVisitor.cpp @@ -1,5 +1,6 @@ #include "storm/logic/ExpressionSubstitutionVisitor.h" #include +#include #include "storm/logic/Formulas.h" @@ -52,7 +53,7 @@ boost::any ExpressionSubstitutionVisitor::visit(RewardOperatorFormula const& f, boost::any ExpressionSubstitutionVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { auto const& substitutionFunction = *boost::any_cast const*>(data); - std::vector> lowerBounds, upperBounds; + std::vector> lowerBounds, upperBounds; std::vector timeBoundReferences; for (uint64_t i = 0; i < f.getDimension(); ++i) { if (f.hasLowerBound(i)) { diff --git a/src/storm/logic/ExtractMaximalStateFormulasVisitor.cpp b/src/storm/logic/ExtractMaximalStateFormulasVisitor.cpp index fffdd79063..ef7787cfb2 100644 --- a/src/storm/logic/ExtractMaximalStateFormulasVisitor.cpp +++ b/src/storm/logic/ExtractMaximalStateFormulasVisitor.cpp @@ -1,5 +1,6 @@ #include "storm/logic/ExtractMaximalStateFormulasVisitor.h" #include +#include #include "storm/logic/Formulas.h" @@ -54,7 +55,7 @@ boost::any ExtractMaximalStateFormulasVisitor::visit(BoundedUntilFormula const& } // Copy bound information - std::vector> lowerBounds, upperBounds; + std::vector> lowerBounds, upperBounds; std::vector timeBoundReferences; for (uint64_t i = 0; i < f.getDimension(); ++i) { if (f.hasLowerBound(i)) { diff --git a/src/storm/logic/RewardAccumulationEliminationVisitor.cpp b/src/storm/logic/RewardAccumulationEliminationVisitor.cpp index 94703b8849..75210bacfa 100644 --- a/src/storm/logic/RewardAccumulationEliminationVisitor.cpp +++ b/src/storm/logic/RewardAccumulationEliminationVisitor.cpp @@ -1,5 +1,6 @@ #include "storm/logic/RewardAccumulationEliminationVisitor.h" #include +#include #include "storm/logic/Formulas.h" #include "storm/storage/jani/Model.h" @@ -37,7 +38,7 @@ void RewardAccumulationEliminationVisitor::eliminateRewardAccumulations(storm::j } boost::any RewardAccumulationEliminationVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { - std::vector> lowerBounds, upperBounds; + std::vector> lowerBounds, upperBounds; std::vector timeBoundReferences; for (uint64_t i = 0; i < f.getDimension(); ++i) { if (f.hasLowerBound(i)) { diff --git a/src/storm/logic/RewardModelNameSubstitutionVisitor.cpp b/src/storm/logic/RewardModelNameSubstitutionVisitor.cpp index fd8116a0ed..e1fbaea70a 100644 --- a/src/storm/logic/RewardModelNameSubstitutionVisitor.cpp +++ b/src/storm/logic/RewardModelNameSubstitutionVisitor.cpp @@ -1,5 +1,6 @@ #include "storm/logic/RewardModelNameSubstitutionVisitor.h" #include +#include #include "storm/logic/Formulas.h" #include "storm/storage/jani/Model.h" @@ -22,7 +23,7 @@ std::shared_ptr RewardModelNameSubstitutionVisitor::substitute(Formula } boost::any RewardModelNameSubstitutionVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { - std::vector> lowerBounds, upperBounds; + std::vector> lowerBounds, upperBounds; std::vector timeBoundReferences; for (uint64_t i = 0; i < f.getDimension(); ++i) { if (f.hasLowerBound(i)) { diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp index c3ebf31335..1bf217f4a1 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp @@ -2,6 +2,7 @@ #include #include +#include #include #include @@ -90,7 +91,7 @@ std::shared_ptr transformBoundedUntilO STORM_LOG_ASSERT(transformations.size() == origBoundedUntil.getDimension(), "Tried to replace the bound of a dimension that is higher than the number of dimensions of the formula."); std::vector> leftSubformulas, rightSubformulas; - std::vector> lowerBounds, upperBounds; + std::vector> lowerBounds, upperBounds; std::vector timeBoundReferences; for (uint64_t dim = 0; dim < origBoundedUntil.getDimension(); ++dim) { @@ -103,12 +104,12 @@ std::shared_ptr transformBoundedUntilO if (origBoundedUntil.hasLowerBound(dim)) { lowerBounds.push_back(storm::logic::TimeBound(origBoundedUntil.isLowerBoundStrict(dim), origBoundedUntil.getLowerBound(dim))); } else { - lowerBounds.push_back(boost::none); + lowerBounds.push_back(std::nullopt); } if (origBoundedUntil.hasUpperBound(dim)) { upperBounds.push_back(storm::logic::TimeBound(origBoundedUntil.isUpperBoundStrict(dim), origBoundedUntil.getUpperBound(dim))); } else { - upperBounds.push_back(boost::none); + upperBounds.push_back(std::nullopt); } } else { // We need a zero expression in all other cases @@ -121,13 +122,13 @@ std::shared_ptr transformBoundedUntilO zero = origBoundedUntil.getUpperBound(dim).getManager().rational(0.0); } if (transformations[dim] == BoundTransformation::LessEqualZero) { - lowerBounds.push_back(boost::none); + lowerBounds.push_back(std::nullopt); upperBounds.push_back(storm::logic::TimeBound(false, zero)); } else { STORM_LOG_ASSERT(transformations[dim] == BoundTransformation::GreaterZero || transformations[dim] == BoundTransformation::GreaterEqualZero, "Unhandled bound transformation."); lowerBounds.push_back(storm::logic::TimeBound(transformations[dim] == BoundTransformation::GreaterZero, zero)); - upperBounds.push_back(boost::none); + upperBounds.push_back(std::nullopt); } } } From 51f9fd0104b007c4988febe64b79c59cf8d1d6e5 Mon Sep 17 00:00:00 2001 From: Alex Bork Date: Thu, 20 Aug 2026 13:43:40 +0200 Subject: [PATCH 03/11] Add comment about conversion to std::optional --- src/storm-parsers/parser/FormulaParserGrammar.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index 19a4c87314..e0ca119b33 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -474,6 +474,8 @@ std::shared_ptr FormulaParserGrammar::createEventua std::shared_ptr>>> const& timeBounds, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const { if (timeBounds && !timeBounds.get().empty()) { + // Conversion of boost::optional to std::optional + // This can be simplified if the input is changed to already use std::optional std::vector> lowerBounds, upperBounds; std::vector timeBoundReferences; for (auto const& timeBound : timeBounds.get()) { @@ -512,6 +514,8 @@ std::shared_ptr FormulaParserGrammar::createUntilFo std::shared_ptr>>> const& timeBounds, std::shared_ptr const& rightSubformula) { if (timeBounds && !timeBounds.get().empty()) { + // Conversion of boost::optional to std::optional + // This can be simplified if the input is changed to already use std::optional std::vector> lowerBounds, upperBounds; std::vector timeBoundReferences; for (auto const& timeBound : timeBounds.get()) { From 7351f2631dc339f58102c2c10e1d67bf3a54db3f Mon Sep 17 00:00:00 2001 From: Alex Bork Date: Fri, 21 Aug 2026 13:42:41 +0200 Subject: [PATCH 04/11] Adjust get*BoundAsOptionalTimeBound --- src/storm/logic/BoundedUntilFormula.cpp | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp index fb6895ef55..7bddd2c960 100644 --- a/src/storm/logic/BoundedUntilFormula.cpp +++ b/src/storm/logic/BoundedUntilFormula.cpp @@ -252,19 +252,11 @@ storm::expressions::Expression const& BoundedUntilFormula::getUpperBound(unsigne } std::optional BoundedUntilFormula::getLowerBoundAsOptionalTimeBound(unsigned i) const { - if (hasLowerBound(i)) { - return lowerBound.at(i).get(); - } else { - return std::nullopt; - } + return lowerBound.at(i); } std::optional BoundedUntilFormula::getUpperBoundAsOptionalTimeBound(unsigned i) const { - if (hasUpperBound(i)) { - return upperBound.at(i).get(); - } else { - return std::nullopt; - } + return upperBound.at(i); } template<> From 9adb1f140db2445bdee5e70a5e6e7260f15973c9 Mon Sep 17 00:00:00 2001 From: Alex Bork Date: Fri, 21 Aug 2026 19:45:22 +0200 Subject: [PATCH 05/11] Change valuetype transformer to only rational-to-double --- .../SparseModelValueTypeTransformer.h | 23 ------ ...parseRationalModelToDoubleTransformer.cpp} | 70 ++++++++----------- .../SparseRationalModelToDoubleTransformer.h | 18 +++++ 3 files changed, 49 insertions(+), 62 deletions(-) delete mode 100644 src/storm/transformer/SparseModelValueTypeTransformer.h rename src/storm/transformer/{SparseModelValueTypeTransformer.cpp => SparseRationalModelToDoubleTransformer.cpp} (60%) create mode 100644 src/storm/transformer/SparseRationalModelToDoubleTransformer.h diff --git a/src/storm/transformer/SparseModelValueTypeTransformer.h b/src/storm/transformer/SparseModelValueTypeTransformer.h deleted file mode 100644 index f6f02ca7e0..0000000000 --- a/src/storm/transformer/SparseModelValueTypeTransformer.h +++ /dev/null @@ -1,23 +0,0 @@ -#pragma once - -#include - -#include "storm/models/sparse/Model.h" - -namespace storm::transformer { - -template -/** Converts the numeric values of a sparse model while preserving its model-specific metadata. */ -class SparseModelValueTypeTransformer { - public: - explicit SparseModelValueTypeTransformer() = default; - - /** - * Returns a model equivalent to @p inputModel with all probabilities, rates, and rewards converted to OutputValueType. - * - * @pre inputModel is not null. - */ - std::shared_ptr> transformModel(std::shared_ptr> const& inputModel); -}; - -} // namespace storm::transformer diff --git a/src/storm/transformer/SparseModelValueTypeTransformer.cpp b/src/storm/transformer/SparseRationalModelToDoubleTransformer.cpp similarity index 60% rename from src/storm/transformer/SparseModelValueTypeTransformer.cpp rename to src/storm/transformer/SparseRationalModelToDoubleTransformer.cpp index eb4c9ec3eb..6d26a6885c 100644 --- a/src/storm/transformer/SparseModelValueTypeTransformer.cpp +++ b/src/storm/transformer/SparseRationalModelToDoubleTransformer.cpp @@ -1,4 +1,4 @@ -#include "SparseModelValueTypeTransformer.h" +#include "SparseRationalModelToDoubleTransformer.h" #include "storm/exceptions/IllegalArgumentTypeException.h" #include "storm/models/sparse/Ctmc.h" @@ -13,91 +13,89 @@ #include "storm/utility/vector.h" namespace storm::transformer { -template -std::shared_ptr> SparseModelValueTypeTransformer::transformModel( - std::shared_ptr> const& inputModel) { +std::shared_ptr> sparseRationalModelToDouble( + std::shared_ptr> const& inputModel) { STORM_LOG_THROW(inputModel, storm::exceptions::IllegalArgumentTypeException, "Cannot transform a null model."); - storm::storage::sparse::ModelComponents convertedComponents; - convertedComponents.transitionMatrix = inputModel->getTransitionMatrix().template toValueType(); + storm::storage::sparse::ModelComponents convertedComponents; + convertedComponents.transitionMatrix = inputModel->getTransitionMatrix().toValueType(); convertedComponents.choiceLabeling = inputModel->getOptionalChoiceLabeling(); convertedComponents.stateLabeling = inputModel->getStateLabeling(); convertedComponents.stateValuations = inputModel->getOptionalStateValuations(); convertedComponents.choiceOrigins = inputModel->getOptionalChoiceOrigins(); for (auto const& [rewardModelName, rewardModel] : inputModel->getRewardModels()) { // Transform reward models - std::optional> optionalStateRewardVector = std::nullopt; - std::optional> optionalStateActionRewardVector = std::nullopt; - std::optional> optionalTransitionRewardMatrix = std::nullopt; + std::optional> optionalStateRewardVector = std::nullopt; + std::optional> optionalStateActionRewardVector = std::nullopt; + std::optional> optionalTransitionRewardMatrix = std::nullopt; if (rewardModel.hasStateRewards()) { - std::vector resultVector; + std::vector resultVector; resultVector.reserve(rewardModel.getStateRewardVector().size()); for (auto const& oldValue : rewardModel.getStateRewardVector()) { - resultVector.push_back(storm::utility::convertNumber(oldValue)); + resultVector.push_back(storm::utility::convertNumber(oldValue)); } optionalStateRewardVector = resultVector; } if (rewardModel.hasStateActionRewards()) { - std::vector resultVector; + std::vector resultVector; resultVector.reserve(rewardModel.getStateActionRewardVector().size()); for (auto const& oldValue : rewardModel.getStateActionRewardVector()) { - resultVector.push_back(storm::utility::convertNumber(oldValue)); + resultVector.push_back(storm::utility::convertNumber(oldValue)); } optionalStateActionRewardVector = resultVector; } if (rewardModel.hasTransitionRewards()) { - optionalTransitionRewardMatrix = rewardModel.getTransitionRewardMatrix().template toValueType(); + optionalTransitionRewardMatrix = rewardModel.getTransitionRewardMatrix().toValueType(); } convertedComponents.rewardModels.emplace( - rewardModelName, storm::models::sparse::StandardRewardModel( + rewardModelName, storm::models::sparse::StandardRewardModel( std::move(optionalStateRewardVector), std::move(optionalStateActionRewardVector), std::move(optionalTransitionRewardMatrix))); } switch (inputModel->getType()) { case storm::models::ModelType::Dtmc: - return std::make_shared>(storm::models::sparse::Dtmc(convertedComponents)); + return std::make_shared>(storm::models::sparse::Dtmc(convertedComponents)); case storm::models::ModelType::Mdp: - return std::make_shared>(storm::models::sparse::Mdp(convertedComponents)); + return std::make_shared>(storm::models::sparse::Mdp(convertedComponents)); case storm::models::ModelType::Ctmc: { - auto ctmc = inputModel->template as>(); - std::vector resultVector; + auto ctmc = inputModel->as>(); + std::vector resultVector; resultVector.reserve(ctmc->getExitRateVector().size()); for (auto const& oldValue : ctmc->getExitRateVector()) { - resultVector.push_back(storm::utility::convertNumber(oldValue)); + resultVector.push_back(storm::utility::convertNumber(oldValue)); } convertedComponents.exitRates = resultVector; // Markov automata store probabilities in their transition matrix and rates separately in exitRates. convertedComponents.rateTransitions = false; - return std::make_shared>(storm::models::sparse::Ctmc(convertedComponents)); + return std::make_shared>(storm::models::sparse::Ctmc(convertedComponents)); } case storm::models::ModelType::MarkovAutomaton: { - auto ma = inputModel->template as>(); - std::vector resultVector; + auto ma = inputModel->as>(); + std::vector resultVector; resultVector.reserve(ma->getExitRates().size()); for (auto const& oldValue : ma->getExitRates()) { - resultVector.push_back(storm::utility::convertNumber(oldValue)); + resultVector.push_back(storm::utility::convertNumber(oldValue)); } convertedComponents.exitRates = resultVector; convertedComponents.rateTransitions = true; convertedComponents.markovianStates = ma->getMarkovianStates(); - return std::make_shared>( - storm::models::sparse::MarkovAutomaton(convertedComponents)); + return std::make_shared>(storm::models::sparse::MarkovAutomaton(convertedComponents)); } case storm::models::ModelType::Pomdp: { - auto pomdp = inputModel->template as>(); + auto pomdp = inputModel->as>(); convertedComponents.observabilityClasses = pomdp->getObservations(); convertedComponents.observationValuations = pomdp->getOptionalObservationValuations(); - return std::make_shared>(models::sparse::Pomdp(convertedComponents, pomdp->isCanonic())); + return std::make_shared>(models::sparse::Pomdp(convertedComponents, pomdp->isCanonic())); } case storm::models::ModelType::Smg: { - auto smg = inputModel->template as>(); + auto smg = inputModel->as>(); convertedComponents.statePlayerIndications = smg->getStatePlayerIndications(); convertedComponents.playerNameToIndexMap = smg->getPlayerNamesToIndex(); - return std::make_shared>(models::sparse::Smg(convertedComponents)); + return std::make_shared>(models::sparse::Smg(convertedComponents)); } case storm::models::ModelType::S2pg: { - auto s2pg = inputModel->template as>(); + auto s2pg = inputModel->as>(); convertedComponents.player1Matrix = s2pg->getPlayer1Matrix(); - return std::make_shared>( - models::sparse::StochasticTwoPlayerGame(convertedComponents)); + return std::make_shared>( + models::sparse::StochasticTwoPlayerGame(convertedComponents)); } default: STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentTypeException, @@ -105,10 +103,4 @@ std::shared_ptr> SparseModelValueT } return nullptr; } - -template class SparseModelValueTypeTransformer; -template class SparseModelValueTypeTransformer; -template class SparseModelValueTypeTransformer; -template class SparseModelValueTypeTransformer; - } // namespace storm::transformer diff --git a/src/storm/transformer/SparseRationalModelToDoubleTransformer.h b/src/storm/transformer/SparseRationalModelToDoubleTransformer.h new file mode 100644 index 0000000000..9532c349a4 --- /dev/null +++ b/src/storm/transformer/SparseRationalModelToDoubleTransformer.h @@ -0,0 +1,18 @@ +#pragma once + +#include + +#include "storm/adapters/RationalNumberForward.h" +#include "storm/models/sparse/Model.h" + +namespace storm::transformer { + +/** + * Returns a model equivalent to @p inputModel with all probabilities, rates, and rewards converted to double. + * + * @pre inputModel is not null. + */ +std::shared_ptr> sparseRationalModelToDouble( + std::shared_ptr> const& inputModel); + +} // namespace storm::transformer From f31dd956a896805fb07a7ab92cb53870b773538d Mon Sep 17 00:00:00 2001 From: Alex Bork Date: Mon, 24 Aug 2026 18:05:12 +0200 Subject: [PATCH 06/11] Add potential normalisation --- .../SparseRationalModelToDoubleTransformer.cpp | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/src/storm/transformer/SparseRationalModelToDoubleTransformer.cpp b/src/storm/transformer/SparseRationalModelToDoubleTransformer.cpp index 6d26a6885c..d0728bf331 100644 --- a/src/storm/transformer/SparseRationalModelToDoubleTransformer.cpp +++ b/src/storm/transformer/SparseRationalModelToDoubleTransformer.cpp @@ -8,6 +8,8 @@ #include "storm/models/sparse/Pomdp.h" #include "storm/models/sparse/Smg.h" #include "storm/models/sparse/StochasticTwoPlayerGame.h" +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/GeneralSettings.h" #include "storm/storage/sparse/ModelComponents.h" #include "storm/utility/macros.h" #include "storm/utility/vector.h" @@ -18,6 +20,12 @@ std::shared_ptr> sparseRationalModelToDoubl STORM_LOG_THROW(inputModel, storm::exceptions::IllegalArgumentTypeException, "Cannot transform a null model."); storm::storage::sparse::ModelComponents convertedComponents; convertedComponents.transitionMatrix = inputModel->getTransitionMatrix().toValueType(); + if (inputModel->getType() != storm::models::ModelType::Ctmc) { + if (auto const precision = storm::settings::getModule().getPrecision(); + !convertedComponents.transitionMatrix.isProbabilistic(precision)) { + convertedComponents.transitionMatrix.divideRowsInPlace(convertedComponents.transitionMatrix.getRowSumVector()); + } + } convertedComponents.choiceLabeling = inputModel->getOptionalChoiceLabeling(); convertedComponents.stateLabeling = inputModel->getStateLabeling(); convertedComponents.stateValuations = inputModel->getOptionalStateValuations(); @@ -63,8 +71,7 @@ std::shared_ptr> sparseRationalModelToDoubl resultVector.push_back(storm::utility::convertNumber(oldValue)); } convertedComponents.exitRates = resultVector; - // Markov automata store probabilities in their transition matrix and rates separately in exitRates. - convertedComponents.rateTransitions = false; + convertedComponents.rateTransitions = true; return std::make_shared>(storm::models::sparse::Ctmc(convertedComponents)); } case storm::models::ModelType::MarkovAutomaton: { @@ -75,7 +82,8 @@ std::shared_ptr> sparseRationalModelToDoubl resultVector.push_back(storm::utility::convertNumber(oldValue)); } convertedComponents.exitRates = resultVector; - convertedComponents.rateTransitions = true; + // Markov automata store probabilities in their transition matrix and rates separately in exitRates. + convertedComponents.rateTransitions = false; convertedComponents.markovianStates = ma->getMarkovianStates(); return std::make_shared>(storm::models::sparse::MarkovAutomaton(convertedComponents)); } From d3d2ce46ad0da21d73d8c53464ae8f2db427e07f Mon Sep 17 00:00:00 2001 From: Alex Bork Date: Tue, 25 Aug 2026 14:56:14 +0200 Subject: [PATCH 07/11] Change precision to be an input parameter --- .../transformer/SparseRationalModelToDoubleTransformer.cpp | 7 ++----- .../transformer/SparseRationalModelToDoubleTransformer.h | 3 ++- 2 files changed, 4 insertions(+), 6 deletions(-) diff --git a/src/storm/transformer/SparseRationalModelToDoubleTransformer.cpp b/src/storm/transformer/SparseRationalModelToDoubleTransformer.cpp index d0728bf331..296e2e62d8 100644 --- a/src/storm/transformer/SparseRationalModelToDoubleTransformer.cpp +++ b/src/storm/transformer/SparseRationalModelToDoubleTransformer.cpp @@ -8,21 +8,18 @@ #include "storm/models/sparse/Pomdp.h" #include "storm/models/sparse/Smg.h" #include "storm/models/sparse/StochasticTwoPlayerGame.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/GeneralSettings.h" #include "storm/storage/sparse/ModelComponents.h" #include "storm/utility/macros.h" #include "storm/utility/vector.h" namespace storm::transformer { std::shared_ptr> sparseRationalModelToDouble( - std::shared_ptr> const& inputModel) { + std::shared_ptr> const& inputModel, double precision) { STORM_LOG_THROW(inputModel, storm::exceptions::IllegalArgumentTypeException, "Cannot transform a null model."); storm::storage::sparse::ModelComponents convertedComponents; convertedComponents.transitionMatrix = inputModel->getTransitionMatrix().toValueType(); if (inputModel->getType() != storm::models::ModelType::Ctmc) { - if (auto const precision = storm::settings::getModule().getPrecision(); - !convertedComponents.transitionMatrix.isProbabilistic(precision)) { + if (!convertedComponents.transitionMatrix.isProbabilistic(precision)) { convertedComponents.transitionMatrix.divideRowsInPlace(convertedComponents.transitionMatrix.getRowSumVector()); } } diff --git a/src/storm/transformer/SparseRationalModelToDoubleTransformer.h b/src/storm/transformer/SparseRationalModelToDoubleTransformer.h index 9532c349a4..06ff990651 100644 --- a/src/storm/transformer/SparseRationalModelToDoubleTransformer.h +++ b/src/storm/transformer/SparseRationalModelToDoubleTransformer.h @@ -10,9 +10,10 @@ namespace storm::transformer { /** * Returns a model equivalent to @p inputModel with all probabilities, rates, and rewards converted to double. * + * @param precision The tolerance used to determine whether the converted transition matrix needs to be normalized. Ignored for CTMCs. * @pre inputModel is not null. */ std::shared_ptr> sparseRationalModelToDouble( - std::shared_ptr> const& inputModel); + std::shared_ptr> const& inputModel, double precision); } // namespace storm::transformer From aac224e45ff4ed066f5da606c380d10868aea7ef Mon Sep 17 00:00:00 2001 From: Alex Bork Date: Tue, 25 Aug 2026 15:12:35 +0200 Subject: [PATCH 08/11] Add tests --- ...seRationalModelToDoubleTransformerTest.cpp | 87 +++++++++++++++ ...ransitionToActionRewardTransformerTest.cpp | 101 ++++++++++++++++++ 2 files changed, 188 insertions(+) create mode 100644 src/test/storm/transformer/SparseRationalModelToDoubleTransformerTest.cpp create mode 100644 src/test/storm/transformer/TransitionToActionRewardTransformerTest.cpp diff --git a/src/test/storm/transformer/SparseRationalModelToDoubleTransformerTest.cpp b/src/test/storm/transformer/SparseRationalModelToDoubleTransformerTest.cpp new file mode 100644 index 0000000000..c6b1433c80 --- /dev/null +++ b/src/test/storm/transformer/SparseRationalModelToDoubleTransformerTest.cpp @@ -0,0 +1,87 @@ +#include "test/storm_gtest.h" + +#include "storm/adapters/RationalNumberAdapter.h" +#include "storm/models/sparse/Ctmc.h" +#include "storm/models/sparse/Dtmc.h" +#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/storage/SparseMatrix.h" +#include "storm/transformer/SparseRationalModelToDoubleTransformer.h" + +namespace { + +constexpr double normalizationPrecision = 1e-17; +constexpr double standardPrecision = 1e-9; + +storm::storage::SparseMatrix buildProbabilityMatrix() { + storm::storage::SparseMatrixBuilder builder(3, 3, 5); + builder.addNextValue(0, 0, storm::RationalNumber("1/5")); + builder.addNextValue(0, 1, storm::RationalNumber("3/5")); + builder.addNextValue(0, 2, storm::RationalNumber("1/5")); + builder.addNextValue(1, 1, storm::RationalNumber(1)); + builder.addNextValue(2, 2, storm::RationalNumber(1)); + return builder.build(); +} + +TEST(SparseRationalModelToDoubleTransformerTest, NormalizesDtmcOutsideConfiguredPrecision) { + auto const matrix = buildProbabilityMatrix(); + + auto const inputModel = std::make_shared>(std::move(matrix), storm::models::sparse::StateLabeling(3)); + auto const result = storm::transformer::sparseRationalModelToDouble(inputModel, normalizationPrecision)->as>(); + + EXPECT_TRUE(result->getTransitionMatrix().isProbabilistic(normalizationPrecision)); + EXPECT_DOUBLE_EQ(1.0, result->getTransitionMatrix().getRowSum(0)); +} + +TEST(SparseRationalModelToDoubleTransformerTest, PreservesDtmcWithinConfiguredPrecision) { + auto matrix = buildProbabilityMatrix(); + auto convertedMatrix = matrix.toValueType(); + ASSERT_TRUE(convertedMatrix.isProbabilistic(standardPrecision)); + ASSERT_NE(1.0, convertedMatrix.getRowSum(0)); + + auto inputModel = std::make_shared>(std::move(matrix), storm::models::sparse::StateLabeling(3)); + auto result = storm::transformer::sparseRationalModelToDouble(inputModel, standardPrecision)->as>(); + + EXPECT_EQ(convertedMatrix, result->getTransitionMatrix()); +} + +TEST(SparseRationalModelToDoubleTransformerTest, PreservesCtmcRates) { + storm::storage::SparseMatrixBuilder builder(2, 2, 4); + builder.addNextValue(0, 0, storm::RationalNumber(2)); + builder.addNextValue(0, 1, storm::RationalNumber(1)); + builder.addNextValue(1, 0, storm::RationalNumber(1)); + builder.addNextValue(1, 1, storm::RationalNumber(3)); + auto matrix = builder.build(); + auto convertedMatrix = matrix.toValueType(); + + auto inputModel = std::make_shared>(std::move(matrix), storm::models::sparse::StateLabeling(2)); + auto result = storm::transformer::sparseRationalModelToDouble(inputModel, standardPrecision)->as>(); + + EXPECT_EQ(convertedMatrix, result->getTransitionMatrix()); + EXPECT_EQ((std::vector{3.0, 4.0}), result->getExitRateVector()); +} + +TEST(SparseRationalModelToDoubleTransformerTest, NormalizesMarkovAutomatonProbabilities) { + storm::storage::SparseMatrixBuilder builder(3, 3, 5, true, true, 3); + builder.newRowGroup(0); + builder.addNextValue(0, 0, storm::RationalNumber(1)); + builder.addNextValue(0, 1, storm::RationalNumber(3)); + builder.addNextValue(0, 2, storm::RationalNumber(1)); + builder.newRowGroup(1); + builder.addNextValue(1, 1, storm::RationalNumber(1)); + builder.newRowGroup(2); + builder.addNextValue(2, 2, storm::RationalNumber(1)); + storm::storage::BitVector markovianStates(3, false); + markovianStates.set(0); + + auto inputModel = std::make_shared>(builder.build(), storm::models::sparse::StateLabeling(3), + std::move(markovianStates)); + ASSERT_FALSE(inputModel->getTransitionMatrix().toValueType().isProbabilistic(normalizationPrecision)); + auto result = storm::transformer::sparseRationalModelToDouble(inputModel, normalizationPrecision)->as>(); + + EXPECT_TRUE(result->getTransitionMatrix().isProbabilistic(normalizationPrecision)); + EXPECT_DOUBLE_EQ(1.0, result->getTransitionMatrix().getRowSum(0)); + EXPECT_EQ(inputModel->getMarkovianStates(), result->getMarkovianStates()); + EXPECT_EQ((std::vector{5.0, 0.0, 0.0}), result->getExitRates()); +} + +} // namespace diff --git a/src/test/storm/transformer/TransitionToActionRewardTransformerTest.cpp b/src/test/storm/transformer/TransitionToActionRewardTransformerTest.cpp new file mode 100644 index 0000000000..f2cf350c3f --- /dev/null +++ b/src/test/storm/transformer/TransitionToActionRewardTransformerTest.cpp @@ -0,0 +1,101 @@ +#include "storm-config.h" +#include "test/storm_gtest.h" + +#include "storm-parsers/api/storm-parsers.h" +#include "storm-parsers/parser/AutoParser.h" +#include "storm-parsers/parser/DeterministicModelParser.h" +#include "storm-parsers/parser/MarkovAutomatonParser.h" +#include "storm/api/storm.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm/models/sparse/Ctmc.h" +#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/transformer/TransitionToActionRewardTransformer.h" + +namespace { +double computeInitialReward(std::shared_ptr> const& model, std::string const& formulaString) { + auto const formula = storm::api::extractFormulasFromProperties(storm::api::parseProperties(formulaString)).front(); + auto const result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(formula, true)); + return result->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()]; +} + +TEST(TransitionToActionRewardTransformerTest, DtmcDie) { + auto const model = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/dtmc/die.tra", STORM_TEST_RESOURCES_DIR "/dtmc/die.lab", "", + STORM_TEST_RESOURCES_DIR "/rew/die.coin_flips.trans.rew"); + + auto const transformed = storm::transformer::transformTransitionToActionRewards(model, {""}); + + EXPECT_EQ(25ull, transformed.model->getNumberOfStates()); + EXPECT_EQ(32ull, transformed.model->getNumberOfTransitions()); + EXPECT_EQ((std::vector{0, 2, 4, 6, 8, 10, 12, 14, 16, 18, 20, 22, 24}), transformed.originalToNewStateIndices); + EXPECT_TRUE(transformed.model->getRewardModel("").hasStateActionRewards()); + EXPECT_FALSE(transformed.model->getRewardModel("").hasTransitionRewards()); + + EXPECT_NEAR(11.0 / 3.0, computeInitialReward(transformed.model, "R=? [F \"done\"]"), 1e-6); +} + +TEST(TransitionToActionRewardTransformerTest, CtmcDie) { + auto const model = std::make_shared>(storm::parser::DeterministicModelParser<>::parseCtmc( + STORM_TEST_RESOURCES_DIR "/tra/die.tra", STORM_TEST_RESOURCES_DIR "/lab/die.lab", "", STORM_TEST_RESOURCES_DIR "/rew/die.coin_flips.trans.rew")); + + auto const transformed = storm::transformer::transformTransitionToActionRewards(model, {""}); + + EXPECT_EQ(storm::models::ModelType::Ctmc, transformed.model->getType()); + EXPECT_EQ(25ull, transformed.model->getNumberOfStates()); + EXPECT_EQ(32ull, transformed.model->getNumberOfTransitions()); + EXPECT_TRUE(transformed.model->getRewardModel("").hasStateActionRewards()); + EXPECT_FALSE(transformed.model->getRewardModel("").hasTransitionRewards()); + + EXPECT_NEAR(11.0 / 3.0, computeInitialReward(transformed.model, "R=? [F \"done\"]"), 1e-6); +} + +TEST(TransitionToActionRewardTransformerTest, MdpTwoDice) { + auto const model = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", "", + STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew"); + + auto const transformed = storm::transformer::transformTransitionToActionRewards(model, {""}); + + EXPECT_EQ(storm::models::ModelType::Mdp, transformed.model->getType()); + EXPECT_EQ(337ull, transformed.model->getNumberOfStates()); + EXPECT_EQ(604ull, transformed.model->getNumberOfTransitions()); + ASSERT_EQ(169ull, transformed.originalToNewStateIndices.size()); + for (uint64_t state = 0; state < transformed.originalToNewStateIndices.size(); ++state) { + EXPECT_EQ(2 * state, transformed.originalToNewStateIndices[state]); + } + EXPECT_TRUE(transformed.model->getRewardModel("").hasStateActionRewards()); + EXPECT_FALSE(transformed.model->getRewardModel("").hasTransitionRewards()); + + EXPECT_NEAR(22.0 / 3.0, computeInitialReward(transformed.model, "Rmin=? [F \"done\"]"), 1e-6); +} + +TEST(TransitionToActionRewardTransformerTest, MarkovAutomatonGeneral) { + auto const model = std::make_shared>(storm::parser::MarkovAutomatonParser<>::parseMarkovAutomaton( + STORM_TEST_RESOURCES_DIR "/tra/ma_general.tra", STORM_TEST_RESOURCES_DIR "/lab/ma_general.lab", STORM_TEST_RESOURCES_DIR "/rew/ma_general.state.rew")); + auto transitionRewards = model->getTransitionMatrix(); + for (auto& entry : transitionRewards) { + entry.setValue(1.0); + } + auto const stateRewards = model->getRewardModel("").getOptionalStateRewardVector(); + model->getRewardModel("") = storm::models::sparse::StandardRewardModel(std::move(stateRewards), std::nullopt, std::move(transitionRewards)); + + auto const transformed = storm::transformer::transformTransitionToActionRewards(model, {""}); + + EXPECT_EQ(storm::models::ModelType::MarkovAutomaton, transformed.model->getType()); + EXPECT_EQ(12ull, transformed.model->getNumberOfStates()); + EXPECT_EQ(18ull, transformed.model->getNumberOfTransitions()); + EXPECT_EQ((std::vector{1, 3, 5, 7, 9, 11}), transformed.originalToNewStateIndices); + EXPECT_TRUE(transformed.model->getRewardModel("").hasStateActionRewards()); + EXPECT_FALSE(transformed.model->getRewardModel("").hasTransitionRewards()); + + auto transformedMa = transformed.model->as>(); + EXPECT_EQ(2ull, transformedMa->getMarkovianStates().getNumberOfSetBits()); + EXPECT_TRUE(transformedMa->isMarkovianState(1)); + EXPECT_EQ(2.0, transformedMa->getExitRate(1)); + EXPECT_TRUE(transformedMa->isMarkovianState(5)); + EXPECT_EQ(15.0, transformedMa->getExitRate(5)); + for (uint64_t state = 0; state < transformedMa->getNumberOfStates(); state += 2) { + EXPECT_TRUE(transformedMa->isProbabilisticState(state)); + } +} + +} // namespace From 83474948eea0eef8a06aed3513cf6c1448f58d78 Mon Sep 17 00:00:00 2001 From: Alex Bork Date: Tue, 25 Aug 2026 21:34:57 +0200 Subject: [PATCH 09/11] Remove normalisation test --- ...seRationalModelToDoubleTransformerTest.cpp | 37 ------------------- 1 file changed, 37 deletions(-) diff --git a/src/test/storm/transformer/SparseRationalModelToDoubleTransformerTest.cpp b/src/test/storm/transformer/SparseRationalModelToDoubleTransformerTest.cpp index c6b1433c80..2b19a6fa38 100644 --- a/src/test/storm/transformer/SparseRationalModelToDoubleTransformerTest.cpp +++ b/src/test/storm/transformer/SparseRationalModelToDoubleTransformerTest.cpp @@ -9,7 +9,6 @@ namespace { -constexpr double normalizationPrecision = 1e-17; constexpr double standardPrecision = 1e-9; storm::storage::SparseMatrix buildProbabilityMatrix() { @@ -22,21 +21,9 @@ storm::storage::SparseMatrix buildProbabilityMatrix() { return builder.build(); } -TEST(SparseRationalModelToDoubleTransformerTest, NormalizesDtmcOutsideConfiguredPrecision) { - auto const matrix = buildProbabilityMatrix(); - - auto const inputModel = std::make_shared>(std::move(matrix), storm::models::sparse::StateLabeling(3)); - auto const result = storm::transformer::sparseRationalModelToDouble(inputModel, normalizationPrecision)->as>(); - - EXPECT_TRUE(result->getTransitionMatrix().isProbabilistic(normalizationPrecision)); - EXPECT_DOUBLE_EQ(1.0, result->getTransitionMatrix().getRowSum(0)); -} - TEST(SparseRationalModelToDoubleTransformerTest, PreservesDtmcWithinConfiguredPrecision) { auto matrix = buildProbabilityMatrix(); auto convertedMatrix = matrix.toValueType(); - ASSERT_TRUE(convertedMatrix.isProbabilistic(standardPrecision)); - ASSERT_NE(1.0, convertedMatrix.getRowSum(0)); auto inputModel = std::make_shared>(std::move(matrix), storm::models::sparse::StateLabeling(3)); auto result = storm::transformer::sparseRationalModelToDouble(inputModel, standardPrecision)->as>(); @@ -60,28 +47,4 @@ TEST(SparseRationalModelToDoubleTransformerTest, PreservesCtmcRates) { EXPECT_EQ((std::vector{3.0, 4.0}), result->getExitRateVector()); } -TEST(SparseRationalModelToDoubleTransformerTest, NormalizesMarkovAutomatonProbabilities) { - storm::storage::SparseMatrixBuilder builder(3, 3, 5, true, true, 3); - builder.newRowGroup(0); - builder.addNextValue(0, 0, storm::RationalNumber(1)); - builder.addNextValue(0, 1, storm::RationalNumber(3)); - builder.addNextValue(0, 2, storm::RationalNumber(1)); - builder.newRowGroup(1); - builder.addNextValue(1, 1, storm::RationalNumber(1)); - builder.newRowGroup(2); - builder.addNextValue(2, 2, storm::RationalNumber(1)); - storm::storage::BitVector markovianStates(3, false); - markovianStates.set(0); - - auto inputModel = std::make_shared>(builder.build(), storm::models::sparse::StateLabeling(3), - std::move(markovianStates)); - ASSERT_FALSE(inputModel->getTransitionMatrix().toValueType().isProbabilistic(normalizationPrecision)); - auto result = storm::transformer::sparseRationalModelToDouble(inputModel, normalizationPrecision)->as>(); - - EXPECT_TRUE(result->getTransitionMatrix().isProbabilistic(normalizationPrecision)); - EXPECT_DOUBLE_EQ(1.0, result->getTransitionMatrix().getRowSum(0)); - EXPECT_EQ(inputModel->getMarkovianStates(), result->getMarkovianStates()); - EXPECT_EQ((std::vector{5.0, 0.0, 0.0}), result->getExitRates()); -} - } // namespace From c5ea70e220bcb896da82b6e6f9aa0d19639060cd Mon Sep 17 00:00:00 2001 From: Alex Bork Date: Wed, 26 Aug 2026 16:31:52 +0200 Subject: [PATCH 10/11] Add interval instantiations --- .../TransitionToActionRewardTransformer.cpp | 91 ++++++++++++------- .../TransitionToActionRewardTransformer.h | 12 ++- 2 files changed, 67 insertions(+), 36 deletions(-) diff --git a/src/storm/transformer/TransitionToActionRewardTransformer.cpp b/src/storm/transformer/TransitionToActionRewardTransformer.cpp index eb84521130..e8047e0bef 100644 --- a/src/storm/transformer/TransitionToActionRewardTransformer.cpp +++ b/src/storm/transformer/TransitionToActionRewardTransformer.cpp @@ -1,5 +1,6 @@ #include "storm/transformer/TransitionToActionRewardTransformer.h" +#include "storm/adapters/IntervalAdapter.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/adapters/RationalNumberAdapter.h" #include "storm/exceptions/UnexpectedException.h" @@ -15,15 +16,15 @@ namespace storm::transformer { namespace detail { -template -using MultiRewardVector = std::vector; +template +using MultiRewardVector = std::vector; -template +template> class RewardTransitionIterator { public: RewardTransitionIterator(storm::storage::SparseMatrix const& m) : transitionMatrix(m) {} - void addRewardModel(storm::models::sparse::StandardRewardModel const& rewardModel) { + void addRewardModel(RewardModelType const& rewardModel) { if (rewardModel.hasTransitionRewards()) { transitionRewards.emplace_back(rewardModel.getTransitionRewardMatrix()); STORM_LOG_ASSERT(transitionRewards.back()->isSubmatrixOf(transitionMatrix), "Invalid reward matrix."); @@ -35,8 +36,8 @@ class RewardTransitionIterator { template void forEachRowEntry(uint64_t rowIndex, bool skip0RewardEntries, CallBackType&& callBack) { // Set-up iterators - std::vector::const_iterator> rewardIterators; - std::vector::const_iterator> rewardIteratorsEnd; + std::vector::const_iterator> rewardIterators; + std::vector::const_iterator> rewardIteratorsEnd; for (auto const& rewardMatrix : transitionRewards) { if (rewardMatrix) { rewardIterators.push_back(rewardMatrix->begin(rowIndex)); @@ -47,7 +48,7 @@ class RewardTransitionIterator { } } - std::vector rewards(transitionRewards.size()); + std::vector rewards(transitionRewards.size()); for (auto const& entry : transitionMatrix.getRow(rowIndex)) { // Fill in rewards for this entry bool skipEntry = skip0RewardEntries; @@ -57,7 +58,7 @@ class RewardTransitionIterator { ++rewardIterators[i]; skipEntry = skipEntry && storm::utility::isZero(rewards[i]); } else { - rewards[i] = storm::utility::zero(); + rewards[i] = storm::utility::zero(); } } if (!skipEntry) { @@ -68,16 +69,17 @@ class RewardTransitionIterator { private: storm::storage::SparseMatrix const& transitionMatrix; - std::vector const>> transitionRewards; + std::vector const>> transitionRewards; }; } // namespace detail -template -TransitionToActionRewardTransformerReturnType transformTransitionToActionRewards( - std::shared_ptr> originalModel, std::vector const& relevantRewardModelNames) { +template +TransitionToActionRewardTransformerReturnType transformTransitionToActionRewards( + std::shared_ptr> originalModel, std::vector const& relevantRewardModelNames) { + using RewardValueType = RewardModelType::ValueType; STORM_LOG_ASSERT(originalModel, "Model must not be null."); - detail::RewardTransitionIterator rewardTransitionIterator(originalModel->getTransitionMatrix()); + detail::RewardTransitionIterator rewardTransitionIterator(originalModel->getTransitionMatrix()); bool hasTransitionRewards = false; for (auto const& rewardModelName : relevantRewardModelNames) { auto const& rewardModel = originalModel->getRewardModel(rewardModelName); @@ -87,24 +89,27 @@ TransitionToActionRewardTransformerReturnType transformTransitionToAc rewardTransitionIterator.addRewardModel(rewardModel); } if (!hasTransitionRewards) { - return {originalModel->template as>(), + return {originalModel->template as>(), {storm::utility::vector::buildVectorForRange(0, originalModel->getNumberOfStates())}}; } - // Make a pass to find the different rewards with which a state is entered - std::vector>> incomingRewards(originalModel->getNumberOfStates()); + // Make a pass to find the different unique rewards with which a state is entered. + // We do not use std::set here as the interval ordering is not a strict weak ordering for overlapping intervals. + // Equality-based deduplication preserves distinct overlapping rewards. + std::vector>> incomingRewards(originalModel->getNumberOfStates()); auto const& transitions = originalModel->getTransitionMatrix(); for (uint64_t row = 0; row < transitions.getRowCount(); ++row) { rewardTransitionIterator.forEachRowEntry( - row, true, - [&incomingRewards](uint64_t column, ValueType, detail::MultiRewardVector const& rewards) { incomingRewards[column].insert(rewards); }); + row, true, [&incomingRewards](uint64_t column, RewardValueType, detail::MultiRewardVector const& rewards) { + storm::utility::vector::findOrInsert(incomingRewards[column], detail::MultiRewardVector(rewards)); + }); } // Create a mapping from original to new indices std::vector originalToNewIndex; uint64_t numStates = 0; - for (auto const& incRewardsSet : incomingRewards) { - numStates += incRewardsSet.size(); + for (auto const& incomingRewardVectors : incomingRewards) { + numStates += incomingRewardVectors.size(); originalToNewIndex.push_back(numStates); ++numStates; } @@ -115,19 +120,19 @@ TransitionToActionRewardTransformerReturnType transformTransitionToAc storm::storage::SparseMatrixBuilder newTransitionsBuilder(transitions.getRowCount() + numIntermediateStates, numStates, transitions.getEntryCount() + numIntermediateStates, true, useGroups, useGroups ? numStates : 0ull); - std::vector> newActionRewards(relevantRewardModelNames.size(), - std::vector(transitions.getRowCount() + numIntermediateStates)); + std::vector> newActionRewards(relevantRewardModelNames.size(), + std::vector(transitions.getRowCount() + numIntermediateStates)); uint64_t currNewRow = 0; for (uint64_t currOrigState = 0; currOrigState < originalModel->getNumberOfStates(); ++currOrigState) { uint64_t const currNewState = originalToNewIndex[currOrigState]; // First add the transitions and rewards for the intermediate states - for (auto const& incRewardsSet : incomingRewards[currOrigState]) { + for (auto const& incomingRewardVector : incomingRewards[currOrigState]) { if (useGroups) { newTransitionsBuilder.newRowGroup(currNewRow); } newTransitionsBuilder.addNextValue(currNewRow, currNewState, storm::utility::one()); auto newRewIt = newActionRewards.begin(); - for (auto const& rew : incRewardsSet) { + for (auto const& rew : incomingRewardVector) { (*newRewIt)[currNewRow] = rew; ++newRewIt; } @@ -141,13 +146,13 @@ TransitionToActionRewardTransformerReturnType transformTransitionToAc rewardTransitionIterator.forEachRowEntry( origRowIndex, false, [&newTransitionsBuilder, &originalToNewIndex, &incomingRewards, &currNewRow](uint64_t column, ValueType prob, - detail::MultiRewardVector const& rewards) { - if (std::all_of(rewards.begin(), rewards.end(), [](ValueType const& r) { return storm::utility::isZero(r); })) { - // No transition reward collected so use originial state + detail::MultiRewardVector const& rewards) { + if (std::all_of(rewards.begin(), rewards.end(), [](RewardValueType const& r) { return storm::utility::isZero(r); })) { + // No transition reward collected so use original state newTransitionsBuilder.addNextValue(currNewRow, originalToNewIndex[column], prob); } else { // Redirect to intermediate state - auto incomingRewardsIt = incomingRewards[column].find(rewards); + auto incomingRewardsIt = std::find(incomingRewards[column].begin(), incomingRewards[column].end(), rewards); STORM_LOG_ASSERT(incomingRewardsIt != incomingRewards[column].end(), "Invalid incoming rewards."); uint64_t const intermediateStateIndex = originalToNewIndex[column] - incomingRewards[column].size() + std::distance(incomingRewards[column].begin(), incomingRewardsIt); @@ -166,7 +171,7 @@ TransitionToActionRewardTransformerReturnType transformTransitionToAc newLabeling.addLabelToState(l, originalToNewIndex[origIndex]); } } - storm::storage::sparse::ModelComponents components(newTransitionsBuilder.build(), std::move(newLabeling)); + storm::storage::sparse::ModelComponents components(newTransitionsBuilder.build(), std::move(newLabeling)); // create new reward models uint64_t rewardIndex = 0; @@ -188,7 +193,7 @@ TransitionToActionRewardTransformerReturnType transformTransitionToAc } } } - storm::models::sparse::StandardRewardModel newRewardModel(std::nullopt, std::move(newActionRewardVector)); + RewardModelType newRewardModel(std::nullopt, std::move(newActionRewardVector)); components.rewardModels.emplace(rewardModelName, std::move(newRewardModel)); } @@ -221,12 +226,32 @@ TransitionToActionRewardTransformerReturnType transformTransitionToAc template struct TransitionToActionRewardTransformerReturnType; template struct TransitionToActionRewardTransformerReturnType; template struct TransitionToActionRewardTransformerReturnType; +template struct TransitionToActionRewardTransformerReturnType; +template struct TransitionToActionRewardTransformerReturnType; +template struct TransitionToActionRewardTransformerReturnType>; +template struct TransitionToActionRewardTransformerReturnType>; -template TransitionToActionRewardTransformerReturnType transformTransitionToActionRewards( +template TransitionToActionRewardTransformerReturnType transformTransitionToActionRewards>( std::shared_ptr> originalModel, std::vector const& relevantRewardModelNames); -template TransitionToActionRewardTransformerReturnType transformTransitionToActionRewards( +template TransitionToActionRewardTransformerReturnType +transformTransitionToActionRewards>( std::shared_ptr> originalModel, std::vector const& relevantRewardModelNames); -template TransitionToActionRewardTransformerReturnType transformTransitionToActionRewards( +template TransitionToActionRewardTransformerReturnType +transformTransitionToActionRewards>( std::shared_ptr> originalModel, std::vector const& relevantRewardModelNames); +template TransitionToActionRewardTransformerReturnType +transformTransitionToActionRewards>( + std::shared_ptr> originalModel, std::vector const& relevantRewardModelNames); +template TransitionToActionRewardTransformerReturnType +transformTransitionToActionRewards>( + std::shared_ptr> originalModel, std::vector const& relevantRewardModelNames); +template TransitionToActionRewardTransformerReturnType> +transformTransitionToActionRewards>( + std::shared_ptr>> originalModel, + std::vector const& relevantRewardModelNames); +template TransitionToActionRewardTransformerReturnType> +transformTransitionToActionRewards>( + std::shared_ptr>> originalModel, + std::vector const& relevantRewardModelNames); } // namespace storm::transformer diff --git a/src/storm/transformer/TransitionToActionRewardTransformer.h b/src/storm/transformer/TransitionToActionRewardTransformer.h index 3af168f198..e180e68b22 100644 --- a/src/storm/transformer/TransitionToActionRewardTransformer.h +++ b/src/storm/transformer/TransitionToActionRewardTransformer.h @@ -9,9 +9,9 @@ namespace storm::transformer { -template +template> struct TransitionToActionRewardTransformerReturnType { - std::shared_ptr> model; + std::shared_ptr> model; std::vector originalToNewStateIndices; }; /*! @@ -35,8 +35,14 @@ struct TransitionToActionRewardTransformerReturnType { * @param relevantRewardModelNames The names of the reward models that should be transformed. Error if the model does not contain a reward model with this name. * @return The transformed model and the positions of the original model states in the new (larger) transformed model. */ +template +TransitionToActionRewardTransformerReturnType transformTransitionToActionRewards( + std::shared_ptr> originalModel, std::vector const& relevantRewardModelNames); + template TransitionToActionRewardTransformerReturnType transformTransitionToActionRewards( - std::shared_ptr> originalModel, std::vector const& relevantRewardModelNames); + std::shared_ptr> originalModel, std::vector const& relevantRewardModelNames) { + return transformTransitionToActionRewards>(originalModel, relevantRewardModelNames); +} } // namespace storm::transformer From 8a42f9d6fb1191f6e313fe89c1dddffaab7a2e41 Mon Sep 17 00:00:00 2001 From: Alex Bork Date: Wed, 26 Aug 2026 16:53:18 +0200 Subject: [PATCH 11/11] Add test cases for intervals --- ...ransitionToActionRewardTransformerTest.cpp | 105 ++++++++++++++++++ 1 file changed, 105 insertions(+) diff --git a/src/test/storm/transformer/TransitionToActionRewardTransformerTest.cpp b/src/test/storm/transformer/TransitionToActionRewardTransformerTest.cpp index f2cf350c3f..bd0ac9eaa6 100644 --- a/src/test/storm/transformer/TransitionToActionRewardTransformerTest.cpp +++ b/src/test/storm/transformer/TransitionToActionRewardTransformerTest.cpp @@ -1,18 +1,80 @@ #include "storm-config.h" #include "test/storm_gtest.h" +#include + #include "storm-parsers/api/storm-parsers.h" #include "storm-parsers/parser/AutoParser.h" #include "storm-parsers/parser/DeterministicModelParser.h" #include "storm-parsers/parser/MarkovAutomatonParser.h" +#include "storm/adapters/IntervalAdapter.h" +#include "storm/adapters/RationalNumberAdapter.h" #include "storm/api/storm.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/models/sparse/Ctmc.h" +#include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" +#include "storm/storage/SparseMatrix.h" +#include "storm/storage/sparse/ModelComponents.h" #include "storm/transformer/TransitionToActionRewardTransformer.h" +#include "storm/utility/constants.h" namespace { +template +std::shared_ptr>> buildDtmcWithTransitionRewards( + RewardValueType const& firstReward, RewardValueType const& secondReward) { + storm::storage::SparseMatrixBuilder transitionBuilder(3, 3, 3); + transitionBuilder.addNextValue(0, 2, storm::utility::one()); + transitionBuilder.addNextValue(1, 2, storm::utility::one()); + transitionBuilder.addNextValue(2, 2, storm::utility::one()); + + storm::storage::SparseMatrixBuilder rewardBuilder(3, 3, 2); + rewardBuilder.addNextValue(0, 2, firstReward); + rewardBuilder.addNextValue(1, 2, secondReward); + + storm::models::sparse::StateLabeling labeling(3); + labeling.addLabel("init"); + labeling.addLabelToState("init", 0); + storm::storage::sparse::ModelComponents> components( + transitionBuilder.build(), std::move(labeling)); + std::optional> transitionRewards(rewardBuilder.build()); + components.rewardModels.emplace("rew", + storm::models::sparse::StandardRewardModel(std::nullopt, std::nullopt, std::move(transitionRewards))); + return std::make_shared>>( + std::move(components)); +} + +template +void checkTransformedDtmc(storm::transformer::TransitionToActionRewardTransformerReturnType< + TransitionValueType, storm::models::sparse::StandardRewardModel> const& transformed, + RewardValueType const& firstReward, RewardValueType const& secondReward) { + ASSERT_EQ(5ull, transformed.model->getNumberOfStates()); + EXPECT_EQ((std::vector{0, 1, 4}), transformed.originalToNewStateIndices); + + auto const& transitionMatrix = transformed.model->getTransitionMatrix(); + auto checkTransition = [&transitionMatrix](uint64_t row, uint64_t column) { + auto const rowEntries = transitionMatrix.getRow(row); + ASSERT_EQ(1ull, rowEntries.getNumberOfEntries()); + auto const& entry = *rowEntries.begin(); + EXPECT_EQ(column, entry.getColumn()); + EXPECT_EQ(storm::utility::one(), entry.getValue()); + }; + checkTransition(0, 2); + checkTransition(1, 3); + checkTransition(2, 4); + checkTransition(3, 4); + checkTransition(4, 4); + + auto const& rewardModel = transformed.model->getRewardModel("rew"); + ASSERT_TRUE(rewardModel.hasStateActionRewards()); + ASSERT_FALSE(rewardModel.hasTransitionRewards()); + auto const& actionRewards = rewardModel.getStateActionRewardVector(); + ASSERT_EQ(5ull, actionRewards.size()); + EXPECT_EQ(firstReward, actionRewards[2]); + EXPECT_EQ(secondReward, actionRewards[3]); +} + double computeInitialReward(std::shared_ptr> const& model, std::string const& formulaString) { auto const formula = storm::api::extractFormulasFromProperties(storm::api::parseProperties(formulaString)).front(); auto const result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(formula, true)); @@ -98,4 +160,47 @@ TEST(TransitionToActionRewardTransformerTest, MarkovAutomatonGeneral) { } } +TEST(TransitionToActionRewardTransformerTest, OverlappingIntervalRewardsAreNotMerged) { + storm::Interval const firstReward(1.0, 3.0); + storm::Interval const secondReward(2.0, 4.0); + auto const model = buildDtmcWithTransitionRewards(firstReward, secondReward); + + auto const transformed = storm::transformer::transformTransitionToActionRewards(model, {"rew"}); + + checkTransformedDtmc(transformed, firstReward, secondReward); +} + +TEST(TransitionToActionRewardTransformerTest, OverlappingRationalIntervalRewardsAreNotMerged) { + storm::RationalInterval const firstReward(storm::RationalNumber(1), storm::RationalNumber(3)); + storm::RationalInterval const secondReward(storm::RationalNumber(2), storm::RationalNumber(4)); + auto const model = buildDtmcWithTransitionRewards(firstReward, secondReward); + + auto const transformed = storm::transformer::transformTransitionToActionRewards(model, {"rew"}); + + checkTransformedDtmc(transformed, firstReward, secondReward); +} + +TEST(TransitionToActionRewardTransformerTest, DoubleOverlappingIntervalRewardsAreNotMerged) { + storm::Interval const firstReward(1.0, 3.0); + storm::Interval const secondReward(2.0, 4.0); + auto const model = buildDtmcWithTransitionRewards(firstReward, secondReward); + + auto const transformed = + storm::transformer::transformTransitionToActionRewards>(model, {"rew"}); + + checkTransformedDtmc(transformed, firstReward, secondReward); +} + +TEST(TransitionToActionRewardTransformerTest, RationalOverlappingRationalIntervalRewardsAreNotMerged) { + storm::RationalInterval const firstReward(storm::RationalNumber(1), storm::RationalNumber(3)); + storm::RationalInterval const secondReward(storm::RationalNumber(2), storm::RationalNumber(4)); + auto const model = buildDtmcWithTransitionRewards(firstReward, secondReward); + + auto const transformed = + storm::transformer::transformTransitionToActionRewards>( + model, {"rew"}); + + checkTransformedDtmc(transformed, firstReward, secondReward); +} + } // namespace