DFTASFChecker.h

Go to the documentation of this file.

#pragma once
 
#include <string>
#include <unordered_map>
#include <vector>
 
#include "SmtConstraint.h"
#include "storm-dft/storage/DFT.h"
#include "storm/solver/SmtSolver.h"
#include "storm/utility/solver.h"
 
namespace storm::dft {
namespace modelchecker {
 
class SpareAndChildPair {
   public:
    SpareAndChildPair(uint64_t spareIndex, uint64_t childIndex) : spareIndex(spareIndex), childIndex(childIndex) {}
 
    friend bool operator<(SpareAndChildPair const& p1, SpareAndChildPair const& p2) {
        return p1.spareIndex < p2.spareIndex || (p1.spareIndex == p2.spareIndex && p1.childIndex < p2.childIndex);
    }
 
   private:
    uint64_t spareIndex;
    uint64_t childIndex;
};
 
class DependencyPair {
   public:
    DependencyPair(uint64_t depIndex, uint64_t childIndex) : depIndex(depIndex), childIndex(childIndex) {}
 
    friend bool operator<(DependencyPair const& p1, DependencyPair const& p2) {
        return p1.depIndex < p2.depIndex || (p1.depIndex == p2.depIndex && p1.childIndex < p2.childIndex);
    }
 
   private:
    uint64_t depIndex;
    uint64_t childIndex;
};
 
class DFTASFChecker {
    using ValueType = double;
 
   public:
    DFTASFChecker(storm::dft::storage::DFT<ValueType> const&);
 
    void convert();
    void toFile(std::string const&);
 
    void toSolver();
 
    storm::solver::SmtSolver::CheckResult checkTleNeverFailed();
 
    storm::solver::SmtSolver::CheckResult checkTleFailsWithEq(uint64_t bound);
 
    storm::solver::SmtSolver::CheckResult checkTleFailsWithLeq(uint64_t bound);
 
    storm::solver::SmtSolver::CheckResult checkDependencyConflict(uint64_t dep1Index, uint64_t dep2Index, uint64_t timeout = 10);
 
    void setSolverTimeout(uint_fast64_t milliseconds);
 
    void unsetSolverTimeout();
 
    storm::dft::storage::DFT<ValueType> const& getDFT() {
        return dft;
    }
 
    storm::solver::SmtSolver::CheckResult checkFailsLeqWithEqNonMarkovianState(uint64_t checkbound, uint64_t nrNonMarkovian);
 
    storm::solver::SmtSolver::CheckResult checkFailsAtTimepointWithEqNonMarkovianState(uint64_t timepoint, uint64_t nrNonMarkovian);
 
   private:
    uint64_t getClaimVariableIndex(uint64_t spareIndex, uint64_t childIndex) const;
 
    std::shared_ptr<SmtConstraint> generateTryToClaimConstraint(std::shared_ptr<storm::dft::storage::elements::DFTSpare<ValueType> const> spare,
                                                                uint64_t childIndex, uint64_t timepoint) const;
 
    void generateAndConstraint(size_t i, std::vector<uint64_t> childVarIndices,
                               std::shared_ptr<storm::dft::storage::elements::DFTElement<ValueType> const> element);
 
    void generateOrConstraint(size_t i, std::vector<uint64_t> childVarIndices,
                              std::shared_ptr<storm::dft::storage::elements::DFTElement<ValueType> const> element);
 
    void generateVotConstraint(size_t i, std::vector<uint64_t> childVarIndices,
                               std::shared_ptr<storm::dft::storage::elements::DFTElement<ValueType> const> element);
 
    void generatePandConstraint(size_t i, std::vector<uint64_t> childVarIndices,
                                std::shared_ptr<storm::dft::storage::elements::DFTElement<ValueType> const> element);
 
    void generatePorConstraint(size_t i, std::vector<uint64_t> childVarIndices,
                               std::shared_ptr<storm::dft::storage::elements::DFTElement<ValueType> const> element);
 
    void generateSeqConstraint(std::vector<uint64_t> childVarIndices, std::shared_ptr<storm::dft::storage::elements::DFTElement<ValueType> const> element);
 
    void generateSpareConstraint(size_t i, std::vector<uint64_t> childVarIndices,
                                 std::shared_ptr<storm::dft::storage::elements::DFTElement<ValueType> const> element);
 
    void generatePdepConstraint(size_t i, std::vector<uint64_t> childVarIndices,
                                std::shared_ptr<storm::dft::storage::elements::DFTElement<ValueType> const> element);
 
    void addClaimingConstraints();
 
    void addMarkovianConstraints();
 
    storm::dft::storage::DFT<ValueType> const& dft;
    std::shared_ptr<storm::solver::SmtSolver> solver = nullptr;
    std::vector<std::string> varNames;
    std::unordered_map<uint64_t, uint64_t> timePointVariables;
    std::vector<std::shared_ptr<SmtConstraint>> constraints;
    std::map<SpareAndChildPair, uint64_t> claimVariables;
    std::unordered_map<uint64_t, uint64_t> dependencyVariables;
    std::unordered_map<uint64_t, uint64_t> markovianVariables;
    std::vector<uint64_t> tmpTimePointVariables;
    uint64_t notFailed;
};
 
}  // namespace modelchecker
}  // namespace storm::dft