Есть ли такой инструмент? Скажем каждый объект это конечный автомат, состояние которого меняется полученным сообщением (актор). Сам он может менять состояние других. Все связаны каждый с каждым. Теперь, для примера на такой сети запускаем программу «Жизнь».
Реально формально описать эту модель с графами переходов состояний и доказать, что полученная модель свободна от дедлоков?
Совсем хорошо, если из нее можно получить код эрланг или с.
