Classes
struct	ModelProcessingInformation

struct	PostprocessingIdentity

struct	SymbolicInput

Typedefs
using	VerificationCallbackType = std::function< std::unique_ptr< storm::modelchecker::CheckResult >(std::shared_ptr< storm::logic::Formula const > const &formula, std::shared_ptr< storm::logic::Formula const > const &states)>

using	PostprocessingCallbackType = std::function< void(std::unique_ptr< storm::modelchecker::CheckResult > const &)>

Functions
bool	parseOptions (const int argc, const char *argv[])

void	setResourceLimits ()

void	setFileLogging ()

void	setLogLevel ()

int	process (std::string const &name, std::string const &executableName, std::function< void(std::string const &, std::string const &)> initSettingsFunc, std::function< void(void)> processOptionsFunc, const int argc, const char **argv)
	Processes the options and returns the exit code.

void	parseSymbolicModelDescription (storm::settings::modules::IOSettings const &ioSettings, SymbolicInput &input)

void	parseProperties (storm::settings::modules::IOSettings const &ioSettings, SymbolicInput &input, boost::optional< std::set< std::string > > const &propertyFilter)

SymbolicInput	parseSymbolicInputQvbs (storm::settings::modules::IOSettings const &ioSettings)

SymbolicInput	parseSymbolicInput ()

void	getModelProcessingInformationAutomatic (SymbolicInput const &input, ModelProcessingInformation &mpi)

ModelProcessingInformation	getModelProcessingInformation (SymbolicInput const &input, std::shared_ptr< SymbolicInput > const &transformedJaniInput=nullptr)
	Sets the model processing information based on the given input.

void	ensureNoUndefinedPropertyConstants (std::vector< storm::jani::Property > const &properties)

std::pair< SymbolicInput, ModelProcessingInformation >	preprocessSymbolicInput (SymbolicInput const &input)

void	exportSymbolicInput (SymbolicInput const &input)

std::vector< std::shared_ptr< storm::logic::Formula const > >	createFormulasToRespect (std::vector< storm::jani::Property > const &properties)

template<storm::dd::DdType DdType, typename ValueType >
std::shared_ptr< storm::models::ModelBase >	buildModelDd (SymbolicInput const &input)

storm::builder::BuilderOptions	createBuildOptionsSparseFromSettings (SymbolicInput const &input)

template<typename ValueType >
std::shared_ptr< storm::models::ModelBase >	buildModelSparse (SymbolicInput const &input, storm::builder::BuilderOptions const &options)

template<typename ValueType >
std::shared_ptr< storm::models::ModelBase >	buildModelExplicit (storm::settings::modules::IOSettings const &ioSettings, storm::settings::modules::BuildSettings const &buildSettings)

template<storm::dd::DdType DdType, typename ValueType >
std::shared_ptr< storm::models::ModelBase >	buildModel (SymbolicInput const &input, storm::settings::modules::IOSettings const &ioSettings, ModelProcessingInformation const &mpi)

template<typename ValueType >
std::shared_ptr< storm::models::sparse::Model< ValueType > >	preprocessSparseMarkovAutomaton (std::shared_ptr< storm::models::sparse::MarkovAutomaton< ValueType > > const &model)

template<typename ValueType >
std::shared_ptr< storm::models::sparse::Model< ValueType > >	preprocessSparseModelBisimulation (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, SymbolicInput const &input, storm::settings::modules::BisimulationSettings const &bisimulationSettings)

template<typename ValueType >
std::pair< std::shared_ptr< storm::models::sparse::Model< ValueType > >, bool >	preprocessSparseModel (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, SymbolicInput const &input, ModelProcessingInformation const &mpi)

template<typename ValueType >
void	exportSparseModel (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, SymbolicInput const &input)

template<storm::dd::DdType DdType, typename ValueType >
void	exportDdModel (std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model, SymbolicInput const &)

template<storm::dd::DdType DdType, typename ValueType >
void	exportModel (std::shared_ptr< storm::models::ModelBase > const &model, SymbolicInput const &input)

template<storm::dd::DdType DdType, typename ValueType >
std::enable_if< DdType!=storm::dd::DdType::Sylvan &&!std::is_same< ValueType, double >::value, std::shared_ptr< storm::models::Model< ValueType > > >::type	preprocessDdMarkovAutomaton (std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model)

