Приложение 3.
Каталог примеров по формализации знаний

В приложении описана (авто)формализация профессиональных знаний до уровня постановок задач, включающих определение объектов и алгоритмов решения. Включены элементы алгоритмизации и программирования для информашин. Вместе с Приложением 4 оно относится к когнитивному обеспечению информатизации и выделено для удобства использования.

Далее будут показаны конкретные случаи визуализации знаний, представляющие как теоретический, так и практический интерес.

Здесь приводятся примеры визуализации задач с применением комплекса языков из числа рассмотренных в данном документе.

Задачи автоматизации (управление реальными объектами)

Управление двумя клапанами (визуализация автоматной спецификации системы)

В примере визуализирована по графит-методу система взаимодействующих процессов, реализующая решение задачи взаимосвязанного управления двумя клапанами¹. Машобраз текстового описания доступен здесь.

Пример базируется на результатах визуализации в примере из п. 1.1.1.

Чтобы специфицировать решение на Promela, нам потребуются некоторые абстракции. Так, процессы внешней среды (в клапанах как объектах управления, на пульте как объекте связи с операторами) нужно представить самостоятельными Promela-алгопроцессами.

Считаем, что алгопроцессы среды взаимодействуют с автоматными алгопроцессами по рандеву-каналам, играющим роль ранее определённых портов ввода/вывода. Очевидно, алгопроцессы среды д.б. «зациклены», причём каждый их тип исходит из следующих посылок.

Алгопроцесс КнопкаОткрыть (и аналогично КнопкаЗакрыть):

Генерация состояний отражает поток воздействия на кнопку оператора. Имея в виду, что выход кнопки – это логическая переменная, соответственно представим её значения; условия на эту переменную сводятся к проверке этих значений.

Отметим, что на пульте применение двух кнопок обусловлено эргономикой: человеку удобнее воспринимать и подвергать воздействию два разных органа управления, а не один (напр., кнопку, которую можно нажимать/отжимать), что для «небытовых» целей приобретает решающее значение.

Сверхцикл представляет процесс отпирания/запирания; вариации отражают реально возможный разброс времени отпирания/запирания.

Команда исходя из постановки задачи представляется парой сигналов на привод; смена команды есть [квази]одновременное изменение значений этих сигналов на противоположные.

Применение двух линий для передачи взаимообратных сигналов одиночными информативными состояниями (вместо одной, принимающей два информативных состояния) обычно для повышения помехоустойчивости (если единичная линия самопроизвольно перейдёт в другое состояние, это может привести к необнаруживаемой ложной команде; при наличии другой линии сохранение ею состояния однозначно будет означать ложность изменения, т.к. состояния станут одинаковыми; необнаруживаемым будет только парный переход в противоположные состояния, но вероятность такого перехода мала).

Исходя из этих посылок и определяются недостающие процессы модели. Головным процессом является инициирующий, вводимый по правилам языка.

Очевидно, что значения для выходов кнопок (команд от пульта автоматам) не обязаны быть взаимообратными или пассивными (т.е. не м.б. исключено наложение нажатий сразу двух кнопок). В то же время от автоматов клапанам должны идти единообразные команды (оба клапана должны открываться либо закрываться, либо (без команды) сохранять достигнутое крайнее положение).

Для обеспечения единообразия м.б. определён пультовой процесс (от кнопки <Открыть/Закрыть>), который о каждом состоянии посылает два сообщения по каналам открытия со взаимообратными значениями; но согласно постановке задачи существуют две отдельных кнопки без памяти. Поэтому детерминация при одновременном нажатии двух кнопок возлагается на автоматные алгопроцессы.

Заметим, что существуют органы управления, отвечающие определению единого пультового процесса, это кнопки, связанные (обычно [электро]механически) в блок так, что действие на одну кнопку переключает весь блок. Тем самым разрешается возможная неопределённость пультовых команд; однако это справедливо только для исправного блока кнопок. Поэтому возможность целесообразного реагирования автоматов на наложение входных сигналов взаимоисключающего смысла важна для гарантоспособности системы управления.

Отметим некоторые особенности информатизации модели.

Смысл различается в том, что Promela-программа фактически используется для моделирования рабочей Оберон-07-программы. При этом применяются некоторые специфические возможности языка Promela (такие, как атомизация цепочек операторов), если они выражают свойства, которые либо обеспечиваются при исполнении рабочим кодом, транслированным с Оберона-07 (в комплексе с исполнителем) естественно, либо являются допустимыми абстракциями от этого комплекса.

