Loading...
Searching...
No Matches
region.h File Reference
#include <boost/optional.hpp>#include <memory>#include <set>#include <string>#include <vector>#include "storm-pars/modelchecker/region/RegionCheckEngine.h"#include "storm-pars/modelchecker/region/RegionResultHypothesis.h"#include "storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h"#include "storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h"#include "storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h"#include "storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.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.
Classes | |
| struct | storm::api::MonotonicitySetting |
Namespaces | |
| namespace | storm |
| LabParser.cpp. | |
| namespace | storm::api |
Functions | |
| 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 > | |
| 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::parseRegions (std::string const &inputString, storm::models::ModelBase const &model) |
| 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 , typename ConstantType > | |
| std::shared_ptr< storm::modelchecker::RegionModelChecker< ParametricType > > | storm::api::initializeParameterLiftingRegionModelChecker (Environment const &env, std::shared_ptr< storm::models::sparse::Model< ParametricType > > const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ParametricType > const &task, bool generateSplitEstimates=false, bool allowModelSimplification=true, bool preconditionsValidatedManually=false, MonotonicitySetting monotonicitySetting=MonotonicitySetting(), boost::optional< std::pair< std::set< typename storm::storage::ParameterRegion< ParametricType >::VariableType >, std::set< typename storm::storage::ParameterRegion< ParametricType >::VariableType > > > monotoneParameters=boost::none) |
| template<typename ParametricType , typename ImpreciseType , typename PreciseType > | |
| std::shared_ptr< storm::modelchecker::RegionModelChecker< ParametricType > > | storm::api::initializeValidatingRegionModelChecker (Environment const &env, std::shared_ptr< storm::models::sparse::Model< ParametricType > > const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ParametricType > const &task, bool generateSplitEstimates=false, bool allowModelSimplification=true) |
| template<typename ValueType > | |
| std::shared_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 generateSplitEstimates=false, bool allowModelSimplification=true, bool preconditionsValidated=false, MonotonicitySetting monotonicitySetting=MonotonicitySetting(), boost::optional< std::pair< std::set< typename storm::storage::ParameterRegion< ValueType >::VariableType >, std::set< typename storm::storage::ParameterRegion< ValueType >::VariableType > > > monotoneParameters=boost::none) |
| template<typename ValueType > | |
| std::shared_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 ®ions, 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 ®ions, storm::modelchecker::RegionCheckEngine engine, storm::modelchecker::RegionResultHypothesis const &hypothesis=storm::modelchecker::RegionResultHypothesis::Unknown, bool sampleVerticesOfRegions=false) |
| template<typename ValueType > | |
| std::unique_ptr< storm::modelchecker::RegionRefinementCheckResult< ValueType > > | storm::api::checkAndRefineRegionWithSparseEngine (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task, storm::storage::ParameterRegion< ValueType > const ®ion, storm::modelchecker::RegionCheckEngine engine, boost::optional< ValueType > const &coverageThreshold, boost::optional< uint64_t > const &refinementDepthThreshold=boost::none, storm::modelchecker::RegionResultHypothesis hypothesis=storm::modelchecker::RegionResultHypothesis::Unknown, bool allowModelSimplification=true, MonotonicitySetting monotonicitySetting=MonotonicitySetting(), 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 (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task, storm::storage::ParameterRegion< ValueType > const ®ion, storm::modelchecker::RegionCheckEngine engine, storm::solver::OptimizationDirection const &dir, boost::optional< ValueType > const &precision, bool absolutePrecision, MonotonicitySetting const &monotonicitySetting, std::optional< storm::logic::Bound > const &boundInvariant, bool generateSplitEstimates=false, std::optional< uint64_t > maxSplitsPerStepThreshold=std::numeric_limits< uint64_t >::max()) |
| Finds the extremal value in the given region. | |
| template<typename ValueType > | |
| bool | storm::api::verifyRegion (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, storm::logic::Formula const &formula, storm::storage::ParameterRegion< ValueType > const ®ion, storm::modelchecker::RegionCheckEngine engine, MonotonicitySetting const &monotonicitySetting, bool generateSplitEstimates=false, std::optional< uint64_t > maxSplitsPerStepThreshold=std::numeric_limits< uint64_t >::max()) |
| 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) |
