GoalStateMerger.h

Go to the documentation of this file.

#pragma once
 
#include <cstdint>
#include <memory>
#include <optional>
#include <set>
#include <string>
#include <unordered_map>
#include <vector>
 
#include "storm/models/sparse/ModelForward.h"
#include "storm/models/sparse/StateLabeling.h"
#include "storm/storage/BitVector.h"
#include "storm/storage/SparseMatrix.h"
 
namespace storm {
namespace logic {
class Formula;
class ProbabilityOperatorFormula;
class RewardOperatorFormula;
}  // namespace logic
namespace transformer {
 
/*
 * Merges the given target and sink states into single states with a selfloop.
 * Supports Dtmc, Ctmc, Mdp, and MarkovAutomaton models.
 */
template<typename ValueType>
class GoalStateMerger {
   public:
    struct ReturnType {
        std::shared_ptr<storm::models::sparse::Model<ValueType>> model;  // The output model
        std::optional<uint64_t> targetState;                             // The target state of the output model (if reachable)
        std::optional<uint64_t> sinkState;                               // The sink state of the output model (if reachable)
        std::vector<uint64_t> oldToNewStateIndexMapping;  // maps a state from the input model to the corresponding state of the output model. Invalid
                                                          // index if the state does not exist
        storm::storage::BitVector keptChoices;            // The choices of the input model that are still present in the output model
    };

    GoalStateMerger(storm::models::sparse::Model<ValueType> const& model);

    ReturnType mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates,
                                        storm::storage::BitVector const& sinkStates,
                                        std::vector<std::string> const& selectedRewardModels = std::vector<std::string>(),
                                        std::optional<storm::storage::BitVector> const& choiceFilter = std::nullopt,
                                        std::optional<uint64_t> representativeTargetState = std::nullopt,
                                        std::optional<uint64_t> representativeSinkState = std::nullopt) const;

    std::optional<ReturnType> mergeForFormula(storm::logic::Formula const& formula, bool const dropUnreachableFromInit) const;
 
   private:
    std::optional<ReturnType> mergeForUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula, bool const dropUnreachableFromInit) const;
    std::optional<ReturnType> mergeForBoundedUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula,
                                                                bool const dropUnreachableFromInit) const;
    std::optional<ReturnType> mergeForReachabilityRewards(storm::logic::RewardOperatorFormula const& formula, bool const dropUnreachableFromInit) const;
    std::optional<ReturnType> mergeForCumulativeRewards(storm::logic::RewardOperatorFormula const& formula, bool const dropUnreachableFromInit) const;
 
    storm::models::sparse::Model<ValueType> const& originalModel;

    std::pair<ReturnType, uint64_t> initialize(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates,
                                               storm::storage::BitVector const& sinkStates,
                                               std::optional<storm::storage::BitVector> const& choiceFilter = std::nullopt) const;

    storm::storage::SparseMatrix<ValueType> buildTransitionMatrix(storm::storage::BitVector const& maybeStates, ReturnType const& resultData,
                                                                  uint64_t transitionCount) const;
    storm::models::sparse::StateLabeling buildStateLabeling(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates,
                                                            storm::storage::BitVector const& sinkStates, ReturnType const& resultData,
                                                            std::optional<uint64_t> const representativeTargetState = std::nullopt,
                                                            std::optional<uint64_t> const representativeSinkState = std::nullopt) const;
    std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> buildRewardModels(
        storm::storage::BitVector const& maybeStates, ReturnType const& resultData, std::vector<std::string> const& selectedRewardModels) const;
};
}  // namespace transformer
}  // namespace storm