diff --git a/src/models/atomic_propositions_labeling.h b/src/models/atomic_propositions_labeling.h index 3d7bfadb6..fde4c67e2 100644 --- a/src/models/atomic_propositions_labeling.h +++ b/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); } /*! diff --git a/src/models/backward_transitions.h b/src/models/backward_transitions.h new file mode 100644 index 000000000..8a4aca260 --- /dev/null +++ b/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 +#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 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* 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 { + 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_ */ diff --git a/src/models/dtmc.h b/src/models/dtmc.h index 007f20212..afe4b3fd2 100644 --- a/src/models/dtmc.h +++ b/src/models/dtmc.h @@ -14,6 +14,7 @@ #include #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* 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 backward_transitions; }; } // namespace models diff --git a/src/sparse/static_sparse_matrix.h b/src/sparse/static_sparse_matrix.h index 43d71fce5..e5d586c37 100644 --- a/src/sparse/static_sparse_matrix.h +++ b/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); } diff --git a/src/utility/utility.cpp b/src/utility/utility.cpp index 299600922..400733e79 100644 --- a/src/utility/utility.cpp +++ b/src/utility/utility.cpp @@ -16,8 +16,10 @@ namespace mrmc { namespace utility { -void dtmcToDot(mrmc::models::DTMC* dtmc, const char* filename) { - FILE *P; +void dtmcToDot(mrmc::models::Dtmc* 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* matrix = dtmc->getTransitions(); mrmc::dtmc::Labeling* labels = dtmc->getLabels(); @@ -71,11 +73,11 @@ void dtmcToDot(mrmc::models::DTMC* dtmc, const char* filename) { fprintf(P, "}\n"); - fclose(P); + fclose(P); */ } mrmc::models::Dtmc* parseDTMC(const char* tra_file, const char* lab_file) { - mrmc::sparse::StaticSparseMatrix* transition_matrix = +/* mrmc::sparse::StaticSparseMatrix* transition_matrix = mrmc::parser::read_tra_file(tra_file); uint_fast64_t node_count = transition_matrix->getRowCount(); @@ -84,7 +86,7 @@ mrmc::models::Dtmc* parseDTMC(const char* tra_file, const char* lab_file mrmc::models::Dtmc* result = new mrmc::models::Dtmc(transition_matrix, labeling); - return result; + return result; */ } } diff --git a/test/parser/read_tra_file_test.cpp b/test/parser/read_tra_file_test.cpp index 0dd29bd76..b0e54b8ae 100644 --- a/test/parser/read_tra_file_test.cpp +++ b/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();