|
| StaminaModelBuilder (std::shared_ptr< storm::generator::PrismNextStateGenerator< ValueType, StateType > > 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, RewardModelType > > | build () |
|
StateType | getStateIndexIfKnown (CompressedState const &state) |
|
double | accumulateProbabilities () |
|
void | reset () |
|
void | setGenerator (std::shared_ptr< storm::generator::PrismNextStateGenerator< ValueType, StateType > > generator) |
|
std::vector< StateType > | 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 StateType | getOrAddStateIndex (CompressedState const &state) |
|
StateType | getStateIndexOrAbsorbing (CompressedState const &state) |
|
double | getLocalKappa () |
|
|
storm::storage::sparse::StateStorage< StateType > | getStateStorage () |
|
void | loadPropertyExpressionFromFormula () |
|
void | connectTerminalStatesToAbsorbing (storm::storage::SparseMatrixBuilder< ValueType > &transitionMatrixBuilder, CompressedState &terminalState, StateType stateId, std::function< StateType(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 (StateType from, StateType to, ValueType probability) |
|
void | createTransition (TransitionInfo transitionInfo) |
|
virtual storm::storage::sparse::ModelComponents< ValueType, RewardModelType > | 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::shared_ptr< threads::ControlThread< StateType, RewardModelType, ValueType > > | controlThread |
|
std::vector< std::shared_ptr< threads::ExplorationThread< StateType, RewardModelType, ValueType > > > | explorationThreads |
|
std::function< StateType(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, StateType > > | generator |
|
util::StateMemoryPool< ProbabilityState< StateType > > | memoryPool |
|
std::deque< std::pair< ProbabilityState< StateType > *, CompressedState > > | statesToExplore |
|
util::StateIndexArray< StateType, ProbabilityState< StateType > > | stateMap |
|
storm::storage::sparse::StateStorage< StateType > & | 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< StateType > * | 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 |
|
◆ StaminaModelBuilder() [1/2]
template<typename ValueType , typename RewardModelType , typename StateType >
stamina::builder::StaminaModelBuilder< ValueType, RewardModelType, StateType >::StaminaModelBuilder |
( |
std::shared_ptr< storm::generator::PrismNextStateGenerator< ValueType, StateType > > const & |
generator, |
|
|
storm::prism::Program const & |
modulesFile, |
|
|
storm::generator::NextStateGeneratorOptions const & |
options |
|
) |
| |
Constructs a StaminaModelBuilder with a given storm::generator::PrismNextStateGenerator
- Parameters
-
generator | The generator we are going to use. |
◆ StaminaModelBuilder() [2/2]
template<typename ValueType , typename RewardModelType , typename StateType >
stamina::builder::StaminaModelBuilder< ValueType, RewardModelType, StateType >::StaminaModelBuilder |
( |
storm::prism::Program const & |
program, |
|
|
storm::generator::NextStateGeneratorOptions const & |
generatorOptions |
|
) |
| |
Constructs a StaminaModelBuilder with a PRISM program and generatorOptions
- Parameters
-
program | The PRISM program we are going to use to build the model with. |
generatorOptions | Options for the storm::generator::PrismNextStateGenerator we are going to use. |
◆ accumulateProbabilities()
template<typename ValueType , typename RewardModelType , typename StateType >
Accumulates all probabilities in T Map and returns
◆ build()
template<typename ValueType , typename RewardModelType , typename StateType >
Creates a model with a truncated state space for the program provided during construction. State space is truncated during this method using the STAMINA II truncation method described by Riley Roberts and Zhen Zhang, and corresponding to the same algorithm used in the Java version of STAMINA.
- Returns
- The truncated model.
◆ buildMatrices()
template<typename ValueType , typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename StateType = uint32_t>
virtual void stamina::builder::StaminaModelBuilder< 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 |
|
) |
| |
|
protectedpure virtual |
Builds transition matrix of truncated state space for the given program.
- Parameters
-
transitionMatrixBuilder | The builder of the transition matrix. |
rewardModelBuilders | The builders for the selected reward models. |
choiceInformationBuilder | The builder for the requested information of the choices |
markovianChoices | is set to a bit vector storing whether a choice is Markovian (is only set if the model type requires this information). |
stateValuationsBuilder | if not boost::none, we insert valuations for the corresponding states |
Implemented in stamina::builder::StaminaIterativeModelBuilder< ValueType, RewardModelType, StateType >, stamina::builder::StaminaIterativeModelBuilder< ValueType, storm::models::sparse::StandardRewardModel< ValueType >, uint32_t >, stamina::builder::StaminaPriorityModelBuilder< ValueType, RewardModelType, StateType >, stamina::builder::StaminaPriorityModelBuilder< ValueType, storm::models::sparse::StandardRewardModel< ValueType >, uint32_t >, stamina::builder::StaminaReExploringModelBuilder< ValueType, RewardModelType, StateType >, stamina::builder::StaminaThreadedIterativeModelBuilder< ValueType, RewardModelType, StateType >, and stamina::builder::StaminaThreadedPriorityModelBuilder< ValueType, RewardModelType, StateType >.
◆ buildModelComponents()
template<typename ValueType , typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename StateType = uint32_t>
Explores state space and truncates the model
- Returns
- The components of the truncated model
Implemented in stamina::builder::StaminaIterativeModelBuilder< ValueType, RewardModelType, StateType >, stamina::builder::StaminaIterativeModelBuilder< ValueType, storm::models::sparse::StandardRewardModel< ValueType >, uint32_t >, stamina::builder::StaminaPriorityModelBuilder< ValueType, RewardModelType, StateType >, stamina::builder::StaminaPriorityModelBuilder< ValueType, storm::models::sparse::StandardRewardModel< ValueType >, uint32_t >, and stamina::builder::StaminaReExploringModelBuilder< ValueType, RewardModelType, StateType >.
◆ buildStateLabeling()
template<typename ValueType , typename RewardModelType , typename StateType >
Builds state labeling for our program
- Returns
- State labeling for our program
◆ connectTerminalStatesToAbsorbing()
template<typename ValueType , typename RewardModelType , typename StateType >
void stamina::builder::StaminaModelBuilder< ValueType, RewardModelType, StateType >::connectTerminalStatesToAbsorbing |
( |
storm::storage::SparseMatrixBuilder< ValueType > & |
transitionMatrixBuilder, |
|
|
CompressedState & |
terminalState, |
|
|
StateType |
stateId, |
|
|
std::function< StateType(CompressedState const &)> |
stateToIdCallback |
|
) |
| |
|
protected |
Connects all terminal states to the absorbing state
◆ createTransition()
template<typename ValueType , typename RewardModelType , typename StateType >
Inserts a TransitionInfo into transitionsToAdd. This method must NOT be called after flushToTransitionMatrix has cleared transitionsToAdd
◆ flushToTransitionMatrix()
template<typename ValueType , typename RewardModelType , typename StateType >
void stamina::builder::StaminaModelBuilder< ValueType, RewardModelType, StateType >::flushToTransitionMatrix |
( |
storm::storage::SparseMatrixBuilder< ValueType > & |
transitionMatrixBuilder | ) |
|
|
protected |
Flushes the elements in transitionsToAdd into the transition matrix
- Parameters
-
transitionMatrixBuilder | The transition matrix builder |
◆ getOrAddStateIndex()
template<typename ValueType , typename RewardModelType , typename StateType >
Gets the state ID of a current state, or adds it to the internal state storage. Performs state exploration and state space truncation from that state.
- Parameters
-
state | Pointer to the state we are looking it |
- Returns
- A pair with the state id and whether or not it was already discovered
Reimplemented in stamina::builder::StaminaIterativeModelBuilder< ValueType, RewardModelType, StateType >, stamina::builder::StaminaIterativeModelBuilder< ValueType, storm::models::sparse::StandardRewardModel< ValueType >, uint32_t >, stamina::builder::StaminaPriorityModelBuilder< ValueType, RewardModelType, StateType >, stamina::builder::StaminaPriorityModelBuilder< ValueType, storm::models::sparse::StandardRewardModel< ValueType >, uint32_t >, and stamina::builder::StaminaReExploringModelBuilder< ValueType, RewardModelType, StateType >.
◆ getPerimeterStates()
template<typename ValueType , typename RewardModelType , typename StateType >
Creates and returns a vector of all perimeter states
- Returns
- a vector of all perimeter states
◆ getStateIndexIfKnown()
template<typename ValueType , typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename StateType = uint32_t>
Gets the state ID of a state known to already exist. This does NOT perform state-space truncation for future states
◆ getStateIndexOrAbsorbing()
template<typename ValueType , typename RewardModelType , typename StateType >
Alterate state ID grabber. Returns state ID if exists. If it does not, returns the absorbing state This is used as an alternative callback function for terminal (perimeter) states
◆ loadPropertyExpressionFromFormula()
template<typename ValueType , typename RewardModelType , typename StateType >
Creates and loads the property expression from the formula
◆ reset()
template<typename ValueType , typename RewardModelType , typename StateType >
Resets stuff to "fresh" state.
◆ setGenerator()
template<typename ValueType , typename RewardModelType , typename StateType >
void stamina::builder::StaminaModelBuilder< ValueType, RewardModelType, StateType >::setGenerator |
( |
std::shared_ptr< storm::generator::PrismNextStateGenerator< ValueType, StateType > > |
generator | ) |
|
Sets the generator while deleting the old one
- Parameters
-
generator | The new generator |
◆ setLocalKappaToGlobal()
template<typename ValueType , typename RewardModelType , typename StateType >
Sets the value of κ in Options to what we have stored locally here
◆ setPropertyFormula()
template<typename ValueType , typename RewardModelType , typename StateType >
void stamina::builder::StaminaModelBuilder< ValueType, RewardModelType, StateType >::setPropertyFormula |
( |
std::shared_ptr< const storm::logic::Formula > |
formula, |
|
|
const storm::prism::Program & |
modulesFile |
|
) |
| |
Sets the property formula for state space truncation optimization. Does not load or create an expression from the formula.
- Parameters
-
formula | The formula to set |
modulesFile | The modules file which contains the expressionmanager |
◆ setUpAbsorbingState()
template<typename ValueType , typename RewardModelType , typename StateType >
void stamina::builder::StaminaModelBuilder< ValueType, RewardModelType, StateType >::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 |
|
) |
| |
|
protected |
Sets up the initial state in the transition matrix
The documentation for this class was generated from the following files:
- /home/josh/Documents/Work/stamina-cplusplus/src/stamina/builder/StaminaModelBuilder.h
- /home/josh/Documents/Work/stamina-cplusplus/src/stamina/builder/StaminaModelBuilder.cpp