DFTModelChecker.h

Go to the documentation of this file.

#pragma once
 
#include "storm/api/storm.h"
#include "storm/logic/Formula.h"
#include "storm/modelchecker/results/CheckResult.h"
#include "storm/utility/Stopwatch.h"
 
#include "storm-dft/storage/DFT.h"
#include "storm-dft/utility/RelevantEvents.h"
 
namespace storm::dft {
namespace modelchecker {
 
template<typename ValueType>
class DFTModelChecker {
   public:
    typedef std::pair<ValueType, ValueType> approximation_result;
    typedef std::vector<boost::variant<ValueType, approximation_result>> dft_results;
    typedef std::vector<std::shared_ptr<storm::logic::Formula const>> property_vector;
 
    class ResultOutputVisitor : public boost::static_visitor<> {
       public:
        void operator()(ValueType result, std::ostream& os) const {
            os << result;
        }
 
        void operator()(std::pair<ValueType, ValueType> const& result, std::ostream& os) const {
            os << "(" << result.first << ", " << result.second << ")";
        }
    };
 
    DFTModelChecker(bool printOutput) : printInfo(printOutput) {}
 
    dft_results check(storm::dft::storage::DFT<ValueType> const& origDft, property_vector const& properties, bool symred = true,
                      bool allowModularisation = true, storm::dft::utility::RelevantEvents const& relevantEvents = {}, bool allowDCForRelevant = false,
                      double approximationError = 0.0,
                      storm::dft::builder::ApproximationHeuristic approximationHeuristic = storm::dft::builder::ApproximationHeuristic::DEPTH,
                      bool eliminateChains = false,
                      storm::transformer::EliminationLabelBehavior labelBehavior = storm::transformer::EliminationLabelBehavior::KeepLabels);
 
    void printTimings(std::ostream& os = std::cout);
 
    void printResults(dft_results const& results, std::ostream& os = std::cout);
 
   private:
    bool printInfo;
 
    // Timing values
    storm::utility::Stopwatch buildingTimer;
    storm::utility::Stopwatch explorationTimer;
    storm::utility::Stopwatch bisimulationTimer;
    storm::utility::Stopwatch modelCheckingTimer;
    storm::utility::Stopwatch totalTimer;
 
    dft_results checkHelper(storm::dft::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred, bool allowModularisation,
                            storm::dft::utility::RelevantEvents const& relevantEvents, bool allowDCForRelevant = false, double approximationError = 0.0,
                            storm::dft::builder::ApproximationHeuristic approximationHeuristic = storm::dft::builder::ApproximationHeuristic::DEPTH,
                            bool eliminateChains = false,
                            storm::transformer::EliminationLabelBehavior labelBehavior = storm::transformer::EliminationLabelBehavior::KeepLabels);
 
    std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> buildModelViaComposition(storm::dft::storage::DFT<ValueType> const& dft,
                                                                                     property_vector const& properties, bool symred, bool allowModularisation,
                                                                                     storm::dft::utility::RelevantEvents const& relevantEvents,
                                                                                     bool allowDCForRelevant);
 
    dft_results checkDFT(storm::dft::storage::DFT<ValueType> const& dft, property_vector const& properties, bool symred,
                         storm::dft::utility::RelevantEvents const& relevantEvents, bool allowDCForRelevant, double approximationError = 0.0,
                         storm::dft::builder::ApproximationHeuristic approximationHeuristic = storm::dft::builder::ApproximationHeuristic::DEPTH,
                         bool eliminateChains = false,
                         storm::transformer::EliminationLabelBehavior labelBehavior = storm::transformer::EliminationLabelBehavior::KeepLabels);
 
    std::vector<ValueType> checkModel(std::shared_ptr<storm::models::sparse::Model<ValueType>>& model, property_vector const& properties);
 
    bool isApproximationSufficient(ValueType lowerBound, ValueType upperBound, double approximationError, bool relative);
};
 
}  // namespace modelchecker
}  // namespace storm::dft