4

私は 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 ステートメントを試してみましたが、明らかに、最初に単純なケースで機能させたいと考えています。任意の洞察をいただければ幸いです。ありがとう！

4

1 に答える 1

3

SPIN 検証を実行すると、印刷出力はありません。エラーが見つかったかどうか (およびその他のパフォーマンス情報) を示すだけです。あなたは初心者なので、'spin -a …' で spin を呼び出すときに 'run a SPIN validation' を行い、コンパイルされたコードを実行することに注意してください。

出力を表示するには 2 つの方法があります。まず、 を使用してシミュレーション モードで 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

于 2014-03-08T15:48:04.447 に答える