Classes
struct	SymbolicInput
struct	ModelProcessingInformation
struct	PostprocessingIdentity

Typedefs
using	VerificationCallbackType
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.
auto	castAndApply (std::shared_ptr< storm::models::ModelBase > const &model, auto const &callback)
auto	applyValueType (ModelProcessingInformation::ValueType vt, auto const &callback)
auto	applyDdLibValueType (storm::dd::DdType dd, ModelProcessingInformation::ValueType vt, auto const &callback)
void	ensureNoUndefinedPropertyConstants (std::vector< storm::jani::Property > const &properties)
std::pair< SymbolicInput, ModelProcessingInformation >	preprocessSymbolicInput (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 (storm::Environment const &env, SymbolicInput const &input)
storm::builder::BuilderOptions	createBuildOptionsSparseFromSettings (SymbolicInput const &input)
template<typename ValueType>
storm::builder::ExplicitModelBuilder< ValueType >::Options	createExplorationOptionsFromSettings ()
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)
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::ModelBase >, bool >	preprocessModel (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, SymbolicInput const &input, ModelProcessingInformation const &mpi)
template<typename ValueType>
void	exportModel (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, SymbolicInput const &input)
template<storm::dd::DdType DdType, typename ValueType>
void	exportModel (std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model, SymbolicInput const &)
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<typename ExportValueType, storm::dd::DdType DdType, typename ValueType>
std::pair< std::shared_ptr< storm::models::ModelBase >, bool >	preprocessDdModelImpl (std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model, SymbolicInput const &input, ModelProcessingInformation const &mpi)
template<storm::dd::DdType DdType, typename ValueType>
std::pair< std::shared_ptr< storm::models::ModelBase >, bool >	preprocessModel (std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model, SymbolicInput const &input, ModelProcessingInformation const &mpi)
void	printModelCheckingProperty (storm::jani::Property const &property)
std::shared_ptr< storm::models::ModelBase >	buildPreprocessModel (SymbolicInput const &input, ModelProcessingInformation const &mpi)
std::shared_ptr< storm::models::ModelBase >	buildPreprocessExportModel (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)
bool	preferEliminationChecker ()
	Returns whether the settings request to prefer the dedicated elimination model checker.
