5#include <unordered_map>
25template<
typename ValueType,
typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>
44 bool isStateReachable(uint64_t
const& modelState, uint64_t
const& memoryState);
48 uint64_t
const&
getResultState(uint64_t
const& modelState, uint64_t
const& memoryState);
55 std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>
build(
bool preserveModelType =
false);
72 void computeMemorySuccessors();
92 std::unordered_map<std::string, RewardModelType>&& rewardModels,
93 bool preserveModelType);
99 std::vector<uint64_t> memorySuccessors;
102 std::vector<uint64_t> toResultStateMapping;
107 uint64_t
const memoryStateCount;
110 boost::optional<storm::storage::MemoryStructure> localMemory;
112 boost::optional<storm::storage::Scheduler<ValueType>
const&> scheduler;
Base class for all sparse models.
This class manages the labeling of the state space with a number of (atomic) labels.
A bit vector that is internally represented as a vector of 64-bit values.
This class represents a (deterministic) memory structure that can be used to encode certain events (s...
This class defines which action is chosen in a particular state of a non-deterministic model.
A class that holds a possibly non-square matrix in the compressed row storage format.
This class builds the product of the given sparse model and the given memory structure.
storm::storage::MemoryStructure const & getMemory() const
std::shared_ptr< storm::models::sparse::Model< ValueType, RewardModelType > > build(bool preserveModelType=false)
Invokes the building of the product under the specified scheduler (if given).
void addReachableState(uint64_t const &modelState, uint64_t const &memoryState)
void setBuildFullProduct()
SparseModelMemoryProductReverseData computeReverseData() const
Extracts the reverse data that can be used to apply results for the product model back to the origina...
storm::models::sparse::Model< ValueType, RewardModelType > const & getOriginalModel() const
bool isStateReachable(uint64_t const &modelState, uint64_t const &memoryState)
uint64_t const & getResultState(uint64_t const &modelState, uint64_t const &memoryState)
Data to restore memory incorporation applied with SparseModelMemoryProduct.