電気ポットの「企画要求仕様」（リスト1）を題材にします。以下の5項目の要求が書かれています。
リスト1 企画要求仕様
PR01: 電気ポットの容量は2リットルとし、10度Cから沸騰するまでの時間は、15分以内とする。
PR02: 電源コンセントをつなぐと、直ちに作動し、ヒータで加熱を始め、沸騰に達したら、90度Cに保温する。
PR03: 再沸騰ボタンが押されたら、再沸騰を始める。
PR04: 水が加えられ、温度が低下したら、再沸騰を始める。
PR05: 保温中であれば、お湯を注ぐことができる。
分析者は、5条項ポットの「企画要求仕様」を読んで、直接、SPINのモデル（リスト2）を書きました。なお、分析者は以前にEvent-Bのモデルを書いていたため、定数の名前などはEvent-Bと共通になっています。
リスト2 SPINのモデル
mtype = {
NO_POWER_SUPPLY, /* 電源が供給されていない。 */
HEAT_UNTIL_BOIL, /* 沸騰するまで加熱する。 */
KEEP_TEMPERATURE, /* 保温する。 */
DISCHARGE_HOT_WATER, /* お湯を注ぐ。 */
};
mtype mode = NO_POWER_SUPPLY;
active proctype pot () {
do
/* ユーザーが電源コンセントをつないだ。[PR02] */
:: mode == NO_POWER_SUPPLY -> mode = HEAT_UNTIL_BOIL
/* 沸騰した。[PR02] */
:: mode == HEAT_UNTIL_BOIL -> mode = KEEP_TEMPERATURE
/* ユーザーがポットに水を注いだ。[PR04] */
/* ユーザーがポットにお湯を注ぐことを要求した。[PR05] */
:: mode == KEEP_TEMPERATURE -> mode = DISCHARGE_HOT_WATER
/* ユーザーがポットにお湯を注ぐことを止めた。[PR05] */
:: mode == DISCHARGE_HOT_WATER -> mode =KEEP_TEMPERATURE
od;
}
続いて、論理式（リスト3）を以下のように定義しました。
リスト3 論理式の定義
#define p1 (mode == NO_POWER_SUPPLY)
#define p2 (mode == HEAT_UNTIL_BOIL)
#define p3 (mode == KEEP_TEMPERATURE)
#define p4 (mode == DISCHARGE_HOT_WATER)
最後に、時相論理を用いた検査を行いました。ここでは、状態に「袋小路」がないこと、すなわち、すべての状態からすべての状態に（必要ならば他の状態を経由して）遷移できることを示すことにしました。
時相論理の細かい説明は省きますが、最初の時相論理式（リスト4）は、「状態p1（NO_POWER_SUPPLY）から状態p2（HEAT_UNTIL_BOIL）へは遷移できない」ことを表します。この時相論理式をSPINで検査すると、「Not valid」というメッセージが出て、「反例」が出力されます。ここでは、状態p1からp2に遷移できることを示したいので、検査結果が「Not valid」なのは、これで正しいです。さらに、出力された「反例」を見ると、実際にどのような状態遷移が行われたのかを見ることができます。
リスト4 p1からp2への遷移が不可能であることを表す時相論理式
[] (p1- > [] ! p2)
さらに、p2からp3、p3からp4、p4からp1への遷移について、それぞれ時相論理式を作りました（リスト5）。もし4個の状態を1周するような状態遷移が可能であれば、すべての状態からすべての状態に遷移できることが分かります。
リスト5 p2からp3、p3からp4、p4からp1への遷移が不可能であることを表す時相論理式
[] (p2-> [] ! p3)
[] (p3-> [] ! p4)
[] (p4-> [] ! p1)
しかしながら、このうち最後の時相論理式は検査結果が「Valid」になります。これは、p4からp1に遷移することはできない、ということが証明されたということです。
実際、もとのモデル（リスト2）を見てみると、他の状態から状態p1（NO_POWER_SUPPLY）に遷移する記述がありません。すなわち、電源を入れる記述はあっても、電源を切る記述がありません。状態p1（NO_POWER_SUPPLY）は、出ることはできても入ることはできない袋小路になっています。
かわりに、状態p4から状態p2への遷移について調べる（リスト6）ことで、状態p2, p3, p4には袋小路がないことを示しました。
リスト6 p4からp2への遷移が不可能であることを表す時相論理式
[] (p4-> [] ! p2)
