#include <memory>
#include <optional>
#include <set>
#include <string>
#include <vector>
#include <boost/algorithm/string.hpp>
#include "storm-pars/modelchecker/region/AnnotatedRegion.h"
#include "storm-pars/modelchecker/region/RegionCheckEngine.h"
#include "storm-pars/modelchecker/region/RegionOptions.h"
#include "storm-pars/modelchecker/region/RegionRefinementChecker.h"
#include "storm-pars/modelchecker/region/RegionResult.h"
#include "storm-pars/modelchecker/region/RegionResultHypothesis.h"
#include "storm-pars/modelchecker/region/RegionSplitEstimateKind.h"
#include "storm-pars/modelchecker/region/RegionSplittingStrategy.h"
#include "storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h"
#include "storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h"
#include "storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.h"
#include "storm-pars/modelchecker/region/monotonicity/MonotonicityBackend.h"
#include "storm-pars/modelchecker/region/monotonicity/OrderBasedMonotonicityBackend.h"
#include "storm-pars/modelchecker/results/RegionCheckResult.h"
#include "storm-pars/modelchecker/results/RegionRefinementCheckResult.h"
#include "storm-pars/parser/MonotonicityParser.h"
#include "storm-pars/parser/ParameterRegionParser.h"
#include "storm-pars/storage/ParameterRegion.h"
#include "storm-pars/utility/parameterlifting.h"
#include "storm/environment/Environment.h"
#include "storm/api/properties.h"
#include "storm/api/transformation.h"
#include "storm/exceptions/InvalidOperationException.h"
#include "storm/exceptions/NotSupportedException.h"
#include "storm/exceptions/UnexpectedException.h"
#include "storm/io/file.h"
#include "storm/models/sparse/Model.h"

Include dependency graph for region.h:

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

Go to the source code of this file.

Namespaces
namespace	storm
	LabParser.cpp.

namespace	storm::api

Typedefs
using	storm::api::MonotonicitySetting = storm::pars::modelchecker::MonotonicityOptions

template<typename ValueType >
using	storm::api::RefinementOptions = storm::pars::modelchecker::RegionRefinementOptions< ValueType >

Functions
template<typename ValueType >
std::set< typename storm::storage::ParameterRegion< ValueType >::VariableType >	storm::api::getModelParameters (storm::models::ModelBase const &model)

template<typename ValueType >
std::vector< typename storm::storage::ParameterRegion< ValueType >::VariableType >	storm::api::parseVariableList (std::string const &inputString, std::set< typename storm::storage::ParameterRegion< ValueType >::VariableType > const &consideredVariables)

template<typename ValueType >
std::vector< typename storm::storage::ParameterRegion< ValueType >::VariableType >	storm::api::parseVariableList (std::string const &inputString, storm::models::ModelBase const &model)

template<typename ValueType >
std::vector< storm::storage::ParameterRegion< ValueType > >	storm::api::parseRegions (std::string const &inputString, std::set< typename storm::storage::ParameterRegion< ValueType >::VariableType > const &consideredVariables)

template<typename ValueType >
std::vector< storm::storage::ParameterRegion< ValueType > >	storm::api::parseRegions (std::string const &inputString, storm::models::ModelBase const &model)

template<typename ValueType >
storm::storage::ParameterRegion< ValueType >	storm::api::createRegion (std::string const &inputString, std::set< typename storm::storage::ParameterRegion< ValueType >::VariableType > const &consideredVariables)

template<typename ValueType >
std::vector< storm::storage::ParameterRegion< ValueType > >	storm::api::createRegion (std::string const &inputString, storm::models::ModelBase const &model)

template<typename ValueType >
storm::storage::ParameterRegion< ValueType >	storm::api::parseRegion (std::string const &inputString, std::set< typename storm::storage::ParameterRegion< ValueType >::VariableType > const &consideredVariables)

template<typename ValueType >
storm::storage::ParameterRegion< ValueType >	storm::api::parseRegion (std::string const &inputString, storm::models::ModelBase const &model)

template<typename ValueType >
std::pair< std::set< typename storm::storage::ParameterRegion< ValueType >::VariableType >, std::set< typename storm::storage::ParameterRegion< ValueType >::VariableType > >	storm::api::parseMonotoneParameters (std::string const &fileName, std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model)

template<typename ParametricType >
std::shared_ptr< storm::models::sparse::Model< ParametricType > >	storm::api::preprocessSparseModelForParameterLifting (std::shared_ptr< storm::models::sparse::Model< ParametricType > > const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ParametricType > const &task, storm::modelchecker::RegionCheckEngine engine, bool preconditionsValidatedManually=false)