template<storm::dd::DdType DdType, typename ValueType >
std::enable_if< DdType==storm::dd::DdType::Sylvan\|\|std::is_same< ValueType, double >::value, std::shared_ptr< storm::models::Model< ValueType > > >::type	preprocessDdMarkovAutomaton (std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model)

template<storm::dd::DdType DdType, typename ValueType , typename ExportValueType = ValueType>
std::shared_ptr< storm::models::Model< ExportValueType > >	preprocessDdModelBisimulation (std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model, SymbolicInput const &input, storm::settings::modules::BisimulationSettings const &bisimulationSettings, ModelProcessingInformation const &mpi)

template<storm::dd::DdType DdType, typename ValueType , typename ExportValueType = ValueType>
std::pair< std::shared_ptr< storm::models::ModelBase >, bool >	preprocessDdModel (std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model, SymbolicInput const &input, ModelProcessingInformation const &mpi)

template<storm::dd::DdType DdType, typename BuildValueType , typename ExportValueType = BuildValueType>
std::pair< std::shared_ptr< storm::models::ModelBase >, bool >	preprocessModel (std::shared_ptr< storm::models::ModelBase > const &model, SymbolicInput const &input, ModelProcessingInformation const &mpi)

void	printComputingCounterexample (storm::jani::Property const &property)

void	printCounterexample (std::shared_ptr< storm::counterexamples::Counterexample > const &counterexample, storm::utility::Stopwatch *watch=nullptr)

template<typename ValueType >
void	generateCounterexamples (std::shared_ptr< storm::models::ModelBase > const &, SymbolicInput const &)

template<>
void	generateCounterexamples< double > (std::shared_ptr< storm::models::ModelBase > const &model, SymbolicInput const &input)

template<typename ValueType >
void	printFilteredResult (std::unique_ptr< storm::modelchecker::CheckResult > const &result, storm::modelchecker::FilterType ft)

void	printModelCheckingProperty (storm::jani::Property const &property)

template<typename ValueType >
void	printResult (std::unique_ptr< storm::modelchecker::CheckResult > const &result, storm::logic::Formula const &filterStatesFormula, storm::modelchecker::FilterType const &filterType, storm::utility::Stopwatch *watch=nullptr)

template<typename ValueType >
void	printResult (std::unique_ptr< storm::modelchecker::CheckResult > const &result, storm::jani::Property const &property, storm::utility::Stopwatch *watch=nullptr)

template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	verifyProperty (std::shared_ptr< storm::logic::Formula const > const &formula, std::shared_ptr< storm::logic::Formula const > const &statesFilter, VerificationCallbackType const &verificationCallback)
	Verifies the given formula plus a filter formula to identify relevant states and warns the user in case of issues.

template<typename ValueType >
void	verifyProperties (SymbolicInput const &input, VerificationCallbackType const &verificationCallback, PostprocessingCallbackType const &postprocessingCallback=PostprocessingIdentity())
	Verifies all (potentially preprocessed) properties given in `input`.

template<typename ValueType >
void	computeStateValues (std::string const &description, std::function< std::unique_ptr< storm::modelchecker::CheckResult >()> const &computationCallback, SymbolicInput const &input, VerificationCallbackType const &verificationCallback, PostprocessingCallbackType const &postprocessingCallback=PostprocessingIdentity())
	Computes values for each state (such as the steady-state probability distribution).

std::vector< storm::expressions::Expression >	parseConstraints (storm::expressions::ExpressionManager const &expressionManager, std::string const &constraintsString)

std::vector< std::vector< storm::expressions::Expression > >	parseInjectedRefinementPredicates (storm::expressions::ExpressionManager const &expressionManager, std::string const &refinementPredicatesString)

template<storm::dd::DdType DdType, typename ValueType >
void	verifyWithAbstractionRefinementEngine (SymbolicInput const &input, ModelProcessingInformation const &mpi)

template<typename ValueType >
void	verifyWithExplorationEngine (SymbolicInput const &input, ModelProcessingInformation const &mpi)

