Index

A

action_index (JaniEdge attribute), [1] actions (SparseModelState attribute), [1] (SparseParametricModelState attribute), [1] add() (JaniOrderedAssignments method), [1] (SmtSolver method) add_automaton() (JaniModel method), [1] add_backward_implication_cuts (SMTCounterExampleGeneratorOptions attribute) 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 attribute) analyze_dft() (in module stormpy.dft) And() (Expression method), [1] apply_scheduler() (SparseMdp method), [1] (SparseParametricMdp method), [1] as_jani_model() (SymbolicModelDescription method) as_prism_program() (SymbolicModelDescription method) assignments (JaniEdgeDestination attribute), [1] (JaniLocation attribute), [1] (JaniTemplateEdge attribute), [1] (JaniTemplateEdgeDestination attribute), [1] (PrismUpdate attribute), [1] at() (ExplicitParametricQuantitativeCheckResult method) (ExplicitQualitativeCheckResult method) (ExplicitQuantitativeCheckResult method) AtomicExpressionFormula (class in stormpy) (class in stormpy.logic) AtomicLabelFormula (class in stormpy) (class in stormpy.logic) automata (JaniModel attribute), [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) 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 attribute) build_info (Version attribute) build_kept_actions (SubsystemBuilderOptions attribute) 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_state_mapping (SubsystemBuilderOptions attribute) 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) CENTERSAT (RegionResult attribute) CENTERVIOLATED (RegionResult attribute) check() (PDtmcInstantiationChecker 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 attribute) check_transitions_outside (SubsystemBuilderOptions attribute) 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] coefficient (FactorizedPolynomial attribute) color (JaniEdge attribute), [1] column (ParametricSparseMatrixEntry attribute), [1] (SparseMatrixEntry attribute), [1] commands (PrismModule attribute), [1] comparison_type (OperatorFormula attribute), [1] ComparisonType (class in stormpy) (class in stormpy.logic) compute_action_support() (SchedulerDouble method), [1] compute_prob01_states() (in module stormpy) compute_prob01max_states() (in module stormpy) compute_prob01min_states() (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 attribute), [1] (PrismProgram attribute), [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 attribute) 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_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) cut_time (SMTCounterExampleGeneratorStats attribute)

D

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

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

E

edges (JaniAutomaton attribute), [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 attribute) Environment (class in stormpy) Eq() (Expression method), [1] EquationSolverType (class in stormpy) evaluate() (FactorizedPolynomial method) (FactorizedRationalFunction method) (Polynomial method) (RationalFunction method) EventuallyFormula (class in stormpy) (class in stormpy.logic) EXISTSBOTH (RegionResult attribute) EXISTSSAT (RegionResult attribute) EXISTSVIOLATED (RegionResult attribute) 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 attribute), [1] (PrismAssignment attribute), [1] expression_manager (JaniModel attribute), [1] (PrismProgram attribute), [1] expression_variable (Constant attribute), [1] (JaniConstant attribute), [1] (JaniVariable attribute), [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) Formula (class in stormpy) (class in stormpy.logic) formulas (ModelFormulasPair attribute)

G

