Index

A

action_index() (JaniEdge property), [1] actions() (SparseModelState property), [1] (SparseParametricModelState property), [1] add() (JaniOrderedAssignments method), [1] (SmtSolver method) add_automaton() (JaniModel method), [1] add_backward_implication_cuts() (SMTCounterExampleGeneratorOptions property) add_bounded_integer_variable() (JaniVariableSet method), [1] add_destination() (JaniTemplateEdge method), [1] add_edge() (JaniAutomaton method), [1] add_initial_location() (JaniAutomaton method), [1] add_label() (ItemLabeling method), [1] add_label_to_state() (StateLabeling method), [1] add_location() (JaniAutomaton method), [1] add_reward_and_threshold() (SMTCounterExampleInput method) add_variable() (JaniVariableSet method), [1] ALLSAT (RegionResult attribute) (RegionResultHypothesis attribute) ALLVIOLATED (RegionResult attribute) (RegionResultHypothesis attribute) analysis_time() (SMTCounterExampleGeneratorStats property) analyze_dft() (in module stormpy.dft)

And (OperatorType attribute), [1] And() (Expression method), [1] apply_scheduler() (SparseMdp method), [1] (SparseParametricMdp method), [1] area() (ParameterRegion property) arity() (Expression property), [1] as_jani_model() (SymbolicModelDescription method) 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]

B

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) boolean_values() (ValuationMapping property), [1] boolean_variables() (PrismModule property), [1] BooleanBinaryStateFormula (class in stormpy) (class in stormpy.logic) BooleanLiteralFormula (class in stormpy) (class in stormpy.logic) BoundedUntilFormula (class in stormpy) (class in stormpy.logic) build() (SMTCounterExampleGenerator method)

build_action_mapping() (SubsystemBuilderOptions property) build_info (Version attribute) build_kept_actions() (SubsystemBuilderOptions property) build_model() (in module stormpy) build_model_from_drn() (in module stormpy) build_parametric_model() (in module stormpy) build_parametric_model_from_drn() (in module stormpy) 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) can_have_nondeterminism() (DFT method) (ParametricDFT method) Ceil (OperatorType attribute), [1] CENTERSAT (RegionResult attribute) CENTERVIOLATED (RegionResult attribute) check() (PDtmcExactInstantiationChecker method) (PDtmcInstantiationChecker method) (PMdpExactInstantiationChecker method) (PMdpInstantiationChecker method) (SmtSolver method) 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] CheckTask (class in stormpy) ChoiceLabeling (class in stormpy) (class in stormpy.storage) ChoiceOrigins (class in stormpy) (class in stormpy.storage) clone() (Formula method), [1] (JaniOrderedAssignments method), [1] (SymbolicExactQuantitativeCheckResult method) (SymbolicParametricQuantitativeCheckResult method) (SymbolicQuantitativeCheckResult method) coefficient() (FactorizedPolynomial property) color() (JaniEdge property), [1] column() (ParametricSparseMatrixEntry property), [1] (SparseMatrixEntry property), [1] commands() (PrismModule property), [1] comparison_type() (OperatorFormula property), [1] ComparisonType (class in stormpy) (class in stormpy.logic) compute_action_support() (SchedulerDouble method), [1] compute_all_until_probabilities() (in module stormpy) compute_prob01_states() (in module stormpy) compute_prob01max_states() (in module stormpy)

compute_prob01min_states() (in module stormpy) compute_transient_probabilities() (in module stormpy) ConditionalFormula (class in stormpy) (class in stormpy.logic) Constant (class in stormpy) (class in stormpy.storage) constant_part() (FactorizedPolynomial method) (FactorizedRationalFunction method) (Polynomial method) (RationalFunction method) constants() (JaniModel property), [1] (PrismProgram property), [1] ConstraintCollector (class in stormpy) construct_submodel() (in module stormpy) contains_label() (ItemLabeling method), [1] contains_variable() (Expression method), [1] contains_variables() (Expression method), [1] continue_after_first_counterexample() (SMTCounterExampleGeneratorOptions property) count() (milliseconds method) create_boolean() (ExpressionManager method), [1] create_boolean_variable() (ExpressionManager method), [1] 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 method) create_integer() (ExpressionManager method), [1] create_integer_variable() (ExpressionManager method), [1] 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) current_state_satisfies() (StateGenerator method), [1] current_state_to_valuation() (StateGenerator method), [1] cut_time() (SMTCounterExampleGeneratorStats property)

