술어 비교

Question

포스터에 합금 기능을 비교하는 방법이 나와 있습니다. 작은 예제 (함수 대신 술어 비교)를 사용하여 질문에 답하는 동안, 나는 다음과 같은 행동을 발견했다.

분석기는 check 명령의 경계가 3보다 크고 사실 'f1'이 활성화 될 때마다 반례를 발견하지 못합니다. 분석기는 예상대로 작동하지 않습니다. 중복 된 사실 'f1'이 분석기의 동작을 왜 수정하고 왜 경계가 3보다 큰지는 왜입니까?

open util/ordering [V] 
sig V {} 

fact f1 { 
    # V > 0 
} 

pred p1 [x: V] { 
    x = last 
} 

pred p2 [x: V] { 
    x = first 
} 

assert a1 { 
    all x: V | p1[x] <=> p2[x] 
} 

check a1 for 3 

체크 경계가 4 이상 및 'F1'때마다 분석 보고서 '0 바르 활성화되어있는 것으로 보인다. 0 기본 vars. 0 개의 조항들. '

Answer 1

세부 사항을 살펴볼 수없는 순간이지만 합금의 정수가 매우 좁습니다 (기본적으로 4 비트라고 생각합니다). 부분적으로는 오버플로 동작이 나타나는 것 같습니다. 2를 정수로 보완하므로 오버플로가 정기적으로 발생합니다.

몇 가지 변경 사항은 설명이 개별적으로 또는 함께있어 동작에 영향을 미치는지 확인할 수 있습니다.

• 다른 서명을합니다 (scope 명령을 사용하여 인터넷 용 명시적인 비트 폭을 제공하는 "오버플 금지"옵션 some V
• 차례 사실 F1 교체는 범위 번호 인스턴스의 최대 개수를 지정 ;에 대한 지능이 지정하는 비트 폭)
루이 Gammaitoni 여기에 또 다른 질문에 넣어함에 따라

"합금의 숫자와 함께 연주 할 때 당신은 항상 조심해야한다."