#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/modelchecker/results/ExplicitParetoCurveCheckResult.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/storage/geometry/Polytope.h" #include "storm/storage/geometry/Hyperrectangle.h" #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/MultiObjectiveSettings.h" #include "storm/settings/SettingsManager.h" #include "storm/utility/storm.h" /* Rationals for MAs not supported at this point TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, serverRationalNumbers) { std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/server.ma"; std::string formulasAsString = "multi(Tmax=? [ F \"error\" ], Pmax=? [ F \"processB\" ]) "; // pareto // formulasAsString += "; \n multi(..)"; // programm, model, formula storm::prism::Program program = storm::parseProgram(programFile); program.checkValidity(); std::vector> formulas = storm::extractFormulasFromProperties(parseFormulasForProgram(formulasAsString, program)); storm::generator::NextStateGeneratorOptions options(formulas); std::shared_ptr> ma = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); storm::modelchecker::SparseMarkovAutomatonCslModelChecker> checker(*ma); std::unique_ptr result = checker.check(storm::modelchecker::CheckTask(*formulas[0], true)); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); storm::RationalNumber p1 = storm::utility::convertNumber(11.0); p1 /= storm::utility::convertNumber(6.0); storm::RationalNumber p2 = storm::utility::convertNumber(1.0); p2 /= storm::utility::convertNumber(2.0); std::vector p = {p1, p2}; storm::RationalNumber q1 = storm::utility::convertNumber(29.0); q1 /= storm::utility::convertNumber(18.0); storm::RationalNumber q2 = storm::utility::convertNumber(2.0); q2 /= storm::utility::convertNumber(3.0); std::vector q = {q1, q2}; auto expectedAchievableValues = storm::storage::geometry::Polytope::createDownwardClosure(std::vector>({p,q})); EXPECT_TRUE(expectedAchievableValues->contains(result->asExplicitParetoCurveCheckResult().getUnderApproximation())); EXPECT_TRUE(result->asExplicitParetoCurveCheckResult().getOverApproximation()->contains(expectedAchievableValues)); }*/ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, server) { std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/server.ma"; std::string formulasAsString = "multi(Tmax=? [ F \"error\" ], Pmax=? [ F \"processB\" ]) "; // pareto 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::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); // we do our checks with rationals to avoid numerical issues when doing polytope computations... std::vector p = {11.0/6.0, 1.0/2.0}; std::vector q = {29.0/18.0, 2.0/3.0}; auto expectedAchievableValues = storm::storage::geometry::Polytope::createDownwardClosure( std::vector>({storm::utility::vector::convertNumericVector(p), storm::utility::vector::convertNumericVector(q)})); // due to precision issues, we enlarge one of the polytopes before checking containement storm::RationalNumber eps = storm::utility::convertNumber(storm::settings::getModule().getPrecision()); std::vector lb(2,-eps), ub(2,eps); auto bloatingBox = storm::storage::geometry::Hyperrectangle(lb,ub).asPolytope(); EXPECT_TRUE(expectedAchievableValues->minkowskiSum(bloatingBox)->contains(result->asExplicitParetoCurveCheckResult().getUnderApproximation()->convertNumberRepresentation())); EXPECT_TRUE(result->asExplicitParetoCurveCheckResult().getOverApproximation()->convertNumberRepresentation()->minkowskiSum(bloatingBox)->contains(expectedAchievableValues)); } TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_pareto_3Obj) { std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma"; std::string formulasAsString = "multi(Tmin=? [ F \"all_jobs_finished\" ], Pmax=? [ F<=0.2 \"half_of_jobs_finished\" ], Pmin=? [ F \"slowest_before_fastest\" ]) "; 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::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); std::vector j12 = {1.266666667,0.1617571721,0.5}; std::vector j13 = {1.283333333,0.1707737575,0.25}; std::vector j23 = {1.333333333,0.1978235137,0.1}; // we do our checks with rationals to avoid numerical issues when doing polytope computations... auto expectedAchievableValues = storm::storage::geometry::Polytope::create( std::vector>({storm::utility::vector::convertNumericVector(j12), storm::utility::vector::convertNumericVector(j13), storm::utility::vector::convertNumericVector(j23)})); // due to precision issues, we enlarge one of the polytopes before checking containement storm::RationalNumber eps = storm::utility::convertNumber(storm::settings::getModule().getPrecision()); std::vector lb(3,-eps), ub(3,eps); auto bloatingBox = storm::storage::geometry::Hyperrectangle(lb,ub).asPolytope(); EXPECT_TRUE(result->asExplicitParetoCurveCheckResult().getOverApproximation()->convertNumberRepresentation()->minkowskiSum(bloatingBox)->contains(expectedAchievableValues)); } TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, 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::Pcaa); 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::Pcaa); ASSERT_TRUE(result2->isExplicitQualitativeCheckResult()); EXPECT_FALSE(result2->asExplicitQualitativeCheckResult()[initState]); } TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_quantitative_3Obj) { std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma"; std::string formulasAsString = "multi(Tmin=? [ F \"all_jobs_finished\" ], P>=0.1797900683 [ F<=0.2 \"half_of_jobs_finished\" ], P<=0.3 [ F \"slowest_before_fastest\" ]) "; //quantitative formulasAsString += "; multi(T<=1.26 [ F \"all_jobs_finished\" ], P>=0.2 [ F<=0.2 \"half_of_jobs_finished\" ], Pmin=? [ 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::Pcaa); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); EXPECT_NEAR(1.3, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); std::unique_ptr result2 = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[1]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result2->isExplicitQualitativeCheckResult()); EXPECT_FALSE(result2->asExplicitQualitativeCheckResult()[initState]); } TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_pareto_2Obj) { std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma"; std::string formulasAsString = "multi( Pmax=? [ F<=0.1 \"one_job_finished\"], Pmin=? [F<=0.2 \"all_jobs_finished\"]) "; 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::unique_ptr result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); std::vector j12 = {0.2591835573, 0.01990529674}; std::vector j13 = {0.329682099, 0.01970194998}; std::vector j23 = {0.3934717664, 0.01948095743}; // we do our checks with rationals to avoid numerical issues when doing polytope computations... auto expectedAchievableValues = storm::storage::geometry::Polytope::create( std::vector>({storm::utility::vector::convertNumericVector(j12), storm::utility::vector::convertNumericVector(j13), storm::utility::vector::convertNumericVector(j23)})); // due to precision issues, we enlarge one of the polytopes before checking containement storm::RationalNumber eps = storm::utility::convertNumber(storm::settings::getModule().getPrecision()); std::vector lb(2,-eps), ub(2,eps); auto bloatingBox = storm::storage::geometry::Hyperrectangle(lb,ub).asPolytope(); EXPECT_TRUE(result->asExplicitParetoCurveCheckResult().getOverApproximation()->convertNumberRepresentation()->minkowskiSum(bloatingBox)->contains(expectedAchievableValues)); } #endif /* defined STORM_HAVE_HYPRO || defined STORM_HAVE_Z3_OPTIMIZE */