Index

A

abs() (in module stormpy.numbers.developer) (in module stormpy.numbers.developer.cln) (in module stormpy.numbers.developer.gmp) (Interval method), [1] ABSOLUTE (MultiObjectivePrecisionType attribute) accepting_label (GenerateMonitorVerifierOptions property) action_index (JaniEdge property) (PrismCommand property) action_name (PrismCommand property) action_sensitive (BisimulationOptions property) ActionMask (class in stormpy.developer) actions (SparseModelState property) ACYCLIC (EquationSolverType attribute) Add (class in stormpy.developer.storage) add() (JaniOrderedAssignments method) (SmtSolver method) (Z3SmtSolver method) add_automaton() (JaniModel method) add_backward_implication_cuts (SMTMinimalLabelSetGeneratorOptions property) add_boolean_variable() (ValuationDescriptionBuilder method) add_constant() (JaniModel method) add_destination() (JaniTemplateEdge method) add_double_variable() (ValuationDescriptionBuilder method) add_edge() (JaniAutomaton method) add_expression() (ValuationTransformer method) add_immediate_transition() (GspnBuilder method) add_inhibition_arc() (GspnBuilder method) add_initial_location() (JaniAutomaton method) add_input_arc() (GspnBuilder method) add_integer_variable() (ValuationDescriptionBuilder method) add_label() (ChoiceLabeling method) (ItemLabeling method) (StateLabeling method) add_label_to_choice() (ChoiceLabeling method) add_label_to_state() (StateLabeling method) add_labels_claiming (ModelBuilderEnvironment property) add_location() (JaniAutomaton method) add_next_value() (SparseMatrixBuilder method) add_next_values() (SparseMatrixBuilder method) add_normal_arc() (GspnBuilder method) add_note() (NoPicklingSupport method) (ParserError method) (StormError method) (StormWarning method) add_output_arc() (GspnBuilder method) add_place() (GspnBuilder method) add_rational_variable() (ValuationDescriptionBuilder method) add_reward_model() (SparseCtmc method) (SparseDtmc method) (SparseMA method) (SparseMdp method) (SparseModel method) (SparsePomdp method) (SparseSmg method) add_reward_threshold_combination() (SMTMinimalLabelSetGeneratorCexInput method) add_string_variable() (ValuationDescriptionBuilder method) add_timed_transition() (GspnBuilder method) add_uncertainty() (in module stormpy.transformations) add_variable() (JaniVariableSet method) AddIterator (class in stormpy.developer.storage) AddUncertainty (class in stormpy.developer) aggregate() (ExplicitQuantitativeCheckResult method) (HybridQuantitativeCheckResult method) (QuantitativeCheckResult method) (SymbolicQuantitativeCheckResult method) AggregatedValue (class in stormpy.results) algorithm (ConditionalModelCheckerEnvironment property) ALL (StateLabelPreservation attribute) ALL_SAT (RegionResult attribute) (RegionResultHypothesis attribute) ALL_VIOLATED (RegionResult attribute) (RegionResultHypothesis attribute)

allow_choice_labeling_as_actions (UmbExportOptions property) allow_choice_origins_as_actions (UmbExportOptions property) allow_dc_for_relevant_events (ModelBuilderEnvironment property) allow_placeholders (DirectEncodingExporterOptions property) analysis_environment (DftEnvironment property) analysis_time (SMTMinimalLabelSetGeneratorStats property) AnalysisEnvironment (class in stormpy.dft) analyze_dft() (in module stormpy.dft) (in module stormpy.dft.developer) analyze_for_initial_states() (IterativePolicySearch method) analyze_region() (RegionModelChecker method) (SparseDtmcParameterLiftingModelChecker method) (SparseMdpParameterLiftingModelChecker method) AND (BinaryBooleanOperatorType attribute) (DFTElementType attribute) (FormulaType attribute) (OperatorType attribute) And() (Expression static method) ANNEALING (CuddReorderingTechnique attribute) apply_scheduler() (SparseMA method) (SparseMdp method) (SparsePomdp method) apply_unknown_fsc() (in module stormpy.pomdp) ApplyFiniteSchedulerToPomdp (class in stormpy.pomdp.developer) approximation_error (AnalysisEnvironment property) approximation_heuristic (AnalysisEnvironment property) ApproximationHeuristic (class in stormpy.dft) ARBITRARY (SchedulerMemoryPattern attribute) area (ParameterRegion property) ARGMAX (FilterType attribute) ARGMIN (FilterType attribute) args (NoPicklingSupport attribute) (ParserError attribute) (StormError attribute) (StormWarning attribute) arity (Expression property) ArrayType (class in stormpy.io) as_be() (FailableElement method) as_be_double() (FailableElement method) as_be_ratfunc() (FailableElement method) as_dependency() (FailableElement method) as_dependency_double() (FailableElement method) as_dependency_ratfunc() (FailableElement method) as_jani_choice_origins() (ChoiceOrigins method) (JaniChoiceOrigins method) (PrismChoiceOrigins method) as_jani_model() (SymbolicModelDescription method) as_prism_choice_origins() (ChoiceOrigins method) (JaniChoiceOrigins method) (PrismChoiceOrigins method) as_prism_program() (SymbolicModelDescription method) assignments (JaniEdgeDestination property) (JaniLocation property) (JaniTemplateEdge property) (JaniTemplateEdgeDestination property) (PrismUpdate property) AtomicExpressionFormula (class in stormpy.logic) AtomicLabelFormula (class in stormpy.logic) AUTO (MultiObjectiveEncodingType attribute) automata (JaniModel property) AUTOMATIC (SteadyStateDistributionAlgorithm attribute) available_actions() (PrismSimulator method) (Simulator method) (SparseSimulator method) average() (ExplicitQuantitativeCheckResult method) (HybridQuantitativeCheckResult method) (QuantitativeCheckResult method) (SymbolicQuantitativeCheckResult method) AVG (FilterType attribute) avg_var_domain_size (JaniInformationObject property)

B

backward_transition_matrix (SparseCtmc property) (SparseDtmc property) (SparseMA property) (SparseMdp property) (SparseModel property) (SparsePomdp property) (SparseSmg property) base_type (ArrayType property) (BoundedType property) BasicType (class in stormpy.io) Bdd (class in stormpy.developer.storage) BE (DFTElementType attribute) belief_mdp_analysis_time_ms (BeliefBasedModelCheckerStatistics property) belief_mdp_build_time_ms (BeliefBasedModelCheckerStatistics property) belief_mdp_choices (BeliefBasedModelCheckerStatistics property) belief_mdp_states (BeliefBasedModelCheckerStatistics property) belief_mdp_transitions (BeliefBasedModelCheckerStatistics property) BeliefBasedModelCheckerOptions (class in stormpy.pomdp.developer) BeliefBasedModelCheckerResult (class in stormpy.pomdp) BeliefBasedModelCheckerStatistics (class in stormpy.pomdp) BeliefSupportTracker (class in stormpy.pomdp) BFS (ExplorationOrder attribute) BinaryBooleanOperatorType (class in stormpy.logic) BinaryBooleanStateFormula (class in stormpy.logic) BinaryPathFormula (class in stormpy.logic) BinaryPomdpTransformer (class in stormpy.pomdp.developer) BinaryStateFormula (class in stormpy.logic) BISECTION (ConditionalAlgorithmSetting attribute) BISECTION_ADVANCED (ConditionalAlgorithmSetting attribute) BISECTION_ADVANCED_PT (ConditionalAlgorithmSetting attribute) BISECTION_PT (ConditionalAlgorithmSetting attribute) bisimulation_type (BisimulationOptions property) BisimulationOptions (class in stormpy.transformations) BisimulationType (class in stormpy.transformations) BitVector (class in stormpy.datastructures) BITVECTOR (DdMetaVariableType attribute) (FormulaType attribute) BLOCK_NUMBERS (ReuseMode attribute) BOOL (DdMetaVariableType attribute) (FormulaType attribute) (VariableType attribute) boolean() (ExpressionManager method) boolean_variables (PrismModule property)

BooleanLiteralFormula (class in stormpy.logic) BOUND_DIFFERENCE (ApproximationHeuristic attribute) BoundedType (class in stormpy.io) BoundedUntilFormula (class in stormpy.logic) BoundedValue (class in stormpy.results) BoundType (class in stormpy.numbers.developer) build() (ExplicitDFTModelBuilder method) (ExplicitModelBuilder method) (MemoryStructureBuilder method) (MemoryStructureProduct method) (PomdpMemoryBuilder method) (SparseMatrixBuilder method) (ValuationTransformer method) build_action_mapping (SubsystemBuilderOptions property) build_choice_labeling (BeliefBasedModelCheckerOptions property) (DirectEncodingParserOptions property) (UmbImportOptions property) build_choice_labels (ExplicitModelParserOptions property) build_class_description() (ValuationDescriptionBuilder method) build_environment() (EnvironmentBuilder static method) build_explicit_drn_model() (in module stormpy.developer) build_explicit_model() (in module stormpy.developer) build_gspn() (GspnBuilder method) build_info() (StormVersion static method) build_jani_model() (in module stormpy.gspn) build_kept_actions (SubsystemBuilderOptions property) build_model() (in module stormpy) (in module stormpy.dft) (in module stormpy.dft.developer) build_model_from_drn() (in module stormpy) build_model_from_explicit() (in module stormpy) build_model_from_umb() (in module stormpy) build_sparse_matrix() (in module stormpy.datastructures) build_sparse_model() (in module stormpy.developer) build_state_generation_info() (DFT method) build_state_mapping (SubsystemBuilderOptions property) build_state_valuations (UmbImportOptions property) build_submodel() (in module stormpy.transformations) build_subsystem() (in module stormpy.developer) build_symbolic_model() (in module stormpy) (in module stormpy.developer) BuilderOptions (class in stormpy) (class in stormpy.developer)

C

cache() (FactorizedPolynomial method) can_have_nondeterminism() (DFT method) canonicize_pomdp (UmbExportOptions property) carl_version() (in module stormpy.numbers.developer) CEIL (OperatorType attribute) ceil() (in module stormpy.numbers.developer) (in module stormpy.numbers.developer.cln) (in module stormpy.numbers.developer.gmp) center() (Interval method), [1] CENTER_SAT (RegionResult attribute) CENTER_VIOLATED (RegionResult attribute) CHANGED_STATES (RefinementMode attribute) check() (PcaaWeightVectorChecker method) (SmtSolver method) (SparseInstantiationModelChecker method) (Z3SmtSolver method) check_dft_validity() (in module stormpy.dft) check_feasibility() (in module stormpy.pars) (in module stormpy.pars.developer) check_threshold_feasible (SMTMinimalLabelSetGeneratorOptions property) check_transitions_outside (SubsystemBuilderOptions property) check_valid() (JaniModel method) CheckResult (class in stormpy) (class in stormpy.results) CheckTask (class in stormpy.developer) Choice (class in stormpy.developer) choice_labeling (SparseCtmc property) (SparseDtmc property) (SparseMA property) (SparseMdp property) (SparseModel property) (SparseModelComponents property) (SparsePomdp property) (SparseSmg property) choice_origins (SparseCtmc property) (SparseDtmc property) (SparseMA property) (SparseMdp property) (SparseModel property) (SparseModelComponents property) (SparsePomdp property) (SparseSmg property) ChoiceLabeling (class in stormpy.models) ChoiceOrigins (class in stormpy.models) chunksize (AnalysisEnvironment property) CLASSIC (MultiObjectiveEncodingType attribute) (SteadyStateDistributionAlgorithm attribute) clear() (BitVector method) clear_bounds() (ExplicitQuantitativeCheckResult method) clear_monomial_pool() (in module stormpy.numbers.developer) clear_pools() (in module stormpy.numbers) clear_variable_pool() (in module stormpy.numbers.developer) clipping_resolutions (BeliefBasedModelCheckerOptions property) ClockType (class in stormpy.io) clone() (AtomicExpressionFormula method) (AtomicLabelFormula method) (BinaryBooleanStateFormula method) (BinaryPathFormula method) (BinaryStateFormula method) (BooleanLiteralFormula method) (BoundedUntilFormula method) (ConditionalFormula method) (CumulativeRewardFormula method) (DiscountedCumulativeRewardFormula method) (DiscountedTotalRewardFormula method) (EventuallyFormula method) (Formula method) (GameFormula method) (GloballyFormula method) (InstantaneousRewardFormula method) (JaniOrderedAssignments method) (LongRunAverageOperatorFormula method) (LongRunAverageRewardFormula method) (MultiObjectiveFormula method) (OperatorFormula method) (PathFormula method) (ProbabilityOperatorFormula method) (Property method) (RewardOperatorFormula method) (StateFormula method) (SymbolicQuantitativeCheckResult method) (TimeOperatorFormula method) (UnaryBooleanStateFormula method) (UnaryPathFormula method) (UnaryStateFormula method) (UntilFormula method) close() (SparseMA method) coeff (Term property), [1] coefficient (FactorizedPolynomial property) collect_all_parameters() (SparseCtmc method) (SparseDtmc method) (SparseMA method) (SparseMdp method) (SparseModel method) (SparsePomdp method) (SparseSmg method) collect_model_information() (in module stormpy.developer.storage) collect_probability_parameters() (SparseCtmc method) (SparseDtmc method) (SparseMA method) (SparseMdp method) (SparseModel method) (SparsePomdp method) (SparseSmg method) collect_rate_parameters() (SparseCtmc method) (SparseDtmc method) (SparseMA method) (SparseMdp method) (SparseModel method) (SparsePomdp method) (SparseSmg method) collect_reward_parameters() (SparseCtmc method) (SparseDtmc method) (SparseMA method) (SparseMdp method) (SparseModel method) (SparsePomdp method) (SparseSmg method)

