From dc7c4142464e616f93d4552630bb0d312fb872cb Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 2 Dec 2012 12:10:55 +0100 Subject: [PATCH 1/5] Merged bit vector and main file. --- src/mrmc.cpp | 5 ++++- src/storage/BitVector.h | 4 ++-- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/src/mrmc.cpp b/src/mrmc.cpp index 67c772157..1233ff1e6 100644 --- a/src/mrmc.cpp +++ b/src/mrmc.cpp @@ -22,6 +22,7 @@ #include "src/models/AtomicPropositionsLabeling.h" #include "src/parser/readLabFile.h" #include "src/parser/readTraFile.h" +#include "src/solver/GraphAnalyzer.h" #include "src/utility/settings.h" #include "Eigen/Sparse" @@ -96,6 +97,9 @@ int main(const int argc, const char* argv[]) { dtmc.printModelInformationToStream(std::cout); + // mrmc::storage::BitVector AU(dtmc.getNumberOfStates()); + // mrmc::solver::GraphAnalyzer::getUniversalReachabilityStates(dtmc, mrmc::storage::BitVector(dtmc.getNumberOfStates(), true), *dtmc.getLabeledStates("elected"), AU); + if (s != nullptr) { delete s; } @@ -104,4 +108,3 @@ int main(const int argc, const char* argv[]) { return 0; } - diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index 8da13efeb..d5fb56c67 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -266,7 +266,7 @@ public: * of the two bit vectors. */ BitVector operator &=(const BitVector bv) { - uint_fast64_t minSize = ((bv.bitCount < this->bitCount) ? bv.bitCount : this->bitCount) >> 6; + uint_fast64_t minSize = (bv.bucketCount < this->bucketCount) ? bv.bucketCount : this->bucketCount; for (uint_fast64_t i = 0; i < minSize; ++i) { this->bucketArray[i] &= bv.bucketArray[i]; @@ -305,7 +305,7 @@ public: * of the two bit vectors. */ BitVector& operator |=(const BitVector bv) { - uint_fast64_t minSize = ((bv.bitCount < this->bitCount) ? bv.bitCount : this->bitCount) >> 6; + uint_fast64_t minSize = (bv.bucketCount < this->bucketCount) ? bv.bucketCount : this->bucketCount; for (uint_fast64_t i = 0; i < minSize; ++i) { this->bucketArray[i] |= bv.bucketArray[i]; From 18b72bc8d7be0333f2227d3a652e04534664f6e2 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 2 Dec 2012 12:13:32 +0100 Subject: [PATCH 2/5] Added necessary include of unistd.h (for close()) to parser. Removed flag MAP_DENYWRITE of mmap for Mac OS and Linux as it is non-existent and ignored, respectively. Changed call to stat64 to call to stat for MAC OS, as stat64 is deprecated and 64-bit mode is turned on by macro that is no correctly set during OS-Detection. --- src/parser/parser.cpp | 9 ++++++++- src/utility/osDetection.h | 5 +++-- 2 files changed, 11 insertions(+), 3 deletions(-) diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index a6daeeb76..4e0a0463e 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -7,6 +7,9 @@ #include #include +#if defined MACOSX + #include +#endif #include #include #include @@ -63,7 +66,11 @@ mrmc::parser::MappedFile::MappedFile(const char* filename) * Do file mapping for reasonable systems. * stat64(), open(), mmap() */ +#ifdef MACOSX + if (stat(filename, &(this->st)) != 0) +#else if (stat64(filename, &(this->st)) != 0) +#endif { LOG4CPLUS_ERROR(logger, "Error in stat(" << filename << ")."); throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in stat()"); @@ -76,7 +83,7 @@ mrmc::parser::MappedFile::MappedFile(const char* filename) throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in open()"); } - this->data = (char*) mmap(NULL, this->st.st_size, PROT_READ, MAP_PRIVATE|MAP_DENYWRITE, this->file, 0); + this->data = (char*) mmap(NULL, this->st.st_size, PROT_READ, MAP_PRIVATE, this->file, 0); if (this->data == (char*)-1) { close(this->file); diff --git a/src/utility/osDetection.h b/src/utility/osDetection.h index c6c863a60..da72a909f 100644 --- a/src/utility/osDetection.h +++ b/src/utility/osDetection.h @@ -2,10 +2,11 @@ #if defined __linux__ || defined __linux #define LINUX -#elif defined TARGET_OS_MAC || defined __apple__ +#elif defined TARGET_OS_MAC || defined __apple__ || defined __APPLE__ #define MACOSX + #define _DARWIN_USE_64_BIT_INODE #elif defined _WIN32 || defined _WIN64 #define WINDOWS #else #error Could not detect Operating System -#endif \ No newline at end of file +#endif From b76f392df1de3b76ff8903020a7d98583b84a92b Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 2 Dec 2012 12:15:16 +0100 Subject: [PATCH 3/5] Added newlines to end of files, because clang++ complains about that. Added case distinction of struct definition in parser.h for Mac OS to work correctly with parser.cpp. --- src/parser/parser.h | 12 ++++++++++-- src/parser/readLabFile.h | 2 +- src/parser/readPrctlFile.cpp | 2 +- src/parser/readPrctlFile.h | 2 +- src/parser/readTraFile.h | 2 +- 5 files changed, 14 insertions(+), 6 deletions(-) diff --git a/src/parser/parser.h b/src/parser/parser.h index 43dbe4637..91ede4b3f 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -64,12 +64,20 @@ namespace parser { HANDLE mapping; #endif -#if defined LINUX || defined MACOSX +#if defined LINUX /*! * @brief stat information about the file. */ struct stat64 st; +#elif defined MACOSX + /*! + * @brief stat information about the file. + */ + struct stat st; #elif defined WINDOWS + /*! + * @brief stat information about the file. + */ struct __stat64 st; #endif @@ -98,4 +106,4 @@ namespace parser { } // namespace parser } // namespace mrmc -#endif /* PARSER_H_ */ \ No newline at end of file +#endif /* PARSER_H_ */ diff --git a/src/parser/readLabFile.h b/src/parser/readLabFile.h index 103fe5570..057773348 100644 --- a/src/parser/readLabFile.h +++ b/src/parser/readLabFile.h @@ -16,4 +16,4 @@ mrmc::models::AtomicPropositionsLabeling * readLabFile(uint_fast64_t node_count, } // namespace parser } // namespace mrmc -#endif /* READLABFILE_H_ */ \ No newline at end of file +#endif /* READLABFILE_H_ */ diff --git a/src/parser/readPrctlFile.cpp b/src/parser/readPrctlFile.cpp index 737f6e61a..40aa6deb4 100644 --- a/src/parser/readPrctlFile.cpp +++ b/src/parser/readPrctlFile.cpp @@ -120,4 +120,4 @@ mrmc::formula::PCTLFormula* mrmc::parser::readPrctlFile(const char* filename) return p.result; } else return NULL; -} \ No newline at end of file +} diff --git a/src/parser/readPrctlFile.h b/src/parser/readPrctlFile.h index c9f8ba470..80393482d 100644 --- a/src/parser/readPrctlFile.h +++ b/src/parser/readPrctlFile.h @@ -14,4 +14,4 @@ mrmc::formula::PCTLFormula* readPrctlFile(const char * filename); } // namespace parser } // namespace mrmc -#endif /* READPRCTLFILE_H_ */ \ No newline at end of file +#endif /* READPRCTLFILE_H_ */ diff --git a/src/parser/readTraFile.h b/src/parser/readTraFile.h index 0f9617ba1..a4f2a7aef 100644 --- a/src/parser/readTraFile.h +++ b/src/parser/readTraFile.h @@ -15,4 +15,4 @@ mrmc::storage::SquareSparseMatrix * readTraFile(const char * filename); } // namespace parser } // namespace mrmc -#endif /* READTRAFILE_H_ */ \ No newline at end of file +#endif /* READTRAFILE_H_ */ From b1cc1a782d227c2d9c93ecbfa3757975f320de0d Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 2 Dec 2012 12:17:02 +0100 Subject: [PATCH 4/5] Adding graph analyzer that is able to perform reachability searches in the state space. --- src/solver/GraphAnalyzer.h | 99 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 99 insertions(+) create mode 100644 src/solver/GraphAnalyzer.h diff --git a/src/solver/GraphAnalyzer.h b/src/solver/GraphAnalyzer.h new file mode 100644 index 000000000..efe1da1e1 --- /dev/null +++ b/src/solver/GraphAnalyzer.h @@ -0,0 +1,99 @@ +/* + * GraphAnalyzer.h + * + * Created on: 28.11.2012 + * Author: Christian Dehnert + */ + +#ifndef GRAPHANALYZER_H_ +#define GRAPHANALYZER_H_ + +#include "src/models/Dtmc.h" + +#include + +namespace mrmc { + +namespace solver { + +class GraphAnalyzer { +public: + /*! + * Performs a backwards depth-first search trough the underlying graph structure + * of the given model to determine which states of the model can reach one + * of the given target states whilst always staying in the set of filter states + * before. The resulting states are written to the given bit vector. + * @param model The model whose graph structure to search. + * @param targetStates The target states of the search. + * @param filterStates A set of states constraining the search. + * @param existentialReachabilityStates The result of the search. + */ + template + static void getExistsPhiUntilPsiStates(mrmc::models::Dtmc& model, const mrmc::storage::BitVector& phiStates, const mrmc::storage::BitVector& psiStates, mrmc::storage::BitVector& existsPhiUntilPsiStates) { + // Get the backwards transition relation from the model to ease the search. + mrmc::models::GraphTransitions& backwardTransitions = model.getBackwardTransitions(); + + // Add all psi states as the already satisfy the condition. + existsPhiUntilPsiStates |= psiStates; + + // Initialize the stack used for the DFS with the states + std::vector stack; + stack.reserve(model.getNumberOfStates()); + psiStates.getList(stack); + + // Perform the actual DFS. + 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) && !existsPhiUntilPsiStates.get(*it)) { + existsPhiUntilPsiStates.set(*it, true); + stack.push_back(*it); + } + } + } + } + + /*! + * Computes the set of states of the given model for which all paths lead to + * the given set of target states and only visit states from the filter set + * before. In order to do this, it uses the given set of states that + * characterizes the states that possess at least one path to a target state. + * The results are written to the given bit vector. + * @param model The model whose graph structure to search. + * @param targetStates The target states of the search. + * @param filterStates A set of states constraining the search. + * @param existentialReachabilityStates The set of states that possess at + * least one path to a target state. + * @param universalReachabilityStates The result of the search. + */ + template + static void getUniversalReachabilityStates(mrmc::models::Dtmc& model, const mrmc::storage::BitVector& phiStates, const mrmc::storage::BitVector& psiStates, const mrmc::storage::BitVector& existsPhiUntilPsiStates, mrmc::storage::BitVector& alwaysPhiUntilPsiStates) { + GraphAnalyzer::getExistsPhiUntilPsiStates(model, ~psiStates, ~existsPhiUntilPsiStates, alwaysPhiUntilPsiStates); + alwaysPhiUntilPsiStates.complement(); + } + + /*! + * Computes the set of states of the given model for which all paths lead to + * the given set of target states and only visit states from the filter set + * before. + * @param model The model whose graph structure to search. + * @param targetStates The target states of the search. + * @param filterStates A set of states constraining the search. + * @param universalReachabilityStates The result of the search. + */ + template + static void getUniversalReachabilityStates(mrmc::models::Dtmc& model, const mrmc::storage::BitVector& phiStates, const mrmc::storage::BitVector& psiStates, mrmc::storage::BitVector& alwaysPhiUntilPsiStates) { + mrmc::storage::BitVector existsPhiUntilPsiStates(model.getNumberOfStates()); + GraphAnalyzer::getExistsPhiUntilPsiStates(model, phiStates, psiStates, existsPhiUntilPsiStates); + GraphAnalyzer::getUniversalReachabilityStates(model, phiStates, psiStates, existsPhiUntilPsiStates, alwaysPhiUntilPsiStates); + } + +}; + +} // namespace solver + +} // namespace mrmc + +#endif /* GRAPHANALYZER_H_ */ From 30827b543e322189266afce69e0965f5c119dbb2 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 2 Dec 2012 12:34:47 +0100 Subject: [PATCH 5/5] Fixed off-by-one error in sparse matrix. Now the tests do not produce a segfault any longer. --- src/storage/SquareSparseMatrix.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storage/SquareSparseMatrix.h b/src/storage/SquareSparseMatrix.h index 732dd2432..b83b91eff 100644 --- a/src/storage/SquareSparseMatrix.h +++ b/src/storage/SquareSparseMatrix.h @@ -530,7 +530,7 @@ public: // them to the matrix individually. uint_fast64_t rowStart; uint_fast64_t rowEnd; - for (uint_fast64_t row = 0; row <= rowCount; ++row) { + for (uint_fast64_t row = 0; row < rowCount; ++row) { rowStart = rowIndications[row]; rowEnd = rowIndications[row + 1];