Classes
struct	MonotonicitySetting

Functions
void	transformJani (storm::jani::Model &janiModel, std::vector< storm::jani::Property > &properties, storm::converter::JaniConversionOptions const &options)

void	transformPrism (storm::prism::Program &prismProgram, std::vector< storm::jani::Property > &properties, bool simplify, bool flatten)

std::pair< storm::jani::Model, std::vector< storm::jani::Property > >	convertPrismToJani (storm::prism::Program const &program, storm::converter::PrismToJaniConverterOptions options)

std::pair< storm::jani::Model, std::vector< storm::jani::Property > >	convertPrismToJani (storm::prism::Program const &program, std::vector< storm::jani::Property > const &properties, storm::converter::PrismToJaniConverterOptions options)

void	exportJaniToFile (storm::jani::Model const &model, std::vector< storm::jani::Property > const &properties, std::string const &filename, bool compact)

void	printJaniToStream (storm::jani::Model const &model, std::vector< storm::jani::Property > const &properties, std::ostream &ostream, bool compact)

void	exportPrismToFile (storm::prism::Program const &program, std::vector< storm::jani::Property > const &properties, std::string const &filename)

void	printPrismToStream (storm::prism::Program const &program, std::vector< storm::jani::Property > const &properties, std::ostream &ostream)

std::shared_ptr< storm::counterexamples::Counterexample >	computeHighLevelCounterexampleMilp (storm::storage::SymbolicModelDescription const &symbolicModel, std::shared_ptr< storm::models::sparse::Mdp< double > > mdp, std::shared_ptr< storm::logic::Formula const > const &formula)

std::shared_ptr< storm::counterexamples::Counterexample >	computeHighLevelCounterexampleMaxSmt (storm::storage::SymbolicModelDescription const &symbolicModel, std::shared_ptr< storm::models::sparse::Model< double > > model, std::shared_ptr< storm::logic::Formula const > const &formula)

std::shared_ptr< storm::counterexamples::Counterexample >	computeKShortestPathCounterexample (std::shared_ptr< storm::models::sparse::Model< double > > model, std::shared_ptr< storm::logic::Formula const > const &formula, size_t maxK)

storm::jani::Model *	buildJani (storm::gspn::GSPN const &gspn)
	Builds JANI model from GSPN.

void	handleGSPNExportSettings (storm::gspn::GSPN const &gspn, std::function< std::vector< storm::jani::Property >(storm::builder::JaniGSPNBuilder const &)> const &janiProperyGetter)

std::unordered_map< std::string, uint64_t >	parseCapacitiesList (std::string const &filename, storm::gspn::GSPN const &gspn)

template<typename ValueType >
void	exportParametricResultToFile (std::optional< ValueType >, storm::OptionalRef< storm::analysis::ConstraintCollector< ValueType > const > const &, std::string const &)

template<>
void	exportParametricResultToFile (std::optional< storm::RationalFunction > result, storm::OptionalRef< storm::analysis::ConstraintCollector< storm::RationalFunction > const > const &constraintCollector, std::string const &path)

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

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

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

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

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

