Stormpy.core

class ActionMaskDouble

class AddIterator_Sylvan_Double

AddIterator

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

class Add_Sylvan_Double

Add

class AtomicExpressionFormula

Formula with an atomic expression

get_expression(self: stormpy.logic.logic.AtomicExpressionFormula) → stormpy.storage.storage.Expression

class AtomicLabelFormula

Formula with an atomic label

property label

label in the formula

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 BinaryBooleanOperatorType

Members:

AND

OR

AND = <BinaryBooleanOperatorType.AND: 0>

OR = <BinaryBooleanOperatorType.OR: 1>

property name

property value

class BinaryPathFormula

Path formula with two operands

property left_subformula

property right_subformula

class BinaryStateFormula

State formula with two operands

class BisimulationType

Types of bisimulation

Members:

STRONG

WEAK

STRONG = <BisimulationType.STRONG: 0>

WEAK = <BisimulationType.WEAK: 1>

property name

property value

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 BooleanBinaryStateFormula

Boolean binary state formula

class BooleanLiteralFormula

Formula with a boolean literal

class BoundedUntilFormula

Until Formula with either a step or a time bound.

property has_lower_bound

property is_multidimensional

Is the bound multi-dimensional

property left_subformula

property right_subformula

property upper_bound_expression

class BuilderOptions

Options for building process

property preserved_label_names

Labels preserved

set_add_out_of_bounds_state(self: stormpy.core.BuilderOptions, new_value: bool = True) → stormpy.core.BuilderOptions

Build with out of bounds state

set_add_overlapping_guards_label(self: stormpy.core.BuilderOptions, new_value: bool = True) → stormpy.core.BuilderOptions

Build with overlapping guards state labeled

set_build_all_labels(self: stormpy.core.BuilderOptions, new_value: bool = True) → stormpy.core.BuilderOptions

Build with all state labels

set_build_all_reward_models(self: stormpy.core.BuilderOptions, new_value: bool = True) → stormpy.core.BuilderOptions

Build with all reward models

set_build_choice_labels(self: stormpy.core.BuilderOptions, new_value: bool = True) → stormpy.core.BuilderOptions

Build with choice labels

set_build_observation_valuations(self: stormpy.core.BuilderOptions, new_value: bool = True) → stormpy.core.BuilderOptions

Build observation valuations

set_build_state_valuations(self: stormpy.core.BuilderOptions, new_value: bool = True) → stormpy.core.BuilderOptions

Build state valuations

set_build_with_choice_origins(self: stormpy.core.BuilderOptions, new_value: bool = True) → stormpy.core.BuilderOptions

Build choice origins

set_exploration_checks(self: stormpy.core.BuilderOptions, new_value: bool = True) → stormpy.core.BuilderOptions

Perform extra checks during exploration

class CheckTask

Task for model checking

set_hint(self: stormpy.core.CheckTask, arg0: storm::modelchecker::ModelCheckerHint) → None

Sets a hint that may speed up the solver

set_produce_schedulers(self: stormpy.core.CheckTask, produce_schedulers: bool = True) → None

Set whether schedulers should be produced (if possible)

set_robust_uncertainty(self: stormpy.core.CheckTask, arg0: bool) → None

Sets whether robust uncertainty should be considered

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 ComparisonType

Members:

LESS

LEQ

GREATER

GEQ

GEQ = <ComparisonType.GEQ: 3>

GREATER = <ComparisonType.GREATER: 2>

LEQ = <ComparisonType.LEQ: 1>

LESS = <ComparisonType.LESS: 0>

property name

property value

class ConditionalFormula

Formula with the right hand side being a condition.

class ConstraintCollector

Collector for constraints on parametric Markov chains

property graph_preserving_constraints

Get the constraints ensuring the graph is preserved

property wellformed_constraints

Get the constraints ensuring a wellformed model

class CumulativeRewardFormula

Summed rewards over a the paths

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 DirectEncodingOptions

property allow_placeholders

class DirectEncodingParserOptions

Options for the .drn parser

property build_choice_labels

Build with choice labels

class Distribution

Finite Support Distribution

class DistributionExact

Finite Support Distribution

class DistributionInterval

Finite Support Distribution

class EliminationLabelBehavior

Behavior of labels while eliminating non-Markovian chains

Members:

KEEP_LABELS

MERGE_LABELS

DELETE_LABELS

DELETE_LABELS = <EliminationLabelBehavior.DELETE_LABELS: 3>

KEEP_LABELS = <EliminationLabelBehavior.KEEP_LABELS: 0>

MERGE_LABELS = <EliminationLabelBehavior.MERGE_LABELS: 2>

property name

property value

class EndComponentEliminatorReturnTypeDouble

Container for result of endcomponent elimination

property matrix

The resulting matrix

property new_to_old_row_mapping

Index mapping that gives for each row fo the new matrix the corresponding row in the original matrix

property old_to_new_state_mapping

For each state of the original matrix (and subsystem) the corresponding state in the result. Removed states are mapped to the EC.

property sink_rows

Rows that indicate staying in the EC forever

class Environment

property solver_environment

solver part of environment

class EquationSolverType

Solver type for equation systems

Members:

native

eigen

elimination

gmmxx

topological

eigen = <EquationSolverType.eigen: 2>

elimination = <EquationSolverType.elimination: 3>

gmmxx = <EquationSolverType.gmmxx: 1>

