diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index df3f86600..801ec2bb2 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -136,7 +136,7 @@ public: * Copy Constructor. Performs a deep copy of the given bit vector. * @param bv A reference to the bit vector to be copied. */ - BitVector(const BitVector &bv) : bucketCount(bv.bucketCount), bitCount(bv.bitCount), endIterator(*this, bitCount, bitCount, false), truncateMask((1ll << (bitCount & mod64mask)) - 1ll) { + BitVector(BitVector const& bv) : bucketCount(bv.bucketCount), bitCount(bv.bitCount), endIterator(*this, bitCount, bitCount, false), truncateMask((1ll << (bitCount & mod64mask)) - 1ll) { LOG4CPLUS_WARN(logger, "Invoking copy constructor."); bucketArray = new uint64_t[bucketCount]; std::copy(bv.bucketArray, bv.bucketArray + this->bucketCount, this->bucketArray); @@ -152,6 +152,25 @@ public: } } + // Equality Operator + /*! + * Compares the given bit vector with the current one. + */ + bool operator==(BitVector const& bv) { + // If the lengths of the vectors do not match, they are considered unequal. + if (this->bitCount != bv.bitCount) return false; + + // If the lengths match, we compare the buckets one by one. + for (uint_fast64_t index = 0; index < this->bucketCount; ++index) { + if (this->bucketArray[index] != bv.bucketArray[index]) { + return false; + } + } + + // All buckets were equal, so the bit vectors are equal. + return true; + } + //! Assignment Operator /*! * Assigns the given bit vector to the current bit vector by a deep copy. @@ -159,7 +178,7 @@ public: * @return A reference to this bit vector after it has been assigned the * given bit vector by means of a deep copy. */ - BitVector& operator=(const BitVector& bv) { + BitVector& operator=(BitVector const& bv) { if (this->bucketArray != nullptr) { delete[] this->bucketArray; } @@ -239,7 +258,7 @@ public: * @param bv A reference to the bit vector to use for the operation. * @return A bit vector corresponding to the logical "and" of the two bit vectors. */ - BitVector operator &(const BitVector &bv) const { + BitVector operator&(BitVector const& bv) const { uint_fast64_t minSize = (bv.bitCount < this->bitCount) ? bv.bitCount : this->bitCount; // Create resulting bit vector and perform the operation on the individual elements. @@ -259,7 +278,7 @@ public: * @return A reference to the current bit vector corresponding to the logical "and" * of the two bit vectors. */ - BitVector operator &=(const BitVector bv) { + BitVector operator&=(BitVector const& bv) { uint_fast64_t minSize = (bv.bucketCount < this->bucketCount) ? bv.bucketCount : this->bucketCount; for (uint_fast64_t i = 0; i < minSize; ++i) { @@ -276,7 +295,7 @@ public: * @param bv A reference to the bit vector to use for the operation. * @return A bit vector corresponding to the logical "or" of the two bit vectors. */ - BitVector operator |(const BitVector &bv) const { + BitVector operator|(BitVector const& bv) const { uint_fast64_t minSize = (bv.bitCount < this->bitCount) ? bv.bitCount : this->bitCount; // Create resulting bit vector and perform the operation on the individual elements. @@ -297,7 +316,7 @@ public: * @return A reference to the current bit vector corresponding to the logical "or" * of the two bit vectors. */ - BitVector& operator |=(const BitVector bv) { + BitVector& operator|=(BitVector const& bv) { uint_fast64_t minSize = (bv.bucketCount < this->bucketCount) ? bv.bucketCount : this->bucketCount; for (uint_fast64_t i = 0; i < minSize; ++i) { @@ -315,7 +334,7 @@ public: * @param bv A reference to the bit vector to use for the operation. * @return A bit vector corresponding to the logical "xor" of the two bit vectors. */ - BitVector operator ^(const BitVector &bv) const { + BitVector operator^(BitVector const& bv) const { uint_fast64_t minSize = (bv.bitCount < this->bitCount) ? bv.bitCount : this->bitCount; // Create resulting bit vector and perform the operation on the individual elements. @@ -332,7 +351,7 @@ public: * Performs a logical "not" on the bit vector. * @return A bit vector corresponding to the logical "not" of the bit vector. */ - BitVector operator ~() const { + BitVector operator~() const { // Create resulting bit vector and perform the operation on the individual elements. BitVector result(this->bitCount); for (uint_fast64_t i = 0; i < this->bucketCount; ++i) { @@ -360,7 +379,7 @@ public: * @param bv A reference to the bit vector to use for the operation. * @return A bit vector corresponding to the logical "implies" of the two bit vectors. */ - BitVector implies(const BitVector& bv) const { + BitVector implies(BitVector const& bv) const { uint_fast64_t minSize = (bv.bitCount < this->bitCount) ? bv.bitCount : this->bitCount; // Create resulting bit vector and perform the operation on the individual elements. @@ -377,7 +396,7 @@ public: * Adds all indices of bits set to one to the provided list. * @param list The list to which to append the indices. */ - void getList(std::vector& list) const { + void addSetIndicesToList(std::vector& list) const { for (auto index : *this) { list.push_back(index); } diff --git a/src/storm.cpp b/src/storm.cpp index 77e58fd52..326b86e96 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -215,8 +215,6 @@ void testCheckingDice(storm::models::Mdp& mdp) { storm::utility::GraphAnalyzer::performProb01Max(mdp, *trueStates, *targetStates, statesWithProbability0, statesWithProbability1); - std::cout << statesWithProbability0->toString() << std::endl << statesWithProbability1->toString() << std::endl; - delete statesWithProbability0; delete statesWithProbability1; delete trueStates; @@ -255,10 +253,15 @@ int main(const int argc, const char* argv[]) { if (!parseOptions(argc, argv)) { return 0; } + + LOG4CPLUS_INFO(logger, "StoRM was invoked."); printHeader(argc, argv); testChecking(); cleanUp(); + + LOG4CPLUS_INFO(logger, "StoRM quit."); + return 0; } diff --git a/src/utility/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h index 9806077a2..f104465b0 100644 --- a/src/utility/GraphAnalyzer.h +++ b/src/utility/GraphAnalyzer.h @@ -79,7 +79,7 @@ public: // Initialize the stack used for the DFS with the states std::vector stack; stack.reserve(model.getNumberOfStates()); - psiStates.getList(stack); + psiStates.addSetIndicesToList(stack); // Perform the actual DFS. while(!stack.empty()) { @@ -182,7 +182,7 @@ public: // Initialize the stack used for the DFS with the states std::vector stack; stack.reserve(model.getNumberOfStates()); - psiStates.getList(stack); + psiStates.addSetIndicesToList(stack); // Perform the actual DFS. while(!stack.empty()) { @@ -202,7 +202,71 @@ public: template static void performProb1E(storm::models::AbstractNondeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) { + // Check for valid parameters. + if (statesWithProbability1 == nullptr) { + LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null."); + throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability1' must not be null."); + } + + // Get some temporaries for convenience. + std::shared_ptr> transitionMatrix = model.getTransitionMatrix(); + std::shared_ptr> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); + + // Get the backwards transition relation from the model to ease the search. + storm::models::GraphTransitions backwardTransitions(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), false); + + storm::storage::BitVector* currentStates = new storm::storage::BitVector(model.getNumberOfStates(), true); + + std::vector stack; + stack.reserve(model.getNumberOfStates()); + + bool done = false; + while (!done) { + stack.clear(); + storm::storage::BitVector* nextStates = new storm::storage::BitVector(psiStates); + psiStates.addSetIndicesToList(stack); + + while (!stack.empty()) { + uint_fast64_t currentState = stack.back(); + stack.pop_back(); + + for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) { + if (phiStates.get(*it) && !nextStates->get(*it)) { + + // Check whether the predecessor has at only successors in the current state set for one of the + // nondeterminstic choices. + for (auto rowIt = nondeterministicChoiceIndices->begin() + *it; rowIt != nondeterministicChoiceIndices->begin() + *it + 1; ++rowIt) { + bool allSuccessorsInCurrentStates = true; + for (auto colIt = transitionMatrix->beginConstColumnIterator(*rowIt); colIt != transitionMatrix->endConstColumnIterator(*rowIt); ++colIt) { + if (currentStates->get(*colIt)) { + allSuccessorsInCurrentStates = false; + break; + } + } + + // If all successors for a given nondeterministic choice are in the current state set, we + // add it to the set of states for the next iteration and perform a backward search from + // that state. + if (allSuccessorsInCurrentStates) { + nextStates->set(*it, true); + stack.push_back(*it); + break; + } + } + } + } + } + + // Check whether we need to perform an additional iteration. + if (*currentStates == *nextStates) { + done = true; + } else { + *currentStates = *nextStates; + } + } + *statesWithProbability1 = *currentStates; + delete currentStates; } template @@ -230,6 +294,7 @@ public: throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability0' must not be null."); } + // Get some temporaries for convenience. std::shared_ptr> transitionMatrix = model.getTransitionMatrix(); std::shared_ptr> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); @@ -242,7 +307,7 @@ public: // Initialize the stack used for the DFS with the states std::vector stack; stack.reserve(model.getNumberOfStates()); - psiStates.getList(stack); + psiStates.addSetIndicesToList(stack); // Perform the actual DFS. while(!stack.empty()) {