Index

A

abs() (in module stormpy.pycarl) (in module stormpy.pycarl.cln) (in module stormpy.pycarl.gmp) (Interval method), [1], [2] action_index (JaniEdge property), [1] (PrismCommand property), [1] action_name (PrismCommand property), [1] ActionMaskDouble (class in stormpy) actions (SparseExactModelState property), [1] (SparseIntervalModelState property), [1] (SparseModelState property), [1] (SparseParametricModelState property), [1] add() (JaniOrderedAssignments method), [1] (SmtSolver method) add_automaton() (JaniModel method), [1] add_backward_implication_cuts (SMTCounterExampleGeneratorOptions property) add_constant() (JaniModel method), [1] add_destination() (JaniTemplateEdge method), [1] add_edge() (JaniAutomaton method), [1] add_immediate_transition() (GSPNBuilder method) add_inhibition_arc() (GSPNBuilder method) add_initial_location() (JaniAutomaton method), [1] add_input_arc() (GSPNBuilder method) add_label() (ItemLabeling method), [1] add_label_to_choice() (ChoiceLabeling method), [1] add_label_to_state() (StateLabeling method), [1] add_location() (JaniAutomaton method), [1] add_next_value() (ExactSparseMatrixBuilder method), [1] (IntervalSparseMatrixBuilder method), [1] (ParametricSparseMatrixBuilder method), [1] (SparseMatrixBuilder method), [1] add_normal_arc() (GSPNBuilder method) add_output_arc() (GSPNBuilder method) add_place() (GSPNBuilder method) add_reward_and_threshold() (SMTCounterExampleInput method) add_state() (StateValuationsBuilder method), [1] Add_Sylvan_Double (class in stormpy) (class in stormpy.storage) add_timed_transition() (GSPNBuilder method) add_variable() (JaniVariableSet method), [1] (StateValuationsBuilder method), [1] AddIterator_Sylvan_Double (class in stormpy) (class in stormpy.storage) allow_placeholders (DirectEncodingOptions property) ALLSAT (RegionResult attribute) (RegionResultHypothesis attribute)

ALLVIOLATED (RegionResult attribute) (RegionResultHypothesis attribute) analysis_time (SMTCounterExampleGeneratorStats property) analyze_dft() (in module stormpy.dft) AND (BinaryBooleanOperatorType attribute), [1] (DFTElementType attribute) (FormulaType attribute) And (OperatorType attribute), [1] And() (Expression static method), [1] apply_scheduler() (SparseExactMA method), [1] (SparseExactMdp method), [1] (SparseIntervalMA method), [1] (SparseIntervalMdp method), [1] (SparseMA method), [1] (SparseMdp method), [1] (SparseParametricMA method), [1] (SparseParametricMdp method), [1] apply_unknown_fsc() (in module stormpy.pomdp) ApproximationHeuristic (class in stormpy.dft) area (ParameterRegion property) arity (Expression property), [1] as_be_double() (FailableElement method) as_be_ratfunc() (FailableElement method) as_dependency_double() (FailableElement method) as_dependency_ratfunc() (FailableElement method) as_int() (BitVector method), [1] as_jani_choice_origins() (ChoiceOrigins method), [1] as_jani_model() (SymbolicModelDescription method) as_prism_choice_origins() (ChoiceOrigins method), [1] as_prism_program() (SymbolicModelDescription method) assignments (JaniEdgeDestination property), [1] (JaniLocation property), [1] (JaniTemplateEdge property), [1] (JaniTemplateEdgeDestination property), [1] (PrismUpdate property), [1] at() (ExplicitExactQuantitativeCheckResult method) (ExplicitParametricQuantitativeCheckResult method) (ExplicitQualitativeCheckResult method) (ExplicitQuantitativeCheckResult method) AtomicExpressionFormula (class in stormpy) (class in stormpy.logic) AtomicLabelFormula (class in stormpy) (class in stormpy.logic) automata (JaniModel property), [1] avg_var_domain_size (JaniInformationObject property), [1]

B

Bdd_Sylvan (class in stormpy) (class in stormpy.storage) BE (DFTElementType attribute) BeliefExplorationModelCheckerDouble (class in stormpy.pomdp) BeliefExplorationModelCheckerOptionsDouble (class in stormpy.pomdp) BeliefExplorationPomdpModelCheckerResultDouble (class in stormpy.pomdp) BeliefMdpExplorerDouble (class in stormpy.pomdp) BeliefSupportTrackerDouble (class in stormpy.pomdp) BeliefSupportTrackerExact (class in stormpy.pomdp) BeliefSupportWinningRegion (class in stormpy.pomdp) BeliefSupportWinningRegionQueryInterfaceDouble (class in stormpy.pomdp) BinaryBooleanOperatorType (class in stormpy) (class in stormpy.logic) BinaryPathFormula (class in stormpy) (class in stormpy.logic) BinaryStateFormula (class in stormpy) (class in stormpy.logic) BisimulationType (class in stormpy) BitVector (class in stormpy) (class in stormpy.storage) Bitvector (DdMetaVariableType attribute), [1] BITVECTOR (FormulaType attribute) Bool (DdMetaVariableType attribute), [1] BOOL (FormulaType attribute) (VariableType attribute) boolean_variables (PrismModule property), [1] BooleanBinaryStateFormula (class in stormpy) (class in stormpy.logic) BooleanLiteralFormula (class in stormpy) (class in stormpy.logic) BOUNDDIFFERENCE (ApproximationHeuristic attribute) BoundedUntilFormula (class in stormpy) (class in stormpy.logic) BoundType (class in stormpy.pycarl) build() (ExactSparseMatrixBuilder method), [1] (ExplicitDFTModelBuilder_double method) (ExplicitDFTModelBuilder_ratfunc method) (ExplicitModelBuilder method) (ExplicitParametricModelBuilder method) (GSPNToJaniBuilder method) (IntervalSparseMatrixBuilder method), [1] (ParametricSparseMatrixBuilder method), [1] (PomdpMemoryBuilder method) (SMTCounterExampleGenerator static method) (SparseMatrixBuilder method), [1] (StateValuationsBuilder method), [1]

build_action_mapping (SubsystemBuilderOptions property) build_choice_labels (DirectEncodingParserOptions property) build_gspn() (GSPNBuilder method) build_info (Version attribute) build_interval_model_from_drn() (in module stormpy) build_kept_actions (SubsystemBuilderOptions property) build_model() (in module stormpy) (in module stormpy.dft) build_model_from_drn() (in module stormpy) build_parametric_model() (in module stormpy) build_parametric_model_from_drn() (in module stormpy) build_parametric_sparse_matrix() (in module stormpy) (in module stormpy.storage) build_sparse_exact_model_with_options() (in module stormpy) build_sparse_matrix() (in module stormpy) (in module stormpy.storage) build_sparse_model() (in module stormpy) build_sparse_model_from_explicit() (in module stormpy) build_sparse_model_with_options() (in module stormpy) build_sparse_parametric_model() (in module stormpy) build_sparse_parametric_model_with_options() (in module stormpy) build_state_mapping (SubsystemBuilderOptions property) build_symbolic_model() (in module stormpy) build_symbolic_parametric_model() (in module stormpy) BuilderOptions (class in stormpy)

C

cache() (FactorizedPolynomial method), [1], [2] can_have_nondeterminism() (DFT_double method) (DFT_ratfunc method) carl_version() (in module stormpy.pycarl) cast_to_double_datatype() (Scheduler method), [1] (SchedulerExact method), [1] (SchedulerParametric method), [1] cast_to_exact_datatype() (Scheduler method), [1] (SchedulerExact method), [1] (SchedulerParametric method), [1] cast_to_interval_datatype() (Scheduler method), [1] (SchedulerExact method), [1] cast_to_parametric_datatype() (Scheduler method), [1] (SchedulerExact method), [1] (SchedulerParametric method), [1] Ceil (OperatorType attribute), [1] ceil() (in module stormpy.pycarl) (in module stormpy.pycarl.cln) (in module stormpy.pycarl.gmp) center() (Interval method), [1], [2] CENTERSAT (RegionResult attribute) CENTERVIOLATED (RegionResult attribute) check() (BeliefExplorationModelCheckerDouble method) (PCtmcExactInstantiationChecker method) (PCtmcInstantiationChecker method) (PDtmcExactInstantiationChecker method) (PDtmcInstantiationChecker method) (PMdpExactInstantiationChecker method) (PMdpInstantiationChecker method) (SmtSolver method) check_interval_mdp() (in module stormpy) check_model_dd() (in module stormpy) check_model_hybrid() (in module stormpy) check_model_sparse() (in module stormpy) check_region() (RegionModelChecker method) check_threshold_feasible (SMTCounterExampleGeneratorOptions property) check_transitions_outside (SubsystemBuilderOptions property) check_valid() (JaniModel method), [1] check_with_environment() (BeliefExplorationModelCheckerDouble method) check_with_environment_and_pre_processing_environment() (BeliefExplorationModelCheckerDouble method) check_with_preprocessing_environment() (BeliefExplorationModelCheckerDouble method) CheckTask (class in stormpy) choice_labeling (SparseExactModelComponents property), [1] (SparseIntervalModelComponents property), [1] (SparseModelComponents property), [1] (SparseParametricModelComponents property), [1] choice_origins (SparseExactModelComponents property), [1] (SparseIntervalModelComponents property), [1] (SparseModelComponents property), [1] (SparseParametricModelComponents property), [1] ChoiceLabeling (class in stormpy) (class in stormpy.storage) ChoiceOrigins (class in stormpy) (class in stormpy.storage) clear_monomial_pool() (in module stormpy.pycarl) clear_pools() (in module stormpy.pycarl) clear_variable_pool() (in module stormpy.pycarl) clipping_grid_res (BeliefExplorationModelCheckerOptionsDouble property) clone() (Formula method), [1] (JaniOrderedAssignments method), [1] (SymbolicExactQuantitativeCheckResult method) (SymbolicParametricQuantitativeCheckResult method) (SymbolicQuantitativeCheckResult method) coeff (Term property), [1] coefficient (FactorizedPolynomial property), [1], [2] collect_information() (in module stormpy) (in module stormpy.storage) color (JaniEdge property), [1] column (ExactSparseMatrixEntry property), [1] (IntervalSparseMatrixEntry property), [1] (ParametricSparseMatrixEntry property), [1] (SparseMatrixEntry property), [1] commands (PrismModule property), [1] comparison_type (OperatorFormula property), [1] ComparisonType (class in stormpy) (class in stormpy.logic) complement() (Interval method), [1], [2] compute_action_support() (Scheduler method), [1] (SchedulerExact method), [1] (SchedulerInterval method), [1] (SchedulerParametric method), [1]

