Browse Source

added a few more tests for multi-objective MAs. Also fixed/improved minor stuff.

tempestpy_adaptions
TimQu 8 years ago
parent
commit
c1063f27cc
  1. 43
      resources/examples/testfiles/ma/jobscheduler.ma
  2. 1
      src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp
  3. 7
      src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp
  4. 2
      src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp
  5. 1
      src/storm/models/sparse/MarkovAutomaton.cpp
  6. 134
      src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp
  7. 10
      src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp

43
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

1
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"

7
src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp

@ -38,9 +38,10 @@ namespace storm {
// obtain the data for the checkresult
std::vector<std::vector<typename SparseModelType::ValueType>> paretoOptimalPoints;
paretoOptimalPoints.reserve(this->refinementSteps.size());
for(auto const& step : this->refinementSteps) {
paretoOptimalPoints.push_back(storm::utility::vector::convertNumericVector<typename SparseModelType::ValueType>(this->transformPointToOriginalModel(step.lowerBoundPoint)));
std::vector<Point> vertices = this->underApproximation->getVertices();
paretoOptimalPoints.reserve(vertices.size());
for(auto const& vertex : vertices) {
paretoOptimalPoints.push_back(storm::utility::vector::convertNumericVector<typename SparseModelType::ValueType>(this->transformPointToOriginalModel(vertex)));
}
return std::unique_ptr<CheckResult>(new ParetoCurveCheckResult<typename SparseModelType::ValueType>(this->originalModel.getInitialStates().getNextSetIndex(0),
std::move(paretoOptimalPoints),

2
src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp

@ -117,7 +117,7 @@ namespace storm {
template <class SparseModelType>
void SparsePcaaWeightVectorChecker<SparseModelType>::unboundedWeightedPhase(std::vector<ValueType> const& weightedRewardVector) {
if(this->objectivesWithNoUpperTimeBound.empty()) {
if(this->objectivesWithNoUpperTimeBound.empty() || !storm::utility::vector::hasNonZeroEntry(weightedRewardVector)) {
this->weightedResult = std::vector<ValueType>(model.getNumberOfStates(), storm::utility::zero<ValueType>());
this->scheduler = storm::storage::TotalScheduler(model.getNumberOfStates());
return;

1
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<std::string, RewardModelType> rewardModels = this->getRewardModels();
return std::make_shared<storm::models::sparse::Ctmc<ValueType, RewardModelType>>(std::move(rateMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling));

134
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<storm::RationalNumber> q = {q1, q2};
auto expectedAchievableValues = storm::storage::geometry::Polytope<storm::RationalNumber>::createDownwardClosure(std::vector<std::vector<storm::RationalNumber>>({p,q}));
EXPECT_TRUE(expectedAchievableValues->contains(result->asParetoCurveCheckResult<storm::RationalNumber>().getUnderApproximation()));
EXPECT_TRUE(result->asParetoCurveCheckResult<storm::RationalNumber>().getUnderApproximation()->contains(expectedAchievableValues));
EXPECT_TRUE(result->asParetoCurveCheckResult<storm::RationalNumber>().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<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program);
std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> ma = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::MarkovAutomaton<double>>();
storm::modelchecker::SparseMarkovAutomatonCslModelChecker<storm::models::sparse::MarkovAutomaton<double>> checker(*ma);
std::unique_ptr<storm::modelchecker::CheckResult> 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<double> p = {11.0/6.0, 1.0/2.0};
std::vector<double> q = {29.0/18.0, 2.0/3.0};
auto expectedAchievableValues = storm::storage::geometry::Polytope<double>::createDownwardClosure(std::vector<std::vector<double>>({p,q}));
auto expectedAchievableValues = storm::storage::geometry::Polytope<storm::RationalNumber>::createDownwardClosure(
std::vector<std::vector<storm::RationalNumber>>({storm::utility::vector::convertNumericVector<storm::RationalNumber>(p),
storm::utility::vector::convertNumericVector<storm::RationalNumber>(q)}));
// due to precision issues, we enlarge one of the polytopes before checking containement
std::vector<double> lb = {-storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision(), -storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()};
std::vector<double> ub = {storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision(), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()};
auto bloatingBox = storm::storage::geometry::Hyperrectangle<double>(lb,ub).asPolytope();
EXPECT_TRUE(expectedAchievableValues->minkowskiSum(bloatingBox)->contains(result->asParetoCurveCheckResult<double>().getUnderApproximation()));
EXPECT_TRUE(result->asParetoCurveCheckResult<double>().getUnderApproximation()->minkowskiSum(bloatingBox)->contains(expectedAchievableValues));
storm::RationalNumber eps = storm::utility::convertNumber<storm::RationalNumber>(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
std::vector<storm::RationalNumber> lb(2,-eps), ub(2,eps);
auto bloatingBox = storm::storage::geometry::Hyperrectangle<storm::RationalNumber>(lb,ub).asPolytope();
EXPECT_TRUE(expectedAchievableValues->minkowskiSum(bloatingBox)->contains(result->asParetoCurveCheckResult<double>().getUnderApproximation()->convertNumberRepresentation<storm::RationalNumber>()));
EXPECT_TRUE(result->asParetoCurveCheckResult<double>().getOverApproximation()->convertNumberRepresentation<storm::RationalNumber>()->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<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program);
std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> ma = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::MarkovAutomaton<double>>();
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isParetoCurveCheckResult());
std::vector<double> j12 = {1.266666667,0.1617571721,0.5};
std::vector<double> j13 = {1.283333333,0.1707737575,0.25};
std::vector<double> 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<storm::RationalNumber>::createDownwardClosure(
std::vector<std::vector<storm::RationalNumber>>({storm::utility::vector::convertNumericVector<storm::RationalNumber>(j12),
storm::utility::vector::convertNumericVector<storm::RationalNumber>(j13),
storm::utility::vector::convertNumericVector<storm::RationalNumber>(j23)}));
// due to precision issues, we enlarge one of the polytopes before checking containement
storm::RationalNumber eps = storm::utility::convertNumber<storm::RationalNumber>(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
std::vector<storm::RationalNumber> lb(3,-eps), ub(3,eps);
auto bloatingBox = storm::storage::geometry::Hyperrectangle<storm::RationalNumber>(lb,ub).asPolytope();
EXPECT_TRUE(expectedAchievableValues->minkowskiSum(bloatingBox)->contains(result->asParetoCurveCheckResult<double>().getUnderApproximation()->convertNumberRepresentation<storm::RationalNumber>()));
EXPECT_TRUE(result->asParetoCurveCheckResult<double>().getOverApproximation()->convertNumberRepresentation<storm::RationalNumber>()->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<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program);
std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> ma = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::MarkovAutomaton<double>>();
uint_fast64_t const initState = *ma->getInitialStates().begin();
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isExplicitQualitativeCheckResult());
EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
std::unique_ptr<storm::modelchecker::CheckResult> 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<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program);
std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> ma = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::MarkovAutomaton<double>>();
uint_fast64_t const initState = *ma->getInitialStates().begin();
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
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::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<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program);
std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> ma = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::MarkovAutomaton<double>>();
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isParetoCurveCheckResult());
std::vector<double> j12 = {0.2591835573, 0.01990529674};
std::vector<double> j13 = {0.329682099, 0.01970194998};
std::vector<double> 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<storm::RationalNumber>::createDownwardClosure(
std::vector<std::vector<storm::RationalNumber>>({storm::utility::vector::convertNumericVector<storm::RationalNumber>(j12),
storm::utility::vector::convertNumericVector<storm::RationalNumber>(j13),
storm::utility::vector::convertNumericVector<storm::RationalNumber>(j23)}));
// due to precision issues, we enlarge one of the polytopes before checking containement
storm::RationalNumber eps = storm::utility::convertNumber<storm::RationalNumber>(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
std::vector<storm::RationalNumber> lb(2,-eps), ub(2,eps);
auto bloatingBox = storm::storage::geometry::Hyperrectangle<storm::RationalNumber>(lb,ub).asPolytope();
EXPECT_TRUE(expectedAchievableValues->minkowskiSum(bloatingBox)->contains(result->asParetoCurveCheckResult<double>().getUnderApproximation()->convertNumberRepresentation<storm::RationalNumber>()));
EXPECT_TRUE(result->asParetoCurveCheckResult<double>().getOverApproximation()->convertNumberRepresentation<storm::RationalNumber>()->minkowskiSum(bloatingBox)->contains(expectedAchievableValues));
}
#endif /* STORM_HAVE_HYPRO */

10
src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp

@ -26,8 +26,6 @@ TEST(SparseMdpPcaaModelCheckerTest, consensus) {
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>();
uint_fast64_t const initState = *mdp->getInitialStates().begin();;
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
EXPECT_NEAR(0.10833260970000025, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
@ -54,8 +52,6 @@ TEST(SparseMdpPcaaModelCheckerTest, zeroconf) {
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>();
uint_fast64_t const initState = *mdp->getInitialStates().begin();
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
EXPECT_NEAR(0.0003075787401574803, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
@ -73,8 +69,6 @@ TEST(SparseMdpPcaaModelCheckerTest, team3with3objectives) {
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>();
uint_fast64_t const initState = *mdp->getInitialStates().begin();
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
EXPECT_NEAR(0.7448979591841851, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
@ -92,8 +86,6 @@ TEST(SparseMdpPcaaModelCheckerTest, scheduler) {
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>();
uint_fast64_t const initState = *mdp->getInitialStates().begin();
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula());
EXPECT_TRUE(result->asExplicitQualitativeCheckResult()[initState]);
}
@ -110,8 +102,6 @@ TEST(SparseMdpPcaaModelCheckerTest, dpm) {
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>();
uint_fast64_t const initState = *mdp->getInitialStates().begin();
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
EXPECT_NEAR(121.61288, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());

Loading…
Cancel
Save