SPIN モデル検査 6.1章

概要

以下の教科書にて、ソースコードが提供されていませんでしたので、自分なりに作成したコードを置いておきます。特に、ユーザ挙動コードについては全く示されていませんでしたので、5章などを見ながら自力で作りました。ご指摘いただければ幸いです。
https://www.amazon.co.jp/gp/product/B01MD13BNP/ref=kinw_myk_ro_title

環境

Ubuntu20.04
Spin 6.5.1

図6.13 想定シナリオ

実行手順:

spin -a cruise.pml
gcc pan.c
./a.out

cruise.pml

# define SYNCH 0
mtype = {enableControl, clearSpeed, recordSpeed, disableControl};
chan toSpeed = [SYNCH] of {mtype};

active proctype SpeedController()
{
Disabled: end:
    do
    :: toSpeed ? enableControl -> goto Enabled
    :: toSpeed ? clearSpeed
    od
Enabled:
    do
    :: toSpeed ? recordSpeed
    :: toSpeed ? disableControl -> goto Disabled
    od
}

mtype = {engineOn, engineOff, on, off, resume};
chan toCruise = [SYNCH] of {mtype};

active proctype CruiseController()
{
Inactive: end:
    do
    :: toCruise ? engineOn -> atomic{toSpeed ! clearSpeed; goto Active}
    od

Active:
Start:
    do
    :: toCruise ? on ->
        atomic{toSpeed ! enableControl; toSpeed ! recordSpeed; goto Running}
    :: toCruise ? engineOff -> atomic{goto Inactive}
    od

Running:
    do
    :: toCruise ? off ->
        atomic{toSpeed ! disableControl; goto Wait}
    :: toCruise ? engineOff ->
        atomic{
            // toSpeed ! disableControl;   //Added
            goto Inactive
        }
    od

Wait:
    do
    :: toCruise ? resume ->
        atomic{toSpeed ! enableControl; goto Running}
    :: toCruise ? on ->
        atomic{toSpeed ! enableControl; toSpeed ! recordSpeed; goto Running}
    :: toCruise ? engineOff ->
        atomic{goto Inactive}
    od
}


mtype = {S0, S1, S2, S3, S4};

active proctype User()
{
    mtype state = S0;
end:
    do
    :: state == S0 -> atomic{toCruise ! engineOn ; state = S1};
    :: state == S1 -> atomic{toCruise ! on ; state = S2};
    :: state == S2 -> atomic{toCruise ! engineOff ; state = S4};
    :: state == S2 -> atomic{toCruise ! off ; state = S3};
    :: state == S3 -> atomic{toCruise ! on ; state = S2};
    :: state == S3 -> atomic{toCruise ! resume ; state = S2};
    od
}

"Added"と示したのが、p108で示された修正箇所です。
これを外した場合、エラーとなります。内容は以下コマンドで見れます。

spin -t -c cruise.pml

図6.14 ゴリラ・シナリオ

用法などは先と同様です。

cruise2.pml

# define SYNCH 0
mtype = {enableControl, clearSpeed, recordSpeed, disableControl};
chan toSpeed = [SYNCH] of {mtype};

active proctype SpeedController()
{
Disabled: end:
    do
    :: toSpeed ? enableControl -> goto Enabled
    :: toSpeed ? clearSpeed
    od
Enabled:
    do
    :: toSpeed ? recordSpeed
    :: toSpeed ? disableControl -> goto Disabled
    od
}

mtype = {engineOn, engineOff, on, off, resume};
chan toCruise = [SYNCH] of {mtype};

active proctype CruiseController()
{
Inactive: end:
    do
    :: toCruise ? engineOn -> atomic{toSpeed ! clearSpeed; goto Active}
    od

Active:
Start:
    do
    :: toCruise ? on ->
        atomic{toSpeed ! enableControl; toSpeed ! recordSpeed; goto Running}
    :: toCruise ? engineOff -> atomic{goto Inactive}
    :: toCruise ? _;skip    // Added
    od

Running:
    do
    :: toCruise ? off ->
        atomic{toSpeed ! disableControl; goto Wait}
    :: toCruise ? engineOff ->
        atomic{toSpeed ! disableControl; goto Inactive}
    :: toCruise ? _;skip    // Added
    od

Wait:
    do
    :: toCruise ? resume ->
        atomic{toSpeed ! enableControl; goto Running}
    :: toCruise ? on ->
        atomic{toSpeed ! enableControl; toSpeed ! recordSpeed; goto Running}
    :: toCruise ? engineOff ->
        atomic{goto Inactive}
    od
}


mtype = {S0, S1, S2, S3, S4, SF};

active proctype User()
{
    mtype state = S0;
end:
    do
    :: state == S0 -> atomic{toCruise ! engineOn ; state = S1};
    :: state == S1 -> atomic{toCruise ! on ; state = S2};
    :: state == S1 -> atomic{toCruise ! off ; state = S3};
    :: state == S1 -> atomic{toCruise ! resume ; state = S4};
    :: state == S2 -> atomic{toCruise ! resume ; state = S4};
    :: state == S2 -> atomic{toCruise ! off ; state = S3};
    :: state == S3 -> atomic{toCruise ! on ; state = S2};
    :: state == S3 -> atomic{toCruise ! resume ; state = S4};
    :: state == S4 -> atomic{toCruise ! off ; state = S3};
    :: state == S4 -> atomic{toCruise ! on ; state = S2};
    :: atomic{toCruise ! engineOff;skip; state=SF}
    od
}