Multiobjective exportschedulers

src/storm-cli-utilities/model-handling.h

@@ -28,6 +28,8 @@
 
 #include "storm/exceptions/OptionParserException.h"
 
+#include "storm/modelchecker/results/CheckResult.h"
+#include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h"
 #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
 
 #include "storm/models/sparse/StandardRewardModel.h"
@@ -1141,7 +1143,21 @@ void verifyWithSparseEngine(std::shared_ptr<storm::models::ModelBase> const& mod
                     STORM_LOG_ERROR("Scheduler requested but could not be generated.");
                 }
             } else {
-                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Scheduler export not supported for this property.");
+                if (result->isExplicitParetoCurveCheckResult()) {
+                    if (result->template asExplicitParetoCurveCheckResult<ValueType>().hasScheduler()) {
+                        auto schedulers = result->template asExplicitParetoCurveCheckResult<ValueType>().getSchedulers();
+                        for (auto const& scheduler : schedulers) {
+                            storm::api::exportScheduler(sparseModel, *scheduler.second.get(),
+                                                        (exportCount == 0 ? std::string("") : std::to_string(exportCount)) +
+                                                            ioSettings.getExportSchedulerFilename() + "-" +
+                                                            storm::utility::vector::toStringNoVerbose(scheduler.first));
+                        }
+                    } else {
+                        STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Scheduler export not supported for this property.");
+                    }
+                } else {
+                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Scheduler export not supported for this property.");
+                }
             }
         }
         if (ioSettings.isExportCheckResultSet()) {

src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp

@@ -1,6 +1,10 @@
 #include "storm/modelchecker/multiobjective/MultiObjectivePostprocessing.h"
 
 #include "storm/adapters/RationalNumberAdapter.h"
+#include "storm/models/sparse/MarkovAutomaton.h"
+#include "storm/models/sparse/Mdp.h"
+#include "storm/storage/Scheduler.h"
+#include "storm/storage/memorystructure/SparseModelMemoryProductReverseData.h"
 
 namespace storm {
 namespace modelchecker {
@@ -66,6 +70,41 @@ std::shared_ptr<storm::storage::geometry::Polytope<GeometryValueType>> transform
     return polytope->affineTransformation(transformationMatrix, transformationVector);
 }
 
+/*
+ * This function is only responsible to reverse changes to the model made in the preprocessor
+ * (not the ones done by specific checkers)
+ */
+template<typename ValueType, typename SparseModelType>
+void transformObjectiveSchedulersToOriginal(storm::storage::SparseModelMemoryProductReverseData const& reverseData,
+                                            std::shared_ptr<SparseModelType> const& originalModel,
+                                            std::map<std::vector<ValueType>, std::shared_ptr<storm::storage::Scheduler<ValueType>>> schedulers) {
+    auto memoryStateCount = reverseData.memory.getNumberOfStates();
+    auto originalModelStates = originalModel->getNumberOfStates();
+    for (auto it = schedulers.begin(); it != schedulers.end(); ++it) {
+        std::shared_ptr<storm::storage::Scheduler<ValueType>> scheduler = it->second;
+        auto point = it->first;
+        storm::storage::Scheduler<ValueType> result(originalModelStates, reverseData.memory);
+        auto currSchedulerModelStates = scheduler->getNumberOfModelStates();
+        for (int state = 0; state < originalModelStates; state++) {
+            for (int memState = 0; memState < memoryStateCount; memState++) {
+                auto const& productState = reverseData.toResultStateMapping[state * memoryStateCount + memState];
+                if (productState != -1) {
+                    // if it's -1 it's unreachable
+                    if (productState >= currSchedulerModelStates) {
+                        // means it's been deleted as irrelevant state
+                        result.setDontCare(productState, memState, true);
+                    } else {
+                        auto choice = scheduler->getChoice(productState);
+                        result.setChoice(choice, state, memState);
+                    }
+                }
+            }
+        }
+        scheduler.reset();
+        schedulers[point] = std::move(std::make_shared<storm::storage::Scheduler<ValueType>>(result));
+    }
+}
+
 template std::vector<storm::RationalNumber> transformObjectiveValuesToOriginal(std::vector<Objective<double>> objectives,
                                                                                std::vector<storm::RationalNumber> const& point);
 template std::shared_ptr<storm::storage::geometry::Polytope<storm::RationalNumber>> transformObjectivePolytopeToOriginal(
@@ -74,6 +113,25 @@ template std::vector<storm::RationalNumber> transformObjectiveValuesToOriginal(s
                                                                                std::vector<storm::RationalNumber> const& point);
 template std::shared_ptr<storm::storage::geometry::Polytope<storm::RationalNumber>> transformObjectivePolytopeToOriginal(
     std::vector<Objective<storm::RationalNumber>> objectives, std::shared_ptr<storm::storage::geometry::Polytope<storm::RationalNumber>> const& polytope);
+
+template void transformObjectiveSchedulersToOriginal(
+    storm::storage::SparseModelMemoryProductReverseData const& reverseData,
+    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> const& originalModel,
+    std::map<std::vector<storm::RationalNumber>, std::shared_ptr<storm::storage::Scheduler<storm::RationalNumber>>> schedulers);
+
+template void transformObjectiveSchedulersToOriginal(storm::storage::SparseModelMemoryProductReverseData const& reverseData,
+                                                     std::shared_ptr<storm::models::sparse::Mdp<double>> const& originalModel,
+                                                     std::map<std::vector<double>, std::shared_ptr<storm::storage::Scheduler<double>>> schedulers);
+
+template void transformObjectiveSchedulersToOriginal(
+    storm::storage::SparseModelMemoryProductReverseData const& reverseData,
+    std::shared_ptr<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>> const& originalModel,
+    std::map<std::vector<storm::RationalNumber>, std::shared_ptr<storm::storage::Scheduler<storm::RationalNumber>>> schedulers);
+
+template void transformObjectiveSchedulersToOriginal(storm::storage::SparseModelMemoryProductReverseData const& reverseData,
+                                                     std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> const& originalModel,
+                                                     std::map<std::vector<double>, std::shared_ptr<storm::storage::Scheduler<double>>> schedulers);
+
 }  // namespace multiobjective
 }  // namespace modelchecker
 }  // namespace storm

