Alloy vars 사이의 링크. 및 기본 vars. 합금 관계 변수

Question

해결이 완료되었을 때 표시되는 vars. 및 primary vars. 숫자의 의미를 이해할 수없는 것 같습니다. 5.2.1 절의 합금 책은 합금 관계 변수가 각 관계의 튜플과 연관된 부울 변수에 매핑된다는 것을 설명합니다. 그러나 나는이 변수 정의와 GUI에 표시된 변수 수 사이의 일치를 이해하지 못합니다. 예를 들어 다음과 같은 코드는 (필자는 합금 분석기 4.2 빌드 날짜 사용하고 있습니다. : 2012년 9월 25일 동부 서머 타임 15시 54분 일) : 실행될 때 존재가 있지만

이

sig A {} 

pred show {} 
run show for 2 

이

0 vars. 0 primary vars. 0 clauses. 

를 표시 하나의 관계.

6 vars. 2 primary vars. 5 clauses. 

나는 아마 2 개 주 바르가 최대로 설정 A의 두 요소를 대응 이해할 수 있지만 내가 돈 ': 그리고 때이 코드가 실행이 같은

sig A {} 
fact {no A } 
pred show {} 
run show for 2 

변수는 계산이다 열거 된 네 가지 변수가 무엇인지 이해해야합니다.

Answer 1

기본적으로 기본 변수는 선언 된 서명의 인스턴스에 해당하는 변수입니다. 그들의 숫자는 전체 Alloy 우주에서 생성 된 모든 인스턴스를 나타냅니다. 반면에, 총 변수의 수는 일반적으로 더 큽니다. SAT 수식에 인코딩 할 때 주어진 사실을 나타 내기 위해 필요한 변수를 반영하기 때문입니다. (KodKod 기반 솔버의 통계에 대한 자세한 내용은 here을 참조하십시오.)

따라서 두 번째 예에서는 2의 서명 인스턴스 제한으로 인해 기본 변수 수가 3입니다. 예를 들어 다른 서명을 추가하면 기본 변수의 수는 4가됩니다.) 총 변수 수는 수식의 (CNF) 인코딩의 총 변수 수를 반영하며 이는 차례로 특정 사실에 따라 달라집니다 선언했다. 첫 번째 예제에서는 확인할 사항이 없으므로 필요한 변수가 없습니다 (솔버가 아무 것도 내 보내지 않아도 됨).