sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Multi-objective tests now set the method via the environment

tempestpy_adaptions
TimQu 7 years ago
parent
7cee81a223
commit
918dc349fb
4 changed files with 45 additions and 24 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 6
      src/test/storm/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp
  2. 25
      src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp
  3. 15
      src/test/storm/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp
  4. 23
      src/test/storm/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp

6
src/test/storm/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp
View File

@ -1,6 +1,7 @@
#include "gtest/gtest.h" #include "gtest/gtest.h"
#include "storm-config.h" #include "storm-config.h"
#include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h"
#include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h" #include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
@ -14,6 +15,7 @@
TEST(SparseMaCbMultiObjectiveModelCheckerTest, server) { TEST(SparseMaCbMultiObjectiveModelCheckerTest, server) {
storm::Environment env; storm::Environment env;
env.modelchecker().multi().setMethod(storm::modelchecker::multiobjective::MultiObjectiveMethod::ConstraintBased);
std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/server.ma"; std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/server.ma";
std::string formulasAsString = "multi(T>=5/3 [ F \"error\" ], P>=7/12 [ F \"processB\" ]) "; // true std::string formulasAsString = "multi(T>=5/3 [ F \"error\" ], P>=7/12 [ F \"processB\" ]) "; // true
@ -27,11 +29,11 @@ TEST(SparseMaCbMultiObjectiveModelCheckerTest, server) {
std::unique_ptr<storm::modelchecker::CheckResult> result; std::unique_ptr<storm::modelchecker::CheckResult> result;
result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased);
result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[0]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[1]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased);
result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[1]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]);
} }

25
src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp
View File

