Browse Source

Merge branch 'refactoring'

Conflicts:
	src/mrmc.cpp
tempestpy_adaptions
Lanchid 12 years ago
parent
commit
c8ec52f111
  1. 2
      src/models/Dtmc.h
  2. 13
      src/mrmc.cpp
  3. 9
      src/parser/AtomicPropositionLabelingParser.cpp
  4. 4
      src/parser/AtomicPropositionLabelingParser.h
  5. 26
      src/parser/DeterministicSparseTransitionParser.cpp
  6. 8
      src/parser/DeterministicSparseTransitionParser.h
  7. 33
      src/parser/DtmcParser.cpp
  8. 39
      src/parser/DtmcParser.h
  9. 5
      src/parser/Parser.cpp
  10. 2
      src/parser/Parser.h
  11. 22
      src/utility/IoUtility.cpp
  12. 4
      src/utility/IoUtility.h
  13. 9
      test/parser/ParseDtmcTest.cpp
  14. 14
      test/parser/ReadLabFileTest.cpp
  15. 14
      test/parser/ReadTraFileTest.cpp

2
src/models/Dtmc.h

@ -113,7 +113,7 @@ public:
/*!
*
*/
std::set<std::string> getPropositionsForState(uint_fast64_t state) {
std::set<std::string> const getPropositionsForState(uint_fast64_t const &state) const {
return stateLabeling->getPropositionsForState(state);
}

13
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/LabParser.h"
#include "src/parser/TraParser.h"
#include "src/parser/DtmcParser.h"
#include "src/parser/PrctlParser.h"
#include "src/solver/GraphAnalyzer.h"
#include "src/utility/Settings.h"
@ -144,16 +143,16 @@ void cleanUp() {
*/
void testChecking() {
mrmc::settings::Settings* s = mrmc::settings::instance();
mrmc::parser::TraParser traparser(s->getString("trafile").c_str());
mrmc::parser::LabParser labparser(traparser.getMatrix()->getRowCount(), s->getString("labfile").c_str());
mrmc::models::Dtmc<double> dtmc(traparser.getMatrix(), labparser.getLabeling());
dtmc.printModelInformationToStream(std::cout);
mrmc::parser::DtmcParser dtmcParser(s->getString("trafile"), s->getString("labfile"));
std::shared_ptr<mrmc::models::Dtmc<double>> dtmc = dtmcParser.getDtmc();
dtmc->printModelInformationToStream(std::cout);
mrmc::formula::Ap<double>* trueFormula = new mrmc::formula::Ap<double>("true");
mrmc::formula::Ap<double>* observe0Greater1Formula = new mrmc::formula::Ap<double>("observe0Greater1");
mrmc::formula::Until<double>* untilFormula = new mrmc::formula::Until<double>(trueFormula, observe0Greater1Formula);
mrmc::formula::ProbabilisticNoBoundsOperator<double>* probFormula = new mrmc::formula::ProbabilisticNoBoundsOperator<double>(untilFormula);
mrmc::modelChecker::GmmxxDtmcPrctlModelChecker<double>* mc = new mrmc::modelChecker::GmmxxDtmcPrctlModelChecker<double>(dtmc);
mrmc::modelChecker::GmmxxDtmcPrctlModelChecker<double>* mc = new mrmc::modelChecker::GmmxxDtmcPrctlModelChecker<double>(*dtmc);
mc->check(*probFormula);
delete mc;

9
src/parser/LabParser.cpp → 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,13 +38,14 @@ 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,
std::string const & filename)
: labeling(nullptr)
{
/*
* open file
*/
MappedFile file(filename);
MappedFile file(filename.c_str());
char* buf = file.data;
/*
@ -176,7 +177,7 @@ LabParser::LabParser(uint_fast64_t node_count, const char * filename)
buf += cnt;
}
}
buf = skipWS(buf);
buf = trimWhitespaces(buf);
}
}
}

4
src/parser/LabParser.h → 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, std::string const &filename);
std::shared_ptr<mrmc::models::AtomicPropositionsLabeling> getLabeling() {
return this->labeling;

26
src/parser/TraParser.cpp → 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;
/*
@ -54,7 +54,7 @@ uint_fast64_t TraParser::firstPass(char* buf, uint_fast64_t &maxnode) {
}
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;
@ -82,7 +82,7 @@ uint_fast64_t TraParser::firstPass(char* buf, uint_fast64_t &maxnode) {
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) {
@ -90,7 +90,7 @@ uint_fast64_t TraParser::firstPass(char* buf, uint_fast64_t &maxnode) {
return 0;
}
if (row == col) non_zero--;
buf = skipWS(tmp);
buf = trimWhitespaces(tmp);
}
return non_zero;
@ -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(std::string const &filename)
: matrix(nullptr)
{
/*
@ -117,7 +117,7 @@ TraParser::TraParser(const char * filename)
/*
* open file
*/
MappedFile file(filename);
MappedFile file(filename.c_str());
char* buf = file.data;
/*
@ -145,7 +145,7 @@ TraParser::TraParser(const char * filename)
*/
buf += 7; // skip "STATES "
checked_strtol(buf, &buf);
buf = skipWS(buf);
buf = trimWhitespaces(buf);
buf += 12; // skip "TRANSITIONS "
checked_strtol(buf, &buf);
@ -178,16 +178,8 @@ TraParser::TraParser(const char * filename)
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);
buf = trimWhitespaces(buf);
}
/*

8
src/parser/TraParser.h → 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(std::string const &filename);
std::shared_ptr<mrmc::storage::SquareSparseMatrix<double>> getMatrix() {
return this->matrix;

33
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<mrmc::models::Dtmc<double> >(new mrmc::models::Dtmc<double>(tp.getMatrix(), lp.getLabeling()));
}
} /* namespace parser */
} /* namespace mrmc */