D

decode_automaton_and_edge_index() (JaniModel method), [1] define_constants() (JaniModel method), [1] (PrismProgram method), [1] defined() (Constant property), [1] (JaniConstant property), [1] (SchedulerChoiceDouble property), [1] degree() (Polynomial method) denominator() (FactorizedRationalFunction property) (Rational property) (RationalFunction property) derive() (FactorizedPolynomial method) (FactorizedRationalFunction method) (Polynomial method) (RationalFunction method)

destinations() (JaniEdge property), [1] (JaniTemplateEdge property), [1] deterministic() (SchedulerChoiceDouble property), [1] (SchedulerDouble property), [1] development (Version attribute) DFT (class in stormpy.dft) distance() (Path property) DistributionDouble (class in stormpy) (class in stormpy.storage) Divide (OperatorType attribute), [1] DTMC (JaniModelType attribute) (ModelType attribute), [1], [2] (PrismModelType attribute), [1] DtmcParameterLiftingModelChecker (class in stormpy.pars)

E

edges() (JaniAutomaton property), [1] eigen (EquationSolverType attribute) eliminate_reward_accumulations() (in module stormpy) (in module stormpy.storage) elimination (EquationSolverType attribute) empty() (JaniVariableSet method), [1] encode_automaton_and_edge_index() (JaniModel method), [1] encode_reachability() (SMTCounterExampleGeneratorOptions property) Environment (class in stormpy) Eq() (Expression method), [1] Equal (OperatorType attribute), [1] EquationSolverType (class in stormpy) evaluate() (FactorizedPolynomial method) (FactorizedRationalFunction method) (Polynomial method) (RationalFunction method) 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) EXISTSBOTH (RegionResult attribute) EXISTSSAT (RegionResult attribute) EXISTSVIOLATED (RegionResult attribute)

expand() (StateGenerator method), [1] ExplicitExactQuantitativeCheckResult (class in stormpy) ExplicitParametricQuantitativeCheckResult (class in stormpy) ExplicitQualitativeCheckResult (class in stormpy) ExplicitQuantitativeCheckResult (class in stormpy) export_dft_json_file() (in module stormpy.dft) export_dft_json_string() (in module stormpy.dft) export_parametric_to_drn() (in module stormpy) export_to_drn() (in module stormpy) Expression (class in stormpy) (class in stormpy.storage) expression() (JaniAssignment property), [1] (PrismAssignment property), [1] expression_manager() (JaniModel property), [1] (PrismProgram property), [1] expression_variable() (Constant property), [1] (JaniConstant property), [1] (JaniVariable 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)

F

factorization() (FactorizedPolynomial method) FactorizedPolynomial (class in stormpy) FactorizedRationalFunction (class in stormpy) finalize() (JaniModel method), [1]

FlatSet (class in stormpy) Floor (OperatorType attribute), [1] Formula (class in stormpy) (class in stormpy.logic) formulas() (ModelFormulasPair property)

G

gather_derivatives() (in module stormpy.pars) gather_variables() (FactorizedPolynomial method) (FactorizedRationalFunction method) (Polynomial method) (RationalFunction method) gauss_seidel (NativeLinearEquationSolverMethod attribute) GEQ (ComparisonType attribute), [1] Geq() (Expression method), [1] get() (BitVector method), [1] get_automaton_index() (JaniModel method), [1] get_boolean_value() (ModelReference method) (SimpleValuation method), [1] get_bound() (RegionModelChecker method) get_bound_all_states() (DtmcParameterLiftingModelChecker method) (MdpParameterLiftingModelChecker method) get_choice() (SchedulerChoiceDouble method), [1] (SchedulerDouble method), [1] get_choice_info() (ChoiceOrigins method), [1] get_constant() (JaniModel method), [1] get_deterministic_choice() (SchedulerChoiceDouble method), [1] get_distance() (ShortestPathsGenerator method) get_edge_index_set() (JaniChoiceOrigins method), [1] get_expression() (Variable method) get_identifier_info() (ChoiceOrigins method), [1] get_integer_value() (ModelReference method) (SimpleValuation method), [1] get_label_expression() (PrismProgram method), [1] get_labels() (ItemLabeling method), [1] get_labels_of_state() (StateLabeling method), [1] get_operand() (Expression method), [1] get_path_as_list() (ShortestPathsGenerator method) get_rational_value() (ModelReference method) get_row() (ParametricSparseMatrix method), [1] (SparseMatrix method), [1] get_row_group_end() (ParametricSparseMatrix method), [1] (SparseMatrix method), [1]