property name

native = <EquationSolverType.native: 0>

topological = <EquationSolverType.topological: 4>

property value

class EventuallyFormula

Formula for eventually

class ExactCheckTask

Task for model checking with exact numbers

set_produce_schedulers(self: stormpy.core.ExactCheckTask, produce_schedulers: bool = True) → None

Set whether schedulers should be produced (if possible)

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 ExplicitExactQuantitativeCheckResult

Explicit exact quantitative model checking result

at(self: stormpy.core.ExplicitExactQuantitativeCheckResult, state: int) → pycarl.gmp.gmp.Rational

Get result for given state

get_values(self: stormpy.core.ExplicitExactQuantitativeCheckResult) → List[pycarl.gmp.gmp.Rational]

Get model checking result values for all states

property scheduler

get scheduler

class ExplicitModelBuilder

Model builder for sparse models

build(self: stormpy.core.ExplicitModelBuilder) → storm::models::sparse::Model<double, storm::models::sparse::StandardRewardModel<double> >

Build the model

export_lookup(self: stormpy.core.ExplicitModelBuilder) → storm::builder::ExplicitStateLookup<unsigned int>

Export a lookup model

class ExplicitModelCheckerHintDouble

Information that may accelerate an explicit state model checker

set_compute_only_maybe_states(self: stormpy.core.ExplicitModelCheckerHintDouble, arg0: bool) → None

value

set_maybe_states(self: stormpy.core.ExplicitModelCheckerHintDouble, arg0: storm::storage::BitVector) → None

sets the maybe states. This is assumed to be correct.

set_result_hint(self: stormpy.core.ExplicitModelCheckerHintDouble, result_hint: List[float] | None) → None

set_scheduler_hint(self: stormpy.core.ExplicitModelCheckerHintDouble, scheduler_hint: Optional[storm::storage::Scheduler<double>]) → None

Set a scheduler that is close to the optimal scheduler

class ExplicitParametricModelBuilder

Model builder for sparse models

build(self: stormpy.core.ExplicitParametricModelBuilder) → storm::models::sparse::Model<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, true>, storm::models::sparse::StandardRewardModel<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, true> > >

Build the model

export_lookup(self: stormpy.core.ExplicitParametricModelBuilder) → storm::builder::ExplicitStateLookup<unsigned int>

Export a lookup model

class ExplicitParametricQuantitativeCheckResult

Explicit parametric quantitative model checking result

at(self: stormpy.core.ExplicitParametricQuantitativeCheckResult, state: int) → pycarl.cln.cln.FactorizedRationalFunction

Get result for given state

get_values(self: stormpy.core.ExplicitParametricQuantitativeCheckResult) → List[pycarl.cln.cln.FactorizedRationalFunction]

Get model checking result values for all states

property scheduler

get scheduler

class ExplicitParetoCurveCheckResultDouble

Result for explicit multiobjective model checking

class ExplicitQualitativeCheckResult

Explicit qualitative model checking result

at(self: stormpy.core.ExplicitQualitativeCheckResult, state: int) → bool

Get result for given state

get_truth_values(self: stormpy.core.ExplicitQualitativeCheckResult) → storm::storage::BitVector

Get BitVector representing the truth values

class ExplicitQuantitativeCheckResult

Explicit quantitative model checking result

at(self: stormpy.core.ExplicitQuantitativeCheckResult, state: int) → float

Get result for given state

get_values(self: stormpy.core.ExplicitQuantitativeCheckResult) → List[float]

Get model checking result values for all states

property scheduler

get scheduler

class ExplicitStateLookup

Lookup model for states

lookup(self: stormpy.core.ExplicitStateLookup, state_description: Dict[storm::expressions::Variable, storm::expressions::Expression]) → object

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 FactorizedPolynomial

Represent a polynomial with its factorization

cache(self: pycarl.cln.cln.FactorizedPolynomial) → pycarl.cln.cln._FactorizationCache

property coefficient

constant_part(self: pycarl.cln.cln.FactorizedPolynomial) → pycarl.cln.cln.Rational

derive(self: pycarl.cln.cln.FactorizedPolynomial, variable: pycarl.core.Variable) → pycarl.cln.cln.FactorizedPolynomial

Compute the derivative

evaluate(self: pycarl.cln.cln.FactorizedPolynomial, arg0: Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]) → pycarl.cln.cln.Rational

factorization(self: pycarl.cln.cln.FactorizedPolynomial) → pycarl.cln.cln.Factorization

Get factorization

gather_variables(self: pycarl.cln.cln.FactorizedPolynomial) → Set[pycarl.core.Variable]

is_constant(self: pycarl.cln.cln.FactorizedPolynomial) → bool

is_one(self: pycarl.cln.cln.FactorizedPolynomial) → bool

polynomial(self: pycarl.cln.cln.FactorizedPolynomial) → pycarl.cln.cln.Polynomial

Get underlying polynomial

to_smt2(self: pycarl.cln.cln.FactorizedPolynomial) → str

class FactorizedRationalFunction

Represent a rational function, that is the fraction of two factorized polynomials

constant_part(self: pycarl.cln.cln.FactorizedRationalFunction) → pycarl.cln.cln.Rational

property denominator

derive(self: pycarl.cln.cln.FactorizedRationalFunction, variable: pycarl.core.Variable) → pycarl.cln.cln.FactorizedRationalFunction

