diff --git a/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp index 937723a73..dbea6504d 100755 --- a/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp @@ -1,9 +1,14 @@ #include "test/storm_gtest.h" #include "storm-config.h" -#include "storm-parsers/parser/FormulaParser.h" +#include "storm/api/builder.h" +#include "storm-conv/api/storm-conv.h" +#include "storm-parsers/api/model_descriptions.h" +#include "storm/api/properties.h" +#include "storm-parsers/api/properties.h" + + #include "storm/logic/Formulas.h" -#include "storm/solver/StandardMinMaxLinearEquationSolver.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" @@ -11,10 +16,7 @@ #include "storm/settings/modules/GeneralSettings.h" #include "storm/environment/solver/MinMaxSolverEnvironment.h" - -#include "storm-parsers/parser/AutoParser.h" -#include "storm-parsers/parser/PrismParser.h" -#include "storm/builder/ExplicitModelBuilder.h" +#include "storm/environment/solver/LongRunAverageSolverEnvironment.h" namespace { class DoubleViEnvironment { @@ -24,6 +26,7 @@ namespace { storm::Environment env; env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-8)); + env.solver().lra().setNondetLraMethod(storm::solver::LraMethod::ValueIteration); return env; } }; @@ -35,6 +38,7 @@ namespace { env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); env.solver().setForceSoundness(true); env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); + env.solver().lra().setNondetLraMethod(storm::solver::LraMethod::ValueIteration); return env; } }; @@ -45,6 +49,7 @@ namespace { storm::Environment env; env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration); env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-8)); + env.solver().lra().setNondetLraMethod(storm::solver::LraMethod::ValueIteration); return env; } }; @@ -73,6 +78,27 @@ namespace { typedef typename TestType::ValueType ValueType; SchedulerGenerationMdpPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {} storm::Environment const& env() const { return _environment; } + + std::pair>, std::vector>> buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { + std::pair>, std::vector>> result; + storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); + program = storm::utility::prism::preprocess(program, constantDefinitionString); + result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + result.first = storm::api::buildSparseModel(program, result.second)->template as>(); + return result; + } + + std::vector> getTasks(std::vector> const& formulas) const { + std::vector> result; + for (auto const& f : formulas) { + result.emplace_back(*f); + result.back().setProduceSchedulers(true); + } + return result; + } + + ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber(input);} + private: storm::Environment _environment; }; @@ -91,52 +117,89 @@ namespace { TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, reachability) { typedef typename TestFixture::ValueType ValueType; - 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->template as>(); - + std::string formulasString = "Pmin=? [F \"target\"]; Pmax=? [F \"target\"];"; + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/scheduler_generation.nm", formulasString); + auto mdp = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(4ull, mdp->getNumberOfStates()); + EXPECT_EQ(11ull, mdp->getNumberOfTransitions()); + ASSERT_EQ(mdp->getType(), storm::models::ModelType::Mdp); EXPECT_EQ(7ull, mdp->getNumberOfChoices()); storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); - std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"target\"]"); - - storm::modelchecker::CheckTask checkTask(*formula); - checkTask.setProduceSchedulers(true); - - std::unique_ptr result = checker.check(this->env(), checkTask); - + auto result = checker.check(this->env(), tasks[0]); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - ASSERT_TRUE(result->asExplicitQuantitativeCheckResult().hasScheduler()); - storm::storage::Scheduler const& scheduler = result->asExplicitQuantitativeCheckResult().getScheduler(); + ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult().hasScheduler()); + storm::storage::Scheduler const& scheduler = result->template 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); - + result = checker.check(tasks[1]); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - ASSERT_TRUE(result->asExplicitQuantitativeCheckResult().hasScheduler()); - storm::storage::Scheduler const& scheduler2 = result->asExplicitQuantitativeCheckResult().getScheduler(); + ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult().hasScheduler()); + storm::storage::Scheduler const& scheduler2 = result->template 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()); } + + TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, lra) { + typedef typename TestFixture::ValueType ValueType; + + std::string formulasString = "R{\"grants\"}max=? [ MP ]; R{\"grants\"}min=? [ MP ];"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/cs_nfail3.nm", formulasString); + auto mdp = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(184ul, mdp->getNumberOfStates()); + EXPECT_EQ(541ul, mdp->getNumberOfTransitions()); + EXPECT_EQ(439ul, mdp->getNumberOfChoices()); + ASSERT_EQ(mdp->getType(), storm::models::ModelType::Mdp); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); + + if (!std::is_same::value) { + GTEST_SKIP() << "Lra scheduler extraction not supported for LP based method"; + } + { + auto result = checker.check(this->env(), tasks[0]); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(this->parseNumber("333/1000"), result->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], this->env().solver().lra().getPrecision()); + ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult().hasScheduler()); + storm::storage::Scheduler const& scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); + EXPECT_TRUE(scheduler.isDeterministicScheduler()); + EXPECT_TRUE(scheduler.isMemorylessScheduler()); + EXPECT_TRUE(!scheduler.isPartialScheduler()); + auto inducedModel = mdp->applyScheduler(scheduler); + ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp); + auto const& inducedMdp = inducedModel->template as>(); + EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates()); + storm::modelchecker::SparseMdpPrctlModelChecker> inducedChecker(*inducedMdp); + auto inducedResult = inducedChecker.check(this->env(), tasks[0]); + ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(this->parseNumber("333/1000"), inducedResult->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], this->env().solver().lra().getPrecision()); + } + { + auto result = checker.check(this->env(), tasks[1]); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(this->parseNumber("0"), result->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], this->env().solver().lra().getPrecision()); + ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult().hasScheduler()); + storm::storage::Scheduler const& scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); + EXPECT_TRUE(scheduler.isDeterministicScheduler()); + EXPECT_TRUE(scheduler.isMemorylessScheduler()); + EXPECT_TRUE(!scheduler.isPartialScheduler()); + auto inducedModel = mdp->applyScheduler(scheduler); + ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp); + auto const& inducedMdp = inducedModel->template as>(); + EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates()); + storm::modelchecker::SparseMdpPrctlModelChecker> inducedChecker(*inducedMdp); + auto inducedResult = inducedChecker.check(this->env(), tasks[1]); + ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(this->parseNumber("0"), inducedResult->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], this->env().solver().lra().getPrecision()); + } + } + } \ No newline at end of file