spin, panコマンドのヘルプとページャ(less)

SPINを勉強しているのですが、spin, 検証器(pan)コマンドのオプションが覚えられずに頻繁にヘルプを参照しています。

私の環境ではヘルプを出力すると作業ターミナルの画面から溢れるのでページャを通して確認することが多いです。ページャを通すと検索機能を使えるため個人的にはとても気に入って使っています。

今回は以下の2つを紹介したいと思います。

使用しているページャはlessです。

$ echo $SHELL
/bin/bash

$ spin --help | less

適当なモデルを記述して検証の生成からコンパイルを行います。

$ cat p.pml 
bool b = true;

active proctype p()
{
  if
  :: b = true
  :: b = false
  fi
}
$ spin -a p.pml 
$ gcc -w pan.c -o pan

以下のようにヘルプを見ようとしても画面出力が流れます。

$ ./pan -h | less

これはヘルプの標準エラーに出力されているためです。

$ ./pan -h |& less

ページャに慣れておくと1画面を超える出力をゆっくり確認したい場合に役立ちますので、個人的にはおすすめです。以下のようなケースでよく使用します。

$ cat *.log | less <-- ログファイルをまとめて確認
$ cat *.log | 各種フィルタコマンド | less <-- 出力結果を1画面ずつ確認

プログラミングなどなど