killするとENDに到達する性質
ogasawara
ちょっと思い立って、下記のような簡単なプロセス実行の状態遷移モデルを記述してみました。
open util/ordering[Step]
enum State { INIT, RUN, SLEEP, EXITING, END } // プロセスの状態
enum Command { START, SUSPEND, RESUME, KILL } // プロセス状態を変化させる命令
sig Step {
state : State, // 現在のプロセス状態
command : lone Command // 現在のプロセスに働きかける命令
}
pred allowTrans[ p, n : Step ] { // 許される状態遷移
p.state = INIT and p.command = START => {
n.state = RUN
}
else p.state = RUN and p.command = SUSPEND => {
n.state = SLEEP
}
else p.state = SLEEP and p.command = RESUME => {
n.state = RUN
}
else p.state in RUN + SLEEP and p.command = KILL => {
n.state = EXITING
}
else p.state = EXITING => {
n.state = END and no n.command
}
else p.state = END => {
n.state = END
}
else { // 上記以外は状態が変化しない。
n.state = p.state
}
}
fact {
all x, y : Step | y = x.next => allowTrans[x, y] // 特定の状態遷移のみ許される
first.state = INIT and first.command = START // 初期状態の規定
}
pred show {}
run show
これを実行すると一応遷移規則を満たす色々なインスタンスが得られます。
で、ここからが問題なのですが、「プロセスにkillコマンドを渡すとその後どこかでEND状態に到達する」
という性質を示したいと思って、次のようなpredを書いたのですが
inconsistentだと言われて悩んでいます。
pred killEnd {
// killするとENDに到達するという性質を示したい。
all x : Step | some y : x.^next | x.command = KILL => y.state = END //これは無理??
}
たぶん、どんなに探索範囲を広げても、その範囲が途切れる直前でkillされたプロセスはENDに到達
する前にnextが無くなってしまうために、この性質は満たされないのかなと推測しています。
こういった性質はどう検証するのがいいのでしょうか？そもそもorderingを使うのではなく、別のやり方が
あるのでしょうか？
なにかご意見があれば頂戴できますと幸いです。よろしくお願い致します。
T.Fujikura
START前にKILLするとRUNのままになるのではないですか?
モデル検査ツールを使えば分かると思います。
Masahiro Sakai
2011年10月7日0:37 ogasawara <ogas...@itpl.co.jp>:
> という性質を示したいと思って、次のようなpredを書いたのですが
> inconsistentだと言われて悩んでいます。
>
> pred killEnd {
> // killするとENDに到達するという性質を示したい。
> all x : Step | some y : x.^next | x.command = KILL => y.state = END
> //これは無理??
> }
>
> たぶん、どんなに探索範囲を広げても、その範囲が途切れる直前でkillされたプロセスはENDに到達
> する前にnextが無くなってしまうために、この性質は満たされないのかなと推測しています。
killとかを考えなくても、有限の領域では満たせないです。
とりあえず、上の論理式で書きたかったのは、
all x : Step | x.command = KILL => some y : x.^next | y.state = END
ではないでしょうか。
そうすれば、checkはともかくrunはできると思います。
-- 酒井 政裕
Takeo Imai
酒井さんと入れ違いになってしまったのですが、書きかけだったので、送信します（＾＾；
killEndを、次のように書きなおしてやれば、killEndはconsistentになります。
pred killEnd {
all x : Step - last |
some y : x.^next | x.command = KILL => y.state = END
}
元のkillEndの制約は
all x: Step | some y: x.^next | P
という形をしていたのですが、この式は * Pに何が来ようと* 成り立ちません。
なんでかというと、任意のxに、後ろに続くステップの集合 x.^next を要求するからです。
言い方を変えると、xが最終ステップのとき、x.^next は空になります。
で、some y: D | P という式は、D が空の時は常に偽になるんです。
（ D = {y1, y2, ... } のとき、上記の式は P[y1/y] or P[y2/y] or ...と同じ意味です。
ならば、Dが空集合の時はどういう値を持つか、と考えてみてください）
更に、これでrunは通るようになりますが、元々示したかったのは、このような性質が「常に」成り立つこと、だと思います。
なのでアサーションに書きなおすべきだと思いますが、これをそのままアサーションに書きなおしても、通らないです。
アサーションとして成立させるには、次のように書く必要があります。
assert killEnd' {
all x : Step - last - last.prev | some y : x.^next | x.command =
KILL => y.state = END
}
killされてからENDに至るまでには2ステップかかるので、xの範囲を「最終ステップから2ステップ前まで」に限定してやる必要があります。
2011/10/7 T.Fujikura <tofuj...@gmail.com>:
--
IMAI Takeo <takeo...@gmail.com>
T.Fujikura
モデル検査ツールのNuSMVでやってみました。util/ordering[Step]については
知らないので等価な振る舞いになっていない かも知れませんが、Alloyのアプ
ローチと比較すると面白いと思います。
MODULE main
VAR
state: { ini, RUN, SLEEP, EXITING, END };
cmd: { START, SUSPEND, RESUME, KILL };
ASSIGN
init(state) := ini;
next(state) := case
state = ini & cmd in { START } : RUN;
state = RUN & cmd in { SUSPEND } : SLEEP;
state = SLEEP & cmd in { RESUME } : RUN;
state in {RUN, SLEEP} & cmd in { KILL } : EXITING;
state = EXITING : END;
TRUE:state;
esac;
INITは使えないのでiniにしています。これで振る舞いを記述して
LTLSPEC G (cmd = KILL -> F state = END)
これで満たすべき性質を記述して検査します。「KILLしたら何時かENDになるこ
とが常に成立する」と言う意味です。
結果は、
-- specification G (cmd = KILL -> F state = END) is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample
-> State: 1.1 <-
state = ini
cmd = SUSPEND
-> State: 1.2 <-
cmd = KILL
-> State: 1.3 <-
cmd = START
-- Loop starts here
-> State: 1.4 <-
state = RUN
-> State: 1.5 <-
の様になって、RUN状態になる前にKILLしても捨てられてしまう、RUNのまま無限
ループが可能なので成立しない場合があることが分かりま す。
Takeo Imai
2011/10/7 T.Fujikura <tofuj...@gmail.com>:
> 藤倉です
> モデル検査ツールのNuSMVでやってみました。util/ordering[Step]については
> 知らないので等価な振る舞いになっていない かも知れませんが、Alloyのアプ
> ローチと比較すると面白いと思います。
(snip)
> 結果は、
(snip)
> の様になって、RUN状態になる前にKILLしても捨てられてしまう、RUNのまま無限
> ループが可能なので成立しない場合があることが分かりま す。
元のAlloy記述では
first.state = INIT and first.command = START // 初期状態の規定
のところで初期コマンドもSTARTに指定されているので、この反例は起こりえないです。
初期コマンドの指定を消して（上の "and first ..." 以下をコメントアウトして）、その上でさっき私が書いた
assert killEnd {
all x : Step - last - last.prev | some y : x.^next | x.command =
KILL => y.state = END
}
check killEnd for 10
というアサーションを検査してみると、（RUN無限とは限りませんが）同様の反例が得られます。
添付画像は、得られた反例の1つです。
今井
> MODULE main
> VAR
> state: { ini, RUN, SLEEP, EXITING, END };
> cmd: { START, SUSPEND, RESUME, KILL };
>
> ASSIGN
> init(state) := ini;
> next(state) := case
> state = ini & cmd in { START } : RUN;
> state = RUN & cmd in { SUSPEND } : SLEEP;
> state = SLEEP & cmd in { RESUME } : RUN;
> state in {RUN, SLEEP} & cmd in { KILL } : EXITING;
> state = EXITING : END;
> TRUE:state;
> esac;
>
> INITは使えないのでiniにしています。これで振る舞いを記述して
>
> LTLSPEC G (cmd = KILL -> F state = END)
>
> これで満たすべき性質を記述して検査します。「KILLしたら何時かENDになるこ
> とが常に成立する」と言う意味です。
>
--
IMAI Takeo <takeo...@gmail.com>
T.Fujikura
init(cmd):= START;
を追加したら
-- specification G (cmd = KILL -> F state = END) is true
パスしました。
Yamamoto Koji 山本晃治
Alloy も NuSMV も使い始めなので，楽しく読んでいます．
> >>> first.state = INIT and first.command = START // 初期状態の規定
alloy の記述でこうなっているので，最初の Step での cmd を START に
しておくと等価な振る舞いな気がしますね．
ASSIGN で
init(cmd) := START;
の行を追加するか，
LTLSPEC cmd = START -> G (cmd = KILL -> F state = END)
でモデル検査するか，でしょうか．
At Fri, 07 Oct 2011 08:41:56 +0900,
Satoshi Ogasawara
多くのご回答を頂いておりびっくりしました。皆様の詳しい解説やNuSMVのコードまで
拝見できてとても勉強になります。ありがとうございます。
(2011/10/07 8:00), Takeo Imai wrote:
> 元のkillEndの制約は
> all x: Step | some y: x.^next | P
> という形をしていたのですが、この式は * Pに何が来ようと* 成り立ちません。
> なんでかというと、任意のxに、後ろに続くステップの集合 x.^next を要求するからです。
酒井さんからもご指摘頂きましたが、lastに対してはx.nextが空になるのでそもそもこ
の書き方がダメなのですね。気づきませんでした。もしかしたら、私だけでなく、初心
者が気づきにくい点かもしれません。
> アサーションとして成立させるには、次のように書く必要があります。
> assert killEnd' {
> all x : Step - last - last.prev | some y : x.^next | x.command =
> KILL => y.state = END
> }
上記assertでうまくいきました。
検索範囲の最後の部分が問題になるという予想はあったのですが、all x : Stepか
らlastとlast.prevを引き算するという操作に思い至りませんでした。また、常に
成り立って欲しい性質なのでアサーションとすべきという点も勉強になります。
精進します。ありがとうございます。
---
小笠原@ITPL
Satoshi Ogasawara
(2011/10/07 8:41), T.Fujikura wrote:
> モデル検査ツールのNuSMVでやってみました。util/ordering[Step]については
> 知らないので等価な振る舞いになっていない かも知れませんが、Alloyのアプ
> ローチと比較すると面白いと思います。
>
> MODULE main
> VAR
> state: { ini, RUN, SLEEP, EXITING, END };
> cmd: { START, SUSPEND, RESUME, KILL };
>
> ASSIGN
> init(state) := ini;
> next(state) := case
> state = ini& cmd in { START } : RUN;
> state = RUN& cmd in { SUSPEND } : SLEEP;
> state = SLEEP& cmd in { RESUME } : RUN;
> state in {RUN, SLEEP}& cmd in { KILL } : EXITING;
> state = EXITING : END;
> TRUE:state;
> esac;
コードまで示して頂いてありがとうございます。NuSMVは初めてなのですが、
モデル検査ツールはもともと状態遷移を念頭に置いているからか、シンプル
に書けていて魅力的に思いました。
Alloyのようなモデル発見器とモデル検査ツールの使い分け、とても興味深
いです。ぜひ今後勉強していきたいと思います。
---
小笠原@ITPL