Index

A

action_index() (JaniEdge property), [1] (PrismCommand 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_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() (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_timed_transition() (GSPNBuilder method) add_variable() (JaniVariableSet method), [1] (StateValuationsBuilder method), [1] 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 (OperatorType attribute), [1] And() (Expression method), [1] apply_scheduler() (SparseMA method), [1] (SparseMdp method), [1] (SparseParametricMA method), [1] (SparseParametricMdp method), [1] area() (ParameterRegion property) arity() (Expression property), [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) 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] Bool (DdMetaVariableType attribute), [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() (ExplicitModelBuilder_Double method) (ExplicitModelBuilder_RF method) (GSPNToJaniBuilder method) (ParametricSparseMatrixBuilder method), [1] (SMTCounterExampleGenerator 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_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_parametric_sparse_matrix() (in module stormpy) (in module stormpy.storage) 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) 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) choice_labeling() (SparseModelComponents property), [1] choice_origins() (SparseModelComponents property), [1] 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) collect_information() (in module stormpy) (in module stormpy.storage) 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_dependency_conflicts() (in module stormpy.dft)

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_transient_probabilities() (in module stormpy) ConditionalFormula (class in stormpy) (class in stormpy.logic) Conjunction() (Expression method), [1] 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) convert_to_ctmc() (SparseMA method), [1] convertible_to_ctmc() (SparseMA property), [1] count() (milliseconds method) create_boolean() (ExpressionManager method), [1] create_boolean_variable() (ExpressionManager method), [1] create_deadlock_properties() (GSPNToJaniBuilder method) 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) cut_time() (SMTCounterExampleGeneratorStats property)

D

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) decode_automaton_and_edge_index() (JaniModel method), [1] define_constants() (JaniModel method), [1] (PrismProgram method), [1] defined() (JaniConstant property), [1] (PrismConstant property), [1] (SchedulerChoiceDouble property), [1] definition() (PrismConstant property), [1] degree() (Polynomial method) DELETE_LABELS (EliminationLabelBehavior attribute) 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) DFTElement (class in stormpy.dft) DFTSymmetries (class in stormpy.dft) DirectEncodingOptions (class in stormpy) DirectEncodingParserOptions (class in stormpy) Disjunction() (Expression method), [1] distance() (Path property) DistributionDouble (class in stormpy) (class in stormpy.storage) Divide (OperatorType attribute), [1] Divide() (Expression method), [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_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] 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) 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] (SparseMA property), [1] (SparseModelComponents property), [1]

ExplicitExactQuantitativeCheckResult (class in stormpy) ExplicitModelBuilder_Double (class in stormpy) ExplicitModelBuilder_RF (class in stormpy) ExplicitParametricQuantitativeCheckResult (class in stormpy) ExplicitQualitativeCheckResult (class in stormpy) ExplicitQuantitativeCheckResult (class in stormpy) ExplicitStateLookup (class in stormpy) 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_Double method) (ExplicitModelBuilder_RF method) 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] (PrismLabel property), [1] expression_manager() (JaniModel property), [1] (PrismProgram 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)

F

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

