storm::api Namespace Reference

Classes
struct	GspnJaniExportOptions
	Options for exporting a GSPN as a JANI model. More...

Typedefs
using	MonotonicitySetting = storm::pars::modelchecker::MonotonicityOptions
template<typename ValueType>
using	RefinementOptions = storm::pars::modelchecker::RegionRefinementOptions<ValueType>

Functions
void	transformJani (storm::jani::Model &janiModel, std::vector< storm::jani::Property > &properties, storm::converter::JaniConversionOptions const &options, std::shared_ptr< storm::utility::solver::SmtSolverFactory > smtSolverFactory)
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::Environment const &env, storm::storage::SymbolicModelDescription const &symbolicModel, std::shared_ptr< storm::models::sparse::Mdp< double > > mdp, std::shared_ptr< storm::logic::Formula const > const &formula, bool includeSchedulerCuts)
std::shared_ptr< storm::counterexamples::Counterexample >	computeHighLevelCounterexampleMaxSmt (storm::Environment const &env, storm::storage::SymbolicModelDescription const &symbolicModel, std::shared_ptr< storm::models::sparse::Model< double > > model, std::shared_ptr< storm::logic::Formula const > const &formula, storm::counterexamples::SMTMinimalLabelSetGenerator< double >::Options const &options)
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	exportGspnToDot (storm::gspn::GSPN const &gspn, std::string const &filename)
void	exportGspnToPnpro (storm::gspn::GSPN const &gspn, std::string const &filename)
void	exportGspnToPnml (storm::gspn::GSPN const &gspn, std::string const &filename)
void	exportGspnToJson (storm::gspn::GSPN const &gspn, std::string const &filename)
void	printGspnStatsToStream (storm::gspn::GSPN const &gspn, std::ostream &out)
void	exportGspnStatsToFile (storm::gspn::GSPN const &gspn, std::string const &filename)
void	exportGspnToJani (storm::gspn::GSPN const &gspn, std::string const &filename, GspnJaniExportOptions const &options, std::function< std::vector< storm::jani::Property >(storm::builder::JaniGSPNBuilder const &)> const &janiPropertyGetter)
std::unordered_map< std::string, uint64_t >	parseCapacitiesList (std::string const &filename, storm::gspn::GSPN const &gspn)
template<typename ParametricType, typename ImpreciseType, typename PreciseType>
std::unique_ptr< storm::modelchecker::RegionModelChecker< ParametricType > >	createRegionModelChecker (storm::modelchecker::RegionCheckEngine engine, storm::models::ModelType modelType)
template std::unique_ptr< storm::modelchecker::RegionModelChecker< storm::RationalFunction > >	createRegionModelChecker< storm::RationalFunction, double, storm::RationalNumber > (storm::modelchecker::RegionCheckEngine engine, storm::models::ModelType modelType)
template<typename ValueType>
std::set< typename storm::storage::ParameterRegion< ValueType >::VariableType >	getModelParameters (storm::models::ModelBase const &model)
template<typename ValueType>
std::vector< typename storm::storage::ParameterRegion< ValueType >::VariableType >	parseVariableList (std::string const &inputString, std::set< typename storm::storage::ParameterRegion< ValueType >::VariableType > const &consideredVariables)
template<typename ValueType>
std::vector< typename storm::storage::ParameterRegion< ValueType >::VariableType >	parseVariableList (std::string const &inputString, storm::models::ModelBase const &model)
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>
std::vector< storm::storage::ParameterRegion< ValueType > >	parseRegions (std::string const &inputString, storm::models::ModelBase const &model)
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 > >	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>
std::shared_ptr< storm::models::sparse::Model< ParametricType > >	preprocessSparseModelForParameterLifting (std::shared_ptr< storm::models::sparse::Model< ParametricType > > const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ParametricType > const &task, storm::modelchecker::RegionCheckEngine engine, bool preconditionsValidatedManually=false)
template<typename ParametricType, typename ImpreciseType = double, typename PreciseType = storm::RationalNumber>
std::unique_ptr< storm::modelchecker::MonotonicityBackend< ParametricType > >	initializeMonotonicityBackend (storm::modelchecker::RegionModelChecker< ParametricType > const &regionChecker, storm::modelchecker::RegionCheckEngine engine, storm::modelchecker::CheckTask< storm::logic::Formula, ParametricType > const &task, MonotonicitySetting const &monotonicitySetting, std::optional< std::pair< std::set< typename storm::storage::ParameterRegion< ParametricType >::VariableType >, std::set< typename storm::storage::ParameterRegion< ParametricType >::VariableType > > > monotoneParameters=std::nullopt)
template<typename ValueType, typename ImpreciseType = double, typename PreciseType = storm::RationalNumber>
std::unique_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 allowModelSimplification=true, storm::pars::analysis::GraphPreservationStatus graphPreservationStatus=storm::pars::analysis::GraphPreservationStatus::GraphPreserving, bool preconditionsValidated=false, MonotonicitySetting monotonicitySetting=MonotonicitySetting(), std::optional< std::pair< std::set< typename storm::storage::ParameterRegion< ValueType >::VariableType >, std::set< typename storm::storage::ParameterRegion< ValueType >::VariableType > > > monotoneParameters=std::nullopt)
template<typename ValueType>
std::unique_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 (Environment const &env, 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 (Environment const &env, 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, typename ImpreciseType = double, typename PreciseType = storm::RationalNumber>
std::unique_ptr< storm::modelchecker::RegionRefinementChecker< ValueType > >	initializeRegionRefinementChecker (Environment const &env, RefinementOptions< ValueType > settings)
template<typename ValueType>
std::unique_ptr< storm::modelchecker::RegionRefinementCheckResult< ValueType > >	checkAndRefineRegionWithSparseEngine (Environment const &env, RefinementOptions< ValueType > settings, storm::storage::ParameterRegion< ValueType > const &region, std::optional< ValueType > const &coverageThreshold, std::optional< uint64_t > const &refinementDepthThreshold=std::nullopt, storm::modelchecker::RegionResultHypothesis hypothesis=storm::modelchecker::RegionResultHypothesis::Unknown, uint64_t monThresh=0)
	Checks and iteratively refines the given region with the sparse engine.
template<typename ValueType>
std::pair< storm::ExtendedRationalNumber, typename storm::storage::ParameterRegion< ValueType >::Valuation >	computeExtremalValue (Environment const &env, RefinementOptions< ValueType > settings, storm::storage::ParameterRegion< ValueType > const &region, storm::solver::OptimizationDirection const &dir, std::optional< ValueType > const &precision, bool absolutePrecision, std::optional< storm::logic::Bound > const &boundInvariant)
	Finds the extremal value in the given region.
template<typename ValueType>
bool	verifyRegion (Environment const &env, RefinementOptions< ValueType > settings, storm::storage::ParameterRegion< ValueType > const &region)
	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, storm::parser::ExplicitModelParserOptions const &options=storm::parser::ExplicitModelParserOptions())
template<typename ValueType>
std::shared_ptr< storm::models::sparse::Model< ValueType > >	buildExplicitDRNModel (std::string const &drnFile, storm::parser::DirectEncodingParserOptions const &options=storm::parser::DirectEncodingParserOptions())
std::shared_ptr< storm::models::ModelBase >	buildExplicitDRNModel (std::string const &drnFile, storm::parser::DirectEncodingValueType valueType=storm::parser::DirectEncodingValueType::Default, storm::parser::DirectEncodingParserOptions const &options=storm::parser::DirectEncodingParserOptions())
std::shared_ptr< storm::models::ModelBase >	buildExplicitUmbModel (std::string const &umbLocation, storm::umb::ImportOptions const &options={})
template<typename ValueType>
std::shared_ptr< storm::models::sparse::Model< ValueType > >	buildExplicitIMCAModel (std::string const &imcaFile, storm::parser::ExplicitModelParserOptions const &options=storm::parser::ExplicitModelParserOptions())
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 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::bisimulation::Options const &options={})
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::bisimulation::BisimulationType const &bisimulationType=storm::bisimulation::BisimulationType::Strong, storm::dd::bisimulation::SignatureMode const &mode=storm::dd::bisimulation::SignatureMode::Eager, storm::dd::bisimulation::QuotientFormat const &quotientFormat=storm::dd::bisimulation::QuotientFormat::Dd, storm::dd::bisimulation::BisimulationOptions const &bisimulationOptions=storm::dd::bisimulation::BisimulationOptions())
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::bisimulation::BisimulationType const &=storm::bisimulation::BisimulationType::Strong, storm::dd::bisimulation::SignatureMode const &=storm::dd::bisimulation::SignatureMode::Eager, storm::dd::bisimulation::QuotientFormat const &=storm::dd::bisimulation::QuotientFormat::Dd, storm::dd::bisimulation::BisimulationOptions const &=storm::dd::bisimulation::BisimulationOptions())
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::Environment const &env, storm::storage::SymbolicModelDescription const &model, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas, bool buildFullModel=false, bool applyMaximumProgress=true, bool fixDeadlocks=true)
template<>
std::shared_ptr< storm::models::symbolic::Model< storm::dd::DdType::CUDD, storm::RationalNumber > >	buildSymbolicModel (storm::Environment const &, storm::storage::SymbolicModelDescription const &, std::vector< std::shared_ptr< storm::logic::Formula const > > const &, bool, bool, bool)
template<>
std::shared_ptr< storm::models::symbolic::Model< storm::dd::DdType::CUDD, storm::RationalFunction > >	buildSymbolicModel (storm::Environment const &, storm::storage::SymbolicModelDescription const &, std::vector< std::shared_ptr< storm::logic::Formula const > > const &, bool, 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, typename storm::builder::ExplicitModelBuilder< ValueType >::Options const &explorationOptions=typename storm::builder::ExplicitModelBuilder< ValueType >::Options())
	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, typename storm::builder::ExplicitModelBuilder< ValueType >::Options const &explorationOptions=typename storm::builder::ExplicitModelBuilder< ValueType >::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<typename ValueType>
