model-handling-main-cli.h File Reference

#include <filesystem>
#include <sstream>
#include "storm-cli-utilities/model-handling.h"
#include "storm-counterexamples/api/counterexamples.h"
#include "storm-gamebased-ar/api/verification.h"
#include "storm-parsers/parser/ExpressionParser.h"
#include "storm/modelchecker/results/CheckResult.h"
#include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h"
#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
#include "storm/settings/modules/AbstractionSettings.h"
#include "storm/settings/modules/CounterexampleGeneratorSettings.h"
#include "storm/utility/NumberTraits.h"
#include "storm/utility/SignalHandler.h"

Include dependency graph for model-handling-main-cli.h:

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

Go to the source code of this file.

Classes
struct	storm::cli::PostprocessingIdentity

Namespaces
namespace	storm
namespace	storm::cli

Typedefs
using	storm::cli::VerificationCallbackType
using	storm::cli::PostprocessingCallbackType = std::function<void(std::unique_ptr<storm::modelchecker::CheckResult> const&)>

Functions
void	storm::cli::exportSymbolicInput (SymbolicInput const &input)
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)
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 &)
void	storm::cli::processInput (SymbolicInput const &input, ModelProcessingInformation const &mpi)