В модели генерация будет оформлена алгопроцедурами; первоначально соответствующие тексты будут заменены простейшими определениями, играющими роль «заглушек».

Определения вводятся через механизм областей. При этом используем возможности вложения областей друг в друга. Предполагается, что вложение «впритык» интерпретируется в РДП-редакторе как строгая иерархия; при этом можно повышать (или сохранять) уровень формальности языка содержания области.

В комментариях к областям вкратце раскрыт смысл алгопроцедур генерации.

Далее рассмотрим построение различных типов процессов.

Начинаем с общего описания модели. Используем ПК-язык для графит-определения состава и структуры модельной программы (в источниках по языку и среде используется термин «спецификация», но мы закрепили его за описанием математически формальным).

Т.к. Promela не является компонентным языком, то программа на нём может трактоваться как одномодульная; в каждый момент среда Spin обрабатывает (исполняет, верифицирует) одну модельную программу (чтобы подчеркнуть это, эргоимя головного процесса уточнено именем среды). Эта программа должна содержать всё необходимое для описания, включая определённое для других программ. Структура определений в принципе совпадает с традиционной: величины, определяемые глобально; типы (включая определения типов процессов); процессы (экземпляры типов, порождённые операторами пуска в головном процессе и/или других процессах и/или глобально).

Программа содержит средства управления совместно протекающими алгопроцессами; в основном они сосредоточены в головном пусковом процессе Init и/или распределены по модельным процессам (в виде рандеву-операторов запуска одних процессов из других).

Отметим, что процедур в языке нет; единственное, что можно представить как «процедурную часть определений модуля» – это операторы глобального порождения экземпляров процессов (active) и/или начального присваивания значений переменных; мы здесь их использовать не будем.

Соответственно зададим в ПК-модуле состав сущностей модельной программы.

Все сущности определим в таблице имён согласно общеязыковым требованиям. Таблица подразделена (двойными границами строк) на секции так же, как ПК-модуль.

Таблица имён – это своего рода узловой элемент РДП-документа; в РДП-редакторе она доступна из любого вхождения любого имени в документе (если трактовать это вхождение как гиперссылку на строку таблицы, то на эту строку можно переходить «по щелчку», как в гипердок-смотрителе). Предполагается, что она может содержать и записи о других типах сущностей, вводимых общеязыковыми определениями (таблицах индексов документа, РДП-листах, областях); но здесь мы ограничились сущностями графит-Promela-программы.

Строка предоставляет базовые сведения об именованной сущности (заполняемые сочинителем); также через неё можно переходить от одного вхождения имени к другому (по списку номеров п/п); она используется для выбора имени при «подстановке по списку»; кроме того, по ссылке на источник можно получить доступ к развёрнутым определениям сущностей (используемым при построении графит-схем и при их трансляции в тексты; обычно сами определения не редактируются, а заполняются по результатам визуального редактирования схем).

Выберем структуру модельной программы с головным процессом, пускающим целевые.

Видно, что каждый целевой процесс запускается своим оператором. Дело в том, что условный «системный канал» для пусковых собщений один и поддерживает коммуникацию «один к одному»; это отражает тот факт, что программа выполняется на непараллельном исполнителе, который реально не может одновременно работать со многими процессами.

Единственное, что стоит сделать – атомизировать последовательность запуска средствами Promela (здесь представлены ДО7Pr-операторами, специфичными для Promela, на что указано в их тексте).

Декларативная часть представлена как АТ-модель; деклар-компонента каждого процесса представлена своей АТ-схемой.

В головной схеме даны общепрограммные (глобальные) определения; при этом АТ-процедуры в секции процессов без «своих» АТ-тел служат, помимо прочего, указаниями на АТ-схемы этих тел (по совпадению имён).

Указанные компоненты описания в формате РДП показаны на следующем рисунке:

Общая часть графит-ЯВС-модели управления клапанами для среды Spin

Здесь и далее мы даём только содержание, без макетирования структуры РДП-документа.

Для чтения следует иметь виду описанные ниже особенности макетирования механизма Область.

Атрибуты, которые не д.б. видимы у реальной области (открываются для просмотра/редактирования по командам, напр., через контекстное меню области), имеют пунктирный контур.

Поля подстановок текста при вхождении области показаны в тексте именами полей, взятыми в квадратные скобки (выделены оранжевым цветом); в реальной области на этих местах находятся сами результаты подстановок (правые части SUBTEXT-правил, в левой части которых то же имя поля). Имя поля является ссылкой, по которой д.б. возможен переход от поля к определяющему правилу и обратно (как для любого имени в документе).

