Namespaces
namespace	analysis
namespace	api
namespace	modelchecker
namespace	utility

Classes
struct	SampleInformation
struct	PreprocessResult
class	FeasibilitySynthesisTask

Enumerations
enum class	FeasibilityMethod { PLA , SCP , GD }

Functions
template<typename VT1>
void	printFeasibilityResult (bool success, std::pair< VT1, typename storm::storage::ParameterRegion< storm::RationalFunction >::Valuation > const &valueValuationPair, storm::utility::Stopwatch const &watch)
std::shared_ptr< FeasibilitySynthesisTask const >	createFeasibilitySynthesisTaskFromSettings (std::shared_ptr< storm::logic::Formula const > const &formula, std::vector< storm::storage::ParameterRegion< storm::RationalFunction > > const &regions)
template<typename ValueType>
void	performFeasibility (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Model< ValueType > > model, std::shared_ptr< storm::pars::FeasibilitySynthesisTask const > const &task, boost::optional< std::set< RationalFunctionVariable > > omittedParameters, storm::api::MonotonicitySetting monotonicitySettings)
template<typename ValueType>
void	runFeasibilityWithGD (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Model< ValueType > > model, std::shared_ptr< storm::pars::FeasibilitySynthesisTask const > const &task, boost::optional< std::set< RationalFunctionVariable > > omittedParameters, storm::api::MonotonicitySetting monotonicitySettings)
template<typename ValueType>
void	runFeasibilityWithPLA (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, std::shared_ptr< storm::pars::FeasibilitySynthesisTask const > const &task, boost::optional< std::set< RationalFunctionVariable > > omittedParameters, storm::api::MonotonicitySetting monotonicitySettings)
template void	performFeasibility (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > > model, std::shared_ptr< storm::pars::FeasibilitySynthesisTask const > const &task, boost::optional< std::set< RationalFunctionVariable > > omittedParameters, storm::api::MonotonicitySetting monotonicitySettings)
template void	runFeasibilityWithGD (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > > model, std::shared_ptr< storm::pars::FeasibilitySynthesisTask const > const &task, boost::optional< std::set< RationalFunctionVariable > > omittedParameters, storm::api::MonotonicitySetting monotonicitySettings)
template void	runFeasibilityWithPLA (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > > const &model, std::shared_ptr< storm::pars::FeasibilitySynthesisTask const > const &task, boost::optional< std::set< RationalFunctionVariable > > omittedParameters, storm::api::MonotonicitySetting monotonicitySettings)
template<typename ValueType>
std::optional< storm::analysis::ConstraintCollector >	collectConstraints (std::shared_ptr< storm::models::ModelBase > const &model)
	Collects the constraints of the model.
template<typename ValueType>
std::optional< storm::pars::analysis::RegionCheckResult >	checkRegionConstraints (std::optional< storm::analysis::ConstraintCollector > const &collector, storm::storage::ParameterRegion< ValueType > const &region, bool wellformedness)
	Checks the well-formedness constraints or the graph-preservation constraints over the region.
std::string	describeViolation (storm::pars::analysis::RegionCheckResult const &result)
	Describes a violated constraint, including the point at which it fails.
template<typename ValueType>
storm::pars::analysis::GraphPreservationStatus	establishGraphPreservation (std::shared_ptr< storm::models::ModelBase > const &model, std::vector< storm::storage::ParameterRegion< ValueType > > const &regions, bool graphPreservationRequired)
	Determines to what extent the regions are known to be well-defined and graph-preserving.
