24 static_assert(!storm::IsIntervalType<ValueType>,
"JaniNextStateGenerator does not support interval types.");
62 std::vector<StateType>
const& initialStateIndices = {},
63 std::vector<StateType>
const& deadlockStateIndices = {},
64 std::vector<StateType>
const& unexploredStateIndices = {})
override;
66 virtual std::shared_ptr<storm::storage::sparse::ChoiceOrigins>
generateChoiceOrigins(std::vector<boost::any>& dataForChoiceOrigins)
const override;
83 uint64_t getLocation(
CompressedState const&
state, LocationVariableInformation
const& locationVariable)
const;
88 void setLocation(
CompressedState&
state, LocationVariableInformation
const& locationVariable, uint64_t locationIndex)
const;
142 TransientVariableValuation<ValueType> getTransientVariableValuationAtLocations(std::vector<uint64_t>
const& locations,
159 Choice<ValueType> expandNonSynchronizingEdge(
storm::jani::Edge const& edge, uint64_t outputActionIndex, uint64_t automatonIndex,
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;
167 typedef std::pair<uint64_t, EdgeSetWithIndices> AutomatonAndEdgeSet;
168 typedef std::vector<AutomatonAndEdgeSet> AutomataEdgeSets;
170 void expandSynchronizingEdgeCombination(AutomataEdgeSets
const& edgeCombination, uint64_t outputActionIndex,
CompressedState const&
state,
171 StateToIdCallback stateToIdCallback, std::vector<Choice<ValueType>>& newChoices);
173 std::vector<EdgeSetWithIndices::const_iterator>
const& iteratorList,
180 void checkGlobalVariableWritesValid(AutomataEdgeSets
const& enabledEdges)
const;
185 std::vector<ValueType> evaluateRewardExpressions()
const;
190 void addEvaluatedRewardExpressions(std::vector<ValueType>& rewards, ValueType
const& factor)
const;
195 void buildRewardModelInformation();
200 void createSynchronizationInformation();
205 void checkValid()
const;
211 std::vector<std::reference_wrapper<storm::jani::Automaton const>> parallelAutomata;
214 std::vector<OutputAndEdges> edges;
217 std::vector<std::pair<std::string, storm::expressions::Expression>> rewardExpressions;
220 std::vector<storm::builder::RewardModelInformation> rewardModelInformation;
223 bool hasStateActionRewards;
226 bool evaluateRewardExpressionsAtEdges;
229 bool evaluateRewardExpressionsAtDestinations;
235 TransientVariableInformation<ValueType> transientVariableInformation;
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
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.