Functions
storm::dft::utility::RelevantEvents	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	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	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	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	analyzeDFTSMT (storm::dft::storage::DFT< double > const &dft, bool printOutput)
template<>
void	analyzeDFTSMT (storm::dft::storage::DFT< storm::RationalFunction > const &dft, bool printOutput)
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 storm::dft::modelchecker::DFTModelChecker< double >::dft_results	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 >	computeBEFailureBounds (storm::dft::storage::DFT< double > const &, bool, double)
template bool	computeDependencyConflicts (storm::dft::storage::DFT< double > &, bool, double)
template storm::dft::modelchecker::DFTModelChecker< storm::RationalFunction >::dft_results	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 >	computeBEFailureBounds (storm::dft::storage::DFT< storm::RationalFunction > const &, bool, double)
template bool	computeDependencyConflicts (storm::dft::storage::DFT< storm::RationalFunction > &, bool, double)
template<typename ValueType>
void	analyzeDFTBdd (storm::dft::DftEnvironment const &env, 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<>
std::pair< std::shared_ptr< storm::gspn::GSPN >, uint64_t >	transformToGSPN (storm::dft::storage::DFT< double > const &dft, bool enableDC, bool extendPriorities, bool enableSmartTransformation, bool mergeDCFailed)
template<>
std::pair< std::shared_ptr< storm::gspn::GSPN >, uint64_t >	transformToGSPN (storm::dft::storage::DFT< storm::RationalFunction > const &dft, bool enableDC, bool extendPriorities, bool enableSmartTransformation, bool mergeDCFailed)
std::pair< std::shared_ptr< storm::jani::Model >, std::vector< storm::jani::Property > >	transformToJani (storm::gspn::GSPN const &gspn, uint64_t toplevelFailedPlace, bool addDeadlockProperties=false)
	Transform GSPN to Jani model.
template<typename ValueType>
std::pair< std::shared_ptr< storm::gspn::GSPN >, uint64_t >	transformToGSPN (storm::dft::storage::DFT< ValueType > const &dft, bool enableDC, bool extendPriorities, bool enableSmartTransformation, bool mergeDCFailed)
	Transform DFT to GSPN.
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>
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 std::shared_ptr< storm::dft::storage::DFT< double > >	loadDFTGalileoFile (std::string const &)
template std::shared_ptr< storm::dft::storage::DFT< double > >	loadDFTJsonString (std::string const &)
template std::shared_ptr< storm::dft::storage::DFT< double > >	loadDFTJsonFile (std::string const &)
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>
void	exportDFTToSMT (storm::dft::storage::DFT< ValueType > const &dft, std::string const &file)
	Export DFT to SMT encoding.
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::pair< bool, std::string >	hasPotentialModelingIssues (storm::dft::storage::DFT< ValueType > const &dft)
	Check whether the DFT has potential modeling issues.
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 std::pair< bool, std::string >	isWellFormed (storm::dft::storage::DFT< double > const &, bool)
template std::pair< bool, std::string >	hasPotentialModelingIssues (storm::dft::storage::DFT< double > const &)
template std::shared_ptr< storm::dft::storage::DFT< double > >	applyTransformations (storm::dft::storage::DFT< double > const &, bool, bool, bool)
template std::shared_ptr< storm::dft::storage::DFT< double > >	prepareForMarkovAnalysis (storm::dft::storage::DFT< double > const &)
template std::pair< bool, std::string >	isWellFormed (storm::dft::storage::DFT< storm::RationalFunction > const &, bool)
template std::pair< bool, std::string >	hasPotentialModelingIssues (storm::dft::storage::DFT< storm::RationalFunction > const &)
template std::shared_ptr< storm::dft::storage::DFT< storm::RationalFunction > >	applyTransformations (storm::dft::storage::DFT< storm::RationalFunction > const &, bool, bool, bool)
template std::shared_ptr< storm::dft::storage::DFT< storm::RationalFunction > >	prepareForMarkovAnalysis (storm::dft::storage::DFT< storm::RationalFunction > const &)

Function Documentation

◆ analyzeDFT() [1/3]

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.

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

Parameters

env	Environment holding the DFT model-checking configuration.
dft	DFT.
properties	PCTL formulas capturing the properties to check.
relevantEvents	Relevant events which should be observed.
printOutput	If true, model information, timings, results, etc. are printed.
exportCallback	If set, invoked whenever a model has been built, to let the caller export it.

Returns: Results.

Definition at line 27 of file analysis.cpp.

◆ analyzeDFT() [2/3]

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 &	)