template<typename ValueType >
storm::storage::ParameterRegion< ValueType >	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 > >	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 > >	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 > >	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 > >	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 > >	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 > >	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 > >	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 >
std::unique_ptr< storm::modelchecker::RegionRefinementCheckResult< ValueType > >	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 &region, 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 >	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 &region, 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	verifyRegion (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, storm::logic::Formula const &formula, storm::storage::ParameterRegion< ValueType > const &region, 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	exportRegionCheckResultToFile (std::unique_ptr< storm::modelchecker::CheckResult > const &checkResult, std::string const &filename, bool onlyConclusiveResults=false)

template<typename ValueType >
std::shared_ptr< storm::models::sparse::Model< ValueType > >	buildExplicitModel (std::string const &transitionsFile, std::string const &labelingFile, boost::optional< std::string > const &stateRewardsFile, boost::optional< std::string > const &transitionRewardsFile, boost::optional< std::string > const &choiceLabelingFile)

template<typename ValueType >
std::shared_ptr< storm::models::sparse::Model< ValueType > >	buildExplicitDRNModel (std::string const &drnFile, storm::parser::DirectEncodingParserOptions const &options=storm::parser::DirectEncodingParserOptions())

template<typename ValueType >
std::shared_ptr< storm::models::sparse::Model< ValueType > >	buildExplicitIMCAModel (std::string const &imcaFile)

storm::prism::Program	parseProgram (std::string const &filename, bool prismCompatibility, bool simplify)

std::pair< storm::jani::Model, std::vector< storm::jani::Property > >	filterProperties (std::pair< storm::jani::Model, std::vector< storm::jani::Property > > &modelAndFormulae, boost::optional< std::vector< std::string > > const &propertyFilter)

std::pair< storm::jani::Model, std::vector< storm::jani::Property > >	parseJaniModel (std::string const &filename, boost::optional< std::vector< std::string > > const &propertyFilter)

std::pair< storm::jani::Model, std::vector< storm::jani::Property > >	parseJaniModelFromString (std::string const &jsonstring, boost::optional< std::vector< std::string > > const &propertyFilter)

std::pair< storm::jani::Model, std::vector< storm::jani::Property > >	parseJaniModel (std::string const &filename, storm::jani::ModelFeatures const &supportedFeatures, boost::optional< std::vector< std::string > > const &propertyFilter)

std::pair< storm::jani::Model, std::vector< storm::jani::Property > >	parseJaniModelFromString (std::string const &jsonstring, storm::jani::ModelFeatures const &supportedFeatures, boost::optional< std::vector< std::string > > const &propertyFilter)

void	simplifyJaniModel (storm::jani::Model &model, std::vector< storm::jani::Property > &properties, storm::jani::ModelFeatures const &supportedFeatures)

boost::optional< std::set< std::string > >	parsePropertyFilter (std::string const &propertyFilter)

std::vector< storm::jani::Property >	parseProperties (storm::parser::FormulaParser &formulaParser, std::string const &inputString, boost::optional< std::set< std::string > > const &propertyFilter)

std::vector< storm::jani::Property >	parseProperties (std::string const &inputString, boost::optional< std::set< std::string > > const &propertyFilter)

std::vector< storm::jani::Property >	parsePropertiesForJaniModel (std::string const &inputString, storm::jani::Model const &model, boost::optional< std::set< std::string > > const &propertyFilter)

std::vector< storm::jani::Property >	parsePropertiesForPrismProgram (std::string const &inputString, storm::prism::Program const &program, boost::optional< std::set< std::string > > const &propertyFilter)

std::vector< storm::jani::Property >	parsePropertiesForSymbolicModelDescription (std::string const &inputString, storm::storage::SymbolicModelDescription const &modelDescription, boost::optional< std::set< std::string > > const &propertyFilter)

template<typename ModelType >
std::shared_ptr< ModelType >	performDeterministicSparseBisimulationMinimization (std::shared_ptr< ModelType > model, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas, storm::storage::BisimulationType type, bool graphPreserving=true)

template<typename ModelType >
std::shared_ptr< ModelType >	performNondeterministicSparseBisimulationMinimization (std::shared_ptr< ModelType > model, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas, storm::storage::BisimulationType type, bool graphPreserving=true)

template<typename ValueType >
std::shared_ptr< storm::models::sparse::Model< ValueType > >	performBisimulationMinimization (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas, storm::storage::BisimulationType type=storm::storage::BisimulationType::Strong, bool graphPreserving=true)

template<storm::dd::DdType DdType, typename ValueType , typename ExportValueType = ValueType>
std::enable_if< DdType==storm::dd::DdType::Sylvan\|\|std::is_same< ValueType, double >::value, std::shared_ptr< storm::models::Model< ExportValueType > > >::type	performBisimulationMinimization (std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas, storm::storage::BisimulationType const &bisimulationType=storm::storage::BisimulationType::Strong, storm::dd::bisimulation::SignatureMode const &mode=storm::dd::bisimulation::SignatureMode::Eager, storm::dd::bisimulation::QuotientFormat const &quotientFormat=storm::dd::bisimulation::QuotientFormat::Dd)

template<storm::dd::DdType DdType, typename ValueType , typename ExportValueType = ValueType>
std::enable_if< DdType!=storm::dd::DdType::Sylvan &&!std::is_same< ValueType, double >::value, std::shared_ptr< storm::models::Model< ExportValueType > > >::type	performBisimulationMinimization (std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &, std::vector< std::shared_ptr< storm::logic::Formula const > > const &, storm::storage::BisimulationType const &=storm::storage::BisimulationType::Strong, storm::dd::bisimulation::SignatureMode const &=storm::dd::bisimulation::SignatureMode::Eager, storm::dd::bisimulation::QuotientFormat const &=storm::dd::bisimulation::QuotientFormat::Dd)

storm::jani::ModelFeatures	getSupportedJaniFeatures (storm::builder::BuilderType const &builderType)

template<storm::dd::DdType LibraryType, typename ValueType >
std::shared_ptr< storm::models::symbolic::Model< LibraryType, ValueType > >	buildSymbolicModel (storm::storage::SymbolicModelDescription const &model, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas, bool buildFullModel=false, bool applyMaximumProgress=true)

template<>
std::shared_ptr< storm::models::symbolic::Model< storm::dd::DdType::CUDD, storm::RationalNumber > >	buildSymbolicModel (storm::storage::SymbolicModelDescription const &, std::vector< std::shared_ptr< storm::logic::Formula const > > const &, bool, bool)

template<>
std::shared_ptr< storm::models::symbolic::Model< storm::dd::DdType::CUDD, storm::RationalFunction > >	buildSymbolicModel (storm::storage::SymbolicModelDescription const &, std::vector< std::shared_ptr< storm::logic::Formula const > > const &, bool, bool)

template<typename ValueType >
storm::builder::ExplicitModelBuilder< ValueType >	makeExplicitModelBuilder (storm::storage::SymbolicModelDescription const &model, storm::builder::BuilderOptions const &options, std::shared_ptr< storm::generator::ActionMask< ValueType > > actionMask=nullptr)
	Initializes an explict model builder; an object/algorithm that is used to build sparse models.

template<typename ValueType >
std::shared_ptr< storm::models::sparse::Model< ValueType > >	buildSparseModel (storm::storage::SymbolicModelDescription const &model, storm::builder::BuilderOptions const &options)

template<typename ValueType >
std::shared_ptr< storm::models::sparse::Model< ValueType > >	buildSparseModel (storm::storage::SymbolicModelDescription const &model, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas)

template<typename ValueType , typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>
std::shared_ptr< storm::models::sparse::Model< ValueType, RewardModelType > >	buildSparseModel (storm::models::ModelType modelType, storm::storage::sparse::ModelComponents< ValueType, RewardModelType > &&components)

void	exportJaniModelAsDot (storm::jani::Model const &model, std::string const &filename)

template<typename ValueType >
void	exportSparseModelAsDrn (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, std::string const &filename, std::vector< std::string > const &parameterNames={}, bool allowPlaceholders=true)

template<storm::dd::DdType Type, typename ValueType >
void	exportSymbolicModelAsDrdd (std::shared_ptr< storm::models::symbolic::Model< Type, ValueType > > const &model, std::string const &filename)

template<typename ValueType >
void	exportSparseModelAsDot (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, std::string const &filename, size_t maxWidth=30)

template<typename ValueType >
void	exportSparseModelAsJson (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, std::string const &filename)

template<storm::dd::DdType Type, typename ValueType >
void	exportSymbolicModelAsDot (std::shared_ptr< storm::models::symbolic::Model< Type, ValueType > > const &model, std::string const &filename)

template<typename ValueType >
void	exportScheduler (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, storm::storage::Scheduler< ValueType > const &scheduler, std::string const &filename)

template<typename ValueType >
void	exportCheckResultToJson (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, std::unique_ptr< storm::modelchecker::CheckResult > const &checkResult, std::string const &filename)

template<>
void	exportCheckResultToJson< storm::RationalFunction > (std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > > const &, std::unique_ptr< storm::modelchecker::CheckResult > const &, std::string const &)

std::vector< storm::jani::Property >	substituteConstantsInProperties (std::vector< storm::jani::Property > const &properties, std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution)

std::vector< storm::jani::Property >	substituteTranscendentalNumbersInProperties (std::vector< storm::jani::Property > const &properties)

std::vector< storm::jani::Property >	filterProperties (std::vector< storm::jani::Property > const &properties, boost::optional< std::set< std::string > > const &propertyFilter)

std::vector< std::shared_ptr< storm::logic::Formula const > >	extractFormulasFromProperties (std::vector< storm::jani::Property > const &properties)

storm::jani::Property	createMultiObjectiveProperty (std::vector< storm::jani::Property > const &properties)

template<typename ValueType >
std::pair< std::shared_ptr< storm::models::sparse::Model< ValueType > >, std::vector< std::shared_ptr< storm::logic::Formula const > > >	eliminateNonMarkovianChains (std::shared_ptr< storm::models::sparse::MarkovAutomaton< ValueType > > const &ma, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas, storm::transformer::EliminationLabelBehavior labelBehavior)
	Eliminates chains of non-Markovian states from a given Markov Automaton.

template<typename ValueType >
std::pair< std::shared_ptr< storm::models::sparse::Model< ValueType > >, std::vector< std::shared_ptr< storm::logic::Formula const > > >	transformContinuousToDiscreteTimeSparseModel (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas)
	Transforms the given continuous model to a discrete time model.

template<typename ValueType >
std::pair< std::shared_ptr< storm::models::sparse::Model< ValueType > >, std::vector< std::shared_ptr< storm::logic::Formula const > > >	transformContinuousToDiscreteTimeSparseModel (storm::models::sparse::Model< ValueType > &&model, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas)
	Transforms the given continuous model to a discrete time model IN PLACE.

template<typename ValueType >
std::shared_ptr< storm::logic::Formula const >	checkAndTransformContinuousToDiscreteTimeFormula (storm::logic::Formula const &formula, std::string const &timeRewardName="_time")

template<storm::dd::DdType Type, typename ValueType >
std::shared_ptr< storm::models::sparse::Model< ValueType > >	transformSymbolicToSparseModel (std::shared_ptr< storm::models::symbolic::Model< Type, ValueType > > const &symbolicModel, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas=std::vector< std::shared_ptr< storm::logic::Formula const > >())
	Transforms the given symbolic model to a sparse model.

template<typename ValueType >
std::shared_ptr< storm::models::sparse::Model< ValueType > >	transformToNondeterministicModel (storm::models::sparse::Model< ValueType > &&model)

template<typename ValueType >
std::shared_ptr< storm::models::sparse::Model< ValueType > >	permuteModelStates (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, storm::utility::permutation::OrderKind order, std::optional< uint64_t > seed=std::nullopt)
	Permutes the order of the states of the model according to the given order.

template<typename ValueType >
storm::modelchecker::CheckTask< storm::logic::Formula, ValueType >	createTask (std::shared_ptr< const storm::logic::Formula > const &formula, bool onlyInitialStatesRelevant=false)

template<typename ValueType >
std::enable_if< std::is_same< ValueType, double >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type	verifyWithExplorationEngine (storm::Environment const &env, storm::storage::SymbolicModelDescription const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

template<typename ValueType >
std::enable_if<!std::is_same< ValueType, double >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type	verifyWithExplorationEngine (storm::Environment const &, storm::storage::SymbolicModelDescription const &, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &)

template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	verifyWithExplorationEngine (storm::storage::SymbolicModelDescription const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	verifyWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Dtmc< ValueType > > const &dtmc, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	verifyWithSparseEngine (std::shared_ptr< storm::models::sparse::Dtmc< ValueType > > const &dtmc, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	verifyWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Ctmc< ValueType > > const &ctmc, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	verifyWithSparseEngine (std::shared_ptr< storm::models::sparse::Ctmc< ValueType > > const &ctmc, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

template<typename ValueType >
std::enable_if<!std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type	verifyWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Mdp< ValueType > > const &mdp, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

template<typename ValueType >
std::enable_if< std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type	verifyWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Mdp< ValueType > > const &mdp, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	verifyWithSparseEngine (std::shared_ptr< storm::models::sparse::Mdp< ValueType > > const &mdp, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

template<typename ValueType >
std::enable_if<!std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type	verifyWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::MarkovAutomaton< ValueType > > const &ma, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

template<typename ValueType >
std::enable_if< std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type	verifyWithSparseEngine (storm::Environment const &, std::shared_ptr< storm::models::sparse::MarkovAutomaton< ValueType > > const &, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &)

template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	verifyWithSparseEngine (std::shared_ptr< storm::models::sparse::MarkovAutomaton< ValueType > > const &ma, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

template<typename ValueType >
std::enable_if<!std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type	verifyWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Smg< ValueType > > const &smg, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

template<typename ValueType >
std::enable_if< std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type	verifyWithSparseEngine (storm::Environment const &, std::shared_ptr< storm::models::sparse::Smg< ValueType > > const &, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &)

template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	verifyWithSparseEngine (std::shared_ptr< storm::models::sparse::Smg< ValueType > > const &smg, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	verifyWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	verifyWithSparseEngine (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	computeSteadyStateDistributionWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Dtmc< ValueType > > const &dtmc)

template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	computeSteadyStateDistributionWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Ctmc< ValueType > > const &ctmc)

template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	computeSteadyStateDistributionWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model)

template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	computeExpectedVisitingTimesWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Dtmc< ValueType > > const &dtmc)

template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	computeExpectedVisitingTimesWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Ctmc< ValueType > > const &ctmc)

template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	computeExpectedVisitingTimesWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model)

template<storm::dd::DdType DdType, typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	verifyWithHybridEngine (storm::Environment const &env, std::shared_ptr< storm::models::symbolic::Dtmc< DdType, ValueType > > const &dtmc, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

template<storm::dd::DdType DdType, typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	verifyWithHybridEngine (std::shared_ptr< storm::models::symbolic::Dtmc< DdType, ValueType > > const &dtmc, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

template<storm::dd::DdType DdType, typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	verifyWithHybridEngine (storm::Environment const &env, std::shared_ptr< storm::models::symbolic::Ctmc< DdType, ValueType > > const &ctmc, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

template<storm::dd::DdType DdType, typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	verifyWithHybridEngine (std::shared_ptr< storm::models::symbolic::Ctmc< DdType, ValueType > > const &ctmc, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

template<storm::dd::DdType DdType, typename ValueType >
std::enable_if<!std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type	verifyWithHybridEngine (storm::Environment const &env, std::shared_ptr< storm::models::symbolic::Mdp< DdType, ValueType > > const &mdp, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

template<storm::dd::DdType DdType, typename ValueType >
std::enable_if< std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type	verifyWithHybridEngine (storm::Environment const &, std::shared_ptr< storm::models::symbolic::Mdp< DdType, ValueType > > const &, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &)

template<storm::dd::DdType DdType, typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	verifyWithHybridEngine (std::shared_ptr< storm::models::symbolic::Mdp< DdType, ValueType > > const &mdp, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

template<storm::dd::DdType DdType, typename ValueType >
std::enable_if<!std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type	verifyWithHybridEngine (storm::Environment const &env, std::shared_ptr< storm::models::symbolic::MarkovAutomaton< DdType, ValueType > > const &ma, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

template<storm::dd::DdType DdType, typename ValueType >
std::enable_if< std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type	verifyWithHybridEngine (storm::Environment const &, std::shared_ptr< storm::models::symbolic::MarkovAutomaton< DdType, ValueType > > const &, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &)

template<storm::dd::DdType DdType, typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	verifyWithHybridEngine (std::shared_ptr< storm::models::symbolic::MarkovAutomaton< DdType, ValueType > > const &ma, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

template<storm::dd::DdType DdType, typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	verifyWithHybridEngine (storm::Environment const &env, std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

template<storm::dd::DdType DdType, typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	verifyWithHybridEngine (std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

template<storm::dd::DdType DdType, typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	verifyWithDdEngine (storm::Environment const &env, std::shared_ptr< storm::models::symbolic::Dtmc< DdType, ValueType > > const &dtmc, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

template<storm::dd::DdType DdType, typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	verifyWithDdEngine (std::shared_ptr< storm::models::symbolic::Dtmc< DdType, ValueType > > const &dtmc, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

template<storm::dd::DdType DdType, typename ValueType >
std::enable_if<!std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type	verifyWithDdEngine (storm::Environment const &env, std::shared_ptr< storm::models::symbolic::Mdp< DdType, ValueType > > const &mdp, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

template<storm::dd::DdType DdType, typename ValueType >
std::enable_if< std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type	verifyWithDdEngine (storm::Environment const &, std::shared_ptr< storm::models::symbolic::Mdp< DdType, ValueType > > const &, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &)

template<storm::dd::DdType DdType, typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	verifyWithDdEngine (std::shared_ptr< storm::models::symbolic::Mdp< DdType, ValueType > > const &mdp, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

template<storm::dd::DdType DdType, typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	verifyWithDdEngine (storm::Environment const &env, std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

template<storm::dd::DdType DdType, typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResult >	verifyWithDdEngine (std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)

Function Documentation

◆ buildExplicitDRNModel()

template<typename ValueType >

std::shared_ptr< storm::models::sparse::Model< ValueType > > storm::api::buildExplicitDRNModel	(	std::string const &	drnFile,
		storm::parser::DirectEncodingParserOptions const &	options = `storm::parser::DirectEncodingParserOptions()`
	)

Definition at line 30 of file explicit_models.h.

◆ buildExplicitIMCAModel()

template<typename ValueType >

std::shared_ptr< storm::models::sparse::Model< ValueType > > storm::api::buildExplicitIMCAModel ( std::string const & imcaFile )

Definition at line 36 of file explicit_models.h.

◆ buildExplicitModel()

template<typename ValueType >

std::shared_ptr< storm::models::sparse::Model< ValueType > > storm::api::buildExplicitModel	(	std::string const &	transitionsFile,
		std::string const &	labelingFile,
		boost::optional< std::string > const &	stateRewardsFile,
		boost::optional< std::string > const &	transitionRewardsFile,
		boost::optional< std::string > const &	choiceLabelingFile
	)

inline

Definition at line 17 of file explicit_models.h.

◆ buildJani()

storm::jani::Model * storm::api::buildJani ( storm::gspn::GSPN const & gspn )

Builds JANI model from GSPN.

Definition at line 15 of file storm-gspn.cpp.

◆ buildSparseModel() [1/3]

template<typename ValueType , typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>

std::shared_ptr< storm::models::sparse::Model< ValueType, RewardModelType > > storm::api::buildSparseModel	(	storm::models::ModelType	modelType,
		storm::storage::sparse::ModelComponents< ValueType, RewardModelType > &&	components
	)

Definition at line 119 of file builder.h.

◆ buildSparseModel() [2/3]

template<typename ValueType >

std::shared_ptr< storm::models::sparse::Model< ValueType > > storm::api::buildSparseModel	(	storm::storage::SymbolicModelDescription const &	model,
		std::vector< std::shared_ptr< storm::logic::Formula const > > const &	formulas
	)

Definition at line 112 of file builder.h.

◆ buildSparseModel() [3/3]

template<typename ValueType >

std::shared_ptr< storm::models::sparse::Model< ValueType > > storm::api::buildSparseModel	(	storm::storage::SymbolicModelDescription const &	model,
		storm::builder::BuilderOptions const &	options
	)

Definition at line 105 of file builder.h.

◆ buildSymbolicModel() [1/3]

template<>

std::shared_ptr< storm::models::symbolic::Model< storm::dd::DdType::CUDD, storm::RationalNumber > > storm::api::buildSymbolicModel	(	storm::storage::SymbolicModelDescription const &	,
		std::vector< std::shared_ptr< storm::logic::Formula const > > const &	,
		bool	,
		bool
	)

inline

Definition at line 69 of file builder.h.

◆ buildSymbolicModel() [2/3]

template<>

std::shared_ptr< storm::models::symbolic::Model< storm::dd::DdType::CUDD, storm::RationalFunction > > storm::api::buildSymbolicModel	(	storm::storage::SymbolicModelDescription const &	,
		std::vector< std::shared_ptr< storm::logic::Formula const > > const &	,
		bool	,
		bool
	)

inline

Definition at line 75 of file builder.h.

◆ buildSymbolicModel() [3/3]

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

std::shared_ptr< storm::models::symbolic::Model< LibraryType, ValueType > > storm::api::buildSymbolicModel	(	storm::storage::SymbolicModelDescription const &	model,
		std::vector< std::shared_ptr< storm::logic::Formula const > > const &	formulas,
		bool	buildFullModel = `false`,
		bool	applyMaximumProgress = `true`
	)

Definition at line 36 of file builder.h.

◆ checkAndRefineRegionWithSparseEngine()

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 &	region,
		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.

Parameters

engine	The considered region checking engine
coverageThreshold	if given, the refinement stops as soon as the fraction of the area of the subregions with inconclusive result is less then this threshold
refinementDepthThreshold	if given, the refinement stops at the given depth. depth=0 means no refinement.
hypothesis	if not 'unknown', it is only checked whether the hypothesis holds (and NOT the complementary result).
allowModelSimplification
useMonotonicity
monThresh	if given, determines at which depth to start using monotonicity

Definition at line 285 of file region.h.

◆ checkAndTransformContinuousToDiscreteTimeFormula()

template<typename ValueType >

std::shared_ptr< storm::logic::Formula const > storm::api::checkAndTransformContinuousToDiscreteTimeFormula	(	storm::logic::Formula const &	formula,
		std::string const &	timeRewardName = `"_time"`
	)

Definition at line 94 of file transformation.h.

◆ checkRegionsWithSparseEngine() [1/2]

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
	)

Definition at line 254 of file region.h.

◆ checkRegionsWithSparseEngine() [2/2]

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

Definition at line 264 of file region.h.

◆ computeExpectedVisitingTimesWithSparseEngine() [1/3]

template<typename ValueType >

std::unique_ptr< storm::modelchecker::CheckResult > storm::api::computeExpectedVisitingTimesWithSparseEngine	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::sparse::Ctmc< ValueType > > const &	ctmc
	)

Definition at line 298 of file verification.h.

◆ computeExpectedVisitingTimesWithSparseEngine() [2/3]

template<typename ValueType >

std::unique_ptr< storm::modelchecker::CheckResult > storm::api::computeExpectedVisitingTimesWithSparseEngine	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::sparse::Dtmc< ValueType > > const &	dtmc
	)

Definition at line 290 of file verification.h.

◆ computeExpectedVisitingTimesWithSparseEngine() [3/3]

template<typename ValueType >

std::unique_ptr< storm::modelchecker::CheckResult > storm::api::computeExpectedVisitingTimesWithSparseEngine	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::sparse::Model< ValueType > > const &	model
	)

Definition at line 306 of file verification.h.

◆ computeExtremalValue()

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 &	region,
		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.

Definition at line 302 of file region.h.

◆ computeHighLevelCounterexampleMaxSmt()

std::shared_ptr< storm::counterexamples::Counterexample > storm::api::computeHighLevelCounterexampleMaxSmt	(	storm::storage::SymbolicModelDescription const &	symbolicModel,
		std::shared_ptr< storm::models::sparse::Model< double > >	model,
		std::shared_ptr< storm::logic::Formula const > const &	formula
	)

Definition at line 16 of file counterexamples.cpp.

◆ computeHighLevelCounterexampleMilp()

std::shared_ptr< storm::counterexamples::Counterexample > storm::api::computeHighLevelCounterexampleMilp	(	storm::storage::SymbolicModelDescription const &	symbolicModel,
		std::shared_ptr< storm::models::sparse::Mdp< double > >	mdp,
		std::shared_ptr< storm::logic::Formula const > const &	formula
	)

Definition at line 9 of file counterexamples.cpp.

◆ computeKShortestPathCounterexample()

std::shared_ptr< storm::counterexamples::Counterexample > storm::api::computeKShortestPathCounterexample	(	std::shared_ptr< storm::models::sparse::Model< double > >	model,
		std::shared_ptr< storm::logic::Formula const > const &	formula,
		size_t	maxK
	)

Definition at line 23 of file counterexamples.cpp.

◆ computeSteadyStateDistributionWithSparseEngine() [1/3]

template<typename ValueType >

std::unique_ptr< storm::modelchecker::CheckResult > storm::api::computeSteadyStateDistributionWithSparseEngine	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::sparse::Ctmc< ValueType > > const &	ctmc
	)

Definition at line 267 of file verification.h.

◆ computeSteadyStateDistributionWithSparseEngine() [2/3]

template<typename ValueType >

std::unique_ptr< storm::modelchecker::CheckResult > storm::api::computeSteadyStateDistributionWithSparseEngine	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::sparse::Dtmc< ValueType > > const &	dtmc
	)

Definition at line 259 of file verification.h.

◆ computeSteadyStateDistributionWithSparseEngine() [3/3]

template<typename ValueType >

std::unique_ptr< storm::modelchecker::CheckResult > storm::api::computeSteadyStateDistributionWithSparseEngine	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::sparse::Model< ValueType > > const &	model
	)

Definition at line 275 of file verification.h.

◆ convertPrismToJani() [1/2]

std::pair< storm::jani::Model, std::vector< storm::jani::Property > > storm::api::convertPrismToJani	(	storm::prism::Program const &	program,
		std::vector< storm::jani::Property > const &	properties,
		storm::converter::PrismToJaniConverterOptions	options
	)

Definition at line 116 of file storm-conv.cpp.

◆ convertPrismToJani() [2/2]

std::pair< storm::jani::Model, std::vector< storm::jani::Property > > storm::api::convertPrismToJani	(	storm::prism::Program const &	program,
		storm::converter::PrismToJaniConverterOptions	options
	)

Definition at line 111 of file storm-conv.cpp.

◆ createMultiObjectiveProperty()

storm::jani::Property storm::api::createMultiObjectiveProperty ( std::vector< storm::jani::Property > const & properties )

Definition at line 72 of file properties.cpp.

◆ createRegion() [1/2]

template<typename ValueType >

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

Definition at line 60 of file region.h.

◆ createRegion() [2/2]

template<typename ValueType >

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

Definition at line 80 of file region.h.

◆ createTask()

template<typename ValueType >

storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > storm::api::createTask	(	std::shared_ptr< const storm::logic::Formula > const &	formula,
		bool	onlyInitialStatesRelevant = `false`
	)

Definition at line 44 of file verification.h.

◆ eliminateNonMarkovianChains()

template<typename ValueType >

std::pair< std::shared_ptr< storm::models::sparse::Model< ValueType > >, std::vector< std::shared_ptr< storm::logic::Formula const > > > storm::api::eliminateNonMarkovianChains	(	std::shared_ptr< storm::models::sparse::MarkovAutomaton< ValueType > > const &	ma,
		std::vector< std::shared_ptr< storm::logic::Formula const > > const &	formulas,
		storm::transformer::EliminationLabelBehavior	labelBehavior
	)

Eliminates chains of non-Markovian states from a given Markov Automaton.

Definition at line 21 of file transformation.h.

◆ exportCheckResultToJson()

template<typename ValueType >

void storm::api::exportCheckResultToJson	(	std::shared_ptr< storm::models::sparse::Model< ValueType > > const &	model,
		std::unique_ptr< storm::modelchecker::CheckResult > const &	checkResult,
		std::string const &	filename
	)

inline

Definition at line 76 of file export.h.

◆ exportCheckResultToJson< storm::RationalFunction >()

template<>

void storm::api::exportCheckResultToJson< storm::RationalFunction >	(	std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > > const &	,
		std::unique_ptr< storm::modelchecker::CheckResult > const &	,
		std::string const &
	)

inline

Definition at line 93 of file export.h.

◆ exportJaniModelAsDot()

void storm::api::exportJaniModelAsDot	(	storm::jani::Model const &	model,
		std::string const &	filename
	)

Definition at line 7 of file export.cpp.

◆ exportJaniToFile()

void storm::api::exportJaniToFile	(	storm::jani::Model const &	model,
		std::vector< storm::jani::Property > const &	properties,
		std::string const &	filename,
		bool	compact
	)

Definition at line 135 of file storm-conv.cpp.

◆ exportParametricResultToFile() [1/2]

template<>

void storm::api::exportParametricResultToFile	(	std::optional< storm::RationalFunction >	result,
		storm::OptionalRef< storm::analysis::ConstraintCollector< storm::RationalFunction > const > const &	constraintCollector,
		std::string const &	path
	)

inline

Definition at line 16 of file export.h.

◆ exportParametricResultToFile() [2/2]

template<typename ValueType >

void storm::api::exportParametricResultToFile	(	std::optional< ValueType >	,
		storm::OptionalRef< storm::analysis::ConstraintCollector< ValueType > const > const &	,
		std::string const &
	)

Definition at line 10 of file export.h.

◆ exportPrismToFile()

void storm::api::exportPrismToFile	(	storm::prism::Program const &	program,
		std::vector< storm::jani::Property > const &	properties,
		std::string const &	filename
	)

Definition at line 143 of file storm-conv.cpp.

◆ exportRegionCheckResultToFile()

template<typename ValueType >

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

Definition at line 349 of file region.h.

◆ exportScheduler()

template<typename ValueType >

void storm::api::exportScheduler	(	std::shared_ptr< storm::models::sparse::Model< ValueType > > const &	model,
		storm::storage::Scheduler< ValueType > const &	scheduler,
		std::string const &	filename
	)

Definition at line 62 of file export.h.

◆ exportSparseModelAsDot()

template<typename ValueType >

void storm::api::exportSparseModelAsDot	(	std::shared_ptr< storm::models::sparse::Model< ValueType > > const &	model,
		std::string const &	filename,
		size_t	maxWidth = `30`
	)

Definition at line 41 of file export.h.

◆ exportSparseModelAsDrn()

template<typename ValueType >

void storm::api::exportSparseModelAsDrn	(	std::shared_ptr< storm::models::sparse::Model< ValueType > > const &	model,
		std::string const &	filename,
		std::vector< std::string > const &	parameterNames = `{}`,
		bool	allowPlaceholders = `true`
	)

Definition at line 25 of file export.h.

◆ exportSparseModelAsJson()

template<typename ValueType >

void storm::api::exportSparseModelAsJson	(	std::shared_ptr< storm::models::sparse::Model< ValueType > > const &	model,
		std::string const &	filename
	)

Definition at line 49 of file export.h.

◆ exportSymbolicModelAsDot()

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

void storm::api::exportSymbolicModelAsDot	(	std::shared_ptr< storm::models::symbolic::Model< Type, ValueType > > const &	model,
		std::string const &	filename
	)

Definition at line 57 of file export.h.

◆ exportSymbolicModelAsDrdd()

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

void storm::api::exportSymbolicModelAsDrdd	(	std::shared_ptr< storm::models::symbolic::Model< Type, ValueType > > const &	model,
		std::string const &	filename
	)

Definition at line 36 of file export.h.

◆ extractFormulasFromProperties()

std::vector< std::shared_ptr< storm::logic::Formula const > > storm::api::extractFormulasFromProperties ( std::vector< storm::jani::Property > const & properties )

Definition at line 64 of file properties.cpp.

◆ filterProperties() [1/2]

std::pair< storm::jani::Model, std::vector< storm::jani::Property > > storm::api::filterProperties	(	std::pair< storm::jani::Model, std::vector< storm::jani::Property > > &	modelAndFormulae,
		boost::optional< std::vector< std::string > > const &	propertyFilter
	)

Definition at line 26 of file model_descriptions.cpp.

◆ filterProperties() [2/2]

std::vector< storm::jani::Property > storm::api::filterProperties	(	std::vector< storm::jani::Property > const &	properties,
		boost::optional< std::set< std::string > > const &	propertyFilter
	)

Definition at line 33 of file properties.cpp.

◆ getSupportedJaniFeatures()

storm::jani::ModelFeatures storm::api::getSupportedJaniFeatures ( storm::builder::BuilderType const & builderType )

inline

Definition at line 31 of file builder.h.

◆ handleGSPNExportSettings()

void storm::api::handleGSPNExportSettings	(	storm::gspn::GSPN const &	gspn,
		std::function< std::vector< storm::jani::Property >(storm::builder::JaniGSPNBuilder const &)> const &	janiProperyGetter
	)

Definition at line 20 of file storm-gspn.cpp.

◆ initializeParameterLiftingRegionModelChecker()

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

Definition at line 131 of file region.h.

◆ initializeRegionModelChecker() [1/2]

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

Definition at line 218 of file region.h.

◆ initializeRegionModelChecker() [2/2]

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
	)

Definition at line 246 of file region.h.

◆ initializeValidatingRegionModelChecker()

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

Definition at line 183 of file region.h.

◆ makeExplicitModelBuilder()

template<typename ValueType >

storm::builder::ExplicitModelBuilder< ValueType > storm::api::makeExplicitModelBuilder	(	storm::storage::SymbolicModelDescription const &	model,
		storm::builder::BuilderOptions const &	options,
		std::shared_ptr< storm::generator::ActionMask< ValueType > >	actionMask = `nullptr`
	)

Initializes an explict model builder; an object/algorithm that is used to build sparse models.

Template Parameters

ValueType Type of the probabilities in the sparse model

Parameters

model	SymbolicModelDescription of the model
options	Builder options
actionMask	An object to restrict which actions are expanded in the builder

Returns: A builder

Definition at line 89 of file builder.h.

◆ parseCapacitiesList()

std::unordered_map< std::string, uint64_t > storm::api::parseCapacitiesList	(	std::string const &	filename,
		storm::gspn::GSPN const &	gspn
	)

Definition at line 84 of file storm-gspn.cpp.

◆ parseJaniModel() [1/2]

std::pair< storm::jani::Model, std::vector< storm::jani::Property > > storm::api::parseJaniModel	(	std::string const &	filename,
		boost::optional< std::vector< std::string > > const &	propertyFilter
	)

Definition at line 49 of file model_descriptions.cpp.

◆ parseJaniModel() [2/2]

std::pair< storm::jani::Model, std::vector< storm::jani::Property > > storm::api::parseJaniModel	(	std::string const &	filename,
		storm::jani::ModelFeatures const &	supportedFeatures,
		boost::optional< std::vector< std::string > > const &	propertyFilter
	)

Definition at line 67 of file model_descriptions.cpp.

◆ parseJaniModelFromString() [1/2]

std::pair< storm::jani::Model, std::vector< storm::jani::Property > > storm::api::parseJaniModelFromString	(	std::string const &	jsonstring,
		boost::optional< std::vector< std::string > > const &	propertyFilter
	)

Definition at line 58 of file model_descriptions.cpp.

◆ parseJaniModelFromString() [2/2]

std::pair< storm::jani::Model, std::vector< storm::jani::Property > > storm::api::parseJaniModelFromString	(	std::string const &	jsonstring,
		storm::jani::ModelFeatures const &	supportedFeatures,
		boost::optional< std::vector< std::string > > const &	propertyFilter
	)

Definition at line 75 of file model_descriptions.cpp.

◆ parseMonotoneParameters()

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
	)

Definition at line 121 of file region.h.

◆ parseProgram()

storm::prism::Program storm::api::parseProgram	(	std::string const &	filename,
		bool	prismCompatibility,
		bool	simplify
	)

Definition at line 17 of file model_descriptions.cpp.

◆ parseProperties() [1/2]

std::vector< storm::jani::Property > storm::api::parseProperties	(	std::string const &	inputString,
		boost::optional< std::set< std::string > > const &	propertyFilter
	)

Definition at line 47 of file properties.cpp.

◆ parseProperties() [2/2]

std::vector< storm::jani::Property > storm::api::parseProperties	(	storm::parser::FormulaParser &	formulaParser,
		std::string const &	inputString,
		boost::optional< std::set< std::string > > const &	propertyFilter
	)

Definition at line 27 of file properties.cpp.

◆ parsePropertiesForJaniModel()

std::vector< storm::jani::Property > storm::api::parsePropertiesForJaniModel	(	std::string const &	inputString,
		storm::jani::Model const &	model,
		boost::optional< std::set< std::string > > const &	propertyFilter
	)

Definition at line 59 of file properties.cpp.

◆ parsePropertiesForPrismProgram()

std::vector< storm::jani::Property > storm::api::parsePropertiesForPrismProgram	(	std::string const &	inputString,
		storm::prism::Program const &	program,
		boost::optional< std::set< std::string > > const &	propertyFilter
	)

Definition at line 69 of file properties.cpp.

◆ parsePropertiesForSymbolicModelDescription()

std::vector< storm::jani::Property > storm::api::parsePropertiesForSymbolicModelDescription	(	std::string const &	inputString,
		storm::storage::SymbolicModelDescription const &	modelDescription,
		boost::optional< std::set< std::string > > const &	propertyFilter
	)

Definition at line 76 of file properties.cpp.

◆ parsePropertyFilter()

boost::optional< std::set< std::string > > storm::api::parsePropertyFilter ( std::string const & propertyFilter )

Definition at line 18 of file properties.cpp.

◆ parseRegion() [1/2]

template<typename ValueType >

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

Definition at line 94 of file region.h.

◆ parseRegion() [2/2]

template<typename ValueType >

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

Definition at line 107 of file region.h.

◆ parseRegions() [1/2]

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
	)

Definition at line 48 of file region.h.

◆ parseRegions() [2/2]

template<typename ValueType >

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

Definition at line 66 of file region.h.

◆ performBisimulationMinimization() [1/3]

template<typename ValueType >

std::shared_ptr< storm::models::sparse::Model< ValueType > > storm::api::performBisimulationMinimization	(	std::shared_ptr< storm::models::sparse::Model< ValueType > > const &	model,
		std::vector< std::shared_ptr< storm::logic::Formula const > > const &	formulas,
		storm::storage::BisimulationType	type = `storm::storage::BisimulationType::Strong`,
		bool	graphPreserving = `true`
	)

Definition at line 64 of file bisimulation.h.

◆ performBisimulationMinimization() [2/3]

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

std::enable_if< DdType!=storm::dd::DdType::Sylvan &&!std::is_same< ValueType, double >::value, std::shared_ptr< storm::models::Model< ExportValueType > > >::type storm::api::performBisimulationMinimization	(	std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &	,
		std::vector< std::shared_ptr< storm::logic::Formula const > > const &	,
		storm::storage::BisimulationType const &	= `storm::storage::BisimulationType::Strong`,
		storm::dd::bisimulation::SignatureMode const &	= `storm::dd::bisimulation::SignatureMode::Eager`,
		storm::dd::bisimulation::QuotientFormat const &	= `storm::dd::bisimulation::QuotientFormat::Dd`
	)

Definition at line 115 of file bisimulation.h.

◆ performBisimulationMinimization() [3/3]

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

std::enable_if< DdType==storm::dd::DdType::Sylvan\|\|std::is_same< ValueType, double >::value, std::shared_ptr< storm::models::Model< ExportValueType > > >::type storm::api::performBisimulationMinimization	(	std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &	model,
		std::vector< std::shared_ptr< storm::logic::Formula const > > const &	formulas,
		storm::storage::BisimulationType const &	bisimulationType = `storm::storage::BisimulationType::Strong`,
		storm::dd::bisimulation::SignatureMode const &	mode = `storm::dd::bisimulation::SignatureMode::Eager`,
		storm::dd::bisimulation::QuotientFormat const &	quotientFormat = `storm::dd::bisimulation::QuotientFormat::Dd`
	)

Definition at line 89 of file bisimulation.h.

◆ performDeterministicSparseBisimulationMinimization()

template<typename ModelType >

std::shared_ptr< ModelType > storm::api::performDeterministicSparseBisimulationMinimization	(	std::shared_ptr< ModelType >	model,
		std::vector< std::shared_ptr< storm::logic::Formula const > > const &	formulas,
		storm::storage::BisimulationType	type,
		bool	graphPreserving = `true`
	)

Definition at line 20 of file bisimulation.h.

◆ performNondeterministicSparseBisimulationMinimization()

template<typename ModelType >

std::shared_ptr< ModelType > storm::api::performNondeterministicSparseBisimulationMinimization	(	std::shared_ptr< ModelType >	model,
		std::vector< std::shared_ptr< storm::logic::Formula const > > const &	formulas,
		storm::storage::BisimulationType	type,
		bool	graphPreserving = `true`
	)

Definition at line 42 of file bisimulation.h.

◆ permuteModelStates()

template<typename ValueType >

std::shared_ptr< storm::models::sparse::Model< ValueType > > storm::api::permuteModelStates	(	std::shared_ptr< storm::models::sparse::Model< ValueType > > const &	model,
		storm::utility::permutation::OrderKind	order,
		std::optional< uint64_t >	seed = `std::nullopt`
	)

Permutes the order of the states of the model according to the given order.

The order of the available choices at a state (of a nondeterministic model) is not changed. A seed can be given which will be respected if a random permutation is requested.

Definition at line 157 of file transformation.h.

◆ printJaniToStream()

void storm::api::printJaniToStream	(	storm::jani::Model const &	model,
		std::vector< storm::jani::Property > const &	properties,
		std::ostream &	ostream,
		bool	compact
	)

Definition at line 139 of file storm-conv.cpp.

◆ printPrismToStream()

void storm::api::printPrismToStream	(	storm::prism::Program const &	program,
		std::vector< storm::jani::Property > const &	properties,
		std::ostream &	ostream
	)

Definition at line 158 of file storm-conv.cpp.

◆ simplifyJaniModel()

void storm::api::simplifyJaniModel	(	storm::jani::Model &	model,
		std::vector< storm::jani::Property > &	properties,
		storm::jani::ModelFeatures const &	supportedFeatures
	)

Definition at line 83 of file model_descriptions.cpp.

◆ substituteConstantsInProperties()

std::vector< storm::jani::Property > storm::api::substituteConstantsInProperties	(	std::vector< storm::jani::Property > const &	properties,
		std::map< storm::expressions::Variable, storm::expressions::Expression > const &	substitution
	)

Definition at line 16 of file properties.cpp.

◆ substituteTranscendentalNumbersInProperties()

std::vector< storm::jani::Property > storm::api::substituteTranscendentalNumbersInProperties ( std::vector< storm::jani::Property > const & properties )

Definition at line 25 of file properties.cpp.

◆ transformContinuousToDiscreteTimeSparseModel() [1/2]

template<typename ValueType >

std::pair< std::shared_ptr< storm::models::sparse::Model< ValueType > >, std::vector< std::shared_ptr< storm::logic::Formula const > > > storm::api::transformContinuousToDiscreteTimeSparseModel	(	std::shared_ptr< storm::models::sparse::Model< ValueType > > const &	model,
		std::vector< std::shared_ptr< storm::logic::Formula const > > const &	formulas
	)

Transforms the given continuous model to a discrete time model.

If such a transformation does not preserve one of the given formulas, a warning is issued.

Definition at line 37 of file transformation.h.

◆ transformContinuousToDiscreteTimeSparseModel() [2/2]

template<typename ValueType >

std::pair< std::shared_ptr< storm::models::sparse::Model< ValueType > >, std::vector< std::shared_ptr< storm::logic::Formula const > > > storm::api::transformContinuousToDiscreteTimeSparseModel	(	storm::models::sparse::Model< ValueType > &&	model,
		std::vector< std::shared_ptr< storm::logic::Formula const > > const &	formulas
	)

Transforms the given continuous model to a discrete time model IN PLACE.

This means that the input continuous time model is replaced by the new discrete time model. If such a transformation does not preserve one of the given formulas, an error is issued.

Definition at line 68 of file transformation.h.

◆ transformJani()

void storm::api::transformJani	(	storm::jani::Model &	janiModel,
		std::vector< storm::jani::Property > &	properties,
		storm::converter::JaniConversionOptions const &	options
	)

Definition at line 19 of file storm-conv.cpp.

◆ transformPrism()

void storm::api::transformPrism	(	storm::prism::Program &	prismProgram,
		std::vector< storm::jani::Property > &	properties,
		bool	simplify,
		bool	flatten
	)

Definition at line 97 of file storm-conv.cpp.

◆ transformSymbolicToSparseModel()

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

std::shared_ptr< storm::models::sparse::Model< ValueType > > storm::api::transformSymbolicToSparseModel	(	std::shared_ptr< storm::models::symbolic::Model< Type, ValueType > > const &	symbolicModel,
		std::vector< std::shared_ptr< storm::logic::Formula const > > const &	formulas = `std::vector<std::shared_ptr<storm::logic::Formula const>>()`
	)

Transforms the given symbolic model to a sparse model.

Definition at line 109 of file transformation.h.

◆ transformToNondeterministicModel()

template<typename ValueType >

std::shared_ptr< storm::models::sparse::Model< ValueType > > storm::api::transformToNondeterministicModel ( storm::models::sparse::Model< ValueType > && model )

Definition at line 133 of file transformation.h.

◆ verifyRegion()

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 &	region,
		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.

Definition at line 326 of file region.h.

◆ verifyWithDdEngine() [1/7]

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

std::unique_ptr< storm::modelchecker::CheckResult > storm::api::verifyWithDdEngine	(	std::shared_ptr< storm::models::symbolic::Dtmc< DdType, ValueType > > const &	dtmc,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task
	)

Definition at line 465 of file verification.h.

◆ verifyWithDdEngine() [2/7]

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

std::unique_ptr< storm::modelchecker::CheckResult > storm::api::verifyWithDdEngine	(	std::shared_ptr< storm::models::symbolic::Mdp< DdType, ValueType > > const &	mdp,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task
	)

Definition at line 493 of file verification.h.

◆ verifyWithDdEngine() [3/7]

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

std::unique_ptr< storm::modelchecker::CheckResult > storm::api::verifyWithDdEngine	(	std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &	model,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task
	)

Definition at line 515 of file verification.h.

◆ verifyWithDdEngine() [4/7]

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

std::enable_if< std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type storm::api::verifyWithDdEngine	(	storm::Environment const &	,
		std::shared_ptr< storm::models::symbolic::Mdp< DdType, ValueType > > const &	,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &
	)

Definition at line 486 of file verification.h.

◆ verifyWithDdEngine() [5/7]

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

std::unique_ptr< storm::modelchecker::CheckResult > storm::api::verifyWithDdEngine	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::symbolic::Dtmc< DdType, ValueType > > const &	dtmc,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task
	)

Definition at line 451 of file verification.h.

◆ verifyWithDdEngine() [6/7]

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

std::enable_if<!std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type storm::api::verifyWithDdEngine	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::symbolic::Mdp< DdType, ValueType > > const &	mdp,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task
	)

Definition at line 472 of file verification.h.

◆ verifyWithDdEngine() [7/7]

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

std::unique_ptr< storm::modelchecker::CheckResult > storm::api::verifyWithDdEngine	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &	model,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task
	)

Definition at line 500 of file verification.h.

◆ verifyWithExplorationEngine() [1/3]

template<typename ValueType >

std::enable_if<!std::is_same< ValueType, double >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type storm::api::verifyWithExplorationEngine	(	storm::Environment const &	,
		storm::storage::SymbolicModelDescription const &	,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &
	)

Definition at line 79 of file verification.h.

◆ verifyWithExplorationEngine() [2/3]

template<typename ValueType >

std::enable_if< std::is_same< ValueType, double >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type storm::api::verifyWithExplorationEngine	(	storm::Environment const &	env,
		storm::storage::SymbolicModelDescription const &	model,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task
	)

Definition at line 53 of file verification.h.

◆ verifyWithExplorationEngine() [3/3]

template<typename ValueType >

std::unique_ptr< storm::modelchecker::CheckResult > storm::api::verifyWithExplorationEngine	(	storm::storage::SymbolicModelDescription const &	model,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task
	)

Definition at line 85 of file verification.h.

◆ verifyWithHybridEngine() [1/12]

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

std::unique_ptr< storm::modelchecker::CheckResult > storm::api::verifyWithHybridEngine	(	std::shared_ptr< storm::models::symbolic::Ctmc< DdType, ValueType > > const &	ctmc,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task
	)

Definition at line 359 of file verification.h.

◆ verifyWithHybridEngine() [2/12]

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

std::unique_ptr< storm::modelchecker::CheckResult > storm::api::verifyWithHybridEngine	(	std::shared_ptr< storm::models::symbolic::Dtmc< DdType, ValueType > > const &	dtmc,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task
	)

Definition at line 338 of file verification.h.

◆ verifyWithHybridEngine() [3/12]

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

std::unique_ptr< storm::modelchecker::CheckResult > storm::api::verifyWithHybridEngine	(	std::shared_ptr< storm::models::symbolic::MarkovAutomaton< DdType, ValueType > > const &	ma,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task
	)

Definition at line 415 of file verification.h.

◆ verifyWithHybridEngine() [4/12]

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

std::unique_ptr< storm::modelchecker::CheckResult > storm::api::verifyWithHybridEngine	(	std::shared_ptr< storm::models::symbolic::Mdp< DdType, ValueType > > const &	mdp,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task
	)

Definition at line 387 of file verification.h.

◆ verifyWithHybridEngine() [5/12]

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

std::unique_ptr< storm::modelchecker::CheckResult > storm::api::verifyWithHybridEngine	(	std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &	model,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task
	)

Definition at line 441 of file verification.h.

◆ verifyWithHybridEngine() [6/12]

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

std::enable_if< std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type storm::api::verifyWithHybridEngine	(	storm::Environment const &	,
		std::shared_ptr< storm::models::symbolic::MarkovAutomaton< DdType, ValueType > > const &	,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &
	)

Definition at line 409 of file verification.h.

◆ verifyWithHybridEngine() [7/12]

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

std::enable_if< std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type storm::api::verifyWithHybridEngine	(	storm::Environment const &	,
		std::shared_ptr< storm::models::symbolic::Mdp< DdType, ValueType > > const &	,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &
	)

Definition at line 381 of file verification.h.

◆ verifyWithHybridEngine() [8/12]

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

std::unique_ptr< storm::modelchecker::CheckResult > storm::api::verifyWithHybridEngine	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::symbolic::Ctmc< DdType, ValueType > > const &	ctmc,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task
	)

Definition at line 345 of file verification.h.

◆ verifyWithHybridEngine() [9/12]

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

std::unique_ptr< storm::modelchecker::CheckResult > storm::api::verifyWithHybridEngine	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::symbolic::Dtmc< DdType, ValueType > > const &	dtmc,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task
	)

Definition at line 324 of file verification.h.

◆ verifyWithHybridEngine() [10/12]

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

std::enable_if<!std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type storm::api::verifyWithHybridEngine	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::symbolic::MarkovAutomaton< DdType, ValueType > > const &	ma,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task
	)

Definition at line 395 of file verification.h.

◆ verifyWithHybridEngine() [11/12]

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

std::enable_if<!std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type storm::api::verifyWithHybridEngine	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::symbolic::Mdp< DdType, ValueType > > const &	mdp,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task
	)

Definition at line 367 of file verification.h.

◆ verifyWithHybridEngine() [12/12]

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

std::unique_ptr< storm::modelchecker::CheckResult > storm::api::verifyWithHybridEngine	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::symbolic::Model< DdType, ValueType > > const &	model,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task
	)