color (JaniEdge property) column (SparseMatrixEntry property) commands (PrismModule property) comparison_type (LongRunAverageOperatorFormula property) (OperatorFormula property) (ProbabilityOperatorFormula property) (RewardOperatorFormula property) (TimeOperatorFormula property) ComparisonType (class in stormpy.logic) complement() (BitVector method) (ExplicitQualitativeCheckResult method) (Interval method), [1] (QualitativeCheckResult method) (SymbolicQualitativeCheckResult method) completed_exploration (BeliefBasedModelCheckerResult property) (BeliefBasedModelCheckerStatistics property) compression (UmbExportOptions property) CompressionMode (class in stormpy.io) compute_action_support() (Scheduler method) compute_all_transient_probabilities() (in module stormpy.developer) compute_all_until_probabilities() (in module stormpy.developer) compute_counterexample_label_set() (SMTMinimalLabelSetGenerator static method) compute_dependency_conflicts() (in module stormpy.dft.developer) compute_depth() (SymbolicCtmc method) (SymbolicDtmc method) (SymbolicMA method) (SymbolicMdp method) (SymbolicModel method) compute_expected_number_of_visits() (in module stormpy.analysis) compute_expected_visiting_times_with_sparse_engine() (in module stormpy.developer) compute_extremal_value() (in module stormpy.pars) (RegionRefinementChecker method) compute_prob01_states() (in module stormpy.analysis) compute_probability_matrix() (SparseCtmc method) compute_relevant_events() (in module stormpy.dft) (in module stormpy.dft.developer) compute_scheduler() (PcaaWeightVectorChecker method) compute_steady_state_distribution() (in module stormpy.analysis) compute_steady_state_distribution_with_sparse_engine() (in module stormpy.developer) compute_winning_region() (IterativePolicySearch method) conditional() (ModelCheckerEnvironment method) conditional_subformula (ConditionalFormula property) ConditionalAlgorithmSetting (class in stormpy.environments) ConditionalFormula (class in stormpy.logic) ConditionalModelCheckerEnvironment (class in stormpy.environments) Conjunction() (Expression static method) constant_part() (FactorizedPolynomial method) (FactorizedRationalFunction method) (Polynomial method) (RationalFunction method), [1] constant_precision (CuddDdManagerEnvironment property) constants (JaniModel property) (PrismProgram property) Constraint (class in stormpy.numbers.developer.cln.formula) (class in stormpy.numbers.developer.gmp.formula) CONSTRAINT (FormulaType attribute) CONSTRAINT_BASED (MultiObjectiveMethod attribute) ConstraintCollector (class in stormpy.pars) contains() (Halfspace method) (Interval method), [1] (Polytope method) contains_label() (ChoiceLabeling method) (ItemLabeling method) (StateLabeling method) contains_undefined_constants() (Property method) contains_variable() (Expression method) contains_variables() (Expression method) CONTINUE (SimulationTraceResult attribute) continue_after_first_counterexample_until (SMTMinimalLabelSetGeneratorOptions property) ContinuousType (class in stormpy.io) convert_to_cln() (in module stormpy.numbers.developer.convert) convert_to_ctmc() (SparseMA method) convert_to_gmp() (in module stormpy.numbers.developer.convert) convertible_to_ctmc (SparseMA property) COOPERATIVE (UncertaintyResolutionMode attribute) core_environment (DftEnvironment property) COUNT (FilterType attribute) count() (ExplicitQualitativeCheckResult method) (milliseconds method) (QualitativeCheckResult method) (SymbolicQualitativeCheckResult method) COUNTER (SchedulerMemoryPattern attribute) create() (EnvironmentFactory method) (ExactEnvironmentFactory method) (RandomGenerator static method) (SoundEnvironmentFactory method) create_downward_closure() (Polytope static method) create_factorized_polynomial() (in module stormpy.numbers.developer.cln) (in module stormpy.numbers.developer.gmp) create_filter() (in module stormpy) create_filter_initial_states() (in module stormpy) create_iterative_policy_search() (in module stormpy.pomdp) (in module stormpy.pomdp.developer) create_memory() (in module stormpy.pomdp) create_memory_scheduler_from_product_scheduler() (SparseModelMemoryProductReverseData method) create_monitor_verifier() (in module stormpy.pomdp) create_monomial() (in module stormpy.numbers.developer) create_nondeterministic_belief_tracker() (in module stormpy.pomdp) create_observation_trace_unfolder() (in module stormpy.pomdp) create_product() (GenerateMonitorVerifier method) create_quotient_choice_mapping (BisimulationOptions property) create_region() (in module stormpy.pars) create_simulator() (in module stormpy.simulator) create_weight_vector_checker() (in module stormpy.developer) CTMC (JaniModelType attribute) (ModelType attribute) (PrismModelType attribute) CTMDP (JaniModelType attribute) (PrismModelType attribute) CUDD (DdType attribute) cudd() (DdEnvironment method) CuddDdManagerEnvironment (class in stormpy.environments) CuddReorderingTechnique (class in stormpy.environments) CumulativeRewardFormula (class in stormpy.logic) cut_time (SMTMinimalLabelSetGeneratorStats property) cut_zero_gap (BeliefBasedModelCheckerOptions property)

D

Dd (class in stormpy.developer.storage) DD (Engine attribute) (QuotientFormat attribute) dd() (Environment method) dd_manager (Add property) (Bdd property) (Dd property) (SymbolicCtmc property) (SymbolicDtmc property) (SymbolicMA property) (SymbolicMdp property) (SymbolicModel property) DdBisimulationOptions (class in stormpy.developer) DdEnvironment (class in stormpy.environments) DdManager (class in stormpy.developer.storage) DdMetaVariable (class in stormpy.developer.storage) DdMetaVariableType (class in stormpy.developer.storage) DdType (class in stormpy.models) deadlock_label (SubsystemBuilderReturnType property) DEBUG (LogLevel attribute) declare_boolean_variable() (ExpressionManager method) declare_integer_variable() (ExpressionManager method) declare_rational_variable() (ExpressionManager method) declare_string_variable() (ExpressionManager method) decode_automaton_and_edge_index() (JaniModel static method) DEFAULT (CompressionMode attribute) (ConditionalAlgorithmSetting attribute) (StateLabelPreservation attribute) (UmbExportValueType attribute) (UmbImportValueType attribute) default() (in module stormpy.environments) define_undefined_constants() (JaniModel method) (PrismProgram method) defined (JaniConstant property) (PrismConstant property) (SchedulerChoice property) definition (PrismConstant property) degree() (Polynomial method) DELETE_LABELS (EliminationLabelBehavior attribute) denominator (FactorizedRationalFunction property) (Rational property) (RationalFunction property), [1] denominator() (in module stormpy.numbers.developer.cln) (in module stormpy.numbers.developer.gmp) dependent_events (DFTDependency property) DEPTH (ApproximationHeuristic attribute) DERIVATIVE (RegionSplitEstimateKind attribute) derive() (FactorizedPolynomial method) (FactorizedRationalFunction method) (Polynomial method) (RationalFunction method), [1] deserialize() (in module stormpy.numbers.developer.parse)

destinations (JaniEdge property) (JaniTemplateEdge property) deterministic (Scheduler property) (SchedulerChoice property) DFS (ExplorationOrder attribute) DFT (class in stormpy.dft) DFTBE (class in stormpy.dft) DFTDependency (class in stormpy.dft) DFTElement (class in stormpy.dft) DFTElementType (class in stormpy.dft) DftEnvironment (class in stormpy.dft) DftIndependentModule (class in stormpy.dft) (class in stormpy.dft.developer) DftInstantiator (class in stormpy.dft) DFTSimulator (class in stormpy.dft) DFTState (class in stormpy.dft) DFTStateGenerationInfo (class in stormpy.dft.developer) DftSymmetries (class in stormpy.dft) DFTTraceSimulator (class in stormpy.dft.developer) diameter() (Interval method), [1] DiceStringVisitor (class in stormpy.developer.storage) difference() (Interval method), [1] DIFFERENCE_PROBABILITY_SUM (NextStateHeuristic attribute) DirectEncodingExporterOptions (class in stormpy.io) DirectEncodingParserOptions (class in stormpy.io) discount_factor_double (DiscountedCumulativeRewardFormula property) (DiscountedTotalRewardFormula property) discount_factor_rational (DiscountedCumulativeRewardFormula property) (DiscountedTotalRewardFormula property) DiscountedCumulativeRewardFormula (class in stormpy.logic) DiscountedTotalRewardFormula (class in stormpy.logic) discovered_beliefs (BeliefBasedModelCheckerStatistics property) DiscreteTimePrismProgramSimulator (class in stormpy.developer) DiscreteTimeSparseModelSimulator (class in stormpy.developer) Disjunction() (Expression static method) distance (Path property) DISTANCE (RegionSplitEstimateKind attribute) distance() (Halfspace method) Distribution (class in stormpy.datastructures) div() (in module stormpy.numbers.developer) (in module stormpy.numbers.developer.cln) (in module stormpy.numbers.developer.gmp) (Interval method), [1] DIVIDE (OperatorType attribute) Divide() (Expression static method) dont_care() (DFTState method) DOUBLE (UmbExportValueType attribute) (UmbImportValueType attribute) DOUBLE_INTERVAL (UmbExportValueType attribute) downward_closure() (Polytope method) DTMC (JaniModelType attribute) (ModelType attribute) (PrismModelType attribute)

E

EAGER (SignatureMode attribute) edges (JaniAutomaton property) EIGEN (EquationSolverType attribute) elements (DftIndependentModule property) eliminate_chains (TransformationEnvironment property) eliminate_non_markovian_chains() (in module stormpy.developer) (in module stormpy.transformations) eliminate_reward_accumulations() (RewardAccumulationEliminationVisitor method) ELIMINATION (EquationSolverType attribute) EliminationLabelBehavior (class in stormpy.transformations) empty() (BitVector method) (JaniVariableSet method) emptyInterval() (Interval static method), [1] encloses() (SolutionBounds method) encode_automaton_and_edge_index() (JaniModel static method) encode_reachability (SMTMinimalLabelSetGeneratorOptions property) encoding_type (MultiObjectiveModelCheckerEnvironment property) EndComponentEliminator (class in stormpy.developer) EndComponentEliminatorReturnType (class in stormpy.developer) Engine (class in stormpy) entity_has_variable() (Valuations method) Environment (class in stormpy) (class in stormpy.environments) EnvironmentBuilder (class in stormpy.developer) EnvironmentFactory (class in stormpy.developer) EQ (Relation attribute) Eq() (Expression static method) EQUAL (OperatorType attribute) EQUATION_SYSTEM (SteadyStateDistributionAlgorithm attribute) EquationSolverType (class in stormpy.environments) erase_variable() (JaniVariableSet method) ERR (LogLevel attribute) evaluate() (FactorizedPolynomial method) (FactorizedRationalFunction method) (Polynomial method) (RationalFunction method), [1] evaluate_as_bool() (Expression method) evaluate_as_double() (Expression method) evaluate_as_int() (Expression method) evaluate_as_rational() (Expression method) EventuallyFormula (class in stormpy.logic) EXACT (CuddReorderingTechnique attribute) exact() (in module stormpy.environments) EXACT_PARAMETER_LIFTING (RegionCheckEngine attribute) ExactEnvironmentFactory (class in stormpy.developer) EXISTS (FilterType attribute) (FormulaType attribute) EXISTS_BOTH (RegionResult attribute) exists_inhibition_arc() (ImmediateTransition method) (TimedTransition method) (Transition method) exists_input_arc() (ImmediateTransition method) (TimedTransition method) (Transition method) exists_output_arc() (ImmediateTransition method) (TimedTransition method) (Transition method) EXISTS_SAT (RegionResult attribute)

exists_true() (ExplicitQualitativeCheckResult method) (QualitativeCheckResult method) (SymbolicQualitativeCheckResult method) EXISTS_VIOLATED (RegionResult attribute) exit_rates (SparseCtmc property) (SparseMA property) (SparseModelComponents property) expand() (in module stormpy.numbers.developer.cln) (in module stormpy.numbers.developer.gmp) EXPECTED_VISITING_TIMES (SteadyStateDistributionAlgorithm attribute) ExplicitDFTModelBuilder (class in stormpy.dft.developer) ExplicitModelBuilder (class in stormpy.developer) ExplicitModelBuilderOptions (class in stormpy.developer) ExplicitModelCheckerHint (class in stormpy) ExplicitModelParserOptions (class in stormpy.io) ExplicitParetoCurveCheckResult (class in stormpy.results) ExplicitQualitativeCheckResult (class in stormpy.results) ExplicitQuantitativeCheckResult (class in stormpy.results) ExplicitStateLookup (class in stormpy.developer) exploration() (Environment method) exploration_order (ExplicitModelBuilderOptions property) exploration_queue_order (BeliefBasedModelCheckerOptions property) exploration_state_limit (ExplicitModelBuilderOptions property) exploration_time_ms (BeliefBasedModelCheckerStatistics property) ExplorationEnvironment (class in stormpy.environments) ExplorationOrder (class in stormpy.developer) ExplorationQueueOrder (class in stormpy.pomdp) explored_beliefs (BeliefBasedModelCheckerStatistics property) exponents (Monomial property) export_dft_json_file() (in module stormpy.dft) (in module stormpy.dft.developer) export_dft_json_string() (in module stormpy.dft) export_explicit_state_lookup() (ExplicitModelBuilder method) export_gspn_pnml_file() (in module stormpy.gspn) export_gspn_pnpro_file() (in module stormpy.gspn) export_jani_to_file() (in module stormpy.io) export_sparse_model_as_drn() (in module stormpy.developer) export_to_drn() (in module stormpy.io) export_to_umb() (in module stormpy.io) Expression (class in stormpy.expressions) expression (JaniAssignment property) (PrismAssignment property) (PrismLabel property) expression_manager (JaniModel property) (PrismProgram property) (SimpleValuation property) (Valuation property) expression_variable (JaniConstant property) (JaniVariable property) (PrismBooleanVariable property) (PrismConstant property) (PrismIntegerVariable property) (PrismVariable property) ExpressionManager (class in stormpy.expressions) ExpressionParser (class in stormpy.expressions) ExpressionType (class in stormpy.expressions) extend() (ObservationTraceUnfolder method) EXTEND_LABELS (EliminationLabelBehavior attribute)

F

Factorization (class in stormpy.numbers.developer.cln) (class in stormpy.numbers.developer.gmp) factorization() (FactorizedPolynomial method) FactorizedPolynomial (class in stormpy.numbers.developer.gmp) FactorizedRationalFunction (class in stormpy.numbers.developer.gmp) FailableElement (class in stormpy.dft.developer) FailableElements (class in stormpy.dft.developer) FailableIterator (class in stormpy.dft.developer) FALSE (FormulaType attribute) FATAL (LogLevel attribute) FeasibilityMethod (class in stormpy.pars) FeasibilityResult (class in stormpy.pars) FeasibilitySynthesisResult (class in stormpy.pars) FIFO (ExplorationQueueOrder attribute) fill() (BitVector method) filter() (CheckResult method) (ExplicitParetoCurveCheckResult method) (ExplicitQualitativeCheckResult method) (ExplicitQuantitativeCheckResult method) (HybridQuantitativeCheckResult method) (ParetoCurveCheckResult method) (QualitativeCheckResult method) (QuantitativeCheckResult method) (SymbolicQualitativeCheckResult method) (SymbolicQuantitativeCheckResult method) filter_initial_states() (in module stormpy) FilterType (class in stormpy.results) finalize() (JaniModel method) FINER (InitialPartitionMode attribute) fire() (ImmediateTransition method) (TimedTransition method) (Transition method) fix_deadlocks (ExplicitModelBuilderOptions property) (ExplicitModelParserOptions property) (SubsystemBuilderOptions property)

FIXED_COUNTER (PomdpMemoryPattern attribute) FIXED_RING (PomdpMemoryPattern attribute) FlatSet (class in stormpy.developer) flatten_composition() (JaniModel method) flatten_modules() (PrismProgram method) FLOOR (OperatorType attribute) floor() (in module stormpy.numbers.developer) (in module stormpy.numbers.developer.cln) (in module stormpy.numbers.developer.gmp) FLOW (MultiObjectiveEncodingType attribute) FORALL (FilterType attribute) (FormulaType attribute) forall_true() (ExplicitQualitativeCheckResult method) (QualitativeCheckResult method) (SymbolicQualitativeCheckResult method) force_exact (SolverEnvironment property) force_soundness (SolverEnvironment property) Formula (class in stormpy.logic) (class in stormpy.numbers.developer.cln.formula) (class in stormpy.numbers.developer.gmp.formula) FORMULA_INDIVIDUAL (StateLabelPreservation attribute) FORMULA_PROPOSITIONAL (StateLabelPreservation attribute) FormulaType (class in stormpy.numbers.developer.formula) friendly_name() (DFTElementType method) (RegionResult method) (RegionResultHypothesis method) (Relation method) FULL (PomdpFscApplicationMode attribute) (PomdpMemoryPattern attribute) (RefinementMode attribute) full() (BitVector method)

