-
Notifications
You must be signed in to change notification settings - Fork 75
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Revised LP Encoding for Multi-objective verification under simple str…
…ategies (#468) * Update findGUROBI.cmake to find Gurobi 11 * Revised implementation of multi-objective Achievability under simple strategies * Added support for achievability queries
- Loading branch information
Showing
18 changed files
with
2,007 additions
and
1,473 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,19 @@ | ||
| mdp | ||
| module main | ||
|
|
||
| x : [0..2]; | ||
| [a] x=0 -> (x'=1); | ||
| [b] x=0 -> (x'=2); | ||
| [c] x=1 -> (x'=1); | ||
| [d] x=1 -> (x'=2); | ||
| [e] x=2 -> (x'=1); | ||
| endmodule | ||
|
|
||
| rewards "one" | ||
| [b] true : 10; | ||
| [c] true : 1; | ||
| endrewards | ||
|
|
||
| rewards "two" | ||
| [e] true : 1; | ||
| endrewards |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
90 changes: 90 additions & 0 deletions
90
...delchecker/multiobjective/deterministicScheds/DeterministicSchedsAchievabilityChecker.cpp
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,90 @@ | ||
| #include "storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsAchievabilityChecker.h" | ||
|
|
||
| #include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h" | ||
| #include "storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h" | ||
| #include "storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.h" | ||
| #include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h" | ||
| #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" | ||
| #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" | ||
| #include "storm/models/sparse/MarkovAutomaton.h" | ||
| #include "storm/models/sparse/Mdp.h" | ||
| #include "storm/models/sparse/StandardRewardModel.h" | ||
|
|
||
| namespace storm::modelchecker::multiobjective { | ||
|
|
||
| template<class SparseModelType, typename GeometryValueType> | ||
| DeterministicSchedsAchievabilityChecker<SparseModelType, GeometryValueType>::DeterministicSchedsAchievabilityChecker( | ||
| preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult) | ||
| : model(preprocessorResult.preprocessedModel), originalModelInitialState(*preprocessorResult.originalModel.getInitialStates().begin()) { | ||
| for (auto const& obj : preprocessorResult.objectives) { | ||
| objectiveHelper.emplace_back(*model, obj); | ||
| if (!objectiveHelper.back().hasThreshold()) { | ||
| STORM_LOG_ASSERT(!optimizingObjectiveIndex.has_value(), | ||
| "Unexpected input: got a (quantitative) achievability query but there are more than one objectives without a threshold."); | ||
| optimizingObjectiveIndex = objectiveHelper.size() - 1; | ||
| } | ||
| } | ||
| lpChecker = std::make_shared<DeterministicSchedsLpChecker<SparseModelType, GeometryValueType>>(*model, objectiveHelper); | ||
| } | ||
|
|
||
| template<class SparseModelType, typename GeometryValueType> | ||
| std::unique_ptr<CheckResult> DeterministicSchedsAchievabilityChecker<SparseModelType, GeometryValueType>::check(Environment const& env) { | ||
| using Point = typename std::vector<GeometryValueType>; | ||
| uint64_t const numObj = objectiveHelper.size(); | ||
| // Create a polytope that contains all the points that would certify achievability of the point induced by the objective threshold | ||
| std::vector<storm::storage::geometry::Halfspace<GeometryValueType>> thresholdHalfspaces; | ||
| std::vector<GeometryValueType> objVector; | ||
| for (uint64_t objIndex = 0; objIndex < numObj; ++objIndex) { | ||
| auto& obj = objectiveHelper[objIndex]; | ||
| obj.computeLowerUpperBounds(env); | ||
| if (!optimizingObjectiveIndex.has_value() || *optimizingObjectiveIndex != objIndex) { | ||
| objVector.assign(numObj, storm::utility::zero<GeometryValueType>()); | ||
| objVector[objIndex] = -storm::utility::one<GeometryValueType>(); | ||
| thresholdHalfspaces.emplace_back(objVector, storm::utility::convertNumber<GeometryValueType, ModelValueType>(-obj.getThreshold())); | ||
| } | ||
| } | ||
| auto thresholdPolytope = storm::storage::geometry::Polytope<GeometryValueType>::create(std::move(thresholdHalfspaces)); | ||
|
|
||
| // Set objective weights (none if this is a qualitative achievability query) | ||
| objVector.assign(numObj, storm::utility::zero<GeometryValueType>()); | ||
| auto eps = objVector; | ||
| if (optimizingObjectiveIndex.has_value()) { | ||
| objVector[*optimizingObjectiveIndex] = storm::utility::one<GeometryValueType>(); | ||
| eps[*optimizingObjectiveIndex] = env.modelchecker().multi().getPrecision() * storm::utility::convertNumber<GeometryValueType, uint64_t>(2u); | ||
| if (env.modelchecker().multi().getPrecisionType() == MultiObjectiveModelCheckerEnvironment::PrecisionType::RelativeToDiff) { | ||
| eps[*optimizingObjectiveIndex] *= storm::utility::convertNumber<GeometryValueType, ModelValueType>( | ||
| objectiveHelper[*optimizingObjectiveIndex].getUpperValueBoundAtState(originalModelInitialState) - | ||
| objectiveHelper[*optimizingObjectiveIndex].getLowerValueBoundAtState(originalModelInitialState)); | ||
| } | ||
| STORM_LOG_INFO("Computing quantitative achievability value with precision " << eps[*optimizingObjectiveIndex] << "."); | ||
| } | ||
| lpChecker->setCurrentWeightVector(env, objVector); | ||
|
|
||
| // Search achieving point | ||
| auto achievingPoint = lpChecker->check(env, thresholdPolytope, eps); | ||
| bool const isAchievable = achievingPoint.has_value(); | ||
| if (isAchievable) { | ||
| STORM_LOG_INFO( | ||
| "Found achievable point: " << storm::utility::vector::toString(achievingPoint->first) << " ( approx. " | ||
| << storm::utility::vector::toString(storm::utility::vector::convertNumericVector<double>(achievingPoint->first)) | ||
| << " )."); | ||
| if (optimizingObjectiveIndex.has_value()) { | ||
| using ValueType = typename SparseModelType::ValueType; | ||
| // Average between obtained lower- and upper bounds | ||
| auto result = | ||
| storm::utility::convertNumber<ValueType, GeometryValueType>(achievingPoint->first[*optimizingObjectiveIndex] + achievingPoint->second); | ||
| result /= storm::utility::convertNumber<ValueType, uint64_t>(2u); | ||
| if (objectiveHelper[*optimizingObjectiveIndex].minimizing()) { | ||
| result *= -storm::utility::one<ValueType>(); | ||
| } | ||
| return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>>(originalModelInitialState, result); | ||
| } | ||
| } | ||
| return std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult>(originalModelInitialState, isAchievable); | ||
| } | ||
|
|
||
| template class DeterministicSchedsAchievabilityChecker<storm::models::sparse::Mdp<double>, storm::RationalNumber>; | ||
| template class DeterministicSchedsAchievabilityChecker<storm::models::sparse::Mdp<storm::RationalNumber>, storm::RationalNumber>; | ||
| template class DeterministicSchedsAchievabilityChecker<storm::models::sparse::MarkovAutomaton<double>, storm::RationalNumber>; | ||
| template class DeterministicSchedsAchievabilityChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>, storm::RationalNumber>; | ||
| } // namespace storm::modelchecker::multiobjective |
46 changes: 46 additions & 0 deletions
46
...modelchecker/multiobjective/deterministicScheds/DeterministicSchedsAchievabilityChecker.h
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,46 @@ | ||
| #pragma once | ||
|
|
||
| #include <memory> | ||
| #include <optional> | ||
| #include <vector> | ||
|
|
||
| namespace storm { | ||
| class Environment; | ||
|
|
||
| namespace modelchecker { | ||
|
|
||
| class CheckResult; | ||
|
|
||
| namespace multiobjective { | ||
| template<typename SparseModelType, typename GeometryValueType> | ||
| class DeterministicSchedsLpChecker; | ||
|
|
||
| template<typename SparseModelType> | ||
| class DeterministicSchedsObjectiveHelper; | ||
|
|
||
| namespace preprocessing { | ||
| template<typename SparseModelType> | ||
| class SparseMultiObjectivePreprocessorResult; | ||
| } | ||
|
|
||
| template<class SparseModelType, typename GeometryValueType> | ||
| class DeterministicSchedsAchievabilityChecker { | ||
| public: | ||
| typedef typename SparseModelType::ValueType ModelValueType; | ||
|
|
||
| DeterministicSchedsAchievabilityChecker(preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult); | ||
|
|
||
| virtual std::unique_ptr<CheckResult> check(Environment const& env); | ||
|
|
||
| private: | ||
| std::shared_ptr<DeterministicSchedsLpChecker<SparseModelType, GeometryValueType>> lpChecker; | ||
| std::vector<DeterministicSchedsObjectiveHelper<SparseModelType>> objectiveHelper; | ||
|
|
||
| std::shared_ptr<SparseModelType> model; | ||
| uint64_t const originalModelInitialState; | ||
| std::optional<uint64_t> optimizingObjectiveIndex; | ||
| }; | ||
|
|
||
| } // namespace multiobjective | ||
| } // namespace modelchecker | ||
| } // namespace storm |
Oops, something went wrong.