analysis.cpp File Reference

#include "analysis.h"
#include <memory>
#include <vector>
#include "storm-dft/adapters/SFTBDDPropertyFormulaAdapter.h"
#include "storm-dft/modelchecker/DftModularizationChecker.h"
#include "storm-dft/modelchecker/SFTBDDChecker.h"
#include "storm-dft/settings/modules/FaultTreeSettings.h"
#include "storm-dft/storage/DFT.h"
#include "storm-dft/storage/SylvanBddManager.h"
#include "storm-dft/utility/FDEPConflictFinder.h"
#include "storm-dft/utility/FailureBoundFinder.h"
#include "storm-dft/utility/MTTFHelper.h"
#include "storm/adapters/RationalFunctionAdapter.h"

Include dependency graph for analysis.cpp:

Go to the source code of this file.

Namespaces
namespace	storm
namespace	storm::dft
namespace	storm::dft::api

Functions
storm::dft::utility::RelevantEvents	storm::dft::api::computeRelevantEvents (std::vector< std::shared_ptr< storm::logic::Formula const > > const &properties, std::vector< std::string > const &additionalRelevantEventNames)
	Get relevant event ids from given relevant event names and labels in properties.
template<typename ValueType>
storm::dft::modelchecker::DFTModelChecker< ValueType >::dft_results	storm::dft::api::analyzeDFT (storm::dft::storage::DFT< ValueType > const &dft, std::vector< std::shared_ptr< storm::logic::Formula const > > 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, bool printOutput=false)
	Compute the exact or approximate analysis result of the given DFT according to the given properties.
template<>
void	storm::dft::api::analyzeDFTBdd (std::shared_ptr< storm::dft::storage::DFT< double > > const &dft, bool const exportToDot, std::string const &filename, bool const calculateMttf, double const mttfPrecision, double const mttfStepsize, std::string const mttfAlgorithmName, bool const calculateMCS, bool const calculateProbability, bool const useModularisation, std::string const importanceMeasureName, std::vector< double > const &timepoints, std::vector< std::shared_ptr< storm::logic::Formula const > > const &properties, std::vector< std::string > const &additionalRelevantEventNames, size_t const chunksize)
template<>
void	storm::dft::api::analyzeDFTBdd (std::shared_ptr< storm::dft::storage::DFT< storm::RationalFunction > > const &dft, bool const exportToDot, std::string const &filename, bool const calculateMttf, double const mttfPrecision, double const mttfStepsize, std::string const mttfAlgorithmName, bool const calculateMCS, bool const calculateProbability, bool const useModularisation, std::string const importanceMeasureName, std::vector< double > const &timepoints, std::vector< std::shared_ptr< storm::logic::Formula const > > const &properties, std::vector< std::string > const &additionalRelevantEventNames, size_t const chunksize)
template<>
void	storm::dft::api::analyzeDFTSMT (storm::dft::storage::DFT< double > const &dft, bool printOutput)
template<>
void	storm::dft::api::analyzeDFTSMT (storm::dft::storage::DFT< storm::RationalFunction > const &dft, bool printOutput)
template<typename ValueType>
std::pair< uint64_t, uint64_t >	storm::dft::api::computeBEFailureBounds (storm::dft::storage::DFT< ValueType > const &dft, bool useSMT, double solverTimeout)
template<typename ValueType>
bool	storm::dft::api::computeDependencyConflicts (storm::dft::storage::DFT< ValueType > &dft, bool useSMT, double solverTimeout)
template storm::dft::modelchecker::DFTModelChecker< double >::dft_results	storm::dft::api::analyzeDFT (storm::dft::storage::DFT< double > const &, std::vector< std::shared_ptr< storm::logic::Formula const > > const &, bool, bool, storm::dft::utility::RelevantEvents const &, bool, double, storm::dft::builder::ApproximationHeuristic, bool, storm::transformer::EliminationLabelBehavior, bool)
template std::pair< uint64_t, uint64_t >	storm::dft::api::computeBEFailureBounds (storm::dft::storage::DFT< double > const &, bool, double)
template bool	storm::dft::api::computeDependencyConflicts (storm::dft::storage::DFT< double > &, bool, double)
template storm::dft::modelchecker::DFTModelChecker< storm::RationalFunction >::dft_results	storm::dft::api::analyzeDFT (storm::dft::storage::DFT< storm::RationalFunction > const &, std::vector< std::shared_ptr< storm::logic::Formula const > > const &, bool, bool, storm::dft::utility::RelevantEvents const &, bool, double, storm::dft::builder::ApproximationHeuristic, bool, storm::transformer::EliminationLabelBehavior, bool)
template std::pair< uint64_t, uint64_t >	storm::dft::api::computeBEFailureBounds (storm::dft::storage::DFT< storm::RationalFunction > const &, bool, double)
template bool	storm::dft::api::computeDependencyConflicts (storm::dft::storage::DFT< storm::RationalFunction > &, bool, double)