G

GameFormula (class in stormpy.logic) gather_derivatives() (in module stormpy.pars) gather_variables() (FactorizedPolynomial method) (FactorizedRationalFunction method) (Polynomial method) (RationalFunction method), [1] GAUSS_SEIDEL (NativeLinearEquationSolverMethod attribute) GD (FeasibilityMethod attribute) generate_policy (BeliefBasedModelCheckerOptions property) GenerateMonitorVerifier (class in stormpy.pomdp.developer) GenerateMonitorVerifierOptions (class in stormpy.pomdp.developer) GENETIC (CuddReorderingTechnique attribute) GEQ (ComparisonType attribute) (Relation attribute) Geq() (Expression static method) get() (AddIterator method) (BitVector method) (SparseBeliefState method) get_achievable_point() (PcaaWeightVectorChecker method) get_action() (ObservationBasedFiniteStateController method) get_action_distribution() (ObservationBasedFiniteStateController method) get_action_index() (Choice method) get_action_name() (ObservationBasedFiniteStateController method) (PrismProgram method) get_all_expression_variables() (PrismProgram method) get_all_variables() (Valuations method) get_as_int() (BitVector method) get_as_variable_to_expression_map() (PrismUpdate method) get_assignment() (PrismUpdate method) get_automaton() (JaniModel method) get_automaton_index() (JaniModel method) get_bit_vector_value() (SimpleValuation method) get_boolean_value() (ModelReference method) (SimpleValuation method) (Valuations method) get_boolean_values() (Valuations method) get_boolean_variable() (PrismModule method) get_bound() (SparseDtmcParameterLiftingModelChecker method) (SparseMdpParameterLiftingModelChecker method) get_bound_at_init_state() (RegionModelChecker method) (SparseDtmcParameterLiftingModelChecker method) (SparseMdpParameterLiftingModelChecker method) get_capacity() (Place method) get_choice() (Scheduler method) get_choice_as_distribution() (SchedulerChoice method) get_choice_index() (SparseMdp method) (SparsePomdp method) get_choice_info() (ChoiceOrigins method) (JaniChoiceOrigins method) (PrismChoiceOrigins method) get_choices() (ChoiceLabeling method) (DiscreteTimePrismProgramSimulator method) get_command_indices_by_action_index() (PrismModule method) get_command_set() (PrismChoiceOrigins method) get_comment() (Property method) get_constant() (JaniModel method) (PrismProgram method) get_constraint() (Formula method), [1] get_current_belief_support() (BeliefSupportTracker method) get_current_beliefs() (NondeterministicBeliefTracker method) get_current_dimension() (NondeterministicBeliefTracker method) get_current_observation() (NondeterministicBeliefTracker method) get_current_risk() (NondeterministicBeliefTracker method) get_current_row_group_count() (SparseMatrixBuilder method) get_current_state() (DiscreteTimePrismProgramSimulator method) (DiscreteTimeSparseModelSimulator method) get_current_state_as_valuation() (DiscreteTimePrismProgramSimulator method) get_current_state_labelling() (DiscreteTimePrismProgramSimulator method) get_current_state_string() (DiscreteTimePrismProgramSimulator method) get_deterministic_choice() (SchedulerChoice method) get_distance() (ShortestPathsGenerator method) get_double_value() (Valuations method) get_double_values() (Valuations method) get_edge_index_set() (JaniChoiceOrigins method) get_element() (DFT method) get_element_by_name() (DFT method) get_elements() (DftIndependentModule method) get_elements_string() (DFT method) get_exact_environment() (in module stormpy.developer) get_explicit_value_vector() (HybridQuantitativeCheckResult method) get_expression() (AtomicExpressionFormula method) (Variable method) get_failable_elements() (DFTState method) get_finite_value_vector() (ExplicitQuantitativeCheckResult method) get_graph_preserving_constraints() (ConstraintCollector method) get_group() (DftSymmetries method) get_id() (ImmediateTransition method) (Place method) (TimedTransition method) (Transition method) get_identifier() (Expression method) get_identifier_info() (ChoiceOrigins method) (JaniChoiceOrigins method) (PrismChoiceOrigins method) get_immediate_transition() (GSPN method) get_immediate_transitions() (GSPN method) get_implication_conclusion() (Formula method), [1] get_implication_premise() (Formula method), [1] get_indices() (DdMetaVariable method) get_inhibition_arc_multiplicity() (ImmediateTransition method) (TimedTransition method) (Transition method) get_inhibition_places() (ImmediateTransition method) (TimedTransition method) (Transition method) get_initial_marking() (GSPN method) get_input_arc_multiplicity() (ImmediateTransition method) (TimedTransition method) (Transition method) get_input_places() (ImmediateTransition method) (TimedTransition method) (Transition method) get_int64_value() (Valuations method) get_int64_values() (Valuations method) get_integer_bigint_value() (Valuations method) get_integer_value() (ModelReference method) (SimpleValuation method) get_integer_variable() (PrismModule method) get_ite_condition() (Formula method), [1] get_ite_first_case() (Formula method), [1] get_ite_second_case() (Formula method), [1] get_label_expression() (PrismProgram method) get_label_names() (BuilderOptions method), [1] get_labels() (Choice method) (ChoiceLabeling method) (ItemLabeling method) (StateLabeling method) get_labels_of_choice() (ChoiceLabeling method) get_labels_of_state() (SparseCtmc method) (SparseDtmc method) (SparseMA method) (SparseMdp method) (SparseModel method) (SparsePomdp method) (SparseSmg method) (StateLabeling method) get_last_column() (SparseMatrixBuilder method) get_last_rewards() (DiscreteTimePrismProgramSimulator method) (DiscreteTimeSparseModelSimulator method) get_last_row() (SparseMatrixBuilder method) get_linear_equation_solver_type() (SolverEnvironment method) get_location_index() (JaniAutomaton method) get_log_level() (in module stormpy.developer) get_lower_bound() (ExplicitQuantitativeCheckResult method) get_lower_bound_vector() (ExplicitQuantitativeCheckResult method) get_max() (ExplicitQuantitativeCheckResult method) (HybridQuantitativeCheckResult method) (QuantitativeCheckResult method) (SymbolicQuantitativeCheckResult method) get_maximal_end_components() (in module stormpy.analysis) get_memory_pattern() (SchedulerClass method) get_memoryless_scheduler_for_memory_state() (Scheduler method) get_meta_variable() (DdManager method) get_min() (ExplicitQuantitativeCheckResult method) (HybridQuantitativeCheckResult method) (QuantitativeCheckResult method) (SymbolicQuantitativeCheckResult method) get_model() (ExplicitDFTModelBuilder method) (SmtSolver method) (Z3SmtSolver method) get_model_information() (UmbModel method) get_module() (PrismProgram method) get_module_indices_by_action_index() (PrismProgram method) get_name() (GSPN method) (ImmediateTransition method) (Place method) (Property method) (TimedTransition method) (Transition method)

get_negation_subformula() (Formula method), [1] get_next_set_index() (BitVector method) get_next_unset_index() (BitVector method) get_nr_available_actions() (SparseMdp method) (SparsePomdp method) get_number_of_beliefs() (NondeterministicBeliefTracker method) get_number_of_entities() (Valuations method) get_number_of_identifiers() (ChoiceOrigins method) (JaniChoiceOrigins method) (PrismChoiceOrigins method) get_number_of_immediate_transitions() (GSPN method) get_number_of_initial_tokens() (Place method) get_number_of_places() (GSPN method) get_number_of_servers() (TimedTransition method) get_number_of_set_bits() (BitVector method) get_number_of_set_bits_before_index() (BitVector method) get_number_of_timed_transitions() (GSPN method) get_observation() (SparsePomdp method) get_observation_as_json() (DiscreteTimePrismProgramSimulator method) get_operand() (Expression method) get_optimal_weighted_sum() (PcaaWeightVectorChecker method) get_output_arc_multiplicity() (ImmediateTransition method) (TimedTransition method) (Transition method) get_output_places() (ImmediateTransition method) (TimedTransition method) (Transition method) get_over_approximation() (ExplicitParetoCurveCheckResult method) (ParetoCurveCheckResult method) get_parameter_names() (SymbolicModelDescription method) get_parameters() (DFT method) (in module stormpy.dft.developer) (SymbolicCtmc method) (SymbolicDtmc method) (SymbolicMA method) (SymbolicMdp method) (SymbolicModel method) get_partial_model() (ExplicitDFTModelBuilder method) get_partitions() (GSPN method) get_path_as_list() (ShortestPathsGenerator method) get_place() (GSPN method) get_places() (GSPN method) get_player_of_state() (SparseSmg method) get_priority() (ImmediateTransition method) (TimedTransition method) (Transition method) get_product() (MonitorVerifier method) get_rate() (TimedTransition method) get_rational_value() (ModelReference method) (SimpleValuation method) (Valuations method) get_rational_values() (Valuations method) get_raw_formula() (Property method) get_reachable_states() (in module stormpy.developer) get_representative() (DftIndependentModule method) get_reward_model() (SparseCtmc method) (SparseDtmc method) (SparseMA method) (SparseMdp method) (SparseModel method) (SparsePomdp method) (SparseSmg method) get_reward_names() (DiscreteTimePrismProgramSimulator method) (PrismSimulator method) (SparseSimulator method) get_rewards() (Choice method) get_row() (SparseMatrix method) get_row_group_end() (SparseMatrix method) get_row_group_start() (SparseMatrix method) get_rows_for_group() (SparseMatrix method) get_scheduler() (ExplicitQualitativeCheckResult method) (ExplicitQuantitativeCheckResult method) get_short_model_information() (UmbModel method) get_solution_bounds() (ExplicitQuantitativeCheckResult method) get_sound_environment() (in module stormpy.developer) get_state() (DFTTraceSimulator method) get_state_action_reward() (SparseRewardModel method) get_state_as_json() (DiscreteTimePrismProgramSimulator method) get_state_has_label() (StateLabeling method) get_state_player_indications() (SparseSmg method) get_state_reward() (SparseRewardModel method) get_states() (ExplicitQualitativeCheckResult method) (ExplicitQuantitativeCheckResult method) (ShortestPathsGenerator method) (StateLabeling method) (SymbolicCtmc method) (SymbolicDtmc method) (SymbolicMA method) (SymbolicMdp method) (SymbolicModel method) get_states_with_parameter() (SparseCtmc method) (SparseDtmc method) (SparseMA method) (SparseMdp method) (SparseModel method) (SparsePomdp method) (SparseSmg method) get_states_with_zero_reward() (SparseRewardModel method) get_string_value() (Valuations method) get_string_values() (Valuations method) get_subformulas() (Formula method), [1] get_submatrix() (SparseMatrix method) get_submodules() (DftIndependentModule method) get_subtree() (DftIndependentModule method) get_successor() (ObservationBasedFiniteStateController method) get_synchronizing_action_indices() (PrismProgram method) get_time() (DFTTraceSimulator method) get_timed_transition() (GSPN method) get_timed_transitions() (GSPN method) get_topological_sort() (in module stormpy.developer.storage) get_total_mass() (Choice method) get_transition() (GSPN method) get_truth_values_vector() (ExplicitQualitativeCheckResult method) (SymbolicQualitativeCheckResult method) get_undefined_constants() (PrismProgram method) (Property method) (SymbolicModelDescription method) get_under_approximation() (ExplicitParetoCurveCheckResult method) (ParetoCurveCheckResult method) get_upper_bound() (ExplicitQuantitativeCheckResult method) get_upper_bound_vector() (ExplicitQuantitativeCheckResult method) get_value() (ExplicitQuantitativeCheckResult method) (SimpleValuation method) (SparseMatrixEntry method) (Valuations method) get_value_vector() (ExplicitQuantitativeCheckResult method) (SymbolicQuantitativeCheckResult method) get_values_states() (Valuations method) get_variable() (ExpressionManager method) get_variable_by_expr_variable() (JaniVariableSet method) get_variable_by_name() (JaniVariableSet method) get_variables() (Expression method) (ExpressionManager method) get_vertices_in_clockwise_order() (Polytope method) get_weight() (ImmediateTransition method) get_weighted_precision() (PcaaWeightVectorChecker method) get_wellformed_constraints() (ConstraintCollector method) git_revision_hash (StormVersion attribute) GLOBAL (PrecomputationType attribute) global_boolean_variables (PrismProgram property) global_index (PrismCommand property) (PrismUpdate property) global_integer_variables (PrismProgram property) GLOBAL_NAMES (SimulatorActionMode attribute) global_variables (JaniModel property) GloballyFormula (class in stormpy.logic) GMMXX (EquationSolverType attribute) GOAL_MEMORY (SchedulerMemoryPattern attribute) GRAPH_PRESERVING (GraphPreservationStatus attribute) GraphPreservationStatus (class in stormpy.pars.developer) GREATER (ComparisonType attribute) (OperatorType attribute) (Relation attribute) Greater() (Expression static method) GREATER_OR_EQUAL (OperatorType attribute) GROUP_SIFT (CuddReorderingTechnique attribute) GROUP_SIFT_CONV (CuddReorderingTechnique attribute) GSPN (class in stormpy.gspn) GspnBuilder (class in stormpy.gspn) guard (JaniEdge property) (JaniTemplateEdge property) guard_expression (PrismCommand property) GZIP (CompressionMode attribute)

H

HA (JaniModelType attribute) Halfspace (class in stormpy.developer.storage) halfspaces (Polytope property) has_action_name() (ObservationBasedFiniteStateController method) has_any (SolutionBounds property) has_bit_vector_type() (Variable method) has_boolean_type() (Expression method) (Variable method) has_bound (LongRunAverageOperatorFormula property) (OperatorFormula property) (ProbabilityOperatorFormula property) (RewardOperatorFormula property) (TimeOperatorFormula property) has_choice_labeling() (SparseCtmc method) (SparseDtmc method) (SparseMA method) (SparseMdp method) (SparseModel method) (SparsePomdp method) (SparseSmg method) has_choice_origins() (SparseCtmc method) (SparseDtmc method) (SparseMA method) (SparseMdp method) (SparseModel method) (SparsePomdp method) (SparseSmg method) has_cln() (in module stormpy.numbers.developer) has_constant() (PrismProgram method) has_failed() (DFTState method) has_infinite_server_semantics() (TimedTransition method) has_initial_states_expression (PrismProgram property) has_integer_type() (Expression method) (Variable method) has_k_server_semantics() (TimedTransition method) has_label() (PrismProgram method) has_labels() (Choice method) has_lower (AggregatedValue property) (BoundedValue property) (SolutionBounds property) has_lower_bound (BoundedUntilFormula property) has_lower_bounds() (ExplicitQuantitativeCheckResult method) has_model() (SymbolicModelDescription method) has_module_with_inner_action_overlap() (OverlappingGuardAnalyser method) has_numerical_type() (Variable method) has_observation_valuations() (SparsePomdp method) has_optimality_type (LongRunAverageOperatorFormula property) (OperatorFormula property) (ProbabilityOperatorFormula property) (RewardOperatorFormula property) (TimeOperatorFormula property) has_output() (ObservationBasedFiniteStateController method) has_parameters (ModelBase property) (SparseCtmc property) (SparseDtmc property) (SparseMA property) (SparseMdp property) (SparseModel property) (SparsePomdp property) (SparseSmg property) (SymbolicCtmc property) (SymbolicDtmc property) (SymbolicMA property) (SymbolicMdp property) (SymbolicModel property)