compute_all_until_probabilities() (in module stormpy) compute_dependency_conflicts() (in module stormpy.dft) compute_expected_number_of_visits() (in module stormpy) compute_extremum() (RegionModelChecker method) compute_indices() (DdMetaVariable_Sylvan method), [1] compute_prob01_states() (in module stormpy) compute_prob01max_states() (in module stormpy) compute_prob01min_states() (in module stormpy) compute_relevant_events() (in module stormpy.dft) compute_steady_state_distribution() (in module stormpy) compute_transient_probabilities() (in module stormpy) compute_winning_policy_for_initial_states() (IterativeQualitativeSearchSolverDouble method) compute_winning_region() (IterativeQualitativeSearchSolverDouble method) ConditionalFormula (class in stormpy) (class in stormpy.logic) Conjunction() (Expression static method), [1] constant_part() (FactorizedPolynomial method), [1], [2] (FactorizedRationalFunction method), [1], [2] (Polynomial method), [1], [2] (RationalFunction method), [1], [2] constants (JaniModel property), [1] (PrismProgram property), [1] Constraint (class in stormpy.pycarl.cln.formula) (class in stormpy.pycarl.gmp.formula) CONSTRAINT (FormulaType attribute) ConstraintCollector (class in stormpy) construct_submodel() (in module stormpy) contains() (Interval method), [1], [2] contains_label() (ItemLabeling method), [1] contains_variable() (Expression method), [1] contains_variables() (Expression method), [1] CONTINUE (SimulationTraceResult attribute) continue_after_first_counterexample (SMTCounterExampleGeneratorOptions property) continue_unfolding() (BeliefExplorationModelCheckerDouble method) convert_to_cln() (in module stormpy.pycarl.convert) convert_to_ctmc() (SparseExactMA method), [1] (SparseIntervalMA method), [1] (SparseMA method), [1] convert_to_gmp() (in module stormpy.pycarl.convert) convertible_to_ctmc (SparseExactMA property), [1] (SparseIntervalMA property), [1] (SparseMA property), [1] count() (milliseconds method) create() (RandomGenerator static method) create_boolean() (ExpressionManager method), [1] create_boolean_variable() (ExpressionManager method), [1] create_deadlock_properties() (GSPNToJaniBuilder method) create_downward_closure() (PolytopeDouble method), [1] (PolytopeExact method), [1] create_factorized_polynomial() (in module stormpy.pycarl.cln) (in module stormpy.pycarl.gmp) create_filter_initial_states_sparse() (in module stormpy) create_filter_initial_states_symbolic() (in module stormpy) create_filter_symbolic() (in module stormpy) create_from_string() (ParameterRegion static method) create_integer() (ExpressionManager method), [1] create_integer_variable() (ExpressionManager method), [1] create_interactive_mc() (in module stormpy.pomdp) create_iterative_qualitative_search_solver_Double() (in module stormpy.pomdp) create_monomial() (in module stormpy.pycarl) create_nondeterminstic_belief_tracker() (in module stormpy.pomdp) create_observation_trace_unfolder() (in module stormpy.pomdp) create_rational() (ExpressionManager method), [1] create_rational_variable() (ExpressionManager method), [1] create_region_checker() (in module stormpy.pars) CTMC (JaniModelType attribute) (ModelType attribute), [1], [2] (PrismModelType attribute), [1] CTMDP (JaniModelType attribute) (PrismModelType attribute), [1] CumulativeRewardFormula (class in stormpy) (class in stormpy.logic) cut_time (SMTCounterExampleGeneratorStats property) cut_zero_gap (BeliefExplorationModelCheckerOptionsDouble property) cutoff_schedulers (BeliefExplorationPomdpModelCheckerResultDouble property)

D

DD (QuotientFormat attribute) dd_manager (Dd_Sylvan property), [1] Dd_Sylvan (class in stormpy) (class in stormpy.storage) DdManager_Sylvan (class in stormpy) (class in stormpy.storage) DdMetaVariable_Sylvan (class in stormpy) (class in stormpy.storage) DdMetaVariableType (class in stormpy) (class in stormpy.storage) deadlock_label (SubsystemBuilderReturnTypeDouble property) (SubsystemBuilderReturnTypeExact property) (SubsystemBuilderReturnTypeRatFunc property) decode_automaton_and_edge_index() (JaniModel static method), [1] define_constants() (JaniModel method), [1] (PrismProgram method), [1] defined (JaniConstant property), [1] (PrismConstant property), [1] (SchedulerChoice property), [1] (SchedulerChoiceExact property), [1] (SchedulerChoiceInterval property), [1] (SchedulerChoiceParametric property), [1] definition (PrismConstant property), [1] degree() (Polynomial method), [1], [2] DELETE_LABELS (EliminationLabelBehavior attribute) denominator (FactorizedRationalFunction property), [1], [2] (Rational property), [1], [2] (RationalFunction property), [1], [2] denominator() (in module stormpy.pycarl.cln) (in module stormpy.pycarl.gmp) dependent_events (DFTDependency_double property) (DFTDependency_ratfunc property) DEPTH (ApproximationHeuristic attribute) derive() (FactorizedPolynomial method), [1], [2] (FactorizedRationalFunction method), [1], [2] (Polynomial method), [1], [2] (RationalFunction method), [1], [2] deserialize() (in module stormpy.pycarl.parse) destinations (JaniEdge property), [1] (JaniTemplateEdge property), [1] deterministic (Scheduler property), [1] (SchedulerChoice property), [1] (SchedulerChoiceExact property), [1] (SchedulerChoiceInterval property), [1] (SchedulerChoiceParametric property), [1] (SchedulerExact property), [1] (SchedulerInterval property), [1] (SchedulerParametric property), [1]

development (Version attribute) DFT_double (class in stormpy.dft) DFT_ratfunc (class in stormpy.dft) DFTBE_double (class in stormpy.dft) DFTBE_ratfunc (class in stormpy.dft) DFTDependency_double (class in stormpy.dft) DFTDependency_ratfunc (class in stormpy.dft) DFTElement_double (class in stormpy.dft) DFTElement_ratfunc (class in stormpy.dft) DFTElementType (class in stormpy.dft) DftIndependentModule (class in stormpy.dft) DFTInstantiator (class in stormpy.dft) DFTSimulator_double (class in stormpy.dft) DFTSimulator_ratfunc (class in stormpy.dft) DFTState_double (class in stormpy.dft) DFTState_ratfunc (class in stormpy.dft) DFTStateInfo (class in stormpy.dft) DftSymmetries (class in stormpy.dft) diameter() (Interval method), [1], [2] DiceStringVisitor (class in stormpy) (class in stormpy.storage) difference() (Interval method), [1], [2] dimension() (NondeterministicBeliefTrackerDoubleSparse method) (NondeterministicBeliefTrackerExactSparse method) DirectEncodingOptions (class in stormpy) DirectEncodingParserOptions (class in stormpy) Disjunction() (Expression static method), [1] distance (Path property) Distribution (class in stormpy) (class in stormpy.storage) DistributionExact (class in stormpy) (class in stormpy.storage) DistributionInterval (class in stormpy) (class in stormpy.storage) div() (in module stormpy.pycarl) (in module stormpy.pycarl.cln) (in module stormpy.pycarl.gmp) (Interval method), [1], [2] Divide (OperatorType attribute), [1] Divide() (Expression static method), [1] dontcare() (DFTState_double method) (DFTState_ratfunc method) DTMC (JaniModelType attribute) (ModelType attribute), [1], [2] (PrismModelType attribute), [1] DtmcParameterLiftingModelChecker (class in stormpy.pars)

E

edges (JaniAutomaton property), [1] eigen (EquationSolverType attribute) elements() (DftIndependentModule method) eliminate_ECs() (in module stormpy) eliminate_non_markovian_chains() (in module stormpy) eliminate_reward_accumulations() (in module stormpy) (in module stormpy.storage) elimination (EquationSolverType attribute) EliminationLabelBehavior (class in stormpy) empty() (JaniVariableSet method), [1] emptyInterval() (Interval static method), [1], [2] encode_automaton_and_edge_index() (JaniModel static method), [1] encode_reachability (SMTCounterExampleGeneratorOptions property) EndComponentEliminatorReturnTypeDouble (class in stormpy) Environment (class in stormpy) EQ (Relation attribute) Eq() (Expression static method), [1] Equal (OperatorType attribute), [1] EquationSolverType (class in stormpy) erase_variable() (JaniVariableSet method), [1] evaluate() (FactorizedPolynomial method), [1], [2] (FactorizedRationalFunction method), [1], [2] (Polynomial method), [1], [2] (RationalFunction method), [1], [2] evaluate_as_bool() (Expression method), [1] evaluate_as_double() (Expression method), [1] evaluate_as_int() (Expression method), [1] evaluate_as_rational() (Expression method), [1] EventuallyFormula (class in stormpy) (class in stormpy.logic) ExactCheckTask (class in stormpy) ExactSparseMatrix (class in stormpy) (class in stormpy.storage) ExactSparseMatrixBuilder (class in stormpy) (class in stormpy.storage) ExactSparseMatrixEntry (class in stormpy) (class in stormpy.storage) ExactSparseMatrixRows (class in stormpy) (class in stormpy.storage) EXISTS (FormulaType attribute) exists_inhibition_arc() (Transition method) exists_input_arc() (Transition method) exists_output_arc() (Transition method) EXISTSBOTH (RegionResult attribute) EXISTSSAT (RegionResult attribute) EXISTSVIOLATED (RegionResult attribute) exit_rates (SparseCtmc property), [1] (SparseExactCtmc property), [1] (SparseExactMA property), [1] (SparseExactModelComponents property), [1] (SparseIntervalCtmc property), [1] (SparseIntervalMA property), [1] (SparseIntervalModelComponents property), [1] (SparseMA property), [1] (SparseModelComponents property), [1] (SparseParametricModelComponents property), [1]

expand() (in module stormpy.pycarl.cln) (in module stormpy.pycarl.gmp) ExplicitDFTModelBuilder_double (class in stormpy.dft) ExplicitDFTModelBuilder_ratfunc (class in stormpy.dft) ExplicitExactQuantitativeCheckResult (class in stormpy) ExplicitModelBuilder (class in stormpy) ExplicitModelCheckerHintDouble (class in stormpy) ExplicitParametricModelBuilder (class in stormpy) ExplicitParametricQuantitativeCheckResult (class in stormpy) ExplicitParetoCurveCheckResultDouble (class in stormpy) ExplicitQualitativeCheckResult (class in stormpy) ExplicitQuantitativeCheckResult (class in stormpy) ExplicitStateLookup (class in stormpy) exploration_heuristic (BeliefExplorationModelCheckerOptionsDouble property) exploration_time_limit (BeliefExplorationModelCheckerOptionsDouble property) exponents (Monomial property) export_dft_json_file() (in module stormpy.dft) export_dft_json_string() (in module stormpy.dft) export_gspn_pnml_file() (GSPN method) export_gspn_pnpro_file() (GSPN method) export_lookup() (ExplicitModelBuilder method) (ExplicitParametricModelBuilder method) export_parametric_dft_json_file() (in module stormpy.dft) export_parametric_dft_json_string() (in module stormpy.dft) export_to_drn() (in module stormpy) Expression (class in stormpy) (class in stormpy.storage) expression (JaniAssignment property), [1] (PrismAssignment property), [1] (PrismLabel property), [1] expression_manager (JaniModel property), [1] (PrismProgram property), [1] (Valuation property), [1] expression_variable (JaniConstant property), [1] (JaniVariable property), [1] (PrismConstant property), [1] (PrismVariable property), [1] ExpressionManager (class in stormpy) (class in stormpy.storage) ExpressionParser (class in stormpy) (class in stormpy.storage) ExpressionType (class in stormpy) (class in stormpy.storage) extend() (ObservationTraceUnfolderDouble method) (ObservationTraceUnfolderExact method) (ObservationTraceUnfolderRf method)