Definition at line 422 of file verification.h.

◆ verifyWithSparseEngine() [1/15]

template<typename ValueType >

std::unique_ptr< storm::modelchecker::CheckResult > storm::api::verifyWithSparseEngine	(	std::shared_ptr< storm::models::sparse::Ctmc< ValueType > > const &	ctmc,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task
	)

Definition at line 134 of file verification.h.

◆ verifyWithSparseEngine() [2/15]

template<typename ValueType >

std::unique_ptr< storm::modelchecker::CheckResult > storm::api::verifyWithSparseEngine	(	std::shared_ptr< storm::models::sparse::Dtmc< ValueType > > const &	dtmc,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task
	)

Definition at line 115 of file verification.h.

◆ verifyWithSparseEngine() [3/15]

template<typename ValueType >

std::unique_ptr< storm::modelchecker::CheckResult > storm::api::verifyWithSparseEngine	(	std::shared_ptr< storm::models::sparse::MarkovAutomaton< ValueType > > const &	ma,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task
	)

Definition at line 198 of file verification.h.

◆ verifyWithSparseEngine() [4/15]

template<typename ValueType >

std::unique_ptr< storm::modelchecker::CheckResult > storm::api::verifyWithSparseEngine	(	std::shared_ptr< storm::models::sparse::Mdp< ValueType > > const &	mdp,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task
	)

