prophesy.data package¶

Submodules¶

prophesy.data.constant module¶

class Constants(*args, **kwargs)¶

Bases: dict

Container that holds constants for a model.

to_key_value_string(to_float=False)¶

Provides a key-value string from variable to constant value.

The key-value string format can be immediately used for storm or prism.

Parameters: to_float – Should the constant value be casted into a float
Returns: A string of the format var1=val1,…,varn=valn

parse_constants_string(input_string)¶

Parses a key-value string

Parameters: input_string –
Returns

prophesy.data.constraint module¶

region_from_polygon(polygon, variables)¶

Compute formula representing polygon (Polygon, LineString or LinearRing).

Area will be considered at the rhs (ccw) of line segments.

Parameters: polygon – Polygon, LineString or LinearRing, must be convex
Returns: Formula s.t. points in polygon are satisfied.
Return type: pycarl.Formula or pycarl.Constraint

prophesy.data.hyperrectangle module¶

class HyperRectangle(*intervals)¶

Bases: object

Defines a hyper-rectangle, that is the Cartisean product of intervals, i.e. the n-dimensional variant of a box.

center()¶

close()¶

contains(point)¶

Parameters: point – A Point
Returns: True if inside, False otherwise

classmethod cube(left_bound, right_bound, dimension, boundtype)¶

Parameters

left_bound – lower bound for all intervals
right_bound – upper bound for all intervals
dimension – dimension of the created interval
boundtype – bound type for all bounds

Returns

A hyperrectangle <left_bound, right_bound>^dimension (with adequate bounds)

dimension()¶

empty()¶

classmethod from_extremal_points(point1, point2, boundtype)¶: Construct a hyperrectangle from two boundary points. :param point1: The first point. :param point2: The second point. :param boundtype: BoundType to use as bounds for the resulting HyperRectangle. :return: HyperRectangle.

classmethod from_region_string(input_string, variables)¶

Constructs a hyperrectangle with dimensions according to the variable order.

Returns: A HyperRectangle

get_vertex(pick_min_bound)¶: Get the vertex that corresponds to the left/right bound for the ith parameter, depending on the argument :param pick_min_bound: Array indicating to take the min (True) or the max (False) :return:

intersect(other)¶: Computes the intersection :return:

is_closed()¶: Checks whether the hyperrectangle is closed in every dimension. :return: True iff all intervals are closed.

non_empty_intersection(other)¶

Returns

setminus(other, dimension=0)¶: Does a setminus operation on hyperrectangles and returns a list with hyperrects covering the resulting area :param other: the other HyperRectangle :param dimension: dimension where to start the operation :return: a list of HyperRectangles

size()¶

Returns: The size of the hyperrectangle

split_in_every_dimension()¶

Splits the hyperrectangle in every dimension

Returns: The 2^n many hyperrectangles obtained by the split

split_in_single_dimension(dimension)¶

to_formula(variables)¶

Given list of variables, compute constraints

Parameters: variables – Variables for each dimension
Returns: A formula specifying the points inside the hyperrectangle
Return type: pc.Constraint or pc.Formula

to_region_string(variables)¶: Constructs a region string, as e.g. used by storm-pars :param variables: An ordered list of the variables :type variables: List[pycarl.Variable] :return:

vertices()¶

prophesy.data.interval module¶

class BoundType(value)¶

Bases: enum.Enum

An enumeration.

closed = 1¶

negated()¶

open = 0¶

class Interval(left_value, left_bt, right_value, right_bt)¶

Bases: object

Interval class for arbitrary (constant) types. Construction from string is possible via string_to_interval

center()¶

Gets the center of the interval.

Returns

close()¶

Create an interval with all bounds closed. Can not be called on unbounded intervals

Returns: A new interval which has closed bounds instead.

contains(pt)¶

Does the interval contain a specific point

Parameters: pt – A value
Returns: True if the value lies between the bounds.

empty()¶

Does the interval contain any points.

Returns: True, iff there exists a point in the interval.

intersect(other)¶

Compute intersection between to intervals

Parameters: other –
Returns

is_bounded()¶

Checks whether the interval is bounded

Returns: The interval is bounded, if both the left and the right bound are not equal to infinity.

