SparseLTLSchedulerHelper.h

Go to the documentation of this file.

#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/storage/MaximalEndComponent.h"
#include "storm/storage/Scheduler.h"
#include "storm/transformer/DAProductBuilder.h"
 
namespace storm {
 
namespace modelchecker {
namespace helper {
namespace internal {
 
template<typename ValueType, bool Nondeterministic>
class SparseLTLSchedulerHelper {
   public:
    using productModelType = typename std::conditional<Nondeterministic, storm::models::sparse::Mdp<ValueType>, storm::models::sparse::Dtmc<ValueType>>::type;
 
    SparseLTLSchedulerHelper(uint_fast64_t numProductStates);
 
    void setRandom();
 
    void saveProductEcChoices(automata::AcceptanceCondition const& acceptance, storm::storage::MaximalEndComponent const& acceptingEC,
                              storm::storage::MaximalEndComponent const& containingMEC,
                              std::vector<automata::AcceptanceCondition::acceptance_expr::ptr> const& conjunction,
                              typename transformer::DAProduct<productModelType>::ptr product);
 
    void prepareScheduler(uint_fast64_t numDaStates, storm::storage::BitVector const& acceptingProductStates,
                          std::unique_ptr<storm::storage::Scheduler<ValueType>> reachScheduler, transformer::DAProductBuilder const& productBuilder,
                          typename transformer::DAProduct<productModelType>::ptr product, storm::storage::BitVector const& modelStatesOfInterest,
                          storm::storage::SparseMatrix<ValueType> const& transitionMatrix);
 
    storm::storage::Scheduler<ValueType> extractScheduler(storm::models::sparse::Model<ValueType> const& model, bool onlyInitialStatesRelevant);
 
   private:
    uint_fast64_t getMemoryState(uint_fast64_t daState, uint_fast64_t infSet);
 
    class InfSetPool {
       public:
        InfSetPool() = default;
 
        uint_fast64_t getOrCreateIndex(storm::storage::BitVector&& infSet);
        storm::storage::BitVector const& get(uint_fast64_t index) const;
 
        uint_fast64_t size() const;
 
       private:
        std::vector<storm::storage::BitVector> _storage;
    } _infSets;
 
    static const uint_fast64_t DEFAULT_INFSET;  
 
    bool _randomScheduler;
    std::vector<storm::storage::BitVector> _dontCareStates;  // memorySate-modelState combinations that are never visited
 
    std::map<std::tuple<uint_fast64_t, uint_fast64_t, uint_fast64_t>, storm::storage::SchedulerChoice<ValueType>>
        _producedChoices;  // <s, q, DEFAULT_INFSET)> -> ReachChoice  and    <s, q, InfSetIndex> -> MecChoice
 
    std::vector<boost::optional<std::set<uint_fast64_t>>>
        _accInfSets;  // Save for each product state (which is assigned to an acceptingMEC), the infSets that need to be visited inf often to satisfy the
                      // acceptance condition. Remaining states belonging to no accepting EC, are assigned  len(_infSets) (REACH scheduler)
 
    // Memory structure
    std::vector<std::vector<storm::storage::BitVector>>
        _memoryTransitions;  // The BitVector contains the model states that lead from startState <q, mec, infSet> to <q', mec', infSet'>. This is
                             // deterministic, because each state <s, q> is assigned to a unique MEC (scheduler).
    std::vector<uint_fast64_t> _memoryInitialStates;  // Save for each relevant state (initial or all) s its unique initial memory state (which memory state is
                                                      // reached from the initial state after reading s)
};
}  // namespace internal
}  // namespace helper
}  // namespace modelchecker
}  // namespace storm