gather_derivatives() (in module stormpy.pars) gather_variables() (FactorizedPolynomial method) (FactorizedRationalFunction method) (Polynomial method) (RationalFunction method) GEQ (ComparisonType attribute), [1] Geq() (Expression method), [1] get() (BitVector method), [1] get_automaton_index() (JaniModel method), [1] get_boolean_value() (ModelReference method) 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) get_labels() (ItemLabeling method), [1] get_labels_of_state() (StateLabeling 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_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() (ExplicitParametricQuantitativeCheckResult method) (ExplicitQuantitativeCheckResult 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 attribute), [1] global_variables (JaniModel attribute), [1] GloballyFormula (class in stormpy) (class in stormpy.logic) gmmxx (EquationSolverType attribute) graph_preserving_constraints (ConstraintCollector attribute) GREATER (ComparisonType attribute), [1] Greater() (Expression method), [1] guard (JaniEdge attribute), [1] (JaniTemplateEdge attribute), [1] guard_expression (PrismCommand attribute), [1]

H

HA (JaniModelType attribute) has_bitvector_type() (Variable method) has_boolean_type() (Expression method), [1] (Variable method) has_bound (OperatorFormula attribute), [1] has_integer_type() (Expression method), [1] (Variable method) has_numerical_type() (Variable method) has_optimality_type (OperatorFormula attribute), [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 attribute), [1] (SparseRewardModel attribute), [1] (SymbolicSylvanParametricRewardModel attribute), [1] (SymbolicSylvanRewardModel attribute), [1]

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

I

I_Minus_P (MatrixFormat attribute) id (SparseModelAction attribute), [1] (SparseModelState attribute), [1] (SparseParametricModelAction attribute), [1] (SparseParametricModelState attribute), [1] (Variable attribute) Iff() (Expression method), [1] Implies() (Expression method), [1] initial_location_indices (JaniAutomaton attribute), [1] initial_states_restriction (JaniAutomaton attribute), [1] (JaniModel attribute), [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) interval_iteration (MinMaxMethod attribute) is_boolean (ExpressionType attribute), [1] is_constant() (FactorizedPolynomial method) (FactorizedRationalFunction method) (Polynomial method) (RationalFunction method) is_integer (ExpressionType attribute), [1] is_jani_model (SymbolicModelDescription attribute) is_literal() (Expression method), [1] is_no_variable (Variable attribute) is_one() (FactorizedPolynomial method) is_prism_program (SymbolicModelDescription attribute) is_probability_operator (Formula attribute), [1] is_rational (ExpressionType attribute), [1] is_reward_operator (Formula attribute), [1] is_subset_of() (FlatSet method) ItemLabeling (class in stormpy) (class in stormpy.storage) iterations (SMTCounterExampleGeneratorStats attribute)

J

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 attribute)

L

labels (SparseModelState attribute), [1] (SparseParametricModelState attribute), [1] left_subformula (BinaryPathFormula attribute), [1] LEQ (ComparisonType attribute), [1] Leq() (Expression method), [1] LESS (ComparisonType attribute), [1] Less() (Expression 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) location_variable (JaniAutomaton attribute), [1] locations (JaniAutomaton attribute), [1] long (Version attribute) LongRunAvarageOperator (class in stormpy) (class in stormpy.logic) LongRunAverageRewardFormula (class in stormpy) (class in stormpy.logic) 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 attribute), [1] MatrixFormat (class in stormpy.utility) Maximize (OptimizationDirection attribute) maximum_counterexamples (SMTCounterExampleGeneratorOptions attribute) maximum_iterations_after_counterexample (SMTCounterExampleGeneratorOptions attribute) MDP (JaniModelType attribute) (ModelType attribute), [1], [2] (PrismModelType attribute), [1] MdpParameterLiftingModelChecker (class in stormpy.pars) memory_size (SchedulerDouble attribute), [1] memoryless (SchedulerDouble attribute), [1] method (MinMaxSolverEnvironment attribute) milliseconds (class in stormpy.utility) Minimize (OptimizationDirection attribute) minmax_solver_environment (SolverEnvironment attribute)

MinMaxMethod (class in stormpy) MinMaxSolverEnvironment (class in stormpy) minor (Version attribute) Minus() (Expression method), [1] model (JaniChoiceOrigins attribute), [1] (ModelFormulasPair attribute) (SmtSolver attribute) (SubsystemBuilderReturnTypeDouble attribute) model_checking() (in module stormpy) model_checking_time (SMTCounterExampleGeneratorStats attribute) model_type (JaniModel attribute), [1] (PrismProgram attribute), [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 attribute), [1] Multiply() (Expression method), [1]

N

name (Constant attribute), [1] (JaniAutomaton attribute), [1] (JaniConstant attribute), [1] (JaniLocation attribute), [1] (JaniModel attribute), [1] (JaniVariable attribute), [1] (PrismModule attribute), [1] (Property attribute) (Variable attribute), [1] native (EquationSolverType attribute) Neq() (Expression method), [1] new_to_old_action_mapping (SubsystemBuilderReturnTypeDouble attribute) new_to_old_state_mapping (SubsystemBuilderReturnTypeDouble attribute) nominator (Rational attribute) (RationalFunction attribute) nondeterministic_choice_indices (SparseMdp attribute), [1] (SparseParametricMdp attribute), [1] nr_be() (DFT method) (ParametricDFT method)

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

