sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Refactored NondeterministicModelParser.h/.cpp 

-Mostly restruturing and tidying up.

Next up: Refatoring AtomicPropositionLabelingParser.h/.cpp


Former-commit-id: c26abad850
tempestpy_adaptions
masawei 11 years ago
parent
cc71a002f4
commit
c279c693e5
6 changed files with 125 additions and 108 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      src/parser/AutoParser.h
  2. 10
      src/parser/DeterministicModelParser.cpp
  3. 8
      src/parser/DeterministicModelParser.h
  4. 113
      src/parser/NondeterministicModelParser.cpp
  5. 96
      src/parser/NondeterministicModelParser.h
  6. 2
      test/functional/parser/ParseMdpTest.cpp

4
src/parser/AutoParser.h
View File

@ -56,11 +56,11 @@ class AutoParser {
break;
}
case storm::models::MDP: {
this->model.reset(new storm::models::Mdp<double>(std::move(NondeterministicModelParserAsMdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))));
this->model.reset(new storm::models::Mdp<double>(std::move(NondeterministicModelParser::parseMdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))));
break;
}
case storm::models::CTMDP: {
this->model.reset(new storm::models::Ctmdp<double>(std::move(NondeterministicModelParserAsCtmdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))));
this->model.reset(new storm::models::Ctmdp<double>(std::move(NondeterministicModelParser::parseCtmdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))));
break;
}
case storm::models::MA: {

10
src/parser/DeterministicModelParser.cpp
View File

@ -26,16 +26,16 @@ 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)
*/
DeterministicModelParser::ResultContainer DeterministicModelParser::parseDeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) {
DeterministicModelParser::Result DeterministicModelParser::parseDeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) {
storm::storage::SparseMatrix<double> resultTransitionSystem(std::move(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(transitionSystemFile)));
uint_fast64_t stateCount = resultTransitionSystem.getColumnCount();
uint_fast64_t rowCount = resultTransitionSystem.getRowCount();
storm::models::AtomicPropositionsLabeling resultLabeling(std::move(storm::parser::AtomicPropositionLabelingParser(stateCount, labelingFile)));
storm::models::AtomicPropositionsLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser(stateCount, labelingFile)));
DeterministicModelParser::ResultContainer result(std::move(resultTransitionSystem), std::move(resultLabeling));
DeterministicModelParser::Result result(std::move(resultTransitionSystem), std::move(labeling));
// Only parse state rewards of a file is given.
if (stateRewardFile != "") {
@ -58,7 +58,7 @@ DeterministicModelParser::ResultContainer DeterministicModelParser::parseDetermi
*/
storm::models::Dtmc<double> DeterministicModelParser::parseDtmc(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) {
DeterministicModelParser::ResultContainer parserResult(std::move(parseDeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)));
DeterministicModelParser::Result parserResult(std::move(parseDeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)));
return storm::models::Dtmc<double>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
}
@ -69,7 +69,7 @@ storm::models::Dtmc<double> DeterministicModelParser::parseDtmc(std::string cons
*/
storm::models::Ctmc<double> DeterministicModelParser::parseCtmc(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) {
DeterministicModelParser::ResultContainer parserResult(std::move(parseDeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)));
DeterministicModelParser::Result parserResult(std::move(parseDeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)));
return storm::models::Ctmc<double>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
}

8
src/parser/DeterministicModelParser.h
View File

