Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
JaniNextStateGenerator.h
Go to the documentation of this file.
1#pragma once
2
5
10
11namespace storm {
12namespace jani {
13class Edge;
14class EdgeDestination;
15} // namespace jani
16
17namespace generator {
18template<typename StateType, typename ValueType>
19class Distribution;
20
21template<typename ValueType, typename StateType = uint32_t>
22class JaniNextStateGenerator : public NextStateGenerator<ValueType, StateType> {
23 public:
24 static_assert(!storm::IsIntervalType<ValueType>, "JaniNextStateGenerator does not support interval types.");
28
30
35
41 static bool canHandle(storm::jani::Model const& model);
42
43 virtual ModelType getModelType() const override;
44 virtual bool isDeterministicModel() const override;
45 virtual bool isDiscreteTimeModel() const override;
46 virtual bool isPartiallyObservable() const override;
47 virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) override;
48
51
52 virtual StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback) override;
53
55 virtual void addStateValuation(storm::storage::sparse::state_type const& currentStateIndex,
56 storm::storage::sparse::StateValuationsBuilder& valuationsBuilder) const override;
57
58 virtual std::size_t getNumberOfRewardModels() const override;
59 virtual storm::builder::RewardModelInformation getRewardModelInformation(uint64_t const& index) const override;
60
62 std::vector<StateType> const& initialStateIndices = {},
63 std::vector<StateType> const& deadlockStateIndices = {},
64 std::vector<StateType> const& unexploredStateIndices = {}) override;
65
66 virtual std::shared_ptr<storm::storage::sparse::ChoiceOrigins> generateChoiceOrigins(std::vector<boost::any>& dataForChoiceOrigins) const override;
67
78
79 private:
83 uint64_t getLocation(CompressedState const& state, LocationVariableInformation const& locationVariable) const;
84
88 void setLocation(CompressedState& state, LocationVariableInformation const& locationVariable, uint64_t locationIndex) const;
89
93 std::vector<uint64_t> getLocations(CompressedState const& state) const;
94
101
111 void applyUpdate(CompressedState& state, storm::jani::EdgeDestination const& destination,
112 storm::generator::LocationVariableInformation const& locationVariable, int64_t assignmentlevel,
113 storm::expressions::ExpressionEvaluator<ValueType> const& expressionEvaluator);
114
124 void applyTransientUpdate(TransientVariableValuation<ValueType>& transientValuation, storm::jani::detail::ConstAssignments const& transientAssignments,
125 storm::expressions::ExpressionEvaluator<ValueType> const& expressionEvaluator) const;
126
134 virtual storm::storage::BitVector evaluateObservationLabels(CompressedState const& state) const override;
135
142 TransientVariableValuation<ValueType> getTransientVariableValuationAtLocations(std::vector<uint64_t> const& locations,
144
153 std::vector<Choice<ValueType>> getActionChoices(std::vector<uint64_t> const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback,
154 EdgeFilter const& edgeFilter = EdgeFilter::All);
155
159 Choice<ValueType> expandNonSynchronizingEdge(storm::jani::Edge const& edge, uint64_t outputActionIndex, uint64_t automatonIndex,
160 CompressedState const& state, StateToIdCallback stateToIdCallback);
161
162 typedef std::vector<std::pair<uint64_t, storm::jani::Edge const*>> EdgeSetWithIndices;
163 typedef std::unordered_map<uint64_t, EdgeSetWithIndices> LocationsAndEdges;
164 typedef std::vector<std::pair<uint64_t, LocationsAndEdges>> AutomataAndEdges;
165 typedef std::pair<boost::optional<uint64_t>, AutomataAndEdges> OutputAndEdges;
166
167 typedef std::pair<uint64_t, EdgeSetWithIndices> AutomatonAndEdgeSet;
168 typedef std::vector<AutomatonAndEdgeSet> AutomataEdgeSets;
169
170 void expandSynchronizingEdgeCombination(AutomataEdgeSets const& edgeCombination, uint64_t outputActionIndex, CompressedState const& state,
171 StateToIdCallback stateToIdCallback, std::vector<Choice<ValueType>>& newChoices);
172 void generateSynchronizedDistribution(storm::storage::BitVector const& state, AutomataEdgeSets const& edgeCombination,
173 std::vector<EdgeSetWithIndices::const_iterator> const& iteratorList,
174 storm::generator::Distribution<StateType, ValueType>& distribution, std::vector<ValueType>& stateActionRewards,
175 EdgeIndexSet& edgeIndices, StateToIdCallback stateToIdCallback);
176
180 void checkGlobalVariableWritesValid(AutomataEdgeSets const& enabledEdges) const;
181
185 std::vector<ValueType> evaluateRewardExpressions() const;
186
190 void addEvaluatedRewardExpressions(std::vector<ValueType>& rewards, ValueType const& factor) const;
191
195 void buildRewardModelInformation();
196
200 void createSynchronizationInformation();
201
205 void checkValid() const;
206
208 storm::jani::Model model;
209
211 std::vector<std::reference_wrapper<storm::jani::Automaton const>> parallelAutomata;
212
214 std::vector<OutputAndEdges> edges;
215
217 std::vector<std::pair<std::string, storm::expressions::Expression>> rewardExpressions;
218
220 std::vector<storm::builder::RewardModelInformation> rewardModelInformation;
221
223 bool hasStateActionRewards;
224
226 bool evaluateRewardExpressionsAtEdges;
227
229 bool evaluateRewardExpressionsAtDestinations;
230
232 storm::jani::ArrayEliminatorData arrayEliminatorData;
233
235 TransientVariableInformation<ValueType> transientVariableInformation;
236};
237
238} // namespace generator
239} // namespace storm
storm::storage::FlatSet< uint_fast64_t > EdgeIndexSet
virtual ModelType getModelType() const override
static storm::jani::ModelFeatures getSupportedJaniFeatures()
Returns the jani features with which this builder can deal natively.
virtual std::shared_ptr< storm::storage::sparse::ChoiceOrigins > generateChoiceOrigins(std::vector< boost::any > &dataForChoiceOrigins) const override
virtual void addStateValuation(storm::storage::sparse::state_type const &currentStateIndex, storm::storage::sparse::StateValuationsBuilder &valuationsBuilder) const override
Adds the valuation for the currently loaded state to the given builder.
virtual StateBehavior< ValueType, StateType > expand(StateToIdCallback const &stateToIdCallback) override
virtual std::vector< StateType > getInitialStates(StateToIdCallback const &stateToIdCallback) override
JaniNextStateGenerator(storm::jani::Model const &model, NextStateGeneratorOptions const &options=NextStateGeneratorOptions())
virtual storm::builder::RewardModelInformation getRewardModelInformation(uint64_t const &index) const override
virtual bool isPartiallyObservable() const override
virtual std::size_t getNumberOfRewardModels() const override
virtual storm::storage::sparse::StateValuationsBuilder initializeStateValuationsBuilder() const override
Initializes a builder for state valuations by adding the appropriate variables.
static bool canHandle(storm::jani::Model const &model)
A quick check to detect whether the given model is not supported.
NextStateGenerator< ValueType, StateType >::StateToIdCallback StateToIdCallback
virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage< StateType > const &stateStorage, std::vector< StateType > const &initialStateIndices={}, std::vector< StateType > const &deadlockStateIndices={}, std::vector< StateType > const &unexploredStateIndices={}) override
virtual void unpackTransientVariableValuesIntoEvaluator(CompressedState const &state, storm::expressions::ExpressionEvaluator< ValueType > &evaluator) const override
Sets the values of all transient variables in the current state to the given evaluator.
std::unique_ptr< storm::expressions::ExpressionEvaluator< BaseValueType > > evaluator
An evaluator used to evaluate expressions.
std::function< StateType(CompressedState const &)> StateToIdCallback
CompressedState const * state
The currently loaded state.
NextStateGeneratorOptions options
The options to be used for next-state generation.
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
storm::storage::BitVector CompressedState
storm::builder::BuilderOptions NextStateGeneratorOptions
boost::container::flat_set< Key, std::less< Key >, boost::container::new_allocator< Key > > FlatSet
Redefinition of flat_set was needed, because from Boost 1.70 on the default allocator is set to void.
Definition BoostTypes.h:13
LabParser.cpp.