diff --git a/resources/3rdparty/ltl2dstar-0.5.1/src/APMonom.hpp b/resources/3rdparty/ltl2dstar-0.5.1/src/APMonom.hpp index 30a11cb58..ed8f4ef53 100644 --- a/resources/3rdparty/ltl2dstar-0.5.1/src/APMonom.hpp +++ b/resources/3rdparty/ltl2dstar-0.5.1/src/APMonom.hpp @@ -29,6 +29,10 @@ #include #include +// As TRUE and FALSE are defined to equal true and false on Windows, they need to be undefined. +#undef TRUE +#undef FALSE + /** * Class representing a subset of 2^AP where AP is the set of * atomic propositions (APSet). It stores two bits per AP: diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index 1ac928fa7..65c993ad4 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -71,7 +71,7 @@ class AbstractModel: public std::enable_shared_from_this> { } if (optionalTransitionRewardMatrix) { // Boost::Optional - this->stateRewardVector.reset(new storm::storage::SparseMatrix(optionalTransitionRewardMatrix.get())); + this->transitionRewardMatrix.reset(new storm::storage::SparseMatrix(optionalTransitionRewardMatrix.get())); } } diff --git a/src/models/AbstractNondeterministicModel.h b/src/models/AbstractNondeterministicModel.h index e9f101315..8f1924716 100644 --- a/src/models/AbstractNondeterministicModel.h +++ b/src/models/AbstractNondeterministicModel.h @@ -35,6 +35,25 @@ class AbstractNondeterministicModel: public AbstractModel { nondeterministicChoiceIndices(nondeterministicChoiceIndices) { } + /*! Constructs an abstract non-determinstic model from the given parameters. + * All values are copied. + * @param transitionMatrix The matrix representing the transitions in the model. + * @param stateLabeling The labeling that assigns a set of atomic + * propositions to each state. + * @param choiceIndices A mapping from states to rows in the transition matrix. + * @param stateRewardVector The reward values associated with the states. + * @param transitionRewardMatrix The reward values associated with the transitions of the model. + */ + AbstractNondeterministicModel( + storm::storage::SparseMatrix const& transitionMatrix, + storm::models::AtomicPropositionsLabeling const& stateLabeling, + std::vector const& nondeterministicChoiceIndices, + boost::optional> const& optionalStateRewardVector, + boost::optional> const& optionalTransitionRewardMatrix) + : AbstractModel(transitionMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix) { + this->nondeterministicChoiceIndices.reset(new std::vector(nondeterministicChoiceIndices)); + } + /*! * Destructor. */ diff --git a/src/models/Ctmdp.h b/src/models/Ctmdp.h index 0d6095ea6..abfcb0485 100644 --- a/src/models/Ctmdp.h +++ b/src/models/Ctmdp.h @@ -49,6 +49,27 @@ public: } } + /*! + * Constructs a CTMDP object from the given transition probability matrix and + * the given labeling of the states. + * All values are copied. + * @param probabilityMatrix The transition probability relation of the + * CTMDP given by a matrix. + * @param stateLabeling The labeling that assigns a set of atomic + * propositions to each state. + */ + Ctmdp(storm::storage::SparseMatrix const& probabilityMatrix, + storm::models::AtomicPropositionsLabeling const& stateLabeling, + std::vector const& nondeterministicChoiceIndices, + boost::optional> const& optionalStateRewardVector, + boost::optional> const& optionalTransitionRewardMatrix) + : AbstractNondeterministicModel(probabilityMatrix, stateLabeling, nondeterministicChoiceIndices, optionalStateRewardVector, optionalTransitionRewardMatrix) { + if (!this->checkValidityOfProbabilityMatrix()) { + LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); + throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; + } + } + //! Copy Constructor /*! * Copy Constructor. Performs a deep copy of the given CTMDP. diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 011c148d4..c2c652e0b 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -74,8 +74,8 @@ public: LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; } - if (this->getTransitionRewardMatrix() != nullptr) { - if (!this->getTransitionRewardMatrix()->containsAllPositionsOf(*this->getTransitionMatrix())) { + if (this->hasTransitionRewards()) { + if (!this->getTransitionRewardMatrix().containsAllPositionsOf(this->getTransitionMatrix())) { LOG4CPLUS_ERROR(logger, "Transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist."); throw storm::exceptions::InvalidArgumentException() << "There are transition rewards for nonexistent transitions."; } diff --git a/src/models/Mdp.h b/src/models/Mdp.h index b2a8d285f..6817c458a 100644 --- a/src/models/Mdp.h +++ b/src/models/Mdp.h @@ -51,6 +51,27 @@ public: } } + /*! + * Constructs a MDP object from the given transition probability matrix and + * the given labeling of the states. + * All values are copied. + * @param probabilityMatrix The transition probability relation of the + * MDP given by a matrix. + * @param stateLabeling The labeling that assigns a set of atomic + * propositions to each state. + */ + Mdp(storm::storage::SparseMatrix const& transitionMatrix, + storm::models::AtomicPropositionsLabeling const& stateLabeling, + std::vector const& nondeterministicChoiceIndices, + boost::optional> const& optionalStateRewardVector, + boost::optional> const& optionalTransitionRewardMatrix) + : AbstractNondeterministicModel(transitionMatrix, stateLabeling, nondeterministicChoiceIndices, optionalStateRewardVector, optionalTransitionRewardMatrix) { + if (!this->checkValidityOfProbabilityMatrix()) { + LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); + throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; + } + } + //! Copy Constructor /*! * Copy Constructor. Performs a deep copy of the given MDP. diff --git a/src/parser/AtomicPropositionLabelingParser.cpp b/src/parser/AtomicPropositionLabelingParser.cpp index e2c590b5b..bed9e6d96 100644 --- a/src/parser/AtomicPropositionLabelingParser.cpp +++ b/src/parser/AtomicPropositionLabelingParser.cpp @@ -44,9 +44,9 @@ storm::models::AtomicPropositionsLabeling AtomicPropositionLabelingParser(uint_f /* * Open file. */ - if (!fileExistsAndIsReadable(filename.c_str())) { + if (!storm::parser::fileExistsAndIsReadable(filename.c_str())) { LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable."); - throw storm::exceptions::WrongFormatException(); + throw storm::exceptions::FileIoException() << "The supplied Labeling input file \"" << filename << "\" does not exist or is not readable by this process."; } MappedFile file(filename.c_str()); diff --git a/src/parser/AutoParser.h b/src/parser/AutoParser.h index bfed158d9..0b84a339d 100644 --- a/src/parser/AutoParser.h +++ b/src/parser/AutoParser.h @@ -30,7 +30,7 @@ namespace parser { * can be obtained via getType() and getModel(). */ template -class AutoParser : Parser { +class AutoParser { public: AutoParser(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "") : model(nullptr) { @@ -47,23 +47,19 @@ class AutoParser : Parser { // Do actual parsing switch (type) { case storm::models::DTMC: { - DeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); - this->model = parser.getDtmc(); + this->model.reset(new storm::models::Dtmc(DeterministicModelParserAsDtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))); break; } case storm::models::CTMC: { - DeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); - this->model = parser.getCtmc(); + this->model.reset(new storm::models::Ctmc(DeterministicModelParserAsCtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))); break; } case storm::models::MDP: { - NondeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); - this->model = parser.getMdp(); + this->model.reset(new storm::models::Mdp(NondeterministicModelParserAsMdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))); break; } case storm::models::CTMDP: { - NondeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); - this->model = parser.getCtmdp(); + this->model.reset(new storm::models::Ctmdp(NondeterministicModelParserAsCtmdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))); break; } default: ; // Unknown @@ -71,7 +67,7 @@ class AutoParser : Parser { if (!this->model) { - LOG4CPLUS_WARN(logger, "Model is still null."); + LOG4CPLUS_WARN(logger, "Unknown/Unhandled Model Type. Model is still null."); } } @@ -101,13 +97,44 @@ class AutoParser : Parser { */ storm::models::ModelType analyzeHint(const std::string& filename) { storm::models::ModelType hintType = storm::models::Unknown; + + // Parse the File and check for the Line Endings + storm::parser::SupportedLineEndingsEnum lineEndings = storm::parser::findUsedLineEndings(filename); + // Open file MappedFile file(filename.c_str()); char* buf = file.data; // parse hint char hint[128]; - sscanf(buf, "%s\n", hint); + // %20s => The Input Hint can be AT MOST 120 chars long + switch (lineEndings) { + case storm::parser::SupportedLineEndingsEnum::SlashN: +#ifdef WINDOWS + sscanf_s(buf, "%120s\n", hint, sizeof(hint)); +#else + sscanf(buf, "%120s\n", hint); +#endif + break; + case storm::parser::SupportedLineEndingsEnum::SlashR: +#ifdef WINDOWS + sscanf_s(buf, "%120s\r", hint, sizeof(hint)); +#else + sscanf(buf, "%120s\r", hint); +#endif + break; + case storm::parser::SupportedLineEndingsEnum::SlashRN: +#ifdef WINDOWS + sscanf_s(buf, "%120s\r\n", hint, sizeof(hint)); +#else + sscanf(buf, "%120s\r\n", hint); +#endif + break; + default: + LOG4CPLUS_ERROR(logger, "The given input file \"" << filename << "\" has no or unsupported line endings. Please use either \\r, \\n or \\r\\n."); + throw storm::exceptions::WrongFormatException() << "The given input file \"" << filename << "\" has no or unsupported line endings. Please use either \\r, \\n or \\r\\n."; + } + for (char* c = hint; *c != '\0'; c++) *c = toupper(*c); // check hint diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index 2d2a5a55f..0a2107ff8 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -139,7 +139,7 @@ storm::storage::SparseMatrix DeterministicSparseTransitionParser(std::st if (!fileExistsAndIsReadable(filename.c_str())) { LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable."); - throw storm::exceptions::WrongFormatException(); + throw storm::exceptions::FileIoException() << "The supplied Transition input file \"" << filename << "\" does not exist or is not readable by this process."; } /* diff --git a/src/parser/LtlFileParser.cpp b/src/parser/LtlFileParser.cpp index e50e5411c..7f77ff4da 100644 --- a/src/parser/LtlFileParser.cpp +++ b/src/parser/LtlFileParser.cpp @@ -11,16 +11,7 @@ namespace storm { namespace parser { -LtlFileParser::LtlFileParser() { - // TODO Auto-generated constructor stub - -} - -LtlFileParser::~LtlFileParser() { - // TODO Auto-generated destructor stub -} - -std::list*> LtlFileParser::parseFormulas(std::string filename) { +std::list*> LtlFileParser(std::string filename) { // Open file std::ifstream inputFileStream(filename, std::ios::in); @@ -35,8 +26,7 @@ std::list*> LtlFileParser::pars std::string line; //The while loop reads the input file line by line while (std::getline(inputFileStream, line)) { - LtlParser parser(line); - result.push_back(parser.getFormula()); + result.push_back(storm::parser::LtlParser(line)); } } diff --git a/src/parser/LtlFileParser.h b/src/parser/LtlFileParser.h index ff8162df4..cb187a82f 100644 --- a/src/parser/LtlFileParser.h +++ b/src/parser/LtlFileParser.h @@ -15,26 +15,13 @@ namespace storm { namespace parser { -class LtlFileParser { -public: - /*! - * Constructor - */ - LtlFileParser(); - - /*! - * Destructor - */ - ~LtlFileParser(); - - /*! - * Parses each line of a given file as prctl formula and returns a list containing the results of the parsing. - * - * @param filename - * @return The list of parsed formulas - */ - std::list*> parseFormulas(std::string filename); -}; +/*! + * Parses each line of a given file as prctl formula and returns a list containing the results of the parsing. + * + * @param filename + * @return The list of parsed formulas + */ +std::list*> LtlFileParser(std::string filename); } //namespace parser } //namespace storm diff --git a/src/parser/NondeterministicModelParser.cpp b/src/parser/NondeterministicModelParser.cpp index 69ab188f1..91b44ee1f 100644 --- a/src/parser/NondeterministicModelParser.cpp +++ b/src/parser/NondeterministicModelParser.cpp @@ -18,8 +18,7 @@ namespace storm { namespace parser { /*! - * Parses a transition file and a labeling file and produces a MDP out of them; a pointer to the mdp - * is saved in the field "mdp" + * 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) @@ -27,27 +26,49 @@ namespace parser { * @param stateRewardFile String containing the location of the state reward file (...srew) * @param transitionRewardFile String containing the location of the transition reward file (...trew) */ -NondeterministicModelParser::NondeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile, +NondeterministicModelParserResultContainer parseNondeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { + NondeterministicSparseTransitionParserResult_t nondeterministicSparseTransitionParserResult = storm::parser::NondeterministicSparseTransitionParser(transitionSystemFile); - uint_fast64_t stateCount = nondeterministicSparseTransitionParserResult.first.getColumnCount(); + storm::storage::SparseMatrix resultTransitionSystem = nondeterministicSparseTransitionParserResult.first; + + uint_fast64_t stateCount = resultTransitionSystem.getRowCount(); + + storm::models::AtomicPropositionsLabeling resultLabeling = storm::parser::AtomicPropositionLabelingParser(stateCount, labelingFile); + NondeterministicModelParserResultContainer result(resultTransitionSystem, nondeterministicSparseTransitionParserResult.second, resultLabeling); + if (stateRewardFile != "") { - std::vector stateRewards = storm::parser::SparseStateRewardParser(stateCount, stateRewardFile); + result.stateRewards.reset(storm::parser::SparseStateRewardParser(stateCount, stateRewardFile)); } if (transitionRewardFile != "") { - RewardMatrixInformationStruct* rewardMatrixInfo = new RewardMatrixInformationStruct(nondeterministicSparseTransitionParserResult.first.getRowCount(), nondeterministicSparseTransitionParserResult.first.getColumnCount(), nondeterministicSparseTransitionParserResult.second); - storm::parser::NondeterministicSparseTransitionParser trp(transitionRewardFile, rewardMatrixInfo); + RewardMatrixInformationStruct* rewardMatrixInfo = new RewardMatrixInformationStruct(nondeterministicSparseTransitionParserResult.first.getRowCount(), nondeterministicSparseTransitionParserResult.first.getColumnCount(), &nondeterministicSparseTransitionParserResult.second); + result.transitionRewards.reset(storm::parser::NondeterministicSparseTransitionParser(transitionRewardFile, rewardMatrixInfo).first); delete rewardMatrixInfo; - this->transitionRewardMatrix = trp.getMatrix(); } + return result; +} - this->probabilityMatrix = tp.getMatrix(); - this->stateLabeling = std::shared_ptr(storm::parser::AtomicPropositionLabelingParser(stateCount, labelingFile)); - this->rowMapping = tp.getRowMapping(); +/*! + * 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 NondeterministicModelParserAsMdp(std::string const & transitionSystemFile, std::string const & labelingFile, + std::string const & stateRewardFile, std::string const & transitionRewardFile) { + NondeterministicModelParserResultContainer parserResult = parseNondeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); + return storm::models::Mdp(parserResult.transitionSystem, parserResult.labeling, parserResult.rowMapping, parserResult.stateRewards, parserResult.transitionRewards); +} - this->mdp = nullptr; - this->ctmdp = nullptr; +/*! + * 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 NondeterministicModelParserAsCtmdp(std::string const & transitionSystemFile, std::string const & labelingFile, + std::string const & stateRewardFile, std::string const & transitionRewardFile) { + NondeterministicModelParserResultContainer parserResult = parseNondeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); + return storm::models::Ctmdp(parserResult.transitionSystem, parserResult.labeling, parserResult.rowMapping, parserResult.stateRewards, parserResult.transitionRewards); } } /* namespace parser */ diff --git a/src/parser/NondeterministicModelParser.h b/src/parser/NondeterministicModelParser.h index bdc4c42d4..c74efc8f6 100644 --- a/src/parser/NondeterministicModelParser.h +++ b/src/parser/NondeterministicModelParser.h @@ -24,40 +24,33 @@ namespace parser { * * @note The labeling representation in the file may use at most as much nodes as are specified in the mdp. */ -class NondeterministicModelParser: public storm::parser::Parser { -public: - NondeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile, - std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); - std::shared_ptr> getMdp() { - if (this->mdp == nullptr) { - this->mdp = std::shared_ptr>(new storm::models::Mdp( - this->probabilityMatrix, this->stateLabeling, this->rowMapping, this->stateRewards, this->transitionRewardMatrix - )); - } - return this->mdp; - } +storm::models::Mdp NondeterministicModelParserAsMdp(std::string const & transitionSystemFile, std::string const & labelingFile, + std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); +storm::models::Ctmdp NondeterministicModelParserAsCtmdp(std::string const & transitionSystemFile, std::string const & labelingFile, + std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); - std::shared_ptr> getCtmdp() { - if (this->ctmdp == nullptr) { - this->ctmdp = std::shared_ptr>(new storm::models::Ctmdp( - this->probabilityMatrix, this->stateLabeling, this->rowMapping, this->stateRewards, this->transitionRewardMatrix - )); - } - return this->ctmdp; - } +/*! + * @brief This Class acts as a container much like std::pair for the five return values of the NondeterministicModelParser + */ +template +class NondeterministicModelParserResultContainer { +public: + storm::storage::SparseMatrix transitionSystem; + storm::models::AtomicPropositionsLabeling labeling; + std::vector rowMapping; + boost::optional> stateRewards; + boost::optional> transitionRewards; + NondeterministicModelParserResultContainer(storm::storage::SparseMatrix transitionSystem, std::vector rowMapping, storm::models::AtomicPropositionsLabeling labeling) : transitionSystem(transitionSystem), rowMapping(rowMapping), labeling(labeling) { } private: - std::shared_ptr> probabilityMatrix; - std::shared_ptr stateLabeling; - std::shared_ptr> rowMapping; - std::shared_ptr> stateRewards; - std::shared_ptr> transitionRewardMatrix; - - std::shared_ptr> mdp; - std::shared_ptr> ctmdp; + NondeterministicModelParserResultContainer() {} }; + +NondeterministicModelParserResultContainer parseNondeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile, + std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); + } /* namespace parser */ } /* namespace storm */ diff --git a/src/parser/Parser.cpp b/src/parser/Parser.cpp index 6a266e51d..7f40d508c 100644 --- a/src/parser/Parser.cpp +++ b/src/parser/Parser.cpp @@ -48,6 +48,16 @@ double storm::parser::checked_strtod(const char* str, char** end) { return res; } +/*! + * @brief Tests whether the given file exists and is readable. + * @return True iff the file exists and is readable. + */ +bool storm::parser::fileExistsAndIsReadable(const char* fileName) { + std::ifstream fin(fileName); + bool returnValue = !fin.fail(); + return returnValue; +} + /*! * Skips spaces, tabs, newlines and carriage returns. Returns pointer * to first char that is not a whitespace. @@ -59,6 +69,31 @@ char* storm::parser::trimWhitespaces(char* buf) { return buf; } +/*! + * @briefs Analyzes the given file and tries to find out the used file endings. + */ +storm::parser::SupportedLineEndingsEnum storm::parser::findUsedLineEndings(std::string const& fileName) { + storm::parser::SupportedLineEndingsEnum result = storm::parser::SupportedLineEndingsEnum::Unsupported; + + MappedFile fileMap(fileName.c_str()); + char* buf = nullptr; + char* const bufferEnd = fileMap.dataend; + + bool sawR = false; + for (buf = fileMap.data; buf != bufferEnd; ++buf) { + if (*buf == '\r') { + // check for following \n + if (((buf + sizeof(char)) < bufferEnd) && (*(buf + sizeof(char)) == '\n')) { + return storm::parser::SupportedLineEndingsEnum::SlashRN; + } + return storm::parser::SupportedLineEndingsEnum::SlashR; + } else if (*buf == '\n') { + return storm::parser::SupportedLineEndingsEnum::SlashN; + } + } + return storm::parser::SupportedLineEndingsEnum::Unsupported; +} + /*! * Will stat the given file, open it and map it to memory. * If anything of this fails, an appropriate exception is raised diff --git a/src/parser/Parser.h b/src/parser/Parser.h index 8df1691b9..b86f7c56e 100644 --- a/src/parser/Parser.h +++ b/src/parser/Parser.h @@ -17,6 +17,7 @@ #include #include #include +#include #include #include "src/exceptions/FileIoException.h" @@ -38,25 +39,16 @@ namespace parser { // Intentionally left empty. } - RewardMatrixInformationStruct(uint_fast64_t rowCount, uint_fast64_t columnCount, std::shared_ptr> nondeterministicChoiceIndices) + RewardMatrixInformationStruct(uint_fast64_t rowCount, uint_fast64_t columnCount, std::vector const * const nondeterministicChoiceIndices) : rowCount(rowCount), columnCount(columnCount), nondeterministicChoiceIndices(nondeterministicChoiceIndices) { // Intentionally left empty. } uint_fast64_t rowCount; uint_fast64_t columnCount; - std::shared_ptr> nondeterministicChoiceIndices; + std::vector const * const nondeterministicChoiceIndices; }; - /*! - * @brief Tests whether the given file exists and is readable. - */ - bool fileExistsAndIsReadable(const char* fileName) { - std::ifstream fin(fileName); - bool returnValue = !fin.fail(); - return returnValue; - } - /*! * @brief Opens a file and maps it to memory providing a char* * containing the file content. @@ -123,26 +115,41 @@ namespace parser { ~MappedFile(); }; - class Parser { - //protected: - - }; - /*! - * @brief Parses integer and checks, if something has been parsed. - */ + * @brief Parses integer and checks, if something has been parsed. + */ uint_fast64_t checked_strtol(const char* str, char** end); /*! - * @brief Parses floating point and checks, if something has been parsed. - */ + * @brief Parses floating point and checks, if something has been parsed. + */ double checked_strtod(const char* str, char** end); /*! - * @brief Skips common whitespaces in a string. - */ + * @brief Skips common whitespaces in a string. + */ char* trimWhitespaces(char* buf); + /*! + * @brief Tests whether the given file exists and is readable. + */ + bool fileExistsAndIsReadable(const char* fileName); + + /*! + * @brief Enum Class Type containing all supported file endings. + */ + enum class SupportedLineEndingsEnum : unsigned short { + Unsupported = 0, + SlashR, + SlashN, + SlashRN + }; + + /*! + * @briefs Analyzes the given file and tries to find out the used line endings. + */ + storm::parser::SupportedLineEndingsEnum findUsedLineEndings(std::string const& fileName); + } // namespace parser } // namespace storm diff --git a/src/parser/PrctlFileParser.cpp b/src/parser/PrctlFileParser.cpp index 5658cb774..a54fc3d48 100644 --- a/src/parser/PrctlFileParser.cpp +++ b/src/parser/PrctlFileParser.cpp @@ -13,15 +13,7 @@ namespace storm { namespace parser { -PrctlFileParser::PrctlFileParser() { - //Intentionally left empty -} - -PrctlFileParser::~PrctlFileParser() { - //intentionally left empty -} - -std::list*> PrctlFileParser::parseFormulas(std::string filename) { +std::list*> PrctlFileParser(std::string filename) { // Open file std::ifstream inputFileStream(filename, std::ios::in); diff --git a/src/parser/PrctlFileParser.h b/src/parser/PrctlFileParser.h index 0ddb7fc4f..b2a4335a2 100644 --- a/src/parser/PrctlFileParser.h +++ b/src/parser/PrctlFileParser.h @@ -16,34 +16,12 @@ namespace storm { namespace parser { /*! - * Reads a PRCTL formula from a file and return the formula tree. + * Parses each line of a given file as prctl formula and returns a list containing the results of the parsing. * - * @note - * This class creates a PctlFormula object which can be accessed through the getFormula() method (of base - * class PrctlParser). However, it will not delete this object. + * @param filename + * @return The list of parsed formulas */ -class PrctlFileParser { -public: - /*! - * Constructor - */ - PrctlFileParser(); - - /*! - * Destructor. - * At this time, empty - * - */ - ~PrctlFileParser(); - - /*! - * Parses each line of a given file as prctl formula and returns a list containing the results of the parsing. - * - * @param filename - * @return The list of parsed formulas - */ - std::list*> parseFormulas(std::string filename); -}; +std::list*> PrctlFileParser(std::string filename); } /* namespace parser */ } /* namespace storm */ diff --git a/src/parser/PrctlParser.h b/src/parser/PrctlParser.h index 7e2b3d13d..848d1de99 100644 --- a/src/parser/PrctlParser.h +++ b/src/parser/PrctlParser.h @@ -18,7 +18,7 @@ namespace parser { * This class creates a PctlFormula object which can be accessed through the getFormula() method (of base * class PrctlParser). However, it will not delete this object. */ -class PrctlParser : Parser { +class PrctlParser { public: /*! * Reads a PRCTL formula from its string representation and parses it into a formula tree, consisting of diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index 456b838dc..587c91dc8 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -32,14 +32,14 @@ namespace parser { * closes the file properly, even if an exception is thrown in the parser. In this case, the * exception is passed on to the caller. */ -storm::ir::Program parseFile(std::string const& filename) { +storm::ir::Program PrismParserFromFile(std::string const& filename) { // Open file and initialize result. std::ifstream inputFileStream(filename, std::ios::in); storm::ir::Program result; // Now try to parse the contents of the file. try { - result = parse(inputFileStream, filename); + result = PrismParser(inputFileStream, filename); } catch(std::exception& e) { // In case of an exception properly close the file before passing exception. inputFileStream.close(); @@ -56,7 +56,7 @@ storm::ir::Program parseFile(std::string const& filename) { * If the parser throws an expectation failure exception, i.e. expected input different than the one * provided, this is caught and displayed properly before the exception is passed on. */ -storm::ir::Program parse(std::istream& inputStream, std::string const& filename) { +storm::ir::Program PrismParser(std::istream& inputStream, std::string const& filename) { // Prepare iterators to input. // TODO: Right now, this parses the whole contents of the file into a string first. // While this is usually not necessary, because there exist adapters that make an input stream diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index 01bd2b830..da8ad0941 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -31,7 +31,7 @@ using namespace storm::ir::expressions; * @param filename the name of the file to parse. * @return a shared pointer to the intermediate representation of the PRISM file. */ -storm::ir::Program parseFile(std::string const& filename); +storm::ir::Program PrismParserFromFile(std::string const& filename); /*! * Parses the given input stream into the intermediate representation assuming it complies with @@ -40,15 +40,7 @@ storm::ir::Program parseFile(std::string const& filename); * @param filename the name of the file the input stream belongs to. Used for diagnostics. * @return a shared pointer to the intermediate representation of the PRISM file. */ -storm::ir::Program parse(std::istream& inputStream, std::string const& filename); - -class PrismParser { -public: - - -private: - -}; +storm::ir::Program PrismParser(std::istream& inputStream, std::string const& filename); } // namespace parser diff --git a/src/parser/SparseStateRewardParser.cpp b/src/parser/SparseStateRewardParser.cpp index 1f34ec7d5..a5d43e024 100644 --- a/src/parser/SparseStateRewardParser.cpp +++ b/src/parser/SparseStateRewardParser.cpp @@ -71,6 +71,7 @@ std::vector SparseStateRewardParser(uint_fast64_t stateCount, std::strin buf = trimWhitespaces(buf); } } + return stateRewards; } } // namespace parser diff --git a/src/utility/ErrorHandling.h b/src/utility/ErrorHandling.h index b832b7c69..cf1988b40 100644 --- a/src/utility/ErrorHandling.h +++ b/src/utility/ErrorHandling.h @@ -24,7 +24,14 @@ std::string demangle(char const* symbol) { char temp[128]; // Check for C++ symbol, on Non-MSVC Only - if (sscanf(symbol, "%*[^(]%*[^_]%127[^)+]", temp) == 1) { + int scanResult = 0; +#ifdef WINDOWS + scanResult = sscanf_s(symbol, "%*[^(]%*[^_]%127[^)+]", temp, sizeof(temp)); +#else + scanResult = sscanf(symbol, "%*[^(]%*[^_]%127[^)+]", temp); +#endif + + if (scanResult == 1) { #ifndef WINDOWS char* demangled; if (NULL != (demangled = abi::__cxa_demangle(temp, NULL, NULL, &status))) { @@ -59,7 +66,13 @@ std::string demangle(char const* symbol) { } // Check for C symbol. - if (sscanf(symbol, "%127s", temp) == 1) { + scanResult = 0; +#ifdef WINDOWS + scanResult = sscanf_s(symbol, "%127s", temp, sizeof(temp)); +#else + scanResult = sscanf(symbol, "%127s", temp); +#endif + if (scanResult == 1) { return temp; } diff --git a/test/functional/parser/CslParserTest.cpp b/test/functional/parser/CslParserTest.cpp index f6657289c..fb758e951 100644 --- a/test/functional/parser/CslParserTest.cpp +++ b/test/functional/parser/CslParserTest.cpp @@ -10,144 +10,130 @@ #include "src/parser/CslParser.h" TEST(CslParserTest, parseApOnlyTest) { - std::string ap = "ap"; - storm::parser::CslParser* cslParser = nullptr; + std::string formula = "ap"; + storm::property::csl::AbstractCslFormula* cslFormula = nullptr; ASSERT_NO_THROW( - cslParser = new storm::parser::CslParser(ap); + cslFormula = storm::parser::CslParser(formula); ); - ASSERT_NE(cslParser->getFormula(), nullptr); - - - ASSERT_EQ(ap, cslParser->getFormula()->toString()); - - delete cslParser->getFormula(); - delete cslParser; + ASSERT_NE(cslFormula, nullptr); + ASSERT_EQ(cslFormula->toString(), formula); + delete cslFormula; } TEST(CslParserTest, parsePropositionalFormulaTest) { - storm::parser::CslParser* cslParser = nullptr; + std::string formula = "!(a & b) | a & ! c"; + storm::property::csl::AbstractCslFormula* cslFormula = nullptr; ASSERT_NO_THROW( - cslParser = new storm::parser::CslParser("!(a & b) | a & ! c") + cslFormula = storm::parser::CslParser(formula); ); - ASSERT_NE(cslParser->getFormula(), nullptr); - - - ASSERT_EQ(cslParser->getFormula()->toString(), "(!(a & b) | (a & !c))"); - - delete cslParser->getFormula(); - delete cslParser; + ASSERT_NE(cslFormula, nullptr); + ASSERT_EQ(cslFormula->toString(), "(!(a & b) | (a & !c))"); + delete cslFormula; } TEST(CslParserTest, parseProbabilisticFormulaTest) { - storm::parser::CslParser* cslParser = nullptr; + std::string formula = "P > 0.5 [ F a ]"; + storm::property::csl::AbstractCslFormula* cslFormula = nullptr; ASSERT_NO_THROW( - cslParser = new storm::parser::CslParser("P > 0.5 [ F a ]") + cslFormula = storm::parser::CslParser(formula); ); - ASSERT_NE(cslParser->getFormula(), nullptr); - - storm::property::csl::ProbabilisticBoundOperator* op = static_cast*>(cslParser->getFormula()); + ASSERT_NE(cslFormula, nullptr); + storm::property::csl::ProbabilisticBoundOperator* op = static_cast*>(cslFormula); ASSERT_EQ(storm::property::GREATER, op->getComparisonOperator()); ASSERT_EQ(0.5, op->getBound()); - ASSERT_EQ(cslParser->getFormula()->toString(), "P > 0.500000 [F a]"); - - delete cslParser->getFormula(); - delete cslParser; + ASSERT_EQ(cslFormula->toString(), "P > 0.500000 [F a]"); + delete cslFormula; } TEST(CslParserTest, parseSteadyStateBoundFormulaTest) { - storm::parser::CslParser* cslParser = nullptr; + std::string formula = "S >= 15 [ P < 0.2 [ a U<=3 b ] ]"; + storm::property::csl::AbstractCslFormula* cslFormula = nullptr; ASSERT_NO_THROW( - cslParser = new storm::parser::CslParser("S >= 15 [ P < 0.2 [ a U<=3 b ] ]") + cslFormula = storm::parser::CslParser(formula); ); - ASSERT_NE(cslParser->getFormula(), nullptr); - - storm::property::csl::SteadyStateBoundOperator* op = static_cast*>(cslParser->getFormula()); + ASSERT_NE(cslFormula, nullptr); + storm::property::csl::SteadyStateBoundOperator* op = static_cast*>(cslFormula); ASSERT_EQ(storm::property::GREATER_EQUAL, op->getComparisonOperator()); ASSERT_EQ(15.0, op->getBound()); - ASSERT_EQ("S >= 15.000000 [P < 0.200000 [a U[0.000000,3.000000] b]]", cslParser->getFormula()->toString()); + ASSERT_EQ(cslFormula->toString(), "S >= 15.000000 [P < 0.200000 [a U[0.000000,3.000000] b]]"); - delete cslParser->getFormula(); - delete cslParser; + delete cslFormula; } TEST(CslParserTest, parseSteadyStateNoBoundFormulaTest) { - storm::parser::CslParser* cslParser = nullptr; + std::string formula = "S = ? [ P <= 0.5 [ F<=3 a ] ]"; + storm::property::csl::AbstractCslFormula* cslFormula = nullptr; ASSERT_NO_THROW( - cslParser = new storm::parser::CslParser("S = ? [ P <= 0.5 [ F<=3 a ] ]") + cslFormula = storm::parser::CslParser(formula); ); - ASSERT_NE(cslParser->getFormula(), nullptr); + ASSERT_NE(cslFormula, nullptr); + ASSERT_EQ(cslFormula->toString(), "S = ? [P <= 0.500000 [F[0.000000,3.000000] a]]"); - - ASSERT_EQ(cslParser->getFormula()->toString(), "S = ? [P <= 0.500000 [F[0.000000,3.000000] a]]"); - - delete cslParser->getFormula(); - delete cslParser; + delete cslFormula; } TEST(CslParserTest, parseProbabilisticNoBoundFormulaTest) { - storm::parser::CslParser* cslParser = nullptr; + std::string formula = "P = ? [ a U [3,4] b & (!c) ]"; + storm::property::csl::AbstractCslFormula* cslFormula = nullptr; ASSERT_NO_THROW( - cslParser = new storm::parser::CslParser("P = ? [ a U [3,4] b & (!c) ]") + cslFormula = storm::parser::CslParser(formula); ); - ASSERT_NE(cslParser->getFormula(), nullptr); - - - ASSERT_EQ(cslParser->getFormula()->toString(), "P = ? [a U[3.000000,4.000000] (b & !c)]"); - - delete cslParser->getFormula(); - delete cslParser; + ASSERT_NE(cslFormula, nullptr); + ASSERT_EQ(cslFormula->toString(), "P = ? [a U[3.000000,4.000000] (b & !c)]"); + delete cslFormula; } TEST(CslParserTest, parseComplexFormulaTest) { - storm::parser::CslParser* cslParser = nullptr; + std::string formula = "S<=0.5 [ P <= 0.5 [ a U c ] ] & (P > 0.5 [ G b] | !P < 0.4 [ G P>0.9 [F >=7 a & b] ]) //and a comment"; + storm::property::csl::AbstractCslFormula* cslFormula = nullptr; ASSERT_NO_THROW( - cslParser = new storm::parser::CslParser("S<=0.5 [ P <= 0.5 [ a U c ] ] & (P > 0.5 [ G b] | !P < 0.4 [ G P>0.9 [F >=7 a & b] ]) //and a comment") + cslFormula = storm::parser::CslParser(formula); ); - ASSERT_NE(cslParser->getFormula(), nullptr); - - ASSERT_EQ("(S <= 0.500000 [P <= 0.500000 [a U c]] & (P > 0.500000 [G b] | !P < 0.400000 [G P > 0.900000 [F>=7.000000 (a & b)]]))", cslParser->getFormula()->toString()); - delete cslParser->getFormula(); - delete cslParser; + ASSERT_NE(cslFormula, nullptr); + ASSERT_EQ(cslFormula->toString(), "(S <= 0.500000 [P <= 0.500000 [a U c]] & (P > 0.500000 [G b] | !P < 0.400000 [G P > 0.900000 [F>=7.000000 (a & b)]]))"); + delete cslFormula; } TEST(CslParserTest, wrongProbabilisticFormulaTest) { - storm::parser::CslParser* cslParser = nullptr; - ASSERT_THROW(cslParser = new storm::parser::CslParser("P > 0.5 [ a ]"), storm::exceptions::WrongFormatException); - - delete cslParser; + std::string formula = "P > 0.5 [ a ]"; + storm::property::csl::AbstractCslFormula* cslFormula = nullptr; + ASSERT_THROW( + cslFormula = storm::parser::CslParser(formula), + storm::exceptions::WrongFormatException + ); } TEST(CslParserTest, wrongFormulaTest) { - storm::parser::CslParser* cslParser = nullptr; + std::string formula = "(a | b) & +"; + storm::property::csl::AbstractCslFormula* cslFormula = nullptr; ASSERT_THROW( - cslParser = new storm::parser::CslParser("(a | b) & +"), - storm::exceptions::WrongFormatException + cslFormula = storm::parser::CslParser(formula), + storm::exceptions::WrongFormatException ); - delete cslParser; } TEST(CslParserTest, wrongFormulaTest2) { - storm::parser::CslParser* cslParser = nullptr; + std::string formula = "P>0 [ F & a ]"; + storm::property::csl::AbstractCslFormula* cslFormula = nullptr; ASSERT_THROW( - cslParser = new storm::parser::CslParser("P>0 [ F & a ]"), - storm::exceptions::WrongFormatException + cslFormula = storm::parser::CslParser(formula), + storm::exceptions::WrongFormatException ); - delete cslParser; } diff --git a/test/functional/parser/LtlParserTest.cpp b/test/functional/parser/LtlParserTest.cpp index c88885372..c9f3cad58 100644 --- a/test/functional/parser/LtlParserTest.cpp +++ b/test/functional/parser/LtlParserTest.cpp @@ -10,34 +10,29 @@ #include "src/parser/LtlParser.h" TEST(LtlParserTest, parseApOnlyTest) { - std::string ap = "ap"; - storm::parser::LtlParser* ltlParser = nullptr; + std::string formula = "ap"; + storm::property::ltl::AbstractLtlFormula* ltlFormula = nullptr; ASSERT_NO_THROW( - ltlParser = new storm::parser::LtlParser(ap); + ltlFormula = storm::parser::LtlParser(formula); ); - ASSERT_NE(ltlParser->getFormula(), nullptr); + ASSERT_NE(ltlFormula, nullptr); + ASSERT_EQ(ltlFormula->toString(), formula); - - ASSERT_EQ(ltlParser->getFormula()->toString(), ap); - - delete ltlParser->getFormula(); - delete ltlParser; + delete ltlFormula; } TEST(LtlParserTest, parsePropositionalFormulaTest) { - storm::parser::LtlParser* ltlParser = nullptr; + std::string formula = "!(a & b) | a & ! c"; + storm::property::ltl::AbstractLtlFormula* ltlFormula = nullptr; ASSERT_NO_THROW( - ltlParser = new storm::parser::LtlParser("!(a & b) | a & ! c") + ltlFormula = storm::parser::LtlParser(formula); ); - ASSERT_NE(ltlParser->getFormula(), nullptr); - - - ASSERT_EQ(ltlParser->getFormula()->toString(), "(!(a & b) | (a & !c))"); + ASSERT_NE(ltlFormula, nullptr); + ASSERT_EQ(ltlFormula->toString(), "(!(a & b) | (a & !c))"); - delete ltlParser->getFormula(); - delete ltlParser; + delete ltlFormula; } /*! @@ -45,18 +40,16 @@ TEST(LtlParserTest, parsePropositionalFormulaTest) { * "Eventually" operator. */ TEST(LtlParserTest, parseAmbiguousFormulaTest) { - storm::parser::LtlParser* ltlParser = nullptr; + std::string formula = "F & b"; + storm::property::ltl::AbstractLtlFormula* ltlFormula = nullptr; ASSERT_NO_THROW( - ltlParser = new storm::parser::LtlParser("F & b") + ltlFormula = storm::parser::LtlParser(formula); ); - ASSERT_NE(ltlParser->getFormula(), nullptr); + ASSERT_NE(ltlFormula, nullptr); + ASSERT_EQ(ltlFormula->toString(), "(F & b)"); - - ASSERT_EQ(ltlParser->getFormula()->toString(), "(F & b)"); - - delete ltlParser->getFormula(); - delete ltlParser; + delete ltlFormula; } /*! @@ -64,89 +57,85 @@ TEST(LtlParserTest, parseAmbiguousFormulaTest) { * depending where it occurs. */ TEST(LtlParserTest, parseAmbiguousFormulaTest2) { - storm::parser::LtlParser* ltlParser = nullptr; + std::string formula = "F F"; + storm::property::ltl::AbstractLtlFormula* ltlFormula = nullptr; ASSERT_NO_THROW( - ltlParser = new storm::parser::LtlParser("F F") + ltlFormula = storm::parser::LtlParser(formula); ); - ASSERT_NE(ltlParser->getFormula(), nullptr); - + ASSERT_NE(ltlFormula, nullptr); + ASSERT_EQ(ltlFormula->toString(), "F F"); - ASSERT_EQ(ltlParser->getFormula()->toString(), "F F"); - - delete ltlParser->getFormula(); - delete ltlParser; + delete ltlFormula; } TEST(LtlParserTest, parseBoundedEventuallyFormulaTest) { - storm::parser::LtlParser* ltlParser = nullptr; + std::string formula = "F<=5 a"; + storm::property::ltl::AbstractLtlFormula* ltlFormula = nullptr; ASSERT_NO_THROW( - ltlParser = new storm::parser::LtlParser("F<=5 a") + ltlFormula = storm::parser::LtlParser(formula); ); - ASSERT_NE(ltlParser->getFormula(), nullptr); - - storm::property::ltl::BoundedEventually* op = static_cast*>(ltlParser->getFormula()); + ASSERT_NE(ltlFormula, nullptr); + storm::property::ltl::BoundedEventually* op = static_cast*>(ltlFormula); ASSERT_EQ(static_cast(5), op->getBound()); - ASSERT_EQ(ltlParser->getFormula()->toString(), "F<=5 a"); - delete ltlParser->getFormula(); - delete ltlParser; + ASSERT_EQ(ltlFormula->toString(), "F<=5 a"); + + delete ltlFormula; } TEST(LtlParserTest, parseBoundedUntilFormulaTest) { - storm::parser::LtlParser* ltlParser = nullptr; + std::string formula = "a U<=3 b"; + storm::property::ltl::AbstractLtlFormula* ltlFormula = nullptr; ASSERT_NO_THROW( - ltlParser = new storm::parser::LtlParser("a U<=3 b") + ltlFormula = storm::parser::LtlParser(formula); ); - ASSERT_NE(ltlParser->getFormula(), nullptr); - - storm::property::ltl::BoundedUntil* op = static_cast*>(ltlParser->getFormula()); + ASSERT_NE(ltlFormula, nullptr); + storm::property::ltl::BoundedUntil* op = static_cast*>(ltlFormula); ASSERT_EQ(static_cast(3), op->getBound()); - ASSERT_EQ("(a U<=3 b)", ltlParser->getFormula()->toString()); - delete ltlParser->getFormula(); - delete ltlParser; + ASSERT_EQ(ltlFormula->toString(), formula); + + delete ltlFormula; } TEST(LtlParserTest, parseComplexUntilTest) { - storm::parser::LtlParser* ltlParser = nullptr; + std::string formula = "a U b U<=3 c"; + storm::property::ltl::AbstractLtlFormula* ltlFormula = nullptr; ASSERT_NO_THROW( - ltlParser = new storm::parser::LtlParser("a U b U<=3 c") + ltlFormula = storm::parser::LtlParser(formula); ); - ASSERT_NE(ltlParser->getFormula(), nullptr); - - - ASSERT_EQ(ltlParser->getFormula()->toString(), "((a U b) U<=3 c)"); + ASSERT_NE(ltlFormula, nullptr); + ASSERT_EQ(ltlFormula->toString(), "((a U b) U<=3 c)"); - delete ltlParser->getFormula(); - delete ltlParser; + delete ltlFormula; } TEST(LtlParserTest, parseComplexFormulaTest) { - storm::parser::LtlParser* ltlParser = nullptr; + std::string formula = "a U F b | G a & F<=3 a U<=7 b // and a comment"; + storm::property::ltl::AbstractLtlFormula* ltlFormula = nullptr; ASSERT_NO_THROW( - ltlParser = new storm::parser::LtlParser("a U F b | G a & F<=3 a U<=7 b //and a comment :P") + ltlFormula = storm::parser::LtlParser(formula); ); - ASSERT_NE(ltlParser->getFormula(), nullptr); + ASSERT_NE(ltlFormula, nullptr); + ASSERT_EQ(ltlFormula->toString(), "(a U F (b | G (a & F<=3 (a U<=7 b))))"); - ASSERT_EQ("(a U F (b | G (a & F<=3 (a U<=7 b))))", ltlParser->getFormula()->toString()); - delete ltlParser->getFormula(); - delete ltlParser; + delete ltlFormula; } TEST(LtlParserTest, wrongFormulaTest) { - storm::parser::LtlParser* ltlParser = nullptr; + std::string formula = "(a | c) & +"; + storm::property::ltl::AbstractLtlFormula* ltlFormula = nullptr; ASSERT_THROW( - ltlParser = new storm::parser::LtlParser("(a | c) & +"), - storm::exceptions::WrongFormatException + ltlFormula = storm::parser::LtlParser(formula), + storm::exceptions::WrongFormatException ); - delete ltlParser; } diff --git a/test/functional/parser/ParseMdpTest.cpp b/test/functional/parser/ParseMdpTest.cpp index a379e82c2..58673269d 100644 --- a/test/functional/parser/ParseMdpTest.cpp +++ b/test/functional/parser/ParseMdpTest.cpp @@ -11,21 +11,15 @@ #include "src/parser/NondeterministicModelParser.h" TEST(ParseMdpTest, parseAndOutput) { - storm::parser::NondeterministicModelParser* mdpParser = nullptr; - ASSERT_NO_THROW(mdpParser = new storm::parser::NondeterministicModelParser( - STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general_input_01.tra", - STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/pctl_general_input_01.lab")); + storm::models::Mdp mdp = storm::parser::NondeterministicModelParserAsMdp( + STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general_input_01.tra", + STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/pctl_general_input_01.lab"); + storm::storage::SparseMatrix const& matrix = mdp.getTransitionMatrix(); - std::shared_ptr> mdp = mdpParser->getMdp(); - storm::storage::SparseMatrix const& matrix = mdp->getTransitionMatrix(); - - ASSERT_EQ(mdp->getNumberOfStates(), (uint_fast64_t)3); - ASSERT_EQ(mdp->getNumberOfTransitions(), (uint_fast64_t)11); + ASSERT_EQ(mdp.getNumberOfStates(), (uint_fast64_t)3); + ASSERT_EQ(mdp.getNumberOfTransitions(), (uint_fast64_t)11); ASSERT_EQ(matrix.getRowCount(), (uint_fast64_t)(2 * 3)); ASSERT_EQ(matrix.getColumnCount(), (uint_fast64_t)3); - - - delete mdpParser; } diff --git a/test/functional/parser/ParsePrismTest.cpp b/test/functional/parser/ParsePrismTest.cpp index a2f23844e..baead3ad3 100644 --- a/test/functional/parser/ParsePrismTest.cpp +++ b/test/functional/parser/ParsePrismTest.cpp @@ -8,9 +8,8 @@ #include "src/models/Mdp.h" TEST(ParsePrismTest, parseCrowds5_5) { - storm::parser::PrismParser parser; storm::ir::Program program; - ASSERT_NO_THROW(program = parser.parseFile("examples/dtmc/crowds/crowds5_5.pm")); + ASSERT_NO_THROW(program = storm::parser::PrismParserFromFile("examples/dtmc/crowds/crowds5_5.pm")); storm::adapters::ExplicitModelAdapter adapter(program); std::shared_ptr> model = adapter.getModel()->as>(); @@ -20,9 +19,8 @@ TEST(ParsePrismTest, parseCrowds5_5) { } TEST(ParsePrismTest, parseTwoDice) { - storm::parser::PrismParser parser; storm::ir::Program program; - ASSERT_NO_THROW(program = parser.parseFile("examples/mdp/two_dice/two_dice.nm")); + ASSERT_NO_THROW(program = storm::parser::PrismParserFromFile("examples/mdp/two_dice/two_dice.nm")); storm::adapters::ExplicitModelAdapter adapter(program); std::shared_ptr> model = adapter.getModel()->as>(); diff --git a/test/functional/parser/ReadLabFileTest.cpp b/test/functional/parser/ReadLabFileTest.cpp index 2c3122209..2e35ee1ae 100644 --- a/test/functional/parser/ReadLabFileTest.cpp +++ b/test/functional/parser/ReadLabFileTest.cpp @@ -15,77 +15,67 @@ #include TEST(ReadLabFileTest, NonExistingFileTest) { - //No matter what happens, please don't create a file with the name "nonExistingFile.not"! :-) + // No matter what happens, please do NOT create a file with the name "nonExistingFile.not"! ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(0,STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), storm::exceptions::FileIoException); } TEST(ReadLabFileTest, ParseTest) { - //This test is based on a test case from the original MRMC. + // This test is based on a test case from the original MRMC. - - storm::parser::AtomicPropositionLabelingParser* parser = nullptr; - //Parsing the file - ASSERT_NO_THROW(parser = new storm::parser::AtomicPropositionLabelingParser(12, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/pctl_general_input_01.lab")); - std::shared_ptr labeling(parser->getLabeling()); + // Parsing the file + storm::models::AtomicPropositionsLabeling labeling = storm::parser::AtomicPropositionLabelingParser(12, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/pctl_general_input_01.lab"); - //Checking whether all propositions are in the labelling + // Checking whether all propositions are in the labelling char phi[] = "phi", psi[] = "psi", smth[] = "smth"; - if (labeling != nullptr) { - ASSERT_TRUE(labeling->containsAtomicProposition(phi)); - ASSERT_TRUE(labeling->containsAtomicProposition(psi)); - ASSERT_TRUE(labeling->containsAtomicProposition(smth)); - - //Testing whether all and only the correct nodes are labeled with "phi" - ASSERT_TRUE(labeling->getStateHasAtomicProposition(phi,0)); - ASSERT_TRUE(labeling->getStateHasAtomicProposition(phi,1)); - ASSERT_TRUE(labeling->getStateHasAtomicProposition(phi,2)); - - ASSERT_FALSE(labeling->getStateHasAtomicProposition(phi,3)); - ASSERT_FALSE(labeling->getStateHasAtomicProposition(phi,4)); - ASSERT_FALSE(labeling->getStateHasAtomicProposition(phi,5)); - ASSERT_FALSE(labeling->getStateHasAtomicProposition(phi,6)); - ASSERT_FALSE(labeling->getStateHasAtomicProposition(phi,7)); - ASSERT_FALSE(labeling->getStateHasAtomicProposition(phi,8)); - ASSERT_FALSE(labeling->getStateHasAtomicProposition(phi,9)); - ASSERT_FALSE(labeling->getStateHasAtomicProposition(phi,10)); - ASSERT_FALSE(labeling->getStateHasAtomicProposition(phi,11)); - - //Testing whether all and only the correct nodes are labeled with "psi" - ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,0)); - ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,1)); - ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,2)); - ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,3)); - ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,4)); - ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,5)); - ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,6)); - ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,7)); - ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,8)); - ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,9)); - ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,10)); - ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,11)); - - //Testing whether all and only the correct nodes are labeled with "smth" - ASSERT_TRUE(labeling->getStateHasAtomicProposition(smth,2)); - - ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,0)); - ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,1)); - ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,3)); - ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,4)); - ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,5)); - ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,6)); - ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,7)); - ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,8)); - ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,9)); - ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,10)); - ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,11)); - - //Deleting the labeling - delete parser; - } else { - FAIL(); - } + ASSERT_TRUE(labeling.containsAtomicProposition(phi)); + ASSERT_TRUE(labeling.containsAtomicProposition(psi)); + ASSERT_TRUE(labeling.containsAtomicProposition(smth)); + + // Testing whether all and only the correct nodes are labeled with "phi" + ASSERT_TRUE(labeling.getStateHasAtomicProposition(phi,0)); + ASSERT_TRUE(labeling.getStateHasAtomicProposition(phi,1)); + ASSERT_TRUE(labeling.getStateHasAtomicProposition(phi,2)); + + ASSERT_FALSE(labeling.getStateHasAtomicProposition(phi,3)); + ASSERT_FALSE(labeling.getStateHasAtomicProposition(phi,4)); + ASSERT_FALSE(labeling.getStateHasAtomicProposition(phi,5)); + ASSERT_FALSE(labeling.getStateHasAtomicProposition(phi,6)); + ASSERT_FALSE(labeling.getStateHasAtomicProposition(phi,7)); + ASSERT_FALSE(labeling.getStateHasAtomicProposition(phi,8)); + ASSERT_FALSE(labeling.getStateHasAtomicProposition(phi,9)); + ASSERT_FALSE(labeling.getStateHasAtomicProposition(phi,10)); + ASSERT_FALSE(labeling.getStateHasAtomicProposition(phi,11)); + + //Testing whether all and only the correct nodes are labeled with "psi" + ASSERT_FALSE(labeling.getStateHasAtomicProposition(psi,0)); + ASSERT_FALSE(labeling.getStateHasAtomicProposition(psi,1)); + ASSERT_FALSE(labeling.getStateHasAtomicProposition(psi,2)); + ASSERT_FALSE(labeling.getStateHasAtomicProposition(psi,3)); + ASSERT_FALSE(labeling.getStateHasAtomicProposition(psi,4)); + ASSERT_FALSE(labeling.getStateHasAtomicProposition(psi,5)); + ASSERT_FALSE(labeling.getStateHasAtomicProposition(psi,6)); + ASSERT_FALSE(labeling.getStateHasAtomicProposition(psi,7)); + ASSERT_FALSE(labeling.getStateHasAtomicProposition(psi,8)); + ASSERT_FALSE(labeling.getStateHasAtomicProposition(psi,9)); + ASSERT_FALSE(labeling.getStateHasAtomicProposition(psi,10)); + ASSERT_FALSE(labeling.getStateHasAtomicProposition(psi,11)); + + //Testing whether all and only the correct nodes are labeled with "smth" + ASSERT_TRUE(labeling.getStateHasAtomicProposition(smth,2)); + + ASSERT_FALSE(labeling.getStateHasAtomicProposition(smth,0)); + ASSERT_FALSE(labeling.getStateHasAtomicProposition(smth,1)); + ASSERT_FALSE(labeling.getStateHasAtomicProposition(smth,3)); + ASSERT_FALSE(labeling.getStateHasAtomicProposition(smth,4)); + ASSERT_FALSE(labeling.getStateHasAtomicProposition(smth,5)); + ASSERT_FALSE(labeling.getStateHasAtomicProposition(smth,6)); + ASSERT_FALSE(labeling.getStateHasAtomicProposition(smth,7)); + ASSERT_FALSE(labeling.getStateHasAtomicProposition(smth,8)); + ASSERT_FALSE(labeling.getStateHasAtomicProposition(smth,9)); + ASSERT_FALSE(labeling.getStateHasAtomicProposition(smth,10)); + ASSERT_FALSE(labeling.getStateHasAtomicProposition(smth,11)); } TEST(ReadLabFileTest, WrongHeaderTest1) { diff --git a/test/functional/parser/ReadTraFileTest.cpp b/test/functional/parser/ReadTraFileTest.cpp index fd86a8820..e6ff86456 100644 --- a/test/functional/parser/ReadTraFileTest.cpp +++ b/test/functional/parser/ReadTraFileTest.cpp @@ -17,59 +17,51 @@ TEST(ReadTraFileTest, NonExistingFileTest) { ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), storm::exceptions::FileIoException); } -/* The following test case is based on one of the original STORM test cases +/* The following test case is based on one of the original MRMC test cases */ TEST(ReadTraFileTest, ParseFileTest1) { - storm::parser::DeterministicSparseTransitionParser* parser = nullptr; - ASSERT_NO_THROW(parser = new storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/csl_general_input_01.tra")); - std::shared_ptr> result = parser->getMatrix(); + storm::storage::SparseMatrix result = storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/csl_general_input_01.tra"); - if (result != nullptr) { - double val = 0; - ASSERT_TRUE(result->getValue(0, 0, &val)); - ASSERT_EQ(val, 0.0); + double val = 0.0; + ASSERT_TRUE(result.getValue(0, 0, &val)); + ASSERT_EQ(val, 0.0); - ASSERT_TRUE(result->getValue(0, 1, &val)); - ASSERT_EQ(val, 1.0); + ASSERT_TRUE(result.getValue(0, 1, &val)); + ASSERT_EQ(val, 1.0); - ASSERT_TRUE(result->getValue(1, 1, &val)); - ASSERT_EQ(val, 0.080645161290322580645161290322581); + ASSERT_TRUE(result.getValue(1, 1, &val)); + ASSERT_EQ(val, 0.080645161290322580645161290322581); - ASSERT_TRUE(result->getValue(1, 2, &val)); - ASSERT_EQ(val, 0.080645161290322580645161290322581); + ASSERT_TRUE(result.getValue(1, 2, &val)); + ASSERT_EQ(val, 0.080645161290322580645161290322581); - //Transition 1->3 was not set in the file, so it is not to appear in the matrix! - ASSERT_FALSE(result->getValue(1, 3, &val)); - ASSERT_EQ(val, 0); + //Transition 1->3 was not set in the file, so it is not to appear in the matrix! + ASSERT_FALSE(result.getValue(1, 3, &val)); + ASSERT_EQ(val, 0); - ASSERT_TRUE(result->getValue(2, 1, &val)); - ASSERT_EQ(val, 0.04032258064516129032258064516129); + ASSERT_TRUE(result.getValue(2, 1, &val)); + ASSERT_EQ(val, 0.04032258064516129032258064516129); - ASSERT_TRUE(result->getValue(2, 2, &val)); - ASSERT_EQ(val, 0.04032258064516129032258064516129); + ASSERT_TRUE(result.getValue(2, 2, &val)); + ASSERT_EQ(val, 0.04032258064516129032258064516129); - ASSERT_TRUE(result->getValue(2, 3, &val)); - ASSERT_EQ(val, 0.04032258064516129032258064516129); + ASSERT_TRUE(result.getValue(2, 3, &val)); + ASSERT_EQ(val, 0.04032258064516129032258064516129); - ASSERT_TRUE(result->getValue(2, 4, &val)); - ASSERT_EQ(val, 0.04032258064516129032258064516129); + ASSERT_TRUE(result.getValue(2, 4, &val)); + ASSERT_EQ(val, 0.04032258064516129032258064516129); - ASSERT_TRUE(result->getValue(3, 2, &val)); - ASSERT_EQ(val, 0.0806451612903225806451612903225812); + ASSERT_TRUE(result.getValue(3, 2, &val)); + ASSERT_EQ(val, 0.0806451612903225806451612903225812); - ASSERT_TRUE(result->getValue(3, 3, &val)); - ASSERT_EQ(val, 0.0); + ASSERT_TRUE(result.getValue(3, 3, &val)); + ASSERT_EQ(val, 0.0); - ASSERT_TRUE(result->getValue(3, 4, &val)); - ASSERT_EQ(val, 0.080645161290322580645161290322581); + ASSERT_TRUE(result.getValue(3, 4, &val)); + ASSERT_EQ(val, 0.080645161290322580645161290322581); - ASSERT_TRUE(result->getValue(4, 4, &val)); - ASSERT_EQ(val, 0.0); - - delete parser; - } else { - FAIL(); - } + ASSERT_TRUE(result.getValue(4, 4, &val)); + ASSERT_EQ(val, 0.0); } TEST(ReadTraFileTest, WrongFormatTestHeader1) {