Functions
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<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<>
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<>
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::storage::DFT< double > const &, std::vector< std::shared_ptr< storm::logic::Formula const > > const &, bool, bool, storm::dft::utility::RelevantEvents const &, bool, double, storm::dft::builder::ApproximationHeuristic, bool, storm::transformer::EliminationLabelBehavior, bool)
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::storage::DFT< storm::RationalFunction > const &, std::vector< std::shared_ptr< storm::logic::Formula const > > const &, bool, bool, storm::dft::utility::RelevantEvents const &, bool, double, storm::dft::builder::ApproximationHeuristic, bool, storm::transformer::EliminationLabelBehavior, bool)
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 (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)
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.
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.
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 storm::dft::modelchecker::DFTModelChecker< double >::dft_results storm::dft::api::analyzeDFT	(	storm::dft::storage::DFT< double > const &	,
		std::vector< std::shared_ptr< storm::logic::Formula const > > const &	,
		bool	,
		bool	,
		storm::dft::utility::RelevantEvents const &	,
		bool	,
		double	,
		storm::dft::builder::ApproximationHeuristic	,
		bool	,
		storm::transformer::EliminationLabelBehavior	,
		bool	)

◆ analyzeDFT() [2/3]

template storm::dft::modelchecker::DFTModelChecker< storm::RationalFunction >::dft_results storm::dft::api::analyzeDFT	(	storm::dft::storage::DFT< storm::RationalFunction > const &	,
		std::vector< std::shared_ptr< storm::logic::Formula const > > const &	,
		bool	,
		bool	,
		storm::dft::utility::RelevantEvents const &	,
		bool	,
		double	,
		storm::dft::builder::ApproximationHeuristic	,
		bool	,
		storm::transformer::EliminationLabelBehavior	,
		bool	)

◆ analyzeDFT() [3/3]

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

◆ 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 45 of file analysis.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 193 of file analysis.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
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 202 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 214 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 219 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 226 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 )

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

Definition at line 17 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 )

Definition at line 40 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 )

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 44 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()