現在の位置
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).