diff --git a/src/parser/PrctlFileParser.cpp b/src/parser/PrctlFileParser.cpp index ad72486e9..beabee439 100644 --- a/src/parser/PrctlFileParser.cpp +++ b/src/parser/PrctlFileParser.cpp @@ -17,7 +17,7 @@ namespace storm { namespace parser { PrctlFileParser::PrctlFileParser(std::string filename, storm::models::Dtmc& dtmc, enum libraries library) { - + //Here ,the model checker which uses the correct library is created and a reference stored in the pointer modelChecker: storm::modelchecker::SparseDtmcPrctlModelChecker* modelChecker = nullptr; switch(library) { //case EIGEN: @@ -30,11 +30,14 @@ PrctlFileParser::PrctlFileParser(std::string filename, storm::models::Dtmc(dtmc); break; } + + //Now, the check function (which works on abstract model checkers) can parse the formulas and invoke the model checker: check(filename, modelChecker); delete modelChecker; } PrctlFileParser::PrctlFileParser(std::string filename, storm::models::Mdp& mdp, enum libraries library) { + //Here ,the model checker which uses the correct library is created and a reference stored in the pointer modelChecker: storm::modelchecker::SparseMdpPrctlModelChecker* modelChecker = nullptr; switch(library) { //case EIGEN: @@ -46,6 +49,8 @@ PrctlFileParser::PrctlFileParser(std::string filename, storm::models::Mdp(mdp); break; } + + //Now, the check function (which works on abstract model checkers) can parse the formulas and invoke the model checker: check(filename, modelChecker); delete modelChecker; } diff --git a/src/parser/PrctlParser.h b/src/parser/PrctlParser.h index 22e11a274..b549c0d62 100644 --- a/src/parser/PrctlParser.h +++ b/src/parser/PrctlParser.h @@ -18,8 +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 : Parser { public: /*! * Reads a PRCTL formula from its string representation and parses it into a formula tree, consisting of @@ -35,8 +34,7 @@ class PrctlParser : Parser /*! * @return a pointer to the parsed formula object */ - storm::formula::AbstractFormula* getFormula() - { + storm::formula::AbstractFormula* getFormula() { return this->formula; }