База ГОСТовallgosts.ru » 25. МАШИНОСТРОЕНИЕ » 25.040. Промышленные автоматизированные системы

ГОСТ Р ИСО 18629-42-2011 Системы промышленной автоматизации и интеграция. Язык спецификаций процесса. Часть 42. Дефинициональные расширения: временные расширения и расширения состояния

Обозначение: ГОСТ Р ИСО 18629-42-2011
Наименование: Системы промышленной автоматизации и интеграция. Язык спецификаций процесса. Часть 42. Дефинициональные расширения: временные расширения и расширения состояния
Статус: Действует

Дата введения: 09/01/2012
Дата отмены: -
Заменен на: -
Код ОКС: 25.040.40
Скачать PDF: ГОСТ Р ИСО 18629-42-2011 Системы промышленной автоматизации и интеграция. Язык спецификаций процесса. Часть 42. Дефинициональные расширения: временные расширения и расширения состояния.pdf
Скачать Word:ГОСТ Р ИСО 18629-42-2011 Системы промышленной автоматизации и интеграция. Язык спецификаций процесса. Часть 42. Дефинициональные расширения: временные расширения и расширения состояния.doc


Текст ГОСТ Р ИСО 18629-42-2011 Системы промышленной автоматизации и интеграция. Язык спецификаций процесса. Часть 42. Дефинициональные расширения: временные расширения и расширения состояния



ФЕДЕРАЛЬНОЕ АГЕНТСТВО

ПО ТЕХНИЧЕСКОМУ РЕГУЛИРОВАНИЮ И МЕТРОЛОГИИ


НАЦИОНАЛЬНЫЙ

СТАНДАРТ

РОССИЙСКОЙ

ФЕДЕРАЦИИ


ГОСТ Р исо 18629-42— 2011


Системы промышленной автоматизации

и интеграция

ЯЗЫК СПЕЦИФИКАЦИЙ ПРОЦЕССА

Часть 42

Дефинициональные расширения: временные расширения и расширения состояния

ISO 18629-42:2006

Industrial automation systems and integration —

Process specification language — Part 42: Definitional extension: Temporal and state extensions

(IDT)

Издание официальное

2014

Предисловие

1    ПОДГОТОВЛЕН Научно-техническим центром «ИНТЕК» на основе собственного аутентичного перевода на русский язык международного стандарта, указанного в пункте 4

2    ВНЕСЕН Техническим комитетом по стандартизации ТК100 «Стратегический и инновационный менеджмент»

3    УТВЕРЖДЕН И ВВЕДЕН В ДЕЙСТВИЕ Приказом Федерального агентства по техническому регулированию и метрологии от 22 декабря 2011г.№1611-ст

4    Настоящий стандарт идентичен международному стандарту ИС0 18629-42:2006 «Системы промышленной автоматизации и интеграция. Язык спецификаций процесса. Часть 42. Дефинициональные расширения: временные расширения и расширения состояния» (IS018629-42:2006 «industrial automation systems and integration — Process specification language — Part 42: Definitional extension: Temporal and state extensions»).

При применении настоящего стандарта рекомендуется использовать вместо ссылочных международных стандартов соответствующие им национальные стандарты Российской Федерации, сведения о которых приведены в дополнительном приложении ДА

5    ВВЕДЕН ВПЕРВЫЕ

Правила применения настоящего стандарта установлены в ГОСТР 1.0—2012 (раздел 8). Информация об изменениях к настоящему стандарту публикуется в ежегодном (по состоянию на 1 января текущего года) информационном указателе «Национальные стандарты», а официальный текст изменении и поправок — в ежемесячном информационном указателе «Национальные стандарты». В случае пересмотра (замены) или отмены настоящего стандарта соответствующее уведомление будет опубликовано в ближайшем выпуске ежемесячного информационного указателя «Национальные стандарты». Соответствующая информация, уведомление и тексты размещаются также е информационной системе общего пользования — на официальном сайте Федерального агентства по техническому регулированию и метрологии в сети Интернет (posf.ru)

©Стандартуыформ. 2014

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

Содержание

62 Описываемая лексика понятий для основанных на состоянии входных условий выполнения

6.3    Теории ядра, обусловленные основанными на состоянии входными условиями выполнения

6.4    Дефинициональные расширения, обусловленные основанными на состоянии входными

6.6    Грамматика соотношений для основанных на состоянии входных условий выполнения

8.4    Дефинициональные расширения, обусловленные временными и основанными на оостояжи

10.4    Дефинициональные расширения, обусловленные предотвращаемыми условиями выполне

я

11.4    Дефинициокальные расширения, обусловленные периодическими входными условиями

14.4    Дефиниииональные расширеии», обусловленные ооюванными на состоянии эффектами

17.4    Дефинициональные расширения, обусловленные эффектами действии: событийные ограни

18.4Дефинициональные расширения, обусловленные эффектами действий: временные и собы-

21.4    Дефинициональные расширения, обусловленные основанным на состоянии распределением

21.6    Грамматика описаний процесса для основанного на состоянии распределения комплексных

22.4    Дефинициональные расширения, обусловленные временным распределением комплексных

23.4    Дефинициональные расширения, обусловленные смешанным распределением комплексных

25.4    Дефинициональные расширения, обусловленные основанной на состоянии вариации комп*

лексных действий.....................................

25.5    Определения основанной на состоянии вариации комплексных действий..........

25.6    Грамматика описаний процесса для основанной на состоянии вариации комплексных дей-

ствий ............................................

26    временная вариация комплексных действий...........................

26.1    Примитивная лексика временной вариации комплексных действий.............

26.2    Описываемые соотношения временной вариации комплексных действий..........

26.3    Теории, обусловленные временной вариацией комплексных действий............

26.4    Дефинициональные расширения, обусловленные временной вариацией комплексных действий ............................................

26.5    Определения временной вариации комплексных действий.................

26.6    Грамматика описаний процесса для временной вариации комплексных действий......

27    Смешанная вариация комплексных действий...........................

27.1    Примитивная лексика смешанной вариации комплексных действий.............

27.2    Описываемые соотношения смешанной вариации комплексных действий..........

27.3    Теории, обусловленные смешанной вариацией комплексных действий...........

27.4    Дефинициональные расширения, обусловленные смешанной вариацией комплексных действий ............................................

27.5    Определения смешанной вариации комплексных действий.................

27.6    Грамматика описаний процесса для смешанной вариации комплексных действий......

28    Встроенные действия: планы...................................

28.1    Примитивая лексика встроенных действий: планы......................

28.2    Описываемые соотношения встроенных действий: планы..................

28.3    Теории, обусловленные встроенными действиями: планы..................

28.4    Дефинициональные расширения, обусловленные встроенными действиями: планы.....

28.5    Определения встроенных действии: планы.........................

28.6    Грамматика описаний процесса для встроенных действий: планы..............

29    встроенные действия: временной разброс............................

29.1    Примитивная лексика встроенных действий: временной разброс..............

29.2    Описываемые соотношения встроенных действий: временной разброс...........

29.3    Теории, обусловленные встроенными действиями: временной разброс...........

29.4    Дефинициональные расширения, обусловленные встроенным* действиями: временной разброс ............................................

29.5    Определения встроенных действий: временной разброс...................

29.6    Грамматика описаний процесса для встроенных действий: временной разброс.......

30    вариация неделимых вверх действий..............................

30.1    Примитивная лексика вариации неделимых вверх действий.................

30.2    Описываемые соотношения вариации неделимых вверх действий..............

30.3    Теории, обусловленные вариацией неделимых вверх действий...............

30.4    Дефинициональные расширения, обусловленные вариацией неделимых вверх действий . .

30.5    Определения вариации неделимых вверх действий.....................

30.6    Грамматика описаний процесса для вариации неделимых вверх действий..........

31    вариация неделимых вниз действий...............................

31.1    Примитивная лексика вариации неделимых вниз действий..................

31.2    Описываемые соотношения вариации неделимых вниз действий..............

31.3    Теории, обусловленные вариацией неделимых вниз действий................

31.4    Дефинициональные расширения, обусловленные вариацией неделимых вниз действий . . .

31.5    Определения вариации неделимых вниз действий.....................

31.6    Грамматика описаний процесса для вариации неделимых вниз действий..........

32    входные условия совместных действий.............................

32.1    Примитивная лексика входных условий совместных действий...............

32.2    Описываемые соотношения входных условий совместных действий............

32.3    Теории, обусловленные входными условиями совместных действий.............

32.4    Дефинициональные расширения, обусловленные входными условиями совмеспых действий

34.4    Дефинициональные расширения, обусловленные вариацией препятствующих входных

35.4    Дефинициональные расширения, обусловленные вариацией эффектов затирания полезных

Введение

ИС018629—это комплекс стандартов на компыотермо-интерлрвтируемый обмен данными обеспечения технологического процесса. Все части комплекса стандартов ИСО 18629 устанавливают групповой язык программирования для описания конкретного технологического процесса, рассматриваемого какчасть всего процесса изготовления изделия либо внутри одной промышленной компании, либо сразу в нескольких промышленных секторах (компаниях) вне его связи с какой-либо моделью компьютерного представления. Природа данного языка программирования такова, что он обеспечивает доступ кслецификациям технологического процесса и технологическим данным изделия на всех стадиях процесса его изготовления.

в настоящем стандарте установлены описания дефинициональмых расширений языка программирования. относящихся к расширениям действий в соответствии с ИС0 18629.

Все части комплекса ИС018629 не связаны с какой-либо конкретной моделью компьютерного представления технологического процесса. Все вместе указанные части ИС018629 обеспечивают структурную технологическую взаимосвязь процессов производства для улучшения оперативной совместимости рассматриваемых технических приложений.

уи

НАЦИОНАЛЬНЫЙ СТАНДАРТ РОССИЙСКОЙ ФЕДЕРАЦИИ

Системы промышленной автоматизации и интеграция ЯЗЫК СПЕЦИФИКАЦИЙ ПРОЦЕССА Часть 42

Дефинициональные расширения: временные расширения и расширения состояния

Industrial automation systems and integration. Process specification language.

Part 42. Definitional extension. Temporal and state extensions

Дата введения — 2012—09—01

1    Область применения

Настоящий стандарт устанавливает спецификацию непримитивных понятий языка программирования. При этом используется набор определений, написанных на языке, установленном ИС018629. Данные определения устанавливают аксиомы для терминологии в соответствии с ИС018629.

Настоящий стандарт распространяется на:

•    определения новых временных и основанных на состоянии понятий в соответствии с ИС018629-11 иИС018629-12:

•    событийные ограничения выполнения действий, сформулированные с использованием временных соотношений в соответствии с ИС018629-11 и соотношений, основанных на состоянии, в соответствии с ИС018629-12.

Настоящий стандарт не распространяется на определения новых понятий, соответствующих ИС018629-11 и ИС018629-12. и новых понятий, не зависимых от временных соотношений и соотношений, зависимых от состояния.

Примечание — Временные понятия и понятия, зависимые от состотия. относятся ко еремеж и статусу какой-либо сущности, связанной с технологическим процессом и используемой для его спецификации.

2    Нормативные ссылки

8 настоящем стандарте исло/ъэовамы нормативные ссылки на следующие международные стандарты. которые необходимо учитывать при использовании настоящего стандарта. В случае ссылок на документы. у которых указана дата утверждения, необходимо пользоваться только указанной редакцией. В случае, когда дата утверждения не приведена, следует пользоваться последней редакцией ссылочных документов, включая любые поправки и изменения к ним:

ИСО/МЭК 8824-1 Информационные технологии. Нотация абстрактного синтаксиса версии 1 (ASN.1). Часть 1. Спецификация базовой нотации (ISO/IEC 8824-1. Information technology—Abstract Syntax Notation One (ASN.1)— Pan 1: Specification of basic notation)

ИС010303-1 Системы промышленной автоматизации и иитвграшя. Представление данных о продукции и обмен данными. Часть 1. Обзор и основные принципы (IS010303-1. Industrial automation systems and integration — Product data representation and exchange — Part 1: Overview and fundamental principles)

ИС015531-1 Системы промышленной автоматизации и интеграция. Упрааллощая информация промышленным производством. Часть 1. Общий обзор (ISO 15531-1. Industrial automation systems and integration — Industrial manufacturing management data — Part 1: General overview)

И C018629-1:2004 Системы промышленной автоматизации и интеграция. Язык спецификаций процесса. Часть 1. Обзор и основные принципы (IS018629-1:2004. Industrial automation systems and integration— Process specification language — Part 1: Overview and basic principles)

Издание официальное

ИСО 18629-11:2005 Системы промышленной автоматизации и интеграция. Язык спецификаций про* цесса. Часть 11. Ядро PSL (ISO 18629*11: 2005. Industrial automation systems and integration — Process specification language — Part 11: PSL core)

ИСО 18629*12 Системы промышленной автоматизации и интеграция. Язык спецификаций процесса. Часть 12. Внешнее ядро (IS018629*12, Industrial automation systems and integration — Process specification language — Part 12: Outer core)

3 Термины, определения и сокращения

3.1    Термины и определения

В настоящем стандарте применены следующие термины с соответствующими определениями:

3.1.1    аксиома (axiom): Точно сформулированное аналитическое выражение на формальном языке, устанавливающее ограничения к интерпретации символов в словаре языка.

[ИС018629*1]

3.12 установленная лексика (defined lexicon): Набор символов в нелогической лексике, обознача* ющих установленные понятия.

Примечание — Установлю ■ юя лесенка состоит из констант, функций и отношены.

Пример — Термины с консервативным определением

[ИС018629-1]

3.1.3    дефинициональное расширение (definitional extension): Расширение ядра PSL, представляющее новые лингвистические понятия, которые могут быть определены с помощью терминов ядра PSL.

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

[ИС018629-1]

3.1.4    расширение (extension): Расширение ядра PSL содержащее дополнительные аксиомы.

Примечание 1 — Ядро PSL представляет собой относитехъмо простой набор аксиом, достаточный для представлены широкого круга основных процессов. Однако для представления более сложных процессов требуются допогыительные ресурсы, отсутствующие е ядре PSL. Ядро PSL с каждым понятием следует ислогъзоеать для описаны того или иного процесса, а для описания разнообразных модульных расширены следует испогъ-эоеать расширение и допогыения ядра PSL. В этом случае пользователь может использовать такой язык, который соответствует требованвш к выразительности.

Примечание 2 — Все раашрения являются теориями ядра иш дефиноюнальшми расширенном.

3.1.5    грамматика (grammar): Правила совместного использования логических символов и словарных терминов для составления точно сформулированных аналитических выражений.

[ИС018629*1]

3.1.6    информация (information): Факты, концепции или инструкции.

[ИС010303-1]

3.1.7    язык (language): Сочетание лексики и грамматики.

[ИС018629*1]

3.1.8    производство (manufacturing): Функция или действие, предусматривающие перевод или превращение материала из сырья или заготовки в завершенное состояние.

