Browse Source

refactor computation of relevantStates from BitVector method to logical AND

tempestpy_adaptions
Lukas Posch 4 years ago
parent
commit
318544a940
  1. 9
      src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
  2. 14
      src/storm/storage/BitVector.cpp
  3. 8
      src/storm/storage/BitVector.h

9
src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp

@ -28,13 +28,8 @@ namespace storm {
//STORM_LOG_DEBUG("psiStates: " << psiStates);
//STORM_LOG_DEBUG("~psiStates: " <<~psiStates);
// 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 relevantStates(phiStates.size());
// TODO: AND for Bitvectors already exists, try to use this instead:
// first: copy one Bitvector to relevantStates, second: logical AND with the other one.
relevantStates.setRelevantStates(phiStates, ~psiStates);
// relevant states are those states which are phiStates and not PsiStates
storm::storage::BitVector relevantStates = phiStates & ~psiStates;
STORM_LOG_DEBUG("relevant states: " << relevantStates);

14
src/storm/storage/BitVector.cpp

@ -1026,17 +1026,6 @@ 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;
@ -1049,9 +1038,6 @@ namespace storm {
}
}
void BitVector::truncateLastBucket() {
if ((bitCount & mod64mask) != 0) {
buckets[bucketCount() - 1] &= ~((1ll << (64 - (bitCount & mod64mask))) - 1ll);

8
src/storm/storage/BitVector.h

@ -536,14 +536,6 @@ 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.
*

Loading…
Cancel
Save