is_closed()¶

Does the interval have closed bounds on both sides.

Returns: True iff both bounds are closed.

left_bound()¶

left_bound_type()¶

open()¶

Create an interval with all bounds open.

Returns: A new interval which has open bounds instead

right_bound()¶

right_bound_type()¶

setminus(other)¶

Compute the setminus of two rectangles

Parameters: other –
Returns

split()¶

Split the interval in two equally large halfs. Can only be called on bounded intervals

Returns: Two intervals, the first from the former left bound to (excluding) middle point (leftbound + rightbound)/2, the second from the middle point (including) till the former right bound

width()¶

The width of the interval

Returns: right bound - left bound, if bounded from both sides, and math.inf otherwise

constraint_to_interval(input, internal_parse_func)¶

create_embedded_closed_interval(interval, epsilon)¶

For an (half) open interval from l to r, create a closed interval [l+eps, r-eps].

Parameters

interval – The interval which goes into the method
epsilon – An epsilon offset used to close.

Returns

A closed interval.

string_to_interval(input_str, internal_parse_func)¶

Parsing intervals

Parameters

input_str – A string of the form [l,r] or (l,r) or the like.
internal_parse_func – the function to parse l and r, in case they are not -infty or infty, respectively

Returns

An interval

prophesy.data.model_type module¶

class ModelType(value)¶

Bases: enum.Enum

The type of a Markovian model.

CTMC = 2¶

DTMC = 0¶

MA = 3¶

MDP = 1¶

is_continuous_time()¶: Checks whether the model type is continuous-time :param model_type: :return:

model_is_nondeterministic(model_type)¶: Checks whether the model type is non-deterministic. :param model_type: :return: True, if the model type encodes a model with potential non-determinism.

prophesy.data.nice_approximation module¶

class FixedDenomFloatApproximation(denom)¶

Bases: object

find(input)¶

prophesy.data.parameter module¶

class Monotonicity(value)¶

Bases: enum.Enum

An enumeration.

NEGATIVE = 0¶

NEITHER = 2¶

POSITIVE = 1¶

UNKNOWN = 3¶

class Parameter(variable, interval)¶

Bases: pycarl.core.Variable

Variable with an associated interval of allowable values.

class ParameterOrder(iterable=(), /)¶

Bases: list

Class to represent on ordered list of parameters.

get_parameter(name)¶: Return the parameter with the given name.

get_parameter_bounds()¶

Computes a list of bounds ordered according to this ParameterOrder.

Returns: list of Interval
Return type: list(Interval)

instantiate(one_or_more_pointlikes)¶

Create ParameterInstantiation(s) from point-like objects.

Returns the same shape as the input, i.e., if the input is a single point-like object (i.e., iterable, hopefully of numbers), returns a single ParameterInstantiation; for a list of points, returns a list of ParameterInstantiations.

make_intervals_closed(epsilon)¶

For several applications, we want to have an embedded closed interval

Parameters: epsilon – How far from an open bound should the embedded interval-bound be away

make_intervals_open()¶

remove_parameter(parameter)¶: Remove parameter represented by a given variable.

update_variables(variables)¶

prophesy.data.point module¶

class Point(*args)¶

Bases: object

An n-dimensional point class.

dimension()¶

The dimension of the point, e.g. the number of coordinates

Returns: The number of entries

distance(other)¶

Computes the (Euclidean) distance between this point and another point

Parameters: other (Point) – Another n-dimensional point
Returns: The Euclidean distance

numerical_distance(other)¶

Computes the (Euclidean) distance between this point and another point, using floating point arithmetic

Parameters: other (Point) – Another n-dimensional point
Returns

projection(dims)¶

Project the point onto the selected dimensions

Parameters: dims – An iterable of dimensions to select
Returns: A len(dims)-dimensional Point

to_float()¶

to_nice_rationals(ApproxType=<class 'prophesy.data.nice_approximation.FixedDenomFloatApproximation'>, approx_type_arg=16384)¶

Transfer the coordinates into rational numbers with smaller coefficients

Parameters

ApproxType – The type of approximation to use
approx_type_arg – An argument for the approximation, typically some sort of precision of the approximation

