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