LexicographicModelCheckerHelper.h

Go to the documentation of this file.

#pragma once
 
#include "storm/modelchecker/helper/SingleValueModelCheckerHelper.h"
 
#include "storm/logic/Formulas.h"
#include "storm/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h"
#include "storm/models/ModelRepresentation.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/storage/BitVector.h"
#include "storm/storage/MaximalEndComponentDecomposition.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/transformer/DAProductBuilder.h"
#include "storm/transformer/SubsystemBuilder.h"
 
namespace storm {
 
class Environment;
 
namespace modelchecker {
namespace helper {
namespace lexicographic {
 
template<typename SparseModelType, typename ValueType, bool Nondeterministic>
class LexicographicModelCheckerHelper : public helper::SingleValueModelCheckerHelper<ValueType, storm::models::ModelRepresentation::Sparse> {
   public:
    typedef std::function<storm::storage::BitVector(storm::logic::Formula const&)> CheckFormulaCallback;
    typedef storm::transformer::SubsystemBuilderReturnType<ValueType, storm::models::sparse::StandardRewardModel<ValueType>> SubsystemReturnType;
    using StateType = storm::storage::sparse::state_type;
    using productModelType = typename storm::models::sparse::Mdp<ValueType>;
 
    // init
    LexicographicModelCheckerHelper(storm::logic::MultiObjectiveFormula const& formula, storm::storage::SparseMatrix<ValueType> const& transitionMatrix)
        : _transitionMatrix(transitionMatrix), formula(formula) {}

    std::pair<std::shared_ptr<storm::transformer::DAProduct<SparseModelType>>, std::vector<uint64_t>> getCompleteProductModel(
        SparseModelType const& model, CheckFormulaCallback const& formulaChecker);

    std::pair<storm::storage::MaximalEndComponentDecomposition<ValueType>, std::vector<std::vector<bool>>> getLexArrays(
        std::shared_ptr<storm::transformer::DAProduct<productModelType>> productModel, std::vector<uint64_t>& acceptanceConditions);

    MDPSparseModelCheckingHelperReturnType<ValueType> lexReachability(Environment const& env,
                                                                      storm::storage::MaximalEndComponentDecomposition<ValueType> const& mecs,
                                                                      std::vector<std::vector<bool>> const& mecLexArray,
                                                                      std::shared_ptr<storm::transformer::DAProduct<SparseModelType>> const& productModel,
                                                                      SparseModelType const& originalMdp);
 
   private:
    static std::map<std::string, storm::storage::BitVector> computeApSets(std::map<std::string, std::shared_ptr<storm::logic::Formula const>> const& extracted,
                                                                          CheckFormulaCallback const& formulaChecker);

    std::vector<storm::automata::AcceptanceCondition::acceptance_expr::ptr> getStreettPairs(
        storm::automata::AcceptanceCondition::acceptance_expr::ptr const& current);

    bool isAcceptingStreettConditions(storm::storage::MaximalEndComponent const& scc,
                                      std::vector<storm::automata::AcceptanceCondition::acceptance_expr::ptr> const& acceptancePairs,
                                      storm::automata::AcceptanceCondition::ptr const& acceptance, productModelType const& model);

    storm::storage::BitVector getGoodStates(storm::storage::MaximalEndComponentDecomposition<ValueType> const& bcc,
                                            std::vector<std::vector<bool>> const& bccLexArray, std::vector<uint64_t> const& oldToNewStateMapping,
                                            uint64_t const& condition, uint64_t const numStates, std::vector<uint64_t> const& compressedToReducedMapping,
                                            std::map<uint64_t, uint64_t> const& bccToStStateMapping);

    MDPSparseModelCheckingHelperReturnType<ValueType> solveOneReachability(Environment const& env, std::vector<uint64_t>& newInitalStates,
                                                                           storm::storage::BitVector const& psiStates,
                                                                           storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
                                                                           SparseModelType const& originalMdp,
                                                                           std::vector<uint64_t> const& compressedToReducedMapping,
                                                                           std::vector<uint64_t> const& oldToNewStateMapping);

    SubsystemReturnType getReducedSubsystem(storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
                                            MDPSparseModelCheckingHelperReturnType<ValueType> const& reachabilityResult,
                                            std::vector<uint64_t> const& newInitalStates, storm::storage::BitVector const& goodStates);

    std::pair<storm::storage::SparseMatrix<ValueType>, std::map<uint64_t, uint64_t>> addSinkStates(
        storm::storage::MaximalEndComponentDecomposition<ValueType> const& mecs,
        std::shared_ptr<storm::transformer::DAProduct<SparseModelType>> const& productModel);
 
    storm::storage::SparseMatrix<ValueType> const& _transitionMatrix;
    storm::logic::MultiObjectiveFormula const& formula;
};
 
}  // namespace lexicographic
}  // namespace helper
}  // namespace modelchecker
}  // namespace storm