diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 609a03e94..8bd2ba44c 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -136,7 +136,7 @@ namespace storm { } template::SupportsExponential, int>::type= 0> - void SparseMarkovAutomatonCslHelper::printTransitions( + void SparseMarkovAutomatonCslHelper::printTransitions(const uint64_t N, ValueType const diff, storm::storage::SparseMatrix const &fullTransitionMatrix, std::vector const &exitRateVector, storm::storage::BitVector const &markovianStates, storm::storage::BitVector const &psiStates, std::vector> relReachability, @@ -169,19 +169,12 @@ namespace storm { } logfile << "\n"; - logfile << "probStates\tmarkovianStates\tgoalStates\tcycleStates\tcycleGoalStates\n"; + /*logfile << "probStates\tmarkovianStates\tgoalStates\tcycleStates\tcycleGoalStates\n"; for (int i =0 ; i< markovianStates.size() ; i++){ logfile << (~markovianStates)[i] << "\t\t" << markovianStates[i] << "\t\t" << psiStates[i] << "\t\t" << cycleStates[i] << "\t\t" << cycleGoalStates[i] << "\n"; - } - - for (int i =0; i> const &solver) { if (unifVectors[kind][k][node]!=-1){return;} - std::ofstream logfile("U+logfile.txt", std::ios::app); - logfile << "calculating vector " << kind << " for k = " << k << " node "<< node << " \t"; + //std::ofstream logfile("U+logfile.txt", std::ios::app); + //logfile << "calculating vector " << kind << " for k = " << k << " node "<< node << " \t"; auto probabilisticStates = ~markovianStates; auto numberOfProbStates = probabilisticStates.getNumberOfSetBits(); @@ -266,7 +259,7 @@ namespace storm { // First Case, k==N, independent from kind of state if (k==N){ - logfile << "k == N! res = 0\n"; + //logfile << "k == N! res = 0\n"; unifVectors[kind][k][node]=0; return; } @@ -285,14 +278,14 @@ namespace storm { // WU unifVectors[kind][k][node]=1; } - logfile << "goal state node " << node << " res = " << res << "\n"; + //logfile << "goal state node " << node << " res = " << res << "\n"; return; } //markovian non-goal State if (markovianStates[node]){ - logfile << "markovian state: "; + //logfile << "markovian state: "; res = 0; auto line = fullTransitionMatrix.getRow(rowGroupIndices[node]); for (auto &element : line){ @@ -303,13 +296,13 @@ namespace storm { res+=element.getValue()*unifVectors[kind][k+1][to]; } unifVectors[kind][k][node]=res; - logfile << " res = " << res << "\n"; + //logfile << " res = " << res << "\n"; return; } //probabilistic non-goal State if (probabilisticStates[node]){ - logfile << "probabilistic state: "; + //logfile << "probabilistic state: "; std::vector b(probSize, 0), x(numberOfProbStates,0); //calculate b uint64_t lineCounter=0; @@ -347,7 +340,7 @@ namespace storm { unifVectors[kind][k][trueI]=x[i]; } - logfile << " res = " << unifVectors[kind][k][node] << " but calculated more \n"; + //logfile << " res = " << unifVectors[kind][k][node] << " but calculated more \n"; } //end probabilistic states } @@ -610,7 +603,7 @@ namespace storm { maxNorm = std::max(maxNorm, diff); } } - printTransitions(fullTransitionMatrix,exitRate,markovianStates,psiStates,relReachability,psiStates, psiStates,unifVectors); //TODO remove + printTransitions(N, maxNorm, fullTransitionMatrix,exitRate,markovianStates,psiStates,relReachability,psiStates, psiStates,unifVectors); //TODO remove // (6) double lambda diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h index 3d5b8d049..49970334b 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h @@ -112,7 +112,7 @@ namespace storm { */ template ::SupportsExponential, int>::type=0> - static void printTransitions(storm::storage::SparseMatrix const& fullTransitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, + static void printTransitions(const uint64_t N, ValueType const diff, storm::storage::SparseMatrix const& fullTransitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::vector> relReachability, storm::storage::BitVector const& cycleStates , storm::storage::BitVector const& cycleGoalStates ,std::vector>>& unifVectors);