Storm 1.13.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
storm::gbar::abstraction Namespace Reference

Namespaces

namespace  jani
namespace  prism

Classes

struct  AbstractionInformationOptions
class  AbstractionInformation
struct  BottomStateResult
class  ExplicitQualitativeGameResult
class  ExplicitQualitativeGameResultMinMax
class  ExplicitQualitativeResult
class  ExplicitQualitativeResultMinMax
class  ExplicitQuantitativeResult
class  ExplicitQuantitativeResultMinMax
class  ExpressionTranslator
struct  GameBddResult
class  LocalExpressionInformation
class  MenuGame
 This class represents a discrete-time stochastic two-player game. More...
struct  MenuGameAbstractorOptions
class  MenuGameAbstractor
struct  PivotStateCandidatesResult
struct  ExplicitDijkstraQueueElement
struct  ExplicitDijkstraQueueElementLess
struct  VariableSetHash
class  RefinementPredicates
struct  SymbolicMostProbablePathsResult
struct  SymbolicPivotStateResult
struct  ExplicitPivotStateResult
struct  MenuGameRefinerOptions
class  MenuGameRefiner
class  SymbolicQualitativeResult
class  QualitativeResult
class  SymbolicQualitativeResultMinMax
class  QualitativeResultMinMax
class  RefinementCommand
class  SymbolicStateSet
class  StateSet
class  StateSetAbstractor
class  SymbolicQualitativeGameResult
class  SymbolicQualitativeGameResultMinMax
class  SymbolicQualitativeMdpResult
class  SymbolicQualitativeMdpResultMinMax
class  SymbolicQuantitativeGameResult
class  SymbolicQuantitativeGameResultMinMax
class  ValidBlockAbstractor
class  AbstractionSettings
 This class represents the settings for the abstraction procedures. More...

Functions

template<storm::dd::DdType DdType>
std::ostream & operator<< (std::ostream &out, LocalExpressionInformation< DdType > const &partition)
template std::ostream & operator<< (std::ostream &out, LocalExpressionInformation< storm::dd::DdType::CUDD > const &partition)
template std::ostream & operator<< (std::ostream &out, LocalExpressionInformation< storm::dd::DdType::Sylvan > const &partition)
template<typename ValueType>
std::string getStateName (std::pair< storm::expressions::SimpleValuation, ValueType > const &stateValue, std::set< storm::expressions::Variable > const &locationVariables, std::set< storm::expressions::Variable > const &predicateVariables, storm::expressions::Variable const &bottomVariable)
template<storm::dd::DdType Type, typename ValueType>
SymbolicMostProbablePathsResult< Type, ValueType > getMostProbablePathSpanningTree (storm::gbar::abstraction::MenuGame< Type, ValueType > const &game, storm::dd::Bdd< Type > const &transitionFilter)
template<storm::dd::DdType Type, typename ValueType>
SymbolicPivotStateResult< Type, ValueType > pickPivotState (AbstractionSettings::PivotSelectionHeuristic const &heuristic, storm::gbar::abstraction::MenuGame< Type, ValueType > const &game, PivotStateCandidatesResult< Type > const &pivotStateCandidateResult, boost::optional< SymbolicQualitativeGameResultMinMax< Type > > const &qualitativeResult, boost::optional< SymbolicQuantitativeGameResultMinMax< Type, ValueType > > const &quantitativeResult)
template<storm::dd::DdType Type, typename ValueType>
PivotStateCandidatesResult< Type > computePivotStates (storm::gbar::abstraction::MenuGame< Type, ValueType > const &game, storm::dd::Bdd< Type > const &transitionMatrixBdd, storm::dd::Bdd< Type > const &minPlayer1Strategy, storm::dd::Bdd< Type > const &minPlayer2Strategy, storm::dd::Bdd< Type > const &maxPlayer1Strategy, storm::dd::Bdd< Type > const &maxPlayer2Strategy)
template<typename ValueType>
void performDijkstraStep (std::set< ExplicitDijkstraQueueElement< ValueType >, ExplicitDijkstraQueueElementLess< ValueType > > &dijkstraQueue, bool probabilityDistances, std::vector< ValueType > &distances, std::vector< std::pair< uint64_t, uint64_t > > &predecessors, bool generatePredecessors, bool lower, uint64_t currentState, ValueType const &currentDistance, bool isPivotState, storm::storage::ExplicitGameStrategyPair const &strategyPair, storm::storage::ExplicitGameStrategyPair const &otherStrategyPair, std::vector< uint64_t > const &player1Labeling, std::vector< uint64_t > const &player2Grouping, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::BitVector const &targetStates, storm::storage::BitVector const &relevantStates)
template<typename ValueType>
boost::optional< ExplicitPivotStateResult< ValueType > > pickPivotState (bool generatePredecessors, AbstractionSettings::PivotSelectionHeuristic pivotSelectionHeuristic, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, std::vector< uint64_t > const &player1Labeling, storm::storage::BitVector const &initialStates, storm::storage::BitVector const &relevantStates, storm::storage::BitVector const &targetStates, storage::ExplicitGameStrategyPair const &minStrategyPair, storage::ExplicitGameStrategyPair const &maxStrategyPair, std::vector< ValueType > const *lowerValues=nullptr, std::vector< ValueType > const *upperValues=nullptr)

Variables

