diff --git a/src/formula/Csl/AbstractCslFormula.h b/src/formula/Csl/AbstractCslFormula.h index 111ba9f39..0770c1cd7 100644 --- a/src/formula/Csl/AbstractCslFormula.h +++ b/src/formula/Csl/AbstractCslFormula.h @@ -2,7 +2,7 @@ * AbstractCslFormula.h * * Created on: 19.04.2013 - * Author: thomas + * Author: Thomas Heinemann */ #ifndef ABSTRACTCSLFORMULA_H_ @@ -25,6 +25,13 @@ public: } }; +/*! + * @brief An encapsulation type for the Return Type of the CslParser. As a pure virtual Class can not be an r-value return type, it has to be encapsulated. + * @see CslParser + */ +template +using AbstractCslFormularRef_t = std::reference_wrapper>; + } /* namespace csl */ } /* namespace property */ } /* namespace storm */ diff --git a/src/formula/Ltl/AbstractLtlFormula.h b/src/formula/Ltl/AbstractLtlFormula.h index 8286f75db..1d275a464 100644 --- a/src/formula/Ltl/AbstractLtlFormula.h +++ b/src/formula/Ltl/AbstractLtlFormula.h @@ -82,6 +82,9 @@ public: virtual void visit(visitor::AbstractLtlFormulaVisitor& visitor) const = 0; }; +template +using AbstractLtlFormularSharedPtr_t = std::shared_ptr; + } /* namespace ltl */ } /* namespace property */ } /* namespace storm */ diff --git a/src/parser/AtomicPropositionLabelingParser.cpp b/src/parser/AtomicPropositionLabelingParser.cpp index 4936b4adb..e2c590b5b 100644 --- a/src/parser/AtomicPropositionLabelingParser.cpp +++ b/src/parser/AtomicPropositionLabelingParser.cpp @@ -40,12 +40,15 @@ namespace parser { * @param filename input .lab file's name. * @return The pointer to the created labeling object. */ -AtomicPropositionLabelingParser::AtomicPropositionLabelingParser(uint_fast64_t node_count, - std::string const & filename) - : labeling(nullptr) { +storm::models::AtomicPropositionsLabeling AtomicPropositionLabelingParser(uint_fast64_t node_count, std::string const & filename) { /* * Open file. */ + if (!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; @@ -96,7 +99,7 @@ AtomicPropositionLabelingParser::AtomicPropositionLabelingParser(uint_fast64_t n /* * create labeling object with given node and proposition count */ - this->labeling = std::shared_ptr(new storm::models::AtomicPropositionsLabeling(node_count, proposition_count)); + storm::models::AtomicPropositionsLabeling labeling(node_count, proposition_count); /* * second run: add propositions and node labels to labeling @@ -130,7 +133,7 @@ AtomicPropositionLabelingParser::AtomicPropositionLabelingParser(uint_fast64_t n if (strncmp(buf, "#END", cnt) == 0) break; strncpy(proposition, buf, cnt); proposition[cnt] = '\0'; - this->labeling->addAtomicProposition(proposition); + labeling.addAtomicProposition(proposition); } else { cnt = 1; // next char is separator, one step forward } @@ -173,13 +176,14 @@ AtomicPropositionLabelingParser::AtomicPropositionLabelingParser(uint_fast64_t n */ strncpy(proposition, buf, cnt); proposition[cnt] = '\0'; - this->labeling->addAtomicPropositionToState(proposition, node); + labeling.addAtomicPropositionToState(proposition, node); buf += cnt; } } buf = trimWhitespaces(buf); } } + return labeling; } } // namespace parser diff --git a/src/parser/AtomicPropositionLabelingParser.h b/src/parser/AtomicPropositionLabelingParser.h index 8ca0413f8..26d370792 100644 --- a/src/parser/AtomicPropositionLabelingParser.h +++ b/src/parser/AtomicPropositionLabelingParser.h @@ -14,20 +14,8 @@ namespace parser { /*! * @brief Load label file and return initialized AtomicPropositionsLabeling object. * - * Note that this class creates a new AtomicPropositionsLabeling object that can - * be accessed via getLabeling(). However, it will not delete this object! */ -class AtomicPropositionLabelingParser : Parser { - public: - AtomicPropositionLabelingParser(uint_fast64_t node_count, std::string const &filename); - - std::shared_ptr getLabeling() { - return this->labeling; - } - - private: - std::shared_ptr labeling; -}; +storm::models::AtomicPropositionsLabeling AtomicPropositionLabelingParser(uint_fast64_t node_count, std::string const &filename); } // namespace parser } // namespace storm diff --git a/src/parser/CslParser.cpp b/src/parser/CslParser.cpp index 8c0457310..3b267ddc3 100644 --- a/src/parser/CslParser.cpp +++ b/src/parser/CslParser.cpp @@ -38,7 +38,7 @@ namespace storm { namespace parser { template -struct CslParser::CslGrammar : qi::grammar*(), Skipper > { +struct CslGrammar : qi::grammar*(), Skipper > { CslGrammar() : CslGrammar::base_type(start) { //This block contains helper rules that may be used several times freeIdentifierName = qi::lexeme[qi::alpha >> *(qi::alnum | qi::char_('_'))]; @@ -166,7 +166,7 @@ struct CslParser::CslGrammar : qi::grammar CslParser(std::string formulaString) { // Prepare iterators to input. BaseIteratorType stringIteratorBegin = formulaString.begin(); BaseIteratorType stringIteratorEnd = formulaString.end(); diff --git a/src/parser/CslParser.h b/src/parser/CslParser.h index 9ae6d2cf3..d0f913709 100644 --- a/src/parser/CslParser.h +++ b/src/parser/CslParser.h @@ -11,23 +11,31 @@ #include "Parser.h" #include "src/formula/Csl.h" -//#include +#include namespace storm { namespace parser { +/*! + * Reads a CSL formula from its string representation and parses it into a formula tree, consisting of + * classes in the namespace storm::property. + * + * If the string could not be parsed successfully, it will throw a wrongFormatException. + * + * @param formulaString The string representation of the formula + * @throw wrongFormatException If the input could not be parsed successfully + */ +storm::property::csl::AbstractCslFormularRef_t CslParser(std::string formulaString); + +/*! + * Struct for the CSL grammar, that Boost::Spirit uses to parse the formulas. + */ +template +struct CslGrammar; + class CslParser: public storm::parser::Parser { public: - /*! - * Reads a CSL formula from its string representation and parses it into a formula tree, consisting of - * classes in the namespace storm::property. - * - * If the string could not be parsed successfully, it will throw a wrongFormatException. - * - * @param formulaString The string representation of the formula - * @throw wrongFormatException If the input could not be parsed successfully - */ - CslParser(std::string formulaString); + virtual ~CslParser(); /*! @@ -41,11 +49,7 @@ private: private: storm::property::csl::AbstractCslFormula* formula; - /*! - * Struct for the CSL grammar, that Boost::Spirit uses to parse the formulas. - */ - template - struct CslGrammar; + }; } /* namespace parser */ diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index d28e1c0d3..2d2a5a55f 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -44,7 +44,7 @@ namespace parser { * @param buf Data to scan. Is expected to be some char array. * @param maxnode Is set to highest id of all nodes. */ -uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation) { +uint_fast64_t firstPass(char* buf, uint_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation) { bool isRewardMatrix = rewardMatrixInformation != nullptr; uint_fast64_t nonZeroEntryCount = 0; @@ -129,8 +129,7 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, uint_fas * @return a pointer to the created sparse matrix. */ -DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing, RewardMatrixInformationStruct* rewardMatrixInformation) - : matrix(nullptr) { +storm::storage::SparseMatrix DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing, RewardMatrixInformationStruct* rewardMatrixInformation) { /* * Enforce locale where decimal point is '.'. */ @@ -138,6 +137,11 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st bool isRewardMatrix = rewardMatrixInformation != nullptr; + if (!fileExistsAndIsReadable(filename.c_str())) { + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable."); + throw storm::exceptions::WrongFormatException(); + } + /* * Open file. */ @@ -148,7 +152,7 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st * Perform first pass, i.e. count entries that are not zero. */ uint_fast64_t maxStateId; - uint_fast64_t nonZeroEntryCount = this->firstPass(file.data, maxStateId, rewardMatrixInformation); + uint_fast64_t nonZeroEntryCount = firstPass(file.data, maxStateId, rewardMatrixInformation); LOG4CPLUS_INFO(logger, "First pass on " << filename << " shows " << nonZeroEntryCount << " NonZeros."); @@ -189,12 +193,12 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st * The number of non-zero elements is computed by firstPass(). */ LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << (maxStateId+1) << " x " << (maxStateId+1) << "."); - this->matrix = std::shared_ptr>(new storm::storage::SparseMatrix(maxStateId + 1)); - if (this->matrix == nullptr) { + storm::storage::SparseMatrix resultMatrix(maxStateId + 1); + resultMatrix.initialize(nonZeroEntryCount); + if (!resultMatrix.isInitialized()) { LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << (maxStateId+1) << " x " << (maxStateId+1) << "."); throw std::bad_alloc(); } - this->matrix->initialize(nonZeroEntryCount); int_fast64_t row, lastRow = -1, col; double val; @@ -218,7 +222,7 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st if (lastRow != row) { if ((lastRow != -1) && (!rowHadDiagonalEntry)) { if (insertDiagonalEntriesIfMissing && !isRewardMatrix) { - this->matrix->addNextValue(lastRow, lastRow, storm::utility::constGetZero()); + resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constGetZero()); LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (1)"); } else if (!isRewardMatrix) { LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself."); @@ -229,7 +233,7 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st for (int_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) { hadDeadlocks = true; if (fixDeadlocks && !isRewardMatrix) { - this->matrix->addNextValue(skippedRow, skippedRow, storm::utility::constGetOne()); + resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::constGetOne()); rowHadDiagonalEntry = true; LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions. A self-loop was inserted."); } else if (!isRewardMatrix) { @@ -246,20 +250,20 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st } else if (col > row && !rowHadDiagonalEntry) { rowHadDiagonalEntry = true; if (insertDiagonalEntriesIfMissing && !isRewardMatrix) { - this->matrix->addNextValue(row, row, storm::utility::constGetZero()); + resultMatrix.addNextValue(row, row, storm::utility::constGetZero()); LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << row << " has no transition to itself. Inserted a 0-transition. (2)"); } else if (!isRewardMatrix) { LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << row << " has no transition to itself."); } } - this->matrix->addNextValue(row, col, val); + resultMatrix.addNextValue(row, col, val); buf = trimWhitespaces(buf); } if (!rowHadDiagonalEntry) { if (insertDiagonalEntriesIfMissing && !isRewardMatrix) { - this->matrix->addNextValue(lastRow, lastRow, storm::utility::constGetZero()); + resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constGetZero()); LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (3)"); } else if (!isRewardMatrix) { LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself."); @@ -271,7 +275,9 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st /* * Finalize Matrix. */ - this->matrix->finalize(); + resultMatrix.finalize(); + + return resultMatrix; } } // namespace parser diff --git a/src/parser/DeterministicSparseTransitionParser.h b/src/parser/DeterministicSparseTransitionParser.h index d4029ad29..7ea82b410 100644 --- a/src/parser/DeterministicSparseTransitionParser.h +++ b/src/parser/DeterministicSparseTransitionParser.h @@ -15,20 +15,7 @@ namespace parser { * @brief Load a deterministic transition system from file and create a * sparse adjacency matrix whose entries represent the weights of the edges */ -class DeterministicSparseTransitionParser : public Parser { - public: - DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing = true, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr); - - std::shared_ptr> getMatrix() { - return this->matrix; - } - - private: - std::shared_ptr> matrix; - - uint_fast64_t firstPass(char* buf, uint_fast64_t &maxnode, RewardMatrixInformationStruct* rewardMatrixInformation); - -}; +storm::storage::SparseMatrix DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing = true, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr); } // namespace parser } // namespace storm diff --git a/src/parser/LtlParser.cpp b/src/parser/LtlParser.cpp index 3d53e5368..da90ad04f 100644 --- a/src/parser/LtlParser.cpp +++ b/src/parser/LtlParser.cpp @@ -41,7 +41,7 @@ namespace storm { namespace parser { template -struct LtlParser::LtlGrammar : qi::grammar*(), Skipper > { +struct LtlGrammar : qi::grammar*(), Skipper > { LtlGrammar() : LtlGrammar::base_type(start) { //This block contains helper rules that may be used several times freeIdentifierName = qi::lexeme[qi::alpha >> *(qi::alnum | qi::char_('_'))]; @@ -128,7 +128,7 @@ struct LtlParser::LtlGrammar : qi::grammar storm::parser::LtlParser(std::string formulaString) { // Prepare iterators to input. BaseIteratorType stringIteratorBegin = formulaString.begin(); BaseIteratorType stringIteratorEnd = formulaString.end(); @@ -178,6 +178,6 @@ storm::parser::LtlParser::LtlParser(std::string formulaString) { throw storm::exceptions::WrongFormatException() << "Syntax error in formula"; } - formula = result_pointer; + return storm::property::ltl::AbstractLtlFormularSharedPtr_t(result_pointer); } diff --git a/src/parser/LtlParser.h b/src/parser/LtlParser.h index e2240ef08..bf173d44f 100644 --- a/src/parser/LtlParser.h +++ b/src/parser/LtlParser.h @@ -14,46 +14,22 @@ namespace storm { namespace parser { -class LtlParser: public storm::parser::Parser { -public: -public: - /*! - * Reads a LTL formula from its string representation and parses it into a formula tree, consisting of - * classes in the namespace storm::property. - * - * If the string could not be parsed successfully, it will throw a wrongFormatException. - * - * @param formulaString The string representation of the formula - * @throw wrongFormatException If the input could not be parsed successfully - */ - LtlParser(std::string formulaString); - - /*! - * @return a pointer to the parsed formula object - */ - storm::property::ltl::AbstractLtlFormula* getFormula() { - return this->formula; - } - - /*! - * Destructor - * - * Does not delete the parsed formula! - */ - virtual ~LtlParser() { - // Intentionally left empty - // The formula is not deleted with the parser. - } - -private: - storm::property::ltl::AbstractLtlFormula* formula; - - /*! - * Struct for the Ltl grammar, that Boost::Spirit uses to parse the formulas. - */ - template - struct LtlGrammar; -}; +/*! + * Reads a LTL formula from its string representation and parses it into a formula tree, consisting of + * classes in the namespace storm::property. + * + * If the string could not be parsed successfully, it will throw a wrongFormatException. + * + * @param formulaString The string representation of the formula + * @throw wrongFormatException If the input could not be parsed successfully + */ +storm::property::ltl::AbstractLtlFormularSharedPtr_t LtlParser(std::string formulaString); + +/*! + * Struct for the Ltl grammar, that Boost::Spirit uses to parse the formulas. + */ +template +struct LtlGrammar; } /* namespace parser */ } /* namespace storm */ diff --git a/src/parser/NondeterministicModelParser.cpp b/src/parser/NondeterministicModelParser.cpp index 3408da9bf..69ab188f1 100644 --- a/src/parser/NondeterministicModelParser.cpp +++ b/src/parser/NondeterministicModelParser.cpp @@ -29,23 +29,21 @@ namespace parser { */ NondeterministicModelParser::NondeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { - storm::parser::NondeterministicSparseTransitionParser tp(transitionSystemFile); - uint_fast64_t stateCount = tp.getMatrix()->getColumnCount(); + NondeterministicSparseTransitionParserResult_t nondeterministicSparseTransitionParserResult = storm::parser::NondeterministicSparseTransitionParser(transitionSystemFile); + uint_fast64_t stateCount = nondeterministicSparseTransitionParserResult.first.getColumnCount(); - storm::parser::AtomicPropositionLabelingParser lp(stateCount, labelingFile); if (stateRewardFile != "") { - storm::parser::SparseStateRewardParser srp(stateCount, stateRewardFile); - this->stateRewards = srp.getStateRewards(); + std::vector stateRewards = storm::parser::SparseStateRewardParser(stateCount, stateRewardFile); } if (transitionRewardFile != "") { - RewardMatrixInformationStruct* rewardMatrixInfo = new RewardMatrixInformationStruct(tp.getMatrix()->getRowCount(), tp.getMatrix()->getColumnCount(), tp.getRowMapping()); + RewardMatrixInformationStruct* rewardMatrixInfo = new RewardMatrixInformationStruct(nondeterministicSparseTransitionParserResult.first.getRowCount(), nondeterministicSparseTransitionParserResult.first.getColumnCount(), nondeterministicSparseTransitionParserResult.second); storm::parser::NondeterministicSparseTransitionParser trp(transitionRewardFile, rewardMatrixInfo); delete rewardMatrixInfo; this->transitionRewardMatrix = trp.getMatrix(); } this->probabilityMatrix = tp.getMatrix(); - this->stateLabeling = lp.getLabeling(); + this->stateLabeling = std::shared_ptr(storm::parser::AtomicPropositionLabelingParser(stateCount, labelingFile)); this->rowMapping = tp.getRowMapping(); this->mdp = nullptr; diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp index 7899c3df8..5d40e0cca 100644 --- a/src/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/parser/NondeterministicSparseTransitionParser.cpp @@ -49,7 +49,7 @@ namespace parser { * @param maxnode Is set to highest id of all nodes. * @return The number of non-zero elements. */ -uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation) { +uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation) { bool isRewardFile = rewardMatrixInformation != nullptr; /* @@ -177,13 +177,17 @@ uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_ * @return a pointer to the created sparse matrix. */ -NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(std::string const &filename, RewardMatrixInformationStruct* rewardMatrixInformation) - : matrix(nullptr) { +NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionParser(std::string const &filename, RewardMatrixInformationStruct* rewardMatrixInformation) { /* * Enforce locale where decimal point is '.'. */ setlocale(LC_NUMERIC, "C"); + if (!fileExistsAndIsReadable(filename.c_str())) { + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable."); + throw storm::exceptions::WrongFormatException(); + } + bool isRewardFile = rewardMatrixInformation != nullptr; /* @@ -197,7 +201,7 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s */ int_fast64_t maxnode; uint_fast64_t choices; - uint_fast64_t nonzero = this->firstPass(file.data, choices, maxnode, rewardMatrixInformation); + uint_fast64_t nonzero = firstPass(file.data, choices, maxnode, rewardMatrixInformation); /* * If first pass returned zero, the file format was wrong. @@ -238,17 +242,18 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s * Those two values, as well as the number of nonzero elements, was been calculated in the first run. */ LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << choices << " x " << (maxnode+1) << " with " << nonzero << " entries."); - this->matrix = std::shared_ptr>(new storm::storage::SparseMatrix(choices, maxnode + 1)); - if (this->matrix == nullptr) { + storm::storage::SparseMatrix matrix(choices, maxnode + 1); + matrix.initialize(nonzero); + if (!matrix.isInitialized()) { LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << choices << " x " << (maxnode+1) << "."); throw std::bad_alloc(); } - this->matrix->initialize(nonzero); + /* * Create row mapping. */ - this->rowMapping = std::shared_ptr>(new std::vector(maxnode+2,0)); + std::vector rowMapping(maxnode + 2, 0); /* * Parse file content. @@ -303,8 +308,8 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s for (int_fast64_t node = lastsource + 1; node < source; node++) { hadDeadlocks = true; if (fixDeadlocks) { - this->rowMapping->at(node) = curRow; - this->matrix->addNextValue(curRow, node, 1); + rowMapping.at(node) = curRow; + matrix.addNextValue(curRow, node, 1); ++curRow; LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted."); } else { @@ -315,14 +320,14 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s /* * Add this source to rowMapping, if this is the first choice we encounter for this state. */ - this->rowMapping->at(source) = curRow; + rowMapping.at(source) = curRow; } } // Read target and value and write it to the matrix. target = checked_strtol(buf, &buf); val = checked_strtod(buf, &buf); - this->matrix->addNextValue(curRow, target, val); + matrix.addNextValue(curRow, target, val); lastsource = source; lastchoice = choice; @@ -338,7 +343,7 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s } for (int_fast64_t node = lastsource + 1; node <= maxnode + 1; node++) { - this->rowMapping->at(node) = curRow + 1; + rowMapping.at(node) = curRow + 1; } if (!fixDeadlocks && hadDeadlocks && !isRewardFile) throw storm::exceptions::WrongFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly."; @@ -346,7 +351,9 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s /* * Finalize matrix. */ - this->matrix->finalize(); + matrix.finalize(); + + return std::make_pair(matrix, rowMapping); } } // namespace parser diff --git a/src/parser/NondeterministicSparseTransitionParser.h b/src/parser/NondeterministicSparseTransitionParser.h index a696b568f..900bc088e 100644 --- a/src/parser/NondeterministicSparseTransitionParser.h +++ b/src/parser/NondeterministicSparseTransitionParser.h @@ -13,29 +13,16 @@ namespace storm { namespace parser { +/*! + * @brief Contains the Result of a call to the NondeterministicSparseTransitionParser function. The first part is the resulting matrix. The second part is the row mapping. + */ +typedef std::pair, std::vector> NondeterministicSparseTransitionParserResult_t; + /*! * @brief Load a nondeterministic transition system from file and create a * sparse adjacency matrix whose entries represent the weights of the edges */ -class NondeterministicSparseTransitionParser : public Parser { - public: - NondeterministicSparseTransitionParser(std::string const &filename, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr); - - inline std::shared_ptr> getMatrix() const { - return this->matrix; - } - - inline std::shared_ptr> getRowMapping() const { - return this->rowMapping; - } - - private: - std::shared_ptr> matrix; - std::shared_ptr> rowMapping; - - uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation); - -}; +NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionParser(std::string const &filename, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr); } // namespace parser } // namespace storm diff --git a/src/parser/Parser.cpp b/src/parser/Parser.cpp index a58796982..6a266e51d 100644 --- a/src/parser/Parser.cpp +++ b/src/parser/Parser.cpp @@ -20,7 +20,7 @@ extern log4cplus::Logger logger; * @param end New pointer will be written there * @return Result of strtol() */ -uint_fast64_t storm::parser::Parser::checked_strtol(const char* str, char** end) { +uint_fast64_t storm::parser::checked_strtol(const char* str, char** end) { uint_fast64_t res = strtol(str, end, 10); if (str == *end) { LOG4CPLUS_ERROR(logger, "Error while parsing integer. Next input token is not a number."); @@ -38,7 +38,7 @@ uint_fast64_t storm::parser::Parser::checked_strtol(const char* str, char** end) * @param end New pointer will be written there * @return Result of strtod() */ -double storm::parser::Parser::checked_strtod(const char* str, char** end) { +double storm::parser::checked_strtod(const char* str, char** end) { double res = strtod(str, end); if (str == *end) { LOG4CPLUS_ERROR(logger, "Error while parsing floating point. Next input token is not a number."); @@ -54,7 +54,7 @@ double storm::parser::Parser::checked_strtod(const char* str, char** end) { * @param buf String buffer * @return pointer to first non-whitespace character */ -char* storm::parser::Parser::trimWhitespaces(char* buf) { +char* storm::parser::trimWhitespaces(char* buf) { while ((*buf == ' ') || (*buf == '\t') || (*buf == '\n') || (*buf == '\r')) buf++; return buf; } diff --git a/src/parser/Parser.h b/src/parser/Parser.h index 5ea30d743..8df1691b9 100644 --- a/src/parser/Parser.h +++ b/src/parser/Parser.h @@ -14,6 +14,7 @@ #include #include #include +#include #include #include @@ -47,6 +48,15 @@ namespace parser { std::shared_ptr> 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. @@ -114,22 +124,24 @@ namespace parser { }; class Parser { - protected: - /*! - * @brief Parses integer and checks, if something has been parsed. - */ - uint_fast64_t checked_strtol(const char* str, char** end); + //protected: + + }; - /*! - * @brief Parses floating point and checks, if something has been parsed. - */ - double checked_strtod(const char* str, char** end); + /*! + * @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. + */ + double checked_strtod(const char* str, char** end); - /*! - * @brief Skips common whitespaces in a string. - */ - char* trimWhitespaces(char* buf); - }; + /*! + * @brief Skips common whitespaces in a string. + */ + char* trimWhitespaces(char* buf); } // namespace parser } // namespace storm diff --git a/src/parser/SparseStateRewardParser.cpp b/src/parser/SparseStateRewardParser.cpp index abd3df7b5..1f34ec7d5 100644 --- a/src/parser/SparseStateRewardParser.cpp +++ b/src/parser/SparseStateRewardParser.cpp @@ -36,16 +36,20 @@ namespace parser { * * @param stateCount The number of states. * @param filename The filename of the state reward file. - * @return A pointer to the created state reward vector. + * @return The created state reward vector. */ -SparseStateRewardParser::SparseStateRewardParser(uint_fast64_t stateCount, std::string const & filename) - : stateRewards(nullptr) { +std::vector SparseStateRewardParser(uint_fast64_t stateCount, std::string const & filename) { // Open file. + if (!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. - this->stateRewards = std::shared_ptr>(new std::vector(stateCount)); + std::vector stateRewards(stateCount); { // Now parse state reward assignments. @@ -62,7 +66,7 @@ SparseStateRewardParser::SparseStateRewardParser(uint_fast64_t stateCount, std:: throw storm::exceptions::WrongFormatException() << "State reward file specifies illegal reward value."; } - (*this->stateRewards)[state] = reward; + stateRewards[state] = reward; buf = trimWhitespaces(buf); } diff --git a/src/parser/SparseStateRewardParser.h b/src/parser/SparseStateRewardParser.h index a6b3e1203..668b76dcc 100644 --- a/src/parser/SparseStateRewardParser.h +++ b/src/parser/SparseStateRewardParser.h @@ -13,17 +13,7 @@ namespace parser { /*! * @brief Load state reward file and return vector of state rewards. */ -class SparseStateRewardParser : Parser { - public: - SparseStateRewardParser(uint_fast64_t stateCount, std::string const &filename); - - std::shared_ptr> getStateRewards() { - return this->stateRewards; - } - - private: - std::shared_ptr> stateRewards; -}; +std::vector SparseStateRewardParser(uint_fast64_t stateCount, std::string const &filename); } // namespace parser