現在の位置
diff プラグインを使用中
- The added line is THIS COLOR.
- The deleted line is THIS COLOR.
- Go to システム検証例.
- Deleting diff of システム検証例
#contents
*エレベーターモデルの検証 [#af907509]
pn(1).//乗客の数
fn(2).//フロアの数
//フロアの生成
fn(F) :- F0=F-1,F>0 | fn(F0),
{ f(F0),btn(false).
//乗客の出入り
p,elv{open(1),$p} :- elv{p,open(1),$p}.
elv{p,open(1),$p} :- p,elv{open(1),$p}.
}.
//乗客の生成
pn(P),{ f(F),$p,@p } :- P0=P-1,P>0,int(F) | pn(P0),{ p,f(F),$p,@p }.
//エレベーターの生成
pn(0),fn(0),{ f(F),$p,@p } :- int(F) | { elv{open(1),act(null),to(0)},f(F),$p,@p }.
//乗客の動作
//フロアにいる乗客がボタンを押す
{ p,btn(false),$p,@p } :- { p,btn(true),$p,@p }.
//エレベーター中にいる乗客がボタンを押す
{ elv{p,to(0),$q[]},$p1[],@p1 },{ f(F),$p2[],@p2 }
:- int(F) | { elv{p,to(F),$q[]},$p1[],@p1 },{ f(F),$p2[],@p2 }.
//エレベーターの動作
//エレベーターのドアを閉める
{ elv{open(Op),act(close),$q},$p,@p } :- int(Op) | { elv{open(0),act(null),$q},$p,@p }.
//エレベーターのドアをあける
{ elv{open(Op),act(open),$q},$p,@p } :- int(Op) | { elv{open(1),act(null),$q},$p,@p }.
//エレベーターの移動
{ elv{act(move(M)),$q[] },$p1[],@p1 },{ f(F),$p2[],@p2 }
:- M=:=F | { $p1[],@p1 },{ elv{act(null),$q[]},f(F),$p2[],@p2 }.
//エレベーターの不移動
{ f(F),elv{act(move(M)),$q[] },$p[],@p }
:- F=:=M | { f(F),elv{act(null),$q[]},$p[],@p }.
//コントローラー
cnt(null).
//ドアを閉じる命令を送信(エレベーター内から受信)
cnt(null),{ elv{act(null),to(T),$q[]},$p[],@p }
:- int(T) | cnt(move(T)),{ elv{act(close),to(T),$q[]},$p[],@p }.
//ドアを閉じる命令を送信(フロアのボタンから受信)
cnt(null),{ f(F),btn(true),$p1[],@p1 },{ elv{act(null),$q[]},$p2[],@p2 }
:- int(F) | cnt(move(F)),{ f(F),btn(true),$p1[],@p1 },{ elv{act(close),$q[]},$p2[],@p2 }.
//移動命令を送信
cnt(move(F)),{ elv{act(null),$q[]},$p[],@p }
:- int(F) | cnt(end),{ elv{act(move(F)),$q[]},$p[],@p }.
//ドアを開く命令を送信
cnt(end),{ btn(B),elv{act(null),to(T),$q[]},$p[],@p }
:- unary(B),int(T) | cnt(null),{ btn(false),elv{act(open),to(0),$q[]},$p[],@p }.
**検証項目 [#h776fbf4]
「エレベーターはドアを開けたまま動くことはない」
シンボル定義：p = { elv{open(1),act(move(M)),$q},$p,@p } :- int(M)
仕様：!<>p
モデル検査をすると、このモデルではそのようなことがないことが分かる。
CENTER:&ref(./elv.jpg);
*Sliding Window Protocolの検証 [#sca04e85]
{
wSize(2). // ウィンドウサイズ
nMAX(3). // 再送処理などの制御に利用するナンバーnの上限値
idMAX(3). // 送信データの正当さをチェックするidの上限値
error(false). // エラー検出フラグ
sender{ n(0), nextId(0), sucId(0), c(0) }. // データ送信者
ss=rr. // データが通る通信路
rs=sr. // ACKが通る通信路
receiver{ n(0), expId(0) }. // データ受信者
// 送信者 : データの送信 sender -> [data]
sd@@ sender{ n(N), nextId(ID), sucId(SucID), c(C) }, nMAX(NMAX), idMAX(IDMAX), wSize(W), ss=SC
:- C<W, C_=C+1, DN=(N+C) mod NMAX, ID_=(ID+1) mod IDMAX, int(SucID)
| sender{ n(N), nextId(ID_),sucId(SucID), c(C_)}, nMAX(NMAX), idMAX(IDMAX), wSize(W), ss=[data(DN,ID)|SC].
// 受信者 : データ受信，ACKの返送(予期していたデータ) [data] -> receiver -> [ack]
rs@@ receiver{ n(N), expId(EID) }, nMAX(NMAX), idMAX(IDMAX), SC=[data(DN,ID)|rr], rs=RC
:- N=:=DN, EID=:=ID, N_=(N+1) mod NMAX, EID_=(EID+1) mod IDMAX
| receiver{ n(N_),expId(EID_)}, nMAX(NMAX), idMAX(IDMAX), SC=rr, rs=[ack(DN)|RC].
// 受信者 : データ受信，データ破棄(受信するはずのデータの消失検出) [data] -> []
ru@@ receiver{ n(N), expId(EID) }, SC=[data(DN,ID)|rr]
:- N=\=DN, int(ID), int(EID), ground(SC)
| receiver{ n(N), expId(EID) }, SC=rr.
// 受信者 : データ受信(正しいメッセージでない) [data] -> receiver -> error
re@@ error(false), receiver{ n(N), expId(EID) }, SC=[data(DN,ID)|rr], rs=RC, sender{ $p[] }
:- N=:=DN, EID=\=ID, ground(SC), ground(RC)
| error(true).
// 送信者 : ACKの受信(予期していたACK) [ack] -> slide
s@@ sender{ n(N), nextId(NextID), sucId(SucID), c(C) }, nMAX(NMAX), idMAX(IDMAX), RC=[ack(ACK)|sr]
:- N=:=ACK, C>0, N_=(N+1) mod NMAX, SucID_=(SucID+1) mod IDMAX, C_=C-1, int(NextID)
| sender{ n(N_),nextId(NextID), sucId(SucID_),c(C_)}, nMAX(NMAX), idMAX(IDMAX), RC=sr.
// 送信者 : ACKの受信，ACKの破棄(データかACKの消失検出) [ack] -> []
r@@ sender{ n(N), nextId(NextID), sucId(SucID), c(C) }, RC=[ack(ACK)|sr]
:- N=\=ACK, int(NextID), int(SucID), int(C)
| sender{ n(N), nextId(NextID), sucId(SucID), c(C) }, RC=sr.
// 送信者 : タイムアウトの検出 [timeout] -> reset
t@@ sender{ n(N), nextId(NextID), sucId(SucID), c(C) }, timeout
:- int(N), int(NextID), int(SucID), int(C)
| sender{ n(N), nextId(SucID), sucId(SucID), c(0) }.
// 通信路 : データ,ACKの消失 [data] -> [], [ack] -> []
ld@@ X=[data(DN,ID)|Y] :- int(DN),int(ID) | X=Y.
la@@ X=[ack(ACK)|Y] :- int(ACK) | X=Y .
}.
// タイムアウトの発生 [] -> [timeout]
o@@ { error(false), $p, @p }/ :- { timeout, error(false), $p, @p }.
**検証項目 [#f18a0c1a]
「データを送信すれば必ず返信が返ってくる」
シンボル定義：
send = { C=data(DN,ID),$p,@p } :- int(DN), int(ID), ground(C) |
ack = { C=ack(ACK),$p,@p } :- int(ACK), ground(C) |
仕様：[](send -> <>ack)
モデル検査をすると「データを送信すると、通信路でデータ消滅してしまうことが繰り返し続く」という経路が見つかる。~
つまり、このモデルでは通信路が途切れている場合、この仕様は満たされないことを示している。
CENTER:&ref(./swp.jpg);
*水差しで量れる水量の検証 [#rbffa19a]
% pot(現在の容量,最大容量)
pot(0,300).
pot(0,700).
% 空にする
pot(X,MAX) :- X>0 | pot(0,MAX).
% 満杯にする
pot(X,MAX) :- X<MAX | pot(MAX,MAX).
% 自分が空になるまで移す
pot(X,MX), pot(Y,MY)
:- X>0, Y<MY, Z=X+Y, Z=<MY
| pot(0, MX), pot(Z, MY).
% 相手が満杯になるまで移す
pot(X,MX), pot(Y,MY)
:- X>0, Y<MY, Z=X-(MY-Y), Z>=0
| pot(Z,MX), pot(MY,MY).
**検証項目 [#hea46506]
「300mlと700mlの水差しから500mlの水が量れる」~
StateViewerの状態検索機能を使うと量れることがわかる。
StateViewerの状態検索機能を使うと量れることがわかる。~
CENTER:&ref(./pot.jpg);
経路を順に見ていくと以下の操作をすることで500mlを量れることが分かる
経路を順に見ていくと以下の操作をすることで500mlを量れる
pot(現在の容量,最大容量)
1. pot(0,300). pot(0,700).
2. pot(0,300). pot(700,700).
3. pot(300,300). pot(400,700).
4. pot(0,300). pot(400,700).
5. pot(300,300). pot(100,700).
6. pot(0,300). pot(100,700).
7. pot(100,300). pot(0,700).
8. pot(100,300). pot(700,700).
9. pot(300,300). pot(500,700).