From 789367a28b8fe19eafd65af99ddfa6f5ce234397 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 27 Jun 2018 09:45:03 +0200 Subject: [PATCH] using new memory incorporation in multi objective model checking --- .../multiObjectiveModelChecking.cpp | 2 +- .../SparseMultiObjectivePreprocessor.cpp | 24 ++++++++++++++++--- .../SparseMultiObjectivePreprocessor.h | 4 +++- .../SparseMultiObjectiveRewardAnalysis.cpp | 1 - 4 files changed, 25 insertions(+), 6 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp b/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp index de3c4ff94..0c15d9a81 100644 --- a/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp +++ b/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp @@ -35,7 +35,7 @@ namespace storm { } // Preprocess the model - auto preprocessorResult = preprocessing::SparseMultiObjectivePreprocessor::preprocess(model, formula); + auto preprocessorResult = preprocessing::SparseMultiObjectivePreprocessor::preprocess(env, model, formula); swPreprocessing.stop(); if (storm::settings::getModule().isShowStatisticsSet()) { STORM_PRINT_AND_LOG("Preprocessing done in " << swPreprocessing << " seconds." << std::endl << " Result: " << preprocessorResult << std::endl); diff --git a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp index 23ecdac36..3251a6a29 100644 --- a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp @@ -3,10 +3,11 @@ #include #include +#include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" -#include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveMemoryIncorporation.h" +#include "storm/transformer/MemoryIncorporation.h" #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" @@ -30,9 +31,26 @@ namespace storm { namespace preprocessing { template - typename SparseMultiObjectivePreprocessor::ReturnType SparseMultiObjectivePreprocessor::preprocess(SparseModelType const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula) { + typename SparseMultiObjectivePreprocessor::ReturnType SparseMultiObjectivePreprocessor::preprocess(Environment const& env, SparseModelType const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula) { + + std::shared_ptr model; + + // 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()); + } else if (schedRestr.getMemoryPattern() == storm::storage::SchedulerClass::MemoryPattern::Arbitrary && schedRestr.getMemoryStates() > 1) { + model = storm::transformer::MemoryIncorporation::incorporateFullMemory(originalModel, schedRestr.getMemoryStates()); + } else if (schedRestr.isPositional()) { + model = std::make_shared(originalModel); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The given scheduler restriction has not been implemented."); + } + } else { + model = storm::transformer::MemoryIncorporation::incorporateGoalMemory(originalModel, originalFormula.getSubformulas()); + } - auto model = SparseMultiObjectiveMemoryIncorporation::incorporateGoalMemory(originalModel, originalFormula); PreprocessorData data(model); //Invoke preprocessing on the individual objectives diff --git a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.h b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.h index ef77c2a94..ad41f932c 100644 --- a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.h +++ b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.h @@ -10,6 +10,8 @@ namespace storm { + class Environment; + namespace modelchecker { namespace multiobjective { namespace preprocessing { @@ -29,7 +31,7 @@ namespace storm { * @param originalModel The considered model * @param originalFormula the considered formula. The subformulas should only contain one OperatorFormula at top level. */ - static ReturnType preprocess(SparseModelType const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula); + static ReturnType preprocess(Environment const& env, SparseModelType const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula); private: diff --git a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveRewardAnalysis.cpp b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveRewardAnalysis.cpp index 8f24c7c4a..6277162fd 100644 --- a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveRewardAnalysis.cpp +++ b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveRewardAnalysis.cpp @@ -7,7 +7,6 @@ #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" -#include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveMemoryIncorporation.h" #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"