diff --git a/src/mrmc.cpp b/src/mrmc.cpp index 67c772157..1233ff1e6 100644 --- a/src/mrmc.cpp +++ b/src/mrmc.cpp @@ -22,6 +22,7 @@ #include "src/models/AtomicPropositionsLabeling.h" #include "src/parser/readLabFile.h" #include "src/parser/readTraFile.h" +#include "src/solver/GraphAnalyzer.h" #include "src/utility/settings.h" #include "Eigen/Sparse" @@ -96,6 +97,9 @@ int main(const int argc, const char* argv[]) { dtmc.printModelInformationToStream(std::cout); + // mrmc::storage::BitVector AU(dtmc.getNumberOfStates()); + // mrmc::solver::GraphAnalyzer::getUniversalReachabilityStates(dtmc, mrmc::storage::BitVector(dtmc.getNumberOfStates(), true), *dtmc.getLabeledStates("elected"), AU); + if (s != nullptr) { delete s; } @@ -104,4 +108,3 @@ int main(const int argc, const char* argv[]) { return 0; } - diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index 8da13efeb..d5fb56c67 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -266,7 +266,7 @@ public: * of the two bit vectors. */ BitVector operator &=(const BitVector bv) { - uint_fast64_t minSize = ((bv.bitCount < this->bitCount) ? bv.bitCount : this->bitCount) >> 6; + uint_fast64_t minSize = (bv.bucketCount < this->bucketCount) ? bv.bucketCount : this->bucketCount; for (uint_fast64_t i = 0; i < minSize; ++i) { this->bucketArray[i] &= bv.bucketArray[i]; @@ -305,7 +305,7 @@ public: * of the two bit vectors. */ BitVector& operator |=(const BitVector bv) { - uint_fast64_t minSize = ((bv.bitCount < this->bitCount) ? bv.bitCount : this->bitCount) >> 6; + uint_fast64_t minSize = (bv.bucketCount < this->bucketCount) ? bv.bucketCount : this->bucketCount; for (uint_fast64_t i = 0; i < minSize; ++i) { this->bucketArray[i] |= bv.bucketArray[i];