Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
storm::cli Namespace Reference

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, ModelProcessingInformationpreprocessSymbolicInput (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::ModelBasebuildModelDd (SymbolicInput const &input)
 
storm::builder::BuilderOptions createBuildOptionsSparseFromSettings (SymbolicInput const &input)
 
template<typename ValueType >
std::shared_ptr< storm::models::ModelBasebuildModelSparse (SymbolicInput const &input, storm::builder::BuilderOptions const &options)
 
template<typename ValueType >
std::shared_ptr< storm::models::ModelBasebuildModelExplicit (storm::settings::modules::IOSettings const &ioSettings, storm::settings::modules::BuildSettings const &buildSettings)
 
std::shared_ptr< storm::models::ModelBasebuildModel (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 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::CheckResultverifyProperty (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::ExpressionparseConstraints (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::ModelBasebuildPreprocessModel (SymbolicInput const &input, ModelProcessingInformation const &mpi)
 
std::shared_ptr< storm::models::ModelBasebuildPreprocessExportModel (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 1074 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 1072 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 399 of file model-handling.h.

◆ applyValueType()

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

Definition at line 386 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 607 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 519 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 587 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 574 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 1516 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 1490 of file model-handling.h.

◆ castAndApply()

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

Definition at line 341 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
descriptionA string description of what is to be computed used for sensible command line output.
computationCallbackA function that performs the actual computation of the state values
inputWhere the properties are read from
verificationCallbackFunction to perform the actual verification task for a given formula plus a filter formula to identify relevant states
postprocessingCallbackFunction that processes the verification result, such as e.g. output to a file

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

◆ createBuildOptionsSparseFromSettings()

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

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

◆ ensureNoUndefinedPropertyConstants()

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

Definition at line 419 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 741 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 781 of file model-handling.h.

◆ exportSymbolicInput()

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

Definition at line 496 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 919 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 925 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 218 of file model-handling.h.

◆ getModelProcessingInformationAutomatic()

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

Definition at line 183 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 1201 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 1228 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 102 of file model-handling.h.

◆ parseSymbolicInput()

SymbolicInput storm::cli::parseSymbolicInput ( )
inline

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

◆ parseSymbolicInputQvbs()

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

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

◆ parseSymbolicModelDescription()

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

Definition at line 73 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 815 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 821 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 831 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 849 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 683 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 888 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 639 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 670 of file model-handling.h.

◆ preprocessSymbolicInput()

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

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

◆ printComputingCounterexample()

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

Definition at line 902 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 906 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 982 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 1044 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 1067 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 1050 of file model-handling.h.

◆ printTimeAndMemoryStatistics()

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

Definition at line 149 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 1524 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 1303 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 1472 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
inputWhere the properties are read from
verificationCallbackFunction to perform the actual verification task for a given formula plus a filter formula to identify relevant states
postprocessingCallbackFunction that processes the verification result, such as e.g. output to a file

Definition at line 1128 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
formulathe formula to check
statesFiltera second formula that identifies the relevant states (needs to be qualitative)
verificationCallbackFunction to perform the actual verification task for a given formula plus a filter formula to identify relevant states

Definition at line 1089 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 1485 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 1461 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 1275 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 1436 of file model-handling.h.

◆ verifyWithExplorationEngine()

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

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