DftToGspnTransformator.h

Go to the documentation of this file.

#pragma once
 
#include "storm-dft/storage/DFT.h"
#include "storm-gspn/storage/gspn/GSPN.h"
#include "storm-gspn/storage/gspn/GspnBuilder.h"
 
namespace storm::dft {
namespace transformations {
 
template<typename ValueType>
class DftToGspnTransformator {
   public:
    DftToGspnTransformator(storm::dft::storage::DFT<ValueType> const &dft);
 
    void transform(std::map<uint64_t, uint64_t> const &priorities, std::set<uint64_t> const &dontCareElements, bool smart = true, bool mergeDCFailed = true,
                   bool extendPriorities = false);
 
    std::map<uint64_t, uint64_t> computePriorities(bool extendedPrio);
 
    gspn::GSPN *obtainGSPN();
 
    uint64_t toplevelFailedPlaceId();
 
   private:
    void translateGSPNElements();
 
    void translateBE(std::shared_ptr<storm::dft::storage::elements::DFTBE<ValueType> const> dftBE);
 
    void translateBEExponential(std::shared_ptr<storm::dft::storage::elements::BEExponential<ValueType> const> dftBE);
 
    void translateBEConst(std::shared_ptr<storm::dft::storage::elements::BEConst<ValueType> const> dftConst);
 
    void translateAND(std::shared_ptr<storm::dft::storage::elements::DFTAnd<ValueType> const> dftAnd);
 
    void translateOR(std::shared_ptr<storm::dft::storage::elements::DFTOr<ValueType> const> dftOr);
 
    void translateVOT(std::shared_ptr<storm::dft::storage::elements::DFTVot<ValueType> const> dftVot);
 
    void translatePAND(std::shared_ptr<storm::dft::storage::elements::DFTPand<ValueType> const> dftPand, bool inclusive = true);
 
    void translatePOR(std::shared_ptr<storm::dft::storage::elements::DFTPor<ValueType> const> dftPor, bool inclusive = true);
 
    void translateSPARE(std::shared_ptr<storm::dft::storage::elements::DFTSpare<ValueType> const> dftSpare);
 
    void translatePDEP(std::shared_ptr<storm::dft::storage::elements::DFTDependency<ValueType> const> dftDependency);
 
    void translateSeq(std::shared_ptr<storm::dft::storage::elements::DFTSeq<ValueType> const> dftSeq);
 
    bool isActiveInitially(std::shared_ptr<storm::dft::storage::elements::DFTElement<ValueType> const> dFTElement);
 
    uint64_t getFailPriority(std::shared_ptr<storm::dft::storage::elements::DFTElement<ValueType> const> dFTElement);
 
    uint64_t addFailedPlace(std::shared_ptr<storm::dft::storage::elements::DFTElement<ValueType> const> dftElement, storm::gspn::LayoutInfo const &layoutInfo,
                            bool initialFailed = false);
 
    uint64_t addUnavailablePlace(std::shared_ptr<storm::dft::storage::elements::DFTElement<ValueType> const> dftElement,
                                 storm::gspn::LayoutInfo const &layoutInfo, bool initialAvailable = true);
 
    uint64_t addDisabledPlace(std::shared_ptr<storm::dft::storage::elements::DFTBE<ValueType> const> dftBe, storm::gspn::LayoutInfo const &layoutInfo);
 
    uint64_t addDontcareTransition(std::shared_ptr<storm::dft::storage::elements::DFTElement<ValueType> const> dftElement,
                                   storm::gspn::LayoutInfo const &layoutInfo);
 
    uint64_t getFailedPlace(std::shared_ptr<storm::dft::storage::elements::DFTElement<ValueType> const> dftElement) {
        return failedPlaces.at(dftElement->id());
    }
 
    storm::dft::storage::DFT<ValueType> const &mDft;
    storm::gspn::GspnBuilder builder;
 
    // Transformation options
    // Flag indicating if smart semantics should be used. Smart semantics will only generate necessary parts of the GSPNs.
    bool smart;
    // Flag indicating if Don't Care places and Failed places should be merged.
    bool mergedDCFailed;
    // Flag indicating if extended priorities should be used for extended GreatSPN compatibility
    bool extendedPriorities;
    // Set of DFT elements which should have Don't Care propagation.
    std::set<uint64_t> dontCareElements;
    // Map from DFT elements to their GSPN priorities
    std::map<uint64_t, uint64_t> priorities;
    // Priority for Don't Care Transitions
    uint64_t dontCarePriority;
 
    // Interface places for DFT elements
    std::vector<uint64_t> failedPlaces;
    std::map<uint64_t, uint64_t> unavailablePlaces;
    std::map<uint64_t, uint64_t> activePlaces;
    std::map<uint64_t, uint64_t> disabledPlaces;
    std::map<uint64_t, uint64_t> dependencyPropagationPlaces;
    std::map<uint64_t, uint64_t> dontcareTransitions;
 
    static constexpr const char *STR_FAILING =
        "_failing";  // Name standard for transitions that point towards a place, which in turn indicates the failure of a gate.
    static constexpr const char *STR_FAILED = "_failed";  // Name standard for place which indicates the failure of a gate.
    static constexpr const char *STR_FAILSAVING =
        "_failsaving";  // Name standard for transition that point towards a place, which in turn indicates the failsave state of a gate.
    static constexpr const char *STR_FAILSAVE = "_failsave";  // Name standard for place which indicates the failsave state of a gate.
    static constexpr const char *STR_ACTIVATING =
        "_activating";                                        // Name standard for transition that point towards a place, which in turn indicates its activity.
    static constexpr const char *STR_ACTIVATED = "_active";   // Name standard for place which indicates the activity.
    static constexpr const char *STR_DONTCARE = "_dontcare";  // Name standard for place which indicates Don't Care.
};
 
}  // namespace transformations
}  // namespace storm::dft