Package org.mpi_sws.jmc.checker

Class JmcModelChecker

java.lang.Object

org.mpi_sws.jmc.checker.JmcModelChecker

public class JmcModelChecker
extends Object

The JmcModelChecker class is responsible for managing the model checking process. It uses a JmcCheckerConfiguration to configure the process and a JmcTestTarget to specify the program under test.

Constructor Summary

Constructors

Constructor	Description
JmcModelChecker(JmcCheckerConfiguration config)	Constructs a new JMC model checker with the given configuration.

Method Summary

Modifier and Type	Method	Description
JmcModelCheckerReport	check(JmcTestTarget target)	Checks the given test target.
void	replay(JmcTestTarget target)	Replays the given test target.

Methods inherited from class java.lang.Object

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

Constructor Details

JmcModelChecker

public JmcModelChecker(JmcCheckerConfiguration config)

Constructs a new JMC model checker with the given configuration.

Parameters:

config - the configuration to use

Method Details

check

public JmcModelCheckerReport check(JmcTestTarget target)
                            throws JmcCheckerException

Checks the given test target. No instrumentation involved.

Parameters:

target - the test target to check

Returns:

the report generated by the model checker

Throws:

JmcCheckerException

replay

public void replay(JmcTestTarget target)
            throws JmcCheckerException

Replays the given test target. The replay is handled by the Strategy

Parameters:

target - the test target to replay

Throws:

JmcCheckerException - if an error occurs during replay