From b155abc0994b8321dce1bc381990ba3766d049cd Mon Sep 17 00:00:00 2001 From: Timo Philipp Gros Date: Sun, 26 Nov 2017 18:55:17 +0100 Subject: [PATCH] fixed stupid, big bug. add exit for stock-case --- .../csl/helper/SparseMarkovAutomatonCslHelper.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 3d12a0cbe..d88a50cec 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -469,6 +469,7 @@ namespace storm { std::ofstream logfile("U+logfile.txt", std::ios::app); ValueType maxNorm = storm::utility::zero(); + ValueType oldDiff = -storm::utility::zero(); //bitvectors to identify different kind of states storm::storage::BitVector markovianStates = markovStates; @@ -556,6 +557,7 @@ namespace storm { } // while not close enough to precision: do { + maxNorm = storm::utility::zero(); // (2) update parameter N = ceil(lambda*T*exp(2)-log(kappa*epsilon)); @@ -615,6 +617,14 @@ namespace storm { // (6) double lambda lambda=2*lambda; + // (7) escape if not coming closer to solution + if (oldDiff!=-1){ + if (oldDiff==maxNorm){ + std::cout << "Not coming closer to solution as " << maxNorm << "/n"; + break; + } + } + oldDiff = maxNorm; } while (maxNorm>epsilon*(1-kappa)); logfile.close();