Implemented Prob1E algorithm for nondeterministic models. Added comparison operator to bit vector.

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.
@@ -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<uint_fast64_t>& list) const {
+	void addSetIndicesToList(std::vector<uint_fast64_t>& list) const {
 		for (auto index : *this) {
 			list.push_back(index);
 		}

src/storm.cpp

@@ -215,8 +215,6 @@ void testCheckingDice(storm::models::Mdp<double>& 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;
 }

src/utility/GraphAnalyzer.h

@@ -79,7 +79,7 @@ public:
 		// Initialize the stack used for the DFS with the states
 		std::vector<uint_fast64_t> 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<uint_fast64_t> stack;
 		stack.reserve(model.getNumberOfStates());
-		psiStates.getList(stack);
+		psiStates.addSetIndicesToList(stack);
 
 		// Perform the actual DFS.
 		while(!stack.empty()) {
@@ -202,7 +202,71 @@ public:
 
 	template <class T>
 	static void performProb1E(storm::models::AbstractNondeterministicModel<T>& 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<storm::storage::SparseMatrix<T>> transitionMatrix = model.getTransitionMatrix();
+		std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices();
+
+		// Get the backwards transition relation from the model to ease the search.
+		storm::models::GraphTransitions<T> backwardTransitions(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), false);
+
+		storm::storage::BitVector* currentStates = new storm::storage::BitVector(model.getNumberOfStates(), true);
+
+		std::vector<uint_fast64_t> 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 <class T>
@@ -230,6 +294,7 @@ public:
 			throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability0' must not be null.");
 		}
 
+		// Get some temporaries for convenience.
 		std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix = model.getTransitionMatrix();
 		std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices();
 
@@ -242,7 +307,7 @@ public:
 		// Initialize the stack used for the DFS with the states
 		std::vector<uint_fast64_t> stack;
 		stack.reserve(model.getNumberOfStates());
-		psiStates.getList(stack);
+		psiStates.addSetIndicesToList(stack);
 
 		// Perform the actual DFS.
 		while(!stack.empty()) {