TLA + Как визуализировать граф состояний

Question

Я новый TLA+ пользователь. Я прочитал, что набор инструментов TLA позволяет нам визуализировать график состояний после завершения проверки модели.

Для этого нужно установить точку, что я и сделал. Но я не понял, как запустить визуализацию. Могу ли я купить его с помощью графического интерфейса или мне нужно использовать выделенную командную строку?

Спасибо

Answer 1

Для визуализации графика состояния вам необходимо:

1. Установите Graphviz на свой компьютер (что вы уже сделали).
2. Настройте TLA+ Toolbox так, чтобы он указывал на местоположение исполняемого файла dot на локальном компьютере: «Настройки» → «TLA + Настройки» → «Просмотр PDF» → «Указать точку». (На моей машине я установил graphviz с помощью homebrew, и моя команда /usr/local/bin/dot).
3. В вашей модели TLC: Дополнительные параметры → Параметры TLC → Визуализировать график состояний после завершения проверки модели (установите этот флажок)

Когда вы запустите вашу модель, появится вкладка State Graph с визуализацией Graphviz графика состояния.