has_potential_modeling_issues() (in module stormpy.dft.developer) has_rational_type() (Expression method) (Variable method) has_restricted_capacity() (Place method) has_reward_model() (PrismProgram method) (SparseCtmc method) (SparseDtmc method) (SparseMA method) (SparseMdp method) (SparseModel method) (SparsePomdp method) (SparseSmg method) has_reward_model_name() (RewardOperatorFormula method) has_scheduler() (CheckResult method) (ExplicitParetoCurveCheckResult method) (ExplicitQualitativeCheckResult method) (ExplicitQuantitativeCheckResult method) (HybridQuantitativeCheckResult method) (ParetoCurveCheckResult method) (QualitativeCheckResult method) (QuantitativeCheckResult method) (SymbolicQualitativeCheckResult method) (SymbolicQuantitativeCheckResult method) has_silent_action() (JaniEdge method) has_single_server_semantics() (TimedTransition method) has_standard_composition() (JaniModel method) has_state_action_rewards (SparseRewardModel property) (SymbolicRewardModel property) has_state_rewards (SparseRewardModel property) (SymbolicRewardModel property) has_state_valuations() (SparseCtmc method) (SparseDtmc method) (SparseMA method) (SparseMdp method) (SparseModel method) (SparsePomdp method) (SparseSmg method) has_string_type() (Variable method) has_timed_out() (NondeterministicBeliefTracker method) has_transition_rewards (SparseRewardModel property) (SymbolicRewardModel property) has_trivial_row_grouping (SparseMatrix property) has_undefined_constants (JaniModel property) (PrismProgram property) has_undefined_constants() (SymbolicModelDescription method) has_unique_set_bit() (BitVector method) has_upper (AggregatedValue property) (BoundedValue property) (SolutionBounds property) has_upper_bounds() (ExplicitQuantitativeCheckResult method) has_value_for_state() (ExplicitQualitativeCheckResult method) (ExplicitQuantitativeCheckResult method) has_variable() (ExpressionManager method) has_zeno_cycle (SparseMA property) horizon_label (GenerateMonitorVerifierOptions property) HYBRID (Engine attribute) HybridQuantitativeCheckResult (class in stormpy.results)

I

I_MINUS_P (MatrixFormat attribute) id (DFTBE property) (DFTDependency property) (DFTElement property) (SparseModelAction property) (SparseModelState property) (Variable property) IFF (FormulaType attribute) (OperatorType attribute) Iff() (Expression static method) immediate_transition_id_to_transition_id() (GSPN static method) ImmediateTransition (class in stormpy.gspn) IMPLIES (FormulaType attribute) (OperatorType attribute) Implies() (Expression static method) import_umb() (in module stormpy.developer.storage) (in module stormpy.io) increment() (BitVector method) index (Variable property) INDEX_LEVEL (SimulatorActionMode attribute) INFO (LogLevel attribute) INFTY (BoundType attribute) init_expression (JaniVariable property) initial_location_indices (JaniAutomaton property) initial_node (ObservationBasedFiniteStateController property) initial_partition_mode (DdBisimulationOptions property) initial_states (SparseCtmc property) (SparseDtmc property) (SparseMA property) (SparseMdp property) (SparseModel property) (SparsePomdp property) (SparseSmg property) (SymbolicCtmc property) (SymbolicDtmc property) (SymbolicMA property) (SymbolicMdp property) (SymbolicModel property) initial_states_as_bitvector (SparseCtmc property) (SparseDtmc property) (SparseMA property) (SparseMdp property) (SparseModel property) (SparsePomdp property) (SparseSmg property) initial_states_expression (PrismProgram property) initial_states_restriction (JaniAutomaton property) (JaniModel property) initial_value_expression (PrismBooleanVariable property) (PrismIntegerVariable property) (PrismVariable property) initialize_region_model_checker() (in module stormpy.pars.developer) initialize_region_refinement_checker() (in module stormpy.pars.developer) InitialPartitionMode (class in stormpy.developer) inner_type (BasicType property) insert() (FlatSet method) insert_set() (FlatSet method) install_signal_handler() (in module stormpy.developer) InstantaneousRewardFormula (class in stormpy.logic) instantiate() (DftInstantiator method) (ModelInstantiator method) instantiate_constants() (in module stormpy) (in module stormpy.io) INT (DdMetaVariableType attribute) (VariableType attribute) Integer (class in stormpy.numbers) (class in stormpy.numbers.developer.cln) integer() (ExpressionManager method) integer_variables (PrismModule property) integralPart() (Interval method), [1] intersect() (Interval method), [1] intersectsWith() (Interval method), [1] Interval (class in stormpy) (class in stormpy.numbers) (class in stormpy.numbers.developer.cln) INTERVAL_ITERATION (MinMaxMethod attribute) (NativeLinearEquationSolverMethod attribute) INVALID (SimulationStepResult attribute) (SimulationTraceResult attribute) inverse() (Interval method), [1] is_array_type (ArrayType property) (BasicType property) (BoundedType property) (ClockType property) (ContinuousType property) (JaniType property) is_basic_type (ArrayType property) (BasicType property) (BoundedType property) (ClockType property) (ContinuousType property) (JaniType property) is_boolean (ExpressionType property) is_bounded_type (ArrayType property) (BasicType property) (BoundedType property) (ClockType property) (ContinuousType property) (JaniType property) is_bounded_until_formula (AtomicExpressionFormula property) (AtomicLabelFormula property) (BinaryBooleanStateFormula property) (BinaryPathFormula property) (BinaryStateFormula property) (BooleanLiteralFormula property) (BoundedUntilFormula property) (ConditionalFormula property) (CumulativeRewardFormula property) (DiscountedCumulativeRewardFormula property) (DiscountedTotalRewardFormula property) (EventuallyFormula property) (Formula property) (GameFormula property) (GloballyFormula property) (InstantaneousRewardFormula property) (LongRunAverageOperatorFormula property) (LongRunAverageRewardFormula property) (MultiObjectiveFormula property) (OperatorFormula property) (PathFormula property) (ProbabilityOperatorFormula property) (RewardOperatorFormula property) (StateFormula property) (TimeOperatorFormula property) (UnaryBooleanStateFormula property) (UnaryPathFormula property) (UnaryStateFormula property) (UntilFormula property) is_build_all_labels_set() (BuilderOptions method), [1] is_build_all_reward_models_set() (BuilderOptions method), [1] is_build_choice_labels_set() (BuilderOptions method), [1] is_build_choice_origins_set() (BuilderOptions method), [1] is_build_observation_valuations_set() (BuilderOptions method), [1] is_build_state_valuations_set() (BuilderOptions method), [1] is_clock_type (ArrayType property) (BasicType property) (BoundedType property) (ClockType property) (ContinuousType property) (JaniType property) is_closed (SparseMA property) is_constant() (FactorizedPolynomial method) (FactorizedRationalFunction method) (Polynomial method) (RationalFunction method), [1] (Term method), [1] is_continuous_type (ArrayType property) (BasicType property) (BoundedType property) (ClockType property) (ContinuousType property) (JaniType property) is_deterministic (SchedulerClass property) is_deterministic() (ObservationBasedFiniteStateController method) is_deterministic_model (PrismProgram property) is_discounted_cumulative_reward_formula (AtomicExpressionFormula property) (AtomicLabelFormula property) (BinaryBooleanStateFormula property) (BinaryPathFormula property) (BinaryStateFormula property) (BooleanLiteralFormula property) (BoundedUntilFormula property) (ConditionalFormula property) (CumulativeRewardFormula property) (DiscountedCumulativeRewardFormula property) (DiscountedTotalRewardFormula property) (EventuallyFormula property) (Formula property) (GameFormula property) (GloballyFormula property) (InstantaneousRewardFormula property) (LongRunAverageOperatorFormula property) (LongRunAverageRewardFormula property) (MultiObjectiveFormula property) (OperatorFormula property) (PathFormula property) (ProbabilityOperatorFormula property) (RewardOperatorFormula property) (StateFormula property) (TimeOperatorFormula property) (UnaryBooleanStateFormula property) (UnaryPathFormula property) (UnaryStateFormula property) (UntilFormula property) is_discounted_total_reward_formula (AtomicExpressionFormula property) (AtomicLabelFormula property) (BinaryBooleanStateFormula property) (BinaryPathFormula property) (BinaryStateFormula property) (BooleanLiteralFormula property) (BoundedUntilFormula property) (ConditionalFormula property) (CumulativeRewardFormula property) (DiscountedCumulativeRewardFormula property) (DiscountedTotalRewardFormula property) (EventuallyFormula property) (Formula property) (GameFormula property) (GloballyFormula property) (InstantaneousRewardFormula property) (LongRunAverageOperatorFormula property) (LongRunAverageRewardFormula property) (MultiObjectiveFormula property) (OperatorFormula property) (PathFormula property) (ProbabilityOperatorFormula property) (RewardOperatorFormula property) (StateFormula property) (TimeOperatorFormula property) (UnaryBooleanStateFormula property) (UnaryPathFormula property) (UnaryStateFormula property) (UntilFormula property) is_discrete_time_model (ModelBase property) (SparseCtmc property) (SparseDtmc property) (SparseMA property) (SparseMdp property) (SparseModel property) (SparsePomdp property) (SparseSmg property) (SymbolicCtmc property) (SymbolicDtmc property) (SymbolicMA property) (SymbolicMdp property) (SymbolicModel property) is_disjoint_from() (BitVector method) is_done() (DFTSimulator method) (PrismSimulator method) (Simulator method) (SparseSimulator method) is_due_dependency() (FailableElement method) is_empty() (Polytope method) is_enabled() (ImmediateTransition method) (TimedTransition method) (Transition method) is_eventually_formula (AtomicExpressionFormula property) (AtomicLabelFormula property) (BinaryBooleanStateFormula property) (BinaryPathFormula property) (BinaryStateFormula property) (BooleanLiteralFormula property) (BoundedUntilFormula property) (ConditionalFormula property) (CumulativeRewardFormula property) (DiscountedCumulativeRewardFormula property) (DiscountedTotalRewardFormula property) (EventuallyFormula property) (Formula property) (GameFormula property) (GloballyFormula property) (InstantaneousRewardFormula property) (LongRunAverageOperatorFormula property) (LongRunAverageRewardFormula property) (MultiObjectiveFormula property) (OperatorFormula property) (PathFormula property) (ProbabilityOperatorFormula property) (RewardOperatorFormula property) (StateFormula property) (TimeOperatorFormula property) (UnaryBooleanStateFormula property) (UnaryPathFormula property) (UnaryStateFormula property) (UntilFormula property) is_exact (ModelBase property) (SolutionBounds property) (SparseCtmc property) (SparseDtmc property) (SparseMA property) (SparseMdp property) (SparseModel property) (SparsePomdp property) (SparseSmg property) (SymbolicCtmc property) (SymbolicDtmc property) (SymbolicMA property) (SymbolicMdp property) (SymbolicModel property) is_explicit() (CheckResult method) (ExplicitParetoCurveCheckResult method) (ExplicitQualitativeCheckResult method) (ExplicitQuantitativeCheckResult method) (HybridQuantitativeCheckResult method) (ParetoCurveCheckResult method) (QualitativeCheckResult method) (QuantitativeCheckResult method) (SymbolicQualitativeCheckResult method) (SymbolicQuantitativeCheckResult method) is_explicit_pareto_curve_check_result() (CheckResult method) (ExplicitParetoCurveCheckResult method) (ExplicitQualitativeCheckResult method) (ExplicitQuantitativeCheckResult method) (HybridQuantitativeCheckResult method) (ParetoCurveCheckResult method) (QualitativeCheckResult method) (QuantitativeCheckResult method) (SymbolicQualitativeCheckResult method) (SymbolicQuantitativeCheckResult method) is_explicit_qualitative_check_result() (CheckResult method) (ExplicitParetoCurveCheckResult method) (ExplicitQualitativeCheckResult method) (ExplicitQuantitativeCheckResult method) (HybridQuantitativeCheckResult method) (ParetoCurveCheckResult method) (QualitativeCheckResult method) (QuantitativeCheckResult method) (SymbolicQualitativeCheckResult method) (SymbolicQuantitativeCheckResult method) is_explicit_quantitative_check_result() (CheckResult method) (ExplicitParetoCurveCheckResult method) (ExplicitQualitativeCheckResult method) (ExplicitQuantitativeCheckResult method) (HybridQuantitativeCheckResult method) (ParetoCurveCheckResult method) (QualitativeCheckResult method) (QuantitativeCheckResult method) (SymbolicQualitativeCheckResult method) (SymbolicQuantitativeCheckResult method) is_export_plot_set() (MultiObjectiveModelCheckerEnvironment method) is_failed() (DFTSimulator method) is_failsafe() (DFTState method) is_fdep (DFTDependency property) is_fully_static (DftIndependentModule property) is_fully_static() (DftIndependentModule method) is_function_application (Expression property) is_game_formula (GameFormula property) is_hybrid() (CheckResult method) (ExplicitParetoCurveCheckResult method) (ExplicitQualitativeCheckResult method) (ExplicitQuantitativeCheckResult method) (HybridQuantitativeCheckResult method) (ParetoCurveCheckResult method) (QualitativeCheckResult method) (QuantitativeCheckResult method) (SymbolicQualitativeCheckResult method) (SymbolicQuantitativeCheckResult method)