Compute the derivative

evaluate(self: pycarl.cln.cln.FactorizedRationalFunction, arg0: Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]) → pycarl.cln.cln.Rational

gather_variables(self: pycarl.cln.cln.FactorizedRationalFunction) → Set[pycarl.core.Variable]

is_constant(self: pycarl.cln.cln.FactorizedRationalFunction) → bool

property numerator

rational_function(self: pycarl.cln.cln.FactorizedRationalFunction) → pycarl.cln.cln.RationalFunction

to_smt2(self: pycarl.cln.cln.FactorizedRationalFunction) → str

class FlatSet

Container to pass to program

insert(self: stormpy.core.FlatSet, arg0: int) → None

insert_set(self: stormpy.core.FlatSet, arg0: stormpy.core.FlatSet) → None

is_subset_of(self: stormpy.core.FlatSet, arg0: stormpy.core.FlatSet) → bool

class Formula

Generic Storm Formula

clone(self: stormpy.logic.logic.Formula) → stormpy.logic.logic.Formula

property is_bounded_until_formula

property is_eventually_formula

property is_multi_objective_formula

property is_probability_operator

is it a probability operator

property is_reward_operator

is it a reward operator

property is_until_formula

substitute(self: stormpy.logic.logic.Formula, constants_map: Dict[stormpy.storage.storage.Variable, stormpy.storage.storage.Expression]) → stormpy.logic.logic.Formula

Substitute variables

substitute_labels_by_labels(self: stormpy.logic.logic.Formula, replacements: Dict[str, str]) → stormpy.logic.logic.Formula

substitute label occurences

class GloballyFormula

Formula for globally

class HybridExactQuantitativeCheckResult

Symbolic exact hybrid quantitative model checking result

get_values(self: stormpy.core.HybridExactQuantitativeCheckResult) → List[pycarl.gmp.gmp.Rational]

Get model checking result values for all states

class HybridParametricQuantitativeCheckResult

Symbolic parametric hybrid quantitative model checking result

get_values(self: stormpy.core.HybridParametricQuantitativeCheckResult) → List[pycarl.cln.cln.FactorizedRationalFunction]

Get model checking result values for all states

class HybridQuantitativeCheckResult

Hybrid quantitative model checking result

get_values(self: stormpy.core.HybridQuantitativeCheckResult) → List[float]

Get model checking result values for all states

class InstantaneousRewardFormula

Instantaneous reward

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]) → 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 0x7fa4be651970>) → 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 JaniModelType

Type of the Jani model

Members:

DTMC

CTMC

MDP

CTMDP

MA

LTS

TA

PTA

STA

HA

PHA

SHA

UNDEFINED

CTMC = <JaniModelType.CTMC: 3>

CTMDP = <JaniModelType.CTMDP: 5>

DTMC = <JaniModelType.DTMC: 2>

HA = <JaniModelType.HA: 10>

LTS = <JaniModelType.LTS: 1>

MA = <JaniModelType.MA: 6>

MDP = <JaniModelType.MDP: 4>

PHA = <JaniModelType.PHA: 11>

PTA = <JaniModelType.PTA: 8>

SHA = <JaniModelType.SHA: 12>

STA = <JaniModelType.STA: 9>

TA = <JaniModelType.TA: 7>

UNDEFINED = <JaniModelType.UNDEFINED: 0>

property name

property value

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

Long run average operator

class LongRunAverageRewardFormula

Long run average reward

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 MinMaxMethod

Method for min-max equation systems

Members:

policy_iteration

value_iteration

linear_programming

topological

rational_search

interval_iteration

sound_value_iteration

optimistic_value_iteration

interval_iteration = <MinMaxMethod.interval_iteration: 5>

linear_programming = <MinMaxMethod.linear_programming: 2>

property name

optimistic_value_iteration = <MinMaxMethod.optimistic_value_iteration: 7>

policy_iteration = <MinMaxMethod.policy_iteration: 1>

rational_search = <MinMaxMethod.rational_search: 4>

sound_value_iteration = <MinMaxMethod.sound_value_iteration: 6>

topological = <MinMaxMethod.topological: 3>

property value

value_iteration = <MinMaxMethod.value_iteration: 0>

class MinMaxSolverEnvironment

Environment for Min-Max-Solvers

property method

property precision

class ModelCheckerHint

Information that may accelerate the model checking process

class ModelFormulasPair

Pair of model and formulas

property formulas

The formulas

property model

The model

class ModelType

Type of the model

Members:

DTMC

MDP

POMDP

CTMC

MA

CTMC = <ModelType.CTMC: 1>

DTMC = <ModelType.DTMC: 0>

MA = <ModelType.MA: 3>

MDP = <ModelType.MDP: 2>

POMDP = <ModelType.POMDP: 5>

property name

property value

class MultiObjectiveFormula

Multi objective formula

property nr_subformulas

Get number of subformulas

property subformulas

Get vector of subformulas

class NativeLinearEquationSolverMethod

Method for linear equation systems with the native solver

Members:

power_iteration

sound_value_iteration

optimistic_value_iteration

interval_iteration

rational_search

jacobi

SOR

gauss_seidel

walker_chae

SOR = <NativeLinearEquationSolverMethod.SOR: 2>

gauss_seidel = <NativeLinearEquationSolverMethod.gauss_seidel: 1>

