Stormpy.core

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

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)

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 DistributionDouble

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(self: stormpy.storage.storage.ExactSparseMatrix, row_start: int, row_end: int) storm::storage::SparseMatrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >::rows

Get rows from start to end

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: Optional[List[float]]) 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::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true>, storm::models::sparse::StandardRewardModel<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true> > >

Build the model

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

Export a lookup model

class ExplicitParametricQuantitativeCheckResult

Explicit parametric quantitative model checking result

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

Get result for given state

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

Get model checking result values for all states

property scheduler

get scheduler

class ExplicitParetoCurveCheckResultDouble

Result for explicit multiobjective model checking

class ExplicitQualitativeCheckResult

Explicit qualitative model checking result

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

Get result for given state

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

Get BitVector representing the truth values

class ExplicitQuantitativeCheckResult

Explicit quantitative model checking result

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

Get result for given state

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

Get model checking result values for all states

property scheduler

get scheduler

class ExplicitStateLookup

Lookup model for states

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

Holds an expression

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

The arity of the expression

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

Check if the expression contains any of the given variables.

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

Check if the expression contains variables.

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

Get the boolean value this expression evaluates to

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

Get the double value this expression evaluates to

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

Get the integer value this expression evaluates to

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

Get the rational number this expression evaluates to

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

Get the operand at the given index

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

Get the variables

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

Check if the expression is a boolean

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

Check if the expression is an integer

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

Check if the expression is a rational

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

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

property is_function_application

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

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

Check if the expression is a literal

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

Check if the expression is a variable

property manager

Get the manager

property operator

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

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

Simplify expression

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

Get the Type

class ExpressionManager

Manages variables for expressions

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

Create expression from boolean

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

create Boolean variable

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

Create expression from integer number

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

create Integer variable

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

Create expression from rational number

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

create Rational variable

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

get variably by name

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

Retrieves the set of all variables known to this manager.

class ExpressionParser

Parser for storm-expressions

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

parse

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

sets identifiers

class ExpressionType

The type of an expression

property is_boolean
property is_integer
property is_rational
class FactorizedPolynomial

Represent a polynomial with its factorization

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

Compute the derivative

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

Get factorization

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

Get underlying polynomial

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

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

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

Compute the derivative

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

Container to pass to program

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

Generic Storm Formula

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

is it a probability operator

property is_reward_operator

is it a reward operator

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

Substitute variables

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

substitute label occurences

class GloballyFormula

Formula for globally

class HybridExactQuantitativeCheckResult

Symbolic exact hybrid quantitative model checking result

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

Get model checking result values for all states

class HybridParametricQuantitativeCheckResult

Symbolic parametric hybrid quantitative model checking result

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

Get model checking result values for all states

class HybridQuantitativeCheckResult

Hybrid quantitative model checking result

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

Get model checking result values for all states

class InstantaneousRewardFormula

Instantaneous reward

class ItemLabeling

Labeling

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

Add label

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

Check if the given label is contained in the labeling

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

Get all labels

class JaniAssignment

Jani Assignment

property expression
property variable

variable that is assigned to, if any

class JaniAutomaton

A Jani Automation

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

adds a new location, returns the index

property edges

get edges

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

initial state restriction

property location_variable
property locations
property name
property variables
class JaniChoiceOrigins

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

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

returns the set of edges that induced the choice

property model

retrieves the associated JANI model

class JaniConstant

A Constant in JANI

property defined

is constant defined by some expression

property expression_variable

expression variable for this constant

property name

name of constant

property type

type of constant

class JaniEdge

A Jani Edge

property action_index

action index

property color

color for the edge

property destinations

edge destinations

property guard

edge guard

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

Is the edge labelled with the silent action

property nr_destinations

nr edge destinations

property rate

edge rate

property source_location_index

index for source location

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

template edge

class JaniEdgeDestination

Destination in Jani

property assignments
property probability
property target_location_index
class JaniInformationObject

An object holding information about a JANI model

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

A Location in JANI

property assignments

location assignments

property name

name of the location

class JaniLocationExpander

A transformer for Jani expanding variables into locations

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

A Jani Model

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

add an automaton (with a unique name)

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

adds constant to model

property automata

get automata

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

Some basic checks to ensure validity

property constants

get constants

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

get edge and automaton from edge/automaton index

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

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

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

get edge/automaton-index

property expression_manager

get expression manager

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

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

