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

Commenting and cleanup. 

-Also threw out a few more unneeded includes.

Next up: Tests and then remerge.


Former-commit-id: 79f35c4409
tempestpy_adaptions
masawei 11 years ago
parent
fe7afc727f
commit
52f130ea5c
21 changed files with 893 additions and 779 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. 8
      src/parser/AtomicPropositionLabelingParser.cpp
  2. 17
      src/parser/AtomicPropositionLabelingParser.h
  3. 29
      src/parser/AutoParser.cpp
  4. 44
      src/parser/AutoParser.h
  5. 76
      src/parser/DeterministicModelParser.cpp
  6. 189
      src/parser/DeterministicModelParser.h
  7. 4
      src/parser/DeterministicSparseTransitionParser.cpp
  8. 157
      src/parser/DeterministicSparseTransitionParser.h
  9. 35
      src/parser/MappedFile.cpp
  10. 86
      src/parser/MappedFile.h
  11. 48
      src/parser/MarkovAutomatonParser.cpp
  12. 49
      src/parser/MarkovAutomatonParser.h
  13. 435
      src/parser/MarkovAutomatonSparseTransitionParser.cpp
  14. 181
      src/parser/MarkovAutomatonSparseTransitionParser.h
  15. 42
      src/parser/NondeterministicModelParser.cpp
  16. 87
      src/parser/NondeterministicModelParser.h
  17. 4
      src/parser/NondeterministicSparseTransitionParser.cpp
  18. 53
      src/parser/NondeterministicSparseTransitionParser.h
  19. 86
      src/parser/SparseStateRewardParser.cpp
  20. 38
      src/parser/SparseStateRewardParser.h
  21. 4
      test/functional/parser/MarkovAutomatonParserTest.cpp

8
src/parser/AtomicPropositionLabelingParser.cpp
View File

@ -25,7 +25,7 @@ namespace storm {
using namespace storm::utility::cstring;
storm::models::AtomicPropositionsLabeling AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(uint_fast64_t node_count, std::string const & filename) {
storm::models::AtomicPropositionsLabeling AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(uint_fast64_t stateCount, std::string const & filename) {
// Open the given file.
if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) {
@ -34,7 +34,7 @@ namespace storm {
}
MappedFile file(filename.c_str());
char* buf = file.data;
char* buf = file.getData();
// First pass: Count the number of propositions.
bool foundDecl = false, foundEnd = false;
@ -76,11 +76,11 @@ namespace storm {
// Create labeling object with given node and proposition count.
storm::models::AtomicPropositionsLabeling labeling(node_count, proposition_count);
storm::models::AtomicPropositionsLabeling labeling(stateCount, proposition_count);
// Second pass: Add propositions and node labels to labeling.
// First thing to do: Reset the file pointer.
buf = file.data;
buf = file.getData();
// Prepare a buffer for proposition names.
char proposition[128];

17
src/parser/AtomicPropositionLabelingParser.h
View File

@ -7,18 +7,23 @@
namespace storm {
namespace parser {
/*!
* This class can be used to parse a labeling file.
*
* Since the labeling is state based, the same label parser can be used for all models.
*/
class AtomicPropositionLabelingParser {
public:
/*
* Reads a label file and puts the result in an AtomicPropositionsLabeling object.
/*!
* Reads a label file and puts the result in an AtomicPropositionsLabeling object.
*
* @param node_count The number of states of the model to be labeled.
* @param filename The path and name of the labeling (.lab) file.
* @return The parsed labeling as an AtomicPropositionsLabeling object.
* @param stateCount The number of states of the model to be labeled.
* @param filename The path and name of the labeling (.lab) file.
* @return The parsed labeling as an AtomicPropositionsLabeling object.
*/
static storm::models::AtomicPropositionsLabeling parseAtomicPropositionLabeling(uint_fast64_t node_count, std::string const &filename);
static storm::models::AtomicPropositionsLabeling parseAtomicPropositionLabeling(uint_fast64_t stateCount, std::string const &filename);
};

29
src/parser/AutoParser.cpp
View File

@ -22,19 +22,19 @@ namespace storm {
using namespace storm::utility::cstring;
std::shared_ptr<storm::models::AbstractModel<double>> AutoParser::parseModel(std::string const & transitionSystemFile,
std::string const & labelingFile,
std::string const & stateRewardFile,
std::string const & transitionRewardFile) {
std::shared_ptr<storm::models::AbstractModel<double>> AutoParser::parseModel(std::string const & transitionsFilename,
std::string const & labelingFilename,
std::string const & stateRewardFilename,
std::string const & transitionRewardFilename) {
// Find and parse the model type hint.
storm::models::ModelType type = AutoParser::analyzeHint(transitionSystemFile);
storm::models::ModelType type = AutoParser::analyzeHint(transitionsFilename);
// In case the hint string is unknown or could not be found, throw an exception.
if (type == storm::models::Unknown) {
LOG4CPLUS_ERROR(logger, "Could not determine file type of " << transitionSystemFile << ".");
LOG4CPLUS_ERROR(logger, "Could not determine file type of " << transitionsFilename << ".");
LOG4CPLUS_ERROR(logger, "The first line of the file should contain a format hint. Please fix your file and try again.");
throw storm::exceptions::WrongFormatException() << "Could not determine type of file " << transitionSystemFile;
throw storm::exceptions::WrongFormatException() << "Could not determine type of file " << transitionsFilename;
} else {
LOG4CPLUS_INFO(logger, "Model type seems to be " << type);
}
@ -43,23 +43,23 @@ namespace storm {
std::shared_ptr<storm::models::AbstractModel<double>> model;
switch (type) {
case storm::models::DTMC: {
model.reset(new storm::models::Dtmc<double>(std::move(DeterministicModelParser::parseDtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))));
model.reset(new storm::models::Dtmc<double>(std::move(DeterministicModelParser::parseDtmc(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename))));
break;
}
case storm::models::CTMC: {
model.reset(new storm::models::Ctmc<double>(std::move(DeterministicModelParser::parseCtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))));
model.reset(new storm::models::Ctmc<double>(std::move(DeterministicModelParser::parseCtmc(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename))));
break;
}
case storm::models::MDP: {
model.reset(new storm::models::Mdp<double>(std::move(NondeterministicModelParser::parseMdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))));
model.reset(new storm::models::Mdp<double>(std::move(NondeterministicModelParser::parseMdp(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename))));
break;
}
case storm::models::CTMDP: {
model.reset(new storm::models::Ctmdp<double>(std::move(NondeterministicModelParser::parseCtmdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))));
model.reset(new storm::models::Ctmdp<double>(std::move(NondeterministicModelParser::parseCtmdp(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename))));
break;
}
case storm::models::MA: {
model.reset(new storm::models::MarkovAutomaton<double>(storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)));
model.reset(new storm::models::MarkovAutomaton<double>(storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename)));
break;
}
default:
@ -69,12 +69,12 @@ namespace storm {
return model;
}
storm::models::ModelType AutoParser::analyzeHint(const std::string& filename) {
storm::models::ModelType AutoParser::analyzeHint(std::string const & filename) {
storm::models::ModelType hintType = storm::models::Unknown;
// Open the file.
MappedFile file(filename.c_str());
char* buf = file.data;
char* buf = file.getData();
// Find and read in the hint.
char hint[65];
@ -96,5 +96,6 @@ namespace storm {
return hintType;
}
} // namespace parser
} // namespace storm

44
src/parser/AutoParser.h
View File

@ -8,37 +8,43 @@
namespace storm {
/*!
* @brief Contains all file parsers and helper classes.
* Contains all file parsers and helper classes.
*
* This namespace contains everything needed to load data files (like
* atomic propositions, transition systems, formulas, etc.) including
* methods for efficient file access (see MappedFile).
* This namespace contains everything needed to load data files (like
* atomic propositions, transition systems, formulas, etc.) including
* methods for efficient file access (see MappedFile).
*/
namespace parser {
/*!
* This class automatically chooses the correct parser for the given files and returns the corresponding model.
* The choice of the parser is made using the model hint at the beginning of the given transition file.
*/
class AutoParser {
public:
/*!
* Checks the given files and parses the model within these files.
* Checks the given files and parses the model within these files.
*
* This parser analyzes the format hint in the first line of the transition
* file. If this is a valid format, it will use the parser for this format,
* otherwise it will throw an exception.
* This parser analyzes the format hint in the first line of the transition file.
* If this is a valid format, it will use the parser for this format, otherwise it will throw an exception.
*
* When the files are parsed successfully, a shared pointer owning the resulting model is returned.
* The concrete model can be obtained using the as<Type>() member of the AbstractModel class.
* When the files are parsed successfully, a shared pointer owning the resulting model is returned.
* The concrete model can be obtained using the as<Type>() member of the AbstractModel class.
*
* @param transitionsFilename The name of the file containing the transitions of the Markov automaton.
* @param labelingFilename The name of the file containing the labels for the states of the Markov automaton.
* @param stateRewardFilename The name of the file that contains the state reward of the Markov automaton.
* @param transitionRewardFilename The name of the file that contains the transition rewards of the Markov automaton.
* @note The number of states of the model is determined by the transitions file.
* The labeling file may therefore not contain labels of states that are not contained in the transitions file.
*
* @param transitionsFilename The path and name of the file containing the transitions of the model.
* @param labelingFilename The path and name of the file containing the labels for the states of the model.
* @param stateRewardFilename The path and name of the file that contains the state reward of the model. This file is optional.
* @param transitionRewardFilename The path and name of the file that contains the transition rewards of the model. This file is optional.
* @return A shared_ptr containing the resulting model.
*/
static std::shared_ptr<storm::models::AbstractModel<double>> parseModel(std::string const & transitionSystemFile,
std::string const & labelingFile,
std::string const & stateRewardFile = "",
std::string const & transitionRewardFile = "");
static std::shared_ptr<storm::models::AbstractModel<double>> parseModel(std::string const & transitionsFilename,
std::string const & labelingFilename,
std::string const & stateRewardFilename = "",
std::string const & transitionRewardFilename = "");
private:
@ -48,7 +54,7 @@ namespace storm {
* @param filename The path and name of the file that is to be analysed.
* @return The type of the model as an enum value.
*/
static storm::models::ModelType analyzeHint(const std::string& filename);
static storm::models::ModelType analyzeHint(std::string const & filename);
};
} // namespace parser

76
src/parser/DeterministicModelParser.cpp
View File

@ -15,65 +15,45 @@
#include "src/parser/SparseStateRewardParser.h"
namespace storm {
namespace parser {
namespace parser {
/*!
* Parses a transition file and a labeling file
* 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)
*/
DeterministicModelParser::Result 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 & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename, std::string const & transitionRewardFilename) {
// Parse the transitions.
storm::storage::SparseMatrix<double> transitions(std::move(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(transitionSystemFile)));
// Parse the transitions.
storm::storage::SparseMatrix<double> transitions(std::move(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(transitionsFilename)));
uint_fast64_t stateCount = transitions.getColumnCount();
uint_fast64_t stateCount = transitions.getColumnCount();
// Parse the state labeling.
storm::models::AtomicPropositionsLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFile)));
// Parse the state labeling.
storm::models::AtomicPropositionsLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFilename)));
// Construct the result.
DeterministicModelParser::Result result(std::move(transitions), std::move(labeling));
// Construct the result.
DeterministicModelParser::Result result(std::move(transitions), std::move(labeling));
// Only parse state rewards if a file is given.
if (stateRewardFile != "") {
result.stateRewards = storm::parser::SparseStateRewardParser::parseSparseStateReward(stateCount, stateRewardFile);
}
// Only parse state rewards if a file is given.
if (stateRewardFilename != "") {
result.stateRewards = storm::parser::SparseStateRewardParser::parseSparseStateReward(stateCount, stateRewardFilename);
}
// Only parse transition rewards if a file is given.
if (transitionRewardFile != "") {
result.transitionRewards = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(transitionRewardFile, result.transitionSystem);
}
// Only parse transition rewards if a file is given.
if (transitionRewardFilename != "") {
result.transitionRewards = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(transitionRewardFilename, result.transitionSystem);
}
return result;
}
return result;
}
/*!
* Uses the parseDeterministicModel function internally to parse the given input files.
* @note This is a short-hand for constructing a Dtmc directly from the data returned by @parseDeterministicModel
* @return A Dtmc Model
*/
storm::models::Dtmc<double> DeterministicModelParser::parseDtmc(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) {
storm::models::Dtmc<double> DeterministicModelParser::parseDtmc(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename, std::string const & transitionRewardFilename) {
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>>>());
}
/*!
* Uses the parseDeterministicModel function internally to parse the given input files.
* @note This is a short-hand for constructing a Ctmc directly from the data returned by @parseDeterministicModel
* @return A Ctmc Model
*/
storm::models::Ctmc<double> DeterministicModelParser::parseCtmc(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) {
DeterministicModelParser::Result parserResult(std::move(parseDeterministicModel(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename)));
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>>>());
}
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>>>());
}
storm::models::Ctmc<double> DeterministicModelParser::parseCtmc(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename, std::string const & transitionRewardFilename) {
} /* namespace parser */
DeterministicModelParser::Result parserResult(std::move(parseDeterministicModel(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename)));
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>>>());
}
} /* namespace parser */
} /* namespace storm */

