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

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¶

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

Game formula

property is_game_formula¶: is it a game formula

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.

Parameters:

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

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

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

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

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

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

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

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

Parameters:

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

class IntervalSparseMatrixEntry¶

Entry of sparse matrix

property column¶: Column

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

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

class IntervalSparseMatrixRows¶: Set of rows in a sparse matrix

class ItemLabeling¶

Labeling

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

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

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

class JaniAssignment¶

Jani Assignment

property expression¶

property variable¶: variable that is assigned to, if any

class JaniAutomaton¶

A Jani Automation

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

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

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

property edges¶: get edges

get_location_index(self: stormpy.storage.storage.JaniAutomaton, name: str) → int¶

property initial_location_indices¶

property initial_states_restriction¶: initial state restriction

property location_variable¶

property locations¶

property name¶

property variables¶

class JaniChoiceOrigins¶

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

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

property model¶: retrieves the associated JANI model

class JaniConstant¶

A Constant in JANI

property defined¶: is constant defined by some expression

property expression_variable¶: expression variable for this constant

property name¶: name of constant

property type¶: type of constant

class JaniEdge¶

A Jani Edge

property action_index¶: action index

property color¶: color for the edge

property destinations¶: edge destinations

property guard¶: edge guard

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

property nr_destinations¶: nr edge destinations

property rate¶: edge rate

property source_location_index¶: index for source location

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

property template_edge¶: template edge

class JaniEdgeDestination¶

Destination in Jani

property assignments¶

property probability¶

property target_location_index¶

class JaniInformationObject¶

An object holding information about a JANI model

property avg_var_domain_size¶

property model_type¶

property nr_automata¶

property nr_edges¶

property nr_variables¶

property state_domain_size¶

class JaniLocation¶

A Location in JANI

property assignments¶: location assignments

property name¶: name of the location

class JaniLocationExpander¶

A transformer for Jani expanding variables into locations

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

class JaniModel¶

A Jani Model

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

add_constant(self: stormpy.storage.storage.JaniModel, constant: storm::jani::Constant) → None¶: adds constant to model

property automata¶: get automata

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

property constants¶: get constants

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

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

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

property expression_manager¶: get expression manager

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

flatten_composition(self: stormpy.storage.storage.JaniModel, smt_solver_factory: stormpy.utility.utility.SmtSolverFactory = <stormpy.utility.utility.SmtSolverFactory object at 0x7f23aa5daef0>) → 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], substitute_transcendental_numbers: bool) → None¶: substitute in rhs according to given substitution map

class JaniScopeChanger¶

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

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

class JaniTemplateEdge¶

Template edge, internal data structure for edges

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

property assignments¶

property destinations¶

property guard¶

class JaniTemplateEdgeDestination¶

Template edge destination, internal data structure for edge destinations

property assignments¶

class JaniVariable¶

A Variable in JANI

property expression_variable¶: expression variable for this variable

property init_expression¶

property name¶: name of constant

class JaniVariableSet¶

Jani Set of Variables

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

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

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

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

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

class 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

SMG

CTMC = <ModelType.CTMC: 1>¶

DTMC = <ModelType.DTMC: 0>¶

MA = <ModelType.MA: 3>¶

MDP = <ModelType.MDP: 2>¶

POMDP = <ModelType.POMDP: 5>¶

SMG = <ModelType.SMG: 6>¶

property name¶

property value¶

class 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: 24>¶

Divide = <OperatorType.Divide: 8>¶

Equal = <OperatorType.Equal: 16>¶

Floor = <OperatorType.Floor: 23>¶

Greater = <OperatorType.Greater: 20>¶

GreaterOrEqual = <OperatorType.GreaterOrEqual: 21>¶

Iff = <OperatorType.Iff: 4>¶

Implies = <OperatorType.Implies: 3>¶

Ite = <OperatorType.Ite: 25>¶

Less = <OperatorType.Less: 18>¶

LessOrEqual = <OperatorType.LessOrEqual: 19>¶

Max = <OperatorType.Max: 10>¶

Min = <OperatorType.Min: 9>¶

Minus = <OperatorType.Minus: 6>¶

Modulo = <OperatorType.Modulo: 12>¶

Not = <OperatorType.Not: 22>¶

NotEqual = <OperatorType.NotEqual: 17>¶

Or = <OperatorType.Or: 1>¶

Plus = <OperatorType.Plus: 5>¶

Power = <OperatorType.Power: 11>¶

Times = <OperatorType.Times: 7>¶

Xor = <OperatorType.Xor: 2>¶

property name¶

property value¶

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

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 0x7f23aafe15b0>) → 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 labels¶: Get choice labels

property origins¶: Get choice origins

property transitions¶: Get transitions

class SparseExactModelActions¶: Actions for state in sparse model

class SparseExactModelComponents¶

