Added backwards transitions class. Small refactorings. Had to comment out some parts in utility.cpp and read_tra_file_test.cpp because they do not compile and seem to not be compliant with the current version in the repository.

src/models/atomic_propositions_labeling.h

@@ -135,28 +135,28 @@ public:
 	/*!
 	 * Adds an atomic proposition to a given state.
 	 * @param ap The name of the atomic proposition.
-	 * @param node The index of the state to label.
+	 * @param state The index of the state to label.
 	 */
-	void addAtomicPropositionToState(std::string ap, const uint_fast32_t state_index) {
+	void addAtomicPropositionToState(std::string ap, const uint_fast32_t state) {
 		if (name_to_labeling_map.count(ap) == 0) {
 			throw std::out_of_range("Atomic Proposition '" + ap + "' unknown.");
 		}
-		if (state_index >= state_count) {
+		if (state >= state_count) {
 			throw std::out_of_range("State index out of range.");
 		}
-		this->single_labelings[name_to_labeling_map[ap]]->addLabelToState(state_index);
+		this->single_labelings[name_to_labeling_map[ap]]->addLabelToState(state);
 	}
 
 	/*!
 	 * Checks whether a given state is labeled with the given atomic proposition.
 	 * @param ap The name of the atomic proposition.
-	 * @param state_index The index of the state to check.
+	 * @param state The index of the state to check.
 	 * @return True if the node is labeled with the atomic proposition, false
 	 * otherwise.
 	 */
 	bool stateHasAtomicProposition(std::string ap,
-			const uint_fast32_t state_index) {
-		return this->single_labelings[name_to_labeling_map[ap]]->hasLabel(state_index);
+			const uint_fast32_t state) {
+		return this->single_labelings[name_to_labeling_map[ap]]->hasLabel(state);
 	}
 
 	/*!

src/models/backward_transitions.h

@@ -0,0 +1,130 @@
+/*
+ * backward_transitions.h
+ *
+ *  Created on: 17.11.2012
+ *      Author: Christian Dehnert
+ */
+
+#ifndef BACKWARD_TRANSITIONS_H_
+#define BACKWARD_TRANSITIONS_H_
+
+#include <iterator>
+#include "src/sparse/static_sparse_matrix.h"
+
+namespace mrmc {
+
+namespace models {
+
+/*!
+ * This class stores the predecessors of all states in a state space of the
+ * given size.
+ */
+template <class T>
+class BackwardTransitions {
+
+public:
+	//! Constructor
+	/*!
+	 * Constructs a backward transitions object from the given sparse matrix
+	 * representing the (forward) transition relation.
+	 * @param transition_matrix The (1-based) matrix representing the transition
+	 * relation.
+	 */
+	BackwardTransitions(mrmc::sparse::StaticSparseMatrix<T>* transition_matrix) {
+		this->state_indices_list = new uint_fast64_t[transition_matrix->getRowCount() + 2];
+		this->predecessor_list = new uint_fast64_t[transition_matrix->getNonZeroEntryCount()];
+
+		// First, we need to count how many backward transitions each state has.
+		// NOTE: We disregard the diagonal here, as we only consider "true"
+		// predecessors.
+		// Start by counting all but the last row.
+		uint_fast64_t* row_indications = transition_matrix->getRowIndicationsPointer();
+		uint_fast64_t* column_indications = transition_matrix->getColumnIndicationsPointer();
+		for (uint_fast64_t i = 1; i < transition_matrix->getRowCount(); i++) {
+			for (uint_fast64_t j = row_indications[i]; j < row_indications[i + 1]; j++) {
+				this->state_indices_list[column_indications[j]]++;
+			}
+		}
+		// Add the last row individually, as the comparison bound in the for-loop
+		// is different in this case.
+		for (uint_fast64_t j = row_indications[transition_matrix->getRowCount()]; j < transition_matrix->getNonZeroEntryCount(); j++) {
+			this->state_indices_list[column_indications[j]]++;
+		}
+
+		// Now compute the accumulated offsets.
+		for (uint_fast64_t i = 1; i < transition_matrix->getRowCount() + 1; i++) {
+			this->state_indices_list[i] = this->state_indices_list[i - 1] + this->state_indices_list[i];
+		}
+
+		// Put a sentinel element at the end of the indices list. This way,
+		// for each state i the range of indices can be read off between
+		// state_indices_list[i] and state_indices_list[i + 1].
+		this->state_indices_list[transition_matrix->getRowCount() + 1] = this->state_indices_list[transition_matrix->getRowCount()];
+
+		// Create an array that stores the next index for each state. Initially
+		// this corresponds to the previously computed accumulated offsets.
+		uint_fast64_t* next_state_index_list = new uint_fast64_t[transition_matrix->getRowCount() + 1];
+		memcpy(next_state_index_list, state_indices_list, (transition_matrix->getRowCount() + 1) * sizeof(uint_fast64_t));
+
+		// Now we are ready to actually fill in the list of predecessors for
+		// every state. Again, we start by considering all but the last row.
+		for (uint_fast64_t i = 1; i < transition_matrix->getRowCount(); i++) {
+			for (uint_fast64_t j = row_indications[i]; j < row_indications[i + 1]; j++) {
+				this->predecessor_list[next_state_index_list[i]++] = column_indications[j];
+			}
+		}
+		// Add the last row individually, as the comparison bound in the for-loop
+		// is different in this case.
+		for (uint_fast64_t j = row_indications[transition_matrix->getRowCount()]; j < transition_matrix->getNonZeroEntryCount(); j++) {
+			this->state_indices_list[next_state_index_list[transition_matrix->getRowCount()]++] = column_indications[j];
+		}
+	}
+
+	~BackwardTransitions() {
+		if (this->predecessor_list != NULL) {
+			delete[] this->predecessor_list;
+		}
+		if (this->state_indices_list != NULL) {
+			delete[] this->state_indices_list;
+		}
+	}
+
+	class const_iterator : public std::iterator<std::input_iterator_tag, uint_fast64_t> {
+		public:
+			const_iterator(uint_fast64_t* ptr) : ptr_(ptr) {	}
+
+			const_iterator operator++() { const_iterator i = *this; ptr_++; return i; }
+			const_iterator operator++(int offset) { ptr_ += offset; return *this; }
+			const uint_fast64_t& operator*() { return *ptr_; }
+			const uint_fast64_t* operator->() { return ptr_; }
+			bool operator==(const const_iterator& rhs) { return ptr_ == rhs.ptr_; }
+			bool operator!=(const const_iterator& rhs) { return ptr_ != rhs.ptr_; }
+		private:
+			uint_fast64_t* ptr_;
+	};
+
+	const_iterator beginPredecessorIterator(uint_fast64_t state) const {
+		return const_iterator(&(this->predecessor_list[this->state_indices_list[state]]));
+	}
+
+	const_iterator endPredecessorIterator(uint_fast64_t state) const {
+		return const_iterator(&(this->predecessor_list[this->state_indices_list[state + 1]]));
+	}
+
+private:
+	/*! A list of predecessors for *all* states. */
+	uint_fast64_t* predecessor_list;
+
+	/*!
+	 * A list of indices indicating at which position in the global array the
+	 * predecessors of a state can be found.
+	 */
+	uint_fast64_t* state_indices_list;
+
+};
+
+} // namespace models
+
+} // namespace mrmc
+
+#endif /* BACKWARD_TRANSITIONS_H_ */

src/models/dtmc.h

@@ -14,6 +14,7 @@
 #include <ostream>
 
 #include "atomic_propositions_labeling.h"
+#include "backward_transitions.h"
 #include "src/sparse/static_sparse_matrix.h"
 
 namespace mrmc {
@@ -38,7 +39,8 @@ public:
 	 * propositions to each state.
 	 */
 	Dtmc(mrmc::sparse::StaticSparseMatrix<T>* probability_matrix,
-			mrmc::models::AtomicPropositionsLabeling* state_labeling) {
+			mrmc::models::AtomicPropositionsLabeling* state_labeling) :
+				backward_transitions(probability_matrix) {
 		this->probability_matrix = probability_matrix;
 		this->state_labeling = state_labeling;
 	}
@@ -99,6 +101,15 @@ public:
 			<< std::endl;
 	}
 
+	mrmc::vector::BitVector* findStatesExistsPath(mrmc::vector::BitVector target_states) {
+		mrmc::vector::BitVector visited_states(target_states);
+		mrmc::vector::BitVector* result = new mrmc::vector::BitVector(target_states);
+
+
+
+		return result;
+	}
+
 private:
 
 	/*! A matrix representing the transition probability function of the DTMC. */
@@ -107,6 +118,11 @@ private:
 	/*! The labeling of the states of the DTMC. */
 	mrmc::models::AtomicPropositionsLabeling* state_labeling;
 
+	/*!
+	 * A data structure that stores the predecessors for all states. This is
+	 * needed for a backwards search.
+	 */
+	mrmc::models::BackwardTransitions<T> backward_transitions;
 };
 
 } // namespace models

