graph.h

Go to the documentation of this file.

#pragma once
 
#include <limits>
#include <set>
 
#include "storm/models/sparse/DeterministicModel.h"
#include "storm/models/sparse/NondeterministicModel.h"
#include "storm/solver/OptimizationDirection.h"
#include "storm/storage/Scheduler.h"
#include "storm/storage/StronglyConnectedComponent.h"
#include "storm/storage/dd/Bdd.h"
#include "storm/storage/dd/DdType.h"
#include "storm/storage/sparse/StateType.h"
 
namespace storm {
namespace storage {
class BitVector;
template<typename VT>
class SparseMatrix;
}  // namespace storage
 
namespace models {
 
namespace symbolic {
template<storm::dd::DdType Type, typename ValueType>
class Model;
 
template<storm::dd::DdType Type, typename ValueType>
class DeterministicModel;
 
template<storm::dd::DdType Type, typename ValueType>
class NondeterministicModel;
 
template<storm::dd::DdType Type, typename ValueType>
class StochasticTwoPlayerGame;
}  // namespace symbolic
 
}  // namespace models
 
namespace dd {
template<storm::dd::DdType Type>
class Bdd;
 
template<storm::dd::DdType Type, typename ValueType>
class Add;
 
}  // namespace dd
 
namespace storage {
class ExplicitGameStrategyPair;
}
 
namespace utility {
namespace graph {

template<typename T>
storm::storage::BitVector getReachableOneStep(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::BitVector const& initialStates);

template<typename T>
storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::BitVector const& initialStates,
                                             storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates,
                                             bool useStepBound = false, uint_fast64_t maximalSteps = 0,
                                             boost::optional<storm::storage::BitVector> const& choiceFilter = boost::none);

template<typename T>
storm::storage::BitVector getBsccCover(storm::storage::SparseMatrix<T> const& transitionMatrix);

template<typename T>
bool hasCycle(storm::storage::SparseMatrix<T> const& transitionMatrix, boost::optional<storm::storage::BitVector> const& subsystem = boost::none);

template<typename T>
bool checkIfECWithChoiceExists(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::SparseMatrix<T> const& backwardTransitions,
                               storm::storage::BitVector const& subsystem, storm::storage::BitVector const& choices);

template<typename T>
std::vector<uint_fast64_t> getDistances(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::BitVector const& initialStates,
                                        boost::optional<storm::storage::BitVector> const& subsystem = boost::none);

template<typename T>
storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates,
                                              storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0);

template<typename T>
storm::storage::BitVector performProb1(storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates,
                                       storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0);

template<typename T>
storm::storage::BitVector performProb1(storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates,
                                       storm::storage::BitVector const& psiStates);

template<typename T>
std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01(storm::models::sparse::DeterministicModel<T> const& model,
                                                                              storm::storage::BitVector const& phiStates,
                                                                              storm::storage::BitVector const& psiStates);

template<typename T>
std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01(storm::storage::SparseMatrix<T> const& backwardTransitions,
                                                                              storm::storage::BitVector const& phiStates,
                                                                              storm::storage::BitVector const& psiStates);

template<storm::dd::DdType Type, typename ValueType>
storm::dd::Bdd<Type> performProbGreater0(storm::models::symbolic::Model<Type, ValueType> const& model, storm::dd::Bdd<Type> const& transitionMatrix,
                                         storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates,
                                         boost::optional<uint_fast64_t> const& stepBound = boost::optional<uint_fast64_t>());
template<storm::dd::DdType Type, typename ValueType>
storm::dd::Bdd<Type> performProb1(storm::models::symbolic::Model<Type, ValueType> const& model, storm::dd::Bdd<Type> const& transitionMatrix,
                                  storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates,
                                  storm::dd::Bdd<Type> const& statesWithProbabilityGreater0);

template<storm::dd::DdType Type, typename ValueType>
storm::dd::Bdd<Type> performProb1(storm::models::symbolic::Model<Type, ValueType> const& model, storm::dd::Bdd<Type> const& transitionMatrix,
                                  storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates);

template<storm::dd::DdType Type, typename ValueType>
std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> performProb01(storm::models::symbolic::DeterministicModel<Type, ValueType> const& model,
                                                                    storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates);

template<storm::dd::DdType Type, typename ValueType>
std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> performProb01(storm::models::symbolic::Model<Type, ValueType> const& model,
                                                                    storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates,
                                                                    storm::dd::Bdd<Type> const& psiStates);

template<typename T, typename SchedulerValueType>
void computeSchedulerStayingInStates(storm::storage::BitVector const& states, storm::storage::SparseMatrix<T> const& transitionMatrix,
                                     storm::storage::Scheduler<SchedulerValueType>& scheduler,
                                     boost::optional<storm::storage::BitVector> const& rowFilter = boost::none);

template<typename T>
void computeSchedulerWithOneSuccessorInStates(storm::storage::BitVector const& states, storm::storage::SparseMatrix<T> const& transitionMatrix,
                                              storm::storage::Scheduler<T>& scheduler);

template<typename T, typename SchedulerValueType>
void computeSchedulerProbGreater0E(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::SparseMatrix<T> const& backwardTransitions,
                                   storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates,
                                   storm::storage::Scheduler<SchedulerValueType>& scheduler,
                                   boost::optional<storm::storage::BitVector> const& rowFilter = boost::none);

template<typename T, typename SchedulerValueType>
void computeSchedulerRewInf(storm::storage::BitVector const& rewInfStates, storm::storage::SparseMatrix<T> const& transitionMatrix,
                            storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::Scheduler<SchedulerValueType>& scheduler);

template<typename T, typename SchedulerValueType>
void computeSchedulerProb0E(storm::storage::BitVector const& prob0EStates, storm::storage::SparseMatrix<T> const& transitionMatrix,
                            storm::storage::Scheduler<SchedulerValueType>& scheduler);

template<typename T, typename SchedulerValueType>
void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix<T> const& transitionMatrix,
                            storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates,
                            storm::storage::BitVector const& psiStates, storm::storage::Scheduler<SchedulerValueType>& scheduler,
                            boost::optional<storm::storage::BitVector> const& rowFilter = boost::none);