Списки индексов вхождения у каждой вынесенной области даны полностью; реально список может раскрываться, а отображаться один (выбранный читателем для текущего ознакомления) индекс.

Если входящая область пуста (а у полной в индексе присутствует код варианта), то предполагается наличие вынесенных областей; в этом случае оператор получает сведения о них (напр., раскрывая список вариантов по щелчку на нём) и выбирает нужную для перехода.

Область, как и схема, имеет статус сочинения. Значение <auto> для входящих областей в данном случае отражает ещё одно свойство, которое целесообразно придать механизму Область: её содержание выбирается из вариантов автоматически, если статус исполнимых (транслируемых) имеют не все варианты (или не имеют вообще никакие; тогда вся схема в принципе неисполнимая).

Появление в индексе входящей области кода языка, совпадающего с языком включающей схемы, указывает на различие языков вариантов уже при чтении самой схемы (напомним, что в РДП-документе вынесенные области размещаются произвольно и не обязаны быть все рядом друг с другом и/или со схемой, как на данном РДП-макете).

Генерация состояний кнопок имеет целью имитировать их нажатия оператором. Можно было бы предоставить возможность ручного ввода (напр., с клавиатуры), но эти средства в Promela отсутствуют; в самом деле, модель предназначена для автоматического «обсчёта». Поэтому нужно задаться каким-то распределением вероятности пребывания каждой кнопки в нажатом и отжатом состояниях (имея в виду, что эти состояния образуют полную группу событий).

Предполагаем, что продолжительность нажатого состояния крайне невелика (один-несколько циклов), а интервалы отжатия, напротив, весьма велики и непостоянны. Соответственно кнопка изначально (при запуске) пребывает в состоянии, выбранном согласно постановке задачи.

Начальное состояние предопределим присваиванием значения переменной; оператор поместим до автоматного цикла (в отличие от силуэтной формы, это не потребует отдельной ветви; ЦД в прогязыках – это обычный сложный оператор, сочетающийся в программе с иными без каких-то особенностей). Изменив алгоритм, можно задать состояние в пусковом процессе (передавая конкретное значение как фактический параметр).

В любом состоянии прежде всего посылается его код связанному автоматному алгопроцессу (интерпретируется как значение выхода кнопки). Далее внутри состояния отжатия кнопки случайно выбирается, будет ли оно сохранено на следующем цикле; если нет, то случайно выбирается длительность нажатия и готовится переход к состоянию нажатия кнопки. В нём значение длительности инкрементируется, затем проверяется равенство его нулю; пока оно не выполняется, готовится переход к текущему состоянию, по выполнении – к состоянию отжатия кнопки. Переход реально происходит в «шапке» цикла Дейкстры.

Передача кода состояния кнопки как сообщения, конечно, абстракция – реальная кнопка в каждом состоянии «передаёт» непрерывный сигнал (не считая возможного дребезга контактов :)); но мы считаем такую абстракцию допустимой (в т.ч. потому, что реальный дискретный исполнитель программы управления – цифровая информашина – будет именно периодически опрашивать состояние входного порта, подобно тому, как Promela-модель исполнителя – процесс Автомат <N> – опрашивает каналы сообщений). Кстати, дребезг можно было бы моделировать через невозможность рандеву (которая м.б. проверена в языке) – но это несколько искусственно.

Простейшее (предварительное) определение процедуры генерации мы ввели как единичное действие с неформальным текстом.

В данном случае мы ввели наружную область с менее формальным языком, чем у включающей схемы. Это дало возможность описать действие по генерации нестрого. Затем мы детализировали это действие через охватывающую область, выбрав для неё снова более формальный язык – в данном случае тот же, что на схеме. Детализацию оформим как вариант (вынесенный); содержанием области-варианта служит вначале действие; впоследствии будет построена схема алгоритма псевдослучайной генерации.

Различие языков вложенных областей, влияющее на исполнимость, отражается статусом сочинения <auto>.

Порассуждаем теперь о построенном алгоритме и посмотрим, можно ли его улучшить.

