1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
|
// Copyright (c) 2026 Progmasoft.
// SPDX-License-Identifier: MPL-2.0 WITH AdditionRef-Progmasoft-Exception-2.0
#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,
makeSystem,
commands,
steps);
};
return Detail::RunPropertyEngine(options, runner);
}
} // namespace Progmasoft::Catch3
|