합금

Question

에서 모듈에 의한 사실을 다시 사용하려면 어떻게 합금에 다음과 같은 사양을 가지고 : 내 모델에서

sig A {} 
sig Q{isA: one A} 

fact { 
    all c1,c2:Q | c1.isA=c2.isA => c1=c2 // injective mapping 
    all a1:A | some c1:Q | c1.isA=a1 //surjective 
} 

위의 사실은 다른 서명 사이에 유사하게 반복합니다.

이

module library/copy [A,Q] 

fact { 
    all c1,c2:Q | c1.isA=c2.isA => c1=c2 // injective mapping 
    all a1:A | some c1:Q | c1.isA=a1 //surjective 
} 

그럼 난 벨으로 그것을 사용하려고 :

module family 

open library/copy [Person,QP] 
sig Person {} 
sig QP{isA:Person} 
run {} for 4 

을하지만 합금은 "이름"사 불평 나는 다음과 같이 모듈을 만든 그래서 별도의 모듈로를 고려하려 " 찾을 수 없다." 모듈에.

내 접근 방식에 어떤 문제가 있습니까? 그리고 왜 합금이 불평합니까?

Answer 1

내 이전의 대답에서 "다른 시그니처 사이의 유사점"지점을 처리하려고했습니다. 즉, 귀하의 주된 목표는 매개 변수와 관련된 신호에 isA이라는 필드가 있음을 어떻게 든 강제하는 것입니다. Q이고 그 isA은 모두 주사 적이며 회상 적입니다. 나는 당신이 원했던 것은 재사용 가능한 술어가 주어진다는 것을 깨닫는다. 이것은 주어진 이진 관계가 주사 적/주관적이라고 주장한다. 이 당신이 합금에서 얻을 수 있습니다

module copy [Domain, Range] 

pred inj[rel: Domain -> Range] { 
    all c1,c2: Domain | c1.rel=c2.rel => c1=c2 // injective mapping 
} 

pred surj[rel: Domain -> Range] { 
    all a1: Range | some c1: Domain | c1.rel=a1 //surjective 
} 

family.als

open copy[QP, Person] 
sig Person {} 
sig QP{isA:Person} 

fact { 
    inj[isA] 
    surj[isA] 
} 

run {} for 4 

사실, 당신은 열 수 있습니다

라이브러리/copy.als 내장 util/relation 모듈과 및 sujective 술어를 사용하여 동일한 결과를 얻으십시오 (예 :

).

패밀리.루게릭 병

open util/relation 
sig Person {} 
sig QP{isA:Person} 

fact { 
    injective[isA, Person] 
    surjective[isA, Person] 
} 

run {} for 4 

당신은 util/relation 파일 (File -> Open Sample Models)를 열고이 두 가지 조건을 구현하는 다른 방법을 볼 수 있습니다. 그런 다음도 단사/surjective 주장의 당신의 방법은 내장 방식에 해당 것을 확인할 수 있습니다

open copy[QP, Person] 
open util/relation 

sig Person {} 
sig QP{isA:Person} 

check { 
    inj[isA] <=> injective[isA, Person] 
    surj[isA] <=> surjective[isA, Person] 
} for 4 expect 0 // no counterexample is expected to be found 

Answer 2

합금의 모듈은 독립적 인 단위로 취급됩니다. 즉, 모듈은 모듈 자체에 정의 된 항목과 해당 모듈에서 명시 적으로 열리는 모듈에만 액세스 할 수 있습니다. 따라서 "복사"모듈을 컴파일 할 때 isA은 실제로 정의되지 않았습니다. . 이론적 인 해결책은 "복사"모듈을 isA 관계로 추가 매개 변수화하는 것이지만, 합금 모듈 매개 변수는 sigs 일 수 있습니다.

문제에 대한 가능한 해결책은 추상적 인 시그마 A와 "복사"모듈 Q을 정의하는 다음 다른 모듈에 A 및 Q, 예를 들어,

copy.als을 확장 콘크리트 시그마를 정의 할 :

module library/copy 

abstract sig A {} 
abstract sig Q {isA: one A} 

fact { 
    all c1,c2:Q | c1.isA=c2.isA => c1=c2 // injective mapping 
    all a1:A | some c1:Q | c1.isA=a1 //surjective 
} 

family.als :

open library/copy 

sig Person extends A {} 
sig QP extends Q {} { 
    this.@isA in Person // restrict the content of isA to Person 
} 

run {} for 4 

이런 종류의 코드 재사용을 달성하기 위해 상속을 사용하는 것은 개념적으로 이상적이지는 않지만, 실제로는 종종 충분하며, 합금에서 다른 방법을 생각할 수 없습니다.