diff --git a/examples/multiobjective/ma/server/server.csl b/examples/multiobjective/ma/server/server.csl new file mode 100644 index 000000000..41a74ec79 --- /dev/null +++ b/examples/multiobjective/ma/server/server.csl @@ -0,0 +1 @@ +multi(Tmax=? [ F "error" ], Pmax=? [ F "processB" ]) diff --git a/examples/multiobjective/ma/server/server.ma b/examples/multiobjective/ma/server/server.ma new file mode 100644 index 000000000..d82c32474 --- /dev/null +++ b/examples/multiobjective/ma/server/server.ma @@ -0,0 +1,34 @@ + +ma + +const double rateProcessing = 2; +const double rateA = 1; +const double rateB = 1; + +module server + + s : [0..5]; // current state: + // 0: wait for request + // 1: received request from A + // 2: received request from B + // 3: starting to process request of B + // 4: processing request + // 5: error + + + + <> s=0 -> rateA : (s'=1) + rateB : (s'=2); + [alpha] s=1 -> 1 : (s'=4); + [alpha] s=2 -> 1 : (s'=3); + [beta] s=2 -> 0.5 : (s'=0) + 0.5 : (s'=3); + [] s=3 -> 1 : (s'=4); + <> s=4 -> rateProcessing : (s'=0) + (rateA+rateB) : (s'=5); + <> s=5 -> 1 : true; + +endmodule + + +label "error" = (s=5); +label "processB" = (s=3); + + diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp index a93134240..eb728b19e 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp @@ -328,7 +328,7 @@ namespace storm { } } } else if(formula.isReachabilityTimeFormula() && data.preprocessedModel.isOfType(storm::models::ModelType::MarkovAutomaton)) { - objectiveRewards = RewardModelType(std::vector(data.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero())); + objectiveRewards = RewardModelType(std::vector(data.preprocessedModel.getNumberOfStates(), storm::utility::zero())); storm::utility::vector::setVectorValues(objectiveRewards.getStateRewardVector(), data.getMarkovianStatesOfPreprocessedModel() & duplicatorResult.firstCopy, storm::utility::one()); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The formula " << formula << " neither considers reachability probabilities nor reachability rewards " << (data.preprocessedModel.isOfType(storm::models::ModelType::MarkovAutomaton) ? "nor reachability time" : "") << ". This is not supported."); diff --git a/test/functional/modelchecker/SparseMaMultiObjectiveModelCheckerTest.cpp b/test/functional/modelchecker/SparseMaMultiObjectiveModelCheckerTest.cpp new file mode 100644 index 000000000..3b630533e --- /dev/null +++ b/test/functional/modelchecker/SparseMaMultiObjectiveModelCheckerTest.cpp @@ -0,0 +1,50 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#ifdef STORM_HAVE_HYPRO + +#include "src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.h" +#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "src/modelchecker/results/ParetoCurveCheckResult.h" +#include "src/models/sparse/MarkovAutomaton.h" +#include "src/storage/geometry/Polytope.h" +#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/SettingsManager.h" +#include "src/utility/storm.h" + + + +TEST(SparseMdpMultiObjectiveModelCheckerTest, server) { + + std::string programFile = STORM_CPP_BASE_PATH "/examples/multiobjective/ma/server/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::parseFormulasForProgram(formulasAsString, program); + storm::generator::NextStateGeneratorOptions options(formulas); + std::shared_ptr> ma = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); + + storm::modelchecker::SparseMaMultiObjectiveModelChecker> checker(*ma); + + std::unique_ptr result = checker.check(storm::modelchecker::CheckTask(*formulas[0], true)); + ASSERT_TRUE(result->isParetoCurveCheckResult()); + + 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->asParetoCurveCheckResult().getUnderApproximation())); + EXPECT_TRUE(result->asParetoCurveCheckResult().getUnderApproximation()->contains(expectedAchievableValues)); + +} + + + +#endif /* STORM_HAVE_HYPRO */