tessellate 0.5.0

use serde_json::Value;
use std::fs;
use std::io::Write;
use std::path::{Path, PathBuf};
use std::process::{Command, Output, Stdio};
use std::sync::atomic::{AtomicU64, Ordering};
use std::sync::{Mutex, MutexGuard};

static NEXT_DIRECTORY: AtomicU64 = AtomicU64::new(0);
static SOLVER_TEST_LOCK: Mutex<()> = Mutex::new(());

fn solver_test_guard() -> MutexGuard<'static, ()> {
    SOLVER_TEST_LOCK
        .lock()
        .unwrap_or_else(std::sync::PoisonError::into_inner)
}

const VALID_SOURCE: &str = r"mod sample

enum Answer:
    Yes
    No

record Subject:
    flag: Bool

dec outcome(s Subject): Answer

sample.policy@Sample policy:
    Flagged subjects receive Yes; unflagged subjects receive No.

    rule yes(s Subject):
        s.flag: outcome(s) = Yes

    rule no(s Subject):
        not s.flag: outcome(s) = No

test yes_case:
    let s = Subject { flag: true }
    expect outcome(s) = Yes

assert total(s Subject):
    outcome(s)
";

const BROKEN_ANALYSIS_SOURCE: &str = r"mod sample

enum Answer:
    Yes
    No

record Subject:
    flag: Bool

dec outcome(s Subject): Answer

sample.policy@Sample policy:
    Flagged subjects receive Yes.

    rule yes(s Subject):
        s.flag: outcome(s) = Yes

assert total(s Subject):
    outcome(s)
";

const BATCH_RUN_SOURCE: &str = r"mod batch

enum Answer:
    Yes
    No

record Subject:
    flag: Bool

dec primary(s Subject): Answer
dec review(s Subject): Answer

rule primary_yes(s Subject):
    s.flag: primary(s) = Yes

rule primary_no(s Subject):
    not s.flag: primary(s) = No

rule review_all(s Subject):
    : review(s) = Yes

test z_case:
    let s = Subject { flag: true }
    expect primary(s) = No
    expect review(s) = No

test a_case:
    let s = Subject { flag: false }
    expect primary(s) = Yes
    expect review(s) = No
";

const EXPLANATION_STATES_SOURCE: &str = r"mod explanation_states

enum Answer:
    Yes
    No

record Subject:
    flag: Bool
    alternate: Bool
    maybe_flag: Bool?

dec resolved(s Subject): Answer
dec empty(s Subject): Answer
dec uncertain(s Subject): Answer
dec disputed(s Subject): Answer
dec replaced(s Subject): Answer

rule resolved_yes(s Subject):
    s.flag: resolved(s) = Yes

rule uncertain_yes(s Subject):
    s.maybe_flag: uncertain(s) = Yes

rule disputed_yes(s Subject):
    s.flag: disputed(s) = Yes

rule disputed_no(s Subject):
    s.alternate: disputed(s) = No

rule replaced_base(s Subject):
    s.flag: replaced(s) = No

rule replaced_exception(s Subject):
    s.flag and s.alternate: replaced(s) = Yes

rule replaced_exception_override(s Subject):
    s.flag and s.alternate: override replaced_base

test all_states:
    let s = Subject { flag: true, alternate: true }
    expect resolved(s) = Yes
    expect empty(s) = Yes
    expect uncertain(s) = Yes
    expect disputed(s) = Yes
    expect replaced(s) = Yes
";

const INTERACTIVE_SOURCE: &str = r"mod interactive

enum Answer:
    Yes
    No

record Subject:
    enabled: Bool
    detail: Bool
    unused: Bool

dec outcome(s Subject): Answer

rule yes(s Subject):
    s.enabled and s.detail: outcome(s) = Yes

rule no(s Subject):
    not s.enabled: outcome(s) = No
";

struct TestDirectory {
    path: PathBuf,
}

impl TestDirectory {
    fn new() -> Self {
        let ordinal = NEXT_DIRECTORY.fetch_add(1, Ordering::Relaxed);
        let path =
            std::env::temp_dir().join(format!("tess-cli-tests-{}-{ordinal}", std::process::id()));
        fs::create_dir_all(&path).unwrap();
        Self { path }
    }

    fn write(&self, name: &str, contents: &str) -> PathBuf {
        let path = self.path.join(name);
        if let Some(parent) = path.parent() {
            fs::create_dir_all(parent).unwrap();
        }
        fs::write(&path, contents).unwrap();
        path
    }
}

impl Drop for TestDirectory {
    fn drop(&mut self) {
        let _ = fs::remove_dir_all(&self.path);
    }
}

fn tess(arguments: &[&str]) -> Output {
    Command::new(env!("CARGO_BIN_EXE_tess"))
        .args(arguments)
        .env("NO_COLOR", "1")
        .env_remove("CLICOLOR_FORCE")
        .output()
        .unwrap()
}

fn tess_without_path(arguments: &[&str]) -> Output {
    Command::new(env!("CARGO_BIN_EXE_tess"))
        .args(arguments)
        .env("NO_COLOR", "1")
        .env("PATH", "/definitely-not-present")
        .env_remove("CLICOLOR_FORCE")
        .output()
        .unwrap()
}

fn tess_with_automatic_color(arguments: &[&str]) -> Output {
    Command::new(env!("CARGO_BIN_EXE_tess"))
        .args(arguments)
        .env_remove("NO_COLOR")
        .env_remove("CLICOLOR")
        .env_remove("CLICOLOR_FORCE")
        .output()
        .unwrap()
}

fn tess_with_forced_color(arguments: &[&str]) -> Output {
    Command::new(env!("CARGO_BIN_EXE_tess"))
        .args(arguments)
        .env_remove("NO_COLOR")
        .env_remove("CLICOLOR")
        .env("CLICOLOR_FORCE", "1")
        .output()
        .unwrap()
}

fn tess_with_no_color_and_force(arguments: &[&str]) -> Output {
    Command::new(env!("CARGO_BIN_EXE_tess"))
        .args(arguments)
        .env("NO_COLOR", "1")
        .env("CLICOLOR_FORCE", "1")
        .output()
        .unwrap()
}

fn tess_in(directory: &Path, arguments: &[&str]) -> Output {
    Command::new(env!("CARGO_BIN_EXE_tess"))
        .current_dir(directory)
        .args(arguments)
        .env("NO_COLOR", "1")
        .env_remove("CLICOLOR_FORCE")
        .output()
        .unwrap()
}

fn tess_with_stdin(arguments: &[&str], stdin: &[u8]) -> Output {
    let mut child = Command::new(env!("CARGO_BIN_EXE_tess"))
        .args(arguments)
        .env("NO_COLOR", "1")
        .env_remove("CLICOLOR_FORCE")
        .stdin(Stdio::piped())
        .stdout(Stdio::piped())
        .stderr(Stdio::piped())
        .spawn()
        .unwrap();
    child.stdin.take().unwrap().write_all(stdin).unwrap();
    child.wait_with_output().unwrap()
}

fn path(path: &Path) -> &str {
    path.to_str().unwrap()
}

fn stdout(output: &Output) -> String {
    String::from_utf8(output.stdout.clone()).unwrap()
}

fn stderr(output: &Output) -> String {
    String::from_utf8(output.stderr.clone()).unwrap()
}

fn workspace_root() -> PathBuf {
    PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("../..")
}