189
src/parser/DeterministicModelParser.h
View File

@ -11,83 +11,120 @@
#include "src/models/Dtmc.h"
#include "src/models/Ctmc.h"
#include <boost/optional.hpp>
namespace storm {
namespace parser {
/*!
* @brief Loads a deterministic model (Dtmc or Ctmc) from files.
*
* Given the file paths of the files holding the transitions, the atomic propositions and optionally the state- and transition rewards
* it loads the files, parses them and returns the desired model.
*
* @note This class creates a new Dtmc or Ctmc 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:
/*!
* @brief A struct containing the parsed components of a deterministic model.
*/
struct Result {
Result(storm::storage::SparseMatrix<double>& transitionSystem, storm::models::AtomicPropositionsLabeling& labeling) : transitionSystem(transitionSystem), labeling(labeling) {
// Intentionally left empty.
}
Result(storm::storage::SparseMatrix<double>&& transitionSystem, storm::models::AtomicPropositionsLabeling&& labeling) : transitionSystem(std::move(transitionSystem)), labeling(std::move(labeling)) {
// 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;
// Optional rewards for each state.
boost::optional<std::vector<double>> stateRewards;
// Optional rewards for each transition.
boost::optional<storm::storage::SparseMatrix<double>> transitionRewards;
};
/*!
* @brief Parse a Dtmc.
*/
static storm::models::Dtmc<double> parseDtmc(std::string const & transitionSystemFile,
std::string const & labelingFile,
std::string const & stateRewardFile = "",
std::string const & transitionRewardFile = "");
/*!
* @brief Parse a Ctmc.
*/
static storm::models::Ctmc<double> parseCtmc(std::string const & transitionSystemFile,
std::string const & labelingFile,
std::string const & stateRewardFile = "",
std::string const & transitionRewardFile = "");
private:
/*!
* @brief Call sub-parsers on the given files and fill the container with the results.
*/
static Result parseDeterministicModel(std::string const & transitionSystemFile,
std::string const & labelingFile,
std::string const & stateRewardFile = "",
std::string const & transitionRewardFile = "");
};
} /* namespace parser */
namespace parser {
/*!
* Loads a deterministic model (Dtmc or Ctmc) from files.
*
* Given the file paths of the files holding the transitions, the atomic propositions and optionally the state- and transition rewards
* it loads the files, parses them and returns the desired model.
*/
class DeterministicModelParser {
public:
/*!
* A structure containing the parsed components of a deterministic model.
*/
struct Result {
/*!
* The copy constructor.
*
* @param transitionSystem The transition system to be contained in the Result.
* @param labeling The the labeling of the transition system to be contained in the Result.
*/
Result(storm::storage::SparseMatrix<double>& transitionSystem, storm::models::AtomicPropositionsLabeling& labeling) : transitionSystem(transitionSystem), labeling(labeling) {
// Intentionally left empty.
}
/*!
* The move constructor.
*
* @param transitionSystem The transition system to be contained in the Result.
* @param labeling The the labeling of the transition system to be contained in the Result.
*/
Result(storm::storage::SparseMatrix<double>&& transitionSystem, storm::models::AtomicPropositionsLabeling&& labeling) : transitionSystem(std::move(transitionSystem)), labeling(std::move(labeling)) {
// 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;
//! Optional rewards for each state.
boost::optional<std::vector<double>> stateRewards;
//! Optional rewards for each transition.
boost::optional<storm::storage::SparseMatrix<double>> transitionRewards;
};
/*!
* Parse a Dtmc.
*
* This method is an adapter to the actual parsing function.
* I.e. it uses @parseDeterministicModel internally to parse the given input files, takes its result and compiles it into a Dtmc.
*
* @note The number of states of the model is determined by the transitions file.
* The labeling file may therefore not contain labels of states that are not contained in the transitions file.
*
* @param transitionsFilename The path and name of the file containing the transitions of the model.
* @param labelingFilename The path and name of the file containing the labels for the states of the model.
* @param stateRewardFilename The path and name of the file containing the state reward of the model. This file is optional.
* @param transitionRewardFilename The path and name of the file containing the transition rewards of the model. This file is optional.
* @return The parsed Dtmc.
*/
static storm::models::Dtmc<double> parseDtmc(std::string const & transitionsFilename,
std::string const & labelingFilename,
std::string const & stateRewardFilename = "",
std::string const & transitionRewardFilename = "");
/*!
* Parse a Ctmc.
*
* This method is an adapter to the actual parsing function.
* I.e. it uses @parseDeterministicModel internally to parse the given input files, takes its result and compiles it into a Ctmc.
*
* @note The number of states of the model is determined by the transitions file.
* The labeling file may therefore not contain labels of states that are not contained in the transitions file.
*
* @param transitionsFilename The path and name of the file containing the transitions of the model.
* @param labelingFilename The path and name of the file containing the labels for the states of the model.
* @param stateRewardFilename The path and name of the file containing the state reward of the model. This file is optional.
* @param transitionRewardFilename The path and name of the file containing the transition rewards of the model. This file is optional.
* @return The parsed Ctmc.
*/
static storm::models::Ctmc<double> parseCtmc(std::string const & transitionsFilename,
std::string const & labelingFilename,
std::string const & stateRewardFilename = "",
std::string const & transitionRewardFilename = "");
private:
/*!
* Parses a deterministic model from the given files.
* Calls sub-parsers on the given files and fills the container with the results.
*
* @note The number of states of the model is determined by the transitions file.
* The labeling file may therefore not contain labels of states that are not contained in the transitions file.
*
* @param transitionsFilename The path and name of the file containing the transitions of the model.
* @param labelingFilename The path and name of the file containing the labels for the states of the model.
* @param stateRewardFilename The path and name of the file containing the state reward of the model. This file is optional.
* @param transitionRewardFilename The path and name of the file containing the transition rewards of the model. This file is optional.
* @return The parsed model encapsulated in a Result structure.
*/
static Result parseDeterministicModel(std::string const & transitionsFilename,
std::string const & labelingFilename,
std::string const & stateRewardFilename = "",
std::string const & transitionRewardFilename = "");
};
} /* namespace parser */
} /* namespace storm */
#endif /* STORM_PARSER_DETERMINISTICMODELPARSER_H_ */

4
src/parser/DeterministicSparseTransitionParser.cpp
View File

@ -53,11 +53,11 @@ namespace storm {
// Open file.
MappedFile file(filename.c_str());
char* buf = file.data;
char* buf = file.getData();
// Perform first pass, i.e. count entries that are not zero.
bool insertDiagonalEntriesIfMissing = !isRewardFile;
DeterministicSparseTransitionParser::FirstPassResult firstPass = DeterministicSparseTransitionParser::firstPass(file.data, insertDiagonalEntriesIfMissing);
DeterministicSparseTransitionParser::FirstPassResult firstPass = DeterministicSparseTransitionParser::firstPass(file.getData(), insertDiagonalEntriesIfMissing);
LOG4CPLUS_INFO(logger, "First pass on " << filename << " shows " << firstPass.numberOfNonzeroEntries << " NonZeros.");

157
src/parser/DeterministicSparseTransitionParser.h
View File

@ -4,82 +4,87 @@
#include "src/storage/SparseMatrix.h"
namespace storm {
namespace parser {
class DeterministicSparseTransitionParser {
public:
/*
* A structure representing the result of the first pass of this parser. It contains the number of non-zero entries in the model and the highest state index.
*/
struct FirstPassResult {
FirstPassResult() : numberOfNonzeroEntries(0), highestStateIndex(0) {
// Intentionally left empty.
}
// The total number of non-zero entries of the model.
uint_fast64_t numberOfNonzeroEntries;
// The highest state index that appears in the model.
uint_fast64_t highestStateIndex;
};
/*!
* Load a deterministic transition system from file and create a
* sparse adjacency matrix whose entries represent the weights of the edges.
*
* @param filename The path of file to be parsed.
* @param insertDiagonalEntriesIfMissing A flag set iff entries on the primary diagonal of the matrix should be added in case they are missing in the parsed file.
* @return A SparseMatrix containing the parsed transition system.
*/
static storm::storage::SparseMatrix<double> parseDeterministicTransitions(std::string const& filename);
/*!
* Load the transition rewards for a deterministic transition system from file and create a
* sparse adjacency matrix whose entries represent the rewards of the respective transitions.
*/
/*!
* Load the transition rewards for a deterministic transition system from file and create a
* sparse adjacency matrix whose entries represent the rewards of the respective transitions.
*
* @param filename The path of file to be parsed.
* @param transitionMatrix The transition matrix of the model in which the reward matrix is to be used in.
* The dimensions (rows and columns) of the two matrices should match.
* @return A SparseMatrix containing the parsed transition rewards.
*/
static storm::storage::SparseMatrix<double> parseDeterministicTransitionRewards(std::string const& filename, storm::storage::SparseMatrix<double> const & transitionMatrix);
private:
/*
* Performs the first pass on the input pointed to by the given buffer to obtain the number of
* transitions and the maximum node id.
*
* @param buffer The buffer that cointains the input.
* @param insertDiagonalEntriesIfMissing A flag set iff entries on the primary diagonal of the matrix should be added in case they are missing in the parsed file.
* @return A structure representing the result of the first pass.
*/
static FirstPassResult firstPass(char* buffer, bool insertDiagonalEntriesIfMissing = true);
/*
* The main parsing routine.
* Opens the given file, calls the first pass and performs the second pass, parsing the content of the file into a SparseMatrix.
*
* @param filename The path of file to be parsed.
* @param rewardFile A flag set iff the file to be parsed contains transition rewards.
* @param insertDiagonalEntriesIfMissing A flag set iff entries on the primary diagonal of the matrix should be added in case they are missing in the parsed file.
* @param transitionMatrix The transition matrix of the model in which the reward matrix is to be used in.
* The dimensions (rows and columns) of the two matrices should match.
* @return A SparseMatrix containing the parsed file contents.
*/
static storm::storage::SparseMatrix<double> parse(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix<double> const & transitionMatrix);
};
} // namespace parser
namespace parser {
/*!
* This class can be used to parse a file containing either transitions or transition rewards of a deterministic model.
*
* The file is parsed in two passes.
* The first pass tests the file format and collects statistical data needed for the second pass.
* The second pass then parses the file data and constructs a SparseMatrix representing it.
*/
class DeterministicSparseTransitionParser {
public:
/*!
* A structure representing the result of the first pass of this parser. It contains the number of non-zero entries in the model and the highest state index.
*/
struct FirstPassResult {
/*!
* The default constructor.
* Constructs an empty FirstPassResult.
*/
FirstPassResult() : numberOfNonzeroEntries(0), highestStateIndex(0) {
// Intentionally left empty.
}
//! The total number of non-zero entries of the model.
uint_fast64_t numberOfNonzeroEntries;
//! The highest state index that appears in the model.
uint_fast64_t highestStateIndex;
};
/*!
* Load a deterministic transition system from file and create a
* sparse adjacency matrix whose entries represent the weights of the edges.
*
* @param filename The path and name of the file to be parsed.
* @param insertDiagonalEntriesIfMissing A flag set iff entries on the primary diagonal of the matrix should be added in case they are missing in the parsed file.
* @return A SparseMatrix containing the parsed transition system.
*/
static storm::storage::SparseMatrix<double> parseDeterministicTransitions(std::string const& filename);
/*!
* Load the transition rewards for a deterministic transition system from file and create a
* sparse adjacency matrix whose entries represent the rewards of the respective transitions.
*
* @param filename The path and name of the file to be parsed.
* @param transitionMatrix The transition matrix of the model in which the reward matrix is to be used in.
* The dimensions (rows and columns) of the two matrices should match.
* @return A SparseMatrix containing the parsed transition rewards.
*/
static storm::storage::SparseMatrix<double> parseDeterministicTransitionRewards(std::string const& filename, storm::storage::SparseMatrix<double> const & transitionMatrix);
private:
/*
* Performs the first pass on the input pointed to by the given buffer to obtain the number of
* transitions and the maximum node id.
*
* @param buffer The buffer that contains the input.
* @param insertDiagonalEntriesIfMissing A flag set iff entries on the primary diagonal of the matrix should be added in case they are missing in the parsed file.
* @return A structure representing the result of the first pass.
*/
static FirstPassResult firstPass(char* buffer, bool insertDiagonalEntriesIfMissing = true);
/*
* The main parsing routine.
* Opens the given file, calls the first pass and performs the second pass, parsing the content of the file into a SparseMatrix.
*
* @param filename The path and name of the file to be parsed.
* @param rewardFile A flag set iff the file to be parsed contains transition rewards.
* @param insertDiagonalEntriesIfMissing A flag set iff entries on the primary diagonal of the matrix should be added in case they are missing in the parsed file.
* @param transitionMatrix The transition matrix of the model in which the reward matrix is to be used in.
* The dimensions (rows and columns) of the two matrices should match.
* @return A SparseMatrix containing the parsed file contents.
*/
static storm::storage::SparseMatrix<double> parse(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix<double> const & transitionMatrix);
};
} // namespace parser
} // namespace storm
#endif /* STORM_PARSER_DETERMINISTICSPARSETRANSITIONPARSER_H_ */

35
src/parser/MappedFile.cpp
View File

@ -24,10 +24,10 @@ namespace storm {
MappedFile::MappedFile(const char* filename) {
#if defined LINUX || defined MACOSX
/*
* Do file mapping for reasonable systems.
* stat64(), open(), mmap()
*/
// Do file mapping for reasonable systems.
// stat64(), open(), mmap()
#ifdef MACOSX
if (stat(filename, &(this->st)) != 0) {
#else
@ -49,12 +49,12 @@ namespace storm {
LOG4CPLUS_ERROR(logger, "Error in mmap(" << filename << "): " << std::strerror(errno));
throw exceptions::FileIoException() << "MappedFile Error in mmap(): " << std::strerror(errno);
}
this->dataend = this->data + this->st.st_size;
this->dataEnd = this->data + this->st.st_size;
#elif defined WINDOWS
/*
* Do file mapping for windows.
* _stat64(), CreateFile(), CreateFileMapping(), MapViewOfFile()
*/
// Do file mapping for windows.
// _stat64(), CreateFile(), CreateFileMapping(), MapViewOfFile()
if (_stat64(filename, &(this->st)) != 0) {
LOG4CPLUS_ERROR(logger, "Error in _stat(" << filename << "): Probably, this file does not exist.");
throw exceptions::FileIoException("MappedFile Error in stat(): Probably, this file does not exist.");
@ -80,7 +80,7 @@ namespace storm {
LOG4CPLUS_ERROR(logger, "Error in MapViewOfFile(" << filename << ").");
throw exceptions::FileIoException("MappedFile Error in MapViewOfFile().");
}
this->dataend = this->data + this->st.st_size;
this->dataEnd = this->data + this->st.st_size;
#endif
}
@ -94,10 +94,19 @@ namespace storm {
#endif
}
bool MappedFile::fileExistsAndIsReadable(const char* fileName) {
std::ifstream fin(fileName);
bool MappedFile::fileExistsAndIsReadable(const char* filename) {
// Test by opening an input file stream and testing the stream flags.
std::ifstream fin(filename);
return fin.good();
}
char* MappedFile::getData() {
return data;
}
char* MappedFile::getDataEnd() {
return dataEnd;
}
} // namespace parser
} // namespace storm

86
src/parser/MappedFile.h
View File

@ -14,88 +14,98 @@
namespace storm {
namespace parser {
/*!
* @brief Opens a file and maps it to memory providing a char*
* containing the file content.
*
* This class is a very simple interface to read files efficiently.
* The given file is opened and mapped to memory using mmap().
* The public member data is a pointer to the actual file content.
* Using this method, the kernel will take care of all buffering. This is
* most probably much more efficient than doing this manually.
*/
#if !defined LINUX && !defined MACOSX && !defined WINDOWS
#error Platform not supported
#endif
/*!
* Opens a file and maps it to memory providing a char*
* containing the file content.
*
* This class is a very simple interface to read files efficiently.
* The given file is opened and mapped to memory using mmap().
* The public member data is a pointer to the actual file content.
* Using this method, the kernel will take care of all buffering.
* This is most probably much more efficient than doing this manually.
*/
class MappedFile {
public:
/*!
* Constructor of MappedFile.
* Will stat the given file, open it and map it to memory.
* If anything of this fails, an appropriate exception is raised
* and a log entry is written.
* @param filename file to be opened
* Constructs a MappedFile.
* This will stat the given file, open it and map it to memory.
* If anything of this fails, an appropriate exception is raised and a log entry is written.
*
* @param filename Path and name of the file to be opened.
*/
MappedFile(const char* filename);
/*!
* Destructor of MappedFile.
* Will unmap the data and close the file.
* Destructs a MappedFile.
* This will unmap the data and close the file.
*/
~MappedFile();
/*!
* @brief Tests whether the given file exists and is readable.
* @return True iff the file exists and is readable.
* Tests whether the given file exists and is readable.
*
* @param filename Path and name of the file to be tested.
* @return True iff the file exists and is readable.
*/
static bool fileExistsAndIsReadable(const char* fileName);
static bool fileExistsAndIsReadable(const char* filename);
/*!
* @brief pointer to actual file content.
* Returns a pointer to the beginning of the mapped file data.
*
* @return A pointer to the first character of the mapped file data.
*/
char* data;
char* getData();
/*!
* @brief pointer to end of file content.
* Returns a pointer to the end of the mapped file data.
*
* @return A pointer to the first position after the last character of the mapped file data.
*/
char* dataend;
char* getDataEnd();
private:
//! A pointer to the mapped file content.
char* data;
//! A pointer to end of the mapped file content.
char* dataEnd;
#if defined LINUX || defined MACOSX
/*!
* @brief file descriptor obtained by open().
*/
//! The file descriptor obtained by open().
int file;
#elif defined WINDOWS
//! The file handle obtained by opening the file.
HANDLE file;
//! The handle referencing the created memory mapping.
HANDLE mapping;
#endif
#if defined LINUX
/*!
* @brief stat information about the file.
*/
//! Stat information about the file.
struct stat64 st;
#elif defined MACOSX
/*!
* @brief stat information about the file.
*/
//! Stat information about the file.
struct stat st;
#elif defined WINDOWS
/*!
* @brief stat information about the file.
*/
//! Stat information about the file.
struct __stat64 st;
#endif
};
} // namespace parser
} // namespace storm
#endif /* STORM_PARSER_MAPPEDFILE_H_ */

48
src/parser/MarkovAutomatonParser.cpp
View File

@ -4,38 +4,36 @@
#include "src/exceptions/WrongFormatException.h"
namespace storm {
namespace parser {
namespace parser {
storm::models::MarkovAutomaton<double> MarkovAutomatonParser::parseMarkovAutomaton(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename, std::string const& transitionRewardFilename) {
storm::models::MarkovAutomaton<double> MarkovAutomatonParser::parseMarkovAutomaton(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename, std::string const& transitionRewardFilename) {
// Parse the transitions of the Markov Automaton.
storm::parser::MarkovAutomatonSparseTransitionParser::Result transitionResult(storm::parser::MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions(transitionsFilename));
// Parse the transitions of the Markov Automaton.
storm::parser::MarkovAutomatonSparseTransitionParser::ResultType transitionResult(storm::parser::MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions(transitionsFilename));
// Build the actual transition matrix using the MatrixBuilder provided by the transitionResult.
storm::storage::SparseMatrix<double> transitionMatrix(transitionResult.transitionMatrixBuilder.build(0,0));
// Build the actual transition matrix using the MatrixBuilder provided by the transitionResult.
storm::storage::SparseMatrix<double> transitionMatrix(transitionResult.transitionMatrixBuilder.build(0,0));
// Parse the state labeling.
storm::models::AtomicPropositionsLabeling resultLabeling(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(transitionMatrix.getColumnCount(), labelingFilename));
// Parse the state labeling.
storm::models::AtomicPropositionsLabeling resultLabeling(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(transitionMatrix.getColumnCount(), labelingFilename));
// If given, parse the state rewards file.
boost::optional<std::vector<double>> stateRewards;
if (stateRewardFilename != "") {
stateRewards.reset(storm::parser::SparseStateRewardParser::parseSparseStateReward(transitionMatrix.getColumnCount(), stateRewardFilename));
}
// If given, parse the state rewards file.
boost::optional<std::vector<double>> stateRewards;
if (stateRewardFilename != "") {
stateRewards.reset(storm::parser::SparseStateRewardParser::parseSparseStateReward(transitionMatrix.getColumnCount(), stateRewardFilename));
}
// Since Markov Automata do not support transition rewards no path should be given here.
if (transitionRewardFilename != "") {
LOG4CPLUS_ERROR(logger, "Transition rewards are unsupported for Markov automata.");
throw storm::exceptions::WrongFormatException() << "Transition rewards are unsupported for Markov automata.";
}
// Since Markov Automata do not support transition rewards no path should be given here.
if (transitionRewardFilename != "") {
LOG4CPLUS_ERROR(logger, "Transition rewards are unsupported for Markov automata.");
throw storm::exceptions::WrongFormatException() << "Transition rewards are unsupported for Markov automata.";
}
// Put the pieces together to generate the Markov Automaton.
storm::models::MarkovAutomaton<double> resultingAutomaton(std::move(transitionMatrix), std::move(resultLabeling), std::move(transitionResult.nondeterministicChoiceIndices), std::move(transitionResult.markovianStates), std::move(transitionResult.exitRates), std::move(stateRewards), boost::optional<storm::storage::SparseMatrix<double>>(), boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
// Put the pieces together to generate the Markov Automaton.
storm::models::MarkovAutomaton<double> resultingAutomaton(std::move(transitionMatrix), std::move(resultLabeling), std::move(transitionResult.nondeterministicChoiceIndices), std::move(transitionResult.markovianStates), std::move(transitionResult.exitRates), std::move(stateRewards), boost::optional<storm::storage::SparseMatrix<double>>(), boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
return resultingAutomaton;
}
} // namespace parser
return resultingAutomaton;
}
} // namespace parser
} // namespace storm

49
src/parser/MarkovAutomatonParser.h
View File

@ -5,28 +5,33 @@
#include "src/parser/MarkovAutomatonSparseTransitionParser.h"
namespace storm {
namespace parser {
/*!
* A class providing the functionality to parse a labeled Markov automaton.
*/
class MarkovAutomatonParser {
public:
/*!
* Parses the given Markov automaton and returns an object representing the automaton.
*
* @param transitionsFilename The name of the file containing the transitions of the Markov automaton.
* @param labelingFilename The name of the file containing the labels for the states of the Markov automaton.
* @param stateRewardFilename The name of the file that contains the state reward of the Markov automaton.
* @param transitionRewardFilename The name of the file that contains the transition rewards of the Markov automaton. This should be empty as transition rewards are not supported by Markov Automata.
*/
static storm::models::MarkovAutomaton<double> parseMarkovAutomaton(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename, std::string const& transitionRewardFilename);
};
} // namespace parser
namespace parser {
/*!
* Loads a labeled Markov automaton from files.
*
* Given the file paths of the files holding the transitions, the atomic propositions and optionally the state rewards
* it loads the files, parses them and returns the desired model.
*/
class MarkovAutomatonParser {
public:
/*!
* Parses the given Markov automaton and returns an object representing the automaton.
*
* @note The number of states of the model is determined by the transitions file.
* The labeling file may therefore not contain labels of states that are not contained in the transitions file.
*
* @param transitionsFilename The name of the file containing the transitions of the Markov automaton.
* @param labelingFilename The name of the file containing the labels for the states of the Markov automaton.
* @param stateRewardFilename The name of the file that contains the state reward of the Markov automaton.
* @param transitionRewardFilename The name of the file that contains the transition rewards of the Markov automaton. This should be empty as transition rewards are not supported by Markov Automata.
* @return The parsed MarkovAutomaton.
*/
static storm::models::MarkovAutomaton<double> parseMarkovAutomaton(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename, std::string const& transitionRewardFilename);
};
} // namespace parser
} // namespace storm
#endif /* STORM_PARSER_MARKOVAUTOMATONPARSER_H_ */

435
src/parser/MarkovAutomatonSparseTransitionParser.cpp
View File

@ -7,268 +7,267 @@
namespace storm {
namespace parser {
namespace parser {
using namespace storm::utility::cstring;
using namespace storm::utility::cstring;
MarkovAutomatonSparseTransitionParser::FirstPassResult MarkovAutomatonSparseTransitionParser::firstPass(char* buf) {
MarkovAutomatonSparseTransitionParser::FirstPassResult result;
MarkovAutomatonSparseTransitionParser::FirstPassResult MarkovAutomatonSparseTransitionParser::firstPass(char* buf) {
MarkovAutomatonSparseTransitionParser::FirstPassResult result;
bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks");
bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks");
// Skip the format hint if it is there.
buf = trimWhitespaces(buf);
if(buf[0] < '0' || buf[0] > '9') {
buf = forwardToLineEnd(buf);
buf = trimWhitespaces(buf);
}
// Skip the format hint if it is there.
buf = trimWhitespaces(buf);
if(buf[0] < '0' || buf[0] > '9') {
buf = forwardToLineEnd(buf);
buf = trimWhitespaces(buf);
}
// Now read the transitions.
uint_fast64_t source, target = 0;
uint_fast64_t lastsource = 0;
bool encounteredEOF = false;
bool stateHasMarkovianChoice = false;
bool stateHasProbabilisticChoice = false;
while (buf[0] != '\0' && !encounteredEOF) {
// At the current point, the next thing to read is the source state of the next choice to come.
source = checked_strtol(buf, &buf);
// Check if we encountered a state index that is bigger than all previously seen ones and record it if necessary.
if (source > result.highestStateIndex) {
result.highestStateIndex = source;
}
// Now read the transitions.
uint_fast64_t source, target = 0;
uint_fast64_t lastsource = 0;
bool encounteredEOF = false;
bool stateHasMarkovianChoice = false;
bool stateHasProbabilisticChoice = false;
while (buf[0] != '\0' && !encounteredEOF) {
// At the current point, the next thing to read is the source state of the next choice to come.
source = checked_strtol(buf, &buf);
// If we have skipped some states, we need to reserve the space for the self-loop insertion in the second pass.
if (source > lastsource + 1) {
if (fixDeadlocks) {
result.numberOfNonzeroEntries += source - lastsource - 1;
result.numberOfChoices += source - lastsource - 1;
} else {
LOG4CPLUS_ERROR(logger, "Found deadlock states (e.g. " << lastsource + 1 << ") during parsing. Please fix them or set the appropriate flag.");
throw storm::exceptions::WrongFormatException() << "Found deadlock states (e.g. " << lastsource + 1 << ") during parsing. Please fix them or set the appropriate flag.";
}
} else if (source < lastsource) {
LOG4CPLUS_ERROR(logger, "Illegal state choice order. A choice of state " << source << " appears at an illegal position.");
throw storm::exceptions::WrongFormatException() << "Illegal state choice order. A choice of state " << source << " appears at an illegal position.";
}
// Check if we encountered a state index that is bigger than all previously seen ones and record it if necessary.
if (source > result.highestStateIndex) {
result.highestStateIndex = source;
}
++result.numberOfChoices;
// If we have skipped some states, we need to reserve the space for the self-loop insertion in the second pass.
if (source > lastsource + 1) {
if (fixDeadlocks) {
result.numberOfNonzeroEntries += source - lastsource - 1;
result.numberOfChoices += source - lastsource - 1;
} else {
LOG4CPLUS_ERROR(logger, "Found deadlock states (e.g. " << lastsource + 1 << ") during parsing. Please fix them or set the appropriate flag.");
throw storm::exceptions::WrongFormatException() << "Found deadlock states (e.g. " << lastsource + 1 << ") during parsing. Please fix them or set the appropriate flag.";
}
} else if (source < lastsource) {
LOG4CPLUS_ERROR(logger, "Illegal state choice order. A choice of state " << source << " appears at an illegal position.");
throw storm::exceptions::WrongFormatException() << "Illegal state choice order. A choice of state " << source << " appears at an illegal position.";
}
// If we have moved to the next state, we need to clear the flag that stores whether or not the source has a Markovian or probabilistic choice.
if (source != lastsource) {
stateHasMarkovianChoice = false;
stateHasProbabilisticChoice = false;
}
++result.numberOfChoices;
// Record that the current source was the last source.
lastsource = source;
// If we have moved to the next state, we need to clear the flag that stores whether or not the source has a Markovian or probabilistic choice.
if (source != lastsource) {
stateHasMarkovianChoice = false;
stateHasProbabilisticChoice = false;
}
buf = trimWhitespaces(buf);
// Record that the current source was the last source.
lastsource = source;
// Depending on the action name, the choice is either a probabilitic one or a markovian one.
bool isMarkovianChoice = false;
if (buf[0] == '!' && skipWord(buf) - buf == 1) {
isMarkovianChoice = true;
}else {
isMarkovianChoice = false;
}
buf = skipWord(buf);
buf = trimWhitespaces(buf);
if (isMarkovianChoice) {
if (stateHasMarkovianChoice) {
LOG4CPLUS_ERROR(logger, "The state " << source << " has multiple Markovian choices.");
throw storm::exceptions::WrongFormatException() << "The state " << source << " has multiple Markovian choices.";
}
if (stateHasProbabilisticChoice) {
LOG4CPLUS_ERROR(logger, "The state " << source << " has a probabilistic choice preceding a Markovian choice. The Markovian choice must be the first choice listed.");
throw storm::exceptions::WrongFormatException() << "The state " << source << " has a probabilistic choice preceding a Markovian choice. The Markovian choice must be the first choice listed.";
}
stateHasMarkovianChoice = true;
} else {
stateHasProbabilisticChoice = true;
}
// Depending on the action name, the choice is either a probabilitic one or a markovian one.
bool isMarkovianChoice = false;
if (buf[0] == '!' && skipWord(buf) - buf == 1) {
isMarkovianChoice = true;
}else {
isMarkovianChoice = false;
}
buf = skipWord(buf);
// Go to the next line where the transitions start.
buf = forwardToNextLine(buf);
if (isMarkovianChoice) {
if (stateHasMarkovianChoice) {
LOG4CPLUS_ERROR(logger, "The state " << source << " has multiple Markovian choices.");
throw storm::exceptions::WrongFormatException() << "The state " << source << " has multiple Markovian choices.";
}
if (stateHasProbabilisticChoice) {
LOG4CPLUS_ERROR(logger, "The state " << source << " has a probabilistic choice preceding a Markovian choice. The Markovian choice must be the first choice listed.");
throw storm::exceptions::WrongFormatException() << "The state " << source << " has a probabilistic choice preceding a Markovian choice. The Markovian choice must be the first choice listed.";
// Now that we have the source state and the information whether or not the current choice is probabilistic or Markovian, we need to read the list of successors and the probabilities/rates.
bool hasSuccessorState = false;
bool encounteredNewDistribution = false;
uint_fast64_t lastSuccessorState = 0;
// At this point, we need to check whether there is an additional successor or we have reached the next choice for the same or a different state.
do {
buf = trimWhitespaces(buf);
// If the end of the file was reached, we need to abort and check whether we are in a legal state.
if (buf[0] == '\0') {
if (!hasSuccessorState) {
LOG4CPLUS_ERROR(logger, "Premature end-of-file. Expected at least one successor state for state " << source << ".");
throw storm::exceptions::WrongFormatException() << "Premature end-of-file. Expected at least one successor state for state " << source << ".";
} else {
// If there was at least one successor for the current choice, this is legal and we need to move on.
encounteredEOF = true;
}
} else if (buf[0] == '*') {
// As we have encountered a "*", we know that there is an additional successor state for the current choice.
buf= skipWord(buf);
// Now we need to read the successor state and check if we already saw a higher state index.
target = checked_strtol(buf, &buf);
if (target > result.highestStateIndex) {
result.highestStateIndex = target;
}
if (hasSuccessorState && target <= lastSuccessorState) {
LOG4CPLUS_ERROR(logger, "Illegal transition order for source state " << source << ".");
throw storm::exceptions::WrongFormatException() << "Illegal transition order for source state " << source << ".";
}
// And the corresponding probability/rate.
double val = checked_strtod(buf, &buf);
if (val <= 0.0) {
LOG4CPLUS_ERROR(logger, "Illegal probability/rate value for transition from " << source << " to " << target << ": " << val << ".");
throw storm::exceptions::WrongFormatException() << "Illegal probability/rate value for transition from " << source << " to " << target << ": " << val << ".";
}
// We need to record that we found at least one successor state for the current choice.
hasSuccessorState = true;
lastSuccessorState = target;
// As we found a new successor, we need to increase the number of nonzero entries.
++result.numberOfNonzeroEntries;
buf = forwardToNextLine(buf);
} else {
// If it was not a "*", we have to assume that we encountered the beginning of a new choice definition. In this case, we don't move the pointer
// to the buffer, because we still need to read the new source state.
encounteredNewDistribution = true;
}
} while (!encounteredEOF && !encounteredNewDistribution);
}
stateHasMarkovianChoice = true;
} else {
stateHasProbabilisticChoice = true;
return result;
}
// Go to the next line where the transitions start.
buf = forwardToNextLine(buf);
MarkovAutomatonSparseTransitionParser::Result MarkovAutomatonSparseTransitionParser::secondPass(char* buf, FirstPassResult const& firstPassResult) {
Result result(firstPassResult);
// Now that we have the source state and the information whether or not the current choice is probabilistic or Markovian, we need to read the list of successors and the probabilities/rates.
bool hasSuccessorState = false;
bool encounteredNewDistribution = false;
uint_fast64_t lastSuccessorState = 0;
bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks");
// At this point, we need to check whether there is an additional successor or we have reached the next choice for the same or a different state.
do {
// Skip the format hint if it is there.
buf = trimWhitespaces(buf);
// If the end of the file was reached, we need to abort and check whether we are in a legal state.
if (buf[0] == '\0') {
if (!hasSuccessorState) {
LOG4CPLUS_ERROR(logger, "Premature end-of-file. Expected at least one successor state for state " << source << ".");
throw storm::exceptions::WrongFormatException() << "Premature end-of-file. Expected at least one successor state for state " << source << ".";
} else {
// If there was at least one successor for the current choice, this is legal and we need to move on.
encounteredEOF = true;
}
} else if (buf[0] == '*') {
// As we have encountered a "*", we know that there is an additional successor state for the current choice.
buf= skipWord(buf);
// Now we need to read the successor state and check if we already saw a higher state index.
target = checked_strtol(buf, &buf);
if (target > result.highestStateIndex) {
result.highestStateIndex = target;
}
if (hasSuccessorState && target <= lastSuccessorState) {
LOG4CPLUS_ERROR(logger, "Illegal transition order for source state " << source << ".");
throw storm::exceptions::WrongFormatException() << "Illegal transition order for source state " << source << ".";
}
if(buf[0] < '0' || buf[0] > '9') {
buf = forwardToLineEnd(buf);
buf = trimWhitespaces(buf);
}
// And the corresponding probability/rate.
double val = checked_strtod(buf, &buf);
if (val <= 0.0) {
LOG4CPLUS_ERROR(logger, "Illegal probability/rate value for transition from " << source << " to " << target << ": " << val << ".");
throw storm::exceptions::WrongFormatException() << "Illegal probability/rate value for transition from " << source << " to " << target << ": " << val << ".";
// Now read the transitions.
uint_fast64_t source, target = 0;
uint_fast64_t lastsource = 0;
bool encounteredEOF = false;
uint_fast64_t currentChoice = 0;
while (buf[0] != '\0' && !encounteredEOF) {
// At the current point, the next thing to read is the source state of the next choice to come.
source = checked_strtol(buf, &buf);
// If we have skipped some states, we need to insert self-loops if requested.
if (source > lastsource + 1) {
if (fixDeadlocks) {
for (uint_fast64_t index = lastsource + 1; index < source; ++index) {
result.nondeterministicChoiceIndices[index] = currentChoice;
result.transitionMatrixBuilder.addNextValue(currentChoice, index, 1);
++currentChoice;
}
} else {
LOG4CPLUS_ERROR(logger, "Found deadlock states (e.g. " << lastsource + 1 << ") during parsing. Please fix them or set the appropriate flag.");
throw storm::exceptions::WrongFormatException() << "Found deadlock states (e.g. " << lastsource + 1 << ") during parsing. Please fix them or set the appropriate flag.";
}
}
// We need to record that we found at least one successor state for the current choice.
hasSuccessorState = true;
lastSuccessorState = target;
// As we found a new successor, we need to increase the number of nonzero entries.
++result.numberOfNonzeroEntries;
buf = forwardToNextLine(buf);
} else {
// If it was not a "*", we have to assume that we encountered the beginning of a new choice definition. In this case, we don't move the pointer
// to the buffer, because we still need to read the new source state.
encounteredNewDistribution = true;
}
} while (!encounteredEOF && !encounteredNewDistribution);
}
return result;
}
MarkovAutomatonSparseTransitionParser::ResultType MarkovAutomatonSparseTransitionParser::secondPass(char* buf, FirstPassResult const& firstPassResult) {
ResultType result(firstPassResult);
bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks");
// Skip the format hint if it is there.
buf = trimWhitespaces(buf);
if(buf[0] < '0' || buf[0] > '9') {
buf = forwardToLineEnd(buf);
buf = trimWhitespaces(buf);
}
// Now read the transitions.
uint_fast64_t source, target = 0;
uint_fast64_t lastsource = 0;
bool encounteredEOF = false;
uint_fast64_t currentChoice = 0;
while (buf[0] != '\0' && !encounteredEOF) {
// At the current point, the next thing to read is the source state of the next choice to come.
source = checked_strtol(buf, &buf);
// If we have skipped some states, we need to insert self-loops if requested.
if (source > lastsource + 1) {
if (fixDeadlocks) {
for (uint_fast64_t index = lastsource + 1; index < source; ++index) {
result.nondeterministicChoiceIndices[index] = currentChoice;
result.transitionMatrixBuilder.addNextValue(currentChoice, index, 1);
++currentChoice;
if (source != lastsource) {
// If we skipped to a new state we need to record the beginning of the choices in the nondeterministic choice indices.
result.nondeterministicChoiceIndices[source] = currentChoice;
}
} else {
LOG4CPLUS_ERROR(logger, "Found deadlock states (e.g. " << lastsource + 1 << ") during parsing. Please fix them or set the appropriate flag.");
throw storm::exceptions::WrongFormatException() << "Found deadlock states (e.g. " << lastsource + 1 << ") during parsing. Please fix them or set the appropriate flag.";
}
}
if (source != lastsource) {
// If we skipped to a new state we need to record the beginning of the choices in the nondeterministic choice indices.
result.nondeterministicChoiceIndices[source] = currentChoice;
}
// Record that the current source was the last source.
lastsource = source;
// Record that the current source was the last source.
lastsource = source;
buf = trimWhitespaces(buf);
buf = trimWhitespaces(buf);
// Depending on the action name, the choice is either a probabilitic one or a markovian one.
bool isMarkovianChoice = false;
if (buf[0] == '!' && skipWord(buf) - buf == 1) {
isMarkovianChoice = true;
// Depending on the action name, the choice is either a probabilitic one or a markovian one.
bool isMarkovianChoice = false;
if (buf[0] == '!' && skipWord(buf) - buf == 1) {
isMarkovianChoice = true;
// Mark the current state as a Markovian one.
result.markovianStates.set(source, true);
} else {
isMarkovianChoice = false;
}
// Mark the current state as a Markovian one.
result.markovianStates.set(source, true);
} else {
isMarkovianChoice = false;
}
// Go to the next line where the transitions start.
buf = forwardToNextLine(buf);
// Go to the next line where the transitions start.
buf = forwardToNextLine(buf);
// Now that we have the source state and the information whether or not the current choice is probabilistic or Markovian, we need to read the list of successors and the probabilities/rates.
bool encounteredNewDistribution = false;
// Now that we have the source state and the information whether or not the current choice is probabilistic or Markovian, we need to read the list of successors and the probabilities/rates.
bool encounteredNewDistribution = false;
// At this point, we need to check whether there is an additional successor or we have reached the next choice for the same or a different state.
do {
buf = trimWhitespaces(buf);
// At this point, we need to check whether there is an additional successor or we have reached the next choice for the same or a different state.
do {
buf = trimWhitespaces(buf);
// If the end of the file was reached, we need to abort and check whether we are in a legal state.
if (buf[0] == '\0') {
// Under the assumption that the currently open choice has at least one successor (which is given after the first run)
// we may legally stop reading here.
encounteredEOF = true;
} else if (buf[0] == '*') {
// If the end of the file was reached, we need to abort and check whether we are in a legal state.
if (buf[0] == '\0') {
// Under the assumption that the currently open choice has at least one successor (which is given after the first run)
// we may legally stop reading here.
encounteredEOF = true;
} else if (buf[0] == '*') {
// As we have encountered a "*", we know that there is an additional successor state for the current choice.
buf = skipWord(buf);
// As we have encountered a "*", we know that there is an additional successor state for the current choice.
buf = skipWord(buf);
// Now we need to read the successor state and check if we already saw a higher state index.
target = checked_strtol(buf, &buf);
// Now we need to read the successor state and check if we already saw a higher state index.
target = checked_strtol(buf, &buf);
// And the corresponding probability/rate.
double val = checked_strtod(buf, &buf);
// And the corresponding probability/rate.
double val = checked_strtod(buf, &buf);
// Record the value as well as the exit rate in case of a Markovian choice.
result.transitionMatrixBuilder.addNextValue(currentChoice, target, val);
if (isMarkovianChoice) {
result.exitRates[source] += val;
}
// Record the value as well as the exit rate in case of a Markovian choice.
result.transitionMatrixBuilder.addNextValue(currentChoice, target, val);
if (isMarkovianChoice) {
result.exitRates[source] += val;
}
buf = forwardToNextLine(buf);
} else {
// If it was not a "*", we have to assume that we encountered the beginning of a new choice definition. In this case, we don't move the pointer
// to the buffer, because we still need to read the new source state.
encounteredNewDistribution = true;
}
} while (!encounteredEOF && !encounteredNewDistribution);
buf = forwardToNextLine(buf);
} else {
// If it was not a "*", we have to assume that we encountered the beginning of a new choice definition. In this case, we don't move the pointer
// to the buffer, because we still need to read the new source state.
encounteredNewDistribution = true;
++currentChoice;
}
} while (!encounteredEOF && !encounteredNewDistribution);
++currentChoice;
}
// Put a sentinel element at the end.
result.nondeterministicChoiceIndices[firstPassResult.highestStateIndex + 1] = currentChoice;
// Put a sentinel element at the end.
result.nondeterministicChoiceIndices[firstPassResult.highestStateIndex + 1] = currentChoice;
return result;
}
return result;
}
MarkovAutomatonSparseTransitionParser::ResultType MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions(std::string const& filename) {
// Set the locale to correctly recognize floating point numbers.
setlocale(LC_NUMERIC, "C");
MarkovAutomatonSparseTransitionParser::Result MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions(std::string const& filename) {
// Set the locale to correctly recognize floating point numbers.
setlocale(LC_NUMERIC, "C");
if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) {
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable.");
throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": File does not exist or is not readable.";
}
if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) {
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable.");
throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": File does not exist or is not readable.";
}
// Open file and prepare pointer to buffer.
MappedFile file(filename.c_str());
char* buf = file.data;
// Open file and prepare pointer to buffer.
MappedFile file(filename.c_str());
char* buf = file.getData();
return secondPass(buf, firstPass(buf));
}
return secondPass(buf, firstPass(buf));
}
} // namespace parser
} // namespace parser
} // namespace storm

181
src/parser/MarkovAutomatonSparseTransitionParser.h
View File

@ -5,93 +5,102 @@
#include "src/storage/BitVector.h"
namespace storm {
namespace parser {
/*
* A class providing the functionality to parse the transitions of a Markov automaton.
*/
class MarkovAutomatonSparseTransitionParser {
public:
/*
* A structure representing the result of the first pass of this parser. It contains the number of non-zero entries in the model, the highest state index
* and the total number of choices.
*/
struct FirstPassResult {
FirstPassResult() : numberOfNonzeroEntries(0), highestStateIndex(0), numberOfChoices(0) {
// Intentionally left empty.
}
// The total number of non-zero entries of the model.
uint_fast64_t numberOfNonzeroEntries;
// The highest state index that appears in the model.
uint_fast64_t highestStateIndex;
// The total number of nondeterministic choices in the model.
uint_fast64_t numberOfChoices;
};
/*
* A structure representing the result of the parser. It contains the sparse matrix that represents the transitions (along with a vector indicating
* at which index the choices of a given state begin) as well as the exit rates for all Markovian choices.
*/
struct ResultType {
/*
* Creates a new instance of the struct using the result of the first pass to correctly initialize the container.
* @param firstPassResult A reference to the result of the first pass.
namespace parser {
/*!
* A class providing the functionality to parse the transitions of a Markov automaton.
*
* The file is parsed in two passes.
* The first pass tests the file format and collects statistical data needed for the second pass.
* The second pass then collects the actual file data and compiles it into a ResultType.
*/
ResultType(FirstPassResult const& firstPassResult) : transitionMatrixBuilder(firstPassResult.numberOfChoices, firstPassResult.highestStateIndex + 1, firstPassResult.numberOfNonzeroEntries), nondeterministicChoiceIndices(firstPassResult.highestStateIndex + 2), markovianChoices(firstPassResult.numberOfChoices), markovianStates(firstPassResult.highestStateIndex + 1), exitRates(firstPassResult.highestStateIndex + 1) {
// Intentionally left empty.
}
// A matrix representing the transitions of the model.
storm::storage::SparseMatrixBuilder<double> transitionMatrixBuilder;
// A vector indicating which rows of the matrix represent the choices of a given state.
std::vector<uint_fast64_t> nondeterministicChoiceIndices;
// A bit vector indicating which choices are Markovian. By duality, all other choices are probabilitic.
storm::storage::BitVector markovianChoices;
// A bit vector indicating which states possess a Markovian choice.
storm::storage::BitVector markovianStates;
// A vector that stores the exit rates for each state. For all states that do not possess Markovian choices this is equal to 0.
std::vector<double> exitRates;
};
/*!
* Parses the given file under the assumption that it contains a Markov automaton specified in the appropriate format.
*
* @param filename The name of the file to parse.
* @return A structure representing the result of the parser.
*/
static ResultType parseMarkovAutomatonTransitions(std::string const& filename);
private:
/*
* Performs the first pass on the input pointed to by the given buffer.
*
* @param buffer The buffer that cointains the input.
* @return A structure representing the result of the first pass.
*/
static FirstPassResult firstPass(char* buffer);
/*
* Performs the second pass on the input pointed to by the given buffer with the information of the first pass.
*
* @param buffer The buffer that cointains the input.
* @param firstPassResult The result of the first pass performed on the same input.
* @return A structure representing the result of the second pass.
*/
static ResultType secondPass(char* buffer, FirstPassResult const& firstPassResult);
};
} // namespace parser
class MarkovAutomatonSparseTransitionParser {
public:
/*!
* A structure representing the result of the first pass of this parser. It contains the number of non-zero entries in the model, the highest state index
* and the total number of choices.
*/
struct FirstPassResult {
/*!
* The default constructor.
* Constructs an empty FirstPassResult.
*/
FirstPassResult() : numberOfNonzeroEntries(0), highestStateIndex(0), numberOfChoices(0) {
// Intentionally left empty.
}
//! The total number of non-zero entries of the model.
uint_fast64_t numberOfNonzeroEntries;
//! The highest state index that appears in the model.
uint_fast64_t highestStateIndex;
//! The total number of nondeterministic choices in the model.
uint_fast64_t numberOfChoices;
};
/*!
* A structure representing the result of the parser. It contains the sparse matrix that represents the transitions (along with a vector indicating
* at which index the choices of a given state begin) as well as the exit rates for all Markovian choices.
*/
struct Result {
/*!
* Creates a new instance of the struct using the result of the first pass to correctly initialize the container.
*
* @param firstPassResult A reference to the result of the first pass.
*/
Result(FirstPassResult const& firstPassResult) : transitionMatrixBuilder(firstPassResult.numberOfChoices, firstPassResult.highestStateIndex + 1, firstPassResult.numberOfNonzeroEntries), nondeterministicChoiceIndices(firstPassResult.highestStateIndex + 2), markovianChoices(firstPassResult.numberOfChoices), markovianStates(firstPassResult.highestStateIndex + 1), exitRates(firstPassResult.highestStateIndex + 1) {
// Intentionally left empty.
}
//! A matrix representing the transitions of the model.
storm::storage::SparseMatrixBuilder<double> transitionMatrixBuilder;
//! A vector indicating which rows of the matrix represent the choices of a given state.
std::vector<uint_fast64_t> nondeterministicChoiceIndices;
//! A bit vector indicating which choices are Markovian. By duality, all other choices are probabilitic.
storm::storage::BitVector markovianChoices;
//! A bit vector indicating which states possess a Markovian choice.
storm::storage::BitVector markovianStates;
//! A vector that stores the exit rates for each state. For all states that do not possess Markovian choices this is equal to 0.
std::vector<double> exitRates;
};
/*!
* Parses the given file under the assumption that it contains a Markov automaton specified in the appropriate format.
*
* @param filename The name of the file to parse.
* @return A structure representing the result of the parser.
*/
static Result parseMarkovAutomatonTransitions(std::string const& filename);
private:
/*!
* Performs the first pass on the input pointed to by the given buffer.
*
* @param buffer The buffer that cointains the input.
* @return A structure representing the result of the first pass.
*/
static FirstPassResult firstPass(char* buffer);
/*!
* Performs the second pass on the input pointed to by the given buffer with the information of the first pass.
*
* @param buffer The buffer that cointains the input.
* @param firstPassResult The result of the first pass performed on the same input.
* @return A structure representing the result of the second pass.
*/
static Result secondPass(char* buffer, FirstPassResult const& firstPassResult);
};
} // namespace parser
} // namespace storm
#endif /* STORM_PARSER_MARKOVAUTOMATONSPARSETRANSITIONPARSER_H_ */

42
src/parser/NondeterministicModelParser.cpp
View File

@ -17,36 +17,26 @@
namespace storm {
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)
*/
NondeterministicModelParser::Result NondeterministicModelParser::parseNondeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile,
std::string const & stateRewardFile, std::string const & transitionRewardFile) {
NondeterministicModelParser::Result NondeterministicModelParser::parseNondeterministicModel(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename, std::string const & transitionRewardFilename) {
// Parse the transitions.
NondeterministicSparseTransitionParser::Result transitions(std::move(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(transitionSystemFile)));
NondeterministicSparseTransitionParser::Result transitions(std::move(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(transitionsFilename)));
uint_fast64_t stateCount = transitions.transitionMatrix.getColumnCount();
// Parse the state labeling.
storm::models::AtomicPropositionsLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFile)));
storm::models::AtomicPropositionsLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFilename)));
// Only parse state rewards if a file is given.
boost::optional<std::vector<double>> stateRewards;
if (stateRewardFile != "") {
stateRewards = storm::parser::SparseStateRewardParser::parseSparseStateReward(stateCount, stateRewardFile);
if (stateRewardFilename != "") {
stateRewards = storm::parser::SparseStateRewardParser::parseSparseStateReward(stateCount, stateRewardFilename);
}
// Only parse transition rewards if a file is given.
boost::optional<storm::storage::SparseMatrix<double>> transitionRewards;
if (transitionRewardFile != "") {
transitionRewards = storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(transitionRewardFile, transitions).transitionMatrix;
if (transitionRewardFilename != "") {
transitionRewards = storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(transitionRewardFilename, transitions).transitionMatrix;
}
// Construct the result.
@ -57,25 +47,15 @@ namespace storm {
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) {
storm::models::Mdp<double> NondeterministicModelParser::parseMdp(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename, std::string const & transitionRewardFilename) {
Result parserResult = parseNondeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
Result parserResult = parseNondeterministicModel(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename);
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) {
storm::models::Ctmdp<double> NondeterministicModelParser::parseCtmdp(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename, std::string const & transitionRewardFilename) {
Result parserResult = parseNondeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
Result parserResult = parseNondeterministicModel(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename);
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>>>());
}

87
src/parser/NondeterministicModelParser.h
View File

@ -14,62 +14,121 @@
namespace storm {
namespace parser {
/*!
* Loads a nondeterministic model (Mdp or Ctmdp) from files.
*
* Given the file paths of the files holding the transitions, the atomic propositions and optionally the state- and transition rewards
* it loads the files, parses them and returns the desired model.
*/
class NondeterministicModelParser {
public:
/*!
* @brief This Class acts as a container much like std::pair for the five return values of the NondeterministicModelParser
* A structure containing the parsed components of a nondeterministic model.
*/
struct Result {
/*!
* The copy constructor.
*
* @param transitionSystem The transition system to be contained in the Result.
* @param rowMapping The mapping between matrix rows and model states to be contained in the Result.
* @param labeling The the labeling of the transition system to be contained in the 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.
}
/*!
* The move constructor.
*
* @param transitionSystem The transition system to be contained in the Result.
* @param rowMapping The mapping between matrix rows and model states to be contained in the Result.
* @param labeling The the labeling of the transition system to be contained in the Result.
*/
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
/*!
* A matrix representing the transitions of the model
*/
storm::storage::SparseMatrix<double> transitionSystem;
// The labels of each state.
/*!
* 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.
/*!
* 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.
/*!
* Optional rewards for each state.
*/
boost::optional<std::vector<double>> stateRewards;
// Optional rewards for each transition.
/*!
* Optional rewards for each transition.
*/
boost::optional<storm::storage::SparseMatrix<double>> transitionRewards;
};
/*!
* @brief Load label and transition file and return initialized Mdp object
* Parse a Mdp.
*
* @note This class creates a new Mdp object that can
* be accessed via getMdp(). However, it will not delete this object!
* This method is an adapter to the actual parsing function.
* I.e. it uses @parseNondeterministicModel internally to parse the given input files, takes its result and compiles it into a Dtmc.
*
* @note The labeling representation in the file may use at most as much nodes as are specified in the mdp.
* @note The number of states of the model is determined by the transitions file.
* The labeling file may therefore not contain labels of states that are not contained in the transitions file.
*
* @param transitionsFilename The path and name of the file containing the transitions of the model.
* @param labelingFilename The path and name of the file containing the labels for the states of the model.
* @param stateRewardFilename The path and name of the file containing the state reward of the model. This file is optional.
* @param transitionRewardFilename The path and name of the file containing the transition rewards of the model. This file is optional.
* @return The parsed 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::Mdp<double> parseMdp(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename = "", std::string const & transitionRewardFilename = "");
/*!
* Parse a Ctmdp.
*
* This method is an adapter to the actual parsing function.
* I.e. it uses @parseNondeterministicModel internally to parse the given input files, takes its result and compiles it into a Dtmc.
*
* @note The number of states of the model is determined by the transitions file.
* The labeling file may therefore not contain labels of states that are not contained in the transitions file.
*
* @param transitionsFilename The path and name of the file containing the transitions of the model.
* @param labelingFilename The path and name of the file containing the labels for the states of the model.
* @param stateRewardFilename The path and name of the file containing the state reward of the model. This file is optional.
* @param transitionRewardFilename The path and name of the file containing the transition rewards of the model. This file is optional.
* @return The parsed Ctmdp.
*/
static storm::models::Ctmdp<double> parseCtmdp(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 & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename = "", std::string const & transitionRewardFilename = "");
private:
/*!
* Parses a nondeterministic model from the given files.
* Calls sub-parsers on the given files and fills the container with the results.
*
* @note The number of states of the model is determined by the transitions file.
* The labeling file may therefore not contain labels of states that are not contained in the transitions file.
*
* @param transitionsFilename The path and name of the file containing the transitions of the model.
* @param labelingFilename The path and name of the file containing the labels for the states of the model.
* @param stateRewardFilename The path and name of the file containing the state reward of the model. This file is optional.
* @param transitionRewardFilename The path and name of the file containing the transition rewards of the model. This file is optional.
* @return The parsed model encapsulated in a Result structure.
*/
static Result parseNondeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "");
static Result parseNondeterministicModel(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename = "", std::string const & transitionRewardFilename = "");
};

4
src/parser/NondeterministicSparseTransitionParser.cpp
View File

@ -49,10 +49,10 @@ namespace storm {
// Open file.
MappedFile file(filename.c_str());
char* buf = file.data;
char* buf = file.getData();
// Perform first pass, i.e. obtain number of columns, rows and non-zero elements.
NondeterministicSparseTransitionParser::FirstPassResult firstPass = NondeterministicSparseTransitionParser::firstPass(file.data, isRewardFile, modelInformation);
NondeterministicSparseTransitionParser::FirstPassResult firstPass = NondeterministicSparseTransitionParser::firstPass(file.getData(), isRewardFile, modelInformation);
// If first pass returned zero, the file format was wrong.
if (firstPass.numberOfNonzeroEntries == 0) {

53
src/parser/NondeterministicSparseTransitionParser.h
View File

@ -8,27 +8,38 @@
namespace storm {
namespace parser {
/*!
* A class providing the functionality to parse the transitions of a nondeterministic model.
*
* The file is parsed in two passes.
* The first pass tests the file format and collects statistical data needed for the second pass.
* The second pass then collects the actual file data and compiles it into a Result.
*/
class NondeterministicSparseTransitionParser {
public:
/*
/*!
* A structure representing the result of the first pass of this parser.
* It contains the number of non-zero entries in the model, the highest state index and the total number if nondeterministic choices.
*/
struct FirstPassResult {
/*!
* The default constructor.
* Constructs an empty FirstPassResult.
*/
FirstPassResult() : numberOfNonzeroEntries(0), highestStateIndex(0), choices(0) {
// Intentionally left empty.
}
// The total number of non-zero entries of the model.
//! The total number of non-zero entries of the model.
uint_fast64_t numberOfNonzeroEntries;
// The highest state index that appears in the model.
//! The highest state index that appears in the model.
uint_fast64_t highestStateIndex;
// The total number of nondeterministic choices within the transition system.
//! The total number of nondeterministic choices within the transition system.
uint_fast64_t choices;
};
@ -38,37 +49,47 @@ namespace storm {
*/
struct Result {
// Constructs an empty Result.
/*!
* The default constructor.
* Constructs an empty Result.
*/
Result() : transitionMatrix(), rowMapping() {
// Intentionally left empty.
}
// Constructs a Result, initializing its members with the given values.
/*!
* Constructs a Result, initializing its members with the given values.
*
* @param transitionMatrix The matrix containing the parsed transition system.
* @param rowMapping A mapping from rows of the matrix to states of the model.
*/
Result(storm::storage::SparseMatrix<double> transitionMatrix, std::vector<uint_fast64_t> rowMapping) : transitionMatrix(transitionMatrix), rowMapping(rowMapping) {
// Intentionally left empty.
}
// The matrix containing the parsed transition system.
/*!
* The matrix containing the parsed transition system.
*/
storm::storage::SparseMatrix<double> transitionMatrix;
// A mapping from rows of the matrix to states of the model.
// This resolves the nondeterministic choices inside the transition system.
/*!
* 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;
};
/*!
* @brief Load a nondeterministic transition system from file and create a
* sparse adjacency matrix whose entries represent the weights of the edges
* Load a nondeterministic transition system from file and create a sparse adjacency matrix whose entries represent the weights of the edges
*
* @param filename The path of file to be parsed.
* @param filename The path and name of file to be parsed.
*/
static Result parseNondeterministicTransitions(std::string const & filename);
/*!
* @brief Load a nondeterministic transition system from file and create a
* sparse adjacency matrix whose entries represent the weights of the edges
* Load a nondeterministic transition system from file and create a sparse adjacency matrix whose entries represent the weights of the edges
*
* @param filename The path of file to be parsed.
* @param filename The path and name of file to be parsed.
* @param modelInformation The information about the transition structure of nondeterministic model in which the transition rewards shall be used.
* @return A struct containing the parsed file contents, i.e. the transition reward matrix and the mapping between its rows and the states of the model.
*/
@ -95,7 +116,7 @@ namespace storm {
* The main parsing routine.
* Opens the given file, calls the first pass and performs the second pass, parsing the content of the file into a SparseMatrix.
*
* @param filename The path of file to be parsed.
* @param filename The path and name of file to be parsed.
* @param rewardFile A flag set iff the file to be parsed contains transition rewards.
* @param insertDiagonalEntriesIfMissing A flag set iff entries on the primary diagonal of the matrix should be added in case they are missing in the parsed file.
* @param modelInformation A struct containing information that is used to check if the transition reward matrix fits to the rest of the model.

86
src/parser/SparseStateRewardParser.cpp
View File

@ -7,10 +7,7 @@
#include "src/parser/SparseStateRewardParser.h"
#include <iostream>
#include "src/exceptions/WrongFormatException.h"
#include "src/exceptions/FileIoException.h"
#include "src/utility/cstring.h"
#include "src/parser/MappedFile.h"
#include "log4cplus/logger.h"
@ -18,52 +15,43 @@
extern log4cplus::Logger logger;
namespace storm {
namespace parser {
using namespace storm::utility::cstring;
/*!
* Reads a state reward file and puts the result in a state reward vector.
*
* @param stateCount The number of states.
* @param filename The filename of the state reward file.
* @return The created state reward vector.
*/
std::vector<double> SparseStateRewardParser::parseSparseStateReward(uint_fast64_t stateCount, std::string const & filename) {
// Open file.
if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) {
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable.");
throw storm::exceptions::WrongFormatException();
}
MappedFile file(filename.c_str());
char* buf = file.data;
// Create state reward vector with given state count.
std::vector<double> stateRewards(stateCount);
// Now parse state reward assignments.
uint_fast64_t state;
double reward;
// Iterate over states.
while (buf[0] != '\0') {
// Parse state number and reward value.
state = checked_strtol(buf, &buf);
reward = checked_strtod(buf, &buf);
if (reward < 0.0) {
LOG4CPLUS_ERROR(logger, "Expected positive reward value but got \"" << reward << "\".");
throw storm::exceptions::WrongFormatException() << "State reward file specifies illegal reward value.";
namespace parser {
using namespace storm::utility::cstring;
std::vector<double> SparseStateRewardParser::parseSparseStateReward(uint_fast64_t stateCount, std::string const & filename) {
// Open file.
if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) {
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable.");
throw storm::exceptions::WrongFormatException();
}
MappedFile file(filename.c_str());
char* buf = file.getData();
// Create state reward vector with given state count.
std::vector<double> stateRewards(stateCount);
// Now parse state reward assignments.
uint_fast64_t state;
double reward;
// Iterate over states.
while (buf[0] != '\0') {
// Parse state number and reward value.
state = checked_strtol(buf, &buf);
reward = checked_strtod(buf, &buf);
if (reward < 0.0) {
LOG4CPLUS_ERROR(logger, "Expected positive reward value but got \"" << reward << "\".");
throw storm::exceptions::WrongFormatException() << "State reward file specifies illegal reward value.";
}
stateRewards[state] = reward;
buf = trimWhitespaces(buf);
}
return stateRewards;
}
stateRewards[state] = reward;
buf = trimWhitespaces(buf);
}
return stateRewards;
}
} // namespace parser
} // namespace parser
} // namespace storm

38
src/parser/SparseStateRewardParser.h
View File

@ -6,24 +6,26 @@
#include <string>
namespace storm {
namespace parser {
/*!
* A class providing the functionality to parse a the state rewards of a model.
*/
class SparseStateRewardParser {
public:
/*!
* @brief Load state reward file and return vector of state rewards.
*/
static std::vector<double> parseSparseStateReward(uint_fast64_t stateCount, std::string const &filename);
};
} // namespace parser
namespace parser {
/*!
* A class providing the functionality to parse a the state rewards of a model.
*/
class SparseStateRewardParser {
public:
/*!
* Reads a state reward file and puts the result in a state reward vector.
*
* @param stateCount The number of states.
* @param filename The path and name of the state reward file.
* @return The created state reward vector.
*/
static std::vector<double> parseSparseStateReward(uint_fast64_t stateCount, std::string const &filename);
};
} // namespace parser
} // namespace storm
#endif /* STORM_PARSER_SPARSESTATEREWARDPARSER_H_ */

4
test/functional/parser/MarkovAutomatonParserTest.cpp
View File

@ -26,7 +26,7 @@ TEST(MarkovAutomatonSparseTransitionParserTest, BasicParseTest) {
std::string filename = STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_general_input_01.tra";
// Execute the parser.
storm::parser::MarkovAutomatonSparseTransitionParser::ResultType result = storm::parser::MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions(filename);
storm::parser::MarkovAutomatonSparseTransitionParser::Result result = storm::parser::MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions(filename);
// Build the actual transition matrix.
storm::storage::SparseMatrix<double> transitionMatrix(result.transitionMatrixBuilder.build(0,0));
@ -103,7 +103,7 @@ TEST(MarkovAutomatonSparseTransitionParserTest, WhiteSpaceTest) {
std::string filename = STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_whitespace_input_01.tra";
// Execute the parser.
storm::parser::MarkovAutomatonSparseTransitionParser::ResultType result = storm::parser::MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions(filename);
storm::parser::MarkovAutomatonSparseTransitionParser::Result result = storm::parser::MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions(filename);
// Build the actual transition matrix.
storm::storage::SparseMatrix<double> transitionMatrix(result.transitionMatrixBuilder.build(0,0));

Write Preview
Loading…
Cancel
Save