#include "storm/api/storm.h"
#include "storm-counterexamples/api/counterexamples.h"
#include "storm-gamebased-ar/api/verification.h"
#include "storm-parsers/api/storm-parsers.h"
#include "storm-parsers/parser/ExpressionParser.h"
#include "AutomaticSettings.h"
#include "storm/io/file.h"
#include "storm/utility/Engine.h"
#include "storm/utility/NumberTraits.h"
#include "storm/utility/SignalHandler.h"
#include "storm/utility/macros.h"
#include "storm/utility/Stopwatch.h"
#include "storm/utility/initialize.h"
#include <filesystem>
#include <type_traits>
#include "storm/storage/SymbolicModelDescription.h"
#include "storm/storage/jani/Property.h"
#include "storm/builder/BuilderType.h"
#include "storm/models/ModelBase.h"
#include "storm/environment/Environment.h"
#include "storm/exceptions/OptionParserException.h"
#include "storm/modelchecker/results/CheckResult.h"
#include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h"
#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/models/symbolic/MarkovAutomaton.h"
#include "storm/models/symbolic/StandardRewardModel.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/AbstractionSettings.h"
#include "storm/settings/modules/BuildSettings.h"
#include "storm/settings/modules/CoreSettings.h"
#include "storm/settings/modules/DebugSettings.h"
#include "storm/settings/modules/HintSettings.h"
#include "storm/settings/modules/IOSettings.h"
#include "storm/settings/modules/ModelCheckerSettings.h"
#include "storm/settings/modules/ResourceSettings.h"
#include "storm/settings/modules/SylvanSettings.h"
#include "storm/settings/modules/TransformationSettings.h"
#include "storm/storage/Qvbs.h"
#include "storm/storage/jani/localeliminator/AutomaticAction.h"
#include "storm/storage/jani/localeliminator/JaniLocalEliminator.h"

Include dependency graph for model-handling.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	storm::cli::SymbolicInput

struct	storm::cli::ModelProcessingInformation

struct	storm::cli::PostprocessingIdentity

Namespaces
namespace	storm
	LabParser.cpp.

namespace	storm::cli

Typedefs
using	storm::cli::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	storm::cli::PostprocessingCallbackType = std::function< void(std::unique_ptr< storm::modelchecker::CheckResult > const &)>

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

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

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

SymbolicInput	storm::cli::parseSymbolicInput ()

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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)

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)

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

template<storm::dd::DdType DdType, typename ValueType >
void	storm::cli::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	storm::cli::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	storm::cli::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 > >	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)

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)

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)

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

void	storm::cli::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	storm::cli::generateCounterexamples (std::shared_ptr< ModelType > const &, SymbolicInput const &)

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)

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

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

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)

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)

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.

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`.

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

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

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

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

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

template<typename ValueType >
void	storm::cli::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	storm::cli::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	storm::cli::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	storm::cli::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	storm::cli::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	storm::cli::verifySymbolicModel (std::shared_ptr< storm::models::ModelBase > const &, SymbolicInput const &, ModelProcessingInformation const &)

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

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

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

Classes

Namespaces

Typedefs

Functions