sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

tests for MinMaxLinearEquationSolver

tempestpy_adaptions
TimQu 7 years ago
parent
5fdb03440d
commit
6a986d2490
2 changed files with 341 additions and 0 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 272
      src/test/storm/modelchecker/LpMdpPrctlModelCheckerTest.cpp
  2. 69
      src/test/storm/solver/LpMinMaxLinearEquationSolverTest.cpp

272
src/test/storm/modelchecker/LpMdpPrctlModelCheckerTest.cpp
View File

@ -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<storm::models::sparse::Model<double>> 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<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
ASSERT_EQ(mdp->getNumberOfStates(), 169ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull);
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::make_unique<storm::solver::LpMinMaxLinearEquationSolverFactory<double>>());
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult7 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.333329499, quantitativeResult7[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult8 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.333329499, quantitativeResult8[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().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<storm::models::sparse::Mdp<double>> stateRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateRewardModelChecker(*mdp, std::make_unique<storm::solver::LpMinMaxLinearEquationSolverFactory<double>>());
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]");
result = stateRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult9 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.333329499, quantitativeResult9[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
result = stateRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult10 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.333329499, quantitativeResult10[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().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<storm::models::sparse::Mdp<double>> stateAndTransitionRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::make_unique<storm::solver::LpMinMaxLinearEquationSolverFactory<double>>());
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]");
result = stateAndTransitionRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult11 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(14.666658998, quantitativeResult11[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
result = stateAndTransitionRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult12 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(14.666658998, quantitativeResult12[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
}
TEST(LpMdpPrctlModelCheckerTest, AsynchronousLeader) {
std::shared_ptr<storm::models::sparse::Model<double>> 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<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
ASSERT_EQ(3172ull, mdp->getNumberOfStates());
ASSERT_EQ(7144ull, mdp->getNumberOfTransitions());
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::make_unique<storm::solver::LpMinMaxLinearEquationSolverFactory<double>>());
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0625, quantitativeResult3[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0625, quantitativeResult4[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(4.285689611, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(4.285689611, quantitativeResult6[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().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<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, options).build();
EXPECT_EQ(4ull, model->getNumberOfStates());
EXPECT_EQ(11ull, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = model->as<storm::models::sparse::Mdp<double>>();
EXPECT_EQ(7ull, mdp->getNumberOfChoices());
auto solverFactory = std::make_unique<storm::solver::LpMinMaxLinearEquationSolverFactory<double>>();
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::move(solverFactory));
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"target\"]");
storm::modelchecker::CheckTask<storm::logic::Formula> checkTask(*formula);
checkTask.setProduceSchedulers(true);
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(checkTask);
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
ASSERT_TRUE(result->asExplicitQuantitativeCheckResult<double>().hasScheduler());
storm::storage::Scheduler<double> const& scheduler = result->asExplicitQuantitativeCheckResult<double>().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<storm::logic::Formula>(*formula);
checkTask.setProduceSchedulers(true);
result = checker.check(checkTask);
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
ASSERT_TRUE(result->asExplicitQuantitativeCheckResult<double>().hasScheduler());
storm::storage::Scheduler<double> const& scheduler2 = result->asExplicitQuantitativeCheckResult<double>().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<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(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<storm::models::sparse::Mdp<double>> mdp = model->as<storm::models::sparse::Mdp<double>>();
EXPECT_EQ(4ull, mdp->getNumberOfChoices());
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::make_unique<storm::solver::LpMinMaxLinearEquationSolverFactory<double>>());
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"target\"]");
storm::modelchecker::CheckTask<storm::logic::Formula> checkTask(*formula);
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(checkTask);
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
EXPECT_NEAR(1, result->asExplicitQuantitativeCheckResult<double>().getValueVector()[0], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(1, result->asExplicitQuantitativeCheckResult<double>().getValueVector()[1], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0, result->asExplicitQuantitativeCheckResult<double>().getValueVector()[2], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
}

69
src/test/storm/solver/LpMinMaxLinearEquationSolverTest.cpp
View File

@ -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<double> builder(0, 0, 0, false, true);
ASSERT_NO_THROW(builder.newRowGroup(0));
ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9));
storm::storage::SparseMatrix<double> A;
ASSERT_NO_THROW(A = builder.build(2));
std::vector<double> x(1);
std::vector<double> b = {0.099, 0.5};
auto factory = storm::solver::LpMinMaxLinearEquationSolverFactory<double>();
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<storm::settings::modules::GeneralSettings>().getPrecision());
ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Maximize, x, b));
ASSERT_LT(std::abs(x[0] - 0.99), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
}
TEST(LpMinMaxLinearEquationSolver, MatrixVectorMultiplication) {
storm::storage::SparseMatrixBuilder<double> 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<double> A;
ASSERT_NO_THROW(A = builder.build());
std::vector<double> x = {0, 1, 0};
auto factory = storm::solver::LpMinMaxLinearEquationSolverFactory<double>();
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<storm::settings::modules::GeneralSettings>().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<storm::settings::modules::GeneralSettings>().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<storm::settings::modules::GeneralSettings>().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<storm::settings::modules::GeneralSettings>().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<storm::settings::modules::GeneralSettings>().getPrecision());
}
Write Preview
Loading…
Cancel
Save