Returns

A point with slightly modified coordinates

Return type

Point

prophesy.data.property module¶

class Point(*args)¶

Bases: object

An n-dimensional point class.

dimension()¶

The dimension of the point, e.g. the number of coordinates

Returns: The number of entries

distance(other)¶

Computes the (Euclidean) distance between this point and another point

Parameters: other (Point) – Another n-dimensional point
Returns: The Euclidean distance

numerical_distance(other)¶

Computes the (Euclidean) distance between this point and another point, using floating point arithmetic

Parameters: other (Point) – Another n-dimensional point
Returns

projection(dims)¶

Project the point onto the selected dimensions

Parameters: dims – An iterable of dimensions to select
Returns: A len(dims)-dimensional Point

to_float()¶

to_nice_rationals(ApproxType=<class 'prophesy.data.nice_approximation.FixedDenomFloatApproximation'>, approx_type_arg=16384)¶

Transfer the coordinates into rational numbers with smaller coefficients

Parameters

ApproxType – The type of approximation to use
approx_type_arg – An argument for the approximation, typically some sort of precision of the approximation

Returns

A point with slightly modified coordinates

Return type

Point

prophesy.data.range module¶

class Range(lower_bound, upper_bound, step_size)¶

Bases: object

A container similar to the Python native range construct, consisting of a lower bound, an upper bound and a step size

values()¶

Returns: A list with all values encoded by the range

create_cartesian_product(ranges)¶

Parameters: ranges – Iterable containing Range elements
Returns: An iterator for the Cartesian product of the ranges.

create_range_from_interval(interval, nr_samples, epsilon=0)¶: Given closed interval [l,h], generate a Range with nr_sample steps in this interval

prophesy.data.samples module¶

class InexactInstantiationResult(rel, threshold)¶: Bases: object

class InexactRelation(value)¶

Bases: enum.Enum

An enumeration.

GEQ = 2¶

GREATER = 3¶

LEQ = 1¶

LESS = 0¶

class InstantiationResult(instantiation, result)¶

Bases: object

Class to represent a single sample. Maps a point (tuple of pycarl.Rational) to a value (pycarl.Rational).

classmethod from_point(pt, res, parameters)¶

Parameters

pt –
res –
parameters –

Returns

get_instantiation_point(parameters)¶

Parameters: variable_order –
Returns

get_parameters()¶

Returns

property well_defined¶

class InstantiationResultDict(*args, parameters=None)¶

Bases: dict

Maintains a set of instantiations with their results.

copy() → a shallow copy of D¶

split(threshold)¶: Split given samples into separated sample dictionaries, where the value is either >= or < threshold or ill-defined.

class InstantiationResultFlag(value)¶

Bases: enum.Enum

An enumeration.

NOT_WELLDEFINED = 0¶

class ParameterInstantiation(*args, **kwargs)¶

Bases: dict

Simple dictionary mapping from a Parameter to pycarl.Rational.

distance(other)¶

Distance between two instantiations over the same parameters (in the same order)

Parameters: other –
Returns: The distance

classmethod from_point(pt, parameters)¶

Construct ParameterInstantiation from Point and ParameterOrder

Parameters

pt – Point of pycarl.Rational
parameters – ParameterOrder

get_parameters()¶

get_point(parameters)¶: Return the Point corresponding to this sample, given variable ordering provided as argument :param parameters: Must correspond to parameters of this sample point. :type parameters: Iterable[Parameter]

numerical_distance(other)¶

to_formula()¶

Given list of variables, compute constraints

Parameters: variables – Variables for each dimension
Returns: A formula specifying the points inside the hyperrectangle
Return type: pc.Constraint or pc.Formula

weighed_interpolation(sample1, sample2, threshold, fudge=0.0)¶

Interpolates between sample sample1 and sample2 to result in a point estimated close to the given threshold (by linear interpolation). Fudge allows to offset this point slightly either positively or negatively.

Parameters

sample1 – Sample
sample2 – Sample
threshold (pycarl.Rational) – The value we are interested in
fudge (float) – Fraction of distance betwen both samples to fudge around

Returns

tuple of pycarl.Rational if interpolated point, or None if the values are too close