template<typename T>
storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates,
                                               storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0);
 
template<typename T>
storm::storage::BitVector performProb0A(storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates,
                                        storm::storage::BitVector const& psiStates);

template<typename T>
storm::storage::BitVector performProb1E(storm::storage::SparseMatrix<T> const& transitionMatrix,
                                        std::vector<uint_fast64_t> const& nondeterministicChoiceIndices,
                                        storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates,
                                        storm::storage::BitVector const& psiStates,
                                        boost::optional<storm::storage::BitVector> const& choiceConstraint = boost::none);

template<typename T, typename RM>
storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel<T, RM> const& model,
                                        storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates,
                                        storm::storage::BitVector const& psiStates);
 
template<typename T>
std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Max(storm::storage::SparseMatrix<T> const& transitionMatrix,
                                                                                 std::vector<uint_fast64_t> const& nondeterministicChoiceIndices,
                                                                                 storm::storage::SparseMatrix<T> const& backwardTransitions,
                                                                                 storm::storage::BitVector const& phiStates,
                                                                                 storm::storage::BitVector const& psiStates);

template<typename T, typename RM>
std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Max(storm::models::sparse::NondeterministicModel<T, RM> const& model,
                                                                                 storm::storage::BitVector const& phiStates,
                                                                                 storm::storage::BitVector const& psiStates);

template<typename T>
storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix<T> const& transitionMatrix,
                                               std::vector<uint_fast64_t> const& nondeterministicChoiceIndices,
                                               storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates,
                                               storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0,
                                               boost::optional<storm::storage::BitVector> const& choiceConstraint = boost::none);

template<typename T, typename RM>
storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel<T, RM> const& model,
                                        storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates,
                                        storm::storage::BitVector const& psiStates);
template<typename T>
storm::storage::BitVector performProb0E(storm::storage::SparseMatrix<T> const& transitionMatrix,
                                        std::vector<uint_fast64_t> const& nondeterministicChoiceIndices,
                                        storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates,
                                        storm::storage::BitVector const& psiStates);

template<typename T, typename RM>
storm::storage::BitVector performProb1A(storm::models::sparse::NondeterministicModel<T, RM> const& model,
                                        storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates,
                                        storm::storage::BitVector const& psiStates);
 