get_row_group_start() (ParametricSparseMatrix method), [1] (SparseMatrix method), [1] get_rows() (ParametricSparseMatrix method), [1] (SparseMatrix method), [1] get_split_suggestion() (RegionModelChecker method) get_state() (StateValuation method), [1] get_state_action_reward() (SparseParametricRewardModel method), [1] (SparseRewardModel method), [1] get_state_reward() (SparseParametricRewardModel method), [1] (SparseRewardModel method), [1] get_states() (ShortestPathsGenerator method) (StateLabeling method), [1] get_truth_values() (ExplicitQualitativeCheckResult method) get_values() (ExplicitExactQuantitativeCheckResult method) (ExplicitParametricQuantitativeCheckResult method) (ExplicitQuantitativeCheckResult method) (HybridExactQuantitativeCheckResult method) (HybridParametricQuantitativeCheckResult method) (HybridQuantitativeCheckResult method) get_variable_by_expr_variable() (JaniVariableSet method), [1] get_variable_by_name() (JaniVariableSet method), [1] get_variables() (Expression method), [1] get_zero_reward_states() (SparseRewardModel method), [1] global_index() (PrismCommand 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() (Expression method), [1] GreaterOrEqual (OperatorType attribute), [1] guard() (JaniEdge property), [1] (JaniTemplateEdge property), [1] guard_expression() (PrismCommand property), [1]

H

HA (JaniModelType attribute) has_bitvector_type() (Variable method) has_boolean_type() (Expression method), [1] (Variable method) has_bound() (OperatorFormula property), [1] has_integer_type() (Expression method), [1] (Variable method) has_numerical_type() (Variable method) has_optimality_type() (OperatorFormula property), [1] has_rational_type() (Expression method), [1] (Variable method) has_reward_name() (RewardOperator method), [1] has_silent_action() (JaniEdge method), [1] has_standard_composition() (JaniModel method), [1] has_state_action_rewards() (SparseParametricRewardModel property), [1] (SparseRewardModel property), [1] (SymbolicSylvanParametricRewardModel property), [1] (SymbolicSylvanRewardModel property), [1]

has_state_label() (StateLabeling method), [1] has_state_rewards() (SparseParametricRewardModel property), [1] (SparseRewardModel property), [1] (SymbolicSylvanParametricRewardModel property), [1] (SymbolicSylvanRewardModel property), [1] has_transition_rewards() (SparseParametricRewardModel property), [1] (SparseRewardModel property), [1] (SymbolicSylvanParametricRewardModel property), [1] (SymbolicSylvanRewardModel property), [1] has_trivial_row_grouping() (ParametricSparseMatrix property), [1] (SparseMatrix property), [1] has_undefined_constants() (JaniModel property), [1] (PrismProgram property), [1] hasUndefinedConstants() (PrismProgram property), [1] HybridExactQuantitativeCheckResult (class in stormpy) HybridParametricQuantitativeCheckResult (class in stormpy) HybridQuantitativeCheckResult (class in stormpy)

I

I_Minus_P (MatrixFormat attribute) id() (SparseModelAction property), [1] (SparseModelState property), [1] (SparseParametricModelAction property), [1] (SparseParametricModelState property), [1] (Variable property) identifier() (Expression method), [1] Iff (OperatorType attribute), [1] Iff() (Expression method), [1] Implies (OperatorType attribute), [1] Implies() (Expression method), [1] initial_location_indices() (JaniAutomaton property), [1] initial_states_restriction() (JaniAutomaton property), [1] (JaniModel property), [1] initial_value_expression() (PrismVariable property), [1] insert() (FlatSet method) insert_set() (FlatSet method) InstantaneousRewardFormula (class in stormpy) (class in stormpy.logic) instantiate() (ModelInstantiator method) (PCtmcInstantiator method) (PDtmcInstantiator method) (PMaInstantiator method) (PMdpInstantiator method) instantiate_constants() (SymbolicModelDescription method)

integer_values() (ValuationMapping property), [1] integer_variables() (PrismModule property), [1] interval_iteration (MinMaxMethod attribute) (NativeLinearEquationSolverMethod attribute) is_boolean() (ExpressionType property), [1] is_constant() (FactorizedPolynomial method) (FactorizedRationalFunction method) (Polynomial method) (RationalFunction method) is_function_application() (Expression property), [1] is_integer() (ExpressionType property), [1] is_jani_model() (SymbolicModelDescription property) is_literal() (Expression method), [1] is_no_variable() (Variable property) is_one() (FactorizedPolynomial method) is_prism_program() (SymbolicModelDescription property) is_probability_operator() (Formula property), [1] is_rational() (ExpressionType property), [1] is_reward_operator() (Formula property), [1] is_subset_of() (FlatSet method) is_variable() (Expression method), [1] isDeterministicModel() (PrismProgram property), [1] Ite (OperatorType attribute), [1] ItemLabeling (class in stormpy) (class in stormpy.storage) iterations() (SMTCounterExampleGeneratorStats property)

J

jacobi (NativeLinearEquationSolverMethod attribute) JaniAssignment (class in stormpy) (class in stormpy.storage) JaniAutomaton (class in stormpy) (class in stormpy.storage) JaniBoundedIntegerVariable (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)

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

K

kept_actions() (SubsystemBuilderReturnTypeDouble property)

L

labels() (SparseModelState property), [1] (SparseParametricModelState property), [1] left_subformula() (BinaryPathFormula property), [1] LEQ (ComparisonType attribute), [1] Leq() (Expression method), [1] LESS (ComparisonType attribute), [1] Less (OperatorType attribute), [1] Less() (Expression method), [1] LessOrEqual (OperatorType attribute), [1] linear_programming (MinMaxMethod attribute) load() (StateGenerator method), [1] 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_initial_state() (StateGenerator method), [1] 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) lower_bound_expression() (PrismIntegerVariable property), [1] LTS (JaniModelType attribute)