Components required for building a sparse model

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

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

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

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

property observability_classes¶: The POMDP observations

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

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

property reward_models¶: Reward models associated with the model

property state_labeling¶: The state labeling

property state_player_indications¶: The vector mapping states to player indices

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

property transition_matrix¶: The transition matrix

class SparseExactModelState¶

State in sparse model

property actions¶: Get actions

property id¶: Id

property labels¶: Get state labels

property valuations¶: Get state valuations

class SparseExactModelStates¶: States in sparse model

class SparseExactPomdp¶

POMDP in sparse representation

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

has_observation_valuations(self: stormpy.storage.storage.SparseExactPomdp) → bool¶

property nr_observations¶

property observation_valuations¶

property observations¶

class SparseExactRewardModel¶

Reward structure for sparse models

get_state_action_reward(self: stormpy.storage.storage.SparseExactRewardModel, arg0: int) → pycarl.gmp.gmp.Rational¶

get_state_reward(self: stormpy.storage.storage.SparseExactRewardModel, arg0: int) → pycarl.gmp.gmp.Rational¶

get_zero_reward_states(self: stormpy.storage.storage.SparseExactRewardModel, transition_matrix: storm::storage::SparseMatrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >) → stormpy.storage.storage.BitVector¶: get states where all rewards are zero

property has_state_action_rewards¶

property has_state_rewards¶

property has_transition_rewards¶

reduce_to_state_based_rewards(self: stormpy.storage.storage.SparseExactRewardModel, transition_matrix: storm::storage::SparseMatrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >, only_state_rewards: bool) → None¶: Reduce to state-based rewards

set_state_reward(self: stormpy.storage.storage.SparseExactRewardModel, arg0: int, arg1: pycarl.gmp.gmp.Rational) → None¶

property state_action_rewards¶

property state_rewards¶

property transition_rewards¶

class SparseExactSmg¶

SMG in sparse representation

get_player_of_state(self: stormpy.storage.storage.SparseExactSmg, state: int) → int¶: Get player for the given state

get_state_player_indications(self: stormpy.storage.storage.SparseExactSmg) → List[int]¶: Get for each state its corresponding player

class SparseIntervalCtmc¶

CTMC in sparse representation

property exit_rates¶

class SparseIntervalDtmc¶: DTMC in sparse representation

class SparseIntervalMA¶

MA in sparse representation

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

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

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

property exit_rates¶

property markovian_states¶

property nondeterministic_choice_indices¶

class SparseIntervalMdp¶

MDP in sparse representation

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

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

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

property nondeterministic_choice_indices¶

class SparseIntervalModelAction¶

Action for state in sparse model

property id¶: Id

property labels¶: Get choice labels

property origins¶: Get choice origins

property transitions¶: Get transitions

class SparseIntervalModelActions¶: Actions for state in sparse model

class SparseIntervalModelComponents¶

Components required for building a sparse model

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

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

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

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

property observability_classes¶: The POMDP observations

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

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

property reward_models¶: Reward models associated with the model

property state_labeling¶: The state labeling

property state_player_indications¶: The vector mapping states to player indices

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

property transition_matrix¶: The transition matrix

class SparseIntervalModelState¶

State in sparse model

property actions¶: Get actions

property id¶: Id

property labels¶: Get state labels

property valuations¶: Get state valuations

class SparseIntervalModelStates¶: States in sparse model

class SparseIntervalPomdp¶

POMDP in sparse representation

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

has_observation_valuations(self: stormpy.storage.storage.SparseIntervalPomdp) → bool¶

property nr_observations¶

property observation_valuations¶

property observations¶

class SparseIntervalRewardModel¶

Reward structure for sparse models

get_state_action_reward(self: stormpy.storage.storage.SparseIntervalRewardModel, arg0: int) → pycarl.core.Interval¶

get_state_reward(self: stormpy.storage.storage.SparseIntervalRewardModel, arg0: int) → pycarl.core.Interval¶

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

property has_state_action_rewards¶

property has_state_rewards¶

property has_transition_rewards¶

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

set_state_reward(self: stormpy.storage.storage.SparseIntervalRewardModel, arg0: int, arg1: pycarl.core.Interval) → None¶

property state_action_rewards¶

property state_rewards¶

property transition_rewards¶

class SparseIntervalSmg¶

SMG in sparse representation

get_player_of_state(self: stormpy.storage.storage.SparseIntervalSmg, state: int) → int¶: Get player for the given state

get_state_player_indications(self: stormpy.storage.storage.SparseIntervalSmg) → List[int]¶: Get for each state its corresponding player

class SparseMA¶

MA in sparse representation

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

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

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

property exit_rates¶

property markovian_states¶

property nondeterministic_choice_indices¶

class SparseMatrix¶

Sparse matrix

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

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

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

