diff --git a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveMemoryIncorporation.cpp b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveMemoryIncorporation.cpp deleted file mode 100644 index 36ccda05f..000000000 --- a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveMemoryIncorporation.cpp +++ /dev/null @@ -1,103 +0,0 @@ -#include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveMemoryIncorporation.h" - -#include "storm/models/sparse/Mdp.h" -#include "storm/models/sparse/MarkovAutomaton.h" -#include "storm/models/sparse/StandardRewardModel.h" -#include "storm/storage/memorystructure/MemoryStructureBuilder.h" -#include "storm/storage/memorystructure/SparseModelMemoryProduct.h" -#include "storm/logic/Formulas.h" -#include "storm/logic/FragmentSpecification.h" -#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" -#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" - -#include "storm/utility/macros.h" - -#include "storm/exceptions/NotImplementedException.h" -#include "storm/exceptions/NotSupportedException.h" -namespace storm { - namespace modelchecker { - namespace multiobjective { - namespace preprocessing { - - template - storm::storage::MemoryStructure getGoalMemory(SparseModelType const& model, storm::logic::Formula const& propositionalGoalStateFormula) { - STORM_LOG_THROW(propositionalGoalStateFormula.isInFragment(storm::logic::propositional()), storm::exceptions::NotSupportedException, "The subformula " << propositionalGoalStateFormula << " should be propositional."); - - storm::modelchecker::SparsePropositionalModelChecker mc(model); - storm::storage::BitVector goalStates = mc.check(propositionalGoalStateFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); - - // Check if the formula is already satisfied for all initial states. In such a case the trivial memory structure suffices. - if (model.getInitialStates().isSubsetOf(goalStates)) { - STORM_LOG_INFO("One objective is already satisfied for all initial states."); - return storm::storage::MemoryStructureBuilder::buildTrivialMemoryStructure(model); - } - - - // Create a memory structure that stores whether a goal state has already been reached - storm::storage::MemoryStructureBuilder builder(2, model); - builder.setTransition(0, 0, ~goalStates); - builder.setTransition(0, 1, goalStates); - builder.setTransition(1, 1, storm::storage::BitVector(model.getNumberOfStates(), true)); - for (auto const& initState : model.getInitialStates()) { - builder.setInitialMemoryState(initState, goalStates.get(initState) ? 1 : 0); - } - return builder.build(); - } - - template - storm::storage::MemoryStructure getUntilFormulaMemory(SparseModelType const& model, storm::logic::Formula const& leftSubFormula, storm::logic::Formula const& rightSubFormula) { - auto notLeftOrRight = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::Or, - std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, leftSubFormula.asSharedPointer()), - rightSubFormula.asSharedPointer()); - return getGoalMemory(model, *notLeftOrRight); - - } - - template - std::shared_ptr SparseMultiObjectiveMemoryIncorporation::incorporateGoalMemory(SparseModelType const& model, storm::logic::MultiObjectiveFormula const& formula) { - storm::storage::MemoryStructure memory = storm::storage::MemoryStructureBuilder::buildTrivialMemoryStructure(model); - - for (auto const& subFormula : formula.getSubformulas()) { - STORM_LOG_THROW(subFormula->isOperatorFormula(), storm::exceptions::NotSupportedException, "The given Formula " << *subFormula << " is not supported."); - auto const& subsubFormula = subFormula->asOperatorFormula().getSubformula(); - if (subsubFormula.isEventuallyFormula()) { - memory = memory.product(getGoalMemory(model, subsubFormula.asEventuallyFormula().getSubformula())); - } else if (subsubFormula.isUntilFormula()) { - memory = memory.product(getUntilFormulaMemory(model, subsubFormula.asUntilFormula().getLeftSubformula(), subsubFormula.asUntilFormula().getRightSubformula())); - } else if (subsubFormula.isBoundedUntilFormula()) { - // For bounded formulas it is only reasonable to add the goal memory if it considers a single upper step/time bound. - auto const& buf = subsubFormula.asBoundedUntilFormula(); - if (!buf.isMultiDimensional() && !buf.getTimeBoundReference().isRewardBound() && (!buf.hasLowerBound() || (!buf.isLowerBoundStrict() && storm::utility::isZero(buf.template getLowerBound())))) { - memory = memory.product(getUntilFormulaMemory(model, buf.getLeftSubformula(), buf.getRightSubformula())); - } - } else if (subsubFormula.isGloballyFormula()) { - auto notPhi = std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, subsubFormula.asGloballyFormula().getSubformula().asSharedPointer()); - memory = memory.product(getGoalMemory(model, *notPhi)); - } else { - STORM_LOG_THROW(subFormula->isOperatorFormula(), storm::exceptions::NotSupportedException, "The given Formula " << subsubFormula << " is not supported."); - } - } - - storm::storage::SparseModelMemoryProduct product = memory.product(model); - return std::dynamic_pointer_cast(product.build()); - } - - template - std::shared_ptr SparseMultiObjectiveMemoryIncorporation::incorporateFullMemory(SparseModelType const& model, uint64_t memoryStates) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "not implemented"); - return nullptr; - } - - - template class SparseMultiObjectiveMemoryIncorporation>; - template class SparseMultiObjectiveMemoryIncorporation>; - - template class SparseMultiObjectiveMemoryIncorporation>; - template class SparseMultiObjectiveMemoryIncorporation>; - - } - } - } -} - - diff --git a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveMemoryIncorporation.h b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveMemoryIncorporation.h deleted file mode 100644 index a16ced952..000000000 --- a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveMemoryIncorporation.h +++ /dev/null @@ -1,33 +0,0 @@ -#pragma once - -#include - -#include "storm/storage/memorystructure/MemoryStructure.h" -#include "storm/logic/MultiObjectiveFormula.h" -#include "storm/logic/Formula.h" - -namespace storm { - namespace modelchecker { - namespace multiobjective { - - namespace preprocessing { - - template - class SparseMultiObjectiveMemoryIncorporation { - - typedef typename SparseModelType::ValueType ValueType; - typedef typename SparseModelType::RewardModelType RewardModelType; - - - - public: - static std::shared_ptr incorporateGoalMemory(SparseModelType const& model, storm::logic::MultiObjectiveFormula const& formula); - static std::shared_ptr incorporateFullMemory(SparseModelType const& model, uint64_t memoryStates); - - }; - } - } - } -} - - diff --git a/src/storm/storage/memorystructure/NondeterministicMemoryStructure.cpp b/src/storm/storage/memorystructure/NondeterministicMemoryStructure.cpp new file mode 100644 index 000000000..7a9ba59cc --- /dev/null +++ b/src/storm/storage/memorystructure/NondeterministicMemoryStructure.cpp @@ -0,0 +1,76 @@ +#include "storm/storage/memorystructure/NondeterministicMemoryStructure.h" +#include "storm/storage/memorystructure/NondeterministicMemoryStructureBuilder.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/InvalidArgumentException.h" + +namespace storm { + namespace storage { + + NondeterministicMemoryStructure::NondeterministicMemoryStructure(std::vector const& transitions, uint64_t initialState) : transitions(transitions), initialState(initialState) { + STORM_LOG_THROW(this->initialState < this->transitions.size(), storm::exceptions::InvalidArgumentException, "Initial state " << this->initialState << " of nondeterministic memory structure is invalid."); + for (auto const& t : this->transitions) { + STORM_LOG_THROW(t.size() == this->transitions.size(), storm::exceptions::InvalidArgumentException, "Invalid dimension of transition matrix of nondeterministic memory structure."); + STORM_LOG_THROW(!t.empty(), storm::exceptions::InvalidArgumentException, "Invalid transition matrix of nondeterministic memory structure: No deadlock states allowed."); + } + } + + uint64_t NondeterministicMemoryStructure::getNumberOfStates() const { + return transitions.size(); + } + + uint64_t NondeterministicMemoryStructure::getInitialState() const { + return initialState; + } + + storm::storage::BitVector const& NondeterministicMemoryStructure::getTransitions(uint64_t state) const { + return transitions.at(state); + } + + uint64_t NondeterministicMemoryStructure::getNumberOfOutgoingTransitions(uint64_t state) const { + return getTransitions(state).getNumberOfSetBits(); + } + + std::vector const& NondeterministicMemoryStructure::getTransitions() const { + return transitions; + } + + std::string NondeterministicMemoryStructure::toString() const { + std::string result = "NondeterministicMemoryStructure with " + std::to_string(getNumberOfStates()) + " states.\n"; + result += "Initial state is " + std::to_string(getInitialState()) + ". Transitions are \n"; + + // header + result += " |"; + for (uint64_t state = 0; state < getNumberOfStates(); ++state) { + if (state < 10) { + result += " "; + } + result += std::to_string(state); + } + result += "\n"; + result += "--|"; + for (uint64_t state = 0; state < getNumberOfStates(); ++state) { + result += "--"; + } + result += "\n"; + + // transition matrix entries + for (uint64_t state = 0; state < getNumberOfStates(); ++state) { + if (state < 10) { + result += " "; + } + result += std::to_string(state) + "|"; + for (uint64_t statePrime = 0; statePrime < getNumberOfStates(); ++statePrime) { + result += " "; + if (getTransitions(state).get(statePrime)) { + result += "1"; + } else { + result += "0"; + } + } + result += "\n"; + } + return result; + } + } +} \ No newline at end of file diff --git a/src/storm/storage/memorystructure/NondeterministicMemoryStructure.h b/src/storm/storage/memorystructure/NondeterministicMemoryStructure.h new file mode 100644 index 000000000..42465e91d --- /dev/null +++ b/src/storm/storage/memorystructure/NondeterministicMemoryStructure.h @@ -0,0 +1,25 @@ +#pragma once + +#include +#include "storm/storage/BitVector.h" + +namespace storm { + namespace storage { + + class NondeterministicMemoryStructure { + + public: + NondeterministicMemoryStructure(std::vector const& transitions, uint64_t initialState); + uint64_t getNumberOfStates() const; + uint64_t getInitialState() const; + storm::storage::BitVector const& getTransitions(uint64_t state) const; + uint64_t getNumberOfOutgoingTransitions(uint64_t state) const; + std::vector const& getTransitions() const; + std::string toString() const; + private: + std::vector transitions; + uint64_t initialState; + }; + + } +} \ No newline at end of file diff --git a/src/storm/storage/memorystructure/NondeterministicMemoryStructureBuilder.cpp b/src/storm/storage/memorystructure/NondeterministicMemoryStructureBuilder.cpp new file mode 100644 index 000000000..d29448885 --- /dev/null +++ b/src/storm/storage/memorystructure/NondeterministicMemoryStructureBuilder.cpp @@ -0,0 +1,115 @@ +#include "storm/storage/memorystructure/NondeterministicMemoryStructure.h" +#include "storm/storage/memorystructure/NondeterministicMemoryStructureBuilder.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/InvalidArgumentException.h" + +namespace storm { + namespace storage { + + std::string toString(NondeterministicMemoryStructurePattern const& pattern) { + switch (pattern) { + case NondeterministicMemoryStructurePattern::Trivial: + return "trivial"; + case NondeterministicMemoryStructurePattern::FixedCounter: + return "fixedcounter"; + case NondeterministicMemoryStructurePattern::SelectiveCounter: + return "selectivecounter"; + case NondeterministicMemoryStructurePattern::FixedRing: + return "fixedring"; + case NondeterministicMemoryStructurePattern::SelectiveRing: + return "ring"; + case NondeterministicMemoryStructurePattern::SettableBits: + return "settablebits"; + case NondeterministicMemoryStructurePattern::Full: + return "full"; + } + return "unknown"; + } + + NondeterministicMemoryStructure NondeterministicMemoryStructureBuilder::build(NondeterministicMemoryStructurePattern pattern, uint64_t numStates) const { + switch (pattern) { + case NondeterministicMemoryStructurePattern::Trivial: + STORM_LOG_ERROR_COND(numStates == 1, "Invoked building trivial nondeterministic memory structure with " << numStates << " states. However, trivial nondeterministic memory structure always has one state."); + return buildTrivialMemory(); + case NondeterministicMemoryStructurePattern::FixedCounter: + return buildFixedCountingMemory(numStates); + case NondeterministicMemoryStructurePattern::SelectiveCounter: + return buildSelectiveCountingMemory(numStates); + case NondeterministicMemoryStructurePattern::FixedRing: + return buildFixedRingMemory(numStates); + case NondeterministicMemoryStructurePattern::SelectiveRing: + return buildSelectiveRingMemory(numStates); + case NondeterministicMemoryStructurePattern::SettableBits: + return buildSettableBitsMemory(numStates); + case NondeterministicMemoryStructurePattern::Full: + return buildFullyConnectedMemory(numStates); + } + } + + NondeterministicMemoryStructure NondeterministicMemoryStructureBuilder::buildTrivialMemory() const { + return buildFullyConnectedMemory(1); + } + + NondeterministicMemoryStructure NondeterministicMemoryStructureBuilder::buildFixedCountingMemory(uint64_t numStates) const { + std::vector transitions(numStates, storm::storage::BitVector(numStates, false)); + for (uint64_t state = 0; state < numStates; ++state) { + transitions[state].set(std::min(state + 1, numStates - 1)); + } + return NondeterministicMemoryStructure(transitions, 0); + } + + NondeterministicMemoryStructure NondeterministicMemoryStructureBuilder::buildSelectiveCountingMemory(uint64_t numStates) const { + std::vector transitions(numStates, storm::storage::BitVector(numStates, false)); + for (uint64_t state = 0; state < numStates; ++state) { + transitions[state].set(state); + transitions[state].set(std::min(state + 1, numStates - 1)); + } + return NondeterministicMemoryStructure(transitions, 0); + } + + NondeterministicMemoryStructure NondeterministicMemoryStructureBuilder::buildFixedRingMemory(uint64_t numStates) const { + std::vector transitions(numStates, storm::storage::BitVector(numStates, false)); + for (uint64_t state = 0; state < numStates; ++state) { + transitions[state].set((state + 1) % numStates); + } + return NondeterministicMemoryStructure(transitions, 0); + } + + NondeterministicMemoryStructure NondeterministicMemoryStructureBuilder::buildSelectiveRingMemory(uint64_t numStates) const { + std::vector transitions(numStates, storm::storage::BitVector(numStates, false)); + for (uint64_t state = 0; state < numStates; ++state) { + transitions[state].set(state); + transitions[state].set((state + 1) % numStates); + } + return NondeterministicMemoryStructure(transitions, 0); + } + + NondeterministicMemoryStructure NondeterministicMemoryStructureBuilder::buildSettableBitsMemory(uint64_t numStates) const { + // compute the number of bits, i.e., floor(log(numStates)) + uint64_t numBits = 0; + uint64_t actualNumStates = 1; + while (actualNumStates * 2 <= numStates) { + actualNumStates *= 2; + ++numBits; + } + + STORM_LOG_WARN_COND(actualNumStates == numStates, "The number of memory states for the settable bits pattern has to be a power of 2. Shrinking the number of memory states to " << actualNumStates << "."); + + std::vector transitions(actualNumStates, storm::storage::BitVector(actualNumStates, false)); + for (uint64_t state = 0; state < actualNumStates; ++state) { + transitions[state].set(state); + for (uint64_t bit = 0; bit < numBits; ++bit) { + uint64_t bitMask = 1u << bit; + transitions[state].set(state | bitMask); + } + } + return NondeterministicMemoryStructure(transitions, 0); + } + + NondeterministicMemoryStructure NondeterministicMemoryStructureBuilder::buildFullyConnectedMemory(uint64_t numStates) const { + std::vector transitions(numStates, storm::storage::BitVector(numStates, true)); + return NondeterministicMemoryStructure(transitions, 0); + } + } +} \ No newline at end of file diff --git a/src/storm/storage/memorystructure/NondeterministicMemoryStructureBuilder.h b/src/storm/storage/memorystructure/NondeterministicMemoryStructureBuilder.h new file mode 100644 index 000000000..25d5503db --- /dev/null +++ b/src/storm/storage/memorystructure/NondeterministicMemoryStructureBuilder.h @@ -0,0 +1,47 @@ +#pragma once + +#include "storm/storage/memorystructure/NondeterministicMemoryStructure.h" + +namespace storm { + namespace storage { + + enum class NondeterministicMemoryStructurePattern { + Trivial, FixedCounter, SelectiveCounter, FixedRing, SelectiveRing, SettableBits, Full + }; + + std::string toString(NondeterministicMemoryStructurePattern const& pattern); + + class NondeterministicMemoryStructureBuilder { + public: + // Builds a memory structure with the given pattern and the given number of states. + NondeterministicMemoryStructure build(NondeterministicMemoryStructurePattern pattern, uint64_t numStates) const; + + // Builds a memory structure that consists of just a single memory state + NondeterministicMemoryStructure buildTrivialMemory() const; + + // Builds a memory structure that consists of a chain of the given number of states. + // Every state has exactly one transition to the next state. The last state has just a selfloop. + NondeterministicMemoryStructure buildFixedCountingMemory(uint64_t numStates) const; + + // Builds a memory structure that consists of a chain of the given number of states. + // Every state has a selfloop and a transition to the next state. The last state just has a selfloop. + NondeterministicMemoryStructure buildSelectiveCountingMemory(uint64_t numStates) const; + + // Builds a memory structure that consists of a ring of the given number of states. + // Every state has a transition to the successor state + NondeterministicMemoryStructure buildFixedRingMemory(uint64_t numStates) const; + + // Builds a memory structure that consists of a ring of the given number of states. + // Every state has a transition to the successor state and a selfloop + NondeterministicMemoryStructure buildSelectiveRingMemory(uint64_t numStates) const; + + // Builds a memory structure that represents floor(log(numStates)) bits that can only be set from zero to one or from zero to zero. + NondeterministicMemoryStructure buildSettableBitsMemory(uint64_t numStates) const; + + // Builds a memory structure that consists of the given number of states which are fully connected. + NondeterministicMemoryStructure buildFullyConnectedMemory(uint64_t numStates) const; + + }; + + } +} \ No newline at end of file diff --git a/src/storm/storage/memorystructure/SparseModelNondeterministicMemoryProduct.cpp b/src/storm/storage/memorystructure/SparseModelNondeterministicMemoryProduct.cpp new file mode 100644 index 000000000..4748a03e8 --- /dev/null +++ b/src/storm/storage/memorystructure/SparseModelNondeterministicMemoryProduct.cpp @@ -0,0 +1,187 @@ +#include "storm/storage/memorystructure/SparseModelNondeterministicMemoryProduct.h" + +#include +#include "storm/storage/sparse/ModelComponents.h" +#include "storm/utility/graph.h" +#include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/models/sparse/StandardRewardModel.h" + +#include "storm/exceptions/NotSupportedException.h" + +namespace storm { + namespace storage { + + template + SparseModelNondeterministicMemoryProduct::SparseModelNondeterministicMemoryProduct(SparseModelType const& model, storm::storage::NondeterministicMemoryStructure const& memory) : model(model), memory(memory) { + // intentionally left empty + } + + template + std::shared_ptr SparseModelNondeterministicMemoryProduct::build() const { + // For simplicity we first build the 'full' product of model and memory (with model.numStates * memory.numStates states). + storm::storage::sparse::ModelComponents components; + components.transitionMatrix = buildTransitions(); + components.stateLabeling = buildStateLabeling(); + + // Now delete unreachable states. + storm::storage::BitVector allStates(components.transitionMatrix.getRowGroupCount(), true); + auto reachableStates = storm::utility::graph::getReachableStates(components.transitionMatrix, components.stateLabeling.getStates("init"), allStates, ~allStates); + components.transitionMatrix = components.transitionMatrix.getSubmatrix(true, reachableStates, reachableStates); + components.stateLabeling = components.stateLabeling.getSubLabeling(reachableStates); + + // build the remaining components + for (auto const& rewModel : model.getRewardModels()) { + components.rewardModels.emplace(rewModel.first, buildRewardModel(rewModel.second, reachableStates)); + } + if (model.isOfType(storm::models::ModelType::MarkovAutomaton)) { + STORM_LOG_ASSERT((std::is_same>::value), "Model has unexpected type."); + auto ma = model.template as>(); + components.exitRates = buildExitRateVector(*ma, reachableStates); + components.markovianStates = buildMarkovianStateLabeling(*ma, reachableStates); + } + return std::make_shared(std::move(components)); + } + + template + storm::storage::SparseMatrix::ValueType> SparseModelNondeterministicMemoryProduct::buildTransitions() const { + storm::storage::SparseMatrix const& origTransitions = model.getTransitionMatrix(); + uint64_t numRows = 0; + uint64_t numEntries = 0; + for (uint64_t modelState = 0; modelState < model.getNumberOfStates(); ++modelState) { + for (uint64_t memState = 0; memState < memory.getNumberOfStates(); ++memState) { + numRows += origTransitions.getRowGroupSize(modelState) * memory.getNumberOfOutgoingTransitions(memState); + numEntries += origTransitions.getRowGroup(modelState).getNumberOfEntries() * memory.getNumberOfOutgoingTransitions(memState); + } + } + storm::storage::SparseMatrixBuilder builder(numRows, + model.getNumberOfStates() * memory.getNumberOfStates(), + numEntries, + true, + true, + model.getNumberOfStates() * memory.getNumberOfStates()); + + uint64_t row = 0; + for (uint64_t modelState = 0; modelState < model.getNumberOfStates(); ++modelState) { + for (uint64_t memState = 0; memState < memory.getNumberOfStates(); ++memState) { + builder.newRowGroup(row); + for (uint64_t origRow = origTransitions.getRowGroupIndices()[modelState]; origRow < origTransitions.getRowGroupIndices()[modelState + 1]; ++origRow) { + for (auto const& memStatePrime : memory.getTransitions(memState)) { + for (auto const& entry : origTransitions.getRow(origRow)) { + builder.addNextValue(row, getProductState(entry.getColumn(), memStatePrime), entry.getValue()); + } + ++row; + } + } + } + } + return builder.build(); + } + + template + storm::models::sparse::StateLabeling SparseModelNondeterministicMemoryProduct::buildStateLabeling() const { + storm::models::sparse::StateLabeling labeling(model.getNumberOfStates() * memory.getNumberOfStates()); + for (auto const& labelName : model.getStateLabeling().getLabels()) { + storm::storage::BitVector newStates(model.getNumberOfStates() * memory.getNumberOfStates(), false); + + // The init label is only assigned to Product states with the initial memory state + if (labelName == "init") { + for (auto const& modelState : model.getStateLabeling().getStates(labelName)) { + newStates.set(getProductState(modelState, memory.getInitialState())); + } + } else { + for (auto const& modelState : model.getStateLabeling().getStates(labelName)) { + for (uint64_t memState = 0; memState < memory.getNumberOfStates(); ++memState) { + newStates.set(getProductState(modelState, memState)); + } + } + } + labeling.addLabel(labelName, std::move(newStates)); + } + return labeling; + } + + template + storm::models::sparse::StandardRewardModel::ValueType> SparseModelNondeterministicMemoryProduct::buildRewardModel(storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& reachableStates) const { + boost::optional> stateRewards, actionRewards; + if (rewardModel.hasStateRewards()) { + stateRewards = std::vector(); + stateRewards->reserve(model.getNumberOfStates() * memory.getNumberOfStates()); + for (uint64_t modelState = 0; modelState < model.getNumberOfStates(); ++modelState) { + for (uint64_t memState = 0; memState < memory.getNumberOfStates(); ++memState) { + if (reachableStates.get(getProductState(modelState, memState))) { + stateRewards->push_back(rewardModel.getStateReward(modelState)); + } + } + } + } + if (rewardModel.hasStateActionRewards()) { + actionRewards = std::vector(); + for (uint64_t modelState = 0; modelState < model.getNumberOfStates(); ++modelState) { + for (uint64_t memState = 0; memState < memory.getNumberOfStates(); ++memState) { + if (reachableStates.get(getProductState(modelState, memState))) { + for (uint64_t origRow = model.getTransitionMatrix().getRowGroupIndices()[modelState]; origRow < model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]; ++origRow) { + ValueType const& actionReward = rewardModel.getStateActionReward(origRow); + actionRewards->insert(actionRewards->end(), memory.getNumberOfOutgoingTransitions(memState), actionReward); + } + } + } + } + } + STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Transition rewards are currently not supported."); + return storm::models::sparse::StandardRewardModel(std::move(stateRewards), std::move(actionRewards)); + } + + template + std::vector::ValueType> SparseModelNondeterministicMemoryProduct::buildExitRateVector(storm::models::sparse::MarkovAutomaton const& modelAsMA, storm::storage::BitVector const& reachableStates) const { + std::vector res; + res.reserve(model.getNumberOfStates() * memory.getNumberOfStates()); + for (uint64_t modelState = 0; modelState < model.getNumberOfStates(); ++modelState) { + for (uint64_t memState = 0; memState < memory.getNumberOfStates(); ++memState) { + if (reachableStates.get(getProductState(modelState, memState))) { + res.push_back(modelAsMA.getExitRate(modelState)); + } + } + } + return res; + } + + template + storm::storage::BitVector SparseModelNondeterministicMemoryProduct::buildMarkovianStateLabeling(storm::models::sparse::MarkovAutomaton const& modelAsMA, storm::storage::BitVector const& reachableStates) const { + storm::storage::BitVector res(reachableStates.getNumberOfSetBits(), false); + uint64_t currReachableState = 0; + for (uint64_t modelState = 0; modelState < model.getNumberOfStates(); ++modelState) { + for (uint64_t memState = 0; memState < memory.getNumberOfStates(); ++memState) { + if (reachableStates.get(getProductState(modelState, memState))) { + if (modelAsMA.isMarkovianState(modelState)) { + res.set(currReachableState, true); + } + ++currReachableState; + } + } + } + assert(currReachableState == reachableStates.getNumberOfSetBits()); + return res; + } + + template + uint64_t SparseModelNondeterministicMemoryProduct::getProductState(uint64_t modelState, uint64_t memoryState) const { + return modelState * memory.getNumberOfStates() + memoryState; + } + + template + uint64_t SparseModelNondeterministicMemoryProduct::getModelState(uint64_t productState) const { + return productState / memory.getNumberOfStates(); + } + + template + uint64_t SparseModelNondeterministicMemoryProduct::getMemoryState(uint64_t productState) const { + return productState % memory.getNumberOfStates(); + } + + template class SparseModelNondeterministicMemoryProduct>; + template class SparseModelNondeterministicMemoryProduct>; + template class SparseModelNondeterministicMemoryProduct>; + template class SparseModelNondeterministicMemoryProduct>; + } +} \ No newline at end of file diff --git a/src/storm/storage/memorystructure/SparseModelNondeterministicMemoryProduct.h b/src/storm/storage/memorystructure/SparseModelNondeterministicMemoryProduct.h new file mode 100644 index 000000000..664d8c63d --- /dev/null +++ b/src/storm/storage/memorystructure/SparseModelNondeterministicMemoryProduct.h @@ -0,0 +1,37 @@ +#pragma once + +#include "storm/storage/memorystructure/NondeterministicMemoryStructure.h" +#include "storm/models/sparse/MarkovAutomaton.h" + +namespace storm { + namespace storage { + + + template + class SparseModelNondeterministicMemoryProduct { + public: + + typedef typename SparseModelType::ValueType ValueType; + + SparseModelNondeterministicMemoryProduct(SparseModelType const& model, storm::storage::NondeterministicMemoryStructure const& memory); + + std::shared_ptr build() const; + + private: + storm::storage::SparseMatrix buildTransitions() const; + storm::models::sparse::StateLabeling buildStateLabeling() const; + storm::models::sparse::StandardRewardModel buildRewardModel(storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& reachableStates) const; + + // Markov automaton specific components + std::vector buildExitRateVector(storm::models::sparse::MarkovAutomaton const& modelAsMA, storm::storage::BitVector const& reachableStates) const; + storm::storage::BitVector buildMarkovianStateLabeling(storm::models::sparse::MarkovAutomaton const& modelAsMA, storm::storage::BitVector const& reachableStates) const; + + uint64_t getProductState(uint64_t modelState, uint64_t memoryState) const; + uint64_t getModelState(uint64_t productState) const; + uint64_t getMemoryState(uint64_t productState) const; + + SparseModelType const& model; + storm::storage::NondeterministicMemoryStructure const& memory; + }; + } +} \ No newline at end of file