Browse Source
StateValuations and ChoiceOrigins are now members of a sparse::Model.
StateValuations and ChoiceOrigins are now members of a sparse::Model.
A model can now be constructed by providing a modelComponents struct.main
TimQu
9 years ago
57 changed files with 895 additions and 1329 deletions
-
55src/storm/builder/ExplicitModelBuilder.cpp
-
33src/storm/builder/ExplicitModelBuilder.h
-
78src/storm/builder/ExplicitModelBuilderResult.cpp
-
34src/storm/builder/ExplicitModelBuilderResult.h
-
27src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
-
4src/storm/builder/jit/ExplicitJitJaniModelBuilder.h
-
12src/storm/builder/jit/ModelComponentsBuilder.cpp
-
12src/storm/cli/entrypoints.h
-
31src/storm/counterexamples/MILPMinimalCommandSetGenerator.h
-
76src/storm/counterexamples/SMTMinimalCommandSetGenerator.h
-
42src/storm/models/sparse/Ctmc.cpp
-
21src/storm/models/sparse/Ctmc.h
-
21src/storm/models/sparse/DeterministicModel.cpp
-
29src/storm/models/sparse/DeterministicModel.h
-
31src/storm/models/sparse/Dtmc.cpp
-
26src/storm/models/sparse/Dtmc.h
-
4src/storm/models/sparse/ItemLabeling.cpp
-
7src/storm/models/sparse/ItemLabeling.h
-
88src/storm/models/sparse/MarkovAutomaton.cpp
-
72src/storm/models/sparse/MarkovAutomaton.h
-
54src/storm/models/sparse/Mdp.cpp
-
16src/storm/models/sparse/Mdp.h
-
127src/storm/models/sparse/Model.cpp
-
135src/storm/models/sparse/Model.h
-
25src/storm/models/sparse/NondeterministicModel.cpp
-
37src/storm/models/sparse/NondeterministicModel.h
-
2src/storm/models/sparse/StateLabeling.h
-
34src/storm/models/sparse/StochasticTwoPlayerGame.cpp
-
43src/storm/models/sparse/StochasticTwoPlayerGame.h
-
37src/storm/parser/DeterministicModelParser.cpp
-
47src/storm/parser/DeterministicModelParser.h
-
18src/storm/parser/DirectEncodingParser.cpp
-
29src/storm/parser/DirectEncodingParser.h
-
20src/storm/parser/MarkovAutomatonParser.cpp
-
23src/storm/parser/NondeterministicModelParser.cpp
-
54src/storm/parser/NondeterministicModelParser.h
-
13src/storm/storage/SparseMatrix.cpp
-
5src/storm/storage/SparseMatrix.h
-
58src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp
-
8src/storm/storage/sparse/ChoiceOrigins.cpp
-
12src/storm/storage/sparse/ChoiceOrigins.h
-
2src/storm/storage/sparse/JaniChoiceOrigins.cpp
-
4src/storm/storage/sparse/JaniChoiceOrigins.h
-
89src/storm/storage/sparse/ModelComponents.h
-
4src/storm/storage/sparse/PrismChoiceOrigins.cpp
-
4src/storm/storage/sparse/PrismChoiceOrigins.h
-
4src/storm/storage/sparse/StateValuations.cpp
-
5src/storm/storage/sparse/StateValuations.h
-
25src/storm/transformer/GoalStateMerger.cpp
-
292src/storm/transformer/StateDuplicator.h
-
68src/storm/transformer/SubsystemBuilder.h
-
47src/storm/utility/ModelInstantiator.h
-
35src/storm/utility/builder.cpp
-
19src/storm/utility/builder.h
-
10src/storm/utility/counterexamples.h
-
16src/storm/utility/storm.h
-
100src/test/transformer/StateDuplicatorTest.cpp
@ -1,78 +0,0 @@ |
|||
#include "storm/builder/ExplicitModelBuilderResult.h"
|
|||
|
|||
#include "storm/utility/macros.h"
|
|||
#include "storm/exceptions/InvalidOperationException.h"
|
|||
|
|||
#include "storm/adapters/CarlAdapter.h"
|
|||
#include "storm/models/sparse/StandardRewardModel.h"
|
|||
|
|||
namespace storm { |
|||
namespace builder { |
|||
|
|||
template <typename ValueType, typename RewardModelType> |
|||
ExplicitModelBuilderResult<ValueType, RewardModelType>::ExplicitModelBuilderResult(std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> model, std::shared_ptr<storm::storage::sparse::StateValuations> stateValuations,std::shared_ptr<storm::storage::sparse::ChoiceOrigins> choiceOrigins) : model(model), stateValuations(stateValuations), choiceOrigins(choiceOrigins) { |
|||
// Intentionally left empty
|
|||
} |
|||
|
|||
template <typename ValueType, typename RewardModelType> |
|||
bool ExplicitModelBuilderResult<ValueType, RewardModelType>::hasModel() { |
|||
return static_cast<bool>(model); |
|||
} |
|||
|
|||
template <typename ValueType, typename RewardModelType> |
|||
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>& ExplicitModelBuilderResult<ValueType, RewardModelType>::getModel() { |
|||
STORM_LOG_THROW(model, storm::exceptions::InvalidOperationException, "Retrieving the model failed since it is not set."); |
|||
return model; |
|||
} |
|||
|
|||
template <typename ValueType, typename RewardModelType> |
|||
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> const& ExplicitModelBuilderResult<ValueType, RewardModelType>::getModel() const { |
|||
STORM_LOG_THROW(model, storm::exceptions::InvalidOperationException, "Retrieving the model failed since it is not set."); |
|||
return model; |
|||
} |
|||
|
|||
template <typename ValueType, typename RewardModelType> |
|||
bool ExplicitModelBuilderResult<ValueType, RewardModelType>::hasStateValuations() { |
|||
return static_cast<bool>(stateValuations); |
|||
} |
|||
|
|||
template <typename ValueType, typename RewardModelType> |
|||
std::shared_ptr<storm::storage::sparse::StateValuations>& ExplicitModelBuilderResult<ValueType, RewardModelType>::getStateValuations() { |
|||
STORM_LOG_THROW(stateValuations, storm::exceptions::InvalidOperationException, "Retrieving the state valuations failed since they are not set."); |
|||
return stateValuations; |
|||
} |
|||
|
|||
template <typename ValueType, typename RewardModelType> |
|||
std::shared_ptr<storm::storage::sparse::StateValuations> const& ExplicitModelBuilderResult<ValueType, RewardModelType>::getStateValuations() const { |
|||
STORM_LOG_THROW(stateValuations, storm::exceptions::InvalidOperationException, "Retrieving the state valuations failed since they are not set."); |
|||
return stateValuations; |
|||
} |
|||
|
|||
template <typename ValueType, typename RewardModelType> |
|||
bool ExplicitModelBuilderResult<ValueType, RewardModelType>::hasChoiceOrigins() { |
|||
return static_cast<bool>(choiceOrigins); |
|||
} |
|||
|
|||
template <typename ValueType, typename RewardModelType> |
|||
std::shared_ptr<storm::storage::sparse::ChoiceOrigins>& ExplicitModelBuilderResult<ValueType, RewardModelType>::getChoiceOrigins() { |
|||
STORM_LOG_THROW(choiceOrigins, storm::exceptions::InvalidOperationException, "Retrieving the choice origins failed since they are not set."); |
|||
return choiceOrigins; |
|||
} |
|||
|
|||
template <typename ValueType, typename RewardModelType> |
|||
std::shared_ptr<storm::storage::sparse::ChoiceOrigins> const& ExplicitModelBuilderResult<ValueType, RewardModelType>::getChoiceOrigins() const { |
|||
STORM_LOG_THROW(choiceOrigins, storm::exceptions::InvalidOperationException, "Retrieving the choice origins failed since they are not set."); |
|||
return choiceOrigins; |
|||
} |
|||
|
|||
// Explicitly instantiate the class.
|
|||
template class ExplicitModelBuilderResult<double, storm::models::sparse::StandardRewardModel<double>>; |
|||
|
|||
#ifdef STORM_HAVE_CARL
|
|||
template class ExplicitModelBuilderResult<RationalNumber, storm::models::sparse::StandardRewardModel<RationalNumber>>; |
|||
template class ExplicitModelBuilderResult<RationalFunction, storm::models::sparse::StandardRewardModel<RationalFunction>>; |
|||
template class ExplicitModelBuilderResult<double, storm::models::sparse::StandardRewardModel<storm::Interval>>; |
|||
#endif
|
|||
|
|||
} |
|||
} |
|||
@ -1,34 +0,0 @@ |
|||
#pragma once |
|||
|
|||
#include <memory> |
|||
#include "storm/models/sparse/Model.h" |
|||
#include "storm/storage/sparse/StateValuations.h" |
|||
#include "storm/storage/sparse/ChoiceOrigins.h" |
|||
|
|||
namespace storm { |
|||
namespace builder { |
|||
|
|||
template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>> |
|||
class ExplicitModelBuilderResult { |
|||
public: |
|||
ExplicitModelBuilderResult(std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> model, std::shared_ptr<storm::storage::sparse::StateValuations> stateValuations = nullptr,std::shared_ptr<storm::storage::sparse::ChoiceOrigins> choiceOrigins = nullptr); |
|||
|
|||
bool hasModel(); |
|||
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>& getModel(); |
|||
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> const& getModel() const; |
|||
|
|||
bool hasStateValuations(); |
|||
std::shared_ptr<storm::storage::sparse::StateValuations>& getStateValuations(); |
|||
std::shared_ptr<storm::storage::sparse::StateValuations> const& getStateValuations() const; |
|||
|
|||
bool hasChoiceOrigins(); |
|||
std::shared_ptr<storm::storage::sparse::ChoiceOrigins>& getChoiceOrigins(); |
|||
std::shared_ptr<storm::storage::sparse::ChoiceOrigins> const& getChoiceOrigins() const; |
|||
|
|||
private: |
|||
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> model; |
|||
std::shared_ptr<storm::storage::sparse::StateValuations> stateValuations; |
|||
std::shared_ptr<storm::storage::sparse::ChoiceOrigins> choiceOrigins; |
|||
}; |
|||
} |
|||
} |
|||
@ -0,0 +1,89 @@ |
|||
#pragma once |
|||
|
|||
#include <vector> |
|||
#include <unordered_map> |
|||
#include <memory> |
|||
#include <boost/optional.hpp> |
|||
|
|||
#include "storm/models/ModelType.h" |
|||
#include "storm/models/sparse/StateLabeling.h" |
|||
#include "storm/models/sparse/ChoiceLabeling.h" |
|||
#include "storm/storage/sparse/StateType.h" |
|||
#include "storm/storage/sparse/StateValuations.h" |
|||
#include "storm/storage/sparse/ChoiceOrigins.h" |
|||
#include "storm/storage/SparseMatrix.h" |
|||
#include "storm/storage/BitVector.h" |
|||
#include "storm/models/sparse/StandardRewardModel.h" |
|||
|
|||
#include "storm/utility/macros.h" |
|||
#include "storm/exceptions/InvalidOperationException.h" |
|||
|
|||
namespace storm { |
|||
namespace storage { |
|||
namespace sparse { |
|||
|
|||
template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>> |
|||
struct ModelComponents { |
|||
|
|||
ModelComponents(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, |
|||
storm::models::sparse::StateLabeling const& stateLabeling = storm::models::sparse::StateLabeling(), |
|||
std::unordered_map<std::string, RewardModelType> const& rewardModels = std::unordered_map<std::string, RewardModelType>(), |
|||
bool rateTransitions = false, |
|||
boost::optional<storm::storage::BitVector> const& markovianStates = boost::none, |
|||
boost::optional<storm::storage::SparseMatrix<storm::storage::sparse::state_type>> const& player1Matrix = boost::none) |
|||
: transitionMatrix(transitionMatrix), stateLabeling(stateLabeling), rewardModels(rewardModels), rateTransitions(rateTransitions), markovianStates(markovianStates), player1Matrix(player1Matrix) { |
|||
// Intentionally left empty |
|||
|
|||
// TODO: remove this output |
|||
std::cout << "Called copy constructor for model components (which should be avoided)" << std::endl; |
|||
} |
|||
|
|||
ModelComponents(storm::storage::SparseMatrix<ValueType>&& transitionMatrix = storm::storage::SparseMatrix<ValueType>(), |
|||
storm::models::sparse::StateLabeling&& stateLabeling = storm::models::sparse::StateLabeling(), |
|||
std::unordered_map<std::string, RewardModelType>&& rewardModels = std::unordered_map<std::string, RewardModelType>(), |
|||
bool rateTransitions = false, |
|||
boost::optional<storm::storage::BitVector>&& markovianStates = boost::none, |
|||
boost::optional<storm::storage::SparseMatrix<storm::storage::sparse::state_type>>&& player1Matrix = boost::none) |
|||
: transitionMatrix(std::move(transitionMatrix)), stateLabeling(std::move(stateLabeling)), rewardModels(std::move(rewardModels)), rateTransitions(rateTransitions), markovianStates(std::move(markovianStates)), player1Matrix(std::move(player1Matrix)) { |
|||
// Intentionally left empty |
|||
} |
|||
|
|||
|
|||
|
|||
|
|||
// General components (applicable for all model types): |
|||
|
|||
// The transition matrix. |
|||
storm::storage::SparseMatrix<ValueType> transitionMatrix; |
|||
// The state labeling. |
|||
storm::models::sparse::StateLabeling stateLabeling; |
|||
// The reward models associated with the model. |
|||
std::unordered_map<std::string, RewardModelType> rewardModels; |
|||
// A vector that stores a labeling for each choice. |
|||
boost::optional<storm::models::sparse::ChoiceLabeling> choiceLabeling; |
|||
// stores for each state to which variable valuation it belongs |
|||
boost::optional<storm::storage::sparse::StateValuations> stateValuations; |
|||
// stores for each choice from which parts of the input model description it originates |
|||
boost::optional<std::shared_ptr<storm::storage::sparse::ChoiceOrigins>> choiceOrigins; |
|||
|
|||
|
|||
// Continuous time specific components (CTMCs, Markov Automata): |
|||
|
|||
// True iff the transition values (for Markovian choices) are interpreted as rates. |
|||
bool rateTransitions; |
|||
|
|||
// The exit rate for each state. Must be given for CTMCs and MAs, if rateTransitions is false. Otherwise, it is optional. |
|||
boost::optional<std::vector<ValueType>> exitRates; |
|||
|
|||
// A vector that stores which states are markovian (only for Markov Automata). |
|||
boost::optional<storm::storage::BitVector> markovianStates; |
|||
|
|||
|
|||
// Stochastic two player game specific components: |
|||
|
|||
// The matrix of player 1 choices (needed for stochastic two player games |
|||
boost::optional<storm::storage::SparseMatrix<storm::storage::sparse::state_type>> player1Matrix; |
|||
}; |
|||
} |
|||
} |
|||
} |
|||
@ -1,292 +0,0 @@ |
|||
#ifndef STORM_TRANSFORMER_STATEDUPLICATOR_H |
|||
#define STORM_TRANSFORMER_STATEDUPLICATOR_H |
|||
|
|||
|
|||
#include <memory> |
|||
#include <boost/optional.hpp> |
|||
|
|||
#include "storm/models/sparse/StandardRewardModel.h" |
|||
#include "storm/utility/constants.h" |
|||
#include "storm/utility/graph.h" |
|||
#include "storm/utility/macros.h" |
|||
#include "storm/utility/vector.h" |
|||
#include "storm/models/sparse/Dtmc.h" |
|||
#include "storm/models/sparse/Mdp.h" |
|||
#include "storm/models/sparse/Ctmc.h" |
|||
#include "storm/models/sparse/MarkovAutomaton.h" |
|||
|
|||
|
|||
namespace storm { |
|||
namespace transformer { |
|||
|
|||
/* |
|||
* 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. |
|||
*/ |
|||
template <typename SparseModelType> |
|||
class StateDuplicator { |
|||
public: |
|||
|
|||
struct StateDuplicatorReturnType { |
|||
std::shared_ptr<SparseModelType> model; // The resulting model |
|||
storm::storage::BitVector firstCopy; // The states of the resulting model that correspond to the first copy |
|||
storm::storage::BitVector secondCopy; // The states of the resulting model that correspond to the second copy |
|||
storm::storage::BitVector gateStates; // The gate states of the resulting model |
|||
std::vector<uint_fast64_t> newToOldStateIndexMapping; // Gives for each state in the resulting model the corresponding state in the original model |
|||
std::vector<uint_fast64_t> firstCopyOldToNewStateIndexMapping; //Maps old indices of states in the first copy to their new indices |
|||
std::vector<uint_fast64_t> secondCopyOldToNewStateIndexMapping; //Maps old indices of states in the second copy to their new indices |
|||
storm::storage::BitVector duplicatedStates; // The states in the original model that have been duplicated |
|||
storm::storage::BitVector reachableStates; // The states in the original model that are reachable from the initial state |
|||
}; |
|||
|
|||
/* |
|||
* 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. |
|||
* |
|||
* Note that only reachable states are kept. |
|||
* Gate states will always belong to the second copy. |
|||
* Rewards and labels are duplicated accordingly. |
|||
* However, the non-gateStates in the second copy will not get the label for initial states. |
|||
* |
|||
* @param originalModel The model to be duplicated |
|||
* @param gateStates The states for which the incoming transitions are redirected |
|||
*/ |
|||
static StateDuplicatorReturnType transform(SparseModelType const& originalModel, storm::storage::BitVector const& gateStates) { |
|||
STORM_LOG_DEBUG("Invoked state duplicator on model with " << originalModel.getNumberOfStates() << " states."); |
|||
StateDuplicatorReturnType result; |
|||
|
|||
// Collect some data for the result |
|||
initializeTransformation(originalModel, gateStates, result); |
|||
|
|||
// Transform the ingedients of the model |
|||
storm::storage::SparseMatrix<typename SparseModelType::ValueType> matrix = transformMatrix(originalModel.getTransitionMatrix(), result, gateStates); |
|||
storm::models::sparse::StateLabeling stateLabeling(matrix.getRowGroupCount()); |
|||
for (auto const& label : originalModel.getStateLabeling().getLabels()) { |
|||
storm::storage::BitVector newBitVectorForLabel = transformStateBitVector(originalModel.getStateLabeling().getStates(label), result); |
|||
if (label=="init") { |
|||
newBitVectorForLabel &= (result.firstCopy | result.gateStates); |
|||
} |
|||
stateLabeling.addLabel(label, std::move(newBitVectorForLabel)); |
|||
} |
|||
|
|||
std::unordered_map<std::string, typename SparseModelType::RewardModelType> rewardModels; |
|||
for (auto const& rewardModel : originalModel.getRewardModels()) { |
|||
rewardModels.insert(std::make_pair(rewardModel.first, transformRewardModel(rewardModel.second, originalModel.getTransitionMatrix().getRowGroupIndices(), result, gateStates))); |
|||
} |
|||
|
|||
boost::optional<storm::models::sparse::ChoiceLabeling> choiceLabeling; |
|||
if (originalModel.hasChoiceLabeling()) { |
|||
for (auto const& label : originalModel.getChoiceLabeling().getLabels()) { |
|||
storm::storage::BitVector newBitVectorForLabel = transformActionBitVector(originalModel.getChoiceLabeling().getChoices(label), originalModel.getTransitionMatrix().getRowGroupIndices(), result); |
|||
choiceLabeling->addLabel(label, std::move(newBitVectorForLabel)); |
|||
} |
|||
} |
|||
|
|||
result.model = std::make_shared<SparseModelType>(createTransformedModel(originalModel, result, matrix, stateLabeling, rewardModels, choiceLabeling)); |
|||
STORM_LOG_DEBUG("State duplicator is done. Resulting model has " << result.model->getNumberOfStates() << " states, where " << result.firstCopy.getNumberOfSetBits() << " are in the first copy."); |
|||
return result; |
|||
} |
|||
|
|||
private: |
|||
|
|||
static void initializeTransformation(SparseModelType const& originalModel, storm::storage::BitVector const& gateStates, StateDuplicatorReturnType& result) { |
|||
|
|||
storm::storage::BitVector noStates(originalModel.getNumberOfStates(), false); |
|||
// Get the states that are reachable without visiting a gateState |
|||
storm::storage::BitVector statesForFirstCopy = storm::utility::graph::getReachableStates(originalModel.getTransitionMatrix(), originalModel.getInitialStates(), ~gateStates, noStates); |
|||
|
|||
// Get the states reachable from gateStates |
|||
storm::storage::BitVector statesForSecondCopy = storm::utility::graph::getReachableStates(originalModel.getTransitionMatrix(), gateStates, ~noStates, noStates); |
|||
|
|||
result.duplicatedStates = statesForFirstCopy & statesForSecondCopy; |
|||
result.reachableStates = statesForFirstCopy | statesForSecondCopy; |
|||
|
|||
uint_fast64_t numStates = statesForFirstCopy.getNumberOfSetBits() + statesForSecondCopy.getNumberOfSetBits(); |
|||
result.firstCopy = statesForFirstCopy % result.reachableStates; // only consider reachable states |
|||
result.firstCopy.resize(numStates, false); // the new states do NOT belong to the first copy |
|||
result.secondCopy = (statesForSecondCopy & (~statesForFirstCopy)) % result.reachableStates; // only consider reachable states |
|||
result.secondCopy.resize(numStates, true); // the new states DO belong to the second copy |
|||
STORM_LOG_ASSERT((result.firstCopy^result.secondCopy).full(), "firstCopy and secondCopy do not partition the state space."); |
|||
|
|||
// Get the state mappings. |
|||
// We initialize them with illegal values to assert that we don't get a valid |
|||
// state when given e.g. an unreachable state or a state from the other copy. |
|||
result.newToOldStateIndexMapping = std::vector<uint_fast64_t>(numStates, std::numeric_limits<uint_fast64_t>::max()); |
|||
result.firstCopyOldToNewStateIndexMapping = std::vector<uint_fast64_t>(originalModel.getNumberOfStates(), std::numeric_limits<uint_fast64_t>::max()); |
|||
result.secondCopyOldToNewStateIndexMapping = std::vector<uint_fast64_t>(originalModel.getNumberOfStates(), std::numeric_limits<uint_fast64_t>::max()); |
|||
uint_fast64_t newState = 0; |
|||
for (auto const& oldState : result.reachableStates) { |
|||
result.newToOldStateIndexMapping[newState] = oldState; |
|||
if (statesForFirstCopy.get(oldState)) { |
|||
result.firstCopyOldToNewStateIndexMapping[oldState] = newState; |
|||
} else { |
|||
result.secondCopyOldToNewStateIndexMapping[oldState] = newState; |
|||
} |
|||
++newState; |
|||
} |
|||
// The remaining states are duplicates. All these states belong to the second copy. |
|||
|
|||
for (auto const& oldState : result.duplicatedStates) { |
|||
result.newToOldStateIndexMapping[newState] = oldState; |
|||
result.secondCopyOldToNewStateIndexMapping[oldState] = newState; |
|||
++newState; |
|||
} |
|||
STORM_LOG_ASSERT(newState == numStates, "Unexpected state Indices"); |
|||
|
|||
result.gateStates = transformStateBitVector(gateStates, result); |
|||
} |
|||
|
|||
template<typename ValueType = typename SparseModelType::ValueType, typename RewardModelType = typename SparseModelType::RewardModelType> |
|||
static typename std::enable_if<std::is_same<RewardModelType, storm::models::sparse::StandardRewardModel<ValueType>>::value, RewardModelType>::type |
|||
transformRewardModel(RewardModelType const& originalRewardModel, std::vector<uint_fast64_t> const& originalRowGroupIndices, StateDuplicatorReturnType const& result, storm::storage::BitVector const& gateStates) { |
|||
boost::optional<std::vector<ValueType>> stateRewardVector; |
|||
boost::optional<std::vector<ValueType>> stateActionRewardVector; |
|||
boost::optional<storm::storage::SparseMatrix<ValueType>> transitionRewardMatrix; |
|||
if (originalRewardModel.hasStateRewards()) { |
|||
stateRewardVector = transformStateValueVector(originalRewardModel.getStateRewardVector(), result); |
|||
} |
|||
if (originalRewardModel.hasStateActionRewards()) { |
|||
stateActionRewardVector = transformActionValueVector(originalRewardModel.getStateActionRewardVector(), originalRowGroupIndices, result); |
|||
} |
|||
if (originalRewardModel.hasTransitionRewards()) { |
|||
transitionRewardMatrix = transformMatrix(originalRewardModel.getTransitionRewardMatrix(), result, gateStates); |
|||
} |
|||
return RewardModelType(std::move(stateRewardVector), std::move(stateActionRewardVector), std::move(transitionRewardMatrix)); |
|||
} |
|||
|
|||
template<typename ValueType = typename SparseModelType::ValueType> |
|||
static storm::storage::SparseMatrix<ValueType> transformMatrix(storm::storage::SparseMatrix<ValueType> const& originalMatrix, StateDuplicatorReturnType const& result, storm::storage::BitVector const& gateStates) { |
|||
// Build the builder |
|||
uint_fast64_t numStates = result.newToOldStateIndexMapping.size(); |
|||
uint_fast64_t numRows = 0; |
|||
uint_fast64_t numEntries = 0; |
|||
for (auto const& oldState : result.newToOldStateIndexMapping) { |
|||
numRows += originalMatrix.getRowGroupSize(oldState); |
|||
numEntries += originalMatrix.getRowGroupEntryCount(oldState); |
|||
} |
|||
storm::storage::SparseMatrixBuilder<ValueType> 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 = originalMatrix.getRowGroupIndices()[oldState]; oldRow < originalMatrix.getRowGroupIndices()[oldState+1]; ++oldRow) { |
|||
for (auto const& entry : originalMatrix.getRow(oldRow)) { |
|||
if (result.firstCopy.get(newState) && !gateStates.get(entry.getColumn())) { |
|||
builder.addNextValue(newRow, result.firstCopyOldToNewStateIndexMapping[entry.getColumn()], entry.getValue()); |
|||
} else if (!result.duplicatedStates.get(entry.getColumn())) { |
|||
builder.addNextValue(newRow, result.secondCopyOldToNewStateIndexMapping[entry.getColumn()], entry.getValue()); |
|||
} |
|||
} |
|||
//To add values in the right order, transitions to duplicated states have to be added in a second run. |
|||
for (auto const& entry : originalMatrix.getRow(oldRow)) { |
|||
if (result.secondCopy.get(newState) && result.duplicatedStates.get(entry.getColumn())) { |
|||
builder.addNextValue(newRow, result.secondCopyOldToNewStateIndexMapping[entry.getColumn()], entry.getValue()); |
|||
} |
|||
} |
|||
++newRow; |
|||
} |
|||
} |
|||
|
|||
return builder.build(); |
|||
} |
|||
|
|||
|
|||
template<typename ValueType = typename SparseModelType::ValueType> |
|||
static std::vector<ValueType> transformActionValueVector(std::vector<ValueType>const& originalVector, std::vector<uint_fast64_t> const& originalRowGroupIndices, StateDuplicatorReturnType const& result) { |
|||
uint_fast64_t numActions = 0; |
|||
for (auto const& oldState : result.newToOldStateIndexMapping) { |
|||
numActions += originalRowGroupIndices[oldState+1] - originalRowGroupIndices[oldState]; |
|||
} |
|||
std::vector<ValueType> v; |
|||
v.reserve(numActions); |
|||
for (auto const& oldState : result.newToOldStateIndexMapping) { |
|||
for (uint_fast64_t oldAction = originalRowGroupIndices[oldState]; oldAction < originalRowGroupIndices[oldState+1]; ++oldAction) { |
|||
v.push_back(originalVector[oldAction]); |
|||
} |
|||
} |
|||
STORM_LOG_ASSERT(v.size() == numActions, "Unexpected vector size."); |
|||
return v; |
|||
} |
|||
|
|||
template<typename ValueType = typename SparseModelType::ValueType> |
|||
static std::vector<ValueType> transformStateValueVector(std::vector<ValueType> const& originalVector, StateDuplicatorReturnType const& result) { |
|||
uint_fast64_t numStates = result.newToOldStateIndexMapping.size(); |
|||
std::vector<ValueType> v; |
|||
v.reserve(numStates); |
|||
for (auto const& oldState : result.newToOldStateIndexMapping) { |
|||
v.push_back(originalVector[oldState]); |
|||
} |
|||
STORM_LOG_ASSERT(v.size() == numStates, "Unexpected vector size."); |
|||
return v; |
|||
} |
|||
|
|||
static storm::storage::BitVector transformActionBitVector(storm::storage::BitVector const& originalBitVector, std::vector<uint_fast64_t> const& originalRowGroupIndices, StateDuplicatorReturnType const& result) { |
|||
uint_fast64_t numActions = 0; |
|||
for (auto const& oldState : result.newToOldStateIndexMapping) { |
|||
numActions += originalRowGroupIndices[oldState+1] - originalRowGroupIndices[oldState]; |
|||
} |
|||
storm::storage::BitVector bv(numActions, false); |
|||
uint_fast64_t newAction = 0; |
|||
for (auto const& oldState : result.newToOldStateIndexMapping) { |
|||
for (uint_fast64_t oldAction = originalRowGroupIndices[oldState]; oldAction < originalRowGroupIndices[oldState+1]; ++oldAction) { |
|||
if (originalBitVector.get(oldAction)) { |
|||
bv.set(newAction, true); |
|||
} |
|||
++newAction; |
|||
} |
|||
} |
|||
STORM_LOG_ASSERT(newAction == numActions, "Unexpected vector size."); |
|||
return bv; |
|||
} |
|||
|
|||
static storm::storage::BitVector transformStateBitVector(storm::storage::BitVector const& originalBitVector, StateDuplicatorReturnType const& result) { |
|||
uint_fast64_t numStates = result.newToOldStateIndexMapping.size(); |
|||
storm::storage::BitVector bv(numStates); |
|||
for (uint_fast64_t newState = 0; newState < numStates; ++newState) { |
|||
uint_fast64_t oldState = result.newToOldStateIndexMapping[newState]; |
|||
bv.set(newState, originalBitVector.get(oldState)); |
|||
} |
|||
return bv; |
|||
} |
|||
|
|||
|
|||
template<typename MT = SparseModelType> |
|||
static typename std::enable_if< |
|||
std::is_same<MT,storm::models::sparse::Dtmc<typename SparseModelType::ValueType>>::value || |
|||
std::is_same<MT,storm::models::sparse::Mdp<typename SparseModelType::ValueType>>::value || |
|||
std::is_same<MT,storm::models::sparse::Ctmc<typename SparseModelType::ValueType>>::value, |
|||
MT>::type |
|||
createTransformedModel(MT const& /*originalModel*/, |
|||
StateDuplicatorReturnType const& /*result*/, |
|||
storm::storage::SparseMatrix<typename MT::ValueType>& matrix, |
|||
storm::models::sparse::StateLabeling& stateLabeling, |
|||
std::unordered_map<std::string, |
|||
typename MT::RewardModelType>& rewardModels, |
|||
boost::optional<storm::models::sparse::ChoiceLabeling>& choiceLabeling ) { |
|||
return MT(std::move(matrix), std::move(stateLabeling), std::move(rewardModels), std::move(choiceLabeling)); |
|||
} |
|||
|
|||
template<typename MT = SparseModelType> |
|||
static typename std::enable_if< |
|||
std::is_same<MT,storm::models::sparse::MarkovAutomaton<typename SparseModelType::ValueType>>::value, |
|||
MT>::type |
|||
createTransformedModel(MT const& originalModel, |
|||
StateDuplicatorReturnType const& result, |
|||
storm::storage::SparseMatrix<typename MT::ValueType>& matrix, |
|||
storm::models::sparse::StateLabeling& stateLabeling, |
|||
std::unordered_map<std::string, |
|||
typename MT::RewardModelType>& rewardModels, |
|||
boost::optional<storm::models::sparse::ChoiceLabeling>& choiceLabeling ) { |
|||
storm::storage::BitVector markovianStates = transformStateBitVector(originalModel.getMarkovianStates(), result); |
|||
std::vector<typename MT::ValueType> exitRates = transformStateValueVector(originalModel.getExitRates(), result); |
|||
return MT(std::move(matrix), std::move(stateLabeling), std::move(markovianStates), std::move(exitRates), true, std::move(rewardModels), std::move(choiceLabeling)); |
|||
} |
|||
|
|||
|
|||
}; |
|||
} |
|||
} |
|||
#endif // STORM_TRANSFORMER_STATEDUPLICATOR_H |
|||
@ -0,0 +1,35 @@ |
|||
#include <storm/models/sparse/StochasticTwoPlayerGame.h>
|
|||
#include "storm/utility/builder.h"
|
|||
|
|||
#include "storm/models/sparse/Dtmc.h"
|
|||
#include "storm/models/sparse/Ctmc.h"
|
|||
#include "storm/models/sparse/Mdp.h"
|
|||
#include "storm/models/sparse/MarkovAutomaton.h"
|
|||
|
|||
namespace storm { |
|||
namespace utility { |
|||
namespace builder { |
|||
|
|||
template<typename ValueType, typename RewardModelType> |
|||
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> buildModelFromComponents(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents<ValueType, RewardModelType>&& components) { |
|||
switch (modelType) { |
|||
case storm::models::ModelType::Dtmc: |
|||
return std::make_shared<storm::models::sparse::Dtmc<ValueType, RewardModelType>>(std::move(components)); |
|||
case storm::models::ModelType::Ctmc: |
|||
return std::make_shared<storm::models::sparse::Ctmc<ValueType, RewardModelType>>(std::move(components)); |
|||
case storm::models::ModelType::Mdp: |
|||
return std::make_shared<storm::models::sparse::Mdp<ValueType, RewardModelType>>(std::move(components)); |
|||
case storm::models::ModelType::MarkovAutomaton: |
|||
return std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType, RewardModelType>>(std::move(components)); |
|||
case storm::models::ModelType::S2pg: |
|||
return std::make_shared<storm::models::sparse::StochasticTwoPlayerGame<ValueType, RewardModelType>>(std::move(components)); |
|||
} |
|||
} |
|||
|
|||
template std::shared_ptr<storm::models::sparse::Model<double>> buildModelFromComponents(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents<double>&& components); |
|||
template std::shared_ptr<storm::models::sparse::Model<double, storm::models::sparse::StandardRewardModel<storm::Interval>>> buildModelFromComponents(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents<double, storm::models::sparse::StandardRewardModel<storm::Interval>>&& components); |
|||
template std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> buildModelFromComponents(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents<storm::RationalNumber>&& components); |
|||
template std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> buildModelFromComponents(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents<storm::RationalFunction>&& components); |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,19 @@ |
|||
#pragma once |
|||
|
|||
#include <memory> |
|||
|
|||
#include "storm/models/ModelType.h" |
|||
#include "storm/models/sparse/StandardRewardModel.h" |
|||
#include "storm/models/sparse/Model.h" |
|||
#include "storm/storage/sparse/ModelComponents.h" |
|||
|
|||
namespace storm { |
|||
namespace utility { |
|||
namespace builder { |
|||
|
|||
template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>> |
|||
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> buildModelFromComponents(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents<ValueType, RewardModelType>&& components); |
|||
|
|||
} |
|||
} |
|||
} |
|||
@ -1,100 +0,0 @@ |
|||
#include "gtest/gtest.h"
|
|||
|
|||
#include "storm/transformer/StateDuplicator.h"
|
|||
|
|||
|
|||
TEST(StateDuplicator, SimpleModelTest) { |
|||
|
|||
storm::storage::SparseMatrix<double> matrix; |
|||
storm::storage::SparseMatrixBuilder<double> builder(6, 4, 7, true, true, 4); |
|||
ASSERT_NO_THROW(builder.newRowGroup(0)); |
|||
ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.3)); |
|||
ASSERT_NO_THROW(builder.addNextValue(0, 1, 0.7)); |
|||
ASSERT_NO_THROW(builder.addNextValue(1, 3, 1.0)); |
|||
ASSERT_NO_THROW(builder.newRowGroup(2)); |
|||
ASSERT_NO_THROW(builder.addNextValue(2, 1, 1.0)); |
|||
ASSERT_NO_THROW(builder.newRowGroup(3)); |
|||
ASSERT_NO_THROW(builder.addNextValue(3, 0, 1.0)); |
|||
ASSERT_NO_THROW(builder.newRowGroup(4)); |
|||
ASSERT_NO_THROW(builder.addNextValue(4, 0, 1.0)); |
|||
ASSERT_NO_THROW(builder.addNextValue(5, 3, 1.0)); |
|||
ASSERT_NO_THROW(matrix = builder.build()); |
|||
|
|||
storm::models::sparse::StateLabeling labeling(4); |
|||
storm::storage::BitVector initStates(4); |
|||
initStates.set(0); |
|||
labeling.addLabel("init", initStates); |
|||
storm::storage::BitVector gateStates(4); |
|||
gateStates.set(3); |
|||
labeling.addLabel("gate", gateStates); |
|||
storm::storage::BitVector aStates(4); |
|||
aStates.set(0); |
|||
aStates.set(2); |
|||
labeling.addLabel("a", aStates); |
|||
storm::storage::BitVector bStates(4); |
|||
bStates.set(1); |
|||
bStates.set(3); |
|||
labeling.addLabel("b", bStates); |
|||
|
|||
std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<double>> rewardModels; |
|||
std::vector<double> stateReward = {1.0, 2.0, 3.0, 4.0}; |
|||
std::vector<double> stateActionReward = {1.1, 1.2, 2.1, 3.1, 4.1, 4.2}; |
|||
rewardModels.insert(std::make_pair("rewards", storm::models::sparse::StandardRewardModel<double>(stateReward, stateActionReward))); |
|||
|
|||
storm::models::sparse::Mdp<double> model(matrix, labeling, rewardModels); |
|||
|
|||
auto res = storm::transformer::StateDuplicator<storm::models::sparse::Mdp<double>>::transform(model, gateStates); |
|||
|
|||
storm::storage::SparseMatrixBuilder<double> expectedBuilder(8, 5, 10, true, true, 5); |
|||
ASSERT_NO_THROW(expectedBuilder.newRowGroup(0)); |
|||
ASSERT_NO_THROW(expectedBuilder.addNextValue(0, 0, 0.3)); |
|||
ASSERT_NO_THROW(expectedBuilder.addNextValue(0, 1, 0.7)); |
|||
ASSERT_NO_THROW(expectedBuilder.addNextValue(1, 2, 1.0)); |
|||
ASSERT_NO_THROW(expectedBuilder.newRowGroup(2)); |
|||
ASSERT_NO_THROW(expectedBuilder.addNextValue(2, 1, 1.0)); |
|||
ASSERT_NO_THROW(expectedBuilder.newRowGroup(3)); |
|||
ASSERT_NO_THROW(expectedBuilder.addNextValue(3, 3, 1.0)); |
|||
ASSERT_NO_THROW(expectedBuilder.addNextValue(4, 2, 1.0)); |
|||
ASSERT_NO_THROW(expectedBuilder.newRowGroup(5)); |
|||
ASSERT_NO_THROW(expectedBuilder.addNextValue(5, 3, 0.3)); |
|||
ASSERT_NO_THROW(expectedBuilder.addNextValue(5, 4, 0.7)); |
|||
ASSERT_NO_THROW(expectedBuilder.addNextValue(6, 2, 1.0)); |
|||
ASSERT_NO_THROW(expectedBuilder.newRowGroup(7)); |
|||
ASSERT_NO_THROW(expectedBuilder.addNextValue(7, 4, 1.0)); |
|||
ASSERT_NO_THROW(matrix = expectedBuilder.build()); |
|||
EXPECT_EQ(matrix, res.model->getTransitionMatrix()); |
|||
|
|||
initStates.resize(5); |
|||
EXPECT_EQ(initStates, res.model->getInitialStates()); |
|||
gateStates=storm::storage::BitVector(5); |
|||
gateStates.set(2); |
|||
EXPECT_EQ(gateStates, res.model->getStates("gate")); |
|||
aStates = initStates; |
|||
aStates.set(3); |
|||
EXPECT_EQ(aStates, res.model->getStates("a")); |
|||
bStates = ~aStates; |
|||
EXPECT_EQ(bStates, res.model->getStates("b")); |
|||
|
|||
EXPECT_TRUE(res.model->hasRewardModel("rewards")); |
|||
EXPECT_TRUE(res.model->getRewardModel("rewards").hasStateRewards()); |
|||
stateReward = {1.0, 2.0, 4.0, 1.0, 2.0}; |
|||
EXPECT_EQ(stateReward, res.model->getRewardModel("rewards").getStateRewardVector()); |
|||
EXPECT_TRUE(res.model->getRewardModel("rewards").hasStateActionRewards()); |
|||
stateActionReward = {1.1, 1.2, 2.1, 4.1, 4.2, 1.1, 1.2, 2.1}; |
|||
EXPECT_EQ(stateActionReward, res.model->getRewardModel("rewards").getStateActionRewardVector()); |
|||
|
|||
storm::storage::BitVector firstCopy(5); |
|||
firstCopy.set(0); |
|||
firstCopy.set(1); |
|||
EXPECT_EQ(firstCopy, res.firstCopy); |
|||
EXPECT_EQ(~firstCopy, res.secondCopy); |
|||
|
|||
std::vector<uint_fast64_t> mapping = {0,1,3,0,1}; |
|||
EXPECT_EQ(mapping, res.newToOldStateIndexMapping); |
|||
uint_fast64_t max = std::numeric_limits<uint_fast64_t>::max(); |
|||
mapping = {0, 1, max, max}; |
|||
EXPECT_EQ(mapping, res.firstCopyOldToNewStateIndexMapping); |
|||
mapping = {3, 4, max, 2}; |
|||
EXPECT_EQ(mapping, res.secondCopyOldToNewStateIndexMapping); |
|||
|
|||
} |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue