storm-dft.h File Reference

#include <type_traits>
#include <utility>
#include <vector>
#include "storm-dft/modelchecker/DFTASFChecker.h"
#include "storm-dft/modelchecker/DFTModelChecker.h"
#include "storm-dft/parser/DFTGalileoParser.h"
#include "storm-dft/parser/DFTJsonParser.h"
#include "storm-dft/transformations/DftToGspnTransformator.h"
#include "storm-dft/transformations/DftTransformer.h"
#include "storm-dft/utility/DftValidator.h"
#include "storm-dft/utility/FDEPConflictFinder.h"
#include "storm-dft/utility/FailureBoundFinder.h"
#include "storm-dft/utility/RelevantEvents.h"
#include "storm-gspn/api/storm-gspn.h"

Include dependency graph for storm-dft.h:

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

Go to the source code of this file.

Namespaces
namespace	storm
	LabParser.cpp.
namespace	storm::dft
namespace	storm::dft::api

Functions
template<typename ValueType >
std::shared_ptr< storm::dft::storage::DFT< ValueType > >	storm::dft::api::loadDFTGalileoFile (std::string const &file)
	Load DFT from Galileo file.
template<typename ValueType >
std::shared_ptr< storm::dft::storage::DFT< ValueType > >	storm::dft::api::loadDFTJsonString (std::string const &jsonString)
	Load DFT from JSON string.
template<typename ValueType >
std::shared_ptr< storm::dft::storage::DFT< ValueType > >	storm::dft::api::loadDFTJsonFile (std::string const &file)
	Load DFT from JSON file.
template<typename ValueType >
std::pair< bool, std::string >	storm::dft::api::isWellFormed (storm::dft::storage::DFT< ValueType > const &dft, bool validForMarkovianAnalysis=true)
	Check whether the DFT is well-formed.
template<typename ValueType >
std::shared_ptr< storm::dft::storage::DFT< ValueType > >	storm::dft::api::applyTransformations (storm::dft::storage::DFT< ValueType > const &dft, bool uniqueBE, bool binaryFDEP, bool exponentialDistributions)
	Apply transformations for DFT.
template<typename ValueType >
std::shared_ptr< storm::dft::storage::DFT< ValueType > >	storm::dft::api::prepareForMarkovAnalysis (storm::dft::storage::DFT< ValueType > const &dft)
	Apply transformations to make DFT feasible for Markovian analysis.
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)
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 >
void	storm::dft::api::exportDFTToJsonFile (storm::dft::storage::DFT< ValueType > const &dft, std::string const &file)
	Export DFT to JSON file.
template<typename ValueType >
std::string	storm::dft::api::exportDFTToJsonString (storm::dft::storage::DFT< ValueType > const &dft)
	Export DFT to JSON string.
template<typename ValueType >
void	storm::dft::api::exportDFTToSMT (storm::dft::storage::DFT< ValueType > const &dft, std::string const &file)
	Export DFT to SMT encoding.
template<typename ValueType >
std::pair< std::shared_ptr< storm::gspn::GSPN >, uint64_t >	storm::dft::api::transformToGSPN (storm::dft::storage::DFT< ValueType > const &dft)
	Transform DFT to GSPN.
std::shared_ptr< storm::jani::Model >	storm::dft::api::transformToJani (storm::gspn::GSPN const &gspn, uint64_t toplevelFailedPlace)
	Transform GSPN to Jani model.