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

src/modelChecker/EigenDtmcPrctlModelChecker.h

@@ -51,7 +51,7 @@ public:
 		mrmc::storage::SquareSparseMatrix<Type> tmpMatrix(*this->getModel().getTransitionProbabilityMatrix());
 
 		// Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula.
-		tmpMatrix.makeRowsAbsorbing((~*leftStates & *rightStates) | *rightStates);
+		tmpMatrix.makeRowsAbsorbing((~*leftStates | *rightStates) | *rightStates);
 
 		// Transform the transition probability matrix to the eigen format to use its arithmetic.
 		Eigen::SparseMatrix<Type, 1, int_fast32_t>* eigenMatrix = tmpMatrix.toEigenSparseMatrix();

src/modelChecker/GmmxxDtmcPrctlModelChecker.h

@@ -14,7 +14,7 @@
 #include "src/modelChecker/DtmcPrctlModelChecker.h"
 #include "src/solver/GraphAnalyzer.h"
 #include "src/utility/Vector.h"
-
+#include "src/utility/ConstTemplates.h"
 #include "src/utility/Settings.h"
 
 #include "gmm/gmm_matrix.h"
@@ -49,19 +49,25 @@ public:
 		mrmc::storage::SquareSparseMatrix<Type> tmpMatrix(*this->getModel().getTransitionProbabilityMatrix());
 
 		// Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula.
-		tmpMatrix.makeRowsAbsorbing(~(*leftStates & *rightStates) | *rightStates);
+		tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates);
 
 		// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
 		gmm::csr_matrix<Type>* gmmxxMatrix = tmpMatrix.toGMMXXSparseMatrix();
 
 		// Create the vector with which to multiply.
 		std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
-		mrmc::utility::setVectorValues(result, *rightStates, static_cast<Type>(1.0));
+		mrmc::utility::setVectorValues(result, *rightStates, mrmc::utility::constGetOne<Type>());
 
 		// Now perform matrix-vector multiplication as long as we meet the bound of the formula.
+		std::vector<Type>* swap = nullptr;
+		std::vector<Type>* tmpResult = new std::vector<Type>(this->getModel().getNumberOfStates());
 		for (uint_fast64_t i = 0; i < formula.getBound(); ++i) {
-			gmm::mult(*gmmxxMatrix, *result, *result);
+			gmm::mult(*gmmxxMatrix, *result, *tmpResult);
+			swap = tmpResult;
+			tmpResult = result;
+			result = swap;
 		}
+		delete tmpResult;
 
 		// Delete intermediate results and return result.
 		delete leftStates;
@@ -78,7 +84,7 @@ public:
 
 		// Create the vector with which to multiply and initialize it correctly.
 		std::vector<Type> x(this->getModel().getNumberOfStates());
-		mrmc::utility::setVectorValues(&x, *nextStates, static_cast<Type>(1.0));
+		mrmc::utility::setVectorValues(&x, *nextStates, mrmc::utility::constGetOne<Type>());
 
 		// Delete obsolete sub-result.
 		delete nextStates;
@@ -215,8 +221,8 @@ public:
 		}
 
 		// Set values of resulting vector that are known exactly.
-		mrmc::utility::setVectorValues<Type>(result, notExistsPhiUntilPsiStates, static_cast<Type>(0));
-		mrmc::utility::setVectorValues<Type>(result, alwaysPhiUntilPsiStates, static_cast<Type>(1.0));
+		mrmc::utility::setVectorValues<Type>(result, notExistsPhiUntilPsiStates, mrmc::utility::constGetZero<Type>());
+		mrmc::utility::setVectorValues<Type>(result, alwaysPhiUntilPsiStates, mrmc::utility::constGetOne<Type>());
 
 		return result;
 	}

src/models/Dtmc.h

@@ -39,9 +39,14 @@ public:
 	 * @param stateLabeling The labeling that assigns a set of atomic
 	 * propositions to each state.
 	 */
