Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Namespaces | Classes | Enumerations | Functions
storm::transformer Namespace Reference

Namespaces

namespace  detail
 

Classes

class  AddUncertainty
 This class is a convenience transformer to add uncertainty. More...
 
class  ApplyFiniteSchedulerToPomdp
 
class  BinaryDtmcTransformer
 
class  BinaryPomdpTransformer
 
struct  BinaryPomdpTransformerRowGroup
 
struct  BinaryPomdpTransformerRowGroupCompare
 
class  ChoiceSelector
 
class  ContinuousToDiscreteTimeModelTransformer
 
class  DAProduct
 
class  DAProductBuilder
 
class  EndComponentEliminator
 
class  GlobalPomdpMecChoiceEliminator
 
class  GlobalPOMDPSelfLoopEliminator
 
class  GoalStateMerger
 
struct  LabelInformation
 
class  MakePOMDPCanonic
 
class  MakeStateSetObservationClosed
 
class  MemoryIncorporation
 Incorporates Memory into the state space of the given model, that is the resulting model is the crossproduct of of the given model plus some type of memory structure. More...
 
class  NonMarkovianChainTransformer
 Transformer for eliminating chains of non-Markovian states (instantaneous path fragment leading to the same outcome) from Markov automata. More...
 
class  ParameterLifter
 This class lifts parameter choices to nondeterminism: For each row in the given matrix that considerd #par parameters, the resulting matrix will have one row group consisting of 2^#par rows. More...
 
class  PomdpMemoryUnfolder
 
struct  PomdpTransformationResult
 
class  Product
 
class  ProductBuilder
 
struct  RationalFunctionConstructor
 
class  SparseParametricDtmcSimplifier
 This class performs different steps to simplify the given (parametric) model. More...
 
class  SparseParametricMdpSimplifier
 This class performs different steps to simplify the given (parametric) model. More...
 
class  SparseParametricModelSimplifier
 This class performs different steps to simplify the given (parametric) model. More...
 
struct  StateWithRow
 
struct  SubsystemBuilderOptions
 
struct  SubsystemBuilderReturnType
 
class  SymbolicCtmcToSparseCtmcTransformer
 
class  SymbolicDtmcToSparseDtmcTransformer
 
class  SymbolicMaToSparseMaTransformer
 
class  SymbolicMdpToSparseMdpTransformer
 
class  TimeTravelling
 

Enumerations

enum class  PomdpFscApplicationMode {
  STANDARD , SIMPLE_LINEAR , SIMPLE_LINEAR_INVERSE , SIMPLE_LOG ,
  FULL
}
 
enum  EliminationLabelBehavior { KeepLabels , ExtendLabels , MergeLabels , DeleteLabels }
 Specify criteria whether a state can be eliminated and how its labels should be treated. More...
 

Functions

bool labelsIntersectedEqual (const std::set< std::string > &labels1, const std::set< std::string > &labels2, const std::set< std::string > &intersection)
 
PomdpFscApplicationMode parsePomdpFscApplicationMode (std::string const &mode)
 
template<typename ValueType >
std::shared_ptr< RawPolynomialCache > getCache (storm::models::sparse::Pomdp< ValueType > const &)
 
template<>
std::shared_ptr< RawPolynomialCache > getCache (storm::models::sparse::Pomdp< storm::RationalFunction > const &model)
 
template<class SparseModelType >
storm::storage::MemoryStructure getGoalMemory (SparseModelType const &model, storm::logic::Formula const &propositionalGoalStateFormula)
 
template<class SparseModelType >
storm::storage::MemoryStructure getUntilFormulaMemory (SparseModelType const &model, storm::logic::Formula const &leftSubFormula, storm::logic::Formula const &rightSubFormula)
 
template<typename ValueType >
std::shared_ptr< storm::models::sparse::Model< ValueType > > permuteStates (storm::models::sparse::Model< ValueType > const &originalModel, std::vector< uint64_t > const &permutation)
 Applies the given permutation to the states of the given model.
 