Definition at line 165 of file verification.h.

◆ verifyWithSparseEngine() [5/15]

template<typename ValueType >

std::unique_ptr< storm::modelchecker::CheckResult > storm::api::verifyWithSparseEngine	(	std::shared_ptr< storm::models::sparse::Model< ValueType > > const &	model,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task
	)

Definition at line 252 of file verification.h.

◆ verifyWithSparseEngine() [6/15]

template<typename ValueType >

std::unique_ptr< storm::modelchecker::CheckResult > storm::api::verifyWithSparseEngine	(	std::shared_ptr< storm::models::sparse::Smg< ValueType > > const &	smg,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task
	)

Definition at line 224 of file verification.h.

◆ verifyWithSparseEngine() [7/15]

template<typename ValueType >

std::enable_if< std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type storm::api::verifyWithSparseEngine	(	storm::Environment const &	,
		std::shared_ptr< storm::models::sparse::MarkovAutomaton< ValueType > > const &	,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &
	)

Definition at line 192 of file verification.h.

◆ verifyWithSparseEngine() [8/15]

template<typename ValueType >

std::enable_if< std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type storm::api::verifyWithSparseEngine	(	storm::Environment const &	,
		std::shared_ptr< storm::models::sparse::Smg< ValueType > > const &	,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &
	)