template<typename ValueType>
const uint64_t ExplicitPivotStateResult< ValueType >::NO_PREDECESSOR = std::numeric_limits<uint64_t>::max()

Function Documentation

◆ computePivotStates()

template<storm::dd::DdType Type, typename ValueType>
PivotStateCandidatesResult< Type > storm::gbar::abstraction::computePivotStates ( storm::gbar::abstraction::MenuGame< Type, ValueType > const & game,
storm::dd::Bdd< Type > const & transitionMatrixBdd,
storm::dd::Bdd< Type > const & minPlayer1Strategy,
storm::dd::Bdd< Type > const & minPlayer2Strategy,
storm::dd::Bdd< Type > const & maxPlayer1Strategy,
storm::dd::Bdd< Type > const & maxPlayer2Strategy )

Definition at line 522 of file MenuGameRefiner.cpp.

◆ getMostProbablePathSpanningTree()

template<storm::dd::DdType Type, typename ValueType>
SymbolicMostProbablePathsResult< Type, ValueType > storm::gbar::abstraction::getMostProbablePathSpanningTree ( storm::gbar::abstraction::MenuGame< Type, ValueType > const & game,
storm::dd::Bdd< Type > const & transitionFilter )

Definition at line 112 of file MenuGameRefiner.cpp.

◆ getStateName()

template<typename ValueType>
std::string storm::gbar::abstraction::getStateName ( std::pair< storm::expressions::SimpleValuation, ValueType > const & stateValue,
std::set< storm::expressions::Variable > const & locationVariables,
std::set< storm::expressions::Variable > const & predicateVariables,
storm::expressions::Variable const & bottomVariable )

Definition at line 32 of file MenuGameAbstractor.cpp.

◆ operator<<() [1/3]

template<storm::dd::DdType DdType>
std::ostream & storm::gbar::abstraction::operator<< ( std::ostream & out,
LocalExpressionInformation< DdType > const & partition )

Definition at line 205 of file LocalExpressionInformation.cpp.

◆ operator<<() [2/3]

template std::ostream & storm::gbar::abstraction::operator<< ( std::ostream & out,
LocalExpressionInformation< storm::dd::DdType::CUDD > const & partition )

◆ operator<<() [3/3]

template std::ostream & storm::gbar::abstraction::operator<< ( std::ostream & out,
LocalExpressionInformation< storm::dd::DdType::Sylvan > const & partition )

◆ performDijkstraStep()

template<typename ValueType>
void storm::gbar::abstraction::performDijkstraStep ( std::set< ExplicitDijkstraQueueElement< ValueType >, ExplicitDijkstraQueueElementLess< ValueType > > & dijkstraQueue,
bool probabilityDistances,
std::vector< ValueType > & distances,
std::vector< std::pair< uint64_t, uint64_t > > & predecessors,
bool generatePredecessors,
bool lower,
uint64_t currentState,
ValueType const & currentDistance,
bool isPivotState,
storm::storage::ExplicitGameStrategyPair const & strategyPair,
storm::storage::ExplicitGameStrategyPair const & otherStrategyPair,
std::vector< uint64_t > const & player1Labeling,
std::vector< uint64_t > const & player2Grouping,
storm::storage::SparseMatrix< ValueType > const & transitionMatrix,
storm::storage::BitVector const & targetStates,
storm::storage::BitVector const & relevantStates )

Definition at line 1136 of file MenuGameRefiner.cpp.

◆ pickPivotState() [1/2]

template<storm::dd::DdType Type, typename ValueType>
SymbolicPivotStateResult< Type, ValueType > storm::gbar::abstraction::pickPivotState ( AbstractionSettings::PivotSelectionHeuristic const & heuristic,
storm::gbar::abstraction::MenuGame< Type, ValueType > const & game,
PivotStateCandidatesResult< Type > const & pivotStateCandidateResult,
boost::optional< SymbolicQualitativeGameResultMinMax< Type > > const & qualitativeResult,
boost::optional< SymbolicQuantitativeGameResultMinMax< Type, ValueType > > const & quantitativeResult )

Definition at line 152 of file MenuGameRefiner.cpp.

◆ pickPivotState() [2/2]

template<typename ValueType>
boost::optional< ExplicitPivotStateResult< ValueType > > storm::gbar::abstraction::pickPivotState ( bool generatePredecessors,
AbstractionSettings::PivotSelectionHeuristic pivotSelectionHeuristic,
storm::storage::SparseMatrix< ValueType > const & transitionMatrix,
std::vector< uint64_t > const & player1Labeling,
storm::storage::BitVector const & initialStates,
storm::storage::BitVector const & relevantStates,
storm::storage::BitVector const & targetStates,
storage::ExplicitGameStrategyPair const & minStrategyPair,
storage::ExplicitGameStrategyPair const & maxStrategyPair,
std::vector< ValueType > const * lowerValues = nullptr,
std::vector< ValueType > const * upperValues = nullptr )

Definition at line 1178 of file MenuGameRefiner.cpp.

Variable Documentation

◆ ExplicitPivotStateResult< ValueType >::NO_PREDECESSOR

template<typename ValueType>
const uint64_t storm::gbar::abstraction::ExplicitPivotStateResult< ValueType >::NO_PREDECESSOR = std::numeric_limits<uint64_t>::max()

Definition at line 728 of file MenuGameRefiner.cpp.