PROMELA에서 사용하는 메모리를 제한하는 방법은 무엇입니까?

PROMELA에서 사용하는 최대 메모리를 -DMEMLIMIT 플래그를 사용하여 제한하려고합니다.PROMELA에서 사용하는 메모리를 제한하는 방법은 무엇입니까?

./spin -a -DMEMLIMIT=1024 code.pml

그러나 여전히 메모리는 계속 증가하고 있습니다. 어떤 생각이야, 왜 그렇게 생각하니?

'-DMEMLIMIT = 1024' 플래그는 프로그램에 전달하는 것이 아니라 컴파일러 플래그처럼 보입니다. 이 _spin_ 프로그램에 대한 문서가 있습니까? – tangrs

실제로 SPIN은 모델 검사를 위해 C 코드를 생성합니다. 그 C 코드는 MEMLIMIT 플래그를 포함하는데, 그 목적은 메모리 사용을 제한하는 것입니다. 그러나 내가보고있는 것으로부터, 기억은 제한적이지 않습니다. – MetallicPriest

_spin_의 설명서를보고 있는데 '-D' 플래그에 대한 언급이 없습니다. 아마도'-DMEMLIMIT = 1024' 플래그로 생성 된 C 파일/s을 컴파일하려고 했었 을까? – tangrs

-DMEMLIM = N은 gcc로 전달되는 컴파일러 플래그입니다. 그것은 그런 식으로 작동합니다

./spin -a code.pml GCC -DMEMLIM = 1024 -o 팬 pan.c ./pan

또한 국가의 더 나은 압축을 적용 할 더 플래그를 추가 할 수 있습니다

예를 들어 -DCOLLAPSE는 필요한 메모리 양을 줄이는 아주 빠른 방법입니다.

2014-01-30 07:39:12 rindPHI

또한 'pan'에 대한'-w' 옵션 : "-wN 2 진 항목의 해시 테이블 (기본값은 -w24)". –

답변