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-test`	List test requests in an IML file
`check-test`	Check test requests 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:

Given a small model:

type payment_method =
  | Card
  | BankTransfer
 
let calculate_fee m amount =
  match m with
  | Card -> 0.029 *. amount +. 0.30
  | BankTransfer -> 0.008 *. amount +. 1.50

$ codelogician eval check fee.iml
Eval succeed

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:

Add a verification goal to the model:

(* A verification goal: the fee should always be smaller than the amount paid. *)
verify (fun m amount ->
  amount >. 0.0 ==>
  calculate_fee m amount <. amount
)

Then check it. ImandraX proves the goal or returns a concrete counterexample:

$ codelogician eval check-vg fee.iml
eval_res: Success
vg_res_list:
- vg_req_index: 0
  kind: verify
  src: |-
    fun m amount ->
      amount >. 0.0 ==>
      calculate_fee m amount <. amount
  vg_res:
    refuted:
      model:
        m_type: Counter_example
        src: |
          module M = struct
 
            let amount = 1.0
            let m = BankTransfer
 
          end
    errors: []
    task: <hidden>

eval list-test

List all test requests specified by test commands in an IML file, without executing them.

codelogician eval list-test [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-test model.iml

eval check-test

Execute test requests specified by test commands in an IML file.

codelogician eval check-test [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 test request to check
`--check-all / --no-check-all`	`--no-check-all`	Check all test requests in the file
`--json / --no-json`	`--no-json`	Output results in JSON format

Example:

codelogician eval check-test --check-all 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