Комплексное определение для информационного моделирования (IDEF1X), страница 44

   (для всех *) (если (v:e2): J имеет n2: I1, (v:e2): J имеет n2: I2 тогда I1=I2)

к теории.

С1.5. Если отношение является обязательным, ограничьте потомка в имении родителей, добавив правило

   (для всех *) ( если существует (v: e2): J

                           тогда (для некоторых I) ((v: e2): J имеет n2: I))

к теории.

С1.6. Если отношение является положительным (P) или единичным (1), ограничьте родителей в обладании потомками, добавив правило

   (для всех *) (если существует (v: e1): I

                           тогда (для некоторых J) ((v:e1) I имеет n1:J)).

к теории.

С1.7. Если отношение нулевое/единичное (Z) или единичное (1), ограничьте родителей иметь не более, чем одного потомка, добавив правило

   (для всех *) (если (v: e1): I имеет n1: J1, (v: e1):I имеет n1: J2 тогда J1=J2)

к теории.

С1.8. Если отношение – определенное положительное число n, где n не 1, ограничьте родителя иметь точно n экземпляров потомков, добавив правило

   (для всех I) (если существует (v: e1): I

                           тогда (для некоторых L)

                                      (список(L),

                                      (для всех J) (представитель (L,J) если (v: e1): I имеет n1: J),

                                      без повторов(L),

                                      считать(L, n)))

к теории.

С1.9 Если отношение имеет ранг от n до m включительно, кроме 0 и 1, добавьте правило

   (для всех I) (если существует (v: e1): I

                           тогда (для некоторых L)

                                      (список(L),

                                      (для всех J) (представитель (L, J) если (v: e1): I имеет n1: J),

                                      без повторов(L),

                                      считать(L, N),

   n 2 N, N 2 m ) ) )

к теории.

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

Пример

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

   (для всех *)

               (если производство_деталь_входит_компонент_структурная_часть (I, J)

               тогда   существует (производство: деталь): I,

                           существует (производство: компонент детали): J).

   Участник представления сущности ((производство: деталь): «входит»).

   Участник представления сущности ((производство: структурная часть): компонент).

               (для всех *) ((производство: деталь): I имеет «входит»: J, если определено

                           производство_деталь_входит_компонент_структурная_часть (I, J)).

               (для всех *) ((производство: структурная часть): I имеет компонент: J,

если определено

                           производство_деталь_входит_компонент_структурная_часть (I, J)).

               (для всех *)

(если      (производство: структурная часть): J имеет компонент: I1,

   (производство: структурная часть): J имеет компонент: I2,

тогда I1 = I2).

               (для всех *)

                           (если существует (производство: структурная часть): J

                           тогда (для некоторых I)

                                      ((производство: структурная часть): J имеет компонент: I)).

Б.4.2.6.Неиднтифицирующие связи

Неидентифицирующие связи формализуются как идентифицирующие, со следующими изменениями:

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

Пропустите правила С1.4 и С1.5.

Примените правила С1.6, С1.7, С1.8, и С1.9 в обоих направлениях.

Б.4.2.7. Отношение категоризации

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

К1. Для каждого представления, v, в множестве представлений и для каждой родовой сущности, е, в представлении, v, где е имеет кластер категории, состоящий из сущностей е1, е2, …, en, сделайте следующее.

К1.1 Для 1≤i≤n сделайте следующее.

К1.1.1 Объявите отношение категории, добавив правило

   v: ei является v: e

к теории.

К1.1.2. Ограничьте каждый экземпляр категории  быть экземпляром рода, добавив правило

(для всех * ) (если существует ( v: ei ): I тогда существует ( v: e ): I )

к теории.

К1.2. Категории внутри кластера взаимоисключающие. Для 1.i < j.n, добавьте правило

(для всех * ) (не (существует ( v: ei ): I, существует ( v: ej ): I ) )

к теории.

К1.3. Если категоризация является полной, обеспечьте экземпляр категории для каждого родового экземпляра, добавив правило

(для всех * )

(если существует ( v: e ): I

тогда существует ( v: e1 ): I или существует ( v: e2 ): I ... или существует ( v: en ): I )

к теории.

К1.4. Если дискриминатор, d, определен для кластера, значение дискриминатора должно быть 1:1 для категории внутри кластера.

К1.4.1. Обеспечьте, чтобы каждый экземпляр категории имел значение дискриминатора и чтобы каждый экземпляр данной категории имеет то же значение дискриминатора, путем добавления правила

(для всех *)

(если      представитель([e1, e2, ..., en ], E ),

существует (v: E): I1,

существует (v: E): I2

тогда (для некоторых D )

(( v: e): I1 имеет d: D,

(v: e): I2 имеет d: D ) )

к теории. Заметьте, что К1.3 и К1.4.1 реализуют то, что дискриминатор для полной категоризации должен иметь значение для каждого экземпляра рода.

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

(для всех *)

(если      ( v: e ): I1 имеет d: D,

( v: e ): I2 имеет d: D,

представитель( [ e1, e2, ..., en ], E ),

существует ( v: E ): I1

тогда     существует ( v: E ): I2 )

к теории.

Заметьте, что аксиомы К1.4.1 and К1.4.2 не препятствуют неполной категоризации, в которой род имеет значение дискриминатора, а не категории до тех пор, пока ни один род с дискриминатором не имеет категорию.