SparseLTLHelper.h

Go to the documentation of this file.

#pragma once
 
#include "storm/modelchecker/helper/SingleValueModelCheckerHelper.h"
#include "storm/modelchecker/helper/ltl/internal/SparseLTLSchedulerHelper.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/transformer/DAProductBuilder.h"
 
namespace storm {
 
class Environment;
 
namespace logic {
class Formula;
class PathFormula;
}  // namespace logic
namespace automata {
class DeterministicAutomaton;
}
 
namespace modelchecker {
namespace helper {

template<typename ValueType, bool Nondeterministic>
class SparseLTLHelper : public SingleValueModelCheckerHelper<ValueType, storm::models::ModelRepresentation::Sparse> {
   public:
    typedef std::function<storm::storage::BitVector(storm::logic::Formula const&)> CheckFormulaCallback;

    using productModelType = typename std::conditional<Nondeterministic, storm::models::sparse::Mdp<ValueType>, storm::models::sparse::Dtmc<ValueType>>::type;

    SparseLTLHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix);

    storm::storage::Scheduler<ValueType> extractScheduler(storm::models::sparse::Model<ValueType> const& model);

    std::vector<ValueType> computeLTLProbabilities(Environment const& env, storm::logic::PathFormula const& formula,
                                                   CheckFormulaCallback const& formulaChecker);

    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<ValueType> computeDAProductProbabilities(Environment const& env, storm::automata::DeterministicAutomaton const& da,
                                                         std::map<std::string, storm::storage::BitVector>& apSatSets);

    std::vector<ValueType> computeLTLProbabilities(Environment const& env, storm::logic::PathFormula const& formula,
                                                   std::map<std::string, storm::storage::BitVector>& apSatSets);
 
   private:
    storm::storage::BitVector computeAcceptingECs(automata::AcceptanceCondition const& acceptance,
                                                  storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
                                                  storm::storage::SparseMatrix<ValueType> const& backwardTransitions,
                                                  typename transformer::DAProduct<productModelType>::ptr product);

    storm::storage::BitVector computeAcceptingBCCs(automata::AcceptanceCondition const& acceptance,
                                                   storm::storage::SparseMatrix<ValueType> const& transitionMatrix);
 
    storm::storage::SparseMatrix<ValueType> const& _transitionMatrix;
 
    boost::optional<storm::modelchecker::helper::internal::SparseLTLSchedulerHelper<ValueType, Nondeterministic>> _schedulerHelper;
};
}  // namespace helper
}  // namespace modelchecker
}  // namespace storm