src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.h

@@ -4,7 +4,9 @@
 #include <vector>
 
 #include "storm/modelchecker/multiobjective/Objective.h"
+#include "storm/storage/Scheduler.h"
 #include "storm/storage/geometry/Polytope.h"
+#include "storm/storage/memorystructure/SparseModelMemoryProductReverseData.h"
 
 namespace storm {
 namespace modelchecker {
@@ -17,6 +19,15 @@ template<typename ValueType, typename GeometryValueType>
 std::shared_ptr<storm::storage::geometry::Polytope<GeometryValueType>> transformObjectivePolytopeToOriginal(
     std::vector<Objective<ValueType>> objectives, std::shared_ptr<storm::storage::geometry::Polytope<GeometryValueType>> const& polytope);
 
+/*
+ * Uses the information from reverse data to edit the objective schedulers in 'schedulers' to ones
+ * apt for the target model.
+ */
+template<typename ValueType, typename SparseModelType>
+void transformObjectiveSchedulersToOriginal(storm::storage::SparseModelMemoryProductReverseData const& reverseData,
+                                            std::shared_ptr<SparseModelType> const& originalModel,
+                                            std::map<std::vector<ValueType>, std::shared_ptr<storm::storage::Scheduler<ValueType>>> schedulers);
+
 }  // namespace multiobjective
 }  // namespace modelchecker
 }  // namespace storm

src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp

@@ -1,12 +1,15 @@
 #include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h"
 
 #include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h"
+#include "storm/modelchecker/multiobjective/MultiObjectivePostprocessing.h"
 #include "storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.h"
 #include "storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.h"
 #include "storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h"
 #include "storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h"
 #include "storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h"
 #include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.h"
+#include "storm/modelchecker/results/CheckResult.h"
+#include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h"
 #include "storm/models/sparse/MarkovAutomaton.h"
 #include "storm/models/sparse/Mdp.h"
 #include "storm/models/sparse/StandardRewardModel.h"
@@ -83,6 +86,13 @@ std::unique_ptr<CheckResult> performMultiObjectiveModelChecking(Environment cons
                 }
 
                 result = query->check(env);