#[test]
fn validate_emits_success_and_failure_json_envelopes() {
    let directory = TestDirectory::new();
    let valid = directory.write("valid.tes", VALID_SOURCE);
    let output = tess(&["validate", path(&valid)]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert_eq!(stdout(&output), format!("validated {}\n", valid.display()));

    let output = tess(&["validate", path(&valid), "--json"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let json: Value = serde_json::from_slice(&output.stdout).unwrap();
    assert_eq!(json["ok"], true);
    assert_eq!(json["command"], "validate");

    let invalid = directory.write("invalid.tes", "mod invalid\nenum E:\n    A B\n");
    let output = tess(&["validate", path(&invalid), "--json"]);
    assert_eq!(output.status.code(), Some(1));
    let json: Value = serde_json::from_slice(&output.stdout).unwrap();
    assert_eq!(json["ok"], false);
    assert_eq!(json["command"], "validate");
    assert!(!json["diagnostics"].as_array().unwrap().is_empty());
}

#[test]
fn help_uses_canonical_commands_targets_and_verification_flags() {
    let output = tess(&["--help"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let help = stdout(&output);
    let has_command = |name: &str, description: &str| {
        help.lines().any(|line| {
            line.trim_start()
                .strip_prefix(name)
                .is_some_and(|rest| rest.starts_with(' ') && rest.trim_start() == description)
        })
    };
    assert!(
        has_command(
            "lock",
            "Generate or update the deterministic local package lockfile"
        ),
        "{help}"
    );
    assert!(
        has_command(
            "validate",
            "Validate Tess syntax, types, names, and project structure"
        ),
        "{help}"
    );
    assert!(
        has_command("completions", "Generate a shell completion script"),
        "{help}"
    );
    assert!(
        has_command(
            "verify",
            "Verify quantified assertions and bounded state traces"
        ),
        "{help}"
    );
    assert!(
        has_command(
            "graph",
            "Render a policy graph or compare it with a recorded JSON baseline"
        ),
        "{help}"
    );
    assert!(!help.lines().any(|line| line.starts_with("  check ")));
    assert!(!help.lines().any(|line| line.starts_with("  explore ")));

    let output = tess(&["lock", "--help"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert!(
        stdout(&output).contains("Usage: tess lock <TARGET>"),
        "{}",
        stdout(&output)
    );

    let output = tess(&["validate", "--help"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let help = stdout(&output);
    assert!(
        help.contains("Usage: tess validate [OPTIONS] <TARGET>"),
        "{help}"
    );

    let output = tess(&["verify", "--help"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let help = stdout(&output);
    assert!(
        help.contains("Usage: tess verify [OPTIONS] <TARGET>"),
        "{help}"
    );
    assert!(help.contains("--assert <NAME>"), "{help}");
    assert!(help.contains("--max-evaluations <N>"), "{help}");
    assert!(!help.contains("--check"), "{help}");
    assert!(!help.contains("--max-combinations"), "{help}");

    for command in ["test", "run"] {
        let output = tess(&[command, "--help"]);
        assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
        let help = stdout(&output);
        assert!(help.contains("--test <NAME>"), "{help}");
        assert!(!help.contains("<CASE>"), "{help}");
    }

    for command in ["run", "explain"] {
        let output = tess(&[command, "--help"]);
        assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
        let help = stdout(&output);
        assert!(help.contains("--verbose"), "{help}");
        assert!(help.contains("complete rule trace"), "{help}");
    }

    let output = tess(&["graph", "--help"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let help = stdout(&output);
    assert!(
        help.contains("Usage: tess graph [OPTIONS] <TARGET>"),
        "{help}"
    );
    assert!(help.contains("--decision <NAME>"), "{help}");
    assert!(help.contains("--format <FORMAT>"), "{help}");
}

#[test]
fn completions_help_lists_supported_shells() {
    let output = tess(&["completions", "--help"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert!(output.stderr.is_empty(), "{}", stderr(&output));
    let help = stdout(&output);
    assert!(help.contains("Usage: tess completions <SHELL>"), "{help}");
    assert!(
        help.contains("possible values: bash, elvish, fish, powershell, zsh"),
        "{help}"
    );
}

#[test]
fn completions_generates_scripts_for_every_supported_shell() {
    for (shell, marker) in [
        ("bash", "complete -F _tess"),
        ("elvish", "edit:completion:arg-completer[tess]"),
        ("fish", "complete -c tess"),
        (
            "powershell",
            "Register-ArgumentCompleter -Native -CommandName 'tess'",
        ),
        ("zsh", "#compdef tess"),
    ] {
        let output = tess(&["completions", shell]);
        assert_eq!(
            output.status.code(),
            Some(0),
            "{shell}: {}",
            stderr(&output)
        );
        assert!(output.stderr.is_empty(), "{shell}: {}", stderr(&output));
        let script = stdout(&output);
        assert!(script.contains(marker), "{shell}: {script}");
        assert!(script.contains("run"), "{shell}: {script}");
    }
}

#[test]
fn completions_rejects_an_unknown_shell() {
    let output = tess(&["completions", "nushell"]);
    assert_eq!(output.status.code(), Some(2));
    assert!(output.stdout.is_empty(), "{}", stdout(&output));
    let error = stderr(&output);
    assert!(error.contains("invalid value 'nushell'"), "{error}");
    assert!(error.contains("possible values"), "{error}");
}

#[test]
fn removed_commands_and_verification_flags_are_usage_errors() {
    let directory = TestDirectory::new();
    let source = directory.write("valid.tes", VALID_SOURCE);

    for arguments in [
        vec!["check", path(&source)],
        vec!["explore", path(&source)],
        vec!["verify", path(&source), "--check", "total"],
        vec!["verify", path(&source), "--max-combinations", "10"],
    ] {
        let output = tess(&arguments);
        assert_eq!(
            output.status.code(),
            Some(2),
            "removed syntax unexpectedly succeeded: {arguments:?}\nstdout: {}\nstderr: {}",
            stdout(&output),
            stderr(&output)
        );
    }
}

#[test]
fn lint_reports_warnings_and_can_apply_a_strict_failure_policy() {
    let directory = TestDirectory::new();
    let warning_source = VALID_SOURCE.replacen("s.flag: outcome(s) = Yes", ": outcome(s) = Yes", 1);
    let source = directory.write("warning.tes", &warning_source);

    let output = tess(&["lint", path(&source)]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert!(stderr(&output).contains("warning[W0401]"));
    assert!(stdout(&output).contains("0 error(s), 1 warning(s)"));

    let output = tess(&["lint", path(&source), "--warnings-as-errors", "--json"]);
    assert_eq!(output.status.code(), Some(1));
    assert!(output.stderr.is_empty());
    let json: Value = serde_json::from_slice(&output.stdout).unwrap();
    assert_eq!(json["ok"], false);
    assert_eq!(json["command"], "lint");
    assert_eq!(json["result"]["errors"], 0);
    assert_eq!(json["result"]["warnings"], 1);
    assert_eq!(json["result"]["warnings_as_errors"], true);
    assert_eq!(json["diagnostics"][0]["severity"], "warning");
}

#[test]
fn lint_reads_explicit_stdin_and_rejects_invalid_utf8() {
    let output = tess_with_stdin(&["lint", "-", "--json"], VALID_SOURCE.as_bytes());
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let json: Value = serde_json::from_slice(&output.stdout).unwrap();
    assert_eq!(json["ok"], true);
    assert_eq!(json["result"]["errors"], 0);

    let output = tess_with_stdin(&["lint", "-"], &[0xff, 0xfe]);
    assert_eq!(output.status.code(), Some(2));
    assert!(stderr(&output).contains("UTF-8 source from stdin"));

    let output = tess_with_stdin(
        &["lint", "-", "--warnings-as-errors"],
        b"mod m\nuse \"model.tes\"\n",
    );
    assert_eq!(output.status.code(), Some(1));
    assert!(stderr(&output).contains("error[M0006]"));
    assert!(stderr(&output).contains("project-aware loader"));
}

#[test]
fn test_filters_cases_and_reports_expectation_failure() {
    let directory = TestDirectory::new();
    let valid = directory.write("valid.tes", VALID_SOURCE);
    let output = tess(&["test", path(&valid), "--test", "yes_case"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert!(stdout(&output).contains("PASS"));

    let failing_source = VALID_SOURCE.replace("expect outcome(s) = Yes", "expect outcome(s) = No");
    let failing = directory.write("failing.tes", &failing_source);
    let output = tess(&["test", path(&failing), "--test", "yes_case"]);
    assert_eq!(output.status.code(), Some(1));
    assert!(stdout(&output).contains("FAIL"));
}

#[test]
fn test_supports_versioned_json_details_and_junit_xml() {
    let directory = TestDirectory::new();
    let source = directory.write("valid.tes", VALID_SOURCE);

    let output = tess(&["test", path(&source), "--format", "json"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let report: Value = serde_json::from_slice(&output.stdout).unwrap();
    assert_eq!(report["command"], "test");
    assert_eq!(report["result"]["schema_version"], "tess.test-report/v2");
    assert_eq!(report["result"]["module"], "sample");
    assert_eq!(
        report["result"]["outcomes"][0]["assertions"][0]["query"],
        "outcome(s)"
    );
    assert_eq!(
        report["result"]["outcomes"][0]["assertions"][0]["actual"]["status"],
        "resolved"
    );

    let output = tess(&["test", path(&source), "--format", "junit"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let xml = stdout(&output);
    assert!(xml.starts_with("<?xml version=\"1.0\""), "{xml}");
    assert!(
        xml.contains("<testsuite name=\"sample\" tests=\"1\""),
        "{xml}"
    );
    assert!(
        xml.contains("<testcase classname=\"sample\" name=\"yes_case\""),
        "{xml}"
    );

    let conflict = tess(&["test", path(&source), "--json", "--format", "junit"]);
    assert_eq!(conflict.status.code(), Some(2));
}

#[test]
fn snapshot_record_and_diff_are_deterministic_and_semantic() {
    let directory = TestDirectory::new();
    let source = directory.write("policy.tes", VALID_SOURCE);
    let baseline = directory.path.join("baseline.json");

    let output = tess(&[
        "snapshot",
        "record",
        path(&source),
        "--output",
        path(&baseline),
    ]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert!(stdout(&output).contains("recorded 1 decision result(s)"));
    let first = fs::read(&baseline).unwrap();
    let snapshot: Value = serde_json::from_slice(&first).unwrap();
    assert_eq!(snapshot["schema_version"], "tess.decision-snapshot/v1");
    assert_eq!(
        snapshot["cases"][0]["decisions"][0]["result"]["status"],
        "resolved"
    );

    let output = tess(&[
        "snapshot",
        "record",
        path(&source),
        "--output",
        path(&baseline),
    ]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert_eq!(fs::read(&baseline).unwrap(), first);

    let output = tess(&[
        "snapshot",
        "diff",
        path(&source),
        "--baseline",
        path(&baseline),
    ]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert!(stdout(&output).contains("snapshot matches"));

    let changed_source =
        VALID_SOURCE.replace("s.flag: outcome(s) = Yes", "s.flag: outcome(s) = No");
    fs::write(&source, changed_source).unwrap();
    let output = tess(&[
        "snapshot",
        "diff",
        path(&source),
        "--baseline",
        path(&baseline),
    ]);
    assert_eq!(output.status.code(), Some(1), "{}", stderr(&output));
    assert!(stdout(&output).contains("CHANGED yes_case: outcome(s)#1"));

    let output = tess(&[
        "snapshot",
        "diff",
        path(&source),
        "--baseline",
        path(&baseline),
        "--json",
    ]);
    assert_eq!(output.status.code(), Some(1), "{}", stderr(&output));
    let report: Value = serde_json::from_slice(&output.stdout).unwrap();
    assert_eq!(report["ok"], false);
    assert_eq!(
        report["result"]["diff"]["schema_version"],
        "tess.snapshot-diff/v1"
    );
    assert_eq!(
        report["result"]["diff"]["changes"][0]["change"],
        "decision_changed"
    );

    let malformed = directory.write("malformed-snapshot.json", "{not json}");
    let output = tess(&[
        "snapshot",
        "diff",
        path(&source),
        "--baseline",
        path(&malformed),
    ]);
    assert_eq!(output.status.code(), Some(2));
    assert!(stderr(&output).contains("invalid decision snapshot"));

    let output = tess(&[
        "snapshot",
        "record",
        path(&source),
        "--output",
        path(&baseline),
        "--test",
        "missing",
    ]);
    assert_eq!(output.status.code(), Some(1));
    assert!(stderr(&output).contains("test `missing` was not found"));
}

#[test]
fn run_and_explain_default_to_concise_output_with_verbose_and_compact_opt_ins() {
    let directory = TestDirectory::new();
    let source = directory.write("valid.tes", VALID_SOURCE);
    let output = tess(&["run", path(&source), "--test", "yes_case"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let output = stdout(&output);
    assert!(output.contains("outcome(s) = Answer.Yes"), "{output}");
    assert!(output.contains("yes_case"), "{output}");
    assert!(output.contains("reason rule `yes`"), "{output}");
    assert!(
        output.contains("basis `sample.policy` @ `Sample policy`"),
        "{output}"
    );
    assert!(!output.contains("-->"), "{output}");
    assert!(!output.contains("let s = Subject"), "{output}");

    let output = tess(&["explain", path(&source), "--test", "yes_case"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let output = stdout(&output);
    assert!(output.contains("outcome(s) = Answer.Yes"), "{output}");
    assert!(output.contains("yes_case"), "{output}");
    assert!(output.contains("reason rule `yes`"), "{output}");
    assert!(!output.contains("-->"), "{output}");

    let output = tess(&["explain", path(&source), "--test", "yes_case", "--verbose"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let output = stdout(&output);
    assert!(output.contains("let s = Subject"), "{output}");
    assert!(output.contains("-->"), "{output}");
    assert!(output.contains("condition"), "{output}");

    let output = tess(&["run", path(&source), "--test", "yes_case", "--compact"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert_eq!(stdout(&output), "outcome(s) = Answer.Yes\n");

    let output = tess(&["explain", path(&source), "--test", "yes_case", "--compact"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert_eq!(stdout(&output), "outcome(s) = Answer.Yes\n");

    let output = tess(&["explain", path(&source), "--test", "yes_case", "--json"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let json: Value = serde_json::from_slice(&output.stdout).unwrap();
    assert_eq!(json["result"]["status"], "resolved");
    assert_eq!(json["result"]["rules"][0]["rule"], "sample.policy.no");
    assert_eq!(json["result"]["rules"][1]["rule"], "sample.policy.yes");
    let basis = "Flagged subjects receive Yes; unflagged subjects receive No.";
    let rule_basis = &json["result"]["rules"][1]["basis"][0];
    assert_eq!(rule_basis["id"], "sample.policy");
    assert_eq!(rule_basis["locator"], "Sample policy");
    assert_eq!(rule_basis["text"].as_str().unwrap().trim_end(), basis);
    assert_eq!(
        json["result"]["candidates"][0]["basis"],
        json["result"]["rules"][1]["basis"]
    );
    assert!(json["result"]["rules"][1].get("source").is_none());
    assert!(json["result"]["candidates"][0].get("source").is_none());

    let output = tess(&[
        "explain",
        path(&source),
        "--test",
        "yes_case",
        "--json",
        "--provenance",
    ]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let json: Value = serde_json::from_slice(&output.stdout).unwrap();
    assert_eq!(json["result"]["provenance"]["schema_version"], 1);
    assert_eq!(
        json["result"]["evaluation"]["result"]["status"]["status"],
        "resolved"
    );
    let nodes = json["result"]["provenance"]["nodes"].as_array().unwrap();
    assert!(nodes.iter().any(|node| node["kind"] == "input_field"));
    assert!(nodes.iter().any(|node| node["kind"] == "decision_result"));

    let output = tess(&[
        "explain",
        path(&source),
        "--test",
        "yes_case",
        "--provenance",
    ]);
    assert_eq!(output.status.code(), Some(2));
    assert!(stderr(&output).contains("--json"));
}

#[test]
fn human_output_colors_only_when_the_output_environment_supports_it() {
    let directory = TestDirectory::new();
    let source = directory.write("valid.tes", VALID_SOURCE);
    let arguments = ["run", path(&source), "--test", "yes_case"];

    let automatic = tess_with_automatic_color(&arguments);
    assert_eq!(automatic.status.code(), Some(0), "{}", stderr(&automatic));
    assert!(!stdout(&automatic).contains("\u{1b}["));

    let forced = tess_with_forced_color(&arguments);
    assert_eq!(forced.status.code(), Some(0), "{}", stderr(&forced));
    let forced = stdout(&forced);
    assert!(forced.contains("\u{1b}["), "{forced:?}");
    assert!(forced.contains('✓'), "{forced:?}");

    let states = directory.write("states.tes", EXPLANATION_STATES_SOURCE);
    let forced_states = tess_with_forced_color(&["run", path(&states)]);
    assert_eq!(forced_states.status.code(), Some(1));
    let forced_states = stdout(&forced_states);
    for (code, meaning) in [
        ("\u{1b}[32m", "resolved"),
        ("\u{1b}[33m", "undefined/unknown"),
        ("\u{1b}[31m", "conflict"),
    ] {
        assert!(
            forced_states.contains(code),
            "missing {meaning} color in {forced_states:?}"
        );
    }

    let no_color = tess_with_no_color_and_force(&arguments);
    assert_eq!(no_color.status.code(), Some(0), "{}", stderr(&no_color));
    assert!(!stdout(&no_color).contains("\u{1b}["));

    let compact =
        tess_with_forced_color(&["run", path(&source), "--test", "yes_case", "--compact"]);
    assert_eq!(stdout(&compact), "outcome(s) = Answer.Yes\n");

    let json = tess_with_forced_color(&["run", path(&source), "--test", "yes_case", "--json"]);
    assert!(!stdout(&json).contains("\u{1b}["));
    let _: Value = serde_json::from_slice(&json.stdout).unwrap();

    let verify_arguments = ["verify", path(&source), "--assert", "total"];
    let automatic = tess_with_automatic_color(&verify_arguments);
    assert_eq!(automatic.status.code(), Some(0), "{}", stderr(&automatic));
    assert!(!stdout(&automatic).contains("\u{1b}["));

    let forced = tess_with_forced_color(&verify_arguments);
    assert_eq!(forced.status.code(), Some(0), "{}", stderr(&forced));
    let forced = stdout(&forced);
    assert!(forced.contains("\u{1b}[32m"), "{forced:?}");
    assert!(forced.contains('✓'), "{forced:?}");

    let broken = directory.write("broken.tes", BROKEN_ANALYSIS_SOURCE);
    let failed = tess_with_forced_color(&["verify", path(&broken), "--assert", "total"]);
    assert_eq!(failed.status.code(), Some(1));
    assert!(stdout(&failed).contains("\u{1b}[31m"));

    let inconclusive = tess_with_forced_color(&[
        "verify",
        path(&source),
        "--assert",
        "total",
        "--max-evaluations",
        "1",
        "--solver",
        "off",
    ]);
    assert_eq!(inconclusive.status.code(), Some(1));
    let inconclusive = stdout(&inconclusive);
    assert!(inconclusive.contains("\u{1b}[33m"), "{inconclusive:?}");
    assert!(inconclusive.contains('?'), "{inconclusive:?}");

    let no_color = tess_with_no_color_and_force(&verify_arguments);
    assert_eq!(no_color.status.code(), Some(0));
    assert!(!stdout(&no_color).contains("\u{1b}["));

    let json = tess_with_forced_color(&["verify", path(&source), "--assert", "total", "--json"]);
    assert!(!stdout(&json).contains("\u{1b}["));
    let _: Value = serde_json::from_slice(&json.stdout).unwrap();
}

#[test]
fn bare_run_uses_declared_expectations_and_bare_explain_uses_the_only_case() {
    let directory = TestDirectory::new();
    let source = directory.write("valid.tes", VALID_SOURCE);

    let output = tess(&["run", path(&source)]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let output = stdout(&output);
    assert!(output.contains("outcome(s) = Answer.Yes"), "{output}");
    assert!(output.contains("yes_case"), "{output}");
    assert!(output.contains("yes"), "{output}");

    let output = tess(&["explain", path(&source)]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let output = stdout(&output);
    assert!(output.contains("outcome(s) = Answer.Yes"), "{output}");
    assert!(output.contains("yes_case"), "{output}");
    assert!(output.contains("yes"), "{output}");
}

#[test]
fn interactive_run_reads_stdin_prompts_on_stderr_and_prints_the_result_on_stdout() {
    let directory = TestDirectory::new();
    let source = directory.write("interactive.tes", INTERACTIVE_SOURCE);

    let output = tess_with_stdin(
        &[
            "run",
            path(&source),
            "--interactive",
            "--query",
            "outcome(s)",
        ],
        b"false\n",
    );

    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let stdout = stdout(&output);
    let stderr = stderr(&output);
    assert!(stdout.contains("outcome(s) = Answer.No"), "{stdout}");
    assert!(stdout.contains("reason rule `no` produced"), "{stdout}");
    assert!(!stdout.contains("interactive ·"), "{stdout}");
    assert!(!stdout.contains("s.enabled"), "{stdout}");
    assert!(stderr.contains("interactive · outcome(s)"), "{stderr}");
    assert!(stderr.contains("s.enabled (Bool)"), "{stderr}");
    assert!(!stderr.contains("s.detail"), "{stderr}");
    assert!(!stderr.contains("s.unused"), "{stderr}");
    assert!(!stderr.contains("Answer.No"), "{stderr}");
}

#[test]
fn interactive_run_prints_compile_warnings_before_collecting_sensitive_input() {
    let directory = TestDirectory::new();
    let source = directory.write(
        "warning.tes",
        r"mod warning

enum Answer:
    Yes
    No

record Subject:
    flag: Bool

dec outcome(s Subject): Answer

rule always_yes(s Subject):
    : outcome(s) = Yes

rule maybe_no(s Subject):
    not s.flag: outcome(s) = No
",
    );

    let output = tess_with_stdin(&["run", path(&source), "--interactive"], b":quit\n");

    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert!(output.stdout.is_empty(), "{}", stdout(&output));
    let stderr = stderr(&output);
    let warning = stderr.find("warning[W0401]").expect("compiler warning");
    let prompt = stderr
        .find("interactive · outcome(s)")
        .expect("questionnaire");
    assert!(warning < prompt, "{stderr}");
    assert!(stderr.contains("cancelled"), "{stderr}");
}

#[test]
fn korean_law_command_entries_validate_and_run_as_named_questionnaires() {
    let root = workspace_root();
    let project = root.join("examples/projects/korean-law");
    let noise = root.join("examples/projects/korean-law/cmd/층간소음.tes");
    let criminal = root.join("examples/projects/korean-law/cmd/형사검토.tes");

    for command in [&noise, &criminal] {
        let output = tess(&["validate", path(command)]);
        assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    }

    let output = tess_with_stdin(&["run", path(&criminal), "--interactive"], b":quit\n");
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert!(output.stdout.is_empty(), "{}", stdout(&output));
    let prompt = stderr(&output);
    assert!(
        prompt.contains("interactive · 형사검토(표현주장)"),
        "{prompt}"
    );
    assert!(!prompt.contains("Select a decision"), "{prompt}");

    let output = tess_with_stdin(&["run", path(&noise), "--interactive"], b"false\n");
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let result = stdout(&output);
    assert!(result.contains("규칙상_층간소음범위비해당"), "{result}");
    let prompt = stderr(&output);
    assert!(prompt.contains("층간소음사건.공동주택"), "{prompt}");
    assert!(!prompt.contains("층간소음사건.입주자등활동"), "{prompt}");

    let output = tess(&["test", path(&project)]);
    assert_eq!(output.status.code(), Some(0), "{}", stdout(&output));
    assert!(
        stdout(&output).contains("0 unresolved"),
        "{}",
        stdout(&output)
    );

    let scenarios = [
        (
            project.join("inputs/insult-claim.json"),
            "형사검토(표현주장)",
            "제311조_적용후보",
        ),
        (
            project.join("inputs/false-online-defamation.json"),
            "형사검토(표현주장)",
            "정보통신망법70조제2항_현행법적용후보",
        ),
        (
            project.join("inputs/public-interest-review.json"),
            "공익성요소(표현주장)",
            "필요정보한정_지지",
        ),
        (
            project.join("inputs/night-noise.json"),
            "층간소음검토(층간소음사건)",
            "직접충격_최고소음기준초과",
        ),
    ];
    for (input, query, expected) in scenarios {
        let output = tess(&[
            "run",
            path(&project),
            "--input",
            path(&input),
            "--query",
            query,
            "--json",
        ]);
        assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
        let json: Value = serde_json::from_slice(&output.stdout).unwrap();
        assert_eq!(json["result"]["status"], "resolved", "{json}");
        assert!(
            json["result"]["values"]
                .as_array()
                .is_some_and(|values| values.iter().any(|value| value == expected)),
            "missing {expected} in {json}"
        );
    }
}

#[test]
fn batch_rejects_modes_that_select_a_single_evaluation() {
    let directory = TestDirectory::new();
    let source = directory.write("valid.tes", VALID_SOURCE);

    for arguments in [
        vec!["run", path(&source), "--batch", "--interactive"],
        vec!["run", path(&source), "--batch", "--query", "outcome(s)"],
        vec!["run", path(&source), "--batch", "--test", "yes_case"],
    ] {
        let output = tess(&arguments);
        assert_eq!(output.status.code(), Some(2), "{}", stderr(&output));
        assert!(
            stderr(&output).contains("cannot be used with"),
            "{}",
            stderr(&output)
        );
    }

    let output = tess(&["explain", path(&source), "--batch"]);
    assert_eq!(output.status.code(), Some(2), "{}", stderr(&output));
    assert!(
        stderr(&output).contains("unexpected argument '--batch'"),
        "{}",
        stderr(&output)
    );
}

#[test]
fn bare_run_evaluates_every_case_and_expectation_in_stable_order() {
    let directory = TestDirectory::new();
    let source = directory.write("batch.tes", BATCH_RUN_SOURCE);

    let output = tess(&["run", path(&source)]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let output = stdout(&output);
    let explicit_batch = tess(&["run", path(&source), "--batch"]);
    assert_eq!(
        explicit_batch.status.code(),
        Some(0),
        "{}",
        stderr(&explicit_batch)
    );
    assert_eq!(stdout(&explicit_batch), output);
    let a_case = output.find("a_case").expect("a_case explanation");
    let z_case = output.find("z_case").expect("z_case explanation");
    assert!(a_case < z_case, "{output}");
    assert_eq!(output.matches("a_case").count(), 1, "{output}");
    assert_eq!(output.matches("z_case").count(), 1, "{output}");
    assert_eq!(output.matches("reason rule").count(), 4, "{output}");
    assert!(output.contains("\n\nz_case\n"), "{output}");
    assert!(!output.contains("let s = Subject"), "{output}");
    assert!(!output.contains("-->"), "{output}");
    assert!(output.contains("primary(s) = Answer.No"), "{output}");
    assert!(output.contains("primary(s) = Answer.Yes"), "{output}");
    assert!(output.contains("review(s) = Answer.Yes"), "{output}");

    let output = tess(&["run", path(&source), "--compact"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert_eq!(
        stdout(&output),
        "a_case:\n  primary(s) = Answer.No\n  review(s) = Answer.Yes\n\nz_case:\n  primary(s) = Answer.Yes\n  review(s) = Answer.Yes\n"
    );

    let output = tess(&["run", path(&source), "--json"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let json: Value = serde_json::from_slice(&output.stdout).unwrap();
    assert_eq!(json["ok"], true);
    assert_eq!(json["result"]["cases"][0]["case"], "a_case");
    assert_eq!(json["result"]["cases"][1]["case"], "z_case");
    assert_eq!(
        json["result"]["cases"][0]["evaluations"]
            .as_array()
            .unwrap()
            .len(),
        2
    );
    assert_eq!(
        json["result"]["cases"][0]["evaluations"][0]["values"][0],
        "No"
    );
    assert!(
        json["result"]["cases"][0]["evaluations"][0]
            .get("rules")
            .is_none()
    );

    let output = tess(&["run", path(&source), "--test", "z_case"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let output = stdout(&output);
    assert!(output.contains("primary(s) = Answer.Yes"), "{output}");
    assert!(output.contains("primary_yes"), "{output}");

    let output = tess(&["run", path(&source), "--test", "z_case", "--compact"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert_eq!(stdout(&output), "primary(s) = Answer.Yes\n");

    let output = tess(&[
        "run",
        path(&source),
        "--test",
        "z_case",
        "--query",
        "review(s)",
    ]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let output = stdout(&output);
    assert!(output.contains("review(s) = Answer.Yes"), "{output}");
    assert!(output.contains("review_all"), "{output}");

    let output = tess(&[
        "run",
        path(&source),
        "--test",
        "z_case",
        "--query",
        "review(s)",
        "--compact",
    ]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert_eq!(stdout(&output), "review(s) = Answer.Yes\n");
}

#[test]
fn bare_run_exit_status_depends_on_evaluation_not_expectation_comparison() {
    let directory = TestDirectory::new();
    let resolved = directory.write("resolved.tes", BATCH_RUN_SOURCE);
    let output = tess(&["run", path(&resolved)]);
    assert_eq!(
        output.status.code(),
        Some(0),
        "resolved values should succeed even when the case's expected values differ"
    );

    let unresolved_source = BATCH_RUN_SOURCE.replace(
        "rule review_all(s Subject):\n    : review(s) = Yes",
        "rule review_all(s Subject):\n    false: review(s) = Yes",
    );
    let unresolved = directory.write("unresolved.tes", &unresolved_source);
    let output = tess(&["run", path(&unresolved)]);
    assert_eq!(output.status.code(), Some(1));
    let output = stdout(&output);
    assert!(output.contains("primary(s) = Answer.No"), "{output}");
    assert!(output.contains("primary(s) = Answer.Yes"), "{output}");
    assert!(output.contains("review(s) = undefined"), "{output}");
}

#[test]
fn detailed_batch_run_explains_resolved_undefined_unknown_conflict_and_override() {
    let directory = TestDirectory::new();
    let source = directory.write("states.tes", EXPLANATION_STATES_SOURCE);

    let output = tess(&["run", path(&source), "--verbose"]);
    assert_eq!(output.status.code(), Some(1), "{}", stderr(&output));
    let output = stdout(&output);

    let resolved = output
        .find("resolved(s) = Answer.Yes")
        .expect("resolved result");
    let undefined = output
        .find("empty(s) = undefined")
        .expect("undefined result");
    let unknown = output
        .find("uncertain(s) = unknown")
        .expect("unknown result");
    let conflict = output
        .find("disputed(s) = conflict")
        .expect("conflict result");
    let overridden = output
        .find("replaced(s) = Answer.Yes")
        .expect("override result");
    assert!(
        resolved < undefined && undefined < unknown && unknown < conflict && conflict < overridden,
        "{output}"
    );
    for evidence in [
        "resolved_yes",
        "uncertain_yes",
        "s.maybe_flag",
        "disputed_yes",
        "disputed_no",
        "replaced_base",
        "replaced_exception",
    ] {
        assert!(
            output.contains(evidence),
            "missing `{evidence}` in:\n{output}"
        );
    }
    assert_eq!(output.matches("all_states").count(), 1, "{output}");
    assert_eq!(output.matches("let s = Subject {").count(), 1, "{output}");
    for status in [
        "  ✓ resolved(s) = Answer.Yes",
        "  ○ empty(s) = undefined",
        "  ? uncertain(s) = unknown",
        "  ✗ disputed(s) = conflict [Answer.No, Answer.Yes]",
        "  ✓ replaced(s) = Answer.Yes",
    ] {
        assert!(output.contains(status), "missing `{status}` in:\n{output}");
    }

    let compact = tess(&["run", path(&source), "--compact"]);
    assert_eq!(compact.status.code(), Some(1), "{}", stderr(&compact));
    assert_eq!(
        stdout(&compact),
        "resolved(s) = Answer.Yes\nempty(s) = undefined\nuncertain(s) = unknown\nmissing: s.maybe_flag\ndisputed(s) = conflict [Answer.No, Answer.Yes]\n  reason: different values remain after explicit overrides\nreplaced(s) = Answer.Yes\n"
    );
}

#[test]
fn detailed_run_marks_allowed_empty_results_as_resolved() {
    let directory = TestDirectory::new();
    let source = directory.write(
        "empty-results.tes",
        r"mod empty_results

enum Answer:
    Yes
record Subject:
    flag: Bool
dec maybe_answer(s Subject): Answer?
dec collection(s Subject): Answer*

test empty:
    let s = Subject { flag: false }
    expect maybe_answer(s) = Yes
    expect collection(s) = Yes
",
    );

    let output = tess(&["run", path(&source), "--verbose"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let output = stdout(&output);
    assert!(output.contains("  ✓ maybe_answer(s) = []"), "{output}");
    assert!(output.contains("  ✓ collection(s) = []"), "{output}");
    assert_eq!(output.matches("empty").count(), 1, "{output}");
    assert!(!output.contains("  ○ "), "{output}");
}

#[test]
fn detailed_run_merges_equal_support_and_reports_the_imported_rule_location() {
    let directory = TestDirectory::new();
    let rules = directory.write(
        "rules.tes",
        r"mod imported
rule first(s Subject):
    s.flag: outcome(s) = Yes
rule second(s Subject):
    s.flag: outcome(s) = Yes
",
    );
    let entry = directory.write(
        "entry.tes",
        r#"mod imported
use "rules.tes"
enum Answer:
    Yes
    No
record Subject:
    flag: Bool
dec outcome(s Subject): Answer
test c:
    let s = Subject { flag: true }
    expect outcome(s) = Yes
"#,
    );

    let output = tess(&["run", path(&entry), "--verbose"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let output = stdout(&output);
    assert!(output.contains("merged candidate `Answer.Yes`"), "{output}");
    assert!(
        output.contains("equal values are merged and count once"),
        "{output}"
    );
    assert!(
        output.contains(&format!("{}:", rules.display())),
        "{output}"
    );
    assert!(output.contains("rule `first`"), "{output}");
    assert!(output.contains("rule `second`"), "{output}");
}

#[test]
fn bare_run_reports_a_case_without_expectations() {
    let directory = TestDirectory::new();
    let source = directory.write(
        "empty-case.tes",
        &format!("{BROKEN_ANALYSIS_SOURCE}\ntest empty:\n    let s = Subject {{ flag: true }}\n"),
    );

    let output = tess(&["run", path(&source)]);
    assert_eq!(output.status.code(), Some(1));
    let error = stderr(&output);
    assert!(error.contains("error[C3003]"), "{error}");
    assert!(error.contains("test `empty` has no expectation"), "{error}");
}

#[test]
fn run_without_an_input_explains_how_to_choose_when_case_count_is_not_one() {
    let directory = TestDirectory::new();
    let no_cases = directory.write("no-cases.tes", BROKEN_ANALYSIS_SOURCE);
    let output = tess(&["run", path(&no_cases)]);
    assert_eq!(output.status.code(), Some(2));
    let error = stderr(&output);
    assert!(error.contains("no tests are declared"), "{error}");
    assert!(error.contains("--input JSON_FILE"), "{error}");

    let multiple_cases_source = format!(
        "{VALID_SOURCE}\ntest no_case:\n    let s = Subject {{ flag: false }}\n    expect outcome(s) = No\n"
    );
    let multiple_cases = directory.write("multiple-cases.tes", &multiple_cases_source);
    let output = tess(&["explain", path(&multiple_cases)]);
    assert_eq!(output.status.code(), Some(2));
    let error = stderr(&output);
    assert!(error.contains("multiple tests are declared"), "{error}");
    assert!(error.contains("`yes_case`"), "{error}");
    assert!(error.contains("`no_case`"), "{error}");
    assert!(error.contains("--test NAME"), "{error}");
    assert!(error.contains("--input JSON_FILE"), "{error}");
}

#[test]
fn run_accepts_a_bare_filename_from_the_current_directory() {
    let directory = TestDirectory::new();
    directory.write("valid.tes", VALID_SOURCE);

    let output = tess_in(&directory.path, &["run", "valid.tes", "--test", "yes_case"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let output = stdout(&output);
    assert!(output.contains("Yes"));
    assert!(!output.contains("-->"), "{output}");
    assert!(
        !output.contains(&directory.path.display().to_string()),
        "{output}"
    );

    let output = tess_in(
        &directory.path,
        &["run", "valid.tes", "--test", "yes_case", "--verbose"],
    );
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let output = stdout(&output);
    assert!(output.contains("--> valid.tes:"), "{output}");
    assert!(
        !output.contains(&directory.path.display().to_string()),
        "{output}"
    );
}

#[test]
fn run_accepts_json_input_and_requires_a_query_for_it() {
    let directory = TestDirectory::new();
    let source = directory.write("valid.tes", VALID_SOURCE);
    let input = directory.write("input.json", r#"{"flag":true}"#);
    let output = tess(&[
        "run",
        path(&source),
        "--input",
        path(&input),
        "--query",
        "outcome(s)",
        "--json",
    ]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let json: Value = serde_json::from_slice(&output.stdout).unwrap();
    assert_eq!(json["result"]["status"], "resolved");
    assert_eq!(json["result"]["values"][0], "Yes");
    assert!(json["result"].get("rules").is_none());

    let output = tess(&["run", path(&source), "--input", path(&input)]);
    assert_eq!(output.status.code(), Some(2));
    assert!(stderr(&output).contains("--query is required"));
}

#[test]
fn run_preserves_full_decimal_precision_in_json_numbers() {
    let directory = TestDirectory::new();
    let source = workspace_root().join("examples/expense-audit/expense.tes");
    let input = directory.write(
        "expense.json",
        r#"{
  "청구금액": 0.1234567890123456789012345679,
  "승인한도": 0.1234567890123456789012345678,
  "영수증첨부": true
}"#,
    );
    let output = tess(&[
        "run",
        path(&source),
        "--input",
        path(&input),
        "--query",
        "감사표시(e)",
        "--json",
    ]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let json: Value = serde_json::from_slice(&output.stdout).unwrap();
    assert_eq!(json["result"]["status"], "resolved");
    assert!(
        json["result"]["values"]
            .as_array()
            .is_some_and(|values| values.iter().any(|value| value == "승인한도초과")),
        "{}",
        stdout(&output)
    );
}

#[test]
fn compact_conflicts_with_json() {
    let directory = TestDirectory::new();
    let source = directory.write("valid.tes", VALID_SOURCE);

    for command in ["run", "explain"] {
        let output = tess(&[
            command,
            path(&source),
            "--test",
            "yes_case",
            "--compact",
            "--json",
        ]);
        assert_eq!(output.status.code(), Some(2));
        let error = stderr(&output);
        assert!(error.contains("--compact"), "{error}");
        assert!(error.contains("--json"), "{error}");
    }
}

#[test]
fn verbose_conflicts_with_compact_and_json() {
    let directory = TestDirectory::new();
    let source = directory.write("valid.tes", VALID_SOURCE);

    for command in ["run", "explain"] {
        for other in ["--compact", "--json"] {
            let output = tess(&[
                command,
                path(&source),
                "--test",
                "yes_case",
                "--verbose",
                other,
            ]);
            assert_eq!(output.status.code(), Some(2));
            let error = stderr(&output);
            assert!(error.contains("--verbose"), "{error}");
            assert!(error.contains(other), "{error}");
        }
    }
}

#[test]
fn repl_supports_piped_dynamic_input_and_queries() {
    let directory = TestDirectory::new();
    let source = directory.write("valid.tes", VALID_SOURCE);
    let script =
        b"help\n:test\n:set s.flag = false\noutcome(s)\n:explain\n:reset\noutcome(s)\nexit\n";

    let output = tess_with_stdin(&["repl", path(&source)], script);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let output = stdout(&output);
    assert!(output.contains("loaded sole test `yes_case`"), "{output}");
    assert!(output.contains("try: outcome(s)"), "{output}");
    assert!(output.contains("Press Tab once"), "{output}");
    assert!(output.contains("* yes_case (current)"), "{output}");
    assert!(output.contains("s.flag = false"), "{output}");
    assert!(output.contains("outcome(s) = Answer.No"), "{output}");
    assert!(output.contains("✓ outcome(s) = Answer.No"), "{output}");
    assert!(
        output.contains("selected candidate `Answer.No`"),
        "{output}"
    );
    assert!(output.contains("restored test `yes_case`"), "{output}");
    assert!(output.contains("outcome(s) = Answer.Yes"), "{output}");
}

#[test]
fn verify_distinguishes_proved_and_refuted_invariants() {
    let directory = TestDirectory::new();
    let valid = directory.write("valid.tes", VALID_SOURCE);
    let output = tess(&["verify", path(&valid), "--assert", "total"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert!(
        stdout(&output).contains("✓ total\n  proved for all inputs"),
        "{}",
        stdout(&output)
    );

    let broken = directory.write("broken.tes", BROKEN_ANALYSIS_SOURCE);
    let output = tess(&["verify", path(&broken), "--assert", "total"]);
    assert_eq!(output.status.code(), Some(1), "{}", stderr(&output));
    assert!(stdout(&output).contains("counterexample"));

    let output = tess(&["verify", path(&valid), "--max-evaluations", "0"]);
    assert_eq!(output.status.code(), Some(2));

    let output = tess(&["verify", path(&valid), "--max-evaluations", "100_000"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
}

#[test]
fn verify_reports_existential_witnesses_and_exact_no_witness_failures() {
    let _solver_guard = solver_test_guard();
    let directory = TestDirectory::new();
    let source = directory.write(
        "existential.tes",
        r"mod existential_cli

enum Answer:
    Yes
    No
record Subject:
    score: Int -100..100
dec outcome(s Subject): Answer

rule yes(s Subject):
    s.score > 10: outcome(s) = Yes

rule no(s Subject):
    s.score <= 10: outcome(s) = No

assert some reachable_yes(s Subject):
    s.score > 0: outcome(s) = Yes

assert some unreachable_yes(s Subject):
    s.score <= 10: outcome(s) = Yes
",
    );

    let output = tess(&[
        "verify",
        path(&source),
        "--assert",
        "reachable_yes",
        "--solver",
        "z3",
    ]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let text = stdout(&output);
    assert!(
        text.contains("satisfying input found · exact solver (Z3)"),
        "{text}"
    );
    assert!(text.contains("witness"), "{text}");
    assert!(text.contains("s: Subject {"), "{text}");

    let output = tess(&[
        "verify",
        path(&source),
        "--assert",
        "reachable_yes",
        "--solver",
        "z3",
        "--json",
    ]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let report: Value = serde_json::from_slice(&output.stdout).unwrap();
    let invariant = &report["result"]["invariants"][0];
    assert_eq!(invariant["quantifier"], "some");
    assert_eq!(invariant["verdict"], "passed");
    assert_eq!(invariant["completeness"], "solver_exact");
    assert_eq!(invariant["evaluated"], 1);
    assert_eq!(invariant["witness"]["bindings"]["s"]["entity"], "Subject");
    assert!(invariant["counterexamples"].as_array().unwrap().is_empty());

    let output = tess(&[
        "verify",
        path(&source),
        "--assert",
        "unreachable_yes",
        "--solver",
        "z3",
        "--json",
    ]);
    assert_eq!(output.status.code(), Some(1), "{}", stderr(&output));
    let report: Value = serde_json::from_slice(&output.stdout).unwrap();
    let invariant = &report["result"]["invariants"][0];
    assert_eq!(invariant["quantifier"], "some");
    assert_eq!(invariant["verdict"], "failed");
    assert_eq!(invariant["completeness"], "solver_exact");
    assert!(invariant.get("witness").is_none());
    assert!(invariant["counterexamples"].as_array().unwrap().is_empty());
}

#[test]
fn verify_covers_the_cartesian_product_of_multiple_quantified_entities() {
    let directory = TestDirectory::new();
    let source_text = r"mod multi_quantified

enum Answer:
    Free
    Paid
enum Tier:
    Standard
    Preferred

record Order:
    amount: Int 0..100_000
record Customer:
    tier: Tier

dec outcome(o Order, c Customer): Answer

rule amount_free(o Order, c Customer):
    o.amount >= 50_000: outcome(o, c) = Free

rule preferred_free(o Order, c Customer):
    c.tier = Preferred: outcome(o, c) = Free

rule standard_paid(o Order, c Customer):
    o.amount < 50_000 and c.tier = Standard: outcome(o, c) = Paid

assert total(o Order, c Customer):
    outcome(o, c)
";
    let valid = directory.write("multi-valid.tes", source_text);

    let output = tess(&["verify", path(&valid), "--assert", "total"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert!(
        stdout(&output).contains("proved for all inputs · 4 exact regions checked"),
        "{}",
        stdout(&output)
    );

    let output = tess(&["verify", path(&valid), "--assert", "total", "--json"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let report: Value = serde_json::from_slice(&output.stdout).unwrap();
    assert_eq!(report["command"], "verify");
    assert!(report["result"].get("checks").is_none());
    let invariant = &report["result"]["invariants"][0];
    assert_eq!(invariant["invariant"], "total");
    assert_eq!(invariant["planned_evaluations"], 4);
    assert_eq!(invariant["evaluated"], 4);
    assert_eq!(invariant["completeness"], "threshold_partitioned");
    assert_eq!(invariant["verdict"], "passed");
    for removed_key in ["check", "candidate_combinations", "explored"] {
        assert!(
            invariant.get(removed_key).is_none(),
            "old key `{removed_key}` survived"
        );
    }

    let broken_text = source_text.replace(
        "o.amount < 50_000 and c.tier = Standard",
        "o.amount < 50_000 and c.tier = Preferred",
    );
    let broken = directory.write("multi-broken.tes", &broken_text);
    let output = tess(&["verify", path(&broken), "--assert", "total"]);
    assert_eq!(output.status.code(), Some(1), "{}", stderr(&output));
    let output = stdout(&output);
    assert!(output.contains("counterexample · undefined"), "{output}");
    assert!(output.contains("c: Customer {"), "{output}");
    assert!(output.contains("o: Order {"), "{output}");
}

#[test]
fn verify_uses_z3_for_relational_integer_gaps_without_false_passes() {
    let _solver_guard = solver_test_guard();
    let directory = TestDirectory::new();
    let source_text = r"mod relational_gap

enum Shipping:
    Free
    Paid

record Order:
    amount: Int 0..100_000
record Coupon:
    discount: Int 0..100_000

dec shipping(o Order, c Coupon): Shipping

rule free(o Order, c Coupon):
    o.amount - c.discount > 50_000: shipping(o, c) = Free

rule paid(o Order, c Coupon):
    o.amount - c.discount < 50_000: shipping(o, c) = Paid

assert total(o Order, c Coupon):
    shipping(o, c)
";
    let broken = directory.write("relational-gap.tes", source_text);

    let output = tess(&[
        "verify",
        path(&broken),
        "--assert",
        "total",
        "--solver",
        "off",
        "--json",
    ]);
    assert_eq!(output.status.code(), Some(1), "{}", stderr(&output));
    let report: Value = serde_json::from_slice(&output.stdout).unwrap();
    let invariant = &report["result"]["invariants"][0];
    assert_eq!(invariant["verdict"], "failed");
    let counterexample = &invariant["counterexamples"][0];
    assert_eq!(counterexample["invariant"], "total");
    assert_eq!(counterexample["kind"], "undefined");
    assert!(counterexample.get("check").is_none());
    assert!(invariant.get("solver").is_none());

    let fixed_text = source_text.replace(
        "o.amount - c.discount > 50_000",
        "o.amount - c.discount >= 50_000",
    );
    let fixed = directory.write("relational-fixed.tes", &fixed_text);
    let output = tess(&[
        "verify",
        path(&fixed),
        "--assert",
        "total",
        "--solver",
        "off",
        "--json",
    ]);
    assert_eq!(output.status.code(), Some(1), "{}", stderr(&output));
    let report: Value = serde_json::from_slice(&output.stdout).unwrap();
    let invariant = &report["result"]["invariants"][0];
    assert_eq!(invariant["verdict"], "inconclusive");
    assert_ne!(invariant["completeness"], "solver_exact");
    assert!(invariant.get("solver").is_none());

    let output = tess_without_path(&[
        "verify",
        path(&broken),
        "--assert",
        "total",
        "--solver",
        "z3",
    ]);
    assert_eq!(output.status.code(), Some(1), "{}", stderr(&output));
    let text = stdout(&output);
    assert!(
        text.contains("✗ total\n  counterexample found · exact solver (Z3)"),
        "{text}"
    );
    assert!(text.contains("counterexample · undefined"), "{text}");
    assert!(!text.contains("solver_exact"), "{text}");
    assert!(!text.contains("negated property"), "{text}");

    let output = tess(&[
        "verify",
        path(&broken),
        "--assert",
        "total",
        "--solver",
        "z3",
        "--json",
    ]);
    assert_eq!(output.status.code(), Some(1), "{}", stderr(&output));
    let report: Value = serde_json::from_slice(&output.stdout).unwrap();
    let invariant = &report["result"]["invariants"][0];
    assert_eq!(invariant["verdict"], "failed");
    assert_eq!(invariant["completeness"], "solver_exact");
    assert_eq!(invariant["evaluated"], 1);
    assert_eq!(invariant["planned_evaluations"], 0);
    assert_eq!(invariant["solver"]["backend"], "z3");
    assert_eq!(invariant["solver"]["logic"], "QF_LIA");
    assert!(
        invariant["notes"][0]
            .as_str()
            .is_some_and(|note| note.contains("model was replayed"))
    );
    assert!(
        invariant["solver"]["version"]
            .as_str()
            .is_some_and(|version| !version.is_empty())
    );
    let bindings = &invariant["counterexamples"][0]["input"]["bindings"];
    let amount = bindings["o"]["fields"]["amount"]["value"].as_i64().unwrap();
    let discount = bindings["c"]["fields"]["discount"]["value"]
        .as_i64()
        .unwrap();
    assert_eq!(amount - discount, 50_000);

    let output = tess(&[
        "verify",
        path(&fixed),
        "--assert",
        "total",
        "--solver",
        "z3",
        "--json",
    ]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let report: Value = serde_json::from_slice(&output.stdout).unwrap();
    let invariant = &report["result"]["invariants"][0];
    assert_eq!(invariant["verdict"], "passed");
    assert_eq!(invariant["completeness"], "solver_exact");
    assert_eq!(invariant["evaluated"], 0);
    assert_eq!(invariant["planned_evaluations"], 0);
    assert_eq!(invariant["solver"]["backend"], "z3");
    assert!(
        invariant["notes"][0]
            .as_str()
            .is_some_and(|note| note.contains("negated property is unsatisfiable"))
    );
}

#[test]
fn every_verifiable_example_uses_a_compact_exact_strategy() {
    let _solver_guard = solver_test_guard();
    let root = workspace_root();
    let targets = [
        ("examples/course-grading/course.tes", 0),
        ("examples/course-grading/broken-exception.tes", 1),
        ("examples/course-grading/broken-gap.tes", 1),
        ("examples/course-grading/broken-overlap.tes", 1),
        ("examples/course-grading/fixed-exception.tes", 0),
        ("examples/creator-payout/payout.tes", 0),
        ("examples/expense-audit/expense.tes", 0),
        ("examples/incident-response/incident.tes", 0),
        ("examples/projects/package-consumer", 0),
        ("examples/projects/shipping-policy", 0),
        ("examples/schedule-conflicts/conflicts.tes", 0),
        ("examples/tutorial/13-assert-all-inputs.tes", 0),
        ("examples/tutorial/14-find-a-gap.tes", 1),
        ("examples/tutorial/15-multiple-inputs.tes", 0),
        ("examples/tutorial/16-relational-gap.tes", 1),
    ];

    for (relative, expected_exit) in targets {
        let target = root.join(relative);
        let output = tess(&["verify", path(&target), "--json"]);
        assert_eq!(
            output.status.code(),
            Some(expected_exit),
            "{relative}\nstdout: {}\nstderr: {}",
            stdout(&output),
            stderr(&output)
        );
        let report: Value = serde_json::from_slice(&output.stdout).unwrap();
        let invariants = report["result"]["invariants"].as_array().unwrap();
        assert!(!invariants.is_empty(), "{relative}");
        for invariant in invariants {
            if invariant["quantifier"] == "some" && invariant["verdict"] == "passed" {
                assert!(
                    invariant["witness"].is_object(),
                    "{relative}: existential success omitted its witness: {invariant}"
                );
            } else {
                assert!(
                    matches!(
                        invariant["completeness"].as_str(),
                        Some("threshold_partitioned" | "solver_exact")
                    ),
                    "{relative}: {invariant}"
                );
            }
            assert_ne!(invariant["verdict"], "inconclusive", "{relative}");
        }
    }
}

#[test]
fn workflow_examples_run_bounded_traces_and_support_trace_selection() {
    let root = workspace_root();
    for (relative, trace_name, bound, reachable_states) in [
        (
            "examples/order-lifecycle/lifecycle.tes",
            "every_order_settles",
            4,
            8,
        ),
        (
            "examples/deployment-rollout/rollout.tes",
            "every_rollout_settles_safely",
            3,
            6,
        ),
        (
            "examples/railway-crossing/crossing.tes",
            "crossing_stays_safe",
            10,
            5,
        ),
        (
            "examples/escrow-transfer/transfer.tes",
            "funds_are_conserved",
            2,
            4,
        ),
    ] {
        let target = root.join(relative);
        let output = tess(&["verify", path(&target), "--trace", trace_name, "--json"]);
        assert_eq!(
            output.status.code(),
            Some(0),
            "{relative}: {}",
            stderr(&output)
        );
        let report: Value = serde_json::from_slice(&output.stdout).unwrap();
        assert!(
            report["result"]["invariants"]
                .as_array()
                .unwrap()
                .is_empty()
        );
        let traces = report["result"]["traces"].as_array().unwrap();
        assert_eq!(traces.len(), 1, "{relative}");
        let trace = &traces[0];
        assert_eq!(trace["trace"], trace_name, "{relative}");
        assert_eq!(trace["verdict"], "passed", "{relative}");
        assert_eq!(trace["completeness"], "bounded_exhaustive", "{relative}");
        assert_eq!(trace["bound"], bound, "{relative}");
        assert_eq!(trace["reachable_states"], reachable_states, "{relative}");
    }

    let target = root.join("examples/order-lifecycle/lifecycle.tes");
    let missing = tess(&["verify", path(&target), "--trace", "missing", "--json"]);
    assert_eq!(missing.status.code(), Some(1));
    let report: Value = serde_json::from_slice(&missing.stdout).unwrap();
    assert_eq!(report["diagnostics"][0]["code"], "C2002");
}

#[test]
fn local_path_packages_enforce_exports_and_use_qualified_aliases() {
    let directory = TestDirectory::new();
    directory.write(
        "common/tess.toml",
        "[project]\nname = \"common\"\nentry = \"src/main.tes\"\n\
         [exports]\nsymbols = [\"Answer\", \"Subject\", \"outcome\"]\n",
    );
    directory.write(
        "common/src/main.tes",
        r"mod common

enum Answer:
    Yes
    No

record Subject:
    enabled: Bool

dec outcome(subject Subject): Answer

rule enabled(subject Subject):
    subject.enabled: outcome(subject) = Yes

rule disabled(subject Subject):
    not subject.enabled: outcome(subject) = No
",
    );
    directory.write(
        "app/tess.toml",
        "[project]\nname = \"app\"\nentry = \"src/main.tes\"\n\
         [dependencies.common]\npath = \"../common\"\n\
         symbols = [\"Answer\", \"Subject\", \"outcome\"]\n",
    );
    directory.write(
        "app/src/main.tes",
        r"mod app

test imported_rule_bundle:
    let subject = common.Subject { enabled: true }
    expect common.outcome(subject) = Yes

assert imported_policy_is_total(subject common.Subject):
    common.outcome(subject)
",
    );
    let app = directory.path.join("app");
    let lock = tess(&["lock", path(&app)]);
    assert_eq!(lock.status.code(), Some(0), "{}", stderr(&lock));
    for command in ["validate", "test", "verify"] {
        let output = tess(&[command, path(&app), "--json"]);
        assert_eq!(
            output.status.code(),
            Some(0),
            "{command}\nstdout: {}\nstderr: {}",
            stdout(&output),
            stderr(&output)
        );
    }
    let dependency_source = directory.path.join("common/src/main.tes");
    let dependency_before = fs::read_to_string(&dependency_source).unwrap();
    let output = tess(&["fmt", path(&app)]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert_eq!(
        fs::read_to_string(&dependency_source).unwrap(),
        dependency_before,
        "formatting a consumer must not rewrite a path dependency"
    );

    directory.write(
        "bad/tess.toml",
        "[project]\nname = \"bad\"\nentry = \"main.tes\"\n\
         [dependencies.common]\npath = \"../common\"\n\
         symbols = [\"private_helper\"]\n",
    );
    directory.write("bad/main.tes", "mod bad\n");
    let output = tess(&["validate", path(&directory.path.join("bad")), "--json"]);
    assert_eq!(output.status.code(), Some(2));
    assert!(stderr(&output).contains("does not export requested symbol"));
}

#[test]
fn transitive_local_packages_honor_versions_and_the_checked_in_lock() {
    let directory = TestDirectory::new();
    directory.write(
        "utility/tess.toml",
        "[project]\nname = \"utility\"\nversion = \"1.3.0\"\nentry = \"main.tes\"\n\
         [exports]\nsymbols = [\"allowed\"]\n",
    );
    directory.write(
        "utility/main.tes",
        r"mod utility

fn allowed(enabled Bool) Bool:
    enabled
",
    );
    directory.write(
        "policy/tess.toml",
        "[project]\nname = \"policy\"\nversion = \"2.0.1\"\nentry = \"main.tes\"\n\
         [exports]\nsymbols = [\"Answer\", \"Subject\", \"outcome\"]\n\
         [dependencies.utility]\npath = \"../utility\"\nversion = \"^1.0\"\nsymbols = [\"allowed\"]\n",
    );
    directory.write(
        "policy/main.tes",
        r"mod policy

enum Answer:
    Yes
    No

record Subject:
    enabled: Bool

dec outcome(subject Subject): Answer

rule enabled(subject Subject):
    utility.allowed(subject.enabled): outcome(subject) = Yes

rule disabled(subject Subject):
    not utility.allowed(subject.enabled): outcome(subject) = No
",
    );
    directory.write(
        "app/tess.toml",
        "[project]\nname = \"app\"\nversion = \"1.0.0\"\nentry = \"main.tes\"\n\
         [dependencies.policy]\npath = \"../policy\"\nversion = \"~2.0\"\n\
         symbols = [\"Answer\", \"Subject\", \"outcome\"]\n",
    );
    directory.write(
        "app/main.tes",
        r"mod app

test transitive_policy_runs:
    let subject = policy.Subject { enabled: true }
    expect policy.outcome(subject) = Yes
",
    );
    let app = directory.path.join("app");
    let missing = tess(&["validate", path(&app)]);
    assert_eq!(missing.status.code(), Some(2));
    assert!(stderr(&missing).contains("tess lock"));
    assert!(!app.join("tess.lock").exists());

    let generated = tess(&["lock", path(&app)]);
    assert_eq!(
        generated.status.code(),
        Some(0),
        "stdout: {}\nstderr: {}",
        stdout(&generated),
        stderr(&generated)
    );
    let output = tess(&["test", path(&app), "--json"]);
    assert_eq!(
        output.status.code(),
        Some(0),
        "stdout: {}\nstderr: {}",
        stdout(&output),
        stderr(&output)
    );
    let lock_path = app.join("tess.lock");
    let lock = fs::read_to_string(&lock_path).unwrap();
    assert!(lock.contains("lock-version = 1"));
    assert!(lock.contains(
        "alias = \"policy\", requirement = \"~2.0\", manifest = \"../policy/tess.toml\", symbols = [\"Answer\", \"Subject\", \"outcome\"]"
    ));
    assert!(lock.contains(
        "alias = \"utility\", requirement = \"^1.0\", manifest = \"../utility/tess.toml\", symbols = [\"allowed\"]"
    ));

    let second = tess(&["validate", path(&app), "--json"]);
    assert_eq!(second.status.code(), Some(0), "{}", stderr(&second));
    assert_eq!(fs::read_to_string(&lock_path).unwrap(), lock);

    fs::write(&lock_path, "lock-version = 999\n").unwrap();
    let stale = tess(&["validate", path(&app)]);
    assert_eq!(stale.status.code(), Some(2));
    assert!(stderr(&stale).contains("out of date"));
    let updated = tess(&["lock", path(&app)]);
    assert_eq!(updated.status.code(), Some(0), "{}", stderr(&updated));
    assert_eq!(fs::read_to_string(&lock_path).unwrap(), lock);
}

#[test]
fn graph_loads_projects_and_renders_stable_dot_and_filtered_json() {
    let directory = TestDirectory::new();
    let project = directory.path.join("graph-project");
    directory.write(
        "graph-project/tess.toml",
        "[project]\nname = \"graph-project\"\nentry = \"main.tes\"\n",
    );
    directory.write(
        "graph-project/main.tes",
        "mod policy\nuse \"model.tes\"\nuse \"rules.tes\"\n",
    );
    directory.write(
        "graph-project/model.tes",
        r"mod policy

enum Answer:
    Yes
    No
record Subject:
    enabled: Bool
dec outcome(s Subject): Answer
dec audit(s Subject): Bool*

policy.unused@Unused:
    Unused
",
    );
    directory.write(
        "graph-project/rules.tes",
        r#"mod policy

policy.statute@Statute:
    Policy "A", section 4.2.

    rule base(s Subject):
        s.enabled: outcome(s) = Yes

policy.memo@Supporting Memo:
    Supporting
    Memo

    rule exception(s Subject):
        not s.enabled: outcome(s) = No

    rule exception_override(s Subject):
        not s.enabled: override policy.statute.base

rule audit_rule(s Subject):
    s.enabled: audit(s) = true
"#,
    );

    let first = tess(&["graph", path(&project)]);
    assert_eq!(first.status.code(), Some(0), "{}", stderr(&first));
    let dot = stdout(&first);
    assert!(
        dot.starts_with("digraph policy {\n  rankdir=LR;\n"),
        "{dot}"
    );
    assert!(dot.contains("Statute"), "{dot}");
    assert!(dot.contains("Supporting Memo"), "{dot}");
    assert!(dot.contains("[label=\"overrides\"]"), "{dot}");
    assert!(dot.contains("[label=\"based_on\"]"), "{dot}");
    let second = tess(&["graph", path(&project), "--format", "dot"]);
    assert_eq!(first.stdout, second.stdout);

    let output = tess(&[
        "graph",
        path(&project),
        "--decision",
        "outcome",
        "--format",
        "json",
    ]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert!(output.stderr.is_empty());
    let graph: Value = serde_json::from_slice(&output.stdout).unwrap();
    assert_eq!(graph["schema_version"], 3);
    assert_eq!(graph["module"], "policy");
    assert_eq!(graph["decision"], "outcome");
    let ids = graph["nodes"]
        .as_array()
        .unwrap()
        .iter()
        .map(|node| node["id"].as_str().unwrap())
        .collect::<Vec<_>>();
    assert_eq!(
        ids,
        [
            "decision:outcome",
            "fragment:policy.memo",
            "fragment:policy.statute",
            "rule:policy.memo.exception",
            "rule:policy.memo.exception_override",
            "rule:policy.statute.base",
        ]
    );
    assert_eq!(graph["edges"].as_array().unwrap().len(), 6);
    assert!(
        graph["edges"]
            .as_array()
            .unwrap()
            .iter()
            .any(|edge| edge["kind"] == "based_on")
    );

    let baseline_output = tess(&["graph", path(&project), "--format", "json"]);
    assert_eq!(baseline_output.status.code(), Some(0));
    let baseline = directory.path.join("policy-graph.json");
    fs::write(&baseline, &baseline_output.stdout).unwrap();
    let unchanged = tess(&["graph", path(&project), "--baseline", path(&baseline)]);
    assert_eq!(unchanged.status.code(), Some(0), "{}", stderr(&unchanged));
    assert_eq!(stdout(&unchanged), "policy graph matches baseline\n");
    let rules = project.join("rules.tes");
    let changed = fs::read_to_string(&rules)
        .unwrap()
        .replace("Policy \"A\", section 4.2.", "Policy \"B\", section 4.2.");
    fs::write(&rules, changed).unwrap();

    let impact = tess(&["graph", path(&project), "--baseline", path(&baseline)]);
    assert_eq!(impact.status.code(), Some(1), "{}", stderr(&impact));
    let impact_text = stdout(&impact);
    assert!(
        impact_text.contains("text: policy.statute"),
        "{impact_text}"
    );
    assert!(impact_text.contains("review rules"), "{impact_text}");
    assert!(impact_text.contains("policy.statute.base"), "{impact_text}");
    assert!(impact_text.contains("review decisions"), "{impact_text}");
    assert!(!impact_text.contains("Policy \"B\""), "{impact_text}");

    let impact = tess(&[
        "graph",
        path(&project),
        "--baseline",
        path(&baseline),
        "--format",
        "json",
    ]);
    assert_eq!(impact.status.code(), Some(1), "{}", stderr(&impact));
    let impact: Value = serde_json::from_slice(&impact.stdout).unwrap();
    assert_eq!(impact["schema_version"], 2);
    assert_eq!(impact["review_functions"], serde_json::json!([]));
    assert_eq!(impact["fragments"][0]["kind"], "text");

    let unsupported = tess(&[
        "graph",
        path(&project),
        "--baseline",
        path(&baseline),
        "--format",
        "dot",
    ]);
    assert_eq!(unsupported.status.code(), Some(2));
    assert!(stderr(&unsupported).contains("supports `--format text` or `--format json`"));
}

#[test]
fn graph_reports_selector_language_failures_and_target_io_failures() {
    let directory = TestDirectory::new();
    let source = directory.write(
        "valid.tes",
        &VALID_SOURCE.replace("rule no(s Subject):", "rule no_rule(s Subject):"),
    );
    let output = tess(&[
        "graph",
        path(&source),
        "--decision",
        "missing",
        "--format",
        "json",
    ]);
    assert_eq!(output.status.code(), Some(1));
    assert!(output.stdout.is_empty());
    let error = stderr(&output);
    assert!(error.contains("error[C4001]"), "{error}");
    assert!(error.contains("available decisions: outcome"), "{error}");

    let invalid = directory.write("invalid.tes", "mod invalid\nenum E:\n    A B\n");
    let output = tess(&["graph", path(&invalid)]);
    assert_eq!(output.status.code(), Some(1));
    assert!(stderr(&output).contains("error[P0002]"));

    let output = tess(&["graph", path(&directory.path.join("missing.tes"))]);
    assert_eq!(output.status.code(), Some(2));
    assert!(stderr(&output).contains("could not read"));

    let output = tess(&["graph", path(&source), "--format", "text"]);
    assert_eq!(output.status.code(), Some(2));
    assert!(stderr(&output).contains("requires --baseline"));

    let malformed = directory.write("malformed-graph.json", "{not json}");
    let output = tess(&["graph", path(&source), "--baseline", path(&malformed)]);
    assert_eq!(output.status.code(), Some(2));
    assert!(stderr(&output).contains("invalid policy graph baseline"));
}

#[test]
fn fmt_check_stdout_and_in_place_modes_are_non_destructive_when_requested() {
    let directory = TestDirectory::new();
    let original = "# module docs\nmod m     # header\n\n# answers\nenum E:\n    A     # first\n    B     # enum end\n";
    let source = directory.write("format.tes", original);

    let output = tess(&["fmt", path(&source), "--check"]);
    assert_eq!(output.status.code(), Some(1));
    assert_eq!(fs::read_to_string(&source).unwrap(), original);

    let output = tess(&["fmt", path(&source), "--stdout"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert!(stdout(&output).contains("    A  # first\n    B  # enum end\n"));
    for comment in [
        "# module docs",
        "# header",
        "# answers",
        "# first",
        "# enum end",
    ] {
        assert!(stdout(&output).contains(comment));
    }
    assert_eq!(fs::read_to_string(&source).unwrap(), original);

    let output = tess(&["fmt", path(&source)]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let formatted = fs::read_to_string(&source).unwrap();
    assert!(formatted.contains("    A  # first\n    B  # enum end\n"));
    assert!(formatted.starts_with("# module docs\nmod m  # header\n"));
    let output = tess(&["fmt", path(&source), "--check"]);
    assert_eq!(output.status.code(), Some(0));
}

#[test]
fn io_and_usage_errors_exit_with_code_two() {
    let directory = TestDirectory::new();
    let missing = directory.path.join("missing.tes");
    let output = tess(&["validate", path(&missing)]);
    assert_eq!(output.status.code(), Some(2));
    assert!(stderr(&output).contains("could not read"));

    let source = directory.write("no-cases.tes", BROKEN_ANALYSIS_SOURCE);
    let output = tess(&["run", path(&source)]);
    assert_eq!(output.status.code(), Some(2));
    assert!(stderr(&output).contains("no tests are declared"));
}

#[test]
fn init_creates_a_working_multi_file_project() {
    let directory = TestDirectory::new();
    let project = directory.path.join("shipping-policy");
    let output = tess(&["init", path(&project)]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert!(stdout(&output).contains("tess validate ."));
    assert!(project.join("tess.toml").is_file());
    assert!(
        fs::read_to_string(project.join("tess.toml"))
            .unwrap()
            .contains("version = \"0.1.0\"")
    );
    assert!(project.join("src/main.tes").is_file());
    assert!(project.join("src/domain/request.tes").is_file());
    assert!(project.join("src/policy/eligibility.tes").is_file());
    assert!(project.join("tests/eligibility.tes").is_file());
    assert!(
        fs::read_to_string(project.join("src/main.tes"))
            .unwrap()
            .contains("use \"domain/request.tes\"")
    );
    let declarations = fs::read_to_string(project.join("tests/eligibility.tes")).unwrap();
    assert!(declarations.contains("assert eligibility_is_total(Request):"));
    let readme = fs::read_to_string(project.join("README.md")).unwrap();
    assert!(readme.contains("tess validate ."));
    assert!(readme.contains("tess verify ."));
    assert!(!readme.contains("tess check ."));
    assert!(!readme.contains("tess explore ."));

    for arguments in [
        vec!["validate", path(&project)],
        vec!["lint", path(&project), "--warnings-as-errors"],
        vec!["test", path(&project)],
        vec!["verify", path(&project)],
        vec!["run", path(&project), "--test", "enabled_is_eligible"],
        vec![
            "explain",
            path(&project.join("tess.toml")),
            "--test",
            "enabled_is_eligible",
        ],
        vec!["fmt", path(&project), "--check"],
    ] {
        let output = tess(&arguments);
        assert_eq!(
            output.status.code(),
            Some(0),
            "command {arguments:?}\nstdout: {}\nstderr: {}",
            stdout(&output),
            stderr(&output)
        );
    }

    let output = tess(&["init", path(&project)]);
    assert_eq!(output.status.code(), Some(2));
    assert!(stderr(&output).contains("non-empty"));
}

#[test]
fn import_graph_diagnostics_report_the_importing_file() {
    let directory = TestDirectory::new();
    let main = directory.write(
        "project/main.tes",
        "mod policy\nuse \"rules.tes\"\nuse \"rules.tes\"\n",
    );
    directory.write(
        "project/rules.tes",
        "mod wrong\nuse \"main.tes\"\nenum Answer:\n    Yes\n",
    );
    let output = tess(&["validate", path(&main)]);
    assert_eq!(output.status.code(), Some(1));
    let error = stderr(&output);
    assert!(error.contains("error[M0003]"), "{error}");
    assert!(error.contains("error[M0004]"), "{error}");
    assert!(error.contains("error[M0005]"), "{error}");
    assert!(error.contains("rules.tes:1:5"), "{error}");
    assert!(error.contains("main.tes:3:5"), "{error}");
}

#[test]
fn directory_formatting_covers_all_reachable_files_and_rejects_stdout() {
    let directory = TestDirectory::new();
    let project = directory.path.join("format-project");
    let output = tess(&["init", path(&project), "--module", "format_project"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let model = project.join("src/domain/request.tes");
    let unformatted = fs::read_to_string(&model)
        .unwrap()
        .replace("    Eligible\n", "    Eligible    \n");
    fs::write(&model, unformatted).unwrap();

    let output = tess(&["fmt", path(&project), "--check"]);
    assert_eq!(output.status.code(), Some(1));
    assert!(stderr(&output).contains("request.tes"));
    let output = tess(&["fmt", path(&project)]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert!(fs::read_to_string(&model).unwrap().contains("    Eligible"));
    assert!(
        fs::read_to_string(project.join("src/main.tes"))
            .unwrap()
            .contains("use \"domain/request.tes\"")
    );

    let output = tess(&["fmt", path(&project), "--stdout"]);
    assert_eq!(output.status.code(), Some(2));
    assert!(stderr(&output).contains("exactly one reachable source"));
}

#[test]
fn malformed_manifest_and_missing_import_have_distinct_exit_codes() {
    let directory = TestDirectory::new();
    let manifest = directory.write("bad/tess.toml", "[project]\nname = \"bad\"\n");
    let output = tess(&["validate", path(&manifest)]);
    assert_eq!(output.status.code(), Some(2));
    assert!(stderr(&output).contains("missing required `entry`"));

    let source = directory.write(
        "missing/main.tes",
        "mod missing\nuse \"does-not-exist.tes\"\n",
    );
    let output = tess(&["validate", path(&source)]);
    assert_eq!(output.status.code(), Some(1));
    assert!(stderr(&output).contains("error[M0001]"));
    assert!(stderr(&output).contains("main.tes:2:5"));
}