From c1063f27cc429d0bedb1d95a5774c66d17dd25f0 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 29 Dec 2016 17:43:31 +0100 Subject: [PATCH] added a few more tests for multi-objective MAs. Also fixed/improved minor stuff. --- .../examples/testfiles/ma/jobscheduler.ma | 43 ++++++ .../pcaa/SparseMaPcaaWeightVectorChecker.cpp | 1 - .../pcaa/SparsePcaaParetoQuery.cpp | 7 +- .../pcaa/SparsePcaaWeightVectorChecker.cpp | 2 +- src/storm/models/sparse/MarkovAutomaton.cpp | 1 + .../SparseMaPcaaModelCheckerTest.cpp | 134 ++++++++++++++++-- .../SparseMdpPcaaModelCheckerTest.cpp | 10 -- 7 files changed, 169 insertions(+), 29 deletions(-) create mode 100644 resources/examples/testfiles/ma/jobscheduler.ma diff --git a/resources/examples/testfiles/ma/jobscheduler.ma b/resources/examples/testfiles/ma/jobscheduler.ma new file mode 100644 index 000000000..d83a199f5 --- /dev/null +++ b/resources/examples/testfiles/ma/jobscheduler.ma @@ -0,0 +1,43 @@ + +// Stochastic Job Scheduling, based on [] +// Encoding by Junges & Quatmann +// RWTH Aachen University +// Please cite Quatmann et al: Multi-objective Model Checking of Markov Automata +ma + +const int x_j1 = 1; +const int x_j2 = 2; +const int x_j3 = 3; +formula is_running = r_j1 + r_j2 + r_j3 > 0; +formula num_finished = f_j1 + f_j2 + f_j3; +module main + + r_j1 : [0..1]; + r_j2 : [0..1]; + r_j3 : [0..1]; + f_j1 : [0..1]; + f_j2 : [0..1]; + f_j3 : [0..1]; + + <> (r_j1 = 1) -> x_j1 : (r_j1' = 0) & (r_j2' = 0) & (r_j3' = 0) & (f_j1' = 1); + <> (r_j2 = 1) -> x_j2 : (r_j1' = 0) & (r_j2' = 0) & (r_j3' = 0) & (f_j2' = 1); + <> (r_j3 = 1) -> x_j3 : (r_j1' = 0) & (r_j2' = 0) & (r_j3' = 0) & (f_j3' = 1); + + [] (!is_running) & (num_finished = 2) & (f_j1 = 0) -> 1: (r_j1' = 1); + [] (!is_running) & (num_finished = 2) & (f_j2 = 0) -> 1: (r_j2' = 1); + [] (!is_running) & (num_finished = 2) & (f_j3 = 0) -> 1: (r_j3' = 1); + + [] (!is_running) & (num_finished <= 1) & (f_j1 = 0) & (f_j2 = 0) -> 1: (r_j1' = 1) & (r_j2' = 1); + [] (!is_running) & (num_finished <= 1) & (f_j1 = 0) & (f_j3 = 0) -> 1: (r_j1' = 1) & (r_j3' = 1); + [] (!is_running) & (num_finished <= 1) & (f_j2 = 0) & (f_j3 = 0) -> 1: (r_j2' = 1) & (r_j3' = 1); + +endmodule + +init + r_j1 = 0 & + r_j2 = 0 & + r_j3 = 0 & + f_j1 = 0 & + f_j2 = 0 & + f_j3 = 0 +endinit \ No newline at end of file diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp index e39c5baba..1c4dd8420 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp @@ -5,7 +5,6 @@ #include "storm/adapters/CarlAdapter.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" -#include "storm/transformer/EndComponentEliminator.h" #include "storm/utility/macros.h" #include "storm/utility/vector.h" diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp index 1123bcdf1..639589592 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp @@ -38,9 +38,10 @@ namespace storm { // obtain the data for the checkresult std::vector> paretoOptimalPoints; - paretoOptimalPoints.reserve(this->refinementSteps.size()); - for(auto const& step : this->refinementSteps) { - paretoOptimalPoints.push_back(storm::utility::vector::convertNumericVector(this->transformPointToOriginalModel(step.lowerBoundPoint))); + std::vector vertices = this->underApproximation->getVertices(); + paretoOptimalPoints.reserve(vertices.size()); + for(auto const& vertex : vertices) { + paretoOptimalPoints.push_back(storm::utility::vector::convertNumericVector(this->transformPointToOriginalModel(vertex))); } return std::unique_ptr(new ParetoCurveCheckResult(this->originalModel.getInitialStates().getNextSetIndex(0), std::move(paretoOptimalPoints), diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp index d18146b40..8cd5245a9 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp @@ -117,7 +117,7 @@ namespace storm { template void SparsePcaaWeightVectorChecker::unboundedWeightedPhase(std::vector const& weightedRewardVector) { - if(this->objectivesWithNoUpperTimeBound.empty()) { + if(this->objectivesWithNoUpperTimeBound.empty() || !storm::utility::vector::hasNonZeroEntry(weightedRewardVector)) { this->weightedResult = std::vector(model.getNumberOfStates(), storm::utility::zero()); this->scheduler = storm::storage::TotalScheduler(model.getNumberOfStates()); return; diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp index 9ba556281..1979e08d0 100644 --- a/src/storm/models/sparse/MarkovAutomaton.cpp +++ b/src/storm/models/sparse/MarkovAutomaton.cpp @@ -349,6 +349,7 @@ namespace storm { optionalChoiceLabeling = storm::utility::vector::filterVector(optionalChoiceLabeling.get(), keepStates); } //TODO update reward models according to kept states + STORM_LOG_WARN_COND(this->getRewardModels().empty(), "Conversion of MA to CTMC does not preserve rewards."); std::unordered_map rewardModels = this->getRewardModels(); return std::make_shared>(std::move(rateMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)); diff --git a/src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp b/src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp index e29754ef3..f1025bd6f 100644 --- a/src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp +++ b/src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp @@ -11,6 +11,7 @@ #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" @@ -42,7 +43,7 @@ TEST(SparseMaPcaaModelCheckerTest, serverRationalNumbers) { std::vector q = {q1, q2}; auto expectedAchievableValues = storm::storage::geometry::Polytope::createDownwardClosure(std::vector>({p,q})); EXPECT_TRUE(expectedAchievableValues->contains(result->asParetoCurveCheckResult().getUnderApproximation())); - EXPECT_TRUE(result->asParetoCurveCheckResult().getUnderApproximation()->contains(expectedAchievableValues)); + EXPECT_TRUE(result->asParetoCurveCheckResult().getOverApproximation()->contains(expectedAchievableValues)); }*/ @@ -51,32 +52,137 @@ TEST(SparseMaPcaaModelCheckerTest, server) { 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 = storm::utility::prism::preprocess(program, ""); std::vector> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program); std::shared_ptr> ma = storm::buildSparseModel(program, formulas)->as>(); - storm::modelchecker::SparseMarkovAutomatonCslModelChecker> checker(*ma); - + std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isParetoCurveCheckResult()); + // 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>({p,q})); + 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 - std::vector lb = {-storm::settings::getModule().getPrecision(), -storm::settings::getModule().getPrecision()}; - std::vector ub = {storm::settings::getModule().getPrecision(), storm::settings::getModule().getPrecision()}; - auto bloatingBox = storm::storage::geometry::Hyperrectangle(lb,ub).asPolytope(); - - EXPECT_TRUE(expectedAchievableValues->minkowskiSum(bloatingBox)->contains(result->asParetoCurveCheckResult().getUnderApproximation())); - EXPECT_TRUE(result->asParetoCurveCheckResult().getUnderApproximation()->minkowskiSum(bloatingBox)->contains(expectedAchievableValues)); + 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->asParetoCurveCheckResult().getUnderApproximation()->convertNumberRepresentation())); + EXPECT_TRUE(result->asParetoCurveCheckResult().getOverApproximation()->convertNumberRepresentation()->minkowskiSum(bloatingBox)->contains(expectedAchievableValues)); } +TEST(SparseMaPcaaModelCheckerTest, jobscheduler_pareto_3Obj) { + + std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma"; + std::string formulasAsString = "multi(Tmin=? [ F num_finished=3 ], Pmax=? [ F<=0.2 num_finished=2 ], Pmin=? [ F f_j1=1 & f_j3=0 ]) "; + + storm::prism::Program program = storm::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, ""); + std::vector> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program); + std::shared_ptr> ma = storm::buildSparseModel(program, formulas)->as>(); + + std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isParetoCurveCheckResult()); + + 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::createDownwardClosure( + 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(expectedAchievableValues->minkowskiSum(bloatingBox)->contains(result->asParetoCurveCheckResult().getUnderApproximation()->convertNumberRepresentation())); + EXPECT_TRUE(result->asParetoCurveCheckResult().getOverApproximation()->convertNumberRepresentation()->minkowskiSum(bloatingBox)->contains(expectedAchievableValues)); + +} + +TEST(SparseMaPcaaModelCheckerTest, jobscheduler_achievability_3Obj) { + + std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma"; + std::string formulasAsString = "multi(T<=1.31 [ F num_finished=3 ], P>=0.17 [ F<=0.2 num_finished=2 ], P<=0.31 [ F f_j1=1 & f_j3=0 ]) "; //true + formulasAsString += "; multi(T<=1.29 [ F num_finished=3 ], P>=0.18 [ F<=0.2 num_finished=2 ], P<=0.29 [ F f_j1=1 & f_j3=0 ])"; //false + + storm::prism::Program program = storm::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, ""); + std::vector> formulas = storm::parseFormulasForPrismProgram(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::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); + EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); + + std::unique_ptr result2 = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[1]->asMultiObjectiveFormula()); + ASSERT_TRUE(result2->isExplicitQualitativeCheckResult()); + EXPECT_FALSE(result2->asExplicitQualitativeCheckResult()[initState]); +} + +TEST(SparseMaPcaaModelCheckerTest, jobscheduler_quantitative_3Obj) { + + std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma"; + std::string formulasAsString = "multi(Tmin=? [ F num_finished=3 ], P>=0.1797900683 [ F<=0.2 num_finished=2 ], P<=0.3 [ F f_j1=1 & f_j3=0 ]) "; //quantitative + formulasAsString += "; multi(T<=1.26 [ F num_finished=3 ], P>=0.2 [ F<=0.2 num_finished=2 ], Pmin=? [ F f_j1=1 & f_j3=0 ])"; //false + + storm::prism::Program program = storm::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, ""); + std::vector> formulas = storm::parseFormulasForPrismProgram(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::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(1.3, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); + + std::unique_ptr result2 = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[1]->asMultiObjectiveFormula()); + ASSERT_TRUE(result2->isExplicitQualitativeCheckResult()); + EXPECT_FALSE(result2->asExplicitQualitativeCheckResult()[initState]); +} + +TEST(SparseMaPcaaModelCheckerTest, jobscheduler_pareto_2Obj) { + + std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma"; + std::string formulasAsString = "multi( Pmax=? [ F<=0.1 num_finished=1], Pmin=? [F<=0.2 num_finished=3]) "; + + storm::prism::Program program = storm::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, ""); + std::vector> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program); + std::shared_ptr> ma = storm::buildSparseModel(program, formulas)->as>(); + + std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula()); + ASSERT_TRUE(result->isParetoCurveCheckResult()); + + 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::createDownwardClosure( + 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(expectedAchievableValues->minkowskiSum(bloatingBox)->contains(result->asParetoCurveCheckResult().getUnderApproximation()->convertNumberRepresentation())); + EXPECT_TRUE(result->asParetoCurveCheckResult().getOverApproximation()->convertNumberRepresentation()->minkowskiSum(bloatingBox)->contains(expectedAchievableValues)); + +} #endif /* STORM_HAVE_HYPRO */ diff --git a/src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp b/src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp index 4918f5c5b..c25872e9c 100644 --- a/src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp +++ b/src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp @@ -26,8 +26,6 @@ TEST(SparseMdpPcaaModelCheckerTest, consensus) { std::shared_ptr> mdp = storm::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin();; - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); - std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); EXPECT_NEAR(0.10833260970000025, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); @@ -54,8 +52,6 @@ TEST(SparseMdpPcaaModelCheckerTest, zeroconf) { std::shared_ptr> mdp = storm::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); - std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); EXPECT_NEAR(0.0003075787401574803, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); @@ -73,8 +69,6 @@ TEST(SparseMdpPcaaModelCheckerTest, team3with3objectives) { std::shared_ptr> mdp = storm::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); - std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); EXPECT_NEAR(0.7448979591841851, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision()); @@ -92,8 +86,6 @@ TEST(SparseMdpPcaaModelCheckerTest, scheduler) { std::shared_ptr> mdp = storm::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); - std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula()); EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); } @@ -110,8 +102,6 @@ TEST(SparseMdpPcaaModelCheckerTest, dpm) { std::shared_ptr> mdp = storm::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); - storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); - std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); EXPECT_NEAR(121.61288, result->asExplicitQuantitativeCheckResult()[initState], storm::settings::getModule().getPrecision());