제약으로 구조를 설명하기
모델은 가능한 구조의 집합을 직접 열거하기보다 제약의 모음으로 설명한다. 시간에 따라 변하는 구조도 다루며 설계가 허용하는 형태를 탐색할 수 있다.
사례와 반례의 생성
Analyzer는 모델의 제약을 만족하는 구조를 찾는다. 이를 통해 가능한 예를 보며 설계를 이해하거나 검사하려는 속성이 깨지는 반례를 살펴볼 수 있다.
관계 중심의 표현
언어의 중심에는 관계를 기반으로 한 논리가 있다. 점진적으로 모델을 구성하고 객체나 구조 사이의 연결을 표현하도록 설계됐다.
시각적인 탐색과 변화
찾은 구조는 그래프로 표시하고 영역에 맞게 모습을 조정할 수 있다. Alloy 6에서는 변할 수 있는 상태와 시간 논리 및 관련 풀이 기능을 더해 시스템 동작의 표현을 넓혔다.