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.

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)

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)

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, bool graphPreserving=true)

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

template<typename ModelType > requires (std::derived_from<ModelType, storm::models::sparse::Model<double>>)
void	generateCounterexamples (std::shared_ptr< ModelType > const &sparseModel, SymbolicInput const &input)

template<typename ValueType > requires (!storm::IsIntervalType<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 > 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)

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

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)

void	processInput (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 1062 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 1060 of file model-handling.h.

Function Documentation

◆ applyDdLibValueType()

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

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

◆ applyValueType()

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

Definition at line 374 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 595 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 507 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 575 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 562 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 1504 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 1478 of file model-handling.h.

◆ castAndApply()

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

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

◆ createBuildOptionsSparseFromSettings()

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

inline

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

◆ ensureNoUndefinedPropertyConstants()

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

inline

Definition at line 407 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 729 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 769 of file model-handling.h.

◆ exportSymbolicInput()

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

inline

Definition at line 484 of file model-handling.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 &
	)

inline

Definition at line 907 of file model-handling.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
	)

inline

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

◆ getModelProcessingInformationAutomatic()

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

inline

Definition at line 171 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 1189 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 1216 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 90 of file model-handling.h.

◆ parseSymbolicInput()

SymbolicInput storm::cli::parseSymbolicInput ( )

inline

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

◆ parseSymbolicInputQvbs()

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

inline

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

◆ parseSymbolicModelDescription()

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

inline

Definition at line 61 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 803 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 809 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 819 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 837 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 671 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 876 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 627 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,
		bool	graphPreserving = `true`
	)

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

◆ preprocessSymbolicInput()

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

inline

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

◆ printComputingCounterexample()

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

inline

Definition at line 890 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 894 of file model-handling.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 970 of file model-handling.h.

◆ printHeader()

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

Definition at line 57 of file print.cpp.

◆ printModelCheckingProperty()

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

inline

Definition at line 1032 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 1055 of file model-handling.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 1038 of file model-handling.h.

◆ printTimeAndMemoryStatistics()

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

Definition at line 159 of file print.cpp.

◆ printVersion()

void storm::cli::printVersion ( )

Definition at line 79 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.

◆ processInput()

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

inline

Definition at line 1512 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 36 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 1291 of file model-handling.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 1460 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 1116 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 1077 of file model-handling.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 1473 of file model-handling.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 1449 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 1263 of file model-handling.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 1424 of file model-handling.h.

◆ verifyWithExplorationEngine()

template<typename ValueType >

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

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

Classes

Typedefs

Functions

Typedef Documentation

◆ PostprocessingCallbackType

◆ VerificationCallbackType

Function Documentation

◆ applyDdLibValueType()

◆ applyValueType()

◆ buildModel()

◆ buildModelDd()

◆ buildModelExplicit()

◆ buildModelSparse()

◆ buildPreprocessExportModel()

◆ buildPreprocessModel()

◆ castAndApply()

◆ computeStateValues()

◆ createBuildOptionsSparseFromSettings()

◆ createFormulasToRespect()

◆ ensureNoUndefinedPropertyConstants()

◆ exportModel() [1/2]

◆ exportModel() [2/2]

◆ exportSymbolicInput()

◆ generateCounterexamples() [1/2]

◆ generateCounterexamples() [2/2]

◆ getModelProcessingInformation()

◆ getModelProcessingInformationAutomatic()

◆ parseConstraints()

◆ parseInjectedRefinementPredicates()

◆ parseOptions()

◆ parseProperties()

◆ parseSymbolicInput()

◆ parseSymbolicInputQvbs()

◆ parseSymbolicModelDescription()

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