저는 Promela와 SPIN을 사용하려는 초보자입니다. 간단한 Promela 사양을 개발할 때 printf ()를 사용하여 프로그램의 변수 값을 확인하고 싶습니다. 이 매뉴얼 페이지를 읽고 간단한 hello world 프로그램을 실행하려고하는데 출력 텍스트가 표시되지 않습니다. 다음은 샘플 hello world 파일입니다.
init {
printf("MSC: passed first test!\n")
}
컴파일하고 실행하는 데 사용하는 단계는 다음과 같습니다.
spin -a hello.pml
cc -o run pan.c
./run
실행 결과는 다음과 같습니다.
hint: this search is more efficient if pan.c is compiled -DSAFETY
(Spin Version 4.2.6 -- 27 October 2005)
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
acceptance cycles - (not selected)
invalid end states +
State-vector 12 byte, depth reached 2, errors: 0
3 states, stored
0 states, matched
3 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
4.879 memory usage (Mbyte)
unreached in proctype :init:
(0 of 2 states)
그렇다면 printf 문에서 내 출력을 어디에서 찾을 수 있습니까? 더 복잡한 promela 파일에서도 printf 문을 시도했지만 분명히 간단한 경우 먼저 작동하도록하고 싶습니다. 모든 통찰력을 주시면 감사하겠습니다. 감사!
SPIN 확인을 실행할 때 인쇄 된 출력이 없습니다. 오류가 발견되었는지 여부 (및 기타 성능 정보) 만 표시됩니다. 초보자이기 때문에 'spin -a…'를 사용하여 spin을 호출 할 때 'SPIN 확인을 실행'한 다음 컴파일 된 코드를 실행합니다.
출력을 보는 방법에는 두 가지가 있습니다. 먼저를 사용하여 시뮬레이션 모드에서 SPIN을 사용 spin hello.pml합니다. 예를 들면 :
$ cat >hello.pml <<EOF
> init { printf ("hello world\n"); }
> EOF
$ spin hello.pml
hello world
1 process created
둘째, 확인 모드에서 SPIN을 사용하되 프로그램에 오류를 삽입합니다. 오류가 발생한 후 추적 파일을 검사하십시오. 예를 들면 :
$ cat >hello.pml <<EOF
> init { printf ("hello world\n"); assert (0); }
> EOF
$ spin -a hello.pml
$ gcc -o hello pan.c
$ ./hello
hint: this search is more efficient if pan.c is compiled -DSAFETY
pan:1: assertion violated 0 (at depth 0)
pan: wrote hello.pml.trail
...
State-vector 12 byte, depth reached 0, errors: 1
...
pan: elapsed time 0 seconds
$ spin -p -t hello.pml
using statement merging
hello world
1: proc 0 (:init:) hello.pml:1 (state 1) [printf('hello world\\n')]
spin: hello.pml:1, Error: assertion violated
spin: text of failed assertion: assert(0)
1: proc 0 (:init:) hello.pml:1 (state 2) [assert(0)]
spin: trail ends after 1 steps
#processes: 1
1: proc 0 (:init:) hello.pml:1 (state 3) <valid end state>
1 process created
위의 'hello world'는 이후에 찾을 수 있습니다. spin -p -t hello.pml
이 기사는 인터넷에서 수집됩니다. 재 인쇄 할 때 출처를 알려주십시오.
침해가 발생한 경우 연락 주시기 바랍니다[email protected] 삭제
몇 마디 만하겠습니다