FailureBoundFinder.h

Go to the documentation of this file.

#pragma once
 
#include "storm-dft/modelchecker/DFTASFChecker.h"
#include "storm-dft/storage/DFT.h"
 
namespace storm::dft {
namespace utility {
 
class FailureBoundFinder {
   public:
    static uint64_t getLeastFailureBound(storm::dft::storage::DFT<double> const &dft, bool useSMT = false, uint_fast64_t timeout = 10);
 
    static uint64_t getLeastFailureBound(storm::dft::storage::DFT<storm::RationalFunction> const &dft, bool useSMT = false, uint_fast64_t timeout = 10);
 
    static uint64_t getAlwaysFailedBound(storm::dft::storage::DFT<double> const &dft, bool useSMT = false, uint_fast64_t timeout = 10);
 
    static uint64_t getAlwaysFailedBound(storm::dft::storage::DFT<storm::RationalFunction> const &dft, bool useSMT = false, uint_fast64_t timeout = 10);
 
   private:
    static uint64_t correctLowerBound(std::shared_ptr<storm::dft::modelchecker::DFTASFChecker> smtchecker, uint64_t bound, uint_fast64_t timeout);
 
    static uint64_t correctUpperBound(std::shared_ptr<storm::dft::modelchecker::DFTASFChecker> smtchecker, uint64_t bound, uint_fast64_t timeout);
};
 
}  // namespace utility
}  // namespace storm::dft