flatten() (PrismProgram method), [1] flatten_composition() (JaniModel method), [1] 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_action_name() (PrismProgram method), [1] get_automaton() (JaniModel method), [1] get_automaton_index() (JaniModel method), [1] get_boolean_value() (ModelReference method) (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() (SchedulerChoiceDouble method), [1] (SchedulerDouble method), [1] get_choice_index() (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_current_row_group_count() (ParametricSparseMatrixBuilder method), [1] (SparseMatrixBuilder method), [1] get_deterministic_choice() (SchedulerChoiceDouble method), [1] get_distance() (ShortestPathsGenerator method) get_edge_index_set() (JaniChoiceOrigins method), [1] get_element() (DFT method) (ParametricDFT method) get_element_by_name() (DFT method) (ParametricDFT method) get_expression() (Variable method) get_id() (Place method) (Transition method) get_identifier_info() (ChoiceOrigins method), [1] get_immediate_transition() (GSPN method) get_immediate_transitions() (GSPN method) 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) (StateValuation method), [1] get_integer_variable() (PrismModule 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() (ParametricSparseMatrixBuilder method), [1] (SparseMatrixBuilder method), [1] get_last_row() (ParametricSparseMatrixBuilder method), [1] (SparseMatrixBuilder method), [1] get_meta_variable() (DdManager_Sylvan method), [1] get_module() (PrismProgram method), [1] get_module_indices_by_action_index() (PrismProgram method), [1] get_name() (GSPN method) (Place method) (Transition method) get_nr_available_actions() (SparseMdp 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() (SparseParametricPomdp method), [1] (SparsePomdp method), [1] get_operand() (Expression method), [1] get_output_arc_multiplicity() (Transition method) get_output_places() (Transition method) get_partitions() (GSPN method) get_path_as_list() (ShortestPathsGenerator method) get_place() (GSPN method) get_places() (GSPN method) get_priority() (Transition method) get_rate() (TimedTransition method) get_rational_value() (ModelReference method) (StateValuation method), [1] get_result() (JaniLocationExpander method), [1] 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_string() (StateValuation method), [1] get_synchronizing_action_indices() (PrismProgram method), [1] get_timed_transition() (GSPN method) get_timed_transitions() (GSPN method) get_transition() (GSPN method) get_truth_values() (ExplicitQualitativeCheckResult method) (SymbolicQualitativeCheckResult method) get_values() (ExplicitExactQuantitativeCheckResult method) (ExplicitParametricQuantitativeCheckResult method) (ExplicitQuantitativeCheckResult method) (HybridExactQuantitativeCheckResult method) (HybridParametricQuantitativeCheckResult method) (HybridQuantitativeCheckResult method) 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] get_weight() (ImmediateTransition method) 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] groups() (DFTSymmetries property) 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) has_boolean_type() (Expression method), [1] (Variable method) has_bound() (OperatorFormula property), [1] has_infinite_server_semantics() (TimedTransition method) has_integer_type() (Expression method), [1] (Variable method) has_k_server_semantics() (TimedTransition method) has_lower_bound() (BoundedUntilFormula property), [1] has_numerical_type() (Variable method) has_optimality_type() (OperatorFormula property), [1] has_rational_type() (Expression method), [1] (Variable method) has_restricted_capacity() (Place method) 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() (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() (DFTElement property) (ParametricDFTElement property) (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] immediate_transition_id_to_transition_id() (GSPN method) ImmediateTransition (class in stormpy.gspn) 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) (PartialPCtmcInstantiator method) (PartialPDtmcInstantiator method) (PartialPMaInstantiator method) (PartialPMdpInstantiator method) (PCtmcInstantiator method) (PDtmcInstantiator method) (PMaInstantiator method) (PMdpInstantiator method) instantiate_constants() (SymbolicModelDescription method) Int (DdMetaVariableType attribute), [1]

integer_variables() (PrismModule property), [1] interval_iteration (MinMaxMethod attribute) (NativeLinearEquationSolverMethod attribute) is_boolean() (ExpressionType property), [1] is_bounded_until_formula() (Formula property), [1] is_constant() (FactorizedPolynomial method) (FactorizedRationalFunction method) (Polynomial method) (RationalFunction method) is_enabled() (Transition method) is_eventually_formula() (Formula property), [1] is_function_application() (Expression property), [1] is_integer() (ExpressionType property), [1] is_jani_choice_origins() (ChoiceOrigins method), [1] is_jani_model() (SymbolicModelDescription property) is_literal() (Expression method), [1] is_multidimensional() (BoundedUntilFormula property), [1] is_no_variable() (Variable property) is_one() (FactorizedPolynomial method) 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_reward_operator() (Formula property), [1] is_subset_of() (FlatSet method) is_until_formula() (Formula property), [1] is_valid() (GSPN method) is_variable() (Expression method), [1] is_well_formed() (in module stormpy.dft) 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) 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)

K

