model-handling.h File Reference

#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 "storm/io/file.h"
#include "storm/utility/AutomaticSettings.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 <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/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.
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)
template<storm::dd::DdType DdType, typename ValueType >
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::sparse::Model< ValueType > >, bool >	storm::cli::preprocessSparseModel (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, SymbolicInput const &input, ModelProcessingInformation const &mpi)
template<typename ValueType >
void	storm::cli::exportSparseModel (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, SymbolicInput const &input)
template<storm::dd::DdType DdType, typename ValueType >
void	storm::cli::exportDdModel (std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model, SymbolicInput const &)
template<storm::dd::DdType DdType, typename ValueType >
void	storm::cli::exportModel (std::shared_ptr< storm::models::ModelBase > const &model, SymbolicInput const &input)
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<storm::dd::DdType DdType, typename ValueType , typename ExportValueType = ValueType>
std::pair< std::shared_ptr< storm::models::ModelBase >, bool >	storm::cli::preprocessDdModel (std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model, SymbolicInput const &input, ModelProcessingInformation const &mpi)
template<storm::dd::DdType DdType, typename BuildValueType , typename ExportValueType = BuildValueType>
std::pair< std::shared_ptr< storm::models::ModelBase >, bool >	storm::cli::preprocessModel (std::shared_ptr< storm::models::ModelBase > 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 ValueType >
void	storm::cli::generateCounterexamples (std::shared_ptr< storm::models::ModelBase > const &, SymbolicInput const &)
template<>
void	storm::cli::generateCounterexamples< double > (std::shared_ptr< storm::models::ModelBase > const &model, SymbolicInput const &input)
template<typename 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 >
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::verifyWithSparseEngine (std::shared_ptr< storm::models::ModelBase > const &model, SymbolicInput const &input, ModelProcessingInformation const &mpi)
template<storm::dd::DdType DdType, typename ValueType >
void	storm::cli::verifyWithHybridEngine (std::shared_ptr< storm::models::ModelBase > const &model, SymbolicInput const &input, ModelProcessingInformation const &mpi)
template<storm::dd::DdType DdType, typename ValueType >
void	storm::cli::verifyWithDdEngine (std::shared_ptr< storm::models::ModelBase > const &model, SymbolicInput const &input, ModelProcessingInformation const &mpi)
template<storm::dd::DdType DdType, typename ValueType >
void	storm::cli::verifyWithAbstractionRefinementEngine (std::shared_ptr< storm::models::ModelBase > const &model, 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 &model, 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 &)
template<storm::dd::DdType DdType, typename ValueType >
void	storm::cli::verifyModel (std::shared_ptr< storm::models::ModelBase > const &model, SymbolicInput const &input, ModelProcessingInformation const &mpi)
template<storm::dd::DdType DdType, typename BuildValueType , typename VerificationValueType = BuildValueType>
std::shared_ptr< storm::models::ModelBase >	storm::cli::buildPreprocessModelWithValueTypeAndDdlib (SymbolicInput const &input, ModelProcessingInformation const &mpi)
template<storm::dd::DdType DdType, typename BuildValueType , typename VerificationValueType = BuildValueType>
std::shared_ptr< storm::models::ModelBase >	storm::cli::buildPreprocessExportModelWithValueTypeAndDdlib (SymbolicInput const &input, ModelProcessingInformation const &mpi)
template<storm::dd::DdType DdType, typename BuildValueType , typename VerificationValueType = BuildValueType>
void	storm::cli::processInputWithValueTypeAndDdlib (SymbolicInput const &input, ModelProcessingInformation const &mpi)
template<typename ValueType >
void	storm::cli::processInputWithValueType (SymbolicInput const &input, ModelProcessingInformation const &mpi)