Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
storm::api Namespace Reference

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::CounterexamplecomputeHighLevelCounterexampleMilp (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::CounterexamplecomputeHighLevelCounterexampleMaxSmt (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::CounterexamplecomputeKShortestPathCounterexample (std::shared_ptr< storm::models::sparse::Model< double > > model, std::shared_ptr< storm::logic::Formula const > const &formula, size_t maxK)
 
storm::jani::ModelbuildJani (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::PropertyparseProperties (storm::parser::FormulaParser &formulaParser, std::string const &inputString, boost::optional< std::set< std::string > > const &propertyFilter)
 
std::vector< storm::jani::PropertyparseProperties (std::string const &inputString, boost::optional< std::set< std::string > > const &propertyFilter)
 
std::vector< storm::jani::PropertyparsePropertiesForJaniModel (std::string const &inputString, storm::jani::Model const &model, boost::optional< std::set< std::string > > const &propertyFilter)
 
std::vector< storm::jani::PropertyparsePropertiesForPrismProgram (std::string const &inputString, storm::prism::Program const &program, boost::optional< std::set< std::string > > const &propertyFilter)
 
std::vector< storm::jani::PropertyparsePropertiesForSymbolicModelDescription (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 , 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::PropertysubstituteConstantsInProperties (std::vector< storm::jani::Property > const &properties, std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution)
 
std::vector< storm::jani::PropertysubstituteTranscendentalNumbersInProperties (std::vector< storm::jani::Property > const &properties)
 
std::vector< storm::jani::PropertyfilterProperties (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::unique_ptr< storm::modelchecker::CheckResultverifyWithExplorationEngine (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::CheckResultverifyWithExplorationEngine (storm::storage::SymbolicModelDescription const &model, storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &task)
 
template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResultverifyWithSparseEngine (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::CheckResultverifyWithSparseEngine (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::CheckResultverifyWithSparseEngine (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::CheckResultverifyWithSparseEngine (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::CheckResultverifyWithSparseEngine (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::CheckResultverifyWithSparseEngine (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::CheckResultverifyWithSparseEngine (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::CheckResultverifyWithSparseEngine (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::CheckResultverifyWithSparseEngine (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::CheckResultverifyWithSparseEngine (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::CheckResultverifyWithSparseEngine (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::CheckResultverifyWithSparseEngine (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::CheckResultcomputeSteadyStateDistributionWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Dtmc< ValueType > > const &dtmc)
 
template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResultcomputeSteadyStateDistributionWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Ctmc< ValueType > > const &ctmc)
 
template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResultcomputeSteadyStateDistributionWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Model< ValueType > > const &model)
 
template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResultcomputeExpectedVisitingTimesWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Dtmc< ValueType > > const &dtmc)
 
template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResultcomputeExpectedVisitingTimesWithSparseEngine (storm::Environment const &env, std::shared_ptr< storm::models::sparse::Ctmc< ValueType > > const &ctmc)
 
template<typename ValueType >
std::unique_ptr< storm::modelchecker::CheckResultcomputeExpectedVisitingTimesWithSparseEngine (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::CheckResultverifyWithHybridEngine (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::CheckResultverifyWithHybridEngine (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::CheckResultverifyWithHybridEngine (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::CheckResultverifyWithHybridEngine (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::CheckResultverifyWithHybridEngine (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::CheckResultverifyWithHybridEngine (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::CheckResultverifyWithHybridEngine (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::CheckResultverifyWithHybridEngine (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::CheckResultverifyWithHybridEngine (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::CheckResultverifyWithHybridEngine (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::CheckResultverifyWithDdEngine (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::CheckResultverifyWithDdEngine (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::CheckResultverifyWithDdEngine (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::CheckResultverifyWithDdEngine (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::CheckResultverifyWithDdEngine (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::CheckResultverifyWithDdEngine (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 123 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 116 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 109 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
engineThe considered region checking engine
coverageThresholdif given, the refinement stops as soon as the fraction of the area of the subregions with inconclusive result is less then this threshold
refinementDepthThresholdif given, the refinement stops at the given depth. depth=0 means no refinement.
hypothesisif not 'unknown', it is only checked whether the hypothesis holds (and NOT the complementary result).
allowModelSimplification
useMonotonicity
monThreshif 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 305 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 293 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 317 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 266 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 254 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 278 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 113 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 130 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.

◆ 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 80 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 66 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 45 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 29 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 53 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 61 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 40 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
ValueTypeType of the probabilities in the sparse model
Parameters
modelSymbolicModelDescription of the model
optionsBuilder options
actionMaskAn 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/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 482 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 507 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 529 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 464 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 489 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 514 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 53 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 83 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 378 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 353 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 428 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 403 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 454 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 360 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 335 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 410 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 385 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 435 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 140 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 
)

Definition at line 117 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 196 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 166 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 
)

Definition at line 247 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 219 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 124 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 
)

Definition at line 93 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 173 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 147 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 
)

Definition at line 226 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 203 of file verification.h.