Stormpy.core

class ActionMaskDouble
class AddIterator_Sylvan_Double

AddIterator

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

Add

class AtomicExpressionFormula

Formula with an atomic expression

get_expression(self: stormpy.logic.logic.AtomicExpressionFormula) stormpy.storage.storage.Expression
class AtomicLabelFormula

Formula with an atomic label

property label

label in the formula

class Bdd_Sylvan

Bdd

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

Members:

AND

OR

AND = <BinaryBooleanOperatorType.AND: 0>
OR = <BinaryBooleanOperatorType.OR: 1>
property name
property value
class BinaryPathFormula

Path formula with two operands

property left_subformula
property right_subformula
class BinaryStateFormula

State formula with two operands

class BisimulationType

Types of bisimulation

Members:

STRONG

WEAK

STRONG = <BisimulationType.STRONG: 0>
WEAK = <BisimulationType.WEAK: 1>
property name
property value
class BitVector
as_int(self: stormpy.storage.storage.BitVector, index: int, no_bits: int) int

Get as unsigned int

get(self: stormpy.storage.storage.BitVector, index: int) bool
static load_from_string(description: str) stormpy.storage.storage.BitVector
number_of_set_bits(self: stormpy.storage.storage.BitVector) int
set(self: stormpy.storage.storage.BitVector, index: int, value: bool = True) None

Set

size(self: stormpy.storage.storage.BitVector) int
store_as_string(self: stormpy.storage.storage.BitVector) str
class BooleanBinaryStateFormula

Boolean binary state formula

class BooleanLiteralFormula

Formula with a boolean literal

class BoundedUntilFormula

Until Formula with either a step or a time bound.

property has_lower_bound
property is_multidimensional

Is the bound multi-dimensional

property left_subformula
property right_subformula
property upper_bound_expression
class BuilderOptions

Options for building process

property preserved_label_names

Labels preserved

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

Build with out of bounds state

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

Build with overlapping guards state labeled

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

Build with all state labels

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

Build with all reward models

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

Build with choice labels

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

Build observation valuations

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

Build state valuations

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

Build choice origins

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

Perform extra checks during exploration

class CheckTask

Task for model checking

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

Sets a hint that may speed up the solver

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

Set whether schedulers should be produced (if possible)

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

Sets whether robust uncertainty should be considered

class ChoiceLabeling

Labeling for choices

add_label_to_choice(self: stormpy.storage.storage.ChoiceLabeling, label: str, state: int) None

Adds a label to a given choice

get_choices(self: stormpy.storage.storage.ChoiceLabeling, label: str) stormpy.storage.storage.BitVector

Get all choices which have the given label

get_labels_of_choice(self: stormpy.storage.storage.ChoiceLabeling, choice: int) Set[str]

Get labels of the given choice

set_choices(self: stormpy.storage.storage.ChoiceLabeling, label: str, choices: stormpy.storage.storage.BitVector) None

Add a label to a the given choices

class ChoiceOrigins

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

as_jani_choice_origins(self: stormpy.storage.storage.ChoiceOrigins) storm::storage::sparse::JaniChoiceOrigins
as_prism_choice_origins(self: stormpy.storage.storage.ChoiceOrigins) storm::storage::sparse::PrismChoiceOrigins
get_choice_info(self: stormpy.storage.storage.ChoiceOrigins, identifier: int) str

human readable string

get_identifier_info(self: stormpy.storage.storage.ChoiceOrigins, identifier: int) str

human readable string

get_number_of_identifiers(self: stormpy.storage.storage.ChoiceOrigins) int

the number of considered identifier

is_jani_choice_origins(self: stormpy.storage.storage.ChoiceOrigins) bool
is_prism_choice_origins(self: stormpy.storage.storage.ChoiceOrigins) bool
class ComparisonType

Members:

LESS

LEQ

GREATER

GEQ

GEQ = <ComparisonType.GEQ: 3>
GREATER = <ComparisonType.GREATER: 2>
LEQ = <ComparisonType.LEQ: 1>
LESS = <ComparisonType.LESS: 0>
property name
property value
class ConditionalFormula

Formula with the right hand side being a condition.

class ConstraintCollector

Collector for constraints on parametric Markov chains

property graph_preserving_constraints

Get the constraints ensuring the graph is preserved

property wellformed_constraints

Get the constraints ensuring a wellformed model

class CumulativeRewardFormula

Summed rewards over a the paths