template<typename ParametricType , typename ImpreciseType = double, typename PreciseType = storm::RationalNumber>
std::unique_ptr< storm::modelchecker::RegionModelChecker< ParametricType > >	storm::api::createRegionModelChecker (storm::modelchecker::RegionCheckEngine engine, storm::models::ModelType modelType)

template<typename ParametricType , typename ImpreciseType = double, typename PreciseType = storm::RationalNumber>
std::unique_ptr< storm::modelchecker::MonotonicityBackend< ParametricType > >	storm::api::initializeMonotonicityBackend (storm::modelchecker::RegionModelChecker< ParametricType > const &regionChecker, storm::modelchecker::RegionCheckEngine engine, storm::modelchecker::CheckTask< storm::logic::Formula, ParametricType > const &task, MonotonicitySetting const &monotonicitySetting, std::optional< std::pair< std::set< typename storm::storage::ParameterRegion< ParametricType >::VariableType >, std::set< typename storm::storage::ParameterRegion< ParametricType >::VariableType > > > monotoneParameters=std::nullopt)

template<typename ValueType , typename ImpreciseType = double, typename PreciseType = storm::RationalNumber>
std::unique_ptr< storm::modelchecker::RegionModelChecker< ValueType > >	storm::api::initializeRegionModelChecker (Environment const &env, std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task, storm::modelchecker::RegionCheckEngine engine, bool allowModelSimplification=true, bool graphPreserving=true, bool preconditionsValidated=false, MonotonicitySetting monotonicitySetting=MonotonicitySetting(), std::optional< std::pair< std::set< typename storm::storage::ParameterRegion< ValueType >::VariableType >, std::set< typename storm::storage::ParameterRegion< ValueType >::VariableType > > > monotoneParameters=std::nullopt)

template<typename ValueType >
std::unique_ptr< storm::modelchecker::RegionModelChecker< ValueType > >	storm::api::initializeRegionModelChecker (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task, storm::modelchecker::RegionCheckEngine engine)

template<typename ValueType >
std::unique_ptr< storm::modelchecker::RegionCheckResult< ValueType > >	storm::api::checkRegionsWithSparseEngine (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task, std::vector< storm::storage::ParameterRegion< ValueType > > const &regions, storm::modelchecker::RegionCheckEngine engine, std::vector< storm::modelchecker::RegionResultHypothesis > const &hypotheses, bool sampleVerticesOfRegions)

template<typename ValueType >
std::unique_ptr< storm::modelchecker::RegionCheckResult< ValueType > >	storm::api::checkRegionsWithSparseEngine (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task, std::vector< storm::storage::ParameterRegion< ValueType > > const &regions, storm::modelchecker::RegionCheckEngine engine, storm::modelchecker::RegionResultHypothesis const &hypothesis=storm::modelchecker::RegionResultHypothesis::Unknown, bool sampleVerticesOfRegions=false)

template<typename ValueType , typename ImpreciseType = double, typename PreciseType = storm::RationalNumber>
std::unique_ptr< storm::modelchecker::RegionRefinementChecker< ValueType > >	storm::api::initializeRegionRefinementChecker (Environment const &env, RefinementOptions< ValueType > settings)

template<typename ValueType >
std::unique_ptr< storm::modelchecker::RegionRefinementCheckResult< ValueType > >	storm::api::checkAndRefineRegionWithSparseEngine (RefinementOptions< ValueType > settings, storm::storage::ParameterRegion< ValueType > const &region, std::optional< ValueType > const &coverageThreshold, std::optional< uint64_t > const &refinementDepthThreshold=std::nullopt, storm::modelchecker::RegionResultHypothesis hypothesis=storm::modelchecker::RegionResultHypothesis::Unknown, uint64_t monThresh=0)
	Checks and iteratively refines the given region with the sparse engine.

template<typename ValueType >
std::pair< storm::RationalNumber, typename storm::storage::ParameterRegion< ValueType >::Valuation >	storm::api::computeExtremalValue (RefinementOptions< ValueType > settings, storm::storage::ParameterRegion< ValueType > const &region, storm::solver::OptimizationDirection const &dir, std::optional< ValueType > const &precision, bool absolutePrecision, std::optional< storm::logic::Bound > const &boundInvariant)
	Finds the extremal value in the given region.

template<typename ValueType >
bool	storm::api::verifyRegion (RefinementOptions< ValueType > settings, storm::storage::ParameterRegion< ValueType > const &region)
	Verifies whether a region satisfies a property.

template<typename ValueType >
void	storm::api::exportRegionCheckResultToFile (std::unique_ptr< storm::modelchecker::CheckResult > const &checkResult, std::string const &filename, bool onlyConclusiveResults=false)

Namespaces

Typedefs

Functions