interval_iteration = <NativeLinearEquationSolverMethod.interval_iteration: 7>

jacobi = <NativeLinearEquationSolverMethod.jacobi: 0>

property name

optimistic_value_iteration = <NativeLinearEquationSolverMethod.optimistic_value_iteration: 6>

power_iteration = <NativeLinearEquationSolverMethod.power_iteration: 4>

rational_search = <NativeLinearEquationSolverMethod.rational_search: 8>

sound_value_iteration = <NativeLinearEquationSolverMethod.sound_value_iteration: 5>

property value

walker_chae = <NativeLinearEquationSolverMethod.walker_chae: 3>

class NativeSolverEnvironment

Environment for Native solvers

property maximum_iterations

property method

property precision

class OperatorFormula

Operator formula

property comparison_type

Comparison type of bound

property has_bound

Flag if formula is bounded

property has_optimality_type

Flag if an optimality type is present

property optimality_type

Flag for the optimality type

remove_bound(self: stormpy.logic.logic.OperatorFormula) → None

remove_optimality_type(self: stormpy.logic.logic.OperatorFormula) → None

remove the optimality type

set_bound(self: stormpy.logic.logic.OperatorFormula, comparison_type: stormpy.logic.logic.ComparisonType, bound: stormpy.storage.storage.Expression) → None

Set bound

set_optimality_type(self: stormpy.logic.logic.OperatorFormula, new_optimality_type: stormpy.core.OptimizationDirection) → None

set the optimality type (use remove optimiality type for clearing)

property threshold

Threshold of bound (currently only applicable to rational expressions)

property threshold_expr

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

Divide = <OperatorType.Divide: 8>

Equal = <OperatorType.Equal: 14>

Floor = <OperatorType.Floor: 21>

Greater = <OperatorType.Greater: 18>

GreaterOrEqual = <OperatorType.GreaterOrEqual: 19>

Iff = <OperatorType.Iff: 4>

Implies = <OperatorType.Implies: 3>

Ite = <OperatorType.Ite: 23>

Less = <OperatorType.Less: 16>

LessOrEqual = <OperatorType.LessOrEqual: 17>

Max = <OperatorType.Max: 10>

Min = <OperatorType.Min: 9>

Minus = <OperatorType.Minus: 6>

Modulo = <OperatorType.Modulo: 12>

Not = <OperatorType.Not: 20>

NotEqual = <OperatorType.NotEqual: 15>

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 OptimizationDirection

Members:

Minimize

Maximize

Maximize = <OptimizationDirection.Maximize: 1>

Minimize = <OptimizationDirection.Minimize: 0>

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 ParametricCheckTask

Task for parametric model checking

set_produce_schedulers(self: stormpy.core.ParametricCheckTask, produce_schedulers: bool = True) → None

Set whether schedulers should be produced (if possible)

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 ParetoCurveCheckResultDouble

Result for multiobjective model checking

get_overapproximation(self: stormpy.core.ParetoCurveCheckResultDouble) → storm::storage::geometry::Polytope<double>

get_underapproximation(self: stormpy.core.ParetoCurveCheckResultDouble) → storm::storage::geometry::Polytope<double>

class PathFormula

Formula about the probability of a set of paths in an automaton

class Polynomial

Represent a multivariate polynomial

constant_part(self: pycarl.cln.cln.Polynomial) → pycarl.cln.cln.Rational

degree(self: pycarl.cln.cln.Polynomial, arg0: pycarl.core.Variable) → int

derive(self: pycarl.cln.cln.Polynomial, variable: pycarl.core.Variable) → pycarl.cln.cln.Polynomial

Compute the derivative

evaluate(self: pycarl.cln.cln.Polynomial, arg0: Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]) → pycarl.cln.cln.Rational

gather_variables(self: pycarl.cln.cln.Polynomial) → Set[pycarl.core.Variable]

is_constant(self: pycarl.cln.cln.Polynomial) → bool

property nr_terms

substitute(self: pycarl.cln.cln.Polynomial, arg0: Dict[pycarl.core.Variable, pycarl.cln.cln.Polynomial]) → pycarl.cln.cln.Polynomial

to_smt2(self: pycarl.cln.cln.Polynomial) → str

property total_degree

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 0x7fa4be8b6930>) → 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 ProbabilityOperator

Probability operator

class Property

property name

Obtain the name of the property

property raw_formula

Obtain the formula directly

class QuotientFormat

Return format of bisimulation quotient

Members:

SPARSE

DD

DD = <QuotientFormat.DD: 1>

SPARSE = <QuotientFormat.SPARSE: 0>

property name

property value

class Rational

Class wrapping gmp-rational numbers

property denominator

property nominator

property numerator

class RationalFunction

Represent a rational function, that is the fraction of two multivariate polynomials

constant_part(self: pycarl.cln.cln.RationalFunction) → pycarl.cln.cln.Rational

property denominator

derive(self: pycarl.cln.cln.RationalFunction, variable: pycarl.core.Variable) → pycarl.cln.cln.RationalFunction

Compute the derivative

evaluate(self: pycarl.cln.cln.RationalFunction, arg0: Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]) → pycarl.cln.cln.Rational

gather_variables(self: pycarl.cln.cln.RationalFunction) → Set[pycarl.core.Variable]

is_constant(self: pycarl.cln.cln.RationalFunction) → bool

property nominator

property numerator

to_smt2(self: pycarl.cln.cln.RationalFunction) → str

