Stormpy.storage

class AddIterator_Sylvan_Double

AddIterator

get(self: stormpy.storage.storage.AddIterator_Sylvan_Double) Tuple[storm::expressions::SimpleValuation, float]
class Add_Sylvan_Double

Add

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
as_int(self: stormpy.storage.storage.BitVector, index: int, no_bits: int) int

Get as unsigned int

get(self: stormpy.storage.storage.BitVector, index: int) bool
static 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

Members:

Int

Bool

Bitvector

Bitvector = <DdMetaVariableType.Bitvector: 2>
Bool = <DdMetaVariableType.Bool: 0>
Int = <DdMetaVariableType.Int: 1>
property name
property value
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

Dd

property dd_manager

get the manager

property meta_variables

the contained meta variables

property node_count

get node count

class DiceStringVisitor

Translate expressions to dice

to_string(self: stormpy.storage.storage.DiceStringVisitor, arg0: stormpy.storage.storage.Expression) str
class Distribution

Finite Support Distribution

class DistributionExact

Finite Support Distribution

class DistributionInterval

Finite Support Distribution

class ExactSparseMatrix

Sparse matrix

get_row(self: stormpy.storage.storage.ExactSparseMatrix, row: int) storm::storage::SparseMatrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >::rows

Get row

get_row_group_end(self: stormpy.storage.storage.ExactSparseMatrix, arg0: int) int
get_row_group_start(self: stormpy.storage.storage.ExactSparseMatrix, arg0: int) int
get_rows_for_group(self: stormpy.storage.storage.ExactSparseMatrix, row_group: int) List[int]

Get rows within a row group

property has_trivial_row_grouping

Trivial row grouping

make_row_grouping_trivial(self: stormpy.storage.storage.ExactSparseMatrix) None

Makes row groups trivial. Use with care.

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.ExactSparseMatrix, row: int) str

Print rows from start to end

row_iter(self: stormpy.storage.storage.ExactSparseMatrix, row_start: int, row_end: int) Iterator

Get iterator from start to end

submatrix(self: stormpy.storage.storage.ExactSparseMatrix, row_constraint: stormpy.storage.storage.BitVector, column_constraint: stormpy.storage.storage.BitVector, insert_diagonal_entries: bool = False) stormpy.storage.storage.ExactSparseMatrix

Get submatrix

class ExactSparseMatrixBuilder

Builder of sparse matrix

add_next_value(self: stormpy.storage.storage.ExactSparseMatrixBuilder, row: int, column: int, value: pycarl.gmp.gmp.Rational) 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 (double) – The value that is to be set at the specified row and column

build(self: stormpy.storage.storage.ExactSparseMatrixBuilder, overridden_row_count: int = 0, overridden_column_count: int = 0, overridden-row_group_count: int = 0) storm::storage::SparseMatrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >

Finalize the sparse matrix

get_current_row_group_count(self: stormpy.storage.storage.ExactSparseMatrixBuilder) int

Get the current row group count

get_last_column(self: stormpy.storage.storage.ExactSparseMatrixBuilder) int

the most recently used column

get_last_row(self: stormpy.storage.storage.ExactSparseMatrixBuilder) int

Get the most recently used row

new_row_group(self: stormpy.storage.storage.ExactSparseMatrixBuilder, starting_row: int) None

Start a new row group in the matrix

