DFTModelChecker.h

Go to the documentation of this file.

#pragma once
 
#include <boost/variant.hpp>
#include <functional>
 
#include "storm-dft/environment/DftEnvironment.h"
#include "storm-dft/storage/DFT.h"
#include "storm-dft/utility/RelevantEvents.h"
#include "storm/logic/Formula.h"
#include "storm/transformer/NonMarkovianChainTransformer.h"
#include "storm/utility/ExtendedNumber.h"
#include "storm/utility/Stopwatch.h"
 
namespace storm::dft {
namespace modelchecker {

template<typename ValueType>
class DFTModelChecker {
   public:
    typedef storm::utility::ExtendedValueType<ValueType> ExtendedValueType;
    typedef std::pair<ExtendedValueType, ExtendedValueType> approximation_result;
    typedef std::vector<boost::variant<ExtendedValueType, approximation_result>> dft_results;
    typedef std::vector<std::shared_ptr<storm::logic::Formula const>> property_vector;

    using ModelExportCallback = std::function<void(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, bool isFinal)>;
 
    class ResultOutputVisitor : public boost::static_visitor<> {
       public:
        void operator()(ExtendedValueType const& result, std::ostream& os) const {
            os << result;
        }
 
        void operator()(approximation_result const& result, std::ostream& os) const {
            os << "(" << result.first << ", " << result.second << ")";
        }
    };

    DFTModelChecker(bool printOutput, ModelExportCallback exportCallback = {}) : printInfo(printOutput), exportCallback(std::move(exportCallback)) {}

    dft_results check(storm::dft::DftEnvironment const& env, storm::dft::storage::DFT<ValueType> const& origDft, property_vector const& properties,
                      storm::dft::utility::RelevantEvents const& relevantEvents = {});

    void printTimings(std::ostream& os = std::cout) const;

    void printResults(dft_results const& results, std::ostream& os = std::cout) const;
 
   private:
    bool printInfo;
    ModelExportCallback exportCallback;
 
    // 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::DftEnvironment const& env, storm::dft::storage::DFT<ValueType> const& dft, property_vector const& properties,
                            storm::dft::utility::RelevantEvents const& relevantEvents);

    std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> buildModelViaComposition(storm::dft::DftEnvironment const& env,
                                                                                     storm::dft::storage::DFT<ValueType> const& dft,
                                                                                     property_vector const& properties,
                                                                                     storm::dft::utility::RelevantEvents const& relevantEvents);

    dft_results checkDFT(storm::dft::DftEnvironment const& env, storm::dft::storage::DFT<ValueType> const& dft, property_vector const& properties,
                         storm::dft::utility::RelevantEvents const& relevantEvents);

    std::vector<ExtendedValueType> checkModel(storm::dft::DftEnvironment const& env, 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