1#ifndef STAMINA_BUILDER_ITERATIVEMODELBUILDER_H
2#define STAMINA_BUILDER_ITERATIVEMODELBUILDER_H
10#include "StaminaModelBuilder.h"
14 template<
typename ValueType,
typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>,
typename StateType = u
int32_t>
23 std::shared_ptr<storm::generator::PrismNextStateGenerator<ValueType, StateType>>
const& generator
24 , storm::prism::Program
const& modulesFile
25 , storm::generator::NextStateGeneratorOptions
const & options
34 storm::prism::Program
const& program
35 , storm::generator::NextStateGeneratorOptions
const& generatorOptions = storm::generator::NextStateGeneratorOptions()
47 storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder
48 , std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders
49 , StateAndChoiceInformationBuilder& choiceInformationBuilder
50 , boost::optional<storm::storage::BitVector>& markovianChoices
51 , boost::optional<storm::storage::sparse::StateValuationsBuilder>& stateValuationsBuilder
66 storm::storage::sparse::ModelComponents<ValueType, RewardModelType>
buildModelComponents()
override;
109 std::deque<std::pair<ProbabilityState<StateType> *, CompressedState>> statesTerminatedLastIteration;
110 uint64_t numberOfExploredStates;
111 uint64_t numberOfExploredStatesSinceLastMessage;
114 template<
typename ValueType,
typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>,
typename StateType = u
int32_t>
Definition: StaminaIterativeModelBuilder.h:15
virtual void buildMatrices(storm::storage::SparseMatrixBuilder< ValueType > &transitionMatrixBuilder, std::vector< RewardModelBuilder< typename RewardModelType::ValueType > > &rewardModelBuilders, StateAndChoiceInformationBuilder &choiceInformationBuilder, boost::optional< storm::storage::BitVector > &markovianChoices, boost::optional< storm::storage::sparse::StateValuationsBuilder > &stateValuationsBuilder) override
Definition: StaminaIterativeModelBuilder.cpp:40
void connectAllTerminalStatesToAbsorbing(storm::storage::SparseMatrixBuilder< ValueType > &transitionMatrixBuilder)
Definition: StaminaIterativeModelBuilder.cpp:467
StateType getOrAddStateIndex(CompressedState const &state) override
Definition: StaminaIterativeModelBuilder.cpp:269
StaminaIterativeModelBuilder(std::shared_ptr< storm::generator::PrismNextStateGenerator< ValueType, StateType > > const &generator, storm::prism::Program const &modulesFile, storm::generator::NextStateGeneratorOptions const &options)
Definition: StaminaIterativeModelBuilder.cpp:11
storm::storage::sparse::ModelComponents< ValueType, RewardModelType > buildModelComponents() override
Definition: StaminaIterativeModelBuilder.cpp:361
void flushStatesTerminated()
Definition: StaminaIterativeModelBuilder.cpp:456
Definition: StaminaModelBuilder.h:61
Definition: ExplicitTruncatedModelBuilder.cpp:40