Generate Test Cases

A region decomposition gives you one concrete input and its exact output for every distinct behaviour of a function. Each region is therefore a test case, and the whole decomposition is a test suite with complete behavioural coverage. This guide covers two ways to turn that into runnable tests: codelogician eval gen-test, a prebuilt generator for Python and TypeScript, and working from the raw region data when you want tests in your own shape.

Step 1: Attach a decomposition request, with `~prune:true`

Test generation reads a region decomposition, so the function needs a [@@decomp] attribute. See Region decomposition if you have not run one yet. It also needs concrete sample inputs, which only appear when pruning is on:

type payment_method =
  | Card
  | BankTransfer
  | Crypto
 
type decision =
  | Approved
  | Review
  | Blocked
  | Rejected
 
let authorize (m : payment_method) (amount : real) (fraud_score : real) : decision =
  if fraud_score >. 0.8 then Blocked
  else
    match m with
    | Card ->
      if amount >. 10000.0 then Review
      else if amount >. 500.0 && fraud_score >. 0.4 then Review
      else Approved
    | BankTransfer -> if amount >. 50000.0 then Review else Approved
    | Crypto -> Rejected
[@@decomp top ~prune:true ()]

`~prune:true` is required here

Without it, ImandraX returns regions with their constraints and invariants but leaves model empty. You get the symbolic answer with no concrete point inside each region.

The model also has to be executable. A model that calls an opaque function cannot be evaluated on concrete inputs, so substitute an approximation first, as described in Handle external dependencies.

Step 2: Check the decomposition first

It is worth looking at the regions before generating tests, since they are what the tests will be built from:

codelogician eval check-decomp authorize.iml

$ codelogician eval check-decomp authorize.iml
eval_res: Success
decomp_res_list:
- decomp_req_index: 0
  function_name: authorize
  decomp_res:
    description: Decomp succeeded with 8 regions
    regions:
    - label_path: 1.1.1.1.1.1
      weight: 1
      constraints:
      - fraud_score <=. 4.0 /. 5.0
      - m <> BankTransfer
      - m = Card
      - amount <=. 10000.0
      - amount >. 500.0
      - fraud_score >. 2.0 /. 5.0
      invariant: Review
      model:
        amount: (2502.0 /. 5.0)
        fraud_score: (4.0 /. 5.0)
        m: Card
      model_eval: Review

Four things to check before going on:

model is populated. If every region shows model: {}, go back and add ~prune:true.
The region count matches what you expected. Eight here. A disagreement means either the model or your mental model is wrong, and it is worth resolving first.
The sample points sit on boundaries. Values such as amount = 500.4 and fraud_score = 0.8 are not arbitrary: they are solutions to the branch conditions, so they land exactly where the behaviour changes.
The count is manageable. Thousands of regions produce thousands of tests. See cutting a decomposition down to size.

Step 3: Generate

codelogician eval gen-test --function authorize --lang python authorize.iml

Both --function (function name) and --lang (python or typescript) are required. --output writes to a file instead of stdout.

The output opens with type definitions mirroring the IML types:

from __future__ import annotations
 
from dataclasses import dataclass
 
 
@dataclass
class Approved:
    pass
 
 
@dataclass
class Review:
    pass
 
 
@dataclass
class Blocked:
    pass
 
 
@dataclass
class Rejected:
    pass
 
 
decision = Approved | Review | Blocked | Rejected
 
 
@dataclass
class Card:
    pass
 
 
@dataclass
class BankTransfer:
    pass
 
 
@dataclass
class Crypto:
    pass
 
 
payment_method = Card | BankTransfer | Crypto

Then one test per region, each carrying the region that produced it in its docstring:

def test_1():
    """test_1
 
    - invariant: Rejected
    - constraints:
        - m <> BankTransfer
        - m <> Card
        - fraud_score <=. (4.0 /. 5.0)
    """
    result: decision = authorize(amount=0.0, fraud_score=0.8, m=Crypto())
    expected: decision = Rejected()
    assert result == expected
 
 
def test_2():
    """test_2
 
    - invariant: Approved
    - constraints:
        - m = Card
        - m <> BankTransfer
        - fraud_score <=. (4.0 /. 5.0)
        - amount <=. 500.0
    """
    result: decision = authorize(amount=500.0, fraud_score=0.8, m=Card())
    expected: decision = Approved()
    assert result == expected

`gen-test` needs the codegen extra

It depends on codelogician[codegen]. If the command reports a missing dependency, install it with pip install 'codelogician[codegen]' or uv tool install 'codelogician[codegen]'.

Generated tests are a faithful account of the model. To run them against your implementation, point the imports at the code under test and, where the model's types differ from yours, map the generated dataclasses onto your own types. The region in each docstring tells you which behaviour a failing test is about.

Generate tests from the raw region data

gen-test gives you a ready-made test module. When you want something else, such as cases that slot into an existing test suite, a language other than Python or TypeScript, or tests that build domain objects rather than call a function with scalars, work from the region data directly. Everything the generator uses is available as JSON, and a short script turns it into tests of whatever shape you like.

Get the regions as JSON

codelogician eval check-decomp --json authorize.iml > regions.json

The payload is small and stable:

{
  "eval_res": "Success",
  "diagnostics": [ ... ],
  "decomp_res_list": [
    {
      "decomp_req_index": 0,
      "function_name": "authorize",
      "decomp_res": {
        "description": "Decomp succeeded with 8 regions",
        "regions": [ ... ]
      }
    }
  ]
}

And one region, verbatim:

