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

Option lists here are not exhaustive

The tables below cover the stable options for each subcommand. Run codelogician eval <subcommand> --help for the complete, current list.

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`	Keep `verify` and `instance` requests before evaluating
`--with-decomps / --no-with-decomps`	`--no-with-decomps`	Keep decomp requests before evaluating
`--with-tests / --no-with-tests`	`--no-with-tests`	Keep `test` requests before evaluating
`--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`	all goals	Index of the verification goal to check, as listed by `list-vg`. Omit to check all
`--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`	all tests	Index of the test request to check, as listed by `list-test`. Omit to check all
`--seed`	—	Random seed, for reproducible random predicate assertions
`--json / --no-json`	`--no-json`	Output results in JSON format

Example:

codelogician eval check-test 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`	all decomps	Index of the decomposition request to check, as listed by `list-decomp`. Omit to check all
`--json / --no-json`	`--no-json`	Output results in JSON format

Example:

# Check every decomposition request in the file
codelogician eval check-decomp model.iml

Each region describes one behavioural case of the function: its constraints plus the invariant. With ~prune:true on the decomposition request, each region also carries a concrete sample input (model) and the output at that input (model_eval), which is what test generation is built from.

JSON output

--json emits the regions in a machine-readable form, for feeding into your own tooling. The shape:

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

One region:

{
  "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	Type	Meaning
`label_path`	string	Position in the decomposition tree, e.g. `1.1.1.1.1.1`. Stable within a run
`weight`	int	Relative size hint for the region
`constraints`	string list	Conditions on the inputs, as IML source. Conjoined
`invariant`	string	Symbolic expression for the output, as IML source
`model`	object	A concrete input inside the region: parameter name → IML value. Empty unless `~prune:true`
`model_eval`	string	The function's output at `model`, as an IML value. `null` when `model` is empty

All values are strings of IML source, not JSON numbers: a real prints as an exact rational such as (2502.0 /. 5.0). Consumers have to evaluate them. See Turn the regions into tests for a worked translator.

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

Requirements

Needs the optional codegen extra (pip install 'codelogician[codegen]'), and a decomposition request declared with ~prune:true. Without concrete sample points there is nothing to build a test from. See Generate test cases.

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