is_hybrid_quantitative_check_result() (CheckResult method) (ExplicitParetoCurveCheckResult method) (ExplicitQualitativeCheckResult method) (ExplicitQuantitativeCheckResult method) (HybridQuantitativeCheckResult method) (ParetoCurveCheckResult method) (QualitativeCheckResult method) (QuantitativeCheckResult method) (SymbolicQualitativeCheckResult method) (SymbolicQuantitativeCheckResult method) is_in_winning_region() (WinningRegionQueryInterface method) is_infinity() (in module stormpy.numbers) is_integer (ExpressionType property) is_invalid() (DFTState method) is_jani_choice_origins() (ChoiceOrigins method) (JaniChoiceOrigins method) (PrismChoiceOrigins method) is_jani_model() (SymbolicModelDescription method) is_labeled (PrismCommand property) is_literal() (Expression method) is_markovian() (Choice method) is_memory_bounded() (SchedulerClass method) is_multi_dimensional (BoundedUntilFormula property) is_multi_objective_formula (AtomicExpressionFormula property) (AtomicLabelFormula property) (BinaryBooleanStateFormula property) (BinaryPathFormula property) (BinaryStateFormula property) (BooleanLiteralFormula property) (BoundedUntilFormula property) (ConditionalFormula property) (CumulativeRewardFormula property) (DiscountedCumulativeRewardFormula property) (DiscountedTotalRewardFormula property) (EventuallyFormula property) (Formula property) (GameFormula property) (GloballyFormula property) (InstantaneousRewardFormula property) (LongRunAverageOperatorFormula property) (LongRunAverageRewardFormula property) (MultiObjectiveFormula property) (OperatorFormula property) (PathFormula property) (ProbabilityOperatorFormula property) (RewardOperatorFormula property) (StateFormula property) (TimeOperatorFormula property) (UnaryBooleanStateFormula property) (UnaryPathFormula property) (UnaryStateFormula property) (UntilFormula property) is_negative_infinity() (in module stormpy.numbers) is_next_dependency_failure() (DFTSimulator method) is_no_variable (Variable property) is_nondeterministic_model (ModelBase property) (SparseCtmc property) (SparseDtmc property) (SparseMA property) (SparseMdp property) (SparseModel property) (SparsePomdp property) (SparseSmg property) (SymbolicCtmc property) (SymbolicDtmc property) (SymbolicMA property) (SymbolicMdp property) (SymbolicModel property) is_one() (FactorizedPolynomial method) (Term method), [1] is_only_initial_states_relevant_set() (CheckTask method) is_operational() (DFTState method) is_pareto_curve_check_result() (CheckResult method) (ExplicitParetoCurveCheckResult method) (ExplicitQualitativeCheckResult method) (ExplicitQuantitativeCheckResult method) (HybridQuantitativeCheckResult method) (ParetoCurveCheckResult method) (QualitativeCheckResult method) (QuantitativeCheckResult method) (SymbolicQualitativeCheckResult method) (SymbolicQuantitativeCheckResult method) is_partially_observable (ModelBase property) (SparseCtmc property) (SparseDtmc property) (SparseMA property) (SparseMdp property) (SparseModel property) (SparsePomdp property) (SparseSmg property) (SymbolicCtmc property) (SymbolicDtmc property) (SymbolicMA property) (SymbolicMdp property) (SymbolicModel property) is_positional() (SchedulerClass method) is_prism_choice_origins() (ChoiceOrigins method) (JaniChoiceOrigins method) (PrismChoiceOrigins method) is_prism_program() (SymbolicModelDescription method) is_probability_operator_formula (AtomicExpressionFormula property) (AtomicLabelFormula property) (BinaryBooleanStateFormula property) (BinaryPathFormula property) (BinaryStateFormula property) (BooleanLiteralFormula property) (BoundedUntilFormula property) (ConditionalFormula property) (CumulativeRewardFormula property) (DiscountedCumulativeRewardFormula property) (DiscountedTotalRewardFormula property) (EventuallyFormula property) (Formula property) (GameFormula property) (GloballyFormula property) (InstantaneousRewardFormula property) (LongRunAverageOperatorFormula property) (LongRunAverageRewardFormula property) (MultiObjectiveFormula property) (OperatorFormula property) (PathFormula property) (ProbabilityOperatorFormula property) (RewardOperatorFormula property) (StateFormula property) (TimeOperatorFormula property) (UnaryBooleanStateFormula property) (UnaryPathFormula property) (UnaryStateFormula property) (UntilFormula property) is_produce_schedulers_set() (CheckTask method) is_qualitative() (CheckResult method) (ExplicitParetoCurveCheckResult method) (ExplicitQualitativeCheckResult method) (ExplicitQuantitativeCheckResult method) (HybridQuantitativeCheckResult method) (ParetoCurveCheckResult method) (QualitativeCheckResult method) (QuantitativeCheckResult method) (SymbolicQualitativeCheckResult method) (SymbolicQuantitativeCheckResult method) is_quantitative() (CheckResult method) (ExplicitParetoCurveCheckResult method) (ExplicitQualitativeCheckResult method) (ExplicitQuantitativeCheckResult method) (HybridQuantitativeCheckResult method) (ParetoCurveCheckResult method) (QualitativeCheckResult method) (QuantitativeCheckResult method) (SymbolicQualitativeCheckResult method) (SymbolicQuantitativeCheckResult method) is_randomised() (ObservationBasedFiniteStateController method) is_rational (ExpressionType property) is_relevant() (RelevantEvents method) is_restart_semantics_set() (ObservationTraceUnfolder method) is_result_for_all_states() (CheckResult method) (ExplicitParetoCurveCheckResult method) (ExplicitQualitativeCheckResult method) (ExplicitQuantitativeCheckResult method) (HybridQuantitativeCheckResult method) (ParetoCurveCheckResult method) (QualitativeCheckResult method) (QuantitativeCheckResult method) (SymbolicQualitativeCheckResult method) (SymbolicQuantitativeCheckResult method) is_reward_operator_formula (AtomicExpressionFormula property) (AtomicLabelFormula property) (BinaryBooleanStateFormula property) (BinaryPathFormula property) (BinaryStateFormula property) (BooleanLiteralFormula property) (BoundedUntilFormula property) (ConditionalFormula property) (CumulativeRewardFormula property) (DiscountedCumulativeRewardFormula property) (DiscountedTotalRewardFormula property) (EventuallyFormula property) (Formula property) (GameFormula property) (GloballyFormula property) (InstantaneousRewardFormula property) (LongRunAverageOperatorFormula property) (LongRunAverageRewardFormula property) (MultiObjectiveFormula property) (OperatorFormula property) (PathFormula property) (ProbabilityOperatorFormula property) (RewardOperatorFormula property) (StateFormula property) (TimeOperatorFormula property) (UnaryBooleanStateFormula property) (UnaryPathFormula property) (UnaryStateFormula property) (UntilFormula property) is_single_be (DftIndependentModule property) is_single_be() (DftIndependentModule method) is_sink_state() (DiscreteTimePrismProgramSimulator method) (SparseCtmc method) (SparseDtmc method) (SparseMA method) (SparseMdp method) (SparseModel method) (SparsePomdp method) (SparseSmg method) is_sparse_model (ModelBase property) (SparseCtmc property) (SparseDtmc property) (SparseMA property) (SparseMdp property) (SparseModel property) (SparsePomdp property) (SparseSmg property) (SymbolicCtmc property) (SymbolicDtmc property) (SymbolicMA property) (SymbolicMdp property) (SymbolicModel property) is_static (DftIndependentModule property) is_static() (DftIndependentModule method) is_string (ExpressionType property) is_subset_of() (BitVector method) (FlatSet method) is_symbolic() (CheckResult method) (ExplicitParetoCurveCheckResult method) (ExplicitQualitativeCheckResult method) (ExplicitQuantitativeCheckResult method) (HybridQuantitativeCheckResult method) (ParetoCurveCheckResult method) (QualitativeCheckResult method) (QuantitativeCheckResult method) (SymbolicQualitativeCheckResult method) (SymbolicQuantitativeCheckResult method) is_symbolic_model (ModelBase property) (SparseCtmc property) (SparseDtmc property) (SparseMA property) (SparseMdp property) (SparseModel property) (SparsePomdp property) (SparseSmg property) (SymbolicCtmc property) (SymbolicDtmc property) (SymbolicMA property) (SymbolicMdp property) (SymbolicModel property) is_symbolic_qualitative_check_result() (CheckResult method) (ExplicitParetoCurveCheckResult method) (ExplicitQualitativeCheckResult method) (ExplicitQuantitativeCheckResult method) (HybridQuantitativeCheckResult method) (ParetoCurveCheckResult method) (QualitativeCheckResult method) (QuantitativeCheckResult method) (SymbolicQualitativeCheckResult method) (SymbolicQuantitativeCheckResult method) is_symbolic_quantitative_check_result() (CheckResult method) (ExplicitParetoCurveCheckResult method) (ExplicitQualitativeCheckResult method) (ExplicitQuantitativeCheckResult method) (HybridQuantitativeCheckResult method) (ParetoCurveCheckResult method) (QualitativeCheckResult method) (QuantitativeCheckResult method) (SymbolicQualitativeCheckResult method) (SymbolicQuantitativeCheckResult method) is_transient (JaniVariable property) is_universal() (Polytope method) is_until_formula (AtomicExpressionFormula property) (AtomicLabelFormula property) (BinaryBooleanStateFormula property) (BinaryPathFormula property) (BinaryStateFormula property) (BooleanLiteralFormula property) (BoundedUntilFormula property) (ConditionalFormula property) (CumulativeRewardFormula property) (DiscountedCumulativeRewardFormula property) (DiscountedTotalRewardFormula property) (EventuallyFormula property) (Formula property) (GameFormula property) (GloballyFormula property) (InstantaneousRewardFormula property) (LongRunAverageOperatorFormula property) (LongRunAverageRewardFormula property) (MultiObjectiveFormula property) (OperatorFormula property) (PathFormula property) (ProbabilityOperatorFormula property) (RewardOperatorFormula property) (StateFormula property) (TimeOperatorFormula property) (UnaryBooleanStateFormula property) (UnaryPathFormula property) (UnaryStateFormula property) (UntilFormula property) is_valid (SparseBeliefState property) is_valid() (GSPN method) is_variable() (Expression method) is_well_formed() (in module stormpy.dft.developer) is_within_precision() (SolutionBounds method) isClosedInterval() (Interval method), [1] isEmpty() (Interval method), [1] isHalfBounded() (Interval method), [1] isInfinite() (Interval method), [1] isInteger() (in module stormpy.numbers.developer) (in module stormpy.numbers.developer.cln) (in module stormpy.numbers.developer.gmp) isNegative() (Interval method), [1] isOne() (Interval method), [1] isOpenInterval() (Interval method), [1] isPointInterval() (Interval method), [1] isPositive() (Interval method), [1] isProperSubset() (Interval method), [1] isSemiNegative() (Interval method), [1] isSemiPositive() (Interval method), [1] isSubset() (Interval method), [1] isUnbounded() (Interval method), [1] isZero() (Interval method), [1] ITE (FormulaType attribute) (OperatorType attribute) ItemLabeling (class in stormpy.developer.storage) iterations (SMTMinimalLabelSetGeneratorStats property) IterativePolicySearch (class in stormpy.pomdp)

J

JACOBI (NativeLinearEquationSolverMethod attribute) JaniAssignment (class in stormpy.io) JaniAutomaton (class in stormpy.io) JaniChoiceOrigins (class in stormpy.models) JaniConstant (class in stormpy.io) JaniEdge (class in stormpy.io) JaniEdgeDestination (class in stormpy.io) JaniInformationObject (class in stormpy.developer.storage) JaniLocation (class in stormpy.io) JaniLocationExpander (class in stormpy.developer.storage)

JaniModel (class in stormpy.io) JaniModelType (class in stormpy.io) JaniOrderedAssignments (class in stormpy.io) JaniScopeChanger (class in stormpy.developer.storage) JaniTemplateEdge (class in stormpy.io) JaniTemplateEdgeDestination (class in stormpy.io) JaniType (class in stormpy.io) JaniVariable (class in stormpy.io) JaniVariableSet (class in stormpy.io) JsonContainer (class in stormpy.datastructures) JsonExporter (class in stormpy.developer.storage)

K

KEEP_LABELS (EliminationLabelBehavior attribute)

kept_actions (SubsystemBuilderReturnType property)

L

label (AtomicLabelFormula property) label_behavior (TransformationEnvironment property) label_unlabelled_commands() (PrismProgram method) labeled (PrismCommand property) labeling (SparseCtmc property) (SparseDtmc property) (SparseMA property) (SparseMdp property) (SparseModel property) (SparsePomdp property) (SparseSmg property) labels (PrismProgram property) (SparseModelAction property) (SparseModelState property) last_winning_region (IterativePolicySearch property) LayoutInfo (class in stormpy.gspn) LAZY (SignatureMode attribute) left_subformula (BinaryPathFormula property) (BoundedUntilFormula property) (UntilFormula property) LEQ (ComparisonType attribute) (Relation attribute) Leq() (Expression static method) LESS (ComparisonType attribute) (OperatorType attribute) (Relation attribute) Less() (Expression static method) LESS_OR_EQUAL (OperatorType attribute) let_fail() (DFTSimulator method)

lhs (Constraint property), [1] lhs() (SimpleConstraint method), [1] (SimpleConstraintRatFunc method), [1] LIFO (ExplorationQueueOrder attribute) LINEAR_PROGRAMMING (MinMaxMethod attribute) load_dft_galileo_file() (in module stormpy.dft) (in module stormpy.dft.developer) load_dft_json_file() (in module stormpy.dft) (in module stormpy.dft.developer) load_dft_json_string() (in module stormpy.dft) load_from_file() (WinningRegion static method) load_from_string() (BitVector static method) load_gspn_file() (in module stormpy.gspn) LOCAL (PrecomputationType attribute) location_variable (JaniAutomaton property) locations (JaniAutomaton property) LogLevel (class in stormpy.developer) long_version_string() (StormVersion static method) LongRunAverageOperatorFormula (class in stormpy.logic) LongRunAverageRewardFormula (class in stormpy.logic) lookup() (ExplicitStateLookup method) lower (AggregatedValue property) (BoundedValue property) (SolutionBounds property) lower() (Interval method), [1] lower_bound (BoundedType property) lower_bound_expression (PrismIntegerVariable property) lowest_value (DdMetaVariable property) ltl2da_tool (ModelCheckerEnvironment property) LTS (JaniModelType attribute)

M

MA (JaniModelType attribute) (ModelType attribute) (PrismModelType attribute) main_subformula (ConditionalFormula property) make_canonic() (in module stormpy.pomdp) make_explicit_model_builder() (in module stormpy.developer) make_row_grouping_trivial (SubsystemBuilderOptions property) make_row_grouping_trivial() (SparseMatrix method) make_simple() (in module stormpy.pomdp) make_standard_jani_compliant() (JaniModel method) make_variables_local() (JaniScopeChanger method) MakePOMDPCanonic (class in stormpy.pomdp.developer) manager (Expression property) (Valuations property) (Variable property) markovian_states (SparseMA property) (SparseModelComponents property) matrix (EndComponentEliminatorReturnType property) MatrixFormat (class in stormpy.developer.utility) MAX (FilterType attribute) (OperatorType attribute) max_depth (ModelBuilderEnvironment property) max_exploration_size (BeliefBasedModelCheckerOptions property) max_exploration_time (BeliefBasedModelCheckerOptions property) max_steps (MultiObjectiveModelCheckerEnvironment property) maximal_memory (CuddDdManagerEnvironment property) (SylvanDdManagerEnvironment property) maximal_number_of_iterations (MinMaxSolverEnvironment property) (NativeSolverEnvironment property) MaximalEndComponent (class in stormpy.analysis) MaximalEndComponentDecomposition (class in stormpy.analysis) MAXIMIZE (OptimizationDirection attribute) (UncertaintyResolutionMode attribute) maximum_counterexamples (SMTMinimalLabelSetGeneratorOptions property) maximum_extra_iterations (SMTMinimalLabelSetGeneratorOptions property) MDP (JaniModelType attribute) (ModelType attribute) (PrismModelType attribute) meets() (Interval method), [1] MemlessSearchOptions (class in stormpy.pomdp.developer) memory_size (Scheduler property) memory_states (SchedulerClass property) memoryless (Scheduler property) MemoryStructure (class in stormpy.models) MemoryStructureBuilder (class in stormpy.models) MemoryStructureProduct (class in stormpy.developer.storage) MERGE_LABELS (EliminationLabelBehavior attribute) meta_variables (Add property) (Bdd property) (Dd property) method (MinMaxSolverEnvironment property) (MultiObjectiveModelCheckerEnvironment property) (NativeSolverEnvironment property) milliseconds (class in stormpy.developer.utility) MIN (FilterType attribute) (OperatorType attribute) min_max() (SolverEnvironment method) MINIMIZE (OptimizationDirection attribute) (UncertaintyResolutionMode attribute) MinMaxMethod (class in stormpy.environments) MinMaxSolverEnvironment (class in stormpy.environments) MINUS (OperatorType attribute) Minus() (Expression static method) model (JaniChoiceOrigins property) (SubsystemBuilderReturnType property) model_builder_environment (DftEnvironment property) model_checking() (in module stormpy) model_checking_time (SMTMinimalLabelSetGeneratorStats property) model_tolerance (Environment property) model_type (JaniInformationObject property) (JaniModel property) (ModelBase property) (PrismProgram property) (SparseCtmc property) (SparseDtmc property) (SparseMA property) (SparseMdp property) (SparseModel property) (SparsePomdp property) (SparseSmg property) (SymbolicCtmc property) (SymbolicDtmc property) (SymbolicMA property) (SymbolicMdp property) (SymbolicModel property)