◆ analyzeDFT() [3/3]

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 &	)

◆ analyzeDFTBdd() [1/3]

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 )

Definition at line 190 of file analysis.cpp.

◆ analyzeDFTBdd() [2/3]

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 )

Definition at line 41 of file analysis.cpp.

◆ analyzeDFTBdd() [3/3]

template<typename ValueType>

void storm::dft::api::analyzeDFTBdd	(	storm::dft::DftEnvironment const &	env,
		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
mttfPrecision	A constant that is used to determine if the mttf calculation converged
mttfStepsize	A constant that is used in the mttf calculation
mttfAlgorithmName	The name of the mttf algorithm to use
calculateMCS	If true calculates the minimal cut sets
calculateProbability	If true calculates the system failure probability
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 200 of file analysis.cpp.

◆ analyzeDFTSMT() [2/3]

template<>

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

Definition at line 212 of file analysis.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.
printOutput	If true, output is printed.

◆ applyTransformations() [1/3]

template std::shared_ptr< storm::dft::storage::DFT< double > > storm::dft::api::applyTransformations	(	storm::dft::storage::DFT< double > const &	,
		bool	,
		bool	,
		bool	)

◆ applyTransformations() [2/3]

template std::shared_ptr< storm::dft::storage::DFT< storm::RationalFunction > > storm::dft::api::applyTransformations	(	storm::dft::storage::DFT< storm::RationalFunction > const &	,
		bool	,
		bool	,
		bool	)

◆ applyTransformations() [3/3]

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 31 of file transformation.cpp.

◆ computeBEFailureBounds() [1/3]

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

◆ computeBEFailureBounds() [2/3]

template std::pair< uint64_t, uint64_t > storm::dft::api::computeBEFailureBounds	(	storm::dft::storage::DFT< storm::RationalFunction > const &	,
		bool	,
		double	)

◆ computeBEFailureBounds() [3/3]

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 217 of file analysis.cpp.

◆ computeDependencyConflicts() [1/3]

template bool storm::dft::api::computeDependencyConflicts	(	storm::dft::storage::DFT< double > &	,
		bool	,
		double	)

◆ computeDependencyConflicts() [2/3]

template bool storm::dft::api::computeDependencyConflicts	(	storm::dft::storage::DFT< storm::RationalFunction > &	,
		bool	,
		double	)

◆ computeDependencyConflicts() [3/3]

template<typename ValueType>

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

Definition at line 224 of file analysis.cpp.

◆ 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,
		bool	addLabelsClaiming )

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.
addLabelsClaiming	Whether labels representing claiming operations are added to the model.

Returns: Relevant events.

Definition at line 19 of file analysis.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 29 of file io.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 34 of file io.cpp.

◆ exportDFTToSMT() [1/3]

template<>

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

Definition at line 41 of file io.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 48 of file io.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.

◆ hasPotentialModelingIssues() [1/3]

template std::pair< bool, std::string > storm::dft::api::hasPotentialModelingIssues ( storm::dft::storage::DFT< double > const & )

◆ hasPotentialModelingIssues() [2/3]

template std::pair< bool, std::string > storm::dft::api::hasPotentialModelingIssues ( storm::dft::storage::DFT< storm::RationalFunction > const & )

◆ hasPotentialModelingIssues() [3/3]

template<typename ValueType>

std::pair< bool, std::string > storm::dft::api::hasPotentialModelingIssues ( storm::dft::storage::DFT< ValueType > const & dft )

Check whether the DFT has potential modeling issues.

Parameters

dft DFT.

Returns: Pair where the first entry is true iff the DFT has potential modeling issues. The second entry contains the warning messages for the issues.

Definition at line 24 of file transformation.cpp.

◆ isWellFormed() [1/3]

template std::pair< bool, std::string > storm::dft::api::isWellFormed	(	storm::dft::storage::DFT< double > const &	,
		bool	)

◆ isWellFormed() [2/3]

template std::pair< bool, std::string > storm::dft::api::isWellFormed	(	storm::dft::storage::DFT< storm::RationalFunction > const &	,
		bool	)

