...
Используется подход нарезанной трассы. Такой подход предполагает проверку какого-то определенного поля объекта, что существенно сокращает количество возможных перестановок.
На вход имеем некоторый алгоритм. Запускает его (тут не понял, зачем именно) Запускаем его и строит трассу.
Сперва записываем:
...
- Проходим по нашей трассе в обратном направлении, берем в нарезанную трассу события, которые непосредственно относятся к свойству P
- Берем в нарезанную трассу события, от которых зависит наше свойство P.
Для чего строим трассу? Потому что каждый поток делаем линейным. То есть, нам плевать, что где-то есть if конструкция, мы просто верим, что если изначально получилось что-то вроде if then, то при како-то перестановке на каких-либо данных получим аналогичное (скорее моя догадка, в статьях ничего не сказано по этому поводу).
На основе векторных часов записываем всё это в множество, в котором учитываем зависимости и атомарные блоки.
...