analysis.h File Reference

#include <memory>
#include <string>
#include <utility>
#include <vector>
#include "storm-dft/builder/DftExplorationHeuristic.h"
#include "storm-dft/modelchecker/DFTModelChecker.h"
#include "storm-dft/storage/DFT.h"
#include "storm-dft/utility/RelevantEvents.h"
#include "storm/logic/Formula.h"

Include dependency graph for analysis.h:

This graph shows which files directly or indirectly include this file:

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<typename ValueType>
void	storm::dft::api::analyzeDFTBdd (std::shared_ptr< storm::dft::storage::DFT< ValueType > > 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)
	Analyze the DFT using BDDs.
template<typename ValueType>
void	storm::dft::api::analyzeDFTSMT (storm::dft::storage::DFT< ValueType > const &dft, bool printOutput)
	Analyze the DFT using the SMT encoding.
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)