@ -35,13 +35,13 @@ public:
/*!
* @brief A struct containing the parsed components of a deterministic model.
*/
struct ResultContainer {
struct Result {
ResultContainer(storm::storage::SparseMatrix<double>& transitionSystem, storm::models::AtomicPropositionsLabeling& labeling) : transitionSystem(transitionSystem), labeling(labeling) {
Result(storm::storage::SparseMatrix<double>& transitionSystem, storm::models::AtomicPropositionsLabeling& labeling) : transitionSystem(transitionSystem), labeling(labeling) {
// Intentionally left empty.
}
ResultContainer(storm::storage::SparseMatrix<double>&& transitionSystem, storm::models::AtomicPropositionsLabeling&& labeling) : transitionSystem(std::move(transitionSystem)), labeling(std::move(labeling)) {
Result(storm::storage::SparseMatrix<double>&& transitionSystem, storm::models::AtomicPropositionsLabeling&& labeling) : transitionSystem(std::move(transitionSystem)), labeling(std::move(labeling)) {
// Intentionally left empty.
}
@ -80,7 +80,7 @@ private:
/*!
* @brief Call sub-parsers on the given files and fill the container with the results.
*/
static ResultContainer parseDeterministicModel(std::string const & transitionSystemFile,
static Result parseDeterministicModel(std::string const & transitionSystemFile,
std::string const & labelingFile,
std::string const & stateRewardFile = "",
std::string const & transitionRewardFile = "");

113
src/parser/NondeterministicModelParser.cpp
View File

@ -15,63 +15,64 @@
#include "src/parser/SparseStateRewardParser.h"
namespace storm {
namespace parser {
namespace parser {
/*!
* Parses a transition file and a labeling file and produces an intermediate Result Container
* 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)
* @param stateRewardFile String containing the location of the state reward file (...srew)
* @param transitionRewardFile String containing the location of the transition reward file (...trew)
*/
NondeterministicModelParserResultContainer<double> parseNondeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile,
std::string const & stateRewardFile, std::string const & transitionRewardFile) {
NondeterministicSparseTransitionParser::Result transitionParserResult(std::move(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(transitionSystemFile)));
storm::storage::SparseMatrix<double> transitions(std::move(transitionParserResult.transitionMatrix));
uint_fast64_t stateCount = transitions.getColumnCount();
uint_fast64_t rowCount = transitions.getRowCount();
storm::models::AtomicPropositionsLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser(stateCount, labelingFile)));
NondeterministicModelParserResultContainer<double> result(std::move(transitions), std::move(transitionParserResult.rowMapping), std::move(labeling));
if (stateRewardFile != "") {
result.stateRewards.reset(storm::parser::SparseStateRewardParser::parseSparseStateReward(stateCount, stateRewardFile));
}
if (transitionRewardFile != "") {
RewardMatrixInformationStruct rewardMatrixInfo(rowCount, stateCount, &result.rowMapping);
result.transitionRewards.reset(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(transitionRewardFile, rewardMatrixInfo).transitionMatrix);
}
return result;
}
/*!
* Uses the Function parseNondeterministicModel internally to parse the given input files.
* @note This is a Short-Hand for Constructing a Mdp directly from the data returned by @parseNondeterministicModel
* @return A Mdp Model
*/
storm::models::Mdp<double> NondeterministicModelParserAsMdp(std::string const & transitionSystemFile, std::string const & labelingFile,
std::string const & stateRewardFile, std::string const & transitionRewardFile) {
NondeterministicModelParserResultContainer<double> parserResult = parseNondeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
return storm::models::Mdp<double>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
}
/*!
* Uses the Function parseNondeterministicModel internally to parse the given input files.
* @note This is a Short-Hand for Constructing a Ctmdp directly from the data returned by @parseNondeterministicModel
* @return A Ctmdp Model
*/
storm::models::Ctmdp<double> NondeterministicModelParserAsCtmdp(std::string const & transitionSystemFile, std::string const & labelingFile,
std::string const & stateRewardFile, std::string const & transitionRewardFile) {
NondeterministicModelParserResultContainer<double> parserResult = parseNondeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
return storm::models::Ctmdp<double>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
}
/*!
* Parses a transition file and a labeling file and produces an intermediate Result Container
* 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)
* @param stateRewardFile String containing the location of the state reward file (...srew)
* @param transitionRewardFile String containing the location of the transition reward file (...trew)
*/
NondeterministicModelParser::Result NondeterministicModelParser::parseNondeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile,
std::string const & stateRewardFile, std::string const & transitionRewardFile) {
NondeterministicSparseTransitionParser::Result transitionParserResult(std::move(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(transitionSystemFile)));
storm::storage::SparseMatrix<double> transitions(std::move(transitionParserResult.transitionMatrix));
uint_fast64_t stateCount = transitions.getColumnCount();
uint_fast64_t rowCount = transitions.getRowCount();
storm::models::AtomicPropositionsLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser(stateCount, labelingFile)));
Result result(std::move(transitions), std::move(transitionParserResult.rowMapping), std::move(labeling));
// Only parse state rewards of a file is given.
if (stateRewardFile != "") {
result.stateRewards.reset(storm::parser::SparseStateRewardParser::parseSparseStateReward(stateCount, stateRewardFile));
}
// Only parse transition rewards of a file is given.
if (transitionRewardFile != "") {
RewardMatrixInformationStruct rewardMatrixInfo(rowCount, stateCount, &result.rowMapping);
result.transitionRewards.reset(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(transitionRewardFile, rewardMatrixInfo).transitionMatrix);
}
return result;
}
/*!
* Uses the Function parseNondeterministicModel internally to parse the given input files.
* @note This is a Short-Hand for Constructing a Mdp directly from the data returned by @parseNondeterministicModel
* @return A Mdp Model
*/
storm::models::Mdp<double> NondeterministicModelParser::parseMdp(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) {
Result parserResult = parseNondeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
return storm::models::Mdp<double>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
}
/*!
* Uses the Function parseNondeterministicModel internally to parse the given input files.
* @note This is a Short-Hand for Constructing a Ctmdp directly from the data returned by @parseNondeterministicModel
* @return A Ctmdp Model
*/
storm::models::Ctmdp<double> NondeterministicModelParser::parseCtmdp(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) {
} /* namespace parser */
Result parserResult = parseNondeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
return storm::models::Ctmdp<double>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
}
} /* namespace parser */
} /* namespace storm */

96
src/parser/NondeterministicModelParser.h
View File