void	exportSparseModelAsDrn (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, std::string const &filename, storm::io::DirectEncodingExporterOptions options, std::vector< std::string > const &parameterNames={})
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<typename ValueType>
void	exportSparseModelAsUmb (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, std::string const &filename, storm::umb::ExportOptions const &options={})
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, typename PointType>
void	exportParetoScheduler (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, std::vector< PointType > const &points, std::vector< storm::storage::Scheduler< ValueType > > const &schedulers, std::string const &baseFilenameStr)
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, bool lexicographic)
template<typename ValueType>
std::shared_ptr< storm::models::sparse::Model< ValueType > >	mergeEquivalentStatesForFormula (std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model, storm::logic::Formula const &formula)
	Identifies states of the given model that are equivalent w.r.t.
template std::shared_ptr< storm::models::sparse::Model< double > >	mergeEquivalentStatesForFormula (std::shared_ptr< storm::models::sparse::Model< double > > const &model, storm::logic::Formula const &formula)
template std::shared_ptr< storm::models::sparse::Model< storm::RationalNumber > >	mergeEquivalentStatesForFormula (std::shared_ptr< storm::models::sparse::Model< storm::RationalNumber > > const &model, storm::logic::Formula const &formula)
template std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > >	mergeEquivalentStatesForFormula (std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > > const &model, storm::logic::Formula const &formula)
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> requires (!storm::IsIntervalType<ValueType>)
storm::modelchecker::CheckTask< storm::logic::Formula, ValueType >	createTask (std::shared_ptr< const storm::logic::Formula > const &formula, bool onlyInitialStatesRelevant=false)
template<typename ValueType> requires (storm::IsIntervalType<ValueType>)
storm::modelchecker::CheckTask< storm::logic::Formula, ValueType >	createTask (std::shared_ptr< const storm::logic::Formula > const &formula, storm::UncertaintyResolutionMode uncertaintyResolution, bool onlyInitialStatesRelevant=false)
template<typename ValueType>
std::unique_ptr< storm::modelchecker::CheckResult >	verifyWithExplorationEngine (storm::Environment const &env, storm::storage::SymbolicModelDescription const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
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, bool preferEliminationChecker=false)
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, bool preferEliminationChecker=false)
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::unique_ptr< storm::modelchecker::CheckResult >	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::unique_ptr< storm::modelchecker::CheckResult >	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::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::unique_ptr< storm::modelchecker::CheckResult >	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::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, bool preferEliminationChecker=false)
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, bool preferEliminationChecker=false)
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::unique_ptr< storm::modelchecker::CheckResult >	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::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::unique_ptr< storm::modelchecker::CheckResult >	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::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::unique_ptr< storm::modelchecker::CheckResult >	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::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)