template<typename ValueType>
void	analyzeMonotonicity (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, cli::SymbolicInput const &input, std::vector< storm::storage::ParameterRegion< ValueType > > const &regions)
template void	analyzeMonotonicity (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > > const &model, cli::SymbolicInput const &input, std::vector< storm::storage::ParameterRegion< storm::RationalFunction > > const &regions)
template<typename ValueType>
void	printInitialStatesResult (std::unique_ptr< storm::modelchecker::CheckResult > const &result, storm::utility::Stopwatch watch, const storm::utility::parametric::Valuation< ValueType > valuation)
template void	printInitialStatesResult< storm::RationalFunction > (std::unique_ptr< storm::modelchecker::CheckResult > const &result, storm::utility::Stopwatch watch, const storm::utility::parametric::Valuation< storm::RationalFunction > valuation)
template<template< typename, typename > class ModelCheckerType, typename ModelType, typename ValueType, typename SolveValueType = double>
void	verifyPropertiesAtSamplePointsDerivative (storm::Environment const &env, ModelType const &model, cli::SymbolicInput const &input, SampleInformation< ValueType > const &samples)
template<template< typename, typename > class ModelCheckerType, typename ModelType, typename ValueType, typename SolveValueType = double, bool Derivative = false>
void	verifyPropertiesAtSamplePoints (storm::Environment const &env, ModelType const &model, cli::SymbolicInput const &input, SampleInformation< ValueType > const &samples)
template<typename ValueType, typename SolveValueType = double>
void	verifyPropertiesAtSamplePointsWithSparseEngineDerivatives (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, cli::SymbolicInput const &input, SampleInformation< ValueType > const &samples)
template<typename ValueType, typename SolveValueType = double>
void	verifyPropertiesAtSamplePointsWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, cli::SymbolicInput const &input, SampleInformation< ValueType > const &samples)
template<typename ValueType>
SampleInformation< ValueType >	parseSamples (std::shared_ptr< storm::models::ModelBase > const &model, std::string const &sampleString, bool graphPreserving)
template<typename ValueType>
void	sampleDerivatives (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Model< ValueType > > model, cli::SymbolicInput const &input, std::string const &instantiationString)
template<typename ValueType>
void	verifyProperties (std::vector< storm::jani::Property > const &properties, std::function< std::unique_ptr< storm::modelchecker::CheckResult >(std::shared_ptr< storm::logic::Formula const > const &formula)> const &verificationCallback, std::function< void(std::unique_ptr< storm::modelchecker::CheckResult > const &)> const &postprocessingCallback)
template<typename ValueType>
void	computeSolutionFunctionsWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, storm::cli::SymbolicInput const &input)
template<storm::dd::DdType DdType, typename ValueType>
void	computeSolutionFunctionsWithSymbolicEngine (storm::Environment const &env, std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model, storm::cli::SymbolicInput const &input)
template void	verifyProperties< storm::RationalFunction > (std::vector< storm::jani::Property > const &, std::function< std::unique_ptr< storm::modelchecker::CheckResult >(std::shared_ptr< storm::logic::Formula const > const &)> const &, std::function< void(std::unique_ptr< storm::modelchecker::CheckResult > const &)> const &)
template void	computeSolutionFunctionsWithSparseEngine< storm::RationalFunction > (storm::Environment const &, std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > > const &, storm::cli::SymbolicInput const &)
template void	computeSolutionFunctionsWithSymbolicEngine< storm::dd::DdType::Sylvan, storm::RationalFunction > (storm::Environment const &, std::shared_ptr< storm::models::symbolic::Model< storm::dd::DdType::Sylvan, storm::RationalFunction > > const &, storm::cli::SymbolicInput const &)
template<typename ValueType>
std::vector< storm::storage::ParameterRegion< ValueType > >	parseRegions (std::shared_ptr< storm::models::ModelBase > const &model)
template<typename ValueType>
std::shared_ptr< storm::models::ModelBase >	eliminateScc (std::shared_ptr< storm::models::ModelBase > const &model)
template<typename ValueType>
std::shared_ptr< storm::models::ModelBase >	simplifyModel (std::shared_ptr< storm::models::ModelBase > const &model, cli::SymbolicInput const &input)
template<typename ValueType>
PreprocessResult	preprocessSparseModel (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, cli::SymbolicInput const &input, storm::cli::ModelProcessingInformation const &mpi)
template<storm::dd::DdType DdType, typename ValueType>
PreprocessResult	preprocessDdModel (std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model, cli::SymbolicInput const &input, storm::cli::ModelProcessingInformation const &mpi)
template<storm::dd::DdType DdType, typename ValueType>
PreprocessResult	preprocessModel (std::shared_ptr< storm::models::ModelBase > const &model, cli::SymbolicInput const &input, storm::cli::ModelProcessingInformation const &mpi)
template<typename ValueType>
void	verifyRegionWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, cli::SymbolicInput const &input, std::vector< storm::storage::ParameterRegion< ValueType > > const &regions, storm::api::MonotonicitySetting monotonicitySettings=storm::api::MonotonicitySetting())
template<typename ValueType>
void	parameterSpacePartitioningWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, cli::SymbolicInput const &input, std::vector< storm::storage::ParameterRegion< ValueType > > const &regions, storm::api::MonotonicitySetting monotonicitySettings=storm::api::MonotonicitySetting(), uint64_t monThresh=0)
void	processInput (cli::SymbolicInput &&input, storm::cli::ModelProcessingInformation const &mpi)
void	processOptions ()

