diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp index f091b364b..ad2bd7152 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp @@ -4,8 +4,8 @@ #include "src/models/sparse/StandardRewardModel.h" #include "src/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" -#include "src/storage/BitVector.h" #include "src/transformer/StateDuplicator.h" +#include "src/transformer/SubsystemBuilder.h" #include "src/utility/macros.h" #include "src/utility/vector.h" #include "src/utility/graph.h" @@ -18,10 +18,11 @@ namespace storm { namespace helper { template - typename SparseMultiObjectivePreprocessor::PreprocessorData SparseMultiObjectivePreprocessor::preprocess(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel) { - PreprocessorData data(std::move(originalModel)); - //Initialize the state mapping. - data.newToOldStateIndexMapping = storm::utility::vector::buildVectorForRange(0, data.preprocessedModel.getNumberOfStates()); + typename SparseMultiObjectivePreprocessor::PreprocessorData SparseMultiObjectivePreprocessor::preprocess(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel, storm::storage::BitVector const& subsystem) { + + auto subsystemBuilderResult = storm::transformer::SubsystemBuilder::transform(originalModel, subsystem); + PreprocessorData data(originalModel, std::move(*subsystemBuilderResult.model), std::move(subsystemBuilderResult.newToOldStateIndexMapping)); + //Invoke preprocessing on the individual objectives for(auto const& subFormula : originalFormula.getSubFormulas()){ STORM_LOG_DEBUG("Preprocessing objective " << *subFormula<< "."); diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h index 10ce6f9bb..a3e91824f 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h @@ -3,6 +3,7 @@ #include "src/logic/Formulas.h" #include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h" +#include "src/storage/BitVector.h" namespace storm { namespace modelchecker { @@ -25,8 +26,10 @@ namespace storm { * Preprocesses the given model w.r.t. the given formulas. * @param originalModel The considered model * @param originalFormula the considered formula. The subformulas should only contain one OperatorFormula at top level, i.e., the formula is simple. + * @param subsystem the states of the original model which should be considered. Choices that have a transition leading outside of the subsystem will be + * removed. Hence, every state in the subsystem has to have one choice that stays inside the subsystem. */ - static PreprocessorData preprocess(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel); + static PreprocessorData preprocess(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel, storm::storage::BitVector const& subsystem); private: diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h index ae2015b48..31b5f22c6 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h @@ -17,8 +17,8 @@ namespace storm { enum class QueryType { Achievability, Numerical, Pareto }; - SparseModelType preprocessedModel; SparseModelType const& originalModel; + SparseModelType preprocessedModel; std::vector newToOldStateIndexMapping; QueryType queryType; @@ -27,7 +27,7 @@ namespace storm { bool produceSchedulers; - SparseMultiObjectivePreprocessorData(SparseModelType const& model) : preprocessedModel(model), originalModel(model), produceSchedulers(false) { + SparseMultiObjectivePreprocessorData(SparseModelType const& originalModel, SparseModelType&& preprocessedModel, std::vector&& newToOldStateIndexMapping) : originalModel(originalModel), preprocessedModel(preprocessedModel), newToOldStateIndexMapping(newToOldStateIndexMapping), produceSchedulers(false) { //Intentionally left empty } diff --git a/src/transformer/StateDuplicator.h b/src/transformer/StateDuplicator.h index 6733fd424..094e3e5ec 100644 --- a/src/transformer/StateDuplicator.h +++ b/src/transformer/StateDuplicator.h @@ -235,7 +235,7 @@ namespace storm { std::is_same>::value, MT>::type createTransformedModel(MT const& originalModel, - StateDuplicatorReturnType& result, + StateDuplicatorReturnType const& result, storm::storage::SparseMatrix& matrix, storm::models::sparse::StateLabeling& stateLabeling, std::unordered_map>::value, MT>::type createTransformedModel(MT const& originalModel, - StateDuplicatorReturnType& result, + StateDuplicatorReturnType const& result, storm::storage::SparseMatrix& matrix, storm::models::sparse::StateLabeling& stateLabeling, std::unordered_map +#include + +#include "src/models/sparse/StandardRewardModel.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/InvalidStateException.h" + +namespace storm { + namespace transformer { + + /* + * Removes all states that are not part of the subsystem + */ + template + class SubsystemBuilder { + public: + + struct SubsystemBuilderReturnType { + // The resulting model + std::shared_ptr model; + // Gives for each state in the resulting model the corresponding state in the original model and vice versa. + // If a state does not exist in the other model, an invalid index is given. + std::vector newToOldStateIndexMapping; + std::vector oldToNewStateIndexMapping; + // marks the actions of the original model that are still available in the subsystem + storm::storage::BitVector subsystemActions; + }; + + /* + * Removes all states that are not part of the subsystem + * all actions (i.e. rows) that lead outside of the subsystem are erased. Note that this might introduce deadlock states. + * + * @param originalModel The model to be duplicated + * @param subsystem The states that will be kept + */ + static SubsystemBuilderReturnType transform(SparseModelType const& originalModel, storm::storage::BitVector const& subsystem) { + STORM_LOG_DEBUG("Invoked subsystem builder on model with " << originalModel.getNumberOfStates() << " states."); + SubsystemBuilderReturnType result; + + uint_fast64_t subsystemStateCount = subsystem.getNumberOfSetBits(); + STORM_LOG_THROW(subsystemStateCount != 0, storm::exceptions::InvalidArgumentException, "Invoked SubsystemBuilder for an empty subsystem."); + if(subsystemStateCount == subsystem.size()) { + result.model = std::make_shared(originalModel); + result.newToOldStateIndexMapping = storm::utility::vector::buildVectorForRange(0, result.model->getNumberOfStates()); + result.oldToNewStateIndexMapping = result.newToOldStateIndexMapping; + result.subsystemActions = storm::storage::BitVector(result.model->getTransitionMatrix().getRowCount(), true); + return result; + } + + result.newToOldStateIndexMapping.reserve(subsystemStateCount); + result.oldToNewStateIndexMapping = std::vector(subsystem.size(), std::numeric_limits::max()); + result.subsystemActions = storm::storage::BitVector(result.model->getTransitionMatrix().getRowCount(), false); + for(auto subsysState : subsystem) { + result.oldToNewStateIndexMapping[subsysState] = result.newToOldStateIndexMapping.size(); + result.newToOldStateIndexMapping.push_back(subsysState); + for(uint_fast64_t row = originalModel.getTransitionMatrix().getRowGroupIndices()[subsysState]; row < originalModel.getTransitionMatrix().getRowGroupIndices()[subsysState+1]; ++row) { + result.subsystemActions.set(row, true); + for(auto const& entry : originalModel.getTransitionMatrix().getRow(row)) { + if(!subsystem.get(entry.getColumn())) { + result.subsystemActions.set(row, false); + break; + } + } + } + } + + // Transform the ingedients of the model + storm::storage::SparseMatrix matrix = transformMatrix(originalModel.getTransitionMatrix(), result); + storm::models::sparse::StateLabeling labeling(matrix.getRowGroupCount()); + for(auto const& label : originalModel.getStateLabeling().getLabels()){ + storm::storage::BitVector newBitVectorForLabel = transformStateBitVector(originalModel.getStateLabeling().getStates(label), subsystem); + labeling.addLabel(label, std::move(newBitVectorForLabel)); + } + std::unordered_map rewardModels; + for(auto const& rewardModel : originalModel.getRewardModels()){ + rewardModels.insert(std::make_pair(rewardModel.first, transformRewardModel(rewardModel.second, originalModel.getTransitionMatrix().getRowGroupIndices(), subsystem, result))); + } + boost::optional> choiceLabeling; + if(originalModel.hasChoiceLabeling()){ + choiceLabeling = transformActionValueVector(originalModel.getChoiceLabeling(), result.subsystemActions); + } + result.model = std::make_shared(createTransformedModel(originalModel, subsystem, result, matrix, labeling, rewardModels, choiceLabeling)); + STORM_LOG_DEBUG("Subsystem Builder is done. Resulting model has " << result.model->getNumberOfStates() << " states."); + return result; + } + + private: + template + static typename std::enable_if>::value, RewardModelType>::type + transformRewardModel(RewardModelType const& originalRewardModel, std::vector const& originalRowGroupIndices, storm::storage::BitVector const& subsystem, SubsystemBuilderReturnType const& result) { + boost::optional> stateRewardVector; + boost::optional> stateActionRewardVector; + boost::optional> transitionRewardMatrix; + if(originalRewardModel.hasStateRewards()){ + stateRewardVector = transformStateValueVector(originalRewardModel.getStateRewardVector(), subsystem); + } + if(originalRewardModel.hasStateActionRewards()){ + stateActionRewardVector = transformActionValueVector(originalRewardModel.getStateActionRewardVector(), result.subsystemActions); + } + if(originalRewardModel.hasTransitionRewards()){ + transitionRewardMatrix = transformMatrix(originalRewardModel.getTransitionRewardMatrix(), result); + } + return RewardModelType(std::move(stateRewardVector), std::move(stateActionRewardVector), std::move(transitionRewardMatrix)); + } + + template + static storm::storage::SparseMatrix transformMatrix(storm::storage::SparseMatrix const& originalMatrix, SubsystemBuilderReturnType const& result) { + // Build the builder + uint_fast64_t const numStates = result.newToOldStateIndexMapping.size(); + uint_fast64_t const numRows = result.subsystemActions.getNumberOfSetBits(); + uint_fast64_t numEntries = 0; + for(auto row : result.subsystemActions) { + numEntries += originalMatrix.getRow(row).getNumberOfEntries(); + } + storm::storage::SparseMatrixBuilder builder(numRows, numStates, numEntries, true, !originalMatrix.hasTrivialRowGrouping(), originalMatrix.hasTrivialRowGrouping() ? 0 : numStates); + + // Fill in the data + uint_fast64_t newRow = 0; + for(uint_fast64_t newState = 0; newState < numStates; ++newState){ + if(!originalMatrix.hasTrivialRowGrouping()){ + builder.newRowGroup(newRow); + } + uint_fast64_t oldState = result.newToOldStateIndexMapping[newState]; + for (uint_fast64_t oldRow = result.subsystemActions.getNextSetIndex(originalMatrix.getRowGroupIndices()[oldState]); oldRow < originalMatrix.getRowGroupIndices()[oldState+1]; oldRow = result.subsystemActions.getNextSetIndex(oldRow+1)){ + for(auto const& entry : originalMatrix.getRow(oldRow)){ + builder.addNextValue(newRow, result.oldToNewStateIndexMapping[entry.getColumn()], entry.getValue()); + } + ++newRow; + } + } + return builder.build(); + } + + + template + static std::vector transformActionValueVector(std::vector const& originalVector, storm::storage::BitVector const& subsystemActions) { + std::vector v; + v.reserve(subsystemActions.getNumberOfSetBits()); + for(auto action : subsystemActions){ + v.push_back(originalVector[action]); + } + return v; + } + + template + static std::vector transformStateValueVector(std::vector const& originalVector, storm::storage::BitVector const& subsystem) { + std::vector v; + v.reserve(subsystem.getNumberOfSetBits()); + for(auto state : subsystem){ + v.push_back(originalVector[state]); + } + return v; + } + + static storm::storage::BitVector transformStateBitVector(storm::storage::BitVector const& originalBitVector, storm::storage::BitVector const& subsystem) { + return originalBitVector % subsystem; + } + + + template + static typename std::enable_if< + std::is_same>::value || + std::is_same>::value || + std::is_same>::value, + MT>::type + createTransformedModel(MT const& originalModel, + storm::storage::BitVector const& subsystem, + SubsystemBuilderReturnType const& result, + storm::storage::SparseMatrix& matrix, + storm::models::sparse::StateLabeling& stateLabeling, + std::unordered_map& rewardModels, + boost::optional>& choiceLabeling ) { + return MT(std::move(matrix), std::move(stateLabeling), std::move(rewardModels), std::move(choiceLabeling)); + } + + template + static typename std::enable_if< + std::is_same>::value, + MT>::type + createTransformedModel(MT const& originalModel, + storm::storage::BitVector const& subsystem, + SubsystemBuilderReturnType const& result, + storm::storage::SparseMatrix& matrix, + storm::models::sparse::StateLabeling& stateLabeling, + std::unordered_map& rewardModels, + boost::optional>& choiceLabeling ) { + storm::storage::BitVector markovianStates = transformStateBitVector(originalModel.getMarkovianStates(), subsystem); + std::vector exitRates = transformStateValueVector(originalModel.getExitRates(), subsystem); + return MT(std::move(matrix), std::move(stateLabeling), std::move(markovianStates), std::move(exitRates), true, std::move(rewardModels), std::move(choiceLabeling)); + } + + + }; + } +} +#endif // STORM_TRANSFORMER_SUBSYSTEMBUILDER_H