template<typename ValueType >
void	verifyWithSparseEngine (std::shared_ptr< storm::models::ModelBase > const &model, SymbolicInput const &input, ModelProcessingInformation const &mpi)

template<storm::dd::DdType DdType, typename ValueType >
void	verifyWithHybridEngine (std::shared_ptr< storm::models::ModelBase > const &model, SymbolicInput const &input, ModelProcessingInformation const &mpi)

template<storm::dd::DdType DdType, typename ValueType >
void	verifyWithDdEngine (std::shared_ptr< storm::models::ModelBase > const &model, SymbolicInput const &input, ModelProcessingInformation const &mpi)

template<storm::dd::DdType DdType, typename ValueType >
void	verifyWithAbstractionRefinementEngine (std::shared_ptr< storm::models::ModelBase > const &model, SymbolicInput const &input, ModelProcessingInformation const &mpi)

template<storm::dd::DdType DdType, typename ValueType >
std::enable_if< DdType!=storm::dd::DdType::CUDD\|\|std::is_same< ValueType, double >::value, void >::type	verifySymbolicModel (std::shared_ptr< storm::models::ModelBase > const &model, SymbolicInput const &input, ModelProcessingInformation const &mpi)

template<storm::dd::DdType DdType, typename ValueType >
std::enable_if< DdType==storm::dd::DdType::CUDD &&!std::is_same< ValueType, double >::value, void >::type	verifySymbolicModel (std::shared_ptr< storm::models::ModelBase > const &, SymbolicInput const &, ModelProcessingInformation const &)

template<storm::dd::DdType DdType, typename ValueType >
void	verifyModel (std::shared_ptr< storm::models::ModelBase > const &model, SymbolicInput const &input, ModelProcessingInformation const &mpi)

template<storm::dd::DdType DdType, typename BuildValueType , typename VerificationValueType = BuildValueType>
std::shared_ptr< storm::models::ModelBase >	buildPreprocessModelWithValueTypeAndDdlib (SymbolicInput const &input, ModelProcessingInformation const &mpi)

template<storm::dd::DdType DdType, typename BuildValueType , typename VerificationValueType = BuildValueType>
std::shared_ptr< storm::models::ModelBase >	buildPreprocessExportModelWithValueTypeAndDdlib (SymbolicInput const &input, ModelProcessingInformation const &mpi)

template<storm::dd::DdType DdType, typename BuildValueType , typename VerificationValueType = BuildValueType>
void	processInputWithValueTypeAndDdlib (SymbolicInput const &input, ModelProcessingInformation const &mpi)

template<typename ValueType >
void	processInputWithValueType (SymbolicInput const &input, ModelProcessingInformation const &mpi)

std::string	shellQuoteSingleIfNecessary (const std::string &arg)
	For a command-line argument, returns a quoted version with single quotes if it contains unsafe characters.

void	printHeader (std::string const &name, const int argc, const char **argv)

void	printVersion ()

void	printTimeAndMemoryStatistics (uint64_t wallclockMilliseconds)

Typedef Documentation

◆ PostprocessingCallbackType

using storm::cli::PostprocessingCallbackType = typedef std::function<void(std::unique_ptr<storm::modelchecker::CheckResult> const&)>

Definition at line 981 of file model-handling.h.

◆ VerificationCallbackType

using storm::cli::VerificationCallbackType = typedef std::function<std::unique_ptr<storm::modelchecker::CheckResult>(std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states)>

Definition at line 979 of file model-handling.h.

Function Documentation

◆ buildModel()

template<storm::dd::DdType DdType, typename ValueType >

std::shared_ptr< storm::models::ModelBase > storm::cli::buildModel	(	SymbolicInput const &	input,
		storm::settings::modules::IOSettings const &	ioSettings,
		ModelProcessingInformation const &	mpi
	)

Definition at line 519 of file model-handling.h.

◆ buildModelDd()

template<storm::dd::DdType DdType, typename ValueType >

std::shared_ptr< storm::models::ModelBase > storm::cli::buildModelDd ( SymbolicInput const & input )

Definition at line 438 of file model-handling.h.

◆ buildModelExplicit()

template<typename ValueType >

std::shared_ptr< storm::models::ModelBase > storm::cli::buildModelExplicit	(	storm::settings::modules::IOSettings const &	ioSettings,
		storm::settings::modules::BuildSettings const &	buildSettings
	)

