Задание цветовых множеств, переменных и начальной маркировки

Для раскраски сети необходимо задать цвета и объявить переменные для фишек. Сделать это можно в меню Declarations:

▼ Declarations

▼ Standarddeclarations

► colorE

► color INT

► color BOOL

► color STRING

Для того, чтобы создать переменные для новой сети, необходимо нажать правой кнопкой «мыши» по вкладке Declarations и выбрать в контекстном меню пункт Append Decl. Чтобы удалить объявленные переменные, нужно выбрать пункт Delete Decl. Для объявления переменной и присвоения ей значения необходимо «перетащить» созданную переменную на рабочую область, как показано на диаграмме.

Далее необходимо для каждой позиции задать свой цвет (тип). Для этого нужно выделить необходимую позицию и нажать клавишу TAB. Рядом с позицией появится подпись TYPE, на ее место следует вписать нужный цвет.

Затем для каждой позиции следует указать начальную маркировку. Для этого нужно нажать еще раз клавишу TAB. Появится надпись INITMARK, на это место вписывают начальную маркировку для данной позиции в виде мультимножества: «количество» «`» «тип» (например: l`р). Эту операцию нужно проделать для каждой позиции.

Выражения на дугах можно записать следующим образом. Мышкой выделяется дуга, рядом с ней появляется надпись: " ехрг". На это место вписывается выражение в виде мультимножества: «количество» «`» «тип» (например: 2`p) или в виде логического выражения. Эту операцию нужно проделать для каждой дуги.

После того, как записаны все маркировки и проставлены все выражения на дугах, можно приступать кпрогонке сети. Это осуществляется следующим образом: в МЕНЮ выбирается пункт Tool Box, в нем подпункт Simulation, который, зажав его левой кнопкой мыши, перетаскивают в рабочую область.

В подменю Simulation имеется возможность запуска проверки сети по одиночным шагам или на несколько шагов сразу.

Количество шагов задается в меню Simulation в пункте Play параметром Number of steps.

Позиции одного типа раскрашиваются одинаково. Переходы, которые могут сработать на следующем шаге, подсвечиваются зеленым цветом.