template<typename T>
storm::storage::BitVector performProb1A(storm::storage::SparseMatrix<T> const& transitionMatrix,
                                        std::vector<uint_fast64_t> const& nondeterministicChoiceIndices,
                                        storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates,
                                        storm::storage::BitVector const& psiStates);
 
template<typename T>
std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::storage::SparseMatrix<T> const& transitionMatrix,
                                                                                 std::vector<uint_fast64_t> const& nondeterministicChoiceIndices,
                                                                                 storm::storage::SparseMatrix<T> const& backwardTransitions,
                                                                                 storm::storage::BitVector const& phiStates,
                                                                                 storm::storage::BitVector const& psiStates);

template<typename T, typename RM>
std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::models::sparse::NondeterministicModel<T, RM> const& model,
                                                                                 storm::storage::BitVector const& phiStates,
                                                                                 storm::storage::BitVector const& psiStates);

template<storm::dd::DdType Type, typename ValueType = double>
storm::dd::Bdd<Type> performProbGreater0E(storm::models::symbolic::NondeterministicModel<Type, ValueType> const& model,
                                          storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates,
                                          storm::dd::Bdd<Type> const& psiStates);

template<storm::dd::DdType Type, typename ValueType>
storm::dd::Bdd<Type> computeSchedulerProbGreater0E(storm::models::symbolic::NondeterministicModel<Type, ValueType> const& model,
                                                   storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates,
                                                   storm::dd::Bdd<Type> const& psiStates);

template<storm::dd::DdType Type, typename ValueType = double>
storm::dd::Bdd<Type> performProb0A(storm::models::symbolic::NondeterministicModel<Type, ValueType> const& model, storm::dd::Bdd<Type> const& transitionMatrix,
                                   storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates);

template<storm::dd::DdType Type, typename ValueType = double>
storm::dd::Bdd<Type> performProbGreater0A(storm::models::symbolic::NondeterministicModel<Type, ValueType> const& model,
                                          storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates,
                                          storm::dd::Bdd<Type> const& psiStates);

template<storm::dd::DdType Type, typename ValueType = double>
storm::dd::Bdd<Type> performProb0E(storm::models::symbolic::NondeterministicModel<Type, ValueType> const& model, storm::dd::Bdd<Type> const& transitionMatrix,
                                   storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates);

template<storm::dd::DdType Type, typename ValueType = double>
storm::dd::Bdd<Type> performProb1A(storm::models::symbolic::NondeterministicModel<Type, ValueType> const& model, storm::dd::Bdd<Type> const& transitionMatrix,
                                   storm::dd::Bdd<Type> const& psiStates, storm::dd::Bdd<Type> const& statesWithProbabilityGreater0A);

template<storm::dd::DdType Type, typename ValueType = double>
storm::dd::Bdd<Type> performProb1E(storm::models::symbolic::NondeterministicModel<Type, ValueType> const& model, storm::dd::Bdd<Type> const& transitionMatrix,
                                   storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates,
                                   storm::dd::Bdd<Type> const& statesWithProbabilityGreater0E);

template<storm::dd::DdType Type, typename ValueType>
storm::dd::Bdd<Type> computeSchedulerProb1E(storm::models::symbolic::NondeterministicModel<Type, ValueType> const& model,
                                            storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates,
                                            storm::dd::Bdd<Type> const& psiStates, storm::dd::Bdd<Type> const& statesWithProbability1E);
 
template<storm::dd::DdType Type, typename ValueType = double>
std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> performProb01Max(storm::models::symbolic::NondeterministicModel<Type, ValueType> const& model,
                                                                       storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates);
 
template<storm::dd::DdType Type, typename ValueType = double>
std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> performProb01Max(storm::models::symbolic::NondeterministicModel<Type, ValueType> const& model,
                                                                       storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates,
                                                                       storm::dd::Bdd<Type> const& psiStates);
 
template<storm::dd::DdType Type, typename ValueType = double>
std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> performProb01Min(storm::models::symbolic::NondeterministicModel<Type, ValueType> const& model,
                                                                       storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates);
 
template<storm::dd::DdType Type, typename ValueType = double>
std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> performProb01Min(storm::models::symbolic::NondeterministicModel<Type, ValueType> const& model,
                                                                       storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates,
                                                                       storm::dd::Bdd<Type> const& psiStates);
 
