Про формальную валидациюю иишечки

Многие задачи проектирования можно свести к взаимодействию нескольких акторов: пользователь-интерфейс, сервис-сервис и т.д. Каждое взаимодействие имеет конечное количество исходов: успешная обработка, бизнес-ошибки, технические проблемы -- и может изменять состояние актора.

При желании мы можем построить полный сценарий взаимодействия со всеми возможным вариантами взаимодействий плюс стейт машину, где каждый переход соответствует атомарному взаимодействию. Будет выглядеть как гигантский сиквенс, из которого мы разворачиваем еще большую FSM. А если упороться еще дальше, то можно сразу строить сеть Петри.

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

Зачем?

Внимательные смотрим, что получилось, и берем сценарии, которые реально нужно реализовать — крайне сомнительно

Валидируем по получившейся сетке сценарии, которые спроектировали до этого. Это интереснее, потому что мы можем:

• просто запихать доки в агента и получить результат
• построить формальную модель для валидации с помощью второго агента
• провалидировать результат из п.1 по модели из п.2 следующим агетном

При желании валидацию можно повторить несколько раз.

Товарищи подсказывают, что строить модель и валидировать по ней решение с помощью агентов ну никак нельзя, потому что они недетерминированые. Это кажется приемлемым, т.к. мы можем принять не абсолютную точность.

Вторая проблема: не по каждой модели и сценарию можно провести за условно конечное время (P / NP), особенно если агент накосячит при построении модели. Вот это кажется серьезнее.

Про сожженные токены думать не будем, не для этого нам игрушки делали.

Если вы дочитали до этого момента, и тоже думали, пробовали, слышали о чем-то таком — напишите же!

P.S. На втором курсе у нас было матмоделирование вычислительных систем, кто бы знал, где и как вспомню о нем.