@ -13,52 +13,68 @@
#include "src/models/Ctmdp.h"
namespace storm {
namespace parser {
namespace parser {
class NondeterministicModelParser {
/*!
* @brief Load label and transition file and return initialized mdp object
*
* @note This class creates a new Mdp object that can
* be accessed via getMdp(). 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 mdp.
*/
public:
storm::models::Mdp<double> NondeterministicModelParserAsMdp(std::string const & transitionSystemFile, std::string const & labelingFile,
std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "");
storm::models::Ctmdp<double> NondeterministicModelParserAsCtmdp(std::string const & transitionSystemFile, std::string const & labelingFile,
std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "");
/*!
* @brief This Class acts as a container much like std::pair for the five return values of the NondeterministicModelParser
*/
struct Result {
Result(storm::storage::SparseMatrix<double>& transitionSystem, std::vector<uint_fast64_t>& rowMapping, storm::models::AtomicPropositionsLabeling& labeling) : transitionSystem(transitionSystem), labeling(labeling), rowMapping(rowMapping) {
// Intentionally left empty.
}
/*!
* @brief This Class acts as a container much like std::pair for the five return values of the NondeterministicModelParser
*/
template <class T>
class NondeterministicModelParserResultContainer {
public:
storm::storage::SparseMatrix<T> transitionSystem;
storm::models::AtomicPropositionsLabeling labeling;
std::vector<uint_fast64_t> rowMapping;
boost::optional<std::vector<T>> stateRewards;
boost::optional<storm::storage::SparseMatrix<T>> transitionRewards;
NondeterministicModelParserResultContainer(storm::storage::SparseMatrix<T>& transitionSystem, std::vector<uint_fast64_t>& rowMapping, storm::models::AtomicPropositionsLabeling& labeling) : transitionSystem(transitionSystem), labeling(labeling), rowMapping(rowMapping) { }
NondeterministicModelParserResultContainer(storm::storage::SparseMatrix<T>&& transitionSystem, std::vector<uint_fast64_t>&& rowMapping, storm::models::AtomicPropositionsLabeling&& labeling) : transitionSystem(std::move(transitionSystem)), labeling(std::move(labeling)), rowMapping(std::move(rowMapping)) { }
NondeterministicModelParserResultContainer(const NondeterministicModelParserResultContainer & other) : transitionSystem(other.transitionSystem),
labeling(other.labeling), rowMapping(other.rowMapping), stateRewards(other.stateRewards), transitionRewards(other.transitionRewards) {}
NondeterministicModelParserResultContainer(NondeterministicModelParserResultContainer && other) : transitionSystem(std::move(other.transitionSystem)),
labeling(std::move(other.labeling)), rowMapping(std::move(other.rowMapping)), stateRewards(std::move(other.stateRewards)), transitionRewards(std::move(other.transitionRewards)) {}
private:
NondeterministicModelParserResultContainer() {}
};
NondeterministicModelParserResultContainer<double> parseNondeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile,
std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "");
} /* namespace parser */
Result(storm::storage::SparseMatrix<double>&& transitionSystem, std::vector<uint_fast64_t>&& rowMapping, storm::models::AtomicPropositionsLabeling&& labeling) : transitionSystem(std::move(transitionSystem)), labeling(std::move(labeling)), rowMapping(std::move(rowMapping)) {
// Intentionally left empty.
}
// A matrix representing the transitions of the model
storm::storage::SparseMatrix<double> transitionSystem;
// The labels of each state.
storm::models::AtomicPropositionsLabeling labeling;
// A mapping from rows of the matrix to states of the model.
// This resolves the nondeterministic choices inside the transition system.
std::vector<uint_fast64_t> rowMapping;
// Optional rewards for each state.
boost::optional<std::vector<double>> stateRewards;
// Optional rewards for each transition.
boost::optional<storm::storage::SparseMatrix<double>> transitionRewards;
};
/*!
* @brief Load label and transition file and return initialized Mdp object
*
* @note This class creates a new Mdp object that can
* be accessed via getMdp(). 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 mdp.
*/
static storm::models::Mdp<double> parseMdp(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "");
/*!
*
*/
static storm::models::Ctmdp<double> parseCtmdp(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "");
private:
/*!
*
*/
static Result parseNondeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "");
};
} /* namespace parser */
} /* namespace storm */
#endif /* STORM_PARSER_NONDETERMINISTICMODELPARSER_H_ */

2
test/functional/parser/ParseMdpTest.cpp
View File

@ -11,7 +11,7 @@
#include "src/parser/NondeterministicModelParser.h"
TEST(ParseMdpTest, parseAndOutput) {
storm::models::Mdp<double> mdp = storm::parser::NondeterministicModelParserAsMdp(
storm::models::Mdp<double> mdp = storm::parser::NondeterministicModelParser::parseMdp(
STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general_input_01.tra",
STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/pctl_general_input_01.lab");
storm::storage::SparseMatrix<double> const& matrix = mdp.getTransitionMatrix();

Write Preview
Loading…
Cancel
Save