KEEP_LABELS (EliminationLabelBehavior attribute)

kept_actions() (SubsystemBuilderReturnTypeDouble property)

L

labeled() (PrismCommand property), [1] labels() (PrismProgram property), [1] (SparseModelState property), [1] (SparseParametricModelState property), [1] LayoutInfo (class in stormpy.gspn) left_subformula() (BinaryPathFormula property), [1] (BoundedUntilFormula 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_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_string() (BitVector 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) lookup() (ExplicitStateLookup method) 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_sparse_model_builder() (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] markovian_states() (SparseMA property), [1] (SparseModelComponents 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] 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 method), [1] model() (JaniChoiceOrigins property), [1] (ModelFormulasPair property) (SmtSolver property) (SubsystemBuilderReturnTypeDouble property) model_checking() (in module stormpy) model_checking_fully_observable() (in module stormpy) model_checking_time() (SMTCounterExampleGeneratorStats property) model_type() (JaniInformationObject property), [1] (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) modularisation() (DFT method) (ParametricDFT method) module stormpy stormpy.dft stormpy.exceptions stormpy.gspn stormpy.info stormpy.logic stormpy.pars stormpy.storage stormpy.utility modules() (PrismProgram property), [1] Modulo (OperatorType attribute), [1] Modulo() (Expression method), [1] Multiply() (Expression method), [1]

N

name() (DdMetaVariable_Sylvan property), [1] (DFTElement property) (JaniAutomaton property), [1] (JaniConstant property), [1] (JaniLocation property), [1] (JaniModel property), [1] (JaniVariable property), [1] (ParametricDFTElement property) (PrismConstant property), [1] (PrismLabel property), [1] (PrismModule property), [1] (PrismRewardModel 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_row_group() (ParametricSparseMatrixBuilder method), [1] (SparseMatrixBuilder method), [1] new_to_old_action_mapping() (SubsystemBuilderReturnTypeDouble property) new_to_old_state_mapping() (SubsystemBuilderReturnTypeDouble property) no_weight_attached() (ImmediateTransition method) node_count() (Dd_Sylvan property), [1] nominator() (Rational property) (RationalFunction property) nondeterministic_choice_indices() (SparseMA property), [1] (SparseMdp property), [1] (SparseParametricMA property), [1] (SparseParametricMdp property), [1]

Not (OperatorType attribute), [1] NotEqual (OperatorType attribute), [1] nr_automata() (JaniInformationObject property), [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_edges() (JaniInformationObject property), [1] nr_elements() (DFT method) (ParametricDFT method) nr_entries() (ParametricSparseMatrix property), [1] (SparseMatrix property), [1] nr_modules() (PrismProgram property), [1] nr_observations() (SparseParametricPomdp property), [1] (SparsePomdp property), [1] nr_rows() (ParametricSparseMatrix property), [1] (SparseMatrix property), [1] nr_terms() (Polynomial property) 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) (Rational property) (RationalFunction property)

O

observability_classes() (SparseModelComponents property), [1] observations() (SparseParametricPomdp property), [1] (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] optimistic_value_iteration (MinMaxMethod attribute) (NativeLinearEquationSolverMethod attribute) 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) ParametricDFTElement (class in stormpy.dft) 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) parse() (ExpressionParser method), [1] (GSPNParser method) 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) partial() (SchedulerDouble 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) 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) Place (class in stormpy.gspn) player1_matrix() (SparseModelComponents property), [1] 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) (NativeSolverEnvironment property) precompute() (SMTCounterExampleGenerator method) predecessorK() (Path property) predecessorNode() (Path property) preprocess_symbolic_input() (in module stormpy) preserved_label_names() (BuilderOptions property) print_row() (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() (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)

R

rank() (Variable property) rate() (JaniEdge property), [1] rate_transitions() (SparseModelComponents property), [1] Rational (class in stormpy) rational_function() (FactorizedRationalFunction method) rational_search (MinMaxMethod attribute) (NativeLinearEquationSolverMethod attribute) 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) 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() (ParametricSparseMatrixBuilder method), [1] (SparseMatrixBuilder method), [1] reset() (SmtSolver method) restrict_commands() (PrismProgram method), [1] restrict_edges() (JaniModel method), [1] reward_models() (PrismProgram property), [1] (SparseModelComponents property), [1] reward_name() (RewardOperator property), [1] RewardOperator (class in stormpy) (class in stormpy.logic) right_subformula() (BinaryPathFormula property), [1] (BoundedUntilFormula property), [1] rotation() (LayoutInfo property) 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_all_labels() (BuilderOptions method) set_build_all_reward_models() (BuilderOptions method) set_build_choice_labels() (BuilderOptions method) set_build_state_valuations() (BuilderOptions method) set_build_with_choice_origins() (BuilderOptions method) set_capacity() (Place method) set_choices() (ChoiceLabeling method), [1] set_force_sound() (SolverEnvironment method) set_graph_preserving() (PDtmcExactInstantiationChecker method) (PDtmcInstantiationChecker method) (PMdpExactInstantiationChecker method) (PMdpInstantiationChecker 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_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) (ParametricCheckTask method) set_rate() (TimedTransition method) set_settings() (in module stormpy) set_single_server_semantics() (TimedTransition method) set_standard_system_composition() (JaniModel method), [1] set_states() (StateLabeling method), [1] set_transition_layout_info() (GSPNBuilder method) set_value() (ParametricSparseMatrixEntry method), [1] (SparseMatrixEntry method), [1] set_weight() (ImmediateTransition method) setup_time() (SMTCounterExampleGeneratorStats property) SHA (JaniModelType attribute) short (Version attribute) ShortestPathsGenerator (class in stormpy.utility) silent() (SMTCounterExampleGeneratorOptions property) simplify() (Expression method), [1] (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) 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] 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) 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) 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) specify() (RegionModelChecker method) STA (JaniModelType attribute) state_action_rewards() (SparseParametricRewardModel property), [1] (SparseRewardModel property), [1] state_domain_size() (JaniInformationObject property), [1] state_labeling() (SparseModelComponents property), [1] state_rewards() (SparseParametricRewardModel property), [1] (SparseRewardModel property), [1] state_valuations() (SparseModelComponents 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) StateValuationsBuilder (class in stormpy) (class in stormpy.storage) store_as_string() (BitVector method), [1] 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.gspn 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_formulas() (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) symmetries() (DFT method) (ParametricDFT method)

