Storm 1.10.0.1
A Modern Probabilistic Model Checker
|
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) |
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) |
using storm::cli::PostprocessingCallbackType = typedef std::function<void(std::unique_ptr<storm::modelchecker::CheckResult> const&)> |
Definition at line 1074 of file model-handling.h.
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.
auto storm::cli::applyDdLibValueType | ( | storm::dd::DdType | dd, |
ModelProcessingInformation::ValueType | vt, | ||
auto const & | callback | ||
) |
Definition at line 399 of file model-handling.h.
auto storm::cli::applyValueType | ( | ModelProcessingInformation::ValueType | vt, |
auto const & | callback | ||
) |
Definition at line 386 of file model-handling.h.
|
inline |
Definition at line 607 of file model-handling.h.
std::shared_ptr< storm::models::ModelBase > storm::cli::buildModelDd | ( | SymbolicInput const & | input | ) |
Definition at line 519 of file model-handling.h.
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.
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.
|
inline |
Definition at line 1516 of file model-handling.h.
|
inline |
Definition at line 1490 of file model-handling.h.
auto storm::cli::castAndApply | ( | std::shared_ptr< storm::models::ModelBase > const & | model, |
auto const & | callback | ||
) |
Definition at line 341 of file model-handling.h.
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.
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 1153 of file model-handling.h.
|
inline |
Definition at line 529 of file model-handling.h.
|
inline |
Definition at line 506 of file model-handling.h.
|
inline |
Definition at line 419 of file model-handling.h.
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.
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.
|
inline |
Definition at line 496 of file model-handling.h.
|
inline |
Definition at line 919 of file model-handling.h.
|
inline |
Definition at line 925 of file model-handling.h.
|
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.
|
inline |
Definition at line 183 of file model-handling.h.
|
inline |
Definition at line 1201 of file model-handling.h.
|
inline |
Definition at line 1228 of file model-handling.h.
bool storm::cli::parseOptions | ( | const int | argc, |
const char * | argv[] | ||
) |
|
inline |
Definition at line 102 of file model-handling.h.
|
inline |
Definition at line 142 of file model-handling.h.
|
inline |
Definition at line 116 of file model-handling.h.
|
inline |
Definition at line 73 of file model-handling.h.
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.
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.
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.
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.
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.
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.
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.
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.
|
inline |
Definition at line 435 of file model-handling.h.
|
inline |
Definition at line 902 of file model-handling.h.
|
inline |
Definition at line 906 of file model-handling.h.
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.
void storm::cli::printHeader | ( | std::string const & | name, |
const int | argc, | ||
const char ** | argv | ||
) |
|
inline |
Definition at line 1044 of file model-handling.h.
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.
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.
void storm::cli::printTimeAndMemoryStatistics | ( | uint64_t | wallclockMilliseconds | ) |
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 | ||
) |
|
inline |
Definition at line 1524 of file model-handling.h.
std::string storm::cli::shellQuoteSingleIfNecessary | ( | const std::string & | arg | ) |
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.
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.
void storm::cli::verifyProperties | ( | SymbolicInput const & | input, |
VerificationCallbackType const & | verificationCallback, | ||
PostprocessingCallbackType const & | postprocessingCallback = PostprocessingIdentity() |
||
) |
Verifies all (potentially preprocessed) properties given in input
.
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 1128 of file model-handling.h.
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.
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 1089 of file model-handling.h.
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.
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.
void storm::cli::verifyWithAbstractionRefinementEngine | ( | SymbolicInput const & | input, |
ModelProcessingInformation const & | mpi | ||
) |
Definition at line 1275 of file model-handling.h.
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.
void storm::cli::verifyWithExplorationEngine | ( | SymbolicInput const & | input, |
ModelProcessingInformation const & | mpi | ||
) |
Definition at line 1291 of file model-handling.h.
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.