src/sparse/static_sparse_matrix.h

@@ -327,6 +327,18 @@ class StaticSparseMatrix {
 		return value_storage;
 	}
 
+	T* getDiagonalStoragePointer() const {
+		return diagonal_storage;
+	}
+
+	uint_fast64_t* getRowIndicationsPointer() const {
+		return row_indications;
+	}
+
+	uint_fast64_t* getColumnIndicationsPointer() const {
+		return column_indications;
+	}
+
 	bool isReadReady() {
 		return (internal_status == MatrixStatus::ReadReady);
 	}

src/utility/utility.cpp

@@ -16,8 +16,10 @@ namespace mrmc {
 
 namespace utility {
 
-void dtmcToDot(mrmc::models::DTMC<double>* dtmc, const char* filename) {
-   FILE *P;
+void dtmcToDot(mrmc::models::Dtmc<double>* dtmc, const char* filename) {
+	//FIXME: adapt this to the refactored names
+	//FIXME: use C++-style for file output here, as performance is not critical here
+/*   FILE *P;
    mrmc::sparse::StaticSparseMatrix<double>* matrix = dtmc->getTransitions();
    mrmc::dtmc::Labeling* labels = dtmc->getLabels();
 
@@ -71,11 +73,11 @@ void dtmcToDot(mrmc::models::DTMC<double>* dtmc, const char* filename) {
 
    fprintf(P, "}\n");
 
-   fclose(P);
+   fclose(P); */
 }
 
 mrmc::models::Dtmc<double>* parseDTMC(const char* tra_file, const char* lab_file) {
-   mrmc::sparse::StaticSparseMatrix<double>* transition_matrix =
+/*   mrmc::sparse::StaticSparseMatrix<double>* transition_matrix =
          mrmc::parser::read_tra_file(tra_file);
    uint_fast64_t node_count = transition_matrix->getRowCount();
 
@@ -84,7 +86,7 @@ mrmc::models::Dtmc<double>* parseDTMC(const char* tra_file, const char* lab_file
 
    mrmc::models::Dtmc<double>* result =
          new mrmc::models::Dtmc<double>(transition_matrix, labeling);
-   return result;
+   return result; */
 }
 
 }

test/parser/read_tra_file_test.cpp

@@ -62,7 +62,8 @@ TEST(ReadTraFileTest, ParseFileTest1) {
 		ASSERT_TRUE(result->getValue(4,4,&val));
 		ASSERT_EQ(val,0);
 
-		result->toDOTFile("output.dot");
+		// FIXME: adapt this test case to the new dot-output routines
+		/* result->toDOTFile("output.dot"); */
 		delete result;
 	} else {
 		FAIL();