연산을 병렬화하기
결정 다이어그램의 연산을 작은 작업으로 나누어 여러 스레드가 처리하도록 구성한다. Sylvan은 Lace 실행 기반을 사용하므로 라이브러리 호출 전에 해당 환경이 실행 중이어야 한다. 여러 코어가 있다는 사실만으로 모든 입력에서 같은 속도 향상이 보장되지는 않는다.
말단값을 확장하기
불리언 함수뿐 아니라 불리언 입력에서 정수나 실수로 이어지는 함수도 표현할 수 있다. 사용자 정의 타입을 말단에서 다루는 방식도 제공한다. 다중 방향 분기의 list decision diagram 연산 역시 별도 표현으로 포함한다.
활용과 지원 구분
예제에는 도달 가능한 상태 계산과 다이어그램 형식 변환 등이 있다. 언어 바인딩은 구현 및 유지 상태가 서로 다를 수 있다. 특정 다이어그램 계열이 별도 브랜치에 있는 경우도 있으므로 사용하는 버전의 실제 지원 범위를 확인한다.
관련 문서
CUDD / NuSMV / Storm 확률 모델 검사기 / Pono