#compdef nucleos

autoload -U is-at-least

_nucleos() {
    typeset -A opt_args
    typeset -a _arguments_options
    local ret=1

    if is-at-least 5.2; then
        _arguments_options=(-s -S -C)
    else
        _arguments_options=(-s -C)
    fi

    local context curcontext="$curcontext" state line
    _arguments "${_arguments_options[@]}" : \
'--threads=[Parallel BFS threads \[1\]]:N:_default' \
'--output=[Output format\: \`text\` (default) or \`json\`]:OUTPUT:(text json)' \
'-v[Verbose\: show per-check progress]' \
'--verbose[Verbose\: show per-check progress]' \
'*-d[Enable debug output and a full diagnostic backtrace on panic]' \
'*--debug[Enable debug output and a full diagnostic backtrace on panic]' \
'-p[Skip well-formedness checking]' \
'--skip-wfc[Skip well-formedness checking]' \
'--no-compress[Disable leaf-LTS compression when composing a system LTS. By default each leaf is replaced by its strong-bisimulation quotient (weak-failures-equivalent, much smaller) before the product BFS, for any leaf above a size threshold; this opts out (exact serial product, byte-identical to the pre-compression output)]' \
'--license[Print the full proprietary licence text and exit]' \
'-h[Print help]' \
'--help[Print help]' \
'-V[Print version]' \
'--version[Print version]' \
":: :_nucleos_commands" \
"*::: :->nucleos" \
&& ret=0
    case $state in
    (nucleos)
        words=($line[1] "${words[@]}")
        (( CURRENT += 1 ))
        curcontext="${curcontext%:*:*}:nucleos-command-$line[1]:"
        case $line[1] in
            (anonymize)
_arguments "${_arguments_options[@]}" : \
'--output=[Output format\: \`text\` (default) or \`json\`]:OUTPUT:(text json)' \
'-h[Print help]' \
'--help[Print help]' \
':model_path -- Path to the `.dzn` source file to anonymize. Use `-` to read from stdin (matches the convention of `parse -E`'\''s output → pipeline use):_default' \
&& ret=0
;;
(bug-report)
_arguments "${_arguments_options[@]}" : \
'-o+[Output path; extension picks format (.zip / .tar.gz / .tgz / .tar)]:FILE:_files' \
'--out=[Output path; extension picks format (.zip / .tar.gz / .tgz / .tar)]:FILE:_files' \
'--model=[Include this .dzn file (flattened via \`parse -E\`)]:DZN:_files' \
'*-I+[Import directory for --model (repeatable)]:DIR:_files' \
'*--import=[Import directory for --model (repeatable)]:DIR:_files' \
'--panic-log=[Include this captured panic stderr (overrides last-panic.log auto-pickup)]:FILE:_files' \
'--capture-output=[Include this captured run output (overrides last-run.log auto-pickup)]:FILE:_files' \
'--description=[Free-text "what went wrong" note]:TEXT:_default' \
'--output=[Output format\: \`text\` (default) or \`json\`]:OUTPUT:(text json)' \
'(--no-anonymize)--anonymize[Force-anonymize the model (skips the anonymize prompt)]' \
'(--anonymize)--no-anonymize[Force-DO-NOT-anonymize the model (skips the anonymize prompt)]' \
'--no-last-panic[Skip auto-pickup of last-panic.log]' \
'--no-last-run[Skip auto-pickup of last-run.log]' \
'--no-infer[Skip argv inference from last-{panic,run}.log]' \
'--no-env[Skip env-var collection (privacy override)]' \
'-y[Non-interactive\: skip all prompts, take each default. The "include source" default is NO unless --model was explicit or --include-source was passed, so scripted runs never bundle source by accident]' \
'--yes[Non-interactive\: skip all prompts, take each default. The "include source" default is NO unless --model was explicit or --include-source was passed, so scripted runs never bundle source by accident]' \
'(--model)--include-source[Force "yes" to the source-inclusion prompt — explicitly opts a non-interactive run into bundling the inferred model. No effect when source is already locked in via \`--model\`. Pair with \`--yes\` for CI use]' \
'-h[Print help]' \
'--help[Print help]' \
&& ret=0
;;
(parse)
_arguments "${_arguments_options[@]}" : \
'*-I+[Add DIR to import path (repeatable)]:DIR:_default' \
'*--import=[Add DIR to import path (repeatable)]:DIR:_default' \
'--output=[Output format\: \`text\` (default) or \`json\`]:OUTPUT:(text json)' \
'-E[Resolve imports and write the flattened source to stdout (gcc-style preprocessor mode). Skips WFC]' \
'--preprocess[Resolve imports and write the flattened source to stdout (gcc-style preprocessor mode). Skips WFC]' \
'-D[With \`-E\`\: omit the \`#file\`/\`#imported\` directive lines, emitting only the concatenated source. Re-parsing such output loses the per-file (line, col) tracking — locations report against the flattened stream instead of the original sources]' \
'--no-directives[With \`-E\`\: omit the \`#file\`/\`#imported\` directive lines, emitting only the concatenated source. Re-parsing such output loses the per-file (line, col) tracking — locations report against the flattened stream instead of the original sources]' \
'-l[Print \`<name> <type>\` for each model declared in FILE — one per line, in source order — then exit. \`<type>\` is one of \`interface\`, \`component\`, \`foreign\`, \`system\`. Only models declared in FILE are listed (imports are not resolved), mirroring \`dzn parse --list-models\`]' \
'--list-models[Print \`<name> <type>\` for each model declared in FILE — one per line, in source order — then exit. \`<type>\` is one of \`interface\`, \`component\`, \`foreign\`, \`system\`. Only models declared in FILE are listed (imports are not resolved), mirroring \`dzn parse --list-models\`]' \
'-h[Print help]' \
'--help[Print help]' \
':model_path -- Path to the .dzn model file:_default' \
&& ret=0
;;
(inspect-ports)
_arguments "${_arguments_options[@]}" : \
'-m+[Restrict introspection to model MODEL (e.g. \`-m hello_bool\`). When omitted the subcommand picks a default the same way \`verify\` does (the file'\''s main-component / iface)]:MODEL:_default' \
'--model=[Restrict introspection to model MODEL (e.g. \`-m hello_bool\`). When omitted the subcommand picks a default the same way \`verify\` does (the file'\''s main-component / iface)]:MODEL:_default' \
'*-I+[Add DIR to import path (repeatable)]:DIR:_default' \
'*--import=[Add DIR to import path (repeatable)]:DIR:_default' \
'--output=[Output format\: \`text\` (default) or \`json\`]:OUTPUT:(text json)' \
'-h[Print help]' \
'--help[Print help]' \
':model_path -- Path to the .dzn model file:_default' \
&& ret=0
;;
(lts)
_arguments "${_arguments_options[@]}" : \
'-m+[Select component/interface by name]:MODEL:_default' \
'--model=[Select component/interface by name]:MODEL:_default' \
'*-I+[Add DIR to import path (repeatable)]:DIR:_default' \
'*--import=[Add DIR to import path (repeatable)]:DIR:_default' \
'-q+[Event queue size \[3\]]:N:_default' \
'--queue-size=[Event queue size \[3\]]:N:_default' \
'--queue-size-defer=[Defer queue size \[2\]]:N:_default' \
'--queue-size-external=[External queue size \[1\]]:N:_default' \
'--output=[Output format\: \`text\` (default) or \`json\`]:OUTPUT:(text json)' \
'--full-lts[Emit the full LTS instead of the fail-fast one. By default \`lts\` stops exploration on the first error edge — the same (possibly truncated) graph \`verify\` consumes — so the two commands agree. \`--full-lts\` forces a complete exploration of every reachable state]' \
'--defer-origin[Tag each \`<defer>\` discharge edge with its origin leaf (\`<defer\:<inst>>\`) in the RTC-product system LTS. OFF by default (bare \`<defer>\`, matching dzn). No effect on non-system models]' \
'-h[Print help]' \
'--help[Print help]' \
':model_path -- Path to the .dzn model file:_default' \
&& ret=0
;;
(traces)
_arguments "${_arguments_options[@]}" : \
'-m+[Select component/interface by name]:MODEL:_default' \
'--model=[Select component/interface by name]:MODEL:_default' \
'*-I+[Add DIR to import path (repeatable)]:DIR:_default' \
'*--import=[Add DIR to import path (repeatable)]:DIR:_default' \
'-o+[Write traces to DIR as \`<model>.trace.<N>\` (default "."); \`-\` writes all traces to stdout. (Long form is \`--output-dir\`; the global \`--output\` selects the text/json report mode.)]:DIR:_default' \
'--output-dir=[Write traces to DIR as \`<model>.trace.<N>\` (default "."); \`-\` writes all traces to stdout. (Long form is \`--output-dir\`; the global \`--output\` selects the text/json report mode.)]:DIR:_default' \
'-q+[Event queue size \[3\]]:N:_default' \
'--queue-size=[Event queue size \[3\]]:N:_default' \
'--queue-size-defer=[Defer queue size \[2\]]:N:_default' \
'--queue-size-external=[External queue size \[1\]]:N:_default' \
'--output=[Output format\: \`text\` (default) or \`json\`]:OUTPUT:(text json)' \
'-f[Include \`<flush>\` events in the traces]' \
'--flush[Include \`<flush>\` events in the traces]' \
'-i[Include traces that lead to an illegal]' \
'--illegal[Include traces that lead to an illegal]' \
'--defer-origin[Tag each \`<defer>\` discharge edge with its origin leaf (\`<defer\:<inst>>\`) in the system LTS. OFF by default (bare \`<defer>\`). Replay such traces with \`simulate --defer-origin\`. No effect on non-system models]' \
'-h[Print help]' \
'--help[Print help]' \
':model_path -- Path to the .dzn model file:_default' \
&& ret=0
;;
(lts-walk)
_arguments "${_arguments_options[@]}" : \
'-m+[Select component/interface by name]:MODEL:_default' \
'--model=[Select component/interface by name]:MODEL:_default' \
'*-I+[Add DIR to import path (repeatable)]:DIR:_default' \
'*--import=[Add DIR to import path (repeatable)]:DIR:_default' \
'-t+[Read trace from FILE (default\: stdin)]:FILE:_default' \
'--trail=[Read trace from FILE (default\: stdin)]:FILE:_default' \
'-q+[Event queue size]:N:_default' \
'--queue-size=[Event queue size]:N:_default' \
'--queue-size-defer=[Defer queue size]:N:_default' \
'--queue-size-external=[External queue size]:N:_default' \
'--compare-aut=[Walk the same trace through a second LTS read from FILE (Aldebaran .aut) and at every step diff the weak-refusal sets. Halts on the first non-empty diff, dumping the full state context. Use to localize structural divergence vs. a dzn/golden LTS]:FILE:_default' \
'--output=[Output format\: \`text\` (default) or \`json\`]:OUTPUT:(text json)' \
'--show-eligible[Print weak-outgoing label set at each step]' \
'--state-as-tau[Treat \`port.<state>(...)\` labels as tau when looking for the next step (off by default — ltscompare'\''s \`--tau\` only covers \`<flush>\`)]' \
'-h[Print help]' \
'--help[Print help]' \
':model_path -- Path to the .dzn model file:_default' \
&& ret=0
;;
(lts-diagnose)
_arguments "${_arguments_options[@]}" : \
'-m+[Select component by name]:MODEL:_default' \
'--model=[Select component by name]:MODEL:_default' \
'*-I+[Add DIR to import path (repeatable)]:DIR:_default' \
'*--import=[Add DIR to import path (repeatable)]:DIR:_default' \
'--state=[Post-trigger LTS state id whose handler exploration to trace verbosely (the state the trigger event lands on; find it with \`lts-walk --compare-aut\`). Equivalent to \`NUC_DBG_STATE\`]:N:_default' \
'-q+[Event queue size]:N:_default' \
'--queue-size=[Event queue size]:N:_default' \
'--queue-size-defer=[Defer queue size]:N:_default' \
'--queue-size-external=[External queue size]:N:_default' \
'--output=[Output format\: \`text\` (default) or \`json\`]:OUTPUT:(text json)' \
'-h[Print help]' \
'--help[Print help]' \
':model_path -- Path to the .dzn model file:_default' \
&& ret=0
;;
(verify)
_arguments "${_arguments_options[@]}" : \
'-m+[Restrict verification to model MODEL]:MODEL:_default' \
'--model=[Restrict verification to model MODEL]:MODEL:_default' \
'*-I+[Add DIR to import path (repeatable)]:DIR:_default' \
'*--import=[Add DIR to import path (repeatable)]:DIR:_default' \
'-q+[Event queue size \[3\]]:N:_default' \
'--queue-size=[Event queue size \[3\]]:N:_default' \
'--queue-size-defer=[Defer queue size \[2\]]:N:_default' \
'--queue-size-external=[External queue size \[1\]]:N:_default' \
'--output=[Output format\: \`text\` (default) or \`json\`]:OUTPUT:(text json)' \
'-k[Keep verifying after finding an error (default\: stop on first)]' \
'--keep-going[Keep verifying after finding an error (default\: stop on first)]' \
'--no-interfaces[Skip interface verification]' \
'-U[Skip the unreachable code check]' \
'--no-unreachable[Skip the unreachable code check]' \
'--full-lts[Explore the full LTS instead of stopping at the first error edge. Verify is fail-fast by default (it stops exploring once a reachable error is found, which is all the report needs); \`--full-lts\` forces a complete exploration of every reachable state. Same flag as \`lts\`]' \
'-h[Print help]' \
'--help[Print help]' \
':model_path -- Path to the .dzn model file:_default' \
&& ret=0
;;
(simulate)
_arguments "${_arguments_options[@]}" : \
'-m+[Select component/interface by name]:MODEL:_default' \
'--model=[Select component/interface by name]:MODEL:_default' \
'*-I+[Add DIR to import path (repeatable)]:DIR:_default' \
'*--import=[Add DIR to import path (repeatable)]:DIR:_default' \
'-t+[Read trace from FILE (default\: stdin)]:FILE:_default' \
'--trail=[Read trace from FILE (default\: stdin)]:FILE:_default' \
'-q+[Event queue size \[3\]]:N:_default' \
'--queue-size=[Event queue size \[3\]]:N:_default' \
'--queue-size-defer=[Defer queue size \[2\]]:N:_default' \
'--queue-size-external=[External queue size \[1\]]:N:_default' \
'--check-trace=[Test the REPL against a golden trace FILE\: drive the interactive engine using the trace as the "user" — at each turn the next env-choosable trace event is selected (it MUST be eligible), the RTC is executed, and each produced event is matched against the head of the trace (a mismatch fails with exit 1). The canonical simulate output is printed to stdout so it can be diffed against the golden \`simulate.N\`. Implies \`--repl\`]:FILE:_default' \
'--output=[Output format\: \`text\` (default) or \`json\`]:OUTPUT:(text json)' \
'--repl[REPL mode\: stay running, after each RTC print the \`(eligible …)\` menu (to stderr) and read the next environment choice from stdin (one event per line); the chosen event is executed and driven to the end of its RTC (or to a valued requires-call awaiting a reply value). The canonical simulate output goes to stdout; \`quit\`/EOF ends the session. Environment choices in, produced events + verdicts deduced. On a terminal the prompt offers Tab completion of the eligible events, command history, and a \`help\` command]' \
'--defer-any-order[Follow the trace'\''s defer discharge order instead of assuming a global defer FIFO. The system LTS is over-approximating (the FIFO is not modelled — too expensive), so with this flag every valid LTS-generated trace renders rather than bailing on a non-FIFO cross-leaf discharge. See docs/global_defer_sync.md]' \
'--defer-origin[Tag each \`<defer>\` discharge edge with its origin leaf (\`<defer\:<inst>>\`) in the RTC-product system LTS. OFF by default (bare \`<defer>\`). A trace generated with this flag must be replayed with it; selfcheck uses it on both ends. Has no effect on non-system models]' \
'-h[Print help]' \
'--help[Print help]' \
':model_path -- Path to the .dzn model file:_default' \
&& ret=0
;;
(trace)
_arguments "${_arguments_options[@]}" : \
'--output=[Output format\: \`text\` (default) or \`json\`]:OUTPUT:(text json)' \
'-h[Print help]' \
'--help[Print help]' \
'::file -- Trace input FILE (default\: stdin):_default' \
&& ret=0
;;
(sim-judge)
_arguments "${_arguments_options[@]}" : \
'--class=[Classification\: shape (default) | exact | goldenartifact | nondet | stateartifact. When omitted, a \`<golden>.judge\` sidecar (first non-comment line) supplies the per-(model,trace) class]:CLASS:_default' \
'--output=[Output format\: \`text\` (default) or \`json\`]:OUTPUT:(text json)' \
'--emit-doc[Emit the normative doc sections (§6/§7/§8) from the code, for the drift check (scripts/check_judge_doc.sh). Ignores golden/ours]' \
'-h[Print help]' \
'--help[Print help]' \
'::golden -- Reference (golden) output file:_default' \
'::ours -- Our output file to judge:_default' \
&& ret=0
;;
        esac
    ;;
esac
}

(( $+functions[_nucleos_commands] )) ||
_nucleos_commands() {
    local commands; commands=(
'anonymize:Rewrite a .dzn source file with identifiers replaced by \`_<N>\` and comments stripped' \
'bug-report:Bundle diagnostic info into a .zip / .tar.gz archive for a support ticket' \
'parse:Parse a Dezyne file and run well-formedness checks' \
'inspect-ports:Emit JSON describing the ports of a component / interface\: names, directions (provides/requires), iface in/out events, param signatures. Read-only; no LTS, no simulation' \
'lts:Generate an LTS for a Dezyne component or interface in \`.aut\` format' \
'traces:Generate an exhaustive set of traces for a Dezyne model (each trace ends at an RTC node). Mirrors \`dzn traces\`' \
'lts-walk:Replay a trace through the generated LTS, dumping state vectors at each step' \
'lts-diagnose:(dev) Stream a verbose \`\[dbg\]\` trace of one handler'\''s LTS exploration (emitted edges, requires-call replies, external- spontaneous fire/no-fire, dedup NEW/MERGE) for a target post-trigger state — for localising weak-failures divergences' \
'verify:Check a Dezyne model for verification errors (deadlock, livelock, illegal, ...)' \
'simulate:Simulate a Dezyne model against a trace' \
'trace:(dev) Convert \`simulate\` textual output to sequence-diagram JSON, identical to \`dzn trace -f json\`. Reads stdin or FILE; output is always JSON (no \`-f\`). Backs the IDE trace view' \
'sim-judge:(dev) Judge a simulate/repl output against a golden under the L4 shape-regression policy (docs/sim_judge_design.md). Prints the verdict; exit 0 Pass/Excused, 1 Fail. Advisory shape check — NOT correctness' \
    )
    _describe -t commands 'nucleos commands' commands "$@"
}
(( $+functions[_nucleos__subcmd__anonymize_commands] )) ||
_nucleos__subcmd__anonymize_commands() {
    local commands; commands=()
    _describe -t commands 'nucleos anonymize commands' commands "$@"
}
(( $+functions[_nucleos__subcmd__bug-report_commands] )) ||
_nucleos__subcmd__bug-report_commands() {
    local commands; commands=()
    _describe -t commands 'nucleos bug-report commands' commands "$@"
}
(( $+functions[_nucleos__subcmd__inspect-ports_commands] )) ||
_nucleos__subcmd__inspect-ports_commands() {
    local commands; commands=()
    _describe -t commands 'nucleos inspect-ports commands' commands "$@"
}
(( $+functions[_nucleos__subcmd__lts_commands] )) ||
_nucleos__subcmd__lts_commands() {
    local commands; commands=()
    _describe -t commands 'nucleos lts commands' commands "$@"
}
(( $+functions[_nucleos__subcmd__lts-diagnose_commands] )) ||
_nucleos__subcmd__lts-diagnose_commands() {
    local commands; commands=()
    _describe -t commands 'nucleos lts-diagnose commands' commands "$@"
}
(( $+functions[_nucleos__subcmd__lts-walk_commands] )) ||
_nucleos__subcmd__lts-walk_commands() {
    local commands; commands=()
    _describe -t commands 'nucleos lts-walk commands' commands "$@"
}
(( $+functions[_nucleos__subcmd__parse_commands] )) ||
_nucleos__subcmd__parse_commands() {
    local commands; commands=()
    _describe -t commands 'nucleos parse commands' commands "$@"
}
(( $+functions[_nucleos__subcmd__sim-judge_commands] )) ||
_nucleos__subcmd__sim-judge_commands() {
    local commands; commands=()
    _describe -t commands 'nucleos sim-judge commands' commands "$@"
}
(( $+functions[_nucleos__subcmd__simulate_commands] )) ||
_nucleos__subcmd__simulate_commands() {
    local commands; commands=()
    _describe -t commands 'nucleos simulate commands' commands "$@"
}
(( $+functions[_nucleos__subcmd__trace_commands] )) ||
_nucleos__subcmd__trace_commands() {
    local commands; commands=()
    _describe -t commands 'nucleos trace commands' commands "$@"
}
(( $+functions[_nucleos__subcmd__traces_commands] )) ||
_nucleos__subcmd__traces_commands() {
    local commands; commands=()
    _describe -t commands 'nucleos traces commands' commands "$@"
}
(( $+functions[_nucleos__subcmd__verify_commands] )) ||
_nucleos__subcmd__verify_commands() {
    local commands; commands=()
    _describe -t commands 'nucleos verify commands' commands "$@"
}

if [ "$funcstack[1]" = "_nucleos" ]; then
    _nucleos "$@"
else
    compdef _nucleos nucleos
fi