F

Factorization (class in stormpy.pycarl.cln) (class in stormpy.pycarl.gmp) factorization() (FactorizedPolynomial method), [1], [2] FactorizedPolynomial (class in stormpy) (class in stormpy.pycarl.cln) (class in stormpy.pycarl.gmp) FactorizedRationalFunction (class in stormpy) (class in stormpy.pycarl.cln) (class in stormpy.pycarl.gmp) failable() (DFTState_double method) (DFTState_ratfunc method) FailableElement (class in stormpy.dft) FailableElements (class in stormpy.dft) FailableIterator (class in stormpy.dft) failed() (DFTState_double method) (DFTState_ratfunc method) failsafe() (DFTState_double method) (DFTState_ratfunc method) FALSE (FormulaType attribute) finalize() (JaniModel method), [1]

fire() (Transition method) fix_deadlocks (SubsystemBuilderOptions property) fixed_counter (PomdpMemoryPattern attribute) fixed_ring (PomdpMemoryPattern attribute) FlatSet (class in stormpy) flatten() (PrismProgram method), [1] flatten_composition() (JaniModel method), [1] Floor (OperatorType attribute), [1] floor() (in module stormpy.pycarl) (in module stormpy.pycarl.cln) (in module stormpy.pycarl.gmp) FORALL (FormulaType attribute) Formula (class in stormpy) (class in stormpy.logic) (class in stormpy.pycarl.cln.formula) (class in stormpy.pycarl.gmp.formula) formulas (ModelFormulasPair property) FormulaType (class in stormpy.pycarl.formula) full (PomdpFscApplicationMode attribute) (PomdpMemoryPattern attribute) fully_static() (DftIndependentModule method)

G

GameFormula (class in stormpy) (class in stormpy.logic) gap_threshold_init (BeliefExplorationModelCheckerOptionsDouble property) gather_derivatives() (in module stormpy.pars) gather_variables() (FactorizedPolynomial method), [1], [2] (FactorizedRationalFunction method), [1], [2] (Polynomial method), [1], [2] (RationalFunction method), [1], [2] gauss_seidel (NativeLinearEquationSolverMethod attribute) GEQ (ComparisonType attribute), [1] (Relation attribute) Geq() (Expression static method), [1] get() (AddIterator_Sylvan_Double method), [1] (BitVector method), [1] (SparseBeliefStateDouble method) (SparseBeliefStateExact method) get_action_name() (PrismProgram method), [1] get_as_variable_to_expression_map() (PrismUpdate method), [1] get_assignment() (PrismUpdate method), [1] get_automaton() (JaniModel method), [1] get_automaton_index() (JaniModel method), [1] get_boolean_value() (ModelReference method) (SimpleValuation method), [1] (StateValuation method), [1] get_boolean_values_states() (StateValuation method), [1] get_boolean_variable() (PrismModule method), [1] get_bound() (RegionModelChecker method) get_bound_all_states() (DtmcParameterLiftingModelChecker method) (MdpParameterLiftingModelChecker method) get_capacity() (Place method) get_choice() (Scheduler method), [1] (SchedulerChoice method), [1] (SchedulerChoiceExact method), [1] (SchedulerChoiceInterval method), [1] (SchedulerChoiceParametric method), [1] (SchedulerExact method), [1] (SchedulerInterval method), [1] (SchedulerParametric method), [1] get_choice_index() (SparseExactMdp method), [1] (SparseIntervalMdp method), [1] (SparseMdp method), [1] get_choice_info() (ChoiceOrigins method), [1] get_choices() (ChoiceLabeling method), [1] get_command_indices_by_action_index() (PrismModule method), [1] get_command_set() (PrismChoiceOrigins method), [1] get_constant() (JaniModel method), [1] (PrismProgram method), [1] get_constraint() (Formula method), [1] get_current_belief_support() (BeliefSupportTrackerDouble method) (BeliefSupportTrackerExact method) get_current_row_group_count() (ExactSparseMatrixBuilder method), [1] (IntervalSparseMatrixBuilder method), [1] (ParametricSparseMatrixBuilder method), [1] (SparseMatrixBuilder method), [1] get_deterministic_choice() (SchedulerChoice method), [1] (SchedulerChoiceExact method), [1] (SchedulerChoiceInterval method), [1] (SchedulerChoiceParametric method), [1] get_distance() (ShortestPathsGenerator method) get_edge_index_set() (JaniChoiceOrigins method), [1] get_element() (DFT_double method) (DFT_ratfunc method) get_element_by_name() (DFT_double method) (DFT_ratfunc method) get_expression() (AtomicExpressionFormula method), [1] (Variable method), [1] get_group() (DftSymmetries method) get_id() (Place method) (Transition method) get_identifier_info() (ChoiceOrigins method), [1] get_immediate_transition() (GSPN method) get_immediate_transitions() (GSPN method) get_implication_conclusion() (Formula method), [1] get_implication_premise() (Formula method), [1] get_inhibition_arc_multiplicity() (Transition method) get_inhibition_places() (Transition method) get_initial_marking() (GSPN method) get_input_arc_multiplicity() (Transition method) get_input_places() (Transition method) get_integer_value() (ModelReference method) (SimpleValuation method), [1] (StateValuation method), [1] get_integer_values_states() (StateValuation method), [1] get_integer_variable() (PrismModule method), [1] get_interactive_belief_explorer() (BeliefExplorationModelCheckerDouble method) get_interactive_result() (BeliefExplorationModelCheckerDouble method) get_ite_condition() (Formula method), [1] get_ite_first_case() (Formula method), [1] get_ite_second_case() (Formula method), [1] get_json() (StateValuation method), [1] get_label_expression() (PrismProgram method), [1] get_labels() (ItemLabeling method), [1] get_labels_of_choice() (ChoiceLabeling method), [1] get_labels_of_state() (StateLabeling method), [1] get_last_column() (ExactSparseMatrixBuilder method), [1] (IntervalSparseMatrixBuilder method), [1] (ParametricSparseMatrixBuilder method), [1] (SparseMatrixBuilder method), [1] get_last_row() (ExactSparseMatrixBuilder method), [1] (IntervalSparseMatrixBuilder method), [1] (ParametricSparseMatrixBuilder method), [1] (SparseMatrixBuilder method), [1] get_location_index() (JaniAutomaton method), [1] get_maximal_end_components() (in module stormpy) (in module stormpy.storage) get_meta_variable() (DdManager_Sylvan method), [1] get_model() (ExplicitDFTModelBuilder_double method) (ExplicitDFTModelBuilder_ratfunc method) get_module() (PrismProgram method), [1] get_module_indices_by_action_index() (PrismProgram method), [1] get_name() (GSPN method) (Place method) (Transition method) get_negation_subformula() (Formula method), [1] get_nr_available_actions() (SparseExactMdp method), [1] (SparseIntervalMdp method), [1] (SparseMdp method), [1] (SparseParametricMdp method), [1]

get_nr_of_states() (StateValuation method), [1] get_number_of_identifiers() (ChoiceOrigins method), [1] 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_timed_transitions() (GSPN method) get_observation() (SparseExactPomdp method), [1] (SparseIntervalPomdp method), [1] (SparseParametricPomdp method), [1] (SparsePomdp method), [1] get_operand() (Expression method), [1] get_output_arc_multiplicity() (Transition method) get_output_places() (Transition method) get_overapproximation() (ParetoCurveCheckResultDouble method) get_parameters() (in module stormpy.dft) get_partial_model() (ExplicitDFTModelBuilder_double method) (ExplicitDFTModelBuilder_ratfunc method) get_partitions() (GSPN method) get_path_as_list() (ShortestPathsGenerator method) get_place() (GSPN method) get_places() (GSPN method) get_player_of_state() (SparseExactSmg method), [1] (SparseIntervalSmg method), [1] (SparseSmg method), [1] get_priority() (Transition method) get_rate() (TimedTransition method) get_rational_value() (ModelReference method) (StateValuation method), [1] get_rational_values_states() (StateValuation method), [1] get_reachable_states() (in module stormpy) get_row() (ExactSparseMatrix method), [1] (IntervalSparseMatrix method), [1] (ParametricSparseMatrix method), [1] (SparseMatrix method), [1] get_row_group_end() (ExactSparseMatrix method), [1] (IntervalSparseMatrix method), [1] (ParametricSparseMatrix method), [1] (SparseMatrix method), [1] get_row_group_start() (ExactSparseMatrix method), [1] (IntervalSparseMatrix method), [1] (ParametricSparseMatrix method), [1] (SparseMatrix method), [1] get_rows_for_group() (ExactSparseMatrix method), [1] (IntervalSparseMatrix method), [1] (ParametricSparseMatrix method), [1] (SparseMatrix method), [1] get_split_suggestion() (RegionModelChecker method) get_state() (DFTSimulator_double method) (DFTSimulator_ratfunc method) get_state_action_reward() (SparseExactRewardModel method), [1] (SparseIntervalRewardModel method), [1] (SparseParametricRewardModel method), [1] (SparseRewardModel method), [1] get_state_player_indications() (SparseExactSmg method), [1] (SparseIntervalSmg method), [1] (SparseSmg method), [1] get_state_reward() (SparseExactRewardModel method), [1] (SparseIntervalRewardModel method), [1] (SparseParametricRewardModel method), [1] (SparseRewardModel method), [1] get_states() (ShortestPathsGenerator method) (StateLabeling method), [1] get_status() (BeliefExplorationModelCheckerDouble method) get_string() (StateValuation method), [1] get_subformulas() (Formula method), [1] get_synchronizing_action_indices() (PrismProgram method), [1] get_time() (DFTSimulator_double method) (DFTSimulator_ratfunc method) get_timed_transition() (GSPN method) get_timed_transitions() (GSPN method) get_transition() (GSPN method) get_truth_values() (ExplicitQualitativeCheckResult method) (SymbolicQualitativeCheckResult method) get_undefined_constants() (PrismProgram method), [1] get_underapproximation() (ParetoCurveCheckResultDouble method) get_value() (SimpleValuation method), [1] (StateValuation method), [1] get_values() (ExplicitExactQuantitativeCheckResult method) (ExplicitParametricQuantitativeCheckResult method) (ExplicitQuantitativeCheckResult method) (HybridExactQuantitativeCheckResult method) (HybridParametricQuantitativeCheckResult method) (HybridQuantitativeCheckResult method) (SymbolicQuantitativeCheckResult method) get_values_states() (StateValuation method), [1] get_variable() (ExpressionManager method), [1] get_variable_by_expr_variable() (JaniVariableSet method), [1] get_variable_by_name() (JaniVariableSet method), [1] get_variables() (Expression method), [1] (ExpressionManager method), [1] (PrismProgram method), [1] get_vertices_clockwise() (PolytopeDouble method), [1] (PolytopeExact method), [1] get_weight() (ImmediateTransition method) get_zero_reward_states() (SparseExactRewardModel method), [1] (SparseIntervalRewardModel method), [1] (SparseRewardModel method), [1] global_boolean_variables (PrismProgram property), [1] global_index (PrismCommand property), [1] (PrismUpdate property), [1] global_integer_variables (PrismProgram property), [1] global_variables (JaniModel property), [1] GloballyFormula (class in stormpy) (class in stormpy.logic) gmmxx (EquationSolverType attribute) graph_preserving_constraints (ConstraintCollector property) GREATER (ComparisonType attribute), [1] Greater (OperatorType attribute), [1] GREATER (Relation attribute) Greater() (Expression static method), [1] GreaterOrEqual (OperatorType attribute), [1] GSPN (class in stormpy.gspn) GSPNBuilder (class in stormpy.gspn) GSPNParser (class in stormpy.gspn) GSPNToJaniBuilder (class in stormpy.gspn) guard (JaniEdge property), [1] (JaniTemplateEdge property), [1] guard_expression (PrismCommand property), [1]