39
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<mrmc::models::Dtmc<double>> getDtmc() {
return this->dtmc;
}
private:
std::shared_ptr<mrmc::models::Dtmc<double>> dtmc;
};
} /* namespace parser */
} /* namespace mrmc */
#endif /* DTMCPARSER_H_ */

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

2
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

22
src/utility/IoUtility.cpp

@ -6,8 +6,8 @@
*/
#include "src/utility/IoUtility.h"
#include "src/parser/TraParser.h"
#include "src/parser/LabParser.h"
#include "src/parser/DeterministicSparseTransitionParser.h"
#include "src/parser/AtomicPropositionLabelingParser.h"
#include <fstream>
@ -15,8 +15,8 @@ namespace mrmc {
namespace utility {
void dtmcToDot(mrmc::models::Dtmc<double>* dtmc, std::string filename) {
std::shared_ptr<mrmc::storage::SquareSparseMatrix<double>> matrix(dtmc->getTransitionProbabilityMatrix());
void dtmcToDot(mrmc::models::Dtmc<double> const &dtmc, std::string filename) {
std::shared_ptr<mrmc::storage::SquareSparseMatrix<double>> matrix(dtmc.getTransitionProbabilityMatrix());
double* diagonal_storage = matrix->getDiagonalStoragePointer();
std::ofstream file;
@ -25,10 +25,10 @@ void dtmcToDot(mrmc::models::Dtmc<double>* 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<std::string> propositions = dtmc->getPropositionsForState(i);
std::set<std::string> propositions = dtmc.getPropositionsForState(i);
for(auto it = propositions.begin();
it != propositions.end();
it++) {
@ -40,7 +40,7 @@ void dtmcToDot(mrmc::models::Dtmc<double>* 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,15 +60,15 @@ void dtmcToDot(mrmc::models::Dtmc<double>* dtmc, std::string filename) {
}
//TODO: Should this stay here or be integrated in the new parser structure?
mrmc::models::Dtmc<double>* parseDTMC(const char* tra_file, const char* lab_file) {
mrmc::parser::TraParser tp(tra_file);
/*mrmc::models::Dtmc<double>* 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();
mrmc::parser::LabParser lp(node_count, lab_file);
mrmc::parser::AtomicPropositionLabelingParser lp(node_count, lab_file);
mrmc::models::Dtmc<double>* result = new mrmc::models::Dtmc<double>(tp.getMatrix(), lp.getLabeling());
return result;
}
}*/
}

4
src/utility/IoUtility.h

@ -25,7 +25,7 @@ namespace utility {
it will be overwritten.
*/
void dtmcToDot(mrmc::models::Dtmc<double>* dtmc, std::string filename);
void dtmcToDot(mrmc::models::Dtmc<double> 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<double>* dtmc, std::string filename);
@returns The DTMC described by the two files.
*/
mrmc::models::Dtmc<double>* parseDTMC(const char* tra_file, const char* lab_file);
//mrmc::models::Dtmc<double>* parseDTMC(std::string const &tra_file, std::string const &lab_file);
} //namespace utility

9
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<double>* 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;
}

14
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<mrmc::models::AtomicPropositionsLabeling> 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);
}

14
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<mrmc::storage::SquareSparseMatrix<double>> 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);
}
Loading…
Cancel
Save