Typedef Documentation

MonotonicitySetting

using storm::api::MonotonicitySetting = storm::pars::modelchecker::MonotonicityOptions

Definition at line 44 of file region.h.

RefinementOptions

template<typename ValueType>

using storm::api::RefinementOptions = storm::pars::modelchecker::RegionRefinementOptions<ValueType>

Definition at line 47 of file region.h.

Function Documentation

buildExplicitDRNModel() [1/2]

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 31 of file explicit_models.h.

buildExplicitDRNModel() [2/2]

std::shared_ptr< storm::models::ModelBase > storm::api::buildExplicitDRNModel ( std::string const & drnFile, storm::parser::DirectEncodingValueType valueType = storm::parser::DirectEncodingValueType::Default, storm::parser::DirectEncodingParserOptions const & options = storm::parser::DirectEncodingParserOptions() )

inline

Definition at line 36 of file explicit_models.h.

buildExplicitIMCAModel()

template<typename ValueType>

std::shared_ptr< storm::models::sparse::Model< ValueType > > storm::api::buildExplicitIMCAModel	(	std::string const &	imcaFile,
		storm::parser::ExplicitModelParserOptions const &	options = storm::parser::ExplicitModelParserOptions() )

Definition at line 47 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, storm::parser::ExplicitModelParserOptions const & options = storm::parser::ExplicitModelParserOptions() )