void	exportSymbolicInput (SymbolicInput const &input)
void	printComputingCounterexample (storm::jani::Property const &property)
void	printCounterexample (std::shared_ptr< storm::counterexamples::Counterexample > const &counterexample, storm::utility::Stopwatch *watch=nullptr)
template<typename ModelType> requires (!std::derived_from<ModelType, storm::models::sparse::Model<double>>)
void	generateCounterexamples (std::shared_ptr< ModelType > const &, SymbolicInput const &, ModelProcessingInformation const &)
template<typename ModelType> requires (std::derived_from<ModelType, storm::models::sparse::Model<double>>)
void	generateCounterexamples (std::shared_ptr< ModelType > const &sparseModel, SymbolicInput const &input, ModelProcessingInformation const &mpi)
template<typename ValueType> requires (!storm::IsIntervalType<ValueType>)
void	printFilteredResult (std::unique_ptr< storm::modelchecker::CheckResult > const &result, storm::modelchecker::FilterType ft)
template<typename ValueType> requires (!storm::IsIntervalType<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)
storm::gbar::api::AbstractionRefinementOptions	getAbstractionRefinementOptions (storm::expressions::ExpressionManager const *expressionManager=nullptr)
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	verifyModel (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &sparseModel, SymbolicInput const &input, ModelProcessingInformation const &mpi)
template<storm::dd::DdType DdType, typename ValueType>
void	verifyWithHybridEngine (std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &symbolicModel, SymbolicInput const &input, ModelProcessingInformation const &mpi)
template<storm::dd::DdType DdType, typename ValueType>
void	verifyWithDdEngine (std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &symbolicModel, SymbolicInput const &input, ModelProcessingInformation const &mpi)
template<storm::dd::DdType DdType, typename ValueType>
void	verifyWithAbstractionRefinementEngine (std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &symbolicModel, 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	verifyModel (std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &symbolicModel, 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 &)
void	processInput (SymbolicInput const &input, ModelProcessingInformation const &mpi)

Typedef Documentation

◆ PostprocessingCallbackType

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

Definition at line 236 of file model-handling-main-cli.h.

◆ VerificationCallbackType

using storm::cli::VerificationCallbackType

Initial value:

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 234 of file model-handling-main-cli.h.

Function Documentation

◆ applyDdLibValueType()

auto storm::cli::applyDdLibValueType	(	storm::dd::DdType	dd,
		ModelProcessingInformation::ValueType	vt,
		auto const &	callback )

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

◆ applyValueType()

auto storm::cli::applyValueType	(	ModelProcessingInformation::ValueType	vt,
		auto const &	callback )

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

◆ buildModel()

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

inline

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

◆ buildModelDd()

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

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

Definition at line 508 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 599 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 582 of file model-handling.h.

◆ buildPreprocessExportModel()

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

inline

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

◆ buildPreprocessModel()

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

inline

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

◆ castAndApply()

auto storm::cli::castAndApply	(	std::shared_ptr< storm::models::ModelBase > const &	model,
		auto const &	callback )

Definition at line 332 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 315 of file model-handling-main-cli.h.

◆ createBuildOptionsSparseFromSettings()

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

inline

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

◆ createExplorationOptionsFromSettings()

template<typename ValueType>

storm::builder::ExplicitModelBuilder< ValueType >::Options storm::cli::createExplorationOptionsFromSettings ( )

Definition at line 570 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 495 of file model-handling.h.

◆ ensureNoUndefinedPropertyConstants()

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

inline

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

◆ exportModel() [1/2]

template<typename ValueType>

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

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

◆ exportModel() [2/2]

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

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

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

◆ exportSymbolicInput()

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

inline

Definition at line 24 of file model-handling-main-cli.h.

◆ generateCounterexamples() [1/2]

template<typename ModelType>
requires (!std::derived_from<ModelType, storm::models::sparse::Model<double>>)

void storm::cli::generateCounterexamples	(	std::shared_ptr< ModelType > const &	,
		SymbolicInput const &	,
		ModelProcessingInformation const &	)

inline

Definition at line 51 of file model-handling-main-cli.h.

◆ generateCounterexamples() [2/2]

template<typename ModelType>
requires (std::derived_from<ModelType, storm::models::sparse::Model<double>>)

void storm::cli::generateCounterexamples	(	std::shared_ptr< ModelType > const &	sparseModel,
		SymbolicInput const &	input,
		ModelProcessingInformation const &	mpi )

inline

Definition at line 57 of file model-handling-main-cli.h.

◆ getAbstractionRefinementOptions()

storm::gbar::api::AbstractionRefinementOptions storm::cli::getAbstractionRefinementOptions ( storm::expressions::ExpressionManager const * expressionManager = nullptr )

inline

Definition at line 436 of file model-handling-main-cli.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 208 of file model-handling.h.

◆ getModelProcessingInformationAutomatic()

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

inline

Definition at line 173 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 363 of file model-handling-main-cli.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 390 of file model-handling-main-cli.h.

◆ parseOptions()

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

Definition at line 22 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 91 of file model-handling.h.

◆ parseSymbolicInput()

SymbolicInput storm::cli::parseSymbolicInput ( )

inline

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

◆ parseSymbolicInputQvbs()

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

inline

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

◆ parseSymbolicModelDescription()

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

inline

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

◆ preferEliminationChecker()

bool storm::cli::preferEliminationChecker ( )

Returns whether the settings request to prefer the dedicated elimination model checker.

Definition at line 11 of file SettingsUtils.cpp.

◆ 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 906 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 900 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 916 of file model-handling.h.

◆ preprocessDdModelImpl()

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

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

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

◆ preprocessModel() [1/2]

template<typename ValueType>

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

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

◆ preprocessModel() [2/2]

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

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

Definition at line 982 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 682 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 712 of file model-handling.h.

◆ preprocessSymbolicInput()

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

inline

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

◆ printComputingCounterexample()

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

inline

Definition at line 34 of file model-handling-main-cli.h.

◆ printCounterexample()

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

inline

Definition at line 38 of file model-handling-main-cli.h.

◆ printFilteredResult()

template<typename ValueType>
requires (!storm::IsIntervalType<ValueType>)

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

Definition at line 119 of file model-handling-main-cli.h.

◆ printHeader()

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

Definition at line 60 of file print.cpp.

◆ printModelCheckingProperty()

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

inline

Definition at line 996 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 229 of file model-handling-main-cli.h.

◆ printResult() [2/2]

template<typename ValueType>
requires (!storm::IsIntervalType<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 212 of file model-handling-main-cli.h.

◆ printTimeAndMemoryStatistics()

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

Definition at line 169 of file print.cpp.

◆ printVersion()

void storm::cli::printVersion ( )

Definition at line 82 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 96 of file cli.cpp.

◆ processInput()

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

inline

Definition at line 699 of file model-handling-main-cli.h.

◆ setFileLogging()

void storm::cli::setFileLogging ( )

Definition at line 62 of file cli.cpp.

◆ setLogLevel()

void storm::cli::setLogLevel ( )

Definition at line 69 of file cli.cpp.

◆ setResourceLimits()

void storm::cli::setResourceLimits ( )

Definition at line 50 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 39 of file print.cpp.

◆ verifyModel() [1/2]

template<typename ValueType>

void storm::cli::verifyModel	(	std::shared_ptr< storm::models::sparse::Model< ValueType > > const &	sparseModel,
		SymbolicInput const &	input,
		ModelProcessingInformation const &	mpi )

Definition at line 491 of file model-handling-main-cli.h.

◆ verifyModel() [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::verifyModel	(	std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &	symbolicModel,
		SymbolicInput const &	input,
		ModelProcessingInformation const &	mpi )

Definition at line 681 of file model-handling-main-cli.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 290 of file model-handling-main-cli.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 251 of file model-handling-main-cli.h.

◆ verifySymbolicModel()

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 694 of file model-handling-main-cli.h.

◆ verifyWithAbstractionRefinementEngine() [1/2]

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

void storm::cli::verifyWithAbstractionRefinementEngine	(	std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &	symbolicModel,
		SymbolicInput const &	input,
		ModelProcessingInformation const &	mpi )

Definition at line 669 of file model-handling-main-cli.h.

◆ verifyWithAbstractionRefinementEngine() [2/2]

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

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

Definition at line 466 of file model-handling-main-cli.h.

◆ verifyWithDdEngine()

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

void storm::cli::verifyWithDdEngine	(	std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &	symbolicModel,
		SymbolicInput const &	input,
		ModelProcessingInformation const &	mpi )

Definition at line 644 of file model-handling-main-cli.h.

◆ verifyWithExplorationEngine()

template<typename ValueType>

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

Definition at line 479 of file model-handling-main-cli.h.

◆ verifyWithHybridEngine()

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

void storm::cli::verifyWithHybridEngine	(	std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &	symbolicModel,
		SymbolicInput const &	input,
		ModelProcessingInformation const &	mpi )

Definition at line 620 of file model-handling-main-cli.h.

Classes

Typedefs

Functions

Typedef Documentation

◆ PostprocessingCallbackType

◆ VerificationCallbackType

Function Documentation

◆ applyDdLibValueType()

◆ applyValueType()

◆ buildModel()

◆ buildModelDd()

◆ buildModelExplicit()

◆ buildModelSparse()

◆ buildPreprocessExportModel()

◆ buildPreprocessModel()

◆ castAndApply()

◆ computeStateValues()

◆ createBuildOptionsSparseFromSettings()

◆ createExplorationOptionsFromSettings()

◆ createFormulasToRespect()

◆ ensureNoUndefinedPropertyConstants()

◆ exportModel() [1/2]

◆ exportModel() [2/2]

◆ exportSymbolicInput()

◆ generateCounterexamples() [1/2]

◆ generateCounterexamples() [2/2]

◆ getAbstractionRefinementOptions()

◆ getModelProcessingInformation()

◆ getModelProcessingInformationAutomatic()

◆ parseConstraints()

◆ parseInjectedRefinementPredicates()

◆ parseOptions()

◆ parseProperties()

◆ parseSymbolicInput()

◆ parseSymbolicInputQvbs()

◆ parseSymbolicModelDescription()

◆ preferEliminationChecker()

◆ preprocessDdMarkovAutomaton() [1/2]

◆ preprocessDdMarkovAutomaton() [2/2]

◆ preprocessDdModelBisimulation()

◆ preprocessDdModelImpl()

◆ preprocessModel() [1/2]

◆ preprocessModel() [2/2]

◆ preprocessSparseMarkovAutomaton()

◆ preprocessSparseModelBisimulation()

◆ preprocessSymbolicInput()

◆ printComputingCounterexample()

◆ printCounterexample()

◆ printFilteredResult()

◆ printHeader()

◆ printModelCheckingProperty()

◆ printResult() [1/2]

◆ printResult() [2/2]

◆ printTimeAndMemoryStatistics()

◆ printVersion()

◆ process()

◆ processInput()

◆ setFileLogging()

◆ setLogLevel()

◆ setResourceLimits()

◆ shellQuoteSingleIfNecessary()

◆ verifyModel() [1/2]

◆ verifyModel() [2/2]

◆ verifyProperties()

◆ verifyProperty()

◆ verifySymbolicModel()

◆ verifyWithAbstractionRefinementEngine() [1/2]

◆ verifyWithAbstractionRefinementEngine() [2/2]

◆ verifyWithDdEngine()

◆ verifyWithExplorationEngine()

◆ verifyWithHybridEngine()