maude続き

研究

最近研究活動が滞っている。活を入れねば。

ところでMaudeでは、LTLの検査モジュールが同梱されており、
これをつかってモデル検査をすることができる。
以下はTurorialの写経。

最初に検査したい本体(tutorial例題ではMUTEX)の動作を定義します。

load model-checker.maude

mod MUTEX is
 sorts Name Mode Proc Token Conf .
 subsorts Token Proc < Conf .
 op none : -> Conf [ctor] .
 op __ : Conf Conf -> Conf [ctor assoc comm id: none] .
 ops a b : -> Name [ctor] .
 ops wait critical : -> Mode [ctor] .
 op [_,_] : Name Mode -> Proc [ctor] .
 ops * $ : -> Token [ctor] .
 rl [a-enter] : $ [a, wait] => [a, critical] .
 rl [b-enter] : * [b, wait] => [b, critical] .
 rl [a-exit] : [a, critical] => [a, wait] * .
 rl [b-exit] : [b, critical] => [b, wait] $ .
endm

つぎに、この本体に対するpredicateを定義します
ここではcritical,waitという述語の意味を定義します。
SATISFACTIONというのはmodel-checker.maudeの中にあります。

mod MUTEX-PREDS is
 protecting MUTEX .
 including SATISFACTION .
 subsort Conf < State .
 op crit : Name -> Prop .
 op wait : Name -> Prop .
 var N : Name .
 var C : Conf .
 var P : Prop .
 eq [N, critical] C |= crit(N) = true .
 eq [N, wait] C |= wait(N) = true .
 eq C |= P = false [owise] .
endm

よいよモデル検査部の作成。初期状態を定義します。

mod MUTEX-CHECK is
 protecting MUTEX-PREDS .
 including MODEL-CHECKER .
 including LTL-SIMPLIFIER .
 ops initial1 initial2 : -> Conf .
 eq initial1 = $ [a, wait] [b, wait] .
 eq initial2 = * [a, wait] [b, wait] .
endm

そこでa,bともにクリティカルセクション(crit)に入らない
ことを検査します。

Maude> red modelCheck(initial1, [] ~(crit(a) /\ crit(b))) .
reduce in MUTEX-CHECK : modelCheck(initial1, []~ (crit(a) /\ crit(b))) .
rewrites: 22 in 10ms cpu (434ms real) (2200 rewrites/second)
result Bool: true