Enumeration Type Documentation

◆ FeasibilityMethod

enum class storm::pars::FeasibilityMethod

strong

Enumerator
PLA
SCP
GD

Definition at line 11 of file FeasibilitySynthesisTask.h.

Function Documentation

◆ analyzeMonotonicity() [1/2]

template void storm::pars::analyzeMonotonicity	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > > const &	model,
		cli::SymbolicInput const &	input,
		std::vector< storm::storage::ParameterRegion< storm::RationalFunction > > const &	regions )

◆ analyzeMonotonicity() [2/2]

template<typename ValueType>

void storm::pars::analyzeMonotonicity	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::sparse::Model< ValueType > > const &	model,
		cli::SymbolicInput const &	input,
		std::vector< storm::storage::ParameterRegion< ValueType > > const &	regions )

Definition at line 35 of file monotonicity.cpp.

◆ checkRegionConstraints()

template<typename ValueType>

std::optional< storm::pars::analysis::RegionCheckResult > storm::pars::checkRegionConstraints	(	std::optional< storm::analysis::ConstraintCollector > const &	collector,
		storm::storage::ParameterRegion< ValueType > const &	region,
		bool	wellformedness )

Checks the well-formedness constraints or the graph-preservation constraints over the region.

Graph preservation includes well-formedness. Returns std::nullopt if they cannot be checked, e.g. if the region does not cover all constrained variables.

Definition at line 48 of file graphPreservation.h.

◆ collectConstraints()

template<typename ValueType>

std::optional< storm::analysis::ConstraintCollector > storm::pars::collectConstraints ( std::shared_ptr< storm::models::ModelBase > const & model )

Collects the constraints of the model.

Returns std::nullopt if the model is not a sparse parametric model.

Definition at line 29 of file graphPreservation.h.

◆ computeSolutionFunctionsWithSparseEngine()

template<typename ValueType>

void storm::pars::computeSolutionFunctionsWithSparseEngine	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::sparse::Model< ValueType > > const &	model,
		storm::cli::SymbolicInput const &	input )

Definition at line 62 of file solutionFunctions.cpp.

◆ computeSolutionFunctionsWithSparseEngine< storm::RationalFunction >()

template void storm::pars::computeSolutionFunctionsWithSparseEngine< storm::RationalFunction >	(	storm::Environment const &	,
		std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > > const &	,
		storm::cli::SymbolicInput const &	)

◆ computeSolutionFunctionsWithSymbolicEngine()

template<storm::dd::DdType DdType, typename ValueType>

void storm::pars::computeSolutionFunctionsWithSymbolicEngine	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &	model,
		storm::cli::SymbolicInput const &	input )

Definition at line 94 of file solutionFunctions.cpp.

◆ computeSolutionFunctionsWithSymbolicEngine< storm::dd::DdType::Sylvan, storm::RationalFunction >()

template void storm::pars::computeSolutionFunctionsWithSymbolicEngine< storm::dd::DdType::Sylvan, storm::RationalFunction >	(	storm::Environment const &	,
		std::shared_ptr< storm::models::symbolic::Model< storm::dd::DdType::Sylvan, storm::RationalFunction > > const &	,
		storm::cli::SymbolicInput const &	)

◆ createFeasibilitySynthesisTaskFromSettings()

std::shared_ptr< FeasibilitySynthesisTask const > storm::pars::createFeasibilitySynthesisTaskFromSettings	(	std::shared_ptr< storm::logic::Formula const > const &	formula,
		std::vector< storm::storage::ParameterRegion< storm::RationalFunction > > const &	regions )

Definition at line 46 of file feasibility.cpp.

◆ describeViolation()

