Как осуществляется верификация компьютерных ролевых игр?
==========================================================

 Предположим, в игре (наподобие Fallout) есть разветвлённая система диалогов. Одни ветки диалога появляются, другие исчезают. Исчерпывающее тестирование крайне затруднено.  
  

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

* Из любого состояния игра проходима.  

* Игрок сможет сотрудничать с любой из семей Мордино, Сальваторе, Бишоп или Райт, но только с одной.  
  

Ну и, разумеется, проверялка должна писаться за пару дней: всё-таки пишем не проверялку, а игру. А может, можно обойтись вообще без проверялки — сама модель устроена так, что видно, в какое состояние она может зайти, а в какое — нет.  
  

Сети Петри? Даже они, кажется, сложны и их надо ограничивать чем-то — например, фишки не появляются и не исчезают. 

 У меня есть одна идея. Построим несколько конечных автоматов. Для каждой реплики задаются:  

— автомат (ноль или один);  

— набор состояний, в которых реплика видна (одно или несколько; имеет смысл, если автомат задан);  

— куда автомат переключить;  

— какие-то дополнительные условия, зависящие от игры (например, уровень интеллекта или разговора);  

— ссылка на функцию-спецусловие (таковых должны быть пара десятков на весь большой Fallout).  

Например, для четвёрки «Мордино/Сальваторе/Бишоп/Райт» состояний будет пять: ни с кем и с какой-то из семей. Тогда достаточно увидеть, что из Мордино нельзя перейти ни в какое другое, вот тебе и доказательство: ты член банды Мордино на всю жизнь. А если какая-то линия диалога включает спецусловия или два автомата одновременно — проверялка выведет сообщение: тут будь настороже.  
  

У некоторых автоматов может быть одно или несколько «конечных» состояний — можно наладить иерархию автоматов. Автоматы верхнего уровня могут требовать, чтобы нижестоящие были в конечном состоянии, но не наоборот.