RationalRF

alias of Rational

class RewardOperator

Reward operator

has_reward_name(self: stormpy.logic.logic.RewardOperator) → bool

property reward_name

class SMTCounterExampleGenerator

Highlevel Counterexample Generator with SMT as backend

static build(env: stormpy.core.Environment, stats: stormpy.core.SMTCounterExampleGeneratorStats, symbolic_model: storm::storage::SymbolicModelDescription, model: storm::models::sparse::Model<double, storm::models::sparse::StandardRewardModel<double> >, cex_input: storm::counterexamples::SMTMinimalLabelSetGenerator<double>::CexInput, dontcare: stormpy.core.FlatSet, options: stormpy.core.SMTCounterExampleGeneratorOptions) → List[stormpy.core.FlatSet]

Compute counterexample

static precompute(env: stormpy.core.Environment, symbolic_model: storm::storage::SymbolicModelDescription, model: storm::models::sparse::Model<double, storm::models::sparse::StandardRewardModel<double> >, formula: storm::logic::Formula) → storm::counterexamples::SMTMinimalLabelSetGenerator<double>::CexInput

Precompute input for counterexample generation

class SMTCounterExampleGeneratorOptions

Options for highlevel counterexample generation

property add_backward_implication_cuts

property check_threshold_feasible

property continue_after_first_counterexample

property encode_reachability

property maximum_counterexamples

property maximum_iterations_after_counterexample

property silent

property use_dynamic_constraints

class SMTCounterExampleGeneratorStats

Stats for highlevel counterexample generation

property analysis_time

property cut_time

property iterations

property model_checking_time

property setup_time

property solver_time

class SMTCounterExampleInput

Precomputed input for counterexample generation

add_reward_and_threshold(self: stormpy.core.SMTCounterExampleInput, reward_name: str, threshold: float) → None

add another reward structure and threshold

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 SolverEnvironment

Environment for solvers

property minmax_solver_environment

property native_solver_environment

set_force_sound(self: stormpy.core.SolverEnvironment, new_value: bool = True) → None

force soundness

set_linear_equation_solver_type(self: stormpy.core.SolverEnvironment, new_value: stormpy.core.EquationSolverType, set_from_default: bool = False) → None

set solver type to use

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

Labels

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

Labels

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

Labels

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 StateFormula

Formula about a state of an automaton

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

get_rational_value(self: stormpy.storage.storage.StateValuation, state: int, variable: storm::expressions::Variable) → pycarl.gmp.gmp.Rational

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

class StateValuationFunctionActionMaskDouble

class StateValuationsBuilder

add_state(self: stormpy.storage.storage.StateValuationsBuilder, state: int, boolean_values: List[bool] = [], integer_values: List[int] = [], rational_values: List[pycarl.gmp.gmp.Rational] = []) → 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) → stormpy.storage.storage.StateValuation

Creates the finalized state valuations object

exception StormError(message)

Base class for exceptions in Storm.

class SubsystemBuilderOptions

Options for constructing the subsystem

property build_action_mapping

property build_kept_actions

property build_state_mapping

property check_transitions_outside

property fix_deadlocks

class SubsystemBuilderReturnTypeDouble

Result of the construction of a subsystem

property deadlock_label

If set, deadlock states have been introduced and have been assigned this label

property kept_actions

Actions of the subsystem available in the original system

property model

the submodel

property new_to_old_action_mapping

for each action in result, the action index in the original model

property new_to_old_state_mapping

for each state in result, the state index in the original model

class SubsystemBuilderReturnTypeExact

Result of the construction of a subsystem

property deadlock_label

If set, deadlock states have been introduced and have been assigned this label

property kept_actions

Actions of the subsystem available in the original system

property model

the submodel

property new_to_old_action_mapping

for each action in result, the action index in the original model

property new_to_old_state_mapping

for each state in result, the state index in the original model

class SubsystemBuilderReturnTypeRatFunc

Result of the construction of a subsystem

property deadlock_label

If set, deadlock states have been introduced and have been assigned this label

property kept_actions

Actions of the subsystem available in the original system

property model

the submodel

property new_to_old_action_mapping

for each action in result, the action index in the original model

property new_to_old_state_mapping

for each state in result, the state index in the original model

class SymbolicExactQuantitativeCheckResult

Symbolic exact quantitative model checking result

clone(self: stormpy.core.SymbolicExactQuantitativeCheckResult) → stormpy.core.SymbolicExactQuantitativeCheckResult

class SymbolicModelDescription

Symbolic description of model

as_jani_model(self: stormpy.core.SymbolicModelDescription) → storm::jani::Model

Return Jani model

as_prism_program(self: stormpy.core.SymbolicModelDescription) → storm::prism::Program

Return Prism program

instantiate_constants(self: stormpy.core.SymbolicModelDescription, constant_definitions: Dict[storm::expressions::Variable, storm::expressions::Expression]) → stormpy.core.SymbolicModelDescription

Instantiate constants in symbolic model description

property is_jani_model

Flag if program is in Jani format

property is_prism_program

Flag if program is in Prism format

parse_constant_definitions(self: stormpy.core.SymbolicModelDescription, String containing constants and their values: str) → Dict[storm::expressions::Variable, storm::expressions::Expression]

Parse given constant definitions

class SymbolicParametricQuantitativeCheckResult

