Merge branch 'master' of https://sselab.de/lab9/private/git/MRMC

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;
 }
-

src/parser/parser.cpp

@@ -7,6 +7,9 @@
 
 #include <sys/stat.h>
 #include <fcntl.h>
+#if defined MACOSX
+	#include <unistd.h>
+#endif
 #include <errno.h>
 #include <iostream>
 #include <cstring>
@@ -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);

src/parser/parser.h

@@ -72,12 +72,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
 			
@@ -106,4 +114,4 @@ namespace parser {
 } // namespace parser
 } // namespace mrmc
 
-#endif /* PARSER_H_ */
+#endif /* PARSER_H_ */

src/parser/readLabFile.h

@@ -16,4 +16,4 @@ mrmc::models::AtomicPropositionsLabeling * readLabFile(uint_fast64_t node_count,
 } // namespace parser
 } // namespace mrmc
 
-#endif /* READLABFILE_H_ */
+#endif /* READLABFILE_H_ */

src/parser/readPrctlFile.cpp

@@ -120,4 +120,4 @@ mrmc::formula::PCTLFormula* mrmc::parser::readPrctlFile(const char* filename)
 		return p.result;
 	}
 	else return NULL;
-}
+}

src/parser/readPrctlFile.h

@@ -14,4 +14,4 @@ mrmc::formula::PCTLFormula* readPrctlFile(const char * filename);
 } // namespace parser
 } // namespace mrmc
 
-#endif /* READPRCTLFILE_H_ */
+#endif /* READPRCTLFILE_H_ */

src/parser/readTraFile.h

@@ -15,4 +15,4 @@ mrmc::storage::SquareSparseMatrix<double> * readTraFile(const char * filename);
 } // namespace parser
 } // namespace mrmc
 
-#endif /* READTRAFILE_H_ */
+#endif /* READTRAFILE_H_ */

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 <iostream>
+
+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 <class T>
+	static void getExistsPhiUntilPsiStates(mrmc::models::Dtmc<T>& 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<T>& 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<uint_fast64_t> 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 <class T>
+	static void getUniversalReachabilityStates(mrmc::models::Dtmc<T>& 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 <class T>
+	static void getUniversalReachabilityStates(mrmc::models::Dtmc<T>& 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_ */

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];

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];
 

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
+#endif