inline

Definition at line 18 of file explicit_models.h.

buildExplicitUmbModel()

std::shared_ptr< storm::models::ModelBase > storm::api::buildExplicitUmbModel ( std::string const & umbLocation, storm::umb::ImportOptions const & options = {} )

inline

Definition at line 42 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 14 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 133 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 126 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,
		typename storm::builder::ExplicitModelBuilder< ValueType >::Options const &	explorationOptions = typename storm::builder::ExplicitModelBuilder<ValueType>::Options() )

Definition at line 117 of file builder.h.

buildSymbolicModel() [1/3]

template<>

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

inline

Definition at line 80 of file builder.h.

buildSymbolicModel() [2/3]

template<>

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

inline

Definition at line 73 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::Environment const &	env,
		storm::storage::SymbolicModelDescription const &	model,
		std::vector< std::shared_ptr< storm::logic::Formula const > > const &	formulas,
		bool	buildFullModel = false,
		bool	applyMaximumProgress = true,
		bool	fixDeadlocks = true )

Definition at line 37 of file builder.h.

checkAndRefineRegionWithSparseEngine()

template<typename ValueType>

std::unique_ptr< storm::modelchecker::RegionRefinementCheckResult< ValueType > > storm::api::checkAndRefineRegionWithSparseEngine	(	Environment const &	env,
		RefinementOptions< ValueType >	settings,
		storm::storage::ParameterRegion< ValueType > const &	region,
		std::optional< ValueType > const &	coverageThreshold,
		std::optional< uint64_t > const &	refinementDepthThreshold = std::nullopt,
		storm::modelchecker::RegionResultHypothesis	hypothesis = storm::modelchecker::RegionResultHypothesis::Unknown,
		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 313 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 92 of file transformation.h.

checkRegionsWithSparseEngine() [1/2]

template<typename ValueType>

std::unique_ptr< storm::modelchecker::RegionCheckResult< ValueType > > storm::api::checkRegionsWithSparseEngine	(	Environment const &	env,
		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 268 of file region.h.

checkRegionsWithSparseEngine() [2/2]

template<typename ValueType>

std::unique_ptr< storm::modelchecker::RegionCheckResult< ValueType > > storm::api::checkRegionsWithSparseEngine	(	Environment const &	env,
		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 277 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 320 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 308 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 332 of file verification.h.

computeExtremalValue()

template<typename ValueType>

std::pair< storm::ExtendedRationalNumber, typename storm::storage::ParameterRegion< ValueType >::Valuation > storm::api::computeExtremalValue	(	Environment const &	env,
		RefinementOptions< ValueType >	settings,
		storm::storage::ParameterRegion< ValueType > const &	region,
		storm::solver::OptimizationDirection const &	dir,
		std::optional< ValueType > const &	precision,
		bool	absolutePrecision,
		std::optional< storm::logic::Bound > const &	boundInvariant )

Finds the extremal value in the given region.

Parameters

settings	The refinement settings
region	The region to be analyzed
dir	The optimization direction
precision	The precision to be used
absolutePrecision	If true, the precision is interpreted as an absolute precision, otherwise as a relative precision
boundInvariant	Bound invariant that should hold

Returns

A pair consisting of the extremal value and a parameter valuation achieving this value

Definition at line 333 of file region.h.

computeHighLevelCounterexampleMaxSmt()

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

Definition at line 17 of file counterexamples.cpp.

computeHighLevelCounterexampleMilp()

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

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 281 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 269 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 293 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 112 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 107 of file storm-conv.cpp.

createMultiObjectiveProperty()

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

Definition at line 70 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 114 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 120 of file region.h.

createRegionModelChecker()

template<typename ParametricType, typename ImpreciseType, typename PreciseType>

std::unique_ptr< storm::modelchecker::RegionModelChecker< ParametricType > > storm::api::createRegionModelChecker	(	storm::modelchecker::RegionCheckEngine	engine,
		storm::models::ModelType	modelType )

Definition at line 16 of file region.cpp.

createRegionModelChecker< storm::RationalFunction, double, storm::RationalNumber >()

template std::unique_ptr< storm::modelchecker::RegionModelChecker< storm::RationalFunction > > storm::api::createRegionModelChecker< storm::RationalFunction, double, storm::RationalNumber >	(	storm::modelchecker::RegionCheckEngine	engine,
		storm::models::ModelType	modelType )

createTask() [1/2]

template<typename ValueType>
requires (!storm::IsIntervalType<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 43 of file verification.h.

createTask() [2/2]

template<typename ValueType>
requires (storm::IsIntervalType<ValueType>)

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

Definition at line 50 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 127 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 145 of file export.h.

exportGspnStatsToFile()

void storm::api::exportGspnStatsToFile	(	storm::gspn::GSPN const &	gspn,
		std::string const &	filename )

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

exportGspnToDot()

void storm::api::exportGspnToDot	(	storm::gspn::GSPN const &	gspn,
		std::string const &	filename )

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

exportGspnToJani()

void storm::api::exportGspnToJani	(	storm::gspn::GSPN const &	gspn,
		std::string const &	filename,
		GspnJaniExportOptions const &	options,
		std::function< std::vector< storm::jani::Property >(storm::builder::JaniGSPNBuilder const &)> const &	janiPropertyGetter )

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

exportGspnToJson()

void storm::api::exportGspnToJson	(	storm::gspn::GSPN const &	gspn,
		std::string const &	filename )

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

exportGspnToPnml()

void storm::api::exportGspnToPnml	(	storm::gspn::GSPN const &	gspn,
		std::string const &	filename )

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

exportGspnToPnpro()

void storm::api::exportGspnToPnpro	(	storm::gspn::GSPN const &	gspn,
		std::string const &	filename )

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

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 131 of file storm-conv.cpp.

exportParetoScheduler()

template<typename ValueType, typename PointType>

void storm::api::exportParetoScheduler	(	std::shared_ptr< storm::models::sparse::Model< ValueType > > const &	model,
		std::vector< PointType > const &	points,
		std::vector< storm::storage::Scheduler< ValueType > > const &	schedulers,
		std::string const &	baseFilenameStr )

Definition at line 94 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 139 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 362 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 80 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 49 of file export.h.

exportSparseModelAsDrn() [1/2]

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 30 of file export.h.

exportSparseModelAsDrn() [2/2]

template<typename ValueType>

void storm::api::exportSparseModelAsDrn	(	std::shared_ptr< storm::models::sparse::Model< ValueType > > const &	model,
		std::string const &	filename,
		storm::io::DirectEncodingExporterOptions	options,
		std::vector< std::string > const &	parameterNames = {} )

Definition at line 38 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 57 of file export.h.

exportSparseModelAsUmb()

template<typename ValueType>

void storm::api::exportSparseModelAsUmb	(	std::shared_ptr< storm::models::sparse::Model< ValueType > > const &	model,
		std::string const &	filename,
		storm::umb::ExportOptions const &	options = {} )

Definition at line 65 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 75 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 44 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 62 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 31 of file properties.cpp.

getModelParameters()

template<typename ValueType>

std::set< typename storm::storage::ParameterRegion< ValueType >::VariableType > storm::api::getModelParameters

(

storm::models::ModelBase const &

model

)

Definition at line 50 of file region.h.

getSupportedJaniFeatures()

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

inline

Definition at line 32 of file builder.h.

initializeMonotonicityBackend()

template<typename ParametricType, typename ImpreciseType = double, typename PreciseType = storm::RationalNumber>

std::unique_ptr< storm::modelchecker::MonotonicityBackend< ParametricType > > storm::api::initializeMonotonicityBackend	(	storm::modelchecker::RegionModelChecker< ParametricType > const &	regionChecker,
		storm::modelchecker::RegionCheckEngine	engine,
		storm::modelchecker::CheckTask< storm::logic::Formula, ParametricType > const &	task,
		MonotonicitySetting const &	monotonicitySetting,
		std::optional< std::pair< std::set< typename storm::storage::ParameterRegion< ParametricType >::VariableType >, std::set< typename storm::storage::ParameterRegion< ParametricType >::VariableType > > >	monotoneParameters = std::nullopt )

Definition at line 199 of file region.h.

initializeRegionModelChecker() [1/2]

template<typename ValueType, typename ImpreciseType = double, typename PreciseType = storm::RationalNumber>

std::unique_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	allowModelSimplification = true,
		storm::pars::analysis::GraphPreservationStatus	graphPreservationStatus = storm::pars::analysis::GraphPreservationStatus::GraphPreserving,
		bool	preconditionsValidated = false,
		MonotonicitySetting	monotonicitySetting = MonotonicitySetting(),
		std::optional< std::pair< std::set< typename storm::storage::ParameterRegion< ValueType >::VariableType >, std::set< typename storm::storage::ParameterRegion< ValueType >::VariableType > > >	monotoneParameters = std::nullopt )

Definition at line 238 of file region.h.

initializeRegionModelChecker() [2/2]

template<typename ValueType>

std::unique_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 260 of file region.h.

initializeRegionRefinementChecker()

template<typename ValueType, typename ImpreciseType = double, typename PreciseType = storm::RationalNumber>

std::unique_ptr< storm::modelchecker::RegionRefinementChecker< ValueType > > storm::api::initializeRegionRefinementChecker	(	Environment const &	env,
		RefinementOptions< ValueType >	settings )

Definition at line 288 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,
		typename storm::builder::ExplicitModelBuilder< ValueType >::Options const &	explorationOptions = typename storm::builder::ExplicitModelBuilder<ValueType>::Options() )

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 95 of file builder.h.

mergeEquivalentStatesForFormula() [1/4]

template std::shared_ptr< storm::models::sparse::Model< double > > storm::api::mergeEquivalentStatesForFormula	(	std::shared_ptr< storm::models::sparse::Model< double > > const &	model,
		storm::logic::Formula const &	formula )

mergeEquivalentStatesForFormula() [2/4]

template std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > > storm::api::mergeEquivalentStatesForFormula	(	std::shared_ptr< storm::models::sparse::Model< storm::RationalFunction > > const &	model,
		storm::logic::Formula const &	formula )

mergeEquivalentStatesForFormula() [3/4]

template std::shared_ptr< storm::models::sparse::Model< storm::RationalNumber > > storm::api::mergeEquivalentStatesForFormula	(	std::shared_ptr< storm::models::sparse::Model< storm::RationalNumber > > const &	model,
		storm::logic::Formula const &	formula )

mergeEquivalentStatesForFormula() [4/4]

template<typename ValueType>

std::shared_ptr< storm::models::sparse::Model< ValueType > > storm::api::mergeEquivalentStatesForFormula	(	std::shared_ptr< storm::models::sparse::Model< ValueType > > const &	model,
		storm::logic::Formula const &	formula )

Identifies states of the given model that are equivalent w.r.t.

to the given formula and merges them into a single state, yielding a (potentially smaller) model on which the given formula can still be checked.

Note

depending on the formula, this merges, e.g., states with probability 0/1 or reward 0/infty based on graph-based analysis.

Returns

the resulting model, or nullptr if merging is not applicable (e.g. because the model type or the formula is not supported).

Definition at line 12 of file transformation.cpp.

parseCapacitiesList()

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

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

parseJaniModel() [1/2]

STORM_PARSERS_API 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]

STORM_PARSERS_API 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]

