MenuGame.h

Go to the documentation of this file.

#pragma once
 
#include <map>
 
#include "storm/models/symbolic/StochasticTwoPlayerGame.h"
 
namespace storm::gbar {
namespace abstraction {
 
template<storm::dd::DdType Type, typename ValueType>
class MenuGame : public storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType> {
   public:
    typedef typename storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType>::RewardModelType RewardModelType;
 
    MenuGame(MenuGame<Type, ValueType> const& other) = default;
    MenuGame& operator=(MenuGame<Type, ValueType> const& other) = default;
    MenuGame(MenuGame<Type, ValueType>&& other) = default;
    MenuGame& operator=(MenuGame<Type, ValueType>&& other) = default;
 
    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);
 
    virtual storm::dd::Bdd<Type> getStates(std::string const& label) const override;
 
    virtual storm::dd::Bdd<Type> getStates(storm::expressions::Expression const& expression) const override;
 
    storm::dd::Bdd<Type> getStates(storm::expressions::Expression const& expression, bool negated) const;
 
    storm::dd::Bdd<Type> getBottomStates() const;
 
    storm::dd::Add<Type, ValueType> const& getExtendedTransitionMatrix() const;
 
    std::set<storm::expressions::Variable> const& getProbabilisticBranchingVariables() const;
 
    virtual bool hasLabel(std::string const& label) const override;
 
   private:
    // The transition relation extended byt the probabilistic branching variables.
    storm::dd::Add<Type, ValueType> extendedTransitionMatrix;
 
    // The meta variables used to probabilistic branching.
    std::set<storm::expressions::Variable> probabilisticBranchingVariables;
 
    // A mapping from expressions that were used in the abstraction process to the the BDDs representing them.
    std::map<storm::expressions::Expression, storm::dd::Bdd<Type>> expressionToBddMap;
 
    // The bottom states of the model.
    storm::dd::Bdd<Type> bottomStates;
};
 
}  // namespace abstraction
}  // namespace storm::gbar