Stormpy.storage¶

class Bdd_Sylvan¶

Bdd

to_expression(self: stormpy.storage.storage.Bdd_Sylvan, expression_manager: storm::expressions::ExpressionManager) → Tuple[List[storm::expressions::Expression], Dict[int, storm::expressions::Variable]]¶

class BitVector¶

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

load_from_string(description: str) → stormpy.storage.storage.BitVector¶

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¶

store_as_string(self: stormpy.storage.storage.BitVector) → str¶

class ChoiceLabeling¶

Labeling for choices

add_label_to_choice(self: stormpy.storage.storage.ChoiceLabeling, label: str, state: int) → None¶: Adds a label to a given choice

get_choices(self: stormpy.storage.storage.ChoiceLabeling, label: str) → stormpy.storage.storage.BitVector¶: Get all choices which have the given label

get_labels_of_choice(self: stormpy.storage.storage.ChoiceLabeling, choice: int) → Set[str]¶: Get labels of the given choice

set_choices(self: stormpy.storage.storage.ChoiceLabeling, label: str, choices: stormpy.storage.storage.BitVector) → None¶: Add a label to a the given choices

class ChoiceOrigins¶

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

as_jani_choice_origins(self: stormpy.storage.storage.ChoiceOrigins) → storm::storage::sparse::JaniChoiceOrigins¶

as_prism_choice_origins(self: stormpy.storage.storage.ChoiceOrigins) → storm::storage::sparse::PrismChoiceOrigins¶

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

get_number_of_identifiers(self: stormpy.storage.storage.ChoiceOrigins) → int¶: the number of considered identifier

is_jani_choice_origins(self: stormpy.storage.storage.ChoiceOrigins) → bool¶

is_prism_choice_origins(self: stormpy.storage.storage.ChoiceOrigins) → bool¶

class DdManager_Sylvan¶

get_meta_variable(self: stormpy.storage.storage.DdManager_Sylvan, expression_variable: storm::expressions::Variable) → stormpy.storage.storage.DdMetaVariable_Sylvan¶

class DdMetaVariableType¶

Bitvector = DdMetaVariableType.Bitvector¶

Bool = DdMetaVariableType.Bool¶

Int = DdMetaVariableType.Int¶

class DdMetaVariable_Sylvan¶

compute_indices(self: stormpy.storage.storage.DdMetaVariable_Sylvan, sorted: bool = True) → List[int]¶

property lowest_value¶

property name¶

property type¶

class Dd_Sylvan¶

property dd_manager¶: get the manager

property meta_variables¶: the contained meta variables

property node_count¶: get node count

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¶