[ИС015531*11

3.1.9    производственный процесс (manufacturing process): Структурированный комплекс видов деятельности или работ, выполняемых с материалом для перевода его из сырья или заготовки в завершенное состояние.

Примечание — Производственные процессы могут быть представлены в виде технологической схемы процесса, схемы движения ододукта. в виде табличной схемы ww схемы фиксированного расположены. К планируемым производственным процессам могут относиться изготовление продукта для складированы, на заказ и для сборки на заказ и т. я. основанным на стратегическом использованы и размещении материально-производственных запасов.

[ИС015531*1]

3.1.10    модель (model): Сочетание набора элементов и истинного назначения, удовлетворяющее всем правильно построенным формулировкам в теории.

Примечание1 — В настоящем стандарте определение термина «модель» отличается от используемого в научной и другой литературе: если предло жопою является верным е определеноюй интерпретацно*. то можно сказать, что интерпретация — это модегъ предложения. Виды семантик, представленных в настоящем стандарте. часто называют теоретически смоделированными семантиками.

Примечание2 — Модель обычно представляют в виде совокупности дополнитегыых структур (чэспм-но у по рядо-юн пых. в качестве структурного или векторного пространства). В этом случае модель определяет значения для терминологии и понятия истины для предложении языка в условиях данной модели. Задавая модель, основной набор аксиом математических структур, используемый в наборе аксиом, используют как основу для определения понятий, представленных в терминах языка, и их логических взаимосвязей, в результате чего набор моделей создает формальные семантики онтологии.

[ИС018629-1]

3.1.11    онтология (ontology): Лексика специализированной терминологии, дополненная необходимой спецификацией значений терминов.

Примечание 1 — Структурированной набор относитехьных терминов, представленный с описанием значемм термноюв на формальном языке. Описанью значения обьяовют. как и почему термины соотносятся. и определяет условия сегментировано» и структурирования набора терминов.

Примечание 2 — Основополагающим компонентом язъкэ технологических спецификаций ИСО 18629 является онтология. Примитивные конщепщы в онтологии, соответствующей определенно ИСО 18629. достаточны для огмсания основных производственных, инженерных и бизнес-процессов.

Примечание 3 — Основное внимание онтологии направлено не только на геркмы. но и на их значения. Произвольный набор терминов включен в онтологию, но эти термины могут приниматься только в том случав, если их значения согласованы. Такие предполагаемые семантики терминов могут быть утверждены и использованы.

Примечание 4 — Любой термин, используемый без точного определения, может быть причиной неясности и путамеы- Сложность для онтологии в том. что структура нуждается е создании терминов, имеющих точное астюние. Для онтологии, соответствующей определению ИСО 18629. необходимо предостаалъ математически строгую характеристику информационного процесса, а также четкое выражение основных логических свойств этой информации на языке, указанном а ИСО 18629.

Примечание 5 — Расширено» включают аксиомы внешнего ядра {оболочка ядра базового языка).

[ИС018629-1]

3.1.12    примитивная концепция (primitive concept): Лексический термин, не имеющий консервативного оп ределения.

[ИС018629-1]

3.1.13    примитивная лексика (primitive lexicon): Набор символов в нелогическом словаре, обознача

ющих ЛПйМАИТЯрМЫА ппнатма

Примечание — Примитивная лексика вкпочэет в себя постоянные, функциональные и реляционные символы.

[ИС018629-1]

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

Примечание — Данное определено» аналогично определению, приведенному в ИСО 10303-49. Тем не менее ИСО 15531 нуждается в понятии структурированного набора деятельностей без какого-либо предопределенного отношения ко времена* или этапам. С точки зрения управления потоком некоторые свободные процессы могут требовать синхронизацию в отношении цеты. хотя в действительности они нончего не выполняют (задэчн-призраки).

[ИС015531-1]

3.1.15    продукт (product): Изделие, материал или вещество, изготовленное е процессе производства.

(ИС010303-1]

3.1.16    ресурс (resource): Любые устройство, инструмент и средства, за исключением сырья и компонентов конечной продукции, имеющиеся в расположении предприятия для производства товаров и услуг.

Примечание 1 — Рассматриваемое понятие ресурса адаптировано по отношенное к ИСО 15531-1. Понятие ресурса, введенное в ИСО 15531-1. не включает сырьевые материалы, продукты и компоненты, являющиеся (с точки зрения системной теории) элементами окружающей среды и. таким образом, не являющиеся частью системы. В настоящем стандарте данное допущение снято. Более того, олределеионе. принятое а ИСО 15531-1. во многом испогъэует определено», принятое в ИСО 10Э03-49. при этом оно включается в определение. принятое в нестоящей части ИСО 18629. В дополнение к понятию ресурса, принятому в ИСО 15531.

понятие ресурса, принятое в настоящем стандарте, включает сырьевые и расходуемые материалы в соответствии с ИСО 18629-14.

Примечание 2 — Ресурсы в соответствии с приведение* выше опредепетем вклепают такие рабочую силу, рассматриваемую как особое средство с эадэ-ыыми возможностями и заданной производительности. Указанные средства рассматриваются как целесообразные для использования в процессе производства на ооювании технического задания. Дэжое определение не включает какого-либо моделирования индивидуального или группового поведения человеческого ресурса, за исключением его способности выполнять заданную работу в процессе производства (например, преобразование сырого материала или полуфабриката, обеспечение логистических услуг и т. п.). Это означает, что человеческие ресурсы, как и другие, рассматриваются с токи эретя их функций, их возможностей и их состояi-мя (например, занят, свободен). При этом исключается какое-либо моделирование или представлемю какого-либо аспекта индивидуального или группового социального поведения.

[ИС015531-11

3.1.17 теория (theory): Набор аксиом и определений, относящийся к данному понятию или набору понятий.

Примечание — Данное определена отражает проход искусственного интеллекта, где теория — это набор предположемм. на которых основано значение соответствующего понятия.

[ИСО 18629-1J

3.2 Сокращения

KIF—формат обмена знаниями (Knowledge Interchange Format).

4 Общая информация об ИСО 18629

Части с41 по 49 комплекса международных стандартов ИС018629 определяют дефинициональные расширения, необходимые для формулировки точных определений и родственных аксиом не примитивных понятий ИС018629. Дефинициональные расширения определены ИС018629-11 и ИС018629-12. где введены новые элементы лексики. Данные элементы дефикициомальных расширений могут быть полностью определены в соответствии с ИС018629-11 и ИС018629-12. Дефинициональные расширения дают точные семантические определения элементов, используемых в спецификациях индивидуальных технических приложений или типов технических приложений, при обеспечении совместных работ. Дефинициональные расширения существуют в следующих категориях:

•    расширения действий.

•    временные расширения и расширения, основанные на состоянии:

•    упорядочивание действий и расширение продолжительности:

•    назначения ресурса:

•    наборы ресурсов:

•    расширения действий процессора.

Ииддеидуагьмым (групповым) пользователям ИС018629 может потребоваться расширение ИС018629 для спецификации понятий, отсутствующих в настоящее время в частях с 41 по 49 комплекса международных стандартов ИСО 18629. Для этих целей они должны использовать элементы, определенные в ИСО 18629. Пользовательские расширения и их определения устанавливают дефинициональные расширения, которые не должны быть включены в части с 41 по 49 ИС018629.

Примечание — Пользовательские расширения дотсны удовлетворять требованиям ИСО 18629 и соответствовать ИСО 18629-1:2004 (подразделы 5.1 и 5.2).

Предметом рассмотрения частей с41 по 49 комплекса стандартов ИС018629 являются:

-    семантические определения (на основе понятий, установленных в ИС018629-11 и ИС018629-12). элементы которых являются характерными для шести понятий, определенных выше:

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

Предметом рассмотрения частей с 41 по 49 комплекса стандартов ИС018629 не являются:

-    определения и аксиомы для понятий, определенных ИС018629*11 и ИС018629-12:

•    элементы, не определенные в соответствии с ИС018629-11 и ИС018629-12:

•    пользовательские расширения.

5    Структура настоящего стандарта

5.1    Введение

Данный раздел характеризует фундаментальные теории, описанные в настоящем стандарте.

5.2    Расширения, определенные в настоящем стандарте

Фундаментальные теории, описанные в настоящем стандарте:

•    основанные на состоянии входные условия выполнения действий;

•    временные входные условия выполнения действий:

•    временные и основанные на состоянии входные условия:

•    событийные входные условия выполнения действий:

•    предотвращаемые условия выполнения действий:

•    периодические входные условия выполнения действий:

•    входные условия нарушения выполнения действий:

•    эффекты действий;

•    эффекты действий: событийные ограютения:

•    эффекты действий: временные и событийные ограничения:

•    дерево флюента;

•    распределение комплексных действий:

•    основанное на состоянии распределение комплексных действий:

•    временное распределение комплексных действий;

•    смешанное распределение комплексных действий;

•    вариация комплексных действий:

•    основанная на состоянии вариация комплексных действий:

•    временная вариация комплексных действий;

•    смешанная вариация комплексных действий:

•    встроенные действия: планы:

•    встроенные действия: временной разброс:

•    вариация неделимых вверх действий.

•    вариация неделимых вниз действий;

•    входные условия совместных действий:

•    эффекты совместных действий:

•    вариация препятствующих входных условий:

•    вариация эффектов затирания полезных данных.

все дефинициональные расширения, определенные в настоящем стандарте, являются расширениями ИС018629-12. которые, в свою очередь, являются расширениями ИСО 18629-11.

6    Основанные на состоянии входные условия выполнения действий

Данный раздел характеризует все определения, обусловленные основанными на состоянии входными условиями выполнения действий. Критерий, используемый для классификации указанных действий: зависит или нет допустимое выполнение действий от состояния системы до выполнения указанных действий.

6.1    Примитивная лексика основанных на состоянии входных условий выполнения действий

Лексика основанных на состоянии входных условий выполнения действий не требует никаких примитивных соотношений.

6.2    Описываемая лексика понятий для основанных на состоянии входных условий выполнения действий

В данном подразделе определены следующие соотношения:

•    (staie_equiv ?s1 ?s2);

•    (markov_precond ?afc

•    (partial_state ?a);

•    (rigid_state ?a).

Каждое понятие определяется неформальной семантикой и аксиомой ЮР.

6.3    Теории ядра, обусловленные основанными на состоянии входными условиями выполнения действий

Для данного расширения необходимо иметь:

•    act_occ.th;

•    complex.th;

•    atomic.th:

•    subactivity.th;

•    drsc_state.th;

•    occtree.th;

•    psl__core.th.

6.4    Дефинициональные расширения, обусловленные основанными на состоянии входными условиями выполнения действий

Для основанных на состоянии входных условий выполнения действий необходимо нижеследующее дефинициональное расширение:

•    preoond.def.

6.5    Определения понятий для основанных на состоянии входных условий выполнения действий

Для основанных на состоянии входных условий выполнения действий определен нижеследующие понятия.

6.5.1    state.equlv

Два события эквивалентны по состоянию, если после наступления данных событий имеет место одно и то же состояние.

(forall (?s1 ?s2) {iff (state_equrv ?s1 ?s2)

(feral (?f)

(iff (holds ?f?s1)

(ho*ds?f?s2)))))

6.5.2    markov_precond

Некоторое действие является маркоесхим действием при заданных входных условиях, если из согласованности двух событий по состоянию следует их согласованность по расширению возможности действия.

(fbrail (?а) (iff (markovjxecood ?а)

(forall (?ei ?с2>

(impSes(state_equiv?s1 ?s2)

(poss_equrv ?a ?s1 ?s2))))

6.5.3    partial.state

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

(forall (?а) (iff (partiaLstate ?а)

(and (exists (?s1)

(forai (?s2)

(implies (state_equiv ?s1 ?s2)

(poss.equiv ?a ?s1 ?s2))))

(exists (?s3 ?s4)

(and (state.equiv ?s3 ?s4)

(not (poss.equiv ?a ?s3 ?s4)))))))

6.5.4    rigid_state

Некоторое действие является жестко зависимым от состояния тогда и только тоща, когда сохраняющая событие перестановка переменах является тривиальной.

(forall (?а) (iff {rig restate ?а)

(forall (?s1)

(exists (?s2)

(and(state_equiv?s1 ?s2)

(not (poss_equiv ?a ?s1 ?s2)))))))

6.6 Грамматика соотношений для основанных на состоянии входных условий выполнения действий

Нижеследующие грамматические утверждения устанавливают описания процессов и вспомогательные правила, определенные в KIF для основанных на состоянии входных условий выполнения действий.

Примечание — Функция и важность грамматических утверждений поясняются в ИСО 18629-1:2004 (подраздеты 3.3.8. 4.2.4 и 5.1).

<    simple_state_precond > (forall (?s)

(implies (and (occurrence ?s)

(legal ?s))

<    simpte_state_axionn >))) |

(foraU(?s)

(implies (and (legal ?s)

<    simpte_state_axiom >)

(legal (successor < term > ?s))))

<    state_precond > ::= (forall (< variable >*)

(implies (and (occurrence < variable > < term >)

(legal < term >))

<    state_axiom >))) ]

(foral (< variable >*)

(implies (and (legal < term >)

<    state_axiom >)

(legal (successor < term > < term >))))

<    simple_state_!iteral > ::=

<    simple_state_formula > ::=

<    simple_state_axiom > ::=

<    statejiterai > ::=

<    statejbrmula > ::=

<    state axiom > ::=


(prior < term > ?s)

<    simple_statejiteral > |

(not < simple_state_fomxjla >) |

((and j or} < simple_state_formuta >*) |

({implies | iff) < simple_state_formula >)

({foraU | exists} < variable >*)

<    simpie_state_formula >)

(prior < term > < variable >}

<    statejiterai > |

(not < state_formula >) |

({and (or} < state_formula >) |

((implies | iff} < state_formula >*)

(forafl (< variable >+) < statejormula >)

7 Временные входные условия выполнения действий

Данный раздел характеризует все определения, обусловленные временными входными условиями выполнения действий. Критерий классификации указанных действий: зависит или нет действительное выполнение некоторого действия толькоот времени выполнения указанных действий.

7.1    Примитивная лексика временных входных условий выполнения действий Лексика временных входных условий выполнения действий не требует примитивных отношений.

7.2    Описываемая лексика понятий для временных входных условий выполнения действий

В данном подразделе описываются нижеследующие отношения:

•    (begin_equrv?s1 ?s2);

•    (time_precond ?а);

•    (partal_time ?а);

-(rigid_time?a).

Каждое понятие определяется неформальной семантикой и аксиомой K1F.

7.3    Теории, обусловленные временными входными условиями выполнения действий

Для данных теорий необходимы:

•    disc_state.th;

•    occtree.th;

- psl_core.th.

7.4    Дефинициоиальиые расширения, обусловленные временными входными условиями выполнения действий

Для временных входных условий действий требуются нижеследующие дефинициоиальиые рэсширетя:

•    precond.def:

•    start.def.

7.5    Определения временных входных условий выполнения действий

Нижеследующие понятия определены для временных входных условий выполнения действий.

7.5.1    begin_equiv

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

(forall (?s1 ?s2) (iff (begin_equrv ?s1 ?s2)

(= (beginof ?s1) (beginof ?s2))))

7.5.2    time_precond

Некоторое действие является действием с временными входными условиями при ограничении: если два неделимых события на дереве событий согласуются по времени начала отсчета, то они согласуются и по расширению возможности данного действия.

(forall (?а) (iff (time_precond ?а)

(forall (?s1 ?s2)

(mplies (begin_equtv ?s1 ?s2))

(poss_equiv ?a ?s1 ?s2)))))

7.5.3    partial_time_precond

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

(forall (?а) Off {partiai_time ?а)

(and (exists (?s1)

(forae(?s2)

(impSes (begin_equiv ?s1 ?s2)

(poss_equiv ?a ?s1 ?s2))))

(exists (?s3 ?s4)

(and (begin_egurv ?s3 ?s4)

(not (poss_equiv ?a ?&3 ?s4)))))))

7.5.4    rigld.time

Некоторое действие является жестким временным действием тогда и только тогда, когда перестановка по временной шкале, сохраняющая событие, является тривиальной.

(forall (?а) (iff (rigid_6me ?а)

(forall (?s1)

(exists (?s2)

(and (begjn_egu/v ?s1 ?s2)

(not(poss_equiv?a?s1 ?s2)))))))

7.6    Грамматика описаний процесса для временных входных условий выполнения действий

Нижеследующие грамматические утверждения определяют описания процессов и вспомогательные правила, установленные в KIF для временных входных условий выполнения действий.

< simple_time_precond > (forall (?s)

(implies (and (occurrence ?s < term >)

(legal ?s))

< simple_bme_axiom >))) |

(foraR (?s)

(implies (and (legal ?s)

<    simple.time.axiom >)

(legal (successor < term > ?s)»)

< ttme_precor>d > ::=


<    sanple.bmejiteral > ::=

<    simpie.bme.formula >

<    sintple.time.axiom >

<    ordered time literal >


< time formula > ::=


< time axiom > ::=


(foraR (?s)

(implies (and (occurrence ?s < term >)

(legal ?s))

< time_axiom >))) |

(foraR (?s)

(implies (and (legal ?s)

<    time.axiom >)

(legal (successor < term > ?s))))

(= (beginof ?s) < term >)

(and < simple_tone_literal >*)

({foral | exists} < variable >*) < simple.time.formuia >)

<    simple_bme Jrteral > \

(before (beginof ?s) < term >) |

(before < term > (beginof ?s))

<    ordered_time_hteral > |

(not < tme.fonmula >) |

({and | or} < time_formuta >*) |

({implies f iff} < bme.fomuda >)

({foral | exists} < variable >*} < time.formula >)

8 Временные и основанные на состоянии входные условия

Данный раздел характеризует все определения, обусловленные временными и основанными на состоянии входными условиями. Критерий, используемый для классификации указанных действий: зависит или нет действительное выполнение действия от состояния до указанного события и от времени выполнения действия.

8.1    Примитивная лексика временных и основанных на состоянии входных условий

Лексика временных и основанных на состоянии входных условий не требует примитивных соотношений.

8.2    Описываемая лексика временных и основанных на состоянии входных условий

8 данном подразделе описаны нижеследующие соотношения:

•    (mixed_precond ?s):

•    (partial_mixed ?s);

•    (rigid.mixed ?s).

Каждое понятие определяется неформальной семантикой и аксиомой ЮГ

8.3    Теории, обусловленные временными и основанными на состоянии входными условиями

Для данной теории необходимы:

•    disc.state.ttt:

•    occtree.th;

•    psl.core.th.

8.4    Дефинициональиые расширения, обусловленные временными и основанными на состоянии входными условиями

Для временных и основанных на состоянии входных условий дефинициональиые расширения не требуются.

8.5    Определения временных и основанных на состоянии входных условий Нижеследующие понятия определены для временных и основанных на состоянии входных условий.

8.5.1    mlxed_precond

Некоторое действие является смешанным действием для заданных входных условий при ограничении: если два события согласуются по состоянию и времени начала отсчета, то они согласуются и по рэсширениию возможности действий.

(forall (?а) (iff (mixed _precond ?а)

(feral (?s1 ?s2)

(implies (and(state_equrv ?s1 ?s2)

(begin__equiv?s1 ?s2))

(poss_equiv ?a ?s1 ?s2)))))

8.5.2    partial.mixed

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

(forall (?а) (iff (partial_mixed ?а)

(and (exists (?s1)

(forai (?s2)

(implies (and (state_equiv?s1 ?s2)

(begn_eqmv ?s1 ?s2))

(poss_equiv ?a ?s1 ?s2))))

(exists (?s3 ?s4)

(and (state_equiv ?s3 ?s4)

(begin_equiv ?s3 ?s4)

(not (poss_equiv ?a ?s3 ?s4)))))))

8.5.3    rigld.mixed

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

(forall (?а) (iff (rigid^mwed ?а)

(forall (?s1)

(exists (?s2)

(and (state_equiv ?sl ?s2)

(begin_equiv ?s1 ?s2)

(not (poss_equiv ?a ?s1 ?s2)))))))

8.6 Грамматика временных и основанных на состоянии входных условий

Нижеследующие грамматические утверждения определяют описания процесса и вспомогательные правила, установленные в KIF для временных и основанных на состоянии входных условий.

< simple_mix_precond > ::= (forall (?s)

(implies (and (occurrence ?s < term >)

(legal ?s))

< simpte_mix_axiom >))) (


(forai (?s)

(implies (and (legal ?s)

< simpl6_mix_axiom >)

(legal (successor < term > ?s))))

< mix_precond > ::= (forall (?s)

(implies (and (occurrence ?s < term >)

(legal ?s))

< mix_formula >)))

<    simple_rmx_literai >

<    simple_mix_formula >

<    simple_mix_axfem > ::=

<    ordered mix literal >


(= (beginof ?s) < term >) (prior ?s)

(and < simple__mtx_literal >*)

({forai | exists) < variable >*) < simple_nnix_formula >)

<    simple_mixjiteral >)

(before (beginof ?s) < term >) (prior < term > ?s) | (before < term > (beginof ?s)) (prior < term > ?s)

< mix formula >


<    ordered_mixJfteral > |

(not < mix_formula >))

{{and | or) < mbc_fomnula >*) |

({impfees | iff) < mix_formuia >)

< mix_axJom > ::=    ({fora! | exists) < variable >*) < mix_formuia >)

9 Событийные входные условия выполнения действий

Данный раздел характеризует все определения, обусловленные событийными входными условиями выполнения действий. Критерий, используемый для классификации указанных действий: зависит или нет реальное выполнение некоторого действия от выполнения других действий.

9.1    Примитивная лексика событийных входных условий выполнения действий

8 лексике событийных входных условий выполнения действий примитивные соотношения не используются.

9.2    Описываемые соотношения событийных входных условий выполнения действий

8 данном подразделе определены следующие соотношения:

•    (tree_equiv ?s1 ?s2):

•    (occurrence_constrained ?a):

•    (ocojrrence_de pendent ?a);

•    (occurrence_independent ?a).

Каждое понятие определяется неформальной семантикой и аксиомой ЮР.

9.3    Теории, обусловленные событийными входными условиями выполнения действий

Для данной теории необходимы:

•    occtree.th:

•    psl_core.th.

9.4Дефинициональиые расширения, обусловленные событийными входными условиями выполнения действий

Для событийных входных условий выполнения действий необходимо нижеследующее дефиницию-нальное расширение:

•    precond.def.

9.5 Определения событийных входных условий выполнения действий

Для событийных входных условий выполнения действий определены нижеследующие понятия.

9.5.1    tree.equiv

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

(forall (?а ?sl ?s2)

(iff (tree_equrv (successor ?a ?s1) (successor ?a ?s2))

(and (legal_equiv ?sl ?s2)

(or (tree_equiv?s1 ?s2)

(initial ?s1)

(initial ?s2)))))

9.5.2    occurrence.constrained

Некоторое действие является событийно ограниченным тогда и только тогда, когда все преобразования дерева событии сохраняют действительное выполнение данного действия.