class DdManager_Sylvan
get_meta_variable(self: stormpy.storage.storage.DdManager_Sylvan, expression_variable: storm::expressions::Variable) stormpy.storage.storage.DdMetaVariable_Sylvan
class DdMetaVariableType

Members:

Int

Bool

Bitvector

Bitvector = <DdMetaVariableType.Bitvector: 2>
Bool = <DdMetaVariableType.Bool: 0>
Int = <DdMetaVariableType.Int: 1>
property name
property value
class DdMetaVariable_Sylvan
compute_indices(self: stormpy.storage.storage.DdMetaVariable_Sylvan, sorted: bool = True) List[int]
property lowest_value
property name
property type
class Dd_Sylvan

Dd

property dd_manager

get the manager

property meta_variables

the contained meta variables

property node_count

get node count

class DiceStringVisitor

Translate expressions to dice

to_string(self: stormpy.storage.storage.DiceStringVisitor, arg0: stormpy.storage.storage.Expression) str
class DirectEncodingOptions
property allow_placeholders
class DirectEncodingParserOptions

Options for the .drn parser

property build_choice_labels

Build with choice labels

class Distribution

Finite Support Distribution

class DistributionExact

Finite Support Distribution

class DistributionInterval

Finite Support Distribution

class EliminationLabelBehavior

Behavior of labels while eliminating non-Markovian chains

Members:

KEEP_LABELS

MERGE_LABELS

DELETE_LABELS

DELETE_LABELS = <EliminationLabelBehavior.DELETE_LABELS: 3>
KEEP_LABELS = <EliminationLabelBehavior.KEEP_LABELS: 0>
MERGE_LABELS = <EliminationLabelBehavior.MERGE_LABELS: 2>
property name
property value
class EndComponentEliminatorReturnTypeDouble

Container for result of endcomponent elimination

property matrix

The resulting matrix

property new_to_old_row_mapping

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

property old_to_new_state_mapping

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

property sink_rows

Rows that indicate staying in the EC forever

class Environment
property solver_environment

solver part of environment

class EquationSolverType

Solver type for equation systems

Members:

native

eigen

elimination

gmmxx

topological

eigen = <EquationSolverType.eigen: 2>
elimination = <EquationSolverType.elimination: 3>
gmmxx = <EquationSolverType.gmmxx: 1>
property name
native = <EquationSolverType.native: 0>
topological = <EquationSolverType.topological: 4>
property value
class EventuallyFormula

Formula for eventually

class ExactCheckTask

Task for model checking with exact numbers

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

Set whether schedulers should be produced (if possible)

class ExactSparseMatrix

Sparse matrix

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

Get row

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

Get rows within a row group

property has_trivial_row_grouping

Trivial row grouping

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

Makes row groups trivial. Use with care.

property nr_columns

Number of columns

property nr_entries

Number of non-zero entries

property nr_rows

Number of rows

print_row(self: stormpy.storage.storage.ExactSparseMatrix, row: int) str

Print rows from start to end

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

Get iterator from start to end

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

Get submatrix

class ExactSparseMatrixBuilder

Builder of sparse matrix

add_next_value(self: stormpy.storage.storage.ExactSparseMatrixBuilder, row: int, column: int, value: pycarl.gmp.gmp.Rational) None

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

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

Parameters:
  • row (double) – The row in which the matrix entry is to be set

  • column (double) – The column in which the matrix entry is to be set

  • value (double) – The value that is to be set at the specified row and column

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

Finalize the sparse matrix

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

Get the current row group count

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

the most recently used column

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

Get the most recently used row

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

Start a new row group in the matrix

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

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

Parameters:
  • replacements (std::vector<double> const&) – replacements Mapping indicating the replacements from offset+i -> value of i

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

class ExactSparseMatrixEntry

Entry of sparse matrix

property column

Column

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

Set value

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

Value

class ExactSparseMatrixRows

Set of rows in a sparse matrix

class ExplicitExactQuantitativeCheckResult

Explicit exact quantitative model checking result

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

Get result for given state

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

Get model checking result values for all states

property scheduler

get scheduler

class ExplicitModelBuilder

Model builder for sparse models

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

Build the model

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

Export a lookup model

class ExplicitModelCheckerHintDouble

Information that may accelerate an explicit state model checker

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

value

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

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

set_result_hint(self: stormpy.core.ExplicitModelCheckerHintDouble, result_hint: List[float] | None) None
set_scheduler_hint(self: stormpy.core.ExplicitModelCheckerHintDouble, scheduler_hint: Optional[storm::storage::Scheduler<double>]) None

Set a scheduler that is close to the optimal scheduler