Задавать определённое состояние нужно, поскольку алгоритм кнопки несимметричен: логика состояний не совпадает, причём второе зависимо от первого. В то же время можно сделать эту логику единообразной. В самом деле, если считать, что «бросание монет» может обеспечить различную вероятность исхода (как параметр процесса генерации, записанный в скобках), то можно заменить им «бросание костей» на длительность; тогда маршрутная структура ветвей-состояний легко унифицируется. И это значит, помимо прочего, что неважно, с какого состояния запускается алгопроцесс; любая ветвь «сыграет свою роль», выполнив независимо ожидаемое (исходя из параметра генерации) число циклов, а затем переход в другое состояние (которому не требуются какие-то данные от первого). Как следствие, в этом варианте не обязательно начальное присваивание.

Также унификация распространима на переменные выбора состояния; можно обойтись одной. Более того мы можем «бросать монету» непосредственно на переменную состояния (псевдослучайно выбирать её значение для следующей итерации ЦД); при этом не нужно специально выбирать и присваивать новое значение этой переменной – оно задано уже «бросанием монеты».

Заметим себе, что варианты процесса неэквивалентны; «ритмический рисунок» (длительности прохождения отдельных участков маршрута, в частности, между выдачами кодов состояния кнопки, и частота появления того или иного состояния) в одинаковых условиях исполнения (на одной машине) будет разным. Это определяется разницей как в длительностях маршрутов каждого состояния (за счёт разного их операторного наполнения – нагрузки), так и в закономерностях выбора состояний (которые заложены в процедурах генерации). Можно пытаться «подогнать» эти закономерности количественно, подбирая (математически рассчитывая) параметры генерации для второго варианта так, чтобы максимально приблизить распределение состояний к первому. При моделировании параллельных процессов длительности нас не интересуют (в силу упомянутого принципа абстрагирования от временных характеристик); но можно пытаться подогнать и здесь характеристики вариантов. Но необходимости ни в том, ни в этом нет – дело в том, что над количественным пониманием смысла задачи стоит качественное².

В данном случае задача – моделировать недетерминированное изменение состояния кнопки человеком (является подзадачей в рамках моделирования всей системы). Качественно цель моделирования мы уже формулировали – задать распределение, при котором длительность пребывания кнопки в нажатом состоянии будет много меньше, чем в отжатом (измеряется в циклах состояний). Т.е. переходы от отжатия кнопки к нажатию будут редкими, а от нажатия к отжатию – напротив, частыми. Это качественное понимание сути обеспечивает и первый вариант, и второй. Если же нужно будет максимально точно выполнить конкретный количественный закон распределения состояний – то в любом варианте для этого нужно будет спроектировать соответствующим образом процедуры генерации.

Удобно показать варианты процесса опять-таки посредством областей. В этом случае правильно охватить областью всё тело схемы.

Также областями (только теперь пустыми во всех вхождениях) мы показываем генерацию значения состояния.

Видно, что теперь используется одна процедура генерации (повторно в разных состояниях); т.о. мы можем повторно использовать её код.

Собственно, мы могли бы оформить процедуру как вставку. При использовании вставки нам не нужны и области, входящие в схему; только область для определения тела вставки (пока оно не написано). Но нужно учитывать, что Promela – язык без процедур. Поэтому мы можем использовать код повторно только на этапе сочинения (включив повторяющийся код заранее); эту возможность нам и обеспечит механизм Область.

В Оберон-07, напротив, есть процедуры. Возможно, что по условиям применения рабочей программы их использование будет обязательно (скажем, для экономии в объёме текста и его кода); в этом случае нужно будет определить ещё и Оберон-варианты участков с процедурами (выбираемые вместо Promela-вариантов для трансляции в Оберон-исхтекст). Это усложнит графит-модель; более существенным может оказаться различие в поведении таких вариантов (появятся особенности рабочей программы, не учитываемые в модельной).

Дело за малым – написать эту процедуру – точнее, тело :) Тогда РДП-редактор при трансляции автоматически подставит тело в каждое место вхождения. Пока что мы ограничились созданием автономной области (имеющей, как видно, самостоятельный индекс в пределах документа), в которой будем писать; затем эту область можно композировать.

Отметим, что новый вариант читать несколько сложнее; так, нужно понять, что переменная состояния логического типа позволяет сокращённо записывать простейшие условия развилок (опуская отношение к её истинному значению); явные присваивания состояний на выходах ветвей ЦД в исходном варианте также «разжёвывали» логику исполнения. Это обычная плата за оптимизацию кода – и не столь большая, принимая во внимание информативность графит-синтаксиса модели в целом (включая табличные описания).

Результаты оформлены как комплексная графит-модель на рисунке ниже:

Графит-ЯВС-модели кнопок управления клапанами для среды Spin

