Stormpy.storage¶

class BitVector¶

get(self: stormpy.storage.storage.BitVector, index: int) → bool ¶

number_of_set_bits(self: stormpy.storage.storage.BitVector) → int ¶

set(self: stormpy.storage.storage.BitVector, index: int, value: bool = True) → None¶: Set

size(self: stormpy.storage.storage.BitVector) → int ¶

class ChoiceLabeling¶: Labeling for choices

class ChoiceOrigins¶

This class represents the origin of choices of a model in terms of the input model spec.

get_choice_info(self: stormpy.storage.storage.ChoiceOrigins, identifier: int) → str ¶: human readable string

get_identifier_info(self: stormpy.storage.storage.ChoiceOrigins, identifier: int) → str ¶: human readable string

class Constant¶

A constant in a Prism program

property defined¶: Is the constant defined?

property expression_variable¶: Expression variable

property name¶: Constant name

property type¶: The type of the constant

class DistributionDouble¶: Finite Support Distribution

class Expression¶

Holds an expression

And(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) → stormpy.storage.storage.Expression¶

Conjunction(arg0: List[stormpy.storage.storage.Expression]) → stormpy.storage.storage.Expression¶

Disjunction(arg0: List[stormpy.storage.storage.Expression]) → stormpy.storage.storage.Expression¶

Eq(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) → stormpy.storage.storage.Expression¶

Geq(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) → stormpy.storage.storage.Expression¶

Greater(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) → stormpy.storage.storage.Expression¶

Iff(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) → stormpy.storage.storage.Expression¶

Implies(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) → stormpy.storage.storage.Expression¶

Leq(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) → stormpy.storage.storage.Expression¶

Less(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) → stormpy.storage.storage.Expression¶

Minus(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) → stormpy.storage.storage.Expression¶

Multiply(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) → stormpy.storage.storage.Expression¶

Neq(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) → stormpy.storage.storage.Expression¶

Or(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) → stormpy.storage.storage.Expression¶

Plus(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) → stormpy.storage.storage.Expression¶

property arity¶: The arity of the expression

contains_variable(self: stormpy.storage.storage.Expression, variables: Set[stormpy.storage.storage.Variable]) → bool ¶: Check if the expression contains any of the given variables.

contains_variables(self: stormpy.storage.storage.Expression) → bool ¶: Check if the expression contains variables.

evaluate_as_bool(self: stormpy.storage.storage.Expression) → bool ¶: Get the boolean value this expression evaluates to

evaluate_as_double(self: stormpy.storage.storage.Expression) → float ¶: Get the double value this expression evaluates to

evaluate_as_int(self: stormpy.storage.storage.Expression) → int ¶: Get the integer value this expression evaluates to

evaluate_as_rational(self: stormpy.storage.storage.Expression) → __gmp_expr<__mpq_struct [1], __mpq_struct [1]>¶: Get the rational number this expression evaluates to

get_operand(self: stormpy.storage.storage.Expression, operandIndex: int) → stormpy.storage.storage.Expression¶: Get the operand at the given index

get_variables(self: stormpy.storage.storage.Expression) → Set[stormpy.storage.storage.Variable]¶: Get the variables

has_boolean_type(self: stormpy.storage.storage.Expression) → bool ¶: Check if the expression is a boolean

has_integer_type(self: stormpy.storage.storage.Expression) → bool ¶: Check if the expression is an integer

has_rational_type(self: stormpy.storage.storage.Expression) → bool ¶: Check if the expression is a rational

identifier(self: stormpy.storage.storage.Expression) → str ¶: Retrieves the identifier associated with this expression if this expression is a variable