STORM_PARSERS_API 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]

STORM_PARSERS_API 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 161 of file region.h.

parseProgram()

STORM_PARSERS_API 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]

STORM_PARSERS_API 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]

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

STORM_PARSERS_API 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 60 of file properties.cpp.

parsePropertiesForPrismProgram()

STORM_PARSERS_API 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 70 of file properties.cpp.

parsePropertiesForSymbolicModelDescription()

STORM_PARSERS_API 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 77 of file properties.cpp.

parsePropertyFilter()

STORM_PARSERS_API 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 134 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 147 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 97 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 109 of file region.h.

parseVariableList() [1/2]

template<typename ValueType>

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

Definition at line 64 of file region.h.

parseVariableList() [2/2]

template<typename ValueType>

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

Definition at line 91 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::bisimulation::Options const &	options = {} )

Definition at line 17 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::bisimulation::BisimulationType const &	= storm::bisimulation::BisimulationType::Strong,
		storm::dd::bisimulation::SignatureMode const &	= storm::dd::bisimulation::SignatureMode::Eager,
		storm::dd::bisimulation::QuotientFormat const &	= storm::dd::bisimulation::QuotientFormat::Dd,
		storm::dd::bisimulation::BisimulationOptions const &	= storm::dd::bisimulation::BisimulationOptions() )

