diff --git a/src/test/storm/modelchecker/LpMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/LpMdpPrctlModelCheckerTest.cpp new file mode 100644 index 000000000..b1b0a884a --- /dev/null +++ b/src/test/storm/modelchecker/LpMdpPrctlModelCheckerTest.cpp @@ -0,0 +1,272 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "storm/parser/FormulaParser.h" +#include "storm/logic/Formulas.h" +#include "storm/solver/LpMinMaxLinearEquationSolver.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/GeneralSettings.h" + +#include "storm/parser/AutoParser.h" +#include "storm/parser/PrismParser.h" +#include "storm/builder/ExplicitModelBuilder.h" + +TEST(LpMdpPrctlModelCheckerTest, Dice) { + std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", "", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew"); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; + + 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::make_unique>()); + + 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::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); + + result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.0277777612209320068, quantitativeResult2[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); + + result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.0555555224418640136, quantitativeResult3[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); + + result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.0555555224418640136, quantitativeResult4[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); + + result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.083333283662796020508, quantitativeResult5[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); + + result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.083333283662796020508, quantitativeResult6[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); + + result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult7 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(7.333329499, quantitativeResult7[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); + + result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult8 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(7.333329499, quantitativeResult8[0], storm::settings::getModule().getPrecision()); + + abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", ""); + + ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); + + std::shared_ptr> stateRewardMdp = abstractModel->as>(); + + storm::modelchecker::SparseMdpPrctlModelChecker> stateRewardModelChecker(*mdp, std::make_unique>()); + + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); + + result = stateRewardModelChecker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult9 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(7.333329499, quantitativeResult9[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); + + result = stateRewardModelChecker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult10 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(7.333329499, quantitativeResult10[0], storm::settings::getModule().getPrecision()); + + abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", STORM_TEST_RESOURCES_DIR "/rew/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::make_unique>()); + + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); + + result = stateAndTransitionRewardModelChecker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult11 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(14.666658998, quantitativeResult11[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); + + result = stateAndTransitionRewardModelChecker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult12 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(14.666658998, quantitativeResult12[0], storm::settings::getModule().getPrecision()); +} + +TEST(LpMdpPrctlModelCheckerTest, AsynchronousLeader) { + std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/leader4.tra", STORM_TEST_RESOURCES_DIR "/lab/leader4.lab", "", STORM_TEST_RESOURCES_DIR "/rew/leader4.trans.rew"); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; + + 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::make_unique>()); + + 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::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); + + result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1, quantitativeResult2[0], storm::settings::getModule().getPrecision()); + + 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::getModule().getPrecision()); + + 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::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); + + result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(4.285689611, quantitativeResult5[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); + + result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(4.285689611, quantitativeResult6[0], storm::settings::getModule().getPrecision()); +} + +TEST(LpMdpPrctlModelCheckerTest, SchedulerGeneration) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/scheduler_generation.nm"); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; + + storm::generator::NextStateGeneratorOptions options; + options.setBuildAllLabels(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).build(); + EXPECT_EQ(4ull, model->getNumberOfStates()); + EXPECT_EQ(11ull, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); + + std::shared_ptr> mdp = model->as>(); + + EXPECT_EQ(7ull, mdp->getNumberOfChoices()); + + auto solverFactory = std::make_unique>(); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::move(solverFactory)); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"target\"]"); + + storm::modelchecker::CheckTask checkTask(*formula); + checkTask.setProduceSchedulers(true); + + std::unique_ptr result = checker.check(checkTask); + + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + ASSERT_TRUE(result->asExplicitQuantitativeCheckResult().hasScheduler()); + storm::storage::Scheduler const& scheduler = result->asExplicitQuantitativeCheckResult().getScheduler(); + EXPECT_EQ(0ull, scheduler.getChoice(0).getDeterministicChoice()); + EXPECT_EQ(1ull, scheduler.getChoice(1).getDeterministicChoice()); + EXPECT_EQ(0ull, scheduler.getChoice(2).getDeterministicChoice()); + EXPECT_EQ(0ull, scheduler.getChoice(3).getDeterministicChoice()); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"target\"]"); + + checkTask = storm::modelchecker::CheckTask(*formula); + checkTask.setProduceSchedulers(true); + result = checker.check(checkTask); + + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + ASSERT_TRUE(result->asExplicitQuantitativeCheckResult().hasScheduler()); + storm::storage::Scheduler const& scheduler2 = result->asExplicitQuantitativeCheckResult().getScheduler(); + EXPECT_EQ(1ull, scheduler2.getChoice(0).getDeterministicChoice()); + EXPECT_EQ(2ull, scheduler2.getChoice(1).getDeterministicChoice()); + EXPECT_EQ(0ull, scheduler2.getChoice(2).getDeterministicChoice()); + EXPECT_EQ(0ull, scheduler2.getChoice(3).getDeterministicChoice()); +} + +// Test is currently disabled as the computation of this property requires eliminating the zero-reward MECs, which is +// currently not implemented and also not supported by PRISM. +TEST(LpMdpPrctlModelCheckerTest, TinyRewards) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/tiny_rewards.nm"); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; + + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(true, true)).build(); + EXPECT_EQ(3ull, model->getNumberOfStates()); + EXPECT_EQ(4ull, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); + + std::shared_ptr> mdp = model->as>(); + + EXPECT_EQ(4ull, mdp->getNumberOfChoices()); + + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::make_unique>()); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"target\"]"); + + storm::modelchecker::CheckTask checkTask(*formula); + + std::unique_ptr result = checker.check(checkTask); + + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(1, result->asExplicitQuantitativeCheckResult().getValueVector()[0], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(1, result->asExplicitQuantitativeCheckResult().getValueVector()[1], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0, result->asExplicitQuantitativeCheckResult().getValueVector()[2], storm::settings::getModule().getPrecision()); +} diff --git a/src/test/storm/solver/LpMinMaxLinearEquationSolverTest.cpp b/src/test/storm/solver/LpMinMaxLinearEquationSolverTest.cpp new file mode 100644 index 000000000..b8de5f689 --- /dev/null +++ b/src/test/storm/solver/LpMinMaxLinearEquationSolverTest.cpp @@ -0,0 +1,69 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "storm/solver/LpMinMaxLinearEquationSolver.h" +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/GeneralSettings.h" + +#include "storm/storage/SparseMatrix.h" + +TEST(LpMinMaxLinearEquationSolver, SolveWithStandardOptions) { + storm::storage::SparseMatrixBuilder builder(0, 0, 0, false, true); + ASSERT_NO_THROW(builder.newRowGroup(0)); + ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9)); + + storm::storage::SparseMatrix A; + ASSERT_NO_THROW(A = builder.build(2)); + + std::vector x(1); + std::vector b = {0.099, 0.5}; + + auto factory = storm::solver::LpMinMaxLinearEquationSolverFactory(); + auto solver = factory.create(A); + ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Minimize, x, b)); + ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::getModule().getPrecision()); + + ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Maximize, x, b)); + ASSERT_LT(std::abs(x[0] - 0.99), storm::settings::getModule().getPrecision()); +} + +TEST(LpMinMaxLinearEquationSolver, MatrixVectorMultiplication) { + storm::storage::SparseMatrixBuilder builder(0, 0, 0, false, true); + ASSERT_NO_THROW(builder.newRowGroup(0)); + ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9)); + ASSERT_NO_THROW(builder.addNextValue(0, 1, 0.099)); + ASSERT_NO_THROW(builder.addNextValue(0, 2, 0.001)); + ASSERT_NO_THROW(builder.addNextValue(1, 1, 0.5)); + ASSERT_NO_THROW(builder.addNextValue(1, 2, 0.5)); + ASSERT_NO_THROW(builder.newRowGroup(2)); + ASSERT_NO_THROW(builder.addNextValue(2, 1, 1)); + ASSERT_NO_THROW(builder.newRowGroup(3)); + ASSERT_NO_THROW(builder.addNextValue(3, 2, 1)); + + storm::storage::SparseMatrix A; + ASSERT_NO_THROW(A = builder.build()); + + std::vector x = {0, 1, 0}; + + auto factory = storm::solver::LpMinMaxLinearEquationSolverFactory(); + auto solver = factory.create(A); + + ASSERT_NO_THROW(solver->repeatedMultiply(storm::OptimizationDirection::Minimize, x, nullptr, 1)); + ASSERT_LT(std::abs(x[0] - 0.099), storm::settings::getModule().getPrecision()); + + x = {0, 1, 0}; + ASSERT_NO_THROW(solver->repeatedMultiply(storm::OptimizationDirection::Minimize, x, nullptr, 2)); + ASSERT_LT(std::abs(x[0] - 0.1881), storm::settings::getModule().getPrecision()); + + x = {0, 1, 0}; + ASSERT_NO_THROW(solver->repeatedMultiply(storm::OptimizationDirection::Minimize, x, nullptr, 20)); + ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::getModule().getPrecision()); + + x = {0, 1, 0}; + ASSERT_NO_THROW(solver->repeatedMultiply(storm::OptimizationDirection::Maximize, x, nullptr, 1)); + ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::getModule().getPrecision()); + + x = {0, 1, 0}; + ASSERT_NO_THROW(solver->repeatedMultiply(storm::OptimizationDirection::Maximize, x, nullptr, 20)); + ASSERT_LT(std::abs(x[0] - 0.9238082658), storm::settings::getModule().getPrecision()); +}