Может быть это были одни и те же корейцы даже.

Один и тот же кореец

Добрый день. Такой вопрос:
У меня есть два компонента (Raspbry + система управления питанием), которые между собой взаимодействуют как конечные автоматы.
Я бы хотел чтобы в комплексе эти две вещи работали максимально "правильно".
У меня есть
1. цепочки переходов состояний  заданные мной, которые приводят к "хорошим" состояниям.
2. цепочки переходов состояний  заданные мной, которые приводят к "плохим" состояниям. но они известны и я готов с ними жить.
Я подумал что я могу использовать FsCheck для того чтобы найти хитрые комбинации событий в системе, которые я не жду и которые приведут к нежелательному дя меня результату.

Пока у меня не получается придумать разумные инварианты. Как я понимаю в терминологии FsCheck это Property. Потому я решил начать с простого и задать вопросы
1. FsCheck это разумный выбор для подобной задачи?
2. Есть ли какие то рекомендации как формировать инварианты для конечных автоматов?

Ну у тебя есть карта переходов из состояния в состояние, как я понимаю

могу сделать в принципе.

Далее , тебе надо составить список правил

Что считать невалидным в результате цепочки преобразований

Например, что ты не можешь попасть из состояния А в состояние Б за н шагов

Я тоже помню. Пионеры F# в Корее

Или состояние С не должно встречаться в цепочке больше одного раза

Потом пилишь генератор и наслаждаешься

Если автоматы асинхронные, то Microsoft Coyote может подойти

правильно ли я понимаю что в качестве модели проверяющей реализацию, будет набор
- сколько шагов прошло с момента А
- сколько раз я попал в состояние С
такого рода утверждения будут для меня проверяющими свойствами, так?

спасибо за наводку, посмотрю.

простите еще раз, а что за кавычка в конце имени функции? plistoffloats'

говорит Plistoffloats prime, что за prime

или это просто название такое

Ну я хз, какие у тебя условия валидности

Это генерик

Типа type<T> в сишарпе