template std::shared_ptr< storm::models::sparse::Model< double > > permuteStates (storm::models::sparse::Model< double > const &originalModel, std::vector< uint64_t > const &permutation)
 
template std::shared_ptr< storm::models::sparse::Model< storm::RationalNumber > > permuteStates (storm::models::sparse::Model< storm::RationalNumber > const &originalModel, std::vector< uint64_t > const &permutation)
 
template std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > > permuteStates (storm::models::sparse::Model< storm::RationalFunction > const &originalModel, std::vector< uint64_t > const &permutation)
 
template<typename ValueType , typename RewardModelType >
void transformModelSpecificComponents (storm::models::sparse::Model< ValueType, RewardModelType > const &originalModel, storm::storage::BitVector const &subsystem, storm::storage::sparse::ModelComponents< ValueType, RewardModelType > &components)
 
template<typename RewardModelType >
RewardModelType transformRewardModel (RewardModelType const &originalRewardModel, storm::storage::BitVector const &subsystem, storm::storage::BitVector const &subsystemActions, bool makeRowGroupingTrivial)
 
template<typename ValueType , typename RewardModelType >
SubsystemBuilderReturnType< ValueType, RewardModelType > internalBuildSubsystem (storm::models::sparse::Model< ValueType, RewardModelType > const &originalModel, storm::storage::BitVector const &subsystemStates, storm::storage::BitVector const &subsystemActions, SubsystemBuilderOptions const &options)
 
template<typename ValueType , typename RewardModelType >
SubsystemBuilderReturnType< ValueType, RewardModelType > buildSubsystem (storm::models::sparse::Model< ValueType, RewardModelType > const &originalModel, storm::storage::BitVector const &subsystemStates, storm::storage::BitVector const &subsystemActions, bool keepUnreachableStates, SubsystemBuilderOptions options)
 
template SubsystemBuilderReturnType< double > buildSubsystem (storm::models::sparse::Model< double > const &originalModel, storm::storage::BitVector const &subsystemStates, storm::storage::BitVector const &subsystemActions, bool keepUnreachableStates=true, SubsystemBuilderOptions options=SubsystemBuilderOptions())
 
template SubsystemBuilderReturnType< double, storm::models::sparse::StandardRewardModel< storm::Interval > > buildSubsystem (storm::models::sparse::Model< double, storm::models::sparse::StandardRewardModel< storm::Interval > > const &originalModel, storm::storage::BitVector const &subsystemStates, storm::storage::BitVector const &subsystemActions, bool keepUnreachableStates=true, SubsystemBuilderOptions options=SubsystemBuilderOptions())
 
template SubsystemBuilderReturnType< storm::RationalNumber > buildSubsystem (storm::models::sparse::Model< storm::RationalNumber > const &originalModel, storm::storage::BitVector const &subsystemStates, storm::storage::BitVector const &subsystemActions, bool keepUnreachableStates=true, SubsystemBuilderOptions options=SubsystemBuilderOptions())
 
template SubsystemBuilderReturnType< storm::RationalFunction > buildSubsystem (storm::models::sparse::Model< storm::RationalFunction > const &originalModel, storm::storage::BitVector const &subsystemStates, storm::storage::BitVector const &subsystemActions, bool keepUnreachableStates=true, SubsystemBuilderOptions options=SubsystemBuilderOptions())
 
template SubsystemBuilderReturnType< storm::Interval > buildSubsystem (storm::models::sparse::Model< storm::Interval > const &originalModel, storm::storage::BitVector const &subsystemStates, storm::storage::BitVector const &subsystemActions, bool keepUnreachableStates=true, SubsystemBuilderOptions options=SubsystemBuilderOptions())
 

Enumeration Type Documentation

◆ EliminationLabelBehavior

enum storm::transformer::EliminationLabelBehavior

