Package org.mpi_sws.jmc.strategies.trust

Class MeasureGraphCoverageStrategyConfig

java.lang.Object

org.mpi_sws.jmc.strategies.trust.MeasureGraphCoverageStrategyConfig

public class MeasureGraphCoverageStrategyConfig
extends Object

Configuration class for the MeasureGraphCoverageStrategy.

This class provides a builder pattern to create instances of the configuration with various options such as enabling debug mode, recording graphs, setting the record path, measuring frequency, and whether to record per iteration.

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	MeasureGraphCoverageStrategyConfig.MeasureGraphCoverageStrategyConfigBuilder

Method Summary

Modifier and Type	Method	Description
static MeasureGraphCoverageStrategyConfig.MeasureGraphCoverageStrategyConfigBuilder	builder()
Duration	getMeasuringFrequency()
String	getRecordPath()
boolean	isDebugEnabled()
boolean	isRecordPerIteration()
boolean	shouldRecordGraphs()

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Method Details

isDebugEnabled

public boolean isDebugEnabled()

shouldRecordGraphs

public boolean shouldRecordGraphs()

getRecordPath

public String getRecordPath()

getMeasuringFrequency

public Duration getMeasuringFrequency()

isRecordPerIteration

public boolean isRecordPerIteration()

builder

public static MeasureGraphCoverageStrategyConfig.MeasureGraphCoverageStrategyConfigBuilder builder()