From 17ba53dafad8bf2a343d3cfc715d09507baf2090 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Mon, 20 Jun 2016 11:39:14 +0200
Subject: [PATCH 1/6] Division by Interval not supported
Former-commit-id: 86b2f555c94c49514141b57f882f6bd9d7d74da6
---
src/storage/SparseMatrix.cpp | 12 ++++++++++++
1 file changed, 12 insertions(+)
diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp
index bfed8f49c..35f4712d3 100644
--- a/src/storage/SparseMatrix.cpp
+++ b/src/storage/SparseMatrix.cpp
@@ -1018,6 +1018,11 @@ namespace storm {
typename std::pair<storm::storage::SparseMatrix<RationalFunction>, std::vector<RationalFunction>> SparseMatrix<RationalFunction>::getJacobiDecomposition() const {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This operation is not supported.");
}
+
+ template<>
+ typename std::pair<storm::storage::SparseMatrix<Interval>, std::vector<Interval>> SparseMatrix<Interval>::getJacobiDecomposition() const {
+ STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This operation is not supported.");
+ }
#endif
template<typename ValueType>
@@ -1143,6 +1148,13 @@ namespace storm {
++currentRow;
}
}
+
+#ifdef STORM_HAVE_CARL
+ template<>
+ void SparseMatrix<Interval>::performSuccessiveOverRelaxationStep(Interval omega, std::vector<Interval>& x, std::vector<Interval> const& b) const {
+ STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This operation is not supported.");
+ }
+#endif
template<typename ValueType>
void SparseMatrix<ValueType>::multiplyVectorWithMatrix(std::vector<value_type> const& vector, std::vector<value_type>& result) const {
From dcf5468b295de2b9f901edf9301050331af473bc Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Mon, 20 Jun 2016 11:40:07 +0200
Subject: [PATCH 2/6] Fixed linker error with static function
Former-commit-id: 95e220763d537009605c3676e857472ee9ace018
---
src/adapters/EigenAdapter.cpp | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/adapters/EigenAdapter.cpp b/src/adapters/EigenAdapter.cpp
index aebdcd0ef..eb2199945 100644
--- a/src/adapters/EigenAdapter.cpp
+++ b/src/adapters/EigenAdapter.cpp
@@ -4,7 +4,7 @@ namespace storm {
namespace adapters {
template<typename ValueType>
- static std::unique_ptr<Eigen::SparseMatrix<ValueType>> toEigenSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix) {
+ std::unique_ptr<Eigen::SparseMatrix<ValueType>> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix) {
// Build a list of triplets and let Eigen care about the insertion.
std::vector<Eigen::Triplet<ValueType>> triplets;
triplets.reserve(matrix.getNonzeroEntryCount());
@@ -20,6 +20,6 @@ namespace storm {
return result;
}
- template std::unique_ptr<Eigen::SparseMatrix<double>> toEigenSparseMatrix(storm::storage::SparseMatrix<double> const& matrix);
+ template std::unique_ptr<Eigen::SparseMatrix<double>> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix<double> const& matrix);
}
-}
\ No newline at end of file
+}
From be9648fc1818f819cabd375a078fa165ad520efa Mon Sep 17 00:00:00 2001
From: PBerger <philipp.berger@rwth-aachen.de>
Date: Tue, 21 Jun 2016 03:03:52 +0200
Subject: [PATCH 3/6] Added -fPIC to Sylvan. Since it is linked into Storm it
is necessary for relocation to be possible, hence PIC. Added includes for
cmath at various points. This is a default include on Mac OS but not on any
sane systems. Changed calls to std::abs to std::fabs to resolve ambigious
call errors.
Former-commit-id: 4d3da21bce54063f79a275249f6e8fac5b59ecb4
---
resources/3rdparty/sylvan/CMakeLists.txt | 4 ++--
src/generator/VariableInformation.cpp | 4 +++-
src/solver/GlpkLpSolver.cpp | 9 ++++++---
src/storage/dd/DdManager.cpp | 4 +++-
src/storage/dd/cudd/CuddAddIterator.cpp | 4 +++-
src/storage/dd/sylvan/SylvanAddIterator.cpp | 4 +++-
6 files changed, 20 insertions(+), 9 deletions(-)
diff --git a/resources/3rdparty/sylvan/CMakeLists.txt b/resources/3rdparty/sylvan/CMakeLists.txt
index 27762655b..d9999a0f3 100644
--- a/resources/3rdparty/sylvan/CMakeLists.txt
+++ b/resources/3rdparty/sylvan/CMakeLists.txt
@@ -2,8 +2,8 @@ cmake_minimum_required(VERSION 2.6)
project(sylvan C CXX)
enable_testing()
-set(CMAKE_C_FLAGS "-O3 -Wextra -Wall -Werror -fno-strict-aliasing -std=gnu11")
-set(CMAKE_CXX_FLAGS "-O3 -Wextra -Wall -Werror -fno-strict-aliasing -Wno-deprecated-register -std=gnu++11")
+set(CMAKE_C_FLAGS "-O3 -Wextra -Wall -Werror -fno-strict-aliasing -std=gnu11 -fPIC")
+set(CMAKE_CXX_FLAGS "-O3 -Wextra -Wall -Werror -fno-strict-aliasing -Wno-deprecated-register -std=gnu++11 -fPIC")
option(WITH_COVERAGE "Add generation of test coverage" OFF)
if(WITH_COVERAGE)
diff --git a/src/generator/VariableInformation.cpp b/src/generator/VariableInformation.cpp
index a5be93a6e..42f924beb 100644
--- a/src/generator/VariableInformation.cpp
+++ b/src/generator/VariableInformation.cpp
@@ -3,6 +3,8 @@
#include "src/utility/macros.h"
#include "src/exceptions/InvalidArgumentException.h"
+#include <cmath>
+
namespace storm {
namespace generator {
@@ -74,4 +76,4 @@ namespace storm {
}
}
-}
\ No newline at end of file
+}
diff --git a/src/solver/GlpkLpSolver.cpp b/src/solver/GlpkLpSolver.cpp
index bcf296865..bc7d72a00 100644
--- a/src/solver/GlpkLpSolver.cpp
+++ b/src/solver/GlpkLpSolver.cpp
@@ -17,6 +17,9 @@
#include "src/settings/modules/DebugSettings.h"
#include "src/settings/modules/GlpkSettings.h"
+
+#include <cmath>
+
namespace storm {
namespace solver {
GlpkLpSolver::GlpkLpSolver(std::string const& name, OptimizationDirection const& optDir) : LpSolver(optDir), lp(nullptr), variableToIndexMap(), nextVariableIndex(1), nextConstraintIndex(1), modelContainsIntegerVariables(false), isInfeasibleFlag(false), isUnboundedFlag(false), rowIndices(), columnIndices(), coefficientValues() {
@@ -298,7 +301,7 @@ namespace storm {
}
// Now check the desired precision was actually achieved.
- STORM_LOG_THROW(std::abs(static_cast<int>(value) - value) <= storm::settings::getModule<storm::settings::modules::GlpkSettings>().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in glpk solution (" << value << ").");
+ STORM_LOG_THROW(std::fabs(static_cast<int>(value) - value) <= storm::settings::getModule<storm::settings::modules::GlpkSettings>().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for integer variable in glpk solution (" << value << ").");
return static_cast<int_fast64_t>(value);
}
@@ -320,7 +323,7 @@ namespace storm {
value = glp_get_col_prim(this->lp, static_cast<int>(variableIndexPair->second));
}
- STORM_LOG_THROW(std::abs(static_cast<int>(value) - value) <= storm::settings::getModule<storm::settings::modules::GlpkSettings>().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for binary variable in glpk solution (" << value << ").");
+ STORM_LOG_THROW(std::fabs(static_cast<int>(value) - value) <= storm::settings::getModule<storm::settings::modules::GlpkSettings>().getIntegerTolerance(), storm::exceptions::InvalidStateException, "Illegal value for binary variable in glpk solution (" << value << ").");
return static_cast<bool>(value);
}
@@ -349,4 +352,4 @@ namespace storm {
}
}
-#endif
\ No newline at end of file
+#endif
diff --git a/src/storage/dd/DdManager.cpp b/src/storage/dd/DdManager.cpp
index 9281a0a33..3bb40b7db 100644
--- a/src/storage/dd/DdManager.cpp
+++ b/src/storage/dd/DdManager.cpp
@@ -6,6 +6,8 @@
#include "src/utility/constants.h"
#include "src/exceptions/InvalidArgumentException.h"
+#include <cmath>
+
namespace storm {
namespace dd {
template<DdType LibraryType>
@@ -349,4 +351,4 @@ namespace storm {
template Add<DdType::Sylvan, double> DdManager<DdType::Sylvan>::getIdentity(storm::expressions::Variable const& variable) const;
template Add<DdType::Sylvan, uint_fast64_t> DdManager<DdType::Sylvan>::getIdentity(storm::expressions::Variable const& variable) const;
}
-}
\ No newline at end of file
+}
diff --git a/src/storage/dd/cudd/CuddAddIterator.cpp b/src/storage/dd/cudd/CuddAddIterator.cpp
index e11b75aec..379a0ff22 100644
--- a/src/storage/dd/cudd/CuddAddIterator.cpp
+++ b/src/storage/dd/cudd/CuddAddIterator.cpp
@@ -4,6 +4,8 @@
#include "src/utility/macros.h"
#include "src/storage/expressions/ExpressionManager.h"
+#include <cmath>
+
namespace storm {
namespace dd {
template<typename ValueType>
@@ -184,4 +186,4 @@ namespace storm {
template class AddIterator<DdType::CUDD, double>;
template class AddIterator<DdType::CUDD, uint_fast64_t>;
}
-}
\ No newline at end of file
+}
diff --git a/src/storage/dd/sylvan/SylvanAddIterator.cpp b/src/storage/dd/sylvan/SylvanAddIterator.cpp
index 4322aa1b6..8c97941a3 100644
--- a/src/storage/dd/sylvan/SylvanAddIterator.cpp
+++ b/src/storage/dd/sylvan/SylvanAddIterator.cpp
@@ -8,6 +8,8 @@
#include "src/utility/macros.h"
#include "src/exceptions/NotImplementedException.h"
+#include <cmath>
+
namespace storm {
namespace dd {
template<typename ValueType>
@@ -186,4 +188,4 @@ namespace storm {
template class AddIterator<DdType::Sylvan, double>;
template class AddIterator<DdType::Sylvan, uint_fast64_t>;
}
-}
\ No newline at end of file
+}
From b99a063ccea413abb02e97ffaaa255e95f0c360a Mon Sep 17 00:00:00 2001
From: PBerger <philipp.berger@rwth-aachen.de>
Date: Thu, 23 Jun 2016 00:23:55 +0200
Subject: [PATCH 4/6] Replaced calls to std::abs with calls to std::fabs and
included cmath.
Former-commit-id: 40fb587e2fc33b9f5919b0a7a79bb3be111c8f11
---
test/functional/solver/GlpkLpSolverTest.cpp | 28 +++++++++++----------
1 file changed, 15 insertions(+), 13 deletions(-)
diff --git a/test/functional/solver/GlpkLpSolverTest.cpp b/test/functional/solver/GlpkLpSolverTest.cpp
index 4aea94cf7..737f8b56e 100644
--- a/test/functional/solver/GlpkLpSolverTest.cpp
+++ b/test/functional/solver/GlpkLpSolverTest.cpp
@@ -13,6 +13,8 @@
#include "src/storage/expressions/Expressions.h"
#include "src/solver/OptimizationDirection.h"
+#include <cmath>
+
TEST(GlpkLpSolver, LPOptimizeMax) {
storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Maximize);
storm::expressions::Variable x;
@@ -34,16 +36,16 @@ TEST(GlpkLpSolver, LPOptimizeMax) {
ASSERT_FALSE(solver.isInfeasible());
double xValue = 0;
ASSERT_NO_THROW(xValue = solver.getContinuousValue(x));
- ASSERT_LT(std::abs(xValue - 1), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ ASSERT_LT(std::fabs(xValue - 1), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
double yValue = 0;
ASSERT_NO_THROW(yValue = solver.getContinuousValue(y));
- ASSERT_LT(std::abs(yValue - 6.5), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ ASSERT_LT(std::fabs(yValue - 6.5), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
double zValue = 0;
ASSERT_NO_THROW(zValue = solver.getContinuousValue(z));
- ASSERT_LT(std::abs(zValue - 2.75), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ ASSERT_LT(std::fabs(zValue - 2.75), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
double objectiveValue = 0;
ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue());
- ASSERT_LT(std::abs(objectiveValue - 14.75), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ ASSERT_LT(std::fabs(objectiveValue - 14.75), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
}
TEST(GlpkLpSolver, LPOptimizeMin) {
@@ -67,16 +69,16 @@ TEST(GlpkLpSolver, LPOptimizeMin) {
ASSERT_FALSE(solver.isInfeasible());
double xValue = 0;
ASSERT_NO_THROW(xValue = solver.getContinuousValue(x));
- ASSERT_LT(std::abs(xValue - 1), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ ASSERT_LT(std::fabs(xValue - 1), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
double yValue = 0;
ASSERT_NO_THROW(yValue = solver.getContinuousValue(y));
- ASSERT_LT(std::abs(yValue - 0), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ ASSERT_LT(std::fabs(yValue - 0), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
double zValue = 0;
ASSERT_NO_THROW(zValue = solver.getContinuousValue(z));
- ASSERT_LT(std::abs(zValue - 5.7), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ ASSERT_LT(std::fabs(zValue - 5.7), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
double objectiveValue = 0;
ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue());
- ASSERT_LT(std::abs(objectiveValue - (-6.7)), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ ASSERT_LT(std::fabs(objectiveValue - (-6.7)), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
}
TEST(GlpkLpSolver, MILPOptimizeMax) {
@@ -106,10 +108,10 @@ TEST(GlpkLpSolver, MILPOptimizeMax) {
ASSERT_EQ(6, yValue);
double zValue = 0;
ASSERT_NO_THROW(zValue = solver.getContinuousValue(z));
- ASSERT_LT(std::abs(zValue - 3), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ ASSERT_LT(std::fabs(zValue - 3), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
double objectiveValue = 0;
ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue());
- ASSERT_LT(std::abs(objectiveValue - 14), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ ASSERT_LT(std::fabs(objectiveValue - 14), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
}
TEST(GlpkLpSolver, MILPOptimizeMin) {
@@ -139,10 +141,10 @@ TEST(GlpkLpSolver, MILPOptimizeMin) {
ASSERT_EQ(0, yValue);
double zValue = 0;
ASSERT_NO_THROW(zValue = solver.getContinuousValue(z));
- ASSERT_LT(std::abs(zValue - 5), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ ASSERT_LT(std::fabs(zValue - 5), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
double objectiveValue = 0;
ASSERT_NO_THROW(objectiveValue = solver.getObjectiveValue());
- ASSERT_LT(std::abs(objectiveValue - (-6)), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+ ASSERT_LT(std::fabs(objectiveValue - (-6)), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
}
TEST(GlpkLpSolver, LPInfeasible) {
@@ -244,4 +246,4 @@ TEST(GlpkLpSolver, MILPUnbounded) {
ASSERT_THROW(solver.getContinuousValue(z), storm::exceptions::InvalidAccessException);
ASSERT_THROW(solver.getObjectiveValue(), storm::exceptions::InvalidAccessException);
}
-#endif
\ No newline at end of file
+#endif
From e443384b91d36d3d3db3aa435ae3ac8ff6575768 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Thu, 23 Jun 2016 17:39:03 +0200
Subject: [PATCH 5/6] Added assertion
Former-commit-id: beeff9bff9053f9e59147b884e83b72efcab9f2f
---
src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
index 08ca016fd..0fa299321 100644
--- a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
+++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
@@ -5,6 +5,7 @@
#include "src/utility/macros.h"
#include "src/utility/vector.h"
#include "src/exceptions/InvalidOperationException.h"
+#include "src/exceptions/InvalidAccessException.h"
#include "src/adapters/CarlAdapter.h"
@@ -60,6 +61,7 @@ namespace storm {
if (this->isResultForAllStates()) {
map_type newMap;
for (auto const& element : filterTruthValues) {
+ STORM_LOG_THROW(element < this->getValueVector().size(), storm::exceptions::InvalidAccessException, "Invalid index in results.");
newMap.emplace(element, this->getValueVector()[element]);
}
this->values = newMap;
@@ -253,4 +255,4 @@ namespace storm {
template class ExplicitQuantitativeCheckResult<storm::RationalFunction>;
#endif
}
-}
\ No newline at end of file
+}
From 711d5cfa12e7704c8a38f46066bd93407ba26c58 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 23 Jun 2016 18:59:23 +0200
Subject: [PATCH 6/6] fixed bug in sparse dtmc elimination model checker.
commented out weird eliminaton functions in CTMC model checker and storm.h
Former-commit-id: 3000123a3d264edc5e98678fe662f6c277acbbad
---
resources/3rdparty/cudd-3.0.0/configure | 1 +
.../csl/helper/SparseCtmcCslHelper.cpp | 32 -----
.../csl/helper/SparseCtmcCslHelper.h | 2 -
.../SparseDtmcEliminationModelChecker.cpp | 131 +++++++++---------
.../SparseDtmcEliminationModelChecker.h | 6 +-
.../ExplicitQuantitativeCheckResult.cpp | 3 +
src/utility/storm.h | 8 +-
7 files changed, 77 insertions(+), 106 deletions(-)
diff --git a/resources/3rdparty/cudd-3.0.0/configure b/resources/3rdparty/cudd-3.0.0/configure
index f0e0e742e..1494802d5 100755
--- a/resources/3rdparty/cudd-3.0.0/configure
+++ b/resources/3rdparty/cudd-3.0.0/configure
@@ -4419,6 +4419,7 @@ else
fi
+
ac_ext=cpp
ac_cpp='$CXXCPP $CPPFLAGS'
ac_compile='$CXX -c $CXXFLAGS $CPPFLAGS conftest.$ac_ext >&5'
diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
index b4c01d13a..8fafb5093 100644
--- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
+++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
@@ -195,12 +195,6 @@ namespace storm {
return SparseDtmcPrctlHelper<ValueType>::computeUntilProbabilities(computeProbabilityMatrix(rateMatrix, exitRateVector), backwardTransitions, phiStates, psiStates, qualitative, linearEquationSolverFactory);
}
- template <typename ValueType>
- std::vector<ValueType> SparseCtmcCslHelper<ValueType>::computeUntilProbabilitiesElimination(storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) {
- // Use "normal" function again, if RationalFunction finally is supported.
- return storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<ValueType>>::computeUntilProbabilities(computeProbabilityMatrix(rateMatrix, exitRateVector), backwardTransitions, initialStates, phiStates, psiStates, false);
- }
-
template <typename ValueType>
std::vector<ValueType> SparseCtmcCslHelper<ValueType>::computeNextProbabilities(storm::storage::SparseMatrix<ValueType> const& rateMatrix, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& nextStates, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
return SparseDtmcPrctlHelper<ValueType>::computeNextProbabilities(computeProbabilityMatrix(rateMatrix, exitRateVector), nextStates, linearEquationSolverFactory);
@@ -675,37 +669,11 @@ namespace storm {
return storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeReachabilityRewards(probabilityMatrix, backwardTransitions, totalRewardVector, targetStates, qualitative, linearEquationSolverFactory);
}
-
- template <typename ValueType>
- std::vector<ValueType> SparseCtmcCslHelper<ValueType>::computeReachabilityTimesElimination(storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative) {
- // Use "normal" function again, if RationalFunction finally is supported.
- // Compute expected time on CTMC by reduction to DTMC with rewards.
- storm::storage::SparseMatrix<ValueType> probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector);
-
- // Initialize rewards.
- std::vector<ValueType> totalRewardVector;
- for (size_t i = 0; i < exitRateVector.size(); ++i) {
- if (targetStates[i] || storm::utility::isZero(exitRateVector[i])) {
- // Set reward for target states or states without outgoing transitions to 0.
- totalRewardVector.push_back(storm::utility::zero<ValueType>());
- } else {
- // Reward is (1 / exitRate).
- totalRewardVector.push_back(storm::utility::one<ValueType>() / exitRateVector[i]);
- }
- }
-
- return storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<ValueType>>::computeReachabilityRewards(probabilityMatrix, backwardTransitions, initialStates, targetStates, totalRewardVector, false);
- }
-
template class SparseCtmcCslHelper<double>;
template std::vector<double> SparseCtmcCslHelper<double>::computeInstantaneousRewards(storm::storage::SparseMatrix<double> const& rateMatrix, std::vector<double> const& exitRateVector, storm::models::sparse::StandardRewardModel<double> const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
template std::vector<double> SparseCtmcCslHelper<double>::computeCumulativeRewards(storm::storage::SparseMatrix<double> const& rateMatrix, std::vector<double> const& exitRateVector, storm::models::sparse::StandardRewardModel<double> const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
template std::vector<double> SparseCtmcCslHelper<double>::computeReachabilityRewards(storm::storage::SparseMatrix<double> const& rateMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, std::vector<double> const& exitRateVector, storm::models::sparse::StandardRewardModel<double> const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
-#ifdef STORM_HAVE_CARL
- template std::vector<storm::RationalFunction> SparseCtmcCslHelper<storm::RationalFunction>::computeUntilProbabilitiesElimination(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative);
- template std::vector<storm::RationalFunction> SparseCtmcCslHelper<storm::RationalFunction>::computeReachabilityTimesElimination(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative);
-#endif
}
}
}
diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.h b/src/modelchecker/csl/helper/SparseCtmcCslHelper.h
index 2b4dd6043..69ca7faad 100644
--- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.h
+++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.h
@@ -16,7 +16,6 @@ namespace storm {
static std::vector<ValueType> computeNextProbabilities(storm::storage::SparseMatrix<ValueType> const& rateMatrix, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& nextStates, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
static std::vector<ValueType> computeUntilProbabilities(storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
- static std::vector<ValueType> computeUntilProbabilitiesElimination(storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative);
template <typename RewardModelType>
static std::vector<ValueType> computeInstantaneousRewards(storm::storage::SparseMatrix<ValueType> const& rateMatrix, std::vector<ValueType> const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
@@ -30,7 +29,6 @@ namespace storm {
static std::vector<ValueType> computeLongRunAverageProbabilities(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<ValueType> const* exitRateVector, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
static std::vector<ValueType> computeReachabilityTimes(storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
- static std::vector<ValueType> computeReachabilityTimesElimination(storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative);
/*!
* Computes the matrix representing the transitions of the uniformized CTMC.
diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
index 5a6045f66..6fb3d79f1 100644
--- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
+++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
@@ -98,7 +98,7 @@ namespace storm {
storm::logic::StateFormula const& stateFormula = checkTask.getFormula();
std::unique_ptr<CheckResult> subResultPointer = this->check(stateFormula);
storm::storage::BitVector const& psiStates = subResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector();
-
+
storm::storage::SparseMatrix<ValueType> const& transitionMatrix = this->getModel().getTransitionMatrix();
uint_fast64_t numberOfStates = transitionMatrix.getRowCount();
if (psiStates.empty()) {
@@ -157,7 +157,7 @@ namespace storm {
// Do some sanity checks to establish some required properties.
RewardModelType const& rewardModel = this->getModel().getRewardModel(checkTask.isRewardModelSet() ? checkTask.getRewardModel() : "");
STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::IllegalArgumentException, "Input model does not have a reward model.");
-
+
storm::storage::BitVector const& initialStates = this->getModel().getInitialStates();
STORM_LOG_THROW(initialStates.getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state.");
STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::IllegalArgumentException, "Cannot compute long-run probabilities for all states.");
@@ -167,7 +167,7 @@ namespace storm {
// Get the state-reward values from the reward model.
std::vector<ValueType> stateRewardValues = rewardModel.getTotalRewardVector(this->getModel().getTransitionMatrix());
-
+
storm::storage::BitVector maybeStates(stateRewardValues.size());
uint_fast64_t index = 0;
for (auto const& value : stateRewardValues) {
@@ -183,7 +183,7 @@ namespace storm {
maybeStates = storm::utility::graph::performProbGreater0(backwardTransitions, allStates, maybeStates);
std::vector<ValueType> result(numberOfStates, storm::utility::zero<ValueType>());
-
+
// Determine whether we need to perform some further computation.
bool furtherComputationNeeded = true;
if (checkTask.isOnlyInitialStatesRelevantSet() && initialStates.isDisjointFrom(maybeStates)) {
@@ -221,7 +221,7 @@ namespace storm {
std::chrono::high_resolution_clock::time_point sccDecompositionStart = std::chrono::high_resolution_clock::now();
storm::storage::StronglyConnectedComponentDecomposition<ValueType> bsccDecomposition(transitionMatrix, storm::storage::BitVector(transitionMatrix.getRowCount(), true), false, true);
auto sccDecompositionEnd = std::chrono::high_resolution_clock::now();
-
+
std::chrono::high_resolution_clock::time_point conversionStart = std::chrono::high_resolution_clock::now();
// Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily.
@@ -232,7 +232,7 @@ namespace storm {
auto conversionEnd = std::chrono::high_resolution_clock::now();
std::chrono::high_resolution_clock::time_point modelCheckingStart = std::chrono::high_resolution_clock::now();
-
+
storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder order = storm::settings::getModule<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings>().getEliminationOrder();
boost::optional<std::vector<uint_fast64_t>> distanceBasedPriorities;
if (eliminationOrderNeedsDistances(order)) {
@@ -294,7 +294,7 @@ namespace storm {
}
stateValues[*representativeIt] = bsccValue;
}
-
+
FlexibleRowType& representativeForwardRow = flexibleMatrix.getRow(*representativeIt);
representativeForwardRow.clear();
representativeForwardRow.shrink_to_fit();
@@ -307,10 +307,10 @@ namespace storm {
}
}
representativeBackwardRow.erase(it);
-
+
++representativeIt;
}
-
+
// If there are states remaining that are not in BSCCs, we need to eliminate them now.
storm::storage::BitVector remainingStates = maybeStates & ~regularStatesInBsccs;
@@ -388,7 +388,7 @@ namespace storm {
storm::storage::BitVector const& initialStates = this->getModel().getInitialStates();
std::vector<ValueType> result(transitionMatrix.getRowCount(), storm::utility::zero<ValueType>());
-
+
if (furtherComputationNeeded) {
uint_fast64_t timeBound = pathFormula.getDiscreteTimeBound();
@@ -399,7 +399,7 @@ namespace storm {
// Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state).
statesWithProbabilityGreater0 &= reachableStates;
}
-
+
// We then build the submatrix that only has the transitions of the maybe states.
storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, statesWithProbabilityGreater0, statesWithProbabilityGreater0, true);
@@ -408,7 +408,7 @@ namespace storm {
if (checkTask.isOnlyInitialStatesRelevantSet()) {
// Determine the set of initial states of the sub-model.
storm::storage::BitVector subInitialStates = this->getModel().getInitialStates() % statesWithProbabilityGreater0;
-
+
// Precompute the distances of the relevant states to the initial states.
distancesFromInitialStates = storm::utility::graph::getDistances(submatrix, subInitialStates, statesWithProbabilityGreater0);
@@ -471,23 +471,19 @@ namespace storm {
std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
storm::storage::BitVector const& phiStates = leftResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector();
storm::storage::BitVector const& psiStates = rightResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector();
-
- std::vector<ValueType> result = computeUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), phiStates, psiStates, checkTask.isOnlyInitialStatesRelevantSet());
-
- // Construct check result.
- std::unique_ptr<CheckResult> checkResult(new ExplicitQuantitativeCheckResult<ValueType>(result));
- return checkResult;
+
+ return computeUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), phiStates, psiStates, checkTask.isOnlyInitialStatesRelevantSet());
}
-
+
template<typename SparseDtmcModelType>
- std::vector<typename SparseDtmcModelType::ValueType> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeUntilProbabilities(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool computeForInitialStatesOnly) {
-
+ std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeUntilProbabilities(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool computeForInitialStatesOnly) {
+
// Then, compute the subset of states that has a probability of 0 or 1, respectively.
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiStates, psiStates);
storm::storage::BitVector statesWithProbability0 = statesWithProbability01.first;
storm::storage::BitVector statesWithProbability1 = statesWithProbability01.second;
storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1);
-
+
// Determine whether we need to perform some further computation.
bool furtherComputationNeeded = true;
if (computeForInitialStatesOnly && initialStates.isDisjointFrom(maybeStates)) {
@@ -497,7 +493,7 @@ namespace storm {
STORM_LOG_DEBUG("The probability for all states was found in a preprocessing step.");
furtherComputationNeeded = false;
}
-
+
std::vector<ValueType> result(maybeStates.size());
if (furtherComputationNeeded) {
// If we compute the results for the initial states only, we can cut off all maybe state that are not
@@ -505,35 +501,39 @@ namespace storm {
if (computeForInitialStatesOnly) {
// Determine the set of states that is reachable from the initial state without jumping over a target state.
storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(probabilityMatrix, initialStates, maybeStates, statesWithProbability1);
-
+
// Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state).
maybeStates &= reachableStates;
}
-
+
// Create a vector for the probabilities to go to a state with probability 1 in one step.
std::vector<ValueType> oneStepProbabilities = probabilityMatrix.getConstrainedRowSumVector(maybeStates, statesWithProbability1);
-
+
// Determine the set of initial states of the sub-model.
storm::storage::BitVector newInitialStates = initialStates % maybeStates;
-
+
// We then build the submatrix that only has the transitions of the maybe states.
storm::storage::SparseMatrix<ValueType> submatrix = probabilityMatrix.getSubmatrix(false, maybeStates, maybeStates);
storm::storage::SparseMatrix<ValueType> submatrixTransposed = submatrix.transpose();
-
+
std::vector<ValueType> subresult = computeReachabilityValues(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, computeForInitialStatesOnly, phiStates, psiStates, oneStepProbabilities);
storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, subresult);
}
-
+
// Construct full result.
storm::utility::vector::setVectorValues<ValueType>(result, statesWithProbability0, storm::utility::zero<ValueType>());
storm::utility::vector::setVectorValues<ValueType>(result, statesWithProbability1, storm::utility::one<ValueType>());
-
+
if (computeForInitialStatesOnly) {
// If we computed the results for the initial (and prob 0 and prob1) states only, we need to filter the
// result to only communicate these results.
- result = storm::utility::vector::filterVector(result, ~maybeStates | initialStates);
+ std::unique_ptr<ExplicitQuantitativeCheckResult<ValueType>> checkResult = std::make_unique<ExplicitQuantitativeCheckResult<ValueType>>();
+ for (auto state : ~maybeStates | initialStates) {
+ (*checkResult)[state] = result[state];
+ }
+ return std::move(checkResult);
}
- return result;
+ return std::make_unique<ExplicitQuantitativeCheckResult<ValueType>>(result);
}
template<typename SparseDtmcModelType>
@@ -547,21 +547,18 @@ namespace storm {
// Do some sanity checks to establish some required properties.
RewardModelType const& rewardModel = this->getModel().getRewardModel(checkTask.isRewardModelSet() ? checkTask.getRewardModel() : "");
-
+
STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::IllegalArgumentException, "Input model does not have a reward model.");
- std::vector<ValueType> result = computeReachabilityRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), targetStates,
- [&] (uint_fast64_t numberOfRows, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates) {
- return rewardModel.getTotalRewardVector(numberOfRows, transitionMatrix, maybeStates);
- },
- checkTask.isOnlyInitialStatesRelevantSet());
-
- // Construct check result.
- std::unique_ptr<CheckResult> checkResult(new ExplicitQuantitativeCheckResult<ValueType>(result));
- return checkResult;
+ return computeReachabilityRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), targetStates,
+ [&] (uint_fast64_t numberOfRows, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates) {
+ return rewardModel.getTotalRewardVector(numberOfRows, transitionMatrix, maybeStates);
+ },
+ checkTask.isOnlyInitialStatesRelevantSet());
+
}
-
+
template<typename SparseDtmcModelType>
- std::vector<typename SparseDtmcModelType::ValueType> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::vector<ValueType>& stateRewardValues, bool computeForInitialStatesOnly) {
+ std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::vector<ValueType>& stateRewardValues, bool computeForInitialStatesOnly) {
return computeReachabilityRewards(probabilityMatrix, backwardTransitions, initialStates, targetStates,
[&] (uint_fast64_t numberOfRows, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates) {
std::vector<ValueType> result(numberOfRows);
@@ -570,10 +567,10 @@ namespace storm {
},
computeForInitialStatesOnly);
}
-
+
template<typename SparseDtmcModelType>
- std::vector<typename SparseDtmcModelType::ValueType> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, bool computeForInitialStatesOnly) {
-
+ std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, bool computeForInitialStatesOnly) {
+
uint_fast64_t numberOfStates = probabilityMatrix.getRowCount();
// Compute the subset of states that has a reachability reward less than infinity.
@@ -594,7 +591,7 @@ namespace storm {
furtherComputationNeeded = false;
}
}
-
+
std::vector<ValueType> result(maybeStates.size());
if (furtherComputationNeeded) {
// If we compute the results for the initial states only, we can cut off all maybe state that are not
@@ -609,14 +606,14 @@ namespace storm {
// Determine the set of initial states of the sub-model.
storm::storage::BitVector newInitialStates = initialStates % maybeStates;
-
+
// We then build the submatrix that only has the transitions of the maybe states.
storm::storage::SparseMatrix<ValueType> submatrix = probabilityMatrix.getSubmatrix(false, maybeStates, maybeStates);
storm::storage::SparseMatrix<ValueType> submatrixTransposed = submatrix.transpose();
// Project the state reward vector to all maybe-states.
std::vector<ValueType> stateRewardValues = totalStateRewardVectorGetter(submatrix.getRowCount(), probabilityMatrix, maybeStates);
-
+
std::vector<ValueType> subresult = computeReachabilityValues(submatrix, stateRewardValues, submatrixTransposed, newInitialStates, computeForInitialStatesOnly, trueStates, targetStates, probabilityMatrix.getConstrainedRowSumVector(maybeStates, targetStates));
storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, subresult);
}
@@ -627,9 +624,13 @@ namespace storm {
if (computeForInitialStatesOnly) {
// If we computed the results for the initial (and inf) states only, we need to filter the result to
// only communicate these results.
- result = storm::utility::vector::filterVector(result, ~maybeStates | initialStates);
+ std::unique_ptr<ExplicitQuantitativeCheckResult<ValueType>> checkResult = std::make_unique<ExplicitQuantitativeCheckResult<ValueType>>();
+ for (auto state : ~maybeStates | initialStates) {
+ (*checkResult)[state] = result[state];
+ }
+ return std::move(checkResult);
}
- return result;
+ return std::make_unique<ExplicitQuantitativeCheckResult<ValueType>>(result);
}
template<typename SparseDtmcModelType>
@@ -711,15 +712,15 @@ namespace storm {
storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder order = storm::settings::getModule<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings>().getEliminationOrder();
if (eliminationOrderNeedsDistances(order)) {
distanceBasedPriorities = getDistanceBasedPriorities(submatrix, submatrixTransposed, newInitialStates, oneStepProbabilities,
- eliminationOrderNeedsForwardDistances(order),
- eliminationOrderNeedsReversedDistances(order));
+ eliminationOrderNeedsForwardDistances(order),
+ eliminationOrderNeedsReversedDistances(order));
}
storm::storage::FlexibleSparseMatrix<ValueType> flexibleMatrix(submatrix);
storm::storage::FlexibleSparseMatrix<ValueType> flexibleBackwardTransitions(submatrixTransposed, true);
std::shared_ptr<StatePriorityQueue<ValueType>> statePriorities = createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, statesToEliminate);
-
+
STORM_LOG_INFO("Computing conditional probilities." << std::endl);
uint_fast64_t numberOfStatesToEliminate = statePriorities->size();
STORM_LOG_INFO("Eliminating " << numberOfStatesToEliminate << " states using the state elimination technique." << std::endl);
@@ -852,7 +853,7 @@ namespace storm {
storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder order = storm::settings::getModule<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings>().getEliminationOrder();
std::vector<storm::storage::sparse::state_type> sortedStates(states.begin(), states.end());
-
+
if (order == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Random) {
std::random_device randomDevice;
std::mt19937 generator(randomDevice());
@@ -944,7 +945,7 @@ namespace storm {
// Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily.
storm::storage::FlexibleSparseMatrix<ValueType> flexibleMatrix(transitionMatrix);
storm::storage::FlexibleSparseMatrix<ValueType> flexibleBackwardTransitions(backwardTransitions);
-
+
storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder order = storm::settings::getModule<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings>().getEliminationOrder();
boost::optional<std::vector<uint_fast64_t>> distanceBasedPriorities;
if (eliminationOrderNeedsDistances(order)) {
@@ -961,7 +962,7 @@ namespace storm {
} else if (storm::settings::getModule<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings>().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::Hybrid) {
maximalDepth = performHybridStateElimination(transitionMatrix, flexibleMatrix, flexibleBackwardTransitions, subsystem, initialStates, computeResultsForInitialStatesOnly, values, distanceBasedPriorities);
}
-
+
STORM_LOG_ASSERT(flexibleMatrix.empty(), "Not all transitions were eliminated.");
STORM_LOG_ASSERT(flexibleBackwardTransitions.empty(), "Not all transitions were eliminated.");
@@ -1004,7 +1005,7 @@ namespace storm {
STORM_LOG_TRACE("Eliminating " << statePriorities->size() << " trivial SCCs.");
performPrioritizedStateElimination(statePriorities, matrix, backwardTransitions, values, initialStates, computeResultsForInitialStatesOnly);
STORM_LOG_TRACE("Eliminated all trivial SCCs.");
-
+
// And then recursively treat the remaining sub-SCCs.
STORM_LOG_TRACE("Eliminating " << remainingSccs.getNumberOfSetBits() << " remaining SCCs on level " << level << ".");
for (auto sccIndex : remainingSccs) {
@@ -1106,22 +1107,22 @@ namespace storm {
for (auto const& predecessor : backwardTransitions.getRow(state)) {
for (auto const& successor : transitionMatrix.getRow(state)) {
penalty += estimateComplexity(predecessor.getValue()) * estimateComplexity(successor.getValue());
-// STORM_LOG_TRACE("1) penalty += " << (estimateComplexity(predecessor.getValue()) * estimateComplexity(successor.getValue())) << " because of " << predecessor.getValue() << " and " << successor.getValue() << ".");
+ // STORM_LOG_TRACE("1) penalty += " << (estimateComplexity(predecessor.getValue()) * estimateComplexity(successor.getValue())) << " because of " << predecessor.getValue() << " and " << successor.getValue() << ".");
}
if (predecessor.getColumn() == state) {
hasParametricSelfLoop = !storm::utility::isConstant(predecessor.getValue());
}
penalty += estimateComplexity(oneStepProbabilities[predecessor.getColumn()]) * estimateComplexity(predecessor.getValue()) * estimateComplexity(oneStepProbabilities[state]);
-// STORM_LOG_TRACE("2) penalty += " << (estimateComplexity(oneStepProbabilities[predecessor.getColumn()]) * estimateComplexity(predecessor.getValue()) * estimateComplexity(oneStepProbabilities[state])) << " because of " << oneStepProbabilities[predecessor.getColumn()] << ", " << predecessor.getValue() << " and " << oneStepProbabilities[state] << ".");
+ // STORM_LOG_TRACE("2) penalty += " << (estimateComplexity(oneStepProbabilities[predecessor.getColumn()]) * estimateComplexity(predecessor.getValue()) * estimateComplexity(oneStepProbabilities[state])) << " because of " << oneStepProbabilities[predecessor.getColumn()] << ", " << predecessor.getValue() << " and " << oneStepProbabilities[state] << ".");
}
// If it is a self-loop that is parametric, we increase the penalty a lot.
if (hasParametricSelfLoop) {
penalty *= 10;
-// STORM_LOG_TRACE("3) penalty *= 100, because of parametric self-loop.");
+ // STORM_LOG_TRACE("3) penalty *= 100, because of parametric self-loop.");
}
-// STORM_LOG_TRACE("New penalty of state " << state << " is " << penalty << ".");
+ // STORM_LOG_TRACE("New penalty of state " << state << " is " << penalty << ".");
return penalty;
}
@@ -1238,8 +1239,8 @@ namespace storm {
template class StatePriorityQueue<double>;
template class SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<double>>;
template uint_fast64_t estimateComplexity(double const& value);
-
-
+
+
#ifdef STORM_HAVE_CARL
template class StatePriorityQueue<storm::RationalFunction>;
template class SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>>;
diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
index 7359ac93f..ec61cb0ef 100644
--- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
+++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
@@ -47,9 +47,9 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula> const& checkTask) override;
// Static helper methods
- static std::vector<ValueType> computeUntilProbabilities(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool computeForInitialStatesOnly);
+ static std::unique_ptr<CheckResult> computeUntilProbabilities(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool computeForInitialStatesOnly);
- static std::vector<ValueType> computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::vector<ValueType>& stateRewardValues, bool computeForInitialStatesOnly);
+ static std::unique_ptr<CheckResult> computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::vector<ValueType>& stateRewardValues, bool computeForInitialStatesOnly);
private:
@@ -91,7 +91,7 @@ namespace storm {
static std::vector<ValueType> computeLongRunValues(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& maybeStates, bool computeResultsForInitialStatesOnly, std::vector<ValueType>& stateValues);
- static std::vector<ValueType> computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, bool computeForInitialStatesOnly);
+ static std::unique_ptr<CheckResult> computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, bool computeForInitialStatesOnly);
static std::vector<ValueType> computeReachabilityValues(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType>& values, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector<ValueType> const& oneStepProbabilitiesToTarget);
diff --git a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
index 0fa299321..5d4a891e5 100644
--- a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
+++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
@@ -60,7 +60,10 @@ namespace storm {
if (this->isResultForAllStates()) {
map_type newMap;
+ std::cout << filterTruthValues << std::endl;
for (auto const& element : filterTruthValues) {
+ std::cout << element << std::endl;
+ std::cout << this->getValueVector().size() << std::endl;
STORM_LOG_THROW(element < this->getValueVector().size(), storm::exceptions::InvalidAccessException, "Invalid index in results.");
newMap.emplace(element, this->getValueVector()[element]);
}
diff --git a/src/utility/storm.h b/src/utility/storm.h
index ce213cf08..5f47631e4 100644
--- a/src/utility/storm.h
+++ b/src/utility/storm.h
@@ -375,8 +375,8 @@ namespace storm {
std::unique_ptr<storm::modelchecker::CheckResult> subResultPointer = propositionalModelchecker.check(eventuallyFormula.getSubformula());
storm::storage::BitVector const& targetStates = subResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector();
- std::vector<storm::RationalFunction> numericResult = storm::modelchecker::helper::SparseCtmcCslHelper<storm::RationalFunction>::computeReachabilityTimesElimination(ctmc->getTransitionMatrix(), ctmc->getBackwardTransitions(), ctmc->getExitRateVector(), ctmc->getInitialStates(), targetStates, false);
- result = std::unique_ptr<storm::modelchecker::CheckResult>(new storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>(std::move(numericResult)));
+// std::vector<storm::RationalFunction> numericResult = storm::modelchecker::helper::SparseCtmcCslHelper<storm::RationalFunction>::computeReachabilityTimesElimination(ctmc->getTransitionMatrix(), ctmc->getBackwardTransitions(), ctmc->getExitRateVector(), ctmc->getInitialStates(), targetStates, false);
+// result = std::unique_ptr<storm::modelchecker::CheckResult>(new storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>(std::move(numericResult)));
} else if (formula->isProbabilityOperatorFormula()) {
// Compute reachability probability for pCTMCs
@@ -406,8 +406,8 @@ namespace storm {
psiStates = resultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector();
}
- std::vector<storm::RationalFunction> numericResult = storm::modelchecker::helper::SparseCtmcCslHelper<storm::RationalFunction>::computeUntilProbabilitiesElimination(ctmc->getTransitionMatrix(), ctmc->getBackwardTransitions(), ctmc->getExitRateVector(), ctmc->getInitialStates(), phiStates, psiStates, false);
- result = std::unique_ptr<storm::modelchecker::CheckResult>(new storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>(std::move(numericResult)));
+// std::vector<storm::RationalFunction> numericResult = storm::modelchecker::helper::SparseCtmcCslHelper<storm::RationalFunction>::computeUntilProbabilitiesElimination(ctmc->getTransitionMatrix(), ctmc->getBackwardTransitions(), ctmc->getExitRateVector(), ctmc->getInitialStates(), phiStates, psiStates, false);
+// result = std::unique_ptr<storm::modelchecker::CheckResult>(new storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>(std::move(numericResult)));
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The parametric engine currently does not support this property on CTMCs.");