결정 구조를 라이브러리로 다루기
결정 다이어그램은 조건에 따른 분기를 그래프로 표현하는 자료구조다. CUDD는 이런 구조를 만들고 조작하는 기능을 제공한다. 그래프를 이용하는 상위 분석 알고리즘은 별도로 구성해야 하므로 라이브러리 자체를 완성된 프로그램 검증기로 이해하면 안 된다.
다른 다이어그램 계열
BDD와 ADD, ZDD는 표현하는 대상과 구조의 사용 목적이 다르다. 한 종류의 다이어그램을 사용하는 코드가 다른 종류에도 그대로 적용되는 것은 아니다. 계산하려는 연산과 자료 표현에 맞는 API 및 관리 규칙을 확인해야 한다.
배포 구성과 점검
기본 라이브러리 외에 저장 관련 dddmp 라이브러리와 객체 지향 래퍼가 포함된다. 정적 또는 공유 라이브러리와 추가 구성 요소는 빌드 옵션에 따라 달라진다. 배포 예제 nanotrav는 설치 상태를 확인하기 위한 단순한 상태 기계 순회 프로그램이다.
관련 문서
Sylvan / Yices / NuSMV / Storm 확률 모델 검사기