From b3178e17f6ec06120a9652ba5a166687e6773e47 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 21 Aug 2015 17:25:54 +0200
Subject: [PATCH] more bug fixes
Former-commit-id: 0b33b30efa15b6f7ed6892eb9842ee2da45aaa61
---
src/builder/DdPrismModelBuilder.cpp | 119 +++++++++---------
src/builder/DdPrismModelBuilder.h | 4 +-
src/builder/ExplicitPrismModelBuilder.cpp | 24 ++--
.../csl/helper/HybridCtmcCslHelper.cpp | 5 +-
.../csl/helper/SparseCtmcCslHelper.cpp | 6 +-
.../prctl/helper/HybridDtmcPrctlHelper.cpp | 2 +
.../prctl/helper/HybridMdpPrctlHelper.cpp | 2 +
.../prctl/helper/SymbolicDtmcPrctlHelper.cpp | 2 +
.../SparsePropositionalModelChecker.cpp | 1 +
.../SymbolicPropositionalModelChecker.cpp | 1 +
.../SparseDtmcEliminationModelChecker.cpp | 1 +
src/models/sparse/Ctmc.cpp | 2 +-
src/models/sparse/DeterministicModel.cpp | 1 +
src/models/sparse/Dtmc.cpp | 2 +-
src/models/sparse/MarkovAutomaton.cpp | 2 +-
src/models/sparse/Mdp.cpp | 2 +
src/models/sparse/Model.cpp | 2 +
src/models/sparse/Model.h | 3 +-
src/models/sparse/NondeterministicModel.cpp | 2 +
src/models/sparse/StandardRewardModel.cpp | 41 +++++-
src/models/sparse/StandardRewardModel.h | 17 +++
src/models/sparse/StochasticTwoPlayerGame.cpp | 2 +
src/models/symbolic/Ctmc.cpp | 3 +-
src/models/symbolic/DeterministicModel.cpp | 2 +
src/models/symbolic/Dtmc.cpp | 3 +-
src/models/symbolic/Mdp.cpp | 4 +-
src/models/symbolic/Model.cpp | 2 +
src/models/symbolic/Model.h | 4 +-
src/models/symbolic/NondeterministicModel.cpp | 3 +-
src/models/symbolic/StandardRewardModel.cpp | 17 ++-
src/models/symbolic/StandardRewardModel.h | 13 +-
.../symbolic/StochasticTwoPlayerGame.cpp | 3 +-
src/parser/AutoParser.cpp | 2 +
src/parser/DeterministicModelParser.cpp | 2 +
src/parser/MarkovAutomatonParser.cpp | 3 +
src/parser/NondeterministicModelParser.cpp | 2 +
...ministicModelBisimulationDecomposition.cpp | 3 +-
.../MaximalEndComponentDecomposition.cpp | 2 +
...tronglyConnectedComponentDecomposition.cpp | 1 +
src/storage/dd/CuddDd.h | 14 +--
src/utility/constants.cpp | 59 ++++++++-
src/utility/constants.h | 47 +------
src/utility/vector.h | 38 ++++++
.../builder/DdPrismModelBuilderTest.cpp | 2 +
.../builder/ExplicitPrismModelBuilderTest.cpp | 1 +
test/functional/builder/cluster2.sm | 12 +-
.../GmmxxDtmcPrctlModelCheckerTest.cpp | 1 +
.../GmmxxHybridDtmcPrctlModelCheckerTest.cpp | 1 +
.../GmmxxHybridMdpPrctlModelCheckerTest.cpp | 1 +
.../GmmxxMdpPrctlModelCheckerTest.cpp | 1 +
.../NativeCtmcCslModelCheckerTest.cpp | 10 +-
.../NativeDtmcPrctlModelCheckerTest.cpp | 1 +
.../NativeHybridDtmcPrctlModelCheckerTest.cpp | 1 +
.../NativeHybridMdpPrctlModelCheckerTest.cpp | 1 +
.../NativeMdpPrctlModelCheckerTest.cpp | 1 +
.../SparseDtmcEliminationModelCheckerTest.cpp | 1 +
.../SymbolicDtmcPrctlModelCheckerTest.cpp | 1 +
...ValueIterationMdpPrctlModelCheckerTest.cpp | 1 +
test/functional/parser/AutoParserTest.cpp | 1 +
.../parser/DeterministicModelParserTest.cpp | 1 +
.../parser/MarkovAutomatonParserTest.cpp | 1 +
.../NondeterministicModelParserTest.cpp | 1 +
...sticModelBisimulationDecompositionTest.cpp | 3 +-
.../MaximalEndComponentDecompositionTest.cpp | 1 +
test/functional/utility/GraphTest.cpp | 2 +
65 files changed, 352 insertions(+), 164 deletions(-)
diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp
index 2807e2f51..461713e9c 100644
--- a/src/builder/DdPrismModelBuilder.cpp
+++ b/src/builder/DdPrismModelBuilder.cpp
@@ -3,6 +3,7 @@
#include "src/models/symbolic/Dtmc.h"
#include "src/models/symbolic/Ctmc.h"
#include "src/models/symbolic/Mdp.h"
+#include "src/models/symbolic/StandardRewardModel.h"
#include "src/storage/dd/CuddDd.h"
#include "src/storage/dd/CuddDdManager.h"
@@ -63,7 +64,10 @@ namespace storm {
// A set of all variables used for encoding the nondeterminism (i.e. nondetermism + synchronization
// variables). This is handy to abstract from this variable set.
std::set<storm::expressions::Variable> allNondeterminismVariables;
-
+
+ // As set of all variables used for encoding the synchronization.
+ std::set<storm::expressions::Variable> allSynchronizationMetaVariables;
+
// DDs representing the identity for each variable.
std::map<storm::expressions::Variable, storm::dd::Add<Type>> variableToIdentityMap;
@@ -82,6 +86,7 @@ namespace storm {
for (auto const& actionIndex : program.getSynchronizingActionIndices()) {
std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = manager->addMetaVariable(program.getActionName(actionIndex));
synchronizationMetaVariables.push_back(variablePair.first);
+ allSynchronizationMetaVariables.insert(variablePair.first);
allNondeterminismVariables.insert(variablePair.first);
}
@@ -640,7 +645,7 @@ namespace storm {
}
template <storm::dd::DdType Type>
- std::pair<storm::dd::Add<Type>, typename DdPrismModelBuilder<Type>::ModuleDecisionDiagram> DdPrismModelBuilder<Type>::createSystemDecisionDiagram(GenerationInformation& generationInfo) {
+ std::tuple<storm::dd::Add<Type>, typename DdPrismModelBuilder<Type>::ModuleDecisionDiagram, boost::optional<storm::dd::Add<Type>>> DdPrismModelBuilder<Type>::createSystemDecisionDiagram(GenerationInformation& generationInfo) {
// Create the initial offset mapping.
std::map<uint_fast64_t, uint_fast64_t> synchronizingActionToOffsetMap;
for (auto const& actionIndex : generationInfo.program.getSynchronizingActionIndices()) {
@@ -698,8 +703,10 @@ namespace storm {
storm::dd::Add<Type> result = createSystemFromModule(generationInfo, system);
// For DTMCs, we normalize each row to 1 (to account for non-determinism).
+ boost::optional<storm::dd::Add<Type>> stateToChoiceCountMap;
if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) {
- result = result / result.sumAbstract(generationInfo.columnMetaVariables);
+ stateToChoiceCountMap = result.sumAbstract(generationInfo.columnMetaVariables);
+ result = result / stateToChoiceCountMap.get();
} else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) {
// For MDPs, we need to throw away the nondeterminism variables from the generation information that
// were never used.
@@ -709,11 +716,11 @@ namespace storm {
generationInfo.nondeterminismMetaVariables.resize(system.numberOfUsedNondeterminismVariables);
}
- return std::make_pair(result, system);
+ return std::make_tuple(result, system, stateToChoiceCountMap);
}
template <storm::dd::DdType Type>
- storm::models::symbolic::StandardRewardModel<Type, double> DdPrismModelBuilder<Type>::createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add<Type> const& fullTransitionMatrix) {
+ storm::models::symbolic::StandardRewardModel<Type, double> DdPrismModelBuilder<Type>::createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add<Type> const& transitionMatrix, storm::dd::Add<Type> const& reachableStatesAdd, boost::optional<storm::dd::Add<Type>> const& stateToChoiceCountMap) {
// Start by creating the state reward vector.
boost::optional<storm::dd::Add<Type>> stateRewards;
@@ -725,7 +732,7 @@ namespace storm {
storm::dd::Add<Type> rewards = generationInfo.rowExpressionAdapter->translateExpression(stateReward.getRewardValueExpression());
// Restrict the rewards to those states that satisfy the condition.
- rewards = states * rewards;
+ rewards = reachableStatesAdd * states * rewards;
// Perform some sanity checks.
STORM_LOG_WARN_COND(rewards.getMin() >= 0, "The reward model assigns negative rewards to some states.");
@@ -744,43 +751,36 @@ namespace storm {
for (auto const& stateActionReward : rewardModel.getStateActionRewards()) {
storm::dd::Add<Type> states = generationInfo.rowExpressionAdapter->translateExpression(stateActionReward.getStatePredicateExpression());
storm::dd::Add<Type> rewards = generationInfo.rowExpressionAdapter->translateExpression(stateActionReward.getRewardValueExpression());
-
storm::dd::Add<Type> synchronization = generationInfo.manager->getAddOne();
- storm::dd::Add<Type> transitions;
if (stateActionReward.isLabeled()) {
if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) {
synchronization = getSynchronizationDecisionDiagram(generationInfo, stateActionReward.getActionIndex());
}
- transitions = globalModule.synchronizingActionToDecisionDiagramMap.at(stateActionReward.getActionIndex()).transitionsDd;
+ states *= globalModule.synchronizingActionToDecisionDiagramMap.at(stateActionReward.getActionIndex()).guardDd * reachableStatesAdd;
} else {
if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) {
synchronization = getSynchronizationDecisionDiagram(generationInfo);
}
- transitions = globalModule.independentAction.transitionsDd;
+ states *= globalModule.independentAction.guardDd * reachableStatesAdd;
}
- storm::dd::Add<Type> transitionRewardDd = synchronization * states * rewards;
- if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) {
- // For DTMCs we need to keep the weighting for the scaling that follows.
- transitionRewardDd = transitions * transitionRewardDd;
- } else {
- // For all other model types, we do not scale the rewards.
- transitionRewardDd = transitions.notZero().toAdd() * transitionRewardDd;
- }
+ storm::dd::Add<Type> stateActionRewardDd = synchronization * states * rewards;
// Perform some sanity checks.
- STORM_LOG_WARN_COND(transitionRewardDd.getMin() >= 0, "The reward model assigns negative rewards to some states.");
- STORM_LOG_WARN_COND(!transitionRewardDd.isZero(), "The reward model does not assign any non-zero rewards.");
+ STORM_LOG_WARN_COND(stateActionRewardDd.getMin() >= 0, "The reward model assigns negative rewards to some states.");
+ STORM_LOG_WARN_COND(!stateActionRewardDd.isZero(), "The reward model does not assign any non-zero rewards.");
// Add the rewards to the global transition reward matrix.
- stateActionRewards.get() += transitionRewardDd;
+ stateActionRewards.get() += stateActionRewardDd;
}
- // Scale transition rewards for DTMCs.
+ // Scale state-action rewards for DTMCs.
if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) {
- stateActionRewards.get() /= fullTransitionMatrix;
+ STORM_LOG_THROW(static_cast<bool>(stateToChoiceCountMap), storm::exceptions::InvalidStateException, "A DD that reflects the number of choices per state was not build, but was expected to exist.");
+ stateActionRewards.get() /= stateToChoiceCountMap.get();
}
+ stateActionRewards.get().exportToDot("rewards.dot");
}
// Then build the transition reward matrix.
@@ -827,7 +827,8 @@ namespace storm {
// Scale transition rewards for DTMCs.
if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) {
- transitionRewards.get() /= fullTransitionMatrix;
+ STORM_LOG_THROW(static_cast<bool>(stateToChoiceCountMap), storm::exceptions::InvalidStateException, "A DD that reflects the number of choices per state was not build, but was expected to exist.");
+ stateActionRewards.get() /= stateToChoiceCountMap.get();
}
}
@@ -868,40 +869,10 @@ namespace storm {
// In particular, this creates the meta variables used to encode the model.
GenerationInformation generationInfo(preparedProgram);
- std::pair<storm::dd::Add<Type>, ModuleDecisionDiagram> transitionMatrixModulePair = createSystemDecisionDiagram(generationInfo);
- storm::dd::Add<Type> transitionMatrix = transitionMatrixModulePair.first;
- ModuleDecisionDiagram const& globalModule = transitionMatrixModulePair.second;
-
- // Finally, we build the DDs for the selected reward structures. It is important to do this now, because
- // we still have the uncut transition matrix, which is needed for the reward computation. This is because
- // the reward computation might divide by the transition probabilities, which must therefore never be 0.
- // However, cutting it to the reachable fragment, there might be zero probability transitions.
- std::vector<std::reference_wrapper<storm::prism::RewardModel const>> selectedRewardModels;
-
- // First, we make sure that all selected reward models actually exist.
- for (auto const& rewardModelName : options.rewardModelsToBuild) {
- STORM_LOG_THROW(rewardModelName.empty() || preparedProgram.hasRewardModel(rewardModelName), storm::exceptions::InvalidArgumentException, "Model does not possess a reward model with the name '" << rewardModelName << "'.");
- }
-
- for (auto const& rewardModel : preparedProgram.getRewardModels()) {
- if (options.buildAllRewardModels || options.rewardModelsToBuild.find(rewardModel.getName()) != options.rewardModelsToBuild.end()) {
- selectedRewardModels.push_back(rewardModel);
- }
- }
- // If no reward model was selected until now and a referenced reward model appears to be unique, we build
- // the only existing reward model (given that no explicit name was given for the referenced reward model).
- if (selectedRewardModels.empty() && preparedProgram.getNumberOfRewardModels() == 1 && options.rewardModelsToBuild.size() == 1 && *options.rewardModelsToBuild.begin() == "") {
- selectedRewardModels.push_back(preparedProgram.getRewardModel(0));
- }
- std::unordered_map<std::string, storm::models::symbolic::StandardRewardModel<Type, double>> rewardModels;
- if (options.buildAllRewardModels || !options.rewardModelsToBuild.empty()) {
- for (auto const& rewardModel : preparedProgram.getRewardModels()) {
- if (options.buildAllRewardModels || options.rewardModelsToBuild.find(rewardModel.getName()) != options.rewardModelsToBuild.end()) {
- STORM_LOG_TRACE("Building reward structure.");
- rewardModels.emplace(rewardModel.getName(), createRewardModelDecisionDiagrams(generationInfo, rewardModel, globalModule, transitionMatrix));
- }
- }
- }
+ std::tuple<storm::dd::Add<Type>, ModuleDecisionDiagram, boost::optional<storm::dd::Add<Type>>> system = createSystemDecisionDiagram(generationInfo);
+ storm::dd::Add<Type> transitionMatrix = std::get<0>(system);
+ ModuleDecisionDiagram const& globalModule = std::get<1>(system);
+ boost::optional<storm::dd::Add<Type>> stateToChoiceCountMap = std::get<2>(system);
// Cut the transitions and rewards to the reachable fragment of the state space.
storm::dd::Bdd<Type> initialStates = createInitialStatesDecisionDiagram(generationInfo);
@@ -912,9 +883,6 @@ namespace storm {
storm::dd::Bdd<Type> reachableStates = computeReachableStates(generationInfo, initialStates, transitionMatrixBdd);
storm::dd::Add<Type> reachableStatesAdd = reachableStates.toAdd();
transitionMatrix *= reachableStatesAdd;
- for (auto& rewardModel : rewardModels) {
- rewardModel.second *= reachableStatesAdd;
- }
// Detect deadlocks and 1) fix them if requested 2) throw an error otherwise.
storm::dd::Bdd<Type> statesWithTransition = transitionMatrixBdd.existsAbstract(generationInfo.columnMetaVariables);
@@ -940,6 +908,35 @@ namespace storm {
}
}
+ // Now build the reward models.
+ std::vector<std::reference_wrapper<storm::prism::RewardModel const>> selectedRewardModels;
+
+ // First, we make sure that all selected reward models actually exist.
+ for (auto const& rewardModelName : options.rewardModelsToBuild) {
+ STORM_LOG_THROW(rewardModelName.empty() || preparedProgram.hasRewardModel(rewardModelName), storm::exceptions::InvalidArgumentException, "Model does not possess a reward model with the name '" << rewardModelName << "'.");
+ }
+
+ for (auto const& rewardModel : preparedProgram.getRewardModels()) {
+ if (options.buildAllRewardModels || options.rewardModelsToBuild.find(rewardModel.getName()) != options.rewardModelsToBuild.end()) {
+ selectedRewardModels.push_back(rewardModel);
+ }
+ }
+ // If no reward model was selected until now and a referenced reward model appears to be unique, we build
+ // the only existing reward model (given that no explicit name was given for the referenced reward model).
+ if (selectedRewardModels.empty() && preparedProgram.getNumberOfRewardModels() == 1 && options.rewardModelsToBuild.size() == 1 && *options.rewardModelsToBuild.begin() == "") {
+ selectedRewardModels.push_back(preparedProgram.getRewardModel(0));
+ }
+
+ std::unordered_map<std::string, storm::models::symbolic::StandardRewardModel<Type, double>> rewardModels;
+ if (options.buildAllRewardModels || !options.rewardModelsToBuild.empty()) {
+ for (auto const& rewardModel : preparedProgram.getRewardModels()) {
+ if (options.buildAllRewardModels || options.rewardModelsToBuild.find(rewardModel.getName()) != options.rewardModelsToBuild.end()) {
+ STORM_LOG_TRACE("Building reward structure.");
+ rewardModels.emplace(rewardModel.getName(), createRewardModelDecisionDiagrams(generationInfo, rewardModel, globalModule, transitionMatrix, reachableStatesAdd, stateToChoiceCountMap));
+ }
+ }
+ }
+
// Build the labels that can be accessed as a shortcut.
std::map<std::string, storm::expressions::Expression> labelToExpressionMapping;
for (auto const& label : preparedProgram.getLabels()) {
diff --git a/src/builder/DdPrismModelBuilder.h b/src/builder/DdPrismModelBuilder.h
index a6d45c3fc..4380598c4 100644
--- a/src/builder/DdPrismModelBuilder.h
+++ b/src/builder/DdPrismModelBuilder.h
@@ -189,9 +189,9 @@ namespace storm {
static storm::dd::Add<Type> createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram const& module);
- static storm::models::symbolic::StandardRewardModel<Type, double> createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add<Type> const& fullTransitionMatrix);
+ static storm::models::symbolic::StandardRewardModel<Type, double> createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add<Type> const& transitionMatrix, storm::dd::Add<Type> const& reachableStatesAdd, boost::optional<storm::dd::Add<Type>> const& stateToChoiceCountMap);
- static std::pair<storm::dd::Add<Type>, ModuleDecisionDiagram> createSystemDecisionDiagram(GenerationInformation& generationInfo);
+ static std::tuple<storm::dd::Add<Type>, ModuleDecisionDiagram, boost::optional<storm::dd::Add<Type>>> createSystemDecisionDiagram(GenerationInformation& generationInfo);
static storm::dd::Bdd<Type> createInitialStatesDecisionDiagram(GenerationInformation& generationInfo);
diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp
index 18c58a69a..c65dc5b3a 100644
--- a/src/builder/ExplicitPrismModelBuilder.cpp
+++ b/src/builder/ExplicitPrismModelBuilder.cpp
@@ -5,6 +5,7 @@
#include "src/models/sparse/Dtmc.h"
#include "src/models/sparse/Ctmc.h"
#include "src/models/sparse/Mdp.h"
+#include "src/models/sparse/StandardRewardModel.h"
#include "src/settings/modules/GeneralSettings.h"
@@ -653,6 +654,11 @@ namespace storm {
for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) {
if (rewardModelIt->get().hasStateRewards()) {
builderIt->stateRewardVector.push_back(storm::utility::zero<ValueType>());
+ for (auto const& stateReward : rewardModelIt->get().getStateRewards()) {
+ if (evaluator.asBool(stateReward.getStatePredicateExpression())) {
+ builderIt->stateRewardVector.back() += ValueType(evaluator.asRational(stateReward.getRewardValueExpression()));
+ }
+ }
}
if (rewardModelIt->get().hasStateActionRewards()) {
@@ -668,14 +674,6 @@ namespace storm {
auto builderIt = rewardModelBuilders.begin();
for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) {
- if (rewardModelIt->get().hasStateRewards()) {
- for (auto const& stateReward : rewardModelIt->get().getStateRewards()) {
- if (evaluator.asBool(stateReward.getStatePredicateExpression())) {
- builderIt->stateRewardVector.back() += ValueType(evaluator.asRational(stateReward.getRewardValueExpression()));
- }
- }
- }
-
if (rewardModelIt->get().hasStateActionRewards()) {
for (auto const& stateActionReward : rewardModelIt->get().getStateActionRewards()) {
if (!stateActionReward.isLabeled()) {
@@ -702,19 +700,11 @@ namespace storm {
auto builderIt = rewardModelBuilders.begin();
for (auto rewardModelIt = selectedRewardModels.begin(), rewardModelIte = selectedRewardModels.end(); rewardModelIt != rewardModelIte; ++rewardModelIt, ++builderIt) {
- if (rewardModelIt->get().hasStateRewards()) {
- for (auto const& stateReward : rewardModelIt->get().getStateRewards()) {
- if (evaluator.asBool(stateReward.getStatePredicateExpression())) {
- builderIt->stateRewardVector.back() += ValueType(evaluator.asRational(stateReward.getRewardValueExpression()));
- }
- }
- }
-
if (rewardModelIt->get().hasStateActionRewards()) {
for (auto const& stateActionReward : rewardModelIt->get().getStateActionRewards()) {
if (stateActionReward.isLabeled() && stateActionReward.getActionIndex() == choice.getActionIndex()) {
if (evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
- builderIt->stateActionRewardVector.back() += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression())) / totalNumberOfChoices;
+ builderIt->stateActionRewardVector.back() += ValueType(evaluator.asRational(stateActionReward.getRewardValueExpression()));
}
}
}
diff --git a/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp b/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp
index cd289f33d..692d56629 100644
--- a/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp
+++ b/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp
@@ -11,6 +11,8 @@
#include "src/utility/macros.h"
#include "src/utility/graph.h"
+#include "src/models/symbolic/StandardRewardModel.h"
+
#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
#include "src/modelchecker/results/HybridQuantitativeCheckResult.h"
@@ -266,7 +268,8 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd);
// Then compute the state reward vector to use in the computation.
- storm::dd::Add<DdType> totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, model.getColumnVariables());
+ storm::dd::Add<DdType> totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, model.getColumnVariables(), exitRateVector);
+ totalRewardVector.exportToDot("rewards.dot");
std::vector<ValueType> explicitTotalRewardVector = totalRewardVector.template toVector<ValueType>(odd);
// Finally, compute the transient probabilities.
diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
index 8c90dd905..deb458f42 100644
--- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
+++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
@@ -314,7 +314,7 @@ namespace storm {
// Initialize result to state rewards of the this->getModel().
std::vector<ValueType> result(rewardModel.getStateRewardVector());
-
+
// If the time-bound is not zero, we need to perform a transient analysis.
if (timeBound > 0) {
ValueType uniformizationRate = 0;
@@ -335,7 +335,7 @@ namespace storm {
std::vector<ValueType> SparseCtmcCslHelper<ValueType, RewardModelType>::computeCumulativeRewards(storm::storage::SparseMatrix<ValueType> const& rateMatrix, std::vector<ValueType> const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
// Only compute the result if the model has a state-based reward this->getModel().
STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
-
+
uint_fast64_t numberOfStates = rateMatrix.getRowCount();
// If the time bound is zero, the result is the constant zero vector.
@@ -356,7 +356,7 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> uniformizedMatrix = computeUniformizedMatrix(rateMatrix, storm::storage::BitVector(numberOfStates, true), uniformizationRate, exitRateVector);
// Compute the total state reward vector.
- std::vector<ValueType> totalRewardVector = rewardModel.getTotalRewardVector(uniformizedMatrix);
+ std::vector<ValueType> totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, exitRateVector);
// Finally, compute the transient probabilities.
return computeTransientProbabilities<true>(uniformizedMatrix, nullptr, timeBound, uniformizationRate, totalRewardVector, linearEquationSolverFactory);
diff --git a/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
index 02b318310..1cdc1f840 100644
--- a/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
+++ b/src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
@@ -7,6 +7,8 @@
#include "src/utility/graph.h"
+#include "src/models/symbolic/StandardRewardModel.h"
+
#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
#include "src/modelchecker/results/HybridQuantitativeCheckResult.h"
diff --git a/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
index 2409fe5d3..46476d95b 100644
--- a/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
+++ b/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
@@ -7,6 +7,8 @@
#include "src/utility/graph.h"
+#include "src/models/symbolic/StandardRewardModel.h"
+
#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
#include "src/modelchecker/results/HybridQuantitativeCheckResult.h"
diff --git a/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp
index cc6853bf2..4ef62691a 100644
--- a/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp
+++ b/src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp
@@ -6,6 +6,8 @@
#include "src/storage/dd/CuddBdd.h"
#include "src/storage/dd/CuddOdd.h"
+#include "src/models/symbolic/StandardRewardModel.h"
+
#include "src/utility/graph.h"
#include "src/exceptions/InvalidPropertyException.h"
diff --git a/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp
index 44d6a454b..ef2a63a2e 100644
--- a/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp
+++ b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp
@@ -6,6 +6,7 @@
#include "src/models/sparse/Ctmc.h"
#include "src/models/sparse/Mdp.h"
#include "src/models/sparse/MarkovAutomaton.h"
+#include "src/models/sparse/StandardRewardModel.h"
#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
diff --git a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp
index e594c2f70..2e51ff7ad 100644
--- a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp
+++ b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp
@@ -6,6 +6,7 @@
#include "src/models/symbolic/Dtmc.h"
#include "src/models/symbolic/Ctmc.h"
#include "src/models/symbolic/Mdp.h"
+#include "src/models/symbolic/StandardRewardModel.h"
#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
index 86a741a09..a16ec2089 100644
--- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
+++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
@@ -11,6 +11,7 @@
#include "src/storage/StronglyConnectedComponentDecomposition.h"
+#include "src/models/sparse/StandardRewardModel.h"
#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
diff --git a/src/models/sparse/Ctmc.cpp b/src/models/sparse/Ctmc.cpp
index a9509ddbb..371d48270 100644
--- a/src/models/sparse/Ctmc.cpp
+++ b/src/models/sparse/Ctmc.cpp
@@ -1,5 +1,5 @@
#include "src/models/sparse/Ctmc.h"
-
+#include "src/models/sparse/StandardRewardModel.h"
#include "src/adapters/CarlAdapter.h"
#include "src/utility/macros.h"
diff --git a/src/models/sparse/DeterministicModel.cpp b/src/models/sparse/DeterministicModel.cpp
index 3942f8301..d774d5e7f 100644
--- a/src/models/sparse/DeterministicModel.cpp
+++ b/src/models/sparse/DeterministicModel.cpp
@@ -1,4 +1,5 @@
#include "src/models/sparse/DeterministicModel.h"
+#include "src/models/sparse/StandardRewardModel.h"
#include "src/utility/constants.h"
#include "src/adapters/CarlAdapter.h"
diff --git a/src/models/sparse/Dtmc.cpp b/src/models/sparse/Dtmc.cpp
index a92872c0f..78a8a4a0f 100644
--- a/src/models/sparse/Dtmc.cpp
+++ b/src/models/sparse/Dtmc.cpp
@@ -1,5 +1,5 @@
#include "src/models/sparse/Dtmc.h"
-
+#include "src/models/sparse/StandardRewardModel.h"
#include "src/adapters/CarlAdapter.h"
#include "src/exceptions/NotImplementedException.h"
#include "src/exceptions/InvalidArgumentException.h"
diff --git a/src/models/sparse/MarkovAutomaton.cpp b/src/models/sparse/MarkovAutomaton.cpp
index 694cb2a07..03b9341f2 100644
--- a/src/models/sparse/MarkovAutomaton.cpp
+++ b/src/models/sparse/MarkovAutomaton.cpp
@@ -1,5 +1,5 @@
#include "src/models/sparse/MarkovAutomaton.h"
-
+#include "src/models/sparse/StandardRewardModel.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "src/utility/constants.h"
#include "src/adapters/CarlAdapter.h"
diff --git a/src/models/sparse/Mdp.cpp b/src/models/sparse/Mdp.cpp
index f89225d27..4d62741e9 100644
--- a/src/models/sparse/Mdp.cpp
+++ b/src/models/sparse/Mdp.cpp
@@ -4,6 +4,8 @@
#include "src/utility/constants.h"
#include "src/adapters/CarlAdapter.h"
+#include "src/models/sparse/StandardRewardModel.h"
+
namespace storm {
namespace models {
namespace sparse {
diff --git a/src/models/sparse/Model.cpp b/src/models/sparse/Model.cpp
index 6e56003ba..81a224a22 100644
--- a/src/models/sparse/Model.cpp
+++ b/src/models/sparse/Model.cpp
@@ -2,6 +2,8 @@
#include <boost/algorithm/string/join.hpp>
+#include "src/models/sparse/StandardRewardModel.h"
+
#include "src/utility/vector.h"
#include "src/adapters/CarlAdapter.h"
diff --git a/src/models/sparse/Model.h b/src/models/sparse/Model.h
index 7aadc01c9..8adc60bb1 100644
--- a/src/models/sparse/Model.h
+++ b/src/models/sparse/Model.h
@@ -7,7 +7,6 @@
#include <boost/optional.hpp>
#include "src/models/ModelBase.h"
-#include "src/models/sparse/StandardRewardModel.h"
#include "src/models/sparse/StateLabeling.h"
#include "src/storage/sparse/StateType.h"
#include "src/storage/BitVector.h"
@@ -21,6 +20,8 @@ namespace storm {
// The type used for storing a set of labels.
typedef boost::container::flat_set<uint_fast64_t> LabelSet;
+ template<typename ValueType>
+ class StandardRewardModel;
/*!
* Base class for all sparse models.
diff --git a/src/models/sparse/NondeterministicModel.cpp b/src/models/sparse/NondeterministicModel.cpp
index a2310d073..fd3f95f02 100644
--- a/src/models/sparse/NondeterministicModel.cpp
+++ b/src/models/sparse/NondeterministicModel.cpp
@@ -1,5 +1,7 @@
#include "src/models/sparse/NondeterministicModel.h"
+#include "src/models/sparse/StandardRewardModel.h"
+
#include "src/adapters/CarlAdapter.h"
namespace storm {
diff --git a/src/models/sparse/StandardRewardModel.cpp b/src/models/sparse/StandardRewardModel.cpp
index f6a3d5a54..0ba437c96 100644
--- a/src/models/sparse/StandardRewardModel.cpp
+++ b/src/models/sparse/StandardRewardModel.cpp
@@ -130,7 +130,7 @@ namespace storm {
template<typename MatrixValueType>
std::vector<ValueType> StandardRewardModel<ValueType>::getTotalRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix) const {
std::vector<ValueType> result = this->hasTransitionRewards() ? transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()) : (this->hasStateActionRewards() ? this->getStateActionRewardVector() : std::vector<ValueType>(transitionMatrix.getRowCount()));
- if (this->hasStateActionRewards() && this->hasStateActionRewards()) {
+ if (this->hasStateActionRewards() && this->hasTransitionRewards()) {
storm::utility::vector::addVectors(result, this->getStateActionRewardVector(), result);
}
if (this->hasStateRewards()) {
@@ -139,6 +139,25 @@ namespace storm {
return result;
}
+ template<typename ValueType>
+ template<typename MatrixValueType>
+ std::vector<ValueType> StandardRewardModel<ValueType>::getTotalRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, std::vector<ValueType> const& weights) const {
+ std::vector<ValueType> result = this->hasTransitionRewards() ? transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()) : (this->hasStateActionRewards() ? this->getStateActionRewardVector() : std::vector<ValueType>(transitionMatrix.getRowCount()));
+ if (!this->hasTransitionRewards() && this->hasStateActionRewards()) {
+ // If we initialized the result with the state-action rewards we can scale the result in place.
+ storm::utility::vector::multiplyVectorsPointwise(result, weights, result);
+ }
+ if (this->hasStateActionRewards() && this->hasTransitionRewards()) {
+ // If we initialized the result with the transition rewards and still have state-action rewards,
+ // we need to add the scaled vector directly.
+ storm::utility::vector::applyPointwise<ValueType>(weights, this->getStateActionRewardVector(), result, [] (ValueType const& a, ValueType const& b, ValueType const& c) { return c + a * b; } );
+ }
+ if (this->hasStateRewards()) {
+ storm::utility::vector::addVectorToGroupedVector(result, this->getStateRewardVector(), transitionMatrix.getRowGroupIndices());
+ }
+ return result;
+ }
+
template<typename ValueType>
template<typename MatrixValueType>
std::vector<ValueType> StandardRewardModel<ValueType>::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, storm::storage::BitVector const& filter) const {
@@ -198,23 +217,43 @@ namespace storm {
return result;
}
+ template <typename ValueType>
+ std::ostream& operator<<(std::ostream& out, StandardRewardModel<ValueType> const& rewardModel) {
+ out << std::boolalpha << "reward model [state reward: "
+ << rewardModel.hasStateRewards()
+ << ", state-action rewards: "
+ << rewardModel.hasStateActionRewards()
+ << ", transition rewards: "
+ << rewardModel.hasTransitionRewards()
+ << "]"
+ << std::noboolalpha;
+ return out;
+ }
+
// Explicitly instantiate the class.
template std::vector<double> StandardRewardModel<double>::getTotalRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix) const;
template std::vector<double> StandardRewardModel<double>::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::BitVector const& filter) const;
+ template std::vector<double> StandardRewardModel<double>::getTotalRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<double> const& weights) const;
template void StandardRewardModel<double>::reduceToStateBasedRewards(storm::storage::SparseMatrix<double> const& transitionMatrix, bool reduceToStateRewards);
template class StandardRewardModel<double>;
+ template std::ostream& operator<<<double>(std::ostream& out, StandardRewardModel<double> const& rewardModel);
template std::vector<float> StandardRewardModel<float>::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix<float> const& transitionMatrix, storm::storage::BitVector const& filter) const;
template std::vector<float> StandardRewardModel<float>::getTotalRewardVector(storm::storage::SparseMatrix<float> const& transitionMatrix) const;
+ template std::vector<float> StandardRewardModel<float>::getTotalRewardVector(storm::storage::SparseMatrix<float> const& transitionMatrix, std::vector<float> const& weights) const;
template void StandardRewardModel<float>::reduceToStateBasedRewards(storm::storage::SparseMatrix<float> const& transitionMatrix, bool reduceToStateRewards);
template class StandardRewardModel<float>;
+// template std::ostream& operator<<<float>(std::ostream& out, StandardRewardModel<float> const& rewardModel);
#ifdef STORM_HAVE_CARL
template std::vector<storm::RationalFunction> StandardRewardModel<storm::RationalFunction>::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::BitVector const& filter) const;
template std::vector<storm::RationalFunction> StandardRewardModel<storm::RationalFunction>::getTotalRewardVector(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix) const;
+ template std::vector<storm::RationalFunction> StandardRewardModel<storm::RationalFunction>::getTotalRewardVector(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::vector<storm::RationalFunction> const& weights) const;
template void StandardRewardModel<storm::RationalFunction>::reduceToStateBasedRewards(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, bool reduceToStateRewards);
template class StandardRewardModel<storm::RationalFunction>;
+// template std::ostream& operator<<<storm::RationalFunction>(std::ostream& out, StandardRewardModel<storm::RationalFunction> const& rewardModel);
#endif
}
+
}
}
\ No newline at end of file
diff --git a/src/models/sparse/StandardRewardModel.h b/src/models/sparse/StandardRewardModel.h
index d1c78cb15..7bf8afe19 100644
--- a/src/models/sparse/StandardRewardModel.h
+++ b/src/models/sparse/StandardRewardModel.h
@@ -168,6 +168,17 @@ namespace storm {
*/
template<typename MatrixValueType>
std::vector<ValueType> getTotalRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix) const;
+
+ /*!
+ * Creates a vector representing the complete reward vector based on the state-, state-action- and
+ * transition-based rewards in the reward model.
+ *
+ * @param transitionMatrix The matrix that is used to weight the values of the transition reward matrix.
+ * @param weights A vector used for scaling the entries of the state-action rewards (if present).
+ * @return The full state-action reward vector.
+ */
+ template<typename MatrixValueType>
+ std::vector<ValueType> getTotalRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, std::vector<ValueType> const& weights) const;
/*!
* Creates a vector representing the complete reward vector based on the state-, state-action- and
@@ -217,6 +228,9 @@ namespace storm {
*/
std::size_t getSizeInBytes() const;
+ template <typename ValueTypePrime>
+ friend std::ostream& operator<<(std::ostream& out, StandardRewardModel<ValueTypePrime> const& rewardModel);
+
private:
// An (optional) vector representing the state rewards.
boost::optional<std::vector<ValueType>> optionalStateRewardVector;
@@ -227,6 +241,9 @@ namespace storm {
// An (optional) matrix representing the transition rewards.
boost::optional<storm::storage::SparseMatrix<ValueType>> optionalTransitionRewardMatrix;
};
+
+ template <typename ValueType>
+ std::ostream& operator<<(std::ostream& out, StandardRewardModel<ValueType> const& rewardModel);
}
}
}
diff --git a/src/models/sparse/StochasticTwoPlayerGame.cpp b/src/models/sparse/StochasticTwoPlayerGame.cpp
index 6158e3588..132410720 100644
--- a/src/models/sparse/StochasticTwoPlayerGame.cpp
+++ b/src/models/sparse/StochasticTwoPlayerGame.cpp
@@ -1,5 +1,7 @@
#include "src/models/sparse/StochasticTwoPlayerGame.h"
+#include "src/models/sparse/StandardRewardModel.h"
+
#include "src/adapters/CarlAdapter.h"
namespace storm {
diff --git a/src/models/symbolic/Ctmc.cpp b/src/models/symbolic/Ctmc.cpp
index d2ad8af65..297b3d99a 100644
--- a/src/models/symbolic/Ctmc.cpp
+++ b/src/models/symbolic/Ctmc.cpp
@@ -1,10 +1,11 @@
#include "src/models/symbolic/Ctmc.h"
-
#include "src/storage/dd/CuddDdManager.h"
#include "src/storage/dd/CuddAdd.h"
#include "src/storage/dd/CuddBdd.h"
+#include "src/models/symbolic/StandardRewardModel.h"
+
namespace storm {
namespace models {
namespace symbolic {
diff --git a/src/models/symbolic/DeterministicModel.cpp b/src/models/symbolic/DeterministicModel.cpp
index 081183eb7..361e6c438 100644
--- a/src/models/symbolic/DeterministicModel.cpp
+++ b/src/models/symbolic/DeterministicModel.cpp
@@ -4,6 +4,8 @@
#include "src/storage/dd/CuddAdd.h"
#include "src/storage/dd/CuddBdd.h"
+#include "src/models/symbolic/StandardRewardModel.h"
+
namespace storm {
namespace models {
namespace symbolic {
diff --git a/src/models/symbolic/Dtmc.cpp b/src/models/symbolic/Dtmc.cpp
index ca1e6d8cb..aed3d9c20 100644
--- a/src/models/symbolic/Dtmc.cpp
+++ b/src/models/symbolic/Dtmc.cpp
@@ -1,10 +1,11 @@
#include "src/models/symbolic/Dtmc.h"
-
#include "src/storage/dd/CuddDdManager.h"
#include "src/storage/dd/CuddAdd.h"
#include "src/storage/dd/CuddBdd.h"
+#include "src/models/symbolic/StandardRewardModel.h"
+
namespace storm {
namespace models {
namespace symbolic {
diff --git a/src/models/symbolic/Mdp.cpp b/src/models/symbolic/Mdp.cpp
index a14d78961..093190106 100644
--- a/src/models/symbolic/Mdp.cpp
+++ b/src/models/symbolic/Mdp.cpp
@@ -1,11 +1,11 @@
#include "src/models/symbolic/Mdp.h"
-
-
#include "src/storage/dd/CuddDdManager.h"
#include "src/storage/dd/CuddAdd.h"
#include "src/storage/dd/CuddBdd.h"
+#include "src/models/symbolic/StandardRewardModel.h"
+
namespace storm {
namespace models {
namespace symbolic {
diff --git a/src/models/symbolic/Model.cpp b/src/models/symbolic/Model.cpp
index fb0538605..7c31e3fa1 100644
--- a/src/models/symbolic/Model.cpp
+++ b/src/models/symbolic/Model.cpp
@@ -10,6 +10,8 @@
#include "src/storage/dd/CuddAdd.h"
#include "src/storage/dd/CuddBdd.h"
+#include "src/models/symbolic/StandardRewardModel.h"
+
namespace storm {
namespace models {
namespace symbolic {
diff --git a/src/models/symbolic/Model.h b/src/models/symbolic/Model.h
index 0d7fb70be..b70c39b97 100644
--- a/src/models/symbolic/Model.h
+++ b/src/models/symbolic/Model.h
@@ -10,7 +10,6 @@
#include "src/storage/expressions/Variable.h"
#include "src/storage/dd/DdType.h"
#include "src/models/ModelBase.h"
-#include "src/models/symbolic/StandardRewardModel.h"
#include "src/utility/OsDetection.h"
namespace storm {
@@ -30,6 +29,9 @@ namespace storm {
namespace models {
namespace symbolic {
+ template<storm::dd::DdType Type, typename ValueType>
+ class StandardRewardModel;
+
/*!
* Base class for all symbolic models.
*/
diff --git a/src/models/symbolic/NondeterministicModel.cpp b/src/models/symbolic/NondeterministicModel.cpp
index 1b080ecee..f5decd7d5 100644
--- a/src/models/symbolic/NondeterministicModel.cpp
+++ b/src/models/symbolic/NondeterministicModel.cpp
@@ -1,10 +1,11 @@
#include "src/models/symbolic/NondeterministicModel.h"
-
#include "src/storage/dd/CuddDdManager.h"
#include "src/storage/dd/CuddAdd.h"
#include "src/storage/dd/CuddBdd.h"
+#include "src/models/symbolic/StandardRewardModel.h"
+
namespace storm {
namespace models {
namespace symbolic {
diff --git a/src/models/symbolic/StandardRewardModel.cpp b/src/models/symbolic/StandardRewardModel.cpp
index 1d2ce401b..4762ff242 100644
--- a/src/models/symbolic/StandardRewardModel.cpp
+++ b/src/models/symbolic/StandardRewardModel.cpp
@@ -97,6 +97,21 @@ namespace storm {
return result;
}
+ template <storm::dd::DdType Type, typename ValueType>
+ storm::dd::Add<Type> StandardRewardModel<Type, ValueType>::getTotalRewardVector(storm::dd::Add<Type> const& transitionMatrix, std::set<storm::expressions::Variable> const& columnVariables, storm::dd::Add<Type> const& weights) const {
+ storm::dd::Add<Type> result = transitionMatrix.getDdManager()->getAddZero();
+ if (this->hasStateRewards()) {
+ result += optionalStateRewardVector.get();
+ }
+ if (this->hasStateActionRewards()) {
+ result += optionalStateActionRewardVector.get() * weights;
+ }
+ if (this->hasTransitionRewards()) {
+ result += (transitionMatrix * this->getTransitionRewardMatrix()).sumAbstract(columnVariables);
+ }
+ return result;
+ }
+
template <storm::dd::DdType Type, typename ValueType>
StandardRewardModel<Type, ValueType>& StandardRewardModel<Type, ValueType>::operator*=(storm::dd::Add<Type> const& filter) {
if (this->hasStateRewards()) {
@@ -116,7 +131,7 @@ namespace storm {
StandardRewardModel<Type, ValueType> StandardRewardModel<Type, ValueType>::divideStateRewardVector(storm::dd::Add<Type> const& divisor) const {
boost::optional<storm::dd::Add<Type>> modifiedStateRewardVector;
if (this->hasStateRewards()) {
- modifiedStateRewardVector.get() = modifiedStateRewardVector.get() / divisor;
+ modifiedStateRewardVector = this->optionalStateRewardVector.get() / divisor;
}
return StandardRewardModel<Type, ValueType>(modifiedStateRewardVector, this->optionalStateActionRewardVector, this->optionalTransitionRewardMatrix);
}
diff --git a/src/models/symbolic/StandardRewardModel.h b/src/models/symbolic/StandardRewardModel.h
index a53cd1a52..76abc9fdd 100644
--- a/src/models/symbolic/StandardRewardModel.h
+++ b/src/models/symbolic/StandardRewardModel.h
@@ -144,11 +144,22 @@ namespace storm {
* transition-based rewards in the reward model.
*
* @param transitionMatrix The matrix that is used to weight the values of the transition reward matrix.
- * @param columnVariables .
+ * @param columnVariables The column variables of the model.
* @return The full state-action reward vector.
*/
storm::dd::Add<Type> getTotalRewardVector(storm::dd::Add<Type> const& transitionMatrix, std::set<storm::expressions::Variable> const& columnVariables) const;
+ /*!
+ * Creates a vector representing the complete reward vector based on the state-, state-action- and
+ * transition-based rewards in the reward model.
+ *
+ * @param transitionMatrix The matrix that is used to weight the values of the transition reward matrix.
+ * @param columnVariables The column variables of the model.
+ * @param weights The weights used to scale the state-action reward vector.
+ * @return The full state-action reward vector.
+ */
+ storm::dd::Add<Type> getTotalRewardVector(storm::dd::Add<Type> const& transitionMatrix, std::set<storm::expressions::Variable> const& columnVariables, storm::dd::Add<Type> const& weights) const;
+
/*!
* Multiplies all components of the reward model with the given DD.
*
diff --git a/src/models/symbolic/StochasticTwoPlayerGame.cpp b/src/models/symbolic/StochasticTwoPlayerGame.cpp
index 6b3fc393a..370df9ffb 100644
--- a/src/models/symbolic/StochasticTwoPlayerGame.cpp
+++ b/src/models/symbolic/StochasticTwoPlayerGame.cpp
@@ -1,10 +1,11 @@
#include "src/models/symbolic/StochasticTwoPlayerGame.h"
-
#include "src/storage/dd/CuddDdManager.h"
#include "src/storage/dd/CuddAdd.h"
#include "src/storage/dd/CuddBdd.h"
+#include "src/models/symbolic/StandardRewardModel.h"
+
namespace storm {
namespace models {
namespace symbolic {
diff --git a/src/parser/AutoParser.cpp b/src/parser/AutoParser.cpp
index 065ad4327..6bd71189d 100644
--- a/src/parser/AutoParser.cpp
+++ b/src/parser/AutoParser.cpp
@@ -1,5 +1,7 @@
#include "src/parser/AutoParser.h"
+#include "src/models/sparse/StandardRewardModel.h"
+
#include "src/parser/MappedFile.h"
#include "src/parser/DeterministicModelParser.h"
diff --git a/src/parser/DeterministicModelParser.cpp b/src/parser/DeterministicModelParser.cpp
index f0d0770cb..fd163c56a 100644
--- a/src/parser/DeterministicModelParser.cpp
+++ b/src/parser/DeterministicModelParser.cpp
@@ -3,6 +3,8 @@
#include <string>
#include <vector>
+#include "src/models/sparse/StandardRewardModel.h"
+
#include "src/parser/DeterministicSparseTransitionParser.h"
#include "src/parser/AtomicPropositionLabelingParser.h"
#include "src/parser/SparseStateRewardParser.h"
diff --git a/src/parser/MarkovAutomatonParser.cpp b/src/parser/MarkovAutomatonParser.cpp
index 7325a922e..bc61a7a1f 100644
--- a/src/parser/MarkovAutomatonParser.cpp
+++ b/src/parser/MarkovAutomatonParser.cpp
@@ -1,6 +1,9 @@
#include "MarkovAutomatonParser.h"
#include "AtomicPropositionLabelingParser.h"
#include "SparseStateRewardParser.h"
+
+#include "src/models/sparse/StandardRewardModel.h"
+
#include "src/exceptions/WrongFormatException.h"
#include "log4cplus/logger.h"
diff --git a/src/parser/NondeterministicModelParser.cpp b/src/parser/NondeterministicModelParser.cpp
index 0a8ad5ae8..8f3e8028d 100644
--- a/src/parser/NondeterministicModelParser.cpp
+++ b/src/parser/NondeterministicModelParser.cpp
@@ -3,6 +3,8 @@
#include <string>
#include <vector>
+#include "src/models/sparse/StandardRewardModel.h"
+
#include "src/parser/NondeterministicSparseTransitionParser.h"
#include "src/parser/AtomicPropositionLabelingParser.h"
#include "src/parser/SparseStateRewardParser.h"
diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp
index 725d46b02..f362da110 100644
--- a/src/storage/DeterministicModelBisimulationDecomposition.cpp
+++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp
@@ -10,6 +10,8 @@
#include "src/modelchecker/propositional/SparsePropositionalModelChecker.h"
#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
+#include "src/models/sparse/StandardRewardModel.h"
+
#include "src/utility/graph.h"
#include "src/utility/constants.h"
#include "src/exceptions/IllegalFunctionCallException.h"
@@ -19,7 +21,6 @@
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/GeneralSettings.h"
-
namespace storm {
namespace storage {
diff --git a/src/storage/MaximalEndComponentDecomposition.cpp b/src/storage/MaximalEndComponentDecomposition.cpp
index 7a8c53cda..f7c314eb4 100644
--- a/src/storage/MaximalEndComponentDecomposition.cpp
+++ b/src/storage/MaximalEndComponentDecomposition.cpp
@@ -1,6 +1,8 @@
#include <list>
#include <queue>
+#include "src/models/sparse/StandardRewardModel.h"
+
#include "src/storage/MaximalEndComponentDecomposition.h"
#include "src/storage/StronglyConnectedComponentDecomposition.h"
diff --git a/src/storage/StronglyConnectedComponentDecomposition.cpp b/src/storage/StronglyConnectedComponentDecomposition.cpp
index a03a22b63..0e3938da3 100644
--- a/src/storage/StronglyConnectedComponentDecomposition.cpp
+++ b/src/storage/StronglyConnectedComponentDecomposition.cpp
@@ -1,5 +1,6 @@
#include "src/storage/StronglyConnectedComponentDecomposition.h"
#include "src/models/sparse/Model.h"
+#include "src/models/sparse/StandardRewardModel.h"
#include "src/adapters/CarlAdapter.h"
namespace storm {
diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h
index b80bfc671..0077bcc8a 100644
--- a/src/storage/dd/CuddDd.h
+++ b/src/storage/dd/CuddDd.h
@@ -105,6 +105,13 @@ namespace storm {
*/
std::shared_ptr<DdManager<DdType::CUDD> const> getDdManager() const;
+ /*!
+ * Retrieves the set of all meta variables contained in the DD.
+ *
+ * @return The set of all meta variables contained in the DD.
+ */
+ std::set<storm::expressions::Variable>& getContainedMetaVariables();
+
protected:
/*!
@@ -123,13 +130,6 @@ namespace storm {
*/
static std::vector<uint_fast64_t> getSortedVariableIndices(DdManager<DdType::CUDD> const& manager, std::set<storm::expressions::Variable> const& metaVariables);
- /*!
- * Retrieves the set of all meta variables contained in the DD.
- *
- * @return The set of all meta variables contained in the DD.
- */
- std::set<storm::expressions::Variable>& getContainedMetaVariables();
-
/*!
* Adds the given set of meta variables to the DD.
*
diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp
index 8e21b2325..c3edc2639 100644
--- a/src/utility/constants.cpp
+++ b/src/utility/constants.cpp
@@ -59,16 +59,62 @@ namespace storm {
return value;
}
+ // For floats we specialize this class and consider the comparison modulo some predefined precision.
+ template<>
+ class ConstantsComparator<float> {
+ public:
+ ConstantsComparator();
+
+ ConstantsComparator(float precision);
+
+ bool isOne(float const& value) const;
+
+ bool isZero(float const& value) const;
+
+ bool isEqual(float const& value1, float const& value2) const;
+
+ bool isConstant(float const& value) const;
+
+ private:
+ // The precision used for comparisons.
+ float precision;
+ };
+
+ // For doubles we specialize this class and consider the comparison modulo some predefined precision.
+ template<>
+ class ConstantsComparator<double> {
+ public:
+ ConstantsComparator();
+
+ ConstantsComparator(double precision);
+
+ bool isOne(double const& value) const;
+
+ bool isZero(double const& value) const;
+
+ bool isInfinity(double const& value) const;
+
+ bool isEqual(double const& value1, double const& value2) const;
+
+ bool isConstant(double const& value) const;
+
+ private:
+ // The precision used for comparisons.
+ double precision;
+ };
+
#ifdef STORM_HAVE_CARL
template<>
RationalFunction& simplify(RationalFunction& value);
template<>
RationalFunction&& simplify(RationalFunction&& value);
-
+
template<>
class ConstantsComparator<storm::RationalFunction> {
public:
+ ConstantsComparator();
+
bool isOne(storm::RationalFunction const& value) const;
bool isZero(storm::RationalFunction const& value) const;
@@ -81,6 +127,8 @@ namespace storm {
template<>
class ConstantsComparator<storm::Polynomial> {
public:
+ ConstantsComparator();
+
bool isOne(storm::Polynomial const& value) const;
bool isZero(storm::Polynomial const& value) const;
@@ -91,7 +139,6 @@ namespace storm {
};
#endif
-
template<typename ValueType>
bool ConstantsComparator<ValueType>::isOne(ValueType const& value) const {
return value == one<ValueType>();
@@ -183,6 +230,10 @@ namespace storm {
return std::move(value);
}
+ ConstantsComparator<storm::RationalFunction>::ConstantsComparator() {
+ // Intentionally left empty.
+ }
+
bool ConstantsComparator<storm::RationalFunction>::isOne(storm::RationalFunction const& value) const {
return value.isOne();
}
@@ -199,6 +250,10 @@ namespace storm {
return value.isConstant();
}
+ ConstantsComparator<storm::Polynomial>::ConstantsComparator() {
+ // Intentionally left empty.
+ }
+
bool ConstantsComparator<storm::Polynomial>::isOne(storm::Polynomial const& value) const {
return value.isOne();
}
diff --git a/src/utility/constants.h b/src/utility/constants.h
index c91ea9fdf..ae2b2c0be 100644
--- a/src/utility/constants.h
+++ b/src/utility/constants.h
@@ -41,6 +41,9 @@ namespace storm {
template<typename ValueType>
class ConstantsComparator {
public:
+ // This needs to be in here, otherwise the template specializations are not used properly.
+ ConstantsComparator();
+
bool isOne(ValueType const& value) const;
bool isZero(ValueType const& value) const;
@@ -52,50 +55,6 @@ namespace storm {
bool isInfinity(ValueType const& value) const;
};
- // For floats we specialize this class and consider the comparison modulo some predefined precision.
- template<>
- class ConstantsComparator<float> {
- public:
- ConstantsComparator();
-
- ConstantsComparator(float precision);
-
- bool isOne(float const& value) const;
-
- bool isZero(float const& value) const;
-
- bool isEqual(float const& value1, float const& value2) const;
-
- bool isConstant(float const& value) const;
-
- private:
- // The precision used for comparisons.
- float precision;
- };
-
- // For doubles we specialize this class and consider the comparison modulo some predefined precision.
- template<>
- class ConstantsComparator<double> {
- public:
- ConstantsComparator();
-
- ConstantsComparator(double precision);
-
- bool isOne(double const& value) const;
-
- bool isZero(double const& value) const;
-
- bool isInfinity(double const& value) const;
-
- bool isEqual(double const& value1, double const& value2) const;
-
- bool isConstant(double const& value) const;
-
- private:
- // The precision used for comparisons.
- double precision;
- };
-
template<typename IndexType, typename ValueType>
storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry);
diff --git a/src/utility/vector.h b/src/utility/vector.h
index 8d4548267..c695fa6d9 100644
--- a/src/utility/vector.h
+++ b/src/utility/vector.h
@@ -192,6 +192,44 @@ namespace storm {
}
}
+ /*!
+ * Applies the given operation pointwise on the two given vectors and writes the result to the third vector.
+ * To obtain an in-place operation, the third vector may be equal to any of the other two vectors.
+ *
+ * @param firstOperand The first operand.
+ * @param secondOperand The second operand.
+ * @param target The target vector.
+ */
+ template<class T>
+ void applyPointwise(std::vector<T> const& firstOperand, std::vector<T> const& secondOperand, std::vector<T>& target, std::function<T (T const&, T const&, T const&)> const& function) {
+#ifdef STORM_HAVE_INTELTBB
+ tbb::parallel_for(tbb::blocked_range<uint_fast64_t>(0, target.size()),
+ [&](tbb::blocked_range<uint_fast64_t> const& range) {
+ auto firstIt = firstOperand.begin() + range.begin();
+ auto firstIte = firstOperand.begin() + range.end();
+ auto secondIt = secondOperand.begin() + range.begin();
+ auto targetIt = target.begin() + range.begin();
+ while (firstIt != firstIte) {
+ *targetIt = function(*firstIt, *secondIt, *targetIt);
+ ++targetIt;
+ ++firstIt;
+ ++secondIt;
+ }
+ });
+#else
+ auto firstIt = firstOperand.begin();
+ auto firstIte = firstOperand.end();
+ auto secondIt = secondOperand.begin();
+ auto targetIt = target.begin();
+ while (firstIt != firstIte) {
+ *targetIt = function(*firstIt, *secondIt, *targetIt);
+ ++targetIt;
+ ++firstIt;
+ ++secondIt;
+ }
+#endif
+ }
+
/*!
* Applies the given operation pointwise on the two given vectors and writes the result to the third vector.
* To obtain an in-place operation, the third vector may be equal to any of the other two vectors.
diff --git a/test/functional/builder/DdPrismModelBuilderTest.cpp b/test/functional/builder/DdPrismModelBuilderTest.cpp
index 096d83fbf..4f9f8cbb5 100644
--- a/test/functional/builder/DdPrismModelBuilderTest.cpp
+++ b/test/functional/builder/DdPrismModelBuilderTest.cpp
@@ -4,7 +4,9 @@
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/GeneralSettings.h"
#include "src/models/symbolic/Dtmc.h"
+#include "src/models/symbolic/Ctmc.h"
#include "src/models/symbolic/Mdp.h"
+#include "src/models/symbolic/StandardRewardModel.h"
#include "src/storage/dd/CuddDd.h"
#include "src/storage/dd/CuddAdd.h"
#include "src/storage/dd/CuddBdd.h"
diff --git a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp
index 8c0a6e81e..3387f730d 100644
--- a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp
+++ b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp
@@ -1,5 +1,6 @@
#include "gtest/gtest.h"
#include "storm-config.h"
+#include "src/models/sparse/StandardRewardModel.h"
#include "src/settings/SettingMemento.h"
#include "src/parser/PrismParser.h"
#include "src/builder/ExplicitPrismModelBuilder.h"
diff --git a/test/functional/builder/cluster2.sm b/test/functional/builder/cluster2.sm
index 5afd88f47..80b1085df 100644
--- a/test/functional/builder/cluster2.sm
+++ b/test/functional/builder/cluster2.sm
@@ -97,14 +97,14 @@ label "premium" = (left_n>=left_mx & toleft_n) | (right_n>=right_mx & toright_n)
// Reward structures
// Percentage of operational workstations stations
-rewards "percent_op"
- true : 100*(left_n+right_n)/(2*N);
-endrewards
+//rewards "percent_op"
+// true : 100*(left_n+right_n)/(2*N);
+//endrewards
// Time that the system is not delivering at least minimum QoS
-rewards "time_not_min"
- !minimum : 1;
-endrewards
+//rewards "time_not_min"
+// !minimum : 1;
+//endrewards
// Number of repairs
rewards "num_repairs"
diff --git a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
index c0ad1325b..d7d1b2524 100644
--- a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
@@ -3,6 +3,7 @@
#include "src/logic/Formulas.h"
#include "src/utility/solver.h"
+#include "src/models/sparse/StandardRewardModel.h"
#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "src/settings/SettingsManager.h"
diff --git a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
index b8cbcd701..5cc56d0ed 100644
--- a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
@@ -10,6 +10,7 @@
#include "src/parser/PrismParser.h"
#include "src/builder/DdPrismModelBuilder.h"
#include "src/models/symbolic/Dtmc.h"
+#include "src/models/symbolic/StandardRewardModel.h"
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/GeneralSettings.h"
#include "src/settings/modules/GmmxxEquationSolverSettings.h"
diff --git a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
index 945d4bc6f..8162d0a5c 100644
--- a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
@@ -11,6 +11,7 @@
#include "src/parser/FormulaParser.h"
#include "src/builder/DdPrismModelBuilder.h"
#include "src/models/symbolic/Dtmc.h"
+#include "src/models/symbolic/StandardRewardModel.h"
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/GeneralSettings.h"
diff --git a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
index 5dc655e56..73541f562 100644
--- a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
@@ -4,6 +4,7 @@
#include "src/parser/FormulaParser.h"
#include "src/logic/Formulas.h"
#include "src/utility/solver.h"
+#include "src/models/sparse/StandardRewardModel.h"
#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "src/settings/SettingsManager.h"
diff --git a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
index adb100e27..ebfc2bbe6 100644
--- a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
+++ b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
@@ -14,7 +14,7 @@
#include "src/settings/modules/GeneralSettings.h"
-TEST(SparseCtmcCslModelCheckerTest, Cluster) {
+TEST(NativeCtmcCslModelCheckerTest, Cluster) {
// Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true);
@@ -90,7 +90,7 @@ TEST(SparseCtmcCslModelCheckerTest, Cluster) {
EXPECT_NEAR(0.8602815057967503, quantitativeCheckResult7[initialState], storm::settings::generalSettings().getPrecision());
}
-TEST(SparseCtmcCslModelCheckerTest, Embedded) {
+TEST(NativeCtmcCslModelCheckerTest, Embedded) {
// Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true);
@@ -152,7 +152,7 @@ TEST(SparseCtmcCslModelCheckerTest, Embedded) {
EXPECT_NEAR(2.7745274082080154, quantitativeCheckResult5[initialState], storm::settings::generalSettings().getPrecision());
}
-TEST(SparseCtmcCslModelCheckerTest, Polling) {
+TEST(NativeCtmcCslModelCheckerTest, Polling) {
// Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true);
@@ -179,14 +179,14 @@ TEST(SparseCtmcCslModelCheckerTest, Polling) {
EXPECT_NEAR(1, quantitativeCheckResult1[initialState], storm::settings::generalSettings().getPrecision());
}
-TEST(SparseCtmcCslModelCheckerTest, Fms) {
+TEST(NativeCtmcCslModelCheckerTest, Fms) {
// Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true);
// No properties to check at this point.
}
-TEST(SparseCtmcCslModelCheckerTest, Tandem) {
+TEST(NativeCtmcCslModelCheckerTest, Tandem) {
// Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true);
diff --git a/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
index 9b6a4aa00..c9730e795 100644
--- a/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
@@ -4,6 +4,7 @@
#include "src/settings/SettingMemento.h"
#include "src/logic/Formulas.h"
#include "src/utility/solver.h"
+#include "src/models/sparse/StandardRewardModel.h"
#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "src/settings/SettingsManager.h"
diff --git a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
index 2a0d8cd7b..688fa8a16 100644
--- a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
@@ -9,6 +9,7 @@
#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
#include "src/parser/PrismParser.h"
#include "src/builder/DdPrismModelBuilder.h"
+#include "src/models/symbolic/StandardRewardModel.h"
#include "src/models/symbolic/Dtmc.h"
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/GeneralSettings.h"
diff --git a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
index 4918451b7..5b67f31e2 100644
--- a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
@@ -11,6 +11,7 @@
#include "src/parser/PrismParser.h"
#include "src/builder/DdPrismModelBuilder.h"
#include "src/models/symbolic/Dtmc.h"
+#include "src/models/symbolic/StandardRewardModel.h"
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/GeneralSettings.h"
diff --git a/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
index 648bdd037..e4123495a 100644
--- a/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
@@ -4,6 +4,7 @@
#include "src/parser/FormulaParser.h"
#include "src/logic/Formulas.h"
#include "src/utility/solver.h"
+#include "src/models/sparse/StandardRewardModel.h"
#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "src/settings/SettingsManager.h"
diff --git a/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp b/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp
index 86b4494f8..d660862ec 100644
--- a/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp
+++ b/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp
@@ -2,6 +2,7 @@
#include "storm-config.h"
#include "src/logic/Formulas.h"
+#include "src/models/sparse/StandardRewardModel.h"
#include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "src/settings/SettingsManager.h"
diff --git a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
index 574f1752c..1b1071a58 100644
--- a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
@@ -8,6 +8,7 @@
#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
#include "src/parser/PrismParser.h"
#include "src/builder/DdPrismModelBuilder.h"
+#include "src/models/symbolic/StandardRewardModel.h"
#include "src/models/symbolic/Dtmc.h"
#include "src/settings/SettingsManager.h"
diff --git a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
index 159568433..e07c04e20 100644
--- a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
@@ -4,6 +4,7 @@
#include "src/parser/FormulaParser.h"
#include "src/logic/Formulas.h"
#include "src/utility/solver.h"
+#include "src/models/sparse/StandardRewardModel.h"
#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "src/settings/SettingsManager.h"
diff --git a/test/functional/parser/AutoParserTest.cpp b/test/functional/parser/AutoParserTest.cpp
index c3d8e0082..dd4ff7286 100644
--- a/test/functional/parser/AutoParserTest.cpp
+++ b/test/functional/parser/AutoParserTest.cpp
@@ -1,6 +1,7 @@
#include "gtest/gtest.h"
#include "storm-config.h"
+#include "src/models/sparse/StandardRewardModel.h"
#include "src/parser/AutoParser.h"
#include "src/exceptions/FileIoException.h"
#include "src/exceptions/WrongFormatException.h"
diff --git a/test/functional/parser/DeterministicModelParserTest.cpp b/test/functional/parser/DeterministicModelParserTest.cpp
index 154b06114..d8c23f2f1 100644
--- a/test/functional/parser/DeterministicModelParserTest.cpp
+++ b/test/functional/parser/DeterministicModelParserTest.cpp
@@ -1,6 +1,7 @@
#include "gtest/gtest.h"
#include "storm-config.h"
+#include "src/models/sparse/StandardRewardModel.h"
#include "src/parser/DeterministicModelParser.h"
#include "src/models/sparse/Dtmc.h"
#include "src/models/sparse/Ctmc.h"
diff --git a/test/functional/parser/MarkovAutomatonParserTest.cpp b/test/functional/parser/MarkovAutomatonParserTest.cpp
index 9152dab08..a9f0552fe 100644
--- a/test/functional/parser/MarkovAutomatonParserTest.cpp
+++ b/test/functional/parser/MarkovAutomatonParserTest.cpp
@@ -2,6 +2,7 @@
#include "storm-config.h"
#include "src/parser/MarkovAutomatonParser.h"
+#include "src/models/sparse/StandardRewardModel.h"
#include "src/exceptions/FileIoException.h"
#include "src/exceptions/OutOfRangeException.h"
diff --git a/test/functional/parser/NondeterministicModelParserTest.cpp b/test/functional/parser/NondeterministicModelParserTest.cpp
index 7f956d06f..9beda9450 100644
--- a/test/functional/parser/NondeterministicModelParserTest.cpp
+++ b/test/functional/parser/NondeterministicModelParserTest.cpp
@@ -3,6 +3,7 @@
#include "src/parser/NondeterministicModelParser.h"
#include "src/models/sparse/Mdp.h"
+#include "src/models/sparse/StandardRewardModel.h"
#include "src/exceptions/FileIoException.h"
#include "src/exceptions/OutOfRangeException.h"
diff --git a/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp b/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp
index 23b3a6be6..a995bbea0 100644
--- a/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp
+++ b/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp
@@ -1,7 +1,8 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include "src/parser/AutoParser.h"
-#include "storage/DeterministicModelBisimulationDecomposition.h"
+#include "src/storage/DeterministicModelBisimulationDecomposition.h"
+#include "src/models/sparse/StandardRewardModel.h"
TEST(DeterministicModelBisimulationDecomposition, Die) {
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", "");
diff --git a/test/functional/storage/MaximalEndComponentDecompositionTest.cpp b/test/functional/storage/MaximalEndComponentDecompositionTest.cpp
index ea3b2826e..0cbac96c1 100644
--- a/test/functional/storage/MaximalEndComponentDecompositionTest.cpp
+++ b/test/functional/storage/MaximalEndComponentDecompositionTest.cpp
@@ -3,6 +3,7 @@
#include "src/parser/AutoParser.h"
#include "src/storage/MaximalEndComponentDecomposition.h"
#include "src/models/sparse/MarkovAutomaton.h"
+#include "src/models/sparse/StandardRewardModel.h"
TEST(MaximalEndComponentDecomposition, FullSystem1) {
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.lab", "", "");
diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp
index 2d4d7615d..d58de5ca9 100644
--- a/test/functional/utility/GraphTest.cpp
+++ b/test/functional/utility/GraphTest.cpp
@@ -5,8 +5,10 @@
#include "src/parser/PrismParser.h"
#include "src/models/symbolic/Dtmc.h"
#include "src/models/symbolic/Mdp.h"
+#include "src/models/symbolic/StandardRewardModel.h"
#include "src/models/sparse/Dtmc.h"
#include "src/models/sparse/Mdp.h"
+#include "src/models/sparse/StandardRewardModel.h"
#include "src/builder/DdPrismModelBuilder.h"
#include "src/builder/ExplicitPrismModelBuilder.h"
#include "src/utility/graph.h"