Merge pull request #7 from Progmasoft/feature/native-property-engine

Add a native property-testing engine with choice-sequence shrinking

17 files changed, 3022 insertions, 2 deletions

diff --git a/src/Progmasoft/BUILD.bazel b/src/Progmasoft/BUILD.bazel
index 14a67bf6..b053c277 100644
--- a/src/Progmasoft/BUILD.bazel
+++ b/src/Progmasoft/BUILD.bazel
@@ -7,6 +7,9 @@ package(default_visibility = ["//visibility:public"])
 cc_library(
     name = "catch3",
     srcs = [
+        "ChoiceShrinker.cpp",
+        "Context.cpp",
+        "PropertyEngine.cpp",
         "Results.cpp",
         "Snapshot.cpp",
         "XmlWriter.cpp",
@@ -16,6 +19,7 @@ cc_library(
         "Catch3/Assertions.hpp",
         "Catch3/Detail/InvalidArgument.hpp",
         "Catch3/Detail/Sequence.hpp",
+        "Catch3/ForAll.hpp",
         "Catch3/Generator.hpp",
         "Catch3/Generators/Boolean.hpp",
         "Catch3/Generators/Element.hpp",
@@ -25,8 +29,16 @@ cc_library(
         "Catch3/Generators/Vector.hpp",
         "Catch3/Property.hpp",
         "Catch3/Random.hpp",
+        "Catch3/Relations.hpp",
         "Catch3/Results.hpp",
         "Catch3/Snapshot.hpp",
+        "Catch3/Stateful.hpp",
+        "Catch3/Strategy/ChoiceSource.hpp",
+        "Catch3/Strategy/Containers.hpp",
+        "Catch3/Strategy/Context.hpp",
+        "Catch3/Strategy/Engine.hpp",
+        "Catch3/Strategy/Numeric.hpp",
+        "Catch3/Strategy/Strategy.hpp",
         "Catch3/XmlWriter.hpp",
     ],
     copts = select({
diff --git a/src/Progmasoft/Catch3.hpp b/src/Progmasoft/Catch3.hpp
index 5fca369a..a1db1db7 100644
--- a/src/Progmasoft/Catch3.hpp
+++ b/src/Progmasoft/Catch3.hpp
@@ -6,6 +6,7 @@
 #include <catch2/catch_all.hpp>
 
 #include <Progmasoft/Catch3/Assertions.hpp>
+#include <Progmasoft/Catch3/ForAll.hpp>
 #include <Progmasoft/Catch3/Generator.hpp>
 #include <Progmasoft/Catch3/Generators/Boolean.hpp>
 #include <Progmasoft/Catch3/Generators/Element.hpp>
@@ -15,6 +16,13 @@
 #include <Progmasoft/Catch3/Generators/Vector.hpp>
 #include <Progmasoft/Catch3/Property.hpp>
 #include <Progmasoft/Catch3/Random.hpp>
+#include <Progmasoft/Catch3/Relations.hpp>
 #include <Progmasoft/Catch3/Results.hpp>
 #include <Progmasoft/Catch3/Snapshot.hpp>
+#include <Progmasoft/Catch3/Stateful.hpp>
+#include <Progmasoft/Catch3/Strategy/ChoiceSource.hpp>
+#include <Progmasoft/Catch3/Strategy/Containers.hpp>
+#include <Progmasoft/Catch3/Strategy/Context.hpp>
+#include <Progmasoft/Catch3/Strategy/Numeric.hpp>
+#include <Progmasoft/Catch3/Strategy/Strategy.hpp>
 #include <Progmasoft/Catch3/XmlWriter.hpp>
diff --git a/src/Progmasoft/Catch3/Assertions.hpp b/src/Progmasoft/Catch3/Assertions.hpp
index 668c086d..61fef04a 100644
--- a/src/Progmasoft/Catch3/Assertions.hpp
+++ b/src/Progmasoft/Catch3/Assertions.hpp
@@ -5,8 +5,14 @@
 #include <catch2/catch_message.hpp>
 #include <catch2/catch_test_macros.hpp>
 
+#include <catch2/interfaces/catch_interfaces_capture.hpp>
+
+#include <Progmasoft/Catch3/ForAll.hpp>
 #include <Progmasoft/Catch3/Property.hpp>
 #include <Progmasoft/Catch3/Snapshot.hpp>
+#include <Progmasoft/Catch3/Strategy/Context.hpp>
+
+#include <string>
 
 /// Runs a property and reports its replay seed and minimized counterexample.
 #define CATCH3_CHECK_PROPERTY( ... )                            \
@@ -25,3 +31,30 @@
         INFO( catch3SnapshotResult.Message );                               \
         CHECK( catch3SnapshotResult.Succeeded() );                          \
     } while ( false )
+
+/// Runs ForAll( [options,] strategy..., body ) under the name of the
+/// current test case, which keys the example database, and reports the
+/// result through Catch2: the minimized counterexample, its notes and its
+/// replay token on failure.
+#define CATCH3_CHECK_FOR_ALL( ... )                                          \
+    do {                                                                     \
+        const ::Progmasoft::Catch3::Detail::PropertyNameScope catch3Name(    \
+            ::Catch::getResultCapture().getCurrentTestName() + ":" +         \
+            std::to_string( __LINE__ ) );                                    \
+        const auto catch3ForAllResult =                                      \
+            ::Progmasoft::Catch3::ForAll( __VA_ARGS__ );                     \
+        INFO( catch3ForAllResult.Describe() );                               \
+        CHECK( catch3ForAllResult.Succeeded() );                             \
+    } while ( false )
+
+/// As CATCH3_CHECK_FOR_ALL, but ends the test case on failure.
+#define CATCH3_REQUIRE_FOR_ALL( ... )                                        \
+    do {                                                                     \
+        const ::Progmasoft::Catch3::Detail::PropertyNameScope catch3Name(    \
+            ::Catch::getResultCapture().getCurrentTestName() + ":" +         \
+            std::to_string( __LINE__ ) );                                    \
+        const auto catch3ForAllResult =                                      \
+            ::Progmasoft::Catch3::ForAll( __VA_ARGS__ );                     \
+        INFO( catch3ForAllResult.Describe() );                               \
+        REQUIRE( catch3ForAllResult.Succeeded() );                           \
+    } while ( false )
diff --git a/src/Progmasoft/Catch3/ForAll.hpp b/src/Progmasoft/Catch3/ForAll.hpp
new file mode 100644
index 00000000..e41bfdb6
--- /dev/null
+++ b/src/Progmasoft/Catch3/ForAll.hpp
@@ -0,0 +1,191 @@
+// Copyright (c) 2026 Progmasoft.
+// SPDX-License-Identifier: MPL-2.0 WITH AdditionRef-Progmasoft-Exception-1.1
+#pragma once
+
+#include <Progmasoft/Catch3/Property.hpp>
+#include <Progmasoft/Catch3/Strategy/Containers.hpp>
+#include <Progmasoft/Catch3/Strategy/Context.hpp>
+#include <Progmasoft/Catch3/Strategy/Engine.hpp>
+#include <Progmasoft/Catch3/Strategy/Strategy.hpp>
+#include <exception>
+#include <functional>
+#include <optional>
+#include <string>
+#include <tuple>
+#include <type_traits>
+#include <utility>
+
+namespace Progmasoft::Catch3
+{
+
+    namespace Detail
+    {
+
+        /// Runs a body on one input and turns what happened into a verdict.
+        /// A body returns bool, or void and fails through
+        /// CATCH3_PROPERTY_ASSERT; an exception from it is a failure.
+        template<typename Body, typename Tuple>
+        void
+        RunBody(Body &&body, const Tuple &values, TrialOutcome &outcome)
+        {
+            TrialRecordScope scope(outcome.Record);
+#if defined(__cpp_exceptions)
+            try
+            {
+#endif
+                using Result = decltype(std::apply(body, values));
+                if constexpr (std::is_void_v<Result>)
+                {
+                    std::apply(body, values);
+                }
+                else
+                {
+                    if (!static_cast<bool>(std::apply(body, values)))
+                    {
+                        RecordPropertyFailureMessage(
+                            "property returned false");
+                    }
+                }
+#if defined(__cpp_exceptions)
+            }
+            catch (const std::exception &exception)
+            {
+                RecordPropertyFailureMessage(
+                    std::string("property threw std::exception: ")
+                    + exception.what());
+            }
+            catch (...)
+            {
+                RecordPropertyFailureMessage(
+                    "property threw a non-standard exception");
+            }
+#endif
+            if (outcome.Record.Failure.has_value())
+            {
+                outcome.Verdict = TrialVerdict::kFailed;
+                outcome.Reason = *outcome.Record.Failure;
+            }
+            else if (outcome.Record.Discarded)
+            {
+                outcome.Verdict = TrialVerdict::kDiscarded;
+            }
+        }
+
+        /// Draws a value, catching what a strategy throws.
+        template<typename ValueType>
+        [[nodiscard]] std::optional<ValueType>
+        DrawGuarded(const Strategy<ValueType> &strategy,
+                    ChoiceSource &source,
+                    TrialOutcome &outcome)
+        {
+#if defined(__cpp_exceptions)
+            try
+            {
+#endif
+                auto value = strategy.Draw(source);
+                if (!value.has_value())
+                {
+                    outcome.Verdict = TrialVerdict::kInvalid;
+                }
+                return value;
+#if defined(__cpp_exceptions)
+            }
+            catch (const std::exception &exception)
+            {
+                outcome.Verdict = TrialVerdict::kErrored;
+                outcome.Reason = std::string("strategy threw std::exception: ")
+                                 + exception.what();
+            }
+            catch (...)
+            {
+                outcome.Verdict = TrialVerdict::kErrored;
+                outcome.Reason = "strategy threw a non-standard exception";
+            }
+            return std::nullopt;
+#endif
+        }
+
+        template<typename... ValueTypes>
+        [[nodiscard]] std::string
+        DescribeArguments(const std::tuple<ValueTypes...> &values)
+        {
+            if constexpr (sizeof...(ValueTypes) == 1)
+            {
+                return DescribeValue(std::get<0>(values));
+            }
+            else
+            {
+                return DescribeValue(values);
+            }
+        }
+
+        template<typename Body, typename... ValueTypes>
+        [[nodiscard]] PropertyResult
+        ForAllWith(const PropertyOptions &options,
+                   Body body,
+                   Strategy<ValueTypes>... strategies)
+        {
+            static_assert(sizeof...(ValueTypes) > 0,
+                          "ForAll needs at least one strategy");
+            const auto input = Gen::Tuples(std::move(strategies)...);
+            const TrialRunner runner =
+                [&](ChoiceSource &source, bool describe) -> TrialOutcome {
+                TrialOutcome outcome;
+                auto values = DrawGuarded(input, source, outcome);
+                if (!values.has_value())
+                {
+                    return outcome;
+                }
+                if (describe)
+                {
+                    outcome.Description = DescribeArguments(*values);
+                }
+                RunBody(body, std::as_const(*values), outcome);
+                return outcome;
+            };
+            return RunPropertyEngine(options, runner);
+        }
+
+        template<typename Type>
+        inline constexpr bool kIsPropertyOptions
+            = std::is_same_v<std::remove_cvref_t<Type>, PropertyOptions>;
+
+    } // namespace Detail
+
+    /// Checks that a property holds for values drawn from strategies.
+    ///
+    ///     ForAll([options,] strategy..., body)
+    ///
+    /// body receives one value per strategy, as const references. It
+    /// returns bool, or returns void and uses CATCH3_PROPERTY_ASSERT and
+    /// CATCH3_PROPERTY_ASSUME; Note, Classify, Cover and Target may be
+    /// called from it. A failure is minimized by shrinking the choices the
+    /// strategies made, and the report carries a replay token for exactly
+    /// the minimized input.
+    template<typename... Arguments>
+    [[nodiscard]] PropertyResult
+    ForAll(Arguments &&...arguments)
+    {
+        constexpr std::size_t kCount = sizeof...(Arguments);
+        static_assert(kCount >= 2, "ForAll needs strategies and a body");
+        auto all = std::forward_as_tuple(std::forward<Arguments>(arguments)...);
+        using First = std::tuple_element_t<0, std::tuple<Arguments...>>;
+        if constexpr (Detail::kIsPropertyOptions<First>)
+        {
+            return [&]<std::size_t... Index>(std::index_sequence<Index...>) {
+                return Detail::ForAllWith(std::get<0>(all),
+                                          std::get<kCount - 1U>(all),
+                                          std::get<Index + 1U>(all)...);
+            }(std::make_index_sequence<kCount - 2U>{});
+        }
+        else
+        {
+            return [&]<std::size_t... Index>(std::index_sequence<Index...>) {
+                return Detail::ForAllWith(PropertyOptions{},
+                                          std::get<kCount - 1U>(all),
+                                          std::get<Index>(all)...);
+            }(std::make_index_sequence<kCount - 1U>{});
+        }
+    }
+
+} // namespace Progmasoft::Catch3
diff --git a/src/Progmasoft/Catch3/Property.hpp b/src/Progmasoft/Catch3/Property.hpp
index 57f7ac7b..bd055148 100644
--- a/src/Progmasoft/Catch3/Property.hpp
+++ b/src/Progmasoft/Catch3/Property.hpp
@@ -31,6 +31,30 @@ namespace Progmasoft::Catch3
         /// reported failure to reproduce that single trial, including its
         /// shrinking, without rerunning the trials before it.
         std::optional<std::uint64_t> ReplayTrialSeed = std::nullopt;
+
+        // The fields below are read by ForAll and the other strategy-based
+        // checks; CheckProperty with a Generator ignores them.
+
+        /// A replay token from a failure report: runs exactly the reported,
+        /// minimized counterexample and nothing else.
+        std::optional<std::string> Replay = std::nullopt;
+        /// Trials that may be discarded, by a filter that found nothing or
+        /// by CATCH3_PROPERTY_ASSUME, per requested trial before the
+        /// property gives up.
+        std::size_t MaxDiscardRatio = 10;
+        /// Extra trials that search for a higher score after the regular
+        /// ones, when the property calls Target. 0 disables the search.
+        std::size_t TargetSteps = 500;
+        /// Directory of the example database. Failing examples are stored
+        /// there and replayed first on the next run. Empty: the directory
+        /// named by CATCH3_PROPERTY_DATABASE, or no database when that is
+        /// unset.
+        std::string DatabasePath;
+        /// Names the property in the database. The CATCH3_ macros fill it
+        /// with the test case name and the source line.
+        std::string Name;
+        /// Adds the Classify and Cover statistics to a passing report.
+        bool ShowStatistics = false;
     };
 
     enum class PropertyStatus : std::uint8_t
@@ -39,6 +63,20 @@ namespace Progmasoft::Catch3
         kFailed,
         kErrored,
         kInvalidConfiguration,
+        /// A Cover requirement was not met.
+        kInsufficientCoverage,
+        /// Too many trials were discarded to trust the result.
+        kGaveUp,
+    };
+
+    /// How often one Classify or Cover label held.
+    struct LabelStatistic final
+    {
+        std::string Label;
+        std::size_t Count = 0;
+        double Percentage = 0.0;
+        /// The percentage a Cover call requires; 0 for Classify.
+        double Required = 0.0;
     };
 
     struct PropertyFailure final
@@ -49,6 +87,11 @@ namespace Progmasoft::Catch3
         std::size_t ShrinkSteps = 0;
         std::string Counterexample;
         std::string Reason;
+        /// Replay token of the minimized counterexample; empty for
+        /// CheckProperty with a Generator, whose replay is TrialSeed.
+        std::string Replay;
+        /// What the property recorded with Note for the counterexample.
+        std::vector<std::string> Notes;
     };
 
     /// Stable, machine-readable outcome with a deterministic human-readable
@@ -59,6 +102,10 @@ namespace Progmasoft::Catch3
         std::size_t TrialsRun = 0;
         std::optional<PropertyFailure> Failure;
         std::string Error;
+        std::size_t Discarded = 0;
+        std::vector<LabelStatistic> Statistics;
+        /// Set when Statistics should be part of a passing report.
+        bool ShowStatistics = false;
 
         [[nodiscard]] bool
         Succeeded() const noexcept
@@ -74,6 +121,23 @@ namespace Progmasoft::Catch3
             {
                 case PropertyStatus::kPassed:
                     output << "property passed: " << TrialsRun << " trials";
+                    if (Discarded != 0)
+                    {
+                        output << ", " << Discarded << " discarded";
+                    }
+                    if (ShowStatistics)
+                    {
+                        DescribeStatistics(output);
+                    }
+                    return output.str();
+                case PropertyStatus::kInsufficientCoverage:
+                    output << "property coverage insufficient after "
+                           << TrialsRun << " trials: " << Error;
+                    DescribeStatistics(output);
+                    return output.str();
+                case PropertyStatus::kGaveUp:
+                    output << "property gave up after " << TrialsRun
+                           << " trials: " << Error;
                     return output.str();
                 case PropertyStatus::kInvalidConfiguration:
                     output << "invalid property configuration: " << Error;
@@ -88,7 +152,7 @@ namespace Progmasoft::Catch3
                     break;
             }
 
-            if (Failure.has_value())
+            if (Failure.has_value() && Failure->Replay.empty())
             {
                 output << "; failing trial " << Failure->Trial << ", root seed "
                        << Failure->RootSeed << ", replay seed "
@@ -99,8 +163,42 @@ namespace Progmasoft::Catch3
                        << "\nreplay: set PropertyOptions::ReplayTrialSeed to "
                        << Failure->TrialSeed;
             }
+            else if (Failure.has_value())
+            {
+                output << "; failing trial " << Failure->Trial << ", root seed "
+                       << Failure->RootSeed << ", shrink checks "
+                       << Failure->ShrinkSteps
+                       << "\ncounterexample: " << Failure->Counterexample
+                       << "\nreason: " << Failure->Reason;
+                for (const auto &note : Failure->Notes)
+                {
+                    output << "\nnote: " << note;
+                }
+                output << "\nreplay: set PropertyOptions::Replay to \""
+                       << Failure->Replay << '"';
+            }
             return output.str();
         }
