SPIN

Menu

---

使い方

    singularity shell --shell /bin/zsh /mnt/nvme0/singularity/teachers/kono/spin/spin.sif
    % ls Examples 
    Book_1991/        a.out*          eratosthenes.pml  for_example.pml         leader_trace.pml  pan.c  pathfinder.pml  snoopy.pml      wordcount.pml
    Exercises/        abp.pml         ex_1f.pml.trail   for_select_example.pml  life.pml          pan.h  peterson.pml    sort.pml
    LTL/              calculator.pml  ex_3a.pml.trail   hajek.pml               loops.pml         pan.m  priorities.pml  test_mtype.pml
    README_tests.txt  cambridge.pml   ex_3c.pml.trail   hello.pml               manna_pnueli.pml  pan.p  rtos1.pml       welfare.pml
    _spin_nvr.tmp     dtp.pml         ex_4.pml.trail    leader0.pml             pan.b             pan.t  sat.pml         werkplaats.pml

---

Spin のExamples を singularity の中からコピーする

    % rsync -av /opt/Spin/Examples ~/src

その Examples を実行してみる

    % spin Examples/for_example.pml 
          1: 1 12 1 (len(x)=3)
          2: 0 10 0 (len(x)=3)
          3: 0 10 0 (len(x)=3)
    1 process created

これは、単なる一回の実行

これをモデル検査するには、pan.c を生成してコンパイルして実行する

    % spin -a  Examples/pathfinder.pml
    % clang -O pan.c
    % ./a.out

これで、モデル検査が実行される

    pan:1: invalid end state (at depth 4)
    pan: wrote pathfinder.pml.trail
    (Spin Version 6.5.2 -- 15 February 2024)
    Warning: Search not completed
            + Partial Order Reduction
    Full statespace search for:
            never claim             - (none specified)
            assertion violations    +
            acceptance   cycles     - (not selected)
            invalid end states      +
    State-vector 28 byte, depth reached 5, errors: 1
            5 states, stored
            1 states, matched
            6 transitions (= stored+matched)
            2 atomic steps
    hash conflicts:         0 (resolved)
    Stats on memory usage (in Megabytes):
        0.000       equivalent memory usage for states (stored*(State-vector + overhead))
        0.290       actual memory usage for states
      128.000       memory used for hash table (-w24)
        0.534       memory used for DFS stack (-m10000)
      128.730       total actual memory usage
    pan: elapsed time 0 seconds