Symbolic parametric quantitative model checking result

clone(self: stormpy.core.SymbolicParametricQuantitativeCheckResult) → stormpy.core.SymbolicParametricQuantitativeCheckResult

class SymbolicQualitativeCheckResult

Symbolic qualitative model checking result

get_truth_values(self: stormpy.core.SymbolicQualitativeCheckResult) → storm::dd::Bdd<(storm::dd::DdType)1>

Get Dd representing the truth values

class SymbolicQuantitativeCheckResult

Symbolic quantitative model checking result

clone(self: stormpy.core.SymbolicQuantitativeCheckResult) → stormpy.core.SymbolicQuantitativeCheckResult

get_values(self: stormpy.core.SymbolicQuantitativeCheckResult) → storm::dd::Add<(storm::dd::DdType)1, double>

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 TimeOperator

The time operator

class UnaryBooleanStateFormula

Unary boolean state formula

class UnaryPathFormula

Path formula with one operand

property subformula

the subformula

class UnaryStateFormula

State formula with one operand

property subformula

the subformula

class UntilFormula

Path Formula for unbounded until

class Valuation

property expression_manager

class Variable

property id

property is_no_variable

property name

property rank

property type

build_interval_model_from_drn(file, options=<stormpy.core.DirectEncodingParserOptions object>)

Build an interval model in sparse representation from the explicit DRN representation.

Parameters:

• file (String) – DRN file containing the model.

• DirectEncodingParserOptions – Options for the parser.

Returns:

Interval model in sparse representation.

build_model(symbolic_description, properties=None)

Build a model in sparse representation from a symbolic description.

Parameters:

• symbolic_description – Symbolic model description to translate into a model.

• properties (List[Property]) – List of properties that should be preserved during the translation. If None, then all properties are preserved.

Returns:

Model in sparse representation.

build_model_from_drn(file, options=<stormpy.core.DirectEncodingParserOptions object>)

Build a model in sparse representation from the explicit DRN representation.

Parameters:

• file (String) – DRN file containing the model.

• DirectEncodingParserOptions – Options for the parser.

Returns:

Model in sparse representation.

build_parametric_model(symbolic_description, properties=None)

Build a parametric model in sparse representation from a symbolic description.

Parameters:

• symbolic_description – Symbolic model description to translate into a model.

• properties (List[Property]) – List of properties that should be preserved during the translation. If None, then all properties are preserved.

Returns:

Parametric model in sparse representation.

build_parametric_model_from_drn(file, options=<stormpy.core.DirectEncodingParserOptions object>)

Build a parametric model in sparse representation from the explicit DRN representation.

Parameters:

• file (String) – DRN file containing the model.

• DirectEncodingParserOptions – Options for the parser.

Returns:

Parametric model in sparse representation.

build_parametric_sparse_matrix(array, row_group_indices=[])

Build a sparse matrix from numpy array. Zero entries are skipped.

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_exact_model_with_options(model_description: storm::storage::SymbolicModelDescription, options: storm::builder::BuilderOptions) → storm::models::ModelBase

Build the model in sparse representation with exact number representation

build_sparse_matrix(array, row_group_indices=[])

Build a sparse matrix from numpy array. Zero entries are skipped.

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.

build_sparse_model(symbolic_description, properties=None)

Build a model in sparse representation from a symbolic description.

Parameters:

• symbolic_description – Symbolic model description to translate into a model.

• properties (List[Property]) – List of properties that should be preserved during the translation. If None, then all properties are preserved.

Returns:

Model in sparse representation.

build_sparse_model_from_explicit(transition_file: str, labeling_file: str, state_reward_file: str | None = '', transition_reward_file: str | None = '', choice_labeling_file: str | None = '') → storm::models::sparse::Model<double, storm::models::sparse::StandardRewardModel<double> >

Build the model model from explicit input

build_sparse_model_with_options(model_description: storm::storage::SymbolicModelDescription, options: storm::builder::BuilderOptions) → storm::models::ModelBase

Build the model in sparse representation

build_sparse_parametric_model(symbolic_description, properties=None)

Build a parametric model in sparse representation from a symbolic description.

Parameters:

• symbolic_description – Symbolic model description to translate into a model.

• properties (List[Property]) – List of properties that should be preserved during the translation. If None, then all properties are preserved.

Returns:

Parametric model in sparse representation.

build_sparse_parametric_model_with_options(model_description: storm::storage::SymbolicModelDescription, options: storm::builder::BuilderOptions) → storm::models::ModelBase

Build the model in sparse representation

build_symbolic_model(symbolic_description, properties=None)

Build a model in symbolic representation from a symbolic description.

Parameters:

• symbolic_description – Symbolic model description to translate into a model.

• properties (List[Property]) – List of properties that should be preserved during the translation. If None, then all properties are preserved.

Returns:

Model in symbolic representation.

build_symbolic_parametric_model(symbolic_description, properties=None)

Build a parametric model in symbolic representation from a symbolic description.

Parameters:

• symbolic_description – Symbolic model description to translate into a model.

• properties (List[Property]) – List of properties that should be preserved during the translation. If None, then all properties are preserved.

Returns:

Parametric model in symbolic representation.

check_interval_mdp(arg0: storm::models::sparse::Mdp<carl::Interval<double>, storm::models::sparse::StandardRewardModel<carl::Interval<double> > >, arg1: stormpy.core.CheckTask, arg2: stormpy.core.Environment) → stormpy.core._CheckResult

