diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index b64a04459..b427bcfbd 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -570,15 +570,12 @@ namespace storm { double T = boundsPair.second; ValueType kappa = storm::utility::one() / 10; // would be better as option-parameter ValueType epsilon = storm::settings::getModule().getPrecision(); - ValueType lambda = exitRateVector[0]; - for (ValueType act: exitRateVector) { + ValueType lambda = exitRate[0]; + for (ValueType act: exitRate) { lambda = std::max(act, lambda); } uint64_t N; - - - //calculate relative ReachabilityVectors std::vector in{}; std::vector> relReachability(transitionMatrix.getRowCount(), in); @@ -621,10 +618,11 @@ namespace storm { //logfile << "starting iteration\n"; maxNorm = storm::utility::zero(); // (2) update parameter + N = ceil(lambda * T * exp(2) - log(kappa * epsilon)); // (3) uniform - just applied to markovian states - for (uint_fast64_t i = 0; i < fullTransitionMatrix.getRowGroupCount(); i++) { - if (!markovianStates[i]) { + for (uint64_t i = 0; i < fullTransitionMatrix.getRowGroupCount(); i++) { + if (!markovianStates[i] || psiStates[i]) { continue; } uint64_t from = rowGroupIndices[i]; //markovian state -> no Nondeterminism -> only one row @@ -638,7 +636,7 @@ namespace storm { ValueType exitNew = lambda; for (auto &v : line) { if (v.getColumn() == i) { //diagonal element - ValueType newSelfLoop = exitNew - exitOld + v.getValue(); + ValueType newSelfLoop = exitNew - exitOld + v.getValue()*exitOld; ValueType newRate = newSelfLoop / exitNew; v.setValue(newRate); } else { //modify probability @@ -654,8 +652,6 @@ namespace storm { storm::utility::numerical::FoxGlynnResult foxGlynnResult = storm::utility::numerical::foxGlynn(lambda*T, epsilon*kappa); - N = std::max(ceil(lambda * T * exp(2) - log(kappa * epsilon)), ceil(foxGlynnResult.right - foxGlynnResult.left +1 )); - // Scale the weights so they add up to one. for (auto& element : foxGlynnResult.weights) { element /= foxGlynnResult.totalWeight; @@ -695,8 +691,8 @@ namespace storm { maxNorm = std::max(maxNorm, diff); } } - printTransitions(N, maxNorm, fullTransitionMatrix, exitRate, markovianStates, psiStates, - relReachability, psiStates, psiStates, unifVectors, logfile); //TODO remove + //printTransitions(N, maxNorm, fullTransitionMatrix, exitRate, markovianStates, psiStates, + // relReachability, psiStates, psiStates, unifVectors, logfile); //TODO remove // (6) double lambda