From f9f5a4e206f721f9ebb1aeba8f6c824035f10a4e Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 25 Aug 2015 10:53:08 +0200 Subject: [PATCH] reincluded tbb in gmm. fixed missing header. extended formula parser to return multiple formulas Former-commit-id: a2849d65344cf8e05c14845f29fab7c78ffb7f0a --- .../3rdparty/gmm-5.0/include/gmm/gmm_blas.h | 87 ++++++++++++++++++- src/models/sparse/Dtmc.cpp | 8 +- src/parser/FormulaParser.cpp | 36 +++++++- src/parser/FormulaParser.h | 24 ++++- src/utility/ConstantsComparator.h | 32 ------- src/utility/cli.cpp | 4 +- src/utility/constants.cpp | 8 ++ .../GmmxxCtmcCslModelCheckerTest.cpp | 46 +++++----- .../GmmxxDtmcPrctlModelCheckerTest.cpp | 38 ++++---- .../GmmxxHybridCtmcCslModelCheckerTest.cpp | 46 +++++----- .../GmmxxHybridDtmcPrctlModelCheckerTest.cpp | 26 +++--- .../GmmxxHybridMdpPrctlModelCheckerTest.cpp | 32 +++---- .../GmmxxMdpPrctlModelCheckerTest.cpp | 40 ++++----- .../NativeCtmcCslModelCheckerTest.cpp | 38 ++++---- .../NativeDtmcPrctlModelCheckerTest.cpp | 38 ++++---- .../NativeHybridCtmcCslModelCheckerTest.cpp | 38 ++++---- .../NativeHybridDtmcPrctlModelCheckerTest.cpp | 26 +++--- .../NativeHybridMdpPrctlModelCheckerTest.cpp | 32 +++---- .../NativeMdpPrctlModelCheckerTest.cpp | 80 ++++++++--------- .../SparseDtmcEliminationModelCheckerTest.cpp | 28 +++--- .../SymbolicDtmcPrctlModelCheckerTest.cpp | 26 +++--- .../SymbolicMdpPrctlModelCheckerTest.cpp | 32 +++---- ...ValueIterationMdpPrctlModelCheckerTest.cpp | 40 ++++----- test/functional/parser/FormulaParserTest.cpp | 52 +++++------ 24 files changed, 479 insertions(+), 378 deletions(-) diff --git a/resources/3rdparty/gmm-5.0/include/gmm/gmm_blas.h b/resources/3rdparty/gmm-5.0/include/gmm/gmm_blas.h index e8008ac05..2c9069c5b 100644 --- a/resources/3rdparty/gmm-5.0/include/gmm/gmm_blas.h +++ b/resources/3rdparty/gmm-5.0/include/gmm/gmm_blas.h @@ -38,6 +38,16 @@ #ifndef GMM_BLAS_H__ #define GMM_BLAS_H__ +// This Version of GMM was modified for StoRM. +// To detect whether the usage of TBB is possible, this include is neccessary +#include "storm-config.h" + +#ifdef STORM_HAVE_INTELTBB +# include // This fixes a potential dependency ordering problem between GMM and TBB +# include "tbb/tbb.h" +# include +#endif + #include "gmm_scaled.h" #include "gmm_transposed.h" #include "gmm_conjugated.h" @@ -1680,16 +1690,85 @@ namespace gmm { if (aux != T(0)) l3[i] = aux; } } + +#ifdef STORM_HAVE_INTELTBB + /* Official Intel Hint on blocked_range vs. linear iterators: http://software.intel.com/en-us/forums/topic/289505 + + */ + template + class forward_range_mult { + IT1 my_begin; + IT1 my_end; + IT2 my_begin_row; + size_t my_size; + public: + IT1 begin() const {return my_begin;} + IT2 begin_row() const {return my_begin_row;} + IT1 end() const {return my_end;} + bool empty() const {return my_begin==my_end;} + bool is_divisible() const {return my_size>1;} + forward_range_mult( IT1 first, IT1 last, IT2 row_first, size_t size ) : my_begin(first), my_end(last), my_begin_row(row_first), my_size(size) { + assert( size==size_t(std::distance( first,last ))); + } + forward_range_mult( IT1 first, IT1 last, IT2 row_first) : my_begin(first), my_end(last), my_begin_row(row_first) { + my_size = std::distance( first,last ); + } + forward_range_mult( forward_range_mult& r, tbb::split ) { + size_t h = r.my_size/2; + my_end = r.my_end; + my_begin = r.my_begin; + my_begin_row = r.my_begin_row; + std::advance( my_begin, h ); // Might be scaling issue + std::advance( my_begin_row, h ); + my_size = r.my_size-h; + r.my_end = my_begin; + r.my_size = h; + } + }; + + + template + class tbbHelper_mult_by_row { + L2 const* my_l2; + + // Typedefs for Iterator Types + typedef typename linalg_traits::iterator frm_IT1; + typedef typename linalg_traits::const_row_iterator frm_IT2; + + public: + void operator()( const forward_range_mult& r ) const { + L2 const& l2 = *my_l2; + + frm_IT1 it = r.begin(); + frm_IT1 ite = r.end(); + frm_IT2 itr = r.begin_row(); + + for (; it != ite; ++it, ++itr) { + *it = vect_sp(linalg_traits::row(itr), l2, + typename linalg_traits::storage_type(), + typename linalg_traits::storage_type()); + } + } + + tbbHelper_mult_by_row(L2 const* l2) : + my_l2(l2) + {} + }; +#endif template void mult_by_row(const L1& l1, const L2& l2, L3& l3, abstract_dense) { typename linalg_traits::iterator it=vect_begin(l3), ite=vect_end(l3); typename linalg_traits::const_row_iterator itr = mat_row_const_begin(l1); - for (; it != ite; ++it, ++itr) - *it = vect_sp(linalg_traits::row(itr), l2, - typename linalg_traits::storage_type(), - typename linalg_traits::storage_type()); +#ifdef STORM_HAVE_INTELTBB + tbb::parallel_for(forward_range_mult::iterator, typename linalg_traits::const_row_iterator>(it, ite, itr), tbbHelper_mult_by_row(&l2)); +#else + for (; it != ite; ++it, ++itr) + *it = vect_sp(linalg_traits::row(itr), l2, + typename linalg_traits::storage_type(), + typename linalg_traits::storage_type()); +#endif } template diff --git a/src/models/sparse/Dtmc.cpp b/src/models/sparse/Dtmc.cpp index c4853496a..9cc968136 100644 --- a/src/models/sparse/Dtmc.cpp +++ b/src/models/sparse/Dtmc.cpp @@ -3,6 +3,7 @@ #include "src/adapters/CarlAdapter.h" #include "src/exceptions/NotImplementedException.h" #include "src/exceptions/InvalidArgumentException.h" +#include "src/utility/constants.h" namespace storm { namespace models { @@ -196,19 +197,18 @@ namespace storm { template void Dtmc::ConstraintCollector::process(storm::models::sparse::Dtmc const& dtmc) { - storm::utility::ConstantsComparator comparator; for(uint_fast64_t state = 0; state < dtmc.getNumberOfStates(); ++state) { ValueType sum = storm::utility::zero(); for (auto const& transition : dtmc.getRows(state)) { sum += transition.getValue(); - if (!comparator.isConstant(transition.getValue())) { + if (!storm::utility::isConstant(transition.getValue())) { wellformedConstraintSet.emplace(transition.getValue() - 1, storm::CompareRelation::LEQ); wellformedConstraintSet.emplace(transition.getValue(), storm::CompareRelation::GEQ); graphPreservingConstraintSet.emplace(transition.getValue(), storm::CompareRelation::GREATER); } } - STORM_LOG_ASSERT(!comparator.isConstant(sum) || comparator.isOne(sum), "If the sum is a constant, it must be equal to 1."); - if(!comparator.isConstant(sum)) { + STORM_LOG_ASSERT(!storm::utility::isConstant(sum) || storm::utility::isOne(sum), "If the sum is a constant, it must be equal to 1."); + if(!storm::utility::isConstant(sum)) { wellformedConstraintSet.emplace(sum - 1, storm::CompareRelation::EQ); } diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp index 862a393b6..5acbba56c 100644 --- a/src/parser/FormulaParser.cpp +++ b/src/parser/FormulaParser.cpp @@ -1,5 +1,7 @@ #include "src/parser/FormulaParser.h" +#include + // If the parser fails due to ill-formed data, this exception is thrown. #include "src/exceptions/WrongFormatException.h" @@ -98,7 +100,7 @@ namespace storm { stateFormula = (orStateFormula); stateFormula.name("state formula"); - start = qi::eps > stateFormula >> qi::skip(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps] >> qi::eoi; + start = qi::eps > (stateFormula % +(qi::char_("\n;"))) >> qi::skip(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps] >> qi::eoi; start.name("start"); /*! @@ -156,13 +158,41 @@ namespace storm { this->identifiers_.add(identifier, expression); } - std::shared_ptr FormulaParser::parseFromString(std::string const& formulaString) { + std::shared_ptr FormulaParser::parseSingleFormulaFromString(std::string const& formulaString) { + std::vector> formulas = parseFromString(formulaString); + STORM_LOG_THROW(formulas.size() == 1, storm::exceptions::WrongFormatException, "Expected exactly one formula, but found " << formulas.size() << " instead."); + return formulas.front(); + } + + std::vector> FormulaParser::parseFromFile(std::string const& filename) { + // Open file and initialize result. + std::ifstream inputFileStream(filename, std::ios::in); + STORM_LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'."); + + std::vector> formulas; + + // Now try to parse the contents of the file. + try { + std::string fileContent((std::istreambuf_iterator(inputFileStream)), (std::istreambuf_iterator())); + formulas = parseFromString(fileContent); + } catch(std::exception& e) { + // In case of an exception properly close the file before passing exception. + inputFileStream.close(); + throw e; + } + + // Close the stream in case everything went smoothly and return result. + inputFileStream.close(); + return formulas; + } + + std::vector> FormulaParser::parseFromString(std::string const& formulaString) { PositionIteratorType first(formulaString.begin()); PositionIteratorType iter = first; PositionIteratorType last(formulaString.end()); // Create empty result; - std::shared_ptr result; + std::vector> result; // Create grammar. try { diff --git a/src/parser/FormulaParser.h b/src/parser/FormulaParser.h index da10e696b..ad8ea8459 100644 --- a/src/parser/FormulaParser.h +++ b/src/parser/FormulaParser.h @@ -12,7 +12,7 @@ namespace storm { namespace parser { - class FormulaParser : public qi::grammar(), Skipper> { + class FormulaParser : public qi::grammar>(), Skipper> { public: FormulaParser(std::shared_ptr const& manager = std::shared_ptr(new storm::expressions::ExpressionManager())); @@ -20,9 +20,25 @@ namespace storm { * Parses the formula given by the provided string. * * @param formulaString The formula as a string. - * @return The resulting formula representation. + * @return The resulting formula. */ - std::shared_ptr parseFromString(std::string const& formulaString); + std::shared_ptr parseSingleFormulaFromString(std::string const& formulaString); + + /*! + * Parses the formula given by the provided string. + * + * @param formulaString The formula as a string. + * @return The contained formulas. + */ + std::vector> parseFromString(std::string const& formulaString); + + /*! + * Parses the formulas in the given file. + * + * @param filename The name of the file to parse. + * @return The contained formulas. + */ + std::vector> parseFromFile(std::string const& filename); /*! * Adds an identifier and the expression it is supposed to be replaced with. This can, for example be used @@ -118,7 +134,7 @@ namespace storm { // they are to be replaced with. qi::symbols identifiers_; - qi::rule(), Skipper> start; + qi::rule>(), Skipper> start; qi::rule, boost::optional, boost::optional>(), qi::locals, boost::optional, boost::optional>, Skipper> operatorInformation; qi::rule(), Skipper> probabilityOperator; diff --git a/src/utility/ConstantsComparator.h b/src/utility/ConstantsComparator.h index 83e92ced3..7cd03eab3 100644 --- a/src/utility/ConstantsComparator.h +++ b/src/utility/ConstantsComparator.h @@ -68,38 +68,6 @@ namespace storm { // The precision used for comparisons. double precision; }; - -#ifdef STORM_HAVE_CARL - template<> - class ConstantsComparator { - public: - ConstantsComparator(); - - bool isOne(storm::RationalFunction const& value) const; - - bool isZero(storm::RationalFunction const& value) const; - - bool isEqual(storm::RationalFunction const& value1, storm::RationalFunction const& value2) const; - - bool isConstant(storm::RationalFunction const& value) const; - }; - - template<> - class ConstantsComparator { - public: - ConstantsComparator(); - - bool isOne(storm::Polynomial const& value) const; - - bool isZero(storm::Polynomial const& value) const; - - bool isEqual(storm::Polynomial const& value1, storm::Polynomial const& value2) const; - - bool isConstant(storm::Polynomial const& value) const; - }; - -#endif - } } diff --git a/src/utility/cli.cpp b/src/utility/cli.cpp index 4b7c2b74b..93ed85ab4 100644 --- a/src/utility/cli.cpp +++ b/src/utility/cli.cpp @@ -223,10 +223,10 @@ namespace storm { std::shared_ptr formula; if (program) { storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer()); - formula = formulaParser.parseFromString(settings.getProperty()); + formula = formulaParser.parseSingleFormulaFromString(settings.getProperty()); } else { storm::parser::FormulaParser formulaParser; - formula = formulaParser.parseFromString(settings.getProperty()); + formula = formulaParser.parseSingleFormulaFromString(settings.getProperty()); } formulas.push_back(formula); } else if (settings.isPropertyFileSet()) { diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp index 1b599185d..f346d2fcc 100644 --- a/src/utility/constants.cpp +++ b/src/utility/constants.cpp @@ -203,6 +203,10 @@ namespace storm { template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); #ifdef STORM_HAVE_CARL + template bool isOne(RationalFunction const& value); + template bool isZero(RationalFunction const& value); + template bool isConstant(RationalFunction const& value); + template RationalFunction one(); template RationalFunction zero(); template storm::RationalFunction infinity(); @@ -215,6 +219,10 @@ namespace storm { template RationalFunction& simplify(RationalFunction& value); template RationalFunction&& simplify(RationalFunction&& value); + template bool isOne(Interval const& value); + template bool isZero(Interval const& value); + template bool isConstant(Interval const& value); + template Interval one(); template Interval zero(); diff --git a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp index d187945fa..420a81530 100644 --- a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp @@ -43,56 +43,56 @@ TEST(GmmxxCtmcCslModelCheckerTest, Cluster) { storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); // Start checking properties. - formula = formulaParser.parseFromString("P=? [ F<=100 !\"minimum\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=100 !\"minimum\"]"); std::unique_ptr checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ F[100,100] !\"minimum\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ F[100,100] !\"minimum\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ F[100,2000] !\"minimum\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ F[100,2000] !\"minimum\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ \"minimum\" U<=10 \"premium\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U<=10 \"premium\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeCheckResult4[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ !\"minimum\" U[1,inf] \"minimum\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"minimum\" U[1,inf] \"minimum\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0, quantitativeCheckResult5[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ \"minimum\" U[1,inf] !\"minimum\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U[1,inf] !\"minimum\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.9999999033633374, quantitativeCheckResult6[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("R=? [C<=100]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [C<=100]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult7 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.8602815057967503, quantitativeCheckResult7[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("LRA=? [\"minimum\"]"); + formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"minimum\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); @@ -126,42 +126,42 @@ TEST(GmmxxCtmcCslModelCheckerTest, Embedded) { storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); // Start checking properties. - formula = formulaParser.parseFromString("P=? [ F<=10000 \"down\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10000 \"down\"]"); std::unique_ptr checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_actuators\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_actuators\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_io\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_io\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_sensors\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_sensors\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("R=? [C<=10000]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [C<=10000]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(2.7745274082080154, quantitativeCheckResult5[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("LRA=? [\"fail_sensors\"]"); + formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"fail_sensors\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); @@ -188,14 +188,14 @@ TEST(GmmxxCtmcCslModelCheckerTest, Polling) { storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); // Start checking properties. - formula = formulaParser.parseFromString("P=?[ F<=10 \"target\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=?[ F<=10 \"target\"]"); std::unique_ptr checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeCheckResult1[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("LRA=?[\"target\"]"); + formula = formulaParser.parseSingleFormulaFromString("LRA=?[\"target\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); @@ -235,49 +235,49 @@ TEST(GmmxxCtmcCslModelCheckerTest, Tandem) { storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); // Start checking properties. - formula = formulaParser.parseFromString("P=? [ F<=10 \"network_full\" ]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"network_full\" ]"); std::unique_ptr checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ F<=10 \"first_queue_full\" ]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"first_queue_full\" ]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [\"second_queue_full\" U<=1 !\"second_queue_full\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [\"second_queue_full\" U<=1 !\"second_queue_full\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeCheckResult3[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("R=? [I=10]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [I=10]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("R=? [C<=10]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [C<=10]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("R=? [F \"first_queue_full\"&\"second_queue_full\"]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [F \"first_queue_full\"&\"second_queue_full\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(262.85103661561755, quantitativeCheckResult6[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("LRA=? [\"first_queue_full\"]"); + formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"first_queue_full\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); diff --git a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp index 224ff209c..59d19a84f 100644 --- a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp @@ -18,7 +18,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.coin_flips.trans.rew"); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); @@ -29,28 +29,28 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("P=? [F \"one\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("P=? [F \"two\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("P=? [F \"three\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("R=? [F \"done\"]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); @@ -64,7 +64,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; std::shared_ptr> dtmc = abstractModel->as>(); @@ -73,21 +73,21 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("P=? [F \"observe0Greater1\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.3328800375801578281, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("P=? [F \"observeIGreater1\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.1522194965, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("P=? [F \"observeOnlyTrueSender\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); @@ -101,7 +101,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; std::shared_ptr> dtmc = abstractModel->as>(); @@ -110,21 +110,21 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("P=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("P=? [F<=20 \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.9999965911265462636, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("R=? [F \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); @@ -137,7 +137,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) { std::shared_ptr> dtmc; // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; { matrixBuilder = storm::storage::SparseMatrixBuilder(2, 2, 2); @@ -153,7 +153,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("LRA=? [\"a\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -177,7 +177,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("LRA=? [\"a\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -201,7 +201,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("LRA=? [\"a\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -217,7 +217,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRA) { std::shared_ptr> mdp; // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; { matrixBuilder = storm::storage::SparseMatrixBuilder(15, 15, 20, true); @@ -264,7 +264,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRA) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("LRA=? [\"a\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); diff --git a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp index 5b4a12ba7..a75910a8c 100644 --- a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp @@ -45,7 +45,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) { storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); // Start checking properties. - formula = formulaParser.parseFromString("P=? [ F<=100 !\"minimum\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=100 !\"minimum\"]"); std::unique_ptr checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -54,7 +54,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) { EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ F[100,100] !\"minimum\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ F[100,100] !\"minimum\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -63,7 +63,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) { EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ F[100,2000] !\"minimum\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ F[100,2000] !\"minimum\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -72,7 +72,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) { EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ \"minimum\" U<=10 \"premium\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U<=10 \"premium\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -81,7 +81,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) { EXPECT_NEAR(1, quantitativeCheckResult4.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(1, quantitativeCheckResult4.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ !\"minimum\" U[1,inf] \"minimum\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"minimum\" U[1,inf] \"minimum\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -90,7 +90,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) { EXPECT_NEAR(0, quantitativeCheckResult5.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0, quantitativeCheckResult5.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ \"minimum\" U[1,inf] !\"minimum\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U[1,inf] !\"minimum\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -99,7 +99,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) { EXPECT_NEAR(0.9999999033633374, quantitativeCheckResult6.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.9999999033633374, quantitativeCheckResult6.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("R=? [C<=100]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [C<=100]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -108,7 +108,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) { EXPECT_NEAR(0.8602815057967503, quantitativeCheckResult7.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.8602815057967503, quantitativeCheckResult7.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("LRA=? [\"minimum\"]"); + formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"minimum\"]"); checkResult = modelchecker.check(*formula); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); @@ -142,7 +142,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded) { storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); // Start checking properties. - formula = formulaParser.parseFromString("P=? [ F<=10000 \"down\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10000 \"down\"]"); std::unique_ptr checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -151,7 +151,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded) { EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_actuators\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_actuators\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -160,7 +160,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded) { EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_io\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_io\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -169,7 +169,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded) { EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_sensors\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_sensors\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -178,7 +178,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded) { EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("R=? [C<=10000]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [C<=10000]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -187,7 +187,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded) { EXPECT_NEAR(2.7745274082080154, quantitativeCheckResult5.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(2.7745274082080154, quantitativeCheckResult5.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("LRA=? [\"fail_sensors\"]"); + formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"fail_sensors\"]"); checkResult = modelchecker.check(*formula); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); @@ -214,7 +214,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling) { storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); // Start checking properties. - formula = formulaParser.parseFromString("P=?[ F<=10 \"target\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=?[ F<=10 \"target\"]"); std::unique_ptr checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -223,7 +223,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling) { EXPECT_NEAR(1, quantitativeCheckResult1.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(1, quantitativeCheckResult1.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("LRA=? [\"target\"]"); + formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"target\"]"); checkResult = modelchecker.check(*formula); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); @@ -265,7 +265,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem) { storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); // Start checking properties. - formula = formulaParser.parseFromString("P=? [ F<=10 \"network_full\" ]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"network_full\" ]"); std::unique_ptr checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -274,7 +274,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem) { EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ F<=10 \"first_queue_full\" ]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"first_queue_full\" ]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -283,7 +283,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem) { EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [\"second_queue_full\" U<=1 !\"second_queue_full\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [\"second_queue_full\" U<=1 !\"second_queue_full\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -292,7 +292,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem) { EXPECT_NEAR(1, quantitativeCheckResult3.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(1, quantitativeCheckResult3.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("R=? [I=10]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [I=10]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -301,7 +301,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem) { EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("R=? [C<=10]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [C<=10]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -310,7 +310,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem) { EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("R=? [F \"first_queue_full\"&\"second_queue_full\"]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [F \"first_queue_full\"&\"second_queue_full\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -319,7 +319,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem) { EXPECT_NEAR(262.85103498583413, quantitativeCheckResult6.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(262.85103498583413, quantitativeCheckResult6.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("LRA=? [\"first_queue_full\"]"); + formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"first_queue_full\"]"); checkResult = modelchecker.check(*formula); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); diff --git a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp index 9cd259aa3..e9c195d80 100644 --- a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp @@ -22,7 +22,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; // Build the die model with its reward model. #ifdef WINDOWS @@ -42,7 +42,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die) { storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("P=? [F \"one\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -51,7 +51,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die) { EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("P=? [F \"two\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -60,7 +60,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die) { EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("P=? [F \"three\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -69,7 +69,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die) { EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("R=? [F \"done\"]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -83,7 +83,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program); EXPECT_EQ(8607ul, model->getNumberOfStates()); @@ -95,7 +95,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds) { storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("P=? [F \"observe0Greater1\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -104,7 +104,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds) { EXPECT_NEAR(0.3328800375801578281, quantitativeResult1.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.3328800375801578281, quantitativeResult1.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("P=? [F \"observeIGreater1\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -113,7 +113,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds) { EXPECT_NEAR(0.1522194965, quantitativeResult2.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.1522194965, quantitativeResult2.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("P=? [F \"observeOnlyTrueSender\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -127,7 +127,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; // Build the die model with its reward model. #ifdef WINDOWS @@ -147,7 +147,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader) { storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("P=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -156,7 +156,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader) { EXPECT_NEAR(1.0, quantitativeResult1.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0, quantitativeResult1.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("P=? [F<=20 \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -165,7 +165,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader) { EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("R=? [F \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); diff --git a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp index 9cffdba66..e1808f717 100644 --- a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp @@ -23,7 +23,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; // Build the die model with its reward model. #ifdef WINDOWS @@ -43,7 +43,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) { storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("Pmin=? [F \"two\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -52,7 +52,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) { EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F \"two\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -61,7 +61,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) { EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmin=? [F \"three\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -70,7 +70,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) { EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F \"three\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -79,7 +79,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) { EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmin=? [F \"four\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -88,7 +88,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) { EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F \"four\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -97,7 +97,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) { EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmin=? [F \"done\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -106,7 +106,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) { EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmax=? [F \"done\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -120,7 +120,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; // Build the die model with its reward model. #ifdef WINDOWS @@ -140,7 +140,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("Pmin=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -149,7 +149,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -158,7 +158,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmin=? [F<=25 \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -167,7 +167,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { EXPECT_NEAR(0.0625, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0625, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F<=25 \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -176,7 +176,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0625, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmin=? [F \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -185,7 +185,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { EXPECT_NEAR(4.2856896106114934, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(4.2856896106114934, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmax=? [F \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); diff --git a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index a79be23f1..c829a94b6 100644 --- a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -19,7 +19,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> 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.trans.rew"); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); @@ -30,56 +30,56 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("Pmin=? [F \"two\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0277777612209320068, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F \"two\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0277777612209320068, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmin=? [F \"three\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0555555224418640136, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F \"three\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0555555224418640136, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmin=? [F \"four\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.083333283662796020508, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F \"four\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.083333283662796020508, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmin=? [F \"done\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult7 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(7.333329499, quantitativeResult7[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmax=? [F \"done\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult8 = result->asExplicitQuantitativeCheckResult(); @@ -94,14 +94,14 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { storm::modelchecker::SparseMdpPrctlModelChecker> stateRewardModelChecker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); - formula = parser.parseFromString("Rmin=? [F \"done\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); result = stateRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult9 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(7.333329499, quantitativeResult9[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmax=? [F \"done\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); result = stateRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult10 = result->asExplicitQuantitativeCheckResult(); @@ -116,14 +116,14 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { storm::modelchecker::SparseMdpPrctlModelChecker> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); - formula = parser.parseFromString("Rmin=? [F \"done\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); result = stateAndTransitionRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult11 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(14.666658998, quantitativeResult11[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmax=? [F \"done\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); result = stateAndTransitionRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult12 = result->asExplicitQuantitativeCheckResult(); @@ -135,7 +135,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { 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"); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; ASSERT_EQ(storm::models::ModelType::Mdp, abstractModel->getType()); @@ -146,42 +146,42 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("Pmin=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmin=? [F<=25 \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0625, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F<=25 \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0625, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmin=? [F \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(4.285689611, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmax=? [F \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); diff --git a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp index 6e74645cb..c37c7b7bc 100644 --- a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp @@ -41,49 +41,49 @@ TEST(NativeCtmcCslModelCheckerTest, Cluster) { storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); // Start checking properties. - formula = formulaParser.parseFromString("P=? [ F<=100 !\"minimum\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=100 !\"minimum\"]"); std::unique_ptr checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ F[100,100] !\"minimum\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ F[100,100] !\"minimum\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ F[100,2000] !\"minimum\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ F[100,2000] !\"minimum\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ \"minimum\" U<=10 \"premium\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U<=10 \"premium\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeCheckResult4[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ !\"minimum\" U[1,inf] \"minimum\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"minimum\" U[1,inf] \"minimum\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0, quantitativeCheckResult5[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ \"minimum\" U[1,inf] !\"minimum\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U[1,inf] !\"minimum\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.9999999033633374, quantitativeCheckResult6[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("R=? [C<=100]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [C<=100]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); @@ -117,35 +117,35 @@ TEST(NativeCtmcCslModelCheckerTest, Embedded) { storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); // Start checking properties. - formula = formulaParser.parseFromString("P=? [ F<=10000 \"down\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10000 \"down\"]"); std::unique_ptr checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_actuators\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_actuators\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_io\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_io\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_sensors\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_sensors\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("R=? [C<=10000]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [C<=10000]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); @@ -172,7 +172,7 @@ TEST(NativeCtmcCslModelCheckerTest, Polling) { storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); // Start checking properties. - formula = formulaParser.parseFromString("P=?[ F<=10 \"target\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=?[ F<=10 \"target\"]"); std::unique_ptr checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); @@ -213,42 +213,42 @@ TEST(NativeCtmcCslModelCheckerTest, Tandem) { storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); // Start checking properties. - formula = formulaParser.parseFromString("P=? [ F<=10 \"network_full\" ]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"network_full\" ]"); std::unique_ptr checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ F<=10 \"first_queue_full\" ]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"first_queue_full\" ]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [\"second_queue_full\" U<=1 !\"second_queue_full\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [\"second_queue_full\" U<=1 !\"second_queue_full\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeCheckResult3[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("R=? [I=10]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [I=10]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("R=? [C<=10]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [C<=10]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5[initialState], storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("R=? [F \"first_queue_full\"&\"second_queue_full\"]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [F \"first_queue_full\"&\"second_queue_full\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); diff --git a/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp index 400e3c8a8..a2ec1d365 100644 --- a/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp @@ -20,7 +20,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, Die) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.coin_flips.trans.rew"); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); @@ -31,28 +31,28 @@ TEST(SparseDtmcPrctlModelCheckerTest, Die) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("P=? [F \"one\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("P=? [F \"two\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("P=? [F \"three\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("R=? [F \"done\"]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); @@ -66,7 +66,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, Crowds) { ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; std::shared_ptr> dtmc = abstractModel->as>(); @@ -75,21 +75,21 @@ TEST(SparseDtmcPrctlModelCheckerTest, Crowds) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("P=? [F \"observe0Greater1\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.33288205191646525, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("P=? [F \"observeIGreater1\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.15222066094730619, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("P=? [F \"observeOnlyTrueSender\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); @@ -103,7 +103,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, SynchronousLeader) { ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; std::shared_ptr> dtmc = abstractModel->as>(); @@ -112,21 +112,21 @@ TEST(SparseDtmcPrctlModelCheckerTest, SynchronousLeader) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("P=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("P=? [F<=20 \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.9999965911265462636, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("R=? [F \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); @@ -139,7 +139,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) { std::shared_ptr> dtmc; // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; { matrixBuilder = storm::storage::SparseMatrixBuilder(2, 2, 2); @@ -155,7 +155,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory(storm::solver::NativeLinearEquationSolver::SolutionMethod::SOR, 0.9))); - std::shared_ptr formula = parser.parseFromString("LRA=? [\"a\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -179,7 +179,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory(storm::solver::NativeLinearEquationSolver::SolutionMethod::SOR, 0.9))); - std::shared_ptr formula = parser.parseFromString("LRA=? [\"a\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -203,7 +203,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory(storm::solver::NativeLinearEquationSolver::SolutionMethod::SOR, 0.9))); - std::shared_ptr formula = parser.parseFromString("LRA=? [\"a\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -219,7 +219,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRA) { std::shared_ptr> mdp; // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; { matrixBuilder = storm::storage::SparseMatrixBuilder(15, 15, 20, true); @@ -266,7 +266,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRA) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory(storm::solver::NativeLinearEquationSolver::SolutionMethod::SOR, 0.9))); - std::shared_ptr formula = parser.parseFromString("LRA=? [\"a\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]"); std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); diff --git a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp index 57b557d4e..69cfe01b0 100644 --- a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp @@ -44,7 +44,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster) { storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); // Start checking properties. - formula = formulaParser.parseFromString("P=? [ F<=100 !\"minimum\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=100 !\"minimum\"]"); std::unique_ptr checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -53,7 +53,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster) { EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ F[100,100] !\"minimum\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ F[100,100] !\"minimum\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -62,7 +62,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster) { EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ F[100,2000] !\"minimum\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ F[100,2000] !\"minimum\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -71,7 +71,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster) { EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ \"minimum\" U<=10 \"premium\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U<=10 \"premium\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -80,7 +80,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster) { EXPECT_NEAR(1, quantitativeCheckResult4.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(1, quantitativeCheckResult4.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ !\"minimum\" U[1,inf] \"minimum\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"minimum\" U[1,inf] \"minimum\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -89,7 +89,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster) { EXPECT_NEAR(0, quantitativeCheckResult5.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0, quantitativeCheckResult5.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ \"minimum\" U[1,inf] !\"minimum\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U[1,inf] !\"minimum\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -98,7 +98,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster) { EXPECT_NEAR(0.9999999033633374, quantitativeCheckResult6.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.9999999033633374, quantitativeCheckResult6.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("R=? [C<=100]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [C<=100]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -133,7 +133,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded) { storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); // Start checking properties. - formula = formulaParser.parseFromString("P=? [ F<=10000 \"down\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10000 \"down\"]"); std::unique_ptr checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -142,7 +142,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded) { EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_actuators\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_actuators\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -151,7 +151,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded) { EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_io\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_io\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -160,7 +160,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded) { EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_sensors\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_sensors\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -169,7 +169,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded) { EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("R=? [C<=10000]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [C<=10000]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -197,7 +197,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling) { storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); // Start checking properties. - formula = formulaParser.parseFromString("P=?[ F<=10 \"target\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=?[ F<=10 \"target\"]"); std::unique_ptr checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -239,7 +239,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem) { storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); // Start checking properties. - formula = formulaParser.parseFromString("P=? [ F<=10 \"network_full\" ]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"network_full\" ]"); std::unique_ptr checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -248,7 +248,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem) { EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [ F<=10 \"first_queue_full\" ]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"first_queue_full\" ]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -257,7 +257,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem) { EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("P=? [\"second_queue_full\" U<=1 !\"second_queue_full\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [\"second_queue_full\" U<=1 !\"second_queue_full\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -266,7 +266,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem) { EXPECT_NEAR(1, quantitativeCheckResult3.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(1, quantitativeCheckResult3.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("R=? [I=10]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [I=10]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -275,7 +275,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem) { EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("R=? [C<=10]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [C<=10]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); @@ -284,7 +284,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem) { EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5.getMin(), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5.getMax(), storm::settings::generalSettings().getPrecision()); - formula = formulaParser.parseFromString("R=? [F \"first_queue_full\"&\"second_queue_full\"]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [F \"first_queue_full\"&\"second_queue_full\"]"); checkResult = modelchecker.check(*formula); ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); diff --git a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp index 2262f10c9..b01a87efa 100644 --- a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp @@ -23,7 +23,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; // Build the die model with its reward model. #ifdef WINDOWS @@ -43,7 +43,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die) { storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("P=? [F \"one\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -52,7 +52,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die) { EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("P=? [F \"two\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -61,7 +61,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die) { EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("P=? [F \"three\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -70,7 +70,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die) { EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("R=? [F \"done\"]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -84,7 +84,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program); EXPECT_EQ(8607ul, model->getNumberOfStates()); @@ -96,7 +96,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds) { storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("P=? [F \"observe0Greater1\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -105,7 +105,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds) { EXPECT_NEAR(0.33288205191646525, quantitativeResult1.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.33288205191646525, quantitativeResult1.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("P=? [F \"observeIGreater1\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -114,7 +114,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds) { EXPECT_NEAR(0.15222066094730619, quantitativeResult2.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.15222066094730619, quantitativeResult2.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("P=? [F \"observeOnlyTrueSender\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -128,7 +128,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; // Build the die model with its reward model. #ifdef WINDOWS @@ -148,7 +148,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader) { storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("P=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -157,7 +157,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader) { EXPECT_NEAR(1.0, quantitativeResult1.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0, quantitativeResult1.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("P=? [F<=20 \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -166,7 +166,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader) { EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("R=? [F \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); diff --git a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp index 50008a237..d0f752f0c 100644 --- a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp @@ -22,7 +22,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; // Build the die model with its reward model. #ifdef WINDOWS @@ -42,7 +42,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) { storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("Pmin=? [F \"two\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -51,7 +51,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) { EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F \"two\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -60,7 +60,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) { EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmin=? [F \"three\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -69,7 +69,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) { EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F \"three\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -78,7 +78,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) { EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmin=? [F \"four\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -87,7 +87,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) { EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F \"four\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -96,7 +96,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) { EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmin=? [F \"done\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -105,7 +105,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) { EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmax=? [F \"done\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -119,7 +119,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; // Build the die model with its reward model. #ifdef WINDOWS @@ -139,7 +139,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("Pmin=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -148,7 +148,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -157,7 +157,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmin=? [F<=25 \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -166,7 +166,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { EXPECT_NEAR(0.0625, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0625, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F<=25 \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -175,7 +175,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0625, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmin=? [F \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -184,7 +184,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { EXPECT_NEAR(4.2856896106114934, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(4.2856896106114934, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmax=? [F \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); diff --git a/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp index e47eaeeeb..14622dae2 100644 --- a/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp @@ -18,7 +18,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> 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.trans.rew"); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); @@ -29,56 +29,56 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("Pmin=? [F \"two\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0277777612209320068, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F \"two\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0277777612209320068, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmin=? [F \"three\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0555555224418640136, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F \"three\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0555555224418640136, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmin=? [F \"four\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.083333283662796020508, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F \"four\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.083333283662796020508, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmin=? [F \"done\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult7 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(7.333329499, quantitativeResult7[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmax=? [F \"done\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult8 = result->asExplicitQuantitativeCheckResult(); @@ -93,14 +93,14 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { storm::modelchecker::SparseMdpPrctlModelChecker> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); - formula = parser.parseFromString("Rmin=? [F \"done\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); result = stateRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult9 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(7.333329499, quantitativeResult9[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmax=? [F \"done\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); result = stateRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult10 = result->asExplicitQuantitativeCheckResult(); @@ -115,14 +115,14 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { storm::modelchecker::SparseMdpPrctlModelChecker> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); - formula = parser.parseFromString("Rmin=? [F \"done\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); result = stateAndTransitionRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult11 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(14.666658998, quantitativeResult11[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmax=? [F \"done\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); result = stateAndTransitionRewardModelChecker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult12 = result->asExplicitQuantitativeCheckResult(); @@ -134,7 +134,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { 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"); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; ASSERT_EQ(storm::models::ModelType::Mdp, abstractModel->getType()); @@ -145,42 +145,42 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("Pmin=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmin=? [F<=25 \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0625, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F<=25 \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0625, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmin=? [F \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(4.285689611, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmax=? [F \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); @@ -193,7 +193,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) { std::shared_ptr> mdp; // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; { matrixBuilder = storm::storage::SparseMatrixBuilder(2, 2, 2); @@ -209,7 +209,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("LRAmax=? [\"a\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -217,7 +217,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) { EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(.5, quantitativeResult1[1], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("LRAmin=? [\"a\"]"); + formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]"); result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); @@ -241,7 +241,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("LRAmax=? [\"a\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -249,7 +249,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) { EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(.5, quantitativeResult1[1], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("LRAmin=? [\"a\"]"); + formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]"); result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); @@ -282,7 +282,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("LRAmax=? [\"a\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -291,7 +291,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) { EXPECT_NEAR(1. / 3., quantitativeResult1[1], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1. / 3., quantitativeResult1[2], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("LRAmin=? [\"a\"]"); + formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]"); result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); @@ -300,7 +300,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) { EXPECT_NEAR(0.0, quantitativeResult2[1], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0, quantitativeResult2[2], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("LRAmax=? [\"b\"]"); + formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"b\"]"); result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); @@ -309,7 +309,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) { EXPECT_NEAR(0.5, quantitativeResult3[1], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.5, quantitativeResult3[2], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("LRAmin=? [\"b\"]"); + formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"b\"]"); result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); @@ -318,7 +318,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) { EXPECT_NEAR(1. / 3., quantitativeResult4[1], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1. / 3., quantitativeResult4[2], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("LRAmax=? [\"c\"]"); + formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"c\"]"); result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); @@ -327,7 +327,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) { EXPECT_NEAR(2. / 3., quantitativeResult5[1], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(2. / 3., quantitativeResult5[2], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("LRAmin=? [\"c\"]"); + formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"c\"]"); result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); @@ -343,7 +343,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) { std::shared_ptr> mdp; // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; { matrixBuilder = storm::storage::SparseMatrixBuilder(4, 3, 4, true, true, 3); @@ -368,7 +368,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("LRAmax=? [\"a\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -377,7 +377,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) { EXPECT_NEAR(0.0, quantitativeResult1[1], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0, quantitativeResult1[2], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("LRAmin=? [\"a\"]"); + formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]"); result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); @@ -386,7 +386,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) { EXPECT_NEAR(0.0, quantitativeResult2[1], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0, quantitativeResult2[2], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("LRAmax=? [\"b\"]"); + formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"b\"]"); result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); @@ -395,7 +395,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) { EXPECT_NEAR(1.0, quantitativeResult3[1], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0, quantitativeResult3[2], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("LRAmin=? [\"b\"]"); + formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"b\"]"); result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); @@ -404,7 +404,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) { EXPECT_NEAR(0.0, quantitativeResult4[1], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0, quantitativeResult4[2], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("LRAmax=? [\"c\"]"); + formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"c\"]"); result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); @@ -413,7 +413,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) { EXPECT_NEAR(1.0, quantitativeResult5[1], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0, quantitativeResult5[2], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("LRAmin=? [\"c\"]"); + formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"c\"]"); result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); @@ -490,7 +490,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("LRAmax=? [\"a\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]"); std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); @@ -503,7 +503,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) { EXPECT_NEAR(101./200., quantitativeResult1[13], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(31./60., quantitativeResult1[14], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("LRAmin=? [\"a\"]"); + formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]"); result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); diff --git a/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp b/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp index b8647c7d4..a4389e881 100644 --- a/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp @@ -16,7 +16,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, Die) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.coin_flips.trans.rew"); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); @@ -27,28 +27,28 @@ TEST(SparseDtmcEliminationModelCheckerTest, Die) { storm::modelchecker::SparseDtmcEliminationModelChecker> checker(*dtmc); - std::shared_ptr formula = parser.parseFromString("P=? [F \"one\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult1[0], storm::settings::generalSettings().getPrecision()); - formula = parser.parseFromString("P=? [F \"two\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult2[0], storm::settings::generalSettings().getPrecision()); - formula = parser.parseFromString("P=? [F \"three\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult3[0], storm::settings::generalSettings().getPrecision()); - formula = parser.parseFromString("R=? [F \"done\"]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); @@ -60,7 +60,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, Crowds) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.lab", "", ""); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); @@ -71,35 +71,35 @@ TEST(SparseDtmcEliminationModelCheckerTest, Crowds) { storm::modelchecker::SparseDtmcEliminationModelChecker> checker(*dtmc); - std::shared_ptr formula = parser.parseFromString("P=? [F \"observe0Greater1\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.3328800375801578281, quantitativeResult1[0], storm::settings::generalSettings().getPrecision()); - formula = parser.parseFromString("P=? [F \"observeIGreater1\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.1522194965, quantitativeResult2[0], storm::settings::generalSettings().getPrecision()); - formula = parser.parseFromString("P=? [F \"observeOnlyTrueSender\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.32153724292835045, quantitativeResult3[0], storm::settings::generalSettings().getPrecision()); - formula = parser.parseFromString("P=? [F \"observe0Greater1\" || F \"observeIGreater1\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\" || F \"observeIGreater1\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.15330064292476167, quantitativeResult4[0], storm::settings::generalSettings().getPrecision()); - formula = parser.parseFromString("P=? [F \"observeOnlyTrueSender\" || F \"observe0Greater1\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\" || F \"observe0Greater1\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); @@ -111,7 +111,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, SynchronousLeader) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.pick.trans.rew"); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); std::shared_ptr> dtmc = abstractModel->as>(); @@ -121,14 +121,14 @@ TEST(SparseDtmcEliminationModelCheckerTest, SynchronousLeader) { storm::modelchecker::SparseDtmcEliminationModelChecker> checker(*dtmc); - std::shared_ptr formula = parser.parseFromString("P=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::generalSettings().getPrecision()); - formula = parser.parseFromString("R=? [F \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); diff --git a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp index 82d91fd76..487257138 100644 --- a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp @@ -21,7 +21,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; // Build the die model with its reward model. #ifdef WINDOWS @@ -41,7 +41,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die) { storm::modelchecker::SymbolicDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("P=? [F \"one\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -50,7 +50,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die) { EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("P=? [F \"two\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -59,7 +59,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die) { EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("P=? [F \"three\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -68,7 +68,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die) { EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("R=? [F \"done\"]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -82,7 +82,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program); EXPECT_EQ(8607ul, model->getNumberOfStates()); @@ -94,7 +94,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds) { storm::modelchecker::SymbolicDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("P=? [F \"observe0Greater1\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -103,7 +103,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds) { EXPECT_NEAR(0.33288236360191303, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.33288236360191303, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("P=? [F \"observeIGreater1\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -112,7 +112,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds) { EXPECT_NEAR(0.15222081144084315, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.15222081144084315, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("P=? [F \"observeOnlyTrueSender\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -126,7 +126,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; // Build the die model with its reward model. #ifdef WINDOWS @@ -146,7 +146,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader) { storm::modelchecker::SymbolicDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("P=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -155,7 +155,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader) { EXPECT_NEAR(1.0, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("P=? [F<=20 \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -164,7 +164,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader) { EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("R=? [F \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); diff --git a/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp index c4a226214..c689a9edd 100644 --- a/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp @@ -21,7 +21,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; // Build the die model with its reward model. #ifdef WINDOWS @@ -41,7 +41,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice) { storm::modelchecker::SymbolicMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("Pmin=? [F \"two\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -50,7 +50,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice) { EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F \"two\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -59,7 +59,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice) { EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmin=? [F \"three\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -68,7 +68,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice) { EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F \"three\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -77,7 +77,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice) { EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmin=? [F \"four\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -86,7 +86,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice) { EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F \"four\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -95,7 +95,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice) { EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmin=? [F \"done\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -104,7 +104,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice) { EXPECT_NEAR(7.3333272933959961, quantitativeResult7.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(7.3333272933959961, quantitativeResult7.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmax=? [F \"done\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -118,7 +118,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; // Build the die model with its reward model. #ifdef WINDOWS @@ -138,7 +138,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader) { storm::modelchecker::SymbolicMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("Pmin=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -147,7 +147,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader) { EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -156,7 +156,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader) { EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmin=? [F<=25 \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -165,7 +165,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader) { EXPECT_NEAR(0.0625, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0625, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F<=25 \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -174,7 +174,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader) { EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0625, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmin=? [F \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); @@ -183,7 +183,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader) { EXPECT_NEAR(4.2856890848060498, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(4.2856890848060498, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmax=? [F \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); diff --git a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp index e07c04e20..f741eabc0 100644 --- a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp @@ -21,50 +21,50 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> mdp = 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.trans.rew")->as>(); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; ASSERT_EQ(mdp->getNumberOfStates(), 169ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); storm::modelchecker::SparseMdpPrctlModelChecker> mc(*mdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("Pmin=? [F \"two\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); std::unique_ptr result = mc.check(*formula); ASSERT_NEAR(0.0277777612209320068, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F \"two\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); result = mc.check(*formula); ASSERT_NEAR(0.0277777612209320068, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmin=? [F \"three\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); result = mc.check(*formula); ASSERT_NEAR(0.0555555224418640136, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F \"three\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); result = mc.check(*formula); ASSERT_NEAR(0.0555555224418640136, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmin=? [F \"four\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); result = mc.check(*formula); ASSERT_NEAR(0.083333283662796020508, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F \"four\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); result = mc.check(*formula); ASSERT_NEAR(0.083333283662796020508, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmin=? [F \"done\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); result = mc.check(*formula); @@ -74,7 +74,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { ASSERT_NEAR(7.33332904, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #endif - formula = parser.parseFromString("Rmax=? [F \"done\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); result = mc.check(*formula); @@ -89,7 +89,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { storm::modelchecker::SparseMdpPrctlModelChecker> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); - formula = parser.parseFromString("Rmin=? [F \"done\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); result = stateRewardModelChecker.check(*formula); @@ -99,7 +99,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { ASSERT_NEAR(7.33332904, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #endif - formula = parser.parseFromString("Rmax=? [F \"done\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); result = stateRewardModelChecker.check(*formula); @@ -114,7 +114,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { storm::modelchecker::SparseMdpPrctlModelChecker> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); - formula = parser.parseFromString("Rmin=? [F \"done\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); result = stateAndTransitionRewardModelChecker.check(*formula); @@ -123,7 +123,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { #else ASSERT_NEAR(14.6666581, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #endif - formula = parser.parseFromString("Rmax=? [F \"done\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); result = stateAndTransitionRewardModelChecker.check(*formula); @@ -138,39 +138,39 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) { std::shared_ptr> mdp = 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")->as>(); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; ASSERT_EQ(mdp->getNumberOfStates(), 3172ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 7144ull); storm::modelchecker::SparseMdpPrctlModelChecker> mc(*mdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("Pmin=? [F \"elected\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); std::unique_ptr result = mc.check(*formula); ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult()[0] - 1), storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); result = mc.check(*formula); ASSERT_NEAR(1, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F<=25 \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); result = mc.check(*formula); ASSERT_NEAR(0.0625, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmin=? [F<=25 \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); result = mc.check(*formula); ASSERT_NEAR(0.0625, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmin=? [F \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); result = mc.check(*formula); @@ -180,7 +180,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_NEAR(4.285701547, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); #endif - formula = parser.parseFromString("Rmax=? [F \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); result = mc.check(*formula); diff --git a/test/functional/parser/FormulaParserTest.cpp b/test/functional/parser/FormulaParserTest.cpp index e544db180..ce80d873c 100644 --- a/test/functional/parser/FormulaParserTest.cpp +++ b/test/functional/parser/FormulaParserTest.cpp @@ -4,21 +4,21 @@ #include "src/exceptions/WrongFormatException.h" TEST(FormulaParserTest, LabelTest) { - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; std::string input = "\"label\""; std::shared_ptr formula(nullptr); - ASSERT_NO_THROW(formula = parser.parseFromString(input)); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); EXPECT_TRUE(formula->isAtomicLabelFormula()); } TEST(FormulaParserTest, ComplexLabelTest) { - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; std::string input = "!(\"a\" & \"b\") | \"a\" & !\"c\""; std::shared_ptr formula(nullptr); - ASSERT_NO_THROW(formula = parser.parseFromString(input)); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); EXPECT_TRUE(formula->isPropositionalFormula()); EXPECT_TRUE(formula->isBinaryBooleanStateFormula()); @@ -29,11 +29,11 @@ TEST(FormulaParserTest, ExpressionTest) { manager->declareBooleanVariable("x"); manager->declareIntegerVariable("y"); - storm::parser::FormulaParser parser(manager); + storm::parser::FormulaParser formulaParser(manager); std::string input = "!(x | y > 3)"; std::shared_ptr formula(nullptr); - ASSERT_NO_THROW(formula = parser.parseFromString(input)); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); EXPECT_TRUE(formula->isPropositionalFormula()); EXPECT_TRUE(formula->isUnaryBooleanStateFormula()); @@ -44,25 +44,25 @@ TEST(FormulaParserTest, LabelAndExpressionTest) { manager->declareBooleanVariable("x"); manager->declareIntegerVariable("y"); - storm::parser::FormulaParser parser(manager); + storm::parser::FormulaParser formulaParser(manager); std::string input = "!\"a\" | x | y > 3"; std::shared_ptr formula(nullptr); - ASSERT_NO_THROW(formula = parser.parseFromString(input)); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); EXPECT_TRUE(formula->isPropositionalFormula()); input = "x | y > 3 | !\"a\""; - ASSERT_NO_THROW(formula = parser.parseFromString(input)); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); EXPECT_TRUE(formula->isPropositionalFormula()); } TEST(FormulaParserTest, ProbabilityOperatorTest) { - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; std::string input = "P<0.9 [\"a\" U \"b\"]"; std::shared_ptr formula(nullptr); - ASSERT_NO_THROW(formula = parser.parseFromString(input)); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); EXPECT_TRUE(formula->isProbabilityOperatorFormula()); EXPECT_TRUE(formula->asProbabilityOperatorFormula().hasBound()); @@ -70,18 +70,18 @@ TEST(FormulaParserTest, ProbabilityOperatorTest) { } TEST(FormulaParserTest, RewardOperatorTest) { - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; std::string input = "Rmin<0.9 [F \"a\"]"; std::shared_ptr formula(nullptr); - ASSERT_NO_THROW(formula = parser.parseFromString(input)); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); EXPECT_TRUE(formula->isRewardOperatorFormula()); EXPECT_TRUE(formula->asRewardOperatorFormula().hasBound()); EXPECT_TRUE(formula->asRewardOperatorFormula().hasOptimalityType()); input = "R=? [I=10]"; - ASSERT_NO_THROW(formula = parser.parseFromString(input)); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); EXPECT_TRUE(formula->isRewardOperatorFormula()); EXPECT_FALSE(formula->asRewardOperatorFormula().hasBound()); @@ -90,11 +90,11 @@ TEST(FormulaParserTest, RewardOperatorTest) { } TEST(FormulaParserTest, ConditionalProbabilityTest) { - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; std::string input = "P<0.9 [F \"a\" || F \"b\"]"; std::shared_ptr formula(nullptr); - ASSERT_NO_THROW(formula = parser.parseFromString(input)); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); EXPECT_TRUE(formula->isProbabilityOperatorFormula()); storm::logic::ProbabilityOperatorFormula const& probFormula = formula->asProbabilityOperatorFormula(); @@ -102,11 +102,11 @@ TEST(FormulaParserTest, ConditionalProbabilityTest) { } TEST(FormulaParserTest, NestedPathFormulaTest) { - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; std::string input = "P<0.9 [F X \"a\"]"; std::shared_ptr formula(nullptr); - ASSERT_NO_THROW(formula = parser.parseFromString(input)); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); EXPECT_TRUE(formula->isProbabilityOperatorFormula()); ASSERT_TRUE(formula->asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()); @@ -114,11 +114,11 @@ TEST(FormulaParserTest, NestedPathFormulaTest) { } TEST(FormulaParserTest, CommentTest) { - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; std::string input = "// This is a comment. And this is a commented out formula: P<=0.5 [ F \"a\" ] The next line contains the actual formula. \n P<=0.5 [ X \"b\" ] // Another comment \n // And again: another comment."; std::shared_ptr formula(nullptr); - ASSERT_NO_THROW(formula = parser.parseFromString(input)); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); EXPECT_TRUE(formula->isProbabilityOperatorFormula()); ASSERT_TRUE(formula->asProbabilityOperatorFormula().getSubformula().isNextFormula()); ASSERT_TRUE(formula->asProbabilityOperatorFormula().getSubformula().asNextFormula().getSubformula().isAtomicLabelFormula()); @@ -130,20 +130,20 @@ TEST(FormulaParserTest, WrongFormatTest) { manager->declareBooleanVariable("x"); manager->declareIntegerVariable("y"); - storm::parser::FormulaParser parser(manager); + storm::parser::FormulaParser formulaParser(manager); std::string input = "P>0.5 [ a ]"; std::shared_ptr formula(nullptr); - EXPECT_THROW(formula = parser.parseFromString(input), storm::exceptions::WrongFormatException); + EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException); input = "P=0.5 [F \"a\"]"; - EXPECT_THROW(formula = parser.parseFromString(input), storm::exceptions::WrongFormatException); + EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException); input = "P>0.5 [F !(x = 0)]"; - EXPECT_THROW(formula = parser.parseFromString(input), storm::exceptions::WrongFormatException); + EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException); input = "P>0.5 [F !y]"; - EXPECT_THROW(formula = parser.parseFromString(input), storm::exceptions::WrongFormatException); + EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException); input = "P>0.5 [F y!=0)]"; - EXPECT_THROW(formula = parser.parseFromString(input), storm::exceptions::WrongFormatException); + EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException); }