From 7577ca48ec8d5d4b03259eab209cd29dd4ac724d Mon Sep 17 00:00:00 2001
From: Timo Philipp Gros <timopgros@gmail.com>
Date: Tue, 19 Dec 2017 17:17:51 +0100
Subject: [PATCH] changed loop of diff checking; ;
---
.../csl/helper/SparseMarkovAutomatonCslHelper.cpp | 9 +++++++--
1 file changed, 7 insertions(+), 2 deletions(-)
diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
index ad8c44b0f..819d684c5 100644
--- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
+++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
@@ -690,10 +690,15 @@ namespace storm {
fullTransitionMatrix, markovianStates, psiStates, solver, logfile,
foxGlynnResult);
//also use iteration to keep maxNorm of vd and vup to date, so the loop-condition is easy to prove
- ValueType diff = std::abs(unifVectors[0][k][i] - unifVectors[1][k][i]);
- maxNorm = std::max(maxNorm, diff);
+ //ValueType diff = std::abs(unifVectors[0][k][i] - unifVectors[1][k][i]);
}
}
+
+ //only iterate over result vector, as the results can only get more precise
+ for (uint64_t i = 0; i < numberOfStates; i++){
+ ValueType diff = std::abs(unifVectors[0][0][i]-unifVectors[1][0][i]);
+ maxNorm = std::max(maxNorm, diff);
+ }
//printTransitions(N, maxNorm, fullTransitionMatrix, exitRate, markovianStates, psiStates,
// relReachability, psiStates, psiStates, unifVectors, logfile); //TODO remove