Спасибо за ссылку, Драконограф!

Воспроизвожу по полученной ссылке форму цикла Дейкстры в языке Promela из указанногоисточника:
## Код:
```
proctype Euclid(int x, y){ 
do
    :: (x > y) -> x = x - y 
    :: (x < y) -> y = y - x 
    :: (x == y) -> goto done 
od;
done: skip 
}
```

Здесьskip- пустой оператор, перед которым стоит меткаdone.



А вот как будет выглядеть тот же пример в PureBuilder:
## Код:
```
┌while
 │▼ x > y
 │    dec (x, y)
 │▼ x < y
└    dec (y, x)
```

Алгоритм функции записывается не внутри длинного программного кода, а в отдельной вкладке интерфейса. Поэтому заголовок функции отсутствует.

Объявление параметров и возвращаемого значения функции Euclid осуществляется в отдельной табличке.

Псевдографика не очень правильно передает скобку слева. На самом деле она непрерывная, с закругленными углами и полностью охватывает строки с while и dec (y, x).

Ключевые слова должны изображаться жирным шрифтом. Значки ▼ используются при необходимости сворачивания соответствующих ветвей цикла. При этом они принимают вид ►.