H

HA (JaniModelType attribute) has_bitvector_type() (Variable method), [1] has_boolean_type() (Expression method), [1] (Variable method), [1] has_bound (OperatorFormula property), [1] has_cln() (in module stormpy.pycarl) has_constant() (PrismProgram method), [1] has_converged() (BeliefExplorationModelCheckerDouble method) has_infinite_server_semantics() (TimedTransition method) has_initial_states_expression (PrismProgram property), [1] has_integer_type() (Expression method), [1] (Variable method), [1] has_k_server_semantics() (TimedTransition method) has_label() (PrismProgram method), [1] has_lower_bound (BoundedUntilFormula property), [1] has_module_with_inner_action_overlapping_guard() (OverlappingGuardAnalyser method), [1] has_numerical_type() (Variable method), [1] has_observation_valuations() (SparseExactPomdp method), [1] (SparseIntervalPomdp method), [1] (SparsePomdp method), [1] has_optimality_type (OperatorFormula property), [1] has_parser() (in module stormpy.pycarl) has_potential_modeling_issues() (in module stormpy.dft) has_rational_type() (Expression method), [1] (Variable method), [1] has_restricted_capacity() (Place method) has_reward_model() (PrismProgram method), [1] has_reward_name() (RewardOperator method), [1] has_silent_action() (JaniEdge method), [1]

has_single_server_semantics() (TimedTransition method) has_standard_composition() (JaniModel method), [1] has_state_action_rewards (SparseExactRewardModel property), [1] (SparseIntervalRewardModel property), [1] (SparseParametricRewardModel property), [1] (SparseRewardModel property), [1] (SymbolicSylvanParametricRewardModel property), [1] (SymbolicSylvanRewardModel property), [1] has_state_label() (StateLabeling method), [1] has_state_rewards (SparseExactRewardModel property), [1] (SparseIntervalRewardModel property), [1] (SparseParametricRewardModel property), [1] (SparseRewardModel property), [1] (SymbolicSylvanParametricRewardModel property), [1] (SymbolicSylvanRewardModel property), [1] has_transition_rewards (SparseExactRewardModel property), [1] (SparseIntervalRewardModel property), [1] (SparseParametricRewardModel property), [1] (SparseRewardModel property), [1] (SymbolicSylvanParametricRewardModel property), [1] (SymbolicSylvanRewardModel property), [1] has_trivial_row_grouping (ExactSparseMatrix property), [1] (IntervalSparseMatrix property), [1] (ParametricSparseMatrix property), [1] (SparseMatrix property), [1] has_undefined_constants (JaniModel property), [1] (PrismProgram property), [1] HybridExactQuantitativeCheckResult (class in stormpy) HybridParametricQuantitativeCheckResult (class in stormpy) HybridQuantitativeCheckResult (class in stormpy)

I

I_Minus_P (MatrixFormat attribute) id (DFTElement_double property) (DFTElement_ratfunc property) (SparseExactModelAction property), [1] (SparseExactModelState property), [1] (SparseIntervalModelAction property), [1] (SparseIntervalModelState property), [1] (SparseModelAction property), [1] (SparseModelState property), [1] (SparseParametricModelAction property), [1] (SparseParametricModelState property), [1] (Variable property) identifier() (Expression method), [1] IFF (FormulaType attribute) Iff (OperatorType attribute), [1] Iff() (Expression static method), [1] immediate_transition_id_to_transition_id() (GSPN static method) ImmediateTransition (class in stormpy.gspn) IMPLIES (FormulaType attribute) Implies (OperatorType attribute), [1] Implies() (Expression static method), [1] index (Variable property), [1] induced_mc_from_scheduler (BeliefExplorationPomdpModelCheckerResultDouble property) INFTY (BoundType attribute) init_expression (JaniVariable property), [1] initial_location_indices (JaniAutomaton property), [1] initial_states_expression (PrismProgram property), [1] initial_states_restriction (JaniAutomaton property), [1] (JaniModel property), [1] initial_value_expression (PrismVariable property), [1] insert() (FlatSet method) insert_set() (FlatSet method) install_signal_handlers() (in module stormpy) InstantaneousRewardFormula (class in stormpy) (class in stormpy.logic) instantiate() (DFTInstantiator method) (ModelInstantiator method) (PartialPCtmcInstantiator method) (PartialPDtmcInstantiator method) (PartialPMaInstantiator method) (PartialPMdpInstantiator method) (PCtmcInstantiator method) (PDtmcInstantiator method) (PMaInstantiator method) (PMdpInstantiator method) instantiate_constants() (SymbolicModelDescription method) Int (DdMetaVariableType attribute), [1] INT (VariableType attribute) Integer (class in stormpy.pycarl.cln) (class in stormpy.pycarl.gmp) integer_variables (PrismModule property), [1] integralPart() (Interval method), [1], [2] interactive_unfolding (BeliefExplorationModelCheckerOptionsDouble property) intersect() (Interval method), [1], [2] intersectsWith() (Interval method), [1], [2] Interval (class in stormpy.pycarl) (class in stormpy.pycarl.cln) (class in stormpy.pycarl.gmp) interval_iteration (MinMaxMethod attribute) (NativeLinearEquationSolverMethod attribute) IntervalSparseMatrix (class in stormpy) (class in stormpy.storage) IntervalSparseMatrixBuilder (class in stormpy) (class in stormpy.storage) IntervalSparseMatrixEntry (class in stormpy) (class in stormpy.storage) IntervalSparseMatrixRows (class in stormpy) (class in stormpy.storage) INVALID (SimulationStepResult attribute) (SimulationTraceResult attribute)

invalid() (DFTState_double method) (DFTState_ratfunc method) inverse() (Interval method), [1], [2] is_boolean (ExpressionType property), [1] is_bounded_until_formula (Formula property), [1] is_constant() (FactorizedPolynomial method), [1], [2] (FactorizedRationalFunction method), [1], [2] (Polynomial method), [1], [2] (RationalFunction method), [1], [2] (Term method), [1] is_deterministic_model (PrismProgram property), [1] is_due_dependency() (FailableElement method) is_enabled() (Transition method) is_eventually_formula (Formula property), [1] is_exploring() (BeliefExplorationModelCheckerDouble method) is_function_application (Expression property), [1] is_game_formula (GameFormula property), [1] is_integer (ExpressionType property), [1] is_jani_choice_origins() (ChoiceOrigins method), [1] is_jani_model (SymbolicModelDescription property) is_labeled (PrismCommand property), [1] is_literal() (Expression method), [1] is_minus_one() (Rational method) is_multi_objective_formula (Formula property), [1] is_multidimensional (BoundedUntilFormula property), [1] is_no_variable (Variable property) is_one() (FactorizedPolynomial method), [1], [2] (Rational method) (Term method), [1] is_prism_choice_origins() (ChoiceOrigins method), [1] is_prism_program (SymbolicModelDescription property) is_probability_operator (Formula property), [1] is_rational (ExpressionType property), [1] is_relevant() (RelevantEvents method) is_result_ready() (BeliefExplorationModelCheckerDouble method) is_reward_operator (Formula property), [1] is_subset_of() (FlatSet method) is_until_formula (Formula property), [1] is_valid (SparseBeliefStateDouble property) (SparseBeliefStateExact property) is_valid() (GSPN method) is_variable() (Expression method), [1] is_well_formed() (in module stormpy.dft) isClosedInterval() (Interval method), [1], [2] isEmpty() (Interval method), [1], [2] isHalfBounded() (Interval method), [1], [2] isInfinite() (Interval method), [1], [2] isInteger() (in module stormpy.pycarl) (in module stormpy.pycarl.cln) (in module stormpy.pycarl.gmp) isNegative() (Interval method), [1], [2] isOne() (Interval method), [1], [2] isOpenInterval() (Interval method), [1], [2] isPointInterval() (Interval method), [1], [2] isPositive() (Interval method), [1], [2] isProperSubset() (Interval method), [1], [2] isSemiNegative() (Interval method), [1], [2] isSemiPositive() (Interval method), [1], [2] isSubset() (Interval method), [1], [2] isUnbounded() (Interval method), [1], [2] isZero() (Interval method), [1], [2] ITE (FormulaType attribute) Ite (OperatorType attribute), [1] ItemLabeling (class in stormpy) (class in stormpy.storage) iterations (SMTCounterExampleGeneratorStats property) IterativeQualitativeSearchOptions (class in stormpy.pomdp) IterativeQualitativeSearchSolverDouble (class in stormpy.pomdp)

J

jacobi (NativeLinearEquationSolverMethod attribute) JaniAssignment (class in stormpy) (class in stormpy.storage) JaniAutomaton (class in stormpy) (class in stormpy.storage) JaniChoiceOrigins (class in stormpy) (class in stormpy.storage) JaniConstant (class in stormpy) (class in stormpy.storage) JaniEdge (class in stormpy) (class in stormpy.storage) JaniEdgeDestination (class in stormpy) (class in stormpy.storage) JaniInformationObject (class in stormpy) (class in stormpy.storage) JaniLocation (class in stormpy) (class in stormpy.storage) JaniLocationExpander (class in stormpy) (class in stormpy.storage)

JaniModel (class in stormpy) (class in stormpy.storage) JaniModelType (class in stormpy) JaniOrderedAssignments (class in stormpy) (class in stormpy.storage) JaniScopeChanger (class in stormpy) (class in stormpy.storage) JaniTemplateEdge (class in stormpy) (class in stormpy.storage) JaniTemplateEdgeDestination (class in stormpy) (class in stormpy.storage) JaniVariable (class in stormpy) (class in stormpy.storage) JaniVariableSet (class in stormpy) (class in stormpy.storage) JsonContainerDouble (class in stormpy.utility) JsonContainerRational (class in stormpy.utility)

K

KEEP_LABELS (EliminationLabelBehavior attribute) kept_actions (SubsystemBuilderReturnTypeDouble property) (SubsystemBuilderReturnTypeExact property) (SubsystemBuilderReturnTypeRatFunc property)

L