Definition at line 498 of file model-handling.h.

◆ buildModelSparse()

template<typename ValueType >

std::shared_ptr< storm::models::ModelBase > storm::cli::buildModelSparse	(	SymbolicInput const &	input,
		storm::builder::BuilderOptions const &	options
	)

Definition at line 493 of file model-handling.h.

◆ buildPreprocessExportModelWithValueTypeAndDdlib()

template<storm::dd::DdType DdType, typename BuildValueType , typename VerificationValueType = BuildValueType>

std::shared_ptr< storm::models::ModelBase > storm::cli::buildPreprocessExportModelWithValueTypeAndDdlib	(	SymbolicInput const &	input,
		ModelProcessingInformation const &	mpi
	)

Definition at line 1400 of file model-handling.h.

◆ buildPreprocessModelWithValueTypeAndDdlib()

template<storm::dd::DdType DdType, typename BuildValueType , typename VerificationValueType = BuildValueType>

std::shared_ptr< storm::models::ModelBase > storm::cli::buildPreprocessModelWithValueTypeAndDdlib	(	SymbolicInput const &	input,
		ModelProcessingInformation const &	mpi
	)

Definition at line 1375 of file model-handling.h.

◆ computeStateValues()

template<typename ValueType >

void storm::cli::computeStateValues	(	std::string const &	description,
		std::function< std::unique_ptr< storm::modelchecker::CheckResult >()> const &	computationCallback,
		SymbolicInput const &	input,
		VerificationCallbackType const &	verificationCallback,
		PostprocessingCallbackType const &	postprocessingCallback = `PostprocessingIdentity()`
	)

Computes values for each state (such as the steady-state probability distribution).

If one or more formulas are given, they serve as filter to identify which states are relevant.

Parameters

description	A string description of what is to be computed used for sensible command line output.
computationCallback	A function that performs the actual computation of the state values
input	Where the properties are read from
verificationCallback	Function to perform the actual verification task for a given formula plus a filter formula to identify relevant states
postprocessingCallback	Function that processes the verification result, such as e.g. output to a file

Definition at line 1055 of file model-handling.h.

◆ createBuildOptionsSparseFromSettings()

storm::builder::BuilderOptions storm::cli::createBuildOptionsSparseFromSettings ( SymbolicInput const & input )

inline

Definition at line 448 of file model-handling.h.

◆ createFormulasToRespect()

std::vector< std::shared_ptr< storm::logic::Formula const > > storm::cli::createFormulasToRespect ( std::vector< storm::jani::Property > const & properties )

inline

Definition at line 425 of file model-handling.h.

◆ ensureNoUndefinedPropertyConstants()

void storm::cli::ensureNoUndefinedPropertyConstants ( std::vector< storm::jani::Property > const & properties )

inline

Definition at line 338 of file model-handling.h.

◆ exportDdModel()

template<storm::dd::DdType DdType, typename ValueType >

void storm::cli::exportDdModel	(	std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &	model,
		SymbolicInput const &
	)

Definition at line 673 of file model-handling.h.

◆ exportModel()

template<storm::dd::DdType DdType, typename ValueType >

void storm::cli::exportModel	(	std::shared_ptr< storm::models::ModelBase > const &	model,
		SymbolicInput const &	input
	)

Definition at line 706 of file model-handling.h.

◆ exportSparseModel()

template<typename ValueType >

void storm::cli::exportSparseModel	(	std::shared_ptr< storm::models::sparse::Model< ValueType > > const &	model,
		SymbolicInput const &	input
	)

Definition at line 633 of file model-handling.h.

◆ exportSymbolicInput()

void storm::cli::exportSymbolicInput ( SymbolicInput const & input )

inline

Definition at line 415 of file model-handling.h.

◆ generateCounterexamples()

template<typename ValueType >

void storm::cli::generateCounterexamples	(	std::shared_ptr< storm::models::ModelBase > const &	,
		SymbolicInput const &
	)

Definition at line 826 of file model-handling.h.

◆ generateCounterexamples< double >()

template<>

void storm::cli::generateCounterexamples< double >	(	std::shared_ptr< storm::models::ModelBase > const &	model,
		SymbolicInput const &	input
	)

