Storm
A Modern Probabilistic Model Checker
|
This is the complete list of members for storm::gbar::abstraction::MenuGame< Type, ValueType >, including all inherited members.
addParameters(std::set< storm::RationalFunctionVariable > const ¶meters) | storm::models::symbolic::Model< Type, ValueType > | |
addParameters(std::set< storm::RationalFunctionVariable > const ¶meters) | storm::models::symbolic::Model< Type, ValueType > | |
as() | storm::models::ModelBase | inline |
as() const | storm::models::ModelBase | inline |
DdType | storm::models::symbolic::Model< Type, ValueType > | static |
getBottomStates() const | storm::gbar::abstraction::MenuGame< Type, ValueType > | |
getColumnAndNondeterminismVariables() const | storm::models::symbolic::Model< Type, ValueType > | |
getColumnVariables() const | storm::models::symbolic::Model< Type, ValueType > | |
getDeadlockStates() const | storm::models::symbolic::Model< Type, ValueType > | |
getExpression(std::string const &label) const | storm::models::symbolic::Model< Type, ValueType > | virtual |
getExtendedTransitionMatrix() const | storm::gbar::abstraction::MenuGame< Type, ValueType > | |
getIllegalMask() const | storm::models::symbolic::NondeterministicModel< Type, ValueType > | |
getIllegalPlayer1Mask() const | storm::models::symbolic::StochasticTwoPlayerGame< Type, ValueType > | |
getIllegalPlayer2Mask() const | storm::models::symbolic::StochasticTwoPlayerGame< Type, ValueType > | |
getIllegalSuccessorMask() const | storm::models::symbolic::NondeterministicModel< Type, ValueType > | |
getInitialStates() const | storm::models::symbolic::Model< Type, ValueType > | |
getLabels() const | storm::models::symbolic::Model< Type, ValueType > | |
getLabelToBddMap() const | storm::models::symbolic::Model< Type, ValueType > | protected |
getLabelToExpressionMap() const | storm::models::symbolic::Model< Type, ValueType > | protected |
getManager() const | storm::models::symbolic::Model< Type, ValueType > | |
getManagerAsSharedPointer() const | storm::models::symbolic::Model< Type, ValueType > | |
getNondeterminismVariables() const override | storm::models::symbolic::NondeterministicModel< Type, ValueType > | virtual |
getNumberOfChoices() const override | storm::models::symbolic::NondeterministicModel< Type, ValueType > | virtual |
getNumberOfPlayer2States() const | storm::models::symbolic::StochasticTwoPlayerGame< Type, ValueType > | |
getNumberOfRewardModels() const | storm::models::symbolic::Model< Type, ValueType > | |
getNumberOfStates() const override | storm::models::symbolic::Model< Type, ValueType > | virtual |
getNumberOfTransitions() const override | storm::models::symbolic::Model< Type, ValueType > | virtual |
getParameters() const | storm::models::symbolic::Model< Type, ValueType > | |
getParameters() const | storm::models::symbolic::Model< Type, ValueType > | |
getPlayer1Variables() const | storm::models::symbolic::StochasticTwoPlayerGame< Type, ValueType > | |
getPlayer2Variables() const | storm::models::symbolic::StochasticTwoPlayerGame< Type, ValueType > | |
getProbabilisticBranchingVariables() const | storm::gbar::abstraction::MenuGame< Type, ValueType > | |
getQualitativeTransitionMatrix(bool keepNondeterminism=true) const override | storm::models::symbolic::NondeterministicModel< Type, ValueType > | virtual |
getReachableStates() const | storm::models::symbolic::Model< Type, ValueType > | |
getRewardModel(std::string const &rewardModelName) const | storm::models::symbolic::Model< Type, ValueType > | |
getRewardModels() | storm::models::symbolic::Model< Type, ValueType > | |
getRewardModels() const | storm::models::symbolic::Model< Type, ValueType > | |
getRowAndNondeterminismVariables() const | storm::models::symbolic::Model< Type, ValueType > | |
getRowColumnIdentity() const | storm::models::symbolic::Model< Type, ValueType > | |
getRowColumnMetaVariablePairs() const | storm::models::symbolic::Model< Type, ValueType > | |
getRowExpressionAdapter() const | storm::models::symbolic::Model< Type, ValueType > | protected |
getRowVariables() const | storm::models::symbolic::Model< Type, ValueType > | |
getStates(std::string const &label) const override | storm::gbar::abstraction::MenuGame< Type, ValueType > | virtual |
getStates(storm::expressions::Expression const &expression) const override | storm::gbar::abstraction::MenuGame< Type, ValueType > | virtual |
getStates(storm::expressions::Expression const &expression, bool negated) const | storm::gbar::abstraction::MenuGame< Type, ValueType > | |
getTransitionMatrix() const | storm::models::symbolic::Model< Type, ValueType > | |
getTransitionMatrix() | storm::models::symbolic::Model< Type, ValueType > | |
getType() const | storm::models::ModelBase | virtual |
getUniqueRewardModel() const | storm::models::symbolic::Model< Type, ValueType > | |
getUniqueRewardModel() | storm::models::symbolic::Model< Type, ValueType > | |
getUniqueRewardModelName() const override | storm::models::symbolic::Model< Type, ValueType > | virtual |
hasLabel(std::string const &label) const override | storm::gbar::abstraction::MenuGame< Type, ValueType > | virtual |
hasParameters() const override | storm::models::symbolic::Model< Type, ValueType > | virtual |
hasRewardModel(std::string const &rewardModelName) const override | storm::models::symbolic::Model< Type, ValueType > | virtual |
hasRewardModel() const | storm::models::symbolic::Model< Type, ValueType > | |
hasUniqueRewardModel() const override | storm::models::symbolic::Model< Type, ValueType > | virtual |
illegalMask | storm::models::symbolic::NondeterministicModel< Type, ValueType > | protected |
isDiscreteTimeModel() const | storm::models::ModelBase | |
isExact() const | storm::models::ModelBase | virtual |
isNondeterministicModel() const | storm::models::ModelBase | |
isOfType(storm::models::ModelType const &modelType) const | storm::models::ModelBase | |
isPartiallyObservable() const | storm::models::ModelBase | virtual |
isSparseModel() const | storm::models::ModelBase | virtual |
isSymbolicModel() const override | storm::models::symbolic::Model< Type, ValueType > | virtual |
MenuGame(MenuGame< Type, ValueType > const &other)=default | storm::gbar::abstraction::MenuGame< Type, ValueType > | |
MenuGame(MenuGame< Type, ValueType > &&other)=default | storm::gbar::abstraction::MenuGame< Type, ValueType > | |
MenuGame(std::shared_ptr< storm::dd::DdManager< Type > > manager, storm::dd::Bdd< Type > reachableStates, storm::dd::Bdd< Type > initialStates, storm::dd::Bdd< Type > deadlockStates, storm::dd::Add< Type, ValueType > transitionMatrix, storm::dd::Bdd< Type > bottomStates, std::set< storm::expressions::Variable > const &rowVariables, std::set< storm::expressions::Variable > const &columnVariables, std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &rowColumnMetaVariablePairs, std::set< storm::expressions::Variable > const &player1Variables, std::set< storm::expressions::Variable > const &player2Variables, std::set< storm::expressions::Variable > const &allNondeterminismVariables, std::set< storm::expressions::Variable > const &probabilisticBranchingVariables, std::map< storm::expressions::Expression, storm::dd::Bdd< Type > > const &expressionToBddMap) | storm::gbar::abstraction::MenuGame< Type, ValueType > | |
Model(Model< Type, ValueType > const &other)=default | storm::models::symbolic::Model< Type, ValueType > | |
Model(Model< Type, ValueType > &&other)=default | storm::models::symbolic::Model< Type, ValueType > | |
Model(storm::models::ModelType const &modelType, std::shared_ptr< storm::dd::DdManager< Type > > manager, storm::dd::Bdd< Type > reachableStates, storm::dd::Bdd< Type > initialStates, storm::dd::Bdd< Type > deadlockStates, storm::dd::Add< Type, ValueType > transitionMatrix, std::set< storm::expressions::Variable > const &rowVariables, std::shared_ptr< storm::adapters::AddExpressionAdapter< Type, ValueType > > rowExpressionAdapter, std::set< storm::expressions::Variable > const &columnVariables, std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &rowColumnMetaVariablePairs, std::map< std::string, storm::expressions::Expression > labelToExpressionMap=std::map< std::string, storm::expressions::Expression >(), std::unordered_map< std::string, RewardModelType > const &rewardModels=std::unordered_map< std::string, RewardModelType >()) | storm::models::symbolic::Model< Type, ValueType > | |
Model(storm::models::ModelType const &modelType, std::shared_ptr< storm::dd::DdManager< Type > > manager, storm::dd::Bdd< Type > reachableStates, storm::dd::Bdd< Type > initialStates, storm::dd::Bdd< Type > deadlockStates, storm::dd::Add< Type, ValueType > transitionMatrix, std::set< storm::expressions::Variable > const &rowVariables, std::set< storm::expressions::Variable > const &columnVariables, std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &rowColumnMetaVariablePairs, std::map< std::string, storm::dd::Bdd< Type > > labelToBddMap=std::map< std::string, storm::dd::Bdd< Type > >(), std::unordered_map< std::string, RewardModelType > const &rewardModels=std::unordered_map< std::string, RewardModelType >()) | storm::models::symbolic::Model< Type, ValueType > | |
storm::models::Model::Model(ModelType const &modelType) | storm::models::Model< ValueType > | inline |
ModelBase(ModelType const &modelType) | storm::models::ModelBase | inline |
NondeterministicModel(NondeterministicModel< Type, ValueType > const &other)=default | storm::models::symbolic::NondeterministicModel< Type, ValueType > | |
NondeterministicModel(NondeterministicModel< Type, ValueType > &&other)=default | storm::models::symbolic::NondeterministicModel< Type, ValueType > | |
NondeterministicModel(storm::models::ModelType const &modelType, std::shared_ptr< storm::dd::DdManager< Type > > manager, storm::dd::Bdd< Type > reachableStates, storm::dd::Bdd< Type > initialStates, storm::dd::Bdd< Type > deadlockStates, storm::dd::Add< Type, ValueType > transitionMatrix, std::set< storm::expressions::Variable > const &rowVariables, std::shared_ptr< storm::adapters::AddExpressionAdapter< Type, ValueType > > rowExpressionAdapter, std::set< storm::expressions::Variable > const &columnVariables, std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &rowColumnMetaVariablePairs, std::set< storm::expressions::Variable > const &nondeterminismVariables, std::map< std::string, storm::expressions::Expression > labelToExpressionMap=std::map< std::string, storm::expressions::Expression >(), std::unordered_map< std::string, RewardModelType > const &rewardModels=std::unordered_map< std::string, RewardModelType >()) | storm::models::symbolic::NondeterministicModel< Type, ValueType > | |
NondeterministicModel(storm::models::ModelType const &modelType, std::shared_ptr< storm::dd::DdManager< Type > > manager, storm::dd::Bdd< Type > reachableStates, storm::dd::Bdd< Type > initialStates, storm::dd::Bdd< Type > deadlockStates, storm::dd::Add< Type, ValueType > transitionMatrix, std::set< storm::expressions::Variable > const &rowVariables, std::set< storm::expressions::Variable > const &columnVariables, std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &rowColumnMetaVariablePairs, std::set< storm::expressions::Variable > const &nondeterminismVariables, std::map< std::string, storm::dd::Bdd< Type > > labelToBddMap=std::map< std::string, storm::dd::Bdd< Type > >(), std::unordered_map< std::string, RewardModelType > const &rewardModels=std::unordered_map< std::string, RewardModelType >()) | storm::models::symbolic::NondeterministicModel< Type, ValueType > | |
operator=(MenuGame< Type, ValueType > const &other)=default | storm::gbar::abstraction::MenuGame< Type, ValueType > | |
operator=(MenuGame< Type, ValueType > &&other)=default | storm::gbar::abstraction::MenuGame< Type, ValueType > | |
StochasticTwoPlayerGame< Type, ValueType >::operator=(StochasticTwoPlayerGame< Type, ValueType > const &other)=default | storm::models::symbolic::StochasticTwoPlayerGame< Type, ValueType > | |
StochasticTwoPlayerGame< Type, ValueType >::operator=(StochasticTwoPlayerGame< Type, ValueType > &&other)=default | storm::models::symbolic::StochasticTwoPlayerGame< Type, ValueType > | |
NondeterministicModel< Type, ValueType >::operator=(NondeterministicModel< Type, ValueType > const &other)=default | storm::models::symbolic::NondeterministicModel< Type, ValueType > | |
NondeterministicModel< Type, ValueType >::operator=(NondeterministicModel< Type, ValueType > &&other)=default | storm::models::symbolic::NondeterministicModel< Type, ValueType > | |
Model< Type, ValueType >::operator=(Model< Type, ValueType > const &other)=default | storm::models::symbolic::Model< Type, ValueType > | |
Model< Type, ValueType >::operator=(Model< Type, ValueType > &&other)=default | storm::models::symbolic::Model< Type, ValueType > | |
printDdVariableInformationToStream(std::ostream &out) const override | storm::models::symbolic::NondeterministicModel< Type, ValueType > | protectedvirtual |
printModelInformationFooterToStream(std::ostream &out) const | storm::models::symbolic::Model< Type, ValueType > | protected |
printModelInformationHeaderToStream(std::ostream &out) const | storm::models::symbolic::Model< Type, ValueType > | protected |
printModelInformationToStream(std::ostream &out) const override | storm::models::symbolic::NondeterministicModel< Type, ValueType > | virtual |
printRewardModelsInformationToStream(std::ostream &out) const | storm::models::symbolic::Model< Type, ValueType > | protected |
reduceToStateBasedRewards() override | storm::models::symbolic::NondeterministicModel< Type, ValueType > | virtual |
Representation | storm::models::symbolic::Model< Type, ValueType > | static |
RewardModelType typedef | storm::gbar::abstraction::MenuGame< Type, ValueType > | |
setTransitionMatrix(storm::dd::Add< Type, ValueType > const &transitionMatrix) | storm::models::symbolic::Model< Type, ValueType > | protected |
StochasticTwoPlayerGame(StochasticTwoPlayerGame< Type, ValueType > const &other)=default | storm::models::symbolic::StochasticTwoPlayerGame< Type, ValueType > | |
StochasticTwoPlayerGame(StochasticTwoPlayerGame< Type, ValueType > &&other)=default | storm::models::symbolic::StochasticTwoPlayerGame< Type, ValueType > | |
StochasticTwoPlayerGame(std::shared_ptr< storm::dd::DdManager< Type > > manager, storm::dd::Bdd< Type > reachableStates, storm::dd::Bdd< Type > initialStates, storm::dd::Bdd< Type > deadlockStates, storm::dd::Add< Type, ValueType > transitionMatrix, std::set< storm::expressions::Variable > const &rowVariables, std::shared_ptr< storm::adapters::AddExpressionAdapter< Type, ValueType > > rowExpressionAdapter, std::set< storm::expressions::Variable > const &columnVariables, std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &rowColumnMetaVariablePairs, std::set< storm::expressions::Variable > const &player1Variables, std::set< storm::expressions::Variable > const &player2Variables, std::set< storm::expressions::Variable > const &allNondeterminismVariables, std::map< std::string, storm::expressions::Expression > labelToExpressionMap=std::map< std::string, storm::expressions::Expression >(), std::unordered_map< std::string, RewardModelType > const &rewardModels=std::unordered_map< std::string, RewardModelType >()) | storm::models::symbolic::StochasticTwoPlayerGame< Type, ValueType > | |
StochasticTwoPlayerGame(std::shared_ptr< storm::dd::DdManager< Type > > manager, storm::dd::Bdd< Type > reachableStates, storm::dd::Bdd< Type > initialStates, storm::dd::Bdd< Type > deadlockStates, storm::dd::Add< Type, ValueType > transitionMatrix, std::set< storm::expressions::Variable > const &rowVariables, std::set< storm::expressions::Variable > const &columnVariables, std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &rowColumnMetaVariablePairs, std::set< storm::expressions::Variable > const &player1Variables, std::set< storm::expressions::Variable > const &player2Variables, std::set< storm::expressions::Variable > const &allNondeterminismVariables, std::map< std::string, storm::dd::Bdd< Type > > labelToBddMap=std::map< std::string, storm::dd::Bdd< Type > >(), std::unordered_map< std::string, RewardModelType > const &rewardModels=std::unordered_map< std::string, RewardModelType >()) | storm::models::symbolic::StochasticTwoPlayerGame< Type, ValueType > | |
supportsParameters() const override | storm::models::symbolic::Model< Type, ValueType > | virtual |
toValueType() const | storm::models::symbolic::StochasticTwoPlayerGame< Type, ValueType > | |
transitionMatrix | storm::models::symbolic::Model< Type, ValueType > | protected |
ValueType typedef | storm::models::symbolic::Model< Type, ValueType > | |
writeDotToFile(std::string const &filename) const | storm::models::symbolic::Model< Type, ValueType > | |
~Model()=default | storm::models::Model< ValueType > | virtual |
~ModelBase() | storm::models::ModelBase | inlinevirtual |