ModelBase (class in stormpy.developer.storage) ModelBuilderEnvironment (class in stormpy.dft) modelchecker() (Environment method) ModelCheckerEnvironment (class in stormpy.environments) ModelCheckerHint (class in stormpy) ModelInstantiator (class in stormpy.pars) ModelReference (class in stormpy.developer) ModelType (class in stormpy.models) module stormpy stormpy.analysis stormpy.datastructures stormpy.developer stormpy.developer.info stormpy.developer.logic stormpy.developer.storage stormpy.developer.utility stormpy.dft stormpy.dft.developer stormpy.environments stormpy.exceptions stormpy.expressions stormpy.gspn stormpy.info stormpy.io stormpy.logic stormpy.models stormpy.numbers stormpy.numbers.developer stormpy.numbers.developer.cln stormpy.numbers.developer.cln.formula stormpy.numbers.developer.convert stormpy.numbers.developer.formula stormpy.numbers.developer.gmp stormpy.numbers.developer.gmp.formula stormpy.numbers.developer.parse stormpy.pars stormpy.pars.developer stormpy.plotting stormpy.pomdp stormpy.pomdp.developer stormpy.results stormpy.simulator stormpy.transformations modules (PrismProgram property) modules() (DFT method) (in module stormpy.dft) modules_json() (in module stormpy.dft) MODULO (OperatorType attribute) Modulo() (Expression static method) MonitorVerifier (class in stormpy.pomdp) Monomial (class in stormpy.numbers.developer) monomial (Term property), [1] mttf_algorithm (AnalysisEnvironment property) mttf_precision (AnalysisEnvironment property) mttf_stepsize (AnalysisEnvironment property) multi() (ModelCheckerEnvironment method) MultiObjectiveEncodingType (class in stormpy.environments) MultiObjectiveFormula (class in stormpy.logic) MultiObjectiveMethod (class in stormpy.environments) MultiObjectiveModelCheckerEnvironment (class in stormpy.environments) MultiObjectivePrecisionType (class in stormpy.environments) Multiply() (Expression static method) MUTEX (DFTElementType attribute)

N

name (DdMetaVariable property) (DFTBE property) (DFTDependency property) (DFTElement property) (JaniAutomaton property) (JaniConstant property) (JaniLocation property) (JaniModel property) (JaniVariable property) (PrismBooleanVariable property) (PrismConstant property) (PrismIntegerVariable property) (PrismLabel property) (PrismModule property) (PrismRewardModel property) (PrismVariable property) (Variable property), [1] NATIVE (EquationSolverType attribute) native() (SolverEnvironment method) NativeLinearEquationSolverMethod (class in stormpy.environments) NativeSolverEnvironment (class in stormpy.environments) NEQ (Relation attribute) Neq() (Expression static method) new_row_group() (SparseMatrixBuilder method) new_to_old_action_index_mapping (SubsystemBuilderReturnType property) new_to_old_row_mapping (EndComponentEliminatorReturnType property) new_to_old_state_index_mapping (SubsystemBuilderReturnType property) next_failures() (DFTSimulator method) next_state_heuristic (ExplorationEnvironment property) NextStateHeuristic (class in stormpy.environments) NO_COMPRESSION (CompressionMode attribute) no_weight_attached() (ImmediateTransition method) node_count (Add property) (Bdd property) (Dd property) nominator (Rational property) (RationalFunction property), [1] nondeterministic_choice_indices (SparseMA property) (SparseMdp property) (SparsePomdp property) NondeterministicBeliefTracker (class in stormpy.pomdp) NondeterministicBeliefTrackerOptions (class in stormpy.pomdp.developer) NONE (CuddReorderingTechnique attribute) (GraphPreservationStatus attribute) (ReuseMode attribute) (StateLabelPreservation attribute) NoPicklingSupport (class in stormpy.numbers.developer) normal_vector (Halfspace property) NOT (FormulaType attribute) (OperatorType attribute) NOT_EQUAL (OperatorType attribute) nr_automata (JaniInformationObject property) nr_available_actions() (PrismSimulator method) (Simulator method) (SparseSimulator method) nr_basic_elements() (DFT method) nr_choices (ModelBase property) (SparseCtmc property) (SparseDtmc property) (SparseMA property) (SparseMdp property) (SparseModel property) (SparsePomdp property) (SparseSmg property) (SymbolicCtmc property) (SymbolicDtmc property) (SymbolicMA property) (SymbolicMdp property) (SymbolicModel property)

nr_columns (SparseMatrix property) nr_destinations (JaniEdge property) nr_dynamic_elements() (DFT method) nr_edges (JaniInformationObject property) nr_elements() (DFT method) nr_entries (SparseMatrix property) nr_modules (PrismProgram property) nr_next_failures() (DFTSimulator method) nr_observations (SparsePomdp property) nr_rows (SparseMatrix property) nr_states (MemoryStructure property) (ModelBase property) (PomdpMemory property) (SparseCtmc property) (SparseDtmc property) (SparseMA property) (SparseMdp property) (SparseModel property) (SparsePomdp property) (SparseSmg property) (SymbolicCtmc property) (SymbolicDtmc property) (SymbolicMA property) (SymbolicMdp property) (SymbolicModel property) nr_subformulas (MultiObjectiveFormula property) nr_terms (Polynomial property) nr_transitions (ModelBase property) (SparseCtmc property) (SparseDtmc property) (SparseMA property) (SparseMdp property) (SparseModel property) (SparsePomdp property) (SparseSmg property) (SymbolicCtmc property) (SymbolicDtmc property) (SymbolicMA property) (SymbolicMdp property) (SymbolicModel property) nr_transitions() (TransitionPartition method) nr_variables (JaniInformationObject property) number_of_threads (SylvanDdManagerEnvironment property) number_of_unlabeled_commands (PrismProgram property) numerator (FactorizedRationalFunction property) (Rational property) (RationalFunction property), [1] numerator() (in module stormpy.numbers.developer.cln) (in module stormpy.numbers.developer.gmp)

O

observability_classes (SparseModelComponents property) observation_default_action (MonitorVerifier property) observation_map (MonitorVerifier property) observation_valuations (SparseModelComponents property) (SparsePomdp property) ObservationBasedFiniteStateController (class in stormpy.pomdp) observations (SparsePomdp property) ObservationTraceUnfolder (class in stormpy.pomdp) ObservationTraceUnfolderOptions (class in stormpy.pomdp.developer) obtain_region_split_estimates() (RegionModelChecker method) (SparseDtmcParameterLiftingModelChecker method) (SparseMdpParameterLiftingModelChecker method) OFF (LogLevel attribute) offset (Halfspace property) (Variable property) old_to_new_state_mapping (EndComponentEliminatorReturnType property) operator (Expression property) OperatorFormula (class in stormpy.logic)

OperatorType (class in stormpy.expressions) optimality_type (LongRunAverageOperatorFormula property) (OperatorFormula property) (ProbabilityOperatorFormula property) (RewardOperatorFormula property) (TimeOperatorFormula property) OPTIMISTIC_VALUE_ITERATION (MinMaxMethod attribute) (NativeLinearEquationSolverMethod attribute) OptimizationDirection (class in stormpy.logic) optimize() (Polytope method) OR (BinaryBooleanOperatorType attribute) (DFTElementType attribute) (FormulaType attribute) (OperatorType attribute) Or() (Expression static method) origins (SparseModelAction property) output_precision (DirectEncodingExporterOptions property) OverlappingGuardAnalyser (class in stormpy.developer.storage)

P

PAND (DFTElementType attribute) PARAMETER_LIFTING (RegionCheckEngine attribute) ParameterRegion (class in stormpy.pars) parameters_of_model() (in module stormpy.developer.storage) ParetoCurveCheckResult (class in stormpy.results) parse_constant_definition_string() (in module stormpy.developer) parse_constant_definitions() (SymbolicModelDescription method) parse_from_string() (ExpressionParser method) parse_jani_model() (in module stormpy) (in module stormpy.developer) (in module stormpy.io) parse_jani_model_from_string() (in module stormpy) (in module stormpy.developer) (in module stormpy.io) parse_prism_program() (in module stormpy) (in module stormpy.io) parse_program() (in module stormpy.developer) parse_properties() (in module stormpy) (in module stormpy.developer) (in module stormpy.logic) parse_properties_for_jani_model() (in module stormpy.developer) parse_properties_for_prism_program() (in module stormpy.developer) parse_properties_for_symbolic_model_description() (in module stormpy.developer) parse_property() (in module stormpy) (in module stormpy.logic) parse_region() (in module stormpy.pars) (in module stormpy.pars.developer) ParserError (class in stormpy.numbers.developer.parse) partial (Scheduler property) Path (class in stormpy.analysis) PathFormula (class in stormpy.logic) PCAA (MultiObjectiveMethod attribute) PcaaWeightVectorChecker (class in stormpy.developer) PDEP (DFTElementType attribute) perform_bisimulation() (in module stormpy.transformations) perform_bisimulation_minimization() (in module stormpy.developer) perform_multi_objective_model_checking() (in module stormpy.developer) perform_prob01() (in module stormpy.developer) perform_prob01_max() (in module stormpy.developer) perform_prob01_min() (in module stormpy.developer) PHA (JaniModelType attribute) PLA (FeasibilityMethod attribute) Place (class in stormpy.gspn) player1_matrix (SparseModelComponents property) plot_convex_pareto_curve_demo() (in module stormpy.plotting) plot_path_over_approximation (MultiObjectiveModelCheckerEnvironment property) plot_path_pareto_points (MultiObjectiveModelCheckerEnvironment property) plot_path_under_approximation (MultiObjectiveModelCheckerEnvironment property) PLUS (OperatorType attribute) Plus() (Expression static method) policy (BeliefBasedModelCheckerResult property) POLICY_ITERATION (ConditionalAlgorithmSetting attribute) (MinMaxMethod attribute) Polynomial (class in stormpy) (class in stormpy.numbers.developer.gmp) (in module stormpy.numbers) polynomial() (FactorizedPolynomial method) Polytope (class in stormpy.developer.storage) POMDP (ModelType attribute) (PrismModelType attribute) PomdpFscApplicationMode (class in stormpy.pomdp) PomdpMemory (class in stormpy.pomdp) PomdpMemoryBuilder (class in stormpy.pomdp.developer)

PomdpMemoryPattern (class in stormpy.pomdp) PomdpMemoryUnfolder (class in stormpy.pomdp.developer) PomdpTransformationResult (class in stormpy.pomdp.developer) pop() (SmtSolver method) (Z3SmtSolver method) POR (DFTElementType attribute) pow() (in module stormpy.numbers.developer) (in module stormpy.numbers.developer.cln) (in module stormpy.numbers.developer.gmp) POWER (NativeLinearEquationSolverMethod attribute) (OperatorType attribute) precision (ConditionalModelCheckerEnvironment property) (ExplorationEnvironment property) (MinMaxSolverEnvironment property) (MultiObjectiveModelCheckerEnvironment property) (NativeSolverEnvironment property) precision_type (MultiObjectiveModelCheckerEnvironment property) precomputation_type (ExplorationEnvironment property) PrecomputationType (class in stormpy.environments) precompute() (SMTMinimalLabelSetGenerator static method) predecessor_k (Path property) predecessor_node (Path property) prefer_signature_refinement (BisimulationOptions property) prepare_for_analysis() (in module stormpy.dft) prepare_for_qualitative_search() (in module stormpy.pomdp) prepare_multiobjective_result_for_plotting() (in module stormpy.plotting) prepare_pomdp_for_qualitative_search() (in module stormpy.pomdp.developer) preprocess() (SymbolicModelDescription method) preserve_all_rewards (BisimulationOptions property) preserve_choice_labels (BisimulationOptions property) preserve_choice_origins (BisimulationOptions property) print_results (MultiObjectiveModelCheckerEnvironment property) print_row() (SparseMatrix method) priority (TransitionPartition property) PrismAssignment (class in stormpy.io) PrismBooleanVariable (class in stormpy.io) PrismChoiceOrigins (class in stormpy.models) PrismCommand (class in stormpy.io) PrismConstant (class in stormpy.io) PrismIntegerVariable (class in stormpy.io) PrismLabel (class in stormpy.io) PrismModelType (class in stormpy.io) PrismModule (class in stormpy.io) PrismProgram (class in stormpy.io) PrismRewardModel (class in stormpy.io) PrismSimulator (class in stormpy.simulator) PrismUpdate (class in stormpy.io) PrismVariable (class in stormpy.io) PROBABILITY (ApproximationHeuristic attribute) probability (JaniEdgeDestination property) PROBABILITY (NextStateHeuristic attribute) probability_expression (PrismUpdate property) ProbabilityOperatorFormula (class in stormpy.logic) processed_mdp_choices (BeliefBasedModelCheckerStatistics property) processed_mdp_states (BeliefBasedModelCheckerStatistics property) processed_mdp_transitions (BeliefBasedModelCheckerStatistics property) product() (MemoryStructure method) product_model() (MemoryStructure method) program (PrismChoiceOrigins property) PROGRAM_LEVEL (SimulatorObservationMode attribute) Property (class in stormpy.logic) PTA (JaniModelType attribute) push() (SmtSolver method) (Z3SmtSolver method)

Q

QUALITATIVE (SignatureMode attribute) QualitativeCheckResult (class in stormpy.results) QuantitativeCheckResult (class in stormpy.results)

quotient() (in module stormpy.numbers.developer) (in module stormpy.numbers.developer.cln) (in module stormpy.numbers.developer.gmp) QuotientFormat (class in stormpy.transformations)

R