inline

Definition at line 831 of file model-handling.h.

◆ getModelProcessingInformation()

ModelProcessingInformation storm::cli::getModelProcessingInformation	(	SymbolicInput const &	input,
		std::shared_ptr< SymbolicInput > const &	transformedJaniInput = `nullptr`
	)

inline

Sets the model processing information based on the given input.

Finding the right model processing information might require a conversion to jani. In this case, the jani conversion is stored in the transformedJaniInput pointer (unless it is null)

Definition at line 215 of file model-handling.h.

◆ getModelProcessingInformationAutomatic()

void storm::cli::getModelProcessingInformationAutomatic	(	SymbolicInput const &	input,
		ModelProcessingInformation &	mpi
	)

inline

Definition at line 180 of file model-handling.h.

◆ parseConstraints()

std::vector< storm::expressions::Expression > storm::cli::parseConstraints	(	storm::expressions::ExpressionManager const &	expressionManager,
		std::string const &	constraintsString
	)

inline

Definition at line 1103 of file model-handling.h.

◆ parseInjectedRefinementPredicates()

std::vector< std::vector< storm::expressions::Expression > > storm::cli::parseInjectedRefinementPredicates	(	storm::expressions::ExpressionManager const &	expressionManager,
		std::string const &	refinementPredicatesString
	)

inline

Definition at line 1130 of file model-handling.h.

◆ parseOptions()

bool storm::cli::parseOptions	(	const int	argc,
		const char *	argv[]
	)

Definition at line 21 of file cli.cpp.

◆ parseProperties()

void storm::cli::parseProperties	(	storm::settings::modules::IOSettings const &	ioSettings,
		SymbolicInput &	input,
		boost::optional< std::set< std::string > > const &	propertyFilter
	)

inline

Definition at line 99 of file model-handling.h.

◆ parseSymbolicInput()

SymbolicInput storm::cli::parseSymbolicInput ( )

inline

Definition at line 139 of file model-handling.h.

◆ parseSymbolicInputQvbs()

SymbolicInput storm::cli::parseSymbolicInputQvbs ( storm::settings::modules::IOSettings const & ioSettings )

inline

Definition at line 113 of file model-handling.h.

◆ parseSymbolicModelDescription()

void storm::cli::parseSymbolicModelDescription	(	storm::settings::modules::IOSettings const &	ioSettings,
		SymbolicInput &	input
	)

inline

Definition at line 70 of file model-handling.h.

◆ preprocessDdMarkovAutomaton() [1/2]

template<storm::dd::DdType DdType, typename ValueType >

std::enable_if< DdType!=storm::dd::DdType::Sylvan &&!std::is_same< ValueType, double >::value, std::shared_ptr< storm::models::Model< ValueType > > >::type storm::cli::preprocessDdMarkovAutomaton ( std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const & model )

Definition at line 716 of file model-handling.h.

◆ preprocessDdMarkovAutomaton() [2/2]

template<storm::dd::DdType DdType, typename ValueType >

std::enable_if< DdType==storm::dd::DdType::Sylvan||std::is_same< ValueType, double >::value, std::shared_ptr< storm::models::Model< ValueType > > >::type storm::cli::preprocessDdMarkovAutomaton ( std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const & model )

Definition at line 722 of file model-handling.h.

◆ preprocessDdModel()

template<storm::dd::DdType DdType, typename ValueType , typename ExportValueType = ValueType>

std::pair< std::shared_ptr< storm::models::ModelBase >, bool > storm::cli::preprocessDdModel	(	std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &	model,
		SymbolicInput const &	input,
		ModelProcessingInformation const &	mpi
	)

Definition at line 750 of file model-handling.h.

◆ preprocessDdModelBisimulation()

template<storm::dd::DdType DdType, typename ValueType , typename ExportValueType = ValueType>

std::shared_ptr< storm::models::Model< ExportValueType > > storm::cli::preprocessDdModelBisimulation	(	std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &	model,
		SymbolicInput const &	input,
		storm::settings::modules::BisimulationSettings const &	bisimulationSettings,
		ModelProcessingInformation const &	mpi
	)

Definition at line 732 of file model-handling.h.