Definition at line 53 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::bisimulation::BisimulationType const &	bisimulationType = storm::bisimulation::BisimulationType::Strong,
		storm::dd::bisimulation::SignatureMode const &	mode = storm::dd::bisimulation::SignatureMode::Eager,
		storm::dd::bisimulation::QuotientFormat const &	quotientFormat = storm::dd::bisimulation::QuotientFormat::Dd,
		storm::dd::bisimulation::BisimulationOptions const &	bisimulationOptions = storm::dd::bisimulation::BisimulationOptions() )

Definition at line 26 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 165 of file transformation.h.

preprocessSparseModelForParameterLifting()

template<typename ParametricType>

std::shared_ptr< storm::models::sparse::Model< ParametricType > > storm::api::preprocessSparseModelForParameterLifting	(	std::shared_ptr< storm::models::sparse::Model< ParametricType > > const &	model,
		storm::modelchecker::CheckTask< storm::logic::Formula, ParametricType > const &	task,
		storm::modelchecker::RegionCheckEngine	engine,
		bool	preconditionsValidatedManually = false )

Definition at line 171 of file region.h.

printGspnStatsToStream()

void storm::api::printGspnStatsToStream	(	storm::gspn::GSPN const &	gspn,
		std::ostream &	out )

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

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 135 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 154 of file storm-conv.cpp.

