diff --git a/src/test/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp b/src/test/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp index 247af5e62..69872ed95 100644 --- a/src/test/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp +++ b/src/test/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp @@ -20,7 +20,7 @@ TEST(SparseMaCbMultiObjectiveModelCheckerTest, server) { 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> ma = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> ma = storm::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *ma->getInitialStates().begin(); std::unique_ptr result; @@ -32,26 +32,4 @@ TEST(SparseMaCbMultiObjectiveModelCheckerTest, server) { result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[1]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased); ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); -} - -TEST(SparseMaCbMultiObjectiveModelCheckerTest, jobscheduler_achievability_3Obj) { - - std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma"; - std::string formulasAsString = "multi(T<=1.31 [ F \"all_jobs_finished\" ], P>=0.17 [ F<=0.2 \"half_of_jobs_finished\" ], P<=0.31 [ F \"slowest_before_fastest\" ]) "; //true - formulasAsString += "; multi(T<=1.29 [ F \"all_jobs_finished\" ], P>=0.18 [ F<=0.2 \"half_of_jobs_finished\" ], P<=0.29 [ F \"slowest_before_fastest\" ])"; //false - - 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> ma = storm::buildSparseModel(program, formulas)->as>(); - uint_fast64_t const initState = *ma->getInitialStates().begin(); - - std::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased); - ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); - EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); - - std::unique_ptr result2 = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[1]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased); - ASSERT_TRUE(result2->isExplicitQualitativeCheckResult()); - EXPECT_FALSE(result2->asExplicitQualitativeCheckResult()[initState]); -} - +} \ No newline at end of file diff --git a/src/test/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp b/src/test/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp index ea9db6683..9f3525948 100644 --- a/src/test/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp +++ b/src/test/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp @@ -20,13 +20,10 @@ TEST(SparseMdpCbMultiObjectiveModelCheckerTest, consensus) { 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>(); + std::shared_ptr> mdp = storm::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin();; 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()); @@ -48,7 +45,7 @@ TEST(SparseMdpCbMultiObjectiveModelCheckerTest, zeroconf) { 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>(); + 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); @@ -56,6 +53,7 @@ TEST(SparseMdpCbMultiObjectiveModelCheckerTest, zeroconf) { EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); } +/* This test takes a little bit too long ... TEST(SparseMdpCbMultiObjectiveModelCheckerTest, team3with3objectives) { std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_team3.nm"; @@ -65,27 +63,12 @@ TEST(SparseMdpCbMultiObjectiveModelCheckerTest, team3with3objectives) { 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>(); + 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->isExplicitQualitativeCheckResult()); EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); } - -TEST(SparseMdpCbMultiObjectiveModelCheckerTest, scheduler) { - - std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_scheduler05.nm"; - std::string formulasAsString = "multi(R{\"time\"}<= 11.778[ F \"tasks_complete\" ], R{\"energy\"}<=1.45 [ F \"tasks_complete\" ]) "; - - // 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); - EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); -} +*/