diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index e56e03044..a5b70f3d2 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -310,49 +310,36 @@ namespace storm { } //probabilistic non-goal State - if (!markovianStates[node]){ - std::vector b(probSize, 0), x(numberOfProbStates,0); - //calculate b - uint64_t lineCounter=0; - for (int i =0; isolveEquations(env, dir, x, b); - - - - for (uint64_t i =0 ; i fullTransitionMatrix = transitionMatrix.getSubmatrix( true, allStates, allStates, true); // delete diagonals - //deleteProbDiagonals(fullTransitionMatrix, markovianStates); //for now leaving this out + deleteProbDiagonals(fullTransitionMatrix, markovianStates); //for now leaving this out typename storm::storage::SparseMatrix probMatrix{}; uint64_t probSize = 0; if (probabilisticStates.getNumberOfSetBits() != 0) { //work around in case there are no prob states @@ -584,7 +571,7 @@ namespace storm { //calculate relative reachability - + /* for (uint64_t i = 0; i < numberOfStates; i++) { if (markovianStates[i]) { continue; @@ -600,20 +587,21 @@ namespace storm { } } - //create equitation solver + //create equitation solver storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, dir); + requirements.clearBounds(); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); - + */ std::unique_ptr> solver; - if (probSize != 0) { + /*if (probSize != 0) { solver = minMaxLinearEquationSolverFactory.create(env, probMatrix); solver->setHasUniqueSolution(); solver->setBounds(storm::utility::zero(), storm::utility::one()); solver->setRequirementsChecked(); solver->setCachingEnabled(true); - } + } */ // while not close enough to precision: do { //logfile << "starting iteration\n"; @@ -690,8 +678,8 @@ namespace storm { 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 + printTransitions(N, maxNorm, fullTransitionMatrix, exitRate, markovianStates, psiStates, + relReachability, psiStates, psiStates, unifVectors, logfile); //TODO remove // (6) double lambda @@ -705,7 +693,7 @@ namespace storm { } } oldDiff = maxNorm; - //std::cout << "Finished Iteration for N = " << N << " with difference " << maxNorm << "\n"; + std::cout << "Finished Iteration for N = " << N << " with difference " << maxNorm << "\n"; } while (maxNorm > epsilon * (1 - kappa)); logfile.close();