diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index bd2c99760..de2459647 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -134,14 +134,23 @@ namespace storm { void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded reachability probabilities is unsupported for this value type."); } - - template ::SupportsExponential, int>::type> - void SparseMarkovAutomatonCslHelper::printTransitions(std::vector> relReachability, std::vector const& exitRateVector, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& cycleStates, storm::storage::BitVector const& cycleGoalStates, std::vector>& vd, std::vector>& vu, std::vector>& wu){ + + template::SupportsExponential, int>::type= 0> + void SparseMarkovAutomatonCslHelper::printTransitions( + storm::storage::SparseMatrix const &fullTransitionMatrix, + std::vector const &exitRateVector, storm::storage::BitVector const &markovianStates, + storm::storage::BitVector const &psiStates, std::vector> relReachability, + const storage::BitVector &cycleStates, const storage::BitVector &cycleGoalStates, + std::vector>> &unifVectors) { + + + std::ofstream logfile("U+logfile.txt", std::ios::app); - + auto const& rowGroupIndices = fullTransitionMatrix.getRowGroupIndices(); auto numberOfStates = fullTransitionMatrix.getRowGroupCount(); + //Transition Matrix logfile << "number of states = num of row group count " << numberOfStates << "\n"; for (uint_fast64_t i = 0; i < fullTransitionMatrix.getRowGroupCount(); i++) { logfile << " from node " << i << " "; @@ -161,8 +170,8 @@ namespace storm { logfile << "\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< 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::SupportsExponential, int>::type> - void SparseMarkovAutomatonCslHelper::calculateVu(std::vector> const& relativeReachability, OptimizationDirection dir, uint64_t k, uint64_t node, ValueType lambda, std::vector>& vu, std::vector>& wu, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::unique_ptr> const& solver){ - if (vu[k][node]!=-1){return;} //dynamic programming. avoiding multiple calculation. - uint64_t N = vu.size()-1; + void SparseMarkovAutomatonCslHelper::calculateVu(std::vector> const& relativeReachability, OptimizationDirection dir, uint64_t k, uint64_t node, uint64_t const kind, ValueType lambda, uint64_t probSize, std::vector>>& unifVectors, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::unique_ptr> const& solver){ + if (unifVectors[1][k][node]!=-1){return;} //dynamic programming. avoiding multiple calculation. + uint64_t N = unifVectors[1].size()-1; auto rowGroupIndices = fullTransitionMatrix.getRowGroupIndices(); ValueType res =0; for (uint64_t i = k ; i < N ; i++ ){ - if (wu[N-1-(i-k)][node]==-1){ - calculateWu(relativeReachability, dir, (N-1-(i-k)),node,lambda,wu,fullTransitionMatrix,markovianStates,psiStates, solver); + if (unifVectors[2][N-1-(i-k)][node]==-1){ + calculateUnifPlusVector(N-1-(i-k),node,2,lambda,probSize,relativeReachability,dir,unifVectors,fullTransitionMatrix, markovianStates,psiStates,solver); + //old: relativeReachability, dir, (N-1-(i-k)),node,lambda,wu,fullTransitionMatrix,markovianStates,psiStates, solver); } - res+=poisson(lambda, i)*wu[N-1-(i-k)][node]; + res+=poisson(lambda, i)*unifVectors[2][N-1-(i-k)][node]; } - vu[k][node]=res; + unifVectors[1][k][node]=res; } - template ::SupportsExponential, int>::type> - void SparseMarkovAutomatonCslHelper::calculateWu(std::vector> const& relativeReachability, OptimizationDirection dir, uint64_t k, uint64_t node, ValueType lambda, std::vector>& wu, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::unique_ptr> const& solver){ - if (wu[k][node]!=-1){return;} //dynamic programming. avoiding multiple calculation. - - std::ofstream logfile("U+logfile.txt", std::ios::app); - - auto probabilisticStates = ~markovianStates; - uint64_t N = wu.size()-1; - auto const& rowGroupIndices = fullTransitionMatrix.getRowGroupIndices( ); - ValueType res; - if (k==N){ - wu[k][node]=0; - return; - } - if (psiStates[node]){ - wu[k][node]=1; - return; - } + template::SupportsExponential, int>::type= 0> + void SparseMarkovAutomatonCslHelper::calculateUnifPlusVector(uint64_t k, uint64_t node, uint64_t const kind, ValueType lambda, uint64_t probSize, + std::vector> const &relativeReachability, + OptimizationDirection dir, + std::vector>> &unifVectors, + storm::storage::SparseMatrix const &fullTransitionMatrix, + storm::storage::BitVector const &markovianStates, + storm::storage::BitVector const &psiStates, + std::unique_ptr> const &solver) { - if (markovianStates[node]){ - res = 0; - auto line = fullTransitionMatrix.getRow(rowGroupIndices[node]); - for (auto &element : line){ - uint64_t to = element.getColumn(); - if (wu[k+1][to]==-1){ - calculateWu(relativeReachability, dir, k+1,to,lambda,wu,fullTransitionMatrix,markovianStates,psiStates, solver); - } - res+=element.getValue()*wu[k+1][to]; - } - wu[k][node]=res; - } else { - // applying simpleMDP stuff - auto numberOfStates=relativeReachability[0].size(); - typename storm::storage::SparseMatrix probMatrix = fullTransitionMatrix.getSubmatrix(true, ~markovianStates , ~markovianStates, true); - auto probSize = probMatrix.getRowGroupCount(); - std::vector b(probMatrix.getRowCount(), 0), x(probSize,0); - - //calculate b - uint64_t lineCounter=0; - for (int i =0; isolveEquations(dir, x, b); - - for (uint64_t i =0 ; i::SupportsExponential, int>::type> - void SparseMarkovAutomatonCslHelper::calculateVd(std::vector> const& relativeReachability, OptimizationDirection dir, uint64_t k, uint64_t node, ValueType lambda, std::vector>& vd, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::unique_ptr> 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"; auto probabilisticStates = ~markovianStates; - - if (vd[k][node]!=-1){return;} //dynamic programming. avoiding multiple calculation. - logfile << "calculating vd for k = " << k << " node "<< node << " \t"; - uint64_t N = vd.size()-1; + auto numberOfStates=fullTransitionMatrix.getRowGroupCount(); + uint64_t N = unifVectors[kind].size()-1; auto const& rowGroupIndices = fullTransitionMatrix.getRowGroupIndices(); - ValueType res; + + // First Case, k==N, independent from kind of state if (k==N){ logfile << "k == N! res = 0\n"; - vd[k][node]=0; + unifVectors[kind][k][node]=0; return; } - + //goal state if (psiStates[node]){ - res = storm::utility::zero(); - for (uint64_t i = k ; i(); + for (uint64_t i = k ; i probMatrix = fullTransitionMatrix.getSubmatrix(true, ~markovianStates , ~markovianStates, true); - auto probSize = probMatrix.getRowGroupCount(); - std::vector b(probMatrix.getRowCount(), 0), x(probSize,0); + return; + } + //probabilistic non-goal State + if (probabilisticStates[node]){ + logfile << "probabilistic state: "; + std::vector b(probSize, 0), x(probabilisticStates.getNumberOfSetBits(),0); //calculate b uint64_t lineCounter=0; - for (int i =0; isolveEquations(dir, x, b); - logfile << "vd goal vector x is \n"; - for (int i =0 ; i::SupportsExponential, int>::type=0> uint64_t SparseMarkovAutomatonCslHelper::trajans(storm::storage::SparseMatrix const& transitionMatrix, uint64_t node, std::vector& disc, std::vector& finish, uint64_t* counter) { auto const& rowGroupIndice = transitionMatrix.getRowGroupIndices(); @@ -585,24 +475,29 @@ namespace storm { std::vector SparseMarkovAutomatonCslHelper::unifPlus(OptimizationDirection dir, std::pair const& boundsPair, std::vector const& exitRateVector, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory){ STORM_LOG_TRACE("Using UnifPlus to compute bounded until probabilities."); - std::ofstream logfile("U+logfile.txt", std::ios::app); - ValueType maxNorm = 0; + ValueType maxNorm = storm::utility::zero(); //bitvectors to identify different kind of states storm::storage::BitVector allStates(markovianStates.size(), true); - auto probabilisticStates = ~markovianStates; + storm::storage::BitVector probabilisticStates = ~markovianStates; //vectors to save calculation std::vector> vd,vu,wu; + std::vector>> unifVectors{}; //transition matrix with diagonal entries. The values can be changed during uniformisation std::vector exitRate{exitRateVector}; typename storm::storage::SparseMatrix fullTransitionMatrix = transitionMatrix.getSubmatrix(true, allStates , allStates , true); - typename storm::storage::SparseMatrix probMatrix = fullTransitionMatrix.getSubmatrix(true, ~markovianStates , ~markovianStates, true); + typename storm::storage::SparseMatrix probMatrix{}; + uint64_t probSize =0; + if (probabilisticStates.getNumberOfSetBits()!=0){ //work around in case there are no prob states + probMatrix = fullTransitionMatrix.getSubmatrix(true, probabilisticStates , probabilisticStates, true); + probSize = probMatrix.getRowCount(); + } - auto rowGroupIndices = fullTransitionMatrix.getRowGroupIndices(); + auto& rowGroupIndices = fullTransitionMatrix.getRowGroupIndices(); //(1) define horizon, epsilon, kappa , N, lambda, @@ -616,13 +511,14 @@ namespace storm { } uint64_t N; + + //calculate relative ReachabilityVectors std::vector in(numberOfStates, 0); std::vector> relReachability(fullTransitionMatrix.getRowCount(),in); - printTransitions(relReachability, exitRateVector, fullTransitionMatrix, markovianStates, psiStates, psiStates, psiStates, vd,vu,wu); // TODO: delete when develepmont is finished - //calculate relative reachability + //calculate relative reachability for(uint64_t i=0 ; i> solver = minMaxLinearEquationSolverFactory.create(probMatrix); - - solver->setHasUniqueSolution(); - solver->setBounds(storm::utility::zero(), storm::utility::one()); - solver->setRequirementsChecked(); - solver->setCachingEnabled(true); - - - printTransitions(relReachability, exitRateVector, fullTransitionMatrix, markovianStates, psiStates, psiStates, psiStates, vd,vu,wu); // TODO: delete when develepmont is finished + std::unique_ptr> solver; + if (probSize!=0){ + solver = minMaxLinearEquationSolverFactory.create(probMatrix); + solver->setHasUniqueSolution(); + solver->setBounds(storm::utility::zero(), storm::utility::one()); + solver->setRequirementsChecked(); + solver->setCachingEnabled(true); + } // while not close enough to precision: do { // (2) update parameter @@ -692,29 +587,37 @@ namespace storm { vd = std::vector> (N + 1, init); vu = std::vector> (N + 1, init); wu = std::vector> (N + 1, init); - + unifVectors.clear(); + unifVectors.push_back(vd); + unifVectors.push_back(vd); + unifVectors.push_back(vd); + + printTransitions(fullTransitionMatrix,exitRate,markovianStates,psiStates,relReachability,psiStates, psiStates,unifVectors); //TODO remove + + //define 0=vd 1=vu 2=wu // (5) calculate vectors and maxNorm for (uint64_t i = 0; i < numberOfStates; i++) { for (uint64_t k = N; k <= N; k--) { - calculateVd(relReachability, dir, k, i, T*lambda, vd, fullTransitionMatrix, markovianStates, psiStates, solver); - calculateWu(relReachability, dir, k, i, T*lambda, wu, fullTransitionMatrix, markovianStates, psiStates, solver); - calculateVu(relReachability, dir, k, i, T*lambda, vu, wu, fullTransitionMatrix, markovianStates, psiStates, solver); - //also use iteration to keep maxNorm of vd and vu up to date, so the loop-condition is easy to prove - ValueType diff = std::abs(vd[k][i]-vu[k][i]); + calculateUnifPlusVector(k,i,0,lambda,probSize,relReachability,dir,unifVectors,fullTransitionMatrix,markovianStates,psiStates,solver); + calculateUnifPlusVector(k,i,2,lambda,probSize,relReachability,dir,unifVectors,fullTransitionMatrix,markovianStates,psiStates,solver); + calculateVu(relReachability,dir,k,i,1,lambda,probSize,unifVectors,fullTransitionMatrix,markovianStates,psiStates,solver); + //also use iteration to keep maxNorm of vd and vup to date, so the loop-condition is easy to prove + ValueType diff = std::abs(unifVectors[0][k][i]-unifVectors[1][k][i]); maxNorm = std::max(maxNorm, diff); } } - - printTransitions(relReachability, exitRateVector, fullTransitionMatrix, markovianStates, psiStates, psiStates, psiStates, vd,vu,wu); // TODO: delete when develepmont is finished + std::cout << "\nTBU was " << unifVectors[0][0][0] << "\n"; + printTransitions(fullTransitionMatrix,exitRate,markovianStates,psiStates,relReachability,psiStates, psiStates,unifVectors); //TODO remove - // (6) double lambda + // (6) double lambda lambda=2*lambda; } while (maxNorm>epsilon*(1-kappa)); - return vd[0]; + + return unifVectors[0][0]; } template ::SupportsExponential, int>::type> @@ -1234,7 +1137,7 @@ namespace storm { return v.front() * uniformizationRate; } - + template std::vector SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template std::vector SparseMarkovAutomatonCslHelper::computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h index d378ded43..3d5b8d049 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h @@ -56,6 +56,8 @@ namespace storm { static std::vector computeReachabilityTimes(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); private: + template ::SupportsExponential, int>::type=0> + static void calculateUnifPlusVector(uint64_t k, uint64_t node, uint64_t const kind, ValueType lambda, uint64_t probSize, std::vector> const& relativeReachability, OptimizationDirection dir, std::vector>>& unifVectors, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::unique_ptr> const& solver); template ::SupportsExponential, int>::type=0> static void deleteProbDiagonals(storm::storage::SparseMatrix& transitionMatrix, storm::storage::BitVector const& markovianStates); @@ -93,27 +95,15 @@ namespace storm { template ::SupportsExponential, int>::type=0> static uint64_t trajans(storm::storage::SparseMatrix const& TransitionMatrix, uint64_t node, std::vector& disc, std::vector& finish, uint64_t * counter); - /*! - * Computes vd vector according to UnifPlus - * - */ - template ::SupportsExponential, int>::type=0> - static void calculateVd(std::vector> const& relativeReachability, OptimizationDirection dir, uint64_t k, uint64_t node, ValueType lambda, std::vector>& vd, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::unique_ptr> const& solver); - -/*! + /* * Computes vu vector according to UnifPlus * */ template ::SupportsExponential, int>::type=0> - static void calculateVu(std::vector> const& relativeReachability, OptimizationDirection dir, uint64_t k, uint64_t node, ValueType lambda, std::vector>& vu, std::vector>& wu, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::unique_ptr> const& solver); + static void calculateVu(std::vector> const& relativeReachability, OptimizationDirection dir, uint64_t k, uint64_t node, uint64_t const kind, ValueType lambda, uint64_t probSize, std::vector>>& unifVectors, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::unique_ptr> const& solver); + - /*! - * Computes wu vector according to UnifPlus - * - */ - template ::SupportsExponential, int>::type=0> - static void calculateWu(std::vector> const& relativeReachability, OptimizationDirection dir, uint64_t k, uint64_t node, ValueType lambda, std::vector>& wu, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::unique_ptr> const& solver); /*! * Prints the TransitionMatrix and the vectors vd, vu, wu to the logfile @@ -122,7 +112,9 @@ namespace storm { */ template ::SupportsExponential, int>::type=0> - static void printTransitions(std::vector> relReachability, std::vector const& exitRateVector, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& cycleStates, storm::storage::BitVector const& cycleGoalStates, std::vector>& vd, std::vector>& vu, std::vector>& wu); + static void printTransitions(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); template ::SupportsExponential, int>::type = 0> static void computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory);