Polytope

Warning

The stormpy developer API is internal and can be subject to change.

class Polytope[ValueType]

Polytope

Template arguments:

• ValueType (type)

Available specializations:

• Polytope[float]

• Polytope[stormpy.numbers.Rational]

Construction

The default specialization is Polytope[float].

Members

Polytope.contains()

For Polytope[float]:

1. contains(self: stormpy.developer.storage.Polytope[ValueType], point: collections.abc.Sequence[typing.SupportsFloat | typing.SupportsIndex]) -> bool

Whether the point is contained

2. contains(self: stormpy.developer.storage.Polytope[ValueType], other: stormpy.developer.storage.Polytope[ValueType]) -> bool

Whether the other polytope is contained

For Polytope[stormpy.numbers.Rational]:

1. contains(self: stormpy.developer.storage.Polytope[ValueType], point: collections.abc.Sequence[ValueType]) -> bool

Whether the point is contained

2. contains(self: stormpy.developer.storage.Polytope[ValueType], other: stormpy.developer.storage.Polytope[ValueType]) -> bool

Whether the other polytope is contained

static Polytope.create_downward_closure()

For Polytope[float]:

create_downward_closure(points: collections.abc.Sequence[collections.abc.Sequence[typing.SupportsFloat | typing.SupportsIndex]]) -> stormpy.developer.storage.Polytope[ValueType]

Create the downward closure of the convex hull of the points

For Polytope[stormpy.numbers.Rational]:

create_downward_closure(points: collections.abc.Sequence[collections.abc.Sequence[ValueType]]) -> stormpy.developer.storage.Polytope[ValueType]

Create the downward closure of the convex hull of the points

Polytope.downward_closure(

self: stormpy.developer.storage.Polytope[ValueType],

) → stormpy.developer.storage.Polytope[ValueType]

Polytope.get_vertices_in_clockwise_order(

self: stormpy.developer.storage.Polytope[ValueType],

) → list[list[ValueType]]

property Polytope.halfspaces

Halfspaces whose intersection is the polytope

Polytope.is_empty(self: stormpy.developer.storage.Polytope[ValueType]) → bool

Whether the polytope is empty

Polytope.is_universal(self: stormpy.developer.storage.Polytope[ValueType]) → bool

Whether the polytope is universal, i.e., contains every point

Polytope.optimize()

For Polytope[float]:

optimize(self: stormpy.developer.storage.Polytope[ValueType], direction: collections.abc.Sequence[typing.SupportsFloat | typing.SupportsIndex]) -> tuple[list[ValueType], bool]

Find a point maximizing the dot product with the direction. Returns the point and whether such a point exists (it does not if the polytope is empty or unbounded in the direction)

For Polytope[stormpy.numbers.Rational]:

optimize(self: stormpy.developer.storage.Polytope[ValueType], direction: collections.abc.Sequence[ValueType]) -> tuple[list[ValueType], bool]

Find a point maximizing the dot product with the direction. Returns the point and whether such a point exists (it does not if the polytope is empty or unbounded in the direction)

property Polytope.vertices