-	Dtmc(std::shared_ptr<mrmc::storage::SquareSparseMatrix<T>> probabilityMatrix, std::shared_ptr<mrmc::models::AtomicPropositionsLabeling> stateLabeling)
-			: probabilityMatrix(probabilityMatrix), stateLabeling(stateLabeling), backwardTransitions(nullptr) {
-		if (! this->checkValidityProbabilityMatrix()) {
+	Dtmc(std::shared_ptr<mrmc::storage::SquareSparseMatrix<T>> probabilityMatrix,
+			std::shared_ptr<mrmc::models::AtomicPropositionsLabeling> stateLabeling,
+			std::shared_ptr<std::vector<T>> stateRewards = nullptr,
+			std::shared_ptr<mrmc::storage::SquareSparseMatrix<T>> transitionRewardMatrix = nullptr)
+			: probabilityMatrix(probabilityMatrix), stateLabeling(stateLabeling),
+			  stateRewards(stateRewards), transitionRewardMatrix(transitionRewardMatrix),
+			  backwardTransitions(nullptr) {
+		if (!this->checkValidityProbabilityMatrix()) {
 			std::cerr << "Probability matrix is invalid" << std::endl;
 		}
 	}
@@ -52,11 +57,12 @@ public:
 	 * @param dtmc A reference to the DTMC that is to be copied.
 	 */
 	Dtmc(const Dtmc<T> &dtmc) : probabilityMatrix(dtmc.probabilityMatrix),
-			stateLabeling(dtmc.stateLabeling) {
+			stateLabeling(dtmc.stateLabeling), stateRewards(dtmc.stateRewards),
+			transitionRewardMatrix(dtmc.transitionRewardMatrix) {
 		if (dtmc.backardTransitions != nullptr) {
 			this->backwardTransitions = new mrmc::models::GraphTransitions<T>(*dtmc.backwardTransitions);
 		}
-		if (! this->checkValidityProbabilityMatrix()) {
+		if (!this->checkValidityProbabilityMatrix()) {
 			std::cerr << "Probability matrix is invalid" << std::endl;
 		}
 	}
@@ -108,6 +114,22 @@ public:
 		return this->probabilityMatrix;
 	}
 
+	/*!
+	 * Returns a pointer to the matrix representing the transition rewards.
+	 * @return A pointer to the matrix representing the transition rewards.
+	 */
+	std::shared_ptr<mrmc::storage::SquareSparseMatrix<T>> getTransitionRewardMatrix() const {
+		return this->transitionRewardMatrix;
+	}
+
+	/*!
+	 * Returns a pointer to the vector representing the state rewards.
+	 * @return A pointer to the vector representing the state rewards.
+	 */
+	std::shared_ptr<std::vector<T>> getStateRewards() const {
+		return this->stateRewards;
+	}
+
 	/*!
 	 *
 	 */
@@ -170,6 +192,12 @@ private:
 	/*! The labeling of the states of the DTMC. */
 	std::shared_ptr<mrmc::models::AtomicPropositionsLabeling> stateLabeling;
 
+	/*! The state-based rewards of the DTMC. */
+	std::shared_ptr<std::vector<T>> stateRewards;
+
+	/*! The transition-based rewards of the DTMC. */
+	std::shared_ptr<mrmc::storage::SquareSparseMatrix<T>> transitionRewardMatrix;
+
 	/*!
 	 * A data structure that stores the predecessors for all states. This is
 	 * needed for backwards directed searches.

src/parser/DtmcParser.cpp

@@ -8,6 +8,7 @@
 #include "DtmcParser.h"
 #include "DeterministicSparseTransitionParser.h"
 #include "AtomicPropositionLabelingParser.h"
+#include "SparseStateRewardParser.h"
 
 namespace mrmc {
 namespace parser {
@@ -19,15 +20,30 @@ namespace parser {
  *
  * @param transitionSystemFile String containing the location of the transition file (....tra)
  * @param labelingFile String containing the location of the labeling file (....lab)
+ * @param stateRewardFile String containing the location of the state reward file (...srew)
+ * @param transitionRewardFile String containing the location of the transition reward file (...trew)
  */
-DtmcParser::DtmcParser(std::string const & transitionSystemFile, std::string const & labelingFile) {
+DtmcParser::DtmcParser(std::string const & transitionSystemFile, std::string const & labelingFile,
+		std::string const & stateRewardFile, std::string const & transitionRewardFile) {
 	mrmc::parser::DeterministicSparseTransitionParser tp(transitionSystemFile);
-	uint_fast64_t nodeCount = tp.getMatrix()->getRowCount();
+	uint_fast64_t stateCount = tp.getMatrix()->getRowCount();
 
-	mrmc::parser::AtomicPropositionLabelingParser lp(nodeCount, labelingFile);
+	std::shared_ptr<std::vector<double>> stateRewards = nullptr;
+	std::shared_ptr<mrmc::storage::SquareSparseMatrix<double>> transitionRewards = nullptr;
 
-	dtmc = std::shared_ptr<mrmc::models::Dtmc<double> >(new mrmc::models::Dtmc<double>(tp.getMatrix(), lp.getLabeling()));
+	mrmc::parser::AtomicPropositionLabelingParser lp(stateCount, labelingFile);
+	if (stateRewardFile != "") {
+		mrmc::parser::SparseStateRewardParser srp(stateCount, stateRewardFile);
+		stateRewards = srp.getStateRewards();
+	}
+	if (transitionRewardFile != "") {
+		mrmc::parser::DeterministicSparseTransitionParser trp(transitionRewardFile);
+		transitionRewards = trp.getMatrix();
+	}
+
+	dtmc = std::shared_ptr<mrmc::models::Dtmc<double>>(new mrmc::models::Dtmc<double>(tp.getMatrix(), lp.getLabeling(), stateRewards, transitionRewards));
 }
 
 } /* namespace parser */
+
 } /* namespace mrmc */

src/parser/DtmcParser.h

@@ -24,7 +24,8 @@ namespace parser {
  */
 class DtmcParser: public mrmc::parser::Parser {
 public:
-	DtmcParser(std::string const & transitionSystemFile, std::string const & labelingFile);
+	DtmcParser(std::string const & transitionSystemFile, std::string const & labelingFile,
+			std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "");
 
 	std::shared_ptr<mrmc::models::Dtmc<double>> getDtmc() {
 		return this->dtmc;

src/parser/SparseStateRewardParser.cpp

@@ -0,0 +1,74 @@
+/*!
+ * SparseStateRewardParser.cpp
+ *
+ *  Created on: 23.12.2012
+ *      Author: Christian Dehnert
+ */
+
+#include "src/parser/SparseStateRewardParser.h"
+#include "src/exceptions/WrongFileFormatException.h"
+#include "src/exceptions/FileIoException.h"
+
+#include "src/utility/OsDetection.h"
+#include <cstdlib>
+#include <cstdio>
+#include <cstring>
+#include <clocale>
+#include <iostream>
+#include <errno.h>
+#include <time.h>
+#include <sys/stat.h>
+#include <fcntl.h>
+#include <locale.h>
+
+#include "log4cplus/logger.h"
+#include "log4cplus/loggingmacros.h"
+extern log4cplus::Logger logger;
+
+namespace mrmc {
+namespace parser {
+
+
+/*!
+ *	Reads a state reward file and puts the result in a state reward vector.
+ *
+ *	@param stateCount The number of states.
+ *	@param filename The filename of the state reward file.
+ *	@return A pointer to the created state reward vector.
+ */
+SparseStateRewardParser::SparseStateRewardParser(uint_fast64_t stateCount, std::string const & filename)
+	: stateRewards(nullptr) {
+	// Open file.
+	MappedFile file(filename.c_str());
+	char* buf = file.data;
+
+	char separator[] = " \r\n\t";
+	
+	// Create state reward vector with given state count.
+	this->stateRewards = std::shared_ptr<std::vector<double>>(new std::vector<double>(stateCount));
+	
+	{
+		// Now parse state reward assignments.
+		uint_fast64_t state;
+		double reward;
+
+		// Iterate over states.
+		while (buf[0] != '\0') {
+			// Parse state number and reward value.
+			state = checked_strtol(buf, &buf);
+			reward = strtod(buf, &buf);
+			if (reward < 0.0) {
+				LOG4CPLUS_ERROR(logger, "Expected positive probability but got \"" << std::string(buf, 0, 16) << "\".");
+				throw mrmc::exceptions::WrongFileFormatException() << "State reward file specifies illegal reward value.";
+			}
+
+			(*this->stateRewards)[state] = reward;
+
+			buf = trimWhitespaces(buf);
+		}
+	}
+}
+
+} //namespace parser
+
+} //namespace mrmc

src/parser/SparseStateRewardParser.h

@@ -0,0 +1,32 @@
+#ifndef MRMC_PARSER_SPARSESTATEREWARDPARSER_H_
+#define MRMC_PARSER_SPARSESTATEREWARDPARSER_H_
+
+#include "boost/integer/integer_mask.hpp"
+#include "src/parser/Parser.h"
+#include <memory>
+#include <vector>
+
+namespace mrmc {
+
+namespace parser {
+
+/*!
+ *	@brief Load state reward file and return vector of state rewards.
+ */
+class SparseStateRewardParser : Parser {
+	public:
+		SparseStateRewardParser(uint_fast64_t stateCount, std::string const &filename);
+
+		std::shared_ptr<std::vector<double>> getStateRewards() {
+			return this->stateRewards;
+		}
+	
+	private:
+		std::shared_ptr<std::vector<double>> stateRewards;
+};
+
+} // namespace parser
+
+} // namespace mrmc
+
+#endif /* MRMC_PARSER_SPARSESTATEREWARDPARSER_H_ */

src/storage/SquareSparseMatrix.h

@@ -81,7 +81,7 @@ public:
 			  internalStatus(ssm.internalStatus), currentSize(ssm.currentSize), lastRow(ssm.lastRow) {
 		LOG4CPLUS_WARN(logger, "Invoking copy constructor.");
 		// Check whether copying the matrix is safe.
-		if (!ssm.hasError()) {
+		if (ssm.hasError()) {
 			LOG4CPLUS_ERROR(logger, "Trying to copy sparse matrix in error state.");
 			throw mrmc::exceptions::InvalidArgumentException("Trying to copy sparse matrix in error state.");
 		} else {

src/utility/Settings.cpp

@@ -130,6 +130,8 @@ void Settings::initDescriptions() {
 		("test-prctl", bpo::value<std::string>(), "name of prctl file")
 		("trafile", bpo::value<std::string>()->required(), "name of the .tra file")
 		("labfile", bpo::value<std::string>()->required(), "name of the .lab file")
+		("transrew", bpo::value<std::string>()->default_value(""), "name of transition reward file")
+		("staterew", bpo::value<std::string>()->default_value(""), "name of state reward file")
 	;
 }