Package org.mpi_sws.jmc.integrations.junit5.engine

Class JmcTestExecutor

java.lang.Object

org.mpi_sws.jmc.integrations.junit5.engine.JmcTestExecutor

public class JmcTestExecutor
extends Object

Executes a JMC test method using the JMC Model Checker.

This class provides methods to execute a test method and check its behavior using the JMC Model Checker. It can also replay the test method to verify its behavior against previously recorded traces.

Constructor Summary

Constructors

Constructor	Description
JmcTestExecutor()

Method Summary

Modifier and Type	Method	Description
static JmcModelCheckerReport	execute(Method testMethod, Object instance, JmcCheckerConfiguration config)	Executes a JMC test method and returns the report generated by the model checker.
static void	executeReplay(Method testMethod, Object instance, JmcCheckerConfiguration config)	Replays a previously executed JMC test method to verify its behavior against recorded traces.

Methods inherited from class java.lang.Object

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

Constructor Details

JmcTestExecutor

public JmcTestExecutor()

Method Details

execute

public static JmcModelCheckerReport execute(Method testMethod,
 Object instance,
 JmcCheckerConfiguration config)
                                     throws JmcCheckerException

Executes a JMC test method and returns the report generated by the model checker.

Parameters:

testMethod - The test method to execute.

instance - The instance of the class containing the test method.

config - The configuration for the JMC checker.

Returns:

A report containing the results of the model checking process.

Throws:

JmcCheckerException - If an error occurs during model checking.

executeReplay

public static void executeReplay(Method testMethod,
 Object instance,
 JmcCheckerConfiguration config)
                          throws JmcCheckerException

Replays a previously executed JMC test method to verify its behavior against recorded traces.

Parameters:

testMethod - The test method to replay.

instance - The instance of the class containing the test method.

config - The configuration for the JMC checker.

Throws:

JmcCheckerException - If an error occurs during replaying the test method.