diff --git a/src/test/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest b/src/test/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest index 0ff8bbdeb..ea9db6683 100644 --- a/src/test/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest +++ b/src/test/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest @@ -1,10 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" -#if defined STORM_HAVE_HYPRO || defined STORM_HAVE_Z3_OPTIMIZE - #include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h" -#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/models/sparse/Mdp.h" #include "storm/settings/modules/GeneralSettings.h" @@ -26,9 +23,10 @@ TEST(SparseMdpCbMultiObjectiveModelCheckerTest, consensus) { std::shared_ptr> mdp = storm::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin();; - std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased); - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(0.10833260970000025, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); + std::unique_ptr result; + // noQuantitativeYet result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased); + // noQuantitativeYet ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + // noQuantitativeYet EXPECT_NEAR(0.10833260970000025, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[1]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased); ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); @@ -40,10 +38,11 @@ TEST(SparseMdpCbMultiObjectiveModelCheckerTest, consensus) { } + TEST(SparseMdpCbMultiObjectiveModelCheckerTest, zeroconf) { std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_zeroconf4.nm"; - std::string formulasAsString = "multi(Pmax=? [ F l=4 & ip=1 ] , P>=0.993141[ G (error=0) ]) "; // numerical + std::string formulasAsString = "multi(P>=0.0003 [ F l=4 & ip=1 ] , P>=0.993141[ G (error=0) ]) "; // numerical // programm, model, formula storm::prism::Program program = storm::parseProgram(programFile); @@ -53,14 +52,14 @@ TEST(SparseMdpCbMultiObjectiveModelCheckerTest, zeroconf) { uint_fast64_t const initState = *mdp->getInitialStates().begin(); std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased); - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(0.0003075787401574803, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); + ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); + EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); } TEST(SparseMdpCbMultiObjectiveModelCheckerTest, team3with3objectives) { std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_team3.nm"; - std::string formulasAsString = "multi(Pmax=? [ F \"task1_compl\" ], R{\"w_1_total\"}>=2.210204082 [ C ], P>=0.5 [ F \"task2_compl\" ])"; // numerical + std::string formulasAsString = "multi(P>=0.75 [ F \"task1_compl\" ], R{\"w_1_total\"}>=2.210204082 [ C ], P>=0.5 [ F \"task2_compl\" ])"; // numerical // programm, model, formula storm::prism::Program program = storm::parseProgram(programFile); @@ -70,8 +69,8 @@ TEST(SparseMdpCbMultiObjectiveModelCheckerTest, team3with3objectives) { uint_fast64_t const initState = *mdp->getInitialStates().begin(); std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased); - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(0.7448979591841851, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); + ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); + EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); } TEST(SparseMdpCbMultiObjectiveModelCheckerTest, scheduler) { @@ -90,24 +89,3 @@ TEST(SparseMdpCbMultiObjectiveModelCheckerTest, scheduler) { EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); } -TEST(SparseMdpCbMultiObjectiveModelCheckerTest, dpm) { - - std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_dpm100.nm"; - std::string formulasAsString = "multi(R{\"power\"}min=? [ C<=100 ], R{\"queue\"}<=70 [ C<=100 ])"; // numerical - - // programm, model, formula - storm::prism::Program program = storm::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, ""); - std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); - std::shared_ptr> mdp = storm::buildSparseModel(program, formulas)->as>(); - uint_fast64_t const initState = *mdp->getInitialStates().begin(); - - std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased); - ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(121.6128842, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); -} - - - - -#endif /* STORM_HAVE_HYPRO || defined STORM_HAVE_Z3_OPTIMIZE */