diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 5fcf85253..48eca36b2 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -32,7 +32,7 @@ file(GLOB_RECURSE STORM_PERMISSIVESCHEDULER_FILES ${PROJECT_SOURCE_DIR}/src/perm file(GLOB STORM_MODELS_FILES ${PROJECT_SOURCE_DIR}/src/models/*.h ${PROJECT_SOURCE_DIR}/src/models/*.cpp) file(GLOB_RECURSE STORM_MODELS_SPARSE_FILES ${PROJECT_SOURCE_DIR}/src/models/sparse/*.h ${PROJECT_SOURCE_DIR}/src/models/sparse/*.cpp) file(GLOB_RECURSE STORM_MODELS_SYMBOLIC_FILES ${PROJECT_SOURCE_DIR}/src/models/symbolic/*.h ${PROJECT_SOURCE_DIR}/src/models/symbolic/*.cpp) -file(GLOB_RECURSE STORM_MODELTRANSFORMER_FILES ${PROJECT_SOURCE_DIR}/src/modeltransformer/*.h ${PROJECT_SOURCE_DIR}/src/modeltransformer/*.cpp) +file(GLOB_RECURSE STORM_TRANSFORMER_FILES ${PROJECT_SOURCE_DIR}/src/transformer/*.h ${PROJECT_SOURCE_DIR}/src/transformer/*.cpp) file(GLOB STORM_PARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/*.h ${PROJECT_SOURCE_DIR}/src/parser/*.cpp) file(GLOB_RECURSE STORM_PARSER_PRISMPARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/prismparser/*.h ${PROJECT_SOURCE_DIR}/src/parser/prismparser/*.cpp) file(GLOB STORM_SETTINGS_FILES ${PROJECT_SOURCE_DIR}/src/settings/*.h ${PROJECT_SOURCE_DIR}/src/settings/*.cpp) @@ -89,7 +89,7 @@ source_group(permissiveschedulers FILES ${STORM_PERMISSIVESCHEDULER_FILES}) source_group(models FILES ${STORM_MODELS_FILES}) source_group(models\\sparse FILES ${STORM_MODELS_SPARSE_FILES}) source_group(models\\symbolic FILES ${STORM_MODELS_SYMBOLIC_FILES}) -source_group(modeltransformer FILES ${STORM_MODELTRANSFORMER_FILES}) +source_group(transformer FILES ${STORM_TRANSFORMER_FILES}) source_group(parser FILES ${STORM_PARSER_FILES}) source_group(parser\\prismparser FILES ${STORM_PARSER_PRISMPARSER_FILES}) source_group(settings FILES ${STORM_SETTINGS_FILES}) diff --git a/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.cpp b/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.cpp index 4366fc1a8..32701b032 100644 --- a/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.cpp @@ -6,6 +6,8 @@ #include "src/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "src/transformer/StateDuplicator.h" + #include "src/storage/BitVector.h" #include "src/utility/macros.h" @@ -24,10 +26,7 @@ namespace storm { Information info(std::move(originalModel)); //Initialize the state mapping. - info.getNewToOldStateMapping().reserve(info.getModel().getNumberOfStates()); - for(uint_fast64_t state = 0; state < info.getModel().getNumberOfStates(); ++state){ - info.getNewToOldStateMapping().push_back(state); - } + info.setNewToOldStateIndexMapping(storm::utility::vector::buildVectorForRange(0, info.getModel().getNumberOfStates())); //Gather information regarding the individual objectives if(!gatherObjectiveInformation(originalFormula, info)){ @@ -201,13 +200,27 @@ namespace storm { storm::storage::BitVector phiStates = mc.check(phiTask)->asExplicitQualitativeCheckResult().getTruthValuesVector(); storm::storage::BitVector psiStates = mc.check(psiTask)->asExplicitQualitativeCheckResult().getTruthValuesVector(); - // modelUnfolder(info.model, (~phiStates) | psiStates) - // info.model = modelUnfolder.info() - // build info.stateMapping from modelUnfolder.stateMapping - // build stateaction reward vector - // insert it in the model information - - // TODO + auto duplicatorResult = storm::transformer::StateDuplicator::transform(info.getModel(), ~phiStates | psiStates); + // duplicatorResult.newToOldStateIndexMapping now reffers to the indices of the model we had before preprocessing this formula. + // This might not be the actual original model. + for(auto & originalModelStateIndex : duplicatorResult.newToOldStateIndexMapping){ + originalModelStateIndex = info.getNewToOldStateIndexMapping()[originalModelStateIndex]; + } + info.setNewToOldStateIndexMapping(duplicatorResult.newToOldStateIndexMapping); + + // build stateAction reward vector that gives (one*transitionProbability) reward whenever a transition leads from the firstCopy to a psiState + storm::storage::BitVector newPsiStates(duplicatorResult.model->getNumberOfStates(), false); + for(auto const& oldPsiState : psiStates){ + //note that psiStates are always located in the second copy + newPsiStates.set(duplicatorResult.secondCopyOldToNewStateIndexMapping[oldPsiState], true); + } + std::vector objectiveRewards = duplicatorResult.model->getTransitionMatrix().getConstrainedRowGroupSumVector(duplicatorResult.firstCopy, newPsiStates); + if(info.areNegativeRewardsConsidered()){ + storm::utility::vector::scaleVectorInPlace(objectiveRewards, -storm::utility::one()); + } + + duplicatorResult.model->getRewardModels().insert(std::make_pair(currentObjective.rewardModelName, RewardModelType(boost::none, objectiveRewards))); + info.setModel(std::move(*duplicatorResult.model)); return success; } diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerInformation.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerInformation.h index 41e1840c4..bc6be45b1 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerInformation.h +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerInformation.h @@ -36,18 +36,28 @@ namespace storm { //Intentionally left empty } - SparseModelType& getModel(){ - return model; + void setModel(SparseModelType&& newModel){ + model = newModel; + } + + void setModel(SparseModelType const& newModel){ + model = newModel; } + SparseModelType const& getModel() const { return model; } - std::vector& getNewToOldStateMapping(){ - return newToOldStateMapping; + void setNewToOldStateIndexMapping(std::vector const& newMapping){ + newToOldStateIndexMapping = newMapping; } - std::vectorconst& getNewToOldStateMapping() const{ - return newToOldStateMapping; + + void setNewToOldStateIndexMapping(std::vector&& newMapping){ + newToOldStateIndexMapping = newMapping; + } + + std::vectorconst& getNewToOldStateIndexMapping() const{ + return newToOldStateIndexMapping; } bool areNegativeRewardsConsidered() { @@ -68,7 +78,7 @@ namespace storm { private: SparseModelType model; - std::vector newToOldStateMapping; + std::vector newToOldStateIndexMapping; bool negativeRewardsConsidered; std::vector objectives; diff --git a/src/modeltransformers/StateDuplicator.h b/src/transformer/StateDuplicator.h similarity index 53% rename from src/modeltransformers/StateDuplicator.h rename to src/transformer/StateDuplicator.h index f96e0f9c6..708663270 100644 --- a/src/modeltransformers/StateDuplicator.h +++ b/src/transformer/StateDuplicator.h @@ -1,36 +1,20 @@ -#ifndef STORM_MDPTRIVIALSTATEELIMINATOR_H -#define STORM_MDPTRIVIALSTATEELIMINATOR_H +#ifndef STORM_TRANSFORMER_STATEDUPLICATOR_H +#define STORM_TRANSFORMER_STATEDUPLICATOR_H -#include "../utility/macros.h" -#include #include #include -#include "src/adapters/CarlAdapter.h" -#include "src/logic/Formulas.h" -#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" -#include "src/modelchecker/region/RegionCheckResult.h" -#include "src/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "src/models/sparse/StandardRewardModel.h" -#include "src/settings/SettingsManager.h" -#include "src/settings/modules/RegionSettings.h" -#include "src/solver/OptimizationDirection.h" -#include "src/storage/sparse/StateType.h" -#include "src/storage/FlexibleSparseMatrix.h" #include "src/utility/constants.h" #include "src/utility/graph.h" #include "src/utility/macros.h" #include "src/utility/vector.h" +#include "src/models/sparse/Dtmc.h" +#include "src/models/sparse/Mdp.h" +#include "src/models/sparse/Ctmc.h" +#include "src/models/sparse/MarkovAutomaton.h" -#include "src/exceptions/InvalidArgumentException.h" -#include "src/exceptions/InvalidPropertyException.h" -#include "src/exceptions/InvalidStateException.h" -#include "src/exceptions/InvalidSettingsException.h" -#include "src/exceptions/NotImplementedException.h" -#include "src/exceptions/UnexpectedException.h" -#include "src/exceptions/NotSupportedException.h" -#include "src/logic/FragmentSpecification.h" namespace storm { namespace transformer { @@ -39,14 +23,12 @@ namespace storm { * Duplicates the state space of the given model and redirects the incoming transitions of gateStates of the first copy to the gateStates of the second copy. * Only states reachable from the initial states are kept. */ -