From 49bed497b0f376b50544283c90daa2af03febb95 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 22 Mar 2015 15:47:57 +0100 Subject: [PATCH] Fixed a model building problem. Included checking of reward properties on CTMCs and wrote tests for it. Former-commit-id: a137bd20ac63cd20d23b14488c2dc373a1db9438 --- examples/ctmc/embedded/embedded_debug.sm | 33 --- src/builder/ExplicitPrismModelBuilder.cpp | 8 +- .../csl/SparseCtmcCslModelChecker.cpp | 38 ++-- .../GmmxxCtmcCslModelCheckerTest.cpp | 213 ++++++++++++++++++ .../GmmxxMdpPrctlModelCheckerTest.cpp | 196 ++++++++++++++++ .../SparseCtmcCslModelCheckerTest.cpp | 58 ++++- .../SparseDtmcEliminationModelCheckerTest.cpp | 23 +- 7 files changed, 499 insertions(+), 70 deletions(-) delete mode 100644 examples/ctmc/embedded/embedded_debug.sm create mode 100644 test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp create mode 100644 test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp diff --git a/examples/ctmc/embedded/embedded_debug.sm b/examples/ctmc/embedded/embedded_debug.sm deleted file mode 100644 index a28bf7939..000000000 --- a/examples/ctmc/embedded/embedded_debug.sm +++ /dev/null @@ -1,33 +0,0 @@ -ctmc - -// constants -const int MAX_COUNT; -const int MIN_SENSORS = 2; -const int MIN_ACTUATORS = 1; - -// rates -const double lambda_p = 1/(365*24*60*60); // 1 year -const double lambda_s = 1/(30*24*60*60); // 1 month -const double lambda_a = 1/(2*30*24*60*60); // 2 months -const double tau = 1/60; // 1 min -const double delta_f = 1/(24*60*60); // 1 day -const double delta_r = 1/30; // 30 secs - -// sensors -module sensors - - s : [0..3] init 3; // number of sensors working - - [] s>1 -> s*lambda_s : (s'=s-1); // failure of a single sensor - -endmodule - -// input processor -// (takes data from sensors and passes onto main processor) -module proci - - i : [0..2] init 2; // 2=ok, 1=transient fault, 0=failed - - [] i>0 & s>=MIN_SENSORS -> lambda_p : (i'=0); // failure of processor - -endmodule diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index bb6b0ede7..05cf9c52e 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -127,11 +127,6 @@ namespace storm { #endif } - // Now that we have defined all the constants in the program, we need to substitute their appearances in - // all expressions in the program so we can then evaluate them without having to store the values of the - // constants in the state (i.e., valuation). - preparedProgram = preparedProgram.substituteConstants(); - storm::prism::RewardModel rewardModel = storm::prism::RewardModel(); // Select the appropriate reward model. @@ -165,6 +160,9 @@ namespace storm { } } + // Now that the program is fixed, we we need to substitute all constants with their concrete value. + preparedProgram = preparedProgram.substituteConstants(); + ModelComponents modelComponents = buildModelComponents(preparedProgram, rewardModel, options); std::shared_ptr> result; diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 64f52bcb1..ab1ec62da 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -339,23 +339,35 @@ namespace storm { template std::vector SparseCtmcCslModelChecker::computeCumulativeRewardsHelper(double timeBound) const { // Only compute the result if the model has a state-based reward this->getModel(). - STORM_LOG_THROW(this->getModel().hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); + STORM_LOG_THROW(this->getModel().hasStateRewards() || this->getModel().hasTransitionRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); - // Initialize result to state rewards of the this->getModel(). - std::vector result(this->getModel().getStateRewardVector()); + // If the time bound is zero, the result is the constant zero vector. + if (timeBound == 0) { + return std::vector(this->getModel().getNumberOfStates(), storm::utility::zero()); + } - // If the time-bound is not zero, we need to perform a transient analysis. - if (timeBound > 0) { - ValueType uniformizationRate = 0; - for (auto const& rate : this->getModel().getExitRateVector()) { - uniformizationRate = std::max(uniformizationRate, rate); + // Otherwise, we need to perform some computations. + + // Start with the uniformization. + ValueType uniformizationRate = 0; + for (auto const& rate : this->getModel().getExitRateVector()) { + uniformizationRate = std::max(uniformizationRate, rate); + } + storm::storage::SparseMatrix uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), storm::storage::BitVector(this->getModel().getNumberOfStates(), true), storm::storage::BitVector(this->getModel().getNumberOfStates()), uniformizationRate, this->getModel().getExitRateVector()); + + // Compute the total state reward vector. + std::vector totalRewardVector; + if (this->getModel().hasTransitionRewards()) { + totalRewardVector = this->getModel().getTransitionMatrix().getPointwiseProductRowSumVector(this->getModel().getTransitionRewardMatrix()); + if (this->getModel().hasStateRewards()) { + storm::utility::vector::addVectorsInPlace(totalRewardVector, this->getModel().getStateRewardVector()); } - - storm::storage::SparseMatrix uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), storm::storage::BitVector(this->getModel().getNumberOfStates(), true), storm::storage::BitVector(this->getModel().getNumberOfStates()), uniformizationRate, this->getModel().getExitRateVector()); - result = this->computeTransientProbabilities(uniformizedMatrix, timeBound, uniformizationRate, result, *this->linearEquationSolver); + } else { + totalRewardVector = std::vector(this->getModel().getStateRewardVector()); } - return result; + // Finally, compute the transient probabilities. + return this->computeTransientProbabilities(uniformizedMatrix, timeBound, uniformizationRate, totalRewardVector, *this->linearEquationSolver); } template @@ -385,7 +397,7 @@ namespace storm { } } - return std::unique_ptr(new ExplicitQuantitativeCheckResult(SparseDtmcPrctlModelChecker::computeReachabilityRewardsHelper(probabilityMatrix, modifiedStateRewardVector, this->getModel().getOptionalTransitionRewardMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), *linearEquationSolver, qualitative))); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(SparseDtmcPrctlModelChecker::computeReachabilityRewardsHelper(probabilityMatrix, modifiedStateRewardVector, this->getModel().getOptionalTransitionRewardMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), *linearEquationSolver, qualitative))); } // Explicitly instantiate the model checker. diff --git a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp new file mode 100644 index 000000000..e284cf442 --- /dev/null +++ b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp @@ -0,0 +1,213 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "src/parser/PrismParser.h" +#include "src/parser/FormulaParser.h" +#include "src/logic/Formulas.h" +#include "src/builder/ExplicitPrismModelBuilder.h" + +#include "src/solver/GmmxxLinearEquationSolver.h" +#include "src/modelchecker/csl/SparseCtmcCslModelChecker.h" +#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" + +#include "src/settings/SettingsManager.h" + +TEST(GmmxxCtmcCslModelCheckerTest, Cluster) { + // Parse the model description. + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); + std::shared_ptr formula(nullptr); + + // Build the model. + typename storm::builder::ExplicitPrismModelBuilder::Options options; + options.buildRewards = true; + options.rewardModelName = "num_repairs"; + std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); + ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); + std::shared_ptr> ctmc = model->as>(); + uint_fast64_t initialState = *ctmc->getInitialStates().begin(); + + // Create model checker. + storm::modelchecker::SparseCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver())); + + // Start checking properties. + formula = formulaParser.parseFromString("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\"]"); + 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=? [ \"minimum\" U<=10 \"premium\"]"); + 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("P=? [ !\"minimum\" U[1,inf] \"minimum\"]"); + checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(0, quantitativeCheckResult4[initialState], storm::settings::generalSettings().getPrecision()); + + formula = formulaParser.parseFromString("R=? [C<=100]"); + checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(0.8602815057967503, quantitativeCheckResult5[initialState], storm::settings::generalSettings().getPrecision()); +} + +TEST(GmmxxCtmcCslModelCheckerTest, Embedded) { + // Parse the model description. + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); + std::shared_ptr formula(nullptr); + + // Build the model. + typename storm::builder::ExplicitPrismModelBuilder::Options options; + options.buildRewards = true; + options.rewardModelName = "up"; + std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); + ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); + std::shared_ptr> ctmc = model->as>(); + uint_fast64_t initialState = *ctmc->getInitialStates().begin(); + + // Create model checker. + storm::modelchecker::SparseCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver())); + + // Start checking properties. + formula = formulaParser.parseFromString("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\"]"); + 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\"]"); + 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\"]"); + 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]"); + checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(2.7719776270427521, quantitativeCheckResult5[initialState], storm::settings::generalSettings().getPrecision()); +} + +TEST(GmmxxCtmcCslModelCheckerTest, Polling) { + // Parse the model description. + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); + std::shared_ptr formula(nullptr); + + // Build the model. + std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); + ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); + std::shared_ptr> ctmc = model->as>(); + uint_fast64_t initialState = *ctmc->getInitialStates().begin(); + + // Create model checker. + storm::modelchecker::SparseCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver())); + + // Start checking properties. + formula = formulaParser.parseFromString("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()); +} + +TEST(GmmxxCtmcCslModelCheckerTest, Fms) { + // No properties to check at this point. +} + +TEST(GmmxxCtmcCslModelCheckerTest, Tandem) { + // Parse the model description. + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); + std::shared_ptr formula(nullptr); + + // Build the model. + typename storm::builder::ExplicitPrismModelBuilder::Options options; + options.buildRewards = true; + options.rewardModelName = "customers"; + std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); + ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); + std::shared_ptr> ctmc = model->as>(); + uint_fast64_t initialState = *ctmc->getInitialStates().begin(); + + // Create model checker. + storm::modelchecker::SparseCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver())); + + // Start checking properties. + formula = formulaParser.parseFromString("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\" ]"); + 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\"]"); + 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]"); + 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]"); + 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\"]"); + checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(262.85103661561755, quantitativeCheckResult6[initialState], storm::settings::generalSettings().getPrecision()); +} diff --git a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp new file mode 100644 index 000000000..b4b4886a7 --- /dev/null +++ b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -0,0 +1,196 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "src/logic/Formulas.h" +#include "src/solver/GmmxxNondeterministicLinearEquationSolver.h" +#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" +#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "src/settings/SettingsManager.h" +#include "src/parser/AutoParser.h" + +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"); + + ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); + + std::shared_ptr> mdp = abstractModel->as>(); + + ASSERT_EQ(mdp->getNumberOfStates(), 169ull); + ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); + + storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::shared_ptr>(new storm::solver::GmmxxNondeterministicLinearEquationSolver())); + + auto labelFormula = std::make_shared("two"); + auto eventuallyFormula = std::make_shared(labelFormula); + auto minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + + std::unique_ptr result = checker.check(*minProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.0277777612209320068, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); + + auto maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + + result = checker.check(*maxProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.0277777612209320068, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("three"); + eventuallyFormula = std::make_shared(labelFormula); + minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + + result = checker.check(*minProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.0555555224418640136, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision()); + + maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + + result = checker.check(*maxProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.0555555224418640136, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("four"); + eventuallyFormula = std::make_shared(labelFormula); + minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + + result = checker.check(*minProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.083333283662796020508, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision()); + + maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + + result = checker.check(*maxProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.083333283662796020508, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("done"); + auto reachabilityRewardFormula = std::make_shared(labelFormula); + auto minRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + + result = checker.check(*minRewardOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult7 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(7.333329499, quantitativeResult7[0], storm::settings::nativeEquationSolverSettings().getPrecision()); + + auto maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + + result = checker.check(*maxRewardOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult8 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(7.333329499, quantitativeResult8[0], storm::settings::nativeEquationSolverSettings().getPrecision()); + + abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", ""); + + ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); + + std::shared_ptr> stateRewardMdp = abstractModel->as>(); + + storm::modelchecker::SparseMdpPrctlModelChecker stateRewardModelChecker(*stateRewardMdp, std::shared_ptr>(new storm::solver::GmmxxNondeterministicLinearEquationSolver())); + + labelFormula = std::make_shared("done"); + reachabilityRewardFormula = std::make_shared(labelFormula); + minRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + + result = stateRewardModelChecker.check(*minRewardOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult9 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(7.333329499, quantitativeResult9[0], storm::settings::nativeEquationSolverSettings().getPrecision()); + + maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + + result = stateRewardModelChecker.check(*maxRewardOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult10 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(7.333329499, quantitativeResult10[0], storm::settings::nativeEquationSolverSettings().getPrecision()); + + abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew"); + + ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); + + std::shared_ptr> stateAndTransitionRewardMdp = abstractModel->as>(); + + storm::modelchecker::SparseMdpPrctlModelChecker stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::shared_ptr>(new storm::solver::GmmxxNondeterministicLinearEquationSolver())); + + labelFormula = std::make_shared("done"); + reachabilityRewardFormula = std::make_shared(labelFormula); + minRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + + result = stateAndTransitionRewardModelChecker.check(*minRewardOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult11 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(14.666658998, quantitativeResult11[0], storm::settings::nativeEquationSolverSettings().getPrecision()); + + maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + + result = stateAndTransitionRewardModelChecker.check(*maxRewardOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult12 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(14.666658998, quantitativeResult12[0], storm::settings::nativeEquationSolverSettings().getPrecision()); +} + +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"); + + ASSERT_EQ(storm::models::ModelType::Mdp, abstractModel->getType()); + + std::shared_ptr> mdp = abstractModel->as>(); + + ASSERT_EQ(3172ull, mdp->getNumberOfStates()); + ASSERT_EQ(7144ull, mdp->getNumberOfTransitions()); + + storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::shared_ptr>(new storm::solver::GmmxxNondeterministicLinearEquationSolver())); + + auto labelFormula = std::make_shared("elected"); + auto eventuallyFormula = std::make_shared(labelFormula); + auto minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + + std::unique_ptr result = checker.check(*minProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); + + auto maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + + result = checker.check(*maxProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("elected"); + auto trueFormula = std::make_shared(true); + auto boundedUntilFormula = std::make_shared(trueFormula, labelFormula, 25); + minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, boundedUntilFormula); + + result = checker.check(*minProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.0625, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision()); + + maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, boundedUntilFormula); + + result = checker.check(*maxProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.0625, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("elected"); + auto reachabilityRewardFormula = std::make_shared(labelFormula); + auto minRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + + result = checker.check(*minRewardOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(4.285689611, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision()); + + auto maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + + result = checker.check(*maxRewardOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(4.285689611, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision()); +} diff --git a/test/functional/modelchecker/SparseCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/SparseCtmcCslModelCheckerTest.cpp index 86792fe8d..5a6ca4a2c 100644 --- a/test/functional/modelchecker/SparseCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseCtmcCslModelCheckerTest.cpp @@ -19,13 +19,16 @@ TEST(SparseCtmcCslModelCheckerTest, Cluster) { std::shared_ptr formula(nullptr); // Build the model. - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); + typename storm::builder::ExplicitPrismModelBuilder::Options options; + options.buildRewards = true; + options.rewardModelName = "num_repairs"; + std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); uint_fast64_t initialState = *ctmc->getInitialStates().begin(); // Create model checker. - storm::modelchecker::SparseCtmcCslModelChecker modelchecker(*ctmc); + storm::modelchecker::SparseCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::solver::NativeLinearEquationSolver())); // Start checking properties. formula = formulaParser.parseFromString("P=? [ F<=100 !\"minimum\"]"); @@ -55,6 +58,13 @@ TEST(SparseCtmcCslModelCheckerTest, Cluster) { ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0, quantitativeCheckResult4[initialState], storm::settings::generalSettings().getPrecision()); + + formula = formulaParser.parseFromString("R=? [C<=100]"); + checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(0.8602815057967503, quantitativeCheckResult5[initialState], storm::settings::generalSettings().getPrecision()); } TEST(SparseCtmcCslModelCheckerTest, Embedded) { @@ -64,13 +74,16 @@ TEST(SparseCtmcCslModelCheckerTest, Embedded) { std::shared_ptr formula(nullptr); // Build the model. - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); + typename storm::builder::ExplicitPrismModelBuilder::Options options; + options.buildRewards = true; + options.rewardModelName = "up"; + std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); uint_fast64_t initialState = *ctmc->getInitialStates().begin(); // Create model checker. - storm::modelchecker::SparseCtmcCslModelChecker modelchecker(*ctmc); + storm::modelchecker::SparseCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::solver::NativeLinearEquationSolver())); // Start checking properties. formula = formulaParser.parseFromString("P=? [ F<=10000 \"down\"]"); @@ -100,6 +113,13 @@ TEST(SparseCtmcCslModelCheckerTest, Embedded) { 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]"); + checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(2.7719776270427521, quantitativeCheckResult5[initialState], storm::settings::generalSettings().getPrecision()); } TEST(SparseCtmcCslModelCheckerTest, Polling) { @@ -136,14 +156,17 @@ TEST(SparseCtmcCslModelCheckerTest, Tandem) { storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); std::shared_ptr formula(nullptr); - // Build the model. - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); + // Build the model with the customers reward structure. + typename storm::builder::ExplicitPrismModelBuilder::Options options; + options.buildRewards = true; + options.rewardModelName = "customers"; + std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); uint_fast64_t initialState = *ctmc->getInitialStates().begin(); // Create model checker. - storm::modelchecker::SparseCtmcCslModelChecker modelchecker(*ctmc); + storm::modelchecker::SparseCtmcCslModelChecker modelchecker(*ctmc, std::unique_ptr>(new storm::solver::NativeLinearEquationSolver())); // Start checking properties. formula = formulaParser.parseFromString("P=? [ F<=10 \"network_full\" ]"); @@ -166,4 +189,25 @@ TEST(SparseCtmcCslModelCheckerTest, Tandem) { 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]"); + 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]"); + 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\"]"); + checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult6 = checkResult->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(262.78584491454814, quantitativeCheckResult6[initialState], storm::settings::generalSettings().getPrecision()); } diff --git a/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp b/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp index 96d6dfde0..55bb8443f 100644 --- a/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp @@ -2,7 +2,6 @@ #include "storm-config.h" #include "src/logic/Formulas.h" -#include "src/solver/GmmxxLinearEquationSolver.h" #include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/settings/SettingsManager.h" @@ -27,7 +26,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, Die) { std::unique_ptr result = checker.check(*eventuallyFormula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(1.0/6.0, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); + EXPECT_NEAR(1.0/6.0, quantitativeResult1[0], storm::settings::generalSettings().getPrecision()); labelFormula = std::make_shared("two"); eventuallyFormula = std::make_shared(labelFormula); @@ -35,7 +34,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, Die) { result = checker.check(*eventuallyFormula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(1.0/6.0, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); + EXPECT_NEAR(1.0/6.0, quantitativeResult2[0], storm::settings::generalSettings().getPrecision()); labelFormula = std::make_shared("three"); eventuallyFormula = std::make_shared(labelFormula); @@ -43,7 +42,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, Die) { result = checker.check(*eventuallyFormula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(1.0/6.0, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); + EXPECT_NEAR(1.0/6.0, quantitativeResult3[0], storm::settings::generalSettings().getPrecision()); auto done = std::make_shared("done"); auto reachabilityRewardFormula = std::make_shared(done); @@ -51,7 +50,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, Die) { result = checker.check(*reachabilityRewardFormula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(11.0/3.0, quantitativeResult4[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); + EXPECT_NEAR(11.0/3.0, quantitativeResult4[0], storm::settings::generalSettings().getPrecision()); } TEST(SparseDtmcEliminationModelCheckerTest, Crowds) { @@ -72,7 +71,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, Crowds) { std::unique_ptr result = checker.check(*eventuallyFormula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(0.3328800375801578281, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.3328800375801578281, quantitativeResult1[0], storm::settings::generalSettings().getPrecision()); labelFormula = std::make_shared("observeIGreater1"); eventuallyFormula = std::make_shared(labelFormula); @@ -80,7 +79,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, Crowds) { result = checker.check(*eventuallyFormula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(0.1522194965, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.1522194965, quantitativeResult2[0], storm::settings::generalSettings().getPrecision()); labelFormula = std::make_shared("observeOnlyTrueSender"); eventuallyFormula = std::make_shared(labelFormula); @@ -88,7 +87,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, Crowds) { result = checker.check(*eventuallyFormula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(0.32153724292835045, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.32153724292835045, quantitativeResult3[0], storm::settings::generalSettings().getPrecision()); labelFormula = std::make_shared("observe0Greater1"); eventuallyFormula = std::make_shared(labelFormula); @@ -100,7 +99,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, Crowds) { result = checker.check(*conditionalFormula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(0.15330064292476167, quantitativeResult4[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.15330064292476167, quantitativeResult4[0], storm::settings::generalSettings().getPrecision()); labelFormula = std::make_shared("observeOnlyTrueSender"); eventuallyFormula = std::make_shared(labelFormula); @@ -112,7 +111,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, Crowds) { result = checker.check(*conditionalFormula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(0.96592521978041668, quantitativeResult5[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.96592521978041668, quantitativeResult5[0], storm::settings::generalSettings().getPrecision()); } TEST(SparseDtmcEliminationModelCheckerTest, SynchronousLeader) { @@ -132,7 +131,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, SynchronousLeader) { std::unique_ptr result = checker.check(*eventuallyFormula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); + EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::generalSettings().getPrecision()); labelFormula = std::make_shared("elected"); auto reachabilityRewardFormula = std::make_shared(labelFormula); @@ -140,5 +139,5 @@ TEST(SparseDtmcEliminationModelCheckerTest, SynchronousLeader) { result = checker.check(*reachabilityRewardFormula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(1.0448979, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); + EXPECT_NEAR(1.0448979, quantitativeResult3[0], storm::settings::generalSettings().getPrecision()); }