std::string storm::pars::describeViolation ( storm::pars::analysis::RegionCheckResult const & result )

inline

Describes a violated constraint, including the point at which it fails.

Definition at line 66 of file graphPreservation.h.

◆ eliminateScc()

template<typename ValueType>

std::shared_ptr< storm::models::ModelBase > storm::pars::eliminateScc ( std::shared_ptr< storm::models::ModelBase > const & model )

Definition at line 75 of file storm-pars.cpp.

◆ establishGraphPreservation()

template<typename ValueType>

storm::pars::analysis::GraphPreservationStatus storm::pars::establishGraphPreservation	(	std::shared_ptr< storm::models::ModelBase > const &	model,
		std::vector< storm::storage::ParameterRegion< ValueType > > const &	regions,
		bool	graphPreservationRequired )

Determines to what extent the regions are known to be well-defined and graph-preserving.

Graph preservation implies well-definedness. If graph preservation is assumed, we only warn about regions that are provably not graph-preserving (or not well-formed). Otherwise, if graphPreservationRequired is set, a proof is required and an exception is raised if there is none. If it is not set (e.g. for robust parameter lifting, which handles non-graph-preserving regions itself), only well-definedness is determined.

Definition at line 85 of file graphPreservation.h.

◆ parameterSpacePartitioningWithSparseEngine()

template<typename ValueType>

void storm::pars::parameterSpacePartitioningWithSparseEngine	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::sparse::Model< ValueType > > const &	model,
		cli::SymbolicInput const &	input,
		std::vector< storm::storage::ParameterRegion< ValueType > > const &	regions,
		storm::api::MonotonicitySetting	monotonicitySettings = storm::api::MonotonicitySetting(),
		uint64_t	monThresh = 0 )

Definition at line 358 of file storm-pars.cpp.

◆ parseRegions()

template<typename ValueType>

std::vector< storm::storage::ParameterRegion< ValueType > > storm::pars::parseRegions ( std::shared_ptr< storm::models::ModelBase > const & model )

Definition at line 63 of file storm-pars.cpp.

◆ parseSamples()

template<typename ValueType>

SampleInformation< ValueType > storm::pars::parseSamples	(	std::shared_ptr< storm::models::ModelBase > const &	model,
		std::string const &	sampleString,
		bool	graphPreserving )

Definition at line 262 of file sampling.h.

◆ performFeasibility() [1/2]

template void storm::pars::performFeasibility	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > >	model,
		std::shared_ptr< storm::pars::FeasibilitySynthesisTask const > const &	task,
		boost::optional< std::set< RationalFunctionVariable > >	omittedParameters,
		storm::api::MonotonicitySetting	monotonicitySettings )

◆ performFeasibility() [2/2]

template<typename ValueType>

void storm::pars::performFeasibility	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::sparse::Model< ValueType > >	model,
		std::shared_ptr< storm::pars::FeasibilitySynthesisTask const > const &	task,
		boost::optional< std::set< RationalFunctionVariable > >	omittedParameters,
		storm::api::MonotonicitySetting	monotonicitySettings )

Definition at line 87 of file feasibility.cpp.

◆ preprocessDdModel()

template<storm::dd::DdType DdType, typename ValueType>

PreprocessResult storm::pars::preprocessDdModel	(	std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &	model,
		cli::SymbolicInput const &	input,
		storm::cli::ModelProcessingInformation const &	mpi )

Definition at line 260 of file storm-pars.cpp.

◆ preprocessModel()

template<storm::dd::DdType DdType, typename ValueType>

PreprocessResult storm::pars::preprocessModel	(	std::shared_ptr< storm::models::ModelBase > const &	model,
		cli::SymbolicInput const &	input,
		storm::cli::ModelProcessingInformation const &	mpi )

Definition at line 290 of file storm-pars.cpp.

◆ preprocessSparseModel()

template<typename ValueType>

PreprocessResult storm::pars::preprocessSparseModel	(	std::shared_ptr< storm::models::sparse::Model< ValueType > > const &	model,
		cli::SymbolicInput const &	input,
		storm::cli::ModelProcessingInformation const &	mpi )

Definition at line 181 of file storm-pars.cpp.

◆ printFeasibilityResult()

template<typename VT1>

