metamon

-module(metamon@stateful).
-compile([no_auto_import, nowarn_unused_vars, nowarn_unused_function, nowarn_nomatch, inline]).
-define(FILEPATH, "src/metamon/stateful.gleam").
-export([run/3, names_of/1, 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(HHU) :: {passed, HHU, integer(), integer()} |
    {failed, integer(), binary(), binary(), HHU}.

-file("src/metamon/stateful.gleam", 47).
-spec run_loop(
    HIB,
    HIC,
    list(metamon@command:command(HIB, HIC)),
    integer(),
    integer()
) -> outcome(HIB).
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", 39).
?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"
).
-spec run(HHV, HHW, list(metamon@command:command(HHV, HHW))) -> outcome(HHV).
run(Initial_model, Initial_real, Commands) ->
    run_loop(Initial_model, Initial_real, Commands, 0, 0).

-file("src/metamon/stateful.gleam", 97).
?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", 101).
-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 => 102}).

-file("src/metamon/stateful.gleam", 78).
?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"
).
-spec assert_passed(outcome(any())) -> nil.
assert_passed(Outcome) ->
    case Outcome of
        {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.