У меня есть следующая простая модель:
sig a{}
sig b{ x:set a}
run { } for 1 expect 1
когда я выполняю предикат в Alloy 4.2 и использую оценщик, я получаю следующие значения:
instance # 1
this/a={}, this/b={}, this/b<:x={}
оценщик:
x in (b lone ->some a) : true
((b-b) -> a) in x : true
((b-b) -> a) in (b lone ->some a) : true
экземпляры # 2
this/a={}, this/b={b$0}, this/b<:x={}
оценщик:
x in (b lone ->some a) : false
((b-b) -> a) in x : true
((b-b) -> a) in (b lone ->some a) : false
экземпляры # 3
this/a={a$0}, this/b={b$0}, this/b<:x={}
оценщик:
x in (b lone ->some a) : false
((b-b) -> a) in x : true
((b-b) -> a) in (b lone ->some a) : false
экземпляры # 4
this/a={a$0}, this/b={}, this/b<:x={}
оценщик:
x in (b lone ->some a) : true
((b-b) -> a) in x : true
((b-b) -> a) in (b lone ->some a) : true
экземпляры # 5
this/a={a$0}, this/b={b$0}, this/b<:x={b$0->a$0}
оценщик:
x in (b lone ->some a) : true
((b-b) -> a) in x : true
((b-b) -> a) in (b lone ->some a) : false
x in (b lone -> some a) не имеет смысла для меня в случаях # 2,3, поскольку пустое отношение является подмножеством любого отношения.
((bb ) -> a) в (b lone -> some a) не имеет смысла для меня в случаях # 2,3,5 по той же причине, что и предыдущая.
Есть ли логическое объяснение этим значениям или что-то не так с Alloy?