From 52f130ea5c99b4be0d3e731203c76c097e1b5439 Mon Sep 17 00:00:00 2001 From: masawei Date: Fri, 7 Feb 2014 21:19:50 +0100 Subject: [PATCH] Commenting and cleanup. -Also threw out a few more unneeded includes. Next up: Tests and then remerge. Former-commit-id: 79f35c440988e0d279055c89cb9cab097aad0e3f --- .../AtomicPropositionLabelingParser.cpp | 8 +- src/parser/AtomicPropositionLabelingParser.h | 17 +- src/parser/AutoParser.cpp | 29 +- src/parser/AutoParser.h | 44 +- src/parser/DeterministicModelParser.cpp | 76 ++- src/parser/DeterministicModelParser.h | 189 +++++--- .../DeterministicSparseTransitionParser.cpp | 4 +- .../DeterministicSparseTransitionParser.h | 157 ++++--- src/parser/MappedFile.cpp | 35 +- src/parser/MappedFile.h | 86 ++-- src/parser/MarkovAutomatonParser.cpp | 48 +- src/parser/MarkovAutomatonParser.h | 49 +- .../MarkovAutomatonSparseTransitionParser.cpp | 435 +++++++++--------- .../MarkovAutomatonSparseTransitionParser.h | 181 ++++---- src/parser/NondeterministicModelParser.cpp | 42 +- src/parser/NondeterministicModelParser.h | 87 +++- ...NondeterministicSparseTransitionParser.cpp | 4 +- .../NondeterministicSparseTransitionParser.h | 53 ++- src/parser/SparseStateRewardParser.cpp | 86 ++-- src/parser/SparseStateRewardParser.h | 38 +- .../parser/MarkovAutomatonParserTest.cpp | 4 +- 21 files changed, 893 insertions(+), 779 deletions(-) diff --git a/src/parser/AtomicPropositionLabelingParser.cpp b/src/parser/AtomicPropositionLabelingParser.cpp index ad5543476..f56cbb025 100644 --- a/src/parser/AtomicPropositionLabelingParser.cpp +++ b/src/parser/AtomicPropositionLabelingParser.cpp @@ -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]; diff --git a/src/parser/AtomicPropositionLabelingParser.h b/src/parser/AtomicPropositionLabelingParser.h index 976dd9f35..19d172235 100644 --- a/src/parser/AtomicPropositionLabelingParser.h +++ b/src/parser/AtomicPropositionLabelingParser.h @@ -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); }; diff --git a/src/parser/AutoParser.cpp b/src/parser/AutoParser.cpp index d9d6bcfa5..808d36f0b 100644 --- a/src/parser/AutoParser.cpp +++ b/src/parser/AutoParser.cpp @@ -22,19 +22,19 @@ namespace storm { using namespace storm::utility::cstring; - std::shared_ptr> AutoParser::parseModel(std::string const & transitionSystemFile, - std::string const & labelingFile, - std::string const & stateRewardFile, - std::string const & transitionRewardFile) { + std::shared_ptr> 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> model; switch (type) { case storm::models::DTMC: { - model.reset(new storm::models::Dtmc(std::move(DeterministicModelParser::parseDtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); + model.reset(new storm::models::Dtmc(std::move(DeterministicModelParser::parseDtmc(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename)))); break; } case storm::models::CTMC: { - model.reset(new storm::models::Ctmc(std::move(DeterministicModelParser::parseCtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); + model.reset(new storm::models::Ctmc(std::move(DeterministicModelParser::parseCtmc(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename)))); break; } case storm::models::MDP: { - model.reset(new storm::models::Mdp(std::move(NondeterministicModelParser::parseMdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); + model.reset(new storm::models::Mdp(std::move(NondeterministicModelParser::parseMdp(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename)))); break; } case storm::models::CTMDP: { - model.reset(new storm::models::Ctmdp(std::move(NondeterministicModelParser::parseCtmdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); + model.reset(new storm::models::Ctmdp(std::move(NondeterministicModelParser::parseCtmdp(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename)))); break; } case storm::models::MA: { - model.reset(new storm::models::MarkovAutomaton(storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))); + model.reset(new storm::models::MarkovAutomaton(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 diff --git a/src/parser/AutoParser.h b/src/parser/AutoParser.h index 88df0d076..993cbe6bb 100644 --- a/src/parser/AutoParser.h +++ b/src/parser/AutoParser.h @@ -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() 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() 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> parseModel(std::string const & transitionSystemFile, - std::string const & labelingFile, - std::string const & stateRewardFile = "", - std::string const & transitionRewardFile = ""); + static std::shared_ptr> 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 diff --git a/src/parser/DeterministicModelParser.cpp b/src/parser/DeterministicModelParser.cpp index 48b613644..379858b24 100644 --- a/src/parser/DeterministicModelParser.cpp +++ b/src/parser/DeterministicModelParser.cpp @@ -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 transitions(std::move(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(transitionSystemFile))); + // Parse the transitions. + storm::storage::SparseMatrix 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 DeterministicModelParser::parseDtmc(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { + storm::models::Dtmc 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(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); -} - -/*! - * 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 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(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); + } - DeterministicModelParser::Result parserResult(std::move(parseDeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))); - return storm::models::Ctmc(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); -} + storm::models::Ctmc 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(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); + } + } /* namespace parser */ } /* namespace storm */ diff --git a/src/parser/DeterministicModelParser.h b/src/parser/DeterministicModelParser.h index 2143ea820..12aba0470 100644 --- a/src/parser/DeterministicModelParser.h +++ b/src/parser/DeterministicModelParser.h @@ -11,83 +11,120 @@ #include "src/models/Dtmc.h" #include "src/models/Ctmc.h" -#include - 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& transitionSystem, storm::models::AtomicPropositionsLabeling& labeling) : transitionSystem(transitionSystem), labeling(labeling) { - // Intentionally left empty. - } - - Result(storm::storage::SparseMatrix&& 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 transitionSystem; - - // The labels of each state. - storm::models::AtomicPropositionsLabeling labeling; - - // Optional rewards for each state. - boost::optional> stateRewards; - - // Optional rewards for each transition. - boost::optional> transitionRewards; - }; - - - /*! - * @brief Parse a Dtmc. - */ - static storm::models::Dtmc 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 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& 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&& 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 transitionSystem; + + //! The labels of each state. + storm::models::AtomicPropositionsLabeling labeling; + + //! Optional rewards for each state. + boost::optional> stateRewards; + + //! Optional rewards for each transition. + boost::optional> 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 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 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_ */ diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index a127ebde0..883908a53 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -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."); diff --git a/src/parser/DeterministicSparseTransitionParser.h b/src/parser/DeterministicSparseTransitionParser.h index d89490bee..e31ef2291 100644 --- a/src/parser/DeterministicSparseTransitionParser.h +++ b/src/parser/DeterministicSparseTransitionParser.h @@ -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 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 parseDeterministicTransitionRewards(std::string const& filename, storm::storage::SparseMatrix 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 parse(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix 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 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 parseDeterministicTransitionRewards(std::string const& filename, storm::storage::SparseMatrix 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 parse(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix const & transitionMatrix); + + }; + + } // namespace parser } // namespace storm #endif /* STORM_PARSER_DETERMINISTICSPARSETRANSITIONPARSER_H_ */ diff --git a/src/parser/MappedFile.cpp b/src/parser/MappedFile.cpp index c1c654aa7..2b7e13a05 100644 --- a/src/parser/MappedFile.cpp +++ b/src/parser/MappedFile.cpp @@ -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 - diff --git a/src/parser/MappedFile.h b/src/parser/MappedFile.h index da2df3c3d..6de9877d4 100644 --- a/src/parser/MappedFile.h +++ b/src/parser/MappedFile.h @@ -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_ */ diff --git a/src/parser/MarkovAutomatonParser.cpp b/src/parser/MarkovAutomatonParser.cpp index 172d71ecd..91a01c286 100644 --- a/src/parser/MarkovAutomatonParser.cpp +++ b/src/parser/MarkovAutomatonParser.cpp @@ -4,38 +4,36 @@ #include "src/exceptions/WrongFormatException.h" namespace storm { + namespace parser { -namespace parser { + storm::models::MarkovAutomaton MarkovAutomatonParser::parseMarkovAutomaton(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename, std::string const& transitionRewardFilename) { -storm::models::MarkovAutomaton 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 transitionMatrix(transitionResult.transitionMatrixBuilder.build(0,0)); - // Build the actual transition matrix using the MatrixBuilder provided by the transitionResult. - storm::storage::SparseMatrix 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> stateRewards; + if (stateRewardFilename != "") { + stateRewards.reset(storm::parser::SparseStateRewardParser::parseSparseStateReward(transitionMatrix.getColumnCount(), stateRewardFilename)); + } - // If given, parse the state rewards file. - boost::optional> 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 resultingAutomaton(std::move(transitionMatrix), std::move(resultLabeling), std::move(transitionResult.nondeterministicChoiceIndices), std::move(transitionResult.markovianStates), std::move(transitionResult.exitRates), std::move(stateRewards), boost::optional>(), boost::optional>>()); - // Put the pieces together to generate the Markov Automaton. - storm::models::MarkovAutomaton resultingAutomaton(std::move(transitionMatrix), std::move(resultLabeling), std::move(transitionResult.nondeterministicChoiceIndices), std::move(transitionResult.markovianStates), std::move(transitionResult.exitRates), std::move(stateRewards), boost::optional>(), boost::optional>>()); - - return resultingAutomaton; -} - -} // namespace parser + return resultingAutomaton; + } + } // namespace parser } // namespace storm diff --git a/src/parser/MarkovAutomatonParser.h b/src/parser/MarkovAutomatonParser.h index ae8005006..6f3ea5d01 100644 --- a/src/parser/MarkovAutomatonParser.h +++ b/src/parser/MarkovAutomatonParser.h @@ -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 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 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_ */ diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/parser/MarkovAutomatonSparseTransitionParser.cpp index a899632a4..775792897 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.cpp +++ b/src/parser/MarkovAutomatonSparseTransitionParser.cpp @@ -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 diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.h b/src/parser/MarkovAutomatonSparseTransitionParser.h index 954f21a63..c6019d934 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.h +++ b/src/parser/MarkovAutomatonSparseTransitionParser.h @@ -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 transitionMatrixBuilder; - - // A vector indicating which rows of the matrix represent the choices of a given state. - std::vector 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 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 transitionMatrixBuilder; + + //! A vector indicating which rows of the matrix represent the choices of a given state. + std::vector 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 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_ */ diff --git a/src/parser/NondeterministicModelParser.cpp b/src/parser/NondeterministicModelParser.cpp index 82a7f3085..d150b8c84 100644 --- a/src/parser/NondeterministicModelParser.cpp +++ b/src/parser/NondeterministicModelParser.cpp @@ -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> 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> 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 NondeterministicModelParser::parseMdp(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { + storm::models::Mdp 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(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); } - /*! - * 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 NondeterministicModelParser::parseCtmdp(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { + storm::models::Ctmdp 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(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); } diff --git a/src/parser/NondeterministicModelParser.h b/src/parser/NondeterministicModelParser.h index 50a0525fb..376c3e8c6 100644 --- a/src/parser/NondeterministicModelParser.h +++ b/src/parser/NondeterministicModelParser.h @@ -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& transitionSystem, std::vector& 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&& transitionSystem, std::vector&& 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 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 rowMapping; - // Optional rewards for each state. + /*! + * Optional rewards for each state. + */ boost::optional> stateRewards; - // Optional rewards for each transition. + /*! + * Optional rewards for each transition. + */ boost::optional> 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 parseMdp(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); + static storm::models::Mdp 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 parseCtmdp(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); + static storm::models::Ctmdp 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 = ""); }; diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp index 6e7c72246..6dc1ffbc2 100644 --- a/src/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/parser/NondeterministicSparseTransitionParser.cpp @@ -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) { diff --git a/src/parser/NondeterministicSparseTransitionParser.h b/src/parser/NondeterministicSparseTransitionParser.h index d754a39c3..aea0f8fcc 100644 --- a/src/parser/NondeterministicSparseTransitionParser.h +++ b/src/parser/NondeterministicSparseTransitionParser.h @@ -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 transitionMatrix, std::vector 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 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 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. diff --git a/src/parser/SparseStateRewardParser.cpp b/src/parser/SparseStateRewardParser.cpp index c79e6f691..ad4d815de 100644 --- a/src/parser/SparseStateRewardParser.cpp +++ b/src/parser/SparseStateRewardParser.cpp @@ -7,10 +7,7 @@ #include "src/parser/SparseStateRewardParser.h" -#include - #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 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 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 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 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 diff --git a/src/parser/SparseStateRewardParser.h b/src/parser/SparseStateRewardParser.h index 2efe0a937..f9e149e83 100644 --- a/src/parser/SparseStateRewardParser.h +++ b/src/parser/SparseStateRewardParser.h @@ -6,24 +6,26 @@ #include 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 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 parseSparseStateReward(uint_fast64_t stateCount, std::string const &filename); + + }; + + } // namespace parser } // namespace storm #endif /* STORM_PARSER_SPARSESTATEREWARDPARSER_H_ */ diff --git a/test/functional/parser/MarkovAutomatonParserTest.cpp b/test/functional/parser/MarkovAutomatonParserTest.cpp index 77af61ef7..e063f1f35 100644 --- a/test/functional/parser/MarkovAutomatonParserTest.cpp +++ b/test/functional/parser/MarkovAutomatonParserTest.cpp @@ -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 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 transitionMatrix(result.transitionMatrixBuilder.build(0,0));