diff --git a/test/functional/modelchecker/SparseMdpMultiObjectiveModelCheckerTest.cpp b/test/functional/modelchecker/SparseMdpMultiObjectiveModelCheckerTest.cpp index 66ed8808e..c7bb0979e 100644 --- a/test/functional/modelchecker/SparseMdpMultiObjectiveModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseMdpMultiObjectiveModelCheckerTest.cpp @@ -65,6 +65,62 @@ TEST(SparseMdpMultiObjectiveModelCheckerTest, probEqual0Objective) { } +TEST(SparseMdpMultiObjectiveModelCheckerTest, preprocessorResultsTest) { + + std::string programFile = STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/multiobjective2.nm"; + std::string formulasAsString = "multi(Rmin=? [ F s=2 ], P>=1 [ s!=1 U s=2 ]) "; + formulasAsString += "; \n multi(Rmax=? [ F s=2 ], P>=1 [ s!=1 U s=2 ]) "; + formulasAsString += "; \n multi(R<=0 [ F s=2 ], P>=1 [ s!=1 U s=2 ]) "; + formulasAsString += "; \n multi(R>0 [ F s=2 ], P>=1 [ s!=1 U s=2 ]) "; + formulasAsString += "; \n multi(Rmin=? [ F s=2 ], P>=1 [ F s=1 ], P>=1 [F s=2]) "; + formulasAsString += "; \n multi(Rmax=? [ F s=2 ], P>=1 [ F s=1 ], P>=1 [F s=2]) "; + formulasAsString += "; \n multi(R>=300 [ F s=2 ], P>=1 [ F s=1 ], P>=1 [F s=2]) "; + formulasAsString += "; \n multi(R<10 [ F s=2 ], P>=1 [ F s=1 ], P>=1 [F s=2]) "; + + // programm, model, formula + storm::prism::Program program = storm::parseProgram(programFile); + program.checkValidity(); + std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); + typename storm::builder::ExplicitPrismModelBuilder::Options options = storm::builder::ExplicitPrismModelBuilder::Options(formulas); + std::shared_ptr> mdp = storm::builder::ExplicitPrismModelBuilder(program, options).translate()->as>(); + uint_fast64_t const initState = *mdp->getInitialStates().begin(); + + storm::modelchecker::SparseMdpMultiObjectiveModelChecker> checker(*mdp); + + std::unique_ptr result = checker.check(storm::modelchecker::CheckTask(*formulas[0], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(0.0, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); + + result = checker.check(storm::modelchecker::CheckTask(*formulas[1], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(0.0, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); + + result = checker.check(storm::modelchecker::CheckTask(*formulas[2], true)); + ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); + EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); + + result = checker.check(storm::modelchecker::CheckTask(*formulas[3], true)); + ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); + EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); + + result = checker.check(storm::modelchecker::CheckTask(*formulas[4], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(10.0, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); + + result = checker.check(storm::modelchecker::CheckTask(*formulas[5], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::infinity(), result->asExplicitQuantitativeCheckResult()[initState]); + + result = checker.check(storm::modelchecker::CheckTask(*formulas[6], true)); + ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); + EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); + + result = checker.check(storm::modelchecker::CheckTask(*formulas[7], true)); + ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); + EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); + +} + TEST(SparseMdpMultiObjectiveModelCheckerTest, consensus) { std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/mdp/consensus/consensus2_3_2.nm"; diff --git a/test/functional/modelchecker/multiobjective2.nm b/test/functional/modelchecker/multiobjective2.nm new file mode 100644 index 000000000..c82411378 --- /dev/null +++ b/test/functional/modelchecker/multiobjective2.nm @@ -0,0 +1,19 @@ + +mdp + +module module1 + + s : [0..2] init 0; + + [A] s=0 -> 1 : (s'=1); + [B] s=0 -> 1 : (s'=2); + [C] s=1 -> 1 : true; + [D] s=1 -> 1 : (s'=2); + [E] s=2 -> 1 : true; +endmodule + +rewards "rew" + [A] true : 10; + [C] true : 3; +endrewards +