introduced name relevantStates,

moved methods to Bitvector class

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<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(states, psiStates);
+                std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates);
 /*                std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(~psiStates, psiStates);
                 for(int counter = 0; counter < states.size(); counter++)
                 {
@@ -61,7 +61,7 @@ namespace storm {
                 //storm::storage::SparseMatrix<ValueType> 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<ValueType> submatrix = transitionMatrix.getSubmatrix(true, states, states, false);
+                storm::storage::SparseMatrix<ValueType> 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) {

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) {

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;