property is_function_application¶: True iff the expression is a function application (of any sort

is_literal(self: stormpy.storage.storage.Expression) → bool ¶: Check if the expression is a literal

is_variable(self: stormpy.storage.storage.Expression) → bool ¶: Check if the expression is a variable

property manager¶: Get the manager

property operator¶: The operator of the expression (if it is a function application)

substitute(self: stormpy.storage.storage.Expression, substitution_map: Dict[stormpy.storage.storage.Variable, stormpy.storage.storage.Expression]) → stormpy.storage.storage.Expression¶

property type¶: Get the Type

class ExpressionManager¶

Manages variables for expressions

create_boolean(self: stormpy.storage.storage.ExpressionManager, boolean: bool) → storm::expressions::Expression¶: Create expression from boolean

create_boolean_variable(self: stormpy.storage.storage.ExpressionManager, name: str, auxiliary: bool = False) → storm::expressions::Variable¶: create Boolean variable

create_integer(self: stormpy.storage.storage.ExpressionManager, integer: int) → storm::expressions::Expression¶: Create expression from integer number

create_integer_variable(self: stormpy.storage.storage.ExpressionManager, name: str, auxiliary: bool = False) → storm::expressions::Variable¶: create Integer variable

create_rational(self: stormpy.storage.storage.ExpressionManager, rational: __gmp_expr<__mpq_struct [1], __mpq_struct [1]>) → storm::expressions::Expression¶: Create expression from rational number

create_rational_variable(self: stormpy.storage.storage.ExpressionManager, name: str, auxiliary: bool = False) → storm::expressions::Variable¶: create Rational variable

class ExpressionParser¶

Parser for storm-expressions

parse(self: stormpy.storage.storage.ExpressionParser, string: str, ignore_error: bool = False) → stormpy.storage.storage.Expression¶: parse

set_identifier_mapping(self: stormpy.storage.storage.ExpressionParser, arg0: Dict[str, stormpy.storage.storage.Expression]) → None¶: sets identifiers

class ExpressionType¶

The type of an expression

property is_boolean¶

property is_integer¶

property is_rational¶

class ItemLabeling¶

Labeling

add_label(self: stormpy.storage.storage.ItemLabeling, label: str) → None¶: Add label

contains_label(self: stormpy.storage.storage.ItemLabeling, label: str) → bool ¶: Check if the given label is contained in the labeling

get_labels(self: stormpy.storage.storage.ItemLabeling) → Set[str]¶: Get all labels

class JaniAssignment¶

Jani Assignment

property expression¶

class JaniAutomaton¶

A Jani Automation

add_edge(self: stormpy.storage.storage.JaniAutomaton, edge: storm::jani::Edge) → None¶

add_initial_location(self: stormpy.storage.storage.JaniAutomaton, index: int) → None¶

add_location(self: stormpy.storage.storage.JaniAutomaton, location: storm::jani::Location) → int ¶: adds a new location, returns the index

property edges¶: get edges

property initial_location_indices¶

property initial_states_restriction¶: initial state restriction

property location_variable¶

property locations¶

property name¶

property variables¶

class JaniBoundedIntegerVariable¶: A Bounded Integer

class JaniChoiceOrigins¶

This class represents for each choice the origin in the jani spec.

get_edge_index_set(self: stormpy.storage.storage.JaniChoiceOrigins, choice_index: int) → stormpy.core.FlatSet¶: returns the set of edges that induced the choice

property model¶: retrieves the associated JANI model

class JaniConstant¶

A Constant in JANI

property defined¶: is constant defined by some expression

property expression_variable¶: expression variable for this constant

property name¶: name of constant

property type¶: type of constant

class JaniEdge¶

A Jani Edge

property action_index¶: action index

property color¶: color for the edge

property destinations¶: edge destinations

property guard¶: edge guard

has_silent_action(self: stormpy.storage.storage.JaniEdge) → bool ¶: Is the edge labelled with the silent action

property nr_destinations¶: nr edge destinations

property rate¶: edge rate

property source_location_index¶: index for source location

substitute(self: stormpy.storage.storage.JaniEdge, mapping: Dict[storm::expressions::Variable, storm::expressions::Expression]) → None¶

property template_edge¶: template edge

class JaniEdgeDestination¶

Destination in Jani

property assignments¶

property probability¶

property target_location_index¶

class JaniInformationObject¶

An object holding information about a JANI model

property avg_var_domain_size¶

property model_type¶

property nr_automata¶

property nr_edges¶

property nr_variables¶

property state_domain_size¶

class JaniLocation¶

A Location in JANI

property assignments¶: location assignments

property name¶: name of the location

class JaniModel¶

A Jani Model

add_automaton(self: stormpy.storage.storage.JaniModel, automaton: storm::jani::Automaton) → int ¶: add an automaton (with a unique name)

property automata¶: get automata

check_valid(self: stormpy.storage.storage.JaniModel) → None¶: Some basic checks to ensure validity

property constants¶: get constants

decode_automaton_and_edge_index(arg0: int) → Tuple[int, int]¶: get edge and automaton from edge/automaton index

define_constants(self: stormpy.storage.storage.JaniModel, map: Dict[storm::expressions::Variable, storm::expressions::Expression]) → stormpy.storage.storage.JaniModel¶: define constants with a mapping from the corresponding expression variables to expressions

encode_automaton_and_edge_index(arg0: int, arg1: int) → int ¶: get edge/automaton-index

property expression_manager¶: get expression manager

finalize(self: stormpy.storage.storage.JaniModel) → None¶: finalizes the model. After this action, be careful changing the data structure.

get_automaton_index(self: stormpy.storage.storage.JaniModel, name: str) → int ¶: get index for automaton name

get_constant(self: stormpy.storage.storage.JaniModel, name: str) → storm::jani::Constant¶: get constant by name

property global_variables¶

has_standard_composition(self: stormpy.storage.storage.JaniModel) → bool ¶: is the composition the standard composition

property has_undefined_constants¶: Flag if program has undefined constants

property initial_states_restriction¶: initial states restriction

make_standard_compliant(self: stormpy.storage.storage.JaniModel) → None¶: make standard JANI compliant

property model_type¶: Model type

property name¶: model name

remove_constant(self: stormpy.storage.storage.JaniModel, constant_name: str) → None¶: remove a constant. Make sure the constant does not appear in the model.

replace_automaton(self: stormpy.storage.storage.JaniModel, index: int, new_automaton: storm::jani::Automaton) → None¶: replace automaton at index

restrict_edges(self: stormpy.storage.storage.JaniModel, edge_set: stormpy.core.FlatSet) → stormpy.storage.storage.JaniModel¶: restrict model to edges given by set

set_model_type(self: stormpy.storage.storage.JaniModel, arg0: stormpy.core.JaniModelType) → None¶: Sets (only) the model type

set_standard_system_composition(self: stormpy.storage.storage.JaniModel) → None¶: sets the composition to the standard composition

substitute_constants(self: stormpy.storage.storage.JaniModel) → stormpy.storage.storage.JaniModel¶: substitute constants

substitute_functions(self: stormpy.storage.storage.JaniModel) → None¶: substitute functions

to_dot(self: stormpy.storage.storage.JaniModel) → str ¶

property undefined_constants_are_graph_preserving¶: Flag if the undefined constants do not change the graph structure

class JaniOrderedAssignments¶

Set of assignments

add(self: stormpy.storage.storage.JaniOrderedAssignments, new_assignment: storm::jani::Assignment, add_to_existing: bool=False) → bool ¶

clone(self: stormpy.storage.storage.JaniOrderedAssignments) → stormpy.storage.storage.JaniOrderedAssignments¶: clone assignments (performs a deep copy)

substitute(self: stormpy.storage.storage.JaniOrderedAssignments, substitution_map: Dict[storm::expressions::Variable, storm::expressions::Expression]) → None¶: substitute in rhs according to given substitution map

class JaniTemplateEdge¶

Template edge, internal data structure for edges

add_destination(self: stormpy.storage.storage.JaniTemplateEdge, arg0: storm::jani::TemplateEdgeDestination) → None¶

property assignments¶

property destinations¶

property guard¶

class JaniTemplateEdgeDestination¶

Template edge destination, internal data structure for edge destinations

property assignments¶

class JaniVariable¶

A Variable in JANI

property expression_variable¶: expression variable for this variable

property name¶: name of constant

class JaniVariableSet¶

Jani Set of Variables

add_bounded_integer_variable(self: stormpy.storage.storage.JaniVariableSet, variable: storm::jani::BoundedIntegerVariable) → storm::jani::BoundedIntegerVariable¶

add_variable(self: stormpy.storage.storage.JaniVariableSet, arg0: storm::jani::Variable) → None¶

empty(self: stormpy.storage.storage.JaniVariableSet) → bool ¶: is there a variable in the set?

get_variable_by_expr_variable(self: stormpy.storage.storage.JaniVariableSet, arg0: storm::expressions::Variable) → storm::jani::Variable¶

get_variable_by_name(self: stormpy.storage.storage.JaniVariableSet, arg0: str) → storm::jani::Variable¶

class ModelType¶

Type of the model

CTMC = ModelType.CTMC¶

DTMC = ModelType.DTMC¶

MA = ModelType.MA¶

MDP = ModelType.MDP¶

POMDP = ModelType.POMDP¶

class OperatorType¶

Type of an operator (of any sort)

And = OperatorType.And¶

Ceil = OperatorType.Ceil¶

Divide = OperatorType.Divide¶

Equal = OperatorType.Equal¶

Floor = OperatorType.Floor¶

Greater = OperatorType.Greater¶

GreaterOrEqual = OperatorType.GreaterOrEqual¶

Iff = OperatorType.Iff¶

Implies = OperatorType.Implies¶

Ite = OperatorType.Ite¶

Less = OperatorType.Less¶

LessOrEqual = OperatorType.LessOrEqual¶

Max = OperatorType.Max¶

Min = OperatorType.Min¶

Minus = OperatorType.Minus¶

Modulo = OperatorType.Modulo¶

Not = OperatorType.Not¶

NotEqual = OperatorType.NotEqual¶

Or = OperatorType.Or¶

Plus = OperatorType.Plus¶

Power = OperatorType.Power¶

Times = OperatorType.Times¶

Xor = OperatorType.Xor¶

class ParametricSparseMatrix¶

Parametric sparse matrix

get_row(self: stormpy.storage.storage.ParametricSparseMatrix, row: int) → storm::storage::SparseMatrix<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true> >::rows¶: Get row

get_row_group_end(self: stormpy.storage.storage.ParametricSparseMatrix, arg0: int) → int ¶

get_row_group_start(self: stormpy.storage.storage.ParametricSparseMatrix, arg0: int) → int ¶

get_rows(self: stormpy.storage.storage.ParametricSparseMatrix, row_start: int, row_end: int) → storm::storage::SparseMatrix<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true> >::rows¶: Get rows from start to end

property has_trivial_row_grouping¶: Trivial row grouping

property nr_columns¶: Number of columns

property nr_entries¶: Number of non-zero entries

property nr_rows¶: Number of rows

print_row(self: stormpy.storage.storage.ParametricSparseMatrix, row: int) → str ¶: Print row

row_iter(self: stormpy.storage.storage.ParametricSparseMatrix, row_start: int, row_end: int) → iterator¶: Get iterator from start to end

submatrix(self: stormpy.storage.storage.ParametricSparseMatrix, row_constraint: stormpy.storage.storage.BitVector, column_constraint: stormpy.storage.storage.BitVector, insert_diagonal_entries: bool = False) → stormpy.storage.storage.ParametricSparseMatrix¶: Get submatrix

class ParametricSparseMatrixEntry¶

Entry of parametric sparse matrix

property column¶: Column

set_value(self: stormpy.storage.storage.ParametricSparseMatrixEntry, value: carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true>) → None¶: Set value

value(self: stormpy.storage.storage.ParametricSparseMatrixEntry) → carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true>¶: Value

class ParametricSparseMatrixRows¶: Set of rows in a parametric sparse matrix

class PrismAssignment¶

An assignment in prism

property expression¶: Expression for the update

property variable¶: Variable that is updated

class PrismBooleanVariable¶: A program boolean variable in a Prism program

class PrismCommand¶

A command in a Prism program

property global_index¶: Get global index

property guard_expression¶: Get guard expression

property updates¶: Updates in the command

class PrismIntegerVariable¶

A program integer variable in a Prism program

property lower_bound_expression¶: The the lower bound expression of this integer variable

property upper_bound_expression¶: The the upper bound expression of this integer variable

class PrismModelType¶

Type of the prism model

CTMC = PrismModelType.CTMC¶

CTMDP = PrismModelType.CTMDP¶

DTMC = PrismModelType.DTMC¶

MA = PrismModelType.MA¶

MDP = PrismModelType.MDP¶

UNDEFINED = PrismModelType.UNDEFINED¶

class PrismModule¶

A module in a Prism program

property boolean_variables¶: All boolean Variables of this module

property commands¶: Commands in the module

property integer_variables¶: All integer Variables of this module

property name¶: Name of the module

class PrismProgram¶

A Prism Program

property constants¶: Get Program Constants

define_constants(self: stormpy.storage.storage.PrismProgram, arg0: Dict[storm::expressions::Variable, storm::expressions::Expression]) → stormpy.storage.storage.PrismProgram¶: Define constants

property expression_manager¶: Get the expression manager for expressions in this program

get_label_expression(self: stormpy.storage.storage.PrismProgram, label: str) → storm::expressions::Expression¶: Get the expression of the given label.

property hasUndefinedConstants¶: Does the program have undefined constants?

property has_undefined_constants¶: Flag if program has undefined constants

property isDeterministicModel¶: Does the program describe a deterministic model?

property model_type¶: Model type

property modules¶: Modules in the program

property nr_modules¶: Number of modules

restrict_commands(self: stormpy.storage.storage.PrismProgram, arg0: stormpy.core.FlatSet) → stormpy.storage.storage.PrismProgram¶: Restrict commands

simplify(self: stormpy.storage.storage.PrismProgram) → stormpy.storage.storage.PrismProgram¶: Simplify

substitute_constants(self: stormpy.storage.storage.PrismProgram) → stormpy.storage.storage.PrismProgram¶: Substitute constants within program

to_jani(self: stormpy.storage.storage.PrismProgram, properties: List[stormpy.core.Property], all_variables_global: bool = True, suffix: str = '') → Tuple[storm::jani::Model, List[stormpy.core.Property]]¶: Transform to Jani program

property undefined_constants_are_graph_preserving¶: Flag if the undefined constants do not change the graph structure

used_constants(self: stormpy.storage.storage.PrismProgram) → List[storm::prism::Constant]¶: Compute Used Constants

property variables¶: Get all Expression Variables used by the program

class PrismUpdate¶

An update in a Prism command

property assignments¶: Assignments in the update

property probability_expression¶: The probability expression for this update

class PrismVariable¶

A program variable in a Prism program

property expression_variable¶: The expression variable corresponding to the variable

property initial_value_expression¶: The expression represented the initial value of the variable

property name¶: Variable name

class SchedulerChoiceDouble¶

A choice of a finite memory scheduler

property defined¶: Is the choice defined by the scheduler?

property deterministic¶: Is the choice deterministic (given by a Dirac distribution)?

get_choice(self: stormpy.storage.storage.SchedulerChoiceDouble) → storm::storage::Distribution<double, unsigned long>¶: Get the distribution over the actions

get_deterministic_choice(self: stormpy.storage.storage.SchedulerChoiceDouble) → int ¶: Get the deterministic choice

class SchedulerDouble¶

A Finite Memory Scheduler

compute_action_support(self: stormpy.storage.storage.SchedulerDouble, nondeterministic_choice_indices: List[int]) → stormpy.storage.storage.BitVector¶

property deterministic¶: Is the scheduler deterministic?

get_choice(self: stormpy.storage.storage.SchedulerDouble, state_index: int, memory_index: int = 0) → storm::storage::SchedulerChoice<double>¶

property memory_size¶: How much memory does the scheduler take?

property memoryless¶: Is the scheduler memoryless?

property partial¶: Is the scheduler partial?

class SimpleValuation¶

Valuations for storm variables

get_boolean_value(self: stormpy.storage.storage.SimpleValuation, arg0: storm::expressions::Variable) → bool ¶

get_integer_value(self: stormpy.storage.storage.SimpleValuation, arg0: storm::expressions::Variable) → int ¶

class SparseCtmc¶: CTMC in sparse representation

class SparseDtmc¶: DTMC in sparse representation

class SparseMA¶

MA in sparse representation

apply_scheduler(self: stormpy.storage.storage.SparseMA, scheduler: storm::storage::Scheduler<double>, drop_unreachable_states: bool=True) → stormpy.storage.storage._SparseModel¶: apply scheduler

convert_to_ctmc(self: stormpy.storage.storage.SparseMA) → stormpy.storage.storage.SparseCtmc¶: Convert the MA into a CTMC.

property convertible_to_ctmc¶: Check whether the MA can be converted into a CTMC.

property nondeterministic_choice_indices¶

class SparseMatrix¶

Sparse matrix

get_row(self: stormpy.storage.storage.SparseMatrix, row: int) → storm::storage::SparseMatrix<double>::rows¶: Get row

get_row_group_end(self: stormpy.storage.storage.SparseMatrix, arg0: int) → int ¶

get_row_group_start(self: stormpy.storage.storage.SparseMatrix, arg0: int) → int ¶

get_rows(self: stormpy.storage.storage.SparseMatrix, row_start: int, row_end: int) → storm::storage::SparseMatrix<double>::rows¶: Get rows from start to end

property has_trivial_row_grouping¶: Trivial row grouping

property nr_columns¶: Number of columns

property nr_entries¶: Number of non-zero entries

property nr_rows¶: Number of rows

print_row(self: stormpy.storage.storage.SparseMatrix, row: int) → str ¶: Print rows from start to end

row_iter(self: stormpy.storage.storage.SparseMatrix, row_start: int, row_end: int) → iterator¶: Get iterator from start to end

submatrix(self: stormpy.storage.storage.SparseMatrix, row_constraint: stormpy.storage.storage.BitVector, column_constraint: stormpy.storage.storage.BitVector, insert_diagonal_entries: bool = False) → stormpy.storage.storage.SparseMatrix¶: Get submatrix

class SparseMatrixEntry¶

Entry of sparse matrix

property column¶: Column

set_value(self: stormpy.storage.storage.SparseMatrixEntry, value: float) → None¶: Set value

value(self: stormpy.storage.storage.SparseMatrixEntry) → float ¶: Value

class SparseMatrixRows¶: Set of rows in a sparse matrix

class SparseMdp¶

MDP in sparse representation

apply_scheduler(self: stormpy.storage.storage.SparseMdp, scheduler: storm::storage::Scheduler<double>, drop_unreachable_states: bool=True) → stormpy.storage.storage._SparseModel¶: apply scheduler

property nondeterministic_choice_indices¶

class SparseModelAction¶

Action for state in sparse model

property id¶: Id

property transitions¶: Get transitions

class SparseModelActions¶: Actions for state in sparse model

class SparseModelState¶

State in sparse model

property actions¶: Get actions

property id¶: Id

property labels¶: Labels

class SparseModelStates¶: States in sparse model

class SparseParametricCtmc¶: pCTMC in sparse representation

class SparseParametricDtmc¶: pDTMC in sparse representation

class SparseParametricMA¶

pMA in sparse representation

apply_scheduler(self: stormpy.storage.storage.SparseParametricMA, scheduler: storm::storage::Scheduler<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true> >, drop_unreachable_states: bool=True) → stormpy.storage.storage._SparseParametricModel¶: apply scheduler

property nondeterministic_choice_indices¶

class SparseParametricMdp¶

pMDP in sparse representation

apply_scheduler(self: stormpy.storage.storage.SparseParametricMdp, scheduler: storm::storage::Scheduler<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true> >, drop_unreachable_states: bool=True) → stormpy.storage.storage._SparseParametricModel¶: apply scheduler

property nondeterministic_choice_indices¶

class SparseParametricModelAction¶

Action for state in sparse parametric model

property id¶: Id

property transitions¶: Get transitions

class SparseParametricModelActions¶: Actions for state in sparse parametric model

class SparseParametricModelState¶

State in sparse parametric model

property actions¶: Get actions

property id¶: Id

property labels¶: Labels

class SparseParametricModelStates¶: States in sparse parametric model

class SparseParametricRewardModel¶

Reward structure for parametric sparse models

get_state_action_reward(self: stormpy.storage.storage.SparseParametricRewardModel, arg0: int) → carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true>¶

get_state_reward(self: stormpy.storage.storage.SparseParametricRewardModel, arg0: int) → carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true>¶

property has_state_action_rewards¶

property has_state_rewards¶

property has_transition_rewards¶

reduce_to_state_based_rewards(self: stormpy.storage.storage.SparseParametricRewardModel, transition_matrix: storm::storage::SparseMatrix<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true> >, only_state_rewards: bool) → None¶: Reduce to state-based rewards

property state_action_rewards¶

property state_rewards¶

property transition_rewards¶

class SparsePomdp¶

POMDP in sparse representation

property nr_observations¶

property observations¶

class SparseRewardModel¶

Reward structure for sparse models

get_state_action_reward(self: stormpy.storage.storage.SparseRewardModel, arg0: int) → float ¶

get_state_reward(self: stormpy.storage.storage.SparseRewardModel, arg0: int) → float ¶

get_zero_reward_states(self: stormpy.storage.storage.SparseRewardModel, transition_matrix: storm::storage::SparseMatrix<double>) → stormpy.storage.storage.BitVector¶: get states where all rewards are zero

property has_state_action_rewards¶

property has_state_rewards¶

property has_transition_rewards¶

reduce_to_state_based_rewards(self: stormpy.storage.storage.SparseRewardModel, transition_matrix: storm::storage::SparseMatrix<double>, only_state_rewards: bool) → None¶: Reduce to state-based rewards

property state_action_rewards¶

property state_rewards¶

property transition_rewards¶

class StateGenerator¶

Interactively explore states using Storm’s PrismNextStateGenerator.

Variables: program – A PRISM program.

current_state_satisfies(self: stormpy.storage.storage.StateGenerator, arg0: storm::expressions::Expression) → bool ¶

Check if the currently loaded state satisfies the given expression.

Parameters: expression (stormpy.Expression) – The expression to check against.
Return type: bool

current_state_to_valuation(self: stormpy.storage.storage.StateGenerator) → stormpy.storage.storage.ValuationMapping¶

Return a valuation for the currently loaded state.

Return type: stormpy.ValuationMapping

expand(self: stormpy.storage.storage.StateGenerator) → List[List[Tuple[int, __gmp_expr<__mpq_struct [1], __mpq_struct [1]>]]]¶

Expand the currently loaded state and return its successors.

Return type: [[(state_id, probability)]]

load(self: stormpy.storage.storage.StateGenerator, arg0: int) → None¶

Parameters: state_id – The ID of the state to load.

load_initial_state(self: stormpy.storage.storage.StateGenerator) → int ¶

Loads the (unique) initial state. Multiple initial states are not supported.

Return type: the ID of the initial state.

class StateLabeling¶

Labeling for states

add_label_to_state(self: stormpy.storage.storage.StateLabeling, label: str, state: int) → None¶: Add label to state

get_labels_of_state(self: stormpy.storage.storage.StateLabeling, state: int) → Set[str]¶: Get labels of given state

get_states(self: stormpy.storage.storage.StateLabeling, label: str) → stormpy.storage.storage.BitVector¶: Get all states which have the given label

has_state_label(self: stormpy.storage.storage.StateLabeling, label: str, state: int) → bool ¶: Check if the given state has the given label

set_states(self: stormpy.storage.storage.StateLabeling, label: str, states: stormpy.storage.storage.BitVector) → None¶: Set all states which have the given label

class StateValuation¶

Valuations for explicit states

get_state(self: stormpy.storage.storage.StateValuation, arg0: int) → storm::expressions::SimpleValuation¶

class SymbolicSylvanCtmc¶: CTMC in symbolic representation

class SymbolicSylvanDtmc¶: DTMC in symbolic representation

class SymbolicSylvanMA¶: MA in symbolic representation

class SymbolicSylvanMdp¶: MDP in symbolic representation

class SymbolicSylvanParametricCtmc¶: pCTMC in symbolic representation

class SymbolicSylvanParametricDtmc¶: pDTMC in symbolic representation

class SymbolicSylvanParametricMA¶: pMA in symbolic representation

class SymbolicSylvanParametricMdp¶: pMDP in symbolic representation

class SymbolicSylvanParametricRewardModel¶

Reward structure for parametric symbolic models

property has_state_action_rewards¶

property has_state_rewards¶

property has_transition_rewards¶

class SymbolicSylvanRewardModel¶

Reward structure for symbolic models

property has_state_action_rewards¶

property has_state_rewards¶

property has_transition_rewards¶

class ValuationMapping¶

A valuation mapping for a state consists of a mapping from variable to value for each of the three types.

property boolean_values¶

property integer_values¶

property rational_values¶

class Variable¶

Represents a variable

get_expression(self: stormpy.storage.storage.Variable) → storm::expressions::Expression¶: Get expression from variable

has_bitvector_type(self: stormpy.storage.storage.Variable) → bool ¶: Check if the variable is of bitvector type

has_boolean_type(self: stormpy.storage.storage.Variable) → bool ¶: Check if the variable is of boolean type

has_integer_type(self: stormpy.storage.storage.Variable) → bool ¶: Check if the variable is of integer type

has_numerical_type(self: stormpy.storage.storage.Variable) → bool ¶: Check if the variable is of numerical type

has_rational_type(self: stormpy.storage.storage.Variable) → bool ¶: Check if the variable is of rational type

property name¶: Variable name

collect_information(arg0: stormpy.storage.storage.JaniModel) → stormpy.storage.storage.JaniInformationObject¶

eliminate_reward_accumulations(model: stormpy.storage.storage.JaniModel, properties: List[stormpy.core.Property]) → List[stormpy.core.Property]¶: Eliminate reward accumulations