RANDOM (CuddReorderingTechnique attribute) random_fail() (DFTSimulator method) RANDOM_PIVOT (CuddReorderingTechnique attribute) random_step() (DFTTraceSimulator method) (DiscreteTimeSparseModelSimulator method) (PrismSimulator method) (SparseSimulator method) RandomGenerator (class in stormpy.dft.developer) rank (Variable property) rate (JaniEdge property) rate_transitions (SparseModelComponents property) Rational (class in stormpy) (class in stormpy.numbers) RATIONAL (UmbExportValueType attribute) (UmbImportValueType attribute) rational() (ExpressionManager method) rational_function() (FactorizedRationalFunction method) RATIONAL_INTERVAL (UmbExportValueType attribute) RATIONAL_SEARCH (MinMaxMethod attribute) (NativeLinearEquationSolverMethod attribute) RationalFunction (class in stormpy) (class in stormpy.numbers.developer.cln) (class in stormpy.numbers.developer.gmp) (in module stormpy.numbers) RationalFunctionCoefficient (class in stormpy) (in module stormpy.numbers) RationalInterval (class in stormpy) (in module stormpy.numbers) RawPolynomial (class in stormpy) (in module stormpy.numbers) reachable_states (SymbolicCtmc property) (SymbolicDtmc property) (SymbolicMA property) (SymbolicMdp property) (SymbolicModel property) REAL (VariableType attribute) reduce() (NondeterministicBeliefTracker method) reduce_to_state_based_rewards() (SparseCtmc method) (SparseDtmc method) (SparseMA method) (SparseMdp method) (SparseModel method) (SparsePomdp method) (SparseRewardModel method) (SparseSmg method) (SymbolicCtmc method) (SymbolicDtmc method) (SymbolicMA method) (SymbolicMdp method) (SymbolicModel method) refinement_mode (DdBisimulationOptions property) RefinementMode (class in stormpy.developer) RegionCheckEngine (class in stormpy.pars) RegionModelChecker (class in stormpy.pars.developer) RegionRefinementChecker (class in stormpy.pars.developer) RegionResult (class in stormpy.pars) RegionResultHypothesis (class in stormpy.pars.developer) RegionSplitEstimateKind (class in stormpy.pars.developer) REGULAR (InitialPartitionMode attribute) rel() (SimpleConstraint method), [1] (SimpleConstraintRatFunc method), [1] Relation (class in stormpy.numbers.developer.formula) relation (Constraint property), [1] relative_precision (ConditionalModelCheckerEnvironment property) relative_termination_criterion (MinMaxSolverEnvironment property) (NativeSolverEnvironment property) RELATIVE_TO_DIFF (MultiObjectivePrecisionType attribute) RelevantEvents (class in stormpy.dft) remove_bound() (LongRunAverageOperatorFormula method) (OperatorFormula method) (ProbabilityOperatorFormula method) (RewardOperatorFormula method) (TimeOperatorFormula method)

remove_constant() (JaniModel method) remove_inhibition_arc() (ImmediateTransition method) (TimedTransition method) (Transition method) remove_input_arc() (ImmediateTransition method) (TimedTransition method) (Transition method) remove_optimality_type() (LongRunAverageOperatorFormula method) (OperatorFormula method) (ProbabilityOperatorFormula method) (RewardOperatorFormula method) (TimeOperatorFormula method) remove_output_arc() (ImmediateTransition method) (TimedTransition method) (Transition method) reordering_enabled (CuddDdManagerEnvironment property) reordering_technique (CuddDdManagerEnvironment property) replace_automaton() (JaniModel method) replace_columns() (SparseMatrixBuilder method) replace_constant_by_variable() (PrismProgram method) replace_variable_initialization_by_init_expression() (PrismProgram method) representative (DftIndependentModule property) reset() (BeliefSupportTracker method) (DFTSimulator method) (DFTTraceSimulator method) (NondeterministicBeliefTracker method) (ObservationTraceUnfolder method) (SmtSolver method) (Z3SmtSolver method) reset_state() (DFTTraceSimulator method) reset_timeout_alarm() (in module stormpy.developer) reset_to_initial() (DiscreteTimePrismProgramSimulator method) (DiscreteTimeSparseModelSimulator method) reset_to_state() (DiscreteTimePrismProgramSimulator method) resize() (BitVector method) RESTART (ConditionalAlgorithmSetting attribute) restart() (PrismSimulator method) (Simulator method) (SparseSimulator method) restrict_commands() (PrismProgram method) restrict_edges() (JaniModel method) reuse_mode (DdBisimulationOptions property) ReuseMode (class in stormpy.developer) reward_models (PrismProgram property) (SparseCtmc property) (SparseDtmc property) (SparseMA property) (SparseMdp property) (SparseModel property) (SparseModelComponents property) (SparsePomdp property) (SparseSmg property) (SymbolicCtmc property) (SymbolicDtmc property) (SymbolicMA property) (SymbolicMdp property) (SymbolicModel property) reward_name (RewardOperatorFormula property) RewardAccumulationEliminationVisitor (class in stormpy.developer.storage) RewardOperatorFormula (class in stormpy.logic) right_subformula (BinaryPathFormula property) (BoundedUntilFormula property) (UntilFormula property) risk (SparseBeliefState property) ROBUST (UncertaintyResolutionMode attribute) ROBUST_PARAMETER_LIFTING (RegionCheckEngine attribute) rotation (LayoutInfo property) row_iter() (SparseMatrix method)

S

sample() (Interval method), [1] sampled_paths_until_precomputation (ExplorationEnvironment property) SAT (SmtCheckResult attribute) Scheduler (class in stormpy.models) scheduler_restriction (MultiObjectiveModelCheckerEnvironment property) SchedulerChoice (class in stormpy.models) SchedulerClass (class in stormpy.developer) SchedulerMemoryPattern (class in stormpy.developer) SCP (FeasibilityMethod attribute) select_entities() (Valuations method) SELECTIVE_COUNTER (PomdpMemoryPattern attribute) SELECTIVE_RING (PomdpMemoryPattern attribute) SEQ (DFTElementType attribute) set() (BitVector method) set_action_mode() (PrismSimulator method) (Simulator method) (SparseSimulator method) set_add_out_of_bounds_state() (BuilderOptions method), [1] set_add_overlapping_guards_label() (BuilderOptions method), [1] set_apply_maximal_progress_assumption() (BuilderOptions method), [1] set_bound() (LongRunAverageOperatorFormula method) (OperatorFormula method) (ProbabilityOperatorFormula method) (RewardOperatorFormula method) (TimeOperatorFormula method) set_build_all_labels() (BuilderOptions method), [1] set_build_all_reward_models() (BuilderOptions method), [1] set_build_choice_labels() (BuilderOptions method), [1] set_build_choice_origins() (BuilderOptions method), [1] set_build_full_product() (MemoryStructureProduct method) set_build_observation_valuations() (BuilderOptions method), [1] set_build_state_valuations() (BuilderOptions method), [1] set_capacity() (Place method) set_choice() (Scheduler method) set_choices() (ChoiceLabeling method) set_compute_only_maybe_states() (ExplicitModelCheckerHint method) set_exploration_checks() (BuilderOptions method), [1] set_from_exploded_string() (in module stormpy.developer) set_full_observability() (PrismSimulator method) (Simulator method) (SparseSimulator method) set_gspn_name() (GspnBuilder method) set_hint() (CheckTask method) set_identifier_mapping() (ExpressionParser method) set_infinite_server_semantics() (TimedTransition method) set_inhibition_arc_multiplicity() (ImmediateTransition method) (TimedTransition method) (Transition method) set_initial_memory_state() (MemoryStructureBuilder method) set_initial_states() (SparseCtmc method) (SparseDtmc method) (SparseMA method) (SparseMdp method) (SparseModel method) (SparsePomdp method) (SparseSmg method) set_input_arc_multiplicity() (ImmediateTransition method) (TimedTransition method) (Transition method) set_instantiations_are_graph_preserving() (SparseInstantiationModelChecker method) set_k_server_semantics() (TimedTransition method) set_label() (MemoryStructureBuilder method) set_linear_equation_solver_type() (SolverEnvironment method) set_log_level() (in module stormpy.developer) set_lower_bounds() (ExplicitQuantitativeCheckResult method) set_maybe_states() (ExplicitModelCheckerHint method) set_memory_pattern() (SchedulerClass method) set_model_type() (JaniModel method) set_name() (GSPN method) (ImmediateTransition method) (Place method) (TimedTransition method) (Transition method) set_no_end_components_in_maybe_states() (ExplicitModelCheckerHint method) set_number_of_initial_tokens() (Place method) set_observation_mode() (PrismSimulator method) (Simulator method) (SparseSimulator method) set_optimality_type() (LongRunAverageOperatorFormula method) (OperatorFormula method) (ProbabilityOperatorFormula method) (RewardOperatorFormula method) (TimeOperatorFormula method) set_output_arc_multiplicity() (ImmediateTransition method) (TimedTransition method) (Transition method) set_place_layout_info() (GspnBuilder method) set_positional() (SchedulerClass method) set_priority() (ImmediateTransition method) (TimedTransition method) (Transition method) set_produce_schedulers() (CheckTask method) set_rate() (TimedTransition method) set_relevant_events() (DFT method) set_result_hint() (ExplicitModelCheckerHint method) set_risk() (GenerateMonitorVerifier method) (NondeterministicBeliefTracker method) set_scale_and_lift_transition_rewards() (BuilderOptions method), [1] set_scheduler_hint() (ExplicitModelCheckerHint method) set_seed() (DiscreteTimePrismProgramSimulator method) (DiscreteTimeSparseModelSimulator method) (PrismSimulator method) (SparseSimulator method) set_single_server_semantics() (TimedTransition method) set_standard_system_composition() (JaniModel method) set_state_reward() (SparseRewardModel method) set_state_valuations() (in module stormpy.transformations) set_states() (StateLabeling method) set_timeout_alarm() (in module stormpy.developer) set_transition() (MemoryStructureBuilder method) set_transition_layout_info() (GspnBuilder method) set_uncertainty_resolution_mode() (CheckTask method) set_upper_bounds() (ExplicitQuantitativeCheckResult method) set_value() (SparseMatrixEntry method) set_values_exact() (ExplicitQuantitativeCheckResult method) set_weight() (ImmediateTransition method) set_weighted_precision() (PcaaWeightVectorChecker method) setLower() (Interval method), [1] SETTABLE_BITS (PomdpMemoryPattern attribute) setup_time (SMTMinimalLabelSetGeneratorStats property) setUpper() (Interval method), [1] SHA (JaniModelType attribute) sharpen() (in module stormpy.developer.utility) short_version_string() (StormVersion static method) shortest_path() (in module stormpy.analysis) ShortestPathsGenerator (class in stormpy.developer.utility) show_progress_delay (DdBisimulationOptions property) SIFT (CuddReorderingTechnique attribute) SIFT_CONV (CuddReorderingTechnique attribute) SignatureMode (class in stormpy.developer) silent (SMTMinimalLabelSetGeneratorOptions property) SIMPLE_LINEAR (PomdpFscApplicationMode attribute) SIMPLE_LINEAR_INVERSE (PomdpFscApplicationMode attribute) SIMPLE_LOG (PomdpFscApplicationMode attribute) SimpleConstraint (class in stormpy.numbers.developer.cln.formula) (class in stormpy.numbers.developer.gmp.formula) SimpleConstraintRatFunc (class in stormpy.numbers.developer.cln.formula) (class in stormpy.numbers.developer.gmp.formula) SimpleValuation (class in stormpy.models) simplified_formula (SparseParametricModelSimplifier property) simplified_model (SparseParametricModelSimplifier property) simplify() (Expression method) (PrismProgram method) (PrismUpdate method) (SparseParametricModelSimplifier method) simulate_trace() (DFTTraceSimulator method) simulate_traces() (DFTSimulator method) SimulationStepResult (class in stormpy.dft) SimulationTraceResult (class in stormpy.dft) Simulator (class in stormpy.simulator) SimulatorActionMode (class in stormpy.simulator) SimulatorObservationMode (class in stormpy.simulator) sink_rows (EndComponentEliminatorReturnType property) size (MaximalEndComponent property) (MaximalEndComponentDecomposition property) size() (BitVector method) (Choice method) (ExplicitStateLookup method) SMG (ModelType attribute) SmtCheckResult (class in stormpy.developer) SMTMinimalLabelSetGenerator (class in stormpy.developer) SMTMinimalLabelSetGeneratorCexInput (class in stormpy.developer) SMTMinimalLabelSetGeneratorOptions (class in stormpy.developer) SMTMinimalLabelSetGeneratorStats (class in stormpy.developer) SmtSolver (class in stormpy.developer) SmtSolverFactory (class in stormpy.developer) SolutionBounds (class in stormpy.results) solve_with_smt (AnalysisEnvironment property) solver() (Environment method) solver_time (SMTMinimalLabelSetGeneratorStats property) SolverEnvironment (class in stormpy.environments) SOR (NativeLinearEquationSolverMethod attribute) sound() (in module stormpy.environments) SOUND_VALUE_ITERATION (MinMaxMethod attribute) (NativeLinearEquationSolverMethod attribute) SoundEnvironmentFactory (class in stormpy.developer) source_location_index (JaniEdge property) SPARE (DFTElementType attribute) spare_uses() (DFTState method) SPARSE (Engine attribute) (QuotientFormat attribute) sparse_model_from_umb() (in module stormpy.developer.storage) sparse_model_to_umb() (in module stormpy.developer.storage) (in module stormpy.io) SparseBeliefState (class in stormpy.pomdp) SparseCtmc (class in stormpy.models) SparseDtmc (class in stormpy.models) SparseDtmcParameterLiftingModelChecker (class in stormpy.pars.developer) SparseInstantiationModelChecker (class in stormpy.pars.developer) SparseMA (class in stormpy.models) SparseMatrix (class in stormpy.datastructures) SparseMatrixBuilder (class in stormpy.datastructures) SparseMatrixEntry (class in stormpy.datastructures) SparseMatrixRows (class in stormpy.datastructures) SparseMdp (class in stormpy.models) SparseMdpParameterLiftingModelChecker (class in stormpy.pars.developer) SparseModel (class in stormpy.models) SparseModelAction (class in stormpy.models) SparseModelActions (class in stormpy.models) SparseModelComponents (class in stormpy.models) SparseModelMemoryProductReverseData (class in stormpy.developer.storage) SparseModelState (class in stormpy.models) SparseModelStates (class in stormpy.models) SparseParametricModelSimplifier (class in stormpy.pars.developer) SparsePomdp (class in stormpy.models) SparseRewardModel (class in stormpy.models) SparseSimulator (class in stormpy.simulator) SparseSmg (class in stormpy.models) specify() (RegionModelChecker method) (RegionRefinementChecker method) (SparseDtmcParameterLiftingModelChecker method) (SparseMdpParameterLiftingModelChecker method) specify_formula() (SparseInstantiationModelChecker method) STA (JaniModelType attribute) STANDARD (PomdpFscApplicationMode attribute) state_action_rewards (SparseRewardModel property) state_domain_size (JaniInformationObject property) state_label_preservation (BisimulationOptions property) state_labeling (MemoryStructure property) (SparseModelComponents property) STATE_LEVEL (SimulatorObservationMode attribute) state_player_indications (SparseModelComponents property) state_rewards (SparseRewardModel property) state_valuations (SparseCtmc property) (SparseDtmc property) (SparseMA property) (SparseMdp property) (SparseModel property) (SparseModelComponents property) (SparsePomdp property) (SparseSmg property) STATE_VALUE_DELTA (RegionSplitEstimateKind attribute) STATE_VALUE_DELTA_WEIGHTED (RegionSplitEstimateKind attribute) StateFormula (class in stormpy.logic) StateLabeling (class in stormpy.models) StateLabelPreservation (class in stormpy.transformations) states (SparseCtmc property) (SparseDtmc property) (SparseMA property) (SparseMdp property) (SparseModel property) (SparsePomdp property) (SparseSmg property)

