Class SamplingResults

• Defined in File sampling_results.hpp

Class Documentation

class SamplingResults

Public Functions

SamplingResults() = delete

explicit SamplingResults(const settings::SmcSettings &settings, const state_properties::PropertyType &prop)

Initialize a SamplingResults object.

Parameters:

• settings – The settings object containing the configuration for the MC task

• prop – Whether we are evaluating a probability or a reward property

inline const size_t &getBatchSize() const

Get the batch_size configured in the constructor.

Returns:

A const reference to the batch_size member variable

BatchResults getBatchResultInstance() const

void addBatchResults(const BatchResults &res, const size_t thread_id)

Add the results from a batch to the Buffer. If all threads reported results, process the data.

Parameters:

• res – Collection of results from a single batch. It is expected to be reset afterwards!

• thread_id – The id of the thread that generated the results

size_t getResultCount(const TraceResult res) const

Get the amount of samples that returned the requested result.

Parameters:

res – The result value we are looking for

Returns:

The n. of times we got the requested result.

double getEstimatedReward() const

Compute the estimated reward from the sampled trajectories.

Returns:

The estimated reward as average of sampled rewards

double getProbabilityVerifiedProperty() const

Compute the probability that a specific property is verified.

Returns:

Prob. that a property is verified as n. of verified samples over the n. of samples

bool newBatchNeeded(const size_t thread_id) const

Check if we need to sample another batch of results. Blocks computation if the related buffer is full.

Parameters:

thread_id – The id of the thread that is checking if a new batch is needed

Returns:

Whether we need to sample a new batch or not.

void printResults() const

Print the Sampling results to std::out stream.