합금의 두 표현식의 차이점은 무엇입니까?

Question

한다고 가정 우리는 다음과 같은 합금 모델이 있습니다

내가 사라 년생 어떤 신입생와 호환되지 않을해야한다는 것을 말하고 싶은

abstract sig Season {} 
one sig Spring, Summer, Fall, Winter extends Season {} 

abstract sig Student { 
    bornIn: one Season 
} 

abstract sig Freshman, Sophomore extends Student {} 
one sig John, Walter extends Freshman {} 
one sig Sarah extends Sophomore {} 

pred isCompatibleWith(s1, s2: Student) { 
    s1.bornIn = s2.bornIn 
} 

.

fact { 
    not Sarah.isCompatibleWith[Freshman] 
} 

합금이 내 구문에 만족합니다.

assert WhyDoesThisNotHold { 
not Sarah.isCompatibleWith[John] 
} 

그러나 합금 카운터 - 예를 발견 : 나는 주장을 추가 사라와 존은 모두 여름에 태어난다!

fact { 
    no f: Freshman | Sarah.isCompatibleWith[f] 
} 

무엇 두 구문의 차이가, 그리고 내가 의도 한대로 왜 첫 번째가 작동하지 않습니다 :이에 fact을 변경할 때 반면

, 합금 카운터 - 예를 찾을 수 있습니까? (이 유효 합금 구문이기 때문에 그리고, 무엇 실제로 말입니까?)이 예상대로 당신은 그러나이 술어에 의미하지 않는다, 매개 변수로 모든 Freshman 세트와 술어 isCompatibleWith를 호출하기 때문에

Answer 1

은 첫 번째 사실은 작동하지 않습니다 두 세트의 학생들 사이의 호환성을 확인하십시오. (이 교차 연산자 &하여 = 기호를 교체하고 결과 세트가 비어 있는지 확인하여이 될 수 있습니다.

지금 존과 사라를 방지하지 않습니다이 사실이 호환되도록하는 방법을 보여줍니다. 가정이 사라 그리고 John은 Winter의 Summer and Walter에서 태어났습니다. 그 이유는 다음과 같습니다.

not Sarah.isCompatibleWith[Freshman] = not Sarah.isCompatibleWith[Walter+John] 
             = not Sarah.bornIn=(Walter+John).bornIn 
             = not Summer = (Summer+Winter) 
             = not false 
             = true