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: stormpy.storage.storage.Variable) → bool

get a value for a boolean variable

get_integer_value(self: stormpy.utility.utility.ModelReference, variable: stormpy.storage.storage.Variable) → int

get a value for an integer variable

get_rational_value(self: stormpy.utility.utility.ModelReference, variable: stormpy.storage.storage.Variable) → float

get a value (as double) for an rational variable

class Path
distance
predecessorK
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) → stormpy.storage.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: stormpy.storage.storage.Expression) → None

addconstraint

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

check

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 Z3SmtSolver

z3 API for storm smtsolver wrapper

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