◆ isWellFormed() [3/3]

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 12 of file transformation.cpp.

◆ loadDFTGalileoFile() [1/2]

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 14 of file io.cpp.

◆ loadDFTGalileoFile() [2/2]

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

◆ loadDFTJsonFile() [1/2]

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 24 of file io.cpp.

◆ loadDFTJsonFile() [2/2]

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

◆ loadDFTJsonString() [1/2]

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 19 of file io.cpp.

◆ loadDFTJsonString() [2/2]

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

◆ prepareForMarkovAnalysis() [1/3]

template std::shared_ptr< storm::dft::storage::DFT< double > > storm::dft::api::prepareForMarkovAnalysis ( storm::dft::storage::DFT< double > const & )

◆ prepareForMarkovAnalysis() [2/3]

template std::shared_ptr< storm::dft::storage::DFT< storm::RationalFunction > > storm::dft::api::prepareForMarkovAnalysis ( storm::dft::storage::DFT< storm::RationalFunction > const & )

◆ prepareForMarkovAnalysis() [3/3]

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 47 of file transformation.cpp.

◆ 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,
		bool	enableDC,
		bool	extendPriorities,
		bool	enableSmartTransformation,
		bool	mergeDCFailed )

Definition at line 12 of file gspn_transformation.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,
		bool	enableDC,
		bool	extendPriorities,
		bool	enableSmartTransformation,
		bool	mergeDCFailed )

Definition at line 32 of file gspn_transformation.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,
		bool	enableDC,
		bool	extendPriorities,
		bool	enableSmartTransformation,
		bool	mergeDCFailed )

Transform DFT to GSPN.

Parameters

dft	DFT.
enableDC	Whether Don't Care propagation is enabled.
extendPriorities	Whether calculation of transition priorities is enabled.
enableSmartTransformation	Whether the smart transformation is enabled.
mergeDCFailed	Whether Don't Care and Failed places are merged into a combined place.

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

◆ transformToJani()

std::pair< std::shared_ptr< storm::jani::Model >, std::vector< storm::jani::Property > > storm::dft::api::transformToJani	(	storm::gspn::GSPN const &	gspn,
		uint64_t	toplevelFailedPlace,
		bool	addDeadlockProperties = false )

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.
addDeadlockProperties	Whether deadlock properties are added to the returned properties.

Returns: Pair of JANI model and its properties.

Definition at line 37 of file gspn_transformation.cpp.

Functions

Function Documentation

◆ analyzeDFT() [1/3]

◆ analyzeDFT() [2/3]

◆ analyzeDFT() [3/3]

◆ analyzeDFTBdd() [1/3]

◆ analyzeDFTBdd() [2/3]

◆ analyzeDFTBdd() [3/3]

◆ analyzeDFTSMT() [1/3]

◆ analyzeDFTSMT() [2/3]

◆ analyzeDFTSMT() [3/3]

◆ applyTransformations() [1/3]

◆ applyTransformations() [2/3]

◆ applyTransformations() [3/3]

◆ computeBEFailureBounds() [1/3]

◆ computeBEFailureBounds() [2/3]

◆ computeBEFailureBounds() [3/3]

◆ computeDependencyConflicts() [1/3]

◆ computeDependencyConflicts() [2/3]

◆ computeDependencyConflicts() [3/3]

◆ 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]

◆ hasPotentialModelingIssues() [1/3]

◆ hasPotentialModelingIssues() [2/3]

◆ hasPotentialModelingIssues() [3/3]

◆ isWellFormed() [1/3]

◆ isWellFormed() [2/3]

◆ isWellFormed() [3/3]

◆ loadDFTGalileoFile() [1/2]

◆ loadDFTGalileoFile() [2/2]

◆ loadDFTJsonFile() [1/2]

◆ loadDFTJsonFile() [2/2]

◆ loadDFTJsonString() [1/2]

◆ loadDFTJsonString() [2/2]

◆ prepareForMarkovAnalysis() [1/3]

◆ prepareForMarkovAnalysis() [2/3]

◆ prepareForMarkovAnalysis() [3/3]

◆ transformToGSPN() [1/3]

◆ transformToGSPN() [2/3]

◆ transformToGSPN() [3/3]

◆ transformToJani()