Package org.mpi_sws.jmc.runtime

Class JmcRuntimeConfiguration

java.lang.Object

org.mpi_sws.jmc.runtime.JmcRuntimeConfiguration

public class JmcRuntimeConfiguration
extends Object

Represents the configuration for the JMC runtime.

This class encapsulates various settings that control the behavior of the JMC runtime, including scheduling strategies, debugging options, report paths, and retry configurations.

Use the JmcRuntimeConfiguration.Builder to create a configuration instance.

The user does not have to specify this explicitly. The JmcCheckerConfiguration provided is used to create and instance of this class

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	JmcRuntimeConfiguration.Builder

Method Summary

Modifier and Type	Method	Description
Boolean	getDebug()
String	getReportPath()
int	getSchedulerTries()
long	getSchedulerTrySleepTimeNanos()
SchedulingStrategy	getStrategy()

Methods inherited from class java.lang.Object

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

Method Details

getStrategy

public SchedulingStrategy getStrategy()

getDebug

public Boolean getDebug()

getReportPath

public String getReportPath()

getSchedulerTries

public int getSchedulerTries()

getSchedulerTrySleepTimeNanos

public long getSchedulerTrySleepTimeNanos()