From 7f5e775395fd98f2e55f8937b7afdcd37ada159d Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 25 Aug 2015 13:53:45 +0200 Subject: [PATCH] adapted counterexample generation to refactoring Former-commit-id: e73d2885cda850a67cf7b10b6fd4c86b671f3335 --- src/adapters/Z3ExpressionAdapter.h | 6 ++-- src/builder/DdPrismModelBuilder.cpp | 4 +++ .../SMTMinimalCommandSetGenerator.h | 18 +++++------ src/models/symbolic/StandardRewardModel.cpp | 1 - src/parser/FormulaParser.cpp | 2 -- .../adapter/MathsatExpressionAdapterTest.cpp | 4 +-- .../GmmxxMdpPrctlModelCheckerTest.cpp | 32 +++++++++---------- .../NativeMdpPrctlModelCheckerTest.cpp | 32 +++++++++---------- ...ValueIterationMdpPrctlModelCheckerTest.cpp | 32 +++++++++---------- 9 files changed, 65 insertions(+), 66 deletions(-) diff --git a/src/adapters/Z3ExpressionAdapter.h b/src/adapters/Z3ExpressionAdapter.h index 70180a241..4fc60c8a5 100644 --- a/src/adapters/Z3ExpressionAdapter.h +++ b/src/adapters/Z3ExpressionAdapter.h @@ -5,6 +5,7 @@ #include #include "storm-config.h" + // Include the headers of Z3 only if it is available. #ifdef STORM_HAVE_Z3 #include "z3++.h" @@ -28,13 +29,15 @@ namespace storm { * context needs to be guaranteed as long as the instance of this adapter is used. */ Z3ExpressionAdapter(storm::expressions::ExpressionManager& manager, z3::context& context); + /*! * Translates the given expression to an equivalent expression for Z3. * * @param expression The expression to translate. * @return An equivalent expression for Z3. */ - z3::expr translateExpression(storm::expressions::Expression const& expression); + z3::expr translateExpression(storm::expressions::Expression const& expression); + /*! * Translates the given variable to an equivalent expression for Z3. * @@ -43,7 +46,6 @@ namespace storm { */ z3::expr translateExpression(storm::expressions::Variable const& variable); - storm::expressions::Expression translateExpression(z3::expr const& expr); /*! * Finds the counterpart to the given z3 variable declaration. diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index dcf76c96f..1d46e2f50 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -107,6 +107,8 @@ namespace storm { int_fast64_t high = integerVariable.getUpperBoundExpression().evaluateAsInt(); std::pair variablePair = manager->addMetaVariable(integerVariable.getName(), low, high); + STORM_LOG_TRACE("Created meta variables for global integer variable: " << variablePair.first.getName() << "[" << variablePair.first.getIndex() << "] and " << variablePair.second.getName() << "[" << variablePair.second.getIndex() << "]"); + rowMetaVariables.insert(variablePair.first); variableToRowMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.first); @@ -120,6 +122,8 @@ namespace storm { for (storm::prism::BooleanVariable const& booleanVariable : program.getGlobalBooleanVariables()) { std::pair variablePair = manager->addMetaVariable(booleanVariable.getName()); + STORM_LOG_TRACE("Created meta variables for global boolean variable: " << variablePair.first.getName() << "[" << variablePair.first.getIndex() << "] and " << variablePair.second.getName() << "[" << variablePair.second.getIndex() << "]"); + rowMetaVariables.insert(variablePair.first); variableToRowMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.first); diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index 658b5a114..41458b94a 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -8,7 +8,7 @@ #include "src/storage/prism/Program.h" #include "src/storage/expressions/Expression.h" -#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" +#include "src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/solver/GmmxxMinMaxLinearEquationSolver.h" #include "src/settings/SettingsManager.h" @@ -190,7 +190,6 @@ namespace storm { variableInformation.hasReachabilityVariables = true; storm::storage::SparseMatrix const& transitionMatrix = labeledMdp.getTransitionMatrix(); - std::vector const& nondeterministicChoiceIndices = labeledMdp.getNondeterministicChoiceIndices(); for (auto state : relevancyInformation.relevantStates) { variableInformation.relevantStatesToOrderVariableIndexMap[state] = variableInformation.stateOrderVariables.size(); @@ -286,7 +285,6 @@ namespace storm { // Get some data from the MDP for convenient access. storm::storage::SparseMatrix const& transitionMatrix = labeledMdp.getTransitionMatrix(); - std::vector const& nondeterministicChoiceIndices = labeledMdp.getNondeterministicChoiceIndices(); storm::storage::BitVector const& initialStates = labeledMdp.getInitialStates(); std::vector> const& choiceLabeling = labeledMdp.getChoiceLabeling(); storm::storage::SparseMatrix backwardTransitions = labeledMdp.getBackwardTransitions(); @@ -312,7 +310,7 @@ namespace storm { for (auto const& entry : transitionMatrix.getRow(currentChoice)) { if (relevancyInformation.relevantStates.get(entry.getColumn())) { for (auto relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(entry.getColumn())) { - followingLabels[choiceLabeling[currentChoice]].insert(choiceLabeling[currentChoice]); + followingLabels[choiceLabeling[currentChoice]].insert(choiceLabeling[relevantChoice]); } } else if (psiStates.get(entry.getColumn())) { canReachTargetState = true; @@ -1628,8 +1626,9 @@ namespace storm { // (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set. double maximalReachabilityProbability = 0; if (checkThresholdFeasible) { - storm::modelchecker::SparseMdpPrctlModelChecker modelchecker(labeledMdp); - std::vector result = modelchecker.computeUntilProbabilitiesHelper(false, phiStates, psiStates, false); + storm::modelchecker::helper::SparseMdpPrctlHelper modelCheckerHelper; + LOG4CPLUS_DEBUG(logger, "Invoking model checker."); + std::vector result = modelCheckerHelper.computeUntilProbabilities(false, labeledMdp.getTransitionMatrix(), labeledMdp.getBackwardTransitions(), phiStates, psiStates, false, storm::utility::solver::MinMaxLinearEquationSolverFactory()); for (auto state : labeledMdp.getInitialStates()) { maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]); } @@ -1679,7 +1678,6 @@ namespace storm { uint_fast64_t iterations = 0; uint_fast64_t currentBound = 0; maximalReachabilityProbability = 0; - auto iterationTimer = std::chrono::high_resolution_clock::now(); uint_fast64_t zeroProbabilityCount = 0; do { LOG4CPLUS_DEBUG(logger, "Computing minimal command set."); @@ -1692,9 +1690,9 @@ namespace storm { modelCheckingClock = std::chrono::high_resolution_clock::now(); commandSet.insert(relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end()); storm::models::sparse::Mdp subMdp = labeledMdp.restrictChoiceLabels(commandSet); - storm::modelchecker::SparseMdpPrctlModelChecker modelchecker(subMdp); + storm::modelchecker::helper::SparseMdpPrctlHelper modelCheckerHelper; LOG4CPLUS_DEBUG(logger, "Invoking model checker."); - std::vector result = modelchecker.computeUntilProbabilitiesHelper(false, phiStates, psiStates, false); + std::vector result = modelCheckerHelper.computeUntilProbabilities(false, subMdp.getTransitionMatrix(), subMdp.getBackwardTransitions(), phiStates, psiStates, false, storm::utility::solver::MinMaxLinearEquationSolverFactory()); LOG4CPLUS_DEBUG(logger, "Computed model checking results."); totalModelCheckingTime += std::chrono::high_resolution_clock::now() - modelCheckingClock; @@ -1769,7 +1767,7 @@ namespace storm { storm::storage::BitVector phiStates; storm::storage::BitVector psiStates; - storm::modelchecker::SparseMdpPrctlModelChecker modelchecker(labeledMdp); + storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(labeledMdp); if (probabilityOperator.getSubformula().isUntilFormula()) { storm::logic::UntilFormula const& untilFormula = probabilityOperator.getSubformula().asUntilFormula(); diff --git a/src/models/symbolic/StandardRewardModel.cpp b/src/models/symbolic/StandardRewardModel.cpp index b98462fa1..e38ee85d3 100644 --- a/src/models/symbolic/StandardRewardModel.cpp +++ b/src/models/symbolic/StandardRewardModel.cpp @@ -89,7 +89,6 @@ namespace storm { result += filterAdd * optionalStateRewardVector.get(); } if (this->hasStateActionRewards()) { - optionalStateActionRewardVector.get().exportToDot("statActRew.dot"); result += filterAdd * optionalStateActionRewardVector.get(); } if (this->hasTransitionRewards()) { diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp index 882bc5ea6..5acbba56c 100644 --- a/src/parser/FormulaParser.cpp +++ b/src/parser/FormulaParser.cpp @@ -202,8 +202,6 @@ namespace storm { STORM_LOG_DEBUG("Parsed formula successfully."); } catch (qi::expectation_failure const& e) { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, e.what_); -// } catch (std::exception const& e) { -// STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Could not parse formula: " << e.what()); } return result; diff --git a/test/functional/adapter/MathsatExpressionAdapterTest.cpp b/test/functional/adapter/MathsatExpressionAdapterTest.cpp index 78b62a48e..cd0d75256 100644 --- a/test/functional/adapter/MathsatExpressionAdapterTest.cpp +++ b/test/functional/adapter/MathsatExpressionAdapterTest.cpp @@ -170,9 +170,7 @@ TEST(MathsatExpressionAdapter, MathsatToStormBasic) { msat_env env = msat_create_env(config); ASSERT_FALSE(MSAT_ERROR_ENV(env)); msat_destroy_config(config); - - unsigned args = 2; - + std::shared_ptr manager(new storm::expressions::ExpressionManager()); manager->declareBooleanVariable("x"); manager->declareBooleanVariable("y"); diff --git a/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 9c891cc06..9d14e2782 100644 --- a/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -17,7 +17,7 @@ TEST(GmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; std::shared_ptr> mdp = abstractModel->as>(); @@ -26,42 +26,42 @@ TEST(GmxxMdpPrctlModelCheckerTest, 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.0, 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.0, 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.0, 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.0, 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(6.172433512, 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(); @@ -75,7 +75,7 @@ TEST(GmxxMdpPrctlModelCheckerTest, Consensus) { ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; std::shared_ptr> mdp = abstractModel->as>(); @@ -84,56 +84,56 @@ TEST(GmxxMdpPrctlModelCheckerTest, Consensus) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("Pmin=? [F \"finished\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0, quantitativeResult1[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmin=? [F \"finished\" & \"all_coins_equal_0\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\" & \"all_coins_equal_0\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.4374282832, quantitativeResult2[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F \"finished\" & \"all_coins_equal_1\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"finished\" & \"all_coins_equal_1\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.5293286369, quantitativeResult3[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F \"finished\" & !\"agree\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"finished\" & !\"agree\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.10414097, quantitativeResult4[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmin=? [F<=50 \"finished\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=50 \"finished\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0, quantitativeResult5[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F<=50 \"finished\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=50 \"finished\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0, quantitativeResult6[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmin=? [F \"finished\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"finished\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult7 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1725.593313, quantitativeResult7[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmax=? [F \"finished\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"finished\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult8 = result->asExplicitQuantitativeCheckResult(); diff --git a/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp index 73b45ba91..2d572d5f1 100644 --- a/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp @@ -18,7 +18,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; std::shared_ptr> mdp = abstractModel->as>(); @@ -27,42 +27,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.0, 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.0, 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.0, 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.0, 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(6.172433512, 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(); @@ -76,7 +76,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) { ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; std::shared_ptr> mdp = abstractModel->as>(); @@ -85,56 +85,56 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) { storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("Pmin=? [F \"finished\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]"); std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0, quantitativeResult1[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmin=? [F \"finished\" & \"all_coins_equal_0\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\" & \"all_coins_equal_0\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.4374282832, quantitativeResult2[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F \"finished\" & \"all_coins_equal_1\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"finished\" & \"all_coins_equal_1\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.5293286369, quantitativeResult3[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F \"finished\" & !\"agree\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"finished\" & !\"agree\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.10414097, quantitativeResult4[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmin=? [F<=50 \"finished\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=50 \"finished\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0, quantitativeResult5[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F<=50 \"finished\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=50 \"finished\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.0, quantitativeResult6[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmin=? [F \"finished\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"finished\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult7 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1725.593313, quantitativeResult7[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmax=? [F \"finished\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"finished\"]"); result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult8 = result->asExplicitQuantitativeCheckResult(); diff --git a/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp index da7bb0214..5b63a8ddd 100644 --- a/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp @@ -15,41 +15,41 @@ TEST(DISABLED_TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLea std::shared_ptr> mdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.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(), 2095783ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385ull); storm::modelchecker::SparseMdpPrctlModelChecker> checker(*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 = checker.check(*formula); ASSERT_NEAR(1.0, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); result = checker.check(*formula); ASSERT_NEAR(1.0, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmin=? [F<=25 \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); result = checker.check(*formula); ASSERT_NEAR(0.0, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F<=25 \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); result = checker.check(*formula); ASSERT_NEAR(0.0, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmin=? [F \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); result = checker.check(*formula); ASSERT_NEAR(6.172433512, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmax=? [F \"elected\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); result = checker.check(*formula); ASSERT_NEAR(6.1724344, result->asExplicitQuantitativeCheckResult()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); @@ -62,50 +62,50 @@ TEST(DISABLED_TopologicalValueIterationMdpPrctlModelCheckerTest, Consensus) { std::shared_ptr> mdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", "")->as>(); // A parser that we use for conveniently constructing the formulas. - storm::parser::FormulaParser parser; + storm::parser::FormulaParser formulaParser; ASSERT_EQ(mdp->getNumberOfStates(), 63616ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 213472ull); storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory())); - std::shared_ptr formula = parser.parseFromString("Pmin=? [F \"finished\"]"); + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]"); std::unique_ptr result = checker.check(*formula); ASSERT_NEAR(1.0, result->asExplicitQuantitativeCheckResult()[31168], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmin=? [F \"finished\" & \"all_coins_equal_0\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\" & \"all_coins_equal_0\"]"); result = checker.check(*formula); ASSERT_NEAR(0.4374282832, result->asExplicitQuantitativeCheckResult()[31168], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F \"finished\" & \"all_coins_equal_1\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"finished\" & \"all_coins_equal_1\"]"); result = checker.check(*formula); ASSERT_NEAR(0.5293286369, result->asExplicitQuantitativeCheckResult()[31168], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F \"finished\" & !\"agree\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"finished\" & !\"agree\"]"); result = checker.check(*formula); ASSERT_NEAR(0.10414097, result->asExplicitQuantitativeCheckResult()[31168], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmin=? [F<=50 \"finished\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=50 \"finished\"]"); result = checker.check(*formula); ASSERT_NEAR(0.0, result->asExplicitQuantitativeCheckResult()[31168], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Pmax=? [F<=50 \"finished\"]"); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=50 \"finished\"]"); result = checker.check(*formula); ASSERT_NEAR(0.0, result->asExplicitQuantitativeCheckResult()[31168], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmin=? [F \"finished\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"finished\"]"); result = checker.check(*formula); ASSERT_NEAR(1725.593313, result->asExplicitQuantitativeCheckResult()[31168], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision()); - formula = parser.parseFromString("Rmax=? [F \"finished\"\"]"); + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"finished\"\"]"); result = checker.check(*formula); ASSERT_NEAR(2183.142422, result->asExplicitQuantitativeCheckResult()[31168], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());