get_rows_for_group(self: stormpy.storage.storage.SparseMatrix, row_group: int) → List[int]¶: Get rows within a row group

property has_trivial_row_grouping¶: Trivial row grouping

make_row_grouping_trivial(self: stormpy.storage.storage.SparseMatrix) → None¶: Makes row groups trivial. Use with care.

property nr_columns¶: Number of columns

property nr_entries¶: Number of non-zero entries

property nr_rows¶: Number of rows

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

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

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

class SparseMatrixBuilder¶

Builder of sparse matrix

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

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

Parameters:

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

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

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

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

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

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

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

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

Parameters:

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

class SparseMatrixEntry¶

Entry of sparse matrix

property column¶: Column

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

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

class SparseMatrixRows¶: Set of rows in a sparse matrix

class SparseMdp¶

MDP in sparse representation

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

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

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

property nondeterministic_choice_indices¶

class SparseModelAction¶

Action for state in sparse model

property id¶: Id

property labels¶: Get choice labels

property origins¶: Get choice origins

property transitions¶: Get transitions

class SparseModelActions¶: Actions for state in sparse model

class SparseModelComponents¶

Components required for building a sparse model

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

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

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

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

property observability_classes¶: The POMDP observations

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

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

property reward_models¶: Reward models associated with the model

property state_labeling¶: The state labeling

property state_player_indications¶: The vector mapping states to player indices

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

property transition_matrix¶: The transition matrix

class SparseModelState¶

State in sparse model

property actions¶: Get actions

property id¶: Id

property labels¶: Get state labels

property valuations¶: Get state valuations

class SparseModelStates¶: States in sparse model

class SparseParametricCtmc¶: pCTMC in sparse representation

class SparseParametricDtmc¶: pDTMC in sparse representation

class SparseParametricMA¶

pMA in sparse representation

apply_scheduler(self: stormpy.storage.storage.SparseParametricMA, scheduler: storm::storage::Scheduler<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, true> >, drop_unreachable_states: bool = True) → stormpy.storage.storage._SparseParametricModel¶: apply scheduler

property nondeterministic_choice_indices¶

class SparseParametricMdp¶

pMDP in sparse representation

apply_scheduler(self: stormpy.storage.storage.SparseParametricMdp, scheduler: storm::storage::Scheduler<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, true> >, drop_unreachable_states: bool = True) → stormpy.storage.storage._SparseParametricModel¶: apply scheduler

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

property nondeterministic_choice_indices¶

class SparseParametricModelAction¶

Action for state in sparse model

property id¶: Id

property labels¶: Get choice labels

property origins¶: Get choice origins

property transitions¶: Get transitions

class SparseParametricModelActions¶: Actions for state in sparse model

class SparseParametricModelComponents¶

Components required for building a sparse model

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

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

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

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

property observability_classes¶: The POMDP observations

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

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

property reward_models¶: Reward models associated with the model

property state_labeling¶: The state labeling

property state_player_indications¶: The vector mapping states to player indices

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

property transition_matrix¶: The transition matrix

class SparseParametricModelState¶

State in sparse model

property actions¶: Get actions

property id¶: Id

property labels¶: Get state labels

property valuations¶: Get state valuations

class SparseParametricModelStates¶: States in sparse model

class SparseParametricPomdp¶

POMDP in sparse representation

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

property nr_observations¶

property observations¶

class SparseParametricRewardModel¶

Reward structure for parametric sparse models

get_state_action_reward(self: stormpy.storage.storage.SparseParametricRewardModel, arg0: int) → pycarl.cln.cln.FactorizedRationalFunction¶

get_state_reward(self: stormpy.storage.storage.SparseParametricRewardModel, arg0: int) → pycarl.cln.cln.FactorizedRationalFunction¶

property has_state_action_rewards¶

property has_state_rewards¶

property has_transition_rewards¶

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

property state_action_rewards¶

property state_rewards¶

property transition_rewards¶

class SparsePomdp¶

POMDP in sparse representation

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

has_observation_valuations(self: stormpy.storage.storage.SparsePomdp) → bool¶

property nr_observations¶

property observation_valuations¶

property observations¶

class SparseRewardModel¶

Reward structure for sparse models

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

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

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

property has_state_action_rewards¶

property has_state_rewards¶

property has_transition_rewards¶

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

set_state_reward(self: stormpy.storage.storage.SparseRewardModel, arg0: int, arg1: float) → None¶

property state_action_rewards¶

property state_rewards¶

property transition_rewards¶

class SparseSmg¶

SMG in sparse representation

get_player_of_state(self: stormpy.storage.storage.SparseSmg, state: int) → int¶: Get player for the given state

get_state_player_indications(self: stormpy.storage.storage.SparseSmg) → List[int]¶: Get for each state its corresponding player

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