From 781f105ca13983189b5531b3254c5aa7301b3b7d Mon Sep 17 00:00:00 2001 From: Lukas Posch Date: Thu, 11 Feb 2021 17:42:39 +0100 Subject: [PATCH] introduced name relevantStates, moved methods to Bitvector class --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 27 ++++++++++--------- src/storm/storage/BitVector.cpp | 25 +++++++++++++++++ src/storm/storage/BitVector.h | 16 +++++++++++ 3 files changed, 56 insertions(+), 12 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index cbbcbed3e..57ea8ba29 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -30,20 +30,20 @@ namespace storm { // states are those states which are phiStates and not PsiStates // so that we can not only leave out the PsiStates in the matrix, but also leave out those which are not in the phiStates - storm::storage::BitVector states(phiStates.size()); - for(int counter = 0; counter < states.size(); counter++) + storm::storage::BitVector relevantStates(phiStates.size()); + relevantStates.setRelevantStates(phiStates, ~psiStates); + +/* for(int counter = 0; counter < states.size(); counter++) { if(phiStates.get(counter) && !psiStates.get(counter)) { states.set(counter); } - } + }*/ - STORM_LOG_DEBUG("states are " << states); + STORM_LOG_DEBUG("relevant states are " << relevantStates); - // TRY to change b to the new states - // TODO: only states in the phiStates can be chosen as initial states, e.g. the output is for initial states = 0, 1, 4 - std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(states, psiStates); + std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates); /* std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(~psiStates, psiStates); for(int counter = 0; counter < states.size(); counter++) { @@ -61,7 +61,7 @@ namespace storm { //storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, ~psiStates, ~psiStates, false); // Reduce TRY to use only the states from phi which satisfy the left side and psi which satisfy the right side - storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, states, states, false); + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); //STORM_LOG_DEBUG("\n" << submatrix); //STORM_LOG_DEBUG("x = " << storm::utility::vector::toString(x)); @@ -72,15 +72,17 @@ namespace storm { //STORM_LOG_DEBUG(statesOfCoalition); //STORM_LOG_DEBUG(clippedStatesOfCoalition); - // TODO move this to BitVector-class - auto clippedStatesCounter = 0; +/* auto clippedStatesCounter = 0; for(uint i = 0; i < psiStates.size(); i++) { std::cout << i << " : " << psiStates.get(i) << " -> " << statesOfCoalition[i] << std::endl; if(!psiStates.get(i)) { clippedStatesOfCoalition.set(clippedStatesCounter, statesOfCoalition[i]); clippedStatesCounter++; } - } + }*/ + + clippedStatesOfCoalition.setClippedStatesOfCoalition(psiStates, statesOfCoalition); + //STORM_LOG_DEBUG(clippedStatesOfCoalition); clippedStatesOfCoalition.complement(); //STORM_LOG_DEBUG(clippedStatesOfCoalition); @@ -93,7 +95,8 @@ namespace storm { viHelper.performValueIteration(env, x, b, goal.direction()); - // TODO: here is the debug output for all states, should I fill up the vector again with 0 for the states i left out? + // TODO: here is the debug output for all states, should I fill up the vector again with 0 for the states i left out + // e.g. phi states are [ 2 3 ], the probability output is for the first state (state 2) but the initial sate is 0 STORM_LOG_DEBUG(storm::utility::vector::toString(x)); if (produceScheduler) { diff --git a/src/storm/storage/BitVector.cpp b/src/storm/storage/BitVector.cpp index f2a716038..9b5db6834 100644 --- a/src/storm/storage/BitVector.cpp +++ b/src/storm/storage/BitVector.cpp @@ -1026,6 +1026,31 @@ namespace storm { } } + void BitVector::setRelevantStates(BitVector bitVector1, BitVector bitVector2) + { + for(int counter = 0; counter < this->size(); counter++) + { + if(bitVector1.get(counter) && bitVector2.get(counter)) + { + this->set(counter); + } + } + } + + void BitVector::setClippedStatesOfCoalition(BitVector psiStates, BitVector statesOfCoalition) + { + auto clippedStatesCounter = 0; + for(uint i = 0; i < psiStates.size(); i++) { + std::cout << i << " : " << psiStates.get(i) << " -> " << statesOfCoalition[i] << std::endl; + if(!psiStates.get(i)) { + this->set(clippedStatesCounter, statesOfCoalition[i]); + clippedStatesCounter++; + } + } + } + + + void BitVector::truncateLastBucket() { if ((bitCount & mod64mask) != 0) { diff --git a/src/storm/storage/BitVector.h b/src/storm/storage/BitVector.h index 323020b48..fc49999b8 100644 --- a/src/storm/storage/BitVector.h +++ b/src/storm/storage/BitVector.h @@ -536,6 +536,22 @@ namespace storm { */ bool compareAndSwap(uint_fast64_t start1, uint_fast64_t start2, uint_fast64_t length); + /*! + * Compare two bitvectors and set the bits which are set in both of them. + * + * @param bitVector1 First Source for comparison. + * @param bitVector2 Second Source for comparison. + */ + void setRelevantStates(BitVector bitVector1, BitVector bitVector2); + + /*! + * Set clipped states of coalition for all states which are not in the winning region. + * + * @param psiStates Bitvector of states which are in the winning region. + * @param statesOfCoalition Bitvector of states which belong to the coalition. + */ + void setClippedStatesOfCoalition(BitVector psiStates, BitVector statesOfCoalition); + friend std::ostream& operator<<(std::ostream& out, BitVector const& bitVector); void store(std::ostream&) const;