From 136084af755ac5678c3b904b8fa4619681f9bb41 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 21 Jun 2018 17:28:40 +0200 Subject: [PATCH] started implementing deterministic scheduler finding approach for multi-objective model checking --- .../MultiObjectivePostprocessing.cpp | 73 ++++ .../MultiObjectivePostprocessing.h | 21 + .../DeterministicParetoExplorer.cpp | 384 ++++++++++++++++++ .../DeterministicParetoExplorer.h | 174 ++++++++ .../MultiObjectiveSchedulerEvaluator.cpp | 32 ++ .../MultiObjectiveSchedulerEvaluator.h | 30 ++ 6 files changed, 714 insertions(+) create mode 100644 src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp create mode 100644 src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.h create mode 100644 src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicParetoExplorer.cpp create mode 100644 src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicParetoExplorer.h create mode 100644 src/storm/modelchecker/multiobjective/deterministicScheds/MultiObjectiveSchedulerEvaluator.cpp create mode 100644 src/storm/modelchecker/multiobjective/deterministicScheds/MultiObjectiveSchedulerEvaluator.h diff --git a/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp b/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp new file mode 100644 index 000000000..fd1f36f73 --- /dev/null +++ b/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp @@ -0,0 +1,73 @@ +#include "storm/modelchecker/multiobjective/MultiObjectivePostprocessing.h" + +#include "storm/adapters/RationalNumberAdapter.h" + +namespace storm { + namespace modelchecker { + namespace multiobjective { + + template + std::vector transformObjectiveValuesToOriginal(std::vector> objectives, std::vector const& point) { + std::vector result; + result.reserve(point.size()); + for (uint_fast64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) { + auto const& obj = objectives[objIndex]; + if (storm::solver::maximize(obj.formula->getOptimalityType())) { + if (obj.considersComplementaryEvent) { + result.push_back(storm::utility::one() - point[objIndex]); + } else { + result.push_back(point[objIndex]); + } + } else { + if (obj.considersComplementaryEvent) { + result.push_back(storm::utility::one() + point[objIndex]); + } else { + result.push_back(-point[objIndex]); + } + } + } + return result; + } + + template + std::shared_ptr> transformObjectivePolytopeToOriginal(std::vector> objectives, std::shared_ptr> const& polytope) { + if(polytope->isEmpty()) { + return storm::storage::geometry::Polytope::createEmptyPolytope(); + } + if(polytope->isUniversal()) { + return storm::storage::geometry::Polytope::createUniversalPolytope(); + } + uint_fast64_t numObjectives = objectives.size(); + std::vector> transformationMatrix(numObjectives, std::vector(numObjectives, storm::utility::zero())); + std::vector transformationVector; + transformationVector.reserve(numObjectives); + for(uint_fast64_t objIndex = 0; objIndex < numObjectives; ++objIndex) { + auto const& obj = objectives[objIndex]; + if (storm::solver::maximize(obj.formula->getOptimalityType())) { + if (obj.considersComplementaryEvent) { + transformationMatrix[objIndex][objIndex] = -storm::utility::one(); + transformationVector.push_back(storm::utility::one()); + } else { + transformationMatrix[objIndex][objIndex] = storm::utility::one(); + transformationVector.push_back(storm::utility::zero()); + } + } else { + if (obj.considersComplementaryEvent) { + transformationMatrix[objIndex][objIndex] = storm::utility::one(); + transformationVector.push_back(storm::utility::one()); + } else { + transformationMatrix[objIndex][objIndex] = -storm::utility::one(); + transformationVector.push_back(storm::utility::zero()); + } + } + } + return polytope->affineTransformation(transformationMatrix, transformationVector); + } + + template std::vector transformObjectiveValuesToOriginal(std::vector> objectives, std::vector const& point); + template std::shared_ptr> transformObjectivePolytopeToOriginal(std::vector> objectives, std::shared_ptr> const& polytope); + template std::vector transformObjectiveValuesToOriginal(std::vector> objectives, std::vector const& point); + template std::shared_ptr> transformObjectivePolytopeToOriginal(std::vector> objectives, std::shared_ptr> const& polytope); + } + } +} \ No newline at end of file diff --git a/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.h b/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.h new file mode 100644 index 000000000..58dd10230 --- /dev/null +++ b/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.h @@ -0,0 +1,21 @@ +#pragma once + +#include +#include + +#include "storm/modelchecker/multiobjective/Objective.h" +#include "storm/storage/geometry/Polytope.h" + +namespace storm { + namespace modelchecker { + namespace multiobjective { + + template + std::vector transformObjectiveValuesToOriginal(std::vector> objectives, std::vector const& point); + + template + std::shared_ptr> transformObjectivePolytopeToOriginal(std::vector> objectives, std::shared_ptr> const& polytope); + + } + } +} \ No newline at end of file diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicParetoExplorer.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicParetoExplorer.cpp new file mode 100644 index 000000000..5c15256e8 --- /dev/null +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicParetoExplorer.cpp @@ -0,0 +1,384 @@ +#include +#include + +#include "storm/modelchecker/multiobjective/deterministicScheds/DeterministicParetoExplorer.h" +#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/StandardRewardModel.h" + + +#include "storm/utility/export.h" + +#include "storm/exceptions/InvalidOperationException.h" + + +namespace storm { + namespace modelchecker { + namespace multiobjective { + + template + DeterministicParetoExplorer::Point::Point(std::vector const& coordinates) : coordinates(coordinates), paretoOptimal(false) { + STORM_LOG_ASSERT(!this->coordinates.empty(), "Points with dimension 0 are not supported"); + } + + template + DeterministicParetoExplorer::Point::Point(std::vector&& coordinates) : coordinates(std::move(coordinates)), paretoOptimal(false) { + STORM_LOG_ASSERT(!this->coordinates.empty(), "Points with dimension 0 are not supported"); + } + + template + std::vector& DeterministicParetoExplorer::Point::get() { + return coordinates; + } + + template + std::vector const& DeterministicParetoExplorer::Point::get() const { + return coordinates; + } + + template + uint64_t DeterministicParetoExplorer::Point::dimension() const { + STORM_LOG_ASSERT(!coordinates.empty(), "Points with dimension 0 are not supported"); + return coordinates.size(); + } + + template + typename DeterministicParetoExplorer::Point::DominanceResult DeterministicParetoExplorer::Point::getDominance(Point const& other) const { + STORM_LOG_ASSERT(this->dimension() == other.dimension(), "Non-Equal dimensions of points: [" << this->toString() << "] vs. [" << other.toString() << "]"); + auto thisIt = this->get().begin(); + auto otherIt = other.get().begin(); + auto thisItE = this->get().end(); + + // Find the first entry where the points differ + while (*thisIt == *otherIt) { + ++thisIt; + ++otherIt; + if (thisIt == thisItE) { + return DominanceResult::Equal; + } + } + + if (*thisIt > *otherIt) { + // *this might dominate other + for (++thisIt, ++otherIt; thisIt != thisItE; ++thisIt, ++otherIt) { + if (*thisIt < *otherIt) { + return DominanceResult::Incomparable; + } + } + return DominanceResult::Dominates; + } else { + assert(*thisIt < *otherIt); + // *this might be dominated by other + for (++thisIt, ++otherIt; thisIt != thisItE; ++thisIt, ++otherIt) { + if (*thisIt > *otherIt) { + return DominanceResult::Incomparable; + } + } + return DominanceResult::Dominated; + } + } + + template + void DeterministicParetoExplorer::Point::setParetoOptimal(bool value) { + paretoOptimal = value; + } + + template + bool DeterministicParetoExplorer::Point::isParetoOptimal() const { + return paretoOptimal; + } + + template + std::string DeterministicParetoExplorer::Point::toString(bool convertToDouble) const { + std::stringstream out; + bool first = true; + for (auto const& pi : this->get()) { + if (first) { + first = false; + } else { + out << ", "; + } + if (convertToDouble) { + out << pi; + } else { + out << pi; + } + } + return out.str(); + } + + // template + // bool operator<(typename DeterministicParetoExplorer::Point const& lhs, typename DeterministicParetoExplorer::Point const& rhs) { + // STORM_LOG_ASSERT(lhs.dimension() == rhs.dimension(), "Non-Equal dimensions of points: " << lhs << " vs. " << rhs); + // for (uint64_t i = 0; i < lhs.dimension(); ++i) { + // if (lhs.get()[i] < rhs.get()[i]) { + // return true; + // } else if (lhs.get()[i] != rhs.get()[i]) { + // return false; + // } + // } + // return false; + // } + + template + DeterministicParetoExplorer::Pointset::Pointset() : currId(1) { + // Intentionally left empty + } + + template + boost::optional::PointId> DeterministicParetoExplorer::Pointset::addPoint(Point const& point) { + + // Find dominated and dominating points + auto pointsIt = points.begin(); + auto pointsItE = points.end(); + while (pointsIt != points.end()) { + switch (point.getDominance(pointsIt->second)) { + case Point::DominanceResult::Incomparable: + // Nothing to be done for this point + ++pointsIt; + case Point::DominanceResult::Dominates: + // Found a point in the set that is dominated by the new point, so we erase it + pointsIt = points.erase(pointsIt); + case Point::DominanceResult::Dominated: + // The new point is dominated by another point. + return boost::none; + case Point::DominanceResult::Equal: + if (point.isParetoOptimal()) { + pointsIt->second.setParetoOptimal(); + } + return pointsIt->first; + } + } + + points.emplace_hint(points.end(), currId, point); + return currId++; + } + + template + typename DeterministicParetoExplorer::Point const& DeterministicParetoExplorer::Pointset::getPoint(PointId const& id) const { + return points.at(id); + } + + template + uint64_t DeterministicParetoExplorer::Pointset::size() const { + return points.size(); + } + + template + void DeterministicParetoExplorer::Pointset::collectPointsInPolytope(std::set& collectedPoints, Polytope const& polytope) { + for (auto const& p : points) { + if (polytope->contains(p.second.get())) { + collectedPoints.insert(p.first); + } + } + } + + template + void DeterministicParetoExplorer::Pointset::printToStream(std::ostream& out, bool includeIDs, bool convertToDouble) { + for (auto const& p : this->points) { + if (includeIDs) { + out << p.first << ": [" << p.second.toString(convertToDouble) << "]" << std::endl; + } else { + out << p.second.toString(convertToDouble) << std::endl; + } + } + } + + template + DeterministicParetoExplorer::Facet::Facet(storm::storage::geometry::Halfspace const& halfspace) : halfspace(halfspace) { + // Intentionally left empty + } + + template + DeterministicParetoExplorer::Facet::Facet(storm::storage::geometry::Halfspace&& halfspace) : halfspace(std::move(halfspace)) { + // Intentionally left empty + } + + template + void DeterministicParetoExplorer::Facet::addPoint(PointId const& pointId) { + paretoPointsOnFacet.push_back(pointId); + } + + template + std::vector::PointId> const& DeterministicParetoExplorer::Facet::getPoints() const { + return paretoPointsOnFacet; + } + + template + uint64_t DeterministicParetoExplorer::Facet::getNumberOfPoints() const { + return paretoPointsOnFacet.size(); + } + + + template + typename DeterministicParetoExplorer::Polytope DeterministicParetoExplorer::Facet::getInducedSimplex(Pointset const& pointset) const { + std::vector> vertices; + STORM_LOG_ASSERT(getNumberOfPoints() > 0, "Tried to compute the induced simplex, but not enough points are given."); + auto pointIdIt = paretoPointsOnFacet.begin(); + auto pointIdItE = paretoPointsOnFacet.end(); + vertices.push_back(pointset.getPoint(*pointIdIt).get()); + std::vector minPoint = vertices.back(); + + for (++pointIdIt; pointIdIt != pointIdItE; ++pointIdIt) { + vertices.push_back(pointset.getPoint(*pointIdIt).get()); + auto pIt = vertices.back().begin(); + for (auto& mi : minPoint) { + mi = std::min(mi, *pIt); + ++pIt; + } + } + vertices.push_back(std::move(minPoint)); + + // This facet might lie at the 'border', which means that the downward closure has to be taken in some directions + storm::storage::BitVector dimensionsForDownwardClosure = storm::utility::vector::filterZero(this->halfspace.normalVector()); + STORM_LOG_ASSERT(dimensionsForDownwardClosure.getNumberOfSetBits() + vertices.size() >= halfspace.normalVector().size() + 1, "The number of points on the facet is insufficient"); + if (dimensionsForDownwardClosure.empty()) { + return storm::storage::geometry::Polytope::create(vertices); + } else { + return storm::storage::geometry::Polytope::createSelectiveDownwardClosure(vertices, dimensionsForDownwardClosure); + } + } + + template + DeterministicParetoExplorer::DeterministicParetoExplorer(preprocessing::SparseMultiObjectivePreprocessorResult& preprocessorResult) { + // Intentionally left empty + } + + template + std::unique_ptr DeterministicParetoExplorer::check(Environment const& env) { + + clean(); + initializeFacets(env); + while (!unprocessedFacets.empty()) { + Facet f = std::move(unprocessedFacets.front()); + unprocessedFacets.pop(); + processFacet(env, f); + } + + // Todo: Prepare check result + return nullptr; + } + + template + void DeterministicParetoExplorer::clean() { + pointset = Pointset(); + unprocessedFacets = std::queue(); + overApproximation = storm::storage::geometry::Polytope::createUniversalPolytope(); + unachievableAreas.clear(); + } + + template + void DeterministicParetoExplorer::initializeFacets(Environment const& env) { + // TODO + } + + template + bool DeterministicParetoExplorer::checkFacetPrecision(Environment const& env, Facet const& f) { + // TODO + return false; + } + + template + void DeterministicParetoExplorer::processFacet(Environment const& env, Facet const& f) { + // TODO + + } + + template + bool DeterministicParetoExplorer::optimizeAndSplitFacet(Environment const& env, Facet const& f) { + // TODO + return false; + + } + + template + bool DeterministicParetoExplorer::findAndCheckCachedPoints(Environment const& env, Facet const& f, Polytope const& inducedSimplex, std::set& collectedPoints) { + // TODO + return false; + } + + template + bool DeterministicParetoExplorer::analyzePointsOnFacet(Environment const& env, Facet const& f, Polytope const& inducedSimplex, std::set& collectedPoints) { + + // TODO + return false; + } + + template + bool DeterministicParetoExplorer::analyzePointsInSimplex(Environment const& env, Facet const& f, Polytope const& inducedSimplex, std::set& collectedPoints) { + + // TODO + return false; + } + + template + void DeterministicParetoExplorer::exportPlotOfCurrentApproximation(Environment const& env) { + /* + STORM_LOG_ERROR_COND(objectives.size()==2, "Exporting plot requested but this is only implemented for the two-dimensional case."); + + auto transformedUnderApprox = transformPolytopeToOriginalModel(underApproximation); + auto transformedOverApprox = transformPolytopeToOriginalModel(overApproximation); + + // Get pareto points as well as a hyperrectangle that is used to guarantee that the resulting polytopes are bounded. + storm::storage::geometry::Hyperrectangle boundaries(std::vector(objectives.size(), storm::utility::zero()), std::vector(objectives.size(), storm::utility::zero())); + std::vector> paretoPoints; + paretoPoints.reserve(refinementSteps.size()); + for(auto const& step : refinementSteps) { + paretoPoints.push_back(transformPointToOriginalModel(step.lowerBoundPoint)); + boundaries.enlarge(paretoPoints.back()); + } + auto underApproxVertices = transformedUnderApprox->getVertices(); + for(auto const& v : underApproxVertices) { + boundaries.enlarge(v); + } + auto overApproxVertices = transformedOverApprox->getVertices(); + for(auto const& v : overApproxVertices) { + boundaries.enlarge(v); + } + + //Further enlarge the boundaries a little + storm::utility::vector::scaleVectorInPlace(boundaries.lowerBounds(), GeometryValueType(15) / GeometryValueType(10)); + storm::utility::vector::scaleVectorInPlace(boundaries.upperBounds(), GeometryValueType(15) / GeometryValueType(10)); + + auto boundariesAsPolytope = boundaries.asPolytope(); + std::vector columnHeaders = {"x", "y"}; + + std::vector> pointsForPlotting; + if (env.modelchecker().multi().getPlotPathUnderApproximation()) { + underApproxVertices = transformedUnderApprox->intersection(boundariesAsPolytope)->getVerticesInClockwiseOrder(); + pointsForPlotting.reserve(underApproxVertices.size()); + for(auto const& v : underApproxVertices) { + pointsForPlotting.push_back(storm::utility::vector::convertNumericVector(v)); + } + storm::utility::exportDataToCSVFile(env.modelchecker().multi().getPlotPathUnderApproximation().get(), pointsForPlotting, columnHeaders); + } + + if (env.modelchecker().multi().getPlotPathOverApproximation()) { + pointsForPlotting.clear(); + overApproxVertices = transformedOverApprox->intersection(boundariesAsPolytope)->getVerticesInClockwiseOrder(); + pointsForPlotting.reserve(overApproxVertices.size()); + for(auto const& v : overApproxVertices) { + pointsForPlotting.push_back(storm::utility::vector::convertNumericVector(v)); + } + storm::utility::exportDataToCSVFile(env.modelchecker().multi().getPlotPathOverApproximation().get(), pointsForPlotting, columnHeaders); + } + + if (env.modelchecker().multi().getPlotPathParetoPoints()) { + pointsForPlotting.clear(); + pointsForPlotting.reserve(paretoPoints.size()); + for(auto const& v : paretoPoints) { + pointsForPlotting.push_back(storm::utility::vector::convertNumericVector(v)); + } + storm::utility::exportDataToCSVFile(env.modelchecker().multi().getPlotPathParetoPoints().get(), pointsForPlotting, columnHeaders); + } + }; + */ + } + + template class DeterministicParetoExplorer, storm::RationalNumber>; + template class DeterministicParetoExplorer, storm::RationalNumber>; + template class DeterministicParetoExplorer, storm::RationalNumber>; + template class DeterministicParetoExplorer, storm::RationalNumber>; + } + } +} \ No newline at end of file diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicParetoExplorer.h b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicParetoExplorer.h new file mode 100644 index 000000000..3ca0b85d0 --- /dev/null +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicParetoExplorer.h @@ -0,0 +1,174 @@ +#pragma once + +#include + +#include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h" +#include "storm/storage/geometry/Polytope.h" +#include "storm/storage/geometry/Halfspace.h" +#include "storm/modelchecker/results/CheckResult.h" + +namespace storm { + + class Environment; + + namespace modelchecker { + namespace multiobjective { + + template + class DeterministicParetoExplorer { + public: + typedef uint64_t PointId; + typedef typename std::shared_ptr> Polytope; + + class Point { + public: + Point(std::vector const& coordinates); + Point(std::vector&& coordinates); + + std::vector const& get() const; + std::vector& get(); + + uint64_t dimension() const; + + enum class DominanceResult { + Incomparable, + Dominates, + Dominated, + Equal + }; + DominanceResult getDominance(Point const& other) const; + + void setParetoOptimal(bool value = true); + bool isParetoOptimal() const; + + std::string toString(bool convertToDouble = false) const; + + private: + std::vector coordinates; + bool paretoOptimal; + }; + + + class Pointset { + public: + Pointset(); + + /*! + * If the given point is not dominated by another point in the set, it is added + * to the set and its ID is returned. + * If the point is dominated by another point, boost::none is returned. + * Erases all points in the set, that are dominated by the given point. + * If the same point is already contained in the set, its id is returned + */ + boost::optional addPoint(Point const& point); + + /*! + * Returns the point with the given ID + */ + Point const& getPoint(PointId const& id) const; + + /*! + * Returns the number of points currently contained in the set + */ + uint64_t size() const; + + void collectPointsInPolytope(std::set& collectedPoints, Polytope const& polytope); + + void printToStream(std::ostream& out, bool includeIDs = true, bool convertToDouble = false); + + private: + std::map points; + PointId currId; + }; + + class Facet { + public: + Facet(storm::storage::geometry::Halfspace const& halfspace); + Facet(storm::storage::geometry::Halfspace&& halfspace); + void addPoint(PointId const& pointId); + std::vector const& getPoints() const; + uint64_t getNumberOfPoints() const; + + /*! + * Creates a polytope that captures all points that lie 'under' the facet + * More precisely, the vertices of the polytope are the points on the facet + * and point p with p_i = min {x_i | x lies on facet} + */ + Polytope getInducedSimplex(Pointset const& pointset) const; + + + + private: + storm::storage::geometry::Halfspace halfspace; + std::vector paretoPointsOnFacet; + }; + + + DeterministicParetoExplorer(preprocessing::SparseMultiObjectivePreprocessorResult& preprocessorResult); + + virtual std::unique_ptr check(Environment const& env); + + void exportPlotOfCurrentApproximation(Environment const& env); + + private: + + /*! + * Cleans up all cached results from a previous check call + */ + void clean(); + + /*! + * Builds the initial facets by optimizing the objectives individually. + * Adds the facets that need further processing to unprocessedFacets + */ + void initializeFacets(Environment const& env); + + /*! + * Checks the precision of the given Facet and returns true, if no further processing of the facet is necessary + */ + bool checkFacetPrecision(Environment const& env, Facet const& f); + + /*! Processes the given facet as follows: + * 1. Optimize in the facet direction. Potentially, this adds new, unprocessed facets + * 2. Find points that have already been collected so far such that they lie in the induced simplex of the facet. + * 3. Find more points that lie on the facet + * 4. Find all points that lie in the induced simplex or prove that there are none + */ + void processFacet(Environment const& env, Facet const& f); + + /*! + * Optimizes in the facet direction. If this results in a point that does not lie on the facet, + * 1. The new Pareto optimal point is added + * 2. New facets are generated and (if not already precise enough) added to unprocessedFacets + * 3. true is returned + */ + bool optimizeAndSplitFacet(Environment const& env, Facet const& f); + + /*! + * Finds all points that lie within the induced Simplex of the given facet. + * Returns true if the facet is sufficiently precise when considering all added points + */ + bool findAndCheckCachedPoints(Environment const& env, Facet const& f, Polytope const& inducedSimplex, std::set& collectedPoints); + + /*! + * Finds points that lie on the facet + * Returns true if the facet has been analyzed sufficiently precise. + * If false is returned, it means that *all* points that lie on the facet have been analyzed but the analysis is still not precise enough + * + * use smt to find an eps-box in the simplex that does not contain a point. Add new points until one in the box is found. repeat. + * stop when no more points or boxes can be found. + */ + bool analyzePointsOnFacet(Environment const& env, Facet const& f, Polytope const& inducedSimplex, std::set& collectedPoints); + + bool analyzePointsInSimplex(Environment const& env, Facet const& f, Polytope const& inducedSimplex, std::set& collectedPoints); + + Pointset pointset; + std::queue unprocessedFacets; + Polytope overApproximation; + std::vector unachievableAreas; + + }; + + } + } +} \ No newline at end of file diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/MultiObjectiveSchedulerEvaluator.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/MultiObjectiveSchedulerEvaluator.cpp new file mode 100644 index 000000000..5a25557ef --- /dev/null +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/MultiObjectiveSchedulerEvaluator.cpp @@ -0,0 +1,32 @@ +#include "storm/modelchecker/multiobjective/deterministicScheds/MultiObjectiveSchedulerEvaluator.h" + +namespace storm { + namespace modelchecker { + namespace multiobjective { + + template + MultiObjectiveSchedulerEvaluator::MultiObjectiveSchedulerEvaluator(preprocessing::SparseMultiObjectivePreprocessorResult& preprocessorResult) { + // TODO + } + + template + void MultiObjectiveSchedulerEvaluator::check(std::vector const& scheduler) { + // TODO + } + + template + std::vector::ValueType> const& MultiObjectiveSchedulerEvaluator::getResultForObjective(uint64_t objIndex) const { + return results[objIndex]; + } + + template + std::vector MultiObjectiveSchedulerEvaluator::getInitialStateResults() const { + std::vector res; + for (auto objResult : results) { + res.push_back(objResult[initialState]); + } + return res; + } + } + } +} \ No newline at end of file diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/MultiObjectiveSchedulerEvaluator.h b/src/storm/modelchecker/multiobjective/deterministicScheds/MultiObjectiveSchedulerEvaluator.h new file mode 100644 index 000000000..0a4ef3c0d --- /dev/null +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/MultiObjectiveSchedulerEvaluator.h @@ -0,0 +1,30 @@ +#pragma once + +#include + +#include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h" + +namespace storm { + namespace modelchecker { + namespace multiobjective { + + template + class MultiObjectiveSchedulerEvaluator { + public: + + typedef typename ModelType::ValueType ValueType; + + MultiObjectiveSchedulerEvaluator(preprocessing::SparseMultiObjectivePreprocessorResult& preprocessorResult); + + void check(std::vector const& scheduler); + + std::vector const& getResultForObjective(uint64_t objIndex) const; + std::vector getInitialStateResults() const; + + private: + std::vector> results; + uint64_t initialState; + }; + } + } +} \ No newline at end of file