+
+    private:
+        void
+        DescribeStatistics(std::ostringstream &output) const
+        {
+            for (const auto &statistic : Statistics)
+            {
+                output << "\n  " << statistic.Label << ": "
+                       << statistic.Count << " ("
+                       << static_cast<long long>(statistic.Percentage * 10.0
+                                                 + 0.5)
+                              / 10.0
+                       << "%";
+                if (statistic.Required > 0.0)
+                {
+                    output << ", required " << statistic.Required << "%";
+                }
+                output << ')';
+            }
+        }
     };
 
     namespace Detail
diff --git a/src/Progmasoft/Catch3/Relations.hpp b/src/Progmasoft/Catch3/Relations.hpp
new file mode 100644
index 00000000..d3c2ec62
--- /dev/null
+++ b/src/Progmasoft/Catch3/Relations.hpp
@@ -0,0 +1,99 @@
+// Copyright (c) 2026 Progmasoft.
+// SPDX-License-Identifier: MPL-2.0 WITH AdditionRef-Progmasoft-Exception-1.1
+#pragma once
+
+#include <Progmasoft/Catch3/ForAll.hpp>
+#include <Progmasoft/Catch3/Strategy/Context.hpp>
+#include <functional>
+#include <string>
+#include <utility>
+
+// Ready-made property bodies for the oracles that need no specification of
+// the expected result: differential, metamorphic and round-trip testing.
+// Each one is passed to ForAll in place of a hand-written body:
+//
+//     ForAll(Gen::Vectors(Gen::Integers<int>()),
+//            Equivalent(ReferenceSort, FastSort));
+
+namespace Progmasoft::Catch3
+{
+
+    /// Differential testing: the candidate must return what the reference
+    /// returns for every input. A mismatch reports both results.
+    template<typename Reference, typename Candidate>
+    [[nodiscard]] auto
+    Equivalent(Reference reference, Candidate candidate)
+    {
+        return [reference, candidate](const auto &...input) mutable {
+            const auto expected = std::invoke(reference, input...);
+            const auto actual = std::invoke(candidate, input...);
+            if (!(expected == actual))
+            {
+                Note("reference: " + Detail::DescribeValue(expected));
+                Note("candidate: " + Detail::DescribeValue(actual));
+                Detail::RecordPropertyFailureMessage(
+                    "the candidate disagrees with the reference");
+            }
+        };
+    }
+
+    /// Metamorphic testing: for every input x, relation(function(x),
+    /// function(transform(x))) must hold, for example that sorting a
+    /// shuffled list gives the same result, or that doubling a length
+    /// doubles a cost.
+    template<typename Function, typename Transform, typename Relation>
+    [[nodiscard]] auto
+    Metamorphic(Function function, Transform transform, Relation relation)
+    {
+        return [function, transform, relation](const auto &input) mutable {
+            const auto source = std::invoke(function, input);
+            const auto followUpInput = std::invoke(transform, input);
+            const auto followUp = std::invoke(function, followUpInput);
+            if (!static_cast<bool>(std::invoke(relation, source, followUp)))
+            {
+                Note("follow-up input: " + Detail::DescribeValue(followUpInput));
+                Note("source output: " + Detail::DescribeValue(source));
+                Note("follow-up output: " + Detail::DescribeValue(followUp));
+                Detail::RecordPropertyFailureMessage(
+                    "the metamorphic relation does not hold");
+            }
+        };
+    }
+
+    /// decode(encode(x)) == x for every input.
+    template<typename Encode, typename Decode>
+    [[nodiscard]] auto
+    RoundTrip(Encode encode, Decode decode)
+    {
+        return [encode, decode](const auto &input) mutable {
+            const auto encoded = std::invoke(encode, input);
+            const auto decoded = std::invoke(decode, encoded);
+            if (!(decoded == input))
+            {
+                Note("encoded: " + Detail::DescribeValue(encoded));
+                Note("decoded: " + Detail::DescribeValue(decoded));
+                Detail::RecordPropertyFailureMessage(
+                    "decoding the encoded input did not give it back");
+            }
+        };
+    }
+
+    /// function(function(x)) == function(x) for every input.
+    template<typename Function>
+    [[nodiscard]] auto
+    Idempotent(Function function)
+    {
+        return [function](const auto &input) mutable {
+            const auto once = std::invoke(function, input);
+            const auto twice = std::invoke(function, once);
+            if (!(twice == once))
+            {
+                Note("once: " + Detail::DescribeValue(once));
+                Note("twice: " + Detail::DescribeValue(twice));
+                Detail::RecordPropertyFailureMessage(
+                    "applying the function twice changed the result");
+            }
+        };
+    }
+
+} // namespace Progmasoft::Catch3
diff --git a/src/Progmasoft/Catch3/Stateful.hpp b/src/Progmasoft/Catch3/Stateful.hpp
new file mode 100644
index 00000000..6bd34caa
--- /dev/null
+++ b/src/Progmasoft/Catch3/Stateful.hpp
@@ -0,0 +1,157 @@
+// Copyright (c) 2026 Progmasoft.
+// SPDX-License-Identifier: MPL-2.0 WITH AdditionRef-Progmasoft-Exception-1.1
+#pragma once
+
+#include <Progmasoft/Catch3/ForAll.hpp>
+#include <Progmasoft/Catch3/Strategy/Containers.hpp>
+#include <functional>
+#include <optional>
+#include <string>
+#include <utility>
+#include <vector>
+
+namespace Progmasoft::Catch3
+{
+
+    /// One step of a stateful test: a description for the report and the
+    /// code that applies the step to the model and to the system under
+    /// test. It checks the system against the model with
+    /// CATCH3_PROPERTY_ASSERT.
+    template<typename Model, typename System>
+    struct Action final
+    {
+        std::string Description;
+        std::function<void(Model &, System &)> Apply;
+    };
+
+    /// A kind of step. Make builds the step from the current model, so its
+    /// arguments can depend on the state, for example by choosing a key
+    /// that the model holds. Precondition says whether the step may run in
+    /// a state; an unset precondition always holds.
+    template<typename Model, typename System>
+    struct Command final
+    {
+        std::string Name;
+        std::function<Strategy<Action<Model, System>>(const Model &)> Make;
+        std::function<bool(const Model &)> Precondition = {};
+    };
+
+    /// A command without arguments.
+    template<typename Model, typename System, typename Apply>
+    [[nodiscard]] Command<Model, System>
+    MakeCommand(std::string name, Apply apply)
+    {
+        return Command<Model, System>{
+            name,
+            [name, apply](const Model &) {
+                return Gen::Just(Action<Model, System>{ name, apply });
+            },
+        };
+    }
+
+    namespace Detail
+    {
+
+        template<typename Model, typename System>
+        [[nodiscard]] TrialOutcome
+        RunCommands(ChoiceSource &source,
+                    bool describe,
+                    const std::function<Model()> &initialModel,
+                    const std::function<System(const Model &)> &makeSystem,
+                    const std::vector<Command<Model, System>> &commands,
+                    const SizeRange &steps)
+        {
+            TrialOutcome outcome;
+            Model model = initialModel();
+            std::optional<System> system;
+            std::vector<std::string> log;
+            {
+                TrialRecordScope scope(outcome.Record);
+                system.emplace(makeSystem(model));
+            }
+            const auto addStep = [&]() -> bool {
+                // The choice names a command; when its precondition does not
+                // hold, the next commands are tried in order, so that the
+                // same choice always leads to the same command.
+                const std::size_t first = static_cast<std::size_t>(
+                    source.Draw(commands.size() - 1U));
+                const Command<Model, System> *chosen = nullptr;
+                for (std::size_t offset = 0; offset < commands.size(); ++offset)
+                {
+                    const auto &candidate
+                        = commands[(first + offset) % commands.size()];
+                    if (!candidate.Precondition || candidate.Precondition(model))
+                    {
+                        chosen = &candidate;
+                        break;
+                    }
+                }
+                if (chosen == nullptr)
+                {
+                    return false;
+                }
+                auto action = DrawGuarded(chosen->Make(model), source, outcome);
+                if (!action.has_value())
+                {
+                    return false;
+                }
+                log.push_back(action->Description);
+                RunBody(
+                    [&]() { action->Apply(model, *system); },
+                    std::tuple<>(),
+                    outcome);
+                return outcome.Verdict == TrialVerdict::kPassed;
+            };
+            (void)Detail::DrawElements(source, steps, addStep);
+            if (outcome.Verdict == TrialVerdict::kInvalid && !log.empty())
+            {
+                // A step that could not be built ends the sequence; the
+                // steps before it still ran and passed.
+                outcome.Verdict = TrialVerdict::kPassed;
+            }
+            if (describe)
+            {
+                std::string text = "{";
+                for (std::size_t index = 0; index < log.size(); ++index)
+                {
+                    text += index == 0 ? " " : ", ";
+                    text += log[index];
+                }
+                outcome.Description = text + (log.empty() ? "}" : " }");
+            }
+            return outcome;
+        }
+
+    } // namespace Detail
+
+    /// Model-based testing: runs random sequences of commands against a
+    /// model and the system under test, side by side. A failing sequence
+    /// shrinks to a short one with simple arguments, since dropping a step
+    /// is deleting its choices.
+    template<typename Model, typename System>
+    [[nodiscard]] PropertyResult
+    CheckStateful(const PropertyOptions &options,
+                  std::function<Model()> initialModel,
+                  std::function<System(const Model &)> makeSystem,
+                  std::vector<Command<Model, System>> commands,
+                  SizeRange steps = {})
+    {
+        if (commands.empty())
+        {
+            Detail::RejectInvalidArgument(
+                "CheckStateful requires at least one command");
+        }
+        Detail::CheckRange(steps);
+        const Detail::TrialRunner runner
+            = [&](ChoiceSource &source, bool describe) {
+                  return Detail::RunCommands(source,
+                                             describe,
+                                             initialModel,
+