Check interval MDP

check_model_dd(model, property, only_initial_states=False, environment=<stormpy.core.Environment object>)

Perform model checking using dd engine. :param model: Model. :param property: Property to check for. :param only_initial_states: If True, only results for initial states are computed, otherwise for all states. :return: Model checking result. :rtype: CheckResult

check_model_hybrid(model, property, only_initial_states=False, environment=<stormpy.core.Environment object>)

Perform model checking using hybrid engine. :param model: Model. :param property: Property to check for. :param only_initial_states: If True, only results for initial states are computed, otherwise for all states. :return: Model checking result. :rtype: CheckResult

check_model_sparse(model, property, only_initial_states=False, extract_scheduler=False, force_fully_observable=False, hint=None, environment=<stormpy.core.Environment object>)

Perform model checking on model for property. :param model: Model. :param property: Property to check for. :param only_initial_states: If True, only results for initial states are computed, otherwise for all states. :param extract_scheduler: If True, try to extract a scheduler :param hint: If not None, this hint is used by the model checker :param force_fully_observable: If True, treat a POMDP as an MDP :return: Model checking result. :rtype: CheckResult

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

compute_all_until_probabilities(arg0: stormpy.core.Environment, arg1: stormpy.core.CheckTask, arg2: storm::models::sparse::Ctmc<double, storm::models::sparse::StandardRewardModel<double> >, arg3: storm::storage::BitVector, arg4: storm::storage::BitVector) → List[float]

Compute forward until probabilities

compute_expected_number_of_visits(environment, model)

Compute the number of expected visits. Model must be deterministic.

Parameters:

• environment – An model checking environment

• model – A DTMC or CTMC

Returns:

A vector with the expected number of visits

compute_prob01_states(model, phi_states, psi_states)

Compute prob01 states for properties of the form phi_states until psi_states

Parameters:

• model (SparseDTMC)

• phi_states (BitVector)

• psi_states (BitVector) – Target states

compute_prob01max_states(model, phi_states, psi_states)

compute_prob01min_states(model, phi_states, psi_states)

compute_steady_state_distribution(environment, model)

Compute the steady-state (aka stationary) distribution. Model must be deterministic.

Parameters:

• environment – A model checking environment

• model – A DTMC or CTMC

Returns:

A vector with the steady-state distribution

compute_transient_probabilities(arg0: stormpy.core.Environment, arg1: storm::models::sparse::Ctmc<double, storm::models::sparse::StandardRewardModel<double> >, arg2: storm::storage::BitVector, arg3: storm::storage::BitVector, arg4: float) → List[float]

Compute transient probabilities

construct_submodel(model, states, actions, keep_unreachable_states=True, options=<stormpy.core.SubsystemBuilderOptions object>)

Parameters:

• model – The model

• states – Which states should be preserved

• actions – Which actions should be preserved

• keep_unreachable_states – If False, run a reachability analysis.

• options – An options object of type SubsystemBuilderOptions

Returns:

A model with fewer states/actions

create_filter_initial_states_sparse(model: storm::models::sparse::Model<double, storm::models::sparse::StandardRewardModel<double> >) → stormpy.core._QualitativeCheckResult

Create a filter for the initial states on a sparse model

create_filter_initial_states_symbolic(model: storm::models::symbolic::Model<(storm::dd::DdType)1, double>) → stormpy.core._QualitativeCheckResult

Create a filter for the initial states on a symbolic model

create_filter_symbolic(model: storm::models::symbolic::Model<(storm::dd::DdType)1, double>, states: storm::expressions::Expression) → stormpy.core._QualitativeCheckResult

Creates a filter for the given states and a symbolic model

eliminate_ECs(matrix, subsystem, possible_ecs, add_sink_row_states, add_self_loop_at_sink_states=False)

For each such EC (that is not contained in another EC), we add a new state and redirect all incoming and outgoing

transitions of the EC to (and from) this state.

Parameters:

• matrix

• subsystem – BitVector with states many entries. Only states in the given subsystem are kept. Transitions leading to a state outside of the subsystem will be removed (but the corresponding row is kept, possibly yielding empty rows). The ECs are then identified on the subsystem.

• possible_ecs – BitVector with rows many entries. Only ECs for which possible_ecs is true for all choices are considered. Furthermore, the rows that contain a transition leading outside of the subsystem are not considered for an EC.

• add_sink_row_states – BitVector with states many entries. If add_sink_row_states is true for at least one state of an eliminated EC, a row is added to the new state (representing the choice to stay at the EC forever).

• add_self_loop_at_sink_states – if true, such rows get a selfloop (with value 1). Otherwise, the row remains empty.

Returns:

A container with various information.

eliminate_non_markovian_chains(ma, properties, label_behavior)

Eliminate chains of non-Markovian states if possible. :param ma: Markov automaton. :param properties: List of properties to transform as well. :param label_behavior: Behavior of labels while elimination. :return: Tuple (converted MA, converted properties).

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

Eliminate reward accumulations

export_to_drn(model, file, options=<stormpy.core.DirectEncodingOptions object>)

Export a model to DRN format :param model: The model :param file: A path :param options: DirectEncodingOptions :return:

get_maximal_end_components(model)

Get maximal end components from model. :param model: Model. :return: Maximal end components.

