eval

Evaluate IML files using the ImandraX reasoning engine. This is the primary command for analyzing formal models — checking syntax, verifying properties, decomposing behavior, and generating tests.

codelogician eval COMMAND [OPTIONS]

Subcommands

Command	Description
`check`	Evaluate an IML file (syntax check and basic reasoning)
`list-vg`	List verification goals in an IML file
`check-vg`	Check verification goals in an IML file
`list-decomp`	List decomposition requests in an IML file
`check-decomp`	Check decomposition requests in an IML file
`gen-test`	Generate test cases from region decomposition

eval check

Evaluate an IML file without running verification goals or decomposition requests. Use this for syntax validation and basic reasoning.

codelogician eval check [OPTIONS] [FILE]

Arguments:

Argument	Description
`FILE`	Path to the IML file. Set to `-` to read from stdin

Options:

Option	Default	Description
`--with-vgs / --no-with-vgs`	`--no-with-vgs`	Include `verify` and `instance` requests during evaluation
`--with-decomps / --no-with-decomps`	`--no-with-decomps`	Include decomposition requests during evaluation
`--json / --no-json`	`--no-json`	Output results in JSON format

Example:

codelogician eval check model.iml

eval list-vg

List all verification goals specified by verify or instance commands in an IML file, without executing them.

codelogician eval list-vg [OPTIONS] [FILE]

Arguments:

Argument	Description
`FILE`	Path to the IML file. Set to `-` to read from stdin

Options:

Option	Default	Description
`--json / --no-json`	`--no-json`	Output results in JSON format

Example:

codelogician eval list-vg model.iml

eval check-vg

Check verification goals specified by verify or instance commands in an IML file. ImandraX will attempt to prove or refute each goal.

codelogician eval check-vg [OPTIONS] [FILE]

Arguments:

Argument	Description
`FILE`	Path to the IML file. Set to `-` to read from stdin

Options:

Option	Default	Description
`--index`	—	Index of a specific verification goal to check
`--check-all / --no-check-all`	`--no-check-all`	Check all verification goals in the file
`--json / --no-json`	`--no-json`	Output results in JSON format

Example:

# Check a specific verification goal
codelogician eval check-vg --index 0 model.iml

eval list-decomp

List all decomposition requests in an IML file, without executing them.

codelogician eval list-decomp [OPTIONS] [FILE]

Arguments:

Argument	Description
`FILE`	Path to the IML file. Set to `-` to read from stdin

Options:

Option	Default	Description
`--json / --no-json`	`--no-json`	Output results in JSON format

Example:

codelogician eval list-decomp model.iml

eval check-decomp

Execute decomposition requests in an IML file. Region decomposition identifies all distinct behavioral regions of a function.

codelogician eval check-decomp [OPTIONS] [FILE]

Arguments:

Argument	Description
`FILE`	Path to the IML file. Set to `-` to read from stdin

Options:

Option	Default	Description
`--index`	—	Index of a specific decomposition request to check
`--check-all / --no-check-all`	`--no-check-all`	Check all decomposition requests in the file
`--json / --no-json`	`--no-json`	Output results in JSON format

Example:

# Check all decompositions
codelogician eval check-decomp --check-all model.iml

eval gen-test

Generate test cases in Python or TypeScript from a region decomposition in an IML file.

codelogician eval gen-test [OPTIONS] IML_PATH

Arguments:

Argument	Description
`IML_PATH`	Path to the IML file. Set to `-` to read from stdin (required)

Options:

Option	Description
`-f, --function`	Name of the function to generate test cases for (required)
`-l, --lang`	Target language — `python` or `typescript` (required)
`-o, --output`	Output file path. Defaults to stdout

Example:

# Generate Python tests for a function
codelogician eval gen-test -f my_function -l python -o test_my_function.py model.iml