Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SparseModelMemoryProduct.h
Go to the documentation of this file.
1#pragma once
2
3#include <memory>
4#include <string>
5#include <unordered_map>
6
13
14namespace storm {
15namespace storage {
25template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>
27 public:
28 // Constructs the product w.r.t. the given model and the given memory structure
30 storm::storage::MemoryStructure const& memoryStructure);
31
32 // Constructs the product w.r.t. the given model and the given (finite memory) scheduler.
35
36 // Enforces that the given model and memory state as well as the successor(s) are considered reachable -- even if they are not reachable from an initial
37 // state.
38 void addReachableState(uint64_t const& modelState, uint64_t const& memoryState);
39
40 // Enforces that every state is considered reachable. If this is set, the result has size #modelStates * #memoryStates
42
43 // Returns true iff the given model and memory state is reachable in the product
44 bool isStateReachable(uint64_t const& modelState, uint64_t const& memoryState);
45
46 // Retrieves the state of the resulting model that represents the given memory and model state.
47 // This method should only be called if the given state is reachable.
48 uint64_t const& getResultState(uint64_t const& modelState, uint64_t const& memoryState);
49
55 std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> build(bool preserveModelType = false);
56
59
65
66 private:
67 // Initializes auxiliary data for building the product
68 void initialize();
69
70 // Computes for each pair of memory state and model transition index the successor memory state
71 // The resulting vector maps (modelTransition * memoryStateCount) + memoryState to the corresponding successor state of the memory structure
72 void computeMemorySuccessors();
73
74 // Computes the reachable states of the resulting model
75 void computeReachableStates(storm::storage::BitVector const& initialStates);
76
77 // Methods that build the model components
78 // Matrix for deterministic models
79 storm::storage::SparseMatrix<ValueType> buildDeterministicTransitionMatrix();
80 // Matrix for nondeterministic models
81 storm::storage::SparseMatrix<ValueType> buildNondeterministicTransitionMatrix();
82 // Matrix for models that consider a scheduler
83 storm::storage::SparseMatrix<ValueType> buildTransitionMatrixForScheduler();
84 // State labeling.
85 storm::models::sparse::StateLabeling buildStateLabeling(storm::storage::SparseMatrix<ValueType> const& resultTransitionMatrix);
86 // Reward models
87 std::unordered_map<std::string, RewardModelType> buildRewardModels(storm::storage::SparseMatrix<ValueType> const& resultTransitionMatrix);
88
89 // Builds the resulting model
90 std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> buildResult(storm::storage::SparseMatrix<ValueType>&& matrix,
92 std::unordered_map<std::string, RewardModelType>&& rewardModels,
93 bool preserveModelType);
94
95 // Stores whether this builder has already been initialized.
96 bool isInitialized;
97
98 // stores the successor memory states for each transition in the product
99 std::vector<uint64_t> memorySuccessors;
100
101 // Maps (modelState * memoryStateCount) + memoryState to the state in the result that represents (memoryState,modelState)
102 std::vector<uint64_t> toResultStateMapping;
103
104 // Indicates which states are considered reachable. (s, m) is reachable if this BitVector is true at (s * memoryStateCount) + m
105 storm::storage::BitVector reachableStates;
106
107 uint64_t const memoryStateCount;
108
110 boost::optional<storm::storage::MemoryStructure> localMemory;
112 boost::optional<storm::storage::Scheduler<ValueType> const&> scheduler;
113};
114} // namespace storage
115} // namespace storm
Base class for all sparse models.
Definition Model.h:32
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.
Definition BitVector.h:16
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.
Definition Scheduler.h:18
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)
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.
LabParser.cpp.