Stormpy.utility

class JsonContainerDouble

Storm-internal container for JSON structures

class JsonContainerRational

Storm-internal container for JSON structures

class MatrixFormat(self: stormpy.utility._utility.MatrixFormat, value: SupportsInt)

Members:

Straight

I_Minus_P

I_Minus_P = <MatrixFormat.I_Minus_P: 1>

Straight = <MatrixFormat.Straight: 0>

property name

property value

class ModelReference

Lightweight Wrapper around results

get_boolean_value(self: stormpy.utility._utility.ModelReference, variable: storm::expressions::Variable) → bool

get a value for a boolean variable

get_integer_value(self: stormpy.utility._utility.ModelReference, variable: storm::expressions::Variable) → int

get a value for an integer variable

get_rational_value(self: stormpy.utility._utility.ModelReference, variable: storm::expressions::Variable) → float

get a value (as double) for an rational variable

class Path(*args, **kwargs)

Overloaded function.

1. __init__(self: stormpy.utility._utility.Path, predecessorNode: typing.SupportsInt, predecessorK: typing.SupportsInt, distance: typing.SupportsFloat) -> None

2. __init__(self: stormpy.utility._utility.Path, predecessorK: typing.SupportsInt, distance: typing.SupportsFloat) -> None

property distance

property predecessorK

property predecessorNode

class ShortestPathsGenerator(*args, **kwargs)

Overloaded function.

1. __init__(self: stormpy.utility._utility.ShortestPathsGenerator, model: storm::models::sparse::Model<double, storm::models::sparse::StandardRewardModel<double> >, target_bitvector: storm::storage::BitVector) -> None

2. __init__(self: stormpy.utility._utility.ShortestPathsGenerator, model: storm::models::sparse::Model<double, storm::models::sparse::StandardRewardModel<double> >, target_state: typing.SupportsInt) -> None

3. __init__(self: stormpy.utility._utility.ShortestPathsGenerator, model: storm::models::sparse::Model<double, storm::models::sparse::StandardRewardModel<double> >, target_state_list: collections.abc.Sequence[typing.SupportsInt]) -> None

4. __init__(self: stormpy.utility._utility.ShortestPathsGenerator, model: storm::models::sparse::Model<double, storm::models::sparse::StandardRewardModel<double> >, target_label: str) -> None

5. __init__(self: stormpy.utility._utility.ShortestPathsGenerator, transition_matrix: storm::storage::SparseMatrix<double>, target_prob_vector: collections.abc.Sequence[typing.SupportsFloat], initial_states: storm::storage::BitVector, matrix_format: stormpy.utility._utility.MatrixFormat) -> None

6. __init__(self: stormpy.utility._utility.ShortestPathsGenerator, transition_matrix: storm::storage::SparseMatrix<double>, target_prob_map: collections.abc.Mapping[typing.SupportsInt, typing.SupportsFloat], initial_states: storm::storage::BitVector, matrix_format: stormpy.utility._utility.MatrixFormat) -> None

get_distance(self: stormpy.utility._utility.ShortestPathsGenerator, k: SupportsInt) → float

get_path_as_list(self: stormpy.utility._utility.ShortestPathsGenerator, k: SupportsInt) → list[int]

get_states(self: stormpy.utility._utility.ShortestPathsGenerator, k: SupportsInt) → storm::storage::BitVector

class SmtCheckResult(self: stormpy.utility._utility.SmtCheckResult, value: SupportsInt)

Result type

Members:

Sat

Unsat

Unknown

Sat = <SmtCheckResult.Sat: 0>

Unknown = <SmtCheckResult.Unknown: 2>

Unsat = <SmtCheckResult.Unsat: 1>

property name

property value

class SmtSolver

Generic Storm SmtSolver Wrapper

add(self: stormpy.utility._utility.SmtSolver, arg0: storm::expressions::Expression) → None

addconstraint

check(self: stormpy.utility._utility.SmtSolver) → stormpy.utility._utility.SmtCheckResult

check

property model

get the model

pop(self: stormpy.utility._utility.SmtSolver, levels: SupportsInt) → None

pop

push(self: stormpy.utility._utility.SmtSolver) → None

push

reset(self: stormpy.utility._utility.SmtSolver) → None

reset

class SmtSolverFactory

Factory for creating SMT Solvers

class Z3SmtSolver(self: stormpy.utility._utility.Z3SmtSolver, arg0: storm::expressions::ExpressionManager)

z3 API for storm smtsolver wrapper

class Z3SmtSolverFactory(self: stormpy.utility._utility.Z3SmtSolverFactory)

Factory for creating z3 based SMT solvers

class milliseconds

count(self: stormpy.utility._utility.milliseconds) → int