Browse Source

Added output functionality to bit vector and moved test-checking lines in storm.cpp to the right place.

tempestpy_adaptions
dehnert 12 years ago
parent
commit
7331544377
  1. 22
      src/storage/BitVector.h
  2. 4
      src/storm.cpp

22
src/storage/BitVector.h

@ -387,11 +387,11 @@ public:
* Returns the number of bits that are set (to one) in this bit vector.
* @return The number of bits that are set (to one) in this bit vector.
*/
uint_fast64_t getNumberOfSetBits() {
uint_fast64_t getNumberOfSetBits() const {
return getNumberOfSetBitsBeforeIndex(bucketCount << 6);
}
uint_fast64_t getNumberOfSetBitsBeforeIndex(uint_fast64_t index) {
uint_fast64_t getNumberOfSetBitsBeforeIndex(uint_fast64_t index) const {
uint_fast64_t result = 0;
// First, count all full buckets.
uint_fast64_t bucket = index >> 6;
@ -437,7 +437,7 @@ public:
/*!
* Retrieves the number of bits this bit vector can store.
*/
uint_fast64_t getSize() {
uint_fast64_t getSize() const {
return bitCount;
}
@ -445,7 +445,7 @@ public:
* Returns the size of the bit vector in memory measured in bytes.
* @return The size of the bit vector in memory measured in bytes.
*/
uint_fast64_t getSizeInMemory() {
uint_fast64_t getSizeInMemory() const {
return sizeof(*this) + sizeof(uint_fast64_t) * bucketCount;
}
@ -463,6 +463,20 @@ public:
return endIterator;
}
/*!
* Returns a string representation of the bit vector.
*/
std::string toString() const {
std::stringstream result;
result << "bit vector(" << this->getNumberOfSetBits() << ") [";
for (auto index : *this) {
result << index << " ";
}
result << "]";
return result.str();
}
private:
/*!

4
src/storm.cpp

@ -216,13 +216,13 @@ void testChecking() {
if (parser.getType() == storm::models::DTMC) {
std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
dtmc->printModelInformationToStream(std::cout);
}
else std::cout << "Input is not DTMC" << std::endl;
// testCheckingDie(*dtmc);
// testCheckingCrowds(*dtmc);
// testCheckingSynchronousLeader(*dtmc, 4);
}
else std::cout << "Input is not DTMC" << std::endl;
}
/*!
* Main entry point.

Loading…
Cancel
Save