(forall (?а) (iff (occurrence_cons trained ?а)

(forall (?s1 ?s2)

(implies (and (occurrence ?sl ?a)

(occurrence ?s2 ?a)

(tree_equrv ?s1 ?s2))

(legal_equiv ?s1 ?s2)))))

9.5.3    occurrence.dependent

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

focal! (?а) (iff (occunrence.dependent ?а)

(exists (?s1)

(and (occurrence ?s1 ?a)

(forail (?s2)

(implies (and (occurrence ?s2 ?a)

(tree.equrv ?s1 ?s2))

(legal.equiv ?s1 ?s2)))))))

9.S.4 occurrenceJndependent

Некоторое действие является не зависящим от события тогда и только тогда, когда не существует нетривиального преобразования дерева событий, сохраняющего действительное выполнение действия, (forail (?а) (iff (occurrence.independent ?а)

(forail (?s1)

(impSes (occurrence ?s1 ?a)

(exists (?s2)

(and (occurrence ?s2?a)

(tree_equiv?s1 ?s2)

(not (legal.equiv ?s1 ?s2))))))))

9.6 Грамматика событийных входных условий выполнения действий

Нижеследующие грамматические утверждения определяют описания процессов и вспомогательные правила, установленные в KIF для событийных входных условий выполнения действий.

<    ooc_constrained_precond > ::=

(forail (?s)

({implies ] iff} (and (occurrence ?s < term >)

(legal ?s)

(ubiquitous < term > < term >))

{< teaf.constrained.axiom > f < inner_constrained_axk>m)))

<    leaf.constrained.formula > ::= (exists (?occ ?s1)

(and (occurrence ?occ < term >)

(teaf_occ ?s1 ?occ)

(= ?s (successor < term > ?s1))))

<    leaf_constrained_axiom > ::= < leaf.constrained.fbrrnula > |

(not < leaf.constrained.fbrmula >)