replace_columns(self: stormpy.storage.storage.ExactSparseMatrixBuilder, 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:
  • replacements (std::vector<double> const&) – replacements Mapping indicating the replacements from offset+i -> value of i

  • offset (int) – Offset to add to each id in vector index.

class ExactSparseMatrixEntry

Entry of sparse matrix

property column

Column

set_value(self: stormpy.storage.storage.ExactSparseMatrixEntry, value: pycarl.gmp.gmp.Rational) None

Set value

value(self: stormpy.storage.storage.ExactSparseMatrixEntry) pycarl.gmp.gmp.Rational

Value

class ExactSparseMatrixRows

Set of rows in a sparse matrix

class Expression

Holds an expression

static And(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression
static Conjunction(arg0: List[stormpy.storage.storage.Expression]) stormpy.storage.storage.Expression
static Disjunction(arg0: List[stormpy.storage.storage.Expression]) stormpy.storage.storage.Expression
static Divide(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression
static Eq(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression
static Geq(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression
static Greater(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression
static Iff(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression
static Implies(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression
static Leq(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression
static Less(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression
static Minus(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression
static Modulo(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression
static Multiply(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression
static Neq(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression
static Or(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression
static 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) pycarl.gmp.gmp.Rational

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: pycarl.gmp.gmp.Rational) 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

get_variables(self: stormpy.storage.storage.ExpressionManager) Set[storm::expressions::Variable]

Retrieves the set of all variables known to this manager.

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 IntervalSparseMatrix

Sparse matrix

get_row(self: stormpy.storage.storage.IntervalSparseMatrix, row: int) storm::storage::SparseMatrix<carl::Interval<double> >::rows

Get row

get_row_group_end(self: stormpy.storage.storage.IntervalSparseMatrix, arg0: int) int
get_row_group_start(self: stormpy.storage.storage.IntervalSparseMatrix, arg0: int) int
get_rows_for_group(self: stormpy.storage.storage.IntervalSparseMatrix, row_group: int) List[int]

Get rows within a row group

property has_trivial_row_grouping

Trivial row grouping

make_row_grouping_trivial(self: stormpy.storage.storage.IntervalSparseMatrix) None

Makes row groups trivial. Use with care.

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.IntervalSparseMatrix, row: int) str

Print rows from start to end

row_iter(self: stormpy.storage.storage.IntervalSparseMatrix, row_start: int, row_end: int) Iterator

Get iterator from start to end

submatrix(self: stormpy.storage.storage.IntervalSparseMatrix, row_constraint: stormpy.storage.storage.BitVector, column_constraint: stormpy.storage.storage.BitVector, insert_diagonal_entries: bool = False) stormpy.storage.storage.IntervalSparseMatrix

Get submatrix

class IntervalSparseMatrixBuilder

Builder of sparse matrix

add_next_value(self: stormpy.storage.storage.IntervalSparseMatrixBuilder, row: int, column: int, value: pycarl.core.Interval) 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 (double) – The value that is to be set at the specified row and column

build(self: stormpy.storage.storage.IntervalSparseMatrixBuilder, overridden_row_count: int = 0, overridden_column_count: int = 0, overridden-row_group_count: int = 0) storm::storage::SparseMatrix<carl::Interval<double> >

Finalize the sparse matrix

get_current_row_group_count(self: stormpy.storage.storage.IntervalSparseMatrixBuilder) int

Get the current row group count

get_last_column(self: stormpy.storage.storage.IntervalSparseMatrixBuilder) int

the most recently used column

get_last_row(self: stormpy.storage.storage.IntervalSparseMatrixBuilder) int

Get the most recently used row

new_row_group(self: stormpy.storage.storage.IntervalSparseMatrixBuilder, starting_row: int) None

Start a new row group in the matrix

replace_columns(self: stormpy.storage.storage.IntervalSparseMatrixBuilder, 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:
  • replacements (std::vector<double> const&) – replacements Mapping indicating the replacements from offset+i -> value of i

  • offset (int) – Offset to add to each id in vector index.

class IntervalSparseMatrixEntry

Entry of sparse matrix

property column

Column

set_value(self: stormpy.storage.storage.IntervalSparseMatrixEntry, value: pycarl.core.Interval) None

Set value

value(self: stormpy.storage.storage.IntervalSparseMatrixEntry) pycarl.core.Interval

Value

class IntervalSparseMatrixRows

Set of rows in a sparse matrix

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

variable that is assigned to, if any

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

get_location_index(self: stormpy.storage.storage.JaniAutomaton, name: str) int
property initial_location_indices
property initial_states_restriction

initial state restriction

property location_variable
property locations
property name
property variables
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], substitute_transcendental_numbers: bool) 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

transform(self: stormpy.storage.storage.JaniLocationExpander, automaton_name: str, variable_name: str) storm::jani::JaniLocationExpander::ReturnType
class JaniModel

A Jani Model

add_automaton(self: stormpy.storage.storage.JaniModel, automaton: storm::jani::Automaton) int

add an automaton (with a unique name)

add_constant(self: stormpy.storage.storage.JaniModel, constant: storm::jani::Constant) None

adds constant to model

property automata

get automata

check_valid(self: stormpy.storage.storage.JaniModel) None

Some basic checks to ensure validity

property constants

get constants

static 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

static 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 0x7f327f773370>) 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], substitute_transcendental_numbers: bool) 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 init_expression
property name

name of constant

class JaniVariableSet

Jani Set of Variables

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?

erase_variable(self: stormpy.storage.storage.JaniVariableSet, arg0: storm::expressions::Variable) storm::jani::Variable

variable

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 MaximalEndComponent

Maximal end component

property size

Number of states in MEC

class MaximalEndComponentDecomposition_double

Decomposition of maximal end components

property size

Number of MECs in the decomposition

class MaximalEndComponentDecomposition_exact

Decomposition of maximal end components

property size

Number of MECs in the decomposition

class MaximalEndComponentDecomposition_interval

Decomposition of maximal end components

property size

Number of MECs in the decomposition

class MaximalEndComponentDecomposition_ratfunc

Decomposition of maximal end components

property size

Number of MECs in the decomposition

class ModelType

Type of the model

Members:

DTMC

MDP

POMDP

CTMC

MA

SMG

CTMC = <ModelType.CTMC: 1>
DTMC = <ModelType.DTMC: 0>
MA = <ModelType.MA: 3>
MDP = <ModelType.MDP: 2>
POMDP = <ModelType.POMDP: 5>
SMG = <ModelType.SMG: 6>
property name
property value
class OperatorType

Type of an operator (of any sort)

Members:

And

Or

Xor

Implies

Iff

Plus

Minus

Times

Divide

Min

Max

Power

Modulo

Equal

NotEqual

Less

LessOrEqual

Greater

GreaterOrEqual

Not

Floor

Ceil

Ite

And = <OperatorType.And: 0>
Ceil = <OperatorType.Ceil: 24>
Divide = <OperatorType.Divide: 8>
Equal = <OperatorType.Equal: 16>
Floor = <OperatorType.Floor: 23>
Greater = <OperatorType.Greater: 20>
GreaterOrEqual = <OperatorType.GreaterOrEqual: 21>
Iff = <OperatorType.Iff: 4>
Implies = <OperatorType.Implies: 3>
Ite = <OperatorType.Ite: 25>
Less = <OperatorType.Less: 18>
LessOrEqual = <OperatorType.LessOrEqual: 19>
Max = <OperatorType.Max: 10>
Min = <OperatorType.Min: 9>
Minus = <OperatorType.Minus: 6>
Modulo = <OperatorType.Modulo: 12>
Not = <OperatorType.Not: 22>
NotEqual = <OperatorType.NotEqual: 17>
Or = <OperatorType.Or: 1>
Plus = <OperatorType.Plus: 5>
Power = <OperatorType.Power: 11>
Times = <OperatorType.Times: 7>
Xor = <OperatorType.Xor: 2>
property name
property value
class OverlappingGuardAnalyser

An SMT driven analysis for overlapping guards

has_module_with_inner_action_overlapping_guard(self: stormpy.storage.storage.OverlappingGuardAnalyser) bool
class ParametricSparseMatrix

Sparse matrix

get_row(self: stormpy.storage.storage.ParametricSparseMatrix, row: int) storm::storage::SparseMatrix<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, 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_for_group(self: stormpy.storage.storage.ParametricSparseMatrix, row_group: int) List[int]

Get rows within a row group

property has_trivial_row_grouping

Trivial row grouping

make_row_grouping_trivial(self: stormpy.storage.storage.ParametricSparseMatrix) None

Makes row groups trivial. Use with care.

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 rows from start to end

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

add_next_value(self: stormpy.storage.storage.ParametricSparseMatrixBuilder, row: int, column: int, value: pycarl.cln.cln.FactorizedRationalFunction) 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 (double) – 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::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, 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:
  • replacements (std::vector<double> const&) – 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 sparse matrix

property column

Column

set_value(self: stormpy.storage.storage.ParametricSparseMatrixEntry, value: pycarl.cln.cln.FactorizedRationalFunction) None

Set value

value(self: stormpy.storage.storage.ParametricSparseMatrixEntry) pycarl.cln.cln.FactorizedRationalFunction

Value

class ParametricSparseMatrixRows

Set of rows in a sparse matrix

class PolytopeDouble
create_downward_closure(self: stormpy.storage.storage.PolytopeDouble) stormpy.storage.storage.PolytopeDouble
get_vertices_clockwise(self: stormpy.storage.storage.PolytopeDouble) List[List[float]]
property vertices
class PolytopeExact
create_downward_closure(self: stormpy.storage.storage.PolytopeExact) stormpy.storage.storage.PolytopeExact
get_vertices_clockwise(self: stormpy.storage.storage.PolytopeExact) List[List[pycarl.gmp.gmp.Rational]]
property vertices
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 action_name

Retrieves the action name of this command

property global_index

Get global index

property guard_expression

Get guard expression

property is_labeled

Retrieves whether the command possesses a synchronization label

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

Members:

DTMC

CTMC

MDP

CTMDP

MA

POMDP

UNDEFINED

CTMC = <PrismModelType.CTMC: 2>
CTMDP = <PrismModelType.CTMDP: 4>
DTMC = <PrismModelType.DTMC: 1>
MA = <PrismModelType.MA: 5>
MDP = <PrismModelType.MDP: 3>
POMDP = <PrismModelType.POMDP: 6>
UNDEFINED = <PrismModelType.UNDEFINED: 0>
property name
property value
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 0x7f327f74d6f0>) 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

Requires that the program has a constant with this name

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

get_undefined_constants(self: stormpy.storage.storage.PrismProgram) List[storm::prism::Constant]

Collect the undefined constants

property global_boolean_variables

Retrieves the global boolean variables of the program

property global_integer_variables

Retrieves the global integer variables of the program

has_constant(self: stormpy.storage.storage.PrismProgram, name: str) bool
property has_initial_states_expression

Is an initial states expression given.

has_label(self: stormpy.storage.storage.PrismProgram, name: str) bool
has_reward_model(self: stormpy.storage.storage.PrismProgram, name: str) bool

Is a reward model with the specified name defined?

property has_undefined_constants

Flag if program has undefined constants

property initial_states_expression

Get the initial states expression, or none, if none exists

property is_deterministic_model

Does the program describe a deterministic model?

label_unlabelled_commands(self: stormpy.storage.storage.PrismProgram, name_suggestions: Dict[int, str]) stormpy.storage.storage.PrismProgram

Label unlabelled commands

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

replace_constant_by_variable(self: stormpy.storage.storage.PrismProgram, constant: storm::prism::Constant, lower_bound: storm::expressions::Expression, upper_bound: storm::expressions::Expression, observable: bool = True) stormpy.storage.storage.PrismProgram

Operation to take a constant and make it into a global variable (ranging from lower to upper bound).

replace_variable_initialization_by_init_expression(self: stormpy.storage.storage.PrismProgram) stormpy.storage.storage.PrismProgram

Replaces initializations from the individual variables to a init expression.

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

substitute_nonstandard_predicates(self: stormpy.storage.storage.PrismProgram) stormpy.storage.storage.PrismProgram

Remove nonstandard predicates from the prism 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

update_initial_states_expression(self: stormpy.storage.storage.PrismProgram, new_expression: storm::expressions::Expression) None

Replace initial expression. Can only be called if initial expression exists.

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

get_as_variable_to_expression_map(self: stormpy.storage.storage.PrismUpdate) Dict[storm::expressions::Variable, storm::expressions::Expression]

Creates a mapping representation of this update

get_assignment(self: stormpy.storage.storage.PrismUpdate, variable_name: str) storm::prism::Assignment

Retrieves a reference to the assignment for the variable with the given name

property global_index

Retrieves the global index of the update, that is, a unique index over all modules

property probability_expression

The probability expression for this update

simplify(self: stormpy.storage.storage.PrismUpdate) stormpy.storage.storage.PrismUpdate

Simplifies the update in various ways (also removes identity assignments)

substitute(self: stormpy.storage.storage.PrismUpdate, arg0: Dict[storm::expressions::Variable, storm::expressions::Expression]) stormpy.storage.storage.PrismUpdate

Substitutes all identifiers in the update according to the given map

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 Scheduler

A Finite Memory Scheduler

cast_to_double_datatype(self: stormpy.storage.storage.Scheduler) stormpy.storage.storage.Scheduler

Construct the scheduler with double value type

cast_to_exact_datatype(self: stormpy.storage.storage.Scheduler) storm::storage::Scheduler<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >

Construct the scheduler with exact value type

cast_to_interval_datatype(self: stormpy.storage.storage.Scheduler) storm::storage::Scheduler<carl::Interval<double> >

Construct the scheduler with interval value type

cast_to_parametric_datatype(self: stormpy.storage.storage.Scheduler) storm::storage::Scheduler<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, true> >

Construct the scheduler with parametric value type

compute_action_support(self: stormpy.storage.storage.Scheduler, nondeterministic_choice_indices: List[int]) stormpy.storage.storage.BitVector
property deterministic

Is the scheduler deterministic?

get_choice(self: stormpy.storage.storage.Scheduler, 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?

set_choice(self: stormpy.storage.storage.Scheduler, choice: storm::storage::SchedulerChoice<double>, state: int, memory_index: int = 0) None
to_json_str(self: stormpy.storage.storage.Scheduler, model: stormpy.storage.storage._SparseModel, skip_unique_choices: bool = False, skip_dont_care_states: bool = False) str
class SchedulerChoice

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.SchedulerChoice) storm::storage::Distribution<double, unsigned long>

Get the distribution over the actions

get_deterministic_choice(self: stormpy.storage.storage.SchedulerChoice) int

Get the deterministic choice

class SchedulerChoiceExact

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.SchedulerChoiceExact) storm::storage::Distribution<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, unsigned long>

Get the distribution over the actions

get_deterministic_choice(self: stormpy.storage.storage.SchedulerChoiceExact) int

Get the deterministic choice

class SchedulerChoiceInterval

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.SchedulerChoiceInterval) storm::storage::Distribution<carl::Interval<double>, unsigned long>

Get the distribution over the actions

get_deterministic_choice(self: stormpy.storage.storage.SchedulerChoiceInterval) int

Get the deterministic choice

class SchedulerChoiceParametric

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.SchedulerChoiceParametric) storm::storage::Distribution<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, true>, unsigned long>

Get the distribution over the actions

get_deterministic_choice(self: stormpy.storage.storage.SchedulerChoiceParametric) int

Get the deterministic choice

class SchedulerExact

A Finite Memory Scheduler

cast_to_double_datatype(self: stormpy.storage.storage.SchedulerExact) stormpy.storage.storage.Scheduler

Construct the scheduler with double value type

cast_to_exact_datatype(self: stormpy.storage.storage.SchedulerExact) stormpy.storage.storage.SchedulerExact

Construct the scheduler with exact value type

cast_to_interval_datatype(self: stormpy.storage.storage.SchedulerExact) storm::storage::Scheduler<carl::Interval<double> >

Construct the scheduler with interval value type

cast_to_parametric_datatype(self: stormpy.storage.storage.SchedulerExact) storm::storage::Scheduler<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, true> >

Construct the scheduler with parametric value type

compute_action_support(self: stormpy.storage.storage.SchedulerExact, nondeterministic_choice_indices: List[int]) stormpy.storage.storage.BitVector
property deterministic

Is the scheduler deterministic?

get_choice(self: stormpy.storage.storage.SchedulerExact, state_index: int, memory_index: int = 0) storm::storage::SchedulerChoice<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >
property memory_size

How much memory does the scheduler take?

property memoryless

Is the scheduler memoryless?

property partial

Is the scheduler partial?

set_choice(self: stormpy.storage.storage.SchedulerExact, choice: storm::storage::SchedulerChoice<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >, state: int, memory_index: int = 0) None
to_json_str(self: stormpy.storage.storage.SchedulerExact, model: stormpy.storage.storage._SparseExactModel, skip_unique_choices: bool = False, skip_dont_care_states: bool = False) str
class SchedulerInterval

A Finite Memory Scheduler

compute_action_support(self: stormpy.storage.storage.SchedulerInterval, nondeterministic_choice_indices: List[int]) stormpy.storage.storage.BitVector
property deterministic

Is the scheduler deterministic?

get_choice(self: stormpy.storage.storage.SchedulerInterval, state_index: int, memory_index: int = 0) storm::storage::SchedulerChoice<carl::Interval<double> >
property memory_size

How much memory does the scheduler take?

property memoryless

Is the scheduler memoryless?

property partial

Is the scheduler partial?

set_choice(self: stormpy.storage.storage.SchedulerInterval, choice: storm::storage::SchedulerChoice<carl::Interval<double> >, state: int, memory_index: int = 0) None
to_json_str(self: stormpy.storage.storage.SchedulerInterval, model: stormpy.storage.storage._SparseIntervalModel, skip_unique_choices: bool = False, skip_dont_care_states: bool = False) str
class SchedulerParametric

A Finite Memory Scheduler

cast_to_double_datatype(self: stormpy.storage.storage.SchedulerParametric) stormpy.storage.storage.Scheduler

Construct the scheduler with double value type

cast_to_exact_datatype(self: stormpy.storage.storage.SchedulerParametric) stormpy.storage.storage.SchedulerExact

Construct the scheduler with exact value type

cast_to_parametric_datatype(self: stormpy.storage.storage.SchedulerParametric) stormpy.storage.storage.SchedulerParametric

Construct the scheduler with parametric value type

compute_action_support(self: stormpy.storage.storage.SchedulerParametric, nondeterministic_choice_indices: List[int]) stormpy.storage.storage.BitVector
property deterministic

Is the scheduler deterministic?

get_choice(self: stormpy.storage.storage.SchedulerParametric, state_index: int, memory_index: int = 0) storm::storage::SchedulerChoice<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, true> >
property memory_size

How much memory does the scheduler take?

property memoryless

Is the scheduler memoryless?

property partial

Is the scheduler partial?

set_choice(self: stormpy.storage.storage.SchedulerParametric, choice: storm::storage::SchedulerChoice<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, true> >, state: int, memory_index: int = 0) None
to_json_str(self: stormpy.storage.storage.SchedulerParametric, model: stormpy.storage.storage._SparseParametricModel, skip_unique_choices: bool = False, skip_dont_care_states: bool = False) str
class SimpleValuation
get_boolean_value(self: stormpy.storage.storage.SimpleValuation, variable: storm::expressions::Variable) bool

Get Boolean Value for expression variable

get_integer_value(self: stormpy.storage.storage.SimpleValuation, variable: storm::expressions::Variable) int

Get Integer Value for expression variable

to_json(self: stormpy.storage.storage.SimpleValuation) stormpy.utility.utility.JsonContainerRational

Convert to JSON

to_string(self: stormpy.storage.storage.SimpleValuation, pretty: bool = True) str

to string

class SparseCtmc

CTMC in sparse representation

property exit_rates
class SparseDtmc

DTMC in sparse representation

class SparseExactCtmc

CTMC in sparse representation

property exit_rates
class SparseExactDtmc

DTMC in sparse representation

class SparseExactMA

MA in sparse representation

apply_scheduler(self: stormpy.storage.storage.SparseExactMA, scheduler: storm::storage::Scheduler<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >, drop_unreachable_states: bool = True) stormpy.storage.storage._SparseExactModel

apply scheduler

convert_to_ctmc(self: stormpy.storage.storage.SparseExactMA) stormpy.storage.storage.SparseExactCtmc

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 SparseExactMdp

MDP in sparse representation

apply_scheduler(self: stormpy.storage.storage.SparseExactMdp, scheduler: storm::storage::Scheduler<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >, drop_unreachable_states: bool = True) stormpy.storage.storage._SparseExactModel

apply scheduler

get_choice_index(self: stormpy.storage.storage.SparseExactMdp, 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.SparseExactMdp, state: int) int
property nondeterministic_choice_indices
class SparseExactModelAction

Action for state in sparse model

property id

Id

property labels

Get choice labels

property origins

Get choice origins

property transitions

Get transitions

class SparseExactModelActions

Actions for state in sparse model

class SparseExactModelComponents

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_player_indications

The vector mapping states to player indices

property state_valuations

A list that stores for each state to which variable valuation it belongs

property transition_matrix

The transition matrix

class SparseExactModelState

State in sparse model

property actions

Get actions

property id

Id

property labels

Get state labels

property valuations

Get state valuations

class SparseExactModelStates

States in sparse model

class SparseExactPomdp

POMDP in sparse representation

get_observation(self: stormpy.storage.storage.SparseExactPomdp, state: int) int
has_observation_valuations(self: stormpy.storage.storage.SparseExactPomdp) bool
property nr_observations
property observation_valuations
property observations
class SparseExactRewardModel

Reward structure for sparse models

get_state_action_reward(self: stormpy.storage.storage.SparseExactRewardModel, arg0: int) pycarl.gmp.gmp.Rational
get_state_reward(self: stormpy.storage.storage.SparseExactRewardModel, arg0: int) pycarl.gmp.gmp.Rational
get_zero_reward_states(self: stormpy.storage.storage.SparseExactRewardModel, transition_matrix: storm::storage::SparseMatrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >) 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.SparseExactRewardModel, transition_matrix: storm::storage::SparseMatrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >, only_state_rewards: bool) None

Reduce to state-based rewards

set_state_reward(self: stormpy.storage.storage.SparseExactRewardModel, arg0: int, arg1: pycarl.gmp.gmp.Rational) None
property state_action_rewards
property state_rewards
property transition_rewards
class SparseExactSmg

SMG in sparse representation

get_player_of_state(self: stormpy.storage.storage.SparseExactSmg, state: int) int

Get player for the given state

get_state_player_indications(self: stormpy.storage.storage.SparseExactSmg) List[int]

Get for each state its corresponding player

class SparseIntervalCtmc

CTMC in sparse representation

property exit_rates
class SparseIntervalDtmc

DTMC in sparse representation

class SparseIntervalMA

MA in sparse representation

apply_scheduler(self: stormpy.storage.storage.SparseIntervalMA, scheduler: storm::storage::Scheduler<carl::Interval<double> >, drop_unreachable_states: bool = True) stormpy.storage.storage._SparseIntervalModel

apply scheduler

convert_to_ctmc(self: stormpy.storage.storage.SparseIntervalMA) stormpy.storage.storage.SparseIntervalCtmc

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 SparseIntervalMdp

MDP in sparse representation

apply_scheduler(self: stormpy.storage.storage.SparseIntervalMdp, scheduler: storm::storage::Scheduler<carl::Interval<double> >, drop_unreachable_states: bool = True) stormpy.storage.storage._SparseIntervalModel

apply scheduler

get_choice_index(self: stormpy.storage.storage.SparseIntervalMdp, 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.SparseIntervalMdp, state: int) int
property nondeterministic_choice_indices
class SparseIntervalModelAction

Action for state in sparse model

property id

Id

property labels

Get choice labels

property origins

Get choice origins

property transitions

Get transitions

class SparseIntervalModelActions

Actions for state in sparse model

class SparseIntervalModelComponents

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_player_indications

The vector mapping states to player indices

property state_valuations

A list that stores for each state to which variable valuation it belongs

property transition_matrix

The transition matrix

class SparseIntervalModelState

State in sparse model

property actions

Get actions

property id

Id

property labels

Get state labels

property valuations

Get state valuations

class SparseIntervalModelStates

States in sparse model

class SparseIntervalPomdp

POMDP in sparse representation

get_observation(self: stormpy.storage.storage.SparseIntervalPomdp, state: int) int
has_observation_valuations(self: stormpy.storage.storage.SparseIntervalPomdp) bool
property nr_observations
property observation_valuations
property observations
class SparseIntervalRewardModel

Reward structure for sparse models

get_state_action_reward(self: stormpy.storage.storage.SparseIntervalRewardModel, arg0: int) pycarl.core.Interval
get_state_reward(self: stormpy.storage.storage.SparseIntervalRewardModel, arg0: int) pycarl.core.Interval
get_zero_reward_states(self: stormpy.storage.storage.SparseIntervalRewardModel, transition_matrix: storm::storage::SparseMatrix<carl::Interval<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.SparseIntervalRewardModel, transition_matrix: storm::storage::SparseMatrix<carl::Interval<double> >, only_state_rewards: bool) None

Reduce to state-based rewards

set_state_reward(self: stormpy.storage.storage.SparseIntervalRewardModel, arg0: int, arg1: pycarl.core.Interval) None
property state_action_rewards
property state_rewards
property transition_rewards
class SparseIntervalSmg

SMG in sparse representation

get_player_of_state(self: stormpy.storage.storage.SparseIntervalSmg, state: int) int

Get player for the given state

get_state_player_indications(self: stormpy.storage.storage.SparseIntervalSmg) List[int]

Get for each state its corresponding player

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_for_group(self: stormpy.storage.storage.SparseMatrix, row_group: int) List[int]

Get rows within a row group

property has_trivial_row_grouping

Trivial row grouping

make_row_grouping_trivial(self: stormpy.storage.storage.SparseMatrix) None

Makes row groups trivial. Use with care.

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.

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 (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:
  • replacements (std::vector<double> const&) – 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 labels

Get choice labels

property origins

Get choice origins

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_player_indications

The vector mapping states to player indices

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

Get state labels

property valuations

Get state valuations

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::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, 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::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, true> >, drop_unreachable_states: bool = True) stormpy.storage.storage._SparseParametricModel

apply scheduler

get_nr_available_actions(self: stormpy.storage.storage.SparseParametricMdp, state: int) int
property nondeterministic_choice_indices
class SparseParametricModelAction

Action for state in sparse model

property id

Id

property labels

Get choice labels

property origins

Get choice origins

property transitions

Get transitions

class SparseParametricModelActions

Actions for state in sparse model

class SparseParametricModelComponents

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_player_indications

The vector mapping states to player indices

property state_valuations

A list that stores for each state to which variable valuation it belongs

property transition_matrix

The transition matrix

class SparseParametricModelState

State in sparse model

property actions

Get actions

property id

Id

property labels

Get state labels

property valuations

Get state valuations

class SparseParametricModelStates

States in sparse 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) pycarl.cln.cln.FactorizedRationalFunction
get_state_reward(self: stormpy.storage.storage.SparseParametricRewardModel, arg0: int) pycarl.cln.cln.FactorizedRationalFunction
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::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, 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
has_observation_valuations(self: stormpy.storage.storage.SparsePomdp) bool
property nr_observations
property observation_valuations
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

set_state_reward(self: stormpy.storage.storage.SparseRewardModel, arg0: int, arg1: float) None
property state_action_rewards
property state_rewards
property transition_rewards
class SparseSmg

SMG in sparse representation

get_player_of_state(self: stormpy.storage.storage.SparseSmg, state: int) int

Get player for the given state

get_state_player_indications(self: stormpy.storage.storage.SparseSmg) List[int]

Get for each state its corresponding player

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) stormpy.utility.utility.JsonContainerRational
get_nr_of_states(self: stormpy.storage.storage.StateValuation) int