diff --git a/src/formula/Csl/CslFilter.h b/src/formula/Csl/CslFilter.h index 1507d1c2b..dbbd22368 100644 --- a/src/formula/Csl/CslFilter.h +++ b/src/formula/Csl/CslFilter.h @@ -154,7 +154,7 @@ public: std::string desc = "Filter: "; desc += "\nActions:"; for(auto action : this->actions) { - desc += "\n\t" + action.toString(); + desc += "\n\t" + action->toString(); } desc += "\nFormula:\n\t" + child->toString(); return desc; diff --git a/src/formula/Prctl/PrctlFilter.h b/src/formula/Prctl/PrctlFilter.h index d5559246b..7302148a3 100644 --- a/src/formula/Prctl/PrctlFilter.h +++ b/src/formula/Prctl/PrctlFilter.h @@ -63,7 +63,7 @@ public: storm::storage::BitVector result; try { - result = evaluate(modelchecker, static_cast*>(child)); + result = evaluate(modelchecker, dynamic_cast*>(child)); } catch (std::exception& e) { std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl; LOG4CPLUS_ERROR(logger, "Error during computation: " << e.what() << "Skipping property."); @@ -80,7 +80,7 @@ public: // Return the results for all states labeled with "init". LOG4CPLUS_INFO(logger, "Result for initial states:"); std::cout << "Result for initial states:" << std::endl; - for (auto initialState : modelchecker.getModel().getInitialStates()) { + for (auto initialState : modelchecker.template getModel>().getInitialStates()) { LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result.get(initialState) ? "satisfied" : "not satisfied")); std::cout << "\t" << initialState << ": " << result.get(initialState) << std::endl; } @@ -95,7 +95,7 @@ public: std::vector result; try { - result = evaluate(modelchecker, static_cast*>(child)); + result = evaluate(modelchecker, dynamic_cast*>(child)); } catch (std::exception& e) { std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl; LOG4CPLUS_ERROR(logger, "Error during computation: " << e.what() << "Skipping property."); @@ -112,7 +112,7 @@ public: // Return the results for all states labeled with "init". LOG4CPLUS_INFO(logger, "Result for initial states:"); std::cout << "Result for initial states:" << std::endl; - for (auto initialState : modelchecker.getModel().getInitialStates()) { + for (auto initialState : modelchecker.template getModel>().getInitialStates()) { LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << result[initialState]); std::cout << "\t" << initialState << ": " << result[initialState] << std::endl; } @@ -127,7 +127,7 @@ public: std::vector result; try { - result = evaluate(modelchecker, static_cast*>(child)); + result = evaluate(modelchecker, dynamic_cast*>(child)); } catch (std::exception& e) { std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl; LOG4CPLUS_ERROR(logger, "Error during computation: " << e.what() << "Skipping property."); @@ -144,7 +144,7 @@ public: // Return the results for all states labeled with "init". LOG4CPLUS_INFO(logger, "Result for initial states:"); std::cout << "Result for initial states:" << std::endl; - for (auto initialState : modelchecker.getModel().getInitialStates()) { + for (auto initialState : modelchecker.template getModel>().getInitialStates()) { LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << result[initialState]); std::cout << "\t" << initialState << ": " << result[initialState] << std::endl; } @@ -208,7 +208,7 @@ private: if(this->getActionCount() != 0 && dynamic_cast*>(this->getAction(0)) != nullptr) { // If there is an action specifying that min/max probabilities should be computed, call the appropriate method of the model checker. - result = modelchecker.checkMinMaxOperator(formula, static_cast*>(this->getAction(0))->getMinimize()); + result = modelchecker.checkMinMaxOperator(*formula, static_cast*>(this->getAction(0))->getMinimize()); } else { result = formula->check(modelchecker); } @@ -227,7 +227,7 @@ private: if(this->getActionCount() != 0 && dynamic_cast*>(this->getAction(0)) != nullptr) { // If there is an action specifying that min/max probabilities should be computed, call the appropriate method of the model checker. - result = modelchecker.checkMinMaxOperator(formula, static_cast*>(this->getAction(0))->getMinimize()); + result = modelchecker.checkMinMaxOperator(*formula, dynamic_cast*>(this->getAction(0))->getMinimize()); } else { result = formula->check(modelchecker, false); } @@ -245,7 +245,7 @@ private: if(this->getActionCount() != 0 && dynamic_cast*>(this->getAction(0)) != nullptr) { // If there is an action specifying that min/max probabilities should be computed, call the appropriate method of the model checker. - result = modelchecker.checkMinMaxOperator(formula, static_cast*>(this->getAction(0))->getMinimize()); + result = modelchecker.checkMinMaxOperator(*formula, dynamic_cast*>(this->getAction(0))->getMinimize()); } else { result = formula->check(modelchecker, false); } diff --git a/src/parser/CslParser.cpp b/src/parser/CslParser.cpp index 52c4012aa..5ae34df1c 100644 --- a/src/parser/CslParser.cpp +++ b/src/parser/CslParser.cpp @@ -43,7 +43,7 @@ namespace storm { namespace parser { template -struct CslGrammar : qi::grammar*(), Skipper > { +struct CslParser::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_('_'))]; @@ -202,7 +202,7 @@ struct CslGrammar : qi::grammar* CslParser(std::string formulaString) { +storm::property::csl::CslFilter* CslParser::parseCslFormula(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 179cde297..ddc767438 100644 --- a/src/parser/CslParser.h +++ b/src/parser/CslParser.h @@ -15,22 +15,29 @@ 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::CslFilter* CslParser(std::string formulaString); +class CslParser { +public: -/*! - * Struct for the CSL grammar, that Boost::Spirit uses to parse the formulas. - */ -template -struct CslGrammar; + /*! + * 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 + */ + static storm::property::csl::CslFilter* parseCslFormula(std::string formulaString); + +private: + + /*! + * Struct for the CSL grammar, that Boost::Spirit uses to parse the formulas. + */ + template + struct CslGrammar; + +}; } /* namespace parser */ } /* namespace storm */ diff --git a/src/parser/PrctlFileParser.cpp b/src/parser/PrctlFileParser.cpp index 9fadfbf2f..ca5905e4e 100644 --- a/src/parser/PrctlFileParser.cpp +++ b/src/parser/PrctlFileParser.cpp @@ -14,7 +14,7 @@ namespace storm { namespace parser { -std::list*> PrctlFileParser(std::string filename) { +std::list*> PrctlFileParser::parsePrctlFile(std::string filename) { // Open file std::ifstream inputFileStream; inputFileStream.open(filename, std::ios::in); @@ -29,11 +29,11 @@ std::list*> PrctlFileParser(std::str std::string line; //The while loop reads the input file line by line while (std::getline(inputFileStream, line)) { - PrctlParser parser(line); - if (!parser.parsedComment()) { + storm::property::prctl::PrctlFilter* formula = PrctlParser::parsePrctlFormula(line); + if (formula != nullptr) { //lines containing comments will be skipped. - LOG4CPLUS_INFO(logger, "Parsed formula \"" + line + "\" into \"" + parser.getFormula()->toString() + "\""); - result.push_back(parser.getFormula()); + LOG4CPLUS_INFO(logger, "Parsed formula \"" + line + "\" into \"" + formula->toString() + "\""); + result.push_back(formula); } } diff --git a/src/parser/PrctlFileParser.h b/src/parser/PrctlFileParser.h index 15fc6b382..4d914d8cc 100644 --- a/src/parser/PrctlFileParser.h +++ b/src/parser/PrctlFileParser.h @@ -16,13 +16,18 @@ namespace storm { namespace parser { -/*! - * 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 - */ -std::list*> PrctlFileParser(std::string filename); +class PrctlFileParser { +public: + + /*! + * 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 + */ + static std::list*> parsePrctlFile(std::string filename); + +}; } /* namespace parser */ } /* namespace storm */ diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp index 82d0a3550..d92cd6178 100644 --- a/src/parser/PrctlParser.cpp +++ b/src/parser/PrctlParser.cpp @@ -32,7 +32,6 @@ namespace qi = boost::spirit::qi; namespace phoenix = boost::phoenix; - namespace storm { namespace parser { @@ -165,7 +164,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar (comment | qi::eps))[qi::_val = qi::_1] | comment) > qi::eoi; + start = (((filter) > (comment | qi::eps))[qi::_val = qi::_1] | comment[qi::_val = nullptr]) > qi::eoi; start.name("PRCTL formula filter"); } @@ -216,7 +215,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar* storm::parser::PrctlParser::parsePrctlFormula(std::string formulaString) { // Prepare iterators to input. BaseIteratorType stringIteratorBegin = formulaString.begin(); BaseIteratorType stringIteratorEnd = formulaString.end(); @@ -259,5 +258,5 @@ storm::parser::PrctlParser::PrctlParser(std::string formulaString) { throw storm::exceptions::WrongFormatException() << msg.str(); } - formula = result_pointer; + return result_pointer; } diff --git a/src/parser/PrctlParser.h b/src/parser/PrctlParser.h index 52a403afd..6e1a55c34 100644 --- a/src/parser/PrctlParser.h +++ b/src/parser/PrctlParser.h @@ -17,43 +17,27 @@ namespace parser { * class PrctlParser). However, it will not delete this object. */ class PrctlParser { - public: - /*! - * Reads a PRCTL 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 - */ - PrctlParser(std::string formulaString); - - /*! - * @return a pointer to the parsed formula object - */ - storm::property::prctl::PrctlFilter* getFormula() { - return this->formula; - } - - /*! - * Checks whether the line which was parsed was a comment line; also returns true if the line was empty (as the semantics are - * the same) - * - * @return True if the parsed line consisted completely of a (valid) comment, false otherwise. - */ - bool parsedComment() { - return (formula == nullptr); - } - - private: - storm::property::prctl::PrctlFilter* formula; - - /*! - * Struct for the Prctl grammar, that Boost::Spirit uses to parse the formulas. - */ - template - struct PrctlGrammar; +public: + + /*! + * Reads a PRCTL 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 + * @return A pointer to the parsed Prctl formula. If the line just contained a comment a nullptr will be returned instead. + */ + static storm::property::prctl::PrctlFilter* parsePrctlFormula(std::string formulaString); + +private: + + /*! + * Struct for the Prctl grammar, that Boost::Spirit uses to parse the formulas. + */ + template + struct PrctlGrammar; }; diff --git a/src/storm.cpp b/src/storm.cpp index a13bf8e23..5b4e06309 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -285,10 +285,10 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker if (s->isSet("prctl")) { std::string const chosenPrctlFile = s->getOptionByLongName("prctl").getArgument(0).getValueAsString(); LOG4CPLUS_INFO(logger, "Parsing prctl file: " << chosenPrctlFile << "."); - std::list*> formulaList = storm::parser::PrctlFileParser(chosenPrctlFile); + std::list*> formulaList = storm::parser::PrctlFileParser::parsePrctlFile(chosenPrctlFile); for (auto formula : formulaList) { - modelchecker.check(*formula); + formula->check(modelchecker); delete formula; } } @@ -339,7 +339,7 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker std::string const chosenPrctlFile = s->getOptionByLongName("prctl").getArgument(0).getValueAsString(); LOG4CPLUS_INFO(logger, "Parsing prctl file: " << chosenPrctlFile << "."); - std::list*> formulaList = storm::parser::PrctlFileParser(chosenPrctlFile); + std::list*> formulaList = storm::parser::PrctlFileParser::parsePrctlFile(chosenPrctlFile); // Test for each formula if a counterexample can be generated for it. if(formulaList.size() == 0) { @@ -369,13 +369,13 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker for (auto formula : formulaList) { // First check if it is a formula type for which a counterexample can be generated. - if (dynamic_cast const*>(formula) == nullptr) { + if (dynamic_cast const*>(formula->getChild()) == nullptr) { LOG4CPLUS_ERROR(logger, "Unexpected kind of formula. Expected a state formula."); delete formula; continue; } - storm::property::prctl::AbstractStateFormula const& stateForm = static_cast const&>(*formula); + storm::property::prctl::AbstractStateFormula const& stateForm = static_cast const&>(*(formula->getChild())); // Do some output std::cout << "Generating counterexample for formula " << fIndex << ":" << std::endl; @@ -552,14 +552,14 @@ int main(const int argc, const char* argv[]) { // Now parse the property file and receive the list of parsed formulas. std::string const& propertyFile = s->getOptionByLongName("mincmd").getArgumentByName("propertyFile").getValueAsString(); - std::list*> formulaList = storm::parser::PrctlFileParser(propertyFile); + std::list*> formulaList = storm::parser::PrctlFileParser::parsePrctlFile(propertyFile); // Now generate the counterexamples for each formula. - for (storm::property::prctl::AbstractPrctlFormula* formulaPtr : formulaList) { + for (storm::property::prctl::PrctlFilter* formulaPtr : formulaList) { if (useMILP) { - storm::counterexamples::MILPMinimalLabelSetGenerator::computeCounterexample(program, *mdp, formulaPtr); + storm::counterexamples::MILPMinimalLabelSetGenerator::computeCounterexample(program, *mdp, formulaPtr->getChild()); } else { - storm::counterexamples::SMTMinimalCommandSetGenerator::computeCounterexample(program, constants, *mdp, formulaPtr); + storm::counterexamples::SMTMinimalCommandSetGenerator::computeCounterexample(program, constants, *mdp, formulaPtr->getChild()); } // Once we are done with the formula, delete it. diff --git a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp index fdff14a66..ac90211b5 100644 --- a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp @@ -24,43 +24,39 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) { storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("one"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); - std::vector result = probFormula->check(mc); + std::vector result = eventuallyFormula->check(mc, false); ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete probFormula; + delete eventuallyFormula; apFormula = new storm::property::prctl::Ap("two"); eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); - result = probFormula->check(mc); + result = eventuallyFormula->check(mc, false); ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete probFormula; + delete eventuallyFormula; apFormula = new storm::property::prctl::Ap("three"); eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); - result = probFormula->check(mc); + result = eventuallyFormula->check(mc, false); ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete probFormula; + delete eventuallyFormula; storm::property::prctl::Ap* done = new storm::property::prctl::Ap("done"); storm::property::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(done); - storm::property::prctl::RewardNoBoundOperator* rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula); - result = rewardFormula->check(mc); + result = reachabilityRewardFormula->check(mc, false); ASSERT_LT(std::abs(result[0] - ((double)11/3)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete rewardFormula; + delete reachabilityRewardFormula; } TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { @@ -73,40 +69,37 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { std::shared_ptr> dtmc = abstractModel->as>(); - ASSERT_EQ(dtmc->getNumberOfStates(), 8607ull); - ASSERT_EQ(dtmc->getNumberOfTransitions(), 22460ull); + ASSERT_EQ(8607ull, dtmc->getNumberOfStates()); + ASSERT_EQ(22460ull, dtmc->getNumberOfTransitions()); storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver()); storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("observe0Greater1"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); - std::vector result = probFormula->check(mc); + std::vector result = eventuallyFormula->check(mc, false); ASSERT_LT(std::abs(result[0] - 0.3328800375801578281), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete probFormula; + delete eventuallyFormula; apFormula = new storm::property::prctl::Ap("observeIGreater1"); eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); - result = probFormula->check(mc); + result = eventuallyFormula->check(mc, false); ASSERT_LT(std::abs(result[0] - 0.1522194965), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete probFormula; + delete eventuallyFormula; apFormula = new storm::property::prctl::Ap("observeOnlyTrueSender"); eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); - result = probFormula->check(mc); + result = eventuallyFormula->check(mc, false); ASSERT_LT(std::abs(result[0] - 0.32153724292835045), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete probFormula; + delete eventuallyFormula; } TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { @@ -118,38 +111,35 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { ASSERT_EQ(abstractModel->getType(), storm::models::DTMC); std::shared_ptr> dtmc = abstractModel->as>(); - ASSERT_EQ(dtmc->getNumberOfStates(), 12400ull); - ASSERT_EQ(dtmc->getNumberOfTransitions(), 28894ull); + ASSERT_EQ(12400ull, dtmc->getNumberOfStates()); + ASSERT_EQ(28894ull, dtmc->getNumberOfTransitions()); storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver()); storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("elected"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); - std::vector result = probFormula->check(mc); + std::vector result = eventuallyFormula->check(mc, false); ASSERT_LT(std::abs(result[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete probFormula; + delete eventuallyFormula; apFormula = new storm::property::prctl::Ap("elected"); storm::property::prctl::BoundedUntil* boundedUntilFormula = new storm::property::prctl::BoundedUntil(new storm::property::prctl::Ap("true"), apFormula, 20); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedUntilFormula); - result = probFormula->check(mc); + result = boundedUntilFormula->check(mc, false); ASSERT_LT(std::abs(result[0] - 0.9999965911265462636), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete probFormula; + delete boundedUntilFormula; apFormula = new storm::property::prctl::Ap("elected"); storm::property::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); - storm::property::prctl::RewardNoBoundOperator* rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula); - result = rewardFormula->check(mc); + result = reachabilityRewardFormula->check(mc, false); ASSERT_LT(std::abs(result[0] - 1.044879046), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete rewardFormula; + delete reachabilityRewardFormula; } diff --git a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp index 67fe2d63a..2fd8e148e 100644 --- a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp @@ -21,81 +21,55 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("two"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); - std::vector result = mc.checkNoBoundOperator(*probFormula); + std::vector result = mc.checkMinMaxOperator(*eventuallyFormula, true); ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete probFormula; - - apFormula = new storm::property::prctl::Ap("two"); - eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); - - result = mc.checkNoBoundOperator(*probFormula); - + result = mc.checkMinMaxOperator(*eventuallyFormula, false); + ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - - delete probFormula; + + delete eventuallyFormula; apFormula = new storm::property::prctl::Ap("three"); eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); - result = mc.checkNoBoundOperator(*probFormula); + result = mc.checkMinMaxOperator(*eventuallyFormula, true); ASSERT_LT(std::abs(result[0] - 0.0555555224418640136), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete probFormula; - - apFormula = new storm::property::prctl::Ap("three"); - eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); - - result = mc.checkNoBoundOperator(*probFormula); - + result = mc.checkMinMaxOperator(*eventuallyFormula, false); + ASSERT_LT(std::abs(result[0] - 0.0555555224418640136), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - - delete probFormula; + + delete eventuallyFormula; apFormula = new storm::property::prctl::Ap("four"); eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); - result = mc.checkNoBoundOperator(*probFormula); + result = mc.checkMinMaxOperator(*eventuallyFormula, true); ASSERT_LT(std::abs(result[0] - 0.083333283662796020508), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - - delete probFormula; - - apFormula = new storm::property::prctl::Ap("four"); - eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); - - result = mc.checkNoBoundOperator(*probFormula); + + result = mc.checkMinMaxOperator(*eventuallyFormula, false); ASSERT_LT(std::abs(result[0] - 0.083333283662796020508), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - - delete probFormula; - + + delete eventuallyFormula; + apFormula = new storm::property::prctl::Ap("done"); storm::property::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); - storm::property::prctl::RewardNoBoundOperator* rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); - - result = mc.checkNoBoundOperator(*rewardFormula); - + + result = mc.checkMinMaxOperator(*reachabilityRewardFormula, true); + ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete rewardFormula; - - apFormula = new storm::property::prctl::Ap("done"); - reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); - rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); - - result = mc.checkNoBoundOperator(*rewardFormula);; - + + result = mc.checkMinMaxOperator(*reachabilityRewardFormula, false); + ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete rewardFormula; + + delete reachabilityRewardFormula; abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", ""); @@ -107,21 +81,16 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { apFormula = new storm::property::prctl::Ap("done"); reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); - rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); - - result = stateRewardModelChecker.checkNoBoundOperator(*rewardFormula); + + result = mc.checkMinMaxOperator(*reachabilityRewardFormula, true); ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete rewardFormula; - - apFormula = new storm::property::prctl::Ap("done"); - reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); - rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); - - result = stateRewardModelChecker.checkNoBoundOperator(*rewardFormula); - + + result = mc.checkMinMaxOperator(*reachabilityRewardFormula, false); + ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete rewardFormula; + + delete reachabilityRewardFormula; abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew"); @@ -133,91 +102,67 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { apFormula = new storm::property::prctl::Ap("done"); reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); - rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); - result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula); + result = mc.checkMinMaxOperator(*reachabilityRewardFormula, true); ASSERT_LT(std::abs(result[0] - 14.666658998), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete rewardFormula; - - apFormula = new storm::property::prctl::Ap("done"); - reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); - rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); - - result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula); - + + result = mc.checkMinMaxOperator(*reachabilityRewardFormula, false); + ASSERT_LT(std::abs(result[0] - 14.666658998), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete rewardFormula; + + delete reachabilityRewardFormula; } TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { storm::settings::Settings* s = storm::settings::Settings::getInstance(); std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.trans.rew"); - ASSERT_EQ(abstractModel->getType(), storm::models::MDP); + ASSERT_EQ(storm::models::MDP, abstractModel->getType()); std::shared_ptr> mdp = abstractModel->as>(); - ASSERT_EQ(mdp->getNumberOfStates(), 3172ull); - ASSERT_EQ(mdp->getNumberOfTransitions(), 7144ull); + ASSERT_EQ(3172ull, mdp->getNumberOfStates()); + ASSERT_EQ(7144ull, mdp->getNumberOfTransitions()); storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, std::shared_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver())); storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("elected"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); - std::vector result = mc.checkNoBoundOperator(*probFormula); + std::vector result = mc.checkMinMaxOperator(*eventuallyFormula, true); ASSERT_LT(std::abs(result[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete probFormula; - - apFormula = new storm::property::prctl::Ap("elected"); - eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); - - result = mc.checkNoBoundOperator(*probFormula); + result = mc.checkMinMaxOperator(*eventuallyFormula, false); ASSERT_LT(std::abs(result[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete probFormula; + delete eventuallyFormula; apFormula = new storm::property::prctl::Ap("elected"); storm::property::prctl::BoundedEventually* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 25); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, false); - result = mc.checkNoBoundOperator(*probFormula); + result = mc.checkMinMaxOperator(*boundedEventuallyFormula, true); ASSERT_LT(std::abs(result[0] - 0.0625), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete probFormula; - - apFormula = new storm::property::prctl::Ap("elected"); - boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 25); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, true); - - result = mc.checkNoBoundOperator(*probFormula); + result = mc.checkMinMaxOperator(*boundedEventuallyFormula, false); ASSERT_LT(std::abs(result[0] - 0.0625), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete probFormula; + delete boundedEventuallyFormula; apFormula = new storm::property::prctl::Ap("elected"); storm::property::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); - storm::property::prctl::RewardNoBoundOperator* rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); - result = mc.checkNoBoundOperator(*rewardFormula);; + result = mc.checkMinMaxOperator(*reachabilityRewardFormula, true); ASSERT_LT(std::abs(result[0] - 4.285689611), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete rewardFormula; - apFormula = new storm::property::prctl::Ap("elected"); - reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); - rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); - - result = mc.checkNoBoundOperator(*rewardFormula);; + result = mc.checkMinMaxOperator(*reachabilityRewardFormula, false); ASSERT_LT(std::abs(result[0] - 4.285689611), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete rewardFormula; + + delete reachabilityRewardFormula; } diff --git a/test/functional/parser/CslParserTest.cpp b/test/functional/parser/CslParserTest.cpp index 4e4a67af9..9b8ad7ea9 100644 --- a/test/functional/parser/CslParserTest.cpp +++ b/test/functional/parser/CslParserTest.cpp @@ -11,130 +11,153 @@ #include "src/exceptions/WrongFormatException.h" TEST(CslParserTest, parseApOnlyTest) { - std::string formula = "ap"; - storm::property::csl::AbstractCslFormula* cslFormula = nullptr; + std::string input = "ap"; + storm::property::csl::CslFilter* formula = nullptr; ASSERT_NO_THROW( - cslFormula = storm::parser::CslParser(formula); + formula = storm::parser::CslParser::parseCslFormula(input); ); - ASSERT_NE(cslFormula, nullptr); - ASSERT_EQ(cslFormula->toString(), formula); + // The parser did not falsely recognize the input as a comment. + ASSERT_NE(formula, nullptr); - delete cslFormula; + // The input was parsed correctly. + ASSERT_EQ(input, formula->toString()); + + delete formula; } TEST(CslParserTest, parsePropositionalFormulaTest) { - std::string formula = "!(a & b) | a & ! c"; - storm::property::csl::AbstractCslFormula* cslFormula = nullptr; + std::string input = "!(a & b) | a & ! c"; + storm::property::csl::CslFilter* formula = nullptr; ASSERT_NO_THROW( - cslFormula = storm::parser::CslParser(formula); + formula = storm::parser::CslParser::parseCslFormula(input); ); - ASSERT_NE(cslFormula, nullptr); - ASSERT_EQ(cslFormula->toString(), "(!(a & b) | (a & !c))"); + // The parser did not falsely recognize the input as a comment. + ASSERT_NE(formula, nullptr); + + // The input was parsed correctly. + ASSERT_EQ("(!(a & b) | (a & !c))", formula->toString()); - delete cslFormula; + delete formula; } TEST(CslParserTest, parseProbabilisticFormulaTest) { - std::string formula = "P > 0.5 [ F a ]"; - storm::property::csl::AbstractCslFormula* cslFormula = nullptr; + std::string input = "P > 0.5 [ F a ]"; + storm::property::csl::CslFilter* formula = nullptr; ASSERT_NO_THROW( - cslFormula = storm::parser::CslParser(formula); + formula = storm::parser::CslParser::parseCslFormula(input); ); - ASSERT_NE(cslFormula, nullptr); + // The parser did not falsely recognize the input as a comment. + ASSERT_NE(formula, nullptr); - storm::property::csl::ProbabilisticBoundOperator* op = static_cast*>(cslFormula); + ASSERT_NE(dynamic_cast*>(formula->getChild()), nullptr); + storm::property::csl::ProbabilisticBoundOperator* op = static_cast*>(formula->getChild()); ASSERT_EQ(storm::property::GREATER, op->getComparisonOperator()); ASSERT_EQ(0.5, op->getBound()); - ASSERT_EQ(cslFormula->toString(), "P > 0.500000 [F a]"); + // Test the string representation for the parsed formula. + ASSERT_EQ("P > 0.500000 [F a]", formula->toString()); - delete cslFormula; + delete formula; } TEST(CslParserTest, parseSteadyStateBoundFormulaTest) { - std::string formula = "S >= 15 [ P < 0.2 [ a U<=3 b ] ]"; - storm::property::csl::AbstractCslFormula* cslFormula = nullptr; + std::string input = "S >= 15 [ P < 0.2 [ a U<=3 b ] ]"; + storm::property::csl::CslFilter* formula = nullptr; ASSERT_NO_THROW( - cslFormula = storm::parser::CslParser(formula); + formula = storm::parser::CslParser::parseCslFormula(input); ); - ASSERT_NE(cslFormula, nullptr); + // The parser did not falsely recognize the input as a comment. + ASSERT_NE(formula, nullptr); - storm::property::csl::SteadyStateBoundOperator* op = static_cast*>(cslFormula); + storm::property::csl::SteadyStateBoundOperator* op = static_cast*>(formula->getChild()); ASSERT_EQ(storm::property::GREATER_EQUAL, op->getComparisonOperator()); ASSERT_EQ(15.0, op->getBound()); - ASSERT_EQ(cslFormula->toString(), "S >= 15.000000 [P < 0.200000 [a U[0.000000,3.000000] b]]"); + // Test the string representation for the parsed formula. + ASSERT_EQ("S >= 15.000000 [P < 0.200000 [a U[0.000000,3.000000] b]]", formula->toString()); - delete cslFormula; + delete formula; } TEST(CslParserTest, parseSteadyStateNoBoundFormulaTest) { - std::string formula = "S = ? [ P <= 0.5 [ F<=3 a ] ]"; - storm::property::csl::AbstractCslFormula* cslFormula = nullptr; + std::string input = "S = ? [ P <= 0.5 [ F<=3 a ] ]"; + storm::property::csl::CslFilter* formula = nullptr; ASSERT_NO_THROW( - cslFormula = storm::parser::CslParser(formula); + formula = storm::parser::CslParser::parseCslFormula(input); ); - ASSERT_NE(cslFormula, nullptr); - ASSERT_EQ(cslFormula->toString(), "S = ? [P <= 0.500000 [F[0.000000,3.000000] a]]"); + // The parser did not falsely recognize the input as a comment. + ASSERT_NE(formula, nullptr); + + // The input was parsed correctly. + ASSERT_EQ("S = ? [P <= 0.500000 [F[0.000000,3.000000] a]]", formula->toString()); - delete cslFormula; + delete formula; } TEST(CslParserTest, parseProbabilisticNoBoundFormulaTest) { - std::string formula = "P = ? [ a U [3,4] b & (!c) ]"; - storm::property::csl::AbstractCslFormula* cslFormula = nullptr; + std::string input = "P = ? [ a U [3,4] b & (!c) ]"; + storm::property::csl::CslFilter* formula = nullptr; ASSERT_NO_THROW( - cslFormula = storm::parser::CslParser(formula); + formula = storm::parser::CslParser::parseCslFormula(input); ); - ASSERT_NE(cslFormula, nullptr); - ASSERT_EQ(cslFormula->toString(), "P = ? [a U[3.000000,4.000000] (b & !c)]"); + // The parser did not falsely recognize the input as a comment. + ASSERT_NE(formula, nullptr); - delete cslFormula; + // The input was parsed correctly. + ASSERT_EQ("P = ? [a U[3.000000,4.000000] (b & !c)]", formula->toString()); + + delete formula; } TEST(CslParserTest, parseComplexFormulaTest) { - std::string formula = "S<=0.5 [ P <= 0.5 [ a U c ] ] & (P > 0.5 [ G b] | !P < 0.4 [ G P>0.9 [F >=7 a & b] ]) //and a comment"; - storm::property::csl::AbstractCslFormula* cslFormula = nullptr; + std::string input = "S<=0.5 [ P <= 0.5 [ a U c ] ] & (P > 0.5 [ G b] | !P < 0.4 [ G P>0.9 [F >=7 a & b] ]) //and a comment"; + storm::property::csl::CslFilter* formula = nullptr; ASSERT_NO_THROW( - cslFormula = storm::parser::CslParser(formula); + formula = storm::parser::CslParser::parseCslFormula(input); ); - ASSERT_NE(cslFormula, nullptr); - ASSERT_EQ(cslFormula->toString(), "(S <= 0.500000 [P <= 0.500000 [a U c]] & (P > 0.500000 [G b] | !P < 0.400000 [G P > 0.900000 [F>=7.000000 (a & b)]]))"); + // The parser did not falsely recognize the input as a comment. + ASSERT_NE(formula, nullptr); + + // The input was parsed correctly. + ASSERT_EQ("(S <= 0.500000 [P <= 0.500000 [a U c]] & (P > 0.500000 [G b] | !P < 0.400000 [G P > 0.900000 [F>=7.000000 (a & b)]]))", formula->toString()); - delete cslFormula; + delete formula; } TEST(CslParserTest, wrongProbabilisticFormulaTest) { - std::string formula = "P > 0.5 [ a ]"; - storm::property::csl::AbstractCslFormula* cslFormula = nullptr; + std::string input = "P > 0.5 [ a ]"; + storm::property::csl::CslFilter* formula = nullptr; ASSERT_THROW( - cslFormula = storm::parser::CslParser(formula), + formula = storm::parser::CslParser::parseCslFormula(input), storm::exceptions::WrongFormatException ); + delete formula; } TEST(CslParserTest, wrongFormulaTest) { - std::string formula = "(a | b) & +"; - storm::property::csl::AbstractCslFormula* cslFormula = nullptr; + std::string input = "(a | b) & +"; + storm::property::csl::CslFilter* formula = nullptr; ASSERT_THROW( - cslFormula = storm::parser::CslParser(formula), + formula = storm::parser::CslParser::parseCslFormula(input), storm::exceptions::WrongFormatException ); + delete formula; } TEST(CslParserTest, wrongFormulaTest2) { - std::string formula = "P>0 [ F & a ]"; - storm::property::csl::AbstractCslFormula* cslFormula = nullptr; + std::string input = "P>0 [ F & a ]"; + storm::property::csl::CslFilter* formula = nullptr; ASSERT_THROW( - cslFormula = storm::parser::CslParser(formula), + formula = storm::parser::CslParser::parseCslFormula(input), storm::exceptions::WrongFormatException ); + delete formula; } diff --git a/test/functional/parser/PrctlParserTest.cpp b/test/functional/parser/PrctlParserTest.cpp index c51cf3164..5db06c465 100644 --- a/test/functional/parser/PrctlParserTest.cpp +++ b/test/functional/parser/PrctlParserTest.cpp @@ -12,149 +12,158 @@ #include "src/exceptions/WrongFormatException.h" TEST(PrctlParserTest, parseApOnlyTest) { - std::string ap = "ap"; - storm::parser::PrctlParser* prctlParser = nullptr; + std::string input = "ap"; + storm::property::prctl::PrctlFilter* formula = nullptr; ASSERT_NO_THROW( - prctlParser = new storm::parser::PrctlParser(ap); + formula = storm::parser::PrctlParser::parsePrctlFormula(input) ); - ASSERT_NE(prctlParser->getFormula(), nullptr); + // The parser did not falsely recognize the input as a comment. + ASSERT_NE(formula, nullptr); + // The input was parsed correctly. + ASSERT_EQ(input, formula->toString()); - ASSERT_EQ(ap, prctlParser->getFormula()->toString()); - - delete prctlParser->getFormula(); - delete prctlParser; + delete formula; } TEST(PrctlParserTest, parsePropositionalFormulaTest) { - storm::parser::PrctlParser* prctlParser = nullptr; + std::string input = "!(a & b) | a & ! c"; + storm::property::prctl::PrctlFilter* formula = nullptr; ASSERT_NO_THROW( - prctlParser = new storm::parser::PrctlParser("!(a & b) | a & ! c") + formula = storm::parser::PrctlParser::parsePrctlFormula(input) ); - ASSERT_NE(prctlParser->getFormula(), nullptr); - + // The parser did not falsely recognize the input as a comment. + ASSERT_NE(formula, nullptr); - ASSERT_EQ(prctlParser->getFormula()->toString(), "(!(a & b) | (a & !c))"); + // The input was parsed correctly. + ASSERT_EQ("(!(a & b) | (a & !c))", formula->toString()); - delete prctlParser->getFormula(); - delete prctlParser; + delete formula; } TEST(PrctlParserTest, parseProbabilisticFormulaTest) { - storm::parser::PrctlParser* prctlParser = nullptr; + std::string input = "P > 0.5 [ F a ]"; + storm::property::prctl::PrctlFilter* formula = nullptr; ASSERT_NO_THROW( - prctlParser = new storm::parser::PrctlParser("P > 0.5 [ F a ]") + formula = storm::parser::PrctlParser::parsePrctlFormula(input) ); - ASSERT_NE(prctlParser->getFormula(), nullptr); + // The parser did not falsely recognize the input as a comment. + ASSERT_NE(formula, nullptr); - storm::property::prctl::ProbabilisticBoundOperator* op = static_cast*>(prctlParser->getFormula()); + + ASSERT_NE(dynamic_cast*>(formula->getChild()), nullptr); + storm::property::prctl::ProbabilisticBoundOperator* op = static_cast*>(formula->getChild()); ASSERT_EQ(storm::property::GREATER, op->getComparisonOperator()); ASSERT_EQ(0.5, op->getBound()); - ASSERT_EQ(prctlParser->getFormula()->toString(), "P > 0.500000 [F a]"); + // Test the string representation for the parsed formula. + ASSERT_EQ("P > 0.500000 [F a]", formula->toString()); - delete prctlParser->getFormula(); - delete prctlParser; + delete formula; } TEST(PrctlParserTest, parseRewardFormulaTest) { - storm::parser::PrctlParser* prctlParser = nullptr; + std::string input = "R >= 15 [ I=5 ]"; + storm::property::prctl::PrctlFilter* formula = nullptr; ASSERT_NO_THROW( - prctlParser = new storm::parser::PrctlParser("R >= 15 [ I=5 ]") + formula = storm::parser::PrctlParser::parsePrctlFormula(input); ); - ASSERT_NE(prctlParser->getFormula(), nullptr); + // The parser did not falsely recognize the input as a comment. + ASSERT_NE(formula, nullptr); - storm::property::prctl::RewardBoundOperator* op = static_cast*>(prctlParser->getFormula()); + ASSERT_NE(dynamic_cast*>(formula->getChild()), nullptr); + storm::property::prctl::RewardBoundOperator* op = static_cast*>(formula->getChild()); ASSERT_EQ(storm::property::GREATER_EQUAL, op->getComparisonOperator()); ASSERT_EQ(15.0, op->getBound()); - ASSERT_EQ("R >= 15.000000 [I=5]", prctlParser->getFormula()->toString()); + // Test the string representation for the parsed formula. + ASSERT_EQ("R >= 15.000000 [I=5]", formula->toString()); - delete prctlParser->getFormula(); - delete prctlParser; + delete formula; } TEST(PrctlParserTest, parseRewardNoBoundFormulaTest) { - storm::parser::PrctlParser* prctlParser = nullptr; + std::string input = "R = ? [ F a ]"; + storm::property::prctl::PrctlFilter* formula = nullptr; ASSERT_NO_THROW( - prctlParser = new storm::parser::PrctlParser("R = ? [ F a ]") + formula = storm::parser::PrctlParser::parsePrctlFormula(input) ); - ASSERT_NE(prctlParser->getFormula(), nullptr); - + // The parser did not falsely recognize the input as a comment. + ASSERT_NE(formula, nullptr); - ASSERT_EQ(prctlParser->getFormula()->toString(), "R = ? [F a]"); - - delete prctlParser->getFormula(); - delete prctlParser; + // The input was parsed correctly. + ASSERT_EQ("R = ? [F a]", formula->toString()); + delete formula; } TEST(PrctlParserTest, parseProbabilisticNoBoundFormulaTest) { - storm::parser::PrctlParser* prctlParser = nullptr; + std::string input = "P = ? [ a U <= 4 b & (!c) ]"; + storm::property::prctl::PrctlFilter* formula = nullptr; ASSERT_NO_THROW( - prctlParser = new storm::parser::PrctlParser("P = ? [ a U <= 4 b & (!c) ]") + formula = storm::parser::PrctlParser::parsePrctlFormula(input) ); - ASSERT_NE(prctlParser->getFormula(), nullptr); - + // The parser did not falsely recognize the input as a comment. + ASSERT_NE(formula, nullptr); - ASSERT_EQ(prctlParser->getFormula()->toString(), "P = ? [a U<=4 (b & !c)]"); - - delete prctlParser->getFormula(); - delete prctlParser; + // The input was parsed correctly. + ASSERT_EQ("P = ? [a U<=4 (b & !c)]", formula->toString()); + delete formula; } TEST(PrctlParserTest, parseComplexFormulaTest) { - storm::parser::PrctlParser* prctlParser = nullptr; + std::string input = "R<=0.5 [ S ] & (R > 15 [ C<=0.5 ] | !P < 0.4 [ G P>0.9 [F<=7 a & b] ])"; + storm::property::prctl::PrctlFilter* formula = nullptr; ASSERT_NO_THROW( - prctlParser = new storm::parser::PrctlParser("R<=0.5 [ S ] & (R > 15 [ C<=0.5 ] | !P < 0.4 [ G P>0.9 [F<=7 a & b] ])") + formula = storm::parser::PrctlParser::parsePrctlFormula(input) ); - ASSERT_NE(prctlParser->getFormula(), nullptr); - + // The parser did not falsely recognize the input as a comment. + ASSERT_NE(formula, nullptr); - ASSERT_EQ("(R <= 0.500000 [S] & (R > 15.000000 [C <= 0.500000] | !P < 0.400000 [G P > 0.900000 [F<=7 (a & b)]]))", prctlParser->getFormula()->toString()); - delete prctlParser->getFormula(); - delete prctlParser; + // The input was parsed correctly. + ASSERT_EQ("(R <= 0.500000 [S] & (R > 15.000000 [C <= 0.500000] | !P < 0.400000 [G P > 0.900000 [F<=7 (a & b)]]))", formula->toString()); + delete formula; } TEST(PrctlParserTest, wrongProbabilisticFormulaTest) { - storm::parser::PrctlParser* prctlParser = nullptr; + storm::property::prctl::PrctlFilter* formula = nullptr; ASSERT_THROW( - prctlParser = new storm::parser::PrctlParser("P > 0.5 [ a ]"), + formula = storm::parser::PrctlParser::parsePrctlFormula("P > 0.5 [ a ]"), storm::exceptions::WrongFormatException ); - delete prctlParser; + delete formula; } TEST(PrctlParserTest, wrongFormulaTest) { - storm::parser::PrctlParser* prctlParser = nullptr; + storm::property::prctl::PrctlFilter* formula = nullptr; ASSERT_THROW( - prctlParser = new storm::parser::PrctlParser("(a | b) & +"), + formula = storm::parser::PrctlParser::parsePrctlFormula("(a | b) & +"), storm::exceptions::WrongFormatException ); - delete prctlParser; + delete formula; } TEST(PrctlParserTest, wrongFormulaTest2) { - storm::parser::PrctlParser* prctlParser = nullptr; + storm::property::prctl::PrctlFilter* formula = nullptr; ASSERT_THROW( - prctlParser = new storm::parser::PrctlParser("P>0 [ F & a ]"), + formula = storm::parser::PrctlParser::parsePrctlFormula("P>0 [ F & a ]"), storm::exceptions::WrongFormatException ); - delete prctlParser; + delete formula; } diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp index 809f602fb..3e2b3c347 100644 --- a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp @@ -16,46 +16,43 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { std::shared_ptr> dtmc = abstractModel->as>(); - ASSERT_EQ(dtmc->getNumberOfStates(), 2036647ull); - ASSERT_EQ(dtmc->getNumberOfTransitions(), 8973900ull); + ASSERT_EQ(2036647ull, dtmc->getNumberOfStates()); + ASSERT_EQ(8973900ull, dtmc->getNumberOfTransitions()); storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver()); storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("observe0Greater1"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); LOG4CPLUS_WARN(logger, "Model Checking P=? [F observe0Greater1] on crowds/crowds20_5..."); - std::vector result = probFormula->check(mc); + std::vector result = eventuallyFormula->check(mc, false); LOG4CPLUS_WARN(logger, "Done."); ASSERT_LT(std::abs(result[0] - 0.2296800237), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete probFormula; + delete eventuallyFormula; apFormula = new storm::property::prctl::Ap("observeIGreater1"); eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); LOG4CPLUS_WARN(logger, "Model Checking P=? [F observeIGreater1] on crowds/crowds20_5..."); - result = probFormula->check(mc); + result = eventuallyFormula->check(mc, false); LOG4CPLUS_WARN(logger, "Done."); ASSERT_LT(std::abs(result[0] - 0.05073232193), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete probFormula; + delete eventuallyFormula; apFormula = new storm::property::prctl::Ap("observeOnlyTrueSender"); eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); LOG4CPLUS_WARN(logger, "Model Checking P=? [F observeOnlyTrueSender] on crowds/crowds20_5..."); - result = probFormula->check(mc); + result = eventuallyFormula->check(mc, false); LOG4CPLUS_WARN(logger, "Done."); ASSERT_LT(std::abs(result[0] - 0.22742171078), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete probFormula; + delete eventuallyFormula; } @@ -67,47 +64,43 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { ASSERT_EQ(abstractModel->getType(), storm::models::DTMC); - std::shared_ptr> dtmc = abstractModel->as>(); - ASSERT_EQ(dtmc->getNumberOfStates(), 1312334ull); - ASSERT_EQ(dtmc->getNumberOfTransitions(), 2886810ull); + ASSERT_EQ(1312334ull, dtmc->getNumberOfStates()); + ASSERT_EQ(2886810ull, dtmc->getNumberOfTransitions()); storm::modelchecker::prctl::SparseDtmcPrctlModelChecker mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver()); storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("elected"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); LOG4CPLUS_WARN(logger, "Model Checking P=? [F elected] on synchronous_leader/leader6_8..."); - std::vector result = probFormula->check(mc); + std::vector result = eventuallyFormula->check(mc, false); LOG4CPLUS_WARN(logger, "Done."); ASSERT_LT(std::abs(result[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete probFormula; + delete eventuallyFormula; apFormula = new storm::property::prctl::Ap("elected"); storm::property::prctl::BoundedUntil* boundedUntilFormula = new storm::property::prctl::BoundedUntil(new storm::property::prctl::Ap("true"), apFormula, 20); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedUntilFormula); LOG4CPLUS_WARN(logger, "Model Checking P=? [F<=20 elected] on synchronous_leader/leader6_8..."); - result = probFormula->check(mc); + result = boundedUntilFormula->check(mc, false); LOG4CPLUS_WARN(logger, "Done."); ASSERT_LT(std::abs(result[0] - 0.9993949793), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete probFormula; + delete boundedUntilFormula; apFormula = new storm::property::prctl::Ap("elected"); storm::property::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); - storm::property::prctl::RewardNoBoundOperator* rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula); LOG4CPLUS_WARN(logger, "Model Checking R=? [F elected] on synchronous_leader/leader6_8..."); - result = rewardFormula->check(mc); + result = reachabilityRewardFormula->check(mc, false); LOG4CPLUS_WARN(logger, "Done."); ASSERT_LT(std::abs(result[0] - 1.025106273), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete rewardFormula; + delete reachabilityRewardFormula; } diff --git a/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp index 8f083f89f..98db638df 100644 --- a/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp @@ -14,64 +14,49 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { std::shared_ptr> mdp = abstractModel->as>(); - ASSERT_EQ(mdp->getNumberOfStates(), 2095783ull); - ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385ull); + ASSERT_EQ(2095783ull, mdp->getNumberOfStates()); + ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions()); storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, std::shared_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver())); storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("elected"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); - std::vector result = mc.checkNoBoundOperator(*probFormula); + std::vector result = mc.checkMinMaxOperator(*eventuallyFormula, true); ASSERT_LT(std::abs(result[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete probFormula; - apFormula = new storm::property::prctl::Ap("elected"); - eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); - - result = mc.checkNoBoundOperator(*probFormula); + result = mc.checkMinMaxOperator(*eventuallyFormula, false); ASSERT_LT(std::abs(result[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete probFormula; + + delete eventuallyFormula; apFormula = new storm::property::prctl::Ap("elected"); storm::property::prctl::BoundedEventually* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 25); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, true); - result = mc.checkNoBoundOperator(*probFormula); + result = mc.checkMinMaxOperator(*boundedEventuallyFormula, true); ASSERT_LT(std::abs(result[0] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete probFormula; - apFormula = new storm::property::prctl::Ap("elected"); - boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 25); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, false); - - result = mc.checkNoBoundOperator(*probFormula); + result = mc.checkMinMaxOperator(*boundedEventuallyFormula, false); ASSERT_LT(std::abs(result[0] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete probFormula; + + delete boundedEventuallyFormula; apFormula = new storm::property::prctl::Ap("elected"); storm::property::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); - storm::property::prctl::RewardNoBoundOperator* rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); - result = mc.checkNoBoundOperator(*rewardFormula); + result = mc.checkMinMaxOperator(*reachabilityRewardFormula, true); ASSERT_LT(std::abs(result[0] - 6.172433512), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete rewardFormula; - apFormula = new storm::property::prctl::Ap("elected"); - reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); - rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); - - result = mc.checkNoBoundOperator(*rewardFormula); + result = mc.checkMinMaxOperator(*reachabilityRewardFormula, false); ASSERT_LT(std::abs(result[0] - 6.1724344), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete rewardFormula; + + delete reachabilityRewardFormula; } TEST(SparseMdpPrctlModelCheckerTest, Consensus) { @@ -85,87 +70,77 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) { std::shared_ptr> mdp = abstractModel->as>(); - ASSERT_EQ(mdp->getNumberOfStates(), 63616ull); - ASSERT_EQ(mdp->getNumberOfTransitions(), 213472ull); + ASSERT_EQ(63616ull, mdp->getNumberOfStates()); + ASSERT_EQ(213472ull, mdp->getNumberOfTransitions()); storm::modelchecker::prctl::SparseMdpPrctlModelChecker mc(*mdp, std::shared_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver())); storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("finished"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); - storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); - std::vector result = mc.checkNoBoundOperator(*probFormula); + std::vector result = mc.checkMinMaxOperator(*eventuallyFormula, true); ASSERT_LT(std::abs(result[31168] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete probFormula; + delete eventuallyFormula; + apFormula = new storm::property::prctl::Ap("finished"); storm::property::prctl::Ap* apFormula2 = new storm::property::prctl::Ap("all_coins_equal_0"); storm::property::prctl::And* andFormula = new storm::property::prctl::And(apFormula, apFormula2); eventuallyFormula = new storm::property::prctl::Eventually(andFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); - result = mc.checkNoBoundOperator(*probFormula); + result = mc.checkMinMaxOperator(*eventuallyFormula, true); ASSERT_LT(std::abs(result[31168] - 0.4374282832), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete probFormula; + + delete eventuallyFormula; apFormula = new storm::property::prctl::Ap("finished"); apFormula2 = new storm::property::prctl::Ap("all_coins_equal_1"); andFormula = new storm::property::prctl::And(apFormula, apFormula2); eventuallyFormula = new storm::property::prctl::Eventually(andFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); - result = mc.checkNoBoundOperator(*probFormula); + result = mc.checkMinMaxOperator(*eventuallyFormula, false); ASSERT_LT(std::abs(result[31168] - 0.5293286369), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete probFormula; + delete eventuallyFormula; + apFormula = new storm::property::prctl::Ap("finished"); apFormula2 = new storm::property::prctl::Ap("agree"); storm::property::prctl::Not* notFormula = new storm::property::prctl::Not(apFormula2); andFormula = new storm::property::prctl::And(apFormula, notFormula); eventuallyFormula = new storm::property::prctl::Eventually(andFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); - result = mc.checkNoBoundOperator(*probFormula); + result = mc.checkMinMaxOperator(*eventuallyFormula, false); ASSERT_LT(std::abs(result[31168] - 0.10414097), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete probFormula; + delete eventuallyFormula; + apFormula = new storm::property::prctl::Ap("finished"); storm::property::prctl::BoundedEventually* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 50ull); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, true); - result = mc.checkNoBoundOperator(*probFormula); + result = mc.checkMinMaxOperator(*boundedEventuallyFormula, true); ASSERT_LT(std::abs(result[31168] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete probFormula; - - apFormula = new storm::property::prctl::Ap("finished"); - boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 50ull); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, false); - - result = mc.checkNoBoundOperator(*probFormula); + result = mc.checkMinMaxOperator(*boundedEventuallyFormula, false); + ASSERT_LT(std::abs(result[31168] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete probFormula; + + delete boundedEventuallyFormula; apFormula = new storm::property::prctl::Ap("finished"); storm::property::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); - storm::property::prctl::RewardNoBoundOperator* rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); - result = mc.checkNoBoundOperator(*rewardFormula); + result = mc.checkMinMaxOperator(*reachabilityRewardFormula, true); ASSERT_LT(std::abs(result[31168] - 1725.593313), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete rewardFormula; - - apFormula = new storm::property::prctl::Ap("finished"); - reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); - rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); - - result = mc.checkNoBoundOperator(*rewardFormula); - + + result = mc.checkMinMaxOperator(*reachabilityRewardFormula, false); + ASSERT_LT(std::abs(result[31168] - 2183.142422), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - delete rewardFormula; + + delete reachabilityRewardFormula; }