나머지 유형의 합금 구문은 무엇입니까?

Question

합집합에서 모든 하위 유형을 명시 적으로 뺄 필요없이, Alloy에서 나머지 유형을 직접 나타낼 수 있습니까? 예를 들어,에 :

sig Test {} 
one sig A, B extends Test {}  

나는 새로운 SIG에 의해 확장됩니다 때마다 Test을 변경할 필요가 없습니다 속기를 통해 표현 Test-(A+B)를 참조 할 수 있도록하고 싶습니다. 이것은 구문 설탕 일 뿐이지 만 모델을 리팩터링 할 때 실수를 피할 수 있습니다.

Answer 1

다음과 같이 나머지를 나타내는 세트를 소개 할 수있다. 나중에 Test을 one sig C을 추가하여 확장하려는 경우, 예를 들어 Remainder은 나머지 세트를 제공합니다.

Answer 2

저는 잠시 동안 합금을 사용하지 않았지만 원하는 방식으로 가능하지 않다고 생각합니다. 그러나 모델에서 하나의 위치 만 조합을 리팩터링 할 수 있습니다. 예 :

sig Test {} 
one sig A, B extends Test {} 

fun Remainder : set Test { 
    Test - (A+B) 
} 

run { some Remainder } for 5 

당신은이 기본 유형에서 모든 하위 유형의 조합을 빼서 정의, 여기 Remainder라는 기능을 사용하여 관계를 정의합니다.
모델에 새로운 하위 유형을 추가 할 때마다 Remainder의 정의에 추가해야한다는 것을 잊지 마세요.

모델 전반에 걸쳐, 당신은 단지 내가 run 명령에 익명의 조건에서 사용되는 것처럼, 모든 순수Test 원자를 얻기 위해 Remainder를 참조 할 수 있습니다.

abstract sig Test {} 
sig Remainder extends Test {} 
one sig A, B extends Test {} 

이것은 Remainder가 Test - (A + B)에 해당되는으로, 세 개의 하위 집합으로 Test 원자의 집합을 분할합니다 :

Answer 3

당신은 정의가 Test가 도입 연장하는 새로운 시그마, 당신이 사용할 수있는 어떤 유지하려면 합금의 작은 당신이 특별한 세트 sig$을 통해 시그마을 반복 할 수 있도록하는, meta capabilities 알려진. 돌이켜에

fun Remainder [] : set Test { 
    {t : Test | all sig : sig$ | sig = Test$ || t not in sig.value} 
}