diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index de2459647..609a03e94 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -258,6 +258,7 @@ namespace storm { logfile << "calculating vector " << kind << " for k = " << k << " node "<< node << " \t"; auto probabilisticStates = ~markovianStates; + auto numberOfProbStates = probabilisticStates.getNumberOfSetBits(); auto numberOfStates=fullTransitionMatrix.getRowGroupCount(); uint64_t N = unifVectors[kind].size()-1; auto const& rowGroupIndices = fullTransitionMatrix.getRowGroupIndices(); @@ -309,7 +310,7 @@ namespace storm { //probabilistic non-goal State if (probabilisticStates[node]){ logfile << "probabilistic state: "; - std::vector b(probSize, 0), x(probabilisticStates.getNumberOfSetBits(),0); + std::vector b(probSize, 0), x(numberOfProbStates,0); //calculate b uint64_t lineCounter=0; for (int i =0; i exitRate{exitRateVector}; typename storm::storage::SparseMatrix fullTransitionMatrix = transitionMatrix.getSubmatrix(true, allStates , allStates , true); + // delete diagonals + deleteProbDiagonals(fullTransitionMatrix, markovianStates); typename storm::storage::SparseMatrix probMatrix{}; uint64_t probSize =0; if (probabilisticStates.getNumberOfSetBits()!=0){ //work around in case there are no prob states @@ -518,6 +522,7 @@ namespace storm { std::vector> relReachability(fullTransitionMatrix.getRowCount(),in); + //calculate relative reachability for(uint64_t i=0 ; i