Открыть файл TwoPhase_Task.tla в любом текстовом редакторе и дописать определения, обозначенные ???, в соответствии с материалом лекции.
Установить TLA+ Toolbox, открыть остальные приложенные и обсуждавшиеся на лекции примеры, создавать модели, проверять свойства и анализировать состояния моделей.
Решить задачу о волке, козе и капусте средствами TLA+.