void storm::pars::printFeasibilityResult	(	bool	success,
		std::pair< VT1, typename storm::storage::ParameterRegion< storm::RationalFunction >::Valuation > const &	valueValuationPair,
		storm::utility::Stopwatch const &	watch )

Definition at line 23 of file feasibility.cpp.

◆ printInitialStatesResult()

template<typename ValueType>

void storm::pars::printInitialStatesResult	(	std::unique_ptr< storm::modelchecker::CheckResult > const &	result,
		storm::utility::Stopwatch *	watch,
		const storm::utility::parametric::Valuation< ValueType > *	valuation )

Definition at line 11 of file print.cpp.

◆ printInitialStatesResult< storm::RationalFunction >()

template void storm::pars::printInitialStatesResult< storm::RationalFunction >	(	std::unique_ptr< storm::modelchecker::CheckResult > const &	result,
		storm::utility::Stopwatch *	watch,
		const storm::utility::parametric::Valuation< storm::RationalFunction > *	valuation )

◆ processInput()

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

Definition at line 431 of file storm-pars.cpp.

◆ processOptions()

void storm::pars::processOptions ( )

Definition at line 584 of file storm-pars.cpp.

◆ runFeasibilityWithGD() [1/2]

template void storm::pars::runFeasibilityWithGD	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > >	model,
		std::shared_ptr< storm::pars::FeasibilitySynthesisTask const > const &	task,
		boost::optional< std::set< RationalFunctionVariable > >	omittedParameters,
		storm::api::MonotonicitySetting	monotonicitySettings )

◆ runFeasibilityWithGD() [2/2]

template<typename ValueType>

void storm::pars::runFeasibilityWithGD	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::sparse::Model< ValueType > >	model,
		std::shared_ptr< storm::pars::FeasibilitySynthesisTask const > const &	task,
		boost::optional< std::set< RationalFunctionVariable > >	omittedParameters,
		storm::api::MonotonicitySetting	monotonicitySettings )

Definition at line 112 of file feasibility.cpp.

◆ runFeasibilityWithPLA() [1/2]

template void storm::pars::runFeasibilityWithPLA	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > > const &	model,
		std::shared_ptr< storm::pars::FeasibilitySynthesisTask const > const &	task,
		boost::optional< std::set< RationalFunctionVariable > >	omittedParameters,
		storm::api::MonotonicitySetting	monotonicitySettings )

◆ runFeasibilityWithPLA() [2/2]

template<typename ValueType>

void storm::pars::runFeasibilityWithPLA	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::sparse::Model< ValueType > > const &	model,
		std::shared_ptr< storm::pars::FeasibilitySynthesisTask const > const &	task,
		boost::optional< std::set< RationalFunctionVariable > >	omittedParameters,
		storm::api::MonotonicitySetting	monotonicitySettings )

Definition at line 199 of file feasibility.cpp.

◆ sampleDerivatives()

template<typename ValueType>

void storm::pars::sampleDerivatives	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::sparse::Model< ValueType > >	model,
		cli::SymbolicInput const &	input,
		std::string const &	instantiationString )

Definition at line 333 of file sampling.h.

◆ simplifyModel()

template<typename ValueType>

std::shared_ptr< storm::models::ModelBase > storm::pars::simplifyModel	(	std::shared_ptr< storm::models::ModelBase > const &	model,
		cli::SymbolicInput const &	input )

Definition at line 149 of file storm-pars.cpp.

◆ verifyProperties()

template<typename ValueType>

void storm::pars::verifyProperties	(	std::vector< storm::jani::Property > const &	properties,
		std::function< std::unique_ptr< storm::modelchecker::CheckResult >(std::shared_ptr< storm::logic::Formula const > const &formula)> const &	verificationCallback,
		std::function< void(std::unique_ptr< storm::modelchecker::CheckResult > const &)> const &	postprocessingCallback )

Definition at line 43 of file solutionFunctions.cpp.

◆ verifyProperties< storm::RationalFunction >()

template void storm::pars::verifyProperties< storm::RationalFunction >	(	std::vector< storm::jani::Property > const &	,
		std::function< std::unique_ptr< storm::modelchecker::CheckResult >(std::shared_ptr< storm::logic::Formula const > const &)> const &	,
		std::function< void(std::unique_ptr< storm::modelchecker::CheckResult > const &)> const &	)

