Сплав - Иррефлексивность

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

module test

abstract sig MySig {    
  my_rel : set MySig
}

//fact my_rel_irrefl {no iden & my_rel }   // this works
fact my_rel_irrelfl {my_rel not in iden} // this does not work

run {}

Почему второй my_rel_irrelfl не работает? Я думал, что, например.

MySig = {N0,N1,N2} идентификатор = {(N0,N0),(N1,N1),(N2,N2)}

Если есть элемент (x,x), где x в MySig в отношении my_rel, то он также должен быть в ident.

Тем не менее, я получаю эту модель:

модель найдена сплавом

т.е. тот, где my_rel является рефлексивным.


alloy
person KamalaKhan    schedule 08.01.2021    source источник
comment
Совет: вместо того, чтобы делать оба факта, сделайте их предикатами и выполните check {pred1 <=> pred2}. Это даст вам контрпример, где одно верно, а другое нет.   -  person Hovercouch    schedule 08.01.2021

Ответы (1)


arrow_upward
0
arrow_downward

my_rel not in iden говорит, что my_rel не является подмножеством iden. Поскольку N0 -> N1 in my_rel и N0 -> N1 not in iden, my_rel не является подмножеством, и этот факт остается в силе.

person Hovercouch    schedule 08.01.2021
comment
Спасибо, это было глупо с моей стороны, я должен знать основы теории множеств ^^ - person KamalaKhan; 08.01.2021