engine/io.github.moonlightsuite.moonlight.statistics/StatisticalModelChecker

StatisticalModelChecker

public class StatisticalModelChecker<S, T, R>

The StatisticalModelChecker is a class for evaluating a property over multiple trajectories and determining the probability of satisfying it. TODO: write some tests for the whole package

Parameters

<S>

The Value Type of Spatial Model edges

<T>

The Type of the Domain of the Input Signal

<R>

The Interpretation Type of the monitoring

See also

for info about the stats recorded and

for info about the result format

Constructors

Link copied to clipboard
public void StatisticalModelChecker(SpatialTemporalMonitor<S, T, R> propertyMonitor, Collection<? extends SpatialTemporalSignal<T>> trajectorySamples, LocationService<Double, S> locationService)
Instantiating a Statistical Model Checker requires the following:

Properties

Link copied to clipboard
public final List<SpatialTemporalSignal<R>> results
Output Results

Functions

Link copied to clipboard
public void compute()
This is the actual execution of the statistical model checking, by executing the chosen monitor over the provided samples.
Link copied to clipboard
Link copied to clipboard