Functions
template<>
void	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	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<typename ValueType >
void	exportDFTToJsonFile (storm::dft::storage::DFT< ValueType > const &dft, std::string const &file)
	Export DFT to JSON file.

template<typename ValueType >
std::string	exportDFTToJsonString (storm::dft::storage::DFT< ValueType > const &dft)
	Export DFT to JSON string.

template<>
void	exportDFTToSMT (storm::dft::storage::DFT< double > const &dft, std::string const &file)

template<>
void	exportDFTToSMT (storm::dft::storage::DFT< storm::RationalFunction > const &dft, std::string const &file)

template<>
void	analyzeDFTSMT (storm::dft::storage::DFT< double > const &dft, bool printOutput)

template<>
void	analyzeDFTSMT (storm::dft::storage::DFT< storm::RationalFunction > const &dft, bool printOutput)

template<>
std::pair< std::shared_ptr< storm::gspn::GSPN >, uint64_t >	transformToGSPN (storm::dft::storage::DFT< double > const &dft)

template<>
std::pair< std::shared_ptr< storm::gspn::GSPN >, uint64_t >	transformToGSPN (storm::dft::storage::DFT< storm::RationalFunction > const &dft)

std::shared_ptr< storm::jani::Model >	transformToJani (storm::gspn::GSPN const &gspn, uint64_t toplevelFailedPlace)
	Transform GSPN to Jani model.

storm::dft::utility::RelevantEvents	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 void	exportDFTToJsonFile (storm::dft::storage::DFT< double > const &, std::string const &)

template std::string	exportDFTToJsonString (storm::dft::storage::DFT< double > const &)

template void	exportDFTToJsonFile (storm::dft::storage::DFT< storm::RationalFunction > const &, std::string const &)

template std::string	exportDFTToJsonString (storm::dft::storage::DFT< storm::RationalFunction > const &)

template<typename ValueType >
std::shared_ptr< storm::dft::storage::DFT< ValueType > >	loadDFTGalileoFile (std::string const &file)
	Load DFT from Galileo file.

template<typename ValueType >
std::shared_ptr< storm::dft::storage::DFT< ValueType > >	loadDFTJsonString (std::string const &jsonString)
	Load DFT from JSON string.

template<typename ValueType >
std::shared_ptr< storm::dft::storage::DFT< ValueType > >	loadDFTJsonFile (std::string const &file)
	Load DFT from JSON file.

template<typename ValueType >
std::pair< bool, std::string >	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 > >	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 > >	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 >	computeBEFailureBounds (storm::dft::storage::DFT< ValueType > const &dft, bool useSMT, double solverTimeout)

template<typename ValueType >
bool	computeDependencyConflicts (storm::dft::storage::DFT< ValueType > &dft, bool useSMT, double solverTimeout)

template<typename ValueType >
storm::dft::modelchecker::DFTModelChecker< ValueType >::dft_results	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	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	analyzeDFTSMT (storm::dft::storage::DFT< ValueType > const &dft, bool printOutput)
	Analyze the DFT using the SMT encoding.

template<typename ValueType >
void	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 >	transformToGSPN (storm::dft::storage::DFT< ValueType > const &dft)
	Transform DFT to GSPN.

Function Documentation

◆ analyzeDFT()

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.

First the Markov model is built from the DFT and then this model is checked against the given properties.

Parameters

dft	DFT.
properties	PCTL formulas capturing the properties to check.
symred	Flag whether symmetry reduction should be used.
allowModularisation	Flag whether modularisation should be applied if possible.
relevantEvents	Relevant events which should be observed.
allowDCForRelevant	Whether to allow Don't Care propagation for relevant events
approximationError	Allowed approximation error. Value 0 indicates no approximation.
approximationHeuristic	Heuristic used for state space exploration.
eliminateChains	If true, chains of non-Markovian states are eliminated from the resulting MA.
labelBehavior	Behavior of labels of eliminated states
printOutput	If true, model information, timings, results, etc. are printed.

Returns: Results.

Definition at line 169 of file storm-dft.h.

◆ analyzeDFTBdd() [1/3]

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
	)

Definition at line 23 of file storm-dft.cpp.

◆ analyzeDFTBdd() [2/3]

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
	)

Definition at line 165 of file storm-dft.cpp.

◆ analyzeDFTBdd() [3/3]

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.

Parameters

dft	DFT
exportToDot	If true exports the bdd representing the top level event of the dft in the dot format
filename	The name of the file for exporting to dot
calculateMTTF	If true calculates the mean time to failure

