storm::transformer::GoalStateMerger< ValueType > Class Template Reference

#include <GoalStateMerger.h>

Classes
struct	ReturnType

Public Member Functions
	GoalStateMerger (storm::models::sparse::Model< ValueType > const &model)
ReturnType	mergeTargetAndSinkStates (storm::storage::BitVector const &maybeStates, storm::storage::BitVector const &targetStates, storm::storage::BitVector const &sinkStates, std::vector< std::string > const &selectedRewardModels=std::vector< std::string >(), std::optional< storm::storage::BitVector > const &choiceFilter=std::nullopt, std::optional< uint64_t > representativeTargetState=std::nullopt, std::optional< uint64_t > representativeSinkState=std::nullopt) const
	Computes a submodel of the specified model that only considers the states given by maybeStates as well as.
std::optional< ReturnType >	mergeForFormula (storm::logic::Formula const &formula, bool const dropUnreachableFromInit) const
	Identifies the maybeStates, targetStates, sinkStates (and, if applicable, the reward model and choice filter) that correspond to the given formula and invokes mergeTargetAndSinkStates accordingly.

Detailed Description

template<typename ValueType>
class storm::transformer::GoalStateMerger< ValueType >

Definition at line 29 of file GoalStateMerger.h.

Constructor & Destructor Documentation

GoalStateMerger()

template<typename ValueType>

storm::transformer::GoalStateMerger< ValueType >::GoalStateMerger

(

storm::models::sparse::Model< ValueType > const &

model

)

Exceptions

storm::exceptions::NotSupportedException

if the given model is not supported by this transformer.

Definition at line 69 of file GoalStateMerger.cpp.

Member Function Documentation

mergeForFormula()

template<typename ValueType>

std::optional< typename GoalStateMerger< ValueType >::ReturnType > storm::transformer::GoalStateMerger< ValueType >::mergeForFormula	(	storm::logic::Formula const &	formula,
		bool const	dropUnreachableFromInit ) const

Identifies the maybeStates, targetStates, sinkStates (and, if applicable, the reward model and choice filter) that correspond to the given formula and invokes mergeTargetAndSinkStates accordingly.

Parameters

dropUnreachableFromInit

if true, maybeStates that are not reachable from the initial states (without hopping over a target/sink state) are dropped. If false, this reachability analysis is skipped, i.e., the result is as if every state of the input model was an initial state.

Returns

the result of the corresponding call to mergeTargetAndSinkStates, or std::nullopt if the given formula is not supported (e.g. because it has non-propositional subformulas or is not one of the supported formula types).

Definition at line 143 of file GoalStateMerger.cpp.

mergeTargetAndSinkStates()

template<typename ValueType>

GoalStateMerger< ValueType >::ReturnType storm::transformer::GoalStateMerger< ValueType >::mergeTargetAndSinkStates	(	storm::storage::BitVector const &	maybeStates,
		storm::storage::BitVector const &	targetStates,
		storm::storage::BitVector const &	sinkStates,
		std::vector< std::string > const &	selectedRewardModels = std::vector<std::string>(),
		std::optional< storm::storage::BitVector > const &	choiceFilter = std::nullopt,
		std::optional< uint64_t >	representativeTargetState = std::nullopt,
		std::optional< uint64_t >	representativeSinkState = std::nullopt ) const

Computes a submodel of the specified model that only considers the states given by maybeStates as well as.

• one target state to which all transitions to a state selected by targetStates are redirected and
• one sink state to which all transitions to a state selected by sinkStates are redirected.

If a choiceFilter is given, choices on maybestates that are not selected by the filter will be removed.

Notes:

• the target (or sink) state is not created, if it is not reachable
• by default, the target (or sink) state will get a label iff it is reachable and at least one of the given targetStates (sinkStates) have that label. If a representative target (sink) state is given, this default behaviour is overridden: the target (sink) state will then get exactly the labels of the representative state instead. This assumes that the provided label names are already known labels of the input model.
• Only the selected reward models will be kept. The target and sink states will not get any reward.
• Choices that lead from a maybeState to a ~(maybeState | target | sink) state will be removed. An exception is thrown if this leads to deadlocks.
• It is assumed that maybeStates, targetStates, and sinkStates are pairwise disjoint. Otherwise, an exception is thrown.
• The order of the maybeStates will not be affected (i.e. s_1 < s_2 in the input model implies s'_1 < s'_2 in the output model).

Definition at line 76 of file GoalStateMerger.cpp.

---

The documentation for this class was generated from the following files:

• src/storm/transformer/GoalStateMerger.h
• src/storm/transformer/GoalStateMerger.cpp