◆ verifyPropertiesAtSamplePoints()

template<template< typename, typename > class ModelCheckerType, typename ModelType, typename ValueType, typename SolveValueType = double, bool Derivative = false>

void storm::pars::verifyPropertiesAtSamplePoints	(	storm::Environment const &	env,
		ModelType const &	model,
		cli::SymbolicInput const &	input,
		SampleInformation< ValueType > const &	samples )

Definition at line 164 of file sampling.h.

◆ verifyPropertiesAtSamplePointsDerivative()

template<template< typename, typename > class ModelCheckerType, typename ModelType, typename ValueType, typename SolveValueType = double>

void storm::pars::verifyPropertiesAtSamplePointsDerivative	(	storm::Environment const &	env,
		ModelType const &	model,
		cli::SymbolicInput const &	input,
		SampleInformation< ValueType > const &	samples )

Definition at line 78 of file sampling.h.

◆ verifyPropertiesAtSamplePointsWithSparseEngine()

template<typename ValueType, typename SolveValueType = double>

void storm::pars::verifyPropertiesAtSamplePointsWithSparseEngine	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::sparse::Model< ValueType > > const &	model,
		cli::SymbolicInput const &	input,
		SampleInformation< ValueType > const &	samples )

Definition at line 245 of file sampling.h.

◆ verifyPropertiesAtSamplePointsWithSparseEngineDerivatives()

template<typename ValueType, typename SolveValueType = double>

void storm::pars::verifyPropertiesAtSamplePointsWithSparseEngineDerivatives	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::sparse::Model< ValueType > > const &	model,
		cli::SymbolicInput const &	input,
		SampleInformation< ValueType > const &	samples )

Definition at line 233 of file sampling.h.

◆ verifyRegionWithSparseEngine()

template<typename ValueType>

void storm::pars::verifyRegionWithSparseEngine	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::sparse::Model< ValueType > > const &	model,
		cli::SymbolicInput const &	input,
		std::vector< storm::storage::ParameterRegion< ValueType > > const &	regions,
		storm::api::MonotonicitySetting	monotonicitySettings = storm::api::MonotonicitySetting() )

Definition at line 309 of file storm-pars.cpp.

Namespaces

Classes

Enumerations

Functions

Enumeration Type Documentation

◆ FeasibilityMethod

Function Documentation

◆ analyzeMonotonicity() [1/2]

◆ analyzeMonotonicity() [2/2]

◆ checkRegionConstraints()

◆ collectConstraints()

◆ computeSolutionFunctionsWithSparseEngine()

◆ computeSolutionFunctionsWithSparseEngine< storm::RationalFunction >()

◆ computeSolutionFunctionsWithSymbolicEngine()

◆ computeSolutionFunctionsWithSymbolicEngine< storm::dd::DdType::Sylvan, storm::RationalFunction >()

◆ createFeasibilitySynthesisTaskFromSettings()

◆ describeViolation()

◆ eliminateScc()

◆ establishGraphPreservation()

◆ parameterSpacePartitioningWithSparseEngine()

◆ parseRegions()

◆ parseSamples()

◆ performFeasibility() [1/2]

◆ performFeasibility() [2/2]

◆ preprocessDdModel()

◆ preprocessModel()

◆ preprocessSparseModel()

◆ printFeasibilityResult()

◆ printInitialStatesResult()

◆ printInitialStatesResult< storm::RationalFunction >()

◆ processInput()

◆ processOptions()

◆ runFeasibilityWithGD() [1/2]

◆ runFeasibilityWithGD() [2/2]

◆ runFeasibilityWithPLA() [1/2]

◆ runFeasibilityWithPLA() [2/2]

◆ sampleDerivatives()

◆ simplifyModel()

◆ verifyProperties()

◆ verifyProperties< storm::RationalFunction >()

◆ verifyPropertiesAtSamplePoints()

◆ verifyPropertiesAtSamplePointsDerivative()

◆ verifyPropertiesAtSamplePointsWithSparseEngine()

◆ verifyPropertiesAtSamplePointsWithSparseEngineDerivatives()

◆ verifyRegionWithSparseEngine()