@parameter mttfPrecision A constant that is used to determine if the mttf calculation converged

@parameter mttfStepsize A constant that is used in the mttf calculation

@parameter mttfAlgorithmName The name of the mttf algorithm to use

Parameters

calculateMCS	If true calculates the minimal cut sets
calculateProbability	If true calculates the system failure propbability
useModularisation	If true tries modularisation
importanceMeasureName	The name of the importance measure to calculate
timepoints	The timebounds for probability calculations
properties	The bounded until formulas to check (emulating the CTMC method)
additionalRelevantEventNames	A vector of relevant events to be considered
chunksize	The size of the chunks of doubles to work on at a time

◆ analyzeDFTSMT() [1/3]

template<>

void storm::dft::api::analyzeDFTSMT	(	storm::dft::storage::DFT< double > const &	dft,
		bool	printOutput
	)

Definition at line 198 of file storm-dft.cpp.

◆ analyzeDFTSMT() [2/3]

template<>

void storm::dft::api::analyzeDFTSMT	(	storm::dft::storage::DFT< storm::RationalFunction > const &	dft,
		bool	printOutput
	)

Definition at line 210 of file storm-dft.cpp.

◆ analyzeDFTSMT() [3/3]

template<typename ValueType >

void storm::dft::api::analyzeDFTSMT	(	storm::dft::storage::DFT< ValueType > const &	dft,
		bool	printOutput
	)

Analyze the DFT using the SMT encoding.

Parameters

dft DFT.

Returns: Result result vector

◆ applyTransformations()

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.

Parameters

dft	DFT.
uniqueBE	Flag whether a unique constant failed BE is created.
binaryFDEP	Flag whether all dependencies should be binary (only one dependent child).
exponentialDistributions	Flag whether distributions should be transformed to exponential distributions (if possible).

Returns: Transformed DFT.

Definition at line 85 of file storm-dft.h.

◆ computeBEFailureBounds()

template<typename ValueType >

std::pair< uint64_t, uint64_t > storm::dft::api::computeBEFailureBounds	(	storm::dft::storage::DFT< ValueType > const &	dft,
		bool	useSMT,
		double	solverTimeout
	)

Definition at line 112 of file storm-dft.h.

◆ computeDependencyConflicts()

template<typename ValueType >

bool storm::dft::api::computeDependencyConflicts	(	storm::dft::storage::DFT< ValueType > &	dft,
		bool	useSMT,
		double	solverTimeout
	)

Definition at line 119 of file storm-dft.h.

◆ computeRelevantEvents()

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.

Parameters

properties	List of properties. All events occurring in a property are relevant.
additionalRelevantEventNames	List of names of additional relevant events.

Returns: Relevant events.

Definition at line 266 of file storm-dft.cpp.

◆ exportDFTToJsonFile() [1/3]

template void storm::dft::api::exportDFTToJsonFile	(	storm::dft::storage::DFT< double > const &	,
		std::string const &
	)

◆ exportDFTToJsonFile() [2/3]

template void storm::dft::api::exportDFTToJsonFile	(	storm::dft::storage::DFT< storm::RationalFunction > const &	,
		std::string const &
	)

◆ exportDFTToJsonFile() [3/3]

template<typename ValueType >

void storm::dft::api::exportDFTToJsonFile	(	storm::dft::storage::DFT< ValueType > const &	dft,
		std::string const &	file
	)

Export DFT to JSON file.

Parameters

dft	DFT.
file	File.

Definition at line 174 of file storm-dft.cpp.

◆ exportDFTToJsonString() [1/3]

template std::string storm::dft::api::exportDFTToJsonString ( storm::dft::storage::DFT< double > const & )

◆ exportDFTToJsonString() [2/3]

template std::string storm::dft::api::exportDFTToJsonString ( storm::dft::storage::DFT< storm::RationalFunction > const & )

◆ exportDFTToJsonString() [3/3]

template<typename ValueType >

std::string storm::dft::api::exportDFTToJsonString ( storm::dft::storage::DFT< ValueType > const & dft )

Export DFT to JSON string.

Parameters

dft DFT.

Returns: DFT in JSON format.

Definition at line 179 of file storm-dft.cpp.

◆ exportDFTToSMT() [1/3]

template<>

void storm::dft::api::exportDFTToSMT	(	storm::dft::storage::DFT< double > const &	dft,
		std::string const &	file
	)

Definition at line 186 of file storm-dft.cpp.

◆ exportDFTToSMT() [2/3]

template<>

