prophesy.regions package

Module contents

Region Checking

prophesy.regions.region_checker module

class RegionCheckResult(value)

Bases: enum.Enum

Result of region check (counterexample, satisfied, refined, homogeneous, unknown).

CounterExample = 0

The region does not satisfy the property; we found a counterexample

Homogenous = 4

All the same color.

Inhomogenous = 5

Contains a border point

Refined = 2

We don’t know, we return a subregion which is still undecided. The remainder is satisfied.

Satisfied = 1

The region satisfies the property.

Splitted = 3

We don’t know, but we found subregions ourselves that are safe/unsafe, and subregions that remain

Unknown = 6

We don’t know.

class RegionChecker

Bases: object

Interface for region checkers.

abstract analyse_region(region, safe)

Analyse the given region and return the result (and a counterexample point if found). :param region: Region as either HyperRectangle or shapely Polygon. :param safe: Boolean to indicate if the region should be considered as safe or unsafe. :return Tuple (RegionCheckResult, counterexample point).

abstract initialize(problem_description, threshold, constants=None)

Initialize region checker. :param problem_description: Data for problem (model, property, solution function). :type problem_description: ProblemDescription. :param threshold: Threshold. :param constants: Constants in model file.

supports_only_closed_regions()

prophesy.regions.region_smtchecker module

class Context(smt_context, fd)

Bases: object

class SmtRegionChecker(backend)

Bases: prophesy.regions.region_checker.RegionChecker

analyse_region(polygon, safe, check_for_eq)

Extends the current area by using the new polygon regions are the newly added regions for the polygon polygon marks the new area to cover safe indicates whether the area is safe or bad returns tuple (valid constraint, polygon/counterexample point) if constraint is valid the tuple is (True, polygon added) if constraint is invalid the tuple is (False, point as counterexample)

Parameters

• polygon – either HyperRectangle or shapely Polygon

• safe – Boolean to indicate if the region should be considered as safe or unsafe

property encoding_timer

abstract initialize(problem_description, threshold, constants=None)

Initialize region checker. :param problem_description: Data for problem (model, property, solution function). :type problem_description: ProblemDescription. :param threshold: Threshold. :param constants: Constants in model file.

abstract over_approximates()

property solver_timer

Region Generation

prophesy.regions.region_generation module

class GenerationRecord

Bases: object

property analysis_time

property area

property bad_regions

property covered_area

property covered_safe_area

property generation_time

property iteration_time

property region

property result

property safe

property safe_area

property safe_regions

set_region(region, safe)

set_regions(safe, bad)

set_result(result)

start_analysis_timer()

start_generation_timer()

start_iteration_timer()

stop_analysis_timer()

stop_generation_timer()

stop_iteration_timer()

class RegionGenerator(samples, parameters, region, threshold, checker, wd_constraints, gp_constraints, generate_plot=True, allow_homogeneity=False)

Bases: object

A generator for regions. This class acts as an iterable that generates new regions (or counterexamples), until the search space is exhausted (which possibly never happens).

abstract accept_region()

Called after a region is accepted.

export_results(path)

export_stats(filename, update=False)

abstract fail_region(homogeneity=False)

Called after a region could not be checked, usually due to memout or timeout. Updates the current set of regions.

generate_constraints(max_iter=- 1, max_area=1, plot_every_n=1, plot_candidates=True, export_statistics=None)

Iteratively generate new regions, heuristically, attempting to find the largest safe or unsafe area. :param max_iter: Number of regions to generate/check at most (not counting SMT failures), -1 for unbounded :param max_area: Maximal area percentage that should be covered. :param plot_every_n: How often should the plot be appended to the PDF. :param plot_candidates: True, iff candidates should be plotted. :return Tuple (safe regions, unsafe regions, samples)

generate_header()

generate_stats(update=False)

abstract ignore_region()

Called for a region which is overall ill-defined. Skip it.

abstract next_region()

Generate a new region. :return Tuple (new region, well-definedness, safe/unsafe) or None if no next region exists.

abstract plot_candidate()

Plot the current candidate.

plot_results(*args, **kwargs)

Plot results. :param args: Arguments. :param kwargs: Arguments.

record_accepted(region, safe)

Record the accepted region.

Returns

record_border(region, additional)

record_cex(region, safe, additional)

Parameters

additional – An additional sample.

Returns

record_contains_border(region, safe)

record_illdefined(region)

record_results(safe_regions, bad_regions)

record_unknown(region, safe)

abstract reject_region(sample)

Called after a region is rejected (sample found). :param sample: Sample acting as a counterexample for the constraint.

start_analysis()

start_generation()

start_iteration()

stop_analysis()

stop_generation()

stop_iteration()

prophesy.regions.region_quads module

class HyperRectangleRegions(samples, parameters, region, threshold, checker, wd_constraints, gp_constraints, split_uniformly=False, generate_plots=False, allow_homogeneity=False, sampler=None)

Bases: prophesy.regions.region_generation.RegionGenerator

Region generation using hyperrectangles.

accept_region()

Called after a region is accepted.

check_region(region, depth=0)

Check if the given region can be assumed safe or bad based on known samples. If samples are mixed, split the region and retry. Resulting regions are added to self.regions. :param region: Region. :param depth: Maximal depth for region refining.

fail_region(homogeneity=False)

Called after a region could not be checked, usually due to memout or timeout. Updates the current set of regions.

ignore_region()

Called for a region which is overall ill-defined. Skip it.

next_region()

Generate a new region. :return Tuple (new region, well-definedness, safe/unsafe) or None if no next region exists.

plot_candidate()

Plot the current candidate.

refine_region(new_regions)

If a region could not be checked, but we know that only a region has to be checked afterwards.

reject_region(sample)

Called after a region is rejected (sample found). :param sample: Sample acting as a counterexample for the constraint.

static split_by_growing_rectangles(region)

Split the region according to growing rectangles. :param region: Region. :return: New regions after splitting.

static split_uniformly_in_every_dimension(region)

Split the region uniformly in every region. :param region: Region. :return: New regions after splitting.