From afb0373358b3112cc4acc78aa9d9a34061dfa7c7 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Wed, 19 Dec 2012 20:28:54 +0100 Subject: [PATCH] Added DtmcParser class that parses a whole DTMC, making use of the labeling and transitions parser. Removed the parseDtmc function from IoUtility, as it became obsolete with the DtmcParser class, fitted test cases accordingly. --- src/models/Dtmc.h | 2 +- src/parser/DtmcParser.cpp | 33 +++++++++++++++++++++++++++++ src/parser/DtmcParser.h | 39 +++++++++++++++++++++++++++++++++++ src/utility/IoUtility.cpp | 14 ++++++------- src/utility/IoUtility.h | 4 ++-- test/parser/ParseDtmcTest.cpp | 9 ++++---- 6 files changed, 87 insertions(+), 14 deletions(-) create mode 100644 src/parser/DtmcParser.cpp create mode 100644 src/parser/DtmcParser.h diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index c3fa93466..f035ebc8d 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -113,7 +113,7 @@ public: /*! * */ - std::set getPropositionsForState(uint_fast64_t state) { + std::set const getPropositionsForState(uint_fast64_t const &state) const { return stateLabeling->getPropositionsForState(state); } diff --git a/src/parser/DtmcParser.cpp b/src/parser/DtmcParser.cpp new file mode 100644 index 000000000..67dc0ac76 --- /dev/null +++ b/src/parser/DtmcParser.cpp @@ -0,0 +1,33 @@ +/* + * DtmcParser.cpp + * + * Created on: 19.12.2012 + * Author: thomas + */ + +#include "DtmcParser.h" +#include "DeterministicSparseTransitionParser.h" +#include "AtomicPropositionLabelingParser.h" + +namespace mrmc { +namespace parser { + +/*! + * Parses a transition file and a labeling file and produces a DTMC out of them; a pointer to the dtmc + * is saved in the field "dtmc" + * Note that the labeling file may have at most as many nodes as the transition file! + * + * @param transitionSystemFile String containing the location of the transition file (....tra) + * @param labelingFile String containing the location of the labeling file (....lab) + */ +DtmcParser::DtmcParser(std::string const & transitionSystemFile, std::string const & labelingFile) { + mrmc::parser::DeterministicSparseTransitionParser tp(transitionSystemFile); + uint_fast64_t nodeCount = tp.getMatrix()->getRowCount(); + + mrmc::parser::AtomicPropositionLabelingParser lp(nodeCount, labelingFile); + + dtmc = std::shared_ptr >(new mrmc::models::Dtmc(tp.getMatrix(), lp.getLabeling())); +} + +} /* namespace parser */ +} /* namespace mrmc */ diff --git a/src/parser/DtmcParser.h b/src/parser/DtmcParser.h new file mode 100644 index 000000000..7db859098 --- /dev/null +++ b/src/parser/DtmcParser.h @@ -0,0 +1,39 @@ +/* + * DtmcParser.h + * + * Created on: 19.12.2012 + * Author: thomas + */ + +#ifndef DTMCPARSER_H_ +#define DTMCPARSER_H_ + +#include "Parser.h" +#include "models/Dtmc.h" + +namespace mrmc { +namespace parser { + +/*! + * @brief Load label and transition file and return initialized dtmc object + * + * @Note This class creates a new Dtmc object that can + * be accessed via getDtmc(). However, it will not delete this object! + * + * @Note The labeling representation in the file may use at most as much nodes as are specified in the dtmc. + */ +class DtmcParser: public mrmc::parser::Parser { +public: + DtmcParser(std::string const & transitionSystemFile, std::string const & labelingFile); + + std::shared_ptr> getDtmc() { + return this->dtmc; + } + +private: + std::shared_ptr> dtmc; +}; + +} /* namespace parser */ +} /* namespace mrmc */ +#endif /* DTMCPARSER_H_ */ diff --git a/src/utility/IoUtility.cpp b/src/utility/IoUtility.cpp index 5f7e4c691..3dc4d49af 100644 --- a/src/utility/IoUtility.cpp +++ b/src/utility/IoUtility.cpp @@ -15,8 +15,8 @@ namespace mrmc { namespace utility { -void dtmcToDot(mrmc::models::Dtmc* dtmc, std::string filename) { - std::shared_ptr> matrix(dtmc->getTransitionProbabilityMatrix()); +void dtmcToDot(mrmc::models::Dtmc const &dtmc, std::string filename) { + std::shared_ptr> matrix(dtmc.getTransitionProbabilityMatrix()); double* diagonal_storage = matrix->getDiagonalStoragePointer(); std::ofstream file; @@ -25,10 +25,10 @@ void dtmcToDot(mrmc::models::Dtmc* dtmc, std::string filename) { file << "digraph dtmc {\n"; //Specify the nodes and their labels - for (uint_fast64_t i = 1; i < dtmc->getNumberOfStates(); i++) { + for (uint_fast64_t i = 1; i < dtmc.getNumberOfStates(); i++) { file << "\t" << i << "[label=\"" << i << "\\n{"; char komma=' '; - std::set propositions = dtmc->getPropositionsForState(i); + std::set propositions = dtmc.getPropositionsForState(i); for(auto it = propositions.begin(); it != propositions.end(); it++) { @@ -40,7 +40,7 @@ void dtmcToDot(mrmc::models::Dtmc* dtmc, std::string filename) { } - for (uint_fast64_t row = 0; row < dtmc->getNumberOfStates(); row++ ) { + for (uint_fast64_t row = 0; row < dtmc.getNumberOfStates(); row++ ) { //write diagonal entry/self loop first if (diagonal_storage[row] != 0) { file << "\t" << row << " -> " << row << " [label=" << diagonal_storage[row] <<"]\n"; @@ -60,7 +60,7 @@ void dtmcToDot(mrmc::models::Dtmc* dtmc, std::string filename) { } //TODO: Should this stay here or be integrated in the new parser structure? -mrmc::models::Dtmc* parseDTMC(std::string const &tra_file, std::string const &lab_file) { +/*mrmc::models::Dtmc* parseDTMC(std::string const &tra_file, std::string const &lab_file) { mrmc::parser::DeterministicSparseTransitionParser tp(tra_file); uint_fast64_t node_count = tp.getMatrix()->getRowCount(); @@ -68,7 +68,7 @@ mrmc::models::Dtmc* parseDTMC(std::string const &tra_file, std::string c mrmc::models::Dtmc* result = new mrmc::models::Dtmc(tp.getMatrix(), lp.getLabeling()); return result; -} +}*/ } diff --git a/src/utility/IoUtility.h b/src/utility/IoUtility.h index 08f529380..112ca85cd 100644 --- a/src/utility/IoUtility.h +++ b/src/utility/IoUtility.h @@ -25,7 +25,7 @@ namespace utility { it will be overwritten. */ -void dtmcToDot(mrmc::models::Dtmc* dtmc, std::string filename); +void dtmcToDot(mrmc::models::Dtmc const &dtmc, std::string filename); /*! Parses a transition file and a labeling file and produces a DTMC out of them. @@ -36,7 +36,7 @@ void dtmcToDot(mrmc::models::Dtmc* dtmc, std::string filename); @returns The DTMC described by the two files. */ -mrmc::models::Dtmc* parseDTMC(std::string const &tra_file, std::string const &lab_file); +//mrmc::models::Dtmc* parseDTMC(std::string const &tra_file, std::string const &lab_file); } //namespace utility diff --git a/test/parser/ParseDtmcTest.cpp b/test/parser/ParseDtmcTest.cpp index 475db9414..e020ce0bb 100644 --- a/test/parser/ParseDtmcTest.cpp +++ b/test/parser/ParseDtmcTest.cpp @@ -8,17 +8,18 @@ #include "gtest/gtest.h" #include "mrmc-config.h" +#include "src/parser/DtmcParser.h" #include "src/utility/IoUtility.h" TEST(ParseDtmcTest, parseAndOutput) { - mrmc::models::Dtmc* myDtmc; - ASSERT_NO_THROW(myDtmc = mrmc::utility::parseDTMC( + mrmc::parser::DtmcParser* dtmcParser; + ASSERT_NO_THROW(dtmcParser = new mrmc::parser::DtmcParser( MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/pctl_general_input_01.tra", MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab")); - ASSERT_NO_THROW(mrmc::utility::dtmcToDot(myDtmc, MRMC_CPP_TESTS_BASE_PATH "/parser/output.dot")); + ASSERT_NO_THROW(mrmc::utility::dtmcToDot(*(dtmcParser->getDtmc()), MRMC_CPP_TESTS_BASE_PATH "/parser/output.dot")); - delete myDtmc; + delete dtmcParser; }