get_reachable_states(model, initial_states, constraint_states, target_states, maximal_steps=None, choice_filter=None)

Get the states that are reachable in a sparse model

Parameters:

• model – A model

• initial_states – Which states should be definitively reachable

• constraint_states

• target_states – Which states should be considered absorbing

• maximal_steps – The maximal depth to explore

• choice_filter

Returns:

install_signal_handlers(arg0: int) → None

make_sparse_model_builder(model_description: storm::storage::SymbolicModelDescription, options: storm::builder::BuilderOptions, action_mask: storm::generator::ActionMask<double, unsigned int> = None) → storm::builder::ExplicitModelBuilder<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>

Construct a builder instance

make_sparse_model_builder_exact(model_description: storm::storage::SymbolicModelDescription, options: storm::builder::BuilderOptions, action_mask: storm::generator::ActionMask<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, unsigned int> = None) → storm::builder::ExplicitModelBuilder<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, storm::models::sparse::StandardRewardModel<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >, unsigned int>

Construct a builder instance

make_sparse_model_builder_parametric(model_description: storm::storage::SymbolicModelDescription, options: storm::builder::BuilderOptions, action_mask: storm::generator::ActionMask<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, true>, unsigned int> = None) → storm::builder::ExplicitModelBuilder<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, true>, storm::models::sparse::StandardRewardModel<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, true> >, unsigned int>

Construct a builder instance

model_checking(model, property, only_initial_states=False, extract_scheduler=False, force_fully_observable=False, environment=<stormpy.core.Environment object>)

Perform model checking on model for property. :param model: Model. :param property: Property to check for. :param only_initial_states: If True, only results for initial states are computed, otherwise for all states. :param extract_scheduler: If True, try to extract a scheduler :return: Model checking result. :rtype: CheckResult

parse_constants_string(expression_manager: storm::expressions::ExpressionManager, definition_string: str) → Dict[storm::expressions::Variable, storm::expressions::Expression]

Parse constants definition

parse_jani_model(path: str) → Tuple[storm::jani::Model, List[stormpy.core.Property]]

Parse Jani model

parse_jani_model_from_string(json_string: str) → Tuple[storm::jani::Model, List[stormpy.core.Property]]

Parse Jani model from string

parse_prism_program(path: str, prism_compat: bool = False, simplify: bool = True) → storm::prism::Program

Parse Prism program

parse_properties(properties, context=None, filters=None)

Parameters:

• properties – A string with the pctl properties

• context – A symbolic model that gives meaning to variables and constants.

• filters – filters, if applicable.

Returns:

A list of properties

parse_properties_for_jani_model(formula_string: str, jani_model: storm::jani::Model, property_filter: Optional[Set[str]] = None) → List[stormpy.core.Property]

parse_properties_for_prism_program(formula_string: str, prism_program: storm::prism::Program, property_filter: Optional[Set[str]] = None) → List[stormpy.core.Property]

Parses properties given in the prism format, allows references to variables in the prism program.

Parameters:

• formula_str (str) – A string of formulas

• prism_program (PrismProgram) – A prism program

• property_filter (str) – A filter

Returns:

A list of properties

parse_properties_without_context(formula_string: str, property_filter: Set[str] | None = None) → List[stormpy.core.Property]

Parse properties given in the prism format.

Parameters:

• formula_str (str) – A string of formulas

• property_filter (str) – A filter

Returns:

A list of properties

perform_bisimulation(model, properties, bisimulation_type)

Perform bisimulation on model. :param model: Model. :param properties: Properties to preserve during bisimulation. :param bisimulation_type: Type of bisimulation (weak or strong). :return: Model after bisimulation.

perform_sparse_bisimulation(model, properties, bisimulation_type)

Perform bisimulation on model in sparse representation. :param model: Model. :param properties: Properties to preserve during bisimulation. :param bisimulation_type: Type of bisimulation (weak or strong). :return: Model after bisimulation.

perform_symbolic_bisimulation(model, properties, quotient_format=<QuotientFormat.DD: 1>)

Perform bisimulation on model in symbolic representation. :param model: Model. :param properties: Properties to preserve during bisimulation. :param quotient_format: Return format of quotient. :return: Model after bisimulation.

preprocess_symbolic_input(symbolic_model_description: storm::storage::SymbolicModelDescription, properties: List[stormpy.core.Property], constant_definition_string: str) → Tuple[storm::storage::SymbolicModelDescription, List[stormpy.core.Property]]

Preprocess symoblic input

prob01max_states(model, eventually_formula)

prob01min_states(model, eventually_formula)

reset_timeout() → None

Reset timeout

set_loglevel_debug() → None

set loglevel for storm to debug

set_loglevel_error() → None

set_loglevel_trace() → None

set_settings(arguments: List[str]) → None

Set settings

set_timeout(timeout: int) → None

Set timeout in seconds

topological_sort(model, forward=True, initial=[])

Parameters:

• model – A sparse model

• forward – A flag whether the sorting should be forward or backwards

• initial – a list of states

Returns:

A topological sort of the states

transform_to_discrete_time_model(model, properties)

Transform continuous-time model to discrete time model. :param model: Continuous-time model. :param properties: List of properties to transform as well. :return: Tuple (Discrete-time model, converted properties).

transform_to_sparse_model(model)

Transform model in symbolic representation into model in sparse representation. :param model: Symbolic model. :return: Sparse model.