SPIN 모델 검사기에서 최대 검색 깊이를 너무 작게 해결하는 방법은 무엇입니까? 가능한 이유는 무엇입니까?

Question

내 모델 검증을하는 동안 나는이 오류를 얻고있다

는 컴파일 문자열 tesTdma.pml

-a

스핀

최대 검색 깊이가 너무 작고, 깊이 = 9999 주

I입니다 이 오류의 원인을 이해하지 못합니다. 나요 누군가가 1.1.4과 SPIN 버전이 사용 ISPIN 건너 온 6.4.7

Answer 1

검색 깊이 경계 된 것으로 나타나고 생성 된 검증 pan에 적절한 옵션을 전달하여 구속을 증가해야합니다

-b

경계 탐색 모드는 트리거 오류 흔적, 탐색의 깊이를 초과하면 오류하게

-mN

N 단계 0

세트 최대 검색 깊이 (기본값 N = 10,000)

는 man page of pan, 또한 man page of spin 참조 :

-run

이 pan.c에서 검증 소스 코드를 생성 (예 : -a) 즉시 확인 프로그램을 컴파일하고 실행하십시오. -run 인수에 따라 옵션 -[ODUE] 또는 런타임 플래그 (다른 모든 옵션) 등의 검증에 시작하는 컴파일러 (옵션을 통해 전달됩니다. 옵션은 -run 인수 선행되어야 자체 스핀 할 수 있습니다.

가 -run 옵션은 대신 별도의, spin에 대한 호출을 통해 pan에 옵션을 전달하려는 경우에 유용합니다

또한, 슬라이드 1 these slides에서 27 페이지의 :.

,

SPIN은 심도 바운드가 전체 상태 공간을 검색하지 못하도록하는 “error: max search depth too small”을 표시합니다.