{
  "label_path": "1.1.1.1.1.1",
  "weight": 1,
  "constraints": [
    "fraud_score <=. 4.0 /. 5.0",
    "m <> BankTransfer",
    "m = Card",
    "amount <=. 10000.0",
    "amount >. 500.0",
    "fraud_score >. 2.0 /. 5.0"
  ],
  "invariant": "Review",
  "model": {
    "amount": "(2502.0 /. 5.0)",
    "fraud_score": "(4.0 /. 5.0)",
    "m": "Card"
  },
  "model_eval": "Review"
}

Field	Meaning
`label_path`	Position in the decomposition tree, e.g. `1.1.1.1.1.1`. Stable within a run; useful as a test name.
`constraints`	Conditions on the inputs, as IML source strings. Conjoined.
`invariant`	Symbolic expression for the output, as an IML source string.
`model`	A concrete input inside the region: parameter name → IML value string. Empty unless the decomposition used `~prune:true`.
`model_eval`	The function's output at `model`, as an IML value string. Your expected value.
...	...

Values are IML source, so reals arrive as exact rationals such as (2502.0 /. 5.0) and variant constructors as bare names such as "Card". Your script decides how each maps onto the target language: an exact fraction or a float, an enum member or a string.

Turn the regions into tests

Here is a complete example, about sixty lines, emitting one parametrised pytest case per region against a hand-written domain API:

"""Turn a `codelogician eval check-decomp --json` payload into pytest cases.
 
Reads the JSON on stdin, writes a test module on stdout. The interesting part
is `iml_value`: every model value arrives as a *string of IML syntax*, so a
translator has to decide what each one means in the target language.
"""
 
import json
import re
import sys
from fractions import Fraction
 
# IML renders reals exactly, as rationals: "(2502.0 /. 5.0)" is 500.4.
RATIONAL = re.compile(r"^\(?\s*(-?[\d.]+)\s*/\.\s*(-?[\d.]+)\s*\)?$")
 
# Map IML constructors onto whatever the code under test actually uses.
ENUMS = {
    "Card": "PaymentMethod.CARD",
    "BankTransfer": "PaymentMethod.BANK_TRANSFER",
    "Crypto": "PaymentMethod.CRYPTO",
    "Approved": "Decision.APPROVED",
    "Review": "Decision.REVIEW",
    "Blocked": "Decision.BLOCKED",
    "Rejected": "Decision.REJECTED",
}
 
 
def iml_value(raw: str) -> str:
    """Render one IML value as a Python literal."""
    raw = raw.strip()
    if raw in ENUMS:
        return ENUMS[raw]
    m = RATIONAL.match(raw)
    if m:
        return repr(float(Fraction(m.group(1)) / Fraction(m.group(2))))
    if re.fullmatch(r"-?\d+\.\d*", raw):
        return repr(float(raw))
    if re.fullmatch(r"-?\d+", raw):
        return raw
    raise ValueError(f"unhandled IML value: {raw!r}")
 
 
def main() -> None:
    payload = json.load(sys.stdin)
    print("import pytest\n")
    print("from payments import Decision, PaymentMethod, authorize\n")
 
    for decomp in payload["decomp_res_list"]:
        fn = decomp["function_name"]
        regions = decomp["decomp_res"]["regions"]
        print(f"# {len(regions)} regions of `{fn}`, one case each.")
        print("@pytest.mark.parametrize(")
        print('    "region,kwargs,expected",')
        print("    [")
        for region in regions:
            kwargs = {k: iml_value(v) for k, v in sorted(region["model"].items())}
            args = ", ".join(f'"{k}": {v}' for k, v in kwargs.items())
            expected = iml_value(region["model_eval"])
            print(f'        ("{region["label_path"]}", {{{args}}}, {expected}),')
        print("    ],")
        print(")")
        print(f"def test_{fn}(region, kwargs, expected):")
        print(f"    assert {fn}(**kwargs) == expected")
 
 
if __name__ == "__main__":
    main()

codelogician eval check-decomp --json authorize.iml | python3 translate_regions.py

import pytest
 
from payments import Decision, PaymentMethod, authorize
 
# 8 regions of `authorize`, one case each.
@pytest.mark.parametrize(
    "region,kwargs,expected",
    [
        ("1.1.1.1.1.1", {"amount": 500.4, "fraud_score": 0.8, "m": PaymentMethod.CARD}, Decision.REVIEW),
        ("1.1.1.2", {"amount": 500.0, "fraud_score": 0.8, "m": PaymentMethod.CARD}, Decision.APPROVED),
        ("1.1.1.3", {"amount": 10001.0, "fraud_score": 0.8, "m": PaymentMethod.CARD}, Decision.REVIEW),
        ("1.1.2", {"amount": 0.0, "fraud_score": 0.8, "m": PaymentMethod.CRYPTO}, Decision.REJECTED),
        ("1.2.1", {"amount": 50000.0, "fraud_score": 0.8, "m": PaymentMethod.BANK_TRANSFER}, Decision.APPROVED),
        ("1.2.2", {"amount": 50001.0, "fraud_score": 0.8, "m": PaymentMethod.BANK_TRANSFER}, Decision.REVIEW),
        ("2.1.1.1.1", {"amount": 501.0, "fraud_score": 0.4, "m": PaymentMethod.CARD}, Decision.APPROVED),
        ("3", {"amount": 0.0, "fraud_score": 1.8, "m": PaymentMethod.CARD}, Decision.BLOCKED),
    ],
)
def test_authorize(region, kwargs, expected):
    assert authorize(**kwargs) == expected

Eight regions, eight cases, in the shape the project actually wants: importing PaymentMethod and Decision from the code under test rather than redeclaring them, parametrised rather than eight separate functions, and each case labelled with the region it came from so a failure points back at a behaviour.

Region decomposition: what these tests guarantee, and how to control how many of them you get
codelogician eval check-decomp: full command reference, including the JSON payload