From f4050e5b1891206e2981bc01ca15050c1451c23c Mon Sep 17 00:00:00 2001 From: PBerger Date: Wed, 5 Jun 2013 17:11:58 +0200 Subject: [PATCH] Edited Parsers, re factored interface into a single function without an encapsulating class. Warning, this is work in Progress and not yet compiling. --- src/exceptions/InvalidStateException.h | 2 +- src/models/AbstractDeterministicModel.h | 13 ++++++ src/models/AbstractModel.h | 27 +++++++++++ src/models/Ctmc.h | 13 ++++++ src/models/Dtmc.h | 25 +++++++++++ src/parser/CslParser.cpp | 9 +--- src/parser/CslParser.h | 21 +-------- src/parser/DeterministicModelParser.cpp | 51 ++++++++++++++------- src/parser/DeterministicModelParser.h | 59 +++++++++++-------------- src/parser/LtlParser.cpp | 4 +- src/parser/LtlParser.h | 2 +- src/parser/PrismParser.cpp | 4 +- src/parser/PrismParser.h | 37 +++++++++------- 13 files changed, 168 insertions(+), 99 deletions(-) diff --git a/src/exceptions/InvalidStateException.h b/src/exceptions/InvalidStateException.h index 13ae5dca2..0489e08ca 100644 --- a/src/exceptions/InvalidStateException.h +++ b/src/exceptions/InvalidStateException.h @@ -8,7 +8,7 @@ namespace storm { namespace exceptions { /*! - * @brief This exception is thrown when a memory request can't be + * @brief This exception is thrown when a memory request can not be * fulfilled. */ STORM_EXCEPTION_DEFINE_NEW(InvalidStateException) diff --git a/src/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h index c09f42f90..921f6cbfb 100644 --- a/src/models/AbstractDeterministicModel.h +++ b/src/models/AbstractDeterministicModel.h @@ -32,6 +32,19 @@ class AbstractDeterministicModel: public AbstractModel { : AbstractModel(transitionMatrix, stateLabeling, stateRewardVector, transitionRewardMatrix) { } + /*! Constructs an abstract 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 stateRewardVector The reward values associated with the states. + * @param transitionRewardMatrix The reward values associated with the transitions of the model. + */ + AbstractDeterministicModel(storm::storage::SparseMatrix const& transitionMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, + boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix) + : AbstractModel(transitionMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix) { + } + /*! * Destructor. */ diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index 31c019e66..1ac928fa7 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -8,6 +8,8 @@ #include #include +#include + namespace storm { namespace models { @@ -48,6 +50,31 @@ class AbstractModel: public std::enable_shared_from_this> { // Intentionally left empty. } + /*! Constructs an abstract model from the given transition matrix and + * the given labeling of the states. Creates copies of all given references. + * @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 stateRewardVector The reward values associated with the states. + * @param transitionRewardMatrix The reward values associated with the transitions of the model. + */ + AbstractModel(storm::storage::SparseMatrix const& transitionMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, + boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix) { + this->transitionMatrix.reset(new storm::storage::SparseMatrix(transitionMatrix)); + this->stateLabeling.reset(new storm::models::AtomicPropositionsLabeling(stateLabeling)); + + this->stateRewardVector = nullptr; + this->transitionRewardMatrix = nullptr; + + if (optionalStateRewardVector) { // Boost::Optional + this->stateRewardVector.reset(new std::vector(optionalStateRewardVector.get())); + } + + if (optionalTransitionRewardMatrix) { // Boost::Optional + this->stateRewardVector.reset(new storm::storage::SparseMatrix(optionalTransitionRewardMatrix.get())); + } + } + /*! * Destructor. */ diff --git a/src/models/Ctmc.h b/src/models/Ctmc.h index 0b8eff5fd..9a51d8732 100644 --- a/src/models/Ctmc.h +++ b/src/models/Ctmc.h @@ -43,6 +43,19 @@ public: : AbstractDeterministicModel(rateMatrix, stateLabeling, stateRewardVector, transitionRewardMatrix) { } + /*! + * Constructs a CTMC object from the given transition rate matrix and + * the given labeling of the states. + * @param rateMatrix The transition rate function of the + * CTMC given by a matrix. + * @param stateLabeling The labeling that assigns a set of atomic + * propositions to each state. + */ + Ctmc(storm::storage::SparseMatrix const& rateMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, + boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix) + : AbstractDeterministicModel(rateMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix) { + } + //! Copy Constructor /*! * Copy Constructor. Performs a deep copy of the given CTMC. diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 97399115d..011c148d4 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -57,6 +57,31 @@ public: } } + /*! + * Constructs a DTMC object from the given transition probability matrix and + * the given labeling of the states. + * All values are copied. + * @param probabilityMatrix The matrix representing the transitions in the model. + * @param stateLabeling The labeling that assigns a set of atomic + * propositions to each state. + * @param stateRewardVector The reward values associated with the states. + * @param transitionRewardMatrix The reward values associated with the transitions of the model. + */ + Dtmc(storm::storage::SparseMatrix const& probabilityMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, + boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix) + : AbstractDeterministicModel(probabilityMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix) { + if (!this->checkValidityOfProbabilityMatrix()) { + 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())) { + 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."; + } + } + } + //! Copy Constructor /*! * Copy Constructor. Performs a deep copy of the given DTMC. diff --git a/src/parser/CslParser.cpp b/src/parser/CslParser.cpp index 3b267ddc3..f66c82926 100644 --- a/src/parser/CslParser.cpp +++ b/src/parser/CslParser.cpp @@ -166,7 +166,7 @@ struct CslGrammar : qi::grammar CslParser(std::string formulaString) { +storm::property::csl::AbstractCslFormula* CslParser(std::string formulaString) { // Prepare iterators to input. BaseIteratorType stringIteratorBegin = formulaString.begin(); BaseIteratorType stringIteratorEnd = formulaString.end(); @@ -216,12 +216,7 @@ storm::property::csl::AbstractCslFormularRef_t CslParser(std::string for throw storm::exceptions::WrongFormatException() << "Syntax error in formula"; } - formula = result_pointer; -} - -CslParser::~CslParser() { - // Intentionally left empty - // Parsed formula is not deleted with the parser! + return result_pointer; } } /* namespace parser */ diff --git a/src/parser/CslParser.h b/src/parser/CslParser.h index d0f913709..8dd4315d3 100644 --- a/src/parser/CslParser.h +++ b/src/parser/CslParser.h @@ -25,7 +25,7 @@ namespace parser { * @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); +storm::property::csl::AbstractCslFormula* CslParser(std::string formulaString); /*! * Struct for the CSL grammar, that Boost::Spirit uses to parse the formulas. @@ -33,25 +33,6 @@ storm::property::csl::AbstractCslFormularRef_t CslParser(std::string for template struct CslGrammar; -class CslParser: public storm::parser::Parser { -public: - - virtual ~CslParser(); - - /*! - * @return a pointer to the parsed formula object - */ - storm::property::csl::AbstractCslFormula* getFormula() { - return this->formula; - } - -private: -private: - storm::property::csl::AbstractCslFormula* formula; - - -}; - } /* namespace parser */ } /* namespace storm */ #endif /* STORM_PARSER_CSLPARSER_H_ */ diff --git a/src/parser/DeterministicModelParser.cpp b/src/parser/DeterministicModelParser.cpp index 5e39170ec..8014fa67e 100644 --- a/src/parser/DeterministicModelParser.cpp +++ b/src/parser/DeterministicModelParser.cpp @@ -18,8 +18,7 @@ namespace storm { namespace parser { /*! - * Parses a transition file and a labeling file and produces a DTMC out of them; a pointer to the dtmc - * is saved in the field "dtmc" + * 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) @@ -27,31 +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) */ -DeterministicModelParser::DeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile, - std::string const & stateRewardFile, std::string const & transitionRewardFile) { - storm::parser::DeterministicSparseTransitionParser tp(transitionSystemFile); - this->transitionSystem = tp.getMatrix(); +DeterministicModelParserResultContainer parseDeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile, + std::string const & stateRewardFile, std::string const & transitionRewardFile) { - uint_fast64_t stateCount = this->transitionSystem->getRowCount(); + storm::storage::SparseMatrix resultTransitionSystem = storm::parser::DeterministicSparseTransitionParser(transitionSystemFile); - storm::parser::AtomicPropositionLabelingParser lp(stateCount, labelingFile); - this->labeling = lp.getLabeling(); + uint_fast64_t stateCount = resultTransitionSystem.getRowCount(); - this->stateRewards = nullptr; - this->transitionRewards = nullptr; + storm::models::AtomicPropositionsLabeling resultLabeling = storm::parser::AtomicPropositionLabelingParser(stateCount, labelingFile); + + DeterministicModelParserResultContainer result(resultTransitionSystem, resultLabeling); if (stateRewardFile != "") { - storm::parser::SparseStateRewardParser srp(stateCount, stateRewardFile); - this->stateRewards = srp.getStateRewards(); + result.stateRewards.reset(storm::parser::SparseStateRewardParser(stateCount, stateRewardFile)); } if (transitionRewardFile != "") { RewardMatrixInformationStruct* rewardMatrixInfo = new RewardMatrixInformationStruct(stateCount, stateCount, nullptr); - storm::parser::DeterministicSparseTransitionParser trp(transitionRewardFile, false, rewardMatrixInfo); + result.transitionRewards.reset(storm::parser::DeterministicSparseTransitionParser(transitionRewardFile, false, rewardMatrixInfo)); delete rewardMatrixInfo; - this->transitionRewards = trp.getMatrix(); } - this->dtmc = nullptr; - this->ctmc = nullptr; + + return result; +} + +/*! + * Uses the Function parseDeterministicModel 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 DeterministicModelParserAsDtmc(std::string const & transitionSystemFile, std::string const & labelingFile, + std::string const & stateRewardFile, std::string const & transitionRewardFile) { + DeterministicModelParserResultContainer parserResult = parseDeterministicModel(transitionRewardFile, labelingFile, stateRewardFile, transitionRewardFile); + return storm::models::Dtmc(parserResult.transitionSystem, parserResult.labeling, parserResult.stateRewards, parserResult.transitionRewards); +} + +/*! + * Uses the Function parseDeterministicModel 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 DeterministicModelParserAsCtmc(std::string const & transitionSystemFile, std::string const & labelingFile, + std::string const & stateRewardFile, std::string const & transitionRewardFile) { + DeterministicModelParserResultContainer parserResult = parseDeterministicModel(transitionRewardFile, labelingFile, stateRewardFile, transitionRewardFile); + return storm::models::Ctmc(parserResult.transitionSystem, parserResult.labeling, parserResult.stateRewards, parserResult.transitionRewards); } } /* namespace parser */ diff --git a/src/parser/DeterministicModelParser.h b/src/parser/DeterministicModelParser.h index de067f925..26bcde2bb 100644 --- a/src/parser/DeterministicModelParser.h +++ b/src/parser/DeterministicModelParser.h @@ -12,51 +12,44 @@ #include "src/models/Dtmc.h" #include "src/models/Ctmc.h" +#include + namespace storm { namespace parser { /*! - * @brief Load label and transition file and return initialized dtmc or ctmc object. + * @brief Load label and transition file and returns an initialized dtmc or ctmc object. * - * @note This class creates a new Dtmc or Ctmc object that can - * be accessed via getDtmc() or getCtmc(). However, it will not delete this object! + * @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 storm::parser::Parser { - public: - DeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile, + + +storm::models::Dtmc DeterministicModelParserAsDtmc(std::string const & transitionSystemFile, std::string const & labelingFile, + std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); +storm::models::Ctmc DeterministicModelParserAsCtmc(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); - /*! - * @brief Get the parsed dtmc model. - */ - std::shared_ptr> getDtmc() { - if (this->dtmc == nullptr) { - this->dtmc = std::shared_ptr>(new storm::models::Dtmc(this->transitionSystem, this->labeling, this->stateRewards, this->transitionRewards)); - } - return this->dtmc; - } - /*! - * @brief Get the parsed ctmc model. - */ - std::shared_ptr> getCtmc() { - if (this->ctmc == nullptr) { - this->ctmc = std::shared_ptr>(new storm::models::Ctmc(this->transitionSystem, this->labeling, this->stateRewards, this->transitionRewards)); - } - return this->ctmc; - } - - private: - std::shared_ptr> transitionSystem; - std::shared_ptr labeling; - std::shared_ptr> stateRewards; - std::shared_ptr> transitionRewards; - - std::shared_ptr> dtmc; - std::shared_ptr> ctmc; +/*! + * @brief This Class acts as a container much like std::pair for the four return values of the DeterministicModelParser + */ +template +class DeterministicModelParserResultContainer { +public: + storm::storage::SparseMatrix transitionSystem; + storm::models::AtomicPropositionsLabeling labeling; + boost::optional> stateRewards; + boost::optional> transitionRewards; + DeterministicModelParserResultContainer(storm::storage::SparseMatrix& transitionSystem, storm::models::AtomicPropositionsLabeling& labeling) : transitionSystem(transitionSystem), labeling(labeling) { } +private: + DeterministicModelParserResultContainer() {} }; + +DeterministicModelParserResultContainer parseDeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile, + std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); + } /* namespace parser */ } /* namespace storm */ #endif /* STORM_PARSER_DETERMINISTICMODELPARSER_H_ */ diff --git a/src/parser/LtlParser.cpp b/src/parser/LtlParser.cpp index da90ad04f..cc1bee3e7 100644 --- a/src/parser/LtlParser.cpp +++ b/src/parser/LtlParser.cpp @@ -128,7 +128,7 @@ struct LtlGrammar : qi::grammar storm::parser::LtlParser(std::string formulaString) { +storm::property::ltl::AbstractLtlFormula* storm::parser::LtlParser(std::string formulaString) { // Prepare iterators to input. BaseIteratorType stringIteratorBegin = formulaString.begin(); BaseIteratorType stringIteratorEnd = formulaString.end(); @@ -178,6 +178,6 @@ storm::property::ltl::AbstractLtlFormularSharedPtr_t storm::parser::LtlP throw storm::exceptions::WrongFormatException() << "Syntax error in formula"; } - return storm::property::ltl::AbstractLtlFormularSharedPtr_t(result_pointer); + return result_pointer; } diff --git a/src/parser/LtlParser.h b/src/parser/LtlParser.h index bf173d44f..20e82896b 100644 --- a/src/parser/LtlParser.h +++ b/src/parser/LtlParser.h @@ -23,7 +23,7 @@ namespace parser { * @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); +storm::property::ltl::AbstractLtlFormula* LtlParser(std::string formulaString); /*! * Struct for the Ltl grammar, that Boost::Spirit uses to parse the formulas. diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index cba3867e7..456b838dc 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -32,7 +32,7 @@ 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 PrismParser::parseFile(std::string const& filename) const { +storm::ir::Program parseFile(std::string const& filename) { // Open file and initialize result. std::ifstream inputFileStream(filename, std::ios::in); storm::ir::Program result; @@ -56,7 +56,7 @@ storm::ir::Program PrismParser::parseFile(std::string const& filename) const { * 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 PrismParser::parse(std::istream& inputStream, std::string const& filename) const { +storm::ir::Program parse(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 48326713f..01bd2b830 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -21,28 +21,33 @@ namespace parser { using namespace storm::ir; using namespace storm::ir::expressions; +/* + * This functions parse the format of the PRISM model checker into an intermediate representation. + */ + +/*! + * Parses the given file into the intermediate representation assuming it complies with the + * PRISM syntax. + * @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); + /*! - * This class parses the format of the PRISM model checker into an intermediate representation. + * Parses the given input stream into the intermediate representation assuming it complies with + * the PRISM syntax. + * @param inputStream the input stream to parse. + * @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: - /*! - * Parses the given file into the intermediate representation assuming it complies with the - * PRISM syntax. - * @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) const; + private: - /*! - * Parses the given input stream into the intermediate representation assuming it complies with - * the PRISM syntax. - * @param inputStream the input stream to parse. - * @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) const; + }; } // namespace parser