プログラミングなどなど

プログラミングに関係しそうな内容を

SPIN:Never Claimと通常プロセスの動作の違いに気をつけよう

LTLでの記述する際に時相論理という論理が使えるのですが、簡単なものから理解していこうと考えて、単純な例を記述してみたのですが、単純と思いきやハマった例を紹介します。ハマった部分を確認しようとしましたが、結果としては現状、手詰まりとなりました。

モデル(never.pml)

以下のようなモデルと検証式があるとします。

bool i = false;

active proctype A()
{
  i = true;
}

ltl { i == false }

検証の実行

上記のLTLの検証結果を予想してみて下さい。

$ spin -run never.pml 
(Spin Version 6.5.0 -- 17 July 2019)
	+ Partial Order Reduction

Full statespace search for:
	never claim         	+ (ltl_0)
	assertion violations	+ (if within scope of claim)
	acceptance   cycles 	+ (fairness disabled)
	invalid end states	- (disabled by never claim)

State-vector 20 byte, depth reached 0, errors: 0
        1 states, stored
        0 states, matched
        1 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.000	equivalent memory usage for states (stored*(State-vector + overhead))
    0.292	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


unreached in proctype A
	never.pml:6, state 2, "-end-"
	(1 of 2 states)
unreached in claim ltl_0
	_spin_nvr.tmp:8, state 8, "-end-"
	(1 of 8 states)

pan: elapsed time 0 seconds

私はエラーが検出される想定だったのですが、なんとエラー無しとなりました。

記述したLTLのPromelaコードの確認

以下のコマンドを実行し、記述したLTLからどの様なNever ClaimがPromeralコードとして生成されたかを確認してみます。

$ spin -a never.pml 
ltl ltl_0: (i==0)
$ cat -n _spin_nvr.tmp 
     1	never ltl_0 {    /* !((i==0)) */
     2	accept_init:
     3	T0_init:
     4		do
     5		:: atomic { (! (((i==0)))) -> assert(!(! (((i==0))))) }
     6		od;
     7	accept_all:
     8		skip
     9	}

現状の私の理解は次のとおりです。

  1. 5行目の!(((i==0)))はプロセスAのi = trueが実行されるまでは、成立しないので、do文で実行可能な処理がなくブロックされる。
  2. プロセスAのi = trueが実行されると、Never Claimの!(((i==0)))が成立し、assertが実行されエラーが検出される。

しかし、エラーは検出されませんでした。

LTLのPromelaコードから通常プロセスを作る

現状、私は通常プロセスとNever Claimの違いは、Never Claimは検証対象のプロセスの1ステップ毎にNever Claimの検証が行われると理解しています。
そこで、得られたPromelaコードを通常プロセスとして実装した場合、検証漏れはあるかもしれませんが、今回のケースでは網羅的な検証でエラーが無いことになっているので、通常プロセスにしても0件になるのではないかと予想し試すことにしました。

追記したコード

ltlの部分を以下のコードに置き換えます。

active proctype B() {    /* !((i==0)) */
accept_init:
T0_init:
  do
  :: atomic { (! (((i==0)))) -> assert(!(! (((i==0))))) }
  od;
accept_all:
  skip
}

検証の実行

$ spin -run never.pml
pan:1: assertion violated  !( !((i==0))) (at depth 1)
pan: wrote never.pml.trail

(Spin Version 6.5.0 -- 17 July 2019)
Warning: Search not completed
	+ Partial Order Reduction

Full statespace search for:
	never claim         	- (none specified)
	assertion violations	+
	acceptance   cycles 	+ (fairness disabled)
	invalid end states	+

State-vector 20 byte, depth reached 1, errors: 1
        2 states, stored
        0 states, matched
        2 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.000	equivalent memory usage for states (stored*(State-vector + overhead))
    0.292	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

なんと、エラーを検出しました。今のPromelaコードの理解としてはこちらの方がしっくりくるのですが、Never Claimの動作理解としては、ここでお手上げとなりました。

状態テーブルに違があるかを確認

他に差異があるかを確認できないかと考えて状態表(-dオプション)を比べて見ましたが、同じでした。

Never Claim

$ ./pan -d
proctype A
	state   1 -(tr   5)-> state   2  [id   0 tp   2] [----G] never.pml:5 => i = 1
	state   2 -(tr   6)-> state   0  [id   1 tp 3500] [--e-L] never.pml:6 => -end-
claim ltl_0
	state   4 -(tr   3)-> state   4  [id   2 tp   2] [-a--G] never.pml:4 => (!((i==0)))

Transition Type: A=atomic; D=d_step; L=local; G=global
Source-State Labels: p=progress; e=end; a=accept;
Note: statement merging was used. Only the first
      stmnt executed in each merge sequence is shown
      (use spin -a -o3 to disable statement merging)

pan: elapsed time 1.72e+07 seconds
pan: rate         0 states/second

通常プロセス

$ ./pan -d
proctype A
	state   1 -(tr   5)-> state   2  [id   0 tp   2] [----G] never.pml:5 => i = 1
	state   2 -(tr   6)-> state   0  [id   1 tp 3500] [--e-L] never.pml:6 => -end-
proctype B
	state   4 -(tr   3)-> state   4  [id   2 tp   2] [-a--G] never.pml:12 => (!((i==0)))

Transition Type: A=atomic; D=d_step; L=local; G=global
Source-State Labels: p=progress; e=end; a=accept;
Note: statement merging was used. Only the first
      stmnt executed in each merge sequence is shown
      (use spin -a -o3 to disable statement merging)

pan: elapsed time 1.72e+07 seconds
pan: rate         0 states/second

結果(手詰まり)

自分は手詰まりとなりました。前回の記事(SPIN:LTLの記述によっては意図した検査にならない? - プログラミングなどなど)のようにデバッグしてみると、Never Claimの遷移処理が走っていますが、どこにも遷移せずにすぐに検証が終了していました。感覚としては、検証時の最初のステップでNver Claimがどこにも移動できないような記述がある時に問題となるケースがありそうです。自分のLTLの記述が悪い感じもあります。

SPIN:LTLの記述によっては意図した検査にならない?

前回モデル(SPIN:モデル(安全性(排他)と応答性) - プログラミングなどなど)でLTLで検証式を記述する際に実は、トライ&エラーを行っていました。その際、記述したLTLで想定していた検査が行われていないようなケースがありました。
そもそも、記述したLTLが誤っているかもしれないので、慣れている人やよく理解している人には無縁かもしれませんが、私は最初気がつかなかったので、メモとして残したいと思います。

モデル(model.pml)(前回と同じもの)

/* OPE-SV間のメッセージ定義 */
mtype = {
  START_SND_SRV, /* 第2サービス開始 */
  STOP_SND_SRV   /* 第2サービス停止 */
}