O

observations (SparsePomdp attribute), [1] OperatorFormula (class in stormpy) (class in stormpy.logic)

optimality_type (OperatorFormula attribute), [1] OptimizationDirection (class in stormpy) 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) patch (Version attribute) Path (class in stormpy.utility) PathFormula (class in stormpy) (class in stormpy.logic) PCtmcInstantiator (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() (Expression method), [1] PMaInstantiator (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) precision (MinMaxSolverEnvironment attribute) precompute() (SMTCounterExampleGenerator method) predecessorK (Path attribute) predecessorNode (Path attribute) preserved_label_names (BuilderOptions attribute) print_row() (ParametricSparseMatrix method), [1] (SparseMatrix method), [1] PrismAssignment (class in stormpy) (class in stormpy.storage) PrismCommand (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) prob01max_states() (in module stormpy) prob01min_states() (in module stormpy) probability (JaniEdgeDestination attribute), [1] ProbabilityOperator (class in stormpy) (class in stormpy.logic) Property (class in stormpy) PTA (JaniModelType attribute) push() (SmtSolver method)

R

rank (Variable attribute) rate (JaniEdge attribute), [1] Rational (class in stormpy) rational_function() (FactorizedRationalFunction method) rational_search (MinMaxMethod attribute) RationalFunction (class in stormpy) RationalRF (in module stormpy) raw_formula (Property attribute) 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 attribute), [1] RewardOperator (class in stormpy) (class in stormpy.logic) right_subformula (BinaryPathFormula attribute), [1] row_iter() (ParametricSparseMatrix method), [1] (SparseMatrix method), [1]

S

Sat (SmtCheckResult attribute) scheduler (ExplicitQuantitativeCheckResult attribute) 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_with_choice_origins() (BuilderOptions method) set_force_sound() (SolverEnvironment method) set_graph_preserving() (PDtmcInstantiationChecker 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_standard_system_composition() (JaniModel method), [1] set_states() (StateLabeling method), [1] set_value() (ParametricSparseMatrixEntry method), [1] (SparseMatrixEntry method), [1] setup_time (SMTCounterExampleGeneratorStats attribute) SHA (JaniModelType attribute) short (Version attribute) ShortestPathsGenerator (class in stormpy.utility) silent (SMTCounterExampleGeneratorOptions attribute) 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 attribute) solver_time (SMTCounterExampleGeneratorStats attribute) SolverEnvironment (class in stormpy) sound_value_iteration (MinMaxMethod attribute) source_location_index (JaniEdge attribute), [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 attribute), [1] (SparseRewardModel attribute), [1] state_rewards (SparseParametricRewardModel attribute), [1] (SparseRewardModel attribute), [1] StateFormula (class in stormpy) (class in stormpy.logic) StateLabeling (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 attribute), [1] (UnaryStateFormula attribute), [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) 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 attribute), [1] template_edge (JaniEdge attribute), [1] threshold (OperatorFormula attribute), [1] threshold_expr (OperatorFormula attribute), [1] TimeOperator (class in stormpy) (class in stormpy.logic) 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 attribute) transform_to_discrete_time_model() (in module stormpy) transform_to_sparse_model() (in module stormpy) transition_rewards (SparseParametricRewardModel attribute), [1] (SparseRewardModel attribute), [1] transitions (SparseModelAction attribute), [1] (SparseParametricModelAction attribute), [1] type (Constant attribute), [1] (Expression attribute), [1] (JaniConstant attribute), [1] (Variable attribute)

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 attribute), [1] (PrismProgram attribute), [1]

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

V

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

variable (PrismAssignment attribute), [1] variables (JaniAutomaton attribute), [1] Version (class in stormpy.info)

W

WEAK (BisimulationType attribute)

wellformed_constraints (ConstraintCollector attribute)

Z

Z3SmtSolver (class in stormpy.utility)