Здесь мы также приводим частные АТ-схемы (связанные с общей через её АТ-процедуры).

Видно, что вынесенные области в основном используются в разных отношениях (рядах) вхождения; в этом случае у области более одного индекса. При этом подстановки разрешаются только по месту вхождения в схему; поэтому вхождение одной вынесенной области в другую вынесенную не содержит правил подстановки (атрибута SUBSTEXT).

Следует понимать, что в реальном РДП-редакторе правила вхождения областей выполняются автоматически; поэтому читатель будет видеть на месте имён полей подстановки (взятых на макете в квадратные скобки) результаты (тексты, подставляемые по SUBSTEXT-правилам). И читать содержание реальных областей будет проще (на макете же читатель должен мысленно выполнять подстановки, что, конечно, затрудняет чтение). В то же время и в реальном документе поля должны зрительно выделяться по крайней мере для сочинителя, допустим, так, как на макете (цветом); также поможет переход от поля к определяющему правилу и обратно (как для любого имени в документе).

Работа сочинителя над подстановками м.б. полезна в плане унификации текстов. Это хорошо видно на данном примере; использованы разные тексты для обозначения одной и той же сущности. Мы можем сокращать их состав (но не за счёт удобства понимания).

Второй алгопроцесс данного типа (для кнопки «Закрыть клапаны»), как видно, написан сразу по усовершенствованному образцу, без вариантов. При этом неважно, будет ли первый алгопроцесс того же образца; напомним, что теория параллельных (совместно-одновременно протекающих) процессов исходит из абстрагирования от динамических свойств процессов при формальном анализе их взаимодействия. То, что процесс в исходном варианте будет иметь другой «ритмический рисунок» исполнения (в силу различности маршрутов в одних и тех же ветвях-состояниях), можно считать «особенностью реализации» кнопки «Открыть клапаны» :)

АТ-схема для первого алгопроцесса единая, также имеющая варианты; в первом алгоритме вариант А использует дополнительные переменные, объявления которых нужно подставить в АТ-схему (для наглядности определено полное замещение содержания ветвей с этими объявлениями). Для второго алгопроцесса АТ-схема своя, разумеется, без вариантов.

Здесь мы предполагаем ещё одно свойство, желательное для механизма Область; сопряжение отношений вхождения по разным родовым семействам языков (здесь – декларативному и императивному). В силу этого области подставляются для разных семейств, исходя из общности номера отношения в индексах.

Условие подстановки «Осн?: ...» для варианта АТ-схемы сформулировано явно; однако можно возложить его контроль на РДП-редактор (в этом случае от сочинителя требуется только правильно задать индексы для разных семейств языков – они должны отличаться только кодом языка).

Мы могли бы допустить и для входящих областей множественность отношений подстановки; при этом входящая область также может иметь список индексов. Однако получающееся при этом многообразие уже трудно контролировать при работе с документом; поэтому такое расширение смысла подстановки – вопрос дискуссионный.

Мы будем пользоваться только множественностью подстановок для вынесенных областей.

Т.к. наша модель всё-таки предназначена для верификации, определим хотя бы одно проверяемое условие. Очевидна возможность проверить значение переменной состояния на входе второй ветви, т.к. оно выбирается как «любое другое, кроме ложного», без точной проверки значения.

В случае булевой переменной это может показаться необязательным; ведь она и так принимает только два значения – не одно, так другое – бит в принципе не может принять ещё какое-то значение (хотя может принять одно из двух ошибочно – допустим, из-за сбоя). Но это на уровне программного представления – при реализации на аппаратуре возможно, что булевы значения представляются не однобитно, а, допустим, байтами (если нет команд работы с более короткими кодами); тогда булевы значения кодируются комбинациями бит – и здесь возможность «ещё какого-то» значения (возникающего опять-таки по ошибке) не вызывает сомнений.

Оператор проверки Д2М-языка прямо представляет Promela-оператор (assert). Его действие в принципе то же, что приводит к хорошо известному пользователям негарантоспособных инфопрогов сообщению «Программа выполнила недопустимую операцию» :) и потому в реальной системе д.б. заменено на процедуру целесообразной обработки ситуации.

Автоматные алгопроцессы эквивалентны СЦД-вариантам из спецификации (с точностью до имён величин).

Здесь также учитываются различия рабочей и модельной программ. Ведь на модели операторы ввода/вывода были заменены на отправку сообщений; в рабочей программе их нужно сохранить.

Различия снова оформим посредством областей.