Definition at line 218 of file verification.h.

◆ verifyWithSparseEngine() [9/15]

template<typename ValueType >

std::unique_ptr< storm::modelchecker::CheckResult > storm::api::verifyWithSparseEngine	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::sparse::Ctmc< ValueType > > const &	ctmc,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task
	)

Definition at line 122 of file verification.h.

◆ verifyWithSparseEngine() [10/15]

template<typename ValueType >

std::unique_ptr< storm::modelchecker::CheckResult > storm::api::verifyWithSparseEngine	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::sparse::Dtmc< ValueType > > const &	dtmc,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task
	)

Definition at line 95 of file verification.h.

◆ verifyWithSparseEngine() [11/15]

template<typename ValueType >

std::enable_if<!std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type storm::api::verifyWithSparseEngine	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::sparse::MarkovAutomaton< ValueType > > const &	ma,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task
	)

Definition at line 173 of file verification.h.

◆ verifyWithSparseEngine() [12/15]

template<typename ValueType >

std::enable_if<!std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type storm::api::verifyWithSparseEngine	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::sparse::Mdp< ValueType > > const &	mdp,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task
	)

Definition at line 142 of file verification.h.

◆ verifyWithSparseEngine() [13/15]

template<typename ValueType >

std::enable_if< std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type storm::api::verifyWithSparseEngine	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::sparse::Mdp< ValueType > > const &	mdp,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task
	)

