diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h index 698aaa466..5c468959f 100644 --- a/src/modelchecker/AbstractModelChecker.h +++ b/src/modelchecker/AbstractModelChecker.h @@ -111,6 +111,13 @@ public: return result; } + /*! + * Checks the given state formula on the DTMC and prints the result (true/false) for all initial + * states. (Abstract) + * @param stateFormula The formula to be checked. + */ + virtual void check(const storm::formula::AbstractStateFormula<Type>& stateFormula) const = 0; + /*! * The check method for a state formula with a bound operator node as root in * its formula tree diff --git a/src/parser/PrctlFileParser.cpp b/src/parser/PrctlFileParser.cpp index 13cede17c..9efa1186a 100644 --- a/src/parser/PrctlFileParser.cpp +++ b/src/parser/PrctlFileParser.cpp @@ -7,10 +7,12 @@ #include "PrctlFileParser.h" +#define LINELENGTH 100 + namespace storm { namespace parser { -PrctlFileParser::PrctlFileParser(std::string filename) { +PrctlFileParser::PrctlFileParser(std::string filename, storm::modelChecker::AbstractModelChecker<double>* modelChecker) { // Open file and initialize result. std::ifstream inputFileStream(filename, std::ios::in); @@ -18,8 +20,12 @@ PrctlFileParser::PrctlFileParser(std::string filename) { // While this is usually not necessary, because there exist adapters that make an input stream // iterable in both directions without storing it into a string, using the corresponding // Boost classes gives an awful output under valgrind and is thus disabled for the time being. - std::string fileContent((std::istreambuf_iterator<char>(inputFileStream)), (std::istreambuf_iterator<char>())); - parse(fileContent); + while(!inputFileStream.eof()) { + char line[LINELENGTH]; + inputFileStream.getline(line, LINELENGTH); + + } + } PrctlFileParser::~PrctlFileParser() { diff --git a/src/parser/PrctlFileParser.h b/src/parser/PrctlFileParser.h index 208550067..83bad00c5 100644 --- a/src/parser/PrctlFileParser.h +++ b/src/parser/PrctlFileParser.h @@ -9,6 +9,7 @@ #define STORM_PARSER_PRCTLFILEPARSER_H_ #include "PrctlParser.h" +#include "modelchecker/AbstractModelChecker.h" namespace storm { namespace parser { @@ -20,7 +21,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 PrctlFileParser: public storm::parser::PrctlParser { +class PrctlFileParser { public: /*! * Reads the formula from the given file and parses it into a formula tree, consisting of @@ -31,7 +32,7 @@ public: * @param filename The name of the file to parse * @throw wrongFormatException If the input could not be parsed successfully */ - PrctlFileParser(std::string filename); + PrctlFileParser(std::string filename, storm::modelChecker::AbstractModelChecker<double>* modelChecker); /*! * Destructor. diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp index f827794f1..e7f166138 100644 --- a/src/parser/PrctlParser.cpp +++ b/src/parser/PrctlParser.cpp @@ -17,6 +17,7 @@ // Needed for file IO. #include <fstream> #include <iomanip> +#include <map> // Some typedefs and namespace definitions to reduce code size. @@ -32,19 +33,19 @@ namespace storm { namespace parser { template<typename Iterator, typename Skipper> -struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::AbstractFormula<double>*(), Skipper> { +struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::AbstractFormula<double>*(), Skipper > { PrctlGrammar() : PrctlGrammar::base_type(start) { freeIdentifierName = qi::lexeme[+(qi::alpha | qi::char_('_'))]; //This block defines rules for parsing state formulas stateFormula %= orFormula; stateFormula.name("state formula"); - andFormula = notFormula[qi::_val = qi::_1] > *(qi::lit("&") > notFormula)[qi::_val = - phoenix::new_<storm::formula::And<double>>(qi::_val, qi::_1)]; - andFormula.name("state formula"); orFormula = andFormula[qi::_val = qi::_1] > *(qi::lit("|") > andFormula)[qi::_val = phoenix::new_<storm::formula::Or<double>>(qi::_val, qi::_1)]; orFormula.name("state formula"); + andFormula = notFormula[qi::_val = qi::_1] > *(qi::lit("&") > notFormula)[qi::_val = + phoenix::new_<storm::formula::And<double>>(qi::_val, qi::_1)]; + andFormula.name("state formula"); notFormula = atomicStateFormula[qi::_val = qi::_1] | (qi::lit("!") > atomicStateFormula)[qi::_val = phoenix::new_<storm::formula::Not<double>>(qi::_1)]; notFormula.name("state formula"); @@ -101,11 +102,11 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::Abstrac globally = (qi::lit("G") > stateFormula)[qi::_val = phoenix::new_<storm::formula::Globally<double> >(qi::_1)]; globally.name("path formula"); - boundedUntil = (stateFormula >> qi::lit("U") >> qi::lit("<=") > qi::int_ > stateFormula)[qi::_val = - phoenix::new_<storm::formula::BoundedUntil<double>>(qi::_1, qi::_3, qi::_2)]; + boundedUntil = (stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") >> qi::lit("<=") > qi::int_ > stateFormula) + [qi::_val = phoenix::new_<storm::formula::BoundedUntil<double>>(phoenix::bind(&storm::formula::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::AbstractStateFormula<double>>::get, qi::_a)), qi::_3, qi::_2)]; boundedUntil.name("path formula"); - until = (stateFormula >> qi::lit("U") > stateFormula)[qi::_val = - phoenix::new_<storm::formula::Until<double>>(qi::_1, qi::_2)]; + until = (stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") > stateFormula)[qi::_val = + phoenix::new_<storm::formula::Until<double>>(phoenix::bind(&storm::formula::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::AbstractStateFormula<double>>::get, qi::_a)), qi::_2)]; until.name("path formula"); start = (noBoundOperator | stateFormula); @@ -132,8 +133,8 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::Abstrac qi::rule<Iterator, storm::formula::BoundedEventually<double>*(), Skipper> boundedEventually; qi::rule<Iterator, storm::formula::Eventually<double>*(), Skipper> eventually; qi::rule<Iterator, storm::formula::Globally<double>*(), Skipper> globally; - qi::rule<Iterator, storm::formula::BoundedUntil<double>*(), Skipper> boundedUntil; - qi::rule<Iterator, storm::formula::Until<double>*(), Skipper> until; + qi::rule<Iterator, storm::formula::BoundedUntil<double>*(), qi::locals< std::shared_ptr<storm::formula::AbstractStateFormula<double>>>, Skipper> boundedUntil; + qi::rule<Iterator, storm::formula::Until<double>*(), qi::locals< std::shared_ptr<storm::formula::AbstractStateFormula<double>>>, Skipper> until; qi::rule<Iterator, std::string(), Skipper> freeIdentifierName; @@ -142,7 +143,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::Abstrac } //namespace storm } //namespace parser -void storm::parser::PrctlParser::parse(std::string formulaString) { +storm::parser::PrctlParser::PrctlParser(std::string formulaString) { // Prepare iterators to input. BaseIteratorType stringIteratorBegin = formulaString.begin(); BaseIteratorType stringIteratorEnd = formulaString.end(); @@ -194,9 +195,3 @@ void storm::parser::PrctlParser::parse(std::string formulaString) { formula = result_pointer; } - -storm::parser::PrctlParser::PrctlParser(std::string formula) { - // delegate the string to the parse function - // this function has to be separate, as it may be called in subclasses which don't call this constructor - parse(formula); -} diff --git a/src/parser/PrctlParser.h b/src/parser/PrctlParser.h index 41771cf3d..7f97d4293 100644 --- a/src/parser/PrctlParser.h +++ b/src/parser/PrctlParser.h @@ -39,33 +39,6 @@ class PrctlParser : Parser { return this->formula; } - - protected: - /*! - * Empty constructor. - * - * Some subclasses do not get a formula string as input (E.g. PrctlFileParser), hence they should not - * call the usual constructor of this class. - * - * However, this constructor should never be called directly (only during construction of an object of - * a subclass), as it will not parse anything (and formula will point to nullptr then); hence, it is - * protected. - */ - PrctlParser() { - formula = nullptr; - } - - /*! - * Does the actual parsing. - * - * Is to be called once in a constructor, and never from any other location. - * The function is not included in the constructor, as sub classes may use constructors - * that calculate the string representation of the formula (e.g. read it from a file), hence they - * cannot hand it over to a constructor of this class. - * - * @param formula The string representation of the formula to parse - */ - void parse(std::string formula); private: storm::formula::AbstractFormula<double>* formula; diff --git a/test/eigen/EigenAdapterTest.cpp b/test/eigen/EigenAdapterTest.cpp index bddb74dd7..fef057fcb 100644 --- a/test/eigen/EigenAdapterTest.cpp +++ b/test/eigen/EigenAdapterTest.cpp @@ -45,6 +45,8 @@ TEST(EigenAdapterTest, SimpleDenseSquareCopy) { col = 0; } } + + delete esm; } TEST(EigenAdapterTest, SimpleSparseSquareCopy) { @@ -93,4 +95,6 @@ TEST(EigenAdapterTest, SimpleSparseSquareCopy) { col = 0; } } + + delete esm; } diff --git a/test/parser/PrctlParserTest.cpp b/test/parser/PrctlParserTest.cpp index f0c89dcb1..dbb6c2a10 100644 --- a/test/parser/PrctlParserTest.cpp +++ b/test/parser/PrctlParserTest.cpp @@ -130,6 +130,7 @@ TEST(PrctlParserTest, parseComplexFormulaTest) { } + TEST(PrctlParserTest, wrongProbabilisticFormulaTest) { storm::parser::PrctlParser* prctlParser = nullptr; ASSERT_THROW( @@ -143,7 +144,7 @@ TEST(PrctlParserTest, wrongProbabilisticFormulaTest) { TEST(PrctlParserTest, wrongFormulaTest) { storm::parser::PrctlParser* prctlParser = nullptr; ASSERT_THROW( - prctlParser = new storm::parser::PrctlFileParser("& a"), + prctlParser = new storm::parser::PrctlFileParser("(a | b) & ΓΌ"), storm::exceptions::WrongFormatException ); delete prctlParser;