T

TA (JaniModelType attribute) target_location_index() (JaniEdgeDestination property), [1] template_edge() (JaniEdge property), [1] threshold() (OperatorFormula property), [1] threshold_expr() (OperatorFormula property), [1] timed_transition_id_to_transition_id() (GSPN 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_smt2() (FactorizedPolynomial method) (FactorizedRationalFunction method) (Polynomial method) (RationalFunction method) top_level_element() (DFT property) (ParametricDFT property) topological (EquationSolverType attribute) (MinMaxMethod attribute)

topological_cuda (MinMaxMethod attribute) topological_sort() (in module stormpy) total_degree() (Polynomial property) transform() (JaniLocationExpander method), [1] 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 method) transition_id_to_timed_transition_id() (GSPN method) transition_matrix() (SparseModelComponents property), [1] transition_rewards() (SparseParametricRewardModel property), [1] (SparseRewardModel property), [1] TransitionPartition (class in stormpy.gspn) transitions() (SparseModelAction property), [1] (SparseParametricModelAction property), [1] (TransitionPartition property) type() (DdMetaVariable_Sylvan property), [1] (Expression property), [1] (JaniConstant property), [1] (PrismConstant 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() (BoundedUntilFormula property), [1] (PrismIntegerVariable property), [1] use_dynamic_constraints() (SMTCounterExampleGeneratorOptions property) 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 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

x() (LayoutInfo property)

Xor (OperatorType attribute), [1]

Y

y() (LayoutInfo property)

Z

Z3SmtSolver (class in stormpy.utility)