Specify criteria whether a state can be eliminated and how its labels should be treated.

  • KeepLabels: only eliminate if the labels of the state and the successors are the same.
  • ExtendLabels: only eliminate if the labels of the state are a subset of the labels of the successors.
  • MergeLabels: eliminate state and add labels of state to labels of the successors.
  • DeleteLabels: eliminate state and do not add its labels to the successors (except "init" label).
Enumerator
KeepLabels 
ExtendLabels 
MergeLabels 
DeleteLabels 

Definition at line 14 of file NonMarkovianChainTransformer.h.

◆ PomdpFscApplicationMode

enum class storm::transformer::PomdpFscApplicationMode
strong
Enumerator
STANDARD 
SIMPLE_LINEAR 
SIMPLE_LINEAR_INVERSE 
SIMPLE_LOG 
FULL 

Definition at line 11 of file ApplyFiniteSchedulerToPomdp.h.

Function Documentation

◆ buildSubsystem() [1/6]

template SubsystemBuilderReturnType< double > storm::transformer::buildSubsystem ( storm::models::sparse::Model< double > const &  originalModel,
storm::storage::BitVector const &  subsystemStates,
storm::storage::BitVector const &  subsystemActions,
bool  keepUnreachableStates = true,
SubsystemBuilderOptions  options = SubsystemBuilderOptions() 
)

◆ buildSubsystem() [2/6]

template SubsystemBuilderReturnType< double, storm::models::sparse::StandardRewardModel< storm::Interval > > storm::transformer::buildSubsystem ( storm::models::sparse::Model< double, storm::models::sparse::StandardRewardModel< storm::Interval > > const &  originalModel,
storm::storage::BitVector const &  subsystemStates,
storm::storage::BitVector const &  subsystemActions,
bool  keepUnreachableStates = true,
SubsystemBuilderOptions  options = SubsystemBuilderOptions() 
)

◆ buildSubsystem() [3/6]

template SubsystemBuilderReturnType< storm::Interval > storm::transformer::buildSubsystem ( storm::models::sparse::Model< storm::Interval > const &  originalModel,
storm::storage::BitVector const &  subsystemStates,
storm::storage::BitVector const &  subsystemActions,
bool  keepUnreachableStates = true,
SubsystemBuilderOptions  options = SubsystemBuilderOptions() 
)

◆ buildSubsystem() [4/6]

template SubsystemBuilderReturnType< storm::RationalFunction > storm::transformer::buildSubsystem ( storm::models::sparse::Model< storm::RationalFunction > const &  originalModel,
storm::storage::BitVector const &  subsystemStates,
storm::storage::BitVector const &  subsystemActions,
bool  keepUnreachableStates = true,
SubsystemBuilderOptions  options = SubsystemBuilderOptions() 
)

◆ buildSubsystem() [5/6]

template SubsystemBuilderReturnType< storm::RationalNumber > storm::transformer::buildSubsystem ( storm::models::sparse::Model< storm::RationalNumber > const &  originalModel,
storm::storage::BitVector const &  subsystemStates,
storm::storage::BitVector const &  subsystemActions,
bool  keepUnreachableStates = true,
SubsystemBuilderOptions  options = SubsystemBuilderOptions() 
)

◆ buildSubsystem() [6/6]

template<typename ValueType , typename RewardModelType >
SubsystemBuilderReturnType< ValueType, RewardModelType > storm::transformer::buildSubsystem ( storm::models::sparse::Model< ValueType, RewardModelType > const &  originalModel,
storm::storage::BitVector const &  subsystemStates,
storm::storage::BitVector const &  subsystemActions,
bool  keepUnreachableStates,
SubsystemBuilderOptions  options 
)

Definition at line 207 of file SubsystemBuilder.cpp.

◆ getCache() [1/2]

template<>
std::shared_ptr< RawPolynomialCache > storm::transformer::getCache ( storm::models::sparse::Pomdp< storm::RationalFunction > const &  model)

Definition at line 39 of file ApplyFiniteSchedulerToPomdp.cpp.

◆ getCache() [2/2]

template<typename ValueType >
std::shared_ptr< RawPolynomialCache > storm::transformer::getCache ( storm::models::sparse::Pomdp< ValueType > const &  )