simplifyJaniModel()

STORM_PARSERS_API 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 14 of file properties.cpp.

substituteTranscendentalNumbersInProperties()

std::vector< storm::jani::Property > storm::api::substituteTranscendentalNumbersInProperties

(

std::vector< storm::jani::Property > const &

properties

)

Definition at line 23 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 67 of file transformation.h.

transformJani()

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

Definition at line 17 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 93 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 107 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 131 of file transformation.h.

verifyRegion()

template<typename ValueType>

bool storm::api::verifyRegion	(	Environment const &	env,
		RefinementOptions< ValueType >	settings,
		storm::storage::ParameterRegion< ValueType > const &	region )

Verifies whether a region satisfies a property.

Parameters

settings	The refinement options
region	The region to be analyzed

Returns

true if the region satisfies the property, false otherwise

Definition at line 350 of file region.h.

verifyWithDdEngine() [1/6]

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 497 of file verification.h.

verifyWithDdEngine() [2/6]

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 522 of file verification.h.

verifyWithDdEngine() [3/6]

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 544 of file verification.h.

verifyWithDdEngine() [4/6]

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 479 of file verification.h.

verifyWithDdEngine() [5/6]

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::Mdp< DdType, ValueType > > const &	mdp,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task )

Definition at line 504 of file verification.h.

