Haskell: Как протестировать (реактивный) FSM с помощью quickcheck?

Question

Я написал конечный автомат для небольшой футбольной игры, в которой я сейчас работаю. Он предоставляет интерфейс для настройки FSM (в основном, его состояний и переходов). Для каждого состояния вы можете предоставить функции, которые будут запущены при входе и выходе или пока FSM останется в одном состоянии, эти функции затем возвратят некоторые сообщения. Он также обеспечивает реактивный интерфейс (Yampa), который дает изменяющееся во времени состояние и собирает сообщения, которые происходят со временем. Код находится здесь Data/FSM.hs.

Я ищу хороший подход для тестирования этого модуля. Поскольку он чист, я подумал о том, чтобы попробовать quickcheck. Я не знаком с быстрым чеком, поэтому любой совет будет оценен! Мое основное понимание до сих пор: можно было бы предоставить некоторые функции, которые будут создавать FSM более или менее случайным образом, а затем запускать некоторые (снова более или менее случайные) переходы на них. Но я не могу понять, как построить тест таким образом ...

Answer 1

Прежде всего, QuickCheck, вероятно, лучше всего подходит для проверки общих общих свойств. Для произвольных данных какого-либо типа выполните некоторые операции, затем используйте предикат, чтобы гарантировать, что результат имеет некоторое свойство относительно ввода. То, что связано с точными деталями поэтапного поведения, может не так хорошо работать в этом стиле, и вы не должны чувствовать себя обязанным делать все в QuickCheck!

При этом, основываясь на более сложном примере, который вы указали в комментарии, вы считали, что просто генерируете ожидаемый результат вместе с FSM и входами? Если вы можете создать желаемый результат, который, как вы знаете, правильный по конструкции, вы можете запустить FSM на входе и сравнить фактический результат с построенной версией.

Это может помочь, если вы избегаете думать о свойствах QuickCheck как проверке функции на некотором входе, а скорее проверяете, удовлетворяет ли одно или несколько значений некоторым предикатам, выраженным в терминах тестируемой функции. Этот набор значений (который может включать в себя несколько входов, выходов, независимо от того, что необходимо) - это то, что на самом деле генерируется QuickCheck QuickMail.