Как повторно использовать факты с помощью модулей в Alloy

В моем предыдущем ответе я пытался обратиться к вашему пункту «аналогично между разными подписями», то есть я думал, что ваша главная цель состояла в том, чтобы иметь модуль, который каким-то образом обеспечивает наличие поля с именем isA в сигнале, связанном с параметром Q, и что isA одновременно инъективен и сюръективен. Теперь я понимаю, что вам, вероятно, нужны повторно используемые предикаты, которые утверждают, что данное бинарное отношение является инъективным/суъективным; этого вы можете достичь в Alloy:

библиотека/copy.als

module copy [Domain, Range]

pred inj[rel: Domain -> Range] {
  all c1,c2: Domain | c1.rel=c2.rel => c1=c2   // injective mapping
}

pred surj[rel: Domain -> Range] {
  all a1: Range | some c1: Domain | c1.rel=a1   //surjective 
}

семья.als

open copy[QP, Person] 
sig Person {} 
sig QP{isA:Person}

fact {
  inj[isA]
  surj[isA]
}

run {} for 4

Фактически, вы можете открыть встроенный модуль util/relation и использовать предикаты injective и sujective для достижения того же результата, например:

семья.als

open util/relation
sig Person {} 
sig QP{isA:Person}

fact {
  injective[isA, Person]
  surjective[isA, Person]
}

run {} for 4

Вы можете открыть файл util/relation (File -> Open Sample Models) и увидеть другой способ реализации этих двух предикатов. Затем вы даже можете проверить, что ваш способ утверждения инъективного/сюръективного эквивалентен встроенному способу:

open copy[QP, Person]
open util/relation

sig Person {} 
sig QP{isA:Person}

check {
  inj[isA] <=> injective[isA, Person]
  surj[isA] <=> surjective[isA, Person]
} for 4 expect 0 // no counterexample is expected to be found

Модули в Alloy рассматриваются как независимые единицы (т. е. модуль может получить доступ только к материалам, определенным в самом этом модуле, и к модулям, явно открытым в этом модуле), поэтому при компиляции модуля «копирования» isA действительно не определено. Теоретически можно было бы дополнительно параметризовать модуль "копировать" отношением isA, но в Alloy параметры модуля могут быть только сигами.

Возможным решением вашей проблемы было бы определение абстрактных знаков A и Q в модуле «копия», а затем в других модулях определение конкретных знаков, которые расширяют A и Q, например,

copy.als:

module library/copy

abstract sig A {}
abstract sig Q {isA: one A}

fact {
   all c1,c2:Q | c1.isA=c2.isA  => c1=c2   // injective mapping
   all a1:A | some c1:Q | c1.isA=a1   //surjective 
}

family.als:

open library/copy 

sig Person extends A {} 
sig QP extends Q {} {
  this.@isA in Person // restrict the content of isA to Person
}

run {} for 4

Использование наследования для достижения такого повторного использования кода концептуально не идеально, но на практике часто бывает достаточно хорошо, и я не могу придумать другого способа сделать это в Alloy.