Testing using Maude

Currently the abs-maven-plugin provide goal 'maudetest' to support simulation of ABS unit tests (test code resides at $project.basedir/src/test/abs by default) in Maude and interpreting the maude simulation output.

To simulate ABS test in Maude from ABS in a ABS Maven project, include the following plugin declaration inside the <build><plugins>...</plugins></build> section of the pom.xml

<plugin>
  <groupId>eu.hats-project</groupId>
  <artifactId>abs-maven-plugin</artifactId>
  <version>1.0-SNAPSHOT</version>
  <executions>
    <execution>
      <id>abs-test</id>
      <goals>
        <goal>maudetest</goal>
      </goals>
      <configuration>
        <maudeInterpreter>/path/to/abs-interpreter.maude</maudeInterpreter>
        <maude>/path/to/maude-executable</maude>
        ... (see optional configuration for detail) ...
      </configuration>
    </execution>
  </executions>
</plugin>

Optional configuration goal maudetest

  • absTestFolder, ABS test folder, default is $project.basedir/src/test/abs.
  • absMaudeBackendTestOutputFile, Maude output file, default is $project.basedir/target/abs/gen/maude/test.maude.
  • generateRunner, whether to generate ABSUnit test runner (.abs file containing a main block that executes all specified ABSUnit tests concurrently.
  • absTestRunnerFile, the file to which the generated ABSUnit test runner is written, default is $project.basedir/target/abs/gen/abs/runner.abs.
  • deltaNames, an ordered list of deltas to applied on Maude rewrite.
    <deltaNames>
      <param>D1</param>
      ...
    </deltaNames>
  • productName, build given product by applying deltas (productName is a string that is the qualified product ID)

Note that productName and deltaNames cannot be declared as the same time. To test the source of the ABS Maven project, invoke the 'test' goal

mvn test