M

MA (JaniModelType attribute) (ModelType attribute), [1], [2] (PrismModelType attribute), [1] major (Version attribute) make_standard_compliant() (JaniModel method), [1] manager() (Expression property), [1] MatrixFormat (class in stormpy.utility) Max (OperatorType attribute), [1] 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) memory_size() (SchedulerDouble property), [1] memoryless() (SchedulerDouble 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 method), [1] model() (JaniChoiceOrigins property), [1] (ModelFormulasPair property) (SmtSolver property) (SubsystemBuilderReturnTypeDouble property) model_checking() (in module stormpy) model_checking_time() (SMTCounterExampleGeneratorStats property) model_type() (JaniModel property), [1] (PrismProgram property), [1] 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) modules() (PrismProgram property), [1] Modulo (OperatorType attribute), [1] Multiply() (Expression method), [1]

N

name() (Constant property), [1] (JaniAutomaton property), [1] (JaniConstant property), [1] (JaniLocation property), [1] (JaniModel property), [1] (JaniVariable property), [1] (PrismModule property), [1] (PrismVariable property), [1] (Property property) (Variable property), [1] native (EquationSolverType attribute) native_solver_environment() (SolverEnvironment property) NativeLinearEquationSolverMethod (class in stormpy) NativeSolverEnvironment (class in stormpy) Neq() (Expression method), [1] new_to_old_action_mapping() (SubsystemBuilderReturnTypeDouble property) new_to_old_state_mapping() (SubsystemBuilderReturnTypeDouble property) nominator() (Rational property) (RationalFunction property) nondeterministic_choice_indices() (SparseMdp property), [1] (SparseParametricMdp property), [1]

Not (OperatorType attribute), [1] NotEqual (OperatorType attribute), [1] nr_be() (DFT method) (ParametricDFT method) nr_columns() (ParametricSparseMatrix property), [1] (SparseMatrix property), [1] nr_destinations() (JaniEdge property), [1] nr_dynamic() (DFT method) (ParametricDFT method) nr_elements() (DFT method) (ParametricDFT method) nr_entries() (ParametricSparseMatrix property), [1] (SparseMatrix property), [1] nr_modules() (PrismProgram property), [1] nr_observations() (SparsePomdp property), [1] nr_rows() (ParametricSparseMatrix property), [1] (SparseMatrix property), [1] nr_terms() (Polynomial property) number_of_set_bits() (BitVector method), [1] numerator() (FactorizedRationalFunction property) (Rational property) (RationalFunction property)

O

observations() (SparsePomdp property), [1] 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] OptimizationDirection (class in stormpy) Or (OperatorType attribute), [1] Or() (Expression method), [1]

P