■< tnner.constrained.forrmjta > (exists (?occ ?s1 ?s2)

(and (occurrence ?occ < term >)

(subactivity .occurrence ?s1 ?occ)

(subactivity .occurrence ?s2 ?occ)

(precedes ?s1 ?s)

(precedes ?s ?s2))>

<    inner.constrained.axiom > ::=    < inner.constrained.fonmula > |

(not < inner.constrained.formula >)

10 Предотвращаемые условия выполнения действий

Данный раздел характеризует все определения, обусловленные предотвращаемыми условиями выполнения действий. Критерий, используемый для классификации указанных действий: зависит или нет действительное выполнение действий от состояния системы до выполнения действий и от выполнения других действий.

10.1    Примитивная лексика предотвращаемых условий выполнения действий

Лексика предотвращаемых условий выполнения действий не требует примитивных соотношений.

10.2    Описываемые соотношения предотвращаемых условий выполнения действий

в данном подразделе определены нижеследующие соотношения:

• (preventable ?а);

•    (possibly_preventabte ?а);

•    (unpreventabte ?а).

Каждое понятие определяется неформальной семантикой и аксиомой ЮГ

10.3    Теории, обусловленные предотвращаемыми условиями выполнения действий

Для данной теории необходимы:

•    occtree.th;

•    psl_core.th.

10.4    Дефииициональиые расширения, обусловленные предотвращаемыми условиями выполнения действий

Для данных расширений необходимы:

•    occ_precond.def;

•    sta*e_precond.def:

•    precond.def.

10.5    Определения предотвращаемых условий выполнения действий

Для предотвращаемых условий выполнения действий определены нижеследующие понятия.

10.5.1    preventable

Некоторое действие является предотвращаемым тоща и только тоща, когда допустимые события зависят от переменных, сохраняющих свое значение при выполнении других действий на дереве событий, (forall (?а) (iff (preventable ?а)

(forall (?s1 ?s2)

(implies (and (occurrence ?sl ?a)

(occurrence ?s2 ?a)

(state_equiv ?s1 ?s2)

(tree_equiv ?s1 ?s2))

(Iegai_equiv?s1 ?s2)))))

10.5.2    poesibiy_preventable

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

(forall (?а) (iff (possfofy_preventable ?а)

(exists (?sl)

(and (occurrence ?s1 ?a)

(foral (?s2)

(implies (and (occurrence ?s2 ?a)

(state.equrv ?s1 ?s2)

(tree_equiv ?s1 ?s2))

(tegal__equiv ?s1 ?s2))))»)

10.5.3    unpreventabte

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

(forall (?а) (iff (unpreventabte ?а)

(forall (?s1)

(implies (occurrence ?s1 ?a)

(exists (?s2)

(and (occurrence ?s2 ?a)

(state_equiv?s1 ?s2)

(tree.equiv ?s1 ?s2)

(not (teQal_equiv ?s1 ?s2))))))))

10.6 Грамматика описаний процесса для предотвращаемых условий выполнения действий

Нижеследующие грамматические утверждения определяют описания процессов, установленные в KIF для предотвращаемых условий выполнения действий:

<    proven tabte_precond > ::=

(forall (?s)

({implies | iff} (and (occurrence ?s < term >)

(legal ?s)

(ubiquitous < term > < term >)

<    simpie_state_axiom >)

{< leaf_constrained_axiom > | < inner_constrained_axiom}))

<    possibly_preventabte j>recond > ::=

(forall (?s)

({impfies | iff} (and (occurrence ?s < term >}

(legal ?s)

(ubiquitous < term > < term >)

<    state_axiom >)

{< leaf_constrained_axiom > | < inner_constrained_axiom}))

11 Периодические входные условия выполнения действий

Данный раздел характеризует все определения, обусловленные периодическими входныьы условия* ми выполнения действий. Критерий, используемый для классификации указанных действий: зависит или нет действительное выполнение некоторого действия от времени его выполнения и от выполнения других действий.

11.1    Примитивная лексика периодических входных условий выполнения действий

Лексика периодических входных условий выполнения действий не требует примитивных соотношений.

11.2    Описываемая лексика периодических входных условий выполнения действий

8 данном подразделе определены следующие соотношения:

•    (periodic ?а):

•    (intermittent ?а);

•    (aperiodic ?а).

Каждое понятие определяется неформальной семантикой и аксиомой ЮР.

11.3    Теории, обусловленные периодическими входными условиями выполнения действий

Для данной теории необходимы:

•    occtree.th;

•    psl_core.th.

11.4    Дефинициональиые расширения, обусловленные периодическими входными условиями выполнения действий

Для данных расширений необходимы.

•    occ_precond.def.

•    time_precond.def;

•    precond.def.

11.5    Определения периодических входных условий выполнения действий

Для периодических входных условий выполнения действий определены нижеследующие понятия

11.5.1 periodic

Некоторое действие является периодическим тогда и только тогда, когда допустимые события зависят от времени выполнения других действий.

(forall (?а) (iff (periodic ?а)

(forall (?s1 ?s2)

(implies (and (occurrence ?s1 ?a)

(occurrence ?s2 ?a)

(begm^equiv ?s1 ?s2)

(tree^equiv ?s1 ?s2))

(legai_equiv ?s1 ?s2)))))

11.5.2    intermittent

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

(forall (?а) (iff (intermittent ?а)

(exists (?s1)

(and (occurrence ?s1 ?a)

(foraH (?s2)

(implies (and (occurrence ?s2 ?a)

(begin_equiv ?si ?s2)

(tree_equrv ?s1 ?s2))

(legal_equiv ?s1 ?s2)))))))

11.5.3    aperiodic

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

(forall (?а) (iff (aperiodic ?а)

(forall (?s1)

(implies (occurrence ?s1 ?a)

(exists (?s2)

(and (occurrence ?s2 ?a)

(begin_equiv ?s1 ?s2)

(tree_equiv ?s1 ?s2)

(not (legaljequiv ?s1 ?s2))))))))

11.6 Грамматика периодических входных условий выполнения действий

Следующие грамматические утверждения определяют описания процесса, установленные в KIF для периодических входных условий выполнения действий.

<    period ю_ргвсопо > ::=

(forall (?s)

({implies | iff} (and (occurrence ?s < term >)

(legal ?s)

(ubiquitous < term > < term >)

< simple_time_axiom >)

{< leaf_constrained_axiom > [ < foner_constrained_axk>m}))

<    mtermittent_precond > ::=

(forall (?s)

({implies | iff} (and (occurrence ?s < term >)

(legal ?s)

(ubiquitous < term > < term >)

< time_axkxn >)

{< leaf_constrained_axiom > | < mner_constrained_ax>om}))

12 Входные условия нарушения выполнения действий

Данный раздел характеризует все определения, обусловленные входшми условиями нарушения выполнения действий. Критерий, используемый для классификации указанных действий: зависит или нет действительное выполнение действий от состояния до выполнения действий, от времени выполнения действий и от выполнения других действий.

12.1    Примитивная лексика входных условий нарушения выполнения действий

Лексика входных условий нарушения выполнения действий не требует примитивных соотношений.

12.2    Описываемая лексика входных условий нарушения выполнения действий

В данном подразделе определены следующие соотношения:

•    (spoiage ?а):

•    (posstb)e_spoiage ?а);

•    (nonspoilage ?а).

Каждое понятие определяется неформальной семантикой и аксиомой ЮР.

12.3    Теории, обусловленные входными условиями нарушения выполнения действий

Для данной теории необходимы:

•    occtree.th:

•    psJ_core.th.

12.4    Дефииициоиальные расширения, обусловленные входными условиями нарушения выполнения действий

Для данных расширений необходимы.

•    occ_precond.def;

•    state jxecond.def:

•    time_precond.def:

•    precond.def.

12.5    Определения входных условий нарушения выполнения действий

Для входных условий нарушения выполнения действий определены следующие понятия.

12.5.1    spoilage

Для некоторого действия имеются входные условия нарушения его выполнения, если:

(forall (?а) (iff (spoilage ?а)

(forall (?s1 ?s2)

(implies (and (occurrence ?sl ?a)

(occurrence ?s2 ?a)

(state_equiv ?s1 ?s2)

(begin_equiv ?s1 ?s2)

(tree_eguiv ?s1 ?s2))

(lAgal_Aquiv?s1 ?я?))))

12.5.2    possibte.spoilage

Для некоторого действия имеются входные условия возможного нарушения его выполнения, если: (forall (?а) (iff (possibie_spoiage ?а)

(exists (?s1)

(and (occurrence ?sl ?a)

(foral (?s2)

(implies (and (occurrence ?s2 ?a)

(state_equiv ?s1 ?s2)

(begin_equiv?s1 ?s2)

(tree_equrv ?s1 ?s2))

(legaLequiv ?s1 ?s2)))))))

12.5.3    nonspollage

Для некоторого действия существуют входные условия без нарушений выполнения действия, если: (forall (?а) (iff (nonspoilage ?а)

(forall (?s1)

(implies (occurrence ?s1 ?a)

(exists (?s2)

(and (occurrence ?s2?a)

(state_equiv?s1 ?s2)

(begin_equiv ?s1 ?s2)

(tree_eQurv?s1 ?s2)

(notflegal_equiv?s1 ?s2))))))))

12.6 Грамматика входных условий нарушения выполнения действий

Грамматика описаний процесса для входных условий нарушения выполнения действий эквивалентна грамматике утверждений общих описаний процесса, определенной в ИС016629-11.

13 Эффекты действий

Данный раздел характеризует все определения, обусловленные эффектами действий. Критерий, используемый для классификации указанных действий: одинаковы ли эффекты некоторого действия для всех выполняемых действий.

13.1    Примитивная лексика эффектов действий

Лексика эффектов действий не требует примитивных соотношений.

13.2    Описываемая лексика эффектов действий

В данном подразделе определены следующие соотношения:

•    (effects_eqixv ?а ?s1 ?s2);

- (conte xt_free ?a);

•    (лий ?a).

Каждое понятие определяется неформальной семантикой и аксиомой ЮР.

13.3    Теории, обусловленные эффектами действий

Для данной теории необходимы:

•    occtree.th;

•    psl_core.th.

13.4    Дефинициоиальные расширения, обусловленные эффектами действий

Для эффектов действий необходимы нижеследующие дефинициоиальные расширения:

13.5    Определения эффектов действий

Для утверждений Spectrum и Subtree Containement определены нижеследующие понятия.

13.5.1    effects.equiv

Два события для некоторого неделимого действия являются эквивалентными эффектами, если после данных событий состояния сохраняются неизменными.

(forall (?а ?s1 ?s2) (iff (effects_equrv ?a ?s1 ?s2)

(and (occurrence ?s1 ?a)

(occurrence ?s2 ?a)

(foral(?0

(iff (holds ?f?s1)

(holds ?f?s2)»)))

13.5.2    context.free

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

(forall (?а) (iff (context_free ?а)

(forall (?s1 ?s2)

(implies (and (occurrence ?s1 ?a)

(occurrence ?s2 ?a))

(effects_equiv ?a ?s1 ?s2)))))

13.5.3    null

Некоторое действие является нулевым тогда и только тогда, когда оно не затрагивает и не фальсифицирует какую-либо переменную.

(forall (?а) (iff (nul ?а)

(forall (?s)

(implies (occurrence ?s ?a)

(foral(?0

(iff (holds ?f?s)

(prior ?f?s)))))))

13.6 Грамматика эффектов действий

Нижеследующие грамматические утверждения определяют описания процесса, установлению в ЮР для эффектов действий:

<    context_free_effect > ::= (forall (?s)

(implies (occurrence ?s)

< simple_holds_axiom >))

<    rnjll^effect > ::= (foral(?s)

(implies (occurrence ?s)

(iff < simple_bokJs_axiom >

< simpte_state_axiom >)))

<    simpie_holdsJiteral > ::= (holds < term > ?s)

<    simple_holds_fonmula > ::= < simp*e_hol<Js_literal > |

(not < simpte_hokls_formula >) |

({and j or) < simple_holds_formuta >*) |

({implies | iff) < s*nple_holds Jormula >)

<    simpie_hokJs_ax»om > ::= ({forall | exists) < variable >*)

< simple_hoWs_formula >)

14 Основанные на состоянии эффекты действий

Данный раздел характеризует все определения, обусловленные основанными на состоянии эффектами действий. Критерий, используемый для классификации указанных действий: зависят или нет эффекты некоторого действия от состояния до выполнения указанных действий.

14.1    Примитивная лексика основанных на состоянии эффектов действий

Лексика основанных на состоянии эффектов действий не требует примитивных соотношений.

14.2    Описываемая лексика основанных на состоянии эффектов действий

В данном подразделе определены следующие соотношения:

•    (markov_effect ?а):

•    (partial_state_effect ?а у,

•    (ngid_state_effect ?а).

Каждое понятие определяется неформальной семантикой и аксиомой ЮГ

14.3    Теории ядра, обусловленные основанными на состоянии эффектами действий

Для данных дефинициональных расширений необходимы:

•    occtree.th;

•    psl_core.th.

14.4    Дефинициональные расширения, обусловленные основанными на состоянии эффектами действий

Нижеследующее дефинициональное расширение необходимо для основанных на состоянии эффектов действий:

•    precond.def.

14.5    Определения основанных на состоянии эффектов действий

Определены нижеследующие понятия для основанных на состоянии эффектов действий.

14.5.1 markov_effect

Некоторое действие является действием с марковским эффектом при условии, если когда-либо какие-либо два выполненных действия согласуются по состоянию (например, по состоянию, сохраняемому после выполнения действия), то они согласуются и по эффектам.

(forall (?a)(tff(martov effects ?а)

(forall (?s1 ?s2)

(implies (and (occurrence ?s1 ?a)

(occurrence ?s2 ?a)

(state_equiv ?s1 ?s2))

(effects_equrv ?a ?s1 ?s2)))))

14.5.2    parti al_state_effect

Некоторое действие является частично ограниченным по состогнию тогда и только тогда, когда суще* ствуют сохраняющие эффект перестановки переменных.

(forall (?а) (iff (partial_state_effects ?а)

(and (exists (?s1)

(forall (?s2)

(impfees (state_equiv ?s1 ?s2)

(effects_equiv ?a ?s1 ?s2))))

(exists (?s3 ?s4)

(and (state.equiv ?s3 ?s4)

(not (effects_equiv ?a ?s3 ?s4)))))))

14.5.3    rigid_state_effect

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

(forall (?а) (iff (rigid_state_effects ?а)

(forall (?s1)

(exists (?s2)

(and (state_equrv ?si ?s2)

(not (effects_equrv ?a ?s1 ?s2)))))))

14.6 Грамматика основанных на состоянии эффектов действий

Грамматика описаний процесса для встроенных ограничений действий.

<    simple_state_effect > ::= (forall (?s)

(impies (and (occurrence ?s)

<    simpte_state_axiom >)

< simple_holds_axiom >)))

<    state_effect >    (foral (< variable >*)

(implies (and (occurrence < variable > < term >)

<    state_axiom >)

< simple_hoids_axiom >)))

15 Временные эффекты действий

Данный раздел характеризует асе определения, обусловленные еремежыми эффектами действий. Критерий, используемый для классификации указанных действий: зависят или нет эффекты некоторого действия только от времени выполнения указанного действия.

15.1    Примитивная лексика временных эффектов действий

Лексика временных эффектов действий не требует примитивных соотношений.

15.2    Описываемая лексика временных эффектов действий

8 данном подразделе определены следующие соотношения:

•    (temporal_effect?a):

•    (partiaJ_temporal ?а);

•    (nontemporal ?а).

Каждое понятие определяется неформальной семантикой и аксиомой K1F.

15.3    Теории ядра, обусловленные временными эффектами действий

Для данных дефинициональных расширений необходимы:

•    occtree.th;

•    psl_core.th.

15.4    Дефииициональные расширения, обусловленные временными эффектами действий Для данных расширений необходимы временные эффекты действий.

15.5    Определения временных эффектов действий

Для временных эффектов действий определены нижеследующие понятия.

15.5.1    temporal.effect

Некоторое действие является действием с временными эффектами при условии, если когда-либо наступление каких-либо двух событий согласуется по времени начала отсчета, то эти события согласуются и по эффектам (например, по состоянию, которое сохраняется после выполнения действия).

(forall (?а) (iff (temporai_effects ?а)

(forall (?sl ?s2)

(implies (and (occurrence ?s1 ?a)

(occurrence ?s2 ?a)

(begin_equiv ?s1 ?s2))

(effects_equiv ?a ?sl ?s2)))))

15.5.2    partiai.temporal

Некоторое действие является действием с частично временными эффектами тогда и только тогда, когда существуют сохраняющие эффект перестановки по временной шкале.

(forall (?а) (iff (part»al_temporal ?а)

(and (exists (?s1)

(foraH (?s2)

(implies (begin_eouiv ?s1 ?s2)

(effects_equiv ?a ?s1 ?s2))))

(exists (?s3 ?s4)

(and (begin_equiv ?s3 ?s4)

(not (effects_equiv ?a ?s3 ?s4)))))))

15.5.3    nontemporal

Некоторое действие является действием с жесткими временными эффектами тогда и только тогда, когда сохраняющая эффект перестановка по временной шкале является тривиальной.

(forall (?а) (rff (nontemporal ?а)

(forall (?s1)

(exists (?s2)

(and (begin^eQuiv ?s1 ?s2)

(not (effects_equrv ?a ?s1 ?s2)))))))

15.6    Грамматика временных эффектов действий

Грамматика описаний процесса временных эффектов действий:

<    simple_time_effects > ::= (foral (?s)

(implies (and (occurrence ?s < term >)

(legal ?s))

<    simple_holds_axiom >)))

<    time_effects > ::=    (foral (?s)

(implies (and (occurrence ?s < term >

(legal ?s)

< time_axiom >)

<    simple_holds_axiom >))

16 Событийные эффекты действий

Данный раздел характеризует все определения, обусловленные событийными эффектами действий. Критерий, используемый для классификации указанных действий: зависят или нет эффекты некоторого действия только от выполнения других действий.

16.1    Примитивная лексика событийных эффектов действий

Лексика событийных эффектов действий не требует примитивных соотношений.

16.2    Описываемая лексика событийных эффектов действий

В данном подразделе определены следующие соотношения:

♦ (occ_effect ?а ?s);

•    (occ_depend_effect ?а ?s);

•    (nonocc_effect ?а).

Каждое понятие определяется неформальной семантикой и аксиомой ЮР.

16.3    Теории ядра, обусловленные событийными эффектами действий

Для данных дефинициональиых расширений необходимы:

•    occtree.th;

•    psl_core.th.

16.4    Дефинициональиые расширения, обусловленные событийными эффектами действий Для событийных эффектов действий дефинициональиые расширения не требуются.

16.5    Определения событийных эффектов действий

Определены нижеследующие понятия для событийных эффектов действий.

16.5.1    occ_effect

Некоторое действие имеет событийные ограниченные эффекты тогда и только тогда, когда указанные эффекты действий сохраняются преобразованиями дерева событий.

(forall (?а) (iff (occ_effects ?а)

(forali (?s1 ?s2)

(impSes (and (occurrence ?s1 ?a)

(occurrence ?s2 ?a)

(tree_equiv ?s1 ?s2))

(effects_equiv ?a ?s1 ?s2)))))

16.5.2    occ_depend_effect

Некоторое действие имеет зависящие от события эффекты тогда и только тогда, когда существуют преобразования дерева событий, сохраняющие эффекты данного действия.

(forall (?а) (iff (occ_depend_effects ?а)

(exists (?s1)

(and (occurrence ?sl ?a)

(foral (?s2)

(implies (and (occurrence ?s2 ?a)

(tree.equrv ?s1 ?s2)>

(effects eouiv ?a ?s1 ?s2)))))))

16.5.3    nonocc.effect

Некоторое действие не имеет зависящих от события эффектов тогда и только тогда, когда преобразование дерева событий, сохраняющее указанные эффекты действий, является тривиальным.

(forall (?а) (iff (nonocc_effects ?а)

(forall (?s1)

(implies (occurrence ?s1 ?a)

(exists (?s2)

(and (occurrence ?s2 ?a)

(tree_equrv ?si ?s2)

(not(effects_equiv?a?s1 ?s2))))))))

16.6    Грамматика событийных эффектов действий

Грамматика описаний процесса событийных эффектов действий:

<    occ_effect_axiom > ::=

(forall (?s)

(implies {< leaf_constrained_axjom > | < inner_constrained_axiom}

<    smple_holds_axiom >))

<    occ_depend_effect_ax>om >

(forall (?s)

(implies {< leaf_constrained_axiom > | < inner_constrained_axiom}

<    holds_axiom >))

17 Эффекты действий: событийные ограничения

Данный раздел характеризует есе определения, относящиеся к эффектам действий: событийные ограничения. Критерий, используемый для классификации указанных действий: зависят или нет эффекты некоторого действия от состояния до выполнения других действий.

17.1    Примитивная лексика эффектов действий: событийные ограничения

Лексика эффектов действий (событийные ограничения) не требует примитивных соотношений.

17.2    Описываемая лексика эффектов действий: событийные ограничения

8 данном подразделе определены следующие соотношения:

•    (Quantum ?а);

•    (semtdassical ?ау,

•    (classical ?а).

Каждое понятие определяется неформальной семантикой и аксиомой ЮР.

17.3    Теории ядра, обусловленные эффектами действий: событийные ограничения

Для данных дефииициомальных расширений необходимы:

•    occtree.th;

•    psJ_core.th.

17.4    Дефинициональные расширения, обусловленные эффектами действий: событийные

ограничения

Данное расширение не требует дефииициональных расширений.

17.5    Определения эффектов действий: событийные ограничения

Для эффектов действий определены нижеследующие понятия: событийные ограничения.

17.5.1    quantum

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

(forall (?а) (iff (quantum ?а)

(forall (?s1 ?s2)

(implies (and (occurrence ?s1 ?a)

(occurrence ?s2 ?a)

(state_equrv ?s1 ?s2)

(tree_equiv ?s1 ?s2))

(effects_equiv?a?s1 ?s2)))))

17.5.2    semiclassica!

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

((oral (?а) (iff (semidassical ?а)

(exists (?s1)

(and (occurrence ?sl ?a)

(forai (?s2)

(implies (and (occurrence ?s2 ?a)

(state.equiv ?s1 ?s2)

(tree_equrv?s1 ?s2))

(effects_eqmv ?a ?s1 ?s2)))))>)

17.5.3    classical

Некоторое действие является классическим тогда и только тогда, когда его эффекты не зависят от выполнения каких-либо других действий на дереве событий.

(forall (?а) (iff (classical ?а)

(forall (?s1)

(impies (occurrence ?s1 ?a)

(exists (?s2)

(and (occurrence ?s2 ?a)

(state_equrv?s1 ?s2)

(tree_equrv ?s1 ?s2)

(not (effects_equiv ?a ?sl ?s2)»)))))

17.6 Грамматика эффектов действий: событийные ограничения

Грамматика описаний процесса для эффектов действий: событие.

<    quantum_axiom > ::=

(forall (?s)

(implies (and {< leaf_constra»ned_axiom > | < inner_constramed_axiom}

<    simple_state_axiom >)

<    simple_hoWs_axiom >))

<    semidassjcal__axkxn > ::=

(forall (?s)

(implies (and {< leaf_constrained_axiorn > | < irmer_oonstrained_axiom}

<    state_axiom >)

<    simp*e_hoWs_axiom >))

18 Эффекты действий: временные и событийные ограничения

Данный раздел характеризует все определения, обусловленные эффектами действий: временные и событийные ограничения. Критерий, используемый для классификации указанных действий: зависят или нет эффекты некоторого действия только от времени выполнения других действий.

18.1    Примитивная лексика эффектов действий: временные и событийные ограничения

Лексика эффектов действий (временные и событийные ограничения) не требует примитивных соотношений.

18.2    Описываемая лексика эффектов действий: временные и событийные ограничения

В данном подразделе определены следующие соотношения:

•    (relativistic ?а);

•    (seminewton ?а);

•    (newton ?а).

Каждое понятие определяется неформальной семантикой и аксиомой ЮГ

18.3    Теории ядра, обусловленные эффектами действий: временные и событийные ограничения

Для данных дефинициональных расширений необходимы:

•    occtree.th:

•    psi_core.th.

18.4    Дефинициональные расширения, обусловленные эффектами действий: временные и событийные ограничения

Для данных расширений необходимы входные условия выполнения действий.

18.5    Определения эффектов действий: временные и событийные ограничения

Определены нижеследующие понятия для эффектов действий: временные и событийные ограничения.

18.5.1 relativistic

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

(forall (?а) (iff (relativistic ?а)

(forall (?s1 ?s2)

(impfees (and (occurrence ?st ?a)

(occurrence ?s2 ?а)

(begin_equiv ?s1 ?s2)

(tree_equiv ?s1 ?s2))

(effects_equiv ?a ?s1 ?s2)))))

18.5.2    seminewton

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

(forall (?а) (iff (seminewton ?а)

(exists (?s1)

(and (occurrence ?s1 ?a)

(foral (?s2)

(implies (and (occurrence ?s2 ?a)

(begin_equiv ?s1 ?s2)

(tree_equiv ?s1 ?s2))

(effects_equiv ?a ?s1 ?s2)))))))

18.5.3    newtonian

Некоторое действие является ньютоновским тогда и только тогда, когда его эффекты не зависят от времени начала отсчета выполнения каких-либо других действий на дереве событий.

(forall (?a)(iff (newtonian ?а)

(forall (?s1)

(implies (occurrence ?s1 ?a)

(exists (?s2)

(and (occurrence ?s2 ?a)

(begin_epuiv ?s1 ?s2)

(tree_eqmv ?s1 ?s2)

(not (effects_equw ?a ?s1 ?s2))))))))

18.6 Грамматика эффектов действий: временные и событийные ограничения

Грамматика описаний процесса для эффектов действий: времегыые и событийные ограничения.

<    relativistic_axiom > ::=

(forall (?s)

(implies (and {< teaf_constrained_axiom > | < inner_constrained_axiom}

<    simp*e_time_axiom >)

<    simple_ho!ds_axiom >))

<    seminewton_axiom >

(forall (?s)

(implies (and {< leaf_constrained_axiom > | < inner_constrained_axiom}

<    time axiom >)

<    simpte_holds_axiom >))

19 Дерево флюента

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

19.1    Примитивная лексика дерева флюента

Лексика дерева флюента не требует примитивных соотношений.

19.2    Описываемые соотношения дерева флюента

В данном подразделе определены следующие соотношения:

•    (achieved ?f ?осс);

- (falsified ?f ?осс);

•    (irreversible ?f):

•    (unachievable ?f);

•    (bounded ?f).

Каждое понятие определяется неформальной семантикой и аксиомой ЮР.

19.3    Теории ядра, обусловленные деревом флюента

Для данных дефинициомальных расширений необходимы:

•    occtree.th:

- psi_core.th.

19.4    Дефинициональиые расширения, обусловленные деревом флюента

Для данных расширений необходимы.

•    occ_precood.def.

•    state_precond.def:

•    precond.def.

19.5    Определения дерева флюента

Для дерева флюента определены нижеследующие понятия.

19.5.1    achieved

Флюента ?f приобретает значение (архивируется) в результате события ?осс при условии, что она не сохраняется до наступления события, но реально сохраняется после события.

(forali (?f ?осс) (iff (achieved ?f ?occ)

(and (holds ?f ?occ)

(not (prior ?f?occ)))))

19.5.2    falsified

Флюента ?f является фальсифицированной (теряет значение) в результате события ?осс при условии, что она сохраняет значение до наступления события, но теряет его после наступления события.

(forali (?f ?осс) (iff (falsified ?f ?occ)

(and (not (holds ?f ?occ))

(prior ?f?occ))))

19.5.3    irreversible

Флюента является необратимой, если она никогда не фальсифицируется.

(forali (?f) (iff (irreverstote ?0 (not (exists (?occ)

(falsified ?f?occ)))))

19.5.4    nonachievable

Флюента является неархивируемой. если она никогда не принимает никаких значений.

(forali <?f) (iff (unachievable ?f)

(not (exists (?occ)

(achieved ?f ?occ)))))

19.5.5    bounded (forali (?f) (iff (bounded ?f)

(exists (?occ1 ?occ2)

(and (achieved ?f ?occ1)

(falsified ?f ?occ2)))))

19.6 Грамматика описаний процесса для дерева флюента

Нижеследующие грамматические утверждения определяют описания процесса, установленные в ЮР для дерева флюента.

20 Распределение комплексных действий

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

20.1    Примитивная лексика распределения комплексных действий

Лексика распределения комплексных действий не требует примитивных соотношений.

20.2    Описываемые соотношения распределения комплексных действий

В данном подразделе определены следующие соотношения:

•    (profile ?осс ?а);

•    (root_equiv ?а ?осс1 ?осс2):

•    (universal ?а);

•    (restricted ?а);

•    (constrained ?а).

Каждое понятие определяется неформальной семантикой и аксиомой ЮР.

20.3    Теории ядра, обусловленные распределением комплексных действий

Для данных дефинициональных расширений необходимы:

•    occtree.th:

•    psl_core.th.

20.4    Дефинициональные расширения, обусловленные распределением комплексных действий

Для данных расширений необходимы.

•    occ_precond.def;

•    state_precond.def:

•    precond.def.

20.5    Определения распределения комплексных действий

Для распределения комплексных действий определены нижеследующие понятия.

20.5.1    profile

Событие ?осс является элементом профиля для заданного действия ?а при условии, что данное событие ?осс является начальным событием на ветви дерева событий, которое, в свою очередь, является событийно*иэоморфическмм для ветви некоторого дерева действий, соответствующего дейстамо ?а.

(forall (?осс ?а) (iff (profile ?осс ?а)

(exists (?осс1 ?осс2 ?а1)

(and (occurrence_of ?осс1 ?а)

(occorrence__of ?осс ?а1)

(occurrence.of ?осс2 ?а 1)

(root_occ ?осс2 ?осс1)

(forall (?оссЗ ?а2)

(impSes (and (subactivity.occurrence ?оссЗ ?осс1)

(occurrence_of ?оссЗ ?а2))

(exists (?осс4)

(and (occurrence_of ?осс4 ?а2)

(precedes ?осс ?осс4)))))))))

20.5.2    root.equiv

Два события ?осс1 и ?осс2 на дереве событий эквивалентны корнями по отношению к некоторому действию ?а тогда и только тогда, когда существуют события ?а, предшествующие как событию ?оос1. так и событию ?осс2.

(forall (?а ?осс1 ?осс2) (iff (root_equtv ?а ?осс1 ?осс2)

(mplies (and (profile ?осс1 ?a)

(profile ?occ2 ?a))

(iff (root ?occ1 ?a)

(root ?occ2 ?a)))))

20.5.3    universal

Некоторое действие является универсальным, если возможно его выполнение когда-либо.

(forall (?а) Off (universal ?а)

(forall (?occ1 ?осс2)

(implies (and (profile ?осс1 ?а)

(profle ?осс2 ?а))

(root.equiv ?а ?осс1 ?осс2)))))

20.5.4    local

Некоторое действие является локальным, если каждое его выполнение порождает события, не эквивалентные корнями.

(forall (?а) (iff (local ?а)

(foral (?а1)

(exists (?occ1 ?occ2)

(and (occurrence_of?occl ?a1)

(occurrence_of ?ooc2 ?a 1)

(profile ?occl ?a)

(profile ?occ2?a)

(not (root_equv ?a ?ooc1 ?occ2)))))))

20.5.5    restricted

Некоторое действие является связанным, если для него существуют другие действия, эквивалентные корнями.

(forall (?а) (iff (restricted ?а)

(and (exists (?а1)

(foral (?occ1 ?occ2)

(implies (and (occurrence_of ?occl ?a1)

(occurrence_of ?occ2 ?al)

(profile ?occl ?a)

(profile ?occ2 ?aj)

(root_epuiv ?a ?occ1 ?ooc2))))

(exists (?a2 ?occ3 ?occ4)

(and (occurrence.of ?occ3 ?a2)

(occurrence.of ?occ4 ?a2)

(pro fie ?occ3 ?a)

(pro fie ?occ4 ?a)

(not (root.equv ?a ?occ3 ?occ4)))))))

20.6 Грамматика описаний процесса распределения комплексных действий

I (ижеспедующие грамматические утверждения определяют описания процесса, установленные в KJF для распределения комплексных действий.

<    universal_axiom > ::= (foral (?s)

(implies (legal ?s)

< d»stnbution_formula>))

<    restricted_axiom >(forall (?s)

(implies < successor_axiom >

< distribution_formula>})

<    dtstribution_forrmjia > ::= (exists (?occ)

(and (occurrence ?occ ?a)

(root_occ ?s ?occ)))

21 Основанное на состоянии распределение комплексных действий

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

21.1 Примитивная лексика основанного на состоянии распределения комплексных действий

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

21.2    Описываемые соотношения основанного на состоянии распределения комплексных действий

В данном подразделе определены следующие соотношения:

•    (trigger ?а);

•    (partial_trigger ?а);

•    (пол trigger ?а).

Каждое понятие определяется неформальной семантикой и аксиомой ЮР.

21.3    Теории, обусловленные основанным на состоянии распределением комплексных действий

Для данной теории необходимы:

•    occtree.th:

•    psl_core.th.

21.4    Дефииициональные расширения, обусловленные основанным на состоянии распределением комплексных действий

Для данных расширений необходимы:

•    occ_precond.def;

•    state jxecond.def;

•    precond.def.

21.5    Определения основанного на состоянии распределения комплексных действий

Для основанного на состоянии распределения комплексных действий определены нижеследующие понятия.

21.5.1    trigger

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

(forall (?а) (iff (trigger ?а)

(forall (?осс1 ?осс2)

(implies (and (profile ?occ1 ?a)

(profle ?occ2 ?a)

(state_equiv ?occ1 ?occ2))

(root_eguiv ?a ?occ1 ?occ2)))))

21.3.2    partial_trigger

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

(forall (?а) (iff (par6al_trigger ?а)

(and (exists (?осс1)

(forall (?осс2)

(impies (and (profile ?occ1 ?a)

(profile ?occ2 ?a)

(state.equiv ?occ1 ?occ2)>

(root_equrv ?a ?occ1 ?occ2))))

(exists (?occ3 ?occ4)

(and (profile ?occ3 ?a)

(profle ?occ4 ?a)

(state_equiv ?occ3 ?occ4)

(not (root_equrv ?a ?occ3 ?occ4)))))))

21.5.3    nontrigger

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

(forall (?а) Off (nontrigger ?а)

(forall (?осс1)

(implies (profle ?осс1 ?а)

(exists (?осс2)

(and (profile ?осс2 ?а)

(state.equiv ?осс1 ?осс2)

(not (root_equiv ?а ?осс1 ?осс2)))))))

21.6 Грамматика описаний процесса для основанного на состоянии распределения комплексных действий

Нижеследующие грамматические утверждения определяют описания процесса, установленные a KJF для основанного на состоянии распределения комплексных действий.

<    trigger_activity > ::= (foraU (?s)

(implies < simpte_state_axiom >

<    distrtxition_formula>»

< partial_trigger > ::=    (foralt (?s < variable >♦)

(implies < state_axiom >

<    distrftxjtion_fonnula>))

22 Временное распределение комплексных действий

Данный раздел характеризует все определения, обусловленные временным распределением комплексных действий. Критерий, ислольэуемый для классификащш указанных действий: зависит или нет действительное выполнение некоторого комплексного действия от времени выполнения указанного действия.

22.1    Примитивная лексика временного распределения комплексных действий

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

22.2    Описываемые соотношения временного распределения комплексных действий

8 данном подразделе определены следующие соотношения:

•    (launch ?а);

•    (partialJaunch ?а):

•    (ngidjaunch ?а).

Каждое понятие определяется неформальной семантикой и аксиомой ЮР.

22.3    Теории, обусловленные временным распределением комплексных действий

Для данной теории необходимы:

•    occxree.tn:

•    psi_core.th.

22.4    Дефинициональмые расширения, обусловленные временным распределением комплексных действий

Для данных расширений необходимы:

•    occ._precond.def;

•    state jxecond.def;

•    precond.def.

22.5    Определения временного распределения комплексных действий

Для временного распределения комплексных действий определены нижеследующие понятия.

22.5.1 launch

Некоторое действие является запускающим при условии: если и только если когда-либо два события согласуются по времени начала отсчета, то они согласуются и по выполнению указанных действий.

(forall (?а) (iff (launch ?а)

(forall (?осс1 ?осс2)

(implies (and (profile ?осс1 ?а)

(profile ?осс2 ?а)

(begin_equiv ?осс1 ?осс2))

(root_equiv ?а ?осс1 ?осс2)))))

22.5.2    partialjaunch

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

(forall (?а) (iff (partiai^launch ?а)

(and (exists (?осс1)

(forall (?осс2)

(implies (and (profile ?occ1 ?a)

(profile ?occ2 ?a)

(begin_equiv ?occ1 ?occ2))

(root__equrv ?a ?occ1 ?occ2))))

(exists (?occ3 ?occ4)

(and (profile ?occ3 ?a)

(profile ?occ4?a)

(begin_eqoiv ?occ3 ?occ4))

(not (root_equiv ?a ?occ3 ?oco4)))))))

22.5.3    rigid.launch

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

(forall (?а) (iff (rigidjaunch ?а)

(forall (?осс1)

(impfies (profile ?осс1 ?a)

(exists (?occ2)

(and (begn_equfv ?occ1 ?occ2)

(not(root_equiv?a?occ1 ?occ2)))))))

22.6 Грамматика описаний процесса для временного распределения комплексных действий

Нижеследующие грамматические утверждения определяют описания процесса, установление в KJF для временного распределения комплексных действий.

<    simple Jaunch_activrty > ::= (foraB (?s)

(impfies < simple_tiiYie_axiom >

< distribution_fbrmula>))

<    partial_launch_acfivity > ::= (forall (?s < variable >+)

(impfies < time_axiom >

■c distribubor^formuta»))

23 Смешанное распределение комплексных действий

Данный раздел характеризует все определения, обусловленные смешанным распределением комплексных действий. Критерий, используемый для классификации указанных действий: зависят или нет допустимые события от состояния до выполнения действий и от времени выполнения данных действий.

23.1    Примитивная лексика смешанного распределения комплексных действий

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

23.2    Описываемые соотношения смешанного распределения комплексных действий

В данном подразделе определены следующие соотношения:

•    (cooditional_trigger?a);

•    (parnal_con<it»onat_tngger?a^

•    (uncondibonaljngger ?а).

Каждое понятие определяется неформальной семантикой и аксиомой ЮР.

23.3    Теории ядра, обусловленные смешанным распределением комплексных действий

Для данной теории необходимы.

•    occtree.th;

•    psl_core.th.

23.4    Дефинициональные расширения, обусловленные смешанным распределением

комплексных действий

Для данных расширений необходимы.

•    occ_precond.def.

•    statejxecond.def:

•    precond.def.

23.5    Определения смешанного распределения комплексных действий

Определены нижеследующие понятия для смешанного распределения комплексных действий.

23.5.1    conditional.launch

Некоторое действие является условно запускающим действием при условии, что если и только если когда-либо два события согласуются по состоянию и по времени начала отсчета, то они согласуются и по событиям.

(forall (?а) (iff (condit>onal_launcfc ?а)

(forall (?осс1 ?осс2)

(implies (and (profile ?осс1 ?а)

(profile ?осс2 ?а)

(state_eqiiiv ?осс1 ?осс2)

(begin_equrv ?осс1 ?осс2»

(root_equiv ?а ?осс1 ?осс2)))))

23.5.2    partial.conditionaljaunch

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

(forall (?а) (iff (partial jxtnditionaNaunch ?а)

(and (exists (?occ1)

(foraB (?occ2)

(implies (and (profile ?occ1 ?a)

(profile ?occ2 ?a)

(state_equiv ?occ1 ?occ2)

(begin_equiv ?occ1 ?occ2))

(root_equrv ?a ?occ1 ?occ2))))

(exists (?occ3 ?occ4)

(and (profile ?occ3 ?a)

(profile ?occ4 ?a)

(state.equiv ?occ3 ?occ4)

(begin_equiv ?occ3 ?occ4)

(not (root_equiv ?a ?occ3 ?occ4)))))))

23.5.3    unconditlonaijaunch

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

(forall (?а) (iff (unconditional launch ?а)

(forall (?осс1)

(implies (profile ?occ1 ?a)

(exists (?occ2)

(and (prof8e ?occ2 ?a)

(state_equiv?occ1 ?occ2)

(begin_equiv ?occ1 ?occ2)

(not (root_equiv ?a ?occ1 ?occ2)))))))

23.6    Грамматика описаний процесса для смешанного распределения комплексных действий

Нижеследующие грамматические утверждения определяют описания процесса, установленные в ЮР для смешанного распределения комплексных действий.

< conditional_launch_activitry > ::= (forall (?s ?s2)

(implies < simp*e_mix_axiom >

< disthbu6on_formuia>))

< partial_conditionaJ_launch > ::= (foraii (?s ?s2 < variable >+)

(implies < mix_formula >

< dislribubon_formuia>))

24 Вариация комплексных действий

Данный раздел характеризует все определения, обусловленные вариацией комплексных действий. Критерий, используемый для классификации указанных действий: ограничены или нет события некоторого комплексного действия.

24.1    Примитивная лексика вариации комплексных действий

Лексика вариации комплексных действий не требует примитивных соотношений.

24.2    Описываемые соотношения вариации комплексных действий

В данном подразделе определены следующие соотношения:

•    (min_equiv ?осс1 ?осс2 ?а):

•    (uniform ?а):

•    (variegated ?аХ

•    (multiform ?а).

Каждое понятие определяется неформальной семантикой и аксиомой ЮГ

24.3    Теории, обусловленные вариацией комплексных действий

Для данных теорий необходимы:

•    occtree.th;

•    psi_core.th.

24.4    Дефинициональиые расширения, обусловленные вариацией комплексных действий

Для данных расширений необходимы.

•    occ_precond.def.

•    state_precond.def:

•    precond.def.

24.5    Определения вариации комплексных действий

Для вариации комплексных действий определены нижеследующие понятия.

24.5.1    min.equiv

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

(forall (?occ1 ?осс2 ?а) (iff (mm_equrv ?осс1 ?осс2 ?а)

(and (subtree_embed ?осс1 ?осс2 ?а)

(subtree_embed ?осс2 ?осс1 ?а))))

24.5.2    uniform

Некоторое действие является однородным, если все его минимальные деревья действий являются изоморфическими.

(forall (?а) (iff (uniform ?а)

(forall (?осс1 ?осс2)

(implies (and (root ?осс1 ?а)

(root ?осс2 ?а)

(min_epu*v ?осс1 ?осс2 ?а)))))

24.5.3    variegated

Некоторое действие ?а является варьированным, если все его минимальные деревья действий (с событийно-эквивалентными корневыми событиями) являются изоморфическими.

(forall (?а) (iff (variegated ?а)

(and (exists (?а1)

(foral (?occ1 ?occ2)

(implies (and (occurrence_of ?осс1 ?а1)

(occurrence_of ?occ2 ?a1)

(root ?occl ?a)

(root ?occ2 ?a))

(min_equiv ?occ1 ?ooc2 ?a))))

(exists (?a2 ?occ3 ?occ4)

(and (occurrence_of ?occ3 ?a2)

(oocurrence_of ?occ4 ?a2)

(root ?occ3 ?a)

(root ?occ4 ?a)

(not (min_equrv ?occ3 ?occ4 ?a)))))))

24.S.4 multiform

Некоторое действие является многообразным, если существуют неиэоморфические деревья действий с «юбытийно-эквивалентными корневыми событиями.

(forall (?a)(iff (multiform ?а)

(forall (?а1 ?occ1)

(implies (and (root ?occ1 ?a)

(occurrence_of?occ1 ?a1))

(exists (?occ1 ?occ2)

(and(occurrence_of?occ1 ?a1)

(occurrence_of ?occ2 ?al)

(root ?occl ?a)

(root ?occ2 ?a)

(not (min_equiv ?occ1 ?occ2 ?a))))))))

24.6 Грамматика описаний процесса для вариации комплексных действий

Нижеследующие грамматические утверждения определяют описания процесса, установленные в KJF для вариации комплексных действий.

<    uniform_axk>m > ::= (foral (?s1 ?s2)

(iff (do < term > ?s1 ?s2)

< variation_formula >+))

<    variegated_axiom > ::= (forall (?s ?s2 < variable >♦)

(iff(do?a?s1 ?s2)

<occ_variaaon_formula >♦))

<    variation_f6rmula > (exists (< variable >*)

(and (subactivity < term > < term >)

(do < term > ?st ?s2)))

<    occ_vanation_formula > (implies < successor_axk>m >

< variat«on_formula >)

25 Основанная на состоянии вариации комплексных действий

Данный раздел характеризует все определения вариации комплексных действий, основанной на состоянии. Критерий, используемый для классификации указанных действий: зависят или нет события от состояния до выполнения указанных действий.

25.1    Примитивная лексика основанной на состоянии вариации комплексных действий

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

25.2    Описываемые соотношения основанной на состоянии вариации комплексных действий

8 данном подразделе определены следующие соотношения:

•    (conditional ?а);

•    (partal_cond№onal ?а);

•    (rigid_conditional ?а).

Каждое понятие определяется неформальной семантикой и аксиомой ЮР.

25.3    Теории, обусловленные основанной на состоянии вариации комплексных действий

Для данной теории необходимы:

•    occtree.th;

•    psl_core.th.

25.4    Дефинициональиые расширения, обусловленные основанной на состоянии вариации комплексных действий

Для данных расширений необходимы:

•    occ_precond.def;

•    state_precond.def;

•    precond.def.

25.5    Определения основанной на состоянии вариации комплексных действий

Для основанной на состоянии вариации комплексных действий определены нижеследующие понятия.

25.5.1    conditional

Некоторое действие является условным при следующем ограничении: какие-либо два его минимальных дерева действий являются иэоморфическими. если корни согласованы по состоянию.

(forall (?а) (iff (conditional ?а)

(forall (?осс1 ?осс2)

(implies (and (root ?осс1 ?а)

(root ?осс2 ?а)

(state_equiv ?осс1 ?осс2)}

(min_eqt*v ?осс1 ?оос2 ?а)))))

25.5.2    partial.conditional

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

(forall (?а) (iff (partial_oonditionaJ ?а)

(and (exists (?осс1)

(ГигаМ (?ouc2)

(implies (and (root ?осс1 ?a)

(root ?occ2 ?a)

(state_equiv ?occl ?occ2))

(min_equiv ?ocd ?occ2 ?a))))

(exists (?occ3 ?occ4)

(and (root ?occ3 ?a)

(root ?occ4 ?a)

(state_equrv ?occ3 ?occ4)

(not (min_equiv ?occ3 ?oc4)))))))

25.5.3    rigld.conditional

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

(forall (?а) (iff (rigid_conditionat ?а)

(forall (?осс1)

(exists (?осс2)

(and (root ?осс1 ?a)

(root ?occ2 ?a)

(state_equiv ?occ1 ?occ2)

(not (m«n_equfv ?occ1 ?occ2 ?a)))))))

Нижеследующие грамматические утверждения определяют описания процесса, установленные в KJF для основанной на состоянии вариации комплексных действий.

<    condibonal_activity > ::= (forall (?s ?s2)

(iff (do ?a ?s?s2)

<    simpie.conditional >))

<    partiai_conditional > (forall (?s ?s2 < variable >*)

(iff (do ?a ?s?s2)

<    condibonal_formula >))

<    simpie_conditionai > ::= (implies < simpte_state_axiom >

<    vanation_formula >)

<    conditional_formuia > ::= (implies < state.axiom >

<    vanation_formula >)

26 Временная вариация комплексных действий

Данный раздел характеризует все определения, обусловленные временной вариацией комплексных действий. Критерий, используемый для классификации указанных действий: зависят или нет события, представляющие собой выполнение составляющих действий некоторого комплексного действия, только от времени выполнения указанного действия.

26.1    Примитивная лексика временной вариации комплексных действий

Лексика временной вариации комплексных действий не требует примитивных соотношений.

26.2    Описываемые соотношения временной вариации комплексных действий

В данном подразделе определены следующие соотношения:

•    (time_condt>onal ?а);

•    (parbaMime_cond rtional ?а);

•    (rigid_time_conditional ?а).

Каждое понятие определяется неформальной семантикой и аксиомой ЮР.

26.3    Теории, обусловленные временной вариацией комплексных действий

Для данной теооии необходимы.

•    occtree.th:

•    psl_core.th.

26.4    Дефииициональиые расширения, обусловленные временной вариацией комплексных действий

Для данных расширений необходимы.

•    occ_precond.def;

•    state_precond.def:

•    precond.def.

26.5    Определения временной вариации комплексных действий

Для предотвращаемых условий выполнения действий определены нижеследующие понятия.

26.5.1 time.conditional

Комплексное действие является временным условным при следующем условии: какие-либо два его минимальных дерева действий являются иэоморфическими. если их корни согласуются по времени начала отсчета.

(forall (?а) (iff (time.conditional ?а)

(forall (?осс1 ?осс2)

(implies (and (root ?осс1 ?а)

(root ?осс2 ?а)

(begin_equiv ?осс1 ?осс2))

(min_equiv ?осс1 ?осс2 ?а)))))

26.5.2    partial_time_conditional

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

(forall (?а) (iff (partiai_time_conditional ?а)

(and (exists (?осс1)

(foral (?осс2)

(implies (and (root ?occ1 ?a)

(root ?occ2 ?a)

(begin_equiv ?occ1 ?occ2)}

(min_equiv ?occ1 ?occ2 ?a))))

(exists (?occ3 ?occ4)

(and (root ?occ3 ?a)

(root?ooc4 ?a)

(begm_equiv ?occ3 ?occ4)

(not (min_eQurv ?occ3 ?oc4)))))>)

26.5.3    rigid_time_conditional

Комплексное действие является жестким еремегыым условным тогда и только тогда, когда сохранясь тая событие по временной шкале перестановка является тривиальной.

(forall (?а) (iff (r>gid_time_conditional ?а)

(forall (?осс1)

(exists (?осс2)

(and (root ?осс1 ?а)

(root ?осс2 ?а)

(begin_equiv ?осс1 ?осс2)

(not (min.equiv ?осс1 ?осс2 ?а)))))))

26.6 Грамматика описаний процесса для временной вариации комплексных действий

Нижеследующие грамматические утверждения определяют описания процесса, установленные в ЮР для временной вариации комплексных действий.

<    time_conditional_activity > ::= (foral (?s ?s2)

(iff (do ?a ?s ?s2)

<    simple_time_conditional >))

<    partial_time conditional > ::= (foral (?s ?s2)

(iff (do ?a ?s ?s2)

<    dme_condidonai_formu*a >))

<    simpte_dme_condiDonal > ::= (implies < simpie_time_axjom >

<    vanabon_formuia >)

<    time_conditk>nal_formula > ::= (implies < trne_axiom >

<    vanabon_formuta >)

27 Смешанная вариация комплексных действий

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

27.1    Примитивная лексика смешанной вариации комплексных действий

Лексика смешанной вариации комплексных действий не требует примитивных соотношений.

27.2    Описываемые соотношения смешанной вариации комплексных действий

В данном подразделе определены следующие соотношения:

•    (m»xed_conditional ?а);

•    (partia!_mixed_condit>onal ?а):

•    (ngk3_mixed_condit)onai ?а).

Каждое понятие определяется неформальной семантикой и аксиомой ЮР.

27.3    Теории, обусловленные смешанной вариацией комплексных действий

Для данной теории необходимы:

•    occtree.th:

•    psl_core.th.

27.4    Дефинициональные расширения, обусловленные смешанной вариацией комплексных действий

Для данных расширений необходимы:

•    occ_precond.def;

•    state_precond.def:

•    precond.def.

27.5    Определения смешанной вариации комплексных действий

Для смешанной вариации комплексных действий определены нижеследующие понятия.

27.5.1    mixed.conditional

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

(forall (?а) (iff (mixed_condibonal ?а)

(forall (?осс1 ?осс2)

(implies (and (root ?осс1 ?а)

(root?occ2?a)

(begin_equiv ?осс1 ?осс2)

(state_equiv ?осс1 ?осс2)}

(min_equiv ?осс1 ?осс2 ?а)))))

27.5.2    partial_mixed_conditional

Некоторое действие является частично смешанным условным тогда и только тогда, когда существуют минимальные иэоморфические деревья действий и их корни согласованы по состоянию и по времени начала действий.

(forall (?а) (iff (partiaJ_mixed_conditionaJ ?а)

(and (exists (?осс1)

(foraH (?осс2)

(implies (and (root?occ1 ?a)

(root ?occ2 ?a)

(begin_equiv ?occ1 ?occ2)

(state_equiv ?occ1 ?occ2)>

(min_equiv ?occ1 ?occ2 ?a))))

(exists (?occ3 ?occ4)

(and (root ?occ3 ?a)

(root ?occ4 ?a)

(begin_eQuiv ?occi ?occ2)

{state_equiv ?occ3 ?occ4)

(not (min_equiv ?occ3 ?oo4)))))))

27.5.3    rigW_mixed_conditional

Некоторое действие является жестким смешанным условным тогда и только тогда, когда сохраняющие событие перестановки, моменты времени и состояние являются тривиальными.

(forall (?a)(iff(rigid_mixed_conditional?a)

(forall (?осс1)

(exists (?осс2)

(and (root ?осс1 ?a)

(root ?occ2 ?a)

(begin_equiv ?ooc1 ?occ2)

(state_equiv ?occ1 ?occ2)

(not (min^equiv ?occ1 ?occ2 ?a)))))))

Нижеследующие грамматические утверждения определяют описания процесса, установленные в ЮР для предотвращаемых условий выполнения действий.

<    mixed_conditional > ::= (feral (?s ?s2)

(iff(do?a?s?s2)

<    simpte_mix_cooditionaJ >))

<    partial_mixed_conditional > ::= (foral (?s ?s2 < variable >♦)

(iff(do?a?s?s2)

<    mix_conditional_fonmuia >))

<    simpie_mtx_con<Jrtionai > ;:= (implies < s*npie_mix_axJom >

<    vahabon_fomxjla >)

<    mixed__conditional_fofnnuia > ::= (implies < mix_axiom >

<    vanaoon_fomnula >)

28 Встроенные действия: планы

Данный раздел характеризует все определения, обусловленные встроенными действиями: планы. Критерий, используемый для классификации указанных действий: зависят или нет события некоторого комплексного действия от состояния в течение выполнения указанного действия.

28.1    Примитивная лексика встроенных действий: планы

Лексика встроенных действий (планов) не требует примитивных соотношений.

28.2    Описываемые соотношения встроенных действий: планы

В данном подразделе определены следующие соотношения:

•    (preventable ?а);

•    (possibly jxeventable ?а);

•    (unpreventable ?а).

Каждое понятие определяется неформальной семантикой и аксиомой ЮР.

28.3    Теории, обусловленные встроенными действиями: планы

Для данной теории необходимы:

•    occtree.th:

-    psl_.core.th.

28.4    Дефинициональные расширения, обусловленные встроенными действиями: планы

Для данных расширений необходимы:

-    occ_precond.def.

•    state_precond.def:

•    preoond.def.

28.5    Определения встроенных действий: планы

Для встроенных действий (планов) определены нижеследующие понятия.

28.5.1    plan

Некоторое дерево действий с корневым событием ?s является планом тоща и только тоща, когда все согласованные по состоянию события в максимальном встроенном поддереве согласуются между собой, (forall (?s) (iff (plan ?s)

(forall <?a ?s1 ?s2)

(implies (and (root ?s ?a)

(embed_tree ?s1 ?s2 ?s ?a)

(state_equiv ?s1 ?s2)>

(subocc_equiv ?s1 ?s2 ?s ?a)))))

28.5.2    nondet.plan

Некоторое дерево действий с корневым событием ?s является недетерминированным планом тоща и только тоща, когда существуют согласованные по состоянию события, заключающиеся в выполнении

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

(forall (?s) (iff (nondet_plan ?s)

(exists (?a ?s1 ?s3 ?s4)

(and (root ?s ?a)

(focal (?s2)

(implies (and (embed_tree ?s1 ?s2 ?s ?a)

(state_equiv?s1 ?s2))

(subocc_equiv ?s1 ?s2 ?s ?a))))

(state_equiv ?s3 ?s4)

(embed_tree ?s3 ?s4 ?s5 ?a)

(not (subocc_equiv ?s3 ?s4 ?s5 ?a))))))

28.5.3 unplan

Некоторое дерево действий с корневым событием ?s является неплановым тогда и только тогда, когда для каждого согласованного по состоянию события существует другое событие, связанное с состав* ляющим действием, но отличное от указанного.

(forall (?s) (iff (unplan ?s)

(forall (?sl?a)

(implies (root ?s ?a)

(exists (?s2)

(and (embed_tree ?s1 ?s2 ?s ?a)

(state_equiv ?s1 ?s2)

(not (subocc_equiv ?s1 ?s2 ?s ?a))))))))

28.6 Грамматика описаний процесса для встроенных действий: планы

Нижеследующие грамматические утверждения определяют описания промесса, установленные в ЮР для встроенных действий: планов.

<    pian_axiom > ::= (forall (?s ?осс < variable >*)

<    simple_plan_axiom >)

<    nondet_pian_axiom > ::= (forall (?s ?occ < variable >♦)

<    noodet_plan_axiom >))

<    plan_formula > ::= (implies < subocc_formula >

<    simpte_state_axiom >)

<    simple_pian_axk>m > ::= < plan_formula> |

(and < s*mpie_ptan_axK>m > < s»mp»e_pian_axiom >♦)

<    nondet_plan_formula > ::= (implies < subocc_formula >

< state_axiom >)

<    nondet_plan_axiom > ::= < oondet_ptan_formula> |

(and < nondet_plan_axiom > < nondet_plan_axiom >♦)

29 Встроенные действия: временной разброс

Данный раздел характеризует все определения, обусловленные встроенными действиями: времен* ной разброс. Критерий, используемый для классификации указанных действий: зависят или нет события некоторого комплексного действия от времени выполнения составляющих действий в процессе выполнения указанного комплексного действия.

29.1    Примитивная лексика встроенных действий: временной разброс

Лексика встроенных действий (временной разброс) не требует примитивных соотношений.

29.2    Описываемые соотношения встроенных действий: временной разброс

В данном подразделе определены следующие соотношения:

•    (preventable ?а);

•    (possiblyjxeventabie ?а);

•    (unpreventabte ?а).

Каждое понятие определяется неформальной семантикой и аксиомой ЮР.

29.3    Теории, обусловленные встроенными действиями: временной разброс

Для данной теории необходимы:

•    occtree.th;

•    psi_core.th.

29.4    Дефинициональные расширения, обусловленные встроенными действиями:

временной разброс

Для данных расширений необходимы:

•    occ_precond.def.

•    state_precond.def:

•    preoond.def.

29.5    Определения встроенных действий: временной разброс

Для встроенных действий (временной разброс) определены нижеследующие понятия.

29.5.1    spread

Некоторое событие ?осс является разбросом тоща и только тоща, когда каждое событие ограничено повремени.

(forali (?осс) (iff (spread ?осс)

(feral (?а ?s1 ?s2 ?s3)

(implies (and (occurrence_of ?occ ?a)

(root_occ ?s3 ?occ)

(subactivity_occurrence ?s1 ?occ)

(iso_occ ?S1 ?s2)

(embedjree ?s1 ?s2 ?s3 ?a)

(begin_eqoiv?s1 ?s2))

(subocc_equiv ?s1 ?s2 ?s3 ?a)))))

29.5.2    partial.spread

Некоторое событие ?ooc является частичным разбросом тогда и только тоща, когда некоторые составляющие действия события ?осс ограничены по времени.

(forali (?осс) (iff (partial„spread ?осс)

(exists (?а ?s ?s1 ?s3 ?&4)

(and (occurrence„of ?occ ?a)

(root_occ ?s ?occ)

(subactivity_occurrence ?s1 ?occ)

(foraM (?«2)

(implies (and (iso.occ ?s1 ?s2)

(embed_tree ?sl ?s2 ?s ?a)

(begin„equfv ?s1 ?s2))

(subocc_equrv ?s1 ?s2 ?s ?a))))

(subactivity„occurrence ?s3 ?occ)

(iso_occ ?s3 ?s4)

(begm„equiv ?s3 ?s4)

(embed_tree ?s3 ?s4 ?s ?a)

(not (subocc_equiv ?s3 ?s4 ?s ?a))))))

29.5.3    tight

Некоторое событие occ? является частично плотным тоща и только тоща, когда ни одно из составляющих действий события ?осс не ограничено по времени.

(feral (?осс) (iff (tight ?осс)

(feral (?s?s1 ?а)

(implies (and (occurrence.of ?occ ?a)

(root__occ ?s ?occ)

(subactrvity„occurrence ?s1 ?occ))

(exists (?s2)

(and (iso„occ ?s1 ?s2)

(embed_tree ?sl ?s2 ?s ?a)

(begin„equrv ?s1 ?s2)

(not (subocc_equrv ?s1 ?s2 ?s ?a))))))))

Нижеследующие грамматические утверждения определяют описания процесса, установленные в ЮР для встроенных действий: временной разброс.

<    spread_ax»om >(foral (?s ?осс < variable >*)

<    simpie_spread_axiom >)

< partial_spread_axiom >    (forall (?s ?occ < variable >♦)

<    partiai_spread_axiom >))

<    spread_formula > (implies < subocc_formula >

<    simpte_time_ax»om >)

<    Sjmple_spread_axiom > ::= < spread_fbrmula> |

(and < simpie_spread_axjom > < simple_spread_axiom >♦)

<    partial_spread_formula > ::= (implies < subocc_formula >

< time_axiom >)

<    partial_spread_axiom > ::= < partial_spread_fc>rmula> |

(and < partial_spread_axiom > < partial_spread_axxxn >+)

30 Вариация неделимых вверх действий

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

30.1    Примитивная лексика вариации неделимых вверх действий

Лексика вариации неделимых вверх действий не требует примитивных соотношений. Критерий, используемый для классификации указанных действий: зависят или нет входные условия неделимых действий от входных условий супердействий для указанного действия.

30.2    Описываемые соотношения вариации неделимых вверх действий

В данном подразделе определены следующие соотношения:

•    (statejilter ?а);

•    (partal_state_fiiter ?а);

•    (rig»d_state_fitter ?а):

•    (time_filter?a):

•    (partialjimejilter ?а);

•    (rxjid time filter ?а);

•    (state_non filter ?a):

. (pamai_state_nonfilter?a);

•(П9Й. _state_nonfilter ?a);

•    (time_nonfifter ?a):

•    (partial_time_nonfil«er ?a);

•    (rigid_time_nonfilter ?a).

Каждое понятие определяется неформальной семантикой и аксиомой ЮР.

30.3    Теории, обусловленные вариацией неделимых вверх действий

Для данной теории необходимы:

•    occtree.th:

•    psl_core.th.

30.4    Дефииициоиальные расширения, обусловленные вариацией неделимых вверх действий

Для данных расширений необходимы:

•    occ_precond.def.

- state_precond.def;

•    precond.def.

30.5    Определения вариации неделимых вверх действий

Для вариации неделимых вверх действий определены нижеследующие понятия.

30.5.1    statejilter

Некоторое неделимое комплексное действие ?а является фильтром состояния при условии: если и только если какие-либо и когда-либо допустимые события для действия ?а согласованы по состоянию, то все составляющие действия ?а могут действительно иметь место.

(forall (?а) (iff (stateJitter ?а)

(forall (?а1 ?sl ?s2)

(implies (and (subactivity ?a 1 ?a)

(poss ?a ?s1)

(pass ?a ?s2)

(state_equiv ?s1 ?s2))

(poss_equiv?a1 ?s1 ?s2)»))

30.5.2    partial_state_filter

Некоторое неделимое комплексное действие ?а является частичным фильтром состояния тогда и только тогда, когда существуют допустимые события для действия ?а. согласованные по состоянию, в которых все составляющие действия для ?а могут действительно иметь место.

(forall (?a)(iff(partiai_state_flter?a)

(and (exists (?s1)

(forall (?s2)

(implies (and (subactivity ?a1 ?a)

(poss?a?s1)

(poss ?a ?s2)

(state_equiv ?s1 ?s2))

(poss_equrv ?a1 ?s1 ?s2))))

(exists (?a2 ?s3 ?s4)

(and (subactivity ?a2 ?a)

(poss ?a ?s3)

(poss ?a ?s4)

(state_equiv ?s3 ?s4)

(not (poss.equiv ?a2 ?s3 ?s4)))))))

30.5.3    rigid_state_filter

Некоторое неделимое комплексное действие ?а является жестким фильтром состояния при условии: если и только если какие-либо и когда-либо допустимые события для действия ?а согласованы по состоянию. то существуют составляющие действия для ?а. которые не могут происходить (случаться).

(forall (?э) (iff (rtgid_etate_filt©f ?а)

(forall (?s1)

(exists (?а1 ?s2)

(and (state_equiv ?s1 ?s2)

(poss ?a ?s1)

(poss ?a ?s2)

(not (poss_equiv ?a1 ?s1 ?s2)))))))

30.5.4    time.filter

Некоторое неделимое комплексное действие ?а является фильтром по времени при условии: если и только если какие-либо и когда-либо допустимые события для ?а согласуются по времени начала отсчета, то все составляющие действия для ?а могут действительно происходить (случаться).

(forall (?а) (iff (timeJitter ?а)

(forall (?а1 ?s1 ?s2)

(implies (and (subactivity ?a1 ?a)

(poss ?a ?s1)

(poss ?a ?s2)

(begfo_equiv ?s1 ?s2))

(poss_epuiv ?a1 ?s1 ?s2)))))

30.5.5    partial_time_ftlter

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

(forall (?а) (iff (partial_time_Bter ?а)

(and (exists (?s1)

(forafl (?s2)

(implies (and (subactivity ?a1 ?a)

(poss?a?s1)

(poss?a?s2)

(begin_equiv?s1 ?s2))

(poss_equrv?a1 ?s1 ?s2))))

(exists (?a2 ?s3 ?s4)

(and (subactivity ?a2 ?a)

(poss ?a ?s3)

(poss ?a ?s4)

(begin_equiv ?s3 ?s4)

(not (poss_equiv ?a2 ?s3 ?s4)))))))

30.5.6    rigid_time_filter

Некоторое неделимое комплексное действие ?а является жестким фильтром по времени при условии: если и только если какие-либо и когда-либо допустимые события для ?а согласуются по времени начала отсчета, то существуют составляющие действия для ?а. которые не могут происходить (случаться).

(forall (?a)(iff(rigid_tirne_filter?a)

(forall (?s1)

(exists (?a1 ?s2)

(and (begin_equrv ?s1 ?s2)

(poss ?a ?s1)

(poss ?a ?s2)

(not (poss_equiv ?a1 ?sl ?s2)))))))

30.5.7    state.nonfilter

Некоторое неделимое комплексное действие ?a не является фильтром состояния при условии: если и только если какие-либо и когда-либо допустимые события для ?а согласованы по состоянию, то все события для составляющих действий ?а согласованы по допустимости.

(forall (?а) (iff (state_non filter ?а)

(forall (?a1 ?s1 ?s2)

(implies (and (subactivity ?a1 ?a)

(not (poss ?a?s1))

(not (poss ?a ?s2))

(state_equrv ?s1 ?s2))

(poss_equiv?a1 ?s1 ?s2)))))

30.5.8    partial_state_nonfilter

Некоторое неделимое комплексное действие ?а не является частичным фильтром по состояюио тогда и только тогда, когда существуют допустимые события для ?а. согласованные по состоянию, в которых все составляющие действия для ?а согласованы по допустимости.

(forall (?a)frff(partial_state_nonfilter?a)

(and (exists (?s1)

(forafl (?s2)

(implies (and (subactivity ?a1 ?a)

(not (poss?a?s1))

(not (poss ?a ?s2))

(state_equiv ?s1 ?s2))

(poss_equtv ?a1 ?s1 ?s2)»>

(exists (?a2 ?s3 ?s4)

(and (subactivity ?a2 ?a)

(not (poss ?a ?s3)>

(not (poss ?a ?s4)}

(state_equiv ?s3 ?s4)

(not (poss_equiv ?a2 ?s3 ?s4))))))>

30.5.9    rigld_state_nonfilter

Некоторое неделимое комплексное действие ?а не является жестким фильтром по состоянию при условии: если и только если какие-либо и когда-либо допустимые события для ?а согласованы по состоянию. то существуют составляющие действия для ?а. не согласованные по допустимости.

(forall (?а) (iff (rigid__state_nonfilter ?а)

(forall (?s1)

(exists (?a1 ?s2)

(and(state_equiv?s1 ?s2)

(not (poss?a?s1))

(not (poss ?a ?s2))

(not(poss_equiv?a1 ?s1 ?s2)))))))

30.5.10    time.nonfilter

Некоторое неделимое комплексное действие ?а не является фильтром по времени при условии: если и только если какие-либо и когда-либо допустимые события для ?а согласуются по времени начала отсчета, то все события для составляющих действий по ?а согласованы по допустимости.

(forall (?а) (iff (time_nonffiter ?а)

(forall (?a1 ?s1 ?s2)

(implies (and (subactivity ?a1 ?a)

(not (poss ?a?s1))

(not (poss ?a ?s2))

(begm_equiv?s1 ?s2))

(poss_equiv ?al ?s1 ?s2)))))

30.5.11    partial_time_nonfllter

Некоторое неделимое комплексное действие ?а не является частичным фильтром по времени тогда и только тогда, когда существуют допустимые события для ?а. согласованные по времени начала отсчета, в которых все составляющие действия для ?а согласованы по допустимости.

(forall (?а) (iff (partal_time_non filter ?а)

(and (exists (?s1)

(feral (?s2)

(impfees (and (subactivity ?a1 ?a)

(not (poss ?a?s1))

(not (poss ?a ?s2))

(begin_equiv ?st ?s2))

(poss_equrv ?a1 ?s1 ?s2))))

(exists (?a2 ?s3 ?s4)

(and (subactivity ?a2 ?a)

(not (poss ?a ?s3))

(not (poss ?a ?s4))

(begin_equrv ?s3 ?s4)

(not (poss^equiv ?a2 ?s3 ?s4))))))>

30.5.12    rigid_time_nonfilter

Некоторое неделимое комплексное действие ?а не является жестким фильтром по времени при условии: если и только если какие-либо и когда-либо допустимые события для ?а согласуются по времени начала отсчета, то существуют составляющие действия для ?а. не согласованные по допустимости.

(forall (?а) (iff (rigid_time_nonfi!ter ?а)

(forall <?s1)

(exists (?a1 ?s2)

(and (begin.equiv ?s1 ?s2)

(not (poss ?a?s1))

(not (poss ?a ?s2>)

(not (poss_equiv ?a1 ?s1 ?s2)))))))

30.6 Грамматика описаний процесса для вариации неделимых вверх действий

Грамматика описаний технологического процесса для классов действий, описываемых для вариации эффекта затирания полезных данных, эквивалентна грамматике общего описания процесса, установленной I4C018629-11.

31 Вариация неделимых вниз действий

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

31.1    Примитивная лексика вариации неделимых вниз действий

Лексика вариации неделимых вниз действий не требует примитивных соотношений.

31.2    Описываемые соотношения вариации неделимых вниз действий

8 данном подразделе определены следующие соотношения:

•    (state Jdeal ?а);

•    (partial_state_kJeal ?а);

*(П9Й. .state_»deai ?а);

•    (time_kteal ?а):

•    (parfcai_time_kJeaI ?а);

•    (rigid_time_kteai ?а);

•    (state_non ideal ?a);

•    (partiai_state_nonideal ?a);

•    (ngid_state_nonideai ?a);

•    (time.nonideal ?a);

•    (partial_time_non'ideal ?a):

•(rigid. time_nori ideal ?a).

Каждое понятие определяется неформальной семантикой и аксиомой KIF.

31.3    Теории, обусловленные вариацией неделимых вниз действий

Для данной теории необходимы:

•    occtree.th:

•    psl._core.th.

31.4    Дефииициоиальиые расширения, обусловленные вариацией неделимых вниз действий

Для данных расширений необходимы:

•    occjxecond.def.

•    state_precond.def;

•    precond.def.

31.5    Определения вариации неделимых вниз действий

Для вариации неделимых вниз действий определены нижеследующие понятия.

31.5.1    state.kleal

Некоторое неделимое комплексное действие ?а является действием с идеальным состоянием при условии: если и только если какие-либо и когда-либо допустимые события для ?а согласованы по состоянию. то все супердействия для ?а согласованы по допустимости.

(forall (?а) (iff (state.ideal ?а)

(forall (?а1 ?s1 ?s2)

(implies (and (subactivity ?a ?a1)

(poss?a?s1)

(poss ?a ?s2)

(state.equiv ?s1 ?s2))

(poss_equiv?a1 ?s1 ?s2)))))

31.5.2    partial_state_ideal

Некоторое неделимое комплексное действие ?а является действием с частично идеальным состоянием тогда и только тогда, когда существуют допустимые события для ?а. согласованные по состоянию, е которых все супердействия для ?а согласованы по допустимости.

(forall (?а) (iff (partial_stat6jd6al ?а)

(and (exists (?s1)

(feral (?s2)

(implies (and (subactivity ?a ?a1)

(poss?a?sl)

(poss ?a ?s2)

(state_equiv ?s1 ?s2)>

(poss_equrv?a1 ?s1 ?s2))))

(exists (?a2 ?s3 ?s4)

(and (subactivity ?a ?a2)

(poss ?a ?s3)

(poss ?a ?s4)

(state_equiv ?s3 ?s4)

(not (poss_equiv ?a2 ?s3 ?s4)»)»>

31.5.3    rigid_state_idea!

Некоторое неделимое комплексное действие ?а является действием с жестким идеальным состоянием при условии: если и только если какие-либо и когда-либо допустимые события для ?а согласованы по состоянию, то существуют супердействия для ?а. не согласованные по допустимости.

(forall (?а) (iff (rigid_state Jdeal ?а)

(forall (?s1)

(exists (?a1?s2)

(and (state_equiv ?s1 ?s2)

(subactivity ?a ?a1)

(poss?a?s1)

(poss ?a ?s2)

(not (poss_epuiv ?a1 ?s1 ?s2)))))))

31.5.4    timejdeal

Некоторое неделимое комплексное действие ?а является действием, идеальным по времени при условии: если и только если какие-либо и когда-либо допустимые события для ?а согласованы по времени начала отсчета, то все супердействия для ?а согласованы по допустимости.

(forall (?a)(iff(time_»deal ?а)

(forall (?a1 ?s1 ?s2)

(implies (and (subactivity ?a ?a1)

(poss ?a ?sl)

(poss ?a ?s2)

(begin.equiv ?s1 ?s2))

<poss_equiv ?a1 ?s1 ?s2)))))

31.5.5    partia!_time_ideal

Некоторое неделимое комплексное действие ?а является частично идеальным по времени тогда и только тогда, когда существуют допустимые события для ?а. согласованные по времени начала отсчета, в которых все супердействия для ?а согласованы по допустимости.

(forall (?а) (iff (part>al_time_ideal ?а)

(and (exists (?s1)

(feral (?s2)

(implies (and (subactivity ?a ?a1)

(poss?a?sl)

(poss ?a ?s2)

(begin_equiv ?s1 ?s2))

(poss^equrv ?a1 ?s1 ?s2))))

(exists (?a2 ?s3 ?s4)

(and (subactivity ?a ?a2)

(poss ?a ?s3)

(poss ?a ?s4)

(begin_equiv ?s3 ?s4)

(not (poss_equiv ?a2 ?s3 ?s4)))))))

31.5.6    rigid_time_ideal

Некоторое неделимое комплексное действие ?а является жестко идеальным по времени при условии: если и только если какие-либо и когда-либо допустимые события для ?а согласованы по состоянию, то существуют супердействия для ?а. не согласованные по допустимости.

(forall (?а) (iff (rigid_time_ideal ?а)

(forall (?s1)

(exists (?a1 ?s2)

(and (begin_equrv ?s1 ?s2)

(poss ?a ?s1)

(poss ?a ?s2)

(not (poss_equiv ?a1 ?si ?s2)))))))

31.5.7    state.nonldeal

Некоторое неделимое комплексное действие ?а является неидеальным по состоянию при условии: если и только если какие-гмбо и когда-либо допустимые события для ?а согласованы по состоянию, то все события для супердействий по ?а согласованы по допустимости.

(forall (?а) (iff (state_nonideal ?а)

(forall (?а1 ?s1 ?s2)

(implies (and (subactivity ?a ?a1)

(not (poss ?a ?s1))

(not (poss ?a ?s2))

(state.equiv ?s1 ?s2>)

(poss_equiv ?a1 ?s1 ?s2)))))

31.5.8    partial_state_nonideaJ

Некоторое неделимое комплексное действие ?а является частично неидеальным по состоянию тоща и только тоща, когда существуют допустимые события для ?а. согласованные по состоянию, в которых все супердействия по ?а согласуются по допустимости.

(forall (?а) (rff (pamai_state_nonideal ?а)

(and (exists (?s1)

(foraS (?s2)

(implies (and (subactivity ?a ?a1)

(not (poss ?a ?s1))

(not (poss ?a ?s2))

(state_equrv?s1 ?s2))

(poee_equrv?3l ?e1 ?e2)))>

(exists (?a2 ?s3 ?s4)

(and (subactivity ?a ?a2)

(not (poss ?a ?s3))

(not (poss ?a ?s4))

(state_equiv ?s3 ?s4)

(not (poss_equiv ?a2 ?s3 ?s4)))))))

31.5.9    rigid_state_nonideal

Некоторое неделимое комплексное действие ?а является жестко неидеальным по состоянию при условии: если и только если какие-либо и когда-либо допустимые события для ?а согласованы по состоянию. то существуют супердействия по ?а. не согласованные по допустимости.

(forall (?а) (iff (rigid__state_nonkJeal ?а)

(forall <?s1)

(exists (?a1 ?s2)

(and (state_equiv ?s1 ?s2)

(not (poss ?a?s1))

(not (poss ?a ?s2))

(not (poss_equiv ?a1 ?s1 ?s2)))))))

31.5.10    tlme.nonideal

Некоторое неделимое комплексное действие ?а является неидеальным по времени при условии: если и тогъко если какие-либо и когда-либо допустимые события для ?а согласуются по времени начала отсчета, то все события для супердействий по ?а согласуются по допустимости.

(forall (?а) (iff (time^non ideal ?а)

(forall (?al ?sl ?s2)

(implies (and (subactivity ?a ?a1)

(not (poss?a?s1))

(not (poss ?a ?s2))

(begin_equiv ?s1 ?s2))

(poss_equiv ?a1 ?s1 ?s2)))))

31.5.11    partial_time_nonldeai

Некоторое неделимое комплексное действие ?а является частично неидеальным по времени тогда и только тогда, когда существуют допустимые события для ?а. согласованные по времени начала отсчета, в которых все супердействия по ?а согласованы по допустимости.

(forall (?а) (iff (paftiaLtime_nontdeaJ ?а)

(and (exists (?s1)

(fora* (?s2)

(impies (and (subactivity ?a ?a1)

(not (poss ?a ?sl))

(not (poss ?a ?s2))

(begin_equiv ?s1 ?s2))

(poss_equiv ?a1 ?s1 ?s2))))

(exists (?a2 ?s3 ?s4)

(and (subactivity ?a ?a2)

(not (poss ?a ?s3))

(not (poss ?a ?s4))

(begm_equrv ?s3 ?s4)

(not (poss.equiv ?a2 ?s3 ?s4)))))))

31.5.12    rigid_time_nonideai

Некоторое неделимое комплексное действие ?а является жестко неидеальным по времени при уело* в»«: если и только если какие-либо и когда-либо допустимые события для ?а согласуются по времени начала отсчета, то существуют супердействия для ?а. не согласованные по допустимости.

(forall (?а) (iff (г igtf_time_nonideal ?а)

(forall (?s1)

(exists (?a1?s2)

(and (begin_equiv ?s1 ?s2)

(subactivity ?a?a1)

(not (poss vavsl)}

(not (poss ?a?s2))

(not (poss.equiv ?a1 ?s1 ?s2)»))))

31.6 Грамматика описаний процесса для вариации неделимых вниз действий

Грамматика описаний технологического процесса для классов действий, описываемых в вариации неделимых вниз действий, эквивалентна грамматике общего описания технологического процесса в соответствии с ИС018629-11.

32 Входные условия совместных действий

Данный раздел характеризует все определения, обусловленные входными условиями совместных действий. Критерий, используемый для классификации указанных действий: сохраняются или нет входные условия заданного неделимого действия составом совместных действий.

32.1    Примитивная лексика входных условий совместных действий

Лексика входных условий совместных действий не требует примитивных соотношений.

32.2    Описываемые соотношения входных условий совместных действий

8 данном подразделе определены следующие соотношения:

- (preserved.fiiter ?а ?a1 ?s);

• (noninterfering ?а);

•    ((interfering ?а);

•    (imperial ?а);

•    (gfobaljnterfere ?а).

Каждое понятие определяется неформальной семантикой и аксиомой K1F.

32.3    Теории, обусловленные входными условиями совместных действий

Для данной теории необходимы:

•    occtree.th:

•    psl_core.th.

32.4    Дефииициональные расширения, обусловленные входными условиями совместных действий

Для данных расширений необходимы:

•    occ_precood.def,

•    statejxecond.def;

•    precond.def.

32.5    Определения входных условий совместных действий

Для входных условий совместных действий определены нижеследующие понятия.

32.5.1    preserved.filter

Действия ?а и ?а1 являются элементами сохраненного фильтра тогда и только тогда, когда допусти* мые события какого-либо супердействия для ?а сохранены указанным составом совместных действий с ?а1.

(forall (?а?а1 ?s)(cff (preserved_filter?a ?а1 ?s)

(fbral(?a2)

(implies (subactivity ?a ?a2)

(iff (poss ?a2 ?s)

(poss (cone ?a2 ?a1) ?s))))))

32.5.2    noninterfering

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

(forall (?а ?s) (iff (noninterfering ?а ?s)

(foral (?а1)

(implies (atomic ?a1)

(preserved_fiiter?a?al ?s)))))

32.5.3    interfering

Некоторое действие является препятствующим тогда и только тогда, когда существует некоторое неделимое действие, не являющееся элементом некоторого сохраненного фильтра с ?а.

(forall (?а ?s) (iff (interfering ?а ?s)

(exists (?а1)

(and (atomic ?a1)

(not(preserved_filter?a?a1 ?s)»)))

32.5.4    imperial

Некоторое действие является имперским тогда и только тогда, когда не существует неделимого действия. являющегося элементом сохраненного фильтра с ?а.

(foral (?а ?s) (iff (imperial ?а ?s)

(fbral (?a1)

(implies (atomic ?a1)

(not(preserved_filter?a?a1 ?s))))))

32.5.5    globaljnterfere

Некоторое действие является глобально препятствующим тогда и только тогда, когда все события для ?а имеют одинаковые сохраненные фигьтры для ?а.

(forall (?а ?s) (rff (globaljnterfere ?а)

(foral (?а1)

(implies (atomic ?a1)

(foral (?s1 ?s2)

(iff (preserved_eter ?a ?al ?s1)

(preserved_flter ?a ?a1 ?s2)))))))

32.6 Грамматика описаний процесса для входных условий совместных действий

Грамматика описаний технологического процесса для классов действий, описываемых для вариации входных условий совместных действий, эквивалентна грамматике общего описания технологического про* цесса в соответствии с ИС018629*11.

33 Эффекты совместных действий

Данный раздел характеризует все определения, обусловленные эффектами совместных действий. Критерий, используемый для классификации указа) в tux действий: сохранены или нет эффекты неделимых действий составом совместных действий.

33.1    Примитивная лексика эффектов совместных действий

Лексика эффектов совместных действий не требует примитивных соотношений.

33.2    Описываемые соотношения эффектов совместных действий

8 данном разделе определены следующие соотношения;

•    (preserved_effect ?а ?a1 ?s):

•    (nonclobbering ?а);

•    (clobbering ?а):

- (meddling Та):

•    (giobaLclobber ?а).

Каждое понятие определяется неформальной семантикой и аксиомой ЮР.

33.3    Теории, обусловленные эффектами совместных действий

Для данной теории необходимы:

•    occtree.th;

•    psl_core.th.

33.4    Дефииициоиальиые расширения, обусловленные эффектами совместных действий

Для данных расширений необходимы.

•    occ_precond.def.

•    statejjrecond.def; precond.def.

33.5    Определения эффектов совместных действий

Для эффектов совместных действий определены нижеследующие понятия.

33.5.1    preserved.effect

Действия ?а и ?а1 сохраняют эффекты тогда и только тоща, когда указанные эффекты событий для какого*либо супердействия для ?а сохранены указанным составом совместных действий с ?а1. (forall(?a?a1 ?s) (iff (preserved_effects ?a ?al ?s)

(foratl (?a2 ?f)

(implies (subactivity ?a ?a2)

(iff (holds ?f (successor ?a2 ?s))

(holds ?f (successor (cone ?a2 ?a1) ?s))))))

33.5.2    nonclobbering

Некоторое действие ?a не затирает полезные данные тоща и только тогда, когда любое неделимое действие сохраняет указанные эффекты для ?а.

(forail (?а ?s) (iff (nonclobbering ?а ?s)

(fora* (?а1)

(implies (atomic ?a1)

(preserved_effects ?a ?al ?s))>)

33.5.3    clobbering

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

(forail (?а ?s) {iff (clobbering ?а ?s)

(exists (?a1)

(and (atomic ?a1)

(not (preserved.effects ?a ?a1 ?s)))))

33.5.4    meddling

Некоторое действие является вмешивающимся тогда и только тогда, когда не существует некоторого неделимого действия, сохраняющего эффекты для ?а.

((oral (?а ?s) (iff (meddling ?а ?s)

(feral (?a1)

(implies (atomic ?a1)

(not (preserved.effects ?a ?a1 ?s)))))

33.5.5    globat_clobber (defrelabon global.dobber (?a)

(feral (?a1)

(implies (atomic ?a1)

(foral(?s1 ?s2)

(iff (preserved.effects ?a ?a1 ?s1)

(preserved_effects ?a ?a1 ?s2))))))

ЗЗ.в Грамматика описаний процесса для эффектов совместных действий

Грамматика описаний технологического процесса для классов действий, описываемых эффектами совместных действий, эквивалентна грамматике общего описания технологического процесса в соответствии с ИСО 18629-11.

34 Вариация препятствующих входных условий

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

34.1    Примитивная лексика вариации препятствующих входных условий

Лексика вариации препятствующих входных условий не требует примитивных соотношений.

34.2    Описываемые соотношения вариации препятствующих входных условий

В данном подразделе определены следующие соотношения:

•    (state .interfere ?а);

•    (partialjnterfere ?а):

•    (uncooditionaljnterfere ?а);

-    (time.inteffere ?а):

•    (sometime.interfere ?а);

•    (rigid .interfere ?а).

Каждое понятие определяется неформальной семантикой и аксиомой K1F.

34.3    Теории, обусловленные вариацией препятствующих входных условий

Для данной теории необходимы:

•    occtree.th;

-    psl.core.th.

34.4    Дефииициоиальные расширения, обусловленные вариацией препятствующих входных условий

Для данных расширений необходимы:

•    occ_precond-def;

-    state jxecond.def:

•    precond.def.

34.5 Определения вариации препятствующих входных условий

Для вариации препятствующих входных условий определены нижеследующие понятия.

34.5.1    statejnterfere

Некоторое действие ?а препятствует состоянию тогда и только тогда, когда какие-либо события, согласованные по состоянию, имеют те же сохраненные фильтры.

(forall (?а) frff (statejnterfere ?а)

(foral! (?а1 ?s1 ?s2)

(implies (and (atomic ?a1)

(state_equrv ?s1 ?s2))

(iff (preservedJiter ?a1 ?a?s1)

(preservedJ#er ?al ?a ?s2)))))

34.5.2    partialjnterfere

Некоторое действие ?a препятствует частично тогда и только тогда, когда существуют события, согласованные по состоянию и имеющие те же сохраненные фильтры.

(forall (?а) (iff (partialjnterfere ?а)

(and (exists (?s1 ?a1)

(foral (?s2)

(implies (and (atomic ?a1)

(state__equiv ?s1 ?s2)>

(iff (preserved_filter?al?a?sl)

(preservodjilter ?a1 ?a ?s2)))))

(exists (?a2 ?s3 ?s4)

(and (atomic ?a2)

(state_equrv ?s3 ?s4)

(preserved Jiter ?a2 ?a ?s3)

(not (preservedJilter ?a2 ?a ?s4)»)))>

34.5.3    unconditionaljnterfere

Некоторое действие препятствует безусловно тогда и только тогда, когда для каких-либо согласованных по состоянию событий существуют различные сохраненные фильтры.

(forall (?а) (Л (unconditional_riterfere ?а)

(forall (?s1)

(exists (?а1 ?s2)

(and (atomic ?a1)

(stato_equiv ?sl ?s2)

(iff (preservedJiter ?al ?a?s1)

(not (preserved_filter ?al ?a ?s2))))))))

34.5.4    timejnterfere

Некоторое действие ?a препятствует no времени тогда и только тогда, когда какие-либо согласованные по времени начала отсчета события имеют те же сохраненные фильтры.

(forall (?а) frff (time_interfere ?а)

(forall (?а1 ?st ?s2)

(implies (and (atomic ?a1)

(begin_equiv ?s1 ?s2)) frff(preserved_filter?al ?a?sl)

(preservedJitter ?a1 ?a?s2))))))

34.5.5    sometimejnterfere

Некоторое действие ?a препятствует тогда тогда и только тогда, когда существуют согласованные по времени начала отсчета события, имеющие те же сохраненные фильтры.

(forall (?а) frff (sometime Jnterfere ?а)

(and (exists (?s1 ?a1)

(foral (?s2)

(implies (and (atomic ?a1)

(begin_equiv ?s1 ?s2)) fiff (preserved Jitter ?a1 ?a?s1)

(preserved_fitter ?a1 ?a ?s2))))>

(exists (?а2 ?s3 ?s4)

(and (atomic ?a2)

(begin_eQuiv ?s3 ?s4)

(preserved_fiitef ?a2 ?a ?s3)

(not (preserved_filter ?a2 ?a ?s4»)))))

34.5.6    rlgidjnterfere

Некоторое действие препятствует жестко тогда и только тогда, когда для каких-либо согласованных по времени начала отсчета событий существуют другие сохраненные фильтры.

(forail (?а) (Л (rigid_interfere ?а)

(forail (?s1)

(exists (?а1 ?s2)

(and (atomic ?al)

(begin_equiv ?s1 ?s2)

(iff(preserved_flter?al ?a?s1)

(not (preserved Jlter ?a1 ?a ?s2))))))))

34.6    Грамматика описаний процесса для вариации препятствующих входных условий

Грамматика описаний технологического процесса для класса действий, описываемых для вариации препятствующих входных условий, эквивалентна грамматике общего описания технологического процесса в соответствии с ИС018629-11.

35 Вариация эффектов затирания полезных данных

Данный раздел характеризует все определения, обусловленные вариацией эффектов затирания полезных данных Критерий, используемый для классификации указанных действий: сохраняются или нет эффекты заданного неделимого действия составом совместных действий, когда состояние, предшествующее выполнению действия, сохраняется.

35.1    Примитивная лексика вариации эффектов затирания полезных данных Лексика вариации эффектов затирания полезных данных не требует примитивных соотношений.

35.2    Описываемые соотношения вариации эффектов затирания полезных данных

8 данном подразделе определены следующие соотношения:

•    (state_clobber ?а);

•    (partial_c*obber ?а);

•    (unoonditionel_clobber ?е);

•    (time_clobber ?а);

•    (sometime_cJobber ?а):

•    (rigid_dobbef ?а).

Каждое понятие определяется неформальной семантикой и аксиомой ЮР.

35.3    Теории, обусловленные вариацией эффектов затирания полезных данных

Для данных теорий необходимы:

•    occtree.th:

•    psJ_core.th.

35.4    Дефинициоиальные расширения, обусловленные вариацией эффектов затирания полезных данных

Для данных расширений необходимы:

•    occ_precond.def;

•    state jxecond.def;

•    precond.def.

35.5    Определения вариации эффектов затирания полезных данных

Для вариации эффектов затирания полезных данных определены нижеследующие понятия.

35.5.1 state.clobber

Некоторое действие ?а затирает данные о состоянии тогда и только тогда, когда какие-либо согласованные по состогыию события сохраняют те же эффекты.

(forall (?a)(iff(state_dobber?a)

(forall(?a1?s1?s2)

(impies (and (atomic ?a1)

(state_equiv ?s1 ?s2)>

(iff (preserved _effects ?al ?a ?s1)

(preserved_effects ?al ?a ?s2))))))

35.5.2    partiaf_state_ck>bber

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

(forall (?а) (iff (parttal_ck>bbef ?а)

(and (exists (?s1 ?a1)

(feral (?s2)

(impies (and (atomic ?a1)

(state__equiv ?s1 ?s2))

(iff (preserved_effects ?a1 ?a ?s1)

(preserved_effects?al ?a?s2)))))

(exists (?a2 ?s3 ?s4)

(and (atomic ?a2)

(state.equiv ?s3 ?s4)

(preserved_effects ?a2 ?a ?s3)

(not (preserved_effects ?a2 ?a ?s4)))))))

35.5.3    unconditional.clobber

Некоторое действие ?a затирает данные безусловно тогда и тогысо тогда, когда существуют согласованные по состоянию события, не сохраняющие те же эффекты.

(forall (?а) (iff (unconditionai.clobber ?а)

(forall (?s1)

(exists (?a1 ?s2)

(and (atomic ?a1)

(state_equiv ?s1 ?s2)

(iff (preserved ^effects ?al ?a ?s1)

(not(preseived_effects?al ?a ?s2))))))))

35.5.4    time.elobber

Некоторое действие ?a затирает данные о времени тогда и только тогда, когда какие-либо согласованные по времени наняла отсчета события сохраняют те же аффекты.

(forall (?а) (iff (time_dobber ?а)

(forall (?а1 ?s1 ?s2)

(implies (and (atomic ?a1)

(begri_eqi«v ?s1 ?s2))

(iff(preserved_effects?a1 ?a?s1)

(preserved_effects ?al ?a ?s2))))))

35.5.5    sometime_ck>bber

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

(forall (?а) (iff (sometime_cfobber ?а)

(and (exists (?sl ?al)

(feral (?s2)

(implies (and (atomic ?a1)

(begin_equiv ?s1 ?s2))

Crff(preserved_effects?a1 ?a?s1)

(preserved_effects ?a1 ?a ?s2)))))

(exists (?a2 ?s3 ?s4)

(and (atomic ?a2)

(begin_equiv ?s3 ?s4)

(preserved_effocts ?a2 ?a ?s3)

(not (preserved_effects ?a2 ?a ?s4)))))})

35.5.6    rigid.clobber

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

(forall (?а) (iff {rigid_cJobbef ?а)

(forall (?s1)

(exists (?a1 ?s2)

(and (atomic ?a1)

(begin_equiv ?s1 ?s2)

(iff (preserved_effects ?a1 ?a ?s1)

(not(preserved_effects?al ?a ?s2))))))))

35.6    Грамматика описаний процесса для вариации эффектов затирания полезных данных

Грамматика описаний технологического процесса для классов действий, описываемых для вариации эффектов затирания полезных данных, эквивалентна грамматике общего описания технологического процесса в соответствии с И С016629-11.

Приложение А (справочное)

ASN.1 Идентификатор настоящего стандарта

Для однозначной идентификацм1 информационного обьегта в открытой системе настоящему стандарту присвоен слвдуюивм идентификатор:

во standard 18629 part 42 version 1

Значение датого идентификатора определено в ИСО/МЭК 8824-1 и детально описано в ИСО 18629-1.

Приложение В (справочное)

Пример описания технологического процесса в соответствии с настоящим стандартом

В данном приложении рассмотрен подробный сценарий использования языка спецификаций процесса PSL (Process Speculation Language) в соответствии с ИСО 18629. Далее рассмотрен частный случай использования программного огмсания технолопьюского процесса.

Даньый сценарий включает совместное выполнение нескольких операций. Целью является повыше* ьно эффективности испольэоеамет данных о технологическом процессе при изготовленми иэдегмя. Подчеркнем, что даный язык программирования прежде всего позволяет повысить эффективность компьютерного обмена данными между сотру дамками планового отдела и руководством производственного подразделеныя.

В .пт~Ш“ приложении рассмотрено расширение примера, использованного в ИСО 18629-11:2005 (приложение С). Пример иптосгрирует технические приложения внешних понятий для спецификащни процесса изготовления изделия GT-350.

В.1 Процесс изготовления изделия GT-350

В данном разделе различные производство! я мо процессы объединены в набор действии высокого уровня, необходимых для создания изделия GT-350. В соответствмг с технологической картой изде/ыя GT-350 (см. ИСО 18629-11:2005. таблица С.1) компоненты данного издегмя либо покупают по контракту или изготовляет внутри самого предприятия. Рассматриваемые описания технологических процессов связаны с конкретными действиями, выпогыяемыми внутри предприятия для изготовленье! компонентов изделия. Данное рассмотрению технологического процесса в направлении «сверху — вниз» дает общую картину происходящего, описание комплексного действия по изготовлению изделия GT-350. состоящего из составляющих действий, выпогыяемых на уровне более мелких подразделений предприятия.

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

ОЯцяе

<<т

Рисунок В.1 — Верхний уровень процесса изготовленье! изделия GT-350

Представление верхнего уровня технологического промесса на языке PSL имеет вид: (subactivity make-chassis make_gt350>

(subactivity make-interior make_gt350)

(subactivity make-drive make qt350)

(subactivity make-tran make gt35Q1 (subactivity mako-engne make qt350)

(subactivity final-assembly make qt350)

(forall (?occ) (iff


(occurrence_of ?occ make ql350>

(exists (?occ1 ?occ2 ?occ3 ?occ4 ?occ5 ?occ6}

(and (occurrence_of ?occ1 make.chassis) (occurrence_of ?occ2 make.inlerior) (occurrence_of ?occ3 make_drive) (occurrence_o( ?occ4 make_trim) (occurrence_of ?occ5 make_engine) (occurrence_of ?occ6 final.assembty)

(subactrvtfy.occixrence ?occ1 ?occ)

(subectivity_occurTence ?occ2 ?occ) (subacbvity_occunence ?occ3 ?occ) (subactivity_occunence ?oco4 ?occ) (subactJV*y_occurrence ?occ5 ?occ) (subactivity_occurrence ?occ6 ?ooc))>

(forall (?occ)

(iff (occurrence_of ?occ make_engir>e) (= (beginof ?occ) 0700)))

(trigger make_engine)

(conditional make_engme) (forall (?s1 ?s2 ?s3 ?s4 ?sS ?s6)

(implies (and (leaf.occ ?s1 ?occ1)

(leaf.occ ?s2 ?occ2)

(leaf.occ ?s3 ?occ3)

(Ы.иа ?ь4 ?uul4)

(leaf.occ ?s5 ?occ5)

(root.occ ?s6 ?occ6>)

(and {mm_precedes ?s1 ?s6 make qt350)

(man.precedes ?s2 ?s6 make qt350)

{min_p re cedes ?s3 ?s6 make_gt350)

(man_precedes ?s4 ?s6 make qt350)

(mm.precedes ?s5 ?s6 make gt350)))))))

Даннов представление форма/мзует технологический промесс в соответствии с рисунком В.1.

Псодействие «make.engine» (изготовление двигателя) не выполняется, если двигатель уже существует. Поэтому комплексное действие «make_gt350* является условным.

Действие «mafce_gt350» выполняется в момент времени 0700. Поэтому данное действие является запускающим.

На базе представления IDEF3 (в терминах представления технологического промесса) для краткого описания действам, встречающихся на различных стадиях процесса изготовления изделия, в настоящем стандарте приведены некоторые примеры использования языка программирования PSL-Outercore в соответствии с ИСО 18629-12.

8.2 Абстрактное действие «make.engine» (изготовление двигателя)

Двигатель изделия GT-350 собирается из агрегатов, изготовленных е нескогъких подразделениях предприятия. Схема промесса изготовления дана на рисунке В.2. Агрегат состоит из двигательного блока, жгутов и кабелей. Составляющие промессы детально рассмотрены в подразделах ниже. Двигатель издегмя GT-3S0 собирается на сборочном стенде А004. Сборка одного двигателя требует 5 мин.

Рисунок В.2 — Процесс изготовления двигателя изделия GT-350

Ниже представлены некоторые действия и данные технологического процесса изготовления двигателя на яэьке PSL (внешнее ядро):

(subactivity make_btock make_engine)

(subactivity make-bamess make_engine)

(subactivrty make-wves make_er>gine)

(subactivity assembie_er>gtne make.engine)

(uniform make_engine)

(unrestricted make_engine)

(not (atomc make_eogine))

(forall (?occ)

(iff (occurrence_of ?occ make_eogine)

(exists (?occ1 ?occ2 ?occ3 ?occ4)

(and (occurrence_of ?occ1 make_block)

(occurrence_of ?occ2 make_hamess)

(occurreoce_of ?occ3 make_wires)

(oocurreoce_of ?occ4 assemble_engme)

(subacbvrty.occurrence ?occ1 ?occ)

(subactmty_occurrence ?occ2 ?occ)

(subactrvrty_occurrence ?occ3 ?occ)

(subacbvity_occurTence ?occ4 ?occ)

(forall (?s1 ?s2 ?s3 ?s4)

(implies (and (teaf.occ ?s1 ?occ1)

(leaf_occ ?s2 ?oce2)

(teaf.occ ?s3 ?occ3)

(noot_occ ?s4 ?occ4))

(and (minjxecedes ?s1 ?s4 make_engme)

(m«n_precedes ?s2 ?s4 make_engine)

(min_precedes ?s3 ?s4 make.engine}))))

B.3 Действие «make_block» (изготовление блока)

Блок изделия GT-350 в^юлняется как агрегат для сборки двигателя изделия GT-350. Изготовление блока требует выполнения всех технологических операций, нэчжая от литья заготовки и ее механичеоой обработки (см. рисунок В.З).


П репсом ню 1Ютвлп11«сг0* ватага нн


Рисунок В.З — Процесс изготовления блока изделия GT-350

Представление некоторых действий и технологически дщвых на языке PSL (внешнее ядро):

(subactivity produce_molded_metal mafce_btock)

(subactivity mech«ne_b(ock make_blocfc)

(primitive mechine_btock)

(primitive produce_molded_metal)

(uniform make_blocfc)

(not (atomic make_b(ock})

(«oral! (?occ)

(iff (occurrence_of ?occ make_Wocfc)

(exists (?occ1 ?occ2)

(and (occurrence_of ?occ1 produce_motded_metal)

(occurrence.of ?occ2 machme_block)

(min_precedes ?occ1 ?occ2 make_btock)))))

(markov_precond machine_btock)

(forall (?occ)

(incites (and (occurrence_of ?occ machtne_block)

(legal ?oec))

(prior molded ?occ)))

(marttov_effects machine_blocfc)

(indies (and (oocurrence_of ?occ machine_b4ock)

(legal ?occ))

(holds finished ?occ)))

(markov_preoond produce_molded_metai)

(implies (and (occurrence_of ?occ machine_blod()

(legal ?occ))

(prior cast ?occ)))

(markov_effects produce_molded_metal)

(indies (and (occurrence_of ?occ machine_b4ocfc)

(legal ?occ))

(holds molded ?occ»)

Данное представление формализует технологический процесс, показанный на рисунке В.З. Составляющее действие *produce_molded_metai» (прессование металлической заготовки) имеет входное условие, в соответствии с которым прессоеачео должно предшествовать гмтъе. Таким образом, это есть действие с марковскими входными условиями (mackov_precond).

Составляющее действие «produce_molded_metal» имеет эффект, заключающийся в том. что штамповка блока происходит после предваритегъного пресс овагыя металлической заготовки (допустимое событие). Это есть маркоесхий эффект действия (markov_effect).

Составляющее действие «тэсМпв_Ыоск» (механическая обработка блока) имеет аховое условие, в соответствии с которым до механической обработки блок штампуется (допустимое событие). Это есть действие с марковскими входными условиями.

Составлявшее действие «mact*ne_block» (механическая обработка блока) имеет эффект, в соответстаюг с которым блок зачищается после прессования металл веской заготовки (допустимое событие). Это есть действие с марковским эффектом (markov_effect).

В.4 Действие «make_hamess» (изготовление жгута)

Жгут изделия GT-350 (см. рисунок В.4) изготовляют как сборочный агрегат двигателя изделия GT-350. Дан шй технологический процесс организован в цехе кабелей и проводов. Рисунок В.5 представляет процесс изготовления провода жгута. Жгут изделия GT-350 собирают на особом стенде из проемов и кабелей. Сборка одного жгута требует 10 ммн.

Рисунок В.4 — Процесс изготовления жгута изделия GT-350

Ниже дано представление некоторых действий и соответствующих технологических данных на языке PSL (внешнее ядоо):

(subactivity make_bamess_vMT8 make_harness)

(subactivrty assembte_hamess make_hamess)

(primitive assembte_hamess)

(occurrence_constramed assemble_hamess)

(forall (?occ)

(trr^lies (and (occurrence_of ?occ make_hamess_wkes)

(legal ?occ>)

(legal (successor assembte_hamess ?occ)}))

(forall (?occ)

(iff (occurrence_of ?occ make_hamass)

(exists (?occ1 ?occ2 ?occ3)

(and (occurrence_of ?occ1 make_hamess_wve)

(occurrence_of ?occ2 assemble_hamess)

(leaf.occ ?occ3 ?occ1)

(min_precedes ?occ3 ?occ2 make_hamess)))))

Датое представление формализует гехюпогинеооад процесс, представленный на рисунке В.4. Составляющее действие •assembte_hamess» (сборка жгута) имеет входное условие, в соответствии с которым сборка следует за изготовлением проводов жгута (make_hamess_wires). поэтому данное дейстаю является событийно ограниченным (occurrence.constrained).

Рисунок В.5 — Процесс изготовления провода жгута

В.5 Действие «make_hamess_wire» (изготовление провода жгута)

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

Рисунок В.6 — Процесс изготовления проводов издетя GT-350

Ниже дано представление некоторых действий и соответствующих технологических данных на языке PSL (внешнее ядро):

(subactivity extrude make_hamess_wtre)

(subactivity twist make_harness_wire)

(subactivity jacket make_hamess_wire)

(primitive extrude)

(primitive twist)

(primitive tacket)

(imconstrained extrude)

(forali (?occ)

(poss extrude ?occ))

(time_effects extrude)

(forali (?occ)

(implies (and (occurrence_of ?occ extrude)

(= (begnot ?occ) 0700))

(holds (temperature wire 100) ?occ)))

(unconstrained twist)

(forali (?occ)

(poss twist ?occ))

(context_free twist)

(unconstrained jacket)

(forali (?occ)

(poss jacket ?occ))

(forali (?occ)

(iff (occurrence_of ?occ make_hamess_wre)

(exists (?occ1 ?occ2 ?occ3)

(and (occurrence_of ?occ1 extrude)

(occurrence_of ?occ2 twist)

(occurrence_of ?occ3 jacket)

(min_precedes ?occ1 ?occ2 make_hamess_wire)

(min_precedes ?occ2 ?occ3 make_hamess_wire))))

Данное представление формализует технологический процесс, представло» и им на рисуисе В.5. Составляющие действия «extrude* (вытяжка), «twist» (офучеэние) и «jacket* (нанесение иэогвиии) всегда возможны. Следоватегъно. эти действия являются неограниченными.

Составляющее действие «twist* (скручивание) всегда имоот один и тот же эффект. Указанное действие является свободным в данном контексте (contexl_free).

Эффекты составляющего действия «extrude» (вытяжка) зависят от времени его выпогхнения (в момент времени 0700 провод имоот температуру 100 *С). Таким образом, это действие с эффектами, зависящими от врвмегм (bme_effect).

Приложение ДА (справочное)

Сведения о соответствии ссылочных международных стандартов ссылочным национальным стандартам

Российской Федерации

Таблица ДА.1

Обозначение ccwno'oioio международного стандарта

Степан»

соотаетстаяя

Обохгчеии* й «яиыенодение соотмтствуошего ияцйоияльмого стандарта

ИСОгМЭК 6824-1

IDT

ГОСТ Р ИСО/МЭК 8824-1—2001 «Информационная технология. Абстрактная синтаксическая нотэдоя версии Окем (АСН.1). Часть 1. Спецификация основной нотации»

ИСО 10303-1

ГОСТ Р ИСО 10303-1—99 «Системы автоматизации производства и их мгтегрэция. Представление данных об издеши и обмен этим* данныьы. Часть 1. Общие представления и основополагающие примдипы»

ИС015531-1

IDT

ГОСТ Р ИСО 15531-1—2008 «Промышленные автоматизированные системы и интеграция. Данные по управлению промышленным производством. Часть 1. Общий обзор»

ИСО 18629-1:2004

в

ИСО 18629-11:2005

в

ИСО 18629-12:2005

в

* Соответствующий национальный стандарт отсутствует (в разработке). До его утверждения рекомендуется использовать перевод на русский язык данного международного стандарта. Перевод данного международного стандарта находится в Федеральном информационном фонде технических регламентов и стандартов.

Примечание — В настоящей таблице ислогъэовано следующее условное обоэначемю стелем* соответствия стандартов:

- ЮТ — идентичные стандарты.

Библиография

[11 ИС010303-49

[2] ИС018629-14 [31 ИС018629-44


Системы промышленной автоматизации и интеграция. Представление данных о продукции и обмен данными. Часть 49. Интегрированные групповые ресурсы: структура и свойства процесса

Системы промышленной автоматизации и интеграция. Язык спецификаций процесса. Часть 14. Теории ресурсов

Системы промышленной автоматизации и интеграция. Язык спецификаций процесса. Часть 44. Дефиниционагъное расширение: расширение ресурсов

УДК 65.011:56.681.3    ОКС 25.040.40

Ключевые слова: автоматизированные промышленные системы, интеграция, жизненный цикл систем, управление производством

Редактор А Д Уайса Техничеоом редактор В. Н. Прусакова Корректор Л. Я. Митрофанова Комгъютерная верстка 7! Ф. Кузнецовой

Сдано a


набор 28.01.2014. Пщпясаио • печать 01.04.2014. Формат 60 x 84'.',    Бумага офсетная. Гарнитура Ар мал

Печать офсетная Уел. печ. а. 6.37. Уч -язя. л. 6.70. Тираж 69 эм Эак. 185

ФГУП «СТАНДЛРТИМФОРМ*. 123995 Москжа. Гранатный лер.. 4. wvrw.gostrrfo iu    info<ggostin(om

Набрано я отпечатано а Калужской типографии стандартов. 248021 Калуга, уя Московская. 256