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

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

1 files changed, 129 insertions, 0 deletions

diff --git a/tests/Progmasoft/Stateful.tests.cpp b/tests/Progmasoft/Stateful.tests.cpp
new file mode 100644
index 00000000..48e2c918
--- /dev/null
+++ b/tests/Progmasoft/Stateful.tests.cpp
@@ -0,0 +1,129 @@
+// Copyright (c) 2026 Progmasoft.
+// SPDX-License-Identifier: MPL-2.0 WITH AdditionRef-Progmasoft-Exception-1.1
+#include <Progmasoft/Catch3.hpp>
+
+#include <cstddef>
+#include <deque>
+#include <string>
+#include <vector>
+
+namespace {
+
+    using Progmasoft::Catch3::Action;
+    using Progmasoft::Catch3::Command;
+    using Progmasoft::Catch3::PropertyOptions;
+    using Progmasoft::Catch3::PropertyStatus;
+    using Progmasoft::Catch3::SizeRange;
+    namespace Gen = Progmasoft::Catch3::Gen;
+
+    // A queue with a bug: past three elements it silently drops the
+    // oldest one.
+    class SmallQueue {
+    public:
+        void Push( int value ) {
+            if ( values_.size() == 3 ) { values_.pop_front(); }
+            values_.push_back( value );
+        }
+        int Pop() {
+            const int value = values_.front();
+            values_.pop_front();
+            return value;
+        }
+        [[nodiscard]] std::size_t Size() const { return values_.size(); }
+
+    private:
+        std::deque<int> values_;
+    };
+
+    using Model = std::deque<int>;
+
+    std::vector<Command<Model, SmallQueue>> QueueCommands() {
+        Command<Model, SmallQueue> push{
+            "push",
+            []( const Model& ) {
+                return Gen::Integers<int>( 0, 100 ).Map( []( int value ) {
+                    return Action<Model, SmallQueue>{
+                        "push(" + std::to_string( value ) + ")",
+                        [value]( Model& model, SmallQueue& queue ) {
+                            model.push_back( value );
+                            queue.Push( value );
+                            CATCH3_PROPERTY_ASSERT( queue.Size() ==
+                                                    model.size() );
+                        } };
+                } );
+            } };
+        Command<Model, SmallQueue> pop{
+            "pop",
+            []( const Model& ) {
+                return Gen::Just( Action<Model, SmallQueue>{
+                    "pop", []( Model& model, SmallQueue& queue ) {
+                        const int expected = model.front();
+                        model.pop_front();
+                        CATCH3_PROPERTY_ASSERT( queue.Pop() == expected );
+                    } } );
+            },
+            []( const Model& model ) { return !model.empty(); } };
+        return { push, pop };
+    }
+
+} // namespace
+
+TEST_CASE( "Stateful tests find and shrink a failing command sequence",
+           "[progmasoft][stateful]" ) {
+    PropertyOptions options;
+    options.Trials = 300;
+    options.Seed = 0x57A7E;
+    options.MaxShrinkSteps = 5000;
+    const auto result = Progmasoft::Catch3::CheckStateful<Model, SmallQueue>(
+        options,
+        [] { return Model{}; },
+        []( const Model& ) { return SmallQueue{}; },
+        QueueCommands() );
+    REQUIRE( result.Status == PropertyStatus::kFailed );
+    // The shortest failure: the fourth push drops an element.
+    CHECK( result.Failure->Counterexample ==
+           "{ push(0), push(0), push(0), push(0) }" );
+    CHECK( result.Failure->Reason.find(
+               "CATCH3_PROPERTY_ASSERT( queue.Size() == model.size() )" ) ==
+           0 );
+}
+
+TEST_CASE( "Stateful tests pass for a correct system and respect preconditions",
+           "[progmasoft][stateful]" ) {
+    struct Correct {
+        std::deque<int> Values;
+    };
+    Command<Model, Correct> push{
+        "push", []( const Model& ) {
+            return Gen::Integers<int>( 0, 9 ).Map( []( int value ) {
+                return Action<Model, Correct>{
+                    "push", [value]( Model& model, Correct& system ) {
+                        model.push_back( value );
+                        system.Values.push_back( value );
+                    } };
+            } );
+        } };
+    Command<Model, Correct> pop{
+        "pop",
+        []( const Model& ) {
+            return Gen::Just( Action<Model, Correct>{
+                "pop", []( Model& model, Correct& system ) {
+                    // The precondition guarantees an element.
+                    CATCH3_PROPERTY_ASSERT( !model.empty() );
+                    CATCH3_PROPERTY_ASSERT( system.Values.front() ==
+                                            model.front() );
+                    model.pop_front();
+                    system.Values.pop_front();
+                } } );
+        },
+        []( const Model& model ) { return !model.empty(); } };
+    PropertyOptions options;
+    options.Trials = 200;
+    const auto result = Progmasoft::Catch3::CheckStateful<Model, Correct>(
+        options,
+        [] { return Model{}; },
+        []( const Model& ) { return Correct{}; },
+        { push, pop },
+        SizeRange{ 0, 50 } );
+    CHECK( result.Status == PropertyStatus::kPassed );
+}