ParameterRegion (class in stormpy.pars) ParametricCheckTask (class in stormpy) ParametricDFT (class in stormpy.dft) ParametricSparseMatrix (class in stormpy) (class in stormpy.storage) ParametricSparseMatrixEntry (class in stormpy) (class in stormpy.storage) ParametricSparseMatrixRows (class in stormpy) (class in stormpy.storage) parse() (ExpressionParser method), [1] parse_constant_definitions() (SymbolicModelDescription method) parse_jani_model() (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) patch (Version attribute) Path (class in stormpy.utility) PathFormula (class in stormpy) (class in stormpy.logic) PCtmcInstantiator (class in stormpy.pars) 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) Plus (OperatorType attribute), [1] Plus() (Expression 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) polynomial() (FactorizedPolynomial method)

POMDP (ModelType attribute), [1], [2] pop() (SmtSolver method) Power (OperatorType attribute), [1] power_iteration (NativeLinearEquationSolverMethod attribute) precision() (MinMaxSolverEnvironment property) precompute() (SMTCounterExampleGenerator method) predecessorK() (Path property) predecessorNode() (Path property) preprocess_prism_program() (in module stormpy) preserved_label_names() (BuilderOptions property) print_row() (ParametricSparseMatrix method), [1] (SparseMatrix method), [1] PrismAssignment (class in stormpy) (class in stormpy.storage) PrismBooleanVariable (class in stormpy) (class in stormpy.storage) PrismCommand (class in stormpy) (class in stormpy.storage) PrismIntegerVariable (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) 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() (JaniEdgeDestination property), [1] probability_expression() (PrismUpdate property), [1] ProbabilityOperator (class in stormpy) (class in stormpy.logic) Property (class in stormpy) PTA (JaniModelType attribute) push() (SmtSolver method)

R

rank() (Variable property) rate() (JaniEdge property), [1] Rational (class in stormpy) rational_function() (FactorizedRationalFunction method) rational_search (MinMaxMethod attribute) (NativeLinearEquationSolverMethod attribute) rational_values() (ValuationMapping property), [1] RationalFunction (class in stormpy) RationalRF (in module stormpy) raw_formula() (Property property) reduce_to_state_based_rewards() (SparseParametricRewardModel method), [1] (SparseRewardModel method), [1] RegionModelChecker (class in stormpy.pars) RegionResult (class in stormpy.pars)

RegionResultHypothesis (class in stormpy.pars) remove_bound() (OperatorFormula method), [1] remove_constant() (JaniModel method), [1] remove_optimality_type() (OperatorFormula method), [1] replace_automaton() (JaniModel method), [1] reset() (SmtSolver method) restrict_commands() (PrismProgram method), [1] restrict_edges() (JaniModel method), [1] reward_name() (RewardOperator property), [1] RewardOperator (class in stormpy) (class in stormpy.logic) right_subformula() (BinaryPathFormula property), [1] row_iter() (ParametricSparseMatrix method), [1] (SparseMatrix method), [1]

S

