|
| StaminaIterativeModelBuilder (std::shared_ptr< storm::generator::PrismNextStateGenerator< ValueType, StateType > > const &generator, storm::prism::Program const &modulesFile, storm::generator::NextStateGeneratorOptions const &options) |
|
| StaminaIterativeModelBuilder (storm::prism::Program const &program, storm::generator::NextStateGeneratorOptions const &generatorOptions=storm::generator::NextStateGeneratorOptions()) |
|
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 |
|
StateType | getOrAddStateIndex (CompressedState const &state) override |
|
storm::storage::sparse::ModelComponents< ValueType, RewardModelType > | buildModelComponents () override |
|
| StaminaModelBuilder (std::shared_ptr< storm::generator::PrismNextStateGenerator< ValueType, uint32_t > > const &generator, storm::prism::Program const &modulesFile, storm::generator::NextStateGeneratorOptions const &options) |
|
| StaminaModelBuilder (storm::prism::Program const &program, storm::generator::NextStateGeneratorOptions const &generatorOptions) |
|
std::shared_ptr< storm::models::sparse::Model< ValueType, storm::models::sparse::StandardRewardModel< ValueType > > > | build () |
|
uint32_t | getStateIndexIfKnown (CompressedState const &state) |
|
double | accumulateProbabilities () |
|
void | reset () |
|
void | setGenerator (std::shared_ptr< storm::generator::PrismNextStateGenerator< ValueType, uint32_t > > generator) |
|
std::vector< uint32_t > | getPerimeterStates () |
|
void | setLocalKappaToGlobal () |
|
void | printStateSpaceInformation () |
|
storm::expressions::Expression * | getPropertyExpression () |
|
void | setPropertyFormula (std::shared_ptr< const storm::logic::Formula > formula, const storm::prism::Program &modulesFile) |
|
virtual uint32_t | getOrAddStateIndex (CompressedState const &state) |
|
uint32_t | getStateIndexOrAbsorbing (CompressedState const &state) |
|
double | getLocalKappa () |
|
|
void | flushStatesTerminated () |
|
void | connectAllTerminalStatesToAbsorbing (storm::storage::SparseMatrixBuilder< ValueType > &transitionMatrixBuilder) |
|
storm::storage::sparse::StateStorage< uint32_t > | getStateStorage () |
|
void | loadPropertyExpressionFromFormula () |
|
void | connectTerminalStatesToAbsorbing (storm::storage::SparseMatrixBuilder< ValueType > &transitionMatrixBuilder, CompressedState &terminalState, uint32_t stateId, std::function< uint32_t(CompressedState const &)> stateToIdCallback) |
|
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)=0 |
|
void | flushToTransitionMatrix (storm::storage::SparseMatrixBuilder< ValueType > &transitionMatrixBuilder) |
|
void | createTransition (uint32_t from, uint32_t to, ValueType probability) |
|
void | createTransition (TransitionInfo transitionInfo) |
|
virtual storm::storage::sparse::ModelComponents< ValueType, storm::models::sparse::StandardRewardModel< ValueType > > | buildModelComponents ()=0 |
|
storm::models::sparse::StateLabeling | buildStateLabeling () |
|
void | setUpAbsorbingState (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) |
|
|
std::deque< std::pair< ProbabilityState< StateType > *, CompressedState > > | statesTerminatedLastIteration |
|
uint64_t | numberOfExploredStates |
|
uint64_t | numberOfExploredStatesSinceLastMessage |
|
std::shared_ptr< threads::ControlThread< uint32_t, storm::models::sparse::StandardRewardModel< ValueType >, ValueType > > | controlThread |
|
std::vector< std::shared_ptr< threads::ExplorationThread< uint32_t, storm::models::sparse::StandardRewardModel< ValueType >, ValueType > > > | explorationThreads |
|
std::function< uint32_t(CompressedState const &)> | terminalStateToIdCallback |
|
storm::expressions::Expression * | propertyExpression |
|
storm::expressions::ExpressionManager * | expressionManager |
|
std::shared_ptr< const storm::logic::Formula > | propertyFormula |
|
std::shared_ptr< storm::generator::PrismNextStateGenerator< ValueType, uint32_t > > | generator |
|
util::StateMemoryPool< ProbabilityState< uint32_t > > | memoryPool |
|
std::deque< std::pair< ProbabilityState< uint32_t > *, CompressedState > > | statesToExplore |
|
util::StateIndexArray< uint32_t, ProbabilityState< uint32_t > > | stateMap |
|
storm::storage::sparse::StateStorage< uint32_t > & | stateStorage |
|
boost::optional< std::vector< uint_fast64_t > > | stateRemapping |
|
std::vector< std::vector< TransitionInfo > > | transitionsToAdd |
|
storm::generator::NextStateGeneratorOptions const & | options |
|
storm::prism::Program const & | modulesFile |
|
ProbabilityState< uint32_t > * | currentProbabilityState |
|
CompressedState | absorbingState |
|
bool | absorbingWasSetUp |
|
bool | isInit |
|
bool | fresh |
|
uint8_t | iteration |
|
bool | firstIteration |
|
double | localKappa |
|
bool | isCtmc |
|
bool | formulaMatchesExpression |
|
uint64_t | numberTerminal |
|
uint64_t | numberStates |
|
uint64_t | numberTransitions |
|
uint_fast64_t | currentRowGroup |
|
uint_fast64_t | currentRow |
|
template<typename ValueType , typename RewardModelType , typename StateType >
void stamina::builder::StaminaIterativeModelBuilder< ValueType, RewardModelType, StateType >::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 |
|
) |
| |
|
overridevirtual |