verifyWithDdEngine() [6/6]

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 529 of file verification.h.

verifyWithExplorationEngine() [1/2]

template<typename ValueType>

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

Definition at line 62 of file verification.h.

verifyWithExplorationEngine() [2/2]

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 92 of file verification.h.

verifyWithHybridEngine() [1/10]

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 393 of file verification.h.

verifyWithHybridEngine() [2/10]

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 368 of file verification.h.

verifyWithHybridEngine() [3/10]

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 443 of file verification.h.

verifyWithHybridEngine() [4/10]

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 418 of file verification.h.

verifyWithHybridEngine() [5/10]

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 469 of file verification.h.

verifyWithHybridEngine() [6/10]

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 375 of file verification.h.

verifyWithHybridEngine() [7/10]

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 350 of file verification.h.

verifyWithHybridEngine() [8/10]

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::MarkovAutomaton< DdType, ValueType > > const &	ma,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task )

Definition at line 425 of file verification.h.

verifyWithHybridEngine() [9/10]

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::Mdp< DdType, ValueType > > const &	mdp,
		storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	task )

Definition at line 400 of file verification.h.

verifyWithHybridEngine() [10/10]

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 450 of file verification.h.

verifyWithSparseEngine() [1/12]

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 153 of file verification.h.

verifyWithSparseEngine() [2/12]

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,
		bool	preferEliminationChecker = false )

Definition at line 129 of file verification.h.

verifyWithSparseEngine() [3/12]

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 209 of file verification.h.

verifyWithSparseEngine() [4/12]

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 179 of file verification.h.

verifyWithSparseEngine() [5/12]

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,
		bool	preferEliminationChecker = false )

Definition at line 261 of file verification.h.

verifyWithSparseEngine() [6/12]

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 232 of file verification.h.

verifyWithSparseEngine() [7/12]

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 137 of file verification.h.

verifyWithSparseEngine() [8/12]

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,
		bool	preferEliminationChecker = false )

Definition at line 102 of file verification.h.

verifyWithSparseEngine() [9/12]

template<typename ValueType>

std::unique_ptr< storm::modelchecker::CheckResult > 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 186 of file verification.h.

verifyWithSparseEngine() [10/12]

template<typename ValueType>

std::unique_ptr< storm::modelchecker::CheckResult > 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 160 of file verification.h.

verifyWithSparseEngine() [11/12]

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,
		bool	preferEliminationChecker = false )

Definition at line 239 of file verification.h.

verifyWithSparseEngine() [12/12]

template<typename ValueType>

std::unique_ptr< storm::modelchecker::CheckResult > 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 216 of file verification.h.