flatten_composition(self: stormpy.storage.storage.JaniModel, smt_solver_factory: stormpy.utility.utility.SmtSolverFactory = <stormpy.utility.utility.SmtSolverFactory object at 0x7f383d232ef0>) stormpy.storage.storage.JaniModel
get_automaton(self: stormpy.storage.storage.JaniModel, name: str) storm::jani::Automaton
get_automaton_index(self: stormpy.storage.storage.JaniModel, name: str) int

get index for automaton name

get_constant(self: stormpy.storage.storage.JaniModel, name: str) storm::jani::Constant

get constant by name

property global_variables
has_standard_composition(self: stormpy.storage.storage.JaniModel) bool

is the composition the standard composition

property has_undefined_constants

Flag if program has undefined constants

property initial_states_restriction

initial states restriction

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

make standard JANI compliant

property model_type

Model type

property name

model name

remove_constant(self: stormpy.storage.storage.JaniModel, constant_name: str) None

remove a constant. Make sure the constant does not appear in the model.

replace_automaton(self: stormpy.storage.storage.JaniModel, index: int, new_automaton: storm::jani::Automaton) None

replace automaton at index

restrict_edges(self: stormpy.storage.storage.JaniModel, edge_set: stormpy.core.FlatSet) stormpy.storage.storage.JaniModel

restrict model to edges given by set

set_model_type(self: stormpy.storage.storage.JaniModel, arg0: stormpy.core.JaniModelType) None

Sets (only) the model type

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

sets the composition to the standard composition

substitute_constants(self: stormpy.storage.storage.JaniModel) stormpy.storage.storage.JaniModel

substitute constants

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

substitute functions

to_dot(self: stormpy.storage.storage.JaniModel) str
property undefined_constants_are_graph_preserving

Flag if the undefined constants do not change the graph structure

class JaniModelType

Type of the Jani model

Members:

DTMC

CTMC

MDP

CTMDP

MA

LTS

TA

PTA

STA

HA

PHA

SHA

UNDEFINED

CTMC = <JaniModelType.CTMC: 3>
CTMDP = <JaniModelType.CTMDP: 5>
DTMC = <JaniModelType.DTMC: 2>
HA = <JaniModelType.HA: 10>
LTS = <JaniModelType.LTS: 1>
MA = <JaniModelType.MA: 6>
MDP = <JaniModelType.MDP: 4>
PHA = <JaniModelType.PHA: 11>
PTA = <JaniModelType.PTA: 8>
SHA = <JaniModelType.SHA: 12>
STA = <JaniModelType.STA: 9>
TA = <JaniModelType.TA: 7>
UNDEFINED = <JaniModelType.UNDEFINED: 0>
property name
property value
class JaniOrderedAssignments

Set of assignments

add(self: stormpy.storage.storage.JaniOrderedAssignments, new_assignment: storm::jani::Assignment, add_to_existing: bool = False) bool
clone(self: stormpy.storage.storage.JaniOrderedAssignments) stormpy.storage.storage.JaniOrderedAssignments

clone assignments (performs a deep copy)

substitute(self: stormpy.storage.storage.JaniOrderedAssignments, substitution_map: Dict[storm::expressions::Variable, storm::expressions::Expression]) None

substitute in rhs according to given substitution map

class JaniScopeChanger

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

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

Template edge, internal data structure for edges

add_destination(self: stormpy.storage.storage.JaniTemplateEdge, arg0: storm::jani::TemplateEdgeDestination) None
property assignments
property destinations
property guard
class JaniTemplateEdgeDestination

Template edge destination, internal data structure for edge destinations

property assignments
class JaniVariable

A Variable in JANI

property expression_variable

expression variable for this variable

property init_expression
property name

name of constant

class JaniVariableSet

Jani Set of Variables

add_variable(self: stormpy.storage.storage.JaniVariableSet, arg0: storm::jani::Variable) None
empty(self: stormpy.storage.storage.JaniVariableSet) bool

is there a variable in the set?

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

variable

get_variable_by_expr_variable(self: stormpy.storage.storage.JaniVariableSet, arg0: storm::expressions::Variable) storm::jani::Variable
get_variable_by_name(self: stormpy.storage.storage.JaniVariableSet, arg0: str) storm::jani::Variable
class LongRunAvarageOperator

Long run average operator

class LongRunAverageRewardFormula

Long run average reward

class MaximalEndComponent

Maximal end component

property size

Number of states in MEC

class MaximalEndComponentDecomposition_double

Decomposition of maximal end components

property size

