diff --git a/resources/examples/testfiles/mdp/one_dim_walk.nm b/resources/examples/testfiles/mdp/one_dim_walk.nm new file mode 100644 index 000000000..7ad51b3e8 --- /dev/null +++ b/resources/examples/testfiles/mdp/one_dim_walk.nm @@ -0,0 +1,21 @@ +mdp +const int N; + +const double p = 0.5; + +module main + x : [0..N] init N/2; + + [right] x p : (x'=x+1) + (1-p) : (x'=x); + [left] x>0 -> p : (x'=x-1) + (1-p) : (x'=x); + +endmodule + +rewards "r" + [right] true : 1; + endrewards + + + rewards "l" + [left] true : 1; + endrewards \ No newline at end of file diff --git a/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp b/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp new file mode 100644 index 000000000..49bd83227 --- /dev/null +++ b/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp @@ -0,0 +1,113 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h" +#include "storm/models/sparse/Mdp.h" +#include "storm/settings/modules/GeneralSettings.h" +#include "storm/settings/SettingsManager.h" +#include "storm/utility/constants.h" +#include "storm/api/storm.h" + + +TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, one_dim_walk_small) { + + std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/one_dim_walk.nm"; + std::string constantsDef = "N=2"; + std::string formulasAsString = "multi(Pmax=? [ F{\"r\"}<=1 x=N ]) "; + formulasAsString += "; \n multi(Pmax=? [ multi( F{\"r\"}<=1 x=N, F{\"l\"}<=2 x=0 )])"; + formulasAsString += "; \n multi(Pmin=? [ multi( F{\"r\"}<=1 x=N, F{\"l\"}<=2 x=0 )])"; + formulasAsString += "; \n multi(Pmax=? [ F{\"r\"}<=1 x=N], Pmax=? [ F{\"l\"}<=2 x=0])"; + formulasAsString += "; \n multi(Pmin=? [ F{\"r\"}<=1 x=N], Pmax=? [ F{\"l\"}<=2 x=0])"; + formulasAsString += "; \n multi(Pmin=? [ F{\"r\"}<=1 x=N], Pmin=? [ F{\"l\"}<=2 x=0])"; + + // programm, model, formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsDef); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); + uint_fast64_t const initState = *mdp->getInitialStates().begin();; + + std::unique_ptr result; + + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(0.5), result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[1]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(0.125), result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[2]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(0.0), result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[3]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); + std::vector p1 = {storm::utility::convertNumber(0.5), storm::utility::convertNumber(0.5)}; + std::vector q1 = {storm::utility::convertNumber(0.125), storm::utility::convertNumber(0.75)}; + auto expectedAchievableValues = storm::storage::geometry::Polytope::createDownwardClosure(std::vector>({p1, q1})); + + EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult().getUnderApproximation())); + EXPECT_TRUE(result->asExplicitParetoCurveCheckResult().getOverApproximation()->contains(expectedAchievableValues)); + + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[4]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); + std::vector p2 = {storm::utility::convertNumber(0.0), storm::utility::convertNumber(0.75)}; + expectedAchievableValues = storm::storage::geometry::Polytope::createDownwardClosure(std::vector>({p2})); + std::vector> transformationMatrix(2, std::vector(2, storm::utility::zero())); + transformationMatrix[0][0] = -storm::utility::one(); + transformationMatrix[1][1] = storm::utility::one(); + expectedAchievableValues = expectedAchievableValues->affineTransformation(transformationMatrix, std::vector(2, storm::utility::zero())); + EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult().getUnderApproximation())); + EXPECT_TRUE(result->asExplicitParetoCurveCheckResult().getOverApproximation()->contains(expectedAchievableValues)); + + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[5]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); + std::vector p3 = {storm::utility::convertNumber(0.0), storm::utility::convertNumber(-0.75)}; + std::vector q3 = {storm::utility::convertNumber(-0.5), storm::utility::convertNumber(0.0)}; + expectedAchievableValues = storm::storage::geometry::Polytope::createDownwardClosure(std::vector>({p3 ,q3})); + transformationMatrix[1][1] = -storm::utility::one(); + expectedAchievableValues = expectedAchievableValues->affineTransformation(transformationMatrix, std::vector(2, storm::utility::zero())); + EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult().getUnderApproximation())); + EXPECT_TRUE(result->asExplicitParetoCurveCheckResult().getOverApproximation()->contains(expectedAchievableValues)); + +} + +TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, one_dim_walk_large) { + + std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/one_dim_walk.nm"; + std::string constantsDef = "N=10"; + std::string formulasAsString = "multi(Pmax=? [ F{\"r\"}<=5 x=N ]) "; + formulasAsString += "; \n multi(Pmax=? [ multi( F{\"r\"}<=5 x=N, F{\"l\"}<=10 x=0 )])"; + formulasAsString += "; \n multi(P>=1/512 [ F{\"r\"}<=5 x=N], Pmax=? [ F{\"l\"}<=10 x=0])"; + + // programm, model, formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsDef); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); + uint_fast64_t const initState = *mdp->getInitialStates().begin();; + + std::unique_ptr result; + + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + storm::RationalNumber expectedResult = storm::utility::pow(storm::utility::convertNumber(0.5), 5); + EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[1]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + expectedResult = storm::utility::pow(storm::utility::convertNumber(0.5), 15); + EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[2]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + expectedResult = storm::utility::convertNumber("2539/4096"); + EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); + +} + +