Definition at line 154 of file verification.h.

◆ verifyWithSparseEngine() [14/15]

template<typename ValueType >

std::unique_ptr< storm::modelchecker::CheckResult > storm::api::verifyWithSparseEngine	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::sparse::Model< ValueType > > const &	model,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task
	)

Definition at line 231 of file verification.h.

◆ verifyWithSparseEngine() [15/15]

template<typename ValueType >

std::enable_if<!std::is_same< ValueType, storm::RationalFunction >::value, std::unique_ptr< storm::modelchecker::CheckResult > >::type storm::api::verifyWithSparseEngine	(	storm::Environment const &	env,
		std::shared_ptr< storm::models::sparse::Smg< ValueType > > const &	smg,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task
	)

Definition at line 206 of file verification.h.

Classes

Functions

Function Documentation

◆ buildExplicitDRNModel()

◆ buildExplicitIMCAModel()

◆ buildExplicitModel()

◆ buildJani()

◆ buildSparseModel() [1/3]

◆ buildSparseModel() [2/3]

◆ buildSparseModel() [3/3]

◆ buildSymbolicModel() [1/3]

◆ buildSymbolicModel() [2/3]

◆ buildSymbolicModel() [3/3]

◆ checkAndRefineRegionWithSparseEngine()

◆ checkAndTransformContinuousToDiscreteTimeFormula()

