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/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, bool addLabelsClaiming)
	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::DftEnvironment const &env, storm::dft::storage::DFT< ValueType > const &dft, std::vector< std::shared_ptr< storm::logic::Formula const > > const &properties, storm::dft::utility::RelevantEvents const &relevantEvents={}, bool printOutput=false, typename storm::dft::modelchecker::DFTModelChecker< ValueType >::ModelExportCallback const &exportCallback={})
	Compute the exact or approximate analysis result of the given DFT according to the given properties.
template<>
void	storm::dft::api::analyzeDFTBdd (storm::dft::DftEnvironment const &env, 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 (storm::dft::DftEnvironment const &, 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::DftEnvironment const &, storm::dft::storage::DFT< double > const &, std::vector< std::shared_ptr< storm::logic::Formula const > > const &, storm::dft::utility::RelevantEvents const &, bool, typename storm::dft::modelchecker::DFTModelChecker< double >::ModelExportCallback const &)
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::DftEnvironment const &, storm::dft::storage::DFT< storm::RationalFunction > const &, std::vector< std::shared_ptr< storm::logic::Formula const > > const &, storm::dft::utility::RelevantEvents const &, bool, typename storm::dft::modelchecker::DFTModelChecker< storm::RationalFunction >::ModelExportCallback const &)
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)