定義 4. 1. 原子隠蔽定数 (atomic state constant)
5.4 安全性の検証
5.4.3 表明 5.1 の検証
モジュール
CLAIM5-1
は，モジュールPROOF
で定義した帰納法を用いて，表明5.1
を 検証するためのモジュールである．このモジュールを図
5.2
に示す．図5.2 (1)
で示した記述は，表明5.1
を論理和標準形 に変換したものである．(2)
は基底段階に関する議論である．次に，帰納法の仮定を隠蔽定数で表現する．論理和標準形に変換した表明
5.1
は，3
つ の節から構成されている．しかし，最初の節は状態に関する言明でないため，合成隠蔽定 数で表現することができない．最初の節には，別途場合分けを与えることとし(
後述)
， 残りの2
つの節について，それらを合成隠蔽定数で表現したものを，図5.2 (3)
に示すよ うに記述した．最後に，帰納段階についての検証を，hyp2
とhyp3
の各場合について行 うことを，図5.2 (4)
に示すように記述した．しかし，表明の最初の節についての場合分 けが行われていない．そこで，図5.2 (5)
と(6)
に示す証明譜を記述し，場合分けを行っ た．(5)
はc1 = c2
の場合について，(6)
はc1 = c2
でない場合について検証する．(5)
の簡約結果はtrue
であり，具体的な結果の記述については割愛する．(6)
の簡約結果を，5.4
安全性の検証51
mod CLAIM5-1 { ...
eq IND = FORALL-ACTION (hyp2 o c2t) | FORALL-ACTION (hyp2 o ~c2t) | FORALL-ACTION (hyp3 o c1t) | FORALL-ACTION (hyp3 o ~c1t) . }
open CLAIM5-1
eq (c1 = c2) = false . red INI | IND . close
-- reduce in %CLAIM1 : INI | IND}
MOVE(c1,t1,c1t1 o gt1',~c1t o c2t)
| MOVE(c2,t2,c2t2 o gt2',~c2t o c1t)
| true : Bool (0.000 sec for parse,
854 rewrites(0.060 sec), 2972 matches)}
red p(move(c1,t1,c1t1 o gt1' o ~c1t o c2t)) . -- reduce in %CLAIM1 :
p(move(c1,t1,c1t1 o gt1' o ~c1t o c2t)) next(pos(c1,c1t1 o gt1' o ~c1t o c2t)) = t xor true : Bool (0.000 sec for parse,
52 rewrites(0.000 sec), 212 matches)
(1) 帰納段階に関する検証指示
(2)c1 ≠ c2 の場合の検証スクリプト
(3) (2)の簡約結果
(4) (a) の場合について，簡約指示 (5) (4)の簡約結果
(a)(b)
図
5.3:
場合分けを追加したモジュールCLAIM5-1
図
5.2 (7)
に示す．(7)
では，2
つの場合について，簡約が停止している．そこで，
hyp2
とhyp3
の各場合について，より詳細な場合分けを試みる．hyp2
につい て，hyp3
で使用している~c2t
とその否定c2t
について場合分けを行う．hyp3
につい ても，同様の場合分けを行う．この場合分けを追加したモジュールCLAIM5-1
を，図5.3
に示す．図5.3 (1)
で示した帰納段階について，場合分けを追加している．c1 = c2
でない場合について検証する証明譜(
図5.3 (2))
を用いて，再度簡約を行った結果を図
5.3 (3)
に示す．依然として検証は完了しないが，この結果からhyp2 o ~c2t
と
hyp2 o ~c1t
の各場合については，検証が成功したことが読みとれる．ここで，検証が成功しない個々の場合
(a)
と(b)
について，簡約を試みる．(a)
に関して簡約を 行うコマンドを図5.3 (4)
に，その結果を図5.3 (5)
に示す．この結果は，列車c1
がmove(c1,t1,S)
によって移動した区間(
つまりt1’)
とt
の関係が不明であるため，簡 約が停止したことを意味している．つまり，t1’ = t
について場合分けが必要と判明し た．(b)
でも同様の議論により，t2’ = t
について場合分けが必要である．CLAIM5-1
において，これらの場合分けを行うため，使い捨ての原始隠蔽定数t1’eqt
，~t1’eqt
，t2’eqt
および~t2’eqt
を定義する．これらを使いhyp2 o c2t
とhyp3 o c1t
の場合について，さらに詳細な場合分けを行う．このようにして書き換えたモジュール
CLAIM5-1
を図5.4
に示す．図5.4 (1)
において，4
つの原始隠蔽定数を追加し，図5.4 (2)
において，追加した原始隠蔽定数を用いて場合52
第5
章 複線区間の鉄道信号システムmod CLAIM5-1 {
ops t1'eqt ~t1'eqt : -> Atom ops t2'eqt ~t2'eqt : -> Atom
ceq (next(pos(c1, ( t1'eqt o C:Case))) = t) = true if comp( t1'eqt, C) .
ceq (next(pos(c1, (~t1'eqt o C:Case))) = t) = false if comp(~t1'eqt, C) .
ceq (next(pos(c2, ( t2'eqt o C:Case))) = t) = true if comp( t2'eqt, C) .
ceq (next(pos(c2, (~t2'eqt o C:Case))) = t) = false if comp(~t2'eqt, C) .
eq tbl ( t1'eqt) = ~t1'eqt . eq tbl (~t1'eqt) = t1'eqt . eq tbl ( t2'eqt) = ~t2'eqt . eq tbl (~t2'eqt) = t2'eqt .
eq IND = FORALL-ACTION (hyp2 o c2t o t1'eqt) | FORALL-ACTION (hyp2 o c2t o ~t1'eqt) | FORALL-ACTION (hyp2 o ~c2t)
| FORALL-ACTION (hyp3 o c1t o t2'eqt) | FORALL-ACTION (hyp3 o c1t o ~t2'eqt) | FORALL-ACTION (hyp3 o ~c1t) . }
open CLAIM5-1
eq (c1 = c2) = false . red INI | IND . close
-- reduce in %CLAIM1 : INI | IND
MOVE(c1,t1,c1t1 o gt1',~c1t o c2t o t1'eqt)
| MOVE(c2,t2,c2t2 o gt2',~c2t o c1t o t2'eqt)
| true : Bool (0.000 sec for parse,
1220 rewrites(0.140 sec), 4727 matches)
(2) 帰納段階に関する検証指示
(3)c1 ≠ c2 の場合の 検証スクリプト (4) (3)の簡約結果 (1) 追加した原始隠蔽定数
図
5.4:
さらに場合分けを追加したモジュールCLAIM5-1
分けを行うように変更されている．
図
5.4 (3)
の証明譜の簡約結果を図5.4 (4)
に示す．~c1t o c2t o t1’eqt
の場合の 検証が成功しない．この場合について簡約を行うと，false
が得られ，表明が崩れている ことがわかる．これを解決するには，補題が必要である．以下に補題5.1
を示す．補題
5.1
任意の状態可能な状態u ∈ Υ
において，任意の列車n
が，同時に任意の区間t ∈ T
に存在するとき，その区間の信号t
は停止信号である．pos n (u) = t ⇒ ¬(green?(num t (u)))
ここでは，この補題が証明できたものとして，議論を続ける
(
補題5.2
を記述したコー ドは，付録B.2.3
に示す)
．~c1t o c2t o t1’eqt
は，列車c2
がt
にいる場合に関す る議論である．さらに，t1’
とt
は等しい場合についての議論である．従って，区間t1’
の信号は，補題
5.1
より停止信号である．同じことが，~c2t o c1t o t2’eqt
について も言える．このため，これらの場合について，t1’
およびt2’
の信号が停止信号である 場合を示す原始隠蔽定数~gt1’
と~gt1’
を加える．帰納段階の議論に補題
5.1
を加えたモジュールCLAIM5-1
を図に示す．また，図5.5
5.4
安全性の検証53
mod CLAIM5-1 {
eq IND = FORALL-ACTION (hyp2 o c2t o t1'eqt o ~gt1') | FORALL-ACTION (hyp2 o c2t o ~t1'eqt) | FORALL-ACTION (hyp2 o ~c2t)
| FORALL-ACTION (hyp3 o c1t o t2'eqt o ~gt2') | FORALL-ACTION (hyp3 o c1t o ~t2'eqt) | FORALL-ACTION (hyp3 o ~c1t) . }
open CLAIM5-1
eq (c1 = c2) = false . red INI | IND . close
-- reduce in %CLAIM1 : INI | IND true : Bool
(0.000 sec for parse,
865 rewrites(0.140 sec), 3300 matches)
(1) 帰納段階に関する 検証指示
(2)c1 ≠ c2 の場合の 検証スクリプト (3) (2)の簡約結果
図
5.5:
最終的なモジュールCLAIM5-1
(2)
の証明譜を用いて簡約した結果を図5.5 (3)
に示す．以上の議論により，すべての場 合についてtrue
が得られ，表明5.1
が成立することが示された．¤
54
第 6 章
単線区間の鉄道信号システム
本章では，より近代的な鉄道信号システムを取り上げ，