Namespaces
namespace	utility

Classes
class	FeasibilitySynthesisTask

struct	PreprocessResult

struct	SampleInformation

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 (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 (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 (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 (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 (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 (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 >
void	analyzeMonotonicity (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 (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	verifyPropertiesAtSamplePoints (ModelType const &model, cli::SymbolicInput const &input, SampleInformation< ValueType > const &samples)

template<typename ValueType , typename SolveValueType = double>
void	verifyPropertiesAtSamplePointsWithSparseEngine (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 (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 (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, cli::SymbolicInput const &input)

template<storm::dd::DdType DdType, typename ValueType >
void	computeSolutionFunctionsWithSymbolicEngine (std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model, cli::SymbolicInput const &input)

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 (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 (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)

template<storm::dd::DdType DdType, typename ValueType >
void	processInputWithValueTypeAndDdlib (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	(	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	(	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 34 of file monotonicity.cpp.

◆ computeSolutionFunctionsWithSparseEngine()

template<typename ValueType >

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

Definition at line 27 of file solutionFunctions.h.

◆ computeSolutionFunctionsWithSymbolicEngine()

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

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

Definition at line 55 of file solutionFunctions.h.

◆ 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 40 of file feasibility.cpp.

◆ eliminateScc()

template<typename ValueType >

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

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

◆ parameterSpacePartitioningWithSparseEngine()

template<typename ValueType >

void storm::pars::parameterSpacePartitioningWithSparseEngine	(	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 345 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 77 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 163 of file sampling.h.

◆ performFeasibility() [1/2]

template void storm::pars::performFeasibility	(	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	(	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 81 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 273 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 303 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 199 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 17 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 10 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
	)

◆ processInputWithValueTypeAndDdlib()

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

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

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

◆ processOptions()

void storm::pars::processOptions ( )

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

◆ runFeasibilityWithGD() [1/2]

template void storm::pars::runFeasibilityWithGD	(	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	(	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 106 of file feasibility.cpp.

◆ runFeasibilityWithPLA() [1/2]

template void storm::pars::runFeasibilityWithPLA	(	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	(	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 188 of file feasibility.cpp.

◆ sampleDerivatives()

template<typename ValueType >

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

Definition at line 234 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 163 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 8 of file solutionFunctions.h.

◆ verifyPropertiesAtSamplePoints()

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

void storm::pars::verifyPropertiesAtSamplePoints	(	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	(	std::shared_ptr< storm::models::sparse::Model< ValueType > > const &	model,
		cli::SymbolicInput const &	input,
		SampleInformation< ValueType > const &	samples
	)

Definition at line 146 of file sampling.h.

◆ verifyRegionWithSparseEngine()

template<typename ValueType >

void storm::pars::verifyRegionWithSparseEngine	(	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 322 of file storm-pars.cpp.

Namespaces

Classes

Enumerations

Functions

Enumeration Type Documentation

◆ FeasibilityMethod

Function Documentation

◆ analyzeMonotonicity() [1/2]

◆ analyzeMonotonicity() [2/2]

◆ computeSolutionFunctionsWithSparseEngine()

◆ computeSolutionFunctionsWithSymbolicEngine()

◆ createFeasibilitySynthesisTaskFromSettings()

◆ eliminateScc()

◆ parameterSpacePartitioningWithSparseEngine()

◆ parseRegions()

◆ parseSamples()

◆ performFeasibility() [1/2]

◆ performFeasibility() [2/2]

◆ preprocessDdModel()

◆ preprocessModel()

◆ preprocessSparseModel()

◆ printFeasibilityResult()

◆ printInitialStatesResult()

◆ printInitialStatesResult< storm::RationalFunction >()

◆ processInputWithValueTypeAndDdlib()

◆ processOptions()

◆ runFeasibilityWithGD() [1/2]

◆ runFeasibilityWithGD() [2/2]

◆ runFeasibilityWithPLA() [1/2]

◆ runFeasibilityWithPLA() [2/2]

◆ sampleDerivatives()

◆ simplifyModel()

◆ verifyProperties()

◆ verifyPropertiesAtSamplePoints()

◆ verifyPropertiesAtSamplePointsWithSparseEngine()

◆ verifyRegionWithSparseEngine()