State machine: shrinking

Падающая CommandSequence может состоять из десятков команд. Shrinking находит кратчайшую, простейшую последовательность, всё ещё воспроизводящую падение, тем же двухфазным подходом, из которого собран Command::shrinks(): сначала удалить команды, потом упростить оставшиеся.

Фаза 1: удаление блоков

CommandSequenceArbitrary шринкает длину раньше всего остального, удаляя смежные блоки команд, а не по одной:

blockSize = count, count/2, count/4, ..., 1
для каждого blockSize:
  для каждого offset, где offset + blockSize <= count:
    выдать последовательность с удалёнными commands[offset .. offset+blockSize)

Сначала пробуется наибольший блок (вся последовательность), затем половины, затем четверти, вплоть до удаления одной команды. Именно это позволяет шринкеру изолировать падающий шаг в середине длинной последовательности: удаление только префиксом (отбросить первую половину, затем первую половину оставшегося) никогда не может прийти к «оставить всё, кроме команды #7» — скольжение окна размером в одну команду по всем offset'ам может. Удаление блока, которое опустило бы последовательность ниже minLength, пропускается, поэтому Gen::commands(..., minLen: 3, ...) никогда не шринкает меньше трёх шагов.

Фаза 2: упрощение по каждой команде

Когда удаление блоков перестаёт находить меньшую падающую последовательность, шринкер фиксирует длину и обходит собственное shrink-дерево каждой оставшейся команды ($command->shrinks()), подставляя по одной упрощённой команде за раз. Push(87) шринкается к Push(0) через дерево IntArbitrary точно так же, как если бы это был обычный параметр — команды шринкаются как любое Shrinkable-значение, потому что они им и являются.

Без ревалидации на реплее — намеренно

Ни одна из фаз не перепроверяет Command::preCondition() при построении кандидатов. Удаление команды #3 может инвалидировать precondition команды #7 (которая зависела от состояния, установленного командой #3), и шринкер об этом не знает — он просто предлагает более короткую последовательность.

Гарантия корректности живёт в раннере, а не в arbitrary: StateMachine::check() перепроверяет preCondition() против бегущей модели для каждой команды в реплеенной последовательности и пропускает любую команду, чья precondition больше не выполняется, вместо того чтобы упасть или бросить исключение:

foreach ($sequence->commands as $command) {
    if (!$command->preCondition($model)) {
        continue; // shrinking инвалидировал этот шаг — пропустить, не падать
    }
    // ... выполнить, проверить postCondition, продвинуть модель ...
}

Это осознанный контракт, а не пробел, который нужно закрыть: ревалидация каждого кандидата внутри arbitrary означала бы повторный прогон команд против реальной модели на каждой попытке шринка (не только принятых шагах) — а это ровно та дорогая работа с side-эффектами, которую shrinking должен избегать до тех пор, пока кандидат не подтверждён как всё ещё падающий. Skip-on-replay держит каждый shrink-кандидат дешёвым в предложении и корректным в исполнении — последовательность в строке Shrunk: всегда та, которую StateMachine::check() реально прогнал команда за командой, а не та, что незаметно пропустилась в «прошла».

Как читать shrunk-трейс

Property falsified after 7 successful run(s); seed=42
  Original: sequence=[Push(3), Pop(), Push(5), Push(1), Pop(), Pop()]
  Shrunk:   sequence=[Push(0), Push(1), Pop()] (9 shrink step(s))
  Failure:  Postcondition failed at step 3 for command Pop(); sequence: [Push(0), Push(1), Pop()]

Шесть команд сжались до трёх: удаление блоков урезало с шести до трёх (отбросив Pop(); Push(5)), затем упрощение по командам свело Push(3) к Push(0). step 3 в строке failure считает только реально выполненные команды — шаг, пропущенный из-за инвалидированной precondition, не двигает счётчик шага, поэтому он остаётся согласован с тем, что вы посчитаете, читая список sequence: слева направо.

См. State machine: концепции — Command, Gen::commands() и полный разобранный пример.