Definition at line 34 of file ApplyFiniteSchedulerToPomdp.cpp.

◆ getGoalMemory()

template<class SparseModelType >
storm::storage::MemoryStructure storm::transformer::getGoalMemory ( SparseModelType const &  model,
storm::logic::Formula const &  propositionalGoalStateFormula 
)

Definition at line 24 of file MemoryIncorporation.cpp.

◆ getUntilFormulaMemory()

template<class SparseModelType >
storm::storage::MemoryStructure storm::transformer::getUntilFormulaMemory ( SparseModelType const &  model,
storm::logic::Formula const &  leftSubFormula,
storm::logic::Formula const &  rightSubFormula 
)

Definition at line 50 of file MemoryIncorporation.cpp.

◆ internalBuildSubsystem()

template<typename ValueType , typename RewardModelType >
SubsystemBuilderReturnType< ValueType, RewardModelType > storm::transformer::internalBuildSubsystem ( storm::models::sparse::Model< ValueType, RewardModelType > const &  originalModel,
storm::storage::BitVector const &  subsystemStates,
storm::storage::BitVector const &  subsystemActions,
SubsystemBuilderOptions const &  options 
)

Definition at line 69 of file SubsystemBuilder.cpp.

◆ labelsIntersectedEqual()

bool storm::transformer::labelsIntersectedEqual ( const std::set< std::string > &  labels1,
const std::set< std::string > &  labels2,
const std::set< std::string > &  intersection 
)

Definition at line 423 of file TimeTravelling.cpp.

◆ parsePomdpFscApplicationMode()

PomdpFscApplicationMode storm::transformer::parsePomdpFscApplicationMode ( std::string const &  mode)

Definition at line 10 of file ApplyFiniteSchedulerToPomdp.cpp.

◆ permuteStates() [1/4]

template std::shared_ptr< storm::models::sparse::Model< double > > storm::transformer::permuteStates ( storm::models::sparse::Model< double > const &  originalModel,
std::vector< uint64_t > const &  permutation 
)

◆ permuteStates() [2/4]

template std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > > storm::transformer::permuteStates ( storm::models::sparse::Model< storm::RationalFunction > const &  originalModel,
std::vector< uint64_t > const &  permutation 
)

◆ permuteStates() [3/4]

template std::shared_ptr< storm::models::sparse::Model< storm::RationalNumber > > storm::transformer::permuteStates ( storm::models::sparse::Model< storm::RationalNumber > const &  originalModel,
std::vector< uint64_t > const &  permutation 
)

◆ permuteStates() [4/4]

template<typename ValueType >
std::shared_ptr< storm::models::sparse::Model< ValueType > > storm::transformer::permuteStates ( storm::models::sparse::Model< ValueType > const &  originalModel,
std::vector< uint64_t > const &  permutation 
)

Applies the given permutation to the states of the given model.

The permutation must be a permutation of the numbers 0, 1, ..., n-1 for n = model.getNumberOfStates(). The state at position i of the input model will be moved to position permutation[i] in the output model.

Template Parameters
ValueType
Parameters
originalModel
permutation
Returns

Definition at line 23 of file StatePermuter.cpp.

◆ transformModelSpecificComponents()

template<typename ValueType , typename RewardModelType >
void storm::transformer::transformModelSpecificComponents ( storm::models::sparse::Model< ValueType, RewardModelType > const &  originalModel,
storm::storage::BitVector const &  subsystem,
storm::storage::sparse::ModelComponents< ValueType, RewardModelType > &  components 
)

Definition at line 28 of file SubsystemBuilder.cpp.

◆ transformRewardModel()

template<typename RewardModelType >
RewardModelType storm::transformer::transformRewardModel ( RewardModelType const &  originalRewardModel,
storm::storage::BitVector const &  subsystem,
storm::storage::BitVector const &  subsystemActions,
bool  makeRowGroupingTrivial 
)

Definition at line 47 of file SubsystemBuilder.cpp.