Sat (SmtCheckResult attribute) scheduler() (ExplicitQuantitativeCheckResult property) SchedulerChoiceDouble (class in stormpy) (class in stormpy.storage) SchedulerDouble (class in stormpy) (class in stormpy.storage) 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_state_valuations() (BuilderOptions method) set_build_with_choice_origins() (BuilderOptions method) set_force_sound() (SolverEnvironment method) set_graph_preserving() (PDtmcExactInstantiationChecker method) (PDtmcInstantiationChecker method) (PMdpExactInstantiationChecker method) (PMdpInstantiationChecker method) set_identifier_mapping() (ExpressionParser method), [1] set_linear_equation_solver_type() (SolverEnvironment method) set_model_type() (JaniModel method), [1] set_optimality_type() (OperatorFormula method), [1] set_produce_schedulers() (CheckTask method) (ParametricCheckTask method) set_settings() (in module stormpy) set_standard_system_composition() (JaniModel method), [1] set_states() (StateLabeling method), [1] set_value() (ParametricSparseMatrixEntry method), [1] (SparseMatrixEntry method), [1] setup_time() (SMTCounterExampleGeneratorStats property) SHA (JaniModelType attribute) short (Version attribute) ShortestPathsGenerator (class in stormpy.utility) silent() (SMTCounterExampleGeneratorOptions property) SimpleValuation (class in stormpy) (class in stormpy.storage) simplify() (PrismProgram method), [1] simplify_model() (in module stormpy.pars) size() (BitVector method), [1] 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) 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] SparseCtmc (class in stormpy) (class in stormpy.storage) SparseDtmc (class in stormpy) (class in stormpy.storage) SparseMA (class in stormpy) (class in stormpy.storage) SparseMatrix (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) 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) SparseParametricModelState (class in stormpy) (class in stormpy.storage) SparseParametricModelStates (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) specify() (RegionModelChecker method) STA (JaniModelType attribute) state_action_rewards() (SparseParametricRewardModel property), [1] (SparseRewardModel property), [1] state_rewards() (SparseParametricRewardModel property), [1] (SparseRewardModel property), [1] StateFormula (class in stormpy) (class in stormpy.logic) StateGenerator (class in stormpy) (class in stormpy.storage) StateLabeling (class in stormpy) (class in stormpy.storage) StateValuation (class in stormpy) (class in stormpy.storage) storm_exact_use_cln() (in module stormpy.info) storm_ratfunc_use_cln() (in module stormpy.info) storm_version() (in module stormpy.info) StormError, [1], [2] stormpy (module) stormpy.dft (module) stormpy.exceptions (module) stormpy.info (module) stormpy.logic (module) stormpy.pars (module) stormpy.storage (module) stormpy.utility (module) Straight (MatrixFormat attribute) STRONG (BisimulationType attribute) subformula() (UnaryPathFormula property), [1] (UnaryStateFormula property), [1] submatrix() (ParametricSparseMatrix method), [1] (SparseMatrix method), [1] substitute() (Expression method), [1] (Formula method), [1] (JaniEdge method), [1] (JaniOrderedAssignments method), [1] (Polynomial method) substitute_constants() (JaniModel method), [1] (PrismProgram method), [1] substitute_functions() (JaniModel method), [1] substitute_labels_by_labels() (Formula method), [1] SubsystemBuilderOptions (class in stormpy) SubsystemBuilderReturnTypeDouble (class in stormpy) 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)

T

TA (JaniModelType attribute) target_location_index() (JaniEdgeDestination property), [1] template_edge() (JaniEdge property), [1] threshold() (OperatorFormula property), [1] threshold_expr() (OperatorFormula property), [1] TimeOperator (class in stormpy) (class in stormpy.logic) Times (OperatorType attribute), [1] to_dot() (JaniModel method), [1] to_jani() (PrismProgram method), [1] to_smt2() (FactorizedPolynomial method) (FactorizedRationalFunction method) (Polynomial method) (RationalFunction method)

topological (EquationSolverType attribute) (MinMaxMethod attribute) topological_cuda (MinMaxMethod attribute) topological_sort() (in module stormpy) total_degree() (Polynomial property) transform_to_discrete_time_model() (in module stormpy) transform_to_sparse_model() (in module stormpy) transition_rewards() (SparseParametricRewardModel property), [1] (SparseRewardModel property), [1] transitions() (SparseModelAction property), [1] (SparseParametricModelAction property), [1] type() (Constant property), [1] (Expression property), [1] (JaniConstant property), [1] (Variable property)

U

UnaryBooleanStateFormula (class in stormpy) (class in stormpy.logic) UnaryPathFormula (class in stormpy) (class in stormpy.logic) UnaryStateFormula (class in stormpy) (class in stormpy.logic) UNDEFINED (JaniModelType attribute) (PrismModelType attribute), [1] undefined_constants_are_graph_preserving() (JaniModel property), [1] (PrismProgram property), [1]

UNKNOWN (RegionResult attribute) (RegionResultHypothesis attribute) Unknown (SmtCheckResult attribute) Unsat (SmtCheckResult attribute) UntilFormula (class in stormpy) (class in stormpy.logic) updates() (PrismCommand property), [1] upper_bound_expression() (PrismIntegerVariable property), [1] use_dynamic_constraints() (SMTCounterExampleGeneratorOptions property) used_constants() (PrismProgram method), [1]

V

ValuationMapping (class in stormpy) (class in stormpy.storage) value() (ParametricSparseMatrixEntry method), [1] (SparseMatrixEntry method), [1] value_iteration (MinMaxMethod attribute)

Variable (class in stormpy) (class in stormpy.storage) variable() (PrismAssignment property), [1] variables() (JaniAutomaton property), [1] (PrismProgram property), [1] Version (class in stormpy.info)

W

walker_chae (NativeLinearEquationSolverMethod attribute)

WEAK (BisimulationType attribute) wellformed_constraints() (ConstraintCollector property)

X

Xor (OperatorType attribute), [1]

Z

Z3SmtSolver (class in stormpy.utility)