From 1c7f5dae56848fc75f139dd39a50b2a6690574a3 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 26 Jan 2016 18:34:33 +0100
Subject: [PATCH 1/2] fixed a bug pointed out by Matthias
Former-commit-id: 0a4355c5804b6febbdaf2783465a9776730dfd8b
---
src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp | 4 ----
1 file changed, 4 deletions(-)
diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
index 564b635bc..5043c8296 100644
--- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
+++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
@@ -262,10 +262,6 @@ namespace storm {
if (startingIteration == 0) {
result = values;
storm::utility::vector::scaleVectorInPlace(result, std::get<3>(foxGlynnResult)[0]);
- std::function<ValueType(ValueType const&, ValueType const&)> addAndScale = [&foxGlynnResult] (ValueType const& a, ValueType const& b) { return a + std::get<3>(foxGlynnResult)[0] * b; };
- if (addVector != nullptr) {
- storm::utility::vector::applyPointwise(result, *addVector, result, addAndScale);
- }
++startingIteration;
} else {
if (computeCumulativeReward) {
From 95c37244a2925a99bed6836c754233bd575f6343 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Tue, 26 Jan 2016 20:22:52 +0100
Subject: [PATCH 2/2] reduced complexity of bisimulation and preprocess call
Former-commit-id: fb6f002af164b40a5f69a170486488e98f3a3832
---
src/models/symbolic/Model.h | 4 +++-
src/utility/storm.h | 27 +++++++++++++++------------
2 files changed, 18 insertions(+), 13 deletions(-)
diff --git a/src/models/symbolic/Model.h b/src/models/symbolic/Model.h
index 3b8804ebe..085c5075f 100644
--- a/src/models/symbolic/Model.h
+++ b/src/models/symbolic/Model.h
@@ -43,9 +43,11 @@ namespace storm {
/*!
* Base class for all symbolic models.
*/
- template<storm::dd::DdType Type, typename ValueType = double>
+ template<storm::dd::DdType Type, typename CValueType = double>
class Model : public storm::models::ModelBase {
public:
+ typedef CValueType ValueType;
+
static const storm::dd::DdType DdType = Type;
typedef StandardRewardModel<Type, ValueType> RewardModelType;
diff --git a/src/utility/storm.h b/src/utility/storm.h
index fb96b7420..701caa634 100644
--- a/src/utility/storm.h
+++ b/src/utility/storm.h
@@ -85,7 +85,6 @@ namespace storm {
std::vector<std::shared_ptr<storm::logic::Formula>> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program);
-
template<typename ValueType, storm::dd::DdType LibraryType = storm::dd::DdType::CUDD>
storm::storage::ModelFormulasPair buildSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
storm::storage::ModelFormulasPair result;
@@ -169,8 +168,10 @@ namespace storm {
return model;
}
- template<typename ModelType, typename ValueType = typename ModelType::ValueType, typename std::enable_if<std::is_base_of<storm::models::sparse::Model<ValueType>, ModelType>::value, bool>::type = 0>
- std::shared_ptr<storm::models::ModelBase> performBisimulationMinimization(std::shared_ptr<ModelType> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas, storm::storage::BisimulationType type) {
+ template<typename ModelType>
+ std::shared_ptr<storm::models::sparse::Model<typename ModelType::ValueType>> performBisimulationMinimization(std::shared_ptr<storm::models::sparse::Model<typename ModelType::ValueType>> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas, storm::storage::BisimulationType type) {
+ using ValueType = typename ModelType::ValueType;
+
STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for DTMCs, CTMCs and MDPs.");
model->reduceToStateBasedRewards();
@@ -183,25 +184,27 @@ namespace storm {
}
}
- template<typename ModelType, typename ValueType = typename ModelType::ValueType, typename std::enable_if<std::is_base_of<storm::models::sparse::Model<ValueType>, ModelType>::value, bool>::type = 0>
- std::shared_ptr<storm::models::ModelBase> preprocessModel(std::shared_ptr<ModelType> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
- if (storm::settings::generalSettings().isBisimulationSet()) {
+ template<typename ModelType>
+ std::shared_ptr<storm::models::sparse::Model<typename ModelType::ValueType>> performBisimulationMinimization(std::shared_ptr<storm::models::sparse::Model<typename ModelType::ValueType>> model, std::shared_ptr<storm::logic::Formula> const& formula, storm::storage::BisimulationType type) {
+ return performBisimulationMinimization(model, {formula}, type);
+ }
+
+
+
+ template<typename ModelType>
+ std::shared_ptr<storm::models::ModelBase> preprocessModel(std::shared_ptr<storm::models::ModelBase> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
+ if (model->isSparseModel() && storm::settings::generalSettings().isBisimulationSet()) {
storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong;
if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) {
bisimType = storm::storage::BisimulationType::Weak;
}
STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for sparse models.");
- return performBisimulationMinimization(model, formulas, bisimType);
+ return performBisimulationMinimization<ModelType>(model->template as<storm::models::sparse::Model<typename ModelType::ValueType>>(), formulas, bisimType);
}
return model;
}
- template<typename ModelType, storm::dd::DdType DdType = ModelType::DdType, typename std::enable_if< std::is_base_of< storm::models::symbolic::Model<DdType>, ModelType >::value, bool>::type = 0>
- std::shared_ptr<storm::models::ModelBase> preprocessModel(std::shared_ptr<ModelType> model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
- // No preprocessing available yet.
- return model;
- }
template<typename ValueType>
void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::shared_ptr<storm::logic::Formula> const& formula) {