From 3d083a171946013598fd757c94ecd07cab8fc699 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Wed, 12 Oct 2016 13:06:59 +0200
Subject: [PATCH] Fixed bug with wrong row in case of nondeterminism
Former-commit-id: 24d7bd672c3df018ab35ebc2b70190b226bbb8b9
---
src/builder/DftExplorationHeuristic.cpp | 2 --
src/builder/ExplicitDFTModelBuilderApprox.cpp | 4 ++--
2 files changed, 2 insertions(+), 4 deletions(-)
diff --git a/src/builder/DftExplorationHeuristic.cpp b/src/builder/DftExplorationHeuristic.cpp
index 74937d4b1..727c29c37 100644
--- a/src/builder/DftExplorationHeuristic.cpp
+++ b/src/builder/DftExplorationHeuristic.cpp
@@ -44,9 +44,7 @@ namespace storm {
template<typename ValueType>
void DFTExplorationHeuristic<ValueType>::setHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) {
- std::cout << "Set priority: " << depth << ", old: " << this->depth << std::endl;
this->depth = depth;
- // TODO Matthias: update rates and exitRates as well
this->rate = rate;
this->exitRate = exitRate;
}
diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp
index 9ed09eccb..0bf848838 100644
--- a/src/builder/ExplicitDFTModelBuilderApprox.cpp
+++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp
@@ -412,7 +412,7 @@ namespace storm {
void ExplicitDFTModelBuilderApprox<ValueType, StateType>::changeMatrixLowerBound(storm::storage::SparseMatrix<ValueType> & matrix) const {
// Set lower bound for skipped states
for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) {
- auto matrixEntry = matrix.getRow(it->first).begin();
+ auto matrixEntry = matrix.getRow(it->first, 0).begin();
STORM_LOG_ASSERT(matrixEntry->getColumn() == failedStateId, "Transition has wrong target state.");
// Get the lower bound by considering the failure of the BE with the highest rate
// The list is sorted by rate, therefore we consider the first BE for the highest failure rate
@@ -424,7 +424,7 @@ namespace storm {
void ExplicitDFTModelBuilderApprox<ValueType, StateType>::changeMatrixUpperBound(storm::storage::SparseMatrix<ValueType> & matrix) const {
// Set uppper bound for skipped states
for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) {
- auto matrixEntry = matrix.getRow(it->first).begin();
+ auto matrixEntry = matrix.getRow(it->first, 0).begin();
STORM_LOG_ASSERT(matrixEntry->getColumn() == failedStateId, "Transition has wrong target state.");
// Get the upper bound by considering the failure of all BEs
// The used formula for the rate is 1/( 1/a + 1/b + ...)