@ -4,6 +4,8 @@
#if defined STORM_HAVE_HYPRO || defined STORM_HAVE_Z3_OPTIMIZE #if defined STORM_HAVE_HYPRO || defined STORM_HAVE_Z3_OPTIMIZE
#include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h" #include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h"
#include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h" #include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h"
@ -19,6 +21,8 @@
TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, serverRationalNumbers) { TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, serverRationalNumbers) {
storm::Environment env; storm::Environment env;
env.modelchecker().multi().setMethod(storm::modelchecker::multiobjective::MultiObjectiveMethod::Pcaa);
std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/server.ma"; std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/server.ma";
std::string formulasAsString = "multi(Tmax=? [ F \"error\" ], Pmax=? [ F \"processB\" ]) "; // pareto std::string formulasAsString = "multi(Tmax=? [ F \"error\" ], Pmax=? [ F \"processB\" ]) "; // pareto
@ -30,7 +34,7 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, serverRationalNumbers) {
storm::generator::NextStateGeneratorOptions options(formulas); storm::generator::NextStateGeneratorOptions options(formulas);
std::shared_ptr<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>> ma = storm::builder::ExplicitModelBuilder<storm::RationalNumber>(program, options).build()->as<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>(); std::shared_ptr<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>> ma = storm::builder::ExplicitModelBuilder<storm::RationalNumber>(program, options).build()->as<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>();
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa);
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[0]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
storm::RationalNumber p1 = storm::utility::convertNumber<storm::RationalNumber>(11.0); p1 /= storm::utility::convertNumber<storm::RationalNumber>(6.0); storm::RationalNumber p1 = storm::utility::convertNumber<storm::RationalNumber>(11.0); p1 /= storm::utility::convertNumber<storm::RationalNumber>(6.0);
@ -48,6 +52,7 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, serverRationalNumbers) {
TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, server) { TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, server) {
storm::Environment env; storm::Environment env;
env.modelchecker().multi().setMethod(storm::modelchecker::multiobjective::MultiObjectiveMethod::Pcaa);
std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/server.ma"; std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/server.ma";
std::string formulasAsString = "multi(Tmax=? [ F \"error\" ], Pmax=? [ F \"processB\" ]) "; // pareto std::string formulasAsString = "multi(Tmax=? [ F \"error\" ], Pmax=? [ F \"processB\" ]) "; // pareto
@ -57,7 +62,7 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, server) {
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> ma = storm::api::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::MarkovAutomaton<double>>(); std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> ma = storm::api::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::MarkovAutomaton<double>>();
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa);
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[0]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
// we do our checks with rationals to avoid numerical issues when doing polytope computations... // we do our checks with rationals to avoid numerical issues when doing polytope computations...
@ -78,6 +83,7 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, server) {
TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_pareto_3Obj) { TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_pareto_3Obj) {
storm::Environment env; storm::Environment env;
env.modelchecker().multi().setMethod(storm::modelchecker::multiobjective::MultiObjectiveMethod::Pcaa);
std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma"; 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\" ]) "; std::string formulasAsString = "multi(Tmin=? [ F \"all_jobs_finished\" ], Pmax=? [ F<=0.2 \"half_of_jobs_finished\" ], Pmin=? [ F \"slowest_before_fastest\" ]) ";
@ -87,7 +93,7 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_pareto_3Obj) {
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> ma = storm::api::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::MarkovAutomaton<double>>(); std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> ma = storm::api::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::MarkovAutomaton<double>>();
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa);
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[0]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
std::vector<double> j12 = {1.266666667,0.1617571721,0.5}; std::vector<double> j12 = {1.266666667,0.1617571721,0.5};
@ -109,6 +115,7 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_pareto_3Obj) {
TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_achievability_3Obj) { TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_achievability_3Obj) {
storm::Environment env; storm::Environment env;
env.modelchecker().multi().setMethod(storm::modelchecker::multiobjective::MultiObjectiveMethod::Pcaa);
std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma"; 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 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
@ -120,17 +127,18 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_achievability_3Obj
std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> ma = storm::api::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::MarkovAutomaton<double>>(); std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> ma = storm::api::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::MarkovAutomaton<double>>();
uint_fast64_t const initState = *ma->getInitialStates().begin(); uint_fast64_t const initState = *ma->getInitialStates().begin();
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa);
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[0]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
std::unique_ptr<storm::modelchecker::CheckResult> result2 = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[1]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa);
std::unique_ptr<storm::modelchecker::CheckResult> result2 = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[1]->asMultiObjectiveFormula());
ASSERT_TRUE(result2->isExplicitQualitativeCheckResult()); ASSERT_TRUE(result2->isExplicitQualitativeCheckResult());
EXPECT_FALSE(result2->asExplicitQualitativeCheckResult()[initState]); EXPECT_FALSE(result2->asExplicitQualitativeCheckResult()[initState]);
} }
TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_quantitative_3Obj) { TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_quantitative_3Obj) {
storm::Environment env; storm::Environment env;
env.modelchecker().multi().setMethod(storm::modelchecker::multiobjective::MultiObjectiveMethod::Pcaa);
std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma"; 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 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
@ -143,17 +151,18 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_quantitative_3Obj)
uint_fast64_t const initState = *ma->getInitialStates().begin(); uint_fast64_t const initState = *ma->getInitialStates().begin();
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa);
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[0]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
EXPECT_NEAR(1.3, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getPrecision()); EXPECT_NEAR(1.3, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getPrecision());
std::unique_ptr<storm::modelchecker::CheckResult> result2 = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[1]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa);
std::unique_ptr<storm::modelchecker::CheckResult> result2 = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[1]->asMultiObjectiveFormula());
ASSERT_TRUE(result2->isExplicitQualitativeCheckResult()); ASSERT_TRUE(result2->isExplicitQualitativeCheckResult());
EXPECT_FALSE(result2->asExplicitQualitativeCheckResult()[initState]); EXPECT_FALSE(result2->asExplicitQualitativeCheckResult()[initState]);
} }
TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_pareto_2Obj) { TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_pareto_2Obj) {
storm::Environment env; storm::Environment env;
env.modelchecker().multi().setMethod(storm::modelchecker::multiobjective::MultiObjectiveMethod::Pcaa);
std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma"; 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\"]) "; std::string formulasAsString = "multi( Pmax=? [ F<=0.1 \"one_job_finished\"], Pmin=? [F<=0.2 \"all_jobs_finished\"]) ";
@ -163,7 +172,7 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_pareto_2Obj) {
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> ma = storm::api::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::MarkovAutomaton<double>>(); std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> ma = storm::api::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::MarkovAutomaton<double>>();
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa);
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[0]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
std::vector<double> j12 = {0.2591835573, 0.01990529674}; std::vector<double> j12 = {0.2591835573, 0.01990529674};

