From f0d6c451a8ba333efa399f294c5e03df16e3ca54 Mon Sep 17 00:00:00 2001 From: Ulises Date: Mon, 13 Feb 2023 10:09:39 +0100 Subject: [PATCH 01/18] explicit pareto curve check result stores mapping from pareto point to scheduler --- .../modelchecker/results/CheckResult.cpp | 2 ++ .../ExplicitParetoCurveCheckResult.cpp | 25 +++++++++++++++++++ .../results/ExplicitParetoCurveCheckResult.h | 12 +++++++++ .../results/ParetoCurveCheckResult.cpp | 1 + 4 files changed, 40 insertions(+) diff --git a/src/storm/modelchecker/results/CheckResult.cpp b/src/storm/modelchecker/results/CheckResult.cpp index 8549ce26d0..f29da19975 100644 --- a/src/storm/modelchecker/results/CheckResult.cpp +++ b/src/storm/modelchecker/results/CheckResult.cpp @@ -230,6 +230,8 @@ template ExplicitQuantitativeCheckResult const& CheckRe template ExplicitParetoCurveCheckResult& CheckResult::asExplicitParetoCurveCheckResult(); template ExplicitParetoCurveCheckResult const& CheckResult::asExplicitParetoCurveCheckResult() const; +template ExplicitParetoCurveCheckResult& CheckResult::asExplicitParetoCurveCheckResult(); +template ExplicitParetoCurveCheckResult const& CheckResult::asExplicitParetoCurveCheckResult() const; template LexicographicCheckResult& CheckResult::asLexicographicCheckResult(); template LexicographicCheckResult const& CheckResult::asLexicographicCheckResult() const; diff --git a/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp index 02f62702cb..00834a76ba 100644 --- a/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp +++ b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp @@ -65,9 +65,34 @@ storm::storage::sparse::state_type const& ExplicitParetoCurveCheckResult +bool ExplicitParetoCurveCheckResult::hasScheduler() const { + return schedulers.size() > 0; +} + +template +void ExplicitParetoCurveCheckResult::setSchedulers( + const std::map, std::shared_ptr>> newSchedulers) { + schedulers = newSchedulers; +} + +template +std::map, std::shared_ptr>> const& ExplicitParetoCurveCheckResult::getSchedulers() + const { + STORM_LOG_THROW(this->hasScheduler(), storm::exceptions::InvalidOperationException, "Unable to retrieve non-existing scheduler."); + return schedulers; +} + +template +std::map, std::shared_ptr>>& ExplicitParetoCurveCheckResult::getSchedulers() { + STORM_LOG_THROW(this->hasScheduler(), storm::exceptions::InvalidOperationException, "Unable to retrieve non-existing scheduler."); + return schedulers; +} + template class ExplicitParetoCurveCheckResult; #ifdef STORM_HAVE_CARL template class ExplicitParetoCurveCheckResult; +template class ExplicitParetoCurveCheckResult; #endif } // namespace modelchecker } // namespace storm diff --git a/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.h b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.h index f2f6472e51..d2cd0ab219 100644 --- a/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.h +++ b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.h @@ -1,9 +1,11 @@ #ifndef STORM_MODELCHECKER_EXPLICITPARETOCURVECHECKRESULT_H_ #define STORM_MODELCHECKER_EXPLICITPARETOCURVECHECKRESULT_H_ +#include #include #include "storm/modelchecker/results/ParetoCurveCheckResult.h" +#include "storm/storage/Scheduler.h" #include "storm/storage/sparse/StateType.h" namespace storm { @@ -36,9 +38,19 @@ class ExplicitParetoCurveCheckResult : public ParetoCurveCheckResult storm::storage::sparse::state_type const& getState() const; + virtual bool hasScheduler() const override; + // void addScheduler(const std::shared_ptr>& scheduler); + void setSchedulers(std::map, std::shared_ptr>> schedulers); + + std::map, std::shared_ptr>> const& getSchedulers() const; + + std::map, std::shared_ptr>>& getSchedulers(); + private: // The state of the checked model to which the result applies storm::storage::sparse::state_type state; + // The corresponding strategies to reach each point in the pareto curve + std::map, std::shared_ptr>> schedulers; }; } // namespace modelchecker } // namespace storm diff --git a/src/storm/modelchecker/results/ParetoCurveCheckResult.cpp b/src/storm/modelchecker/results/ParetoCurveCheckResult.cpp index 771d2e5a98..baa69b4f2f 100644 --- a/src/storm/modelchecker/results/ParetoCurveCheckResult.cpp +++ b/src/storm/modelchecker/results/ParetoCurveCheckResult.cpp @@ -96,6 +96,7 @@ template class ParetoCurveCheckResult; #ifdef STORM_HAVE_CARL template class ParetoCurveCheckResult; +template class ParetoCurveCheckResult; #endif } // namespace modelchecker } // namespace storm From 1a9cff88bc6bc62104094671fd28d6900ef13142 Mon Sep 17 00:00:00 2001 From: Ulises Date: Mon, 13 Feb 2023 10:11:12 +0100 Subject: [PATCH 02/18] scheduler expose number of choices --- src/storm/storage/Scheduler.h | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/storm/storage/Scheduler.h b/src/storm/storage/Scheduler.h index c33dde45b0..d7f970a0b2 100644 --- a/src/storm/storage/Scheduler.h +++ b/src/storm/storage/Scheduler.h @@ -56,6 +56,12 @@ class Scheduler { */ SchedulerChoice const& getChoice(uint_fast64_t modelState, uint_fast64_t memoryState = 0) const; + /*! + * Returns the ammount of stored choices in this scheduler. + */ + int getNumberOfChoices() const { + return schedulerChoices.front().size(); + } /*! * Set the combination of model state and memoryStructure state to dontCare. * These states are considered unreachable and are ignored when printing the scheduler. From 6e22da3618bf4c2cfc4f90a4a90f233e1c268467 Mon Sep 17 00:00:00 2001 From: Ulises Date: Mon, 13 Feb 2023 11:32:27 +0100 Subject: [PATCH 03/18] multiobjective postprocessing schedulers --- .../MultiObjectivePostprocessing.cpp | 36 +++++++++++++++++++ .../MultiObjectivePostprocessing.h | 5 +++ 2 files changed, 41 insertions(+) diff --git a/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp b/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp index 11be8df9d5..dcba730726 100644 --- a/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp +++ b/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp @@ -1,6 +1,9 @@ #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" namespace storm { namespace modelchecker { @@ -66,6 +69,29 @@ std::shared_ptr> 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 +std::shared_ptr> transformObjectiveSchedulerToOriginal(std::shared_ptr const& originalModel, + std::shared_ptr> scheduler) { + storm::storage::Scheduler result(originalModel->getNumberOfStates()); + // set common states + for (int state = 0; state < scheduler->getNumberOfChoices(); state++) { + for (int memory = 0; memory < scheduler->getNumberOfMemoryStates(); memory++) { + result.setChoice(scheduler->getChoice(state, memory), state); + } + } + // add irrelevant states removed in preprocessing + for (int state = scheduler->getNumberOfChoices(); state < originalModel->getNumberOfStates(); state++) { + for (int memory = 0; memory < scheduler->getNumberOfMemoryStates(); memory++) { + result.setDontCare(state, memory, false); + } + } + return std::make_shared>(result); +} + template std::vector transformObjectiveValuesToOriginal(std::vector> objectives, std::vector const& point); template std::shared_ptr> transformObjectivePolytopeToOriginal( @@ -74,6 +100,16 @@ template std::vector transformObjectiveValuesToOriginal(s std::vector const& point); template std::shared_ptr> transformObjectivePolytopeToOriginal( std::vector> objectives, std::shared_ptr> const& polytope); +template std::shared_ptr> transformObjectiveSchedulerToOriginal( + std::shared_ptr> const& originalModel, + std::shared_ptr> scheduler); +template std::shared_ptr> transformObjectiveSchedulerToOriginal( + std::shared_ptr> const& originalModel, std::shared_ptr> scheduler); +template std::shared_ptr> transformObjectiveSchedulerToOriginal( + std::shared_ptr> const& originalModel, + std::shared_ptr> scheduler); +template std::shared_ptr> transformObjectiveSchedulerToOriginal( + std::shared_ptr> const& originalModel, std::shared_ptr> scheduler); } // namespace multiobjective } // namespace modelchecker } // namespace storm \ No newline at end of file diff --git a/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.h b/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.h index 549c4c15a1..32c44ea086 100644 --- a/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.h +++ b/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.h @@ -4,6 +4,7 @@ #include #include "storm/modelchecker/multiobjective/Objective.h" +#include "storm/storage/Scheduler.h" #include "storm/storage/geometry/Polytope.h" namespace storm { @@ -17,6 +18,10 @@ template std::shared_ptr> transformObjectivePolytopeToOriginal( std::vector> objectives, std::shared_ptr> const& polytope); +template +std::shared_ptr> transformObjectiveSchedulerToOriginal(std::shared_ptr const& originalModel, + std::shared_ptr> scheduler); + } // namespace multiobjective } // namespace modelchecker } // namespace storm \ No newline at end of file From 77d5008bc8415e16830617b5c2e33ec9369f585f Mon Sep 17 00:00:00 2001 From: Ulises Date: Mon, 13 Feb 2023 13:07:05 +0100 Subject: [PATCH 04/18] return schedulers for each point during pcaa --- .../pcaa/PcaaWeightVectorChecker.h | 8 ++++++++ .../pcaa/SparsePcaaParetoQuery.cpp | 20 +++++++++++++++++-- .../pcaa/SparsePcaaParetoQuery.h | 8 ++++++++ .../pcaa/StandardPcaaWeightVectorChecker.cpp | 18 ++++++++++++++++- .../pcaa/StandardPcaaWeightVectorChecker.h | 10 ++++++++++ 5 files changed, 61 insertions(+), 3 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h index 38d8c8f137..2bdb94560e 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h @@ -69,6 +69,14 @@ class PcaaWeightVectorChecker { */ virtual storm::storage::Scheduler 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 computeOriginalScheduler() const { + return computeScheduler(); + } + protected: /*! * Computes the weighted lower or upper bounds for the provided set of objectives. diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp index 24c8030628..a0df74ae12 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp @@ -10,6 +10,7 @@ #include "storm/utility/SignalHandler.h" #include "storm/utility/constants.h" #include "storm/utility/vector.h" +#include "storm/storage/Scheduler.h" namespace storm { namespace modelchecker { @@ -50,12 +51,25 @@ std::unique_ptr SparsePcaaParetoQuery(transformObjectiveValuesToOriginal(this->objectives, vertex))); } - return std::unique_ptr(new ExplicitParetoCurveCheckResult( + auto result = new ExplicitParetoCurveCheckResult( this->originalModel.getInitialStates().getNextSetIndex(0), std::move(paretoOptimalPoints), transformObjectivePolytopeToOriginal(this->objectives, this->underApproximation) ->template convertNumberRepresentation(), transformObjectivePolytopeToOriginal(this->objectives, this->overApproximation) - ->template convertNumberRepresentation())); + ->template convertNumberRepresentation()); + result->setSchedulers(std::move(schedulers)); + return std::unique_ptr(result); +} + +template +void SparsePcaaParetoQuery::updateSchedulers() { + auto scheduler = + std::make_shared>( + this->weightVectorChecker->computeOriginalScheduler()); + std::vector point = this->weightVectorChecker->getUnderApproximationOfInitialStateResults(); + auto targetScheduler = transformObjectiveSchedulerToOriginal( + std::make_shared(std::move(this->originalModel)), std::move(scheduler)); + this->schedulers[point] = targetScheduler; // it overrides preexisting scheduler for this point } template @@ -68,6 +82,7 @@ void SparsePcaaParetoQuery::exploreSetOfAchi WeightVector direction(this->objectives.size(), storm::utility::zero()); direction[objIndex] = storm::utility::one(); this->performRefinementStep(env, std::move(direction)); + this->updateSchedulers(); if (storm::utility::resources::isTerminate()) { break; } @@ -95,6 +110,7 @@ void SparsePcaaParetoQuery::exploreSetOfAchi STORM_LOG_INFO("Current precision of the approximation of the pareto curve is ~" << storm::utility::convertNumber(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."); } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h index cb8c8b490b..78248cd12f 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h @@ -31,11 +31,19 @@ class SparsePcaaParetoQuery : public SparsePcaaQuery 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::shared_ptr>> schedulers; }; } // namespace multiobjective diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp index 60c437ec0c..080629f002 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp @@ -61,7 +61,7 @@ void StandardPcaaWeightVectorChecker::initialize( obj.formula->gatherReferencedRewardModels(relevantRewardModels); } storm::transformer::GoalStateMerger merger(*preprocessorResult.preprocessedModel); - auto mergerResult = + mergerResult = merger.mergeTargetAndSinkStates(maybeStates, rewardAnalysis.reward0AStates, storm::storage::BitVector(maybeStates.size(), false), std::vector(relevantRewardModels.begin(), relevantRewardModels.end()), finiteTotalRewardChoices); @@ -235,6 +235,22 @@ StandardPcaaWeightVectorChecker::computeScheduler() const { return result; } +template +storm::storage::Scheduler::ValueType> +StandardPcaaWeightVectorChecker::computeOriginalScheduler() const { + auto scheduler = computeScheduler(); + for (int state=0; state(getUnderApproximationOfInitialStateResults()))); + return scheduler; +} + template void computeSchedulerProb1(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& consideredStates, storm::storage::BitVector const& statesToReach, std::vector& choices, diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h index ef58c5d40b..fe67e9fe0e 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h +++ b/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 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 computeOriginalScheduler() const override; + protected: void initialize(preprocessing::SparseMultiObjectivePreprocessorResult const& preprocessorResult); virtual void initializeModelTypeSpecificData(SparseModelType const& model) = 0; @@ -173,6 +180,9 @@ class StandardPcaaWeightVectorChecker : public PcaaWeightVectorChecker ecQuotient; + // Merge results + typename storm::transformer::GoalStateMerger::ReturnType mergerResult; + struct LraMecDecomposition { storm::storage::MaximalEndComponentDecomposition mecs; std::vector auxMecValues; From 97a2bfcbcad1625627cf8de3b015d31b97698621 Mon Sep 17 00:00:00 2001 From: Ulises Date: Mon, 13 Feb 2023 13:43:55 +0100 Subject: [PATCH 05/18] make format --- .../multiobjective/pcaa/SparsePcaaParetoQuery.cpp | 11 ++++------- .../multiobjective/pcaa/SparsePcaaParetoQuery.h | 1 + .../pcaa/StandardPcaaWeightVectorChecker.cpp | 10 ++++------ 3 files changed, 9 insertions(+), 13 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp index a0df74ae12..156040cc91 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp @@ -7,10 +7,10 @@ #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/StandardRewardModel.h" +#include "storm/storage/Scheduler.h" #include "storm/utility/SignalHandler.h" #include "storm/utility/constants.h" #include "storm/utility/vector.h" -#include "storm/storage/Scheduler.h" namespace storm { namespace modelchecker { @@ -63,13 +63,10 @@ std::unique_ptr SparsePcaaParetoQuery void SparsePcaaParetoQuery::updateSchedulers() { - auto scheduler = - std::make_shared>( - this->weightVectorChecker->computeOriginalScheduler()); + auto scheduler = std::make_shared>(this->weightVectorChecker->computeOriginalScheduler()); std::vector point = this->weightVectorChecker->getUnderApproximationOfInitialStateResults(); - auto targetScheduler = transformObjectiveSchedulerToOriginal( - std::make_shared(std::move(this->originalModel)), std::move(scheduler)); - this->schedulers[point] = targetScheduler; // it overrides preexisting scheduler for this point + auto targetScheduler = transformObjectiveSchedulerToOriginal(std::make_shared(std::move(this->originalModel)), std::move(scheduler)); + this->schedulers[point] = targetScheduler; // it overrides preexisting scheduler for this point } template diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h index 78248cd12f..6984aa2b5b 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h @@ -35,6 +35,7 @@ class SparsePcaaParetoQuery : public SparsePcaaQuery::computeScheduler() const { } template -storm::storage::Scheduler::ValueType> +storm::storage::Scheduler::ValueType> StandardPcaaWeightVectorChecker::computeOriginalScheduler() const { auto scheduler = computeScheduler(); - for (int state=0; state Date: Mon, 13 Feb 2023 13:44:24 +0100 Subject: [PATCH 06/18] storm-cli to allow scheduler exporting in multiobjective analysis --- src/storm-cli-utilities/model-handling.h | 18 +++++++++++++++++- src/storm/utility/vector.h | 19 +++++++++++++++++++ 2 files changed, 36 insertions(+), 1 deletion(-) diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 0476d1dc22..ae9dc2b3fa 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/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 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().hasScheduler()) { + auto schedulers = result->template asExplicitParetoCurveCheckResult().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()) { diff --git a/src/storm/utility/vector.h b/src/storm/utility/vector.h index 0a5e3be2fa..5390cc802f 100644 --- a/src/storm/utility/vector.h +++ b/src/storm/utility/vector.h @@ -1263,6 +1263,25 @@ std::string toString(std::vector const& vector) { stream << " ]"; return stream.str(); } + +/*! + * Less verbose, no space vector to string representation. + * @param vector Vector to output. + * @return String containing the representation of the vector. + */ +template +std::string toStringNoVerbose(std::vector const& vector) { + std::stringstream stream; + stream << "("; + if (!vector.empty()) { + for (uint_fast64_t i = 0; i < vector.size() - 1; ++i) { + stream << vector[i] << ","; + } + stream << vector.back(); + } + stream << ")"; + return stream.str(); +} } // namespace vector } // namespace utility } // namespace storm From 22635c97228ecf6419a9ce0f4cc3466ce6f103d5 Mon Sep 17 00:00:00 2001 From: Ulises Date: Mon, 13 Feb 2023 16:59:03 +0100 Subject: [PATCH 07/18] avoid recomputing scheduler if point is already stored --- .../multiobjective/pcaa/SparsePcaaParetoQuery.cpp | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp index 156040cc91..68c2828f22 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp @@ -63,10 +63,14 @@ std::unique_ptr SparsePcaaParetoQuery void SparsePcaaParetoQuery::updateSchedulers() { - auto scheduler = std::make_shared>(this->weightVectorChecker->computeOriginalScheduler()); std::vector point = this->weightVectorChecker->getUnderApproximationOfInitialStateResults(); - auto targetScheduler = transformObjectiveSchedulerToOriginal(std::make_shared(std::move(this->originalModel)), std::move(scheduler)); - this->schedulers[point] = targetScheduler; // it overrides preexisting scheduler for this point + if (!this->schedulers.count(point)){ + auto scheduler = std::make_shared>(this->weightVectorChecker->computeOriginalScheduler()); + std::vector vect; + vect.push_back(this->schedulers.size()+1); + auto targetScheduler = transformObjectiveSchedulerToOriginal(std::make_shared(std::move(this->originalModel)), std::move(scheduler)); + this->schedulers[vect] = targetScheduler; // it overrides preexisting scheduler for this point + } } template From 651cd2c553215fd55c865619d9e0ef686074ecf5 Mon Sep 17 00:00:00 2001 From: Ulises Date: Mon, 13 Feb 2023 22:41:49 +0100 Subject: [PATCH 08/18] fix compute original scheduler --- .../multiobjective/pcaa/SparsePcaaParetoQuery.cpp | 4 +--- .../pcaa/StandardPcaaWeightVectorChecker.cpp | 14 ++++++-------- 2 files changed, 7 insertions(+), 11 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp index 68c2828f22..da3c60a855 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp @@ -66,10 +66,8 @@ void SparsePcaaParetoQuery::updateSchedulers std::vector point = this->weightVectorChecker->getUnderApproximationOfInitialStateResults(); if (!this->schedulers.count(point)){ auto scheduler = std::make_shared>(this->weightVectorChecker->computeOriginalScheduler()); - std::vector vect; - vect.push_back(this->schedulers.size()+1); auto targetScheduler = transformObjectiveSchedulerToOriginal(std::make_shared(std::move(this->originalModel)), std::move(scheduler)); - this->schedulers[vect] = targetScheduler; // it overrides preexisting scheduler for this point + this->schedulers[point] = targetScheduler; // it overrides preexisting scheduler for this point } } diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp index 4cd85b413b..f696b5e051 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp @@ -238,15 +238,13 @@ StandardPcaaWeightVectorChecker::computeScheduler() const { template storm::storage::Scheduler::ValueType> StandardPcaaWeightVectorChecker::computeOriginalScheduler() const { - auto scheduler = computeScheduler(); - for (int state = 0; state < scheduler.getNumberOfChoices(); state++) { - for (int memory = 0; memory < scheduler.getNumberOfMemoryStates(); memory++) { - scheduler.setChoice(scheduler.getChoice(mergerResult.oldToNewStateIndexMapping[state], memory), state); - } + storm::storage::Scheduler result(this->optimalChoices.size()); + uint_fast64_t state = 0; + for (auto const& choice : optimalChoices) { + result.setChoice(optimalChoices[mergerResult.oldToNewStateIndexMapping[state]], state); + ++state; } - STORM_LOG_INFO("Original Scheduler calculated for: " - << storm::utility::vector::toString(storm::utility::vector::convertNumericVector(getUnderApproximationOfInitialStateResults()))); - return scheduler; + return result; } template From 199e49ff9d1e21baecb9df290e2056740151a3e6 Mon Sep 17 00:00:00 2001 From: Ulises Date: Mon, 13 Feb 2023 23:21:04 +0100 Subject: [PATCH 09/18] pcaa scheduler to original consider non trivial schedulers --- .../multiobjective/MultiObjectivePostprocessing.cpp | 6 +++--- .../pcaa/StandardPcaaWeightVectorChecker.cpp | 11 ++++++----- src/storm/storage/Scheduler.cpp | 5 +++++ src/storm/storage/Scheduler.h | 10 ++++------ 4 files changed, 18 insertions(+), 14 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp b/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp index dcba730726..b8a7145120 100644 --- a/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp +++ b/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp @@ -78,13 +78,13 @@ std::shared_ptr> transformObjectiveSchedule std::shared_ptr> scheduler) { storm::storage::Scheduler result(originalModel->getNumberOfStates()); // set common states - for (int state = 0; state < scheduler->getNumberOfChoices(); state++) { + for (int state = 0; state < scheduler->getNumberOfModelStates(); state++) { for (int memory = 0; memory < scheduler->getNumberOfMemoryStates(); memory++) { - result.setChoice(scheduler->getChoice(state, memory), state); + result.setChoice(scheduler->getChoice(state, memory), state, memory); } } // add irrelevant states removed in preprocessing - for (int state = scheduler->getNumberOfChoices(); state < originalModel->getNumberOfStates(); state++) { + for (int state = scheduler->getNumberOfModelStates(); state < originalModel->getNumberOfStates(); state++) { for (int memory = 0; memory < scheduler->getNumberOfMemoryStates(); memory++) { result.setDontCare(state, memory, false); } diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp index f696b5e051..5ee0b815a7 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp @@ -238,11 +238,12 @@ StandardPcaaWeightVectorChecker::computeScheduler() const { template storm::storage::Scheduler::ValueType> StandardPcaaWeightVectorChecker::computeOriginalScheduler() const { - storm::storage::Scheduler result(this->optimalChoices.size()); - uint_fast64_t state = 0; - for (auto const& choice : optimalChoices) { - result.setChoice(optimalChoices[mergerResult.oldToNewStateIndexMapping[state]], state); - ++state; + auto scheduler = this->computeScheduler(); + storm::storage::Scheduler result(scheduler.getNumberOfModelStates(), scheduler.getMemoryStructure()); + for (int state = 0; state < scheduler.getNumberOfModelStates(); state++) { + for (int memory = 0; memory < scheduler.getNumberOfMemoryStates(); memory++) { + result.setChoice(scheduler.getChoice(mergerResult.oldToNewStateIndexMapping[state], memory), state, memory); + } } return result; } diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp index 3cc57db960..135dda7b8a 100644 --- a/src/storm/storage/Scheduler.cpp +++ b/src/storm/storage/Scheduler.cpp @@ -159,6 +159,11 @@ uint_fast64_t Scheduler::getNumberOfMemoryStates() const { return memoryStructure ? memoryStructure->getNumberOfStates() : 1; } +template +uint_fast64_t Scheduler::getNumberOfModelStates() const { + return schedulerChoices.front().size(); +} + template boost::optional const& Scheduler::getMemoryStructure() const { return memoryStructure; diff --git a/src/storm/storage/Scheduler.h b/src/storm/storage/Scheduler.h index d7f970a0b2..4bf67f486a 100644 --- a/src/storm/storage/Scheduler.h +++ b/src/storm/storage/Scheduler.h @@ -56,12 +56,6 @@ class Scheduler { */ SchedulerChoice const& getChoice(uint_fast64_t modelState, uint_fast64_t memoryState = 0) const; - /*! - * Returns the ammount of stored choices in this scheduler. - */ - int getNumberOfChoices() const { - return schedulerChoices.front().size(); - } /*! * Set the combination of model state and memoryStructure state to dontCare. * These states are considered unreachable and are ignored when printing the scheduler. @@ -110,6 +104,10 @@ class Scheduler { * Retrieves the number of memory states this scheduler considers. */ uint_fast64_t getNumberOfMemoryStates() const; + /*! + * Retrieves the number of model states this scheduler considers. + */ + uint_fast64_t getNumberOfModelStates() const; /*! * Retrieves the memory structure associated with this scheduler From fce5e6026e8197795f8f277c0774f4f52856626c Mon Sep 17 00:00:00 2001 From: Ulises Date: Wed, 15 Feb 2023 09:59:19 +0100 Subject: [PATCH 10/18] transforming schedulers from incorporated memory models to schedulers with memory --- .../MultiObjectivePostprocessing.cpp | 67 +++++++++++++------ .../MultiObjectivePostprocessing.h | 6 +- .../multiObjectiveModelChecking.cpp | 12 ++++ .../pcaa/SparsePcaaParetoQuery.cpp | 7 +- .../pcaa/StandardPcaaWeightVectorChecker.cpp | 8 +-- .../SparseMultiObjectivePreprocessor.cpp | 14 +++- .../SparseMultiObjectivePreprocessor.h | 5 ++ .../SparseMultiObjectivePreprocessorResult.h | 5 ++ .../SparseModelMemoryProduct.h | 4 ++ .../SparseModelMemoryProductReverseData.h | 24 +++++++ src/storm/transformer/MemoryIncorporation.cpp | 6 +- src/storm/transformer/MemoryIncorporation.h | 5 +- 12 files changed, 124 insertions(+), 39 deletions(-) create mode 100644 src/storm/storage/memorystructure/SparseModelMemoryProductReverseData.h diff --git a/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp b/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp index b8a7145120..89bcc8f53f 100644 --- a/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp +++ b/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp @@ -4,6 +4,7 @@ #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 { @@ -74,22 +75,30 @@ std::shared_ptr> transform * (not the ones done by specific checkers) */ template -std::shared_ptr> transformObjectiveSchedulerToOriginal(std::shared_ptr const& originalModel, - std::shared_ptr> scheduler) { - storm::storage::Scheduler result(originalModel->getNumberOfStates()); - // set common states - for (int state = 0; state < scheduler->getNumberOfModelStates(); state++) { - for (int memory = 0; memory < scheduler->getNumberOfMemoryStates(); memory++) { - result.setChoice(scheduler->getChoice(state, memory), state, memory); - } - } - // add irrelevant states removed in preprocessing - for (int state = scheduler->getNumberOfModelStates(); state < originalModel->getNumberOfStates(); state++) { - for (int memory = 0; memory < scheduler->getNumberOfMemoryStates(); memory++) { - result.setDontCare(state, memory, false); +std::map, std::shared_ptr>> transformObjectiveSchedulersToOriginal( + storm::storage::SparseModelMemoryProductReverseData const& reverseData, std::shared_ptr const& originalModel, + std::map, std::shared_ptr>> schedulers) { + auto num = originalModel->getNumberOfStates(); + auto memoryStateCount = reverseData.memory.getNumberOfStates(); + + for (auto const& tuple : schedulers) { + std::shared_ptr> scheduler = tuple.second; + auto point = tuple.first; + storm::storage::Scheduler result(originalModel->getNumberOfStates(), reverseData.memory); + for (int state = 0; state < result.getNumberOfModelStates(); state++) { + for (int memState = 0; memState < memoryStateCount; memState++) { + auto const& productState = + reverseData.toResultStateMapping[state * memoryStateCount + memState]; // reverseData.getResultState(state, memState); + if (productState != -1) { + auto choice = scheduler->getChoice(productState); + result.setChoice(choice, state, memState); + } + } } + schedulers[point] = std::move(std::make_shared>(result)); } - return std::make_shared>(result); + + return schedulers; } template std::vector transformObjectiveValuesToOriginal(std::vector> objectives, @@ -100,16 +109,30 @@ template std::vector transformObjectiveValuesToOriginal(s std::vector const& point); template std::shared_ptr> transformObjectivePolytopeToOriginal( std::vector> objectives, std::shared_ptr> const& polytope); -template std::shared_ptr> transformObjectiveSchedulerToOriginal( + +template std::map, std::shared_ptr>> transformObjectiveSchedulersToOriginal( + storm::storage::SparseModelMemoryProductReverseData const& modelMemoryProduct, std::shared_ptr> const& originalModel, - std::shared_ptr> scheduler); -template std::shared_ptr> transformObjectiveSchedulerToOriginal( - std::shared_ptr> const& originalModel, std::shared_ptr> scheduler); -template std::shared_ptr> transformObjectiveSchedulerToOriginal( + // std::shared_ptr, std::shared_ptr>>> schedulers); + std::map, std::shared_ptr>> schedulers); + +template std::map, std::shared_ptr>> transformObjectiveSchedulersToOriginal( + storm::storage::SparseModelMemoryProductReverseData const& modelMemoryProduct, std::shared_ptr> const& originalModel, + // std::shared_ptr, std::shared_ptr>>> schedulers); + std::map, std::shared_ptr>> schedulers); + +template std::map, std::shared_ptr>> transformObjectiveSchedulersToOriginal( + storm::storage::SparseModelMemoryProductReverseData const& modelMemoryProduct, std::shared_ptr> const& originalModel, - std::shared_ptr> scheduler); -template std::shared_ptr> transformObjectiveSchedulerToOriginal( - std::shared_ptr> const& originalModel, std::shared_ptr> scheduler); + // std::shared_ptr, std::shared_ptr>>> schedulers); + std::map, std::shared_ptr>> schedulers); + +template std::map, std::shared_ptr>> transformObjectiveSchedulersToOriginal( + storm::storage::SparseModelMemoryProductReverseData const& modelMemoryProduct, + std::shared_ptr> const& originalModel, + // std::shared_ptr, std::shared_ptr>>> schedulers); + std::map, std::shared_ptr>> schedulers); + } // namespace multiobjective } // namespace modelchecker } // namespace storm \ No newline at end of file diff --git a/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.h b/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.h index 32c44ea086..168e962419 100644 --- a/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.h +++ b/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.h @@ -6,6 +6,7 @@ #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 { @@ -19,8 +20,9 @@ std::shared_ptr> transform std::vector> objectives, std::shared_ptr> const& polytope); template -std::shared_ptr> transformObjectiveSchedulerToOriginal(std::shared_ptr const& originalModel, - std::shared_ptr> scheduler); +std::map, std::shared_ptr>> transformObjectiveSchedulersToOriginal( + storm::storage::SparseModelMemoryProductReverseData const& modelMemoryProduct, std::shared_ptr const& originalModel, + std::map, std::shared_ptr>> schedulers); } // namespace multiobjective } // namespace modelchecker diff --git a/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp b/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp index a8065df454..c7f8dbb053 100644 --- a/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp +++ b/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" @@ -84,6 +87,15 @@ std::unique_ptr performMultiObjectiveModelChecking(Environment cons result = query->check(env); + if (preprocessorResult.memoryIncorporationReverseData && result->isExplicitParetoCurveCheckResult() && + result->template asExplicitParetoCurveCheckResult().hasScheduler()) { + // we have information to post-process schedulers + auto schedulers = result->template asExplicitParetoCurveCheckResult().getSchedulers(); + result->template asExplicitParetoCurveCheckResult().setSchedulers( + transformObjectiveSchedulersToOriginal(std::move(preprocessorResult.memoryIncorporationReverseData.value()), + std::make_shared(model), schedulers)); + } + if (env.modelchecker().multi().isExportPlotSet()) { query->exportPlotOfCurrentApproximation(env); } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp index da3c60a855..115fe7135a 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp @@ -64,10 +64,9 @@ std::unique_ptr SparsePcaaParetoQuery void SparsePcaaParetoQuery::updateSchedulers() { std::vector point = this->weightVectorChecker->getUnderApproximationOfInitialStateResults(); - if (!this->schedulers.count(point)){ - auto scheduler = std::make_shared>(this->weightVectorChecker->computeOriginalScheduler()); - auto targetScheduler = transformObjectiveSchedulerToOriginal(std::make_shared(std::move(this->originalModel)), std::move(scheduler)); - this->schedulers[point] = targetScheduler; // it overrides preexisting scheduler for this point + if (!this->schedulers.count(point)) { + this->schedulers[point] = + std::make_shared>(this->weightVectorChecker->computeOriginalScheduler()); } } diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp index 5ee0b815a7..9749fa5ccd 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp @@ -239,11 +239,9 @@ template storm::storage::Scheduler::ValueType> StandardPcaaWeightVectorChecker::computeOriginalScheduler() const { auto scheduler = this->computeScheduler(); - storm::storage::Scheduler result(scheduler.getNumberOfModelStates(), scheduler.getMemoryStructure()); - for (int state = 0; state < scheduler.getNumberOfModelStates(); state++) { - for (int memory = 0; memory < scheduler.getNumberOfMemoryStates(); memory++) { - result.setChoice(scheduler.getChoice(mergerResult.oldToNewStateIndexMapping[state], memory), state, memory); - } + storm::storage::Scheduler result(mergerResult.oldToNewStateIndexMapping.size()); + for (int state = 0; state < result.getNumberOfModelStates(); state++) { + result.setChoice(scheduler.getChoice(mergerResult.oldToNewStateIndexMapping[state]), state); } return result; } diff --git a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp index 0cd023781c..79dfef614f 100644 --- a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp @@ -14,6 +14,7 @@ #include "storm/settings/modules/GeneralSettings.h" #include "storm/storage/MaximalEndComponentDecomposition.h" #include "storm/storage/expressions/ExpressionManager.h" +#include "storm/storage/memorystructure/SparseModelMemoryProductReverseData.h" #include "storm/transformer/EndComponentEliminator.h" #include "storm/transformer/MemoryIncorporation.h" #include "storm/transformer/SubsystemBuilder.h" @@ -35,12 +36,16 @@ template typename SparseMultiObjectivePreprocessor::ReturnType SparseMultiObjectivePreprocessor::preprocess( Environment const& env, SparseModelType const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula) { std::shared_ptr model; + boost::optional memoryIncorporationReverseData; // Incorporate the necessary memory if (env.modelchecker().multi().isSchedulerRestrictionSet()) { auto const& schedRestr = env.modelchecker().multi().getSchedulerRestriction(); if (schedRestr.getMemoryPattern() == storm::storage::SchedulerClass::MemoryPattern::GoalMemory) { - model = storm::transformer::MemoryIncorporation::incorporateGoalMemory(originalModel, originalFormula.getSubformulas()); + // trying to do "auto [model, modelMemoryProduct]" causes seg fault when trying to access model + auto res = storm::transformer::MemoryIncorporation::incorporateGoalMemory(originalModel, originalFormula.getSubformulas()); + model = std::move(std::get<0>(res)); + memoryIncorporationReverseData = std::move(std::get<1>(res)); } else if (schedRestr.getMemoryPattern() == storm::storage::SchedulerClass::MemoryPattern::Arbitrary && schedRestr.getMemoryStates() > 1) { model = storm::transformer::MemoryIncorporation::incorporateFullMemory(originalModel, schedRestr.getMemoryStates()); } else if (schedRestr.getMemoryPattern() == storm::storage::SchedulerClass::MemoryPattern::Counter && schedRestr.getMemoryStates() > 1) { @@ -51,7 +56,10 @@ typename SparseMultiObjectivePreprocessor::ReturnType SparseMul STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The given scheduler restriction has not been implemented."); } } else { - model = storm::transformer::MemoryIncorporation::incorporateGoalMemory(originalModel, originalFormula.getSubformulas()); + // trying to do "auto [model, modelMemoryProduct]" causes seg fault when trying to access model + auto res = storm::transformer::MemoryIncorporation::incorporateGoalMemory(originalModel, originalFormula.getSubformulas()); + model = std::move(std::get<0>(res)); + memoryIncorporationReverseData = std::move(std::get<1>(res)); } // Remove states that are irrelevant for all properties (e.g. because they are only reachable via goal states @@ -60,6 +68,7 @@ typename SparseMultiObjectivePreprocessor::ReturnType SparseMul PreprocessorData data(model); data.deadlockLabel = deadlockLabel; + data.memoryIncorporationReverseData = std::move(memoryIncorporationReverseData); // Invoke preprocessing on the individual objectives for (auto const& subFormula : originalFormula.getSubformulas()) { @@ -726,6 +735,7 @@ typename SparseMultiObjectivePreprocessor::ReturnType SparseMul ReturnType result(originalFormula, originalModel); auto backwardTransitions = data.model->getBackwardTransitions(); result.preprocessedModel = data.model; + result.memoryIncorporationReverseData = std::move(data.memoryIncorporationReverseData); for (auto& obj : data.objectives) { result.objectives.push_back(std::move(*obj)); diff --git a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.h b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.h index da5981991e..fa6c2c740b 100644 --- a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.h +++ b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.h @@ -7,6 +7,8 @@ #include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h" #include "storm/storage/BitVector.h" #include "storm/storage/memorystructure/MemoryStructure.h" +#include "storm/storage/memorystructure/SparseModelMemoryProduct.h" +#include "storm/storage/memorystructure/SparseModelMemoryProductReverseData.h" namespace storm { @@ -49,6 +51,9 @@ class SparseMultiObjectivePreprocessor { // If set, some states have been merged to a deadlock state with this label. boost::optional deadlockLabel; + // Mapping of incorporated memory to model+memory + boost::optional memoryIncorporationReverseData; + PreprocessorData(std::shared_ptr model); }; diff --git a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h index 6e708790f1..6e058826e6 100644 --- a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h +++ b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h @@ -7,6 +7,8 @@ #include "storm/logic/Formulas.h" #include "storm/modelchecker/multiobjective/Objective.h" #include "storm/storage/BitVector.h" +#include "storm/storage/memorystructure/SparseModelMemoryProduct.h" +#include "storm/storage/memorystructure/SparseModelMemoryProductReverseData.h" #include "storm/exceptions/UnexpectedException.h" @@ -23,6 +25,9 @@ struct SparseMultiObjectivePreprocessorResult { storm::logic::MultiObjectiveFormula const& originalFormula; SparseModelType const& originalModel; + // Mapping of incorporated memory to model+memory + boost::optional memoryIncorporationReverseData; + // The preprocessed model and objectives std::shared_ptr preprocessedModel; std::vector> objectives; diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.h b/src/storm/storage/memorystructure/SparseModelMemoryProduct.h index 017bbb30cd..9742e12db1 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.h +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.h @@ -52,6 +52,10 @@ class SparseModelMemoryProduct { storm::models::sparse::Model const& getOriginalModel() const; storm::storage::MemoryStructure const& getMemory() const; + std::vector getResultStateMapping() { + return toResultStateMapping; + } + private: // Initializes auxiliary data for building the product void initialize(); diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProductReverseData.h b/src/storm/storage/memorystructure/SparseModelMemoryProductReverseData.h new file mode 100644 index 0000000000..89d5e4a43e --- /dev/null +++ b/src/storm/storage/memorystructure/SparseModelMemoryProductReverseData.h @@ -0,0 +1,24 @@ +#pragma once + +#include +#include +#include +#include "storm/storage/memorystructure/MemoryStructure.h" + +namespace storm { +namespace storage { +// Data to restore memory incorporation applied with SparseModelMemoryProduct +// Only stores the least necessary to reverse data from SparseModelMemoryProduct +struct SparseModelMemoryProductReverseData { + storm::storage::MemoryStructure memory; + // Maps (modelState * memoryStateCount) + memoryState to the state in the result that represents (memoryState,modelState) + std::vector toResultStateMapping; + + SparseModelMemoryProductReverseData(storm::storage::MemoryStructure const& memory, std::vector const& toResultStateMapping) + : memory(memory), toResultStateMapping(toResultStateMapping) { + // Intentionally left empty + } +}; + +} // namespace storage +} // namespace storm diff --git a/src/storm/transformer/MemoryIncorporation.cpp b/src/storm/transformer/MemoryIncorporation.cpp index 18a2fc38c4..a4de1c4e2d 100644 --- a/src/storm/transformer/MemoryIncorporation.cpp +++ b/src/storm/transformer/MemoryIncorporation.cpp @@ -10,6 +10,7 @@ #include "storm/storage/memorystructure/MemoryStructureBuilder.h" #include "storm/storage/memorystructure/NondeterministicMemoryStructureBuilder.h" #include "storm/storage/memorystructure/SparseModelMemoryProduct.h" +#include "storm/storage/memorystructure/SparseModelMemoryProductReverseData.h" #include "storm/storage/memorystructure/SparseModelNondeterministicMemoryProduct.h" #include "storm/utility/macros.h" @@ -56,7 +57,7 @@ storm::storage::MemoryStructure getUntilFormulaMemory(SparseModelType const& mod } template -std::shared_ptr MemoryIncorporation::incorporateGoalMemory( +std::tuple, storm::storage::SparseModelMemoryProductReverseData> MemoryIncorporation::incorporateGoalMemory( SparseModelType const& model, std::vector> const& formulas) { storm::storage::MemoryStructure memory = storm::storage::MemoryStructureBuilder::buildTrivialMemoryStructure(model); @@ -87,7 +88,8 @@ std::shared_ptr MemoryIncorporation::incorpora } storm::storage::SparseModelMemoryProduct product = memory.product(model); - return std::dynamic_pointer_cast(product.build()); + return std::make_tuple(std::dynamic_pointer_cast(product.build()), + storm::storage::SparseModelMemoryProductReverseData(product.getMemory(), product.getResultStateMapping())); } template diff --git a/src/storm/transformer/MemoryIncorporation.h b/src/storm/transformer/MemoryIncorporation.h index 2bea33690a..5040b50b18 100644 --- a/src/storm/transformer/MemoryIncorporation.h +++ b/src/storm/transformer/MemoryIncorporation.h @@ -5,6 +5,7 @@ #include "storm/logic/Formula.h" #include "storm/logic/MultiObjectiveFormula.h" #include "storm/storage/memorystructure/MemoryStructure.h" +#include "storm/storage/memorystructure/SparseModelMemoryProductReverseData.h" namespace storm { namespace transformer { @@ -24,8 +25,8 @@ class MemoryIncorporation { * Incorporates memory that stores whether a 'goal' state has already been reached. This supports operatorformulas whose subformula is * a (bounded-) until formula, eventually formula, or a globally formula. Total reward formulas and cumulative reward formulas will be ignored. */ - static std::shared_ptr incorporateGoalMemory(SparseModelType const& model, - std::vector> const& formulas); + static std::tuple, storm::storage::SparseModelMemoryProductReverseData> incorporateGoalMemory( + SparseModelType const& model, std::vector> const& formulas); /*! * Incorporates a memory structure where the nondeterminism of the model decides which successor state to choose. From cf5210308852a5ad881f9c7f96a0d933883a2c04 Mon Sep 17 00:00:00 2001 From: Ulises Date: Wed, 15 Feb 2023 10:58:55 +0100 Subject: [PATCH 11/18] flag to compute schedulers only when exportScheduler is needed in multiobjective --- .../multiobjective/pcaa/SparsePcaaParetoQuery.cpp | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp index 115fe7135a..15f3080595 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp @@ -11,6 +11,9 @@ #include "storm/utility/SignalHandler.h" #include "storm/utility/constants.h" #include "storm/utility/vector.h" +#include "storm/settings/modules/IOSettings.h" +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/CoreSettings.h" namespace storm { namespace modelchecker { @@ -63,10 +66,12 @@ std::unique_ptr SparsePcaaParetoQuery void SparsePcaaParetoQuery::updateSchedulers() { - std::vector point = this->weightVectorChecker->getUnderApproximationOfInitialStateResults(); - if (!this->schedulers.count(point)) { - this->schedulers[point] = - std::make_shared>(this->weightVectorChecker->computeOriginalScheduler()); + if (storm::settings::getModule().isExportSchedulerSet()) { + std::vector point = this->weightVectorChecker->getUnderApproximationOfInitialStateResults(); + if (!this->schedulers.count(point)) { + this->schedulers[point] = + std::make_shared>(this->weightVectorChecker->computeOriginalScheduler()); + } } } From 67703061da809a7143d2a23dd916b099ac0e0a7c Mon Sep 17 00:00:00 2001 From: Ulises Date: Wed, 15 Feb 2023 12:02:28 +0100 Subject: [PATCH 12/18] make format --- .../multiobjective/pcaa/SparsePcaaParetoQuery.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp index 15f3080595..ce65178f45 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp @@ -7,13 +7,13 @@ #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" -#include "storm/settings/modules/IOSettings.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/CoreSettings.h" namespace storm { namespace modelchecker { From 186f4a4e822e9c6d96aee7719f72c26b6eb74986 Mon Sep 17 00:00:00 2001 From: Ulises Date: Thu, 16 Feb 2023 10:41:56 +0100 Subject: [PATCH 13/18] standard pcaa vector checker only stores needed information from merge result --- .../pcaa/StandardPcaaWeightVectorChecker.cpp | 8 ++++---- .../multiobjective/pcaa/StandardPcaaWeightVectorChecker.h | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp index 9749fa5ccd..a5326f2fa2 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp @@ -61,10 +61,10 @@ void StandardPcaaWeightVectorChecker::initialize( obj.formula->gatherReferencedRewardModels(relevantRewardModels); } storm::transformer::GoalStateMerger merger(*preprocessorResult.preprocessedModel); - mergerResult = + auto mergerResult = merger.mergeTargetAndSinkStates(maybeStates, rewardAnalysis.reward0AStates, storm::storage::BitVector(maybeStates.size(), false), std::vector(relevantRewardModels.begin(), relevantRewardModels.end()), finiteTotalRewardChoices); - + goalStateMergerIndexMapping = mergerResult.oldToNewStateIndexMapping; // Initialize data specific for the considered model type initializeModelTypeSpecificData(*mergerResult.model); @@ -239,9 +239,9 @@ template storm::storage::Scheduler::ValueType> StandardPcaaWeightVectorChecker::computeOriginalScheduler() const { auto scheduler = this->computeScheduler(); - storm::storage::Scheduler result(mergerResult.oldToNewStateIndexMapping.size()); + storm::storage::Scheduler result(goalStateMergerIndexMapping.size()); for (int state = 0; state < result.getNumberOfModelStates(); state++) { - result.setChoice(scheduler.getChoice(mergerResult.oldToNewStateIndexMapping[state]), state); + result.setChoice(scheduler.getChoice(goalStateMergerIndexMapping[state]), state); } return result; } diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h index fe67e9fe0e..7adcb8751b 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h @@ -181,7 +181,7 @@ class StandardPcaaWeightVectorChecker : public PcaaWeightVectorChecker ecQuotient; // Merge results - typename storm::transformer::GoalStateMerger::ReturnType mergerResult; + std::vector goalStateMergerIndexMapping; struct LraMecDecomposition { storm::storage::MaximalEndComponentDecomposition mecs; From 59de1576f8fc70ba8b6ee2e19b3bf8c71eb91f46 Mon Sep 17 00:00:00 2001 From: Ulises Date: Thu, 16 Feb 2023 22:31:49 +0100 Subject: [PATCH 14/18] multiobjective scheduler postprocessing set dont care to irrelevant states deleted in preprocessing --- .../MultiObjectivePostprocessing.cpp | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp b/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp index 89bcc8f53f..5b4f05ccf6 100644 --- a/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp +++ b/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp @@ -78,7 +78,6 @@ template std::map, std::shared_ptr>> transformObjectiveSchedulersToOriginal( storm::storage::SparseModelMemoryProductReverseData const& reverseData, std::shared_ptr const& originalModel, std::map, std::shared_ptr>> schedulers) { - auto num = originalModel->getNumberOfStates(); auto memoryStateCount = reverseData.memory.getNumberOfStates(); for (auto const& tuple : schedulers) { @@ -88,11 +87,19 @@ std::map, std::shared_ptrgetChoice(productState); - result.setChoice(choice, state, memState); + // if it's -1 it's unreachable + if (productState>=scheduler->getNumberOfModelStates()) { + // means it's been deleted as irrelevant state + result.setDontCare(productState, memState, true); + } + else { + auto choice = scheduler->getChoice(productState); + result.setChoice(choice, state, memState); + } } + } } schedulers[point] = std::move(std::make_shared>(result)); From fe39c84caebc89ad497cca2dafc6a9d7672ec21f Mon Sep 17 00:00:00 2001 From: Ulises Date: Mon, 20 Feb 2023 01:50:41 +0100 Subject: [PATCH 15/18] fixed bug only happening on release build --- .../preprocessing/SparseMultiObjectivePreprocessor.cpp | 10 +++++----- src/storm/transformer/MemoryIncorporation.cpp | 3 ++- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp index 79dfef614f..17ec3fd000 100644 --- a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp @@ -44,8 +44,8 @@ typename SparseMultiObjectivePreprocessor::ReturnType SparseMul if (schedRestr.getMemoryPattern() == storm::storage::SchedulerClass::MemoryPattern::GoalMemory) { // trying to do "auto [model, modelMemoryProduct]" causes seg fault when trying to access model auto res = storm::transformer::MemoryIncorporation::incorporateGoalMemory(originalModel, originalFormula.getSubformulas()); - model = std::move(std::get<0>(res)); - memoryIncorporationReverseData = std::move(std::get<1>(res)); + model = std::get<0>(res); + memoryIncorporationReverseData = std::get<1>(res); } else if (schedRestr.getMemoryPattern() == storm::storage::SchedulerClass::MemoryPattern::Arbitrary && schedRestr.getMemoryStates() > 1) { model = storm::transformer::MemoryIncorporation::incorporateFullMemory(originalModel, schedRestr.getMemoryStates()); } else if (schedRestr.getMemoryPattern() == storm::storage::SchedulerClass::MemoryPattern::Counter && schedRestr.getMemoryStates() > 1) { @@ -58,8 +58,8 @@ typename SparseMultiObjectivePreprocessor::ReturnType SparseMul } else { // trying to do "auto [model, modelMemoryProduct]" causes seg fault when trying to access model auto res = storm::transformer::MemoryIncorporation::incorporateGoalMemory(originalModel, originalFormula.getSubformulas()); - model = std::move(std::get<0>(res)); - memoryIncorporationReverseData = std::move(std::get<1>(res)); + model = std::get<0>(res); + memoryIncorporationReverseData = std::get<1>(res); } // Remove states that are irrelevant for all properties (e.g. because they are only reachable via goal states @@ -735,7 +735,7 @@ typename SparseMultiObjectivePreprocessor::ReturnType SparseMul ReturnType result(originalFormula, originalModel); auto backwardTransitions = data.model->getBackwardTransitions(); result.preprocessedModel = data.model; - result.memoryIncorporationReverseData = std::move(data.memoryIncorporationReverseData); + result.memoryIncorporationReverseData = data.memoryIncorporationReverseData; for (auto& obj : data.objectives) { result.objectives.push_back(std::move(*obj)); diff --git a/src/storm/transformer/MemoryIncorporation.cpp b/src/storm/transformer/MemoryIncorporation.cpp index a4de1c4e2d..7adf7e7a00 100644 --- a/src/storm/transformer/MemoryIncorporation.cpp +++ b/src/storm/transformer/MemoryIncorporation.cpp @@ -88,7 +88,8 @@ std::tuple, storm::storage::SparseModelMemoryPr } storm::storage::SparseModelMemoryProduct product = memory.product(model); - return std::make_tuple(std::dynamic_pointer_cast(product.build()), + auto result = std::dynamic_pointer_cast(product.build()); + return std::make_tuple(result, storm::storage::SparseModelMemoryProductReverseData(product.getMemory(), product.getResultStateMapping())); } From 423d01de6fee05b1b5122fd66c245238551ae40e Mon Sep 17 00:00:00 2001 From: Ulises Date: Tue, 21 Feb 2023 09:58:34 +0100 Subject: [PATCH 16/18] optimizations and improvements for scheduler export in multiobjective modelchecking --- .../MultiObjectivePostprocessing.cpp | 47 +++++++++---------- .../MultiObjectivePostprocessing.h | 10 ++-- .../multiObjectiveModelChecking.cpp | 6 +-- .../pcaa/SparsePcaaParetoQuery.cpp | 8 ++-- .../pcaa/StandardPcaaWeightVectorChecker.cpp | 3 +- .../ExplicitParetoCurveCheckResult.cpp | 10 ++++ .../results/ExplicitParetoCurveCheckResult.h | 5 ++ src/storm/storage/Scheduler.cpp | 2 +- src/storm/transformer/MemoryIncorporation.cpp | 3 +- 9 files changed, 53 insertions(+), 41 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp b/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp index 5b4f05ccf6..a61e695248 100644 --- a/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp +++ b/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp @@ -75,37 +75,34 @@ std::shared_ptr> transform * (not the ones done by specific checkers) */ template -std::map, std::shared_ptr>> transformObjectiveSchedulersToOriginal( - storm::storage::SparseModelMemoryProductReverseData const& reverseData, std::shared_ptr const& originalModel, - std::map, std::shared_ptr>> schedulers) { +void transformObjectiveSchedulersToOriginal(storm::storage::SparseModelMemoryProductReverseData const& reverseData, + std::shared_ptr const& originalModel, + std::map, std::shared_ptr>> schedulers) { auto memoryStateCount = reverseData.memory.getNumberOfStates(); - - for (auto const& tuple : schedulers) { - std::shared_ptr> scheduler = tuple.second; - auto point = tuple.first; - storm::storage::Scheduler result(originalModel->getNumberOfStates(), reverseData.memory); - for (int state = 0; state < result.getNumberOfModelStates(); state++) { + auto originalModelStates = originalModel->getNumberOfStates(); + for (auto it = schedulers.begin(); it != schedulers.end(); ++it) { + std::shared_ptr> scheduler = it->second; + auto point = it->first; + storm::storage::Scheduler 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]; + auto const& productState = reverseData.toResultStateMapping[state * memoryStateCount + memState]; if (productState != -1) { // if it's -1 it's unreachable - if (productState>=scheduler->getNumberOfModelStates()) { + if (productState >= currSchedulerModelStates) { // means it's been deleted as irrelevant state result.setDontCare(productState, memState, true); - } - else { + } else { auto choice = scheduler->getChoice(productState); result.setChoice(choice, state, memState); } } - } } + scheduler.reset(); schedulers[point] = std::move(std::make_shared>(result)); } - - return schedulers; } template std::vector transformObjectiveValuesToOriginal(std::vector> objectives, @@ -117,25 +114,25 @@ template std::vector transformObjectiveValuesToOriginal(s template std::shared_ptr> transformObjectivePolytopeToOriginal( std::vector> objectives, std::shared_ptr> const& polytope); -template std::map, std::shared_ptr>> transformObjectiveSchedulersToOriginal( - storm::storage::SparseModelMemoryProductReverseData const& modelMemoryProduct, +template void transformObjectiveSchedulersToOriginal( + storm::storage::SparseModelMemoryProductReverseData const& reverseData, std::shared_ptr> const& originalModel, // std::shared_ptr, std::shared_ptr>>> schedulers); std::map, std::shared_ptr>> schedulers); -template std::map, std::shared_ptr>> transformObjectiveSchedulersToOriginal( - storm::storage::SparseModelMemoryProductReverseData const& modelMemoryProduct, std::shared_ptr> const& originalModel, +template void transformObjectiveSchedulersToOriginal( + storm::storage::SparseModelMemoryProductReverseData const& reverseData, std::shared_ptr> const& originalModel, // std::shared_ptr, std::shared_ptr>>> schedulers); std::map, std::shared_ptr>> schedulers); -template std::map, std::shared_ptr>> transformObjectiveSchedulersToOriginal( - storm::storage::SparseModelMemoryProductReverseData const& modelMemoryProduct, +template void transformObjectiveSchedulersToOriginal( + storm::storage::SparseModelMemoryProductReverseData const& reverseData, std::shared_ptr> const& originalModel, // std::shared_ptr, std::shared_ptr>>> schedulers); std::map, std::shared_ptr>> schedulers); -template std::map, std::shared_ptr>> transformObjectiveSchedulersToOriginal( - storm::storage::SparseModelMemoryProductReverseData const& modelMemoryProduct, +template void transformObjectiveSchedulersToOriginal( + storm::storage::SparseModelMemoryProductReverseData const& reverseData, std::shared_ptr> const& originalModel, // std::shared_ptr, std::shared_ptr>>> schedulers); std::map, std::shared_ptr>> schedulers); diff --git a/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.h b/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.h index 168e962419..927da19b8e 100644 --- a/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.h +++ b/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.h @@ -19,10 +19,14 @@ template std::shared_ptr> transformObjectivePolytopeToOriginal( std::vector> objectives, std::shared_ptr> const& polytope); +/* + * Uses the information from reverse data to edit the objective schedulers in 'schedulers' to ones + * apt for the target model. + */ template -std::map, std::shared_ptr>> transformObjectiveSchedulersToOriginal( - storm::storage::SparseModelMemoryProductReverseData const& modelMemoryProduct, std::shared_ptr const& originalModel, - std::map, std::shared_ptr>> schedulers); +void transformObjectiveSchedulersToOriginal(storm::storage::SparseModelMemoryProductReverseData const& reverseData, + std::shared_ptr const& originalModel, + std::map, std::shared_ptr>> schedulers); } // namespace multiobjective } // namespace modelchecker diff --git a/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp b/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp index c7f8dbb053..e774316c25 100644 --- a/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp +++ b/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp @@ -86,14 +86,12 @@ std::unique_ptr performMultiObjectiveModelChecking(Environment cons } result = query->check(env); - if (preprocessorResult.memoryIncorporationReverseData && result->isExplicitParetoCurveCheckResult() && result->template asExplicitParetoCurveCheckResult().hasScheduler()) { // we have information to post-process schedulers auto schedulers = result->template asExplicitParetoCurveCheckResult().getSchedulers(); - result->template asExplicitParetoCurveCheckResult().setSchedulers( - transformObjectiveSchedulersToOriginal(std::move(preprocessorResult.memoryIncorporationReverseData.value()), - std::make_shared(model), schedulers)); + transformObjectiveSchedulersToOriginal(std::move(preprocessorResult.memoryIncorporationReverseData.value()), + std::make_shared(model), schedulers); } if (env.modelchecker().multi().isExportPlotSet()) { diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp index ce65178f45..87e770364e 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp @@ -54,14 +54,12 @@ std::unique_ptr SparsePcaaParetoQuery(transformObjectiveValuesToOriginal(this->objectives, vertex))); } - auto result = new ExplicitParetoCurveCheckResult( - this->originalModel.getInitialStates().getNextSetIndex(0), std::move(paretoOptimalPoints), + return std::unique_ptr(new ExplicitParetoCurveCheckResult( + this->originalModel.getInitialStates().getNextSetIndex(0), std::move(paretoOptimalPoints), std::move(schedulers), transformObjectivePolytopeToOriginal(this->objectives, this->underApproximation) ->template convertNumberRepresentation(), transformObjectivePolytopeToOriginal(this->objectives, this->overApproximation) - ->template convertNumberRepresentation()); - result->setSchedulers(std::move(schedulers)); - return std::unique_ptr(result); + ->template convertNumberRepresentation())); } template diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp index a5326f2fa2..87729957b4 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp @@ -240,7 +240,8 @@ storm::storage::Scheduler::computeOriginalScheduler() const { auto scheduler = this->computeScheduler(); storm::storage::Scheduler result(goalStateMergerIndexMapping.size()); - for (int state = 0; state < result.getNumberOfModelStates(); state++) { + auto numOfModelStates = result.getNumberOfModelStates(); + for (int state = 0; state < numOfModelStates; state++) { result.setChoice(scheduler.getChoice(goalStateMergerIndexMapping[state]), state); } return result; diff --git a/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp index 00834a76ba..34a53a52fa 100644 --- a/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp +++ b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp @@ -33,6 +33,16 @@ ExplicitParetoCurveCheckResult::ExplicitParetoCurveCheckResult(storm: // Intentionally left empty. } +template +ExplicitParetoCurveCheckResult::ExplicitParetoCurveCheckResult( + storm::storage::sparse::state_type const& state, std::vector::point_type>&& points, + std::map, std::shared_ptr>>&& schedulers, + typename ParetoCurveCheckResult::polytope_type&& underApproximation, + typename ParetoCurveCheckResult::polytope_type&& overApproximation) + : ParetoCurveCheckResult(points, underApproximation, overApproximation), state(state), schedulers(schedulers) { + // Intentionally left empty. +} + template std::unique_ptr ExplicitParetoCurveCheckResult::clone() const { return std::make_unique>(this->state, this->points, this->underApproximation, this->overApproximation); diff --git a/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.h b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.h index d2cd0ab219..9393368ef2 100644 --- a/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.h +++ b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.h @@ -22,6 +22,11 @@ class ExplicitParetoCurveCheckResult : public ParetoCurveCheckResult std::vector::point_type>&& points, typename ParetoCurveCheckResult::polytope_type&& underApproximation = nullptr, typename ParetoCurveCheckResult::polytope_type&& overApproximation = nullptr); + ExplicitParetoCurveCheckResult(storm::storage::sparse::state_type const& state, + std::vector::point_type>&& points, + std::map, std::shared_ptr>>&& schedulers, + typename ParetoCurveCheckResult::polytope_type&& underApproximation = nullptr, + typename ParetoCurveCheckResult::polytope_type&& overApproximation = nullptr); ExplicitParetoCurveCheckResult(ExplicitParetoCurveCheckResult const& other) = default; ExplicitParetoCurveCheckResult& operator=(ExplicitParetoCurveCheckResult const& other) = default; diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp index 135dda7b8a..82bc5caea6 100644 --- a/src/storm/storage/Scheduler.cpp +++ b/src/storm/storage/Scheduler.cpp @@ -161,7 +161,7 @@ uint_fast64_t Scheduler::getNumberOfMemoryStates() const { template uint_fast64_t Scheduler::getNumberOfModelStates() const { - return schedulerChoices.front().size(); + return schedulerChoices.empty() ? 0 : schedulerChoices.front().size(); } template diff --git a/src/storm/transformer/MemoryIncorporation.cpp b/src/storm/transformer/MemoryIncorporation.cpp index 7adf7e7a00..79b5994bca 100644 --- a/src/storm/transformer/MemoryIncorporation.cpp +++ b/src/storm/transformer/MemoryIncorporation.cpp @@ -89,8 +89,7 @@ std::tuple, storm::storage::SparseModelMemoryPr storm::storage::SparseModelMemoryProduct product = memory.product(model); auto result = std::dynamic_pointer_cast(product.build()); - return std::make_tuple(result, - storm::storage::SparseModelMemoryProductReverseData(product.getMemory(), product.getResultStateMapping())); + return std::make_tuple(result, storm::storage::SparseModelMemoryProductReverseData(product.getMemory(), product.getResultStateMapping())); } template From 8e0a4c13a311f6de2e1a334b6dc056653a909325 Mon Sep 17 00:00:00 2001 From: Ulises Date: Fri, 10 Mar 2023 11:26:23 +0100 Subject: [PATCH 17/18] remove leftover comments --- .../multiobjective/MultiObjectivePostprocessing.cpp | 4 ---- .../modelchecker/results/ExplicitParetoCurveCheckResult.cpp | 1 - .../modelchecker/results/ExplicitParetoCurveCheckResult.h | 2 +- 3 files changed, 1 insertion(+), 6 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp b/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp index a61e695248..263b760f4a 100644 --- a/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp +++ b/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp @@ -117,24 +117,20 @@ template std::shared_ptr> const& originalModel, - // std::shared_ptr, std::shared_ptr>>> schedulers); std::map, std::shared_ptr>> schedulers); template void transformObjectiveSchedulersToOriginal( storm::storage::SparseModelMemoryProductReverseData const& reverseData, std::shared_ptr> const& originalModel, - // std::shared_ptr, std::shared_ptr>>> schedulers); std::map, std::shared_ptr>> schedulers); template void transformObjectiveSchedulersToOriginal( storm::storage::SparseModelMemoryProductReverseData const& reverseData, std::shared_ptr> const& originalModel, - // std::shared_ptr, std::shared_ptr>>> schedulers); std::map, std::shared_ptr>> schedulers); template void transformObjectiveSchedulersToOriginal( storm::storage::SparseModelMemoryProductReverseData const& reverseData, std::shared_ptr> const& originalModel, - // std::shared_ptr, std::shared_ptr>>> schedulers); std::map, std::shared_ptr>> schedulers); } // namespace multiobjective diff --git a/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp index 34a53a52fa..af8468fb23 100644 --- a/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp +++ b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp @@ -40,7 +40,6 @@ ExplicitParetoCurveCheckResult::ExplicitParetoCurveCheckResult( typename ParetoCurveCheckResult::polytope_type&& underApproximation, typename ParetoCurveCheckResult::polytope_type&& overApproximation) : ParetoCurveCheckResult(points, underApproximation, overApproximation), state(state), schedulers(schedulers) { - // Intentionally left empty. } template diff --git a/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.h b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.h index 9393368ef2..90e8422957 100644 --- a/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.h +++ b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.h @@ -44,7 +44,7 @@ class ExplicitParetoCurveCheckResult : public ParetoCurveCheckResult storm::storage::sparse::state_type const& getState() const; virtual bool hasScheduler() const override; - // void addScheduler(const std::shared_ptr>& scheduler); + void setSchedulers(std::map, std::shared_ptr>> schedulers); std::map, std::shared_ptr>> const& getSchedulers() const; From e186866a73b7fbb3206393ed181996059c2a2694 Mon Sep 17 00:00:00 2001 From: Ulises Date: Fri, 10 Mar 2023 11:50:22 +0100 Subject: [PATCH 18/18] fix format --- .../multiobjective/MultiObjectivePostprocessing.cpp | 13 ++++++------- .../results/ExplicitParetoCurveCheckResult.cpp | 3 +-- 2 files changed, 7 insertions(+), 9 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp b/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp index 263b760f4a..7f92c3a994 100644 --- a/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp +++ b/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp @@ -119,19 +119,18 @@ template void transformObjectiveSchedulersToOriginal( std::shared_ptr> const& originalModel, std::map, std::shared_ptr>> schedulers); -template void transformObjectiveSchedulersToOriginal( - storm::storage::SparseModelMemoryProductReverseData const& reverseData, std::shared_ptr> const& originalModel, - std::map, std::shared_ptr>> schedulers); +template void transformObjectiveSchedulersToOriginal(storm::storage::SparseModelMemoryProductReverseData const& reverseData, + std::shared_ptr> const& originalModel, + std::map, std::shared_ptr>> schedulers); template void transformObjectiveSchedulersToOriginal( storm::storage::SparseModelMemoryProductReverseData const& reverseData, std::shared_ptr> const& originalModel, std::map, std::shared_ptr>> schedulers); -template void transformObjectiveSchedulersToOriginal( - storm::storage::SparseModelMemoryProductReverseData const& reverseData, - std::shared_ptr> const& originalModel, - std::map, std::shared_ptr>> schedulers); +template void transformObjectiveSchedulersToOriginal(storm::storage::SparseModelMemoryProductReverseData const& reverseData, + std::shared_ptr> const& originalModel, + std::map, std::shared_ptr>> schedulers); } // namespace multiobjective } // namespace modelchecker diff --git a/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp index af8468fb23..e9d2ee00dc 100644 --- a/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp +++ b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp @@ -39,8 +39,7 @@ ExplicitParetoCurveCheckResult::ExplicitParetoCurveCheckResult( std::map, std::shared_ptr>>&& schedulers, typename ParetoCurveCheckResult::polytope_type&& underApproximation, typename ParetoCurveCheckResult::polytope_type&& overApproximation) - : ParetoCurveCheckResult(points, underApproximation, overApproximation), state(state), schedulers(schedulers) { -} + : ParetoCurveCheckResult(points, underApproximation, overApproximation), state(state), schedulers(schedulers) {} template std::unique_ptr ExplicitParetoCurveCheckResult::clone() const {