Skip to content

Tests

Statix has its own test format. These tests can help to debug your specification and isolate issues. In this section, we explain the format and the output of such tests.

Test Format

Statix tests should reside in *.stxtest files, and look as follows:

resolve $Constraint

$Section*

At the top level, the resolve keyword indicates this is a test file. After this keyword, the constraint that should be solved when executing the test is provided. Finally, any section that can be found in a regular module can be added to a test.

A test can be executed using the traditional or the concurrent solver with the Spoofax > Evaluate > Evaluate Test or Spoofax > Evaluate > Evaluate Test (Concurrent) menu, respectively.

Test Output

When a test is executed, a .stxresult file with the test result will open. This file contains three sections.

First, under the substitution header, a mapping from the top-level existentially quantified variables to their values is provided. Due to the normalization Statix applies, there are sometimes additional entries for wildcards and return values of functional predicates.

Secondly, under analysis and scope graph, the scope graph that models the test constraint is shown. A scope graph consists of a list of scope terms, which look as follows

$ScopeName {
  relations {
    $RelationID : $Term+
  }
  edges {
    $LabelID: $Scope+
  }
}

That is, for each label and relation for which entries exists in a scope, a list of associated scopes/data is shown.

Empty Scopes

Note that no entry for an empty scope will be present.

Finally, under the errors, warnings and notes headers, the appropriate messages of these types are shown. The message value is equal to the top line of a regular Statix message, but no traces are displayed. Terms in templates are formatted three levels deep.


Last update: March 22, 2024
Created: March 22, 2024