15
src/test/storm/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp
View File

@ -1,6 +1,7 @@
#include "gtest/gtest.h" #include "gtest/gtest.h"
#include "storm-config.h" #include "storm-config.h"
#include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h"
#include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h" #include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/Mdp.h"
@ -12,7 +13,8 @@
TEST(SparseMdpCbMultiObjectiveModelCheckerTest, consensus) { TEST(SparseMdpCbMultiObjectiveModelCheckerTest, consensus) {
storm::Environment env; storm::Environment env;
env.modelchecker().multi().setMethod(storm::modelchecker::multiobjective::MultiObjectiveMethod::ConstraintBased);
std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_consensus2_3_2.nm"; std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_consensus2_3_2.nm";
std::string formulasAsString = "multi(Pmax=? [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ]) "; // numerical std::string formulasAsString = "multi(Pmax=? [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ]) "; // numerical
formulasAsString += "; \n multi(P>=0.1 [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ])"; // achievability (true) formulasAsString += "; \n multi(P>=0.1 [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ])"; // achievability (true)
@ -27,11 +29,11 @@ TEST(SparseMdpCbMultiObjectiveModelCheckerTest, consensus) {
std::unique_ptr<storm::modelchecker::CheckResult> result; std::unique_ptr<storm::modelchecker::CheckResult> result;
result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[1]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased);
result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[1]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[2]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased);
result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[2]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]);
@ -39,6 +41,7 @@ TEST(SparseMdpCbMultiObjectiveModelCheckerTest, consensus) {
TEST(SparseMdpCbMultiObjectiveModelCheckerTest, zeroconf) { TEST(SparseMdpCbMultiObjectiveModelCheckerTest, zeroconf) {
storm::Environment env; storm::Environment env;
env.modelchecker().multi().setMethod(storm::modelchecker::multiobjective::MultiObjectiveMethod::ConstraintBased);
std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_zeroconf4.nm"; std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_zeroconf4.nm";
std::string formulasAsString = "multi(P>=0.0003 [ 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
@ -50,14 +53,14 @@ TEST(SparseMdpCbMultiObjectiveModelCheckerTest, zeroconf) {
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp = storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>(); std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp = storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
uint_fast64_t const initState = *mdp->getInitialStates().begin(); uint_fast64_t const initState = *mdp->getInitialStates().begin();
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased);
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
} }
/* This test takes a little bit too long ... /* This test takes a little bit too long ...
TEST(SparseMdpCbMultiObjectiveModelCheckerTest, team3with3objectives) { TEST(SparseMdpCbMultiObjectiveModelCheckerTest, team3with3objectives) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_team3.nm"; std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_team3.nm";
std::string formulasAsString = "multi(P>=0.75 [ 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
@ -68,7 +71,7 @@ TEST(SparseMdpCbMultiObjectiveModelCheckerTest, team3with3objectives) {
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp = storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>(); std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> mdp = storm::api::buildSparseModel<storm::RationalNumber>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
uint_fast64_t const initState = *mdp->getInitialStates().begin(); uint_fast64_t const initState = *mdp->getInitialStates().begin();
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::ConstraintBased);
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(*mdp, formulas[0]->asMultiObjectiveFormula())
ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]);
} }

23
src/test/storm/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp
View File

@ -4,6 +4,8 @@
#if defined STORM_HAVE_HYPRO || defined STORM_HAVE_Z3_OPTIMIZE #if defined STORM_HAVE_HYPRO || defined STORM_HAVE_Z3_OPTIMIZE
#include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h" #include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h"
#include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/Mdp.h"
@ -14,6 +16,7 @@
TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, consensus) { TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, consensus) {
storm::Environment env; storm::Environment env;
env.modelchecker().multi().setMethod(storm::modelchecker::multiobjective::MultiObjectiveMethod::Pcaa);
std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_consensus2_3_2.nm"; std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_consensus2_3_2.nm";
std::string formulasAsString = "multi(Pmax=? [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ]) "; // numerical std::string formulasAsString = "multi(Pmax=? [ F \"one_proc_err\" ], P>=0.8916673903 [ G \"one_coin_ok\" ]) "; // numerical
@ -27,15 +30,15 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, consensus) {
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::api::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>(); std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::api::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>();
uint_fast64_t const initState = *mdp->getInitialStates().begin();; uint_fast64_t const initState = *mdp->getInitialStates().begin();;
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa);
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
EXPECT_NEAR(0.10833260970000025, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); EXPECT_NEAR(0.10833260970000025, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[1]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa);
result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[1]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[2]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa);
result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[2]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isExplicitQualitativeCheckResult()); ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]); EXPECT_FALSE(result->asExplicitQualitativeCheckResult()[initState]);
@ -43,6 +46,7 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, consensus) {
TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, zeroconf) { TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, zeroconf) {
storm::Environment env; storm::Environment env;
env.modelchecker().multi().setMethod(storm::modelchecker::multiobjective::MultiObjectiveMethod::Pcaa);
std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_zeroconf4.nm"; 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(Pmax=? [ F l=4 & ip=1 ] , P>=0.993141[ G (error=0) ]) "; // numerical
@ -54,14 +58,15 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, zeroconf) {
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::api::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>(); std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::api::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>();
uint_fast64_t const initState = *mdp->getInitialStates().begin(); uint_fast64_t const initState = *mdp->getInitialStates().begin();
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa);
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
EXPECT_NEAR(0.0003075787401574803, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); EXPECT_NEAR(0.0003075787401574803, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
} }
TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, team3with3objectives) { TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, team3with3objectives) {
storm::Environment env; storm::Environment env;
env.modelchecker().multi().setMethod(storm::modelchecker::multiobjective::MultiObjectiveMethod::Pcaa);
std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_team3.nm"; 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(Pmax=? [ F \"task1_compl\" ], R{\"w_1_total\"}>=2.210204082 [ C ], P>=0.5 [ F \"task2_compl\" ])"; // numerical
@ -72,13 +77,14 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, team3with3objectives) {
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::api::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>(); std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::api::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>();
uint_fast64_t const initState = *mdp->getInitialStates().begin(); uint_fast64_t const initState = *mdp->getInitialStates().begin();
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa);
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
EXPECT_NEAR(0.7448979591841851, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); EXPECT_NEAR(0.7448979591841851, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
} }
TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, scheduler) { TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, scheduler) {
storm::Environment env; storm::Environment env;
env.modelchecker().multi().setMethod(storm::modelchecker::multiobjective::MultiObjectiveMethod::Pcaa);
std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_scheduler05.nm"; 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\" ]) "; std::string formulasAsString = "multi(R{\"time\"}<= 11.778[ F \"tasks_complete\" ], R{\"energy\"}<=1.45 [ F \"tasks_complete\" ]) ";
@ -90,12 +96,13 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, scheduler) {
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::api::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>(); std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::api::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>();
uint_fast64_t const initState = *mdp->getInitialStates().begin(); uint_fast64_t const initState = *mdp->getInitialStates().begin();
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa);
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula());
EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]); EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
} }
TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, dpm) { TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, dpm) {
storm::Environment env; storm::Environment env;
env.modelchecker().multi().setMethod(storm::modelchecker::multiobjective::MultiObjectiveMethod::Pcaa);
std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_dpm100.nm"; 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 std::string formulasAsString = "multi(R{\"power\"}min=? [ C<=100 ], R{\"queue\"}<=70 [ C<=100 ])"; // numerical
@ -107,7 +114,7 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, dpm) {
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::api::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>(); std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::api::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>();
uint_fast64_t const initState = *mdp->getInitialStates().begin(); uint_fast64_t const initState = *mdp->getInitialStates().begin();
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula(), storm::modelchecker::multiobjective::MultiObjectiveMethodSelection::Pcaa);
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *mdp, formulas[0]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
EXPECT_NEAR(121.6128842, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); EXPECT_NEAR(121.6128842, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
} }

Write Preview
Loading…
Cancel
Save