label (AtomicLabelFormula property), [1] label_unlabelled_commands() (PrismProgram method), [1] labeled (PrismCommand property), [1] labels (PrismProgram property), [1] (SparseExactModelAction property), [1] (SparseExactModelState property), [1] (SparseIntervalModelAction property), [1] (SparseIntervalModelState property), [1] (SparseModelAction property), [1] (SparseModelState property), [1] (SparseParametricModelAction property), [1] (SparseParametricModelState property), [1] last_winning_region (IterativeQualitativeSearchSolverDouble property) LayoutInfo (class in stormpy.gspn) left_subformula (BinaryPathFormula property), [1] (BoundedUntilFormula property), [1] LEQ (ComparisonType attribute), [1] (Relation attribute) Leq() (Expression static method), [1] LESS (ComparisonType attribute), [1] Less (OperatorType attribute), [1] LESS (Relation attribute) Less() (Expression static method), [1] LessOrEqual (OperatorType attribute), [1]

lhs (Constraint property), [1] lhs() (SimpleConstraint method), [1] (SimpleConstraintRatFunc method), [1] linear_programming (MinMaxMethod attribute) load_dft_galileo_file() (in module stormpy.dft) load_dft_json_file() (in module stormpy.dft) load_dft_json_string() (in module stormpy.dft) load_from_file() (BeliefSupportWinningRegion static method) load_from_string() (BitVector static method), [1] load_parametric_dft_galileo_file() (in module stormpy.dft) load_parametric_dft_json_file() (in module stormpy.dft) load_parametric_dft_json_string() (in module stormpy.dft) location_variable (JaniAutomaton property), [1] locations (JaniAutomaton property), [1] long (Version attribute) LongRunAvarageOperator (class in stormpy) (class in stormpy.logic) LongRunAverageRewardFormula (class in stormpy) (class in stormpy.logic) lookup() (ExplicitStateLookup method) lower() (Interval method), [1], [2] lower_bound (BeliefExplorationPomdpModelCheckerResultDouble property) lower_bound_expression (PrismIntegerVariable property), [1] lowest_value (DdMetaVariable_Sylvan property), [1] LTS (JaniModelType attribute)

M

MA (JaniModelType attribute) (ModelType attribute), [1], [2] (PrismModelType attribute), [1] major (Version attribute) make_canonic() (in module stormpy.pomdp) make_row_grouping_trivial() (ExactSparseMatrix method), [1] (IntervalSparseMatrix method), [1] (ParametricSparseMatrix method), [1] (SparseMatrix method), [1] make_simple() (in module stormpy.pomdp) make_sparse_model_builder() (in module stormpy) make_sparse_model_builder_exact() (in module stormpy) make_sparse_model_builder_parametric() (in module stormpy) make_standard_compliant() (JaniModel method), [1] make_variables_local() (JaniScopeChanger method), [1] manager (Expression property), [1] (Variable property), [1] markovian_states (SparseExactMA property), [1] (SparseExactModelComponents property), [1] (SparseIntervalMA property), [1] (SparseIntervalModelComponents property), [1] (SparseMA property), [1] (SparseModelComponents property), [1] (SparseParametricModelComponents property), [1] matrix (EndComponentEliminatorReturnTypeDouble property) MatrixFormat (class in stormpy.utility) Max (OperatorType attribute), [1] MaximalEndComponent (class in stormpy) (class in stormpy.storage) MaximalEndComponentDecomposition_double (class in stormpy) (class in stormpy.storage) MaximalEndComponentDecomposition_exact (class in stormpy) (class in stormpy.storage) MaximalEndComponentDecomposition_interval (class in stormpy) (class in stormpy.storage) MaximalEndComponentDecomposition_ratfunc (class in stormpy) (class in stormpy.storage) Maximize (OptimizationDirection attribute) maximum_counterexamples (SMTCounterExampleGeneratorOptions property) maximum_iterations (NativeSolverEnvironment property) maximum_iterations_after_counterexample (SMTCounterExampleGeneratorOptions property) MDP (JaniModelType attribute) (ModelType attribute), [1], [2] (PrismModelType attribute), [1] MdpParameterLiftingModelChecker (class in stormpy.pars) meets() (Interval method), [1], [2] memory_size (Scheduler property), [1] (SchedulerExact property), [1] (SchedulerInterval property), [1] (SchedulerParametric property), [1] memoryless (Scheduler property), [1] (SchedulerExact property), [1] (SchedulerInterval property), [1] (SchedulerParametric property), [1] MERGE_LABELS (EliminationLabelBehavior attribute) meta_variables (Dd_Sylvan property), [1] method (MinMaxSolverEnvironment property) (NativeSolverEnvironment property) milliseconds (class in stormpy.utility)

Min (OperatorType attribute), [1] Minimize (OptimizationDirection attribute) minmax_solver_environment (SolverEnvironment property) MinMaxMethod (class in stormpy) MinMaxSolverEnvironment (class in stormpy) minor (Version attribute) Minus (OperatorType attribute), [1] Minus() (Expression static method), [1] model (JaniChoiceOrigins property), [1] (ModelFormulasPair property) (SmtSolver property) (SubsystemBuilderReturnTypeDouble property) (SubsystemBuilderReturnTypeExact property) (SubsystemBuilderReturnTypeRatFunc property) model_checking() (in module stormpy) model_checking_time (SMTCounterExampleGeneratorStats property) model_type (JaniInformationObject property), [1] (JaniModel property), [1] (PrismProgram property), [1] ModelCheckerHint (class in stormpy) ModelFormulasPair (class in stormpy) ModelInstantiator (class in stormpy.pars) ModelReference (class in stormpy.utility) ModelType (class in stormpy) (class in stormpy.pars) (class in stormpy.storage) module stormpy stormpy.dft stormpy.exceptions stormpy.gspn stormpy.info stormpy.logic stormpy.pars stormpy.pomdp stormpy.pycarl stormpy.pycarl.cln stormpy.pycarl.cln.formula stormpy.pycarl.cln.parse stormpy.pycarl.convert stormpy.pycarl.formula stormpy.pycarl.gmp stormpy.pycarl.gmp.formula stormpy.pycarl.gmp.parse stormpy.pycarl.parse stormpy.storage stormpy.utility modules (PrismProgram property), [1] modules() (DFT_double method) (DFT_ratfunc method) modules_json() (in module stormpy.dft) Modulo (OperatorType attribute), [1] Modulo() (Expression static method), [1] Monomial (class in stormpy.pycarl) monomial (Term property), [1] MultiObjectiveFormula (class in stormpy) (class in stormpy.logic) Multiply() (Expression static method), [1] MUTEX (DFTElementType attribute)

N

name (ApproximationHeuristic property) (BinaryBooleanOperatorType property), [1] (BisimulationType property) (BoundType property) (ComparisonType property), [1] (DdMetaVariable_Sylvan property), [1] (DdMetaVariableType property), [1] (DFTElement_double property) (DFTElement_ratfunc property) (DFTElementType property) (EliminationLabelBehavior property) (EquationSolverType property) (FormulaType property) (JaniAutomaton property), [1] (JaniConstant property), [1] (JaniLocation property), [1] (JaniModel property), [1] (JaniModelType property) (JaniVariable property), [1] (MatrixFormat property) (MinMaxMethod property) (ModelType property), [1], [2] (NativeLinearEquationSolverMethod property) (OperatorType property), [1] (OptimizationDirection property) (PomdpFscApplicationMode property) (PomdpMemoryPattern property) (PrismConstant property), [1] (PrismLabel property), [1] (PrismModelType property), [1] (PrismModule property), [1] (PrismRewardModel property), [1] (PrismVariable property), [1] (Property property) (QuotientFormat property) (RegionResult property) (RegionResultHypothesis property) (Relation property) (SimulationStepResult property) (SimulationTraceResult property) (SmtCheckResult property) (Variable property), [1], [2] (VariableType property) native (EquationSolverType attribute) native_solver_environment (SolverEnvironment property) NativeLinearEquationSolverMethod (class in stormpy) NativeSolverEnvironment (class in stormpy) NEQ (Relation attribute) Neq() (Expression static method), [1] new_row_group() (ExactSparseMatrixBuilder method), [1] (IntervalSparseMatrixBuilder method), [1] (ParametricSparseMatrixBuilder method), [1] (SparseMatrixBuilder method), [1] new_to_old_action_mapping (SubsystemBuilderReturnTypeDouble property) (SubsystemBuilderReturnTypeExact property) (SubsystemBuilderReturnTypeRatFunc property) new_to_old_row_mapping (EndComponentEliminatorReturnTypeDouble property) new_to_old_state_mapping (SubsystemBuilderReturnTypeDouble property) (SubsystemBuilderReturnTypeExact property) (SubsystemBuilderReturnTypeRatFunc property)

no_weight_attached() (ImmediateTransition method) node_count (Dd_Sylvan property), [1] nominator (Rational property), [1], [2] (RationalFunction property), [1], [2] nondeterministic_choice_indices (SparseExactMA property), [1] (SparseExactMdp property), [1] (SparseIntervalMA property), [1] (SparseIntervalMdp property), [1] (SparseMA property), [1] (SparseMdp property), [1] (SparseParametricMA property), [1] (SparseParametricMdp property), [1] NondeterministicBeliefTrackerDoubleSparse (class in stormpy.pomdp) NondeterministicBeliefTrackerDoubleSparseOptions (class in stormpy.pomdp) NondeterministicBeliefTrackerExactSparse (class in stormpy.pomdp) NondeterministicBeliefTrackerExactSparseOptions (class in stormpy.pomdp) NoPicklingSupport NOT (FormulaType attribute) Not (OperatorType attribute), [1] NotEqual (OperatorType attribute), [1] nr_automata (JaniInformationObject property), [1] nr_be() (DFT_double method) (DFT_ratfunc method) nr_columns (ExactSparseMatrix property), [1] (IntervalSparseMatrix property), [1] (ParametricSparseMatrix property), [1] (SparseMatrix property), [1] nr_destinations (JaniEdge property), [1] nr_dynamic() (DFT_double method) (DFT_ratfunc method) nr_edges (JaniInformationObject property), [1] nr_elements() (DFT_double method) (DFT_ratfunc method) nr_entries (ExactSparseMatrix property), [1] (IntervalSparseMatrix property), [1] (ParametricSparseMatrix property), [1] (SparseMatrix property), [1] nr_modules (PrismProgram property), [1] nr_observations (SparseExactPomdp property), [1] (SparseIntervalPomdp property), [1] (SparseParametricPomdp property), [1] (SparsePomdp property), [1] nr_rows (ExactSparseMatrix property), [1] (IntervalSparseMatrix property), [1] (ParametricSparseMatrix property), [1] (SparseMatrix property), [1] nr_states (PomdpMemory property) nr_subformulas (MultiObjectiveFormula property), [1] nr_terms (Polynomial property), [1], [2] nr_transitions() (TransitionPartition method) nr_variables (JaniInformationObject property), [1] number_of_set_bits() (BitVector method), [1] number_of_unlabeled_commands (PrismProgram property), [1] numerator (FactorizedRationalFunction property), [1], [2] (Rational property), [1], [2] (RationalFunction property), [1], [2] numerator() (in module stormpy.pycarl.cln) (in module stormpy.pycarl.gmp)

O