◆ checkRegionsWithSparseEngine() [1/2]

◆ checkRegionsWithSparseEngine() [2/2]

◆ computeExpectedVisitingTimesWithSparseEngine() [1/3]

◆ computeExpectedVisitingTimesWithSparseEngine() [2/3]

◆ computeExpectedVisitingTimesWithSparseEngine() [3/3]

◆ computeExtremalValue()

◆ computeHighLevelCounterexampleMaxSmt()

◆ computeHighLevelCounterexampleMilp()

◆ computeKShortestPathCounterexample()

◆ computeSteadyStateDistributionWithSparseEngine() [1/3]

◆ computeSteadyStateDistributionWithSparseEngine() [2/3]

◆ computeSteadyStateDistributionWithSparseEngine() [3/3]

◆ convertPrismToJani() [1/2]

◆ convertPrismToJani() [2/2]

◆ createMultiObjectiveProperty()

◆ createRegion() [1/2]

◆ createRegion() [2/2]

◆ createTask()

◆ eliminateNonMarkovianChains()

◆ exportCheckResultToJson()

◆ exportCheckResultToJson< storm::RationalFunction >()

◆ exportJaniModelAsDot()

◆ exportJaniToFile()

◆ exportParametricResultToFile() [1/2]

◆ exportParametricResultToFile() [2/2]

