defmodule Mix.Tasks.Firebreak.Spec do
  @shortdoc "Generate TLA+ lifecycle specs from the supervision model"

  @moduledoc """
  Generates a formal lifecycle spec per supervisor, derived purely from
  firebreak's supervision model (`mix firebreak --format model`). Each spec models
  the restart/escalation lifecycle and — only where firebreak found a synchronous
  cross-tree crossing — an external-caller availability property.

      mix firebreak.spec                          # TLA+ + TLC config -> firebreak_specs/
      mix firebreak.spec --lang quint             # Quint modules instead
      mix firebreak.spec ../some_app --out specs  # analyse another project
      mix firebreak.spec --no-compile             # static only

  Run a generated spec:

      # TLA+ (default)
      java -cp tla2tools.jar tlc2.TLC -deadlock -config <Sup>.cfg <Sup>.tla
      # Quint
      quint verify --invariant SupNeverDies <Sup>.qnt

  `:one_for_all`, `:one_for_one`, and `:rest_for_one` are templated (plus a
  `:temporary` synchronous-target refinement); other shapes are reported as
  skipped rather than modelled unfaithfully. TLA+ and Quint emit the same model.
  """

  use Mix.Task

  @impl Mix.Task
  def run(argv) do
    {opts, args} =
      OptionParser.parse!(argv, strict: [out: :string, compile: :boolean, lang: :string])

    root = List.first(args) || File.cwd!()
    if args == [] and opts[:compile] != false, do: maybe_compile()

    analyze_opts = if opts[:compile] == false, do: [runtime: false], else: []
    lang = parse_lang(opts[:lang])
    out = opts[:out] || "firebreak_specs"
    File.mkdir_p!(out)

    {written, skipped} =
      root
      |> Firebreak.analyze(analyze_opts)
      |> Firebreak.Model.build()
      |> Enum.reduce({[], []}, fn bundle, {written, skipped} ->
        case write_spec(bundle, out, lang) do
          {:ok, name} -> {[name | written], skipped}
          :unsupported -> {written, [bundle.supervisor | skipped]}
        end
      end)

    ext = if lang == :quint, do: ".qnt", else: ".tla / .cfg"

    Mix.shell().info(
      "firebreak: wrote #{length(written)} #{lang} spec(s) to #{out}/ " <>
        "(#{length(skipped)} supervisor(s) not templated)"
    )

    written |> Enum.reverse() |> Enum.each(&Mix.shell().info("  + #{&1}#{ext}"))
  end

  defp parse_lang(nil), do: :tla
  defp parse_lang("tla"), do: :tla
  defp parse_lang("quint"), do: :quint

  defp parse_lang(other),
    do: Mix.raise("unknown --lang #{inspect(other)} (expected: tla | quint)")

  defp write_spec(bundle, out, :quint) do
    case Firebreak.Quint.generate(bundle) do
      {:ok, name, qnt} ->
        File.write!(Path.join(out, name <> ".qnt"), qnt)
        {:ok, name}

      {:unsupported, _reason} ->
        :unsupported
    end
  end

  defp write_spec(bundle, out, :tla) do
    case Firebreak.Tla.generate(bundle) do
      {:ok, name, tla, cfg} ->
        File.write!(Path.join(out, name <> ".tla"), tla)
        File.write!(Path.join(out, name <> ".cfg"), cfg)
        {:ok, name}

      {:unsupported, _reason} ->
        :unsupported
    end
  end

  defp maybe_compile do
    Mix.Task.run("compile", ["--no-deps-check"])
  rescue
    _ -> :ok
  catch
    _, _ -> :ok
  end
end