ГОСТ Р ИСО 18629-14—2011
П р и м е ч а н и е — Примитивный символ функции agg_demand содержит элемент операции в виде аргу
мента. Поскольку элементы операции обладают уникальными временными точками начала beglnof и конца endof,
временные ограничения на характеристики ресурсов могут выражаться с помощью временного интервала, в кото
ром соответствующая операция имеет место.
6.6.5 Определяющий символ отношения resource
KIF-формат обозначения определяющего символа отношения resource таков:
(resource ?г).
Неформальная семантика для примитивного символа отношения resource такова.
(resource ?г) в интерпретации теории потребности в ресурсах принимает значение TRUE тогда и
только тогда, когда существует операция, которая требует ресурса ?г.
6.7 Определения теории потребности в ресурсах
6.7.1 Определение 1:
Ресурс — это любой объект, который требуется каким-либо элементом операции.
(forall (?r) (iff (resource ?r)
(and (object ?r)
(exists (?a)
(res_requlres ?a ?r))>)
6.8 Аксиомы теории потребности в ресурсах
6.8.1 Аксиома 1
Ресурс для операции доступен в том случае, когда доступный объем ресурса для этой операции
превышает разность между объемом позиции спроса и суммой совокупного спроса на него испроса для
данной операции на него же.
(foraII (?а ?af ?r ?s)
(implies (and (res_requires ?a ?r)
(subactivity ?al ?a)
(atomic ?a1))
(iff (and (greater (resource_polnt ?r ?s)
(agg_demand ?r ?s))
(greater (agg_demand ?r ?s) zero_quantity))
(exists (?occ ?occ
1
)
(and(occurrence ?occ ?a)
(occurrence ?occ1 ?a1>
(subactlvity_occurrence ?occ1 ?occ»))))
6.8.2 Аксиома 2
Символ отношения res_requires необходим для неделимой операции тогда и только тогда, когда
спрос на ресурс ненулевой.
(foraII (?r ?а ?s)
(implies (and (atomic ?a>
(occurrence ?s ?a))
(iff (res_requires ?a ?r)
(not {= (demand ?r ?sj zero_quantity)))))
6.8.3 Аксиома 3
Запрос одновременно действующих операций на ресурс является суммой запросов всех субопе
раций на этот ресурс.
(foraII (?a1 а2 ?r ?s)
(= (demand (?r (successor (cone ?а1 ?а2) ?s)j
(quantity_plus (demand ?r (successor ?a1 ?s>) (demand ?r (successor ?a2 ?s)))))
6.8.4 Аксиома 4
Совокупный запрос на ресурсы является суммой запросов от всех операций, которые в них нужда
ются.
(foraII (?а ?r ?s)
(= (agg_demand ?r (successor ?a ?s))
(quantity_plus (agg_demand ?r ?s) (demand ?r (successor ?a1 ?s))))}
6