Когда я выполняю следующий пример с использованием Alloy, v4.2 или v5, я получаю экземпляр, который дважды появляется в пространстве решения.
sig A {}
sig B extends A { }
pred P { }
run P for 2
Сгенерированные экземпляры:
1:A={}, B={}
2:A={A$0}, B={}
3:A={B$0}, B={B$0}
4:A={A$0, B$0}, B={B$0}
5:A={A$0, A$1}, B={}
6:A={A$0, B$0}, B={B$0} // same as instance 4
7:A={B$0, B$1}, B={B$0, B$1}
Есть предложения?