diff --git a/src/parser/PrctlFileParser.cpp b/src/parser/PrctlFileParser.cpp index 434adfed4..f155a11cb 100644 --- a/src/parser/PrctlFileParser.cpp +++ b/src/parser/PrctlFileParser.cpp @@ -16,69 +16,29 @@ 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: - //Eigen Model Checker is not completely implemented at the moment, thus using Eigen is not possible... - //Current behaviour: Fall back to GMMXX... - //modelChecker = new storm::modelchecker::EigenDtmcPrctlModelChecker(dtmc); - // break; - case GMMXX: - default: //Note: GMMXX is default, hence default branches here, too. - modelChecker = new storm::modelchecker::GmmxxDtmcPrctlModelChecker(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: - //Eigen MDP Model Checker is not implemented yet - //Current behaviour: Fall back to GMMXX... - // break; - case GMMXX: - default: //Note: GMMXX is default, hence default branches here, too. - modelChecker = new storm::modelchecker::GmmxxMdpPrctlModelChecker(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; +PrctlFileParser::PrctlFileParser() { + //Intentionally left empty } PrctlFileParser::~PrctlFileParser() { //intentionally left empty } -void PrctlFileParser::check(std::string filename, storm::modelchecker::AbstractModelChecker* modelChecker) { +std::list*> parseFormulas(std::string filename) { // Open file std::ifstream inputFileStream(filename, std::ios::in); + std::list*> result; while(!inputFileStream.eof()) { std::string line; //The while loop reads the input file line by line while (std::getline(inputFileStream, line)) { PrctlParser parser(line); - storm::property::prctl::AbstractStateFormula* stateFormula = dynamic_cast*>(parser.getFormula()); - if (stateFormula != nullptr) { - modelChecker->check(*stateFormula); - } - storm::property::prctl::AbstractNoBoundOperator* noBoundFormula = dynamic_cast*>(parser.getFormula()); - if (noBoundFormula != nullptr) { - modelChecker->check(*noBoundFormula); - } - delete parser.getFormula(); + result.push_back(parser.getFormula()); } } + + return result; } } /* namespace parser */ diff --git a/src/parser/PrctlFileParser.h b/src/parser/PrctlFileParser.h index f82b62574..ee0987cfe 100644 --- a/src/parser/PrctlFileParser.h +++ b/src/parser/PrctlFileParser.h @@ -8,10 +8,9 @@ #ifndef STORM_PARSER_PRCTLFILEPARSER_H_ #define STORM_PARSER_PRCTLFILEPARSER_H_ -#include "models/Dtmc.h" -#include "models/Mdp.h" #include "formula/Prctl.h" -#include "modelchecker/AbstractModelChecker.h" + +#include namespace storm { namespace parser { @@ -25,46 +24,25 @@ namespace parser { */ class PrctlFileParser { public: - enum libraries { - GMMXX, - EIGEN - }; - /*! - * Reads a given file of formulas and checks each of these against a given DTMC. - * - * @param filename The name of the file to parse - * @param dtmc The DTMC model to check - * @param library Specifies the library that should perform the algebraic operations during model checking (default is GMMxx) - */ - PrctlFileParser(std::string filename, storm::models::Dtmc& dtmc, enum libraries library=GMMXX); - - /*! - * Reads a given file of formulas and checks each of these against a given MDP. - * - * @param filename The name of the file to parse - * @param mdp The MDP model to check - * @param library Specifies the library that should perform the algebraic operations during model checking (default is GMMxx, which at the moment also is the only implemented version...) + * Constructor */ - PrctlFileParser(std::string filename, storm::models::Mdp& mdp, enum libraries library=GMMXX); + PrctlFileParser(); -protected: /*! - * Does the actual checking. - * This procedure is equal for all model types (only the model checker is different, so it has to be created in - * different methods beforehand) + * Destructor. + * At this time, empty * - * @param filename The name of the file to parse - * @param modelChecker The model checker that checks the formula (has to know its model!) */ - void check(std::string filename, storm::modelchecker::AbstractModelChecker* modelChecker); + virtual ~PrctlFileParser(); /*! - * Destructor. - * At this time, empty + * 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 */ - virtual ~PrctlFileParser(); + std::list*> parseFormulas(std::string filename); }; } /* namespace parser */