void storm::dft::api::exportDFTToSMT	(	storm::dft::storage::DFT< storm::RationalFunction > const &	dft,
		std::string const &	file
	)

Definition at line 193 of file storm-dft.cpp.

◆ exportDFTToSMT() [3/3]

template<typename ValueType >

void storm::dft::api::exportDFTToSMT	(	storm::dft::storage::DFT< ValueType > const &	dft,
		std::string const &	file
	)

Export DFT to SMT encoding.

Parameters

dft	DFT.
file	File.

◆ isWellFormed()

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.

Parameters

dft	DFT.
validForMarkovianAnalysis	If true, additional checks are performed to check whether the DFT is valid for analysis via Markov models.

Returns: Pair where the first entry is true iff the DFT is well-formed. The second entry contains the error messages for ill-formed parts.

Definition at line 64 of file storm-dft.h.

◆ loadDFTGalileoFile()

template<typename ValueType >

std::shared_ptr< storm::dft::storage::DFT< ValueType > > storm::dft::api::loadDFTGalileoFile ( std::string const & file )

Load DFT from Galileo file.

Parameters

file	File containing DFT description in Galileo format.

Returns: DFT.

Definition at line 30 of file storm-dft.h.

◆ loadDFTJsonFile()

template<typename ValueType >

std::shared_ptr< storm::dft::storage::DFT< ValueType > > storm::dft::api::loadDFTJsonFile ( std::string const & file )

Load DFT from JSON file.

Parameters

file	File containing DFT description in JSON format.

Returns: DFT.

Definition at line 52 of file storm-dft.h.

◆ loadDFTJsonString()

template<typename ValueType >

std::shared_ptr< storm::dft::storage::DFT< ValueType > > storm::dft::api::loadDFTJsonString ( std::string const & jsonString )

Load DFT from JSON string.

Parameters

jsonString String containing DFT description in JSON format.

Returns: DFT.

Definition at line 41 of file storm-dft.h.

◆ prepareForMarkovAnalysis()

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.

Parameters

dft DFT.

Returns: Transformed DFT.

Definition at line 107 of file storm-dft.h.

◆ transformToGSPN() [1/3]

template<>

std::pair< std::shared_ptr< storm::gspn::GSPN >, uint64_t > storm::dft::api::transformToGSPN ( storm::dft::storage::DFT< double > const & dft )

Definition at line 215 of file storm-dft.cpp.

◆ transformToGSPN() [2/3]

template<>

std::pair< std::shared_ptr< storm::gspn::GSPN >, uint64_t > storm::dft::api::transformToGSPN ( storm::dft::storage::DFT< storm::RationalFunction > const & dft )

Definition at line 238 of file storm-dft.cpp.

◆ transformToGSPN() [3/3]

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.

Parameters

dft DFT.

Returns: Pair of GSPN and id of failed place corresponding to the top level element.

◆ transformToJani()

std::shared_ptr< storm::jani::Model > storm::dft::api::transformToJani	(	storm::gspn::GSPN const &	gspn,
		uint64_t	toplevelFailedPlace
	)

Transform GSPN to Jani model.

Parameters

gspn	GSPN.
toplevelFailedPlace	Id of the failed place in the GSPN for the top level element in the DFT.

Returns: JANI model.

Definition at line 242 of file storm-dft.cpp.

Functions

Function Documentation

◆ analyzeDFT()

◆ analyzeDFTBdd() [1/3]

◆ analyzeDFTBdd() [2/3]

◆ analyzeDFTBdd() [3/3]

◆ analyzeDFTSMT() [1/3]

◆ analyzeDFTSMT() [2/3]

◆ analyzeDFTSMT() [3/3]

◆ applyTransformations()

◆ computeBEFailureBounds()

◆ computeDependencyConflicts()

◆ computeRelevantEvents()

◆ exportDFTToJsonFile() [1/3]

◆ exportDFTToJsonFile() [2/3]

◆ exportDFTToJsonFile() [3/3]

◆ exportDFTToJsonString() [1/3]

◆ exportDFTToJsonString() [2/3]

◆ exportDFTToJsonString() [3/3]

◆ exportDFTToSMT() [1/3]

◆ exportDFTToSMT() [2/3]

◆ exportDFTToSMT() [3/3]

◆ isWellFormed()

◆ loadDFTGalileoFile()

◆ loadDFTJsonFile()

◆ loadDFTJsonString()

◆ prepareForMarkovAnalysis()

◆ transformToGSPN() [1/3]

◆ transformToGSPN() [2/3]

◆ transformToGSPN() [3/3]

◆ transformToJani()