/* SVとの通信用チャネル */
chan svCh = [2] of { mtype }

/* 運用者による操作を受付てSVに操作に対応するメッセージを送信するプロセス */
active proctype OPE()
{
  bool sndSrvOrd = false;

  /* 運用者による第2サービス開始操作 */
  atomic { sndSrvOrd = true;  svCh ! START_SND_SRV; }

  /* 時間経過などもろもろ */

  /* 運用者による第2サービス停止操作 */
  atomic { sndSrvOrd = false; svCh ! STOP_SND_SRV;  }
}

/* 実際のサービスを制御するサーバプロセス */
active proctype SV()
{
  /* デフォルトでは第1サービスが有効になっているものとする。*/
  /* 運用者から第2サービスの開始操作が行われた場合に、 第2サービスを開始する。*/
  /* 第1サービスと第2サービスは排他関係になっており、両者が共に有効になってはならない。*/
  bool isFstSrvOn = true;
  bool isSndSrvOn = false;

  mtype event;
  do
  :: svCh ? event ->
       if
       :: atomic { event == START_SND_SRV -> isFstSrvOn = false; isSndSrvOn = true;  }
       :: atomic { event == STOP_SND_SRV  -> isFstSrvOn = true;  isSndSrvOn = false; }
       fi
  od
}

前回の検証式

前回は、運用者からの第2サービスの開始にともなって第2サービスが有効になること。また、停止に伴って第2サービスが停止することを、応答性として以下の様に記述しました。

応答性(第2サービス開始)

/* 運用者による第2サービスの開始操作が行われたら、第2サービスが有効になる。*/
ltl  liveSndStart {  [](OPE:sndSrvOrd == true -> <>(SV:isFstSrvOn == false && SV:isSndSrvOn == true)) }

応答性2(第2サービス停止)

/* 運用者による第2サービスの停止操作が行われたら、第1サービスが有効になる。*/
ltl  liveSndStop {  [](OPE:sndSrvOrd == false -> <>(SV:isFstSrvOn == true && SV:isSndSrvOn == false)) }

検証式(誤り?)

上記の形になる試行錯誤の前は以下の様に記述していました。
注目して頂きたいのは前提条件(OPE:sndSrvOrd == true, OPE:sndSrvOrd == false)の部分となります。

例1
/* 運用者による第2サービスの開始操作が行われたら、第2サービスが有効になる。*/
ltl  liveSndStart2 {   OPE:sndSrvOrd == true -> <>[](SV:isSndSrvOn == true) }
ltl nliveSndStart2 { !(OPE:sndSrvOrd == true -> <>[](SV:isSndSrvOn == true)) }
例2
/* 運用者による第2サービスの停止操作が行われたら、第1サービスが有効になる。*/
ltl  liveSndStop2 {   OPE:sndSrvOrd == false -> <>[](SV:isFstSrvOn == true) }
ltl nliveSndStop2 { !(OPE:sndSrvOrd == false -> <>[](SV:isFstSrvOn == true)) }

検証の実行

例1

例1の検証を実行してみると、確かにエラーが0件であることは想定どおりなのですが、「1 states, stored」となっていたり、「unreached」に実行を想定している行が出力されていたりと怪しい感じが出ています。

$ spin -run -ltl liveSndStart2 model.pml
pan: ltl formula liveSndStart2

(Spin Version 6.5.0 -- 17 July 2019)
	+ Partial Order Reduction

Full statespace search for:
	never claim         	+ (liveSndStart2)
	assertion violations	+ (if within scope of claim)
	acceptance   cycles 	+ (fairness disabled)
	invalid end states	- (disabled by never claim)

State-vector 52 byte, depth reached 0, errors: 0
        1 states, stored
        0 states, matched
        1 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.000	equivalent memory usage for states (stored*(State-vector + overhead))
    0.261	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


unreached in proctype OPE
	model.pml:16, state 2, "svCh!START_SND_SRV"
	model.pml:21, state 5, "svCh!STOP_SND_SRV"
	model.pml:21, state 6, "sndSrvOrd = 0"
	model.pml:22, state 7, "-end-"
	(4 of 7 states)
unreached in proctype SV
	model.pml:37, state 3, "isFstSrvOn = 0"
	model.pml:37, state 4, "isSndSrvOn = 1"
	model.pml:38, state 7, "isFstSrvOn = 1"
	model.pml:38, state 8, "isSndSrvOn = 0"
	model.pml:37, state 10, "((event==START_SND_SRV))"
	model.pml:37, state 10, "((event==STOP_SND_SRV))"
	model.pml:41, state 15, "-end-"
	(6 of 15 states)
unreached in claim liveSndStart2
	_spin_nvr.tmp:101, state 10, "(1)"
	_spin_nvr.tmp:105, state 17, "(!((SV.isSndSrvOn==1)))"
	_spin_nvr.tmp:105, state 17, "(1)"
	_spin_nvr.tmp:108, state 20, "-end-"
	(3 of 20 states)

pan: elapsed time 0 seconds

例2

因みに例2を実行した場合は、ちゃんと探索してくれていそうな感じがあります。

$ spin -run -ltl liveSndStop2 model.pml
pan: ltl formula liveSndStop2

(Spin Version 6.5.0 -- 17 July 2019)
	+ Partial Order Reduction

Full statespace search for:
	never claim         	+ (liveSndStop2)
	assertion violations	+ (if within scope of claim)
	acceptance   cycles 	+ (fairness disabled)
	invalid end states	- (disabled by never claim)

State-vector 52 byte, depth reached 20, errors: 0
       12 states, stored (17 visited)
        9 states, matched
       26 transitions (= visited+matched)
       20 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.001	equivalent memory usage for states (stored*(State-vector + overhead))
    0.261	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


unreached in proctype OPE
	(0 of 7 states)
unreached in proctype SV
	model.pml:41, state 15, "-end-"
	(1 of 15 states)
unreached in claim liveSndStop2
	_spin_nvr.tmp:143, state 20, "-end-"
	(1 of 20 states)

pan: elapsed time 0 seconds

デバッグ

例1で探索が行われていないのかを部分を見たいと考えデバッグしてみることにしました。検証器のコンパイルまでに行った手順は以下となります。

検証器コードの整形とデバッグオプション付きでのコンパイル

$ spin -a model.pml
ltl safe: [] (! (((SV:isFstSrvOn==1)) && ((SV:isSndSrvOn==1))))
:
ltl nliveSndStart3: ! ([] (<> ((! ((OPE:sndSrvOrd==1))) || (<> ([] ((SV:isSndSrvOn==1)))))))
  the model contains 13 never claims: nliveSndStart3, liveSndStart3, nliveSndStop2, liveSndStop2, nliveSndStart2, liveSndStart2, nliveSndStop, liveSndStop, nliveSndStart, liveSndStart, notStop, nsafe, safe
  only one claim is used in a verification run
  choose which one with ./pan -a -N name (defaults to -N safe)
  or use e.g.: spin -search -ltl safe model.pml