Number of MECs in the decomposition

class MaximalEndComponentDecomposition_exact

Decomposition of maximal end components

property size

Number of MECs in the decomposition

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

topological_cuda

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>
topological_cuda = <MinMaxMethod.topological_cuda: 8>
property value
value_iteration = <MinMaxMethod.value_iteration: 0>
class MinMaxSolverEnvironment

Environment for Min-Max-Solvers

property method
property precision
class ModelCheckerHint

Information that may accelerate the model checking process

class ModelFormulasPair

Pair of model and formulas

property formulas

The formulas

property model

The model

class ModelType

Type of the model

Members:

DTMC

MDP

POMDP

CTMC

MA

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

Multi objective formula

property nr_subformulas

Get number of subformulas

property subformulas

Get vector of subformulas

class NativeLinearEquationSolverMethod

Method for linear equation systems with the native solver

Members:

power_iteration

sound_value_iteration

optimistic_value_iteration

interval_iteration

rational_search

jacobi

SOR

gauss_seidel

walker_chae

SOR = <NativeLinearEquationSolverMethod.SOR: 2>
gauss_seidel = <NativeLinearEquationSolverMethod.gauss_seidel: 1>
interval_iteration = <NativeLinearEquationSolverMethod.interval_iteration: 7>
jacobi = <NativeLinearEquationSolverMethod.jacobi: 0>
property name
optimistic_value_iteration = <NativeLinearEquationSolverMethod.optimistic_value_iteration: 6>
power_iteration = <NativeLinearEquationSolverMethod.power_iteration: 4>
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: 21>
Divide = <OperatorType.Divide: 8>
Equal = <OperatorType.Equal: 13>
Floor = <OperatorType.Floor: 20>
Greater = <OperatorType.Greater: 17>
GreaterOrEqual = <OperatorType.GreaterOrEqual: 18>
Iff = <OperatorType.Iff: 4>
Implies = <OperatorType.Implies: 3>
Ite = <OperatorType.Ite: 22>
Less = <OperatorType.Less: 15>
LessOrEqual = <OperatorType.LessOrEqual: 16>
Max = <OperatorType.Max: 10>
Min = <OperatorType.Min: 9>
Minus = <OperatorType.Minus: 6>
Modulo = <OperatorType.Modulo: 12>
Not = <OperatorType.Not: 19>
NotEqual = <OperatorType.NotEqual: 14>
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::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true> >::rows

Get row

get_row_group_end(self: stormpy.storage.storage.ParametricSparseMatrix, arg0: int) int
get_row_group_start(self: stormpy.storage.storage.ParametricSparseMatrix, arg0: int) int
get_rows(self: stormpy.storage.storage.ParametricSparseMatrix, row_start: int, row_end: int) storm::storage::SparseMatrix<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true> >::rows

Get rows from start to end

property has_trivial_row_grouping

Trivial row grouping

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::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true> >

Finalize the sparse matrix

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

Get the current row group count

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

the most recently used column

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

Get the most recently used row

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

Start a new row group in the matrix

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

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

Parameters:
  • 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 0x7f383d2374b0>) 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

property hasUndefinedConstants

Does the program have undefined constants?

has_constant(self: stormpy.storage.storage.PrismProgram, name: str) bool
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 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

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

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 SchedulerChoiceDouble

A choice of a finite memory scheduler

property defined

Is the choice defined by the scheduler?

property deterministic

Is the choice deterministic (given by a Dirac distribution)?

get_choice(self: stormpy.storage.storage.SchedulerChoiceDouble) storm::storage::Distribution<double, unsigned long>

Get the distribution over the actions

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

Get the deterministic choice

class 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 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::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true>, unsigned long>

Get the distribution over the actions

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

Get the deterministic choice

class SchedulerDouble

A Finite Memory Scheduler

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

Construct the scheduler with double value type

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

Construct the scheduler with exact value type

cast_to_parametric_datatype(self: stormpy.storage.storage.SchedulerDouble) storm::storage::Scheduler<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true> >

Construct the scheduler with parametric value type

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

Is the scheduler deterministic?

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

How much memory does the scheduler take?

property memoryless

Is the scheduler memoryless?

property partial

Is the scheduler partial?

to_json_str(self: stormpy.storage.storage.SchedulerDouble, model: stormpy.storage.storage._SparseModel, skip_unique_choices: bool = False, skip_dont_care_states: bool = False) str
class SchedulerExact

A Finite Memory Scheduler