observability_classes (SparseExactModelComponents property), [1] (SparseIntervalModelComponents property), [1] (SparseModelComponents property), [1] (SparseParametricModelComponents property), [1] observation_valuations (SparseExactPomdp property), [1] (SparseIntervalPomdp property), [1] (SparsePomdp property), [1] observations (SparseExactPomdp property), [1] (SparseIntervalPomdp property), [1] (SparseParametricPomdp property), [1] (SparsePomdp property), [1] ObservationTraceUnfolderDouble (class in stormpy.pomdp) ObservationTraceUnfolderExact (class in stormpy.pomdp) ObservationTraceUnfolderRf (class in stormpy.pomdp) obtain_beliefs() (NondeterministicBeliefTrackerDoubleSparse method) (NondeterministicBeliefTrackerExactSparse method) obtain_current_risk() (NondeterministicBeliefTrackerDoubleSparse method) (NondeterministicBeliefTrackerExactSparse method) obtain_last_observation() (NondeterministicBeliefTrackerDoubleSparse method) (NondeterministicBeliefTrackerExactSparse method) offset (Variable property), [1] old_to_new_state_mapping (EndComponentEliminatorReturnTypeDouble property)

operational() (DFTState_double method) (DFTState_ratfunc method) operator (Expression property), [1] OperatorFormula (class in stormpy) (class in stormpy.logic) OperatorType (class in stormpy) (class in stormpy.storage) optimality_type (OperatorFormula property), [1] optimistic_value_iteration (MinMaxMethod attribute) (NativeLinearEquationSolverMethod attribute) OptimizationDirection (class in stormpy) OR (BinaryBooleanOperatorType attribute), [1] (DFTElementType attribute) (FormulaType attribute) Or (OperatorType attribute), [1] Or() (Expression static method), [1] origins (SparseExactModelAction property), [1] (SparseIntervalModelAction property), [1] (SparseModelAction property), [1] (SparseParametricModelAction property), [1] OverlappingGuardAnalyser (class in stormpy) (class in stormpy.storage)

P

PAND (DFTElementType attribute) ParameterRegion (class in stormpy.pars) ParametricCheckTask (class in stormpy) ParametricSparseMatrix (class in stormpy) (class in stormpy.storage) ParametricSparseMatrixBuilder (class in stormpy) (class in stormpy.storage) ParametricSparseMatrixEntry (class in stormpy) (class in stormpy.storage) ParametricSparseMatrixRows (class in stormpy) (class in stormpy.storage) ParetoCurveCheckResultDouble (class in stormpy) parse() (ExpressionParser method), [1] (GSPNParser method) parse_constant_definitions() (SymbolicModelDescription method) parse_constants_string() (in module stormpy) parse_jani_model() (in module stormpy) parse_jani_model_from_string() (in module stormpy) parse_prism_program() (in module stormpy) parse_properties() (in module stormpy) parse_properties_for_jani_model() (in module stormpy) parse_properties_for_prism_program() (in module stormpy) parse_properties_without_context() (in module stormpy) ParserError partial (Scheduler property), [1] (SchedulerExact property), [1] (SchedulerInterval property), [1] (SchedulerParametric property), [1] PartialPCtmcInstantiator (class in stormpy.pars) PartialPDtmcInstantiator (class in stormpy.pars) PartialPMaInstantiator (class in stormpy.pars) PartialPMdpInstantiator (class in stormpy.pars) patch (Version attribute) Path (class in stormpy.utility) PathFormula (class in stormpy) (class in stormpy.logic) pause_unfolding() (BeliefExplorationModelCheckerDouble method) PCtmcExactInstantiationChecker (class in stormpy.pars) PCtmcInstantiationChecker (class in stormpy.pars) PCtmcInstantiator (class in stormpy.pars) PDEP (DFTElementType attribute) PDtmcExactInstantiationChecker (class in stormpy.pars) PDtmcInstantiationChecker (class in stormpy.pars) PDtmcInstantiator (class in stormpy.pars) perform_bisimulation() (in module stormpy) perform_sparse_bisimulation() (in module stormpy) perform_symbolic_bisimulation() (in module stormpy) PHA (JaniModelType attribute) Place (class in stormpy.gspn) player1_matrix (SparseExactModelComponents property), [1] (SparseIntervalModelComponents property), [1] (SparseModelComponents property), [1] (SparseParametricModelComponents property), [1] Plus (OperatorType attribute), [1] Plus() (Expression static method), [1] PMaInstantiator (class in stormpy.pars) PMdpExactInstantiationChecker (class in stormpy.pars) PMdpInstantiationChecker (class in stormpy.pars) PMdpInstantiator (class in stormpy.pars) policy_iteration (MinMaxMethod attribute) Polynomial (class in stormpy) (class in stormpy.pycarl.cln) (class in stormpy.pycarl.gmp) polynomial() (FactorizedPolynomial method), [1], [2] PolytopeDouble (class in stormpy) (class in stormpy.storage)

PolytopeExact (class in stormpy) (class in stormpy.storage) POMDP (ModelType attribute), [1], [2] (PrismModelType attribute), [1] PomdpFscApplicationMode (class in stormpy.pomdp) PomdpMemory (class in stormpy.pomdp) PomdpMemoryBuilder (class in stormpy.pomdp) PomdpMemoryPattern (class in stormpy.pomdp) pop() (SmtSolver method) POR (DFTElementType attribute) pow() (in module stormpy.pycarl) (in module stormpy.pycarl.cln) (in module stormpy.pycarl.gmp) Power (OperatorType attribute), [1] power_iteration (NativeLinearEquationSolverMethod attribute) precision (MinMaxSolverEnvironment property) (NativeSolverEnvironment property) precompute() (SMTCounterExampleGenerator static method) predecessorK (Path property) predecessorNode (Path property) prepare_for_analysis() (in module stormpy.dft) prepare_pomdp_for_qualitative_search_Double() (in module stormpy.pomdp) preprocess_symbolic_input() (in module stormpy) preserved_label_names (BuilderOptions property) print_info() (in module stormpy.pycarl) print_row() (ExactSparseMatrix method), [1] (IntervalSparseMatrix method), [1] (ParametricSparseMatrix method), [1] (SparseMatrix method), [1] priority (TransitionPartition property) PrismAssignment (class in stormpy) (class in stormpy.storage) PrismBooleanVariable (class in stormpy) (class in stormpy.storage) PrismChoiceOrigins (class in stormpy) (class in stormpy.storage) PrismCommand (class in stormpy) (class in stormpy.storage) PrismConstant (class in stormpy) (class in stormpy.storage) PrismIntegerVariable (class in stormpy) (class in stormpy.storage) PrismLabel (class in stormpy) (class in stormpy.storage) PrismModelType (class in stormpy) (class in stormpy.storage) PrismModule (class in stormpy) (class in stormpy.storage) PrismProgram (class in stormpy) (class in stormpy.storage) PrismRewardModel (class in stormpy) (class in stormpy.storage) PrismUpdate (class in stormpy) (class in stormpy.storage) PrismVariable (class in stormpy) (class in stormpy.storage) prob01max_states() (in module stormpy) prob01min_states() (in module stormpy) PROBABILITY (ApproximationHeuristic attribute) probability (JaniEdgeDestination property), [1] probability_expression (PrismUpdate property), [1] ProbabilityOperator (class in stormpy) (class in stormpy.logic) program (PrismChoiceOrigins property), [1] Property (class in stormpy) PTA (JaniModelType attribute) push() (SmtSolver method)

Q

query_action() (BeliefSupportWinningRegionQueryInterfaceDouble method) query_current_belief() (BeliefSupportWinningRegionQueryInterfaceDouble method) quotient() (in module stormpy.pycarl) (in module stormpy.pycarl.cln) (in module stormpy.pycarl.gmp)

QuotientFormat (class in stormpy)

R

random_step() (DFTSimulator_double method) (DFTSimulator_ratfunc method) RandomGenerator (class in stormpy.dft) rank (Variable property) rate (JaniEdge property), [1] rate_transitions (SparseExactModelComponents property), [1] (SparseIntervalModelComponents property), [1] (SparseModelComponents property), [1] (SparseParametricModelComponents property), [1] Rational (class in stormpy) (class in stormpy.pycarl.cln) (class in stormpy.pycarl.gmp) rational_function() (FactorizedRationalFunction method), [1], [2] rational_search (MinMaxMethod attribute) (NativeLinearEquationSolverMethod attribute) RationalFunction (class in stormpy) (class in stormpy.pycarl.cln) (class in stormpy.pycarl.gmp) RationalRF (in module stormpy) raw_formula (Property property) REAL (VariableType attribute) reduce() (NondeterministicBeliefTrackerDoubleSparse method) (NondeterministicBeliefTrackerExactSparse method) reduce_to_state_based_rewards() (SparseExactRewardModel method), [1] (SparseIntervalRewardModel method), [1] (SparseParametricRewardModel method), [1] (SparseRewardModel method), [1] reduction_timed_out() (NondeterministicBeliefTrackerDoubleSparse method) (NondeterministicBeliefTrackerExactSparse method) reduction_timeout (NondeterministicBeliefTrackerDoubleSparseOptions property) (NondeterministicBeliefTrackerExactSparseOptions property) reduction_wiggle (NondeterministicBeliefTrackerDoubleSparseOptions property) (NondeterministicBeliefTrackerExactSparseOptions property) refine (BeliefExplorationModelCheckerOptionsDouble property) refine_precision (BeliefExplorationModelCheckerOptionsDouble property) refine_step_limit (BeliefExplorationModelCheckerOptionsDouble property) RegionModelChecker (class in stormpy.pars) RegionResult (class in stormpy.pars) RegionResultHypothesis (class in stormpy.pars) rel() (SimpleConstraint method), [1] (SimpleConstraintRatFunc method), [1] Relation (class in stormpy.pycarl.formula) relation (Constraint property), [1] RelevantEvents (class in stormpy.dft)

remove_bound() (OperatorFormula method), [1] remove_constant() (JaniModel method), [1] remove_inhibition_arc() (Transition method) remove_input_arc() (Transition method) remove_optimality_type() (OperatorFormula method), [1] remove_output_arc() (Transition method) replace_automaton() (JaniModel method), [1] replace_columns() (ExactSparseMatrixBuilder method), [1] (IntervalSparseMatrixBuilder method), [1] (ParametricSparseMatrixBuilder method), [1] (SparseMatrixBuilder method), [1] replace_constant_by_variable() (PrismProgram method), [1] replace_variable_initialization_by_init_expression() (PrismProgram method), [1] representative() (DftIndependentModule method) reset() (DFTSimulator_double method) (DFTSimulator_ratfunc method) (NondeterministicBeliefTrackerDoubleSparse method) (NondeterministicBeliefTrackerExactSparse method) (ObservationTraceUnfolderDouble method) (ObservationTraceUnfolderExact method) (ObservationTraceUnfolderRf method) (SmtSolver method) reset_state() (DFTSimulator_double method) (DFTSimulator_ratfunc method) reset_timeout() (in module stormpy) restrict_commands() (PrismProgram method), [1] restrict_edges() (JaniModel method), [1] reward_models (PrismProgram property), [1] (SparseExactModelComponents property), [1] (SparseIntervalModelComponents property), [1] (SparseModelComponents property), [1] (SparseParametricModelComponents property), [1] reward_name (RewardOperator property), [1] RewardOperator (class in stormpy) (class in stormpy.logic) right_subformula (BinaryPathFormula property), [1] (BoundedUntilFormula property), [1] risk (SparseBeliefStateDouble property) (SparseBeliefStateExact property) rotation (LayoutInfo property) row_iter() (ExactSparseMatrix method), [1] (IntervalSparseMatrix method), [1] (ParametricSparseMatrix method), [1] (SparseMatrix method), [1]