StateValuationFunctionMask (class in stormpy.developer) statistics (BeliefBasedModelCheckerResult property) status (FeasibilitySynthesisResult property) status() (DFTSimulator method) stays_in_winning_region() (WinningRegionQueryInterface method) steady_state_distribution_algorithm (ModelCheckerEnvironment property) SteadyStateDistributionAlgorithm (class in stormpy.environments) step() (DFTTraceSimulator method) (DiscreteTimePrismProgramSimulator method) (DiscreteTimeSparseModelSimulator method) (PrismSimulator method) (Simulator method) (SparseSimulator method) step_prefix (GenerateMonitorVerifierOptions property) steps_until_precomputation (ExplorationEnvironment property) store_as_string() (BitVector method) store_to_file() (WinningRegion method) storm_build_info() (in module stormpy.info) storm_build_type() (in module stormpy.info) storm_development_version() (in module stormpy.info) storm_directory() (in module stormpy.info) storm_exact_use_cln() (in module stormpy.info) storm_from_system() (in module stormpy.info) storm_full_version() (in module stormpy.info) storm_long_version() (in module stormpy.info) storm_origin_info() (in module stormpy.info) storm_ratfunc_use_cln() (in module stormpy.info) storm_version() (in module stormpy.info) StormError (class in stormpy.exceptions) stormpy module stormpy.analysis module stormpy.datastructures module stormpy.developer module stormpy.developer.info module stormpy.developer.logic module stormpy.developer.storage module stormpy.developer.utility module stormpy.dft module stormpy.dft.developer module stormpy.environments module stormpy.exceptions module stormpy.expressions module stormpy.gspn module stormpy.info module stormpy.io module stormpy.logic module stormpy.models module stormpy.numbers module stormpy.numbers.developer module stormpy.numbers.developer.cln module stormpy.numbers.developer.cln.formula module stormpy.numbers.developer.convert module stormpy.numbers.developer.formula module stormpy.numbers.developer.gmp module stormpy.numbers.developer.gmp.formula module stormpy.numbers.developer.parse module stormpy.pars module stormpy.pars.developer module stormpy.plotting module stormpy.pomdp module stormpy.pomdp.developer module stormpy.results module stormpy.simulator module stormpy.transformations module StormVersion (class in stormpy.developer.info) StormWarning (class in stormpy.exceptions) STRAIGHT (MatrixFormat attribute) STRICT (BoundType attribute) STRONG (BisimulationType attribute) subformula (EventuallyFormula property) (GameFormula property) (GloballyFormula property) (LongRunAverageOperatorFormula property) (OperatorFormula property) (ProbabilityOperatorFormula property) (RewardOperatorFormula property) (TimeOperatorFormula property) (UnaryBooleanStateFormula property) (UnaryPathFormula property) (UnaryStateFormula property) subformulas (MultiObjectiveFormula property) submodules (DftIndependentModule property) substitute() (AtomicExpressionFormula method) (AtomicLabelFormula method) (BinaryBooleanStateFormula method) (BinaryPathFormula method) (BinaryStateFormula method) (BooleanLiteralFormula method) (BoundedUntilFormula method) (ConditionalFormula method) (CumulativeRewardFormula method) (DiscountedCumulativeRewardFormula method) (DiscountedTotalRewardFormula method) (EventuallyFormula method) (Expression method) (Formula method) (GameFormula method) (GloballyFormula method) (InstantaneousRewardFormula method) (JaniEdge method) (JaniOrderedAssignments method) (LongRunAverageOperatorFormula method) (LongRunAverageRewardFormula method) (MultiObjectiveFormula method) (OperatorFormula method) (PathFormula method) (Polynomial method) (PrismUpdate method) (ProbabilityOperatorFormula method) (Property method) (RewardOperatorFormula method) (StateFormula method) (TimeOperatorFormula method) (UnaryBooleanStateFormula method) (UnaryPathFormula method) (UnaryStateFormula method) (UntilFormula method) substitute_constants() (JaniModel method) (PrismProgram method) substitute_constants_in_properties() (in module stormpy.developer) substitute_formulas() (PrismProgram method) substitute_functions() (JaniModel method) substitute_labels_by_labels() (AtomicExpressionFormula method) (AtomicLabelFormula method) (BinaryBooleanStateFormula method) (BinaryPathFormula method) (BinaryStateFormula method) (BooleanLiteralFormula method) (BoundedUntilFormula method) (ConditionalFormula method) (CumulativeRewardFormula method) (DiscountedCumulativeRewardFormula method) (DiscountedTotalRewardFormula method) (EventuallyFormula method) (Formula method) (GameFormula method) (GloballyFormula method) (InstantaneousRewardFormula method) (LongRunAverageOperatorFormula method) (LongRunAverageRewardFormula method) (MultiObjectiveFormula method) (OperatorFormula method) (PathFormula method) (ProbabilityOperatorFormula method) (RewardOperatorFormula method) (StateFormula method) (TimeOperatorFormula method) (UnaryBooleanStateFormula method) (UnaryPathFormula method) (UnaryStateFormula method) (UntilFormula method) substitute_non_standard_predicates() (PrismProgram method) SubsystemBuilderOptions (class in stormpy.transformations) SubsystemBuilderReturnType (class in stormpy.transformations) subtree() (DftIndependentModule method) SUCCESSFUL (SimulationStepResult attribute) (SimulationTraceResult attribute) SUM (FilterType attribute) sum() (ExplicitQuantitativeCheckResult method) (HybridQuantitativeCheckResult method) (QuantitativeCheckResult method) (SymbolicQuantitativeCheckResult method) supports_parameters (ModelBase property) (SparseCtmc property) (SparseDtmc property) (SparseMA property) (SparseMdp property) (SparseModel property) (SparsePomdp property) (SparseSmg property) (SymbolicCtmc property) (SymbolicDtmc property) (SymbolicMA property) (SymbolicMdp property) (SymbolicModel property) supports_uncertainty (SparseCtmc property) (SparseDtmc property) (SparseMA property) (SparseMdp property) (SparseModel property) (SparsePomdp property) (SparseSmg property) Sylvan (DdType attribute) sylvan() (DdEnvironment method) SylvanDdManagerEnvironment (class in stormpy.environments) SymbolicCtmc (class in stormpy.models) SymbolicDtmc (class in stormpy.models) SymbolicMA (class in stormpy.models) SymbolicMdp (class in stormpy.models) SymbolicModel (class in stormpy.models) SymbolicModelDescription (class in stormpy.io) SymbolicQualitativeCheckResult (class in stormpy.results) SymbolicQuantitativeCheckResult (class in stormpy.results) SymbolicRewardModel (class in stormpy.models) SYMMETRIC_SIFT (CuddReorderingTechnique attribute) SYMMETRIC_SIFT_CONV (CuddReorderingTechnique attribute) symmetricDifference() (Interval method), [1] symmetries() (DFT method)

T

TA (JaniModelType attribute) take_first_dependency (ModelBuilderEnvironment property) target_location_index (JaniEdgeDestination property) tdeg (Monomial property) (Term property), [1] template_edge (JaniEdge property) Term (class in stormpy.numbers.developer.cln) (class in stormpy.numbers.developer.gmp) threshold (LongRunAverageOperatorFormula property) (OperatorFormula property) (ProbabilityOperatorFormula property) (RewardOperatorFormula property) (TimeOperatorFormula property) threshold_expr (LongRunAverageOperatorFormula property) (OperatorFormula property) (ProbabilityOperatorFormula property) (RewardOperatorFormula property) (TimeOperatorFormula property) time_out (NondeterministicBeliefTrackerOptions property) timed_transition_id_to_transition_id() (GSPN static method) TimedTransition (class in stormpy.gspn) TimeOperatorFormula (class in stormpy.logic) TIMES (OperatorType attribute) to_archive() (in module stormpy.developer.storage) to_dot() (JaniModel method) (ObservationBasedFiniteStateController method) (SparseCtmc method) (SparseDtmc method) (SparseMA method) (SparseMdp method) (SparseModel method) (SparsePomdp method) (SparseSmg method) to_expression() (Bdd method) to_file() (JsonExporter static method) to_jani() (PrismProgram method) to_json() (ObservationBasedFiniteStateController method) (SimpleValuation method) (Valuations method) to_json_str() (Scheduler method) to_smt2() (Constraint method), [1] (FactorizedPolynomial method) (FactorizedRationalFunction method) (Formula method), [1] (Polynomial method) (RationalFunction method), [1] to_str() (Scheduler method) to_string() (DFTState method) (DiceStringVisitor method) (SimpleValuation method) (Valuations method) to_value_type() (in module stormpy.developer.storage) (Scheduler method) tolerance (BisimulationOptions property)

top_level_element (DFT property) TOPOLOGICAL (EquationSolverType attribute) (MinMaxMethod attribute) topological_sort() (in module stormpy.analysis) total_degree (Polynomial property) TRACE (LogLevel attribute) track() (BeliefSupportTracker method) (NondeterministicBeliefTracker method) track_time_out (NondeterministicBeliefTrackerOptions property) transform() (AddUncertainty method) (ApplyFiniteSchedulerToPomdp method) (BinaryPomdpTransformer method) (EndComponentEliminator static method) (JaniLocationExpander method) (MakePOMDPCanonic method) (ObservationTraceUnfolder method) (PomdpMemoryUnfolder method) transform_continuous_to_discrete_time_sparse_model() (in module stormpy.developer) transform_dft() (in module stormpy.dft.developer) transform_symbolic_to_sparse_model() (in module stormpy.developer) transform_to_discrete_time_model() (in module stormpy.transformations) transform_to_sparse_model() (in module stormpy.transformations) transformation_environment (DftEnvironment property) TransformationEnvironment (class in stormpy.dft) transformed_pomdp (PomdpTransformationResult property) transformed_state_to_original_state_map (PomdpTransformationResult property) Transition (class in stormpy.gspn) transition_id_to_immediate_transition_id() (GSPN static method) transition_id_to_timed_transition_id() (GSPN static method) transition_matrix (SparseCtmc property) (SparseDtmc property) (SparseMA property) (SparseMdp property) (SparseModel property) (SparseModelComponents property) (SparsePomdp property) (SparseSmg property) transition_rewards (SparseRewardModel property) TransitionPartition (class in stormpy.gspn) transitions (SparseModelAction property) (TransitionPartition property) trigger_event (DFTDependency property) TRIVIAL (PomdpMemoryPattern attribute) TRUE (FormulaType attribute) type (DdMetaVariable property) (DFTBE property) (DFTDependency property) (DFTElement property) (Expression property) (Formula property), [1] (JaniConstant property) (JaniVariable property) (PrismConstant property) (Variable property)

U

UEQ (FormulaType attribute) umb_to_archive() (in module stormpy.io) UmbExportOptions (class in stormpy.io) UmbExportValueType (class in stormpy.io) UmbImportOptions (class in stormpy.io) UmbImportValueType (class in stormpy.io) UmbModel (class in stormpy.io) UnaryBooleanStateFormula (class in stormpy.logic) UnaryPathFormula (class in stormpy.logic) UnaryStateFormula (class in stormpy.logic) unboundedInterval() (Interval static method), [1] UncertaintyResolutionMode (class in stormpy) UNDEFINED (JaniModelType attribute) (PrismModelType attribute) undefined_constants_are_graph_preserving (JaniModel property) (PrismProgram property) unfold_memory() (in module stormpy.pomdp) UNIFORM (NextStateHeuristic attribute) unique_failed_be (ModelBuilderEnvironment property) unite() (Interval method), [1] UNKNOWN (GraphPreservationStatus attribute) (RegionResult attribute) (RegionResultHypothesis attribute) (SmtCheckResult attribute) UNORDERED (ExplorationQueueOrder attribute) UNSAT (SmtCheckResult attribute)

UNSET (UncertaintyResolutionMode attribute) UNSUCCESSFUL (SimulationStepResult attribute) (SimulationTraceResult attribute) UntilFormula (class in stormpy.logic) update_initial_states_expression() (PrismProgram method) updates (PrismCommand property) upper (AggregatedValue property) (BoundedValue property) (SolutionBounds property) upper() (Interval method), [1] upper_bound (BoundedType property) upper_bound_expression (BoundedUntilFormula property) (PrismIntegerVariable property) use_bisimulation (TransformationEnvironment property) use_bscc_order_encoding (MultiObjectiveModelCheckerEnvironment property) use_clipping (BeliefBasedModelCheckerOptions property) use_dynamic_constraints (SMTMinimalLabelSetGeneratorOptions property) use_indicator_constraints (MultiObjectiveModelCheckerEnvironment property) use_modularisation (AnalysisEnvironment property) use_original_variables (DdBisimulationOptions property) use_redundant_bscc_constraints (MultiObjectiveModelCheckerEnvironment property) use_representatives (DdBisimulationOptions property) use_restart_semantics (GenerateMonitorVerifierOptions property) (ObservationTraceUnfolderOptions property) use_symmetry_reduction (ModelBuilderEnvironment property) used_constants() (PrismProgram method)

V

validate() (UmbModel method) validate_or_throw() (UmbModel method) VALIDATING_PARAMETER_LIFTING (RegionCheckEngine attribute) Valuation (class in stormpy.developer.storage) valuation (FeasibilityResult property) ValuationClassDescription (class in stormpy.models) ValuationDescriptionBuilder (class in stormpy.models) Valuations (class in stormpy.models) valuations (SparseModelState property) ValuationTransformer (class in stormpy.models) value (AggregatedValue property) (BeliefBasedModelCheckerResult property) (BoundedValue property) (FeasibilityResult property) (SparseMatrixEntry property) VALUE_ITERATION (MinMaxMethod attribute) value_type (UmbExportOptions property) (UmbImportOptions property) VALUES (FilterType attribute) Variable (class in stormpy.expressions) (class in stormpy.numbers) variable (JaniAssignment property) (PrismAssignment property)

variable_with_name() (in module stormpy.numbers) variables (JaniAutomaton property) (PrismProgram property) VariableType (class in stormpy.numbers.developer) verbose (DdBisimulationOptions property) verify() (in module stormpy.pars) (in module stormpy.pars.developer) verify_with_belief_discretization() (in module stormpy.pomdp) (in module stormpy.pomdp.developer) verify_with_belief_unfolding() (in module stormpy.pomdp) (in module stormpy.pomdp.developer) verify_with_dd_engine() (in module stormpy.developer) verify_with_hybrid_engine() (in module stormpy.developer) verify_with_sparse_engine() (in module stormpy.developer) version_dev (StormVersion attribute) version_major (StormVersion attribute) version_minor (StormVersion attribute) version_patch (StormVersion attribute) version_tweak (StormVersion attribute) vertices (Polytope property) VOT (DFTElementType attribute)

W

WALKER_CHAE (NativeLinearEquationSolverMethod attribute) WARN (LogLevel attribute) WEAK (BisimulationType attribute) (BoundType attribute) WELL_DEFINED (GraphPreservationStatus attribute) wiggle (NondeterministicBeliefTrackerOptions property) WIN2 (CuddReorderingTechnique attribute) WIN2_CONV (CuddReorderingTechnique attribute) WIN3 (CuddReorderingTechnique attribute) WIN3_CONV (CuddReorderingTechnique attribute) WIN4 (CuddReorderingTechnique attribute) WIN4_CONV (CuddReorderingTechnique attribute) WinningRegion (class in stormpy.pomdp)

WinningRegionQueryInterface (class in stormpy.pomdp) with_traceback() (NoPicklingSupport method) (ParserError method) (StormError method) (StormWarning method) witness (FeasibilitySynthesisResult property) write_bool_value() (Valuations method) write_double_value() (Valuations method) write_int64_value() (Valuations method) write_integer_bigint_value() (Valuations method) write_rational_value() (Valuations method) write_string_value() (Valuations method) write_value() (Valuations method)

X

x (LayoutInfo property) XOR (FormulaType attribute) (OperatorType attribute)

XZ (CompressionMode attribute)

Y

y (LayoutInfo property)

Z

Z3SmtSolver (class in stormpy.developer)

Z3SmtSolverFactory (class in stormpy.developer) zeroInterval() (Interval static method), [1]