Stormpy.utility

class MatrixFormat
I_Minus_P = MatrixFormat.I_Minus_P
Straight = MatrixFormat.Straight
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
property distance
property predecessorK
property predecessorNode
class ShortestPathsGenerator
get_distance(self: stormpy.utility.utility.ShortestPathsGenerator, k: int) float
get_path_as_list(self: stormpy.utility.utility.ShortestPathsGenerator, k: int) List[int]
get_states(self: stormpy.utility.utility.ShortestPathsGenerator, k: int) storm::storage::BitVector
class SmtCheckResult

Result type

Sat = SmtCheckResult.Sat
Unknown = SmtCheckResult.Unknown
Unsat = SmtCheckResult.Unsat
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: int) 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

z3 API for storm smtsolver wrapper

class milliseconds
count(self: stormpy.utility.utility.milliseconds) int