◆ exportPrismToFile()

◆ exportRegionCheckResultToFile()

◆ exportScheduler()

◆ exportSparseModelAsDot()

◆ exportSparseModelAsDrn()

◆ exportSparseModelAsJson()

◆ exportSymbolicModelAsDot()

◆ exportSymbolicModelAsDrdd()

◆ extractFormulasFromProperties()

◆ filterProperties() [1/2]

◆ filterProperties() [2/2]

◆ getSupportedJaniFeatures()

◆ handleGSPNExportSettings()

◆ initializeParameterLiftingRegionModelChecker()

◆ initializeRegionModelChecker() [1/2]

◆ initializeRegionModelChecker() [2/2]

◆ initializeValidatingRegionModelChecker()

◆ makeExplicitModelBuilder()

◆ parseCapacitiesList()

◆ parseJaniModel() [1/2]

◆ parseJaniModel() [2/2]

◆ parseJaniModelFromString() [1/2]

◆ parseJaniModelFromString() [2/2]

◆ parseMonotoneParameters()

◆ parseProgram()

◆ parseProperties() [1/2]

◆ parseProperties() [2/2]

◆ parsePropertiesForJaniModel()

◆ parsePropertiesForPrismProgram()

◆ parsePropertiesForSymbolicModelDescription()

◆ parsePropertyFilter()

◆ parseRegion() [1/2]

◆ parseRegion() [2/2]

◆ parseRegions() [1/2]

◆ parseRegions() [2/2]

◆ performBisimulationMinimization() [1/3]

◆ performBisimulationMinimization() [2/3]

◆ performBisimulationMinimization() [3/3]

◆ performDeterministicSparseBisimulationMinimization()

◆ performNondeterministicSparseBisimulationMinimization()