Stormpy.utility¶

class JsonContainerDouble¶: Storm-internal container for JSON structures

class JsonContainerRational¶: Storm-internal container for JSON structures

class MatrixFormat¶

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¶

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

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: 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 Z3SmtSolverFactory¶: Factory for creating z3 based SMT solvers

class milliseconds¶

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