◆ preprocessModel()

template<storm::dd::DdType DdType, typename BuildValueType , typename ExportValueType = BuildValueType>

std::pair< std::shared_ptr< storm::models::ModelBase >, bool > storm::cli::preprocessModel	(	std::shared_ptr< storm::models::ModelBase > const &	model,
		SymbolicInput const &	input,
		ModelProcessingInformation const &	mpi
	)

Definition at line 789 of file model-handling.h.

◆ preprocessSparseMarkovAutomaton()

template<typename ValueType >

std::shared_ptr< storm::models::sparse::Model< ValueType > > storm::cli::preprocessSparseMarkovAutomaton ( std::shared_ptr< storm::models::sparse::MarkovAutomaton< ValueType > > const & model )

Definition at line 547 of file model-handling.h.

◆ preprocessSparseModel()

template<typename ValueType >

std::pair< std::shared_ptr< storm::models::sparse::Model< ValueType > >, bool > storm::cli::preprocessSparseModel	(	std::shared_ptr< storm::models::sparse::Model< ValueType > > const &	model,
		SymbolicInput const &	input,
		ModelProcessingInformation const &	mpi
	)

Definition at line 586 of file model-handling.h.

◆ preprocessSparseModelBisimulation()

template<typename ValueType >

std::shared_ptr< storm::models::sparse::Model< ValueType > > storm::cli::preprocessSparseModelBisimulation	(	std::shared_ptr< storm::models::sparse::Model< ValueType > > const &	model,
		SymbolicInput const &	input,
		storm::settings::modules::BisimulationSettings const &	bisimulationSettings
	)

Definition at line 573 of file model-handling.h.

◆ preprocessSymbolicInput()

std::pair< SymbolicInput, ModelProcessingInformation > storm::cli::preprocessSymbolicInput ( SymbolicInput const & input )

inline

Definition at line 354 of file model-handling.h.

◆ printComputingCounterexample()

void storm::cli::printComputingCounterexample ( storm::jani::Property const & property )

inline

Definition at line 810 of file model-handling.h.

◆ printCounterexample()

void storm::cli::printCounterexample	(	std::shared_ptr< storm::counterexamples::Counterexample > const &	counterexample,
		storm::utility::Stopwatch *	watch = `nullptr`
	)

inline

Definition at line 814 of file model-handling.h.

◆ printFilteredResult()

template<typename ValueType >

void storm::cli::printFilteredResult	(	std::unique_ptr< storm::modelchecker::CheckResult > const &	result,
		storm::modelchecker::FilterType	ft
	)

Definition at line 890 of file model-handling.h.

◆ printHeader()

void storm::cli::printHeader	(	std::string const &	name,
		const int	argc,
		const char **	argv
	)

Definition at line 56 of file print.cpp.

◆ printModelCheckingProperty()

void storm::cli::printModelCheckingProperty ( storm::jani::Property const & property )

inline

Definition at line 952 of file model-handling.h.

◆ printResult() [1/2]

template<typename ValueType >

void storm::cli::printResult	(	std::unique_ptr< storm::modelchecker::CheckResult > const &	result,
		storm::jani::Property const &	property,
		storm::utility::Stopwatch *	watch = `nullptr`
	)

Definition at line 974 of file model-handling.h.

◆ printResult() [2/2]

template<typename ValueType >

void storm::cli::printResult	(	std::unique_ptr< storm::modelchecker::CheckResult > const &	result,
		storm::logic::Formula const &	filterStatesFormula,
		storm::modelchecker::FilterType const &	filterType,
		storm::utility::Stopwatch *	watch = `nullptr`
	)

Definition at line 957 of file model-handling.h.

◆ printTimeAndMemoryStatistics()

void storm::cli::printTimeAndMemoryStatistics ( uint64_t wallclockMilliseconds )

Definition at line 148 of file print.cpp.

◆ printVersion()

void storm::cli::printVersion ( )

Definition at line 78 of file print.cpp.

◆ process()

int storm::cli::process	(	std::string const &	name,
		std::string const &	executableName,
		std::function< void(std::string const &, std::string const &)>	initSettingsFunc,
		std::function< void(void)>	processOptionsFunc,
		const int	argc,
		const char **	argv
	)

