ExplicitDFTModelBuilder.h

Go to the documentation of this file.

#pragma once
 
#include <boost/optional/optional.hpp>
#include <limits>
#include <stack>
#include <unordered_set>
 
#include "storm/models/sparse/ChoiceLabeling.h"
#include "storm/models/sparse/Model.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/models/sparse/StateLabeling.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/storage/sparse/StateStorage.h"
 
#include "storm-dft/builder/DftExplorationHeuristic.h"
#include "storm-dft/generator/DftNextStateGenerator.h"
#include "storm-dft/storage/BucketPriorityQueue.h"
#include "storm-dft/storage/DFT.h"
#include "storm-dft/storage/DftSymmetries.h"
 
namespace storm::dft {
namespace builder {
 
template<typename ValueType, typename StateType = uint32_t>
class ExplicitDFTModelBuilder {
    using DFTStatePointer = std::shared_ptr<storm::dft::storage::DFTState<ValueType>>;
    using ExplorationHeuristic = DFTExplorationHeuristic<ValueType>;
    using ExplorationHeuristicPointer = std::shared_ptr<ExplorationHeuristic>;
 
    // A structure holding the individual components of a model.
    struct ModelComponents {
        // Constructor
        ModelComponents();
 
        // The transition matrix.
        storm::storage::SparseMatrix<ValueType> transitionMatrix;
 
        // The state labeling.
        storm::models::sparse::StateLabeling stateLabeling;
 
        // The Markovian states.
        storm::storage::BitVector markovianStates;
 
        // The exit rates.
        std::vector<ValueType> exitRates;
 
        // A vector that stores a labeling for each choice.
        boost::optional<storm::models::sparse::ChoiceLabeling> choiceLabeling;
 
        // A flag indicating if the model is deterministic.
        bool deterministicModel;
    };
 
    // A class holding the information for building the transition matrix.
    class MatrixBuilder {
       public:
        // Constructor
        MatrixBuilder(bool canHaveNondeterminism);
 
        void setRemapping(StateType id) {
            STORM_LOG_ASSERT(id < stateRemapping.size(), "Invalid index for remapping.");
            stateRemapping[id] = currentRowGroup;
        }
 
        void newRowGroup() {
            if (canHaveNondeterminism) {
                builder.newRowGroup(currentRow);
            }
            ++currentRowGroup;
        }
 
        void addTransition(StateType index, ValueType value) {
            builder.addNextValue(currentRow, index, value);
        }
 
        void finishRow() {
            ++currentRow;
        }
 
        void remap() {
            builder.replaceColumns(stateRemapping, mappingOffset);
        }
 
        StateType getCurrentRowGroup() {
            return currentRowGroup;
        }
 
        StateType getRemapping(StateType id) {
            STORM_LOG_ASSERT(id < stateRemapping.size(), "Invalid index for remapping.");
            return stateRemapping[id];
        }
 
        // Matrix builder.
        storm::storage::SparseMatrixBuilder<ValueType> builder;
 
        // Offset to distinguish states which will not be remapped anymore and those which will.
        size_t mappingOffset;
 
        // A mapping from state ids to the row group indices in which they actually reside.
        // TODO: avoid hack with fixed int type
        std::vector<uint_fast64_t> stateRemapping;
 
       private:
        // Index of the current row group.
        StateType currentRowGroup;
 
        // Index of the current row.
        StateType currentRow;
 
        // Flag indicating if row groups are needed.
        bool canHaveNondeterminism;
    };
 
   public:
    ExplicitDFTModelBuilder(storm::dft::storage::DFT<ValueType> const& dft, storm::dft::storage::DftSymmetries const& symmetries);
 
    void buildModel(size_t iteration, double approximationThreshold = 0.0,
                    storm::dft::builder::ApproximationHeuristic approximationHeuristic = storm::dft::builder::ApproximationHeuristic::DEPTH);
 
    std::shared_ptr<storm::models::sparse::Model<ValueType>> getModel();
 
    std::shared_ptr<storm::models::sparse::Model<ValueType>> getModelApproximation(bool lowerBound, bool expectedTime);
 
   private:
    void exploreStateSpace(double approximationThreshold);
 
    void initializeNextIteration();
 
    void buildLabeling();
 
    StateType getOrAddStateIndex(DFTStatePointer const& state);
 
    void setMarkovian(bool markovian);
 
    void changeMatrixBound(storm::storage::SparseMatrix<ValueType>& matrix, bool lowerBound) const;
 
    ValueType getLowerBound(DFTStatePointer const& state) const;
 
    ValueType getUpperBound(DFTStatePointer const& state) const;
 
    ValueType computeMTTFAnd(std::vector<ValueType> const& rates, size_t size) const;
 
    bool isPriorityGreater(StateType idA, StateType idB) const;
 
    void printNotExplored() const;
 
    std::shared_ptr<storm::models::sparse::Model<ValueType>> createModel(bool copy);
 
    // Initial size of the bitvector.
    const size_t INITIAL_BITVECTOR_SIZE = 20000;
    // Offset used for pseudo states.
    const StateType OFFSET_PSEUDO_STATE = std::numeric_limits<StateType>::max() / 2;
 
    // Dft
    storm::dft::storage::DFT<ValueType> const& dft;
 
    // General information for state generation
    // TODO: use const reference
    std::shared_ptr<storm::dft::storage::DFTStateGenerationInfo> stateGenerationInfo;
 
    // Heuristic used for approximation
    storm::dft::builder::ApproximationHeuristic usedHeuristic;
 
    // Current id for new state
    size_t newIndex = 0;
 
    // Whether to use a unique state for all failed states
    // If used, the unique failed state has the id 0
    bool uniqueFailedState = false;
 
    // Id of initial state
    size_t initialStateIndex = 0;
 
    // Next state generator for exploring the state space
    storm::dft::generator::DftNextStateGenerator<ValueType, StateType> generator;
 
    // Structure for the components of the model.
    ModelComponents modelComponents;
 
    // Structure for the transition matrix builder.
    MatrixBuilder matrixBuilder;
 
    // Internal information about the states that were explored.
    storm::storage::sparse::StateStorage<StateType> stateStorage;
 
    // A priority queue of states that still need to be explored.
    storm::dft::storage::BucketPriorityQueue<ExplorationHeuristic> explorationQueue;
 
    // A mapping of not yet explored states from the id to the tuple (state object, heuristic values).
    std::map<StateType, std::pair<DFTStatePointer, ExplorationHeuristicPointer>> statesNotExplored;
 
    // Holds all skipped states which were not yet expanded. More concretely it is a mapping from matrix indices
    // to the corresponding skipped states.
    // Notice that we need an ordered map here to easily iterate in increasing order over state ids.
    // TODO remove again
    std::map<StateType, std::pair<DFTStatePointer, ExplorationHeuristicPointer>> skippedStates;
 
    // List of independent subtrees and the BEs contained in them.
    std::vector<std::vector<size_t>> subtreeBEs;
};
 
}  // namespace builder
}  // namespace storm::dft