Browse Source

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.
tempestpy_adaptions
Lanchid 12 years ago
parent
commit
afb0373358
  1. 2
      src/models/Dtmc.h
  2. 33
      src/parser/DtmcParser.cpp
  3. 39
      src/parser/DtmcParser.h
  4. 14
      src/utility/IoUtility.cpp
  5. 4
      src/utility/IoUtility.h
  6. 9
      test/parser/ParseDtmcTest.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);
}

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_ */

14
src/utility/IoUtility.cpp

@ -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,7 +60,7 @@ 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(std::string const &tra_file, std::string const &lab_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();
@ -68,7 +68,7 @@ mrmc::models::Dtmc<double>* parseDTMC(std::string const &tra_file, std::string c
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(std::string const &tra_file, std::string const &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;
}
Loading…
Cancel
Save