S

sample() (Interval method), [1], [2] Sat (SmtCheckResult attribute) Scheduler (class in stormpy) (class in stormpy.storage) scheduler (ExplicitExactQuantitativeCheckResult property) (ExplicitParametricQuantitativeCheckResult property) (ExplicitQuantitativeCheckResult property) SchedulerChoice (class in stormpy) (class in stormpy.storage) SchedulerChoiceExact (class in stormpy) (class in stormpy.storage) SchedulerChoiceInterval (class in stormpy) (class in stormpy.storage) SchedulerChoiceParametric (class in stormpy) (class in stormpy.storage) SchedulerExact (class in stormpy) (class in stormpy.storage) SchedulerInterval (class in stormpy) (class in stormpy.storage) SchedulerParametric (class in stormpy) (class in stormpy.storage) selective_counter (PomdpMemoryPattern attribute) selective_ring (PomdpMemoryPattern attribute) SEQ (DFTElementType attribute) set() (BitVector method), [1] set_add_out_of_bounds_state() (BuilderOptions method) set_add_overlapping_guards_label() (BuilderOptions method) set_bound() (OperatorFormula method), [1] set_build_all_labels() (BuilderOptions method) set_build_all_reward_models() (BuilderOptions method) set_build_choice_labels() (BuilderOptions method) set_build_observation_valuations() (BuilderOptions method) set_build_state_valuations() (BuilderOptions method) set_build_with_choice_origins() (BuilderOptions method) set_capacity() (Place method) set_choice() (Scheduler method), [1] (SchedulerExact method), [1] (SchedulerInterval method), [1] (SchedulerParametric method), [1] set_choices() (ChoiceLabeling method), [1] set_compute_only_maybe_states() (ExplicitModelCheckerHintDouble method) set_exploration_checks() (BuilderOptions method) set_force_exact() (SolverEnvironment method) set_force_sound() (SolverEnvironment method) set_fsc_values() (BeliefExplorationModelCheckerDouble method) (BeliefMdpExplorerDouble method) set_graph_preserving() (PCtmcExactInstantiationChecker method) (PCtmcInstantiationChecker method) (PDtmcExactInstantiationChecker method) (PDtmcInstantiationChecker method) (PMdpExactInstantiationChecker method) (PMdpInstantiationChecker method) set_hint() (CheckTask method) set_identifier_mapping() (ExpressionParser method), [1] set_infinite_server_semantics() (TimedTransition method) set_inhibition_arc_multiplicity() (Transition method) set_input_arc_multiplicity() (Transition method) set_k_server_semantics() (TimedTransition method) set_linear_equation_solver_type() (SolverEnvironment method) set_loglevel_debug() (in module stormpy) set_loglevel_error() (in module stormpy) set_loglevel_trace() (in module stormpy) set_maybe_states() (ExplicitModelCheckerHintDouble method) set_model_type() (JaniModel method), [1] set_name() (GSPN method) (GSPNBuilder method) (Place method) (Transition method) set_number_of_initial_tokens() (Place method) set_optimality_type() (OperatorFormula method), [1] set_output_arc_multiplicity() (Transition method) set_place_layout_info() (GSPNBuilder method) set_priority() (Transition method) set_produce_schedulers() (CheckTask method) (ExactCheckTask method) (ParametricCheckTask method) set_rate() (TimedTransition method) set_relevant_events() (DFT_double method) (DFT_ratfunc method) set_result_hint() (ExplicitModelCheckerHintDouble method) set_risk() (NondeterministicBeliefTrackerDoubleSparse method) (NondeterministicBeliefTrackerExactSparse method) set_robust_uncertainty() (CheckTask method) set_scheduler_hint() (ExplicitModelCheckerHintDouble method) set_settings() (in module stormpy) set_single_server_semantics() (TimedTransition method) set_standard_system_composition() (JaniModel method), [1] set_state_reward() (SparseExactRewardModel method), [1] (SparseIntervalRewardModel method), [1] (SparseRewardModel method), [1] set_states() (StateLabeling method), [1] set_timeout() (in module stormpy) set_transition_layout_info() (GSPNBuilder method) set_value() (ExactSparseMatrixEntry method), [1] (IntervalSparseMatrixEntry method), [1] (ParametricSparseMatrixEntry method), [1] (SparseMatrixEntry method), [1] set_weight() (ImmediateTransition method) setLower() (Interval method), [1], [2] settable_bits (PomdpMemoryPattern attribute) setup_time (SMTCounterExampleGeneratorStats property) setUpper() (Interval method), [1], [2] SHA (JaniModelType attribute) short (Version attribute) ShortestPathsGenerator (class in stormpy.utility) silent (SMTCounterExampleGeneratorOptions property) simple_linear (PomdpFscApplicationMode attribute) simple_linear_inverse (PomdpFscApplicationMode attribute) simple_log (PomdpFscApplicationMode attribute) SimpleConstraint (class in stormpy.pycarl.cln.formula) (class in stormpy.pycarl.gmp.formula) SimpleConstraintRatFunc (class in stormpy.pycarl.cln.formula) (class in stormpy.pycarl.gmp.formula) SimpleValuation (class in stormpy) (class in stormpy.storage) simplify() (Expression method), [1] (PrismProgram method), [1] (PrismUpdate method), [1] simplify_model() (in module stormpy.pars) simulate_trace() (DFTSimulator_double method) (DFTSimulator_ratfunc method) SimulationStepResult (class in stormpy.dft) SimulationTraceResult (class in stormpy.dft) single_be() (DftIndependentModule method) sink_rows (EndComponentEliminatorReturnTypeDouble property) size (MaximalEndComponent property), [1] (MaximalEndComponentDecomposition_double property), [1] (MaximalEndComponentDecomposition_exact property), [1] (MaximalEndComponentDecomposition_interval property), [1] (MaximalEndComponentDecomposition_ratfunc property), [1] size() (BitVector method), [1] (NondeterministicBeliefTrackerDoubleSparse method) (NondeterministicBeliefTrackerExactSparse method) size_threshold_factor (BeliefExplorationModelCheckerOptionsDouble property) size_threshold_init (BeliefExplorationModelCheckerOptionsDouble property) skip_heuristic_schedulers (BeliefExplorationModelCheckerOptionsDouble property) SMG (ModelType attribute), [1], [2] SmtCheckResult (class in stormpy.utility) SMTCounterExampleGenerator (class in stormpy) SMTCounterExampleGeneratorOptions (class in stormpy) SMTCounterExampleGeneratorStats (class in stormpy) SMTCounterExampleInput (class in stormpy) SmtSolver (class in stormpy.utility) SmtSolverFactory (class in stormpy.utility) solver_environment (Environment property) solver_time (SMTCounterExampleGeneratorStats property) SolverEnvironment (class in stormpy) SOR (NativeLinearEquationSolverMethod attribute) sound_value_iteration (MinMaxMethod attribute) (NativeLinearEquationSolverMethod attribute) source_location_index (JaniEdge property), [1] SPARE (DFTElementType attribute) spare_uses() (DFTState_double method) (DFTState_ratfunc method) SPARSE (QuotientFormat attribute) SparseBeliefStateDouble (class in stormpy.pomdp) SparseBeliefStateExact (class in stormpy.pomdp) SparseCtmc (class in stormpy) (class in stormpy.storage) SparseDtmc (class in stormpy) (class in stormpy.storage) SparseExactCtmc (class in stormpy) (class in stormpy.storage) SparseExactDtmc (class in stormpy) (class in stormpy.storage) SparseExactMA (class in stormpy) (class in stormpy.storage) SparseExactMdp (class in stormpy) (class in stormpy.storage) SparseExactModelAction (class in stormpy) (class in stormpy.storage) SparseExactModelActions (class in stormpy) (class in stormpy.storage) SparseExactModelComponents (class in stormpy) (class in stormpy.storage) SparseExactModelState (class in stormpy) (class in stormpy.storage) SparseExactModelStates (class in stormpy) (class in stormpy.storage) SparseExactPomdp (class in stormpy) (class in stormpy.storage) SparseExactRewardModel (class in stormpy) (class in stormpy.storage) SparseExactSmg (class in stormpy) (class in stormpy.storage) SparseIntervalCtmc (class in stormpy) (class in stormpy.storage) SparseIntervalDtmc (class in stormpy) (class in stormpy.storage) SparseIntervalMA (class in stormpy) (class in stormpy.storage) SparseIntervalMdp (class in stormpy) (class in stormpy.storage) SparseIntervalModelAction (class in stormpy) (class in stormpy.storage) SparseIntervalModelActions (class in stormpy) (class in stormpy.storage) SparseIntervalModelComponents (class in stormpy) (class in stormpy.storage) SparseIntervalModelState (class in stormpy) (class in stormpy.storage)

