Namespaces
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 (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)
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	(	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 44 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 84 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 375 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 55 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 85 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 274 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 304 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 194 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 21 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 )

◆ processInput()

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

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

◆ processOptions()

void storm::pars::processOptions ( )

Definition at line 589 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 110 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 209 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 158 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 323 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 >()

◆ processInput()

◆ processOptions()

◆ runFeasibilityWithGD() [1/2]

◆ runFeasibilityWithGD() [2/2]

◆ runFeasibilityWithPLA() [1/2]

◆ runFeasibilityWithPLA() [2/2]

◆ sampleDerivatives()

◆ simplifyModel()

◆ verifyProperties()

◆ verifyPropertiesAtSamplePoints()

◆ verifyPropertiesAtSamplePointsWithSparseEngine()

◆ verifyRegionWithSparseEngine()