Processes the options and returns the exit code.

Definition at line 84 of file cli.cpp.

◆ processInputWithValueType()

template<typename ValueType >

void storm::cli::processInputWithValueType	(	SymbolicInput const &	input,
		ModelProcessingInformation const &	mpi
	)

Definition at line 1433 of file model-handling.h.

◆ processInputWithValueTypeAndDdlib()

template<storm::dd::DdType DdType, typename BuildValueType , typename VerificationValueType = BuildValueType>

void storm::cli::processInputWithValueTypeAndDdlib	(	SymbolicInput const &	input,
		ModelProcessingInformation const &	mpi
	)

Definition at line 1409 of file model-handling.h.

◆ setFileLogging()

void storm::cli::setFileLogging ( )

Definition at line 61 of file cli.cpp.

◆ setLogLevel()

void storm::cli::setLogLevel ( )

Definition at line 68 of file cli.cpp.

◆ setResourceLimits()

void storm::cli::setResourceLimits ( )

Definition at line 49 of file cli.cpp.

◆ shellQuoteSingleIfNecessary()

std::string storm::cli::shellQuoteSingleIfNecessary ( const std::string & arg )

For a command-line argument, returns a quoted version with single quotes if it contains unsafe characters.

Otherwise, just returns the unquoted argument.

Definition at line 35 of file print.cpp.

◆ verifyModel()

template<storm::dd::DdType DdType, typename ValueType >

void storm::cli::verifyModel	(	std::shared_ptr< storm::models::ModelBase > const &	model,
		SymbolicInput const &	input,
		ModelProcessingInformation const &	mpi
	)

Definition at line 1365 of file model-handling.h.

◆ verifyProperties()

template<typename ValueType >

void storm::cli::verifyProperties	(	SymbolicInput const &	input,
		VerificationCallbackType const &	verificationCallback,
		PostprocessingCallbackType const &	postprocessingCallback = `PostprocessingIdentity()`
	)

Verifies all (potentially preprocessed) properties given in input.

Parameters

input	Where the properties are read from
verificationCallback	Function to perform the actual verification task for a given formula plus a filter formula to identify relevant states
postprocessingCallback	Function that processes the verification result, such as e.g. output to a file

Definition at line 1030 of file model-handling.h.

◆ verifyProperty()

template<typename ValueType >

std::unique_ptr< storm::modelchecker::CheckResult > storm::cli::verifyProperty	(	std::shared_ptr< storm::logic::Formula const > const &	formula,
		std::shared_ptr< storm::logic::Formula const > const &	statesFilter,
		VerificationCallbackType const &	verificationCallback
	)

Verifies the given formula plus a filter formula to identify relevant states and warns the user in case of issues.

Parameters

formula	the formula to check
statesFilter	a second formula that identifies the relevant states (needs to be qualitative)
verificationCallback	Function to perform the actual verification task for a given formula plus a filter formula to identify relevant states

Definition at line 996 of file model-handling.h.

◆ verifySymbolicModel() [1/2]

template<storm::dd::DdType DdType, typename ValueType >

std::enable_if< DdType==storm::dd::DdType::CUDD &&!std::is_same< ValueType, double >::value, void >::type storm::cli::verifySymbolicModel	(	std::shared_ptr< storm::models::ModelBase > const &	,
		SymbolicInput const &	,
		ModelProcessingInformation const &
	)

Definition at line 1359 of file model-handling.h.

◆ verifySymbolicModel() [2/2]

template<storm::dd::DdType DdType, typename ValueType >

std::enable_if< DdType!=storm::dd::DdType::CUDD\|\|std::is_same< ValueType, double >::value, void >::type storm::cli::verifySymbolicModel	(	std::shared_ptr< storm::models::ModelBase > const &	model,
		SymbolicInput const &	input,
		ModelProcessingInformation const &	mpi
	)

Definition at line 1347 of file model-handling.h.

◆ verifyWithAbstractionRefinementEngine() [1/2]

template<storm::dd::DdType DdType, typename ValueType >

void storm::cli::verifyWithAbstractionRefinementEngine	(	std::shared_ptr< storm::models::ModelBase > const &	model,
		SymbolicInput const &	input,
		ModelProcessingInformation const &	mpi
	)