SparseIntervalModelStates (class in stormpy) (class in stormpy.storage) SparseIntervalPomdp (class in stormpy) (class in stormpy.storage) SparseIntervalRewardModel (class in stormpy) (class in stormpy.storage) SparseIntervalSmg (class in stormpy) (class in stormpy.storage) SparseMA (class in stormpy) (class in stormpy.storage) SparseMatrix (class in stormpy) (class in stormpy.storage) SparseMatrixBuilder (class in stormpy) (class in stormpy.storage) SparseMatrixEntry (class in stormpy) (class in stormpy.storage) SparseMatrixRows (class in stormpy) (class in stormpy.storage) SparseMdp (class in stormpy) (class in stormpy.storage) SparseModelAction (class in stormpy) (class in stormpy.storage) SparseModelActions (class in stormpy) (class in stormpy.storage) SparseModelComponents (class in stormpy) (class in stormpy.storage) SparseModelState (class in stormpy) (class in stormpy.storage) SparseModelStates (class in stormpy) (class in stormpy.storage) SparseParametricCtmc (class in stormpy) (class in stormpy.storage) SparseParametricDtmc (class in stormpy) (class in stormpy.storage) SparseParametricMA (class in stormpy) (class in stormpy.storage) SparseParametricMdp (class in stormpy) (class in stormpy.storage) SparseParametricModelAction (class in stormpy) (class in stormpy.storage) SparseParametricModelActions (class in stormpy) (class in stormpy.storage) SparseParametricModelComponents (class in stormpy) (class in stormpy.storage) SparseParametricModelState (class in stormpy) (class in stormpy.storage) SparseParametricModelStates (class in stormpy) (class in stormpy.storage) SparseParametricPomdp (class in stormpy) (class in stormpy.storage) SparseParametricRewardModel (class in stormpy) (class in stormpy.storage) SparsePomdp (class in stormpy) (class in stormpy.storage) SparseRewardModel (class in stormpy) (class in stormpy.storage) SparseSmg (class in stormpy) (class in stormpy.storage) specify() (RegionModelChecker method) STA (JaniModelType attribute) standard (PomdpFscApplicationMode attribute) state_action_rewards (SparseExactRewardModel property), [1] (SparseIntervalRewardModel property), [1] (SparseParametricRewardModel property), [1] (SparseRewardModel property), [1] state_domain_size (JaniInformationObject property), [1] state_generation_info() (DFT_double method) (DFT_ratfunc method) state_labeling (SparseExactModelComponents property), [1] (SparseIntervalModelComponents property), [1] (SparseModelComponents property), [1] (SparseParametricModelComponents property), [1] state_player_indications (SparseExactModelComponents property), [1] (SparseIntervalModelComponents property), [1] (SparseModelComponents property), [1] (SparseParametricModelComponents property), [1] state_rewards (SparseExactRewardModel property), [1] (SparseIntervalRewardModel property), [1] (SparseParametricRewardModel property), [1] (SparseRewardModel property), [1] state_valuations (SparseExactModelComponents property), [1] (SparseIntervalModelComponents property), [1] (SparseModelComponents property), [1] (SparseParametricModelComponents property), [1] StateFormula (class in stormpy) (class in stormpy.logic) StateLabeling (class in stormpy) (class in stormpy.storage) StateValuation (class in stormpy) (class in stormpy.storage) StateValuationFunctionActionMaskDouble (class in stormpy) StateValuationsBuilder (class in stormpy) (class in stormpy.storage) static() (DftIndependentModule method) step() (DFTSimulator_double method) (DFTSimulator_ratfunc method) store_as_string() (BitVector method), [1] store_to_file() (BeliefSupportWinningRegion method) storm_exact_use_cln() (in module stormpy.info) storm_ratfunc_use_cln() (in module stormpy.info) storm_version() (in module stormpy.info) StormError stormpy module stormpy.dft module stormpy.exceptions module stormpy.gspn module stormpy.info module stormpy.logic module stormpy.pars module stormpy.pomdp module stormpy.pycarl module stormpy.pycarl.cln module stormpy.pycarl.cln.formula module stormpy.pycarl.cln.parse module stormpy.pycarl.convert module stormpy.pycarl.formula module stormpy.pycarl.gmp module stormpy.pycarl.gmp.formula module stormpy.pycarl.gmp.parse module stormpy.pycarl.parse module stormpy.storage module stormpy.utility module str_long() (DFT_double method) (DFT_ratfunc method) Straight (MatrixFormat attribute) STRICT (BoundType attribute) STRONG (BisimulationType attribute) subformula (UnaryPathFormula property), [1] (UnaryStateFormula property), [1] subformulas (MultiObjectiveFormula property), [1] submatrix() (ExactSparseMatrix method), [1] (IntervalSparseMatrix method), [1] (ParametricSparseMatrix method), [1] (SparseMatrix method), [1] submodules() (DftIndependentModule method) substitute() (Expression method), [1] (Formula method), [1] (JaniEdge method), [1] (JaniOrderedAssignments method), [1] (Polynomial method), [1], [2] (PrismUpdate method), [1] substitute_constants() (JaniModel method), [1] (PrismProgram method), [1] substitute_formulas() (PrismProgram method), [1] substitute_functions() (JaniModel method), [1] substitute_labels_by_labels() (Formula method), [1] substitute_nonstandard_predicates() (PrismProgram method), [1] SubsystemBuilderOptions (class in stormpy) SubsystemBuilderReturnTypeDouble (class in stormpy) SubsystemBuilderReturnTypeExact (class in stormpy) SubsystemBuilderReturnTypeRatFunc (class in stormpy) SUCCESSFUL (SimulationStepResult attribute) (SimulationTraceResult attribute) SymbolicExactQuantitativeCheckResult (class in stormpy) SymbolicModelDescription (class in stormpy) SymbolicParametricQuantitativeCheckResult (class in stormpy) SymbolicQualitativeCheckResult (class in stormpy) SymbolicQuantitativeCheckResult (class in stormpy) SymbolicSylvanCtmc (class in stormpy) (class in stormpy.storage) SymbolicSylvanDtmc (class in stormpy) (class in stormpy.storage) SymbolicSylvanMA (class in stormpy) (class in stormpy.storage) SymbolicSylvanMdp (class in stormpy) (class in stormpy.storage) SymbolicSylvanParametricCtmc (class in stormpy) (class in stormpy.storage) SymbolicSylvanParametricDtmc (class in stormpy) (class in stormpy.storage) SymbolicSylvanParametricMA (class in stormpy) (class in stormpy.storage) SymbolicSylvanParametricMdp (class in stormpy) (class in stormpy.storage) SymbolicSylvanParametricRewardModel (class in stormpy) (class in stormpy.storage) SymbolicSylvanRewardModel (class in stormpy) (class in stormpy.storage) symmetricDifference() (Interval method), [1], [2] symmetries() (DFT_double method) (DFT_ratfunc method)

T

TA (JaniModelType attribute) target_location_index (JaniEdgeDestination property), [1] tdeg (Monomial property) (Term property), [1] template_edge (JaniEdge property), [1] Term (class in stormpy.pycarl.cln) (class in stormpy.pycarl.gmp) terminate_unfolding() (BeliefExplorationModelCheckerDouble method) threshold (OperatorFormula property), [1] threshold_expr (OperatorFormula property), [1] timed_transition_id_to_transition_id() (GSPN static method) TimedTransition (class in stormpy.gspn) TimeOperator (class in stormpy) (class in stormpy.logic) Times (OperatorType attribute), [1] to_dot() (JaniModel method), [1] to_expression() (Bdd_Sylvan method), [1] to_jani() (PrismProgram method), [1] to_json() (SimpleValuation method), [1] to_json_str() (Scheduler method), [1] (SchedulerExact method), [1] (SchedulerInterval method), [1] (SchedulerParametric method), [1] to_smt2() (Constraint method), [1] (FactorizedPolynomial method), [1], [2] (FactorizedRationalFunction method), [1], [2] (Formula method), [1] (Polynomial method), [1], [2] (RationalFunction method), [1], [2] to_string() (DFTState_double method) (DFTState_ratfunc method) (DiceStringVisitor method), [1] (SimpleValuation method), [1] top_level_element (DFT_double property) (DFT_ratfunc property) topological (EquationSolverType attribute) (MinMaxMethod attribute) topological_sort() (in module stormpy) total_degree (Polynomial property), [1], [2] track() (BeliefSupportTrackerDouble method) (BeliefSupportTrackerExact method) (NondeterministicBeliefTrackerDoubleSparse method) (NondeterministicBeliefTrackerExactSparse method)

track_timeout (NondeterministicBeliefTrackerDoubleSparseOptions property) (NondeterministicBeliefTrackerExactSparseOptions property) transform() (JaniLocationExpander method), [1] (ObservationTraceUnfolderDouble method) (ObservationTraceUnfolderExact method) (ObservationTraceUnfolderRf method) transform_dft() (in module stormpy.dft) transform_to_discrete_time_model() (in module stormpy) transform_to_sparse_model() (in module stormpy) 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 (SparseExactModelComponents property), [1] (SparseIntervalModelComponents property), [1] (SparseModelComponents property), [1] (SparseParametricModelComponents property), [1] transition_rewards (SparseExactRewardModel property), [1] (SparseIntervalRewardModel property), [1] (SparseParametricRewardModel property), [1] (SparseRewardModel property), [1] TransitionPartition (class in stormpy.gspn) transitions (SparseExactModelAction property), [1] (SparseIntervalModelAction property), [1] (SparseModelAction property), [1] (SparseParametricModelAction property), [1] (TransitionPartition property) trigger (DFTDependency_double property) (DFTDependency_ratfunc property) trivial (PomdpMemoryPattern attribute) TRUE (FormulaType attribute) type (DdMetaVariable_Sylvan property), [1] (DFTElement_double property) (DFTElement_ratfunc property) (Expression property), [1] (Formula property), [1] (JaniConstant property), [1] (PrismConstant property), [1] (Variable property)

U

UEQ (FormulaType attribute) UnaryBooleanStateFormula (class in stormpy) (class in stormpy.logic) UnaryPathFormula (class in stormpy) (class in stormpy.logic) UnaryStateFormula (class in stormpy) (class in stormpy.logic) unboundedInterval() (Interval static method), [1], [2] UNDEFINED (JaniModelType attribute) (PrismModelType attribute), [1] undefined_constants_are_graph_preserving (JaniModel property), [1] (PrismProgram property), [1] unfold_memory() (in module stormpy.pomdp) unite() (Interval method), [1], [2] UNKNOWN (RegionResult attribute) (RegionResultHypothesis attribute)

Unknown (SmtCheckResult attribute) Unsat (SmtCheckResult attribute) UNSUCCESSFUL (SimulationStepResult attribute) (SimulationTraceResult attribute) UntilFormula (class in stormpy) (class in stormpy.logic) update_initial_states_expression() (PrismProgram method), [1] updates (PrismCommand property), [1] upper() (Interval method), [1], [2] upper_bound (BeliefExplorationPomdpModelCheckerResultDouble property) upper_bound_expression (BoundedUntilFormula property), [1] (PrismIntegerVariable property), [1] use_clipping (BeliefExplorationModelCheckerOptionsDouble property) use_dynamic_constraints (SMTCounterExampleGeneratorOptions property) use_state_elimination_cutoff (BeliefExplorationModelCheckerOptionsDouble property) used_constants() (PrismProgram method), [1]

V

Valuation (class in stormpy) (class in stormpy.storage) valuations (SparseExactModelState property), [1] (SparseIntervalModelState property), [1] (SparseModelState property), [1] (SparseParametricModelState property), [1] value (ApproximationHeuristic property) (BinaryBooleanOperatorType property), [1] (BisimulationType property) (BoundType property) (ComparisonType property), [1] (DdMetaVariableType property), [1] (DFTElementType property) (EliminationLabelBehavior property) (EquationSolverType property) (FormulaType property) (JaniModelType property) (MatrixFormat property) (MinMaxMethod property) (ModelType property), [1], [2] (NativeLinearEquationSolverMethod property) (OperatorType property), [1] (OptimizationDirection property) (PomdpFscApplicationMode property) (PomdpMemoryPattern property) (PrismModelType property), [1] (QuotientFormat property) (RegionResult property) (RegionResultHypothesis property) (Relation property) (SimulationStepResult property) (SimulationTraceResult property) (SmtCheckResult property) (VariableType property)

value() (ExactSparseMatrixEntry method), [1] (IntervalSparseMatrixEntry method), [1] (ParametricSparseMatrixEntry method), [1] (SparseMatrixEntry method), [1] value_iteration (MinMaxMethod attribute) Variable (class in stormpy) (class in stormpy.pycarl) (class in stormpy.storage) variable (JaniAssignment property), [1] (PrismAssignment property), [1] variable_with_name() (in module stormpy.pycarl) variables (JaniAutomaton property), [1] (PrismProgram property), [1] VariableType (class in stormpy.pycarl) Version (class in stormpy.info) vertices (PolytopeDouble property), [1] (PolytopeExact property), [1] VOT (DFTElementType attribute)

W

walker_chae (NativeLinearEquationSolverMethod attribute) WEAK (BisimulationType attribute) (BoundType attribute)

wellformed_constraints (ConstraintCollector property)

X

x (LayoutInfo property)

XOR (FormulaType attribute) Xor (OperatorType attribute), [1]

Y

y (LayoutInfo property)

Z

Z3SmtSolver (class in stormpy.utility)

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