From b0b8c98f6b7a6adac8403b777f0dabdb28db231d Mon Sep 17 00:00:00 2001 From: Lanchid Date: Wed, 19 Dec 2012 18:21:47 +0100 Subject: [PATCH 1/8] Renamed TraParser to DeterministicSparseTransitionParser --- src/mrmc.cpp | 4 ++-- ...cpp => DeterministicSparseTransitionParser.cpp} | 6 +++--- ...ser.h => DeterministicSparseTransitionParser.h} | 8 ++++---- src/utility/IoUtility.cpp | 4 ++-- test/parser/ReadTraFileTest.cpp | 14 +++++++------- 5 files changed, 18 insertions(+), 18 deletions(-) rename src/parser/{TraParser.cpp => DeterministicSparseTransitionParser.cpp} (95%) rename src/parser/{TraParser.h => DeterministicSparseTransitionParser.h} (73%) diff --git a/src/mrmc.cpp b/src/mrmc.cpp index 9bb62172a..6659b8e13 100644 --- a/src/mrmc.cpp +++ b/src/mrmc.cpp @@ -25,7 +25,7 @@ #include "src/modelChecker/EigenDtmcPrctlModelChecker.h" #include "src/modelChecker/GmmxxDtmcPrctlModelChecker.h" #include "src/parser/LabParser.h" -#include "src/parser/TraParser.h" +#include "src/parser/DeterministicSparseTransitionParser.h" #include "src/parser/PrctlParser.h" #include "src/solver/GraphAnalyzer.h" #include "src/utility/Settings.h" @@ -101,7 +101,7 @@ int main(const int argc, const char* argv[]) { LOG4CPLUS_INFO(logger, "Enable verbose mode, log output gets printed to console."); } - mrmc::parser::TraParser traparser(s->getString("trafile").c_str()); + mrmc::parser::DeterministicSparseTransitionParser traparser(s->getString("trafile").c_str()); mrmc::parser::LabParser labparser(traparser.getMatrix()->getRowCount(), s->getString("labfile").c_str()); mrmc::models::Dtmc dtmc(traparser.getMatrix(), labparser.getLabeling()); diff --git a/src/parser/TraParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp similarity index 95% rename from src/parser/TraParser.cpp rename to src/parser/DeterministicSparseTransitionParser.cpp index 7f38187d7..636d43655 100644 --- a/src/parser/TraParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -5,7 +5,7 @@ * Author: Gereon Kremer */ -#include "src/parser/TraParser.h" +#include "src/parser/DeterministicSparseTransitionParser.h" #include "src/exceptions/FileIoException.h" #include "src/exceptions/WrongFileFormatException.h" #include "boost/integer/integer_mask.hpp" @@ -42,7 +42,7 @@ namespace parser{ * @param buf Data to scan. Is expected to be some char array. * @param maxnode Is set to highest id of all nodes. */ -uint_fast64_t TraParser::firstPass(char* buf, uint_fast64_t &maxnode) { +uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t &maxnode) { uint_fast64_t non_zero = 0; /* @@ -106,7 +106,7 @@ uint_fast64_t TraParser::firstPass(char* buf, uint_fast64_t &maxnode) { * @return a pointer to the created sparse matrix. */ -TraParser::TraParser(const char * filename) +DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(const char * filename) : matrix(nullptr) { /* diff --git a/src/parser/TraParser.h b/src/parser/DeterministicSparseTransitionParser.h similarity index 73% rename from src/parser/TraParser.h rename to src/parser/DeterministicSparseTransitionParser.h index a7079ea66..561f9aa50 100644 --- a/src/parser/TraParser.h +++ b/src/parser/DeterministicSparseTransitionParser.h @@ -12,15 +12,15 @@ namespace mrmc { namespace parser { /*! - * @brief Load transition system from file and return initialized - * StaticSparseMatrix object. + * @brief Load a deterministic transition system from file and create a + * sparse adjacency matrix whose entries represent the weights of the edges * * Note that this class creates a new StaticSparseMatrix object that can be * accessed via getMatrix(). However, it does not delete this object! */ -class TraParser : Parser { +class DeterministicSparseTransitionParser : Parser { public: - TraParser(const char* filename); + DeterministicSparseTransitionParser(const char* filename); std::shared_ptr> getMatrix() { return this->matrix; diff --git a/src/utility/IoUtility.cpp b/src/utility/IoUtility.cpp index 299527044..73f0f7d17 100644 --- a/src/utility/IoUtility.cpp +++ b/src/utility/IoUtility.cpp @@ -6,7 +6,7 @@ */ #include "src/utility/IoUtility.h" -#include "src/parser/TraParser.h" +#include "src/parser/DeterministicSparseTransitionParser.h" #include "src/parser/LabParser.h" #include @@ -61,7 +61,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(const char* tra_file, const char* lab_file) { - mrmc::parser::TraParser tp(tra_file); + mrmc::parser::DeterministicSparseTransitionParser tp(tra_file); uint_fast64_t node_count = tp.getMatrix()->getRowCount(); mrmc::parser::LabParser lp(node_count, lab_file); diff --git a/test/parser/ReadTraFileTest.cpp b/test/parser/ReadTraFileTest.cpp index 99c374a6b..9f4793dc0 100644 --- a/test/parser/ReadTraFileTest.cpp +++ b/test/parser/ReadTraFileTest.cpp @@ -8,7 +8,7 @@ #include "gtest/gtest.h" #include "mrmc-config.h" #include "src/storage/SquareSparseMatrix.h" -#include "src/parser/TraParser.h" +#include "src/parser/DeterministicSparseTransitionParser.h" #include "src/exceptions/FileIoException.h" #include "src/exceptions/WrongFileFormatException.h" @@ -16,14 +16,14 @@ TEST(ReadTraFileTest, NonExistingFileTest) { //No matter what happens, please don't create a file with the name "nonExistingFile.not"! :-) - ASSERT_THROW(mrmc::parser::TraParser(MRMC_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), mrmc::exceptions::FileIoException); + ASSERT_THROW(mrmc::parser::DeterministicSparseTransitionParser(MRMC_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), mrmc::exceptions::FileIoException); } /* The following test case is based on one of the original MRMC test cases */ TEST(ReadTraFileTest, ParseFileTest1) { - mrmc::parser::TraParser* parser; - ASSERT_NO_THROW(parser = new mrmc::parser::TraParser(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/csl_general_input_01.tra")); + mrmc::parser::DeterministicSparseTransitionParser* parser; + ASSERT_NO_THROW(parser = new mrmc::parser::DeterministicSparseTransitionParser(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/csl_general_input_01.tra")); std::shared_ptr> result = parser->getMatrix(); if (result != NULL) { @@ -69,13 +69,13 @@ TEST(ReadTraFileTest, ParseFileTest1) { } TEST(ReadTraFileTest, WrongFormatTestHeader1) { - ASSERT_THROW(mrmc::parser::TraParser(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_header1.tra"), mrmc::exceptions::WrongFileFormatException); + ASSERT_THROW(mrmc::parser::DeterministicSparseTransitionParser(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_header1.tra"), mrmc::exceptions::WrongFileFormatException); } TEST(ReadTraFileTest, WrongFormatTestHeader2) { - ASSERT_THROW(mrmc::parser::TraParser(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_header2.tra"), mrmc::exceptions::WrongFileFormatException); + ASSERT_THROW(mrmc::parser::DeterministicSparseTransitionParser(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_header2.tra"), mrmc::exceptions::WrongFileFormatException); } TEST(ReadTraFileTest, WrongFormatTestTransition) { - ASSERT_THROW(mrmc::parser::TraParser(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_transition.tra"), mrmc::exceptions::WrongFileFormatException); + ASSERT_THROW(mrmc::parser::DeterministicSparseTransitionParser(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_transition.tra"), mrmc::exceptions::WrongFileFormatException); } From 2da19207de4c5e4b3cf9fb0eef17da8ddcd9680c Mon Sep 17 00:00:00 2001 From: Lanchid Date: Wed, 19 Dec 2012 18:25:32 +0100 Subject: [PATCH 2/8] Removed check for valid probablilities, as we want to use the DeterministicSparseTransitionParser for CTMCs (which have edges that are not labeled with probabilities, but with weights) later on --- src/parser/DeterministicSparseTransitionParser.cpp | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index 636d43655..d62661521 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -82,7 +82,7 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, uint_fas if (col > maxnode) maxnode = col; /* * read value. if value is 0.0, either strtod could not read a number or we encountered a probability of zero. - * if row == col, we have a diagonal element which is treated seperately and this non_zero must be decreased. + * if row == col, we have a diagonal element which is treated separately and this non_zero must be decreased. */ val = strtod(buf, &tmp); if (val == 0.0) { @@ -178,14 +178,6 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(const c col = checked_strtol(buf, &buf); val = strtod(buf, &buf); - /* - * only values in (0, 1] are meaningful - */ - if ((val <= 0.0) || (val > 1.0)) - { - LOG4CPLUS_ERROR(logger, "Found transition probability of " << val << ", but we think probabilities should be from (0,1]."); - throw mrmc::exceptions::WrongFileFormatException(); - } this->matrix->addNextValue(row,col,val); buf = skipWS(buf); } From 3c741fae4a74716bd10f16510536cb531d5d1cbd Mon Sep 17 00:00:00 2001 From: Lanchid Date: Wed, 19 Dec 2012 18:35:10 +0100 Subject: [PATCH 3/8] Changed filename parameter for DeterministicSparseTransitionParser to a const reference to an std::string, instead of char pointer --- src/mrmc.cpp | 2 +- src/parser/DeterministicSparseTransitionParser.cpp | 4 ++-- src/parser/DeterministicSparseTransitionParser.h | 2 +- src/utility/IoUtility.cpp | 2 +- src/utility/IoUtility.h | 2 +- 5 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/mrmc.cpp b/src/mrmc.cpp index 6659b8e13..478b6425a 100644 --- a/src/mrmc.cpp +++ b/src/mrmc.cpp @@ -101,7 +101,7 @@ int main(const int argc, const char* argv[]) { LOG4CPLUS_INFO(logger, "Enable verbose mode, log output gets printed to console."); } - mrmc::parser::DeterministicSparseTransitionParser traparser(s->getString("trafile").c_str()); + mrmc::parser::DeterministicSparseTransitionParser traparser(s->getString("trafile")); mrmc::parser::LabParser labparser(traparser.getMatrix()->getRowCount(), s->getString("labfile").c_str()); mrmc::models::Dtmc dtmc(traparser.getMatrix(), labparser.getLabeling()); diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index d62661521..2c4f86c04 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -106,7 +106,7 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, uint_fas * @return a pointer to the created sparse matrix. */ -DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(const char * filename) +DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::string const &filename) : matrix(nullptr) { /* @@ -117,7 +117,7 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(const c /* * open file */ - MappedFile file(filename); + MappedFile file(filename.c_str()); char* buf = file.data; /* diff --git a/src/parser/DeterministicSparseTransitionParser.h b/src/parser/DeterministicSparseTransitionParser.h index 561f9aa50..9dd3b18e7 100644 --- a/src/parser/DeterministicSparseTransitionParser.h +++ b/src/parser/DeterministicSparseTransitionParser.h @@ -20,7 +20,7 @@ namespace parser { */ class DeterministicSparseTransitionParser : Parser { public: - DeterministicSparseTransitionParser(const char* filename); + DeterministicSparseTransitionParser(std::string const &filename); std::shared_ptr> getMatrix() { return this->matrix; diff --git a/src/utility/IoUtility.cpp b/src/utility/IoUtility.cpp index 73f0f7d17..9667a3ff8 100644 --- a/src/utility/IoUtility.cpp +++ b/src/utility/IoUtility.cpp @@ -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(const char* tra_file, const char* lab_file) { +mrmc::models::Dtmc* parseDTMC(std::string const &tra_file, const char* lab_file) { mrmc::parser::DeterministicSparseTransitionParser tp(tra_file); uint_fast64_t node_count = tp.getMatrix()->getRowCount(); diff --git a/src/utility/IoUtility.h b/src/utility/IoUtility.h index 5b691d9b2..d05bf2afb 100644 --- a/src/utility/IoUtility.h +++ b/src/utility/IoUtility.h @@ -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(const char* tra_file, const char* lab_file); +mrmc::models::Dtmc* parseDTMC(std::string const &tra_file, const char* lab_file); } //namespace utility From 64784d4e922fdff8819c8c6c5638b443bdd6c301 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Wed, 19 Dec 2012 18:42:46 +0100 Subject: [PATCH 4/8] Renamed LabParser to AtomicPropositionLabelingParser --- src/mrmc.cpp | 4 ++-- ...ser.cpp => AtomicPropositionLabelingParser.cpp} | 4 ++-- ...bParser.h => AtomicPropositionLabelingParser.h} | 4 ++-- src/utility/IoUtility.cpp | 4 ++-- test/parser/ReadLabFileTest.cpp | 14 +++++++------- 5 files changed, 15 insertions(+), 15 deletions(-) rename src/parser/{LabParser.cpp => AtomicPropositionLabelingParser.cpp} (96%) rename src/parser/{LabParser.h => AtomicPropositionLabelingParser.h} (85%) diff --git a/src/mrmc.cpp b/src/mrmc.cpp index 478b6425a..d9b938e2d 100644 --- a/src/mrmc.cpp +++ b/src/mrmc.cpp @@ -24,7 +24,7 @@ #include "src/models/AtomicPropositionsLabeling.h" #include "src/modelChecker/EigenDtmcPrctlModelChecker.h" #include "src/modelChecker/GmmxxDtmcPrctlModelChecker.h" -#include "src/parser/LabParser.h" +#include "src/parser/AtomicPropositionLabelingParser.h" #include "src/parser/DeterministicSparseTransitionParser.h" #include "src/parser/PrctlParser.h" #include "src/solver/GraphAnalyzer.h" @@ -102,7 +102,7 @@ int main(const int argc, const char* argv[]) { } mrmc::parser::DeterministicSparseTransitionParser traparser(s->getString("trafile")); - mrmc::parser::LabParser labparser(traparser.getMatrix()->getRowCount(), s->getString("labfile").c_str()); + mrmc::parser::AtomicPropositionLabelingParser labparser(traparser.getMatrix()->getRowCount(), s->getString("labfile").c_str()); mrmc::models::Dtmc dtmc(traparser.getMatrix(), labparser.getLabeling()); dtmc.printModelInformationToStream(std::cout); diff --git a/src/parser/LabParser.cpp b/src/parser/AtomicPropositionLabelingParser.cpp similarity index 96% rename from src/parser/LabParser.cpp rename to src/parser/AtomicPropositionLabelingParser.cpp index 45274347d..8c4d7b5a5 100644 --- a/src/parser/LabParser.cpp +++ b/src/parser/AtomicPropositionLabelingParser.cpp @@ -5,7 +5,7 @@ * Author: Gereon Kremer */ -#include "src/parser/LabParser.h" +#include "src/parser/AtomicPropositionLabelingParser.h" #include "src/exceptions/WrongFileFormatException.h" #include "src/exceptions/FileIoException.h" @@ -38,7 +38,7 @@ namespace parser { * @param filename input .lab file's name. * @return The pointer to the created labeling object. */ -LabParser::LabParser(uint_fast64_t node_count, const char * filename) +AtomicPropositionLabelingParser::AtomicPropositionLabelingParser(uint_fast64_t node_count, const char * filename) : labeling(nullptr) { /* diff --git a/src/parser/LabParser.h b/src/parser/AtomicPropositionLabelingParser.h similarity index 85% rename from src/parser/LabParser.h rename to src/parser/AtomicPropositionLabelingParser.h index bb1e2d992..e1b5c4211 100644 --- a/src/parser/LabParser.h +++ b/src/parser/AtomicPropositionLabelingParser.h @@ -17,9 +17,9 @@ namespace parser { * Note that this class creates a new AtomicPropositionsLabeling object that can * be accessed via getLabeling(). However, it will not delete this object! */ -class LabParser : Parser { +class AtomicPropositionLabelingParser : Parser { public: - LabParser(uint_fast64_t node_count, const char* filename); + AtomicPropositionLabelingParser(uint_fast64_t node_count, const char* filename); std::shared_ptr getLabeling() { return this->labeling; diff --git a/src/utility/IoUtility.cpp b/src/utility/IoUtility.cpp index 9667a3ff8..a8d61d32c 100644 --- a/src/utility/IoUtility.cpp +++ b/src/utility/IoUtility.cpp @@ -7,7 +7,7 @@ #include "src/utility/IoUtility.h" #include "src/parser/DeterministicSparseTransitionParser.h" -#include "src/parser/LabParser.h" +#include "src/parser/AtomicPropositionLabelingParser.h" #include @@ -64,7 +64,7 @@ mrmc::models::Dtmc* parseDTMC(std::string const &tra_file, const char* l mrmc::parser::DeterministicSparseTransitionParser tp(tra_file); uint_fast64_t node_count = tp.getMatrix()->getRowCount(); - mrmc::parser::LabParser lp(node_count, lab_file); + mrmc::parser::AtomicPropositionLabelingParser lp(node_count, lab_file); mrmc::models::Dtmc* result = new mrmc::models::Dtmc(tp.getMatrix(), lp.getLabeling()); return result; diff --git a/test/parser/ReadLabFileTest.cpp b/test/parser/ReadLabFileTest.cpp index 97e201151..d019bc986 100644 --- a/test/parser/ReadLabFileTest.cpp +++ b/test/parser/ReadLabFileTest.cpp @@ -8,7 +8,7 @@ #include "gtest/gtest.h" #include "mrmc-config.h" #include "src/models/AtomicPropositionsLabeling.h" -#include "src/parser/LabParser.h" +#include "src/parser/AtomicPropositionLabelingParser.h" #include "src/exceptions/FileIoException.h" #include "src/exceptions/WrongFileFormatException.h" @@ -16,16 +16,16 @@ TEST(ReadLabFileTest, NonExistingFileTest) { //No matter what happens, please don't create a file with the name "nonExistingFile.not"! :-) - ASSERT_THROW(mrmc::parser::LabParser(0,MRMC_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), mrmc::exceptions::FileIoException); + ASSERT_THROW(mrmc::parser::AtomicPropositionLabelingParser(0,MRMC_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), mrmc::exceptions::FileIoException); } TEST(ReadLabFileTest, ParseTest) { //This test is based on a test case from the original MRMC. - mrmc::parser::LabParser* parser; + mrmc::parser::AtomicPropositionLabelingParser* parser; //Parsing the file - ASSERT_NO_THROW(parser = new mrmc::parser::LabParser(12, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab")); + ASSERT_NO_THROW(parser = new mrmc::parser::AtomicPropositionLabelingParser(12, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab")); std::shared_ptr labeling(parser->getLabeling()); //Checking whether all propositions are in the labelling @@ -86,14 +86,14 @@ TEST(ReadLabFileTest, ParseTest) { } TEST(ReadLabFileTest, WrongHeaderTest1) { - ASSERT_THROW(mrmc::parser::LabParser(3, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_header1.lab"), mrmc::exceptions::WrongFileFormatException); + ASSERT_THROW(mrmc::parser::AtomicPropositionLabelingParser(3, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_header1.lab"), mrmc::exceptions::WrongFileFormatException); } TEST(ReadLabFileTest, WrongHeaderTest2) { - ASSERT_THROW(mrmc::parser::LabParser(3, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_header2.lab"), mrmc::exceptions::WrongFileFormatException); + ASSERT_THROW(mrmc::parser::AtomicPropositionLabelingParser(3, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_header2.lab"), mrmc::exceptions::WrongFileFormatException); } TEST(ReadLabFileTest, WrongPropositionTest) { - ASSERT_THROW(mrmc::parser::LabParser(3, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_proposition.lab"), mrmc::exceptions::WrongFileFormatException); + ASSERT_THROW(mrmc::parser::AtomicPropositionLabelingParser(3, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_proposition.lab"), mrmc::exceptions::WrongFileFormatException); } From daa5cf297a6b7595cf20e1f9feeb302d8d39ce04 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Wed, 19 Dec 2012 18:46:25 +0100 Subject: [PATCH 5/8] Changed type of parameter filename to std::string const & (was const char*) --- src/mrmc.cpp | 2 +- src/parser/AtomicPropositionLabelingParser.cpp | 5 +++-- src/parser/AtomicPropositionLabelingParser.h | 2 +- src/utility/IoUtility.cpp | 2 +- src/utility/IoUtility.h | 2 +- 5 files changed, 7 insertions(+), 6 deletions(-) diff --git a/src/mrmc.cpp b/src/mrmc.cpp index d9b938e2d..b107844ef 100644 --- a/src/mrmc.cpp +++ b/src/mrmc.cpp @@ -102,7 +102,7 @@ int main(const int argc, const char* argv[]) { } mrmc::parser::DeterministicSparseTransitionParser traparser(s->getString("trafile")); - mrmc::parser::AtomicPropositionLabelingParser labparser(traparser.getMatrix()->getRowCount(), s->getString("labfile").c_str()); + mrmc::parser::AtomicPropositionLabelingParser labparser(traparser.getMatrix()->getRowCount(), s->getString("labfile")); mrmc::models::Dtmc dtmc(traparser.getMatrix(), labparser.getLabeling()); dtmc.printModelInformationToStream(std::cout); diff --git a/src/parser/AtomicPropositionLabelingParser.cpp b/src/parser/AtomicPropositionLabelingParser.cpp index 8c4d7b5a5..1f307450a 100644 --- a/src/parser/AtomicPropositionLabelingParser.cpp +++ b/src/parser/AtomicPropositionLabelingParser.cpp @@ -38,13 +38,14 @@ namespace parser { * @param filename input .lab file's name. * @return The pointer to the created labeling object. */ -AtomicPropositionLabelingParser::AtomicPropositionLabelingParser(uint_fast64_t node_count, const char * filename) +AtomicPropositionLabelingParser::AtomicPropositionLabelingParser(uint_fast64_t node_count, + std::string const & filename) : labeling(nullptr) { /* * open file */ - MappedFile file(filename); + MappedFile file(filename.c_str()); char* buf = file.data; /* diff --git a/src/parser/AtomicPropositionLabelingParser.h b/src/parser/AtomicPropositionLabelingParser.h index e1b5c4211..d6d7fa84c 100644 --- a/src/parser/AtomicPropositionLabelingParser.h +++ b/src/parser/AtomicPropositionLabelingParser.h @@ -19,7 +19,7 @@ namespace parser { */ class AtomicPropositionLabelingParser : Parser { public: - AtomicPropositionLabelingParser(uint_fast64_t node_count, const char* filename); + AtomicPropositionLabelingParser(uint_fast64_t node_count, std::string const &filename); std::shared_ptr getLabeling() { return this->labeling; diff --git a/src/utility/IoUtility.cpp b/src/utility/IoUtility.cpp index a8d61d32c..5f7e4c691 100644 --- a/src/utility/IoUtility.cpp +++ b/src/utility/IoUtility.cpp @@ -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, const char* 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(); diff --git a/src/utility/IoUtility.h b/src/utility/IoUtility.h index d05bf2afb..08f529380 100644 --- a/src/utility/IoUtility.h +++ b/src/utility/IoUtility.h @@ -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, const char* lab_file); +mrmc::models::Dtmc* parseDTMC(std::string const &tra_file, std::string const &lab_file); } //namespace utility From 383f34e7453eaf595432a4514609fe11f9ba4e2c Mon Sep 17 00:00:00 2001 From: Lanchid Date: Wed, 19 Dec 2012 20:25:50 +0100 Subject: [PATCH 6/8] Function renaming --- src/parser/AtomicPropositionLabelingParser.cpp | 2 +- src/parser/DeterministicSparseTransitionParser.cpp | 8 ++++---- src/parser/Parser.cpp | 5 ++++- src/parser/Parser.h | 2 +- 4 files changed, 10 insertions(+), 7 deletions(-) diff --git a/src/parser/AtomicPropositionLabelingParser.cpp b/src/parser/AtomicPropositionLabelingParser.cpp index 1f307450a..8469f8ef0 100644 --- a/src/parser/AtomicPropositionLabelingParser.cpp +++ b/src/parser/AtomicPropositionLabelingParser.cpp @@ -177,7 +177,7 @@ AtomicPropositionLabelingParser::AtomicPropositionLabelingParser(uint_fast64_t n buf += cnt; } } - buf = skipWS(buf); + buf = trimWhitespaces(buf); } } } diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index 2c4f86c04..d5dd504c1 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -54,7 +54,7 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, uint_fas } buf += 7; // skip "STATES " if (strtol(buf, &buf, 10) == 0) return 0; - buf = skipWS(buf); + buf = trimWhitespaces(buf); if (strncmp(buf, "TRANSITIONS ", 12) != 0) { LOG4CPLUS_ERROR(logger, "Expected \"TRANSITIONS\" but got \"" << std::string(buf, 0, 16) << "\"."); return 0; @@ -90,7 +90,7 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, uint_fas return 0; } if (row == col) non_zero--; - buf = skipWS(tmp); + buf = trimWhitespaces(tmp); } return non_zero; @@ -145,7 +145,7 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st */ buf += 7; // skip "STATES " checked_strtol(buf, &buf); - buf = skipWS(buf); + buf = trimWhitespaces(buf); buf += 12; // skip "TRANSITIONS " checked_strtol(buf, &buf); @@ -179,7 +179,7 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st val = strtod(buf, &buf); this->matrix->addNextValue(row,col,val); - buf = skipWS(buf); + buf = trimWhitespaces(buf); } /* diff --git a/src/parser/Parser.cpp b/src/parser/Parser.cpp index 1e25ee404..cbcfc0b57 100644 --- a/src/parser/Parser.cpp +++ b/src/parser/Parser.cpp @@ -34,7 +34,10 @@ uint_fast64_t mrmc::parser::Parser::checked_strtol(const char* str, char** end) * @param buf String buffer * @return pointer to first non-whitespace character */ -char* mrmc::parser::Parser::skipWS(char* buf) { +char* mrmc::parser::Parser::trimWhitespaces(char* buf) { + /*TODO: Maybe use memcpy to copy all the stuff from the first non-whitespace char + * to the position of the buffer, so we don't have to keep track of 2 pointers. + */ while ((*buf == ' ') || (*buf == '\t') || (*buf == '\n') || (*buf == '\r')) buf++; return buf; } diff --git a/src/parser/Parser.h b/src/parser/Parser.h index 81938ecf7..03f6f002a 100644 --- a/src/parser/Parser.h +++ b/src/parser/Parser.h @@ -106,7 +106,7 @@ namespace parser { /*! * @brief Skips common whitespaces in a string. */ - char* skipWS(char* buf); + char* trimWhitespaces(char* buf); }; } // namespace parser From afb0373358b3112cc4acc78aa9d9a34061dfa7c7 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Wed, 19 Dec 2012 20:28:54 +0100 Subject: [PATCH 7/8] 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; } From ef03284369a09a2a110b7ac93dd46fd24f39ec26 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Wed, 19 Dec 2012 20:37:29 +0100 Subject: [PATCH 8/8] Changed mrmc.cpp to use the new Dtmc parser instead of the separate ones. --- src/mrmc.cpp | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/src/mrmc.cpp b/src/mrmc.cpp index b107844ef..ad5486cc9 100644 --- a/src/mrmc.cpp +++ b/src/mrmc.cpp @@ -24,8 +24,7 @@ #include "src/models/AtomicPropositionsLabeling.h" #include "src/modelChecker/EigenDtmcPrctlModelChecker.h" #include "src/modelChecker/GmmxxDtmcPrctlModelChecker.h" -#include "src/parser/AtomicPropositionLabelingParser.h" -#include "src/parser/DeterministicSparseTransitionParser.h" +#include "src/parser/DtmcParser.h" #include "src/parser/PrctlParser.h" #include "src/solver/GraphAnalyzer.h" #include "src/utility/Settings.h" @@ -101,11 +100,10 @@ int main(const int argc, const char* argv[]) { LOG4CPLUS_INFO(logger, "Enable verbose mode, log output gets printed to console."); } - mrmc::parser::DeterministicSparseTransitionParser traparser(s->getString("trafile")); - mrmc::parser::AtomicPropositionLabelingParser labparser(traparser.getMatrix()->getRowCount(), s->getString("labfile")); - mrmc::models::Dtmc dtmc(traparser.getMatrix(), labparser.getLabeling()); + mrmc::parser::DtmcParser dtmcParser(s->getString("trafile"), s->getString("labfile")); + std::shared_ptr> dtmc = dtmcParser.getDtmc(); - dtmc.printModelInformationToStream(std::cout); + dtmc->printModelInformationToStream(std::cout); if (s != nullptr) { delete s;