Package org.mpi_sws.jmc.integrations.junit5.descriptors

Class JmcMethodTestDescriptor

java.lang.Object
org.junit.platform.engine.support.descriptor.AbstractTestDescriptor
org.mpi_sws.jmc.integrations.junit5.descriptors.JmcMethodTestDescriptor
All Implemented Interfaces:
org.junit.platform.engine.TestDescriptor, JmcExecutableTestDescriptor
public class JmcMethodTestDescriptor extends org.junit.platform.engine.support.descriptor.AbstractTestDescriptor implements JmcExecutableTestDescriptor
A JUnit 5 test descriptor for a JMC method test.

This descriptor represents a single test method annotated with JMC annotations, allowing for the execution of JMC checks as part of the test lifecycle.

  • Nested Class Summary

    Nested classes/interfaces inherited from interface org.junit.platform.engine.TestDescriptor

    org.junit.platform.engine.TestDescriptor.Type, org.junit.platform.engine.TestDescriptor.Visitor

  • Field Summary

    Fields inherited from class org.junit.platform.engine.support.descriptor.AbstractTestDescriptor

    children

  • Constructor Summary

    Constructors
    Constructor
    Description
    JmcMethodTestDescriptor(Method testMethod, JmcClassTestDescriptor parent)
     

  • Method Summary

    Modifier and Type
    Method
    Description
    void
    execute()
    Executes the JMC test method.
    org.junit.platform.engine.TestDescriptor.Type
    getType()
     

    Methods inherited from class org.junit.platform.engine.support.descriptor.AbstractTestDescriptor

    addChild, equals, findByUniqueId, getChildren, getDisplayName, getParent, getSource, getTags, getUniqueId, hashCode, removeChild, removeFromHierarchy, setParent, toString

    Methods inherited from class java.lang.Object

    clone, finalize, getClass, notify, notifyAll, wait, wait, wait

    Methods inherited from interface org.junit.platform.engine.TestDescriptor

    accept, getAncestors, getDescendants, getLegacyReportingName, isContainer, isRoot, isTest, mayRegisterTests, prune

  • Constructor Details

  • Method Details

    • getType

      public org.junit.platform.engine.TestDescriptor.Type getType()
      Specified by:
      getType in interface org.junit.platform.engine.TestDescriptor

    • execute

      public void execute() throws JmcCheckerException
      Executes the JMC test method.

      This method creates an instance of the test class, configures the JMC checker based on annotations, and executes the test method using the JMC Model Checker.

      Execution can be either running the model checker or replaying a previous execution and depends on the annotation provided for the test method. If the method is annotated with JmcReplay, it will replay the test method instead of executing it.

      Specified by:
      execute in interface JmcExecutableTestDescriptor
      Throws:
      JmcCheckerException - If an error occurs during execution or configuration.