template<storm::dd::DdType Type>
struct SymbolicGameProb01Result {
    SymbolicGameProb01Result() = default;
    SymbolicGameProb01Result(storm::dd::Bdd<Type> const& player1States, storm::dd::Bdd<Type> const& player2States,
                             boost::optional<storm::dd::Bdd<Type>> const& player1Strategy = boost::none,
                             boost::optional<storm::dd::Bdd<Type>> const& player2Strategy = boost::none)
        : player1States(player1States), player2States(player2States), player1Strategy(player1Strategy), player2Strategy(player2Strategy) {
        // Intentionally left empty.
    }
 
    bool hasPlayer1Strategy() const {
        return static_cast<bool>(player1Strategy);
    }
 
    storm::dd::Bdd<Type> const& getPlayer1Strategy() const {
        return player1Strategy.get();
    }
 
    boost::optional<storm::dd::Bdd<Type>> const& getOptionalPlayer1Strategy() {
        return player1Strategy;
    }
 
    bool hasPlayer2Strategy() const {
        return static_cast<bool>(player2Strategy);
    }
 
    storm::dd::Bdd<Type> const& getPlayer2Strategy() const {
        return player2Strategy.get();
    }
 
    boost::optional<storm::dd::Bdd<Type>> const& getOptionalPlayer2Strategy() {
        return player2Strategy;
    }
 
    storm::dd::Bdd<Type> const& getPlayer1States() const {
        return player1States;
    }
 
    storm::dd::Bdd<Type> const& getPlayer2States() const {
        return player2States;
    }
 
    storm::dd::Bdd<Type> player1States;
    storm::dd::Bdd<Type> player2States;
    boost::optional<storm::dd::Bdd<Type>> player1Strategy;
    boost::optional<storm::dd::Bdd<Type>> player2Strategy;
};

template<storm::dd::DdType Type, typename ValueType>
SymbolicGameProb01Result<Type> performProb0(storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType> const& model,
                                            storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates,
                                            storm::dd::Bdd<Type> const& psiStates, storm::OptimizationDirection const& player1Strategy,
                                            storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false,
                                            bool producePlayer2Strategy = false);

template<storm::dd::DdType Type, typename ValueType>
SymbolicGameProb01Result<Type> performProb1(storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType> const& model,
                                            storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates,
                                            storm::dd::Bdd<Type> const& psiStates, storm::OptimizationDirection const& player1Strategy,
                                            storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false,
                                            bool producePlayer2Strategy = false, boost::optional<storm::dd::Bdd<Type>> const& player1Candidates = boost::none);
 
struct ExplicitGameProb01Result {
    ExplicitGameProb01Result() = default;
    ExplicitGameProb01Result(uint64_t numberOfPlayer1States, uint64_t numberOfPlayer2States)
        : player1States(numberOfPlayer1States), player2States(numberOfPlayer2States) {
        // Intentionally left empty.
    }
 
    ExplicitGameProb01Result(storm::storage::BitVector const& player1States, storm::storage::BitVector const& player2States)
        : player1States(player1States), player2States(player2States) {
        // Intentionally left empty.
    }
 
    storm::storage::BitVector const& getPlayer1States() const {
        return player1States;
    }
 
    storm::storage::BitVector const& getPlayer2States() const {
        return player2States;
    }
 
    storm::storage::BitVector player1States;
    storm::storage::BitVector player2States;
};

template<typename ValueType>
ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups,
                                      storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions,
                                      std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates,
                                      storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction,
                                      storm::OptimizationDirection const& player2Direction, storm::storage::ExplicitGameStrategyPair* strategyPair = nullptr);

template<typename ValueType>
ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups,
                                      storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions,
                                      std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates,
                                      storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction,
                                      storm::OptimizationDirection const& player2Direction, storm::storage::ExplicitGameStrategyPair* strategyPair = nullptr,
                                      boost::optional<storm::storage::BitVector> const& player1Candidates = boost::none);

template<typename T>
std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<T> const& matrix, std::vector<uint64_t> const& firstStates = {});
 
template<typename T>
std::vector<uint_fast64_t> getBFSSort(storm::storage::SparseMatrix<T> const& matrix, std::vector<uint_fast64_t> const& firstStates);
 
}  // namespace graph
}  // namespace utility
}  // namespace storm