class ExplicitParametricModelBuilder

Model builder for sparse models

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

Build the model

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

Export a lookup model

class ExplicitParametricQuantitativeCheckResult

Explicit parametric quantitative model checking result

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

Get result for given state

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

Get model checking result values for all states

property scheduler

get scheduler

class ExplicitParetoCurveCheckResultDouble

Result for explicit multiobjective model checking

class ExplicitQualitativeCheckResult

Explicit qualitative model checking result

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

Get result for given state

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

Get BitVector representing the truth values

class ExplicitQuantitativeCheckResult

Explicit quantitative model checking result

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

Get result for given state

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

Get model checking result values for all states

property scheduler

get scheduler

class ExplicitStateLookup

Lookup model for states

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

Holds an expression

static And(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression
static Conjunction(arg0: List[stormpy.storage.storage.Expression]) stormpy.storage.storage.Expression
static Disjunction(arg0: List[stormpy.storage.storage.Expression]) stormpy.storage.storage.Expression
static Divide(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression
static Eq(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression
static Geq(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression
static Greater(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression
static Iff(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression
static Implies(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression
static Leq(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression
static Less(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression
static Minus(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression
static Modulo(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression
static Multiply(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression
static Neq(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression
static Or(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression
static Plus(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression
property arity

The arity of the expression

contains_variable(self: stormpy.storage.storage.Expression, variables: Set[stormpy.storage.storage.Variable]) bool

Check if the expression contains any of the given variables.

contains_variables(self: stormpy.storage.storage.Expression) bool

Check if the expression contains variables.

evaluate_as_bool(self: stormpy.storage.storage.Expression) bool

Get the boolean value this expression evaluates to

evaluate_as_double(self: stormpy.storage.storage.Expression) float

Get the double value this expression evaluates to

evaluate_as_int(self: stormpy.storage.storage.Expression) int

Get the integer value this expression evaluates to

evaluate_as_rational(self: stormpy.storage.storage.Expression) pycarl.gmp.gmp.Rational

Get the rational number this expression evaluates to

get_operand(self: stormpy.storage.storage.Expression, operandIndex: int) stormpy.storage.storage.Expression

Get the operand at the given index

get_variables(self: stormpy.storage.storage.Expression) Set[stormpy.storage.storage.Variable]

Get the variables

has_boolean_type(self: stormpy.storage.storage.Expression) bool

Check if the expression is a boolean

has_integer_type(self: stormpy.storage.storage.Expression) bool

Check if the expression is an integer

has_rational_type(self: stormpy.storage.storage.Expression) bool

Check if the expression is a rational

identifier(self: stormpy.storage.storage.Expression) str

Retrieves the identifier associated with this expression if this expression is a variable

property is_function_application

True iff the expression is a function application (of any sort

is_literal(self: stormpy.storage.storage.Expression) bool

Check if the expression is a literal

is_variable(self: stormpy.storage.storage.Expression) bool

Check if the expression is a variable

property manager

Get the manager

property operator

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

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

Simplify expression

substitute(self: stormpy.storage.storage.Expression, substitution_map: Dict[stormpy.storage.storage.Variable, stormpy.storage.storage.Expression]) stormpy.storage.storage.Expression
property type

Get the Type

class ExpressionManager

Manages variables for expressions

create_boolean(self: stormpy.storage.storage.ExpressionManager, boolean: bool) storm::expressions::Expression

Create expression from boolean

create_boolean_variable(self: stormpy.storage.storage.ExpressionManager, name: str, auxiliary: bool = False) storm::expressions::Variable

create Boolean variable

create_integer(self: stormpy.storage.storage.ExpressionManager, integer: int) storm::expressions::Expression

Create expression from integer number

create_integer_variable(self: stormpy.storage.storage.ExpressionManager, name: str, auxiliary: bool = False) storm::expressions::Variable

create Integer variable

create_rational(self: stormpy.storage.storage.ExpressionManager, rational: pycarl.gmp.gmp.Rational) storm::expressions::Expression

Create expression from rational number

create_rational_variable(self: stormpy.storage.storage.ExpressionManager, name: str, auxiliary: bool = False) storm::expressions::Variable

create Rational variable

get_variable(self: stormpy.storage.storage.ExpressionManager, name: str) storm::expressions::Variable

get variably by name

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

Retrieves the set of all variables known to this manager.

class ExpressionParser

Parser for storm-expressions

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

parse

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

sets identifiers

class ExpressionType

The type of an expression

property is_boolean
property is_integer
property is_rational
class FactorizedPolynomial

Represent a polynomial with its factorization

cache(self: pycarl.cln.cln.FactorizedPolynomial) pycarl.cln.cln._FactorizationCache
property coefficient
constant_part(self: pycarl.cln.cln.FactorizedPolynomial) pycarl.cln.cln.Rational
derive(self: pycarl.cln.cln.FactorizedPolynomial, variable: pycarl.core.Variable) pycarl.cln.cln.FactorizedPolynomial

Compute the derivative

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

Get factorization

gather_variables(self: pycarl.cln.cln.FactorizedPolynomial) Set[pycarl.core.Variable]
is_constant(self: pycarl.cln.cln.FactorizedPolynomial) bool
is_one(self: pycarl.cln.cln.FactorizedPolynomial) bool
polynomial(self: pycarl.cln.cln.FactorizedPolynomial) pycarl.cln.cln.Polynomial

Get underlying polynomial

to_smt2(self: pycarl.cln.cln.FactorizedPolynomial) str
class FactorizedRationalFunction

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

constant_part(self: pycarl.cln.cln.FactorizedRationalFunction) pycarl.cln.cln.Rational
property denominator
derive(self: pycarl.cln.cln.FactorizedRationalFunction, variable: pycarl.core.Variable) pycarl.cln.cln.FactorizedRationalFunction

Compute the derivative

evaluate(self: pycarl.cln.cln.FactorizedRationalFunction, arg0: Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]) pycarl.cln.cln.Rational
gather_variables(self: pycarl.cln.cln.FactorizedRationalFunction) Set[pycarl.core.Variable]
is_constant(self: pycarl.cln.cln.FactorizedRationalFunction) bool
property numerator
rational_function(self: pycarl.cln.cln.FactorizedRationalFunction) pycarl.cln.cln.RationalFunction
to_smt2(self: pycarl.cln.cln.FactorizedRationalFunction) str
class FlatSet

Container to pass to program

insert(self: stormpy.core.FlatSet, arg0: int) None
insert_set(self: stormpy.core.FlatSet, arg0: stormpy.core.FlatSet) None
is_subset_of(self: stormpy.core.FlatSet, arg0: stormpy.core.FlatSet) bool
class Formula

Generic Storm Formula

clone(self: stormpy.logic.logic.Formula) stormpy.logic.logic.Formula
property is_bounded_until_formula
property is_eventually_formula
property is_multi_objective_formula
property is_probability_operator

is it a probability operator

property is_reward_operator

is it a reward operator

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

Substitute variables

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

substitute label occurences

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

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

Parameters:
  • row (double) – The row in which the matrix entry is to be set

  • column (double) – The column in which the matrix entry is to be set

  • value (double) – The value that is to be set at the specified row and column

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

Finalize the sparse matrix

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

Get the current row group count

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

the most recently used column

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

Get the most recently used row

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

Start a new row group in the matrix

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

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

Parameters:
  • replacements (std::vector<double> const&) – replacements Mapping indicating the replacements from offset+i -> value of i

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

class IntervalSparseMatrixEntry

Entry of sparse matrix

property column

Column

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

Set value

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

Value

class IntervalSparseMatrixRows

Set of rows in a sparse matrix

class ItemLabeling

Labeling

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

Add label

contains_label(self: stormpy.storage.storage.ItemLabeling, label: str) bool

Check if the given label is contained in the labeling

get_labels(self: stormpy.storage.storage.ItemLabeling) Set[str]

Get all labels

class JaniAssignment

Jani Assignment

property expression
property variable

variable that is assigned to, if any

class JaniAutomaton

A Jani Automation

add_edge(self: stormpy.storage.storage.JaniAutomaton, edge: storm::jani::Edge) None
add_initial_location(self: stormpy.storage.storage.JaniAutomaton, index: int) None
add_location(self: stormpy.storage.storage.JaniAutomaton, location: storm::jani::Location) int

adds a new location, returns the index

property edges

get edges

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

initial state restriction

property location_variable
property locations
property name
property variables
class JaniChoiceOrigins

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

get_edge_index_set(self: stormpy.storage.storage.JaniChoiceOrigins, choice_index: int) stormpy.core.FlatSet

returns the set of edges that induced the choice

property model

retrieves the associated JANI model

class JaniConstant

A Constant in JANI

property defined

is constant defined by some expression

property expression_variable

expression variable for this constant

property name

name of constant

property type

type of constant

class JaniEdge

A Jani Edge

property action_index

action index

property color

color for the edge

property destinations

edge destinations

property guard

edge guard

has_silent_action(self: stormpy.storage.storage.JaniEdge) bool

Is the edge labelled with the silent action

property nr_destinations

nr edge destinations

property rate

edge rate

property source_location_index

index for source location

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

template edge

class JaniEdgeDestination

Destination in Jani

property assignments
property probability
property target_location_index
class JaniInformationObject

An object holding information about a JANI model

property avg_var_domain_size
property model_type
property nr_automata
property nr_edges
property nr_variables
property state_domain_size
class JaniLocation

A Location in JANI

property assignments

location assignments

property name

name of the location

class JaniLocationExpander

A transformer for Jani expanding variables into locations

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

A Jani Model

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

add an automaton (with a unique name)

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

adds constant to model

property automata

get automata

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

Some basic checks to ensure validity

property constants

get constants

static decode_automaton_and_edge_index(arg0: int) Tuple[int, int]

get edge and automaton from edge/automaton index

define_constants(self: stormpy.storage.storage.JaniModel, map: Dict[storm::expressions::Variable, storm::expressions::Expression]) stormpy.storage.storage.JaniModel

define constants with a mapping from the corresponding expression variables to expressions

static encode_automaton_and_edge_index(arg0: int, arg1: int) int

get edge/automaton-index

property expression_manager

get expression manager

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

finalizes the model. After this action, be careful changing the data structure.

flatten_composition(self: stormpy.storage.storage.JaniModel, smt_solver_factory: stormpy.utility.utility.SmtSolverFactory = <stormpy.utility.utility.SmtSolverFactory object at 0x7f04b7896870>) 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>
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>
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.

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

Parameters:
  • row (double) – The row in which the matrix entry is to be set

  • column (double) – The column in which the matrix entry is to be set

  • value (double) – The value that is to be set at the specified row and column

build(self: stormpy.storage.storage.ParametricSparseMatrixBuilder, overridden_row_count: int = 0, overridden_column_count: int = 0, overridden-row_group_count: int = 0) storm::storage::SparseMatrix<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, true> >

Finalize the sparse matrix

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

Get the current row group count

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

the most recently used column

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

Get the most recently used row

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

Start a new row group in the matrix

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

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

Parameters:
  • replacements (std::vector<double> const&) – replacements Mapping indicating the replacements from offset+i -> value of i

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

class ParametricSparseMatrixEntry

Entry of sparse matrix

property column

Column

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

Set value

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

Value

class ParametricSparseMatrixRows

Set of rows in a sparse matrix

class ParetoCurveCheckResultDouble

Result for multiobjective model checking

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

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

class Polynomial

Represent a multivariate polynomial

constant_part(self: pycarl.cln.cln.Polynomial) pycarl.cln.cln.Rational
degree(self: pycarl.cln.cln.Polynomial, arg0: pycarl.core.Variable) int
derive(self: pycarl.cln.cln.Polynomial, variable: pycarl.core.Variable) pycarl.cln.cln.Polynomial

Compute the derivative

evaluate(self: pycarl.cln.cln.Polynomial, arg0: Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]) pycarl.cln.cln.Rational
gather_variables(self: pycarl.cln.cln.Polynomial) Set[pycarl.core.Variable]
is_constant(self: pycarl.cln.cln.Polynomial) bool
property nr_terms
substitute(self: pycarl.cln.cln.Polynomial, arg0: Dict[pycarl.core.Variable, pycarl.cln.cln.Polynomial]) pycarl.cln.cln.Polynomial
to_smt2(self: pycarl.cln.cln.Polynomial) str
property total_degree
class PolytopeDouble
create_downward_closure(self: stormpy.storage.storage.PolytopeDouble) stormpy.storage.storage.PolytopeDouble
get_vertices_clockwise(self: stormpy.storage.storage.PolytopeDouble) List[List[float]]
property vertices
class PolytopeExact
create_downward_closure(self: stormpy.storage.storage.PolytopeExact) stormpy.storage.storage.PolytopeExact
get_vertices_clockwise(self: stormpy.storage.storage.PolytopeExact) List[List[pycarl.gmp.gmp.Rational]]
property vertices
class PrismAssignment

An assignment in prism

property expression

Expression for the update

property variable

Variable that is updated

class PrismBooleanVariable

A program boolean variable in a Prism program

class PrismChoiceOrigins

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

get_command_set(self: stormpy.storage.storage.PrismChoiceOrigins, choice_index: int) stormpy.core.FlatSet

Returns the set of prism commands that induced the choice

property<