From ebe6775b279fbecd1fb1281c97dab0f9bc7785df Mon Sep 17 00:00:00 2001
From: hbruintjes <h.bruintjes@cs.rwth-aachen.de>
Date: Fri, 1 Jul 2016 10:45:08 +0200
Subject: [PATCH] Fix missing ValueType template arguments (which defaulted to
double)
Former-commit-id: a97910eaf929907bd2ba6e1c70c727bb62875566
---
src/builder/DdPrismModelBuilder.cpp | 25 ++++++++-----------
src/builder/DdPrismModelBuilder.h | 2 +-
src/models/symbolic/Ctmc.cpp | 2 +-
src/models/symbolic/DeterministicModel.cpp | 4 +--
src/models/symbolic/Dtmc.cpp | 2 +-
src/models/symbolic/Mdp.cpp | 2 +-
src/models/symbolic/Model.cpp | 2 +-
src/models/symbolic/StandardRewardModel.cpp | 2 +-
src/storage/dd/Add.cpp | 2 +-
src/storage/dd/cudd/InternalCuddAdd.cpp | 2 +-
src/storage/dd/cudd/InternalCuddDdManager.cpp | 2 +-
11 files changed, 22 insertions(+), 25 deletions(-)
diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp
index 2af7fed58..a397b0de0 100644
--- a/src/builder/DdPrismModelBuilder.cpp
+++ b/src/builder/DdPrismModelBuilder.cpp
@@ -32,12 +32,9 @@ namespace storm {
template <storm::dd::DdType Type, typename ValueType>
class DdPrismModelBuilder<Type, ValueType>::GenerationInformation {
public:
- GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared<storm::dd::DdManager<Type>>()), rowMetaVariables(), variableToRowMetaVariableMap(std::make_shared<std::map<storm::expressions::Variable, storm::expressions::Variable>>()), rowExpressionAdapter(std::make_shared<storm::adapters::AddExpressionAdapter<Type>>(manager, variableToRowMetaVariableMap)), columnMetaVariables(), variableToColumnMetaVariableMap((std::make_shared<std::map<storm::expressions::Variable, storm::expressions::Variable>>())), columnExpressionAdapter(std::make_shared<storm::adapters::AddExpressionAdapter<Type>>(manager, variableToColumnMetaVariableMap)), rowColumnMetaVariablePairs(), nondeterminismMetaVariables(), variableToIdentityMap(), allGlobalVariables(), moduleToIdentityMap() {
+ GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared<storm::dd::DdManager<Type>>()), rowMetaVariables(), variableToRowMetaVariableMap(std::make_shared<std::map<storm::expressions::Variable, storm::expressions::Variable>>()), rowExpressionAdapter(std::make_shared<storm::adapters::AddExpressionAdapter<Type, ValueType>>(manager, variableToRowMetaVariableMap)), columnMetaVariables(), variableToColumnMetaVariableMap((std::make_shared<std::map<storm::expressions::Variable, storm::expressions::Variable>>())), columnExpressionAdapter(std::make_shared<storm::adapters::AddExpressionAdapter<Type, ValueType>>(manager, variableToColumnMetaVariableMap)), rowColumnMetaVariablePairs(), nondeterminismMetaVariables(), variableToIdentityMap(), allGlobalVariables(), moduleToIdentityMap() {
// Initializes variables and identity DDs.
createMetaVariablesAndIdentities();
-
- rowExpressionAdapter = std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>>(new storm::adapters::AddExpressionAdapter<Type>(manager, variableToRowMetaVariableMap));
- columnExpressionAdapter = std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>>(new storm::adapters::AddExpressionAdapter<Type>(manager, variableToColumnMetaVariableMap));
}
// The program that is currently translated.
@@ -49,12 +46,12 @@ namespace storm {
// The meta variables for the row encoding.
std::set<storm::expressions::Variable> rowMetaVariables;
std::shared_ptr<std::map<storm::expressions::Variable, storm::expressions::Variable>> variableToRowMetaVariableMap;
- std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>> rowExpressionAdapter;
+ std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> rowExpressionAdapter;
// The meta variables for the column encoding.
std::set<storm::expressions::Variable> columnMetaVariables;
std::shared_ptr<std::map<storm::expressions::Variable, storm::expressions::Variable>> variableToColumnMetaVariableMap;
- std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>> columnExpressionAdapter;
+ std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> columnExpressionAdapter;
// All pairs of row/column meta variables.
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> rowColumnMetaVariablePairs;
@@ -794,7 +791,7 @@ namespace storm {
}
}
- result.setValue(metaVariableNameToValueMap, 1);
+ result.setValue(metaVariableNameToValueMap, ValueType(1));
return result;
}
@@ -835,7 +832,7 @@ namespace storm {
for (uint_fast64_t currentChoices = 1; currentChoices <= maxChoices; ++currentChoices) {
// Determine the set of states with exactly currentChoices choices.
- equalsNumberOfChoicesDd = sumOfGuards.equals(generationInfo.manager->getConstant(static_cast<double>(currentChoices)));
+ equalsNumberOfChoicesDd = sumOfGuards.equals(generationInfo.manager->getConstant(ValueType(currentChoices)));
// If there is no such state, continue with the next possible number of choices.
if (equalsNumberOfChoicesDd.isZero()) {
@@ -1110,7 +1107,7 @@ namespace storm {
}
template <storm::dd::DdType Type, typename ValueType>
- storm::models::symbolic::StandardRewardModel<Type, double> DdPrismModelBuilder<Type, ValueType>::createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add<Type, ValueType> const& transitionMatrix, storm::dd::Add<Type, ValueType> const& reachableStatesAdd, storm::dd::Add<Type, ValueType> const& stateActionDd) {
+ storm::models::symbolic::StandardRewardModel<Type, ValueType> DdPrismModelBuilder<Type, ValueType>::createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add<Type, ValueType> const& transitionMatrix, storm::dd::Add<Type, ValueType> const& reachableStatesAdd, storm::dd::Add<Type, ValueType> const& stateActionDd) {
// Start by creating the state reward vector.
boost::optional<storm::dd::Add<Type, ValueType>> stateRewards;
@@ -1222,7 +1219,7 @@ namespace storm {
}
}
- return storm::models::symbolic::StandardRewardModel<Type, double>(stateRewards, stateActionRewards, transitionRewards);
+ return storm::models::symbolic::StandardRewardModel<Type, ValueType>(stateRewards, stateActionRewards, transitionRewards);
}
template <storm::dd::DdType Type, typename ValueType>
@@ -1394,7 +1391,7 @@ namespace storm {
selectedRewardModels.push_back(preparedProgram->getRewardModel(0));
}
- std::unordered_map<std::string, storm::models::symbolic::StandardRewardModel<Type, double>> rewardModels;
+ std::unordered_map<std::string, storm::models::symbolic::StandardRewardModel<Type, ValueType>> rewardModels;
for (auto const& rewardModel : selectedRewardModels) {
rewardModels.emplace(rewardModel.get().getName(), createRewardModelDecisionDiagrams(generationInfo, rewardModel.get(), globalModule, transitionMatrix, reachableStatesAdd, stateActionDd));
}
@@ -1406,11 +1403,11 @@ namespace storm {
}
if (program.getModelType() == storm::prism::Program::ModelType::DTMC) {
- return std::shared_ptr<storm::models::symbolic::Model<Type>>(new storm::models::symbolic::Dtmc<Type>(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels));
+ return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Dtmc<Type, ValueType>(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels));
} else if (program.getModelType() == storm::prism::Program::ModelType::CTMC) {
- return std::shared_ptr<storm::models::symbolic::Model<Type>>(new storm::models::symbolic::Ctmc<Type>(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels));
+ return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Ctmc<Type, ValueType>(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels));
} else if (program.getModelType() == storm::prism::Program::ModelType::MDP) {
- return std::shared_ptr<storm::models::symbolic::Model<Type>>(new storm::models::symbolic::Mdp<Type>(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, generationInfo.allNondeterminismVariables, labelToExpressionMapping, rewardModels));
+ return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Mdp<Type, ValueType>(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, generationInfo.allNondeterminismVariables, labelToExpressionMapping, rewardModels));
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid model type.");
}
diff --git a/src/builder/DdPrismModelBuilder.h b/src/builder/DdPrismModelBuilder.h
index 0cb8cc6fd..6db0c4639 100644
--- a/src/builder/DdPrismModelBuilder.h
+++ b/src/builder/DdPrismModelBuilder.h
@@ -238,7 +238,7 @@ namespace storm {
static storm::dd::Add<Type, ValueType> 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, ValueType> const& transitionMatrix, storm::dd::Add<Type, ValueType> const& reachableStatesAdd, storm::dd::Add<Type, ValueType> const& stateActionDd);
+ static storm::models::symbolic::StandardRewardModel<Type, ValueType> createRewardModelDecisionDiagrams(GenerationInformation& generationInfo, storm::prism::RewardModel const& rewardModel, ModuleDecisionDiagram const& globalModule, storm::dd::Add<Type, ValueType> const& transitionMatrix, storm::dd::Add<Type, ValueType> const& reachableStatesAdd, storm::dd::Add<Type, ValueType> const& stateActionDd);
static SystemResult createSystemDecisionDiagram(GenerationInformation& generationInfo);
diff --git a/src/models/symbolic/Ctmc.cpp b/src/models/symbolic/Ctmc.cpp
index 2f1e65aec..1c612d090 100644
--- a/src/models/symbolic/Ctmc.cpp
+++ b/src/models/symbolic/Ctmc.cpp
@@ -23,7 +23,7 @@ namespace storm {
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
std::map<std::string, storm::expressions::Expression> labelToExpressionMap,
std::unordered_map<std::string, RewardModelType> const& rewardModels)
- : DeterministicModel<Type>(storm::models::ModelType::Ctmc, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) {
+ : DeterministicModel<Type, ValueType>(storm::models::ModelType::Ctmc, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) {
exitRates = this->getTransitionMatrix().sumAbstract(this->getColumnVariables());
}
diff --git a/src/models/symbolic/DeterministicModel.cpp b/src/models/symbolic/DeterministicModel.cpp
index 66f97bc87..6824357d6 100644
--- a/src/models/symbolic/DeterministicModel.cpp
+++ b/src/models/symbolic/DeterministicModel.cpp
@@ -24,7 +24,7 @@ namespace storm {
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
std::map<std::string, storm::expressions::Expression> labelToExpressionMap,
std::unordered_map<std::string, RewardModelType> const& rewardModels)
- : Model<Type>(modelType, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) {
+ : Model<Type, ValueType>(modelType, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) {
// Intentionally left empty.
}
@@ -34,4 +34,4 @@ namespace storm {
} // namespace symbolic
} // namespace models
-} // namespace storm
\ No newline at end of file
+} // namespace storm
diff --git a/src/models/symbolic/Dtmc.cpp b/src/models/symbolic/Dtmc.cpp
index a9483862f..6f63ff394 100644
--- a/src/models/symbolic/Dtmc.cpp
+++ b/src/models/symbolic/Dtmc.cpp
@@ -33,4 +33,4 @@ namespace storm {
} // namespace symbolic
} // namespace models
-} // namespace storm
\ No newline at end of file
+} // namespace storm
diff --git a/src/models/symbolic/Mdp.cpp b/src/models/symbolic/Mdp.cpp
index 70017195a..f438e6f1d 100644
--- a/src/models/symbolic/Mdp.cpp
+++ b/src/models/symbolic/Mdp.cpp
@@ -34,4 +34,4 @@ namespace storm {
} // namespace symbolic
} // namespace models
-} // namespace storm
\ No newline at end of file
+} // namespace storm
diff --git a/src/models/symbolic/Model.cpp b/src/models/symbolic/Model.cpp
index 25bc5404b..16339c0d1 100644
--- a/src/models/symbolic/Model.cpp
+++ b/src/models/symbolic/Model.cpp
@@ -249,4 +249,4 @@ namespace storm {
} // namespace symbolic
} // namespace models
-} // namespace storm
\ No newline at end of file
+} // namespace storm
diff --git a/src/models/symbolic/StandardRewardModel.cpp b/src/models/symbolic/StandardRewardModel.cpp
index 4ec405405..1342abb3d 100644
--- a/src/models/symbolic/StandardRewardModel.cpp
+++ b/src/models/symbolic/StandardRewardModel.cpp
@@ -155,4 +155,4 @@ namespace storm {
template class StandardRewardModel<storm::dd::DdType::Sylvan, double>;
}
}
-}
\ No newline at end of file
+}
diff --git a/src/storage/dd/Add.cpp b/src/storage/dd/Add.cpp
index bcff0e3da..a6cb3daac 100644
--- a/src/storage/dd/Add.cpp
+++ b/src/storage/dd/Add.cpp
@@ -767,4 +767,4 @@ namespace storm {
template class Add<storm::dd::DdType::Sylvan, double>;
template class Add<storm::dd::DdType::Sylvan, uint_fast64_t>;
}
-}
\ No newline at end of file
+}
diff --git a/src/storage/dd/cudd/InternalCuddAdd.cpp b/src/storage/dd/cudd/InternalCuddAdd.cpp
index 0925b4f58..393e8d262 100644
--- a/src/storage/dd/cudd/InternalCuddAdd.cpp
+++ b/src/storage/dd/cudd/InternalCuddAdd.cpp
@@ -596,4 +596,4 @@ namespace storm {
template class InternalAdd<DdType::CUDD, double>;
template class InternalAdd<DdType::CUDD, uint_fast64_t>;
}
-}
\ No newline at end of file
+}
diff --git a/src/storage/dd/cudd/InternalCuddDdManager.cpp b/src/storage/dd/cudd/InternalCuddDdManager.cpp
index 9f33c803d..5fc5ebcd0 100644
--- a/src/storage/dd/cudd/InternalCuddDdManager.cpp
+++ b/src/storage/dd/cudd/InternalCuddDdManager.cpp
@@ -106,4 +106,4 @@ namespace storm {
template InternalAdd<DdType::CUDD, double> InternalDdManager<DdType::CUDD>::getConstant(double const& value) const;
template InternalAdd<DdType::CUDD, uint_fast64_t> InternalDdManager<DdType::CUDD>::getConstant(uint_fast64_t const& value) const;
}
-}
\ No newline at end of file
+}