metamon

-module(metamon@stateful).
-compile([no_auto_import, nowarn_unused_vars, nowarn_unused_function, nowarn_nomatch, inline]).
-define(FILEPATH, "src/metamon/stateful.gleam").
-export([names_of/1, run/3, assert_passed/1]).
-export_type([outcome/1]).

-if(?OTP_RELEASE >= 27).
-define(MODULEDOC(Str), -moduledoc(Str)).
-define(DOC(Str), -doc(Str)).
-else.
-define(MODULEDOC(Str), -compile([])).
-define(DOC(Str), -compile([])).
-endif.

?MODULEDOC(
    " Run a sequence of `Command(model, real)` against an initial\n"
    " `(model, real)` pair, asserting that every command's\n"
    " `precondition` holds against the model and that `run` against\n"
    " the real returns `Ok(Nil)`.\n"
    "\n"
    " This is the minimum surface needed for model-based testing. It\n"
    " intentionally does not generate command sequences: callers\n"
    " construct the list themselves (or with `metamon.forall_with` over\n"
    " a list-of-commands generator). Shrinking command sequences and\n"
    " scheduler-based parallelism are out of scope for this minimum;\n"
    " the explicit list-driven flow is enough to catch model/real\n"
    " drift in straightforward state machines.\n"
).

-type outcome(HXV) :: {passed, HXV, integer(), integer()} |
    {failed, integer(), binary(), binary(), HXV}.

-file("src/metamon/stateful.gleam", 58).
-spec run_loop(
    HYC,
    HYD,
    list(metamon@command:command(HYC, HYD)),
    integer(),
    integer()
) -> outcome(HYC).
run_loop(Model, Real, Commands, Index, Skipped) ->
    case Commands of
        [] ->
            {passed, Model, Index - Skipped, Skipped};

        [Cmd | Rest] ->
            case (erlang:element(3, Cmd))(Model) of
                false ->
                    run_loop(Model, Real, Rest, Index + 1, Skipped + 1);

                true ->
                    case (erlang:element(5, Cmd))(Real) of
                        {error, Reason} ->
                            {failed,
                                Index,
                                erlang:element(2, Cmd),
                                Reason,
                                Model};

                        {ok, nil} ->
                            run_loop(
                                (erlang:element(4, Cmd))(Model),
                                Real,
                                Rest,
                                Index + 1,
                                Skipped
                            )
                    end
            end
    end.

-file("src/metamon/stateful.gleam", 130).
?DOC(
    " Names of all commands in the sequence, in order. Useful for the\n"
    " stateful test's own failure messages.\n"
).
-spec names_of(list(metamon@command:command(any(), any()))) -> list(binary()).
names_of(Commands) ->
    gleam@list:map(Commands, fun metamon@command:name_of/1).

-file("src/metamon/stateful.gleam", 134).
-spec panic_with_message(binary()) -> nil.
panic_with_message(Message) ->
    erlang:error(#{gleam_error => panic,
            message => Message,
            file => <<?FILEPATH/utf8>>,
            module => <<"metamon/stateful"/utf8>>,
            function => <<"panic_with_message"/utf8>>,
            line => 135}).

-file("src/metamon/stateful.gleam", 43).
?DOC(
    " Run `commands` left-to-right starting from `initial_model` and\n"
    " `initial_real`. Commands whose preconditions fail are skipped\n"
    " (counted but not run). The first real-side `Error(_)` halts the\n"
    " sequence and is returned as `Failed`.\n"
    "\n"
    " Passing `[]` is a programming error (vacuous test) and panics with\n"
    " a structured message — pass at least one Command, or use\n"
    " `forall(...)` for a non-stateful property.\n"
).
-spec run(HXW, HXX, list(metamon@command:command(HXW, HXX))) -> outcome(HXW).
run(Initial_model, Initial_real, Commands) ->
    case Commands of
        [] ->
            panic_with_message(
                <<"metamon.stateful.run: empty commands list (vacuous test). Pass at least one Command or use forall(...) for a non-stateful property."/utf8>>
            );

        _ ->
            nil
    end,
    run_loop(Initial_model, Initial_real, Commands, 0, 0).

-file("src/metamon/stateful.gleam", 99).
?DOC(
    " Convenience: assert that the outcome is `Passed`. On `Failed`,\n"
    " panic with a structured message that mirrors the regular failure\n"
    " report style.\n"
    "\n"
    " A `Passed` outcome with `ran == 0` is treated as a vacuous pass\n"
    " and panics:\n"
    "\n"
    " - `ran == 0 && skipped == 0` — \"empty commands list\" (matches the\n"
    "   panic from `run([])`).\n"
    " - `ran == 0 && skipped > 0` — every command's `precondition`\n"
    "   returned `False` for the model the runner walked. The test\n"
    "   never compared model and real, so silently passing would hide\n"
    "   precondition / initial-model bugs.\n"
).
-spec assert_passed(outcome(any())) -> nil.
assert_passed(Outcome) ->
    case Outcome of
        {passed, _, 0, 0} ->
            panic_with_message(
                <<"metamon.stateful.run: empty commands list (vacuous test). Pass at least one Command or use forall(...) for a non-stateful property."/utf8>>
            );

        {passed, _, 0, Skipped} ->
            panic_with_message(
                erlang:list_to_binary(
                    [<<"metamon.stateful.assert_passed: 0 commands ran (all "/utf8>>,
                        erlang:integer_to_binary(Skipped),
                        <<" skipped). Adjust preconditions or initial model so at least one command fires."/utf8>>]
                )
            );

        {passed, _, _, _} ->
            nil;

        {failed, Index, Name, Reason, _} ->
            panic_with_message(
                erlang:list_to_binary(
                    [<<"× stateful command failed\n  command:    `"/utf8>>,
                        Name,
                        <<"`\n  index:      "/utf8>>,
                        erlang:integer_to_binary(Index),
                        <<"\n  reason:     "/utf8>>,
                        Reason]
                )
            )
    end.