Definition at line 1335 of file model-handling.h.

◆ verifyWithAbstractionRefinementEngine() [2/2]

template<storm::dd::DdType DdType, typename ValueType >

void storm::cli::verifyWithAbstractionRefinementEngine	(	SymbolicInput const &	input,
		ModelProcessingInformation const &	mpi
	)

Definition at line 1177 of file model-handling.h.

◆ verifyWithDdEngine()

template<storm::dd::DdType DdType, typename ValueType >

void storm::cli::verifyWithDdEngine	(	std::shared_ptr< storm::models::ModelBase > const &	model,
		SymbolicInput const &	input,
		ModelProcessingInformation const &	mpi
	)

Definition at line 1310 of file model-handling.h.

◆ verifyWithExplorationEngine()

template<typename ValueType >

void storm::cli::verifyWithExplorationEngine	(	SymbolicInput const &	input,
		ModelProcessingInformation const &	mpi
	)

Definition at line 1193 of file model-handling.h.

◆ verifyWithHybridEngine()

template<storm::dd::DdType DdType, typename ValueType >

void storm::cli::verifyWithHybridEngine	(	std::shared_ptr< storm::models::ModelBase > const &	model,
		SymbolicInput const &	input,
		ModelProcessingInformation const &	mpi
	)

Definition at line 1286 of file model-handling.h.

◆ verifyWithSparseEngine()

template<typename ValueType >

void storm::cli::verifyWithSparseEngine	(	std::shared_ptr< storm::models::ModelBase > const &	model,
		SymbolicInput const &	input,
		ModelProcessingInformation const &	mpi
	)

Definition at line 1205 of file model-handling.h.

Classes

Typedefs

Functions

Typedef Documentation

◆ PostprocessingCallbackType

◆ VerificationCallbackType

Function Documentation

◆ buildModel()

◆ buildModelDd()

◆ buildModelExplicit()

◆ buildModelSparse()

◆ buildPreprocessExportModelWithValueTypeAndDdlib()

◆ buildPreprocessModelWithValueTypeAndDdlib()

◆ computeStateValues()

◆ createBuildOptionsSparseFromSettings()

◆ createFormulasToRespect()

◆ ensureNoUndefinedPropertyConstants()

◆ exportDdModel()

◆ exportModel()

◆ exportSparseModel()

◆ exportSymbolicInput()

◆ generateCounterexamples()

◆ generateCounterexamples< double >()

◆ getModelProcessingInformation()

◆ getModelProcessingInformationAutomatic()

◆ parseConstraints()

◆ parseInjectedRefinementPredicates()

◆ parseOptions()

◆ parseProperties()

◆ parseSymbolicInput()

◆ parseSymbolicInputQvbs()

◆ parseSymbolicModelDescription()

◆ preprocessDdMarkovAutomaton() [1/2]

◆ preprocessDdMarkovAutomaton() [2/2]

◆ preprocessDdModel()

◆ preprocessDdModelBisimulation()

◆ preprocessModel()

◆ preprocessSparseMarkovAutomaton()

◆ preprocessSparseModel()

◆ preprocessSparseModelBisimulation()

◆ preprocessSymbolicInput()

◆ printComputingCounterexample()

◆ printCounterexample()

◆ printFilteredResult()

◆ printHeader()

◆ printModelCheckingProperty()

◆ printResult() [1/2]

◆ printResult() [2/2]

◆ printTimeAndMemoryStatistics()

◆ printVersion()

◆ process()

◆ processInputWithValueType()

◆ processInputWithValueTypeAndDdlib()

◆ setFileLogging()

◆ setLogLevel()

◆ setResourceLimits()

◆ shellQuoteSingleIfNecessary()

◆ verifyModel()

◆ verifyProperties()

◆ verifyProperty()

◆ verifySymbolicModel() [1/2]

◆ verifySymbolicModel() [2/2]

◆ verifyWithAbstractionRefinementEngine() [1/2]

◆ verifyWithAbstractionRefinementEngine() [2/2]

◆ verifyWithDdEngine()

◆ verifyWithExplorationEngine()

◆ verifyWithHybridEngine()

◆ verifyWithSparseEngine()