Divide(arg0: stormpy.storage.storage.Expression, arg1: 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¶

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

simplify(self: stormpy.storage.storage.Expression) → stormpy.storage.storage.Expression¶: Simplify expression

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

get_variable(self: stormpy.storage.storage.ExpressionManager, name: str) → storm::expressions::Variable¶: get variably by name

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 JaniLocationExpander¶

A transformer for Jani expanding variables into locations

get_result(self: stormpy.storage.storage.JaniLocationExpander) → stormpy.storage.storage.JaniModel¶

transform(self: stormpy.storage.storage.JaniLocationExpander, automaton_name: str, variable_name: str) → None¶

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.

flatten_composition(self: stormpy.storage.storage.JaniModel, smt_solver_factory: stormpy.utility.utility.SmtSolverFactory=<stormpy.utility.utility.SmtSolverFactory object at 0x7f626df20e30>) → stormpy.storage.storage.JaniModel¶

get_automaton(self: stormpy.storage.storage.JaniModel, name: str) → storm::jani::Automaton¶

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 JaniScopeChanger¶

A transformer for Jani changing variables from local to global and vice versa

make_variables_local(self: stormpy.storage.storage.JaniScopeChanger, model: stormpy.storage.storage.JaniModel, properties: List[stormpy.core.Property] = []) → stormpy.storage.storage.JaniModel¶

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 ParametricSparseMatrixBuilder¶

Builder of parametric sparse matrix

add_next_value(self: stormpy.storage.storage.ParametricSparseMatrixBuilder, row: int, column: int, value: carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true>) → None¶

Sets the matrix entry at the given row and column to the given value. After all entries have been added, calling function build() is mandatory.

Note: this is a linear setter. That is, it must be called consecutively for each entry, row by row and column by column. As multiple entries per column are admitted, consecutive calls to this method are admitted to mention the same row-column-pair. If rows are skipped entirely, the corresponding rows are treated as empty. If these constraints are not met, an exception is thrown.

Parameters

row (double) – The row in which the matrix entry is to be set
column (double) – The column in which the matrix entry is to be set
value (RationalFunction) – The value that is to be set at the specified row and column

build(self: stormpy.storage.storage.ParametricSparseMatrixBuilder, overridden_row_count: int=0, overridden_column_count: int=0, overridden-row_group_count: int=0) → 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> >¶: Finalize the sparse matrix

get_current_row_group_count(self: stormpy.storage.storage.ParametricSparseMatrixBuilder) → int¶: Get the current row group count

get_last_column(self: stormpy.storage.storage.ParametricSparseMatrixBuilder) → int¶: the most recently used column

get_last_row(self: stormpy.storage.storage.ParametricSparseMatrixBuilder) → int¶: Get the most recently used row

new_row_group(self: stormpy.storage.storage.ParametricSparseMatrixBuilder, starting_row: int) → None¶: Start a new row group in the matrix

replace_columns(self: stormpy.storage.storage.ParametricSparseMatrixBuilder, replacements: List[int], offset: int) → None¶

Replaces all columns with id >= offset according to replacements. Every state with id offset+i is replaced by the id in replacements[i]. Afterwards the columns are sorted.

Parameters

const& replacements (std::vector<double>) – replacements Mapping indicating the replacements from offset+i -> value of i
offset (int) – Offset to add to each id in vector index.

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 PrismChoiceOrigins¶

This class represents for each choice the set of prism commands that induced the choice.

get_command_set(self: stormpy.storage.storage.PrismChoiceOrigins, choice_index: int) → stormpy.core.FlatSet¶: Returns the set of prism commands that induced the choice

property program¶: retrieves the associated Prism program

class PrismCommand¶

A command in a Prism program

property action_index¶: What is the action index of the command

property global_index¶: Get global index

property guard_expression¶: Get guard expression

property labeled¶: Is the command labeled

property updates¶: Updates in the command

class PrismConstant¶

A constant in a Prism program

property defined¶: Is the constant defined?

property definition¶: Defining expression

property expression_variable¶: Expression variable

property name¶: Constant name

property type¶: The type of the constant

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 PrismLabel¶

A label in prism

property expression¶

property name¶

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

get_boolean_variable(self: stormpy.storage.storage.PrismModule, variable_name: str) → storm::prism::BooleanVariable¶

get_command_indices_by_action_index(self: stormpy.storage.storage.PrismModule, action_index: int) → Set[int]¶

get_integer_variable(self: stormpy.storage.storage.PrismModule, variable_name: str) → storm::prism::IntegerVariable¶

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

flatten(self: stormpy.storage.storage.PrismProgram, smt_factory: stormpy.utility.utility.SmtSolverFactory=<stormpy.utility.utility.SmtSolverFactory object at 0x7f626df1a370>) → stormpy.storage.storage.PrismProgram¶: Put program into a single module

get_action_name(self: stormpy.storage.storage.PrismProgram, action_index: int) → str¶: Get the action name for a given action index

get_constant(self: stormpy.storage.storage.PrismProgram, name: str) → storm::prism::Constant¶

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

get_module(self: stormpy.storage.storage.PrismProgram, module_name: str) → storm::prism::Module¶

get_module_indices_by_action_index(self: stormpy.storage.storage.PrismProgram, action_index: int) → Set[int]¶: get all modules that have a particular action index

get_synchronizing_action_indices(self: stormpy.storage.storage.PrismProgram) → Set[int]¶: Get the synchronizing action indices

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 labels¶: Get all labels in the program

property model_type¶: Model type

property modules¶: Modules in the program

property nr_modules¶: Number of modules

property number_of_unlabeled_commands¶: Gets the number of commands that are not labelled

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

property reward_models¶: The defined reward models

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

substitute_formulas(self: stormpy.storage.storage.PrismProgram) → stormpy.storage.storage.PrismProgram¶: Substitute formulas 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 PrismRewardModel¶

Reward declaration in prism

property name¶: get name of the reward model

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 SparseCtmc¶

CTMC in sparse representation

property exit_rates¶

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 exit_rates¶

property markovian_states¶

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 SparseMatrixBuilder¶

Builder of sparse matrix

add_next_value(self: stormpy.storage.storage.SparseMatrixBuilder, row: int, column: int, value: float) → None¶

Sets the matrix entry at the given row and column to the given value. After all entries have been added, calling function build() is mandatory.

Parameters

row (double) – The row in which the matrix entry is to be set
column (double) – The column in which the matrix entry is to be set
value (double) – The value that is to be set at the specified row and column

build(self: stormpy.storage.storage.SparseMatrixBuilder, overridden_row_count: int=0, overridden_column_count: int=0, overridden-row_group_count: int=0) → storm::storage::SparseMatrix<double>¶: Finalize the sparse matrix

get_current_row_group_count(self: stormpy.storage.storage.SparseMatrixBuilder) → int¶: Get the current row group count

get_last_column(self: stormpy.storage.storage.SparseMatrixBuilder) → int¶: the most recently used column

get_last_row(self: stormpy.storage.storage.SparseMatrixBuilder) → int¶: Get the most recently used row

new_row_group(self: stormpy.storage.storage.SparseMatrixBuilder, starting_row: int) → None¶: Start a new row group in the matrix

replace_columns(self: stormpy.storage.storage.SparseMatrixBuilder, replacements: List[int], offset: int) → None¶

Replaces all columns with id >= offset according to replacements. Every state with id offset+i is replaced by the id in replacements[i]. Afterwards the columns are sorted.

Parameters

const& replacements (std::vector<double>) – replacements Mapping indicating the replacements from offset+i -> value of i
offset (int) – Offset to add to each id in vector index.

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

get_choice_index(self: stormpy.storage.storage.SparseMdp, state: int, action_offset: int) → int¶: gets the choice index for the offset action from the given state.

get_nr_available_actions(self: stormpy.storage.storage.SparseMdp, state: int) → int¶

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 SparseModelComponents¶

Components required for building a sparse model

property choice_labeling¶: A list that stores a labeling for each choice

property choice_origins¶: Stores for each choice from which parts of the input model description it originates

property exit_rates¶: The exit rate for each state. Must be given for CTMCs and MAs, if rate_transitions is false. Otherwise, it is optional.

property markovian_states¶: A list that stores which states are Markovian (only for Markov Automata)

property observability_classes¶: The POMDP observations

property player1_matrix¶: Matrix of player 1 choices (needed for stochastic two player games

property rate_transitions¶: True iff the transition values (for Markovian choices) are interpreted as rates

property reward_models¶: Reward models associated with the model

property state_labeling¶: The state labeling

property state_valuations¶: A list that stores for each state to which variable valuation it belongs

property transition_matrix¶: The transition matrix

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 SparseParametricPomdp¶

POMDP in sparse representation

get_observation(self: stormpy.storage.storage.SparseParametricPomdp, state: int) → int¶

property nr_observations¶

property observations¶

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

get_observation(self: stormpy.storage.storage.SparsePomdp, state: int) → int¶

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 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¶: Add a label to the given states

class StateValuation¶

Valuations for explicit states

get_boolean_value(self: stormpy.storage.storage.StateValuation, state: int, variable: storm::expressions::Variable) → bool¶

get_integer_value(self: stormpy.storage.storage.StateValuation, state: int, variable: storm::expressions::Variable) → int¶

get_json(self: stormpy.storage.storage.StateValuation, state: int, selected_variables: Optional[Set[storm::expressions::Variable]]=None) → str¶

get_nr_of_states(self: stormpy.storage.storage.StateValuation) → int¶

get_rational_value(self: stormpy.storage.storage.StateValuation, state: int, variable: storm::expressions::Variable) → __gmp_expr<__mpq_struct [1], __mpq_struct [1]>¶

get_string(self: stormpy.storage.storage.StateValuation, state: int, pretty: bool=True, selected_variables: Optional[Set[storm::expressions::Variable]]=None) → str¶

class StateValuationsBuilder¶

add_state(self: stormpy.storage.storage.StateValuationsBuilder, state: int, boolean_values: List[bool]=[], integer_values: List[int]=[], rational_values: List[__gmp_expr<__mpq_struct [1], __mpq_struct [1]>]=[]) → None¶: Adds a new state, no more variables should be added afterwards

add_variable(self: stormpy.storage.storage.StateValuationsBuilder, variable: storm::expressions::Variable) → None¶: Adds a new variable

build(self: stormpy.storage.storage.StateValuationsBuilder, arg0: int) → stormpy.storage.storage.StateValuation¶: Creates the finalized state valuations object

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

build_parametric_sparse_matrix(array, row_group_indices=[])¶

Build a sparse matrix from numpy array.

Parameters

array (numpy) – The array.
row_group_indices (List[double]) – List containing the starting row of each row group in ascending order.

Returns

Parametric sparse matrix.

build_sparse_matrix(array, row_group_indices=[])¶

Build a sparse matrix from numpy array.

Parameters

array (numpy) – The array.
row_group_indices (List[double]) – List containing the starting row of each row group in ascending order.

Returns

Sparse matrix.

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