$ gcc -E -C -P -DNOREDUCE pan.c > ppan.c
$ indent ppan.c -o pppan.c
$ gcc -g3 -O0 pppan.c

GDBによるデバッグ

do_transit関数にブレークポイントを設定しステップ実行していくと、確かにすぐに検証を完了したルートに入っていそうでした。

$ gdb --args ./a.out -a -N liveSndStart2
(gdb) break do_transit 
Breakpoint 1 at 0x6d09: file pppan.c, line 9653.
(gdb) r
Starting program: /home/makoto/blog/ltlNG/a.out -a -N liveSndStart2
pan: ltl formula liveSndStart2

Breakpoint 1, do_transit (t=0x19010, II=32767) at pppan.c:9653
9653	{
(gdb) backtrace 
#0  do_transit (t=0x19010, II=32767) at pppan.c:9653
#1  0x0000555555561645 in new_state () at pppan.c:11685
#2  0x000055555555acf2 in do_the_search () at pppan.c:9648
#3  0x00005555555587e0 in run () at pppan.c:8945
#4  0x000055555556485d in main (argc=1, argv=0x7fffffffdd80) at pppan.c:13316

上記設定後に処理を再開させてステップ実行させていくと、他状態への遷移がなく、すぐにrun関数から戻り、結果の出力処理へと進みました。

SPIN:モデル(安全性(排他)と応答性)

LTLに少し慣れた気がしたので、簡単なモデルを記述し練習してみることにしました。

モデルとしては、サーバでは標準で第1サービスが有効になっているが、運用者から第2サービスの開始操作があった場合に、サービスを切り替えるというものです。サービスは排他関係になっており、第1と第2サービスがともに有効になってはならないものとしています。検査の範囲としては、運用者が第2サービスを開始操作を行い、その後、停止操作を行うという流れを考えています。

モデル(model.pml)

/* OPE-SV間のメッセージ定義 */
mtype = {
  START_SND_SRV, /* 第2サービス開始 */
  STOP_SND_SRV   /* 第2サービス停止 */
}

/* SVとの通信用チャネル */
chan svCh = [2] of { mtype }

/* 運用者による操作を受付てSVに操作に対応するメッセージを送信するプロセス */
active proctype OPE()
{
  bool sndSrvOrd = false;

  /* 運用者による第2サービス開始操作 */
  atomic { sndSrvOrd = true;  svCh ! START_SND_SRV; }

  /* 時間経過などもろもろ */

  /* 運用者による第2サービス停止操作 */
  atomic { sndSrvOrd = false; svCh ! STOP_SND_SRV;  }
}

/* 実際のサービスを制御するサーバプロセス */
active proctype SV()
{
  /* デフォルトでは第1サービスが有効になっているものとする。*/
  /* 運用者から第2サービスの開始操作が行われた場合に、 第2サービスを開始する。*/
  /* 第1サービスと第2サービスは排他関係になっており、両者が共に有効になってはならない。*/
  bool isFstSrvOn = true;
  bool isSndSrvOn = false;

  mtype event;
  do
  :: svCh ? event ->
       if
       :: atomic { event == START_SND_SRV -> isFstSrvOn = false; isSndSrvOn = true;  }
       :: atomic { event == STOP_SND_SRV  -> isFstSrvOn = true;  isSndSrvOn = false; }
       fi
  od
}

検証式の追加

先頭にnが付いているものは、動作確認用にエラーを出力させるために用意しました。

安全性

/* 第1サービスと第2サービスが共に有効で無い状態が、常に成り立つ。*/
ltl  safe {  []!(SV:isFstSrvOn == true && SV:isSndSrvOn == true) }
ltl nsafe { ![]!(SV:isFstSrvOn == true && SV:isSndSrvOn == true) }

/* 第1サービスと第2サービスが共に無効な状態は、常に成立しない。*/
/* -> どちらかのサービスは有効である。*/
ltl notStop { []!(SV:isFstSrvOn == false && SV:isSndSrvOn == false) }

応答性(第2サービス開始)

/* 運用者による第2サービスの開始操作が行われたら、第1サービスが無効になり、第2サービスが有効になる。*/
ltl  liveSndStart {  [](OPE:sndSrvOrd == true -> <>(SV:isFstSrvOn == false && SV:isSndSrvOn == true)) }
ltl nliveSndStart { ![](OPE:sndSrvOrd == true -> <>(SV:isFstSrvOn == false && SV:isSndSrvOn == true)) }

応答性2(第2サービス停止)

/* 運用者による第2サービスの停止操作が行われたら、第1サービスが有効になり、第2サービスが無効になる。*/
ltl  liveSndStop {  [](OPE:sndSrvOrd == false -> <>(SV:isFstSrvOn == true && SV:isSndSrvOn == false)) }
ltl nliveSndStop { ![](OPE:sndSrvOrd == false -> <>(SV:isFstSrvOn == true && SV:isSndSrvOn == false)) }

試し

試しにSVがSTOP_SND_SRVイベントの処理を行う部分のatomicを取り除き以下の様にしてみます。

//       :: atomic { event == STOP_SND_SRV  -> isFstSrvOn = true;  isSndSrvOn = false; }
       :: event == STOP_SND_SRV  -> isFstSrvOn = true;  isSndSrvOn = false; 

すると、安全性の検査でisFstSrvOnとisSndSrvOnの両方がtrueになるケースがエラーとして検出されます。

検出例

$ spin -t -p -l model.pml
pan: ltl formula safe
pan:1: assertion violated  !( !( !(((SV.isFstSrvOn==1)&&(SV.isSndSrvOn==1))))) (at depth 19)
pan: wrote model.pml.trail

(Spin Version 6.5.0 -- 17 July 2019)
Warning: Search not completed
	+ Partial Order Reduction

Full statespace search for:
	never claim         	+ (safe)
	assertion violations	+ (if within scope of claim)
	acceptance   cycles 	+ (fairness disabled)
	invalid end states	- (disabled by never claim)

State-vector 44 byte, depth reached 19, errors: 1
        8 states, stored
        0 states, matched
        8 transitions (= stored+matched)
        5 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.001	equivalent memory usage for states (stored*(State-vector + overhead))
    0.278	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
$ spin -t -p -l model.pml
ltl safe: [] (! (((SV:isFstSrvOn==1)) && ((SV:isSndSrvOn==1))))
ltl nsafe: ! ([] (! (((SV:isFstSrvOn==1)) && ((SV:isSndSrvOn==1)))))
ltl notStop: [] (! (((SV:isFstSrvOn==0)) && ((SV:isSndSrvOn==0))))
ltl liveSndStart: [] ((! ((OPE:sndSrvOrd==1))) || (<> (((SV:isFstSrvOn==0)) && ((SV:isSndSrvOn==1)))))
ltl nliveSndStart: ! ([] ((! ((OPE:sndSrvOrd==1))) || (<> (((SV:isFstSrvOn==0)) && ((SV:isSndSrvOn==1))))))
ltl liveSndStop: [] ((! ((OPE:sndSrvOrd==0))) || (<> (((SV:isFstSrvOn==1)) && ((SV:isSndSrvOn==0)))))
ltl nliveSndStop: ! ([] ((! ((OPE:sndSrvOrd==0))) || (<> (((SV:isFstSrvOn==1)) && ((SV:isSndSrvOn==0))))))
starting claim 2
Never claim moves to line 4	[(1)]
  2:	proc  0 (OPE:1) model.pml:16 (state 1)	[sndSrvOrd = 1]
		OPE(0):sndSrvOrd = 1
  3:	proc  0 (OPE:1) model.pml:16 (state 2)	[svCh!START_SND_SRV]
  5:	proc  1 (SV:1) model.pml:35 (state 1)	[svCh?event]
		SV(1):event = START_SND_SRV
  7:	proc  1 (SV:1) model.pml:37 (state 2)	[((event==START_SND_SRV))]
  8:	proc  1 (SV:1) model.pml:37 (state 3)	[isFstSrvOn = 0]
		SV(1):isFstSrvOn = 0
  9:	proc  1 (SV:1) model.pml:37 (state 4)	[isSndSrvOn = 1]
		SV(1):isSndSrvOn = 1
 11:	proc  0 (OPE:1) model.pml:21 (state 4)	[sndSrvOrd = 0]
		OPE(0):sndSrvOrd = 0
 12:	proc  0 (OPE:1) model.pml:21 (state 5)	[svCh!STOP_SND_SRV]
 14:	proc  1 (SV:1) model.pml:35 (state 1)	[svCh?event]
		SV(1):event = STOP_SND_SRV
 16:	proc  1 (SV:1) model.pml:39 (state 6)	[((event==STOP_SND_SRV))]
 18:	proc  1 (SV:1) model.pml:39 (state 7)	[isFstSrvOn = 1]
		SV(1):isFstSrvOn = 1
Never claim moves to line 3	[(!(!(((SV.isFstSrvOn==1)&&(SV.isSndSrvOn==1)))))]
spin: _spin_nvr.tmp:3, Error: assertion violated
spin: text of failed assertion: assert(!(!(!(((SV.isFstSrvOn==1)&&(SV.isSndSrvOn==1))))))
spin: trail ends after 20 steps
#processes: 2
		queue 1 (svCh): 
 20:	proc  1 (SV:1) model.pml:39 (state 8)
		SV(1):event = STOP_SND_SRV
		SV(1):isSndSrvOn = 1
		SV(1):isFstSrvOn = 1
 20:	proc  0 (OPE:1) model.pml:22 (state 7) <valid end state>
		OPE(0):sndSrvOrd = 0
 20:	proc  - (safe:1) _spin_nvr.tmp:2 (state 6)
2 processes created

SPIN:2プロセスからのメッセージ受信順序確認

前回(SPIN:LTLを使った2プロセスの実行順序確認 - プログラミングなどなど)の内容と似ていますが、今度は2つのプロセスA,BがプロセスCにメッセージ送信する例を考えてみました。前回の内容とほぼ同じなので、同じオプションで結果が得られると考えていましたが、Bが先に送信するケースだけが検出されトライ&エラーを繰り返すこととなりました。

結果として、最適化オプションの無効化-o1または-o2を行うことで欲しいケースを得ることができました。(結果以上のことは理解していません。)

モデル

$ cat -n 2msg.pml
     1	mtype = { msgA, msgB }
     2	
     3	chan ch = [2] of { mtype }
     4	
     5	bool isRcvA = false;
     6	bool isRcvB = false;
     7	
     8	active proctype A()
     9	{
    10	  ch ! msgA
    11	}
    12	
    13	active proctype B()
    14	{
    15	  ch ! msgB
    16	}
    17	
    18	active proctype C()
    19	{
    20	  mtype msg;
    21	  do
    22	  :: ch ? msg ->
    23	       if
    24	       :: msg == msgA -> isRcvA = true;
    25	       :: msg == msgB -> isRcvB = true;
    26	       fi
    27	  od
    28	}

プロセスAとBが、プロセスCに向けてメッセージを送信するモデルです。実行の制約は無いので、22行目:プロセスCのch ? msg では、msgAを先に受信する場合とmsgBを先に受信する場合があるはずです。

ランダムシミュレーション

ランダムシミュレーションを何度か行ってみると、確かに上記の2ケースが結果として出てきます。

msgAを先に受信するケース

$ spin -r 2msg.pml
  3:	proc  2 (C:1) 2msg.pml:22 Recv msgA	<- queue 1 (ch)
  8:	proc  2 (C:1) 2msg.pml:22 Recv msgB	<- queue 1 (ch)
      timeout
#processes: 3
		queue 1 (ch): 
		isRcvA = 1
		isRcvB = 1
 12:	proc  2 (C:1) 2msg.pml:21 (state 8)
 12:	proc  1 (B:1) 2msg.pml:16 (state 2) <valid end state>
 12:	proc  0 (A:1) 2msg.pml:11 (state 2) <valid end state>
3 processes created

msgBを先に受信するケース

$ spin -r 2msg.pml
  3:	proc  2 (C:1) 2msg.pml:22 Recv msgB	<- queue 1 (ch)
  8:	proc  2 (C:1) 2msg.pml:22 Recv msgA	<- queue 1 (ch)
      timeout
#processes: 3
		queue 1 (ch): 
		isRcvA = 1
		isRcvB = 1
 12:	proc  2 (C:1) 2msg.pml:21 (state 8)
 12:	proc  1 (B:1) 2msg.pml:16 (state 2) <valid end state>
 12:	proc  0 (A:1) 2msg.pml:11 (state 2) <valid end state>
3 processes created

LTLでの確認

確認したい性質としては先の例と同じなので同様の式を追加して検証してみます。

検証式

以下の検証式をモデルに追加します。

検証したい性質
ltl a01 { <>[](isRcvA == true && isRcvB == true) }
検証したい性質の否定
ltl c01 { !<>[](isRcvA == true && isRcvB == true) }
実行
検証したい性質の確認
$ spin -run -ltl a01 2msg.pml
pan: ltl formula a01

(Spin Version 6.5.0 -- 17 July 2019)
	+ Partial Order Reduction

Full statespace search for:
	never claim         	+ (a01)
	assertion violations	+ (if within scope of claim)
	acceptance   cycles 	+ (fairness disabled)
	invalid end states	- (disabled by never claim)

State-vector 44 byte, depth reached 17, errors: 0
       43 states, stored (83 visited)
       83 states, matched
      166 transitions (= visited+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.003	equivalent memory usage for states (stored*(State-vector + overhead))
    0.289	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


unreached in proctype A
	(0 of 2 states)
unreached in proctype B
	(0 of 2 states)
unreached in proctype C
	2msg.pml:28, state 11, "-end-"
	(1 of 11 states)
unreached in claim a01
	_spin_nvr.tmp:10, state 13, "-end-"
	(1 of 13 states)
unreached in claim c02
	_spin_nvr.tmp:19, state 10, "(((isRcvA==1)&&(isRcvB==1)))"
	_spin_nvr.tmp:21, state 13, "-end-"
	(2 of 13 states)

pan: elapsed time 0 seconds
検証したい性質がどのように成り立ったかの確認
$ spin -run -ltl c01 -c0 -e 2msg.pml 
pan: ltl formula c01
pan:1: acceptance cycle (at depth 18)
pan: wrote 2msg.pml1.trail
pan: wrote 2msg.pml2.trail

(Spin Version 6.5.0 -- 17 July 2019)
	+ Partial Order Reduction

Full statespace search for:
	never claim         	+ (c01)
	assertion violations	+ (if within scope of claim)
	acceptance   cycles 	+ (fairness disabled)
	invalid end states	- (disabled by never claim)

State-vector 44 byte, depth reached 18, errors: 2
       23 states, stored (24 visited)
        8 states, matched
       32 transitions (= visited+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.002	equivalent memory usage for states (stored*(State-vector + overhead))
    0.289	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


unreached in proctype A
	(0 of 2 states)
unreached in proctype B
	(0 of 2 states)
unreached in proctype C
	2msg.pml:28, state 11, "-end-"
	(1 of 11 states)
unreached in claim c01
	_spin_nvr.tmp:21, state 13, "-end-"
	(1 of 13 states)

pan: elapsed time 0 seconds

エラートレイルの確認

エラートレイルを確認すると検出された2件ともmsgBを先に受信したケースとなっています。

1件目
$ spin -t1 -r 2msg.pml
ltl a01: <> ([] (((isRcvA==1)) && ((isRcvB==1))))
ltl c01: ! (<> ([] (((isRcvA==1)) && ((isRcvB==1)))))
starting claim 4
Never claim moves to line 15	[(1)]
  4:	proc  2 (C:1) 2msg.pml:22 Recv msgB	<- queue 1 (ch)
 12:	proc  2 (C:1) 2msg.pml:22 Recv msgA	<- queue 1 (ch)
Never claim moves to line 14	[(((isRcvA==1)&&(isRcvB==1)))]
Never claim moves to line 19	[(((isRcvA==1)&&(isRcvB==1)))]
  <<<<<START OF CYCLE>>>>>
spin: trail ends after 19 steps
#processes: 3
		queue 1 (ch): 
		isRcvA = 1
		isRcvB = 1
 19:	proc  2 (C:1) 2msg.pml:21 (state 8)
 19:	proc  1 (B:1) 2msg.pml:16 (state 2) <valid end state>
 19:	proc  0 (A:1) 2msg.pml:11 (state 2) <valid end state>
 19:	proc  - (c01:1) _spin_nvr.tmp:18 (state 10)
2件目
$ spin -t2 -r 2msg.pml
ltl a01: <> ([] (((isRcvA==1)) && ((isRcvB==1))))
ltl c01: ! (<> ([] (((isRcvA==1)) && ((isRcvB==1)))))
starting claim 4
Never claim moves to line 15	[(1)]
  4:	proc  2 (C:1) 2msg.pml:22 Recv msgB	<- queue 1 (ch)
 12:	proc  2 (C:1) 2msg.pml:22 Recv msgA	<- queue 1 (ch)
Never claim moves to line 14	[(((isRcvA==1)&&(isRcvB==1)))]
Never claim moves to line 19	[(((isRcvA==1)&&(isRcvB==1)))]
  <<<<<START OF CYCLE>>>>>
spin: trail ends after 19 steps
#processes: 3
		queue 1 (ch): 
		isRcvA = 1
		isRcvB = 1
 19:	proc  2 (C:1) 2msg.pml:21 (state 8)
 19:	proc  1 (B:1) 2msg.pml:16 (state 2) <valid end state>
 19:	proc  0 (A:1) 2msg.pml:11 (state 2) <valid end state>
 19:	proc  - (c01:1) _spin_nvr.tmp:18 (state 10)
3 processes created

トライ&エラー

検証式はあっているだろうとの考えから、今回はオプションが関係していないかと思い--helpオプションで出力される内容から該当しそうなものを試していきました。
試した結果、詳しい理由はわかりませんが以下のオプションを使用することで、msgAから受信するケースとmsgBから受信するケースの両方を検出させることができました。

オプション -o1 turn off dataflow-optimizations in verifier

$ spin -o1 -run -ltl c01 -c0 -e 2msg.pml
:
State-vector 44 byte, depth reached 18, errors: 4
       25 states, stored (27 visited)
       10 states, matched
       37 transitions (= visited+matched)
        0 atomic steps
hash conflicts:         0 (resolved)
msgBから受信するケース
$ spin -t1 -r 2msg.pml
ltl a01: <> ([] (((isRcvA==1)) && ((isRcvB==1))))
ltl c01: ! (<> ([] (((isRcvA==1)) && ((isRcvB==1)))))
starting claim 4
Never claim moves to line 15	[(1)]
  4:	proc  2 (C:1) 2msg.pml:22 Recv msgB	<- queue 1 (ch)
 12:	proc  2 (C:1) 2msg.pml:22 Recv msgA	<- queue 1 (ch)
Never claim moves to line 14	[(((isRcvA==1)&&(isRcvB==1)))]
Never claim moves to line 19	[(((isRcvA==1)&&(isRcvB==1)))]
  <<<<<START OF CYCLE>>>>>
spin: trail ends after 19 steps
#processes: 3
		queue 1 (ch): 
		isRcvA = 1
		isRcvB = 1
 19:	proc  2 (C:1) 2msg.pml:21 (state 8)
 19:	proc  1 (B:1) 2msg.pml:16 (state 2) <valid end state>
 19:	proc  0 (A:1) 2msg.pml:11 (state 2) <valid end state>
 19:	proc  - (c01:1) _spin_nvr.tmp:18 (state 10)
3 processes created
msgBから受信するケース
$ spin -t3 -r 2msg.pml
ltl a01: <> ([] (((isRcvA==1)) && ((isRcvB==1))))
ltl c01: ! (<> ([] (((isRcvA==1)) && ((isRcvB==1)))))
starting claim 4
Never claim moves to line 15	[(1)]
  4:	proc  2 (C:1) 2msg.pml:22 Recv msgA	<- queue 1 (ch)
 12:	proc  2 (C:1) 2msg.pml:22 Recv msgB	<- queue 1 (ch)
Never claim moves to line 14	[(((isRcvA==1)&&(isRcvB==1)))]
Never claim moves to line 19	[(((isRcvA==1)&&(isRcvB==1)))]
  <<<<<START OF CYCLE>>>>>
spin: trail ends after 19 steps
#processes: 3
		queue 1 (ch): 
		isRcvA = 1
		isRcvB = 1
 19:	proc  2 (C:1) 2msg.pml:21 (state 8)
 19:	proc  1 (B:1) 2msg.pml:16 (state 2) <valid end state>
 19:	proc  0 (A:1) 2msg.pml:11 (state 2) <valid end state>
 19:	proc  - (c01:1) _spin_nvr.tmp:18 (state 10)
3 processes created

オプション -o2 don't hide write-only variables in verifier

$ spin -o2 -run -ltl c01 -c0 -e 2msg.pml 
:
State-vector 44 byte, depth reached 18, errors: 4
       25 states, stored (27 visited)
       10 states, matched
       37 transitions (= visited+matched)
        0 atomic steps
hash conflicts:         0 (resolved)
msgBから受信するケース
$ spin -t1 -r 2msg.pml
ltl a01: <> ([] (((isRcvA==1)) && ((isRcvB==1))))
ltl c01: ! (<> ([] (((isRcvA==1)) && ((isRcvB==1)))))
starting claim 4
Never claim moves to line 15	[(1)]
  4:	proc  2 (C:1) 2msg.pml:22 Recv msgB	<- queue 1 (ch)
 12:	proc  2 (C:1) 2msg.pml:22 Recv msgA	<- queue 1 (ch)
Never claim moves to line 14	[(((isRcvA==1)&&(isRcvB==1)))]
Never claim moves to line 19	[(((isRcvA==1)&&(isRcvB==1)))]
  <<<<<START OF CYCLE>>>>>
spin: trail ends after 19 steps
#processes: 3
		queue 1 (ch): 
		isRcvA = 1
		isRcvB = 1
 19:	proc  2 (C:1) 2msg.pml:21 (state 8)
 19:	proc  1 (B:1) 2msg.pml:16 (state 2) <valid end state>
 19:	proc  0 (A:1) 2msg.pml:11 (state 2) <valid end state>
 19:	proc  - (c01:1) _spin_nvr.tmp:18 (state 10)
3 processes created
msbAから受信するケース
$ spin -t3 -r 2msg.pml
ltl a01: <> ([] (((isRcvA==1)) && ((isRcvB==1))))
ltl c01: ! (<> ([] (((isRcvA==1)) && ((isRcvB==1)))))
starting claim 4
Never claim moves to line 15	[(1)]
  4:	proc  2 (C:1) 2msg.pml:22 Recv msgA	<- queue 1 (ch)
 12:	proc  2 (C:1) 2msg.pml:22 Recv msgB	<- queue 1 (ch)
Never claim moves to line 14	[(((isRcvA==1)&&(isRcvB==1)))]
Never claim moves to line 19	[(((isRcvA==1)&&(isRcvB==1)))]
  <<<<<START OF CYCLE>>>>>
spin: trail ends after 19 steps
#processes: 3
		queue 1 (ch): 
		isRcvA = 1
		isRcvB = 1
 19:	proc  2 (C:1) 2msg.pml:21 (state 8)
 19:	proc  1 (B:1) 2msg.pml:16 (state 2) <valid end state>
 19:	proc  0 (A:1) 2msg.pml:11 (state 2) <valid end state>
 19:	proc  - (c01:1) _spin_nvr.tmp:18 (state 10)
3 processes created

SPIN:LTLを使った2プロセスの実行順序確認

SPINでは記述したモデルについてLTLで記述した性質の検証を行うことで反例がないかどうかをチェックしてくれます。私はまだ理解が浅いのでLTLで記述した検証が意図したものになっているかどうかについて自信がありません。そこで、記述した検証が、意図した検証になっていそうだということを確かめたいと思いました。

結論としては解をつかめていないのですが、大丈夫そうだと思える部分まで行くことができましたので、行った手順とメモを残します。

モデルとしては、2つのプロセスがそれぞれが管理する変数を更新するパターンが2通りあるということを検出したいと思います。

モデル

$ cat -n 2pro.pml
     1	bool isAProced = false;
     2	bool isBProced = false;
     3	
     4	active proctype A()
     5	{
     6	  isAProced = true;
     7	}
     8	
     9	active proctype B()
    10	{
    11	  isBProced = true;
    12	}

プロセスAとBがあり、並列に動作するモデルです。実行の制約は無いので、6行目:プロセスAのisAProced = trueが先に実行される場合と11行目:プロセスBのisBProced = trueが先に実行される場合があるはずです。

ランダムシミュレーション

ランダムシミュレーションを何度か行ってみると、確かに上記の2ケースが結果として出てきます。

プロセスAの処理が先に実行されるケース

$ spin -p 2pro.pml
  0:	proc  - (:root:) creates proc  0 (A)
  0:	proc  - (:root:) creates proc  1 (B)
  1:	proc  0 (A:1) 2pro.pml:6 (state 1)	[isAProced = 1]
  2:	proc  1 (B:1) 2pro.pml:11 (state 1)	[isBProced = 1]
  2:	proc  1 (B:1)           terminates
  2:	proc  0 (A:1)       terminates
2 processes created

プロセスBの処理が先に実行されるケース

$ spin -p 2pro.pml
  0:	proc  - (:root:) creates proc  0 (A)
  0:	proc  - (:root:) creates proc  1 (B)
  1:	proc  1 (B:1) 2pro.pml:11 (state 1)	[isBProced = 1]
  1:	proc  1 (B:1)           terminates
  2:	proc  0 (A:1) 2pro.pml:6 (state 1)	[isAProced = 1]
  2:	proc  0 (A:1)       terminates
2 processes created

LTLでの確認

上記のモデルではプロセスA,Bのどちらが先に実行されても最終的にisAProced == true && isBProced == trueが成立します。成立する性質の否定を使って、プロセスAから実行される場合とプロセスBから実行される場合を検出させたいと思います。

検証式

以下の検証式をモデルに追加します。

検証したい性質
ltl a01 { <>[](isAProced == true && isBProced == true) }
検証したい性質の否定
ltl c01 { !<>[](isAProced == true && isBProced == true) }
実行
検証したい性質の確認
$ spin -run -ltl a01 2pro.pml
pan: ltl formula a01

(Spin Version 6.5.0 -- 17 July 2019)
	+ Partial Order Reduction

Full statespace search for:
	never claim         	+ (a01)
	assertion violations	+ (if within scope of claim)
	acceptance   cycles 	+ (fairness disabled)
	invalid end states	- (disabled by never claim)

State-vector 28 byte, depth reached 9, errors: 0
       12 states, stored (21 visited)
       13 states, matched
       34 transitions (= visited+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.001	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


unreached in proctype A
	(0 of 2 states)
unreached in proctype B
	(0 of 2 states)
unreached in claim a01
	_spin_nvr.tmp:10, state 13, "-end-"
	(1 of 13 states)
unreached in claim c01
	_spin_nvr.tmp:19, state 10, "(((isAProced==1)&&(isBProced==1)))"
	_spin_nvr.tmp:21, state 13, "-end-"
	(2 of 13 states)

pan: elapsed time 0 seconds
検証したい性質がどのように成り立ったかの確認

実行してみるとエラーが3件検出されます。私の理想としては、2件の検出なのですがどの様な式にすればよいのかわかりませんでした。

$ spin -run -ltl c01 -c0 -e 2pro.pml
pan: ltl formula c01
pan:1: acceptance cycle (at depth 8)
pan: wrote 2pro.pml1.trail
pan: wrote 2pro.pml2.trail
pan: wrote 2pro.pml3.trail

(Spin Version 6.5.0 -- 17 July 2019)
	+ Partial Order Reduction

Full statespace search for:
	never claim         	+ (c01)
	assertion violations	+ (if within scope of claim)
	acceptance   cycles 	+ (fairness disabled)
	invalid end states	- (disabled by never claim)

State-vector 28 byte, depth reached 9, errors: 3
        9 states, stored (11 visited)
        7 states, matched
       18 transitions (= visited+matched)
        0 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


unreached in proctype A
	(0 of 2 states)
unreached in proctype B
	(0 of 2 states)
unreached in claim c01
	_spin_nvr.tmp:21, state 13, "-end-"
	(1 of 13 states)

pan: elapsed time 0 seconds

エラートレイルの確認

プロセスBの処理が先に実行されるケース
$ spin -t1 -p 2pro.pml
ltl a01: <> ([] (((isAProced==1)) && ((isBProced==1))))
ltl c01: ! (<> ([] (((isAProced==1)) && ((isBProced==1)))))
starting claim 3
Never claim moves to line 15	[(1)]
  2:	proc  1 (B:1) 2pro.pml:11 (state 1)	[isBProced = 1]
  4: proc 1 terminates
  6:	proc  0 (A:1) 2pro.pml:6 (state 1)	[isAProced = 1]
Never claim moves to line 14	[(((isAProced==1)&&(isBProced==1)))]
  8: proc 0 terminates
  <<<<<START OF CYCLE>>>>>
Never claim moves to line 19	[(((isAProced==1)&&(isBProced==1)))]
spin: trail ends after 10 steps
#processes: 0
		isAProced = 1
		isBProced = 1
 10:	proc  - (c01:1) _spin_nvr.tmp:18 (state 10)
2 processes created

$ spin -t2 -p 2pro.pml
ltl a01: <> ([] (((isAProced==1)) && ((isBProced==1))))
ltl c01: ! (<> ([] (((isAProced==1)) && ((isBProced==1)))))
starting claim 3
Never claim moves to line 15	[(1)]
  2:	proc  1 (B:1) 2pro.pml:11 (state 1)	[isBProced = 1]
  4: proc 1 terminates
  6:	proc  0 (A:1) 2pro.pml:6 (state 1)	[isAProced = 1]
Never claim moves to line 14	[(((isAProced==1)&&(isBProced==1)))]
  8: proc 0 terminates
Never claim moves to line 19	[(((isAProced==1)&&(isBProced==1)))]
  <<<<<START OF CYCLE>>>>>
spin: trail ends after 10 steps
#processes: 0
		isAProced = 1
		isBProced = 1
 10:	proc  - (c01:1) _spin_nvr.tmp:18 (state 10)
2 processes created
プロセスAの処理が先に実行されるケース
$ spin -t3 -p 2pro.pml
ltl a01: <> ( (((isAProced==1)) && ((isBProced==1))))
ltl c01: ! (<> ( (((isAProced==1)) && ((isBProced==1)))))
starting claim 3
Never claim moves to line 15	[(1)]
  2:	proc  0 (A:1) 2pro.pml:6 (state 1)	[isAProced = 1]
  4:	proc  1 (B:1) 2pro.pml:11 (state 1)	[isBProced = 1]
Never claim moves to line 14	[(((isAProced==1)&&(isBProced==1)))]
  6: proc 1 terminates
Never claim moves to line 19	[(((isAProced==1)&&(isBProced==1)))]
  8: proc 0 terminates
spin: trail ends after 8 steps
#processes: 0
		isAProced = 1
		isBProced = 1
  8:	proc  - (c01:1) _spin_nvr.tmp:18 (state 10)
2 processes created

トライ&エラー

上記の結果が得られるまで、あ〜だ。こ〜だ。とトライ&エラーを繰り返しました。今後の役に立ちそうだったので残しておきます。

常に失敗させる

以下の様なLTLを記述して常に失敗させました。結果としては、18のエラーが検出されました。中身を確認すると、確かに欲しい結果が入っていたので、これを元に検証したい性質でエラーが出るように進めました。

/* errors: 18 */
ltl l01 { false }

改良1

ゴールにすこし近づくように以下を記述しました。なぜ、エラー検出数が異なるのかは、まだ理解できていません。

/* errors: 6 */
ltl l02 { !<>(isAProced == true) }

/* errors: 7 */
ltl l03 { !<>(isBProced == true) }

改良2

さらにゴールに近づけました。
これに[]を追加したものが最初に紹介した検証式となります。

/* errors: 5 */
ltl l04 { !<>(isAProced == true && isBProced == true) }

Linux系:manコマンド使ってみよう!

私は、普段の開発はほぼLinuxで行っています。
その際に、「コマンドのオプションなんだっけ?」とか、「関数の引数なんだっけ?」と思うことがあります。

インターネットで調べるのも有りですが、ぱっと調べられるので使えるようになっていると便利です。

manコマンドでmanを調べる

manコマンドでmanについても調べることができます。

$ man man

以下はページャで出力されます。

MAN(1)                             マニュアルページユーティリティー                             MAN(1)

名前
       man - an interface to the system reference manuals

書式
       man [man options] [[section] page ...] ...
       man -k [apropos options] regexp ...
       man -K [man options] [section] term ...
       man -f [whatis options] page ...
       man -l [man options] file ...
       man -w|-W [man options] page ...

説明
       man  is  the  system's manual pager.  Each page argument given to man is normally the name of a
       program, utility or function.  The manual page associated with each of these arguments is  then
       found  and  displayed.  A section, if provided, will direct man to look only in that section of
       the manual.  The default action is to search in all  of  the  available  sections  following  a
       pre-defined order (see DEFAULTS), and to show only the first page found, even if page exists in
       several sections.

       次の表はマニュアルの section 番号およびその section に含まれるページの種類を示します。

       1   実行プログラムまたはシェルコマンド
       2   システムコール (カーネルが提供する関数)
       3   ライブラリー呼び出し (プログラムライブラリーに含まれる関数)
       4   Special files (usually found in /dev)
       5   File formats and conventions, e.g. /etc/passwd
       6   ゲーム
       7   Miscellaneous (including macro packages and conventions), e.g. man(7), groff(7)
       8   システム管理コマンド (通常は root 用)
       9   カーネルルーチン [非標準]

       マニュアルページ page は複数の節で構成されます。
:

私はセクション1,2,3をよく見ます。セクション1を見ていると、よく使っているコマンドでも知らないオプションについて記述があったり、別の機会に使えそうなオプションの記述があったりと発見があります。

調べたい内容が出力されない場合

例えばですが、printfについて調べようとするとセクション1のprintfコマンドの内容が出力されます。

$ man printf
PRINTF(1)                                    User Commands                                   PRINTF(1)

NAME
       printf - format and print data

SYNOPSIS
       printf FORMAT [ARGUMENT]...
       printf OPTION

DESCRIPTION
       Print ARGUMENT(s) according to FORMAT, or execute according to OPTION:
:

printfコマンドについて調べる場合はこれでよいのですが、printf関数について調べたい場合はライブラリーのセクション3を指定して調べます。

$ man 3 printf
PRINTF(3)                              Linux Programmer's Manual                             PRINTF(3)

NAME
       printf, fprintf, dprintf, sprintf, snprintf, vprintf, vfprintf, vdprintf, vsprintf, vsnprintf -
       formatted output conversion

SYNOPSIS
       #include <stdio.h>

       int printf(const char *format, ...);
       int fprintf(FILE *stream, const char *format, ...);
       int dprintf(int fd, const char *format, ...);
       int sprintf(char *str, const char *format, ...);
       int snprintf(char *str, size_t size, const char *format, ...);
:

どのセクションにあるかよくわからない場合は-kオプションが助けになると思います。

$ man -k printf
Printf (3o)          - Formatted output functions.
asprintf (3)         - print to allocated string
dprintf (3)          - formatted output conversion
fprintf (3)          - formatted output conversion
fwprintf (3)         - formatted wide-character output conversion
printf (1)           - format and print data
printf (3)           - formatted output conversion
set_matchpathcon_printf (3) - set flags controlling the operation of matchpathcon or matchpathcon_inde...
snprintf (3)         - formatted output conversion
sprintf (3)          - formatted output conversion
Stdlib.Printf (3o)   - no description
swprintf (3)         - formatted wide-character output conversion
vasprintf (3)        - print to allocated string
vdprintf (3)         - formatted output conversion
vfprintf (3)         - formatted output conversion
vfwprintf (3)        - formatted wide-character output conversion
vprintf (3)          - formatted output conversion
vsnprintf (3)        - formatted output conversion
vsprintf (3)         - formatted output conversion
vswprintf (3)        - formatted wide-character output conversion
vwprintf (3)         - formatted wide-character output conversion
wprintf (3)          - formatted wide-character output conversion
XtAsprintf (3)       - memory management functions

shell:天気情報をWebAPIで取得してみる

Twitter APIを使ってみようと思ったのですが、認証やら何やらが必要になりそうでした。これまでWebAPIは使ったことがなかったので、ひつまず手に届きそうな天気情報を取得するものから試してみました。

お天気Webサービス仕様

手に届きそうなものを探していたらちょうど「お天気Webサービス仕様」(http://weather.livedoor.com/weather_hacks/webservice)というものを見つけました。

横浜の天気情報をリクエストする

説明を読むと同ページからリンクしている「全国の地点定義表(RSS)」に記載されている一次細分区のidを使って天気情報をリクエストできるようでした。
試しに、横浜(140010)を使ってリクエストを投げてみます。

リクエストを送信する
$ GET http://weather.livedoor.com/forecast/webservice/json/v1?city=140010
{"pinpointLocations":[{"link":"http://weather.livedoor.com/area/forecast/1410000","name":"\
:

JSONデータから必要情報を得る

取得した情報から自分が欲しい情報を抽出します。
欲しい情報は予報(forecasts)の以下です。

dateLabel
date
telop

jqコマンドでの抽出
$ GET http://weather.livedoor.com/forecast/webservice/json/v1?city=140010 | jq -r '.forecasts | .[] | [ .dateLabel, .date, .telop]'
[
  "今日",
  "2020-06-11",
  "雨"
]
[
  "明日",
  "2020-06-12",
  "曇のち雨"
]
[
  "明後日",
  "2020-06-13",
  "曇時々雨"
]

整形

好みの形に整形します。

$ GET http://weather.livedoor.com/forecast/webservice/json/v1?city=140010 | jq -r '.forecasts | .[] | [ .dateLabel, .date, .telop] | @sh' | sed s/\'//g
今日 2020-06-11 雨
明日 2020-06-12 曇のち雨
明後日 2020-06-13 曇時々雨

スクリプト化(weather.sh)

#!/bin/bash
#-----------------------------------------
# 天気情報取得スクリプト
#-----------------------------------------

if [ $# -eq 0 -o _"$1" = _"-h" ]; then
  echo Usage : $(basename $0) 一次細分区ID
  echo 例 東京 : $(basename $0) 130010
  echo 例 横浜 : $(basename $0) 140010
  exit 1;
fi

city=$1
url=http://weather.livedoor.com/forecast/webservice/json/v1?city=${city}

#-----------------------------------------
# 一次細分区で指定した天気情報を得る。
#-----------------------------------------
GET ${url}                               |
#-----------------------------------------
# JSONから欲しい情報を得る。
#-----------------------------------------
jq -r '
    #-----------------------------
    # 予報部分の抽出
    #-----------------------------
    .forecasts                   |
    #-----------------------------
    # 配列の全要素を抽出(今日・明日・明後日)
    #-----------------------------
    .[]                          |
    #-----------------------------
    # 必要情報を抽出
    #-----------------------------
    [ .dateLabel, .date, .telop] |
    @sh'                                 |
#-----------------------------------------
# クォート(')を除外する。
#-----------------------------------------
sed s/\'//g

実行

$ ./weather.sh 140010
今日 2020-06-11 雨
明日 2020-06-12 曇のち雨
明後日 2020-06-13 曇時々雨