1
nusmv에서 실행되는 사양 중에 몇 시간이 걸리며 결과적으로 "kill 9"가 반환됩니다. 실행 속도를 높이려면 어떻게해야합니까? 사양 실행 중에 NuSMV가 사용할 수있는 메모리 양을 늘릴 수있는 옵션이 있습니까?사양 실행 중에 NuSMV가 사용할 수있는 메모리 양을 늘릴 수있는 옵션이 있습니까?
A
답변
2
NuSMV의 후속 버전 인 nuXmv https://es-static.fbk.eu/tools/nuxmv/을 사용할 수 있습니다. BDD 기반 메모리보다 적은 메모리를 사용하는 새로운 SAT 기반 모델 검사 알고리즘을 제공하며 NuSMV와 동일한 모델 사양을 허용합니다.
전반적으로 NuSMV가 메모리가 부족한 이유에 따라 다릅니다. 대부분의 경우 모델을 빌드 할 수 없으므로 모델 크기를 줄여야합니다. 이를 위해 일부 상태 변수가 상태가없는 부울 신호가 될지 또는 일부 변수의 범위를 줄이는 지 여부를 알아볼 수 있습니다.
매개 변수 모델이있는 경우 (예 : 가변 개수의 모듈이 사용되거나 일부 변수의 비트 폭이 변경 될 수있는 경우) 간단한 변형을 실행하고 어떤 부분이 메모리 수요가 증가합니다. 이 부분은 다른 방식으로 모델링되어야합니다.
귀하의 요구에 맞지 않을 수도 있지만 귀하의 웹 사이트에서 [FAQ # 003] (http://nusmv.fbk.eu/faq.html#003)을 보셨습니까? –