모델의 정수

Question

의 유한 집합 다음은 정수의 집합을 나타내는 합금 모델입니다. 0을 2에 어떻게 통합시킬 수 있습니까? 0 및 2은 (는) 세트가 아닙니다. 나는 조합 운영자가 세트에만 적용되는 줄 알았습니까? 이것이 조합의 기본 개념을 위반하지 않습니까?

두 번째 질문 :이 모델을 만드는 더 좋은 방법이 있습니까?인지 적으로 덜 거슬리는 것입니까?

one sig List { 
    numbers: set Int 
} { 
    numbers = 0 + 2 + 4 + 6 
} 

Answer 1

합금에서 작업하는 모든 것은 튜플 세트입니다. none은 빈 세트이며, 많은 세트가 릴레이션 세트 (arity가 1보다 큰 튜플)입니다. 또한 각 정수는 여러분이 그것을 사용할 때, 1과 릴레이션 1의 관계를 가진 집합입니다. 당신이 1을 사용할 때 그것은 원자 1을 포함하는 타입의 집합 인 정말로 {(1)}입니다. 정의처럼 현실입니다 : 합금에

 enum Int {-8,-7,-6,-5,-4,-3,-2,-1,0,1,2,3,4,5,6,7} 

의 int 원자의 유한 집합이 문제는 일반적으로하지 않습니다 :-(다만 아주 좋지 않다 정수가 있지만 INTS으로 정말 유용 할 그들 중 아주 소수가 있습니다 . 더 나쁜, 그들은 신속하게 오버 플로우 및 합금은이 모든 것을 취급 좋지 않다.

하지만 그것은 추한 보인다. 내가 서열과 더 나쁜 문제가 동의.

 0-A + 1->B + 2->C + 3->C 

이미 추가 실험 literal seq를 Alloy로 가져가 실험 버전을 실행 중입니다.

 // does not work in Alloy 4 
    seq [ A, B, C, C ] = 0->A + 1->B + 2->C + 3->C 
    set [ 1, 2, 3, 3 ] = 1+2+3 

오늘이 작업을 수행 할 수 있습니다 : 수 세트는이 방법으로 구현 될 수

let x[a , b ] = { a + b } 

run { 
    x[1,x[2,x[3,4]]] = 1+2+3+4 
} for 4 int 

을하지만하지 않도록 내가 더 나은이를 좋아한다. 매크로는 메타 필드 것 또는 시퀀스 (대부분의 통역을 가지고있는 것처럼)과 인수를 사용할 수 있도록 할 경우, 우리는 seq [ A, B, C, C ] 구문이 마음이

// does not work in Alloy 4 
let list[ args ... ] = Int.args // args = seq univ 
run { 
    range[ list[1,2,3,4,4] ] = 1+2+3+4 
} 

을 할 수 또는 변수 인수는 다음 AlloyTools 목록에 스레드를 시작 . 말씀 드린대로 seq [ A, B, C, C ]이 프로토 타입으로 작동합니다.