+                if (preprocessorResult.memoryIncorporationReverseData && result->isExplicitParetoCurveCheckResult() &&
+                    result->template asExplicitParetoCurveCheckResult<typename SparseModelType::ValueType>().hasScheduler()) {
+                    // we have information to post-process schedulers
+                    auto schedulers = result->template asExplicitParetoCurveCheckResult<typename SparseModelType::ValueType>().getSchedulers();
+                    transformObjectiveSchedulersToOriginal(std::move(preprocessorResult.memoryIncorporationReverseData.value()),
+                                                           std::make_shared<SparseModelType>(model), schedulers);
+                }
 
                 if (env.modelchecker().multi().isExportPlotSet()) {
                     query->exportPlotOfCurrentApproximation(env);

src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h

@@ -69,6 +69,14 @@ class PcaaWeightVectorChecker {
      */
     virtual storm::storage::Scheduler<ValueType> computeScheduler() const;
 
+    /*!
+     * If changes has been made to the given model this function should inverse them to return a scheduler
+     * for the given model
+     */
+    virtual storm::storage::Scheduler<ValueType> computeOriginalScheduler() const {
+        return computeScheduler();
+    }
+
    protected:
     /*!
      * Computes the weighted lower or upper bounds for the provided set of objectives.

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

@@ -7,6 +7,10 @@
 #include "storm/models/sparse/MarkovAutomaton.h"
 #include "storm/models/sparse/Mdp.h"
 #include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/CoreSettings.h"
+#include "storm/settings/modules/IOSettings.h"
+#include "storm/storage/Scheduler.h"
 #include "storm/utility/SignalHandler.h"
 #include "storm/utility/constants.h"
 #include "storm/utility/vector.h"
@@ -51,13 +55,24 @@ std::unique_ptr<CheckResult> SparsePcaaParetoQuery<SparseModelType, GeometryValu
             storm::utility::vector::convertNumericVector<typename SparseModelType::ValueType>(transformObjectiveValuesToOriginal(this->objectives, vertex)));
     }
     return std::unique_ptr<CheckResult>(new ExplicitParetoCurveCheckResult<typename SparseModelType::ValueType>(
-        this->originalModel.getInitialStates().getNextSetIndex(0), std::move(paretoOptimalPoints),
+        this->originalModel.getInitialStates().getNextSetIndex(0), std::move(paretoOptimalPoints), std::move(schedulers),
         transformObjectivePolytopeToOriginal(this->objectives, this->underApproximation)
             ->template convertNumberRepresentation<typename SparseModelType::ValueType>(),
         transformObjectivePolytopeToOriginal(this->objectives, this->overApproximation)
             ->template convertNumberRepresentation<typename SparseModelType::ValueType>()));
 }
 
+template<class SparseModelType, typename GeometryValueType>
+void SparsePcaaParetoQuery<SparseModelType, GeometryValueType>::updateSchedulers() {
+    if (storm::settings::getModule<storm::settings::modules::IOSettings>().isExportSchedulerSet()) {
+        std::vector<typename SparseModelType::ValueType> point = this->weightVectorChecker->getUnderApproximationOfInitialStateResults();
+        if (!this->schedulers.count(point)) {
+            this->schedulers[point] =
+                std::make_shared<storm::storage::Scheduler<typename SparseModelType::ValueType>>(this->weightVectorChecker->computeOriginalScheduler());
+        }
+    }
+}
+
 template<class SparseModelType, typename GeometryValueType>
 void SparsePcaaParetoQuery<SparseModelType, GeometryValueType>::exploreSetOfAchievablePoints(Environment const& env) {
     STORM_LOG_THROW(env.modelchecker().multi().getPrecisionType() == MultiObjectiveModelCheckerEnvironment::PrecisionType::Absolute,
@@ -68,6 +83,7 @@ void SparsePcaaParetoQuery<SparseModelType, GeometryValueType>::exploreSetOfAchi
         WeightVector direction(this->objectives.size(), storm::utility::zero<GeometryValueType>());
         direction[objIndex] = storm::utility::one<GeometryValueType>();
         this->performRefinementStep(env, std::move(direction));
+        this->updateSchedulers();
         if (storm::utility::resources::isTerminate()) {
             break;
         }
@@ -95,6 +111,7 @@ void SparsePcaaParetoQuery<SparseModelType, GeometryValueType>::exploreSetOfAchi
         STORM_LOG_INFO("Current precision of the approximation of the pareto curve is ~" << storm::utility::convertNumber<double>(farestDistance));
         WeightVector direction = underApproxHalfspaces[farestHalfspaceIndex].normalVector();
         this->performRefinementStep(env, std::move(direction));
+        this->updateSchedulers();
     }
     STORM_LOG_ERROR("Could not reach the desired precision: Termination requested or maximum number of refinement steps exceeded.");
 }

src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h

@@ -31,11 +31,20 @@ class SparsePcaaParetoQuery : public SparsePcaaQuery<SparseModelType, GeometryVa
      */
     virtual std::unique_ptr<CheckResult> check(Environment const& env) override;
 
+    /*
+     * Compute the scheduler for current underaproximated point and store it
+     */
+    void updateSchedulers();
+
    private:
     /*
      * Performs refinement steps until the approximation is sufficiently precise
      */
     void exploreSetOfAchievablePoints(Environment const& env);
+    /*
+     * Schedulers corresponding to the pareto optimal points
+     */
+    std::map<std::vector<typename SparseModelType::ValueType>, std::shared_ptr<storm::storage::Scheduler<typename SparseModelType::ValueType>>> schedulers;
 };
 
 }  // namespace multiobjective