Алгопроцесс объекта (комплекса «клапан-привод-датчики») логично организовать по образцу автоматного; разумеется, логика состояний будет специфическая (хотя их состав тот же).

Со «своим» автоматным алгопроцессом объектовый обменивается уже не номерами состояний, а значениями объектовых переменных. На первый взгляд это не соответствует принципу связи, принятому между автоматами; но здесь уже взаимодействуют не однородные сущности (автоматы-управители между собой), а управители и управляемые; просто и те, и другие представлены моделями с явным выделением состояний (напомним, что это и есть суть автоматного программирования).

Начальное состояние здесь также предопределим присваиванием.

Далее обсудим логику состояний (веток ЦД модельной программы, соотвествующих явно выделенным состояниям объекта) подробнее. Сразу отметим, что два состояния объекта динамические («Отпирается» и «Запирается»); в каждом из них наблюдаемые параметры объекта (представленные вовне датчиковыми переменными) должны меняться, пока действует команда, вызвавшая переход в это состояние. Два других статические (в них объект должен сохранять наблюдаемые параметры неизменными).

Состояние объекта в динамике моделируется, как уже говорилось, сверхциклами отпирания/запирания над циклами динамических состояний в модельной программе. Эти состояния независимы от состояний автоматов (но возникают по их командам на приводы). Параметр сверхцикла и есть величина, моделирующая динамику состояния; некое конечное его значение показывает, что объект достиг цели, определяемой командой на привод.

Автомат управления даёт команду, а затем должен ждать, пока клапан движется, движется, движется... (причём в первой же итерации датчик исходного положения клапана меняет значение — и сохраняет новое значение до перехода модели объекта в противоположное динамическое состояние).

Т.е. при определённом вычислительном состоянии автомата объект проходит (реально непрерывно; на модели — дискретно, итерациями ЯВС-цикла Дейкстры) последовательность состояний изменения положения клапана (реально бесконечную; на модели — конечную). Когда ей завершиться (переходом в статическое состояние, соответствующее достижению цели движения объекта) — на модели решается, как видно, опять-таки случайно («бросанием монеты» на номер состояния в следующей итерации модельного цикла). Как следствие, в новом состоянии автомату отправляется новое значение сигнала с датчика целевого положения — означающее достижение цели.

Заметим, что клапан может и не закрыться :) На модели это можно представить дополнительным маршрутом динамического состояния, в котором условие выбора состояния следующей итерации «застывает» на номере текущего. Но важнее — как должна отрабатываться ситуация «за конечное время не поступил сигнал с датчика, означающий достижение целевого положения клапана». Исходная спецификация не содержит решения; предполагается, что клапан откроется/закроется «когда-нибудь» (точнее — за допустимое время).

Здесь мы также оставим вопрос без решения; но зафиксируем его в комментариях. Тогда разработчики смогут выработать какое-то решение и реализовать его в программе каждого автомата - и рабочей, и модельной (ведь это тоже надо проверить).

Генерация продолжительности сверхцикла отпирания/запирания имеет целью ввести определённый разброс вокруг некоей продолжительности, принимаемой за эталонную. Поэтому тут имеем распределение с математическим ожиданием и отклонением.

Одновременность смены команд можно определить (для Promela-модели) атомизацией последовательности действий по их выдаче.

Можно унифицировать однотипные процессы для Promela, как предлагается в /Поликарпов, Шалыто, с. 68-69/, введя единые обобщённые имена переменных, имеющих общий смысл, как формальные параметры, и передавая конкретные имена как фактические параметры запуска (создания процесса как proctype-экземпляра); но следует определить, является ли такая абстракция допустимой относительно реально исполняемой Оберон-07-программы (где нет такого механизма порождения и каждый конкретный процесс описывается и кодируется отдельно – если не применять специальных «объектных» приёмов³, соответствие которых средствам Promela нужно ещё уточнить).

С учётом сказанного можно построить ДО7Pr-модель, визуализирующую Promela-текст.

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

1 Источник: Поликарпова Н.И., Шалыто А.А. Автоматное программирование. – СПб.: Питер, 2010. – п. 2.1.2.

2 О соотношении количественного и качественного см., напр., в п. «Комьютеру-компьютерово, остальное-человеку» статьи: Бестужев-Лада И. Человек и машина: кто есть кто? // Техника-молодёжи, №7/1983. – С.10-13.

3 Для языков Оберон и Оберон-2 некоторые приёмы изложены в: Свердлов С.З., 2007- С.159-173.