Browse Source

"Creating" DeterministicModelParser

this new parser is actually the old DtmcParser.
It can now also create Ctmc models...
tempestpy_adaptions
gereon 12 years ago
parent
commit
c2669ccec4
  1. 9
      src/parser/AutoParser.cpp
  2. 26
      src/parser/DeterministicModelParser.cpp
  3. 56
      src/parser/DeterministicModelParser.h
  4. 40
      src/parser/DtmcParser.h
  5. 6
      test/parser/ParseDtmcTest.cpp

9
src/parser/AutoParser.cpp

@ -5,7 +5,7 @@
#include "src/exceptions/WrongFileFormatException.h"
#include "src/models/AbstractModel.h"
#include "src/parser/DtmcParser.h"
#include "src/parser/DeterministicModelParser.h"
#include "src/parser/MdpParser.h"
namespace storm {
@ -27,12 +27,15 @@ AutoParser::AutoParser(std::string const & transitionSystemFile, std::string con
// Do actual parsing
switch (type) {
case storm::models::DTMC: {
DtmcParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
DeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
this->model = parser.getDtmc();
break;
}
case storm::models::CTMC:
case storm::models::CTMC: {
DeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
this->model = parser.getCtmc();
break;
}
case storm::models::MDP: {
MdpParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
this->model = parser.getMdp();

26
src/parser/DtmcParser.cpp → src/parser/DeterministicModelParser.cpp

@ -1,11 +1,11 @@
/*
* DtmcParser.cpp
* DeterministicModelParser.cpp
*
* Created on: 19.12.2012
* Author: thomas
*/
#include "src/parser/DtmcParser.h"
#include "src/parser/DeterministicModelParser.h"
#include <string>
#include <vector>
@ -27,25 +27,29 @@ namespace parser {
* @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,
DeterministicModelParser::DeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile,
std::string const & stateRewardFile, std::string const & transitionRewardFile) {
storm::parser::DeterministicSparseTransitionParser tp(transitionSystemFile);
uint_fast64_t stateCount = tp.getMatrix()->getRowCount();
std::shared_ptr<std::vector<double>> stateRewards = nullptr;
std::shared_ptr<storm::storage::SparseMatrix<double>> transitionRewards = nullptr;
this->transitionSystem = tp.getMatrix();
uint_fast64_t stateCount = this->transitionSystem->getRowCount();
storm::parser::AtomicPropositionLabelingParser lp(stateCount, labelingFile);
this->labeling = lp.getLabeling();
this->stateRewards = nullptr;
this->transitionRewards = nullptr;
if (stateRewardFile != "") {
storm::parser::SparseStateRewardParser srp(stateCount, stateRewardFile);
stateRewards = srp.getStateRewards();
this->stateRewards = srp.getStateRewards();
}
if (transitionRewardFile != "") {
storm::parser::DeterministicSparseTransitionParser trp(transitionRewardFile);
transitionRewards = trp.getMatrix();
this->transitionRewards = trp.getMatrix();
}
this->dtmc = std::shared_ptr<storm::models::Dtmc<double>>(new storm::models::Dtmc<double>(tp.getMatrix(), lp.getLabeling(), stateRewards, transitionRewards));
this->dtmc = nullptr;
this->ctmc = nullptr;
}
} /* namespace parser */

56
src/parser/DeterministicModelParser.h

@ -0,0 +1,56 @@
/*
* DtmcParser.h
*
* Created on: 19.12.2012
* Author: thomas
*/
#ifndef STORM_PARSER_DETERMINISTICMODELPARSER_H_
#define STORM_PARSER_DETERMINISTICMODELPARSER_H_
#include "src/parser/Parser.h"
#include "src/models/Dtmc.h"
#include "src/models/Ctmc.h"
namespace storm {
namespace parser {
/*!
* @brief Load label and transition file and return initialized dtmc or ctmc object.
*
* @Note This class creates a new Dtmc or Ctmc object that can
* be accessed via getDtmc() or getCtmc(). 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 transition system.
*/
class DeterministicModelParser: public storm::parser::Parser {
public:
DeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile,
std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "");
std::shared_ptr<storm::models::Dtmc<double>> getDtmc() {
if (this->dtmc == nullptr) {
this->dtmc = std::shared_ptr<storm::models::Dtmc<double>>(new storm::models::Dtmc<double>(this->transitionSystem, this->labeling, this->stateRewards, this->transitionRewards));
}
return this->dtmc;
}
std::shared_ptr<storm::models::Ctmc<double>> getCtmc() {
if (this->ctmc == nullptr) {
this->ctmc = std::shared_ptr<storm::models::Ctmc<double>>(new storm::models::Ctmc<double>(this->transitionSystem, this->labeling, this->stateRewards, this->transitionRewards));
}
return this->ctmc;
}
private:
std::shared_ptr<storm::storage::SparseMatrix<double>> transitionSystem;
std::shared_ptr<storm::models::AtomicPropositionsLabeling> labeling;
std::shared_ptr<std::vector<double>> stateRewards;
std::shared_ptr<storm::storage::SparseMatrix<double>> transitionRewards;
std::shared_ptr<storm::models::Dtmc<double>> dtmc;
std::shared_ptr<storm::models::Ctmc<double>> ctmc;
};
} /* namespace parser */
} /* namespace storm */
#endif /* STORM_PARSER_DETERMINISTICMODELPARSER_H_ */

40
src/parser/DtmcParser.h

@ -1,40 +0,0 @@
/*
* DtmcParser.h
*
* Created on: 19.12.2012
* Author: thomas
*/
#ifndef STORM_PARSER_DTMCPARSER_H_
#define STORM_PARSER_DTMCPARSER_H_
#include "src/parser/Parser.h"
#include "src/models/Dtmc.h"
namespace storm {
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 storm::parser::Parser {
public:
DtmcParser(std::string const & transitionSystemFile, std::string const & labelingFile,
std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "");
std::shared_ptr<storm::models::Dtmc<double>> getDtmc() {
return this->dtmc;
}
private:
std::shared_ptr<storm::models::Dtmc<double>> dtmc;
};
} /* namespace parser */
} /* namespace storm */
#endif /* STORM_PARSER_DTMCPARSER_H_ */

6
test/parser/ParseDtmcTest.cpp

@ -8,12 +8,12 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include "src/parser/DtmcParser.h"
#include "src/parser/DeterministicModelParser.h"
#include "src/utility/IoUtility.h"
TEST(ParseDtmcTest, parseAndOutput) {
storm::parser::DtmcParser* dtmcParser;
ASSERT_NO_THROW(dtmcParser = new storm::parser::DtmcParser(
storm::parser::DeterministicModelParser* dtmcParser;
ASSERT_NO_THROW(dtmcParser = new storm::parser::DeterministicModelParser(
STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/pctl_general_input_01.tra",
STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));

Loading…
Cancel
Save