src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp

@@ -64,7 +64,7 @@ void StandardPcaaWeightVectorChecker<SparseModelType>::initialize(
     auto mergerResult =
         merger.mergeTargetAndSinkStates(maybeStates, rewardAnalysis.reward0AStates, storm::storage::BitVector(maybeStates.size(), false),
                                         std::vector<std::string>(relevantRewardModels.begin(), relevantRewardModels.end()), finiteTotalRewardChoices);
-
+    goalStateMergerIndexMapping = mergerResult.oldToNewStateIndexMapping;
     // Initialize data specific for the considered model type
     initializeModelTypeSpecificData(*mergerResult.model);
 
@@ -235,6 +235,18 @@ StandardPcaaWeightVectorChecker<SparseModelType>::computeScheduler() const {
     return result;
 }
 
+template<class SparseModelType>
+storm::storage::Scheduler<typename StandardPcaaWeightVectorChecker<SparseModelType>::ValueType>
+StandardPcaaWeightVectorChecker<SparseModelType>::computeOriginalScheduler() const {
+    auto scheduler = this->computeScheduler();
+    storm::storage::Scheduler<ValueType> result(goalStateMergerIndexMapping.size());
+    auto numOfModelStates = result.getNumberOfModelStates();
+    for (int state = 0; state < numOfModelStates; state++) {
+        result.setChoice(scheduler.getChoice(goalStateMergerIndexMapping[state]), state);
+    }
+    return result;
+}
+
 template<typename ValueType>
 void computeSchedulerProb1(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions,
                            storm::storage::BitVector const& consideredStates, storm::storage::BitVector const& statesToReach, std::vector<uint64_t>& choices,

src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h

@@ -12,6 +12,7 @@
 #include "storm/storage/Scheduler.h"
 #include "storm/storage/SparseMatrix.h"
 #include "storm/transformer/EndComponentEliminator.h"
+#include "storm/transformer/GoalStateMerger.h"
 #include "storm/utility/vector.h"
 
 namespace storm {
@@ -67,6 +68,12 @@ class StandardPcaaWeightVectorChecker : public PcaaWeightVectorChecker<SparseMod
      */
     virtual storm::storage::Scheduler<ValueType> computeScheduler() const override;
 
+    /*!
+     * Use the "oldToNewStateIndexMapping" from the merge result to build a scheduler fit for the original scheduler
+     * from the calculated scheduler from "computerScheduler"
+     */
+    virtual storm::storage::Scheduler<ValueType> computeOriginalScheduler() const override;
+
    protected:
     void initialize(preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType> const& preprocessorResult);
     virtual void initializeModelTypeSpecificData(SparseModelType const& model) = 0;
@@ -173,6 +180,9 @@ class StandardPcaaWeightVectorChecker : public PcaaWeightVectorChecker<SparseMod
     };
     boost::optional<EcQuotient> ecQuotient;
 
+    // Merge results
+    std::vector<uint_fast64_t> goalStateMergerIndexMapping;
